Merge pull request #6279 from feliperodri/handle-tmp-dead

Skip checking frame conditions for local variables

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 _ --pointer-primitive-check
+^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_17/main.c

@@ -0,0 +1,16 @@
+#include <assert.h>
+
+int x = 0;
+
+void pure() __CPROVER_assigns()
+{
+  int x;
+  x++;
+}
+
+int main()
+{
+  pure();
+  assert(x == 0);
+  return 0;
+}

regression/contracts/assigns_enforce_17/test.desc

@@ -0,0 +1,11 @@
+CORE
+main.c
+--enforce-all-contracts
+^EXIT=0$
+^SIGNAL=0$
+^\[main.assertion.\d+\] line \d+ assertion x \=\= 0\: SUCCESS$
+^VERIFICATION SUCCESSFUL$
+--
+--
+Checks whether verification correctly distincts local variables
+and global variables with same name when checking frame conditions.

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_replace_03/main.c

@@ -1,17 +1,18 @@
 #include <assert.h>
+#include <stdlib.h>
 
 int y;
 double z;
 
-void bar(char **c) __CPROVER_assigns(y, z, **c) __CPROVER_ensures(**c == 6)
+void bar(char *c) __CPROVER_assigns(y, z, *c) __CPROVER_ensures(*c == 6)
 {
 }
 
 int main()
 {
-  char **b;
+  char *b = malloc(sizeof(*b));
   bar(b);
-  assert(**b == 6);
+  assert(*b == 6);
 
   return 0;
 }

regression/contracts/assigns_replace_03/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---replace-all-calls-with-contracts
+--replace-all-calls-with-contracts _ --pointer-primitive-check
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/contracts/assigns_type_checking_valid_cases/main.c

@@ -45,8 +45,7 @@ void foo5(struct buf buffer) __CPROVER_assigns(buffer)
   buffer.len = 0;
 }
 
-void foo6(struct buf *buffer)
-  __CPROVER_assigns(buffer->data, *(buffer->data), buffer->len)
+void foo6(struct buf *buffer) __CPROVER_assigns(buffer->data, buffer->len)
 {
   buffer->data = malloc(sizeof(*(buffer->data)));
   *(buffer->data) = 1;

regression/contracts/assigns_type_checking_valid_cases/test.desc

@@ -1,10 +1,11 @@
 CORE
 main.c
---enforce-all-contracts
+--enforce-all-contracts _ --pointer-primitive-check
 ^EXIT=0$
 ^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

@@ -396,7 +396,7 @@ void code_contractst::replace_old_parameter(
 
     if(
       parameter.id() == ID_dereference || parameter.id() == ID_member ||
-      parameter.id() == ID_symbol)
+      parameter.id() == ID_symbol || parameter.id() == ID_ptrmember)
     {
       auto it = parameter2history.find(parameter);
 
@@ -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());