Remove original_loop_number from instructiont

We now use a map in `code_contractst` to store oringinal loop
numbers.

Author: qinheping

src/goto-instrument/contracts/contracts.cpp

@@ -59,6 +59,7 @@ void code_contractst::check_apply_loop_contracts(
   const irep_idt &mode)
 {
   const auto loop_head_location = loop_head->source_location();
+  const unsigned loop_number = loop_end->loop_number;
 
   // Vector representing a (possibly multidimensional) decreases clause
   const auto &decreases_clause_exprs = decreases_clause.operands();
@@ -294,12 +295,6 @@ void code_contractst::check_apply_loop_contracts(
   // Generate havocing code for assignment targets.
   havoc_assigns_targetst havoc_gen(to_havoc, ns);
   havoc_gen.append_full_havoc_code(loop_head_location, pre_loop_head_instrs);
-  // Add loop number to the havoc_code
-  for(auto &havoc_instr : pre_loop_head_instrs.instructions)
-  {
-    if(is_loop_havoc(havoc_instr))
-      havoc_instr.original_loop_number = loop_end->loop_number;
-  }
 
   // Insert the second block of pre_loop_head_instrs: the havocing code.
   // We do not `add_pragma_disable_assigns_check`,
@@ -446,6 +441,28 @@ void code_contractst::check_apply_loop_contracts(
     loop_end,
     add_pragma_disable_assigns_check(pre_loop_end_instrs));
 
+  // Record original loop number for some instrumented instructions.
+  for(goto_programt::const_targett it_instr =
+        goto_function.body.instructions.begin();
+      it_instr != goto_function.body.instructions.end();
+      it_instr++)
+  {
+    // Don't override original loop numbers.
+    if(original_loop_number_map.count(it_instr) != 0)
+      continue;
+
+    // Store loop number for
+    // ASSIGN ENTERED_LOOP = TRUE
+    if(
+      is_assignment_to_instrumented_variable(it_instr, ENTERED_LOOP) &&
+      it_instr->assign_rhs() == true_exprt())
+      original_loop_number_map[it_instr] = loop_number;
+
+    // Store loop number for loop havoc.
+    if(is_loop_havoc(*it_instr))
+      original_loop_number_map[it_instr] = loop_number;
+  }
+
   // change the back edge into assume(false) or assume(guard)
   loop_end->turn_into_assume();
   loop_end->condition_nonconst() = boolean_negate(loop_end->condition());

src/goto-instrument/contracts/contracts.h

@@ -122,6 +122,12 @@ class code_contractst
   symbol_tablet &get_symbol_table();
   goto_functionst &get_goto_functions();
 
+  std::unordered_map<goto_programt::const_targett, unsigned, const_target_hash>
+  get_original_loop_number_map() const
+  {
+    return original_loop_number_map;
+  }
+
   namespacet ns;
 
 protected:
@@ -137,6 +143,13 @@ class code_contractst
   /// Name of loops we are going to unwind.
   std::list<std::string> loop_names;
 
+  /// Store the map from instrumented instructions for loop contracts to their
+  /// original loop numbers. Following instrumented instructions are stored.
+  /// 1. loop-havoc   ---   begin of transformed loops
+  /// 2. ASSIGN ENTERED_LOOP = TRUE   ---   end of transformed loops
+  std::unordered_map<goto_programt::const_targett, unsigned, const_target_hash>
+    original_loop_number_map;
+
 public:
   /// \brief Enforce contract of a single function
   void enforce_contract(const irep_idt &function);

src/goto-programs/goto_program.h

@@ -541,10 +541,6 @@ class goto_programt
     /// Number unique per function to identify loops
     unsigned loop_number = 0;
 
-    /// We record the original loop number for some instrumended instructions
-    /// so that we know which loop they are transformed from.
-    optionalt<unsigned> original_loop_number;
-
     /// A number to identify branch targets.
     /// This is \ref nil_target if it's not a target.
     unsigned target_number = nil_target;

src/goto-synthesizer/cegis_verifier.cpp

@@ -154,15 +154,58 @@ optionalt<loop_idt> cegis_verifiert::get_cause_loop_id(
         from.has_value() && to.has_value() &&
         dependence_graph.is_flow_dependent(from.value(), to.value()))
       {
-        result =
-          loop_idt(step.function_id, step.pc->original_loop_number.value());
+        result = loop_idt(step.function_id, original_loop_number_map[step.pc]);
         return result;
       }
     }
   }
   return result;
 }
 
+bool cegis_verifiert::is_instruction_in_transfomed_loop(
+  const loop_idt &loop_id,
+  const goto_functiont &function,
+  unsigned location_number_of_target)
+{
+  // The loop body after transformation are instructions from
+  // loop havocing instructions
+  // to
+  // loop end of transformed code.
+  unsigned location_number_of_havocing = 0;
+
+  for(goto_programt::const_targett it = function.body.instructions.begin();
+      it != function.body.instructions.end();
+      ++it)
+  {
+    // Record the location number of the begin of a transformed loop.
+    if(
+      is_loop_havoc(*it) && original_loop_number_map[it] == loop_id.loop_number)
+    {
+      location_number_of_havocing = it->location_number;
+    }
+
+    // Reach the end of a transformed loop.
+    if(
+      is_transformed_loop_end(it) &&
+      original_loop_number_map[it] == loop_id.loop_number)
+    {
+      INVARIANT(
+        location_number_of_havocing != 0,
+        "We must have entered the transformed loop before reaching the end");
+
+      // Check if `location_number_of_target` is between the begin and the end
+      // of the transformed loop.
+      if((location_number_of_havocing < location_number_of_target &&
+          location_number_of_target < it->location_number))
+      {
+        return true;
+      }
+    }
+  }
+
+  return false;
+}
+
 cext cegis_verifiert::build_cex(
   const goto_tracet &goto_trace,
   const source_locationt &loop_entry_loc)
@@ -391,6 +434,7 @@ optionalt<cext> cegis_verifiert::verify()
   // Apply loop contracts we annotated.
   code_contractst cont(goto_model, log);
   cont.apply_loop_contracts();
+  original_loop_number_map = cont.get_original_loop_number_map();
 
   // Get the checker same as CBMC api without any flag.
   // TODO: replace the checker with CBMC api once it is implemented.

src/goto-synthesizer/cegis_verifier.h

@@ -131,13 +131,25 @@ class cegis_verifiert
     const goto_tracet &goto_trace,
     const source_locationt &loop_entry_loc);
 
+  /// Decide whether the target instruction is in the body of the transformed
+  /// loop specified by `loop_id`.
+  bool is_instruction_in_transfomed_loop(
+    const loop_idt &loop_id,
+    const goto_functiont &function,
+    unsigned location_number_of_target);
+
   const invariant_mapt &invariant_candidates;
   goto_modelt &goto_model;
   messaget log;
 
   /// Map from function names to original functions. It is used to
   /// restore functions with annotated loops to original functions.
   std::unordered_map<irep_idt, goto_programt> original_functions;
+
+  /// Map from instrumented instructions for loop contracts to their
+  /// original loop numbers. Returned by `code_contractst`
+  std::unordered_map<goto_programt::const_targett, unsigned, const_target_hash>
+    original_loop_number_map;
 };
 
 #endif // CPROVER_GOTO_SYNTHESIZER_CEGIS_VERIFIER_H

src/goto-synthesizer/synthesizer_utils.cpp

@@ -116,45 +116,6 @@ void annotate_invariants(
   }
 }
 
-bool is_instruction_in_transfomed_loop(
-  const loop_idt &loop_id,
-  const goto_functiont &function,
-  unsigned location_number_of_target)
-{
-  // The loop body after transformation are instructions from
-  // loop havocing instructions
-  // to
-  // loop end of transformed code.
-
-  unsigned location_number_of_havocing = 0;
-
-  for(goto_programt::const_targett it = function.body.instructions.begin();
-      it != function.body.instructions.end();
-      ++it)
-  {
-    // Record the location number of the begin of a transformed loop.
-    if(is_loop_havoc(*it) && it->loop_number == loop_id.loop_number)
-    {
-      location_number_of_havocing = it->location_number;
-    }
-
-    // Reach the end of a transformed loop.
-    if(is_transformed_loop_end(it) && it->loop_number == loop_id.loop_number)
-    {
-      // Check if `location_number_of_target` is between the begin and the end
-      // of the transformed loop.
-
-      if((location_number_of_havocing < location_number_of_target &&
-          location_number_of_target < it->location_number))
-      {
-        return true;
-      }
-    }
-  }
-
-  return false;
-}
-
 invariant_mapt combine_in_and_post_invariant_clauses(
   const invariant_mapt &in_clauses,
   const invariant_mapt &post_clauses,

src/goto-synthesizer/synthesizer_utils.h

@@ -51,13 +51,6 @@ void annotate_invariants(
   const invariant_mapt &invariant_map,
   goto_modelt &goto_model);
 
-/// Decide whether the target instruction is in the body of the transformed loop
-/// specified by `loop_id`.
-bool is_instruction_in_transfomed_loop(
-  const loop_idt &loop_id,
-  const goto_functiont &function,
-  unsigned location_number_of_target);
-
 /// Combine invariant of form
 /// (in_inv || !guard) && (!guard -> pos_inv)
 invariant_mapt combine_in_and_post_invariant_clauses(