Fixes & Desiderata

src/cdomains/apron/sharedFunctions.apron.ml

@@ -80,38 +80,49 @@ struct
       | _ -> None (* for other exception *)
     )
 
-  (** This still tries to establish bounds via Bounds.bound_texpr, which may be more precise in case ana.int.interval
-      is disabled and the relational analysis manages to evaluate a value to an interval, which can then not be represented
-      as the result of an EvalInt query. This is a workaround and works as long as only one relational domain is used.
-      With multiple domains and disabled interval domain, the queries will not be able to exchange interval information,
-      and each analysis will only be able to establish constant bounds, but only its own interval bounds and not interval bounds
-      established by other analyses.*)
-  let overflow_handling no_ov ik env expr d exp =
-    match Cilfacade.get_ikind_exp exp with
-    | exception Invalid_argument e ->  raise (Unsupported_CilExp Exp_not_supported)       (* expression is not an integer expression, i.e. float *)
-    | ik ->
-      if IntDomain.should_wrap ik || not (Lazy.force no_ov) then (
-        let (type_min, type_max) = IntDomain.Size.range ik in
-        let texpr1 = Texpr1.of_expr env expr in
-        match Bounds.bound_texpr d texpr1 with
-        | Some min, Some max when Z.compare type_min min <= 0 && Z.compare max type_max <= 0 ->
-          ()
-        | min_opt, max_opt ->
-          if M.tracing then M.trace "apron" "may overflow: %a (%a, %a)\n" CilType.Exp.pretty exp (Pretty.docOpt (IntOps.BigIntOps.pretty ())) min_opt (Pretty.docOpt (IntOps.BigIntOps.pretty ())) max_opt;
-          raise (Unsupported_CilExp Overflow)
-      )
 
   let texpr1_expr_of_cil_exp (ask:Queries.ask) d env exp no_ov =
     let conv exp  =
+      let module IDT = IntDomain.IntDomTuple in
       let query e ik =
         let res =
         match ask.f (EvalInt e) with
         | `Bot -> raise (Unsupported_CilExp Exp_not_supported) (* This should never happen according to Michael Schwarz *)
-        | `Top -> IntDomain.IntDomTuple.top_of ik
-        | `Lifted x -> x (* Cast should be unnecessary because it should be taken care of by EvalInt. *) in
-        if M.tracing then M.trace "relation" "texpr1_expr_of_cil_exp/query: %a -> %a\n" d_plainexp e IntDomain.IntDomTuple.pretty res;
+        | `Top ->
+          IDT.top_of ik
+        | `Lifted x -> x (* Cast should be unnecessary because it should be taken care of by EvalInt. *)
+        in
+        if M.tracing then M.trace "relation" "texpr1_expr_of_cil_exp/query: %a -> %a\n" d_plainexp e IDT.pretty res;
         res
       in
+      (** This still tries to establish bounds via Bounds.bound_texpr, which may be more precise in case ana.int.interval
+          is disabled and the relational analysis manages to evaluate a value to an interval, which can then not be represented
+          as the result of an EvalInt query. This is a workaround and works as long as only one relational domain is used.
+          With multiple domains and disabled interval domain, the queries will not be able to exchange interval information,
+          and each analysis will only be able to establish constant bounds, but only its own interval bounds and not interval bounds
+          established by other analyses.*)
+      let overflow_handling no_ov ik env expr d exp =
+        match Cilfacade.get_ikind_exp exp with
+        | exception Invalid_argument e ->  raise (Unsupported_CilExp Exp_not_supported)       (* expression is not an integer expression, i.e. float *)
+        | ik ->
+          if IntDomain.should_wrap ik || not (Lazy.force no_ov) then (
+            let (type_min, type_max) = IntDomain.Size.range ik in
+            let texpr1 = Texpr1.of_expr env expr in
+            match Bounds.bound_texpr d texpr1 with
+            | Some min, Some max when Z.compare type_min min <= 0 && Z.compare max type_max <= 0 ->
+              ()
+            | min_opt, max_opt ->
+              (* Bounds did not manage to bound this, so we ask a query *)
+              let i = query exp ik in
+              match IDT.minimal i, IDT.maximal i with
+              | Some min, Some max when not (IDT.is_top_of ik (IDT.of_interval ~suppress_ovwarn:true ik (min, max))) ->
+                (* Checks that the interval information is not interval top. This works as we do not have dedicated wrap-around handling *)
+                ()
+              | _ ->
+                if M.tracing then M.trace "relation" "may overflow: %a (%a, %a)\n" CilType.Exp.pretty exp (Pretty.docOpt (IntOps.BigIntOps.pretty ())) min_opt (Pretty.docOpt (IntOps.BigIntOps.pretty ())) max_opt;
+                raise (Unsupported_CilExp Overflow)
+          )
+      in
       (* recurse without env and ask arguments *)
       let rec texpr1_expr_of_cil_exp = function
         | Lval (Var v, NoOffset) when Tracked.varinfo_tracked v ->
@@ -140,8 +151,8 @@ struct
               let simplify e =
                 let ikind = try (Cilfacade.get_ikind_exp e) with Invalid_argument _ -> raise (Unsupported_CilExp Exp_not_supported)   in
                 let simp = query e ikind in
-                let const = IntDomain.IntDomTuple.to_int @@ IntDomain.IntDomTuple.cast_to ikind simp in
-                if M.tracing then M.trace "relation" "texpr1_expr_of_cil_exp/simplify: %a -> %a\n" d_plainexp e IntDomain.IntDomTuple.pretty simp;
+                let const = IDT.to_int @@ IDT.cast_to ikind simp in
+                if M.tracing then M.trace "relation" "texpr1_expr_of_cil_exp/simplify: %a -> %a\n" d_plainexp e IDT.pretty simp;
                 BatOption.map_default (fun c -> Const (CInt (c, ikind, None))) e const
               in
               let texpr1 e = texpr1_expr_of_cil_exp (simplify e) in
@@ -162,14 +173,14 @@ struct
                     (* try to evaluate e by EvalInt Query *)
                     let res = try (query e @@ Cilfacade.get_ikind_exp e) with Invalid_argument _ -> raise (Unsupported_CilExp Exp_not_supported)  in
                     (* convert response to a constant *)
-                    let const = IntDomain.IntDomTuple.to_int @@ IntDomain.IntDomTuple.cast_to t_ik res in
+                    let const = IDT.to_int @@ IDT.cast_to t_ik res in
                     match const with
                     | Some c -> Cst (Coeff.s_of_mpqf (Mpqf.of_mpz (Z_mlgmpidl.mpz_of_z c))) (* Got a constant value -> use it straight away *)
                     (* I gotten top, we can not guarantee injectivity *)
-                    | None -> if IntDomain.IntDomTuple.is_top_of t_ik res then raise (Unsupported_CilExp (Cast_not_injective t))
+                    | None -> if IDT.is_top_of t_ik res then raise (Unsupported_CilExp (Cast_not_injective t))
                       else ( (* Got a ranged value different from top, so let's check bounds manually *)
                         let (ik_min, ik_max) = IntDomain.Size.range t_ik in
-                        match IntDomain.IntDomTuple.minimal res, IntDomain.IntDomTuple.maximal res with
+                        match IDT.minimal res, IDT.maximal res with
                         | Some min, Some max when min >= ik_min && max <= ik_max -> texpr1_expr_of_cil_exp e
                         | _ -> raise (Unsupported_CilExp (Cast_not_injective t)))
                     | exception Cilfacade.TypeOfError _ (* typeOf inner e, not outer exp *)

tests/regression/77-lin2vareq/31-unsigned-non-const.c

@@ -0,0 +1,16 @@
+// SKIP PARAM: --set ana.activated[+] lin2vareq --enable ana.int.interval
+#include <goblint.h>
+
+int main(void) {
+  int top;
+  unsigned int i = 0;
+  unsigned int j;
+
+  if(top) {
+    i = 1;
+  }
+
+  j = i+1;
+
+  __goblint_check(j == i+1);
+}

tests/regression/77-lin2vareq/32-ahooga.c

@@ -0,0 +1,18 @@
+// SKIP PARAM: --set ana.activated[+] lin2vareq --enable ana.int.interval
+#include <goblint.h>
+#include <limits.h>
+
+int main(void) {
+  int top;
+  unsigned int i = 2;
+  unsigned int j;
+
+  if(top) {
+    i = 3;
+  }
+
+  j = i + UINT_MAX;
+
+  // Holds in the concrete
+  __goblint_check(j == i-1); //UNKNOWN
+}