Removes subset relationship check from contracts

Signed-off-by: Felipe R. Monteiro <felisous@amazon.com>

Author: feliperodri

…sion/contracts/assigns_enforce_22/main.c …sion/contracts/assigns_enforce_21/main.cregression/contracts/assigns_enforce_22/main.c renamed to regression/contracts/assigns_enforce_21/main.c regression/contracts/assigns_enforce_22/main.c renamed to regression/contracts/assigns_enforce_21/main.c

@@ -3,7 +3,7 @@
 
 int x = 0;
 
-void quz() __CPROVER_assigns(x)
+void quz() __CPROVER_assigns(x) __CPROVER_ensures(x == -1)
 {
   x = -1;
 }
@@ -17,6 +17,7 @@ void bar(int *y, int w) __CPROVER_assigns(*y)
 {
   *y = 3;
   w = baz();
+  assert(w == 5);
   quz();
 }
 

…n/contracts/assigns_enforce_22/test.desc …n/contracts/assigns_enforce_21/test.descregression/contracts/assigns_enforce_22/test.desc renamed to regression/contracts/assigns_enforce_21/test.desc regression/contracts/assigns_enforce_22/test.desc renamed to regression/contracts/assigns_enforce_21/test.desc

@@ -1,14 +1,14 @@
 CORE
 main.c
---enforce-contract foo
+--enforce-contract foo --replace-call-with-contract quz
 ^EXIT=10$
 ^SIGNAL=0$
 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$
-^\[quz.\d+\] line \d+ Check that x is assignable: FAILURE$
 ^VERIFICATION FAILED$
 --
 --

regression/contracts/assigns_replace_08/test.desc

@@ -3,12 +3,10 @@ main.c
 --enforce-contract foo --replace-call-with-contract bar _ --pointer-primitive-check
 ^EXIT=10$
 ^SIGNAL=0$
-\[foo.\d+\] line \d+ Check that bar\'s assigns clause is a subset of foo\'s assigns clause: FAILURE$
 \[foo.\d+\] line \d+ Check that \*z is assignable: FAILURE$
-^.* 2 of \d+ failed \(\d+ iteration.*\)$
+^.* 1 of \d+ failed \(\d+ iteration.*\)$
 ^VERIFICATION FAILED$
 --
-\[\d+\] file main.c line \d+ Check that bar\'s assigns clause is a subset of foo\'s assigns clause: SUCCESS$
 \[\d+\] file main.c line \d+ Check that \*z is assignable: SUCCESS$
 ^VERIFICATION SUCCESSFUL$
 --

regression/contracts/assigns_replace_09/test.desc

@@ -3,7 +3,6 @@ main.c
 --replace-call-with-contract bar --enforce-contract foo
 ^EXIT=0$
 ^SIGNAL=0$
-\[foo.\d+\] line \d+ Check that bar\'s assigns clause is a subset of foo\'s assigns clause: SUCCESS$
 \[foo.\d+\] line \d+ Check that \*z is assignable: SUCCESS$
 ^VERIFICATION SUCCESSFUL$
 --

regression/contracts/assigns_validity_pointer_02/test.desc

@@ -13,9 +13,7 @@ main.c
 ^VERIFICATION SUCCESSFUL$
 --
 ^\[postcondition.\d+\] file main.c line \d+ Check ensures clause: FAILURE$
-^\[foo.\d+\] line \d+ Check that bar\'s assigns clause is a subset of foo\'s assigns clause: FAILURE$
 ^\[foo.\d+\] line \d+ Check that \*x is assignable: FAILURE$
-^\[foo.\d+\] line \d+ Check that baz\'s assigns clause is a subset of foo\'s assigns clause: FAILURE$
 --
 Verification:
 This test checks support for a NULL pointer that is assigned to by

regression/contracts/assigns_validity_pointer_04/test.desc

@@ -3,10 +3,8 @@ main.c
 --enforce-contract foo --replace-call-with-contract bar --replace-call-with-contract baz _ --pointer-primitive-check
 ^EXIT=10$
 ^SIGNAL=0$
-^\[foo.\d+\] line \d+ Check that bar\'s assigns clause is a subset of foo\'s assigns clause: FAILURE$
-^\[foo.\d+\] line \d+ Check that baz\'s assigns clause is a subset of foo\'s assigns clause: FAILURE$
 ^\[foo.\d+\] line \d+ Check that z is assignable: FAILURE$
-^.* 3 of \d+ failed \(\d+ iteration.*\)$
+^.* 1 of \d+ failed \(\d+ iteration.*\)$
 ^VERIFICATION FAILED$
 // bar
 ASSERT \*foo::x > 0

src/goto-instrument/contracts/assigns.cpp

@@ -150,24 +150,3 @@ exprt assigns_clauset::generate_containment_check(const exprt &lhs) const
   }
   return disjunction(condition);
 }
-
-exprt assigns_clauset::generate_subset_check(
-  const assigns_clauset &subassigns) const
-{
-  if(subassigns.write_set.empty())
-    return true_exprt();
-
-  exprt result = true_exprt();
-  for(const auto &subtarget : subassigns.write_set)
-  {
-    exprt::operandst current_subtarget_found_conditions;
-    for(const auto &target : write_set)
-    {
-      current_subtarget_found_conditions.push_back(
-        target.generate_containment_check(subtarget.address));
-    }
-    result = and_exprt(result, disjunction(current_subtarget_found_conditions));
-  }
-
-  return result;
-}

src/goto-instrument/contracts/assigns.h

@@ -63,7 +63,6 @@ class assigns_clauset
 
   goto_programt generate_havoc_code(const source_locationt &) const;
   exprt generate_containment_check(const exprt &) const;
-  exprt generate_subset_check(const assigns_clauset &) const;
 
   const messaget &log;
   const namespacet &ns;

src/goto-instrument/contracts/contracts.cpp

@@ -433,8 +433,7 @@ code_contractst::create_ensures_instruction(
 bool code_contractst::apply_function_contract(
   const irep_idt &function,
   goto_programt &function_body,
-  goto_programt::targett &target,
-  const std::set<std::string> &enforced_functions)
+  goto_programt::targett &target)
 {
   const auto &const_target =
     static_cast<const goto_programt::targett &>(target);
@@ -568,30 +567,9 @@ bool code_contractst::apply_function_contract(
   {
     assigns_clauset assigns_clause(targets.operands(), log, ns);
 
-    // Retrieve assigns clause of the caller function if exists.
-    auto caller_assigns =
-      to_code_with_contract_type(ns.lookup(function).type).assigns();
-
-    if(enforced_functions.find(function.c_str()) != enforced_functions.end())
-    {
-      // check subset relationship of assigns clause for called function
-      assigns_clauset caller_assigns_clause(caller_assigns, log, ns);
-      goto_programt subset_check_assertion;
-      subset_check_assertion.add(goto_programt::make_assertion(
-        caller_assigns_clause.generate_subset_check(assigns_clause),
-        const_target->source_location));
-      subset_check_assertion.instructions.back().source_location.set_comment(
-        "Check that " + id2string(target_function) +
-        "'s assigns clause is a subset of " +
-        id2string(const_target->source_location.get_function()) +
-        "'s assigns clause");
-      insert_before_swap_and_advance(
-        function_body, target, subset_check_assertion);
-    }
-
     // Havoc all targets in global write set
     auto assigns_havoc =
-      assigns_clause.generate_havoc_code(const_target->source_location);
+      assigns_clause.generate_havoc_code(target->source_location);
 
     // Insert the non-deterministic assignment immediately before the call site.
     insert_before_swap_and_advance(function_body, target, assigns_havoc);
@@ -1097,9 +1075,7 @@ void code_contractst::add_contract_check(
   dest.destructive_insert(dest.instructions.begin(), check);
 }
 
-bool code_contractst::replace_calls(
-  const std::set<std::string> &to_replace,
-  const std::set<std::string> &to_enforce)
+bool code_contractst::replace_calls(const std::set<std::string> &to_replace)
 {
   if(to_replace.empty())
     return false;
@@ -1123,7 +1099,7 @@ bool code_contractst::replace_calls(
           continue;
 
         fail |= apply_function_contract(
-          goto_function.first, goto_function.second.body, ins, to_enforce);
+          goto_function.first, goto_function.second.body, ins);
       }
     }
   }

src/goto-instrument/contracts/contracts.h

@@ -74,8 +74,7 @@ class code_contractst
   /// it using `cbmc --function F`.
   ///
   /// \return `true` on failure, `false` otherwise
-  bool
-  replace_calls(const std::set<std::string> &, const std::set<std::string> &);
+  bool replace_calls(const std::set<std::string> &);
 
   /// \brief Turn requires & ensures into assumptions and assertions for each of
   ///        the named functions
@@ -178,8 +177,7 @@ class code_contractst
   bool apply_function_contract(
     const irep_idt &,
     goto_programt &,
-    goto_programt::targett &,
-    const std::set<std::string> &);
+    goto_programt::targett &);
 
   /// Instruments `wrapper_function` adding assumptions based on requires
   /// clauses and assertions based on ensures clauses.