From 16d3a2bd75af83bfcddab17fdac1984ebb10bc92 Mon Sep 17 00:00:00 2001 From: Fotis Koutoulakis Date: Thu, 26 Aug 2021 10:07:17 +0100 Subject: [PATCH 1/5] 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. --- jbmc/src/jbmc/Makefile | 1 + jbmc/src/jdiff/Makefile | 1 + jbmc/unit/Makefile | 1 + src/cbmc/Makefile | 1 + src/goto-checker/properties.h | 4 +- src/goto-diff/Makefile | 1 + src/goto-instrument/Makefile | 1 + src/goto-instrument/cover.cpp | 9 ++++ src/goto-instrument/cover.h | 1 + src/goto-instrument/cover_instrument.h | 20 +++++++ .../cover_instrument_assume.cpp | 52 +++++++++++++++++++ unit/Makefile | 1 + 12 files changed, 91 insertions(+), 2 deletions(-) create mode 100644 src/goto-instrument/cover_instrument_assume.cpp diff --git a/jbmc/src/jbmc/Makefile b/jbmc/src/jbmc/Makefile index aa34a1f1810..a9fc7fa445a 100644 --- a/jbmc/src/jbmc/Makefile +++ b/jbmc/src/jbmc/Makefile @@ -24,6 +24,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) \ diff --git a/jbmc/src/jdiff/Makefile b/jbmc/src/jdiff/Makefile index 4ceab462591..eed40713bef 100644 --- a/jbmc/src/jdiff/Makefile +++ b/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) \ diff --git a/jbmc/unit/Makefile b/jbmc/unit/Makefile index d18567da013..bbe89ee617c 100644 --- a/jbmc/unit/Makefile +++ b/jbmc/unit/Makefile @@ -105,6 +105,7 @@ CPROVER_LIBS =../src/java_bytecode/java_bytecode$(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) \ diff --git a/src/cbmc/Makefile b/src/cbmc/Makefile index f2e80d151a0..a4b64d9fde7 100644 --- a/src/cbmc/Makefile +++ b/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) \ diff --git a/src/goto-checker/properties.h b/src/goto-checker/properties.h index cc2ce74bb56..9a74b700fd3 100644 --- a/src/goto-checker/properties.h +++ b/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 +#include #include @@ -73,7 +73,7 @@ struct property_infot }; /// A map of property IDs to property infos -typedef std::unordered_map propertiest; +typedef std::map propertiest; /// Returns the properties in the goto model propertiest initialize_properties(const abstract_goto_modelt &); diff --git a/src/goto-diff/Makefile b/src/goto-diff/Makefile index 2b4ae9e9fea..1528e8374d2 100644 --- a/src/goto-diff/Makefile +++ b/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) \ diff --git a/src/goto-instrument/Makefile b/src/goto-instrument/Makefile index 9e0b68fb2d5..aa54b13f969 100644 --- a/src/goto-instrument/Makefile +++ b/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 \ diff --git a/src/goto-instrument/cover.cpp b/src/goto-instrument/cover.cpp index bd67daf16e0..bb0d43999b2 100644 --- a/src/goto-instrument/cover.cpp +++ b/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(symbol_table, goal_filters)); + break; + case coverage_criteriont::ASSUME: + instrumenters.push_back( + util_make_unique(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); } diff --git a/src/goto-instrument/cover.h b/src/goto-instrument/cover.h index f894c885e2f..367e94a6d89 100644 --- a/src/goto-instrument/cover.h +++ b/src/goto-instrument/cover.h @@ -41,6 +41,7 @@ class optionst; enum class coverage_criteriont { + ASSUME, LOCATION, BRANCH, DECISION, diff --git a/src/goto-instrument/cover_instrument.h b/src/goto-instrument/cover_instrument.h index a898fbe52f5..519020a9fec 100644 --- a/src/goto-instrument/cover_instrument.h +++ b/src/goto-instrument/cover_instrument.h @@ -292,4 +292,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 diff --git a/src/goto-instrument/cover_instrument_assume.cpp b/src/goto-instrument/cover_instrument_assume.cpp new file mode 100644 index 00000000000..b0098b94f9c --- /dev/null +++ b/src/goto-instrument/cover_instrument_assume.cpp @@ -0,0 +1,52 @@ +/// \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 + +/// Instrument program to check coverage of assume statements. +/// \param function_id The name of the function under instrumentation. +/// \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(); + } + } +} diff --git a/unit/Makefile b/unit/Makefile index 39591b9dd8c..730050466b4 100644 --- a/unit/Makefile +++ b/unit/Makefile @@ -221,6 +221,7 @@ BMC_DEPS =../src/cbmc/c_test_input_generator$(OBJEXT) \ ../src/goto-instrument/cover$(OBJEXT) \ ../src/goto-instrument/cover_basic_blocks$(OBJEXT) \ ../src/goto-instrument/cover_filter$(OBJEXT) \ + ../src/goto-instrument/cover_instrument_assume$(OBJEXT) \ ../src/goto-instrument/cover_instrument_branch$(OBJEXT) \ ../src/goto-instrument/cover_instrument_condition$(OBJEXT) \ ../src/goto-instrument/cover_instrument_decision$(OBJEXT) \ From ba0d13883e6e800aa9ead4d6d5db4bf514276a0f Mon Sep 17 00:00:00 2001 From: Fotis Koutoulakis Date: Thu, 2 Sep 2021 15:15:44 +0100 Subject: [PATCH 2/5] Add reference test case for `--cover assume` code. This was provided as reference for an issue described in https://github.com/diffblue/cbmc/issues/6057. --- regression/cbmc-cover/assume_assert1/assume_assert.c | 9 +++++++++ regression/cbmc-cover/assume_assert1/test.desc | 11 +++++++++++ 2 files changed, 20 insertions(+) create mode 100644 regression/cbmc-cover/assume_assert1/assume_assert.c create mode 100644 regression/cbmc-cover/assume_assert1/test.desc diff --git a/regression/cbmc-cover/assume_assert1/assume_assert.c b/regression/cbmc-cover/assume_assert1/assume_assert.c new file mode 100644 index 00000000000..0261db8fc00 --- /dev/null +++ b/regression/cbmc-cover/assume_assert1/assume_assert.c @@ -0,0 +1,9 @@ +#include + +int main() +{ + int x; + __CPROVER_assume(x > 0); + __CPROVER_assume(x < 0); + assert(0 == 1); +} diff --git a/regression/cbmc-cover/assume_assert1/test.desc b/regression/cbmc-cover/assume_assert1/test.desc new file mode 100644 index 00000000000..a8ca17a76f3 --- /dev/null +++ b/regression/cbmc-cover/assume_assert1/test.desc @@ -0,0 +1,11 @@ +CORE +assume_assert.c +--cover assume +^EXIT=0$ +^SIGNAL=0$ +^\[main.coverage.1\] file assume_assert.c line \d function main assert\(false\) before assume\(x > 0\): SATISFIED$ +^\[main.coverage.2\] file assume_assert.c line \d function main assert\(false\) after assume\(x > 0\): SATISFIED$ +^\[main.coverage.3\] file assume_assert.c line \d function main assert\(false\) before assume\(x < 0\): SATISFIED$ +^\[main.coverage.4\] file assume_assert.c line \d function main assert\(false\) after assume\(x < 0\): FAILED$ +-- +^warning: ignoring From 9b7d9e2cc5bf2ba0f58de115ba549a6057765d69 Mon Sep 17 00:00:00 2001 From: Fotis Koutoulakis Date: Mon, 6 Sep 2021 15:08:20 +0100 Subject: [PATCH 3/5] Add second test case that features assume statement hidden behind branch. --- .../cbmc-cover/assume_assert2/assume_assert.c | 20 +++++++++++++++++++ .../cbmc-cover/assume_assert2/test.desc | 9 +++++++++ 2 files changed, 29 insertions(+) create mode 100644 regression/cbmc-cover/assume_assert2/assume_assert.c create mode 100644 regression/cbmc-cover/assume_assert2/test.desc diff --git a/regression/cbmc-cover/assume_assert2/assume_assert.c b/regression/cbmc-cover/assume_assert2/assume_assert.c new file mode 100644 index 00000000000..77b2467c35e --- /dev/null +++ b/regression/cbmc-cover/assume_assert2/assume_assert.c @@ -0,0 +1,20 @@ +#include + +int main(int argc, char *argv[]) +{ + int a; + + if(a > 0) + { + assert(a > 0); + } + else if(a < 0) + { + __CPROVER_assume(a >= 0); + assert(a < 0); + } + else + { + assert(a == 0); + } +} diff --git a/regression/cbmc-cover/assume_assert2/test.desc b/regression/cbmc-cover/assume_assert2/test.desc new file mode 100644 index 00000000000..e974286f122 --- /dev/null +++ b/regression/cbmc-cover/assume_assert2/test.desc @@ -0,0 +1,9 @@ +CORE +assume_assert.c +--cover assume +^EXIT=0$ +^SIGNAL=0$ +^\[main.coverage.1\] file assume_assert.c line \d+ function main assert\(false\) before assume\(a >= 0\): SATISFIED$ +^\[main.coverage.2\] file assume_assert.c line \d+ function main assert\(false\) after assume\(a >= 0\): FAILED$ +-- +^warning: ignoring From 3514772a5304d85b46119d63bd0156bb8e7d2100 Mon Sep 17 00:00:00 2001 From: Fotis Koutoulakis Date: Mon, 6 Sep 2021 15:25:47 +0100 Subject: [PATCH 4/5] [DOCS] Add documentation for the new `--cover assume` coverage criterion. --- doc/cprover-manual/modeling-assumptions.md | 34 ++++++++++++++++++++++ doc/cprover-manual/test-suite.md | 1 + 2 files changed, 35 insertions(+) diff --git a/doc/cprover-manual/modeling-assumptions.md b/doc/cprover-manual/modeling-assumptions.md index 6d3757f393f..9c92c2a6948 100644 --- a/doc/cprover-manual/modeling-assumptions.md +++ b/doc/cprover-manual/modeling-assumptions.md @@ -71,3 +71,37 @@ int main() { This code fails, as there is a choice of x and y which results in a counterexample (any choice in which x and y are different). +## Coverage + +You can ask CBMC to give coverage information regarding `__CPROVER_assume` statements. +This is useful when you need, for example, to check which assume statements may have +led to an emptying of the search state space, resulting in `assert` statements being +vaccuously passed. + +To use that invoke CBMC with the `--cover assume` option. For example, for a file: + +```c +#include + +int main() +{ + int x; + __CPROVER_assume(x > 0); + __CPROVER_assume(x < 0); + assert(0 == 1); +} +``` + +CBMC invoked with `cbmc --cover assume test.c` will report: + +```sh +[main.1] file assume_assert.c line 6 function main assert(false) before assume(x > 0): SATISFIED +[main.2] file assume_assert.c line 6 function main assert(false) after assume(x > 0): SATISFIED +[main.3] file assume_assert.c line 7 function main assert(false) before assume(x < 0): SATISFIED +[main.4] file assume_assert.c line 7 function main assert(false) after assume(x < 0): FAILED +``` + +When an `assert(false)` statement before the assume has the property status `SATISFIED`, +but is followed by an `assert(false)` statement *after* the assume statement that has status +`FAILED`, this is an indication that this specific assume statement (on the line reported) +is one that is emptying the search space for model checking. diff --git a/doc/cprover-manual/test-suite.md b/doc/cprover-manual/test-suite.md index 31765b61055..e6c27017f1c 100644 --- a/doc/cprover-manual/test-suite.md +++ b/doc/cprover-manual/test-suite.md @@ -213,6 +213,7 @@ The table below summarizes the coverage criteria that CBMC supports. Criterion |Definition ----------|---------- assertion |For every assertion, generate a test that reaches it +assume |For every assume, generate tests before and after the assume statement to indicate coverage before and after it location |For every location, generate a test that reaches it branch |Generate a test for every branch outcome decision |Generate a test for both outcomes of every Boolean expression that is not an operand of a propositional connective From f869882dfd9cf7f5314a55bb04007ba31b04eda3 Mon Sep 17 00:00:00 2001 From: Thomas Given-Wilson Date: Wed, 8 Sep 2021 20:42:22 +0100 Subject: [PATCH 5/5] Fix Windows error by changing scope of namespace This moves a dummy namespace needed for expr2c to be created as the argument to the call. --- src/goto-instrument/cover_instrument_assume.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/goto-instrument/cover_instrument_assume.cpp b/src/goto-instrument/cover_instrument_assume.cpp index b0098b94f9c..2d09aa67ad0 100644 --- a/src/goto-instrument/cover_instrument_assume.cpp +++ b/src/goto-instrument/cover_instrument_assume.cpp @@ -21,11 +21,11 @@ void cover_assume_instrumentert::instrument( 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 assume_condition = + expr2c(i_it->get_condition(), namespacet{symbol_tablet()}); const auto comment_before = "assert(false) before assume(" + assume_condition + ")"; const auto comment_after =