Implement proper naïve unassume in var_eq

src/analyses/varEq.ml

@@ -378,8 +378,8 @@ struct
     && interesting rv
     && is_global_var ask rv = Some false
     && (isIntegralType lvt || isPointerType lvt)
-    then D.add_eq (rv,Lval lv) (remove ask lv st)
-    else remove ask lv st
+    then D.add_eq (rv,Lval lv) st
+    else st
   (*    in
         match rv with
         | Lval rlval -> begin
@@ -393,6 +393,11 @@ struct
             end
         | _ -> st
   *)
+
+  (* removes all equalities with lval and then tries to make a new one: lval=rval *)
+  let assign_eq ask lv rv st =
+    add_eq ask lv rv (remove ask lv st)
+
   (* Give the set of reachables from argument. *)
   let reachables ~deep (ask: Queries.ask) es =
     let reachable acc e =
@@ -406,18 +411,39 @@ struct
   (* Probably ok as is. *)
   let body man f = man.local
 
-  (* Branch could be improved to set invariants like base tries to do. *)
-  let branch man exp tv = man.local
+  (* Assume equalities from expression. *)
+  let rec assume ask exp st =
+    match exp with
+    | BinOp (Eq, e1, e2, t) ->
+      (* Pointer equalities have casts on both sides. Strip them to get to the actual Lval. *)
+      begin match stripCasts e1, stripCasts e2 with
+        | Lval lval, exp
+        | exp, Lval lval ->
+          add_eq ask lval exp st
+        | _, _ ->
+          st
+      end
+    | BinOp (LAnd, e1, e2, _) -> (* Handle for unassume. *)
+      assume ask e2 (assume ask e1 st)
+    | BinOp (LOr, e1, e2, _) -> (* Handle for unassume. *)
+      D.join (assume ask e1 st) (assume ask e2 st)
+    | _ -> st
+
+  let branch man exp tv =
+    if tv then
+      assume (Analyses.ask_of_man man) exp man.local
+    else
+      (* TODO: support != from false branch. *)
+      man.local
 
   (* Just remove things that go out of scope. *)
   let return man exp fundec  =
     let rm acc v = remove (Analyses.ask_of_man man) (Cil.var v) acc in
     List.fold_left rm man.local ([email protected])
 
-  (* removes all equalities with lval and then tries to make a new one: lval=rval *)
   let assign man (lval:lval) (rval:exp) : D.t  =
     let rval = constFold true (stripCasts rval) in
-    add_eq (Analyses.ask_of_man man) lval rval man.local
+    assign_eq (Analyses.ask_of_man man) lval rval man.local
 
   (* First assign arguments to parameters. Then join it with reachables, to get
      rid of equalities that are not reachable. *)
@@ -428,8 +454,7 @@ struct
       | _ -> r
     in
     let assign_one_param st v exp =
-      let rm = remove (Analyses.ask_of_man man) (Cil.var v) st in
-      add_eq (Analyses.ask_of_man man) (Cil.var v) exp rm
+      assign_eq (Analyses.ask_of_man man) (Cil.var v) exp st
     in
     let nst =
       try fold_left2 assign_one_param man.local f.sformals args
@@ -587,6 +612,8 @@ struct
       |> List.fold_left (fun st lv ->
           remove (Analyses.ask_of_man man) lv st
         ) man.local
+      |> assume (Analyses.ask_of_man man) exp (* Still naive unassume to not lose precision unassuming equalities which we know. *)
+      |> D.join man.local
     | Events.Escape vars ->
       if EscapeDomain.EscapedVars.is_top vars then
         D.top ()

tests/regression/06-symbeq/53-var_eq-branch.c

@@ -0,0 +1,9 @@
+// PARAM: --set ana.activated[+] var_eq
+#include <goblint.h>
+
+int main() {
+  int i, j;
+  if (i == j)
+    __goblint_check(i == j);
+  return 0;
+}

tests/regression/56-witness/74-var_eq-unassume-interval.c

@@ -0,0 +1,11 @@
+// SKIP PARAM: --set ana.activated[+] var_eq --enable ana.int.interval --set ana.activated[+] unassume --set witness.yaml.unassume 74-var_eq-unassume-interval.yml
+#include <assert.h>
+
+int main() {
+  int i = 0;
+  while (i < 100) { // TODO: location invariant before loop doesn't work anymore
+    i++;
+  }
+  assert(i == 100);
+  return 0;
+}

tests/regression/56-witness/74-var_eq-unassume-interval.t

@@ -0,0 +1,31 @@
+All of these disable def_exc to avoid it forcing extra widening iterations in its range.
+This matches the var_eq extra widening iteration, so we couldn't test if var_eq unassumes at all.
+
+## From scratch
+
+  $ goblint --set ana.activated[+] var_eq --disable ana.int.def_exc --enable ana.int.interval 74-var_eq-unassume-interval.c
+  [Success][Assert] Assertion "i == 100" will succeed (74-var_eq-unassume-interval.c:9:3-9:29)
+  [Info][Deadcode] Logical lines of code (LLoC) summary:
+    live: 6
+    dead: 0
+    total lines: 6
+
+Easiest to run again to get evals.
+  $ goblint --set ana.activated[+] var_eq --disable ana.int.def_exc --enable ana.int.interval 74-var_eq-unassume-interval.c -v 2>&1 | grep 'evals'
+  [Info] vars = 9    evals = 12    narrow_reuses = 1
+
+## Unassume
+
+  $ goblint --set ana.activated[+] var_eq --disable ana.int.def_exc --enable ana.int.interval --set ana.activated[+] unassume --set witness.yaml.unassume 74-var_eq-unassume-interval.yml 74-var_eq-unassume-interval.c
+  [Info][Witness] unassume invariant: (long long )i >= 0LL && 100LL - (long long )i >= 0LL (74-var_eq-unassume-interval.c:5:7-5:12)
+  [Info][Witness] unassume invariant: (long long )i >= 0LL && 100LL - (long long )i >= 0LL (74-var_eq-unassume-interval.c:7:5-7:8)
+  [Success][Assert] Assertion "i == 100" will succeed (74-var_eq-unassume-interval.c:9:3-9:29)
+  [Info][Deadcode] Logical lines of code (LLoC) summary:
+    live: 6
+    dead: 0
+    total lines: 6
+
+Evals less than from scratch.
+If var_eq didn't do any unassume (and kept i == 0 in first iteration), then there would be extra widening iteration and 10 evals instead.
+  $ goblint --set ana.activated[+] var_eq --disable ana.int.def_exc --enable ana.int.interval --set ana.activated[+] unassume --set witness.yaml.unassume 74-var_eq-unassume-interval.yml 74-var_eq-unassume-interval.c -v 2>&1 | grep 'evals'
+  [Info] vars = 9    evals = 8    narrow_reuses = 1

tests/regression/56-witness/74-var_eq-unassume-interval.yml

@@ -0,0 +1,37 @@
+- entry_type: invariant_set
+  metadata:
+    format_version: "2.0"
+    uuid: 0a72f7b3-7826-4f68-bc7b-25425e95946e
+    creation_time: 2022-07-26T09:11:03Z
+    producer:
+      name: Goblint
+      version: heads/yaml-witness-unassume-0-g48503c690-dirty
+      command_line: '''./goblint'' ''--enable'' ''dbg.debug'' ''--enable'' ''dbg.regression''
+        ''--html'' ''--set'' ''ana.activated[+]'' ''apron'' ''--enable'' ''witness.yaml.enabled''
+        ''74-var_eq-unassume-interval.c'''
+    task:
+      input_files:
+      - 74-var_eq-unassume-interval.c
+      input_file_hashes:
+        74-var_eq-unassume-interval.c: 71e40ed99b5217343d0831e293e7207e5bd30ce53f6ab73f0c1ef6ced1afcc60
+      data_model: LP64
+      language: C
+  content:
+  - invariant:
+      type: loop_invariant
+      location:
+        file_name: 74-var_eq-unassume-interval.c
+        line: 6
+        column: 3
+        function: main
+      value: 100LL - (long long )i >= 0LL
+      format: c_expression
+  - invariant:
+      type: loop_invariant
+      location:
+        file_name: 74-var_eq-unassume-interval.c
+        line: 6
+        column: 3
+        function: main
+      value: (long long )i >= 0LL
+      format: c_expression

tests/regression/56-witness/75-var_eq-unassume-equal.c

@@ -0,0 +1,9 @@
+// PARAM: --set ana.activated[+] var_eq --set ana.activated[+] unassume --set witness.yaml.unassume 75-var_eq-unassume-equal.yml
+#include <goblint.h>
+
+int main() {
+  int i, j;
+  i = j;
+  __goblint_check(i == j); // var_eq unassume should keep i == j by assuming it in naive unassume
+  return 0;
+}

tests/regression/56-witness/75-var_eq-unassume-equal.yml

@@ -0,0 +1,25 @@
+- entry_type: invariant_set
+  metadata:
+    format_version: "2.0"
+    uuid: 828f8b0f-590b-4180-bef1-d2b18cc240e7
+    creation_time: 2025-10-24T11:09:00Z
+    producer:
+      name: Simmo Saan
+      version: n/a
+    task:
+      input_files:
+      - 75-var_eq-unassume-equal.c
+      input_file_hashes:
+        75-var_eq-unassume-equal.c: a1dbab3d2dc60945ace118bcacd88e4d448ddb3aaa5e9aebe3d0872266256f89
+      data_model: LP64
+      language: C
+  content:
+  - invariant:
+      type: location_invariant
+      location:
+        file_name: 75-var_eq-unassume-equal.c
+        line: 7
+        column: 3
+        function: main
+      value: i == j
+      format: c_expression