Skip function parameters and auxiliary variables when checking assigns clauses and check loop-freeness

regression/contracts/assigns_enforce_04/test.desc

@@ -3,12 +3,6 @@ main.c
 --enforce-contract f1
 ^EXIT=0$
 ^SIGNAL=0$
-^\[f1.\d+\] line \d+ Check that x2 is assignable: SUCCESS$
-^\[f1.\d+\] line \d+ Check that y2 is assignable: SUCCESS$
-^\[f1.\d+\] line \d+ Check that z2 is assignable: SUCCESS$
-^\[f2.\d+\] line \d+ Check that x3 is assignable: SUCCESS$
-^\[f2.\d+\] line \d+ Check that y3 is assignable: SUCCESS$
-^\[f2.\d+\] line \d+ Check that z3 is assignable: SUCCESS$
 ^\[f3.\d+\] line \d+ Check that \*x3 is assignable: SUCCESS$
 ^\[f3.\d+\] line \d+ Check that \*y3 is assignable: SUCCESS$
 ^\[f3.\d+\] line \d+ Check that \*z3 is assignable: SUCCESS$

regression/contracts/assigns_enforce_05/test.desc

@@ -3,7 +3,6 @@ main.c
 --enforce-contract f1 --enforce-contract f2 --enforce-contract f3
 ^EXIT=0$
 ^SIGNAL=0$
-^\[f1.1\] line \d+ .*: SUCCESS$
 ^VERIFICATION SUCCESSFUL$
 --
 --

regression/contracts/assigns_enforce_18/test.desc

@@ -7,7 +7,6 @@ main.c
 ^\[bar.\d+\] line \d+ Check that \*b is assignable: SUCCESS$
 ^\[baz.\d+\] line \d+ Check that POINTER_OBJECT\(\(void \*\)c\) is assignable: FAILURE$
 ^\[baz.\d+\] line \d+ Check that \*a is assignable: SUCCESS$
-^\[foo.\d+\] line \d+ Check that a is assignable: SUCCESS$
 ^\[foo.\d+\] line \d+ Check that yp is assignable: SUCCESS$
 ^\[foo.\d+\] line \d+ Check that z is assignable: SUCCESS$
 ^\[foo.\d+\] line \d+ Check that \*xp is assignable: SUCCESS$

regression/contracts/assigns_enforce_21/test.desc

@@ -6,9 +6,6 @@ main.c
 main.c function bar
 ^\[bar.\d+\] line \d+ Check that \*y is assignable: SUCCESS$
 ^\[bar.\d+\] line \d+ Check that x is assignable: FAILURE$
-^\[baz.\d+\] line \d+ Check that w is assignable: SUCCESS$
-^\[foo.\d+\] line \d+ Check that w is assignable: SUCCESS$
-^\[foo.\d+\] line \d+ Check that z is assignable: SUCCESS$
 ^VERIFICATION FAILED$
 --
 --

regression/contracts/assigns_enforce_free_dead/test.desc

@@ -10,7 +10,6 @@ main.c
 ^\[foo.\d+\] line \d+ Check that a is assignable: SUCCESS$
 ^\[foo.\d+\] line \d+ Check that q is assignable: SUCCESS$
 ^\[foo.\d+\] line \d+ Check that w is assignable: SUCCESS$
-^\[foo.\d+\] line \d+ Check that x is assignable: SUCCESS$
 ^\[foo.\d+\] line \d+ Check that y is assignable: SUCCESS$
 ^\[foo.\d+\] line \d+ Check that z is assignable: SUCCESS$
 ^\[foo.\d+\] line \d+ Check that POINTER_OBJECT\(\(void \*\)z\) is assignable: SUCCESS$
@@ -25,7 +24,6 @@ main.c
 ^\[foo.\d+\] line \d+ Check that a is assignable: FAILURE$
 ^\[foo.\d+\] line \d+ Check that q is assignable: FAILURE$
 ^\[foo.\d+\] line \d+ Check that w is assignable: FAILURE$
-^\[foo.\d+\] line \d+ Check that x is assignable: FAILURE$
 ^\[foo.\d+\] line \d+ Check that y is assignable: FAILURE$
 ^\[foo.\d+\] line \d+ Check that z is assignable: FAILURE$
 ^\[foo.\d+\] line \d+ Check that POINTER_OBJECT\(\(void \*\)z\) is assignable: FAILURE$

regression/contracts/assigns_enforce_structs_04/test.desc

@@ -6,7 +6,6 @@ main.c
 ^\[f1.\d+\] line \d+ Check that p->y is assignable: FAILURE$
 ^\[f2.\d+\] line \d+ Check that p->x is assignable: FAILURE$
 ^\[f3.\d+\] line \d+ Check that p->y is assignable: SUCCESS$
-^\[f4.\d+\] line \d+ Check that p is assignable: SUCCESS$
 ^VERIFICATION FAILED$
 --
 --

regression/contracts/assigns_enforce_subfunction_calls/test.desc

@@ -3,28 +3,15 @@ main.c
 --enforce-contract foo
 ^EXIT=10$
 ^SIGNAL=0$
-^main.c function bar$
-^\[bar.1\] line \d+ Check that x is assignable: SUCCESS$
-^\[bar.2\] line \d+ Check that y is assignable: SUCCESS$
-^\[bar.3\] line \d+ Check that x is assignable: SUCCESS$
-^\[bar.4\] line \d+ Check that y is assignable: SUCCESS$
 ^main.c function baz$
 ^\[baz.1\] line \d+ Check that \*x is assignable: SUCCESS$
 ^\[baz.2\] line \d+ Check that \*x is assignable: SUCCESS$
 ^\[baz.3\] line \d+ Check that \*x is assignable: FAILURE$
 ^\[baz.4\] line \d+ Check that \*x is assignable: FAILURE$
 ^main.c function foo$
-^\[foo.1\] line \d+ Check that x is assignable: SUCCESS$
-^\[foo.2\] line \d+ Check that y is assignable: SUCCESS$
 ^\[foo.assertion.1\] line \d+ foo.x.set: SUCCESS$
-^\[foo.3\] line \d+ Check that x is assignable: SUCCESS$
-^\[foo.4\] line \d+ Check that y is assignable: SUCCESS$
 ^\[foo.assertion.2\] line \d+ foo.local.set: SUCCESS$
-^\[foo.5\] line \d+ Check that x is assignable: SUCCESS$
-^\[foo.6\] line \d+ Check that y is assignable: SUCCESS$
 ^\[foo.assertion.3\] line \d+ foo.y.set: SUCCESS$
-^\[foo.7\] line \d+ Check that x is assignable: SUCCESS$
-^\[foo.8\] line \d+ Check that y is assignable: SUCCESS$
 ^\[foo.assertion.4\] line \d+ foo.z.set: SUCCESS$
 ^VERIFICATION FAILED$
 --

regression/contracts/assigns_function_pointer/test.desc

@@ -3,7 +3,6 @@ main.c
 --enforce-contract bar
 ^EXIT=0$
 ^SIGNAL=0$
-^\[bar.1\] line \d+ Check that fun\_ptr is assignable: SUCCESS$
 ^\[main.assertion.\d+\] line \d+ assertion x \=\= 0: SUCCESS$
 ^\[main.assertion.\d+\] line \d+ assertion x \=\= 1: SUCCESS$
 ^VERIFICATION SUCCESSFUL$

regression/contracts/assigns_type_checking_valid_cases/test.desc

@@ -3,13 +3,9 @@ main.c
 --enforce-contract foo1 --enforce-contract foo2 --enforce-contract foo3 --enforce-contract foo4 --enforce-contract foo5 --enforce-contract foo6 --enforce-contract foo7 --enforce-contract foo8 --enforce-contract foo9 --enforce-contract foo10 _ --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$
-^\[foo4.\d+\] line \d+ Check that b is assignable: SUCCESS$
 ^\[foo4.\d+\] line \d+ Check that \*c is assignable: SUCCESS$
 ^\[foo4.\d+\] line \d+ Check that \*x is assignable: SUCCESS$
 ^\[foo5.\d+\] line \d+ Check that buffer.data is assignable: SUCCESS$
@@ -28,7 +24,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 array is assignable: SUCCESS$
 ^VERIFICATION SUCCESSFUL$
 --
 Checks whether CBMC parses correctly all standard cases for assigns clauses.

regression/contracts/assigns_validity_pointer_02/test.desc

@@ -7,8 +7,6 @@ main.c
 ^\[bar.\d+\] line \d+ Check that \*x is assignable: SUCCESS$
 ^\[bar.\d+\] line \d+ Check that \*y is assignable: SUCCESS$
 ^\[baz.\d+\] line \d+ Check that \*z is assignable: SUCCESS$
-^\[foo.\d+\] line \d+ Check that x is assignable: SUCCESS$
-^\[foo.\d+\] line \d+ Check that y is assignable: SUCCESS$
 ^\[foo.\d+\] line \d+ Check that \*x is assignable: SUCCESS$
 ^VERIFICATION SUCCESSFUL$
 --

regression/contracts/history-pointer-enforce-10/main.c

@@ -23,7 +23,7 @@ void bar(struct pair *p) __CPROVER_assigns(p->y)
   p->y = (p->y + 5);
 }
 
-void baz(struct pair p) __CPROVER_assigns(p)
+void baz(struct pair p) __CPROVER_assigns()
   __CPROVER_ensures(p == __CPROVER_old(p))
 {
   struct pair pp = p;

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 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$
 ^\[foo.\d+\] line \d+ Check that z is assignable: SUCCESS$
 ^\[main.assertion.\d+\] line \d+ assertion \*\(p->y\) == 7: SUCCESS$
@@ -19,3 +17,5 @@ main.c
 This test checks that history variables are supported for structs, symbols, and
 struct members. By using the --enforce-contract flag, the postcondition
 (with history variable) is asserted. In this case, this assertion should pass.
+Note: A function is always authorized to assign the variables that store
+its arguments, there is no need to mention them in the assigns clause.

regression/contracts/test_aliasing_ensure_indirect/main.c

@@ -2,7 +2,7 @@
 #include <stdbool.h>
 #include <stdlib.h>
 
-void bar(int *z) __CPROVER_assigns(z)
+void bar(int *z) __CPROVER_assigns()
   __CPROVER_ensures(__CPROVER_is_fresh(z, sizeof(int)))
 {
   z = malloc(sizeof(*z));

regression/contracts/test_aliasing_ensure_indirect/test.desc

@@ -4,7 +4,6 @@ main.c
 ^EXIT=0$
 ^SIGNAL=0$
 \[postcondition.\d+\] file main.c line \d+ Check ensures clause: SUCCESS
-\[bar.\d+\] line \d+ Check that z is assignable: SUCCESS
 \[foo.\d+\] line \d+ Check that \*x is assignable: SUCCESS
 \[main.assertion.\d+\] line \d+ assertion \!\(n \< 4\): SUCCESS
 ^VERIFICATION SUCCESSFUL$

src/goto-instrument/contracts/contracts.cpp

@@ -309,7 +309,13 @@ void code_contractst::check_apply_loop_contracts(
 
   // Perform write set instrumentation on the entire loop.
   check_frame_conditions(
-    function_name, goto_function.body, loop_head, loop_end, loop_assigns);
+    function_name,
+    goto_function.body,
+    loop_head,
+    loop_end,
+    loop_assigns,
+    // do not skip checks on function parameter assignments
+    false);
 
   havoc_assigns_targetst havoc_gen(to_havoc, ns);
   havoc_gen.append_full_havoc_code(
@@ -1171,7 +1177,9 @@ bool code_contractst::check_frame_conditions_function(const irep_idt &function)
     function_obj->second.body,
     instruction_it,
     function_obj->second.body.instructions.end(),
-    assigns);
+    assigns,
+    // skip checks on function parameter assignments
+    true);
 
   return false;
 }
@@ -1181,14 +1189,21 @@ void code_contractst::check_frame_conditions(
   goto_programt &body,
   goto_programt::targett instruction_it,
   const goto_programt::targett &instruction_end,
-  assigns_clauset &assigns)
+  assigns_clauset &assigns,
+  bool skip_parameter_assigns)
 {
   for(; instruction_it != instruction_end; ++instruction_it)
   {
     const auto &pragmas = instruction_it->source_location().get_pragmas();
     if(pragmas.find(CONTRACT_PRAGMA_DISABLE_ASSIGNS_CHECK) != pragmas.end())
       continue;
 
+    if(skip_parameter_assigns && is_parameter_assign(instruction_it, ns))
+      continue;
+
+    if(is_auxiliary_decl_dead_or_assign(instruction_it, ns))
+      continue;
+
     // Do not instrument this instruction again in the future,
     // since we are going to instrument it now below.
     add_pragma_disable_assigns_check(*instruction_it);

src/goto-instrument/contracts/contracts.h

@@ -132,7 +132,8 @@ class code_contractst
     goto_programt &,
     goto_programt::targett,
     const goto_programt::targett &,
-    assigns_clauset &);
+    assigns_clauset &,
+    bool skip_parameter_assigns);
 
   /// Inserts an assertion into the goto program to ensure that
   /// an expression is within the assignable memory frame.

src/goto-instrument/contracts/utils.cpp

@@ -163,3 +163,50 @@ void disable_pointer_checks(source_locationt &source_location)
   source_location.add_pragma("disable:pointer-primitive-check");
   source_location.add_pragma("disable:pointer-overflow-check");
 }
+
+bool is_parameter_assign(
+  const goto_programt::targett &instruction_it,
+  namespacet &ns)
+{
+  optionalt<symbol_exprt> sym = {};
+
+  // extract symbol
+  if(instruction_it->is_assign())
+  {
+    const auto &lhs = instruction_it->assign_lhs();
+    if(can_cast_expr<symbol_exprt>(lhs))
+      sym = to_symbol_expr(lhs);
+  }
+
+  // check condition
+  if(sym.has_value())
+    return ns.lookup(sym.value().get_identifier()).is_parameter;
+
+  return false;
+}
+
+bool is_auxiliary_decl_dead_or_assign(
+  const goto_programt::targett &instruction_it,
+  namespacet &ns)
+{
+  optionalt<symbol_exprt> sym = {};
+
+  // extract symbol
+  if(instruction_it->is_decl())
+    sym = instruction_it->decl_symbol();
+  else if(instruction_it->is_dead())
+    sym = instruction_it->dead_symbol();
+  else if(instruction_it->is_assign())
+  {
+    const auto &lhs = instruction_it->assign_lhs();
+    if(can_cast_expr<symbol_exprt>(lhs))
+      sym = to_symbol_expr(lhs);
+  }
+
+  // check condition
+  if(sym.has_value())
+    return ns.lookup(sym.value().get_identifier()).is_auxiliary;
+
+  return false;
+}
+

src/goto-instrument/contracts/utils.h

@@ -112,17 +112,29 @@ void insert_before_swap_and_advance(
 /// \param mode: The mode for the new symbol, e.g. ID_C, ID_java.
 /// \param symtab: The symbol table to which the new symbol is to be added.
 /// \param suffix: Suffix to use to generate the unique name
-/// \param is_auxiliary: Do not print symbol in traces if true (default = false)
+/// \param is_auxiliary: Do not print symbol in traces if true (default = true)
 /// \return The new symbolt object.
 const symbolt &new_tmp_symbol(
   const typet &type,
   const source_locationt &location,
   const irep_idt &mode,
   symbol_table_baset &symtab,
   std::string suffix = "tmp_cc",
-  bool is_auxiliary = false);
+  bool is_auxiliary = true);
 
 /// Add disable pragmas for all pointer checks on the given location
 void disable_pointer_checks(source_locationt &source_location);
 
+/// Returns true iff the instruction is a `DECL x`, `DEAD x`,
+/// or `ASSIGN x := expr` where `x` has the `is_parameter` flag set.
+bool is_parameter_assign(
+  const goto_programt::targett &instruction_it,
+  namespacet &ns);
+
+/// Returns true iff the instruction is a `DECL x`, `DEAD x`,
+/// or `ASSIGN x := expr` where `x` has the `is_auxiliary` flag set.
+bool is_auxiliary_decl_dead_or_assign(
+  const goto_programt::targett &instruction_it,
+  namespacet &ns);
+
 #endif // CPROVER_GOTO_INSTRUMENT_CONTRACTS_UTILS_H