remove repeated inclusion checks in nested loops

Author: SaswatPadhi

src/goto-instrument/contracts/assigns.cpp

@@ -117,6 +117,8 @@ assigns_clauset::conditional_address_ranget::generate_snapshot_instructions()
     location));
 
   instructions.destructive_append(skip_program);
+
+  add_pragma_disable_assigns_check(instructions);
   return instructions;
 }
 

src/goto-instrument/contracts/contracts.cpp

@@ -140,9 +140,6 @@ void code_contractst::check_apply_loop_contracts(
     generated_code,
     ID_loop_entry);
 
-  // Create 'loop_entry' history variables
-  insert_before_swap_and_advance(goto_function.body, loop_head, generated_code);
-
   // Generate: assert(invariant) just before the loop
   // We use a block scope to create a temporary assertion,
   // and immediately convert it to goto instructions.
@@ -154,6 +151,14 @@ void code_contractst::check_apply_loop_contracts(
       "Check loop invariant before entry");
   }
 
+  // Add 'loop_entry' history variables and base case assertion.
+  // These variables are local and thus
+  // need not be checked against the enclosing scope's write set.
+  insert_before_swap_and_advance(
+    goto_function.body,
+    loop_head,
+    add_pragma_disable_assigns_check(generated_code));
+
   // havoc the variables that may be modified
   modifiest modifies;
   if(assigns.is_nil())
@@ -176,7 +181,8 @@ void code_contractst::check_apply_loop_contracts(
     for(const auto &target : assigns.operands())
       modifies.insert(target);
 
-    // create snapshots of the CARs -- must be done before havocing
+    // Create snapshots of write set CARs.
+    // This must be done before havocing the write set.
     for(const auto &car : loop_assigns.get_write_set())
     {
       auto snapshot_instructions = car.generate_snapshot_instructions();
@@ -188,7 +194,17 @@ void code_contractst::check_apply_loop_contracts(
   havoc_assigns_targetst havoc_gen(modifies, ns);
   havoc_gen.append_full_havoc_code(
     loop_head->source_location(), generated_code);
-  insert_before_swap_and_advance(goto_function.body, loop_head, generated_code);
+
+  // Add the havocing code, but only check against the enclosing scope's
+  // write set if it was manually specified.
+  if(assigns.is_nil())
+    insert_before_swap_and_advance(
+      goto_function.body,
+      loop_head,
+      add_pragma_disable_assigns_check(generated_code));
+  else
+    insert_before_swap_and_advance(
+      goto_function.body, loop_head, generated_code);
 
   // Generate: assume(invariant) just after havocing
   // We use a block scope to create a temporary assumption,
@@ -726,7 +742,6 @@ void code_contractst::instrument_assign_statement(
     instruction_it->is_assign(),
     "The first instruction of instrument_assign_statement should always be"
     " an assignment");
-
   add_inclusion_check(
     program, assigns_clause, instruction_it, instruction_it->assign_lhs());
 }
@@ -816,7 +831,9 @@ void code_contractst::instrument_call_statement(
 
     alias_checking_instructions.destructive_append(skip_program);
     insert_before_swap_and_advance(
-      body, instruction_it, alias_checking_instructions);
+      body,
+      instruction_it,
+      add_pragma_disable_assigns_check(alias_checking_instructions));
 
     // move past the call and then insert the invalidation instructions
     instruction_it++;
@@ -848,7 +865,9 @@ void code_contractst::instrument_call_statement(
 
     invalidation_instructions.destructive_append(skip_program);
     insert_before_swap_and_advance(
-      body, instruction_it, invalidation_instructions);
+      body,
+      instruction_it,
+      add_pragma_disable_assigns_check(invalidation_instructions));
 
     instruction_it--;
   }
@@ -985,6 +1004,14 @@ void code_contractst::check_frame_conditions(
 
   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;
+
+    // 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);
+
     if(instruction_it->is_decl())
     {
       // grab the declared symbol

src/goto-instrument/contracts/utils.cpp

@@ -14,6 +14,21 @@ Date: September 2021
 #include <util/pointer_expr.h>
 #include <util/pointer_predicates.h>
 
+goto_programt::instructiont &
+add_pragma_disable_assigns_check(goto_programt::instructiont &instr)
+{
+  instr.source_location_nonconst().add_pragma(
+    CONTRACT_PRAGMA_DISABLE_ASSIGNS_CHECK);
+  return instr;
+}
+
+goto_programt &add_pragma_disable_assigns_check(goto_programt &prog)
+{
+  Forall_goto_program_instructions(it, prog)
+    add_pragma_disable_assigns_check(*it);
+  return prog;
+}
+
 static void append_safe_havoc_code_for_expr(
   const source_locationt location,
   const namespacet &ns,

src/goto-instrument/contracts/utils.h

@@ -17,6 +17,8 @@ Date: September 2021
 
 #include <goto-programs/goto_model.h>
 
+#define CONTRACT_PRAGMA_DISABLE_ASSIGNS_CHECK "contracts:disable:assigns-check"
+
 /// \brief A class that overrides the low-level havocing functions in the base
 ///        utility class, to havoc only when expressions point to valid memory,
 ///        i.e. if all dereferences within an expression are valid
@@ -42,6 +44,20 @@ class havoc_if_validt : public havoc_utilst
   const namespacet &ns;
 };
 
+/// \brief Adds a pragma on a GOTO instruction to disable inclusion checking.
+///
+/// \param instr: A mutable reference to the GOTO instruction.
+/// \return The same reference after mutation (i.e., adding the pragma).
+goto_programt::instructiont &
+add_pragma_disable_assigns_check(goto_programt::instructiont &instr);
+
+/// \brief Adds pragmas on all instructions in a GOTO program
+///        to disable inclusion checking on them.
+///
+/// \param prog: A mutable reference to the GOTO program.
+/// \return The same reference after mutation (i.e., adding the pragmas).
+goto_programt &add_pragma_disable_assigns_check(goto_programt &prog);
+
 /// \brief Generate a validity check over all dereferences in an expression
 ///
 /// This function generates a formula: