CONTRACTS: new method to detect static locals for contract instrumentation

regression/contracts/assigns_enforce_19/main.c

@@ -6,7 +6,9 @@ static int c = 0;
 int f() __CPROVER_assigns()
 {
   static int a = 0;
+  static int aa = 0;
   a++;
+  aa++;
   return a;
 }
 

regression/contracts/assigns_enforce_19/test.desc

@@ -1,18 +1,21 @@
 CORE
 main.c
 --enforce-contract f --enforce-contract g
-^\[f.assigns.\d+\] line 9 Check that a is assignable: SUCCESS$
-^\[g.assigns.\d+\] line 14 Check that b is valid: SUCCESS$
-^\[g.assigns.\d+\] line 16 Check that b is assignable: SUCCESS$
-^\[g.assigns.\d+\] line 17 Check that c is assignable: FAILURE$
-^\[g.assigns.\d+\] line 18 Check that \*points_to_b is assignable: SUCCESS$
-^\[g.assigns.\d+\] line 19 Check that \*points_to_c is assignable: FAILURE$
+^\[f.assigns.\d+\] line \d+ Check that a is assignable: SUCCESS$
+^\[f.assigns.\d+\] line \d+ Check that aa is assignable: SUCCESS$
+^\[g.assigns.\d+\] line \d+ Check that b is valid: SUCCESS$
+^\[g.assigns.\d+\] line \d+ Check that b is assignable: SUCCESS$
+^\[g.assigns.\d+\] line \d+ Check that c is assignable: FAILURE$
+^\[g.assigns.\d+\] line \d+ Check that \*points_to_b is assignable: SUCCESS$
+^\[g.assigns.\d+\] line \d+ Check that \*points_to_c is assignable: FAILURE$
 ^VERIFICATION FAILED$
 ^EXIT=10$
 ^SIGNAL=0$
 --
 --
 Checks whether contract enforcement works with (local and global) static variables.
 Local static variables should be part of the local write set.
+Shows that we detect using the source location  even when there is space 
+before the declaration and the actual start of the program.
 Global static variables should be included in the global write set,
 otherwise any assignment to it is invalid.

regression/contracts/assigns_enforce_detect_replaced_local_statics/main.c

@@ -0,0 +1,33 @@
+#include <assert.h>
+#include <stdbool.h>
+#include <stdlib.h>
+
+int baz() __CPROVER_requires(true) __CPROVER_ensures(true) __CPROVER_assigns()
+{
+  static int __local_static = 0;
+  __local_static = 0;
+
+  return __local_static;
+}
+
+int bar() __CPROVER_requires(true) __CPROVER_ensures(true) __CPROVER_assigns()
+{
+  static int __local_static_arr[2];
+  __local_static_arr[0] = 0;
+  __local_static_arr[1] = 0;
+
+  baz();
+  return __local_static_arr[0] | __local_static_arr[1];
+}
+
+void foo() __CPROVER_requires(true) __CPROVER_ensures(true) __CPROVER_assigns()
+{
+  bar();
+}
+
+int main()
+{
+  foo();
+  __CPROVER_assert(baz() == 0, "expecting FAILURE");
+  __CPROVER_assert(bar() == 0, "expecting FAILURE");
+}

regression/contracts/assigns_enforce_detect_replaced_local_statics/test.desc

@@ -0,0 +1,23 @@
+CORE
+main.c
+--replace-call-with-contract bar --replace-call-with-contract baz --enforce-contract foo _ --pointer-check
+^\[foo.assigns.\d+\] line \d+ Check that __local_static \(assigned by the contract of bar\) is assignable: SUCCESS$
+^\[foo.assigns.\d+\] line \d+ Check that __local_static_arr \(assigned by the contract of bar\) is assignable: SUCCESS$
+^\[main.assertion.\d+\] line \d+ expecting FAILURE: FAILURE$
+^\[main.assertion.\d+\] line \d+ expecting FAILURE: FAILURE$
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+This test checks that locally declared static variables are correctly detected 
+and tracked when function contract replacement is used.
+Here, baz declares a local static variable, 
+bar calls baz, and we replace the call to baz in bar.
+bar also declares a local static array variable.
+the call to bar is replaced by its contract in foo.
+We see that in foo, two assignments to these local statics are checked,
+showing that the replacement of bar in foo is modeled as nondet assignments.
+We also see that these assignments are succesfully checked against the empty
+assigns clause of foo, which shows that they are automatically propagated to 
+the assigns clause of foo as expected.

regression/contracts/loop_assigns_scoped_local_statics/main.c

@@ -0,0 +1,91 @@
+#include <assert.h>
+
+int j;
+
+int before_loop()
+{
+  static int __static_local;
+  __static_local = 0;
+  return __static_local;
+}
+
+int after_loop()
+{
+  static int __static_local;
+  __static_local = 0;
+  return __static_local;
+}
+
+int lowerbound()
+{
+  static int __static_local;
+  __static_local = 0;
+  return 0;
+}
+
+int upperbound()
+{
+  static int __static_local;
+  __static_local = 0;
+  return 10;
+}
+
+void incr(int *i)
+{
+  static int __static_local;
+  __static_local = 0;
+  (*i)++;
+}
+
+int body_1(int i)
+{
+  static int __static_local;
+  __static_local = 0;
+  j = i;
+  return __static_local;
+}
+
+int body_2(int *i)
+{
+  static int __static_local;
+  __static_local = 0;
+  (*i)++;
+  (*i)--;
+  return __static_local;
+}
+
+int body_3(int *i)
+{
+  static int __static_local;
+  __static_local = 0;
+  (*i)++;
+  if(*i == 4)
+    return 1;
+
+  (*i)--;
+  return 0;
+}
+
+int main()
+{
+  assert(before_loop() == 0);
+
+  for(int i = lowerbound(); i < upperbound(); incr(&i))
+    // clang-format off
+    __CPROVER_assigns(i, j)
+    __CPROVER_loop_invariant(0 <= i && i <= 10)
+    __CPROVER_loop_invariant(i != 0 ==> j + 1 == i)
+    // clang-format on
+    {
+      body_1(i);
+
+      if(body_3(&i))
+        return 1;
+
+      body_2(&i);
+    }
+
+  assert(j == 9);
+  assert(before_loop() == 0);
+  assert(after_loop() == 0);
+}

regression/contracts/loop_assigns_scoped_local_statics/test.desc

@@ -0,0 +1,28 @@
+CORE
+main.c
+--apply-loop-contracts
+^EXIT=0$
+^SIGNAL=0$
+^\[body_1.assigns.\d+\] .* Check that j is assignable: SUCCESS$
+^\[body_2.assigns.\d+\] .* Check that \*i is assignable: SUCCESS$
+^\[body_3.assigns.\d+\] .* Check that \*i is assignable: SUCCESS$
+^\[incr.assigns.\d+\] .* Check that \*i is assignable: SUCCESS$
+^\[main.assigns.\d+\] .* Check that i is assignable: SUCCESS$
+^\[main.\d+\] .* Check loop invariant before entry: SUCCESS$
+^\[main.\d+\] .* Check that loop invariant is preserved: SUCCESS$
+^\[main.assertion.\d+\] .* assertion j == 9: SUCCESS$
+^\[body_1.assigns.\d+\] line \d+ Check that __static_local is assignable: SUCCESS$
+^\[body_2.assigns.\d+\] line \d+ Check that __static_local is assignable: SUCCESS$
+^\[body_3.assigns.\d+\] line \d+ Check that __static_local is assignable: SUCCESS$
+^\[incr.assigns.\d+\] line \d+ Check that __static_local is assignable: SUCCESS$
+^\[main.assertion.\d+\] line \d+ assertion before_loop\(\) == 0: SUCCESS$
+^\[main.assertion.\d+\] line \d+ assertion after_loop\(\) == 0: SUCCESS$
+^\[upperbound.assigns.\d+\] line \d+ Check that __static_local is assignable: SUCCESS$
+^VERIFICATION SUCCESSFUL$
+--
+--
+This test checks assigns clause checking presence of locally declared static 
+variables.
+We observe that the local static variables declared within the loop's
+scope are correctly gathered and added to the write set,
+and are havoced (body_1 and body_2 do not return 0 anymore after the loop). 

regression/contracts/loop_assigns_scoped_local_statics_propagate/main.c

@@ -0,0 +1,46 @@
+#include <assert.h>
+#include <stdbool.h>
+
+int j;
+
+int before_loop()
+{
+  static int __static_local;
+  __static_local = 0;
+  return __static_local;
+}
+
+int after_loop()
+{
+  static int __static_local;
+  __static_local = 0;
+  return __static_local;
+}
+
+int bar(int i) __CPROVER_requires(true) __CPROVER_ensures(j == i)
+  __CPROVER_assigns(j)
+{
+  static int __static_local;
+  __static_local = 0;
+  j = i;
+  return __static_local;
+}
+
+int main()
+{
+  assert(before_loop() == 0);
+
+  for(int i = 0; i < 10; i++)
+    // clang-format off
+    __CPROVER_assigns(i, j)
+    __CPROVER_loop_invariant(0 <= i && i <= 10)
+    __CPROVER_loop_invariant(i != 0 ==> j + 1 == i)
+    // clang-format on
+    {
+      bar(i);
+    }
+
+  assert(j == 9);
+  assert(before_loop() == 0);
+  assert(after_loop() == 0);
+}

regression/contracts/loop_assigns_scoped_local_statics_propagate/test.desc

@@ -0,0 +1,24 @@
+CORE
+main.c
+--replace-call-with-contract bar --apply-loop-contracts
+^EXIT=0$
+^SIGNAL=0$
+^\[main.assigns.\d+\] line \d+ Check that j \(assigned by the contract of bar\) is assignable: SUCCESS$
+^\[main.assigns.\d+\] line \d+ Check that __static_local \(assigned by the contract of bar\) is assignable: SUCCESS$
+^\[main.assertion.\d+\] line \d+ assertion before_loop\(\) == 0: SUCCESS$
+^\[main.\d+\] line \d+ Check loop invariant before entry: SUCCESS$
+^\[main.\d+\] line \d+ Check that loop invariant is preserved: SUCCESS$
+^\[main.assigns.\d+\] line \d+ Check that i is assignable: SUCCESS$
+^\[main.assigns.\d+\] line \d+ Check that i is valid: SUCCESS$
+^\[main.assigns.\d+\] line \d+ Check that j is valid: SUCCESS$
+^\[main.assertion.\d+\] line \d+ assertion j == 9: SUCCESS$
+^\[main.assertion.\d+\] line \d+ assertion before_loop\(\) == 0: SUCCESS$
+^\[main.assertion.\d+\] line \d+ assertion after_loop\(\) == 0: SUCCESS$
+^VERIFICATION SUCCESSFUL$
+--
+--
+This test checks assigns clause checking presence of locally declared static 
+variables and loops.
+We observe that the local static variables declared within the loop's
+scope are correctly gathered and added to the write set,
+and are havoced (body_1 and body_2 do not return 0 anymore after the loop). 

src/goto-instrument/contracts/contracts.cpp

@@ -257,11 +257,8 @@ void code_contractst::check_apply_loop_contracts(
   // assigns clause snapshots
   goto_programt snapshot_instructions;
 
-  instrument_spec_assigns.track_static_locals(snapshot_instructions);
-
-  // ^^^ FIXME ^^^ we should only allow assignments to static locals
-  // declared in functions that are called in the loop body, not from the whole
-  // function...
+  instrument_spec_assigns.track_static_locals_between(
+    loop_head, loop_end, snapshot_instructions);
 
   // set of targets to havoc
   assignst to_havoc;
@@ -799,25 +796,22 @@ bool code_contractst::apply_function_contract(
     targets.add_to_operands(std::move(target));
   common_replace(targets);
 
-  // Create a sequence of non-deterministic assignments...
+  // Create a sequence of non-deterministic assignments ...
+
+  // ... for the assigns clause targets and static locals
   goto_programt havoc_instructions;
 
-  // ...for assigns clause targets
-  if(!assigns_clause.empty())
-  {
-    // Havoc all targets in the assigns clause
-    // TODO: handle local statics possibly touched by this function
-    havoc_assigns_clause_targetst havocker(
-      target_function,
-      targets.operands(),
-      goto_functions,
-      location,
-      symbol_table,
-      log.get_message_handler());
-    havocker.get_instructions(havoc_instructions);
-  }
+  havoc_assigns_clause_targetst havocker(
+    target_function,
+    targets.operands(),
+    goto_functions,
+    location,
+    symbol_table,
+    log.get_message_handler());
+
+  havocker.get_instructions(havoc_instructions);
 
-  // ...for the return value
+  // ... for the return value
   if(call_ret_opt.has_value())
   {
     auto &call_ret = call_ret_opt.value();