Skip checking frame conditions for local variables

feliperodri · feliperodri · commit d508a3ab1ddc · 2021-08-09T04:38:03.000Z
It avoids unnecessary assertions (improving performance) and
it prevents cases where memory primitives are invoked with dead objects.

Signed-off-by: Felipe R. Monteiro &lt;felisous@amazon.com&gt;
diff --git a/regression/contracts/assigns_enforce_16/main.c b/regression/contracts/assigns_enforce_16/main.c
@@ -0,0 +1,16 @@
+void foo(int *xp) __CPROVER_assigns(*xp)
+{
+  {
+    int y;
+    y = 2;
+  }
+  int z = 3;
+  *xp = 1;
+}
+
+int main()
+{
+  int *xp = malloc(sizeof(*xp));
+  foo(xp);
+  return 0;
+}
diff --git a/regression/contracts/assigns_enforce_16/test.desc b/regression/contracts/assigns_enforce_16/test.desc
@@ -0,0 +1,10 @@
+CORE
+main.c
+--enforce-all-contracts
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+Checks whether verification fails when enforcing a contract
+for functions, without assigns clauses, that modify an input.
diff --git a/regression/contracts/assigns_enforce_scoping_01/test.desc b/regression/contracts/assigns_enforce_scoping_01/test.desc
@@ -3,7 +3,6 @@ main.c
 --enforce-all-contracts
 ^EXIT=10$
 ^SIGNAL=0$
-^\[f1.\d+\] line \d+ Check that f1\$\$1\$\$1\$\$b is assignable: SUCCESS$
 ^\[f1.\d+\] line \d+ Check that \*f1\$\$1\$\$1\$\$b is assignable: SUCCESS$
 ^\[f1.\d+\] line \d+ Check that \*b is assignable: FAILURE$
 ^VERIFICATION FAILED$
diff --git a/regression/contracts/assigns_type_checking_valid_cases/test.desc b/regression/contracts/assigns_type_checking_valid_cases/test.desc
@@ -5,6 +5,7 @@ main.c
 ^SIGNAL=0$
 ^\[foo1.\d+\] line \d+ Check that a is assignable: SUCCESS$
 ^\[foo10.\d+\] line \d+ Check that buffer\-\>len is assignable: SUCCESS$
+^\[foo10.\d+\] line \d+ Check that buffer\-\>aux\.allocated is assignable: SUCCESS$
 ^\[foo2.\d+\] line \d+ Check that b is assignable: SUCCESS$
 ^\[foo3.\d+\] line \d+ Check that b is assignable: SUCCESS$
 ^\[foo3.\d+\] line \d+ Check that y is assignable: SUCCESS$
@@ -27,7 +28,6 @@ main.c
 ^\[foo8.\d+\] line \d+ Check that array\[\(.* int\)7\] is assignable: SUCCESS$
 ^\[foo8.\d+\] line \d+ Check that array\[\(.* int\)8\] is assignable: SUCCESS$
 ^\[foo8.\d+\] line \d+ Check that array\[\(.* int\)9\] is assignable: SUCCESS$
-^\[foo9.\d+\] line \d+ Check that new_array is assignable: SUCCESS$
 ^\[foo9.\d+\] line \d+ Check that array is assignable: SUCCESS$
 ^VERIFICATION SUCCESSFUL$
 --
diff --git a/regression/contracts/function-calls-05/test.desc b/regression/contracts/function-calls-05/test.desc
@@ -4,7 +4,6 @@ main.c
 ^EXIT=0$
 ^SIGNAL=0$
 \[postcondition.\d+\] file main.c line \d+ Check ensures clause: SUCCESS
-\[foo.\d+\] line \d+ Check that sum is assignable: SUCCESS
 \[main.assertion.\d+\] line \d+ assertion foo\(\&x, \&y\) \=\= 10: SUCCESS
 ^VERIFICATION SUCCESSFUL$
 --
diff --git a/regression/contracts/history-pointer-enforce-10/test.desc b/regression/contracts/history-pointer-enforce-10/test.desc
@@ -7,8 +7,6 @@ main.c
 ^\[postcondition.\d+\] file main.c line \d+ Check ensures clause\: SUCCESS$
 ^\[postcondition.\d+\] file main.c line \d+ Check ensures clause\: SUCCESS$
 ^\[bar.\d+\] line \d+ Check that p\-\>y is assignable\: SUCCESS$
-^\[baz.\d+\] line \d+ Check that pp is assignable\: SUCCESS$
-^\[baz.\d+\] line \d+ Check that empty is assignable\: SUCCESS$
 ^\[baz.\d+\] line \d+ Check that p is assignable\: SUCCESS$
 ^\[baz.\d+\] line \d+ Check that p is assignable\: SUCCESS$
 ^\[foo.\d+\] line \d+ Check that \*p\-\>y is assignable\: SUCCESS$
diff --git a/regression/contracts/quantifiers-exists-requires-enforce/test.desc b/regression/contracts/quantifiers-exists-requires-enforce/test.desc
@@ -4,10 +4,6 @@ main.c
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[postcondition.\d+\] file main.c line \d+ Check ensures clause: SUCCESS$
-^\[f1.\d+\] line \d+ Check that found\_four is assignable: SUCCESS$
-^\[f1.\d+\] line \d+ Check that i is assignable: SUCCESS$
-^\[f1.\d+\] line \d+ Check that i is assignable: SUCCESS$
-^\[f1.\d+\] line \d+ Check that found\_four is assignable: SUCCESS$
 ^VERIFICATION SUCCESSFUL$
 --
 ^warning: ignoring
diff --git a/regression/contracts/quantifiers-forall-ensures-enforce/test.desc b/regression/contracts/quantifiers-forall-ensures-enforce/test.desc
@@ -4,8 +4,6 @@ main.c
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[postcondition.\d+\] file main.c line \d+ Check ensures clause: SUCCESS$
-^\[f1.\d+\] line \d+ Check that i is assignable: SUCCESS$
-^\[f1.\d+\] line \d+ Check that i is assignable: SUCCESS$
 ^\[f1.\d+\] line \d+ Check that arr\[\(.*\)i\] is assignable: SUCCESS$
 ^VERIFICATION SUCCESSFUL$
 --
diff --git a/regression/contracts/quantifiers-forall-requires-enforce/test.desc b/regression/contracts/quantifiers-forall-requires-enforce/test.desc
@@ -4,10 +4,6 @@ main.c
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[postcondition.\d+\] file main.c line \d+ Check ensures clause: SUCCESS$
-^\[f1.\d+\] line \d+ Check that is\_identity is assignable: SUCCESS$
-^\[f1.\d+\] line \d+ Check that i is assignable: SUCCESS$
-^\[f1.\d+\] line \d+ Check that i is assignable: SUCCESS$
-^\[f1.\d+\] line \d+ Check that is\_identity is assignable: SUCCESS$
 ^VERIFICATION SUCCESSFUL$
 --
 ^warning: ignoring
diff --git a/regression/contracts/test_array_memory_enforce/test.desc b/regression/contracts/test_array_memory_enforce/test.desc
@@ -7,7 +7,6 @@ main.c
 \[foo.\d+\] line \d+ Check that \*x is assignable: SUCCESS
 \[foo.\d+\] line \d+ Check that x\[\(.* int\)5\] is assignable: SUCCESS
 \[foo.\d+\] line \d+ Check that x\[\(.* int\)9\] is assignable: SUCCESS
-\[foo.\d+\] line \d+ Check that y is assignable: SUCCESS
 ^VERIFICATION SUCCESSFUL$
 --
 --
diff --git a/src/goto-instrument/contracts/contracts.cpp b/src/goto-instrument/contracts/contracts.cpp
@@ -675,14 +675,19 @@ void code_contractst::instrument_assign_statement(
 
   const exprt &lhs = instruction_iterator->assign_lhs();
 
-  goto_programt alias_assertion;
-  alias_assertion.add(goto_programt::make_assertion(
-    assigns_clause.alias_expression(lhs),
-    instruction_iterator->source_location));
-  alias_assertion.instructions.back().source_location.set_comment(
-    "Check that " + from_expr(ns, lhs.id(), lhs) + " is assignable");
-  insert_before_swap_and_advance(
-    program, instruction_iterator, alias_assertion);
+  if(
+    freely_assignable_symbols.find(lhs.get(ID_identifier)) ==
+    freely_assignable_symbols.end())
+  {
+    goto_programt alias_assertion;
+    alias_assertion.add(goto_programt::make_assertion(
+      assigns_clause.alias_expression(lhs),
+      instruction_iterator->source_location));
+    alias_assertion.instructions.back().source_location.set_comment(
+      "Check that " + from_expr(ns, lhs.id(), lhs) + " is assignable");
+    insert_before_swap_and_advance(
+      program, instruction_iterator, alias_assertion);
+  }
 }
 
 void code_contractst::instrument_call_statement(
@@ -894,14 +899,6 @@ void code_contractst::check_frame_conditions(
 
   // Create a list of variables that are okay to assign.
   std::set<irep_idt> freely_assignable_symbols;
-  // Add all parameters that are not pointers to the freely assignable set
-  for(code_typet::parametert param : type.parameters())
-  {
-    if(param.type().id() != ID_pointer)
-    {
-      freely_assignable_symbols.insert(param.get_identifier());
-    }
-  }
 
   // Create temporary variables to hold the assigns
   // clause targets before they can be modified.
@@ -917,6 +914,7 @@ void code_contractst::check_frame_conditions(
   {
     if(instruction_it->is_decl())
     {
+      // Local variables are always freely assignable
       freely_assignable_symbols.insert(
         instruction_it->get_decl().symbol().get_identifier());
 
