Merge pull request #1818 from goblint/issue-1722

Fix some questionable invariants in SV-COMP 2025 witnesses

Author: sim642

src/analyses/varEq.ml

@@ -17,12 +17,16 @@ struct
   struct
     include PartitionDomain.ExpPartitions
 
+    let is_str_constant = function
+      | Const (CStr _ | CWStr _) -> true
+      | _ -> false
+
     let invariant ~scope ss =
       fold (fun s a ->
           if B.mem MyCFG.unknown_exp s then
             a
           else (
-            let s' = B.filter (fun x -> not (InvariantCil.exp_contains_tmp x) && InvariantCil.exp_is_in_scope scope x) s in
+            let s' = B.filter (fun x -> not (InvariantCil.exp_contains_tmp x) && InvariantCil.exp_is_in_scope scope x && not (is_str_constant x)) s in
             if B.cardinal s' >= 2 then (
               (* instead of returning quadratically many pairwise equalities from a cluster,
                  output linear number of equalities with just one expression *)

src/cdomain/value/domains/invariantCil.ml

@@ -26,15 +26,23 @@ let exp_deep_unroll_types =
   let visitor = new exp_deep_unroll_types_visitor in
   visitCilExpr visitor
 
+let var_may_be_shadowed scope vi =
+  let vi_original_name = Cilfacade.find_original_name vi in
+  let local_may_shadow local =
+    not (CilType.Varinfo.equal vi local) && (* exclude self-equality by vid because the original names would always equal *)
+      vi_original_name = Cilfacade.find_original_name local
+  in
+  List.exists local_may_shadow scope.sformals || List.exists local_may_shadow scope.slocals
 
 let var_is_in_scope scope vi =
   match Cilfacade.find_scope_fundec vi with
-  | None -> vi.vstorage <> Static (* CIL pulls static locals into globals, but they aren't syntactically in global scope *)
+  | None ->
+    vi.vstorage <> Static && (* CIL pulls static locals into globals, but they aren't syntactically in global scope *)
+      not (var_may_be_shadowed scope vi)
   | Some fd ->
-    if CilType.Fundec.equal fd scope then
-      GobConfig.get_bool "witness.invariant.all-locals" || (not @@ hasAttribute "goblint_cil_nested" vi.vattr)
-    else
-      false
+    CilType.Fundec.equal fd scope &&
+      (GobConfig.get_bool "witness.invariant.all-locals" || (not @@ hasAttribute "goblint_cil_nested" vi.vattr)) &&
+      not (var_may_be_shadowed scope vi) (* TODO: could distinguish non-nested and nested? *)
 
 class exp_is_in_scope_visitor (scope: fundec) (acc: bool ref) = object
   inherit nopCilVisitor

src/util/library/libraryFunctions.ml

@@ -647,6 +647,7 @@ let glibc_desc_list: (string * LibraryDesc.t) list = LibraryDsl.[
     ("ferror_unlocked", unknown [drop "stream" [r_deep; w_deep]]);
     ("fwrite_unlocked", unknown [drop "buffer" [r]; drop "size" []; drop "count" []; drop "stream" [r_deep; w_deep]]);
     ("clearerr_unlocked", unknown [drop "stream" [w]]); (* TODO: why only w? *)
+    ("__fpending", unknown [drop "stream" [r_deep]]);
     ("futimesat", unknown [drop "dirfd" []; drop "pathname" [r]; drop "times" [r]]);
     ("error", unknown ((drop "status" []) :: (drop "errnum" []) :: (drop "format" [r]) :: (VarArgs (drop' [r]))));
     ("warn", unknown (drop "format" [r] :: VarArgs (drop' [r])));

tests/regression/56-witness/72-var_eq-str-invariant.c

@@ -0,0 +1,5 @@
+// CRAM PARAM: --set ana.activated[+] var_eq
+int main() {
+  char text = "foobar";
+  return 0;
+}

tests/regression/56-witness/72-var_eq-str-invariant.t

@@ -0,0 +1,16 @@
+  $ goblint --set ana.activated[+] var_eq --enable witness.yaml.enabled --enable witness.invariant.other 72-var_eq-str-invariant.c
+  [Info][Deadcode] Logical lines of code (LLoC) summary:
+    live: 3
+    dead: 0
+    total lines: 3
+  [Info][Witness] witness generation summary:
+    location invariants: 0
+    loop invariants: 0
+    flow-insensitive invariants: 0
+    total generation entries: 1
+
+Should not contain invariant with string literal equality:
+
+  $ yamlWitnessStrip < witness.yml
+  - entry_type: invariant_set
+    content: []

tests/regression/56-witness/73-shadowing-invariant.c

@@ -0,0 +1,13 @@
+// CRAM PARAM: --set ana.activated[+] var_eq
+
+int foo = 1;
+
+int main() {
+  int foo = 2; // shadows global
+
+  int bar = 3;
+  {
+    int bar = 4; // shadows outer block
+    return 0;
+  }
+}

tests/regression/56-witness/73-shadowing-invariant.t

@@ -0,0 +1,71 @@
+  $ goblint --set ana.activated[+] var_eq --enable witness.yaml.enabled --enable witness.invariant.other 73-shadowing-invariant.c
+  [Info][Deadcode] Logical lines of code (LLoC) summary:
+    live: 5
+    dead: 0
+    total lines: 5
+  [Info][Witness] witness generation summary:
+    location invariants: 6
+    loop invariants: 0
+    flow-insensitive invariants: 0
+    total generation entries: 1
+
+Should not contain invariants containing shadowed variables.
+They can be wrong and contradicting.
+
+  $ yamlWitnessStrip < witness.yml
+  - entry_type: invariant_set
+    content:
+    - invariant:
+        type: location_invariant
+        location:
+          file_name: 73-shadowing-invariant.c
+          line: 8
+          column: 3
+          function: main
+        value: 2 == foo
+        format: c_expression
+    - invariant:
+        type: location_invariant
+        location:
+          file_name: 73-shadowing-invariant.c
+          line: 8
+          column: 3
+          function: main
+        value: foo == 2
+        format: c_expression
+    - invariant:
+        type: location_invariant
+        location:
+          file_name: 73-shadowing-invariant.c
+          line: 10
+          column: 5
+          function: main
+        value: 2 == foo
+        format: c_expression
+    - invariant:
+        type: location_invariant
+        location:
+          file_name: 73-shadowing-invariant.c
+          line: 10
+          column: 5
+          function: main
+        value: foo == 2
+        format: c_expression
+    - invariant:
+        type: location_invariant
+        location:
+          file_name: 73-shadowing-invariant.c
+          line: 11
+          column: 5
+          function: main
+        value: 2 == foo
+        format: c_expression
+    - invariant:
+        type: location_invariant
+        location:
+          file_name: 73-shadowing-invariant.c
+          line: 11
+          column: 5
+          function: main
+        value: foo == 2
+        format: c_expression