Add option witness.invariant.all-locals to only print locals definitely in scope

src/cdomain/value/domains/invariantCil.ml

@@ -21,7 +21,11 @@ let exp_replace_original_name e =
 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 *)
-  | Some fd -> CilType.Fundec.equal fd scope
+  | 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
 
 class exp_is_in_scope_visitor (scope: fundec) (acc: bool ref) = object
   inherit nopCilVisitor

src/config/options.schema.json

@@ -2450,6 +2450,12 @@
                 "RETURN"
               ]
             },
+            "all-locals": {
+              "title": "witness.invariant.all-locals",
+              "description": "Emit invariants for local variables under the assumption they are always in scope within their function.",
+              "type": "boolean",
+              "default": true
+            },
             "goblint": {
               "title": "witness.invariant.goblint",
               "description": "Emit non-standard Goblint-specific invariants. Currently array invariants with all_index offsets.",

src/maingoblint.ml

@@ -144,6 +144,7 @@ let check_arguments () =
   if get_bool "incremental.restart.sided.enabled" && get_string_list "incremental.restart.list" <> [] then warn "Passing a non-empty list to incremental.restart.list (manual restarting) while incremental.restart.sided.enabled (automatic restarting) is activated.";
   if get_bool "ana.autotune.enabled" && get_bool "incremental.load" then (set_bool "ana.autotune.enabled" false; warn "ana.autotune.enabled implicitly disabled by incremental.load");
   if get_bool "exp.basic-blocks" && not (get_bool "justcil") && List.mem "assert" @@ get_string_list "trans.activated" then (set_bool "exp.basic-blocks" false; warn "The option exp.basic-blocks implicitely disabled by activating the \"assert\" tranformation.");
+  if (not @@ get_bool "witness.invariant.all-locals") && (not @@ get_bool "cil.addNestedScopeAttr") then (set_bool "cil.addNestedScopeAttr" true; warn "Disabling witness.invariant.all-locals implicitly enables cil.addNestedScopeAttr.");
   if List.mem "remove_dead_code" @@ get_string_list "trans.activated" then (
     (* 'assert' transform happens before 'remove_dead_code' transform *)
     ignore @@ List.fold_left

tests/regression/56-witness/08-witness-all-locals.c

@@ -0,0 +1,10 @@
+// CRAM PARAM: --enable witness.yaml.enabled --set witness.yaml.entry-types '["location_invariant"]' --disable witness.invariant.all-locals
+int main() {
+  int x;
+  x = 5;
+  {
+    int y;
+    y = 10;
+  }
+  return 0;
+}

tests/regression/56-witness/08-witness-all-locals.t

@@ -0,0 +1,22 @@
+  $ goblint --enable witness.yaml.enabled --set witness.yaml.entry-types '["location_invariant"]' --enable witness.invariant.all-locals 08-witness-all-locals.c
+  [Info][Deadcode] Logical lines of code (LLoC) summary:
+    live: 4
+    dead: 0
+    total lines: 4
+  [Info][Witness] witness generation summary:
+    total generation entries: 3
+
+TODO: check witness.yml content with yamlWitnessStrip
+
+Fewer entries are emitted if locals from nested block scopes are excluded:
+
+  $ goblint --enable witness.yaml.enabled --set witness.yaml.entry-types '["location_invariant"]' --disable witness.invariant.all-locals 08-witness-all-locals.c
+  [Warning] Disabling witness.invariant.all-locals implicitly enables cil.addNestedScopeAttr.
+  [Info][Deadcode] Logical lines of code (LLoC) summary:
+    live: 4
+    dead: 0
+    total lines: 4
+  [Info][Witness] witness generation summary:
+    total generation entries: 2
+
+TODO: check witness.yml content with yamlWitnessStrip

tests/regression/56-witness/dune

@@ -0,0 +1,2 @@
+(cram
+ (deps (glob_files *.c) (glob_files ??-*.yml)))