Merge pull request #1493 from goblint/issue_1328

make cil_exp_of_linexpr1 work with fractional expressions

src/cdomains/apron/sharedFunctions.apron.ml

@@ -6,7 +6,8 @@ open GobApron
 
 module M = Messages
 
-let int_of_scalar ?round (scalar: Scalar.t) =
+
+let int_of_scalar ?(scalewith=Z.one) ?round (scalar: Scalar.t) =
   if Scalar.is_infty scalar <> 0 then (* infinity means unbounded *)
     None
   else
@@ -20,18 +21,21 @@ let int_of_scalar ?round (scalar: Scalar.t) =
         | None when Stdlib.Float.is_integer f -> Some f
         | None -> None
       in
-      Z.of_float f
+      Z.(of_float f * scalewith)
     | Mpqf scalar -> (* octMPQ, boxMPQ, polkaMPQ *)
       let n = Mpqf.get_num scalar in
       let d = Mpqf.get_den scalar in
+      let scale = Z_mlgmpidl.mpz_of_z scalewith in
       let+ z =
         if Mpzf.cmp_int d 1 = 0 then (* exact integer (denominator 1) *)
-          Some n
+          Some (Mpzf.mul scale n)
         else
           begin match round with
-            | Some `Floor -> Some (Mpzf.fdiv_q n d) (* floor division *)
-            | Some `Ceil -> Some (Mpzf.cdiv_q n d) (* ceiling division *)
-            | None -> None
+            | Some `Floor -> Some (Mpzf.mul scale (Mpzf.fdiv_q n d)) (* floor division *)
+            | Some `Ceil ->  Some (Mpzf.mul scale (Mpzf.cdiv_q n d)) (* ceiling division *)
+            | None -> let product = Mpzf.mul scale n in if Mpz.divisible_p product d then
+                Some (Mpzf.divexact product d) (* scale, preferably with common denominator *)
+              else None
           end
       in
       Z_mlgmpidl.z_of_mpzf z
@@ -245,11 +249,11 @@ module CilOfApron (V: SV) =
 struct
   exception Unsupported_Linexpr1
 
-  let cil_exp_of_linexpr1 (linexpr1:Linexpr1.t) =
+  let cil_exp_of_linexpr1 ?scalewith (linexpr1:Linexpr1.t) =
     let longlong = TInt(ILongLong,[]) in
     let coeff_to_const consider_flip (c:Coeff.union_5) = match c with
       | Scalar c ->
-        (match int_of_scalar c with
+        (match int_of_scalar ?scalewith c with
          | Some i ->
            let ci,truncation = truncateCilint ILongLong i in
            if truncation = NoTruncation then
@@ -285,11 +289,38 @@ struct
     !expr
 
 
+  let lcm_den linexpr1 =
+    let exception UnsupportedScalar 
+    in
+    let frac_of_scalar scalar =
+      if Scalar.is_infty scalar <> 0 then (* infinity means unbounded *)
+        None
+      else match scalar with
+        | Float f -> if Stdlib.Float.is_integer f then Some (Q.of_float f) else None
+        | Mpqf f -> Some (Z_mlgmpidl.q_of_mpqf f)
+        | _ -> raise UnsupportedScalar
+    in
+    let extract_den (c:Coeff.union_5) =
+      match c with
+      | Scalar c -> BatOption.map Q.den (frac_of_scalar c)
+      | _ -> None
+    in
+    let lcm_denom = ref (BatOption.default Z.one (extract_den (Linexpr1.get_cst linexpr1))) in
+    let lcm_coeff (c:Coeff.union_5) _ =
+      match (extract_den c) with
+      | Some z -> lcm_denom := Z.lcm z !lcm_denom
+      | _      -> ()
+    in
+    try
+      Linexpr1.iter lcm_coeff linexpr1; !lcm_denom
+    with UnsupportedScalar -> Z.one
+
   let cil_exp_of_lincons1 (lincons1:Lincons1.t) =
     let zero = Cil.kinteger ILongLong 0 in
     try
       let linexpr1 = Lincons1.get_linexpr1 lincons1 in
-      let cilexp = cil_exp_of_linexpr1 linexpr1 in
+      let common_denominator = lcm_den linexpr1 in
+      let cilexp = cil_exp_of_linexpr1 ~scalewith:common_denominator linexpr1 in
       match Lincons1.get_typ lincons1 with
       | EQ -> Some (Cil.constFold false @@ BinOp(Eq, cilexp, zero, TInt(IInt,[])))
       | SUPEQ -> Some (Cil.constFold false @@ BinOp(Ge, cilexp, zero, TInt(IInt,[])))