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