Merge pull request #1387 from goblint/issue-1373

Fix test for relational unassume with strengthening

src/analyses/apron/relationAnalysis.apron.ml

@@ -722,7 +722,9 @@ struct
       in
       let rel = RD.remove_vars st.rel (List.map RV.local (VH.values v_ins |> List.of_enum)) in (* remove temporary g#in-s *)
 
+      if M.tracing then M.traceli "apron" "unassume join\n";
       let st = D.join ctx.local {st with rel} in (* (strengthening) join *)
+      if M.tracing then M.traceu "apron" "unassume join\n";
       M.info ~category:Witness "relation unassumed invariant: %a" d_exp e_orig;
       st
     | _ ->

src/cdomains/apron/apronDomain.apron.ml

@@ -639,14 +639,21 @@ struct
       (* Whether [con1] contains a var in [env]. *)
       let env_exists_mem_con1 env con1 =
         try
-          Lincons1.iter (fun _ var ->
-              if Environment.mem_var env var then
-                raise Not_found
+          Lincons1.iter (fun coeff var ->
+              (* Lincons1 from polyhedra may contain variable with zero coefficient.
+                 These are silently not printed! *)
+              if not (Coeff.is_zero coeff) && Environment.mem_var env var then
+                raise Stdlib.Exit (* found *)
             ) con1;
           false
-        with Not_found ->
+        with Stdlib.Exit -> (* found *)
           true
       in
+      let env_exists_mem_con1 env con1 =
+        let r = env_exists_mem_con1 env con1 in
+        if M.tracing then M.trace "apron" "env_exists_mem_con1 %s %s -> %B\n" (Format.asprintf "%a" (Environment.print: Format.formatter -> Environment.t -> unit) env) (Lincons1.show con1) r;
+        r
+      in
       (* Heuristically reorder constraints to pass 36/12 with singlethreaded->multithreaded mode switching. *)
       (* Put those constraints which strictly are in one argument's env first, to (hopefully) ensure they remain. *)
       let (x_cons1_some_y, x_cons1_only_x) = Array.partition (env_exists_mem_con1 y_env) x_cons1 in

tests/regression/56-witness/25-apron-unassume-strengthening.c

@@ -1,13 +1,22 @@
-// SKIP PARAM: --set ana.activated[+] apron --set ana.activated[+] unassume --set witness.yaml.unassume 25-apron-unassume-strengthening.yml --enable ana.apron.strengthening --set sem.int.signed_overflow assume_none
+// SKIP PARAM: --set ana.activated[+] apron --set ana.activated[+] unassume --set witness.yaml.unassume 25-apron-unassume-strengthening.yml --enable ana.apron.strengthening --set sem.int.signed_overflow assume_none --set ana.apron.domain octagon
 #include <goblint.h>
 
 int main() {
   int x, y;
   x = 0;
-  if (x < y) {
+  if (x <= y) {
     __goblint_check(x == 0); // UNKNOWN (intentional by unassume)
     __goblint_check(x >= 0);
-    __goblint_check(x < y); // TODO: https://github.com/goblint/analyzer/issues/1373
+    __goblint_check(x <= y);
+  }
+
+  // With type bounds we have y <= 2147483647.
+  if (x < y) { // Assuming this implies x <= 2147483646 in closure.
+    // Unassuming 0 <= x actually unassumes 0 <= x <= 2147483647.
+    // Thus, strengthening cannot add x < y back.
+    __goblint_check(x == 0); // UNKNOWN (intentional by unassume)
+    __goblint_check(x >= 0);
+    __goblint_check(x < y); // TODO? Used to work without type bounds: https://github.com/goblint/analyzer/issues/1373.
   }
   return 0;
 }

tests/regression/56-witness/25-apron-unassume-strengthening.yml

@@ -23,3 +23,28 @@
     string: x >= 0
     type: assertion
     format: C
+- entry_type: location_invariant
+  metadata:
+    format_version: "0.1"
+    uuid: dec4db01-03ed-47dd-ae55-c84f8dcd51ed
+    creation_time: 2022-09-13T11:38:16Z
+    producer:
+      name: Simmo Saan
+      version: n/a
+    task:
+      input_files:
+      - 25-apron-unassume-strengthening.c
+      input_file_hashes:
+        25-apron-unassume-strengthening.c: b2a50e3b423ade600ec2de58fa8ace6ec9a08b85fdc016cbdb7fbe9a3ba80d83
+      data_model: LP64
+      language: C
+  location:
+    file_name: 25-apron-unassume-strengthening.c
+    file_hash: b2a50e3b423ade600ec2de58fa8ace6ec9a08b85fdc016cbdb7fbe9a3ba80d83
+    line: 17
+    column: 4
+    function: main
+  location_invariant:
+    string: x >= 0
+    type: assertion
+    format: C