From 639ef8195ce865d800bffcca853440b61f7b8e04 Mon Sep 17 00:00:00 2001 From: Nathan Chong Date: Fri, 2 Aug 2019 11:00:18 -0400 Subject: [PATCH] Add --insert-final-assert-false to goto-instrument This option takes a function name (usually the test harness entry point) and inserts `assert(false)` at the end of the function body. This assertion is *expected to fail*. If it passes then this may indicate that the test harness has inconsistent assumptions. Note that there are other reasons why the assert may pass (such as insufficient loop unwind depth). It is up to the user to interpret the results. --- .../insert-final-assert-false1/main.c | 13 ++++ .../insert-final-assert-false1/test.desc | 12 ++++ .../insert-final-assert-false2/main.c | 11 ++++ .../insert-final-assert-false2/test.desc | 12 ++++ .../insert-final-assert-false3/main.c | 14 +++++ .../insert-final-assert-false3/test.desc | 12 ++++ .../insert-final-assert-false4/main.c | 15 +++++ .../insert-final-assert-false4/test.desc | 12 ++++ .../insert-final-assert-false5/main.c | 6 ++ .../insert-final-assert-false5/test.desc | 10 ++++ src/goto-instrument/Makefile | 1 + .../goto_instrument_parse_options.cpp | 16 +++++ .../goto_instrument_parse_options.h | 2 + .../insert_final_assert_false.cpp | 60 +++++++++++++++++++ .../insert_final_assert_false.h | 59 ++++++++++++++++++ 15 files changed, 255 insertions(+) create mode 100644 regression/goto-instrument/insert-final-assert-false1/main.c create mode 100644 regression/goto-instrument/insert-final-assert-false1/test.desc create mode 100644 regression/goto-instrument/insert-final-assert-false2/main.c create mode 100644 regression/goto-instrument/insert-final-assert-false2/test.desc create mode 100644 regression/goto-instrument/insert-final-assert-false3/main.c create mode 100644 regression/goto-instrument/insert-final-assert-false3/test.desc create mode 100644 regression/goto-instrument/insert-final-assert-false4/main.c create mode 100644 regression/goto-instrument/insert-final-assert-false4/test.desc create mode 100644 regression/goto-instrument/insert-final-assert-false5/main.c create mode 100644 regression/goto-instrument/insert-final-assert-false5/test.desc create mode 100644 src/goto-instrument/insert_final_assert_false.cpp create mode 100644 src/goto-instrument/insert_final_assert_false.h diff --git a/regression/goto-instrument/insert-final-assert-false1/main.c b/regression/goto-instrument/insert-final-assert-false1/main.c new file mode 100644 index 00000000000..baf48305fec --- /dev/null +++ b/regression/goto-instrument/insert-final-assert-false1/main.c @@ -0,0 +1,13 @@ +#include + +int main() +{ + size_t n; + int *p = (int *)malloc(n); + int *q = (int *)malloc(n); + __CPROVER_assert(p, "not-null"); + __CPROVER_assert(q, "not-null"); + // the following is the same as assuming false + __CPROVER_assume(__CPROVER_POINTER_OBJECT(p) == __CPROVER_POINTER_OBJECT(q)); + return 0; +} diff --git a/regression/goto-instrument/insert-final-assert-false1/test.desc b/regression/goto-instrument/insert-final-assert-false1/test.desc new file mode 100644 index 00000000000..19e261dbbdc --- /dev/null +++ b/regression/goto-instrument/insert-final-assert-false1/test.desc @@ -0,0 +1,12 @@ +CORE +main.c +--insert-final-assert-false main +^EXIT=0$ +^SIGNAL=0$ +insert-final-assert-false \(should fail\) : SUCCESS +^VERIFICATION SUCCESSFUL$ +-- +-- +This test has a false assumption meaning the program passes vacuously. A sign +that this is the case is that verification succeeds with a false assert inserted +automatically by the --insert-final-assert-false flag. diff --git a/regression/goto-instrument/insert-final-assert-false2/main.c b/regression/goto-instrument/insert-final-assert-false2/main.c new file mode 100644 index 00000000000..9b024dda329 --- /dev/null +++ b/regression/goto-instrument/insert-final-assert-false2/main.c @@ -0,0 +1,11 @@ +#include + +int main() +{ + size_t n; + int *p = (int *)malloc(n); + int *q = (int *)malloc(n); + __CPROVER_assert(p, "not-null"); + __CPROVER_assert(q, "not-null"); + return 0; +} diff --git a/regression/goto-instrument/insert-final-assert-false2/test.desc b/regression/goto-instrument/insert-final-assert-false2/test.desc new file mode 100644 index 00000000000..9a5ade76c0d --- /dev/null +++ b/regression/goto-instrument/insert-final-assert-false2/test.desc @@ -0,0 +1,12 @@ +CORE +main.c +--insert-final-assert-false main +^EXIT=10$ +^SIGNAL=0$ +insert-final-assert-false \(should fail\) : FAILURE +^VERIFICATION FAILED$ +-- +-- +This test does not have a false assumption. A sign that this is the case is +that verification fails with a false assert inserted automatically by the +--insert-final-assert-false flag. diff --git a/regression/goto-instrument/insert-final-assert-false3/main.c b/regression/goto-instrument/insert-final-assert-false3/main.c new file mode 100644 index 00000000000..235da1bf95c --- /dev/null +++ b/regression/goto-instrument/insert-final-assert-false3/main.c @@ -0,0 +1,14 @@ +#include + +int nondet_int(); +int main() +{ + if(nondet_int()) + { + return 0; + } + else + { + return 1; + } +} diff --git a/regression/goto-instrument/insert-final-assert-false3/test.desc b/regression/goto-instrument/insert-final-assert-false3/test.desc new file mode 100644 index 00000000000..dd450318f88 --- /dev/null +++ b/regression/goto-instrument/insert-final-assert-false3/test.desc @@ -0,0 +1,12 @@ +CORE +main.c +--insert-final-assert-false main +^EXIT=10$ +^SIGNAL=0$ +insert-final-assert-false \(should fail\) : FAILURE +^VERIFICATION FAILED$ +-- +-- +This test does not have a false assumption (and has multiple return paths). A +sign that this is the case is that verification fails with a false assert +inserted automatically by the --insert-final-assert-false flag. diff --git a/regression/goto-instrument/insert-final-assert-false4/main.c b/regression/goto-instrument/insert-final-assert-false4/main.c new file mode 100644 index 00000000000..80a4be8ddfc --- /dev/null +++ b/regression/goto-instrument/insert-final-assert-false4/main.c @@ -0,0 +1,15 @@ +#include + +int nondet_int(); +int main() +{ + if(nondet_int()) + { + __CPROVER_assume(0 == 1); + return 0; + } + else + { + return 1; + } +} diff --git a/regression/goto-instrument/insert-final-assert-false4/test.desc b/regression/goto-instrument/insert-final-assert-false4/test.desc new file mode 100644 index 00000000000..3a2e18f6a7e --- /dev/null +++ b/regression/goto-instrument/insert-final-assert-false4/test.desc @@ -0,0 +1,12 @@ +CORE +main.c +--insert-final-assert-false main +^EXIT=10$ +^SIGNAL=0$ +insert-final-assert-false \(should fail\) : FAILURE +^VERIFICATION FAILED$ +-- +-- +This test has a false assumption on one of its return paths (but not both). +This shows a limitation of the --insert-final-assert-false pass since the +verification still fails with the inserted assert. diff --git a/regression/goto-instrument/insert-final-assert-false5/main.c b/regression/goto-instrument/insert-final-assert-false5/main.c new file mode 100644 index 00000000000..a069bf6aa60 --- /dev/null +++ b/regression/goto-instrument/insert-final-assert-false5/main.c @@ -0,0 +1,6 @@ +#include + +int main() +{ + return 0; +} diff --git a/regression/goto-instrument/insert-final-assert-false5/test.desc b/regression/goto-instrument/insert-final-assert-false5/test.desc new file mode 100644 index 00000000000..131b7b712ee --- /dev/null +++ b/regression/goto-instrument/insert-final-assert-false5/test.desc @@ -0,0 +1,10 @@ +CORE +main.c +--insert-final-assert-false function_that_does_not_exist +^EXIT=6$ +^SIGNAL=0$ +insert-final-assert-false: could not find function +-- +-- +This test tries to use --insert-final-assert-false on a function that does not +exist in the program. diff --git a/src/goto-instrument/Makefile b/src/goto-instrument/Makefile index 8dc28944f66..928228243f9 100644 --- a/src/goto-instrument/Makefile +++ b/src/goto-instrument/Makefile @@ -42,6 +42,7 @@ SRC = accelerate/accelerate.cpp \ goto_program2code.cpp \ havoc_loops.cpp \ horn_encoding.cpp \ + insert_final_assert_false.cpp \ interrupt.cpp \ k_induction.cpp \ loop_utils.cpp \ diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp index 6442032fc38..030a0b205bd 100644 --- a/src/goto-instrument/goto_instrument_parse_options.cpp +++ b/src/goto-instrument/goto_instrument_parse_options.cpp @@ -86,6 +86,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "function.h" #include "havoc_loops.h" #include "horn_encoding.h" +#include "insert_final_assert_false.h" #include "interrupt.h" #include "k_induction.h" #include "mmio.h" @@ -257,6 +258,20 @@ int goto_instrument_parse_optionst::doit() return CPROVER_EXIT_SUCCESS; } + if(cmdline.isset("insert-final-assert-false")) + { + log.status() << "Inserting final assert false" << messaget::eom; + bool fail = insert_final_assert_false( + goto_model, + cmdline.get_value("insert-final-assert-false"), + ui_message_handler); + if(fail) + { + return CPROVER_EXIT_INTERNAL_ERROR; + } + // otherwise, fall-through to write new binary + } + if(cmdline.isset("show-value-sets")) { do_indirect_call_and_rtti_removal(); @@ -1648,6 +1663,7 @@ void goto_instrument_parse_optionst::help() " --undefined-function-is-assume-false\n" // NOLINTNEXTLINE(whitespace/line_length) " convert each call to an undefined function to assume(false)\n" + HELP_INSERT_FINAL_ASSERT_FALSE HELP_REPLACE_FUNCTION_BODY HELP_ANSI_C_LANGUAGE "\n" diff --git a/src/goto-instrument/goto_instrument_parse_options.h b/src/goto-instrument/goto_instrument_parse_options.h index 6db5ec4fe57..769914ef5a2 100644 --- a/src/goto-instrument/goto_instrument_parse_options.h +++ b/src/goto-instrument/goto_instrument_parse_options.h @@ -31,6 +31,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "aggressive_slicer.h" #include "generate_function_bodies.h" +#include "insert_final_assert_false.h" #include "count_eloc.h" @@ -59,6 +60,7 @@ Author: Daniel Kroening, kroening@kroening.com "(max-var):(max-po-trans):(ignore-arrays)" \ "(cfg-kill)(no-dependencies)(force-loop-duplication)" \ "(call-graph)(reachable-call-graph)" \ + OPT_INSERT_FINAL_ASSERT_FALSE \ OPT_SHOW_CLASS_HIERARCHY \ "(no-po-rendering)(render-cluster-file)(render-cluster-function)" \ "(nondet-volatile)(isr):" \ diff --git a/src/goto-instrument/insert_final_assert_false.cpp b/src/goto-instrument/insert_final_assert_false.cpp new file mode 100644 index 00000000000..3871d4dfe08 --- /dev/null +++ b/src/goto-instrument/insert_final_assert_false.cpp @@ -0,0 +1,60 @@ +/*******************************************************************\ + +Module: Insert assert(false) at end of entry function + +Author: Nathan Chong, Kareem Khazem + +\*******************************************************************/ + +/// \file +/// Insert final assert false into a function + +#include "insert_final_assert_false.h" + +#include +#include + +#include +#include + +insert_final_assert_falset::insert_final_assert_falset( + message_handlert &_message_handler) + : log(_message_handler) +{ +} + +bool insert_final_assert_falset:: +operator()(goto_modelt &goto_model, const std::string &function_to_instrument) +{ + const irep_idt entry(function_to_instrument); + auto it = goto_model.goto_functions.function_map.find(entry); + if(it == goto_model.goto_functions.function_map.end()) + { + log.error() << "insert-final-assert-false: could not find function " + << "'" << function_to_instrument << "'" << messaget::eom; + return true; + } + goto_programt &entry_function = (it->second).body; + goto_programt::instructionst &instructions = entry_function.instructions; + auto instr_it = instructions.end(); + auto last_instruction = std::prev(instr_it); + DATA_INVARIANT( + last_instruction->is_end_function(), + "last instruction in function should be END_FUNCTION"); + source_locationt assert_location = last_instruction->source_location; + assert_location.set_property_class(ID_assertion); + assert_location.set_comment("insert-final-assert-false (should fail) "); + goto_programt::instructiont false_assert = + goto_programt::make_assertion(false_exprt(), assert_location); + entry_function.insert_before_swap(last_instruction, false_assert); + return false; +} + +bool insert_final_assert_false( + goto_modelt &goto_model, + const std::string &function_to_instrument, + message_handlert &message_handler) +{ + insert_final_assert_falset ifaf(message_handler); + return ifaf(goto_model, function_to_instrument); +} diff --git a/src/goto-instrument/insert_final_assert_false.h b/src/goto-instrument/insert_final_assert_false.h new file mode 100644 index 00000000000..710b3270294 --- /dev/null +++ b/src/goto-instrument/insert_final_assert_false.h @@ -0,0 +1,59 @@ +/*******************************************************************\ + +Module: Insert assert(false) at end of entry function + +Author: Nathan Chong, Kareem Khazem + +\*******************************************************************/ + +/// \file +/// Insert final assert false into a function + +/// This transform can be used to check for some cases of vacuous proofs +/// Usually the given function is the test harness / entry point +/// The instrumented assert is expected to fail +/// If it does not then this may indicate inconsistent assumptions + +#ifndef CPROVER_GOTO_INSTRUMENT_INSERT_FINAL_ASSERT_FALSE_H +#define CPROVER_GOTO_INSTRUMENT_INSERT_FINAL_ASSERT_FALSE_H + +#include + +#include + +class goto_modelt; + +class insert_final_assert_falset +{ +public: + explicit insert_final_assert_falset(message_handlert &_message_handler); + bool operator()(goto_modelt &, const std::string &); + +private: + messaget log; +}; + +/// Transform a goto program by inserting assert(false) at the end of a given +/// function \p function_to_instrument. The instrumented assert is expected +/// to fail. If it does not then this may indicate inconsistent assumptions. +/// +/// \param goto_model: The goto program to modify. +/// \param function_to_instrument: Name of the function to instrument. +/// \param message_handler: Handles logging. +/// \returns false on success +bool insert_final_assert_false( + goto_modelt &goto_model, + const std::string &function_to_instrument, + message_handlert &message_handler); + +// clang-format off +#define OPT_INSERT_FINAL_ASSERT_FALSE \ + "(insert-final-assert-false):" + +#define HELP_INSERT_FINAL_ASSERT_FALSE \ + " --insert-final-assert-false \n" \ + /* NOLINTNEXTLINE(whitespace/line_length) */ \ + " generate assert(false) at end of function\n" +// clang-format on + +#endif // CPROVER_GOTO_INSTRUMENT_INSERT_FINAL_ASSERT_FALSE_H