Skip checking frame conditions for local variables

It avoids unnecessary assertions (improving performance) and
it prevents cases where memory primitives are invoked with dead objects.

Signed-off-by: Felipe R. Monteiro <[email protected]>

Author: feliperodri

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;
+}

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.

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$

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$
 --

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$
 --

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$

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

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$
 --

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

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$
 --
 --

src/goto-instrument/contracts/contracts.cpp

@@ -665,7 +665,7 @@ void code_contractst::instrument_assign_statement(
   goto_programt::instructionst::iterator &instruction_iterator,
   goto_programt &program,
   exprt &assigns,
-  std::set<irep_idt> &freely_assignable_symbols,
+  std::set<irep_idt> &local_assignable_symbols,
   assigns_clauset &assigns_clause)
 {
   INVARIANT(
@@ -675,21 +675,26 @@ 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(
+    local_assignable_symbols.find(lhs.get(ID_identifier)) ==
+    local_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(
   goto_programt::instructionst::iterator &instruction_iterator,
   goto_programt &program,
   exprt &assigns,
-  std::set<irep_idt> &freely_assignable_symbols,
+  std::set<irep_idt> &local_assignable_symbols,
   assigns_clauset &assigns_clause)
 {
   INVARIANT(
@@ -736,9 +741,9 @@ void code_contractst::instrument_call_statement(
 
   if(
     call.lhs().is_not_nil() && call.lhs().id() == ID_symbol &&
-    freely_assignable_symbols.find(
+    local_assignable_symbols.find(
       to_symbol_expr(call.lhs()).get_identifier()) ==
-      freely_assignable_symbols.end())
+      local_assignable_symbols.end())
   {
     exprt alias_expr = assigns_clause.alias_expression(call.lhs());
 
@@ -893,15 +898,7 @@ void code_contractst::check_frame_conditions(
   assigns_clauset assigns(assigns_expr, *this, target.name, log);
 
   // 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());
-    }
-  }
+  std::set<irep_idt> local_assignable_symbols;
 
   // Create temporary variables to hold the assigns
   // clause targets before they can be modified.
@@ -917,7 +914,7 @@ void code_contractst::check_frame_conditions(
   {
     if(instruction_it->is_decl())
     {
-      freely_assignable_symbols.insert(
+      local_assignable_symbols.insert(
         instruction_it->get_decl().symbol().get_identifier());
 
       assigns_clause_targett *new_target =
@@ -936,7 +933,7 @@ void code_contractst::check_frame_conditions(
         instruction_it,
         program,
         assigns_expr,
-        freely_assignable_symbols,
+        local_assignable_symbols,
         assigns);
     }
     else if(instruction_it->is_function_call())
@@ -945,7 +942,7 @@ void code_contractst::check_frame_conditions(
         instruction_it,
         program,
         assigns_expr,
-        freely_assignable_symbols,
+        local_assignable_symbols,
         assigns);
     }
   }

src/goto-instrument/contracts/contracts.h

@@ -164,7 +164,7 @@ class code_contractst
     goto_programt::instructionst::iterator &instruction_it,
     goto_programt &program,
     exprt &assigns,
-    std::set<irep_idt> &freely_assignable_symbols,
+    std::set<irep_idt> &local_assignable_symbols,
     assigns_clauset &assigns_clause);
 
   /// Inserts an assertion statement into program before the function call at
@@ -175,7 +175,7 @@ class code_contractst
     goto_programt::instructionst::iterator &ins_it,
     goto_programt &program,
     exprt &assigns,
-    std::set<irep_idt> &freely_assignable_symbols,
+    std::set<irep_idt> &local_assignable_symbols,
     assigns_clauset &assigns_clause);
 
   /// Creates a boolean expression which is true when there exists an expression