Skip to content

Commit 8c7609e

Browse files
karkhazkarkhaz
authored
Merge pull request #4985 from nchong-at-aws/insert-final-assert-false-pass
Insert final assert false pass
2 parents 3e42990 + 639ef81 commit 8c7609e

File tree

15 files changed

+255
-0
lines changed

15 files changed

+255
-0
lines changed

Diff for: ‎regression/goto-instrument/insert-final-assert-false1/main.c

+13
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
#include <stdlib.h>
2+
3+
int main()
4+
{
5+
size_t n;
6+
int *p = (int *)malloc(n);
7+
int *q = (int *)malloc(n);
8+
__CPROVER_assert(p, "not-null");
9+
__CPROVER_assert(q, "not-null");
10+
// the following is the same as assuming false
11+
__CPROVER_assume(__CPROVER_POINTER_OBJECT(p) == __CPROVER_POINTER_OBJECT(q));
12+
return 0;
13+
}

Diff for: ‎regression/goto-instrument/insert-final-assert-false1/test.desc

+12
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
CORE
2+
main.c
3+
--insert-final-assert-false main
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
insert-final-assert-false \(should fail\) : SUCCESS
7+
^VERIFICATION SUCCESSFUL$
8+
--
9+
--
10+
This test has a false assumption meaning the program passes vacuously. A sign
11+
that this is the case is that verification succeeds with a false assert inserted
12+
automatically by the --insert-final-assert-false flag.

Diff for: ‎regression/goto-instrument/insert-final-assert-false2/main.c

+11
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
#include <stdlib.h>
2+
3+
int main()
4+
{
5+
size_t n;
6+
int *p = (int *)malloc(n);
7+
int *q = (int *)malloc(n);
8+
__CPROVER_assert(p, "not-null");
9+
__CPROVER_assert(q, "not-null");
10+
return 0;
11+
}

Diff for: ‎regression/goto-instrument/insert-final-assert-false2/test.desc

+12
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
CORE
2+
main.c
3+
--insert-final-assert-false main
4+
^EXIT=10$
5+
^SIGNAL=0$
6+
insert-final-assert-false \(should fail\) : FAILURE
7+
^VERIFICATION FAILED$
8+
--
9+
--
10+
This test does not have a false assumption. A sign that this is the case is
11+
that verification fails with a false assert inserted automatically by the
12+
--insert-final-assert-false flag.

Diff for: ‎regression/goto-instrument/insert-final-assert-false3/main.c

+14
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
#include <stdlib.h>
2+
3+
int nondet_int();
4+
int main()
5+
{
6+
if(nondet_int())
7+
{
8+
return 0;
9+
}
10+
else
11+
{
12+
return 1;
13+
}
14+
}

Diff for: ‎regression/goto-instrument/insert-final-assert-false3/test.desc

+12
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
CORE
2+
main.c
3+
--insert-final-assert-false main
4+
^EXIT=10$
5+
^SIGNAL=0$
6+
insert-final-assert-false \(should fail\) : FAILURE
7+
^VERIFICATION FAILED$
8+
--
9+
--
10+
This test does not have a false assumption (and has multiple return paths). A
11+
sign that this is the case is that verification fails with a false assert
12+
inserted automatically by the --insert-final-assert-false flag.

Diff for: ‎regression/goto-instrument/insert-final-assert-false4/main.c

+15
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,15 @@
1+
#include <stdlib.h>
2+
3+
int nondet_int();
4+
int main()
5+
{
6+
if(nondet_int())
7+
{
8+
__CPROVER_assume(0 == 1);
9+
return 0;
10+
}
11+
else
12+
{
13+
return 1;
14+
}
15+
}

Diff for: ‎regression/goto-instrument/insert-final-assert-false4/test.desc

+12
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
CORE
2+
main.c
3+
--insert-final-assert-false main
4+
^EXIT=10$
5+
^SIGNAL=0$
6+
insert-final-assert-false \(should fail\) : FAILURE
7+
^VERIFICATION FAILED$
8+
--
9+
--
10+
This test has a false assumption on one of its return paths (but not both).
11+
This shows a limitation of the --insert-final-assert-false pass since the
12+
verification still fails with the inserted assert.

Diff for: ‎regression/goto-instrument/insert-final-assert-false5/main.c

+6
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,6 @@
1+
#include <stdlib.h>
2+
3+
int main()
4+
{
5+
return 0;
6+
}

Diff for: ‎regression/goto-instrument/insert-final-assert-false5/test.desc

+10
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
CORE
2+
main.c
3+
--insert-final-assert-false function_that_does_not_exist
4+
^EXIT=6$
5+
^SIGNAL=0$
6+
insert-final-assert-false: could not find function
7+
--
8+
--
9+
This test tries to use --insert-final-assert-false on a function that does not
10+
exist in the program.

Diff for: ‎src/goto-instrument/Makefile

+1
Original file line numberDiff line numberDiff line change
@@ -42,6 +42,7 @@ SRC = accelerate/accelerate.cpp \
4242
goto_program2code.cpp \
4343
havoc_loops.cpp \
4444
horn_encoding.cpp \
45+
insert_final_assert_false.cpp \
4546
interrupt.cpp \
4647
k_induction.cpp \
4748
loop_utils.cpp \

Diff for: ‎src/goto-instrument/goto_instrument_parse_options.cpp

+16
Original file line numberDiff line numberDiff line change
@@ -86,6 +86,7 @@ Author: Daniel Kroening, [email protected]
8686
#include "function.h"
8787
#include "havoc_loops.h"
8888
#include "horn_encoding.h"
89+
#include "insert_final_assert_false.h"
8990
#include "interrupt.h"
9091
#include "k_induction.h"
9192
#include "mmio.h"
@@ -257,6 +258,20 @@ int goto_instrument_parse_optionst::doit()
257258
return CPROVER_EXIT_SUCCESS;
258259
}
259260

261+
if(cmdline.isset("insert-final-assert-false"))
262+
{
263+
log.status() << "Inserting final assert false" << messaget::eom;
264+
bool fail = insert_final_assert_false(
265+
goto_model,
266+
cmdline.get_value("insert-final-assert-false"),
267+
ui_message_handler);
268+
if(fail)
269+
{
270+
return CPROVER_EXIT_INTERNAL_ERROR;
271+
}
272+
// otherwise, fall-through to write new binary
273+
}
274+
260275
if(cmdline.isset("show-value-sets"))
261276
{
262277
do_indirect_call_and_rtti_removal();
@@ -1648,6 +1663,7 @@ void goto_instrument_parse_optionst::help()
16481663
" --undefined-function-is-assume-false\n"
16491664
// NOLINTNEXTLINE(whitespace/line_length)
16501665
" convert each call to an undefined function to assume(false)\n"
1666+
HELP_INSERT_FINAL_ASSERT_FALSE
16511667
HELP_REPLACE_FUNCTION_BODY
16521668
HELP_ANSI_C_LANGUAGE
16531669
"\n"

Diff for: ‎src/goto-instrument/goto_instrument_parse_options.h

+2
Original file line numberDiff line numberDiff line change
@@ -31,6 +31,7 @@ Author: Daniel Kroening, [email protected]
3131

3232
#include "aggressive_slicer.h"
3333
#include "generate_function_bodies.h"
34+
#include "insert_final_assert_false.h"
3435

3536
#include "count_eloc.h"
3637

@@ -59,6 +60,7 @@ Author: Daniel Kroening, [email protected]
5960
"(max-var):(max-po-trans):(ignore-arrays)" \
6061
"(cfg-kill)(no-dependencies)(force-loop-duplication)" \
6162
"(call-graph)(reachable-call-graph)" \
63+
OPT_INSERT_FINAL_ASSERT_FALSE \
6264
OPT_SHOW_CLASS_HIERARCHY \
6365
"(no-po-rendering)(render-cluster-file)(render-cluster-function)" \
6466
"(nondet-volatile)(isr):" \

Diff for: ‎src/goto-instrument/insert_final_assert_false.cpp

+60
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,60 @@
1+
/*******************************************************************\
2+
3+
Module: Insert assert(false) at end of entry function
4+
5+
Author: Nathan Chong, Kareem Khazem
6+
7+
\*******************************************************************/
8+
9+
/// \file
10+
/// Insert final assert false into a function
11+
12+
#include "insert_final_assert_false.h"
13+
14+
#include <goto-programs/goto_model.h>
15+
#include <util/irep.h>
16+
17+
#include <iterator>
18+
#include <list>
19+
20+
insert_final_assert_falset::insert_final_assert_falset(
21+
message_handlert &_message_handler)
22+
: log(_message_handler)
23+
{
24+
}
25+
26+
bool insert_final_assert_falset::
27+
operator()(goto_modelt &goto_model, const std::string &function_to_instrument)
28+
{
29+
const irep_idt entry(function_to_instrument);
30+
auto it = goto_model.goto_functions.function_map.find(entry);
31+
if(it == goto_model.goto_functions.function_map.end())
32+
{
33+
log.error() << "insert-final-assert-false: could not find function "
34+
<< "'" << function_to_instrument << "'" << messaget::eom;
35+
return true;
36+
}
37+
goto_programt &entry_function = (it->second).body;
38+
goto_programt::instructionst &instructions = entry_function.instructions;
39+
auto instr_it = instructions.end();
40+
auto last_instruction = std::prev(instr_it);
41+
DATA_INVARIANT(
42+
last_instruction->is_end_function(),
43+
"last instruction in function should be END_FUNCTION");
44+
source_locationt assert_location = last_instruction->source_location;
45+
assert_location.set_property_class(ID_assertion);
46+
assert_location.set_comment("insert-final-assert-false (should fail) ");
47+
goto_programt::instructiont false_assert =
48+
goto_programt::make_assertion(false_exprt(), assert_location);
49+
entry_function.insert_before_swap(last_instruction, false_assert);
50+
return false;
51+
}
52+
53+
bool insert_final_assert_false(
54+
goto_modelt &goto_model,
55+
const std::string &function_to_instrument,
56+
message_handlert &message_handler)
57+
{
58+
insert_final_assert_falset ifaf(message_handler);
59+
return ifaf(goto_model, function_to_instrument);
60+
}

Diff for: ‎src/goto-instrument/insert_final_assert_false.h

+59
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,59 @@
1+
/*******************************************************************\
2+
3+
Module: Insert assert(false) at end of entry function
4+
5+
Author: Nathan Chong, Kareem Khazem
6+
7+
\*******************************************************************/
8+
9+
/// \file
10+
/// Insert final assert false into a function
11+
12+
/// This transform can be used to check for some cases of vacuous proofs
13+
/// Usually the given function is the test harness / entry point
14+
/// The instrumented assert is expected to fail
15+
/// If it does not then this may indicate inconsistent assumptions
16+
17+
#ifndef CPROVER_GOTO_INSTRUMENT_INSERT_FINAL_ASSERT_FALSE_H
18+
#define CPROVER_GOTO_INSTRUMENT_INSERT_FINAL_ASSERT_FALSE_H
19+
20+
#include <string>
21+
22+
#include <util/message.h>
23+
24+
class goto_modelt;
25+
26+
class insert_final_assert_falset
27+
{
28+
public:
29+
explicit insert_final_assert_falset(message_handlert &_message_handler);
30+
bool operator()(goto_modelt &, const std::string &);
31+
32+
private:
33+
messaget log;
34+
};
35+
36+
/// Transform a goto program by inserting assert(false) at the end of a given
37+
/// function \p function_to_instrument. The instrumented assert is expected
38+
/// to fail. If it does not then this may indicate inconsistent assumptions.
39+
///
40+
/// \param goto_model: The goto program to modify.
41+
/// \param function_to_instrument: Name of the function to instrument.
42+
/// \param message_handler: Handles logging.
43+
/// \returns false on success
44+
bool insert_final_assert_false(
45+
goto_modelt &goto_model,
46+
const std::string &function_to_instrument,
47+
message_handlert &message_handler);
48+
49+
// clang-format off
50+
#define OPT_INSERT_FINAL_ASSERT_FALSE \
51+
"(insert-final-assert-false):"
52+
53+
#define HELP_INSERT_FINAL_ASSERT_FALSE \
54+
" --insert-final-assert-false <function>\n" \
55+
/* NOLINTNEXTLINE(whitespace/line_length) */ \
56+
" generate assert(false) at end of function\n"
57+
// clang-format on
58+
59+
#endif // CPROVER_GOTO_INSTRUMENT_INSERT_FINAL_ASSERT_FALSE_H

0 commit comments

Comments
 (0)