Merge pull request #1506 from goblint/apron-compare-fix

Fix Apron `compare` function usage

dune-project

@@ -67,7 +67,7 @@ Goblint includes analyses for assertions, overflows, deadlocks, etc and can be e
     conf-gcc ; ensures opam-repository CI installs real gcc from homebrew on MacOS
   )
   (depopts
-    apron
+    (apron (>= v0.9.15))
     z3
   )
   (conflicts

goblint.opam

@@ -66,7 +66,10 @@ depends: [
   "benchmark" {with-test}
   "conf-gcc"
 ]
-depopts: ["apron" "z3"]
+depopts: [
+  "apron" {>= "v0.9.15"}
+  "z3"
+]
 conflicts: [
   "result" {< "1.5"}
   "ez-conf-lib" {= "1"}

goblint.opam.locked

@@ -23,7 +23,7 @@ doc: "https://goblint.readthedocs.io/en/latest/"
 bug-reports: "https://github.com/goblint/analyzer/issues"
 depends: [
   "angstrom" {= "0.15.0"}
-  "apron" {= "v0.9.14~beta.2"}
+  "apron" {= "v0.9.15"}
   "arg-complete" {= "0.1.0"}
   "astring" {= "0.8.5"}
   "base-bigarray" {= "base"}

src/cdomains/apron/affineEqualityDomain.apron.ml

@@ -257,7 +257,7 @@ struct
   let meet t1 t2 = timing_wrap "meet" (meet t1) t2
 
   let leq t1 t2 =
-    let env_comp = Environment.compare t1.env t2.env in (* Apron's Environment.compare has defined return values. *)
+    let env_comp = Environment.cmp t1.env t2.env in (* Apron's Environment.cmp has defined return values. *)
     if env_comp = -2 || env_comp > 0 then
       (* -2:  environments are not compatible (a variable has different types in the 2 environements *)
       (* -1: if env1 is a subset of env2,  (OK)  *)
@@ -334,7 +334,7 @@ struct
     else
       match Option.get a.d, Option.get b.d with
       | x, y when is_top_env a || is_top_env b -> {d = Some (Matrix.empty ()); env = Environment.lce a.env b.env}
-      | x, y when (Environment.compare a.env b.env <> 0) ->
+      | x, y when (Environment.cmp a.env b.env <> 0) ->
         let sup_env = Environment.lce a.env b.env in
         let mod_x = dim_add (Environment.dimchange a.env sup_env) x in
         let mod_y = dim_add (Environment.dimchange b.env sup_env) y in

src/cdomains/apron/apronDomain.apron.ml

@@ -451,9 +451,9 @@ struct
   let hash (x:t) =
     A.hash Man.mgr x
 
-  let compare (x:t) y: int =
-    (* there is no A.compare, but polymorphic compare should delegate to Abstract0 and Environment compare's implemented in Apron's C *)
-    Stdlib.compare x y
+  let compare (x: t) (y: t): int =
+    failwith "Apron.Abstract1 doesn't have total order" (* https://github.com/antoinemine/apron/issues/99 *)
+
   let printXml f x = BatPrintf.fprintf f "<value>\n<map>\n<key>\nconstraints\n</key>\n<value>\n%s</value>\n<key>\nenv\n</key>\n<value>\n%s</value>\n</map>\n</value>\n" (XmlUtil.escape (Format.asprintf "%a" A.print x)) (XmlUtil.escape (Format.asprintf "%a" (Environment.print: Format.formatter -> Environment.t -> unit) (A.env x)))
 
   let to_yojson (x: t) =

src/cdomains/apron/gobApron.apron.ml

@@ -19,7 +19,9 @@ struct
   include Lincons1
 
   let show = Format.asprintf "%a" print
-  let compare x y = String.compare (show x) (show y) (* HACK *)
+  let compare x y =
+    (* TODO: implement proper total Lincons1 order *)
+    String.compare (show x) (show y) (* HACK *)
 
   let num_vars x =
     (* Apron.Linexpr0.get_size returns some internal nonsense, so we count ourselves. *)
@@ -49,6 +51,10 @@ module Environment =
 struct
   include Environment
 
+  let compare (x: t) (y: t): int =
+    (* TODO: implement total Environment order in OCaml *)
+    failwith "Apron.Environment doesn't have total order" (* https://github.com/antoinemine/apron/issues/99 *)
+
   let ivars_only env =
     let ivs, fvs = Environment.vars env in
     assert (Array.length fvs = 0); (* shouldn't ever contain floats *)

src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml

@@ -459,7 +459,7 @@ struct
   let meet t1 t2 = timing_wrap "meet" (meet t1) t2
 
   let leq t1 t2 =
-    let env_comp = Environment.compare t1.env t2.env in (* Apron's Environment.compare has defined return values. *)
+    let env_comp = Environment.cmp t1.env t2.env in (* Apron's Environment.cmp has defined return values. *)
     let implies ts i (var, offs, divi) =
       let tuple_cmp = Tuple3.eq (Option.eq ~eq:(Tuple2.eq (Z.equal) (Int.equal))) (Z.equal) (Z.equal) in
       match var with
@@ -543,7 +543,7 @@ struct
     | Some x, Some y when is_top a || is_top b ->
       let new_env = Environment.lce a.env b.env in
       top_of new_env
-    | Some x, Some y when (Environment.compare a.env b.env <> 0) ->
+    | Some x, Some y when (Environment.cmp a.env b.env <> 0) ->
       let sup_env = Environment.lce a.env b.env in
       let mod_x = dim_add (Environment.dimchange a.env sup_env) x in
       let mod_y = dim_add (Environment.dimchange b.env sup_env) y in