Enfold assume in an assert(false) to allow for easier debugging.

This allows for easier debugging by allowing `assume(false)`s that
end up emptying the search state space to be identified on a more
granular basis.

Author: NlightNFotis

jbmc/src/jdiff/Makefile

@@ -18,6 +18,7 @@ OBJ += ../$(CPROVER_DIR)/src/ansi-c/ansi-c$(LIBEXT) \
       ../$(CPROVER_DIR)/src/goto-instrument/cover$(OBJEXT) \
       ../$(CPROVER_DIR)/src/goto-instrument/cover_basic_blocks$(OBJEXT) \
       ../$(CPROVER_DIR)/src/goto-instrument/cover_filter$(OBJEXT) \
+      ../$(CPROVER_DIR)/src/goto-instrument/cover_instrument_assume$(OBJEXT) \
       ../$(CPROVER_DIR)/src/goto-instrument/cover_instrument_branch$(OBJEXT) \
       ../$(CPROVER_DIR)/src/goto-instrument/cover_instrument_condition$(OBJEXT) \
       ../$(CPROVER_DIR)/src/goto-instrument/cover_instrument_decision$(OBJEXT) \

src/cbmc/Makefile

@@ -26,6 +26,7 @@ OBJ += ../ansi-c/ansi-c$(LIBEXT) \
       ../goto-instrument/cover$(OBJEXT) \
       ../goto-instrument/cover_basic_blocks$(OBJEXT) \
       ../goto-instrument/cover_filter$(OBJEXT) \
+      ../goto-instrument/cover_instrument_assume$(OBJEXT) \
       ../goto-instrument/cover_instrument_branch$(OBJEXT) \
       ../goto-instrument/cover_instrument_condition$(OBJEXT) \
       ../goto-instrument/cover_instrument_decision$(OBJEXT) \

src/goto-checker/properties.h

@@ -12,7 +12,7 @@ Author: Daniel Kroening, Peter Schrammel
 #ifndef CPROVER_GOTO_CHECKER_PROPERTIES_H
 #define CPROVER_GOTO_CHECKER_PROPERTIES_H
 
-#include <unordered_map>
+#include <map>
 
 #include <goto-programs/goto_program.h>
 
@@ -73,7 +73,7 @@ struct property_infot
 };
 
 /// A map of property IDs to property infos
-typedef std::unordered_map<irep_idt, property_infot> propertiest;
+typedef std::map<irep_idt, property_infot> propertiest;
 
 /// Returns the properties in the goto model
 propertiest initialize_properties(const abstract_goto_modelt &);

src/goto-diff/Makefile

@@ -18,6 +18,7 @@ OBJ += ../ansi-c/ansi-c$(LIBEXT) \
       ../goto-instrument/cover$(OBJEXT) \
       ../goto-instrument/cover_basic_blocks$(OBJEXT) \
       ../goto-instrument/cover_filter$(OBJEXT) \
+      ../goto-instrument/cover_instrument_assume$(OBJEXT) \
       ../goto-instrument/cover_instrument_branch$(OBJEXT) \
       ../goto-instrument/cover_instrument_condition$(OBJEXT) \
       ../goto-instrument/cover_instrument_decision$(OBJEXT) \

src/goto-instrument/Makefile

@@ -24,6 +24,7 @@ SRC = accelerate/accelerate.cpp \
       cover.cpp \
       cover_basic_blocks.cpp \
       cover_filter.cpp \
+      cover_instrument_assume.cpp \
       cover_instrument_branch.cpp \
       cover_instrument_condition.cpp \
       cover_instrument_decision.cpp \

src/goto-instrument/cover.cpp

@@ -99,6 +99,10 @@ void cover_instrumenterst::add_from_criterion(
   case coverage_criteriont::COVER:
     instrumenters.push_back(
       util_make_unique<cover_cover_instrumentert>(symbol_table, goal_filters));
+    break;
+  case coverage_criteriont::ASSUME:
+    instrumenters.push_back(
+      util_make_unique<cover_assume_instrumentert>(symbol_table, goal_filters));
   }
 }
 
@@ -126,6 +130,8 @@ parse_coverage_criterion(const std::string &criterion_string)
     c = coverage_criteriont::MCDC;
   else if(criterion_string == "cover")
     c = coverage_criteriont::COVER;
+  else if(criterion_string == "assume")
+    c = coverage_criteriont::ASSUME;
   else
   {
     std::stringstream s;
@@ -201,6 +207,9 @@ cover_configt get_cover_config(
 
     if(c == coverage_criteriont::ASSERTION)
       cover_config.keep_assertions = true;
+    // Make sure that existing assertions don't get replaced by assumes
+    else if(c == coverage_criteriont::ASSUME)
+      cover_config.keep_assertions = true;
 
     instrumenters.add_from_criterion(c, symbol_table, *goal_filters);
   }

src/goto-instrument/cover.h

@@ -41,6 +41,7 @@ class optionst;
 
 enum class coverage_criteriont
 {
+  ASSUME,
   LOCATION,
   BRANCH,
   DECISION,

src/goto-instrument/cover_instrument.h

@@ -290,4 +290,24 @@ void cover_instrument_end_of_function(
   goto_programt &goto_program,
   const cover_instrumenter_baset::assertion_factoryt &);
 
+// assume-instructions instrumenter.
+class cover_assume_instrumentert : public cover_instrumenter_baset
+{
+public:
+  cover_assume_instrumentert(
+    const symbol_tablet &_symbol_table,
+    const goal_filterst &_goal_filters)
+    : cover_instrumenter_baset(_symbol_table, _goal_filters, "location")
+  {
+  }
+
+protected:
+  void instrument(
+    const irep_idt &,
+    goto_programt &,
+    goto_programt::targett &,
+    const cover_blocks_baset &,
+    const assertion_factoryt &) const override;
+};
+
 #endif // CPROVER_GOTO_INSTRUMENT_COVER_INSTRUMENT_H

src/goto-instrument/cover_instrument_assume.cpp

@@ -0,0 +1,51 @@
+/// \file cover_instrument_assume.cpp
+/// Author: Diffblue Ltd.
+/// Coverage Instrumentation for ASSUME instructions.
+
+#include "cover_instrument.h"
+
+#include "ansi-c/expr2c.h"
+#include "goto-programs/goto_program.h"
+#include "util/std_expr.h"
+#include <util/namespace.h>
+
+/// Instrument program to check coverage of assume statements.
+/// \param goto_program The goto-program (function under instrumentation).
+/// \param i_it The current instruction (instruction under instrumentation).
+/// \param make_assertion The assertion generator function.
+void cover_assume_instrumentert::instrument(
+  const irep_idt &function_id,
+  goto_programt &goto_program,
+  goto_programt::targett &i_it,
+  const cover_blocks_baset &,
+  const assertion_factoryt &make_assertion) const
+{
+  namespacet ns{symbol_tablet()};
+  if(i_it->is_assume())
+  {
+    const auto location = i_it->source_location;
+    const auto assume_condition = expr2c(i_it->get_condition(), ns);
+    const auto comment_before =
+      "assert(false) before assume(" + assume_condition + ")";
+    const auto comment_after =
+      "assert(false) after assume(" + assume_condition + ")";
+
+    const auto assert_before = make_assertion(false_exprt{}, location);
+    goto_programt::targett t = goto_program.insert_before(i_it, assert_before);
+    initialize_source_location(t, comment_before, function_id);
+
+    const auto assert_after = make_assertion(false_exprt{}, location);
+    t = goto_program.insert_after(i_it, assert_after);
+    initialize_source_location(t, comment_after, function_id);
+  }
+  // Otherwise, skip existing assertions.
+  else if(i_it->is_assert())
+  {
+    const auto location = i_it->source_location;
+    // Filter based on if assertion was added by us as part of instrumentation.
+    if(location.get_property_class() != "coverage")
+    {
+      i_it->turn_into_skip();
+    }
+  }
+}