Make assertions made by existing instrumenters customisable

This allows for additional logic to be added to the existing coverage
instrumenters. For example instead of generating an assertion of the
form `assert(guard)` we want to be able to generate an assertion of the
form `assert(!in_region_of_interest || guard)`. These customised forms
of instrumentation will still add assertions in the same locations and
be based on top of the original expressions.

Author: thomasspriggs

src/goto-instrument/cover.cpp

@@ -30,12 +30,17 @@ Date: May 2016
 /// \param mode: mode of the function to instrument (for instance ID_C or
 ///   ID_java)
 /// \param message_handler: a message handler
-void instrument_cover_goals(
+/// \param make_assertion: A function which takes an expression, with a source
+///   location and makes an assertion based on that expression. The expression
+///   asserted is expected to include the expression passed in, but may include
+///   other additional conditions.
+static void instrument_cover_goals(
   const irep_idt &function_id,
   goto_programt &goto_program,
   const cover_instrumenterst &instrumenters,
   const irep_idt &mode,
-  message_handlert &message_handler)
+  message_handlert &message_handler,
+  const cover_instrumenter_baset::assertion_factoryt &make_assertion)
 {
   const std::unique_ptr<cover_blocks_baset> basic_blocks =
     mode == ID_java ? std::unique_ptr<cover_blocks_baset>(
@@ -45,7 +50,7 @@ void instrument_cover_goals(
 
   basic_blocks->report_block_anomalies(
     function_id, goto_program, message_handler);
-  instrumenters(function_id, goto_program, *basic_blocks);
+  instrumenters(function_id, goto_program, *basic_blocks, make_assertion);
 }
 
 /// Create and add an instrumenter based on the given criterion
@@ -309,15 +314,17 @@ static void instrument_cover_goals(
       function.body,
       cover_config.cover_instrumenters,
       function_symbol.mode,
-      message_handler);
+      message_handler,
+      cover_config.make_assertion);
     changed = true;
   }
 
   if(
     cover_config.traces_must_terminate &&
     function_symbol.name == goto_functionst::entry_point())
   {
-    cover_instrument_end_of_function(function_symbol.name, function.body);
+    cover_instrument_end_of_function(
+      function_symbol.name, function.body, cover_config.make_assertion);
     changed = true;
   }
 

src/goto-instrument/cover.h

@@ -44,6 +44,8 @@ struct cover_configt
   std::unique_ptr<goal_filterst> goal_filters =
     util_make_unique<goal_filterst>();
   cover_instrumenterst cover_instrumenters;
+  cover_instrumenter_baset::assertion_factoryt make_assertion =
+    goto_programt::make_assertion;
 };
 
 void instrument_cover_goals(

src/goto-instrument/cover_instrument.h

@@ -36,18 +36,36 @@ class cover_instrumenter_baset
   {
   }
 
+  /// The type of function used to make goto_program assertions.
+  using assertion_factoryt = std::function<
+    goto_programt::instructiont(const exprt &, const source_locationt &)>;
+  static_assert(
+    std::is_same<
+      assertion_factoryt,
+      std::function<decltype(goto_programt::make_assertion)>>::value,
+    "`assertion_factoryt` is expected to have the same type as "
+    "`goto_programt::make_assertion`.");
+
   /// Instruments a goto program
   /// \param function_id: name of \p goto_program
   /// \param goto_program: a goto program
   /// \param basic_blocks: detected basic blocks
+  /// \param make_assertion: A function which makes goto program assertions.
+  ///    This parameter may be used to customise the expressions asserted.
   void operator()(
     const irep_idt &function_id,
     goto_programt &goto_program,
-    const cover_blocks_baset &basic_blocks) const
+    const cover_blocks_baset &basic_blocks,
+    const assertion_factoryt &make_assertion) const
   {
     Forall_goto_program_instructions(i_it, goto_program)
     {
-      instrument(function_id, goto_program, i_it, basic_blocks);
+      instrument(
+        function_id,
+        goto_program,
+        i_it,
+        basic_blocks,
+        make_assertion);
     }
   }
 
@@ -63,7 +81,9 @@ class cover_instrumenter_baset
     const irep_idt &function_id,
     goto_programt &,
     goto_programt::targett &,
-    const cover_blocks_baset &) const = 0;
+    const cover_blocks_baset &,
+    const assertion_factoryt &)
+    const = 0;
 
   void initialize_source_location(
     goto_programt::targett t,
@@ -96,13 +116,16 @@ class cover_instrumenterst
   /// \param function_id: name of \p goto_program
   /// \param goto_program: a goto program
   /// \param basic_blocks: detected basic blocks of the goto program
+  /// \param make_assertion: A function which makes goto program assertions.
+  ///    This parameter may be used to customise the expressions asserted.
   void operator()(
     const irep_idt &function_id,
     goto_programt &goto_program,
-    const cover_blocks_baset &basic_blocks) const
+    const cover_blocks_baset &basic_blocks,
+    const cover_instrumenter_baset::assertion_factoryt &make_assertion) const
   {
     for(const auto &instrumenter : instrumenters)
-      (*instrumenter)(function_id, goto_program, basic_blocks);
+      (*instrumenter)(function_id, goto_program, basic_blocks, make_assertion);
   }
 
 private:
@@ -125,7 +148,8 @@ class cover_location_instrumentert : public cover_instrumenter_baset
     const irep_idt &function_id,
     goto_programt &,
     goto_programt::targett &,
-    const cover_blocks_baset &) const override;
+    const cover_blocks_baset &,
+    const assertion_factoryt &) const override;
 };
 
 /// Branch coverage instrumenter
@@ -144,7 +168,8 @@ class cover_branch_instrumentert : public cover_instrumenter_baset
     const irep_idt &function_id,
     goto_programt &,
     goto_programt::targett &,
-    const cover_blocks_baset &) const override;
+    const cover_blocks_baset &,
+    const assertion_factoryt &) const override;
 };
 
 /// Condition coverage instrumenter
@@ -163,7 +188,8 @@ class cover_condition_instrumentert : public cover_instrumenter_baset
     const irep_idt &function_id,
     goto_programt &,
     goto_programt::targett &,
-    const cover_blocks_baset &) const override;
+    const cover_blocks_baset &,
+    const assertion_factoryt &) const override;
 };
 
 /// Decision coverage instrumenter
@@ -182,7 +208,8 @@ class cover_decision_instrumentert : public cover_instrumenter_baset
     const irep_idt &function_id,
     goto_programt &,
     goto_programt::targett &,
-    const cover_blocks_baset &) const override;
+    const cover_blocks_baset &,
+    const assertion_factoryt &) const override;
 };
 
 /// MC/DC coverage instrumenter
@@ -201,7 +228,8 @@ class cover_mcdc_instrumentert : public cover_instrumenter_baset
     const irep_idt &function_id,
     goto_programt &,
     goto_programt::targett &,
-    const cover_blocks_baset &) const override;
+    const cover_blocks_baset &,
+    const assertion_factoryt &) const override;
 };
 
 /// Path coverage instrumenter
@@ -220,7 +248,8 @@ class cover_path_instrumentert : public cover_instrumenter_baset
     const irep_idt &function_id,
     goto_programt &,
     goto_programt::targett &,
-    const cover_blocks_baset &) const override;
+    const cover_blocks_baset &,
+    const assertion_factoryt &) const override;
 };
 
 /// Assertion coverage instrumenter
@@ -239,7 +268,8 @@ class cover_assertion_instrumentert : public cover_instrumenter_baset
     const irep_idt &function_id,
     goto_programt &,
     goto_programt::targett &,
-    const cover_blocks_baset &) const override;
+    const cover_blocks_baset &,
+    const assertion_factoryt &) const override;
 };
 
 /// __CPROVER_cover coverage instrumenter
@@ -258,11 +288,13 @@ class cover_cover_instrumentert : public cover_instrumenter_baset
     const irep_idt &function_id,
     goto_programt &,
     goto_programt::targett &,
-    const cover_blocks_baset &) const override;
+    const cover_blocks_baset &,
+    const assertion_factoryt &) const override;
 };
 
 void cover_instrument_end_of_function(
   const irep_idt &function_id,
-  goto_programt &goto_program);
+  goto_programt &goto_program,
+  const cover_instrumenter_baset::assertion_factoryt &);
 
 #endif // CPROVER_GOTO_INSTRUMENT_COVER_INSTRUMENT_H

src/goto-instrument/cover_instrument_branch.cpp

@@ -17,7 +17,8 @@ void cover_branch_instrumentert::instrument(
   const irep_idt &function_id,
   goto_programt &goto_program,
   goto_programt::targett &i_it,
-  const cover_blocks_baset &basic_blocks) const
+  const cover_blocks_baset &basic_blocks,
+  const assertion_factoryt &make_assertion) const
 {
   if(is_non_cover_assertion(i_it))
     i_it->turn_into_skip();
@@ -40,7 +41,7 @@ void cover_branch_instrumentert::instrument(
     source_locationt source_location = i_it->source_location;
 
     goto_programt::targett t = goto_program.insert_before(
-      i_it, goto_programt::make_assertion(false_exprt(), source_location));
+      i_it, make_assertion(false_exprt(), source_location));
     initialize_source_location(t, comment, function_id);
   }
 
@@ -55,11 +56,11 @@ void cover_branch_instrumentert::instrument(
     source_locationt source_location = i_it->source_location;
 
     goto_program.insert_before_swap(i_it);
-    *i_it = goto_programt::make_assertion(not_exprt(guard), source_location);
+    *i_it = make_assertion(not_exprt(guard), source_location);
     initialize_source_location(i_it, true_comment, function_id);
 
     goto_program.insert_before_swap(i_it);
-    *i_it = goto_programt::make_assertion(guard, source_location);
+    *i_it = make_assertion(guard, source_location);
     initialize_source_location(i_it, false_comment, function_id);
 
     std::advance(i_it, 2);

src/goto-instrument/cover_instrument_condition.cpp

@@ -20,7 +20,8 @@ void cover_condition_instrumentert::instrument(
   const irep_idt &function_id,
   goto_programt &goto_program,
   goto_programt::targett &i_it,
-  const cover_blocks_baset &) const
+  const cover_blocks_baset &,
+  const assertion_factoryt &make_assertion) const
 {
   if(is_non_cover_assertion(i_it))
     i_it->turn_into_skip();
@@ -38,12 +39,12 @@ void cover_condition_instrumentert::instrument(
 
       const std::string comment_t = "condition '" + c_string + "' true";
       goto_program.insert_before_swap(i_it);
-      *i_it = goto_programt::make_assertion(c, source_location);
+      *i_it = make_assertion(c, source_location);
       initialize_source_location(i_it, comment_t, function_id);
 
       const std::string comment_f = "condition '" + c_string + "' false";
       goto_program.insert_before_swap(i_it);
-      *i_it = goto_programt::make_assertion(not_exprt(c), source_location);
+      *i_it = make_assertion(not_exprt(c), source_location);
       initialize_source_location(i_it, comment_f, function_id);
     }
 

src/goto-instrument/cover_instrument_decision.cpp

@@ -19,7 +19,8 @@ void cover_decision_instrumentert::instrument(
   const irep_idt &function_id,
   goto_programt &goto_program,
   goto_programt::targett &i_it,
-  const cover_blocks_baset &) const
+  const cover_blocks_baset &,
+  const assertion_factoryt &make_assertion) const
 {
   if(is_non_cover_assertion(i_it))
     i_it->turn_into_skip();
@@ -37,12 +38,12 @@ void cover_decision_instrumentert::instrument(
 
       const std::string comment_t = "decision '" + d_string + "' true";
       goto_program.insert_before_swap(i_it);
-      *i_it = goto_programt::make_assertion(d, source_location);
+      *i_it = make_assertion(d, source_location);
       initialize_source_location(i_it, comment_t, function_id);
 
       const std::string comment_f = "decision '" + d_string + "' false";
       goto_program.insert_before_swap(i_it);
-      *i_it = goto_programt::make_assertion(not_exprt(d), source_location);
+      *i_it = make_assertion(not_exprt(d), source_location);
       initialize_source_location(i_it, comment_f, function_id);
     }
 

src/goto-instrument/cover_instrument_location.cpp

@@ -18,7 +18,8 @@ void cover_location_instrumentert::instrument(
   const irep_idt &function_id,
   goto_programt &goto_program,
   goto_programt::targett &i_it,
-  const cover_blocks_baset &basic_blocks) const
+  const cover_blocks_baset &basic_blocks,
+  const assertion_factoryt &make_assertion) const
 {
   if(is_non_cover_assertion(i_it))
     i_it->turn_into_skip();
@@ -40,7 +41,7 @@ void cover_location_instrumentert::instrument(
       const std::string comment =
         "block " + b + " (lines " + source_lines + ")";
       goto_program.insert_before_swap(i_it);
-      *i_it = goto_programt::make_assertion(false_exprt(), source_location);
+      *i_it = make_assertion(false_exprt(), source_location);
       initialize_source_location(i_it, comment, function_id);
       i_it++;
     }

src/goto-instrument/cover_instrument_mcdc.cpp

@@ -623,7 +623,8 @@ void cover_mcdc_instrumentert::instrument(
   const irep_idt &function_id,
   goto_programt &goto_program,
   goto_programt::targett &i_it,
-  const cover_blocks_baset &) const
+  const cover_blocks_baset &,
+  const assertion_factoryt &make_assertion) const
 {
   if(is_non_cover_assertion(i_it))
     i_it->turn_into_skip();
@@ -661,15 +662,15 @@ void cover_mcdc_instrumentert::instrument(
 
       std::string comment_t = description + " '" + p_string + "' true";
       goto_program.insert_before_swap(i_it);
-      *i_it = goto_programt::make_assertion(not_exprt(p), source_location);
+      *i_it = make_assertion(not_exprt(p), source_location);
       i_it->source_location.set_comment(comment_t);
       i_it->source_location.set(ID_coverage_criterion, coverage_criterion);
       i_it->source_location.set_property_class(property_class);
       i_it->source_location.set_function(function_id);
 
       std::string comment_f = description + " '" + p_string + "' false";
       goto_program.insert_before_swap(i_it);
-      *i_it = goto_programt::make_assertion(p, source_location);
+      *i_it = make_assertion(p, source_location);
       i_it->source_location.set_comment(comment_f);
       i_it->source_location.set(ID_coverage_criterion, coverage_criterion);
       i_it->source_location.set_property_class(property_class);
@@ -694,7 +695,7 @@ void cover_mcdc_instrumentert::instrument(
         "MC/DC independence condition '" + p_string + "'";
 
       goto_program.insert_before_swap(i_it);
-      *i_it = goto_programt::make_assertion(not_exprt(p), source_location);
+      *i_it = make_assertion(not_exprt(p), source_location);
       i_it->source_location.set_comment(description);
       i_it->source_location.set(ID_coverage_criterion, coverage_criterion);
       i_it->source_location.set_property_class(property_class);