Skip to content

Commit 2b050a0

Browse files
peterschrammelpeterschrammel
authored
Merge pull request #1372 from diffblue/preconditions
Preconditions
2 parents 1d81035 + 6a509a8 commit 2b050a0

File tree

24 files changed

+228
-44
lines changed

24 files changed

+228
-44
lines changed

‎regression/cbmc-cover/branch3/test.desc

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,6 +3,7 @@ main.c
33
--cover branch --unwind 6
44
^EXIT=0$
55
^SIGNAL=0$
6-
^\*\* .* of .* covered \(100.0%\)$
6+
^\*\* .* of .* covered \(.*\)$
77
--
88
^warning: ignoring
9+
^\[main.coverage.*\] file main.c line .* function main block .* branch .*: FAILED$

‎regression/cbmc-cover/built-ins1/main.c

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,11 @@
1+
#include <string.h>
2+
13
int main()
24
{
35
char a[10];
46
__CPROVER_input("a[3]", a[3]);
57

6-
int len = strlen(a);
8+
int len=strlen(a);
79

810
if(len==3)
911
{
@@ -13,5 +15,6 @@ int main()
1315
{
1416
return -1;
1517
}
18+
1619
return 1;
1720
}

‎regression/cbmc-cover/built-ins1/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ main.c
33
--cover location --unwind 1
44
^EXIT=0$
55
^SIGNAL=0$
6-
^\*\* 4 of 7 covered
6+
^\*\* 5 of 8 covered
77
--
88
^warning: ignoring
99
^\[.*<builtin-library-

‎regression/cbmc-cover/built-ins3/main.c

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -5,6 +5,8 @@ int main()
55
const char *s="test";
66
int ret=puts(s); //return value is nondet (internal to built-in, thus non-controllable)
77

8+
__CPROVER_input("return value puts", ret);
9+
810
if(ret<0)
911
{
1012
return 1;

‎regression/cbmc-cover/built-ins3/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ main.c
33
--cover location --unwind 10
44
^EXIT=0$
55
^SIGNAL=0$
6-
^\*\* 4 of 4 covered
6+
^\*\* 5 of .* covered
77
--
88
^warning: ignoring
99
^\[.*<builtin-library-

‎regression/cbmc-cover/built-ins4/main.c

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,5 @@
1+
#include <string.h>
2+
13
int main()
24
{
35
char a[10];

‎regression/cbmc-cover/built-ins5/main.c

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,5 @@
1+
#include <string.h>
2+
13
int main()
24
{
35
char a[10];

‎regression/cbmc-cover/built-ins6/main.c

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,5 @@
1+
#include <string.h>
2+
13
int main()
24
{
35
char a[10];

‎regression/cbmc-cover/built-ins7/main.c

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,5 @@
1+
#include <string.h>
2+
13
int main()
24
{
35
char a[10];

‎regression/cbmc-cover/inlining1/main.c

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,5 @@
1+
// Discussion point: is the branch below one goal or two?
2+
13
inline void my_func(int x)
24
{
35
if(x)

‎regression/cbmc-cover/inlining1/test.desc

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -3,9 +3,9 @@ main.c
33
--cover branch
44
^EXIT=0$
55
^SIGNAL=0$
6-
^\[my_func.coverage.1\] file main.c line 3 function my_func block 1 branch false: SATISFIED$
7-
^\[my_func.coverage.2\] file main.c line 3 function my_func block 1 branch true: FAILED$
8-
^\[my_func.coverage.3\] file main.c line 3 function my_func block 2 branch false: FAILED$
9-
^\[my_func.coverage.4\] file main.c line 3 function my_func block 2 branch true: SATISFIED$
6+
^\[main.coverage.1\] file main.c line 15 function main entry point: SATISFIED$
7+
^\[my_func.coverage.1\] file main.c line 5 function my_func entry point: SATISFIED$
8+
^\[my_func.coverage.2\] file main.c line 5 function my_func block 1 branch false: SATISFIED$
9+
^\[my_func.coverage.3\] file main.c line 5 function my_func block 1 branch true: SATISFIED$
1010
--
1111
^warning: ignoring

‎regression/cbmc/Free2/test.desc

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,10 @@
11
CORE
22
main.c
3-
--pointer-check
3+
44
^EXIT=10$
55
^SIGNAL=0$
6+
^.*free argument must be dynamic object: FAILURE$
7+
^.*free argument has offset zero: SUCCESS$
68
^VERIFICATION FAILED$
79
--
810
^warning: ignoring

‎src/ansi-c/ansi_c_internal_additions.cpp

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -112,6 +112,8 @@ void ansi_c_internal_additions(std::string &code)
112112
"void __VERIFIER_assume(__CPROVER_bool assumption);\n"
113113
// NOLINTNEXTLINE(whitespace/line_length)
114114
"void __CPROVER_assert(__CPROVER_bool assertion, const char *description);\n"
115+
// NOLINTNEXTLINE(whitespace/line_length)
116+
"void __CPROVER_precondition(__CPROVER_bool precondition, const char *description);\n"
115117
"__CPROVER_bool __CPROVER_equal();\n"
116118
"__CPROVER_bool __CPROVER_same_object(const void *, const void *);\n"
117119
"__CPROVER_bool __CPROVER_invalid_pointer(const void *);\n"

‎src/ansi-c/library/cprover.h

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -19,6 +19,7 @@ extern const void *__CPROVER_memory_leak;
1919

2020
void __CPROVER_assume(__CPROVER_bool assumption) __attribute__((__noreturn__));
2121
void __CPROVER_assert(__CPROVER_bool assertion, const char *description);
22+
void __CPROVER_precondition(__CPROVER_bool assertion, const char *description);
2223

2324
__CPROVER_bool __CPROVER_is_zero_string(const void *);
2425
__CPROVER_size_t __CPROVER_zero_string_length(const void *);

‎src/ansi-c/library/stdlib.c

Lines changed: 5 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -145,14 +145,13 @@ inline void free(void *ptr)
145145
{
146146
__CPROVER_HIDE:;
147147
// If ptr is NULL, no operation is performed.
148+
__CPROVER_precondition(ptr==0 || __CPROVER_DYNAMIC_OBJECT(ptr),
149+
"free argument must be dynamic object");
150+
__CPROVER_precondition(ptr==0 || __CPROVER_POINTER_OFFSET(ptr)==0,
151+
"free argument has offset zero");
152+
148153
if(ptr!=0)
149154
{
150-
// is it dynamic?
151-
__CPROVER_assert(__CPROVER_DYNAMIC_OBJECT(ptr),
152-
"free argument is dynamic object");
153-
__CPROVER_assert(__CPROVER_POINTER_OFFSET(ptr)==0,
154-
"free argument has offset zero");
155-
156155
// catch double free
157156
if(__CPROVER_deallocated==ptr)
158157
__CPROVER_assert(0, "double free");

‎src/cbmc/bmc_cover.cpp

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -204,8 +204,6 @@ bool bmc_covert::operator()()
204204
// This maps property IDs to 'goalt'
205205
forall_goto_functions(f_it, goto_functions)
206206
{
207-
// Functions are already inlined.
208-
if(f_it->second.is_inlined()) continue;
209207
forall_goto_program_instructions(i_it, f_it->second.body)
210208
{
211209
if(i_it->is_assert())

‎src/cbmc/cbmc_parse_options.cpp

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -27,6 +27,7 @@ Author: Daniel Kroening, kroening@kroening.com
2727

2828
#include <goto-programs/convert_nondet.h>
2929
#include <goto-programs/initialize_goto_model.h>
30+
#include <goto-programs/instrument_preconditions.h>
3031
#include <goto-programs/goto_convert_functions.h>
3132
#include <goto-programs/goto_inline.h>
3233
#include <goto-programs/link_to_library.h>
@@ -780,9 +781,8 @@ bool cbmc_parse_optionst::process_goto_program(
780781

781782
mm_io(goto_model);
782783

783-
// do partial inlining
784-
status() << "Partial Inlining" << eom;
785-
goto_partial_inline(goto_model, get_message_handler());
784+
// instrument library preconditions
785+
instrument_preconditions(goto_model);
786786

787787
// remove returns, gcc vectors, complex
788788
remove_returns(goto_model);

‎src/goto-instrument/goto_instrument_parse_options.cpp

Lines changed: 1 addition & 17 deletions
Original file line numberDiff line numberDiff line change
@@ -259,7 +259,6 @@ int goto_instrument_parse_optionst::doit()
259259
if(cmdline.isset("show-value-sets"))
260260
{
261261
do_indirect_call_and_rtti_removal();
262-
do_partial_inlining();
263262

264263
// recalculate numbers, etc.
265264
goto_model.goto_functions.update();
@@ -275,7 +274,6 @@ int goto_instrument_parse_optionst::doit()
275274
if(cmdline.isset("show-global-may-alias"))
276275
{
277276
do_indirect_call_and_rtti_removal();
278-
do_partial_inlining();
279277
do_remove_returns();
280278
parameter_assignments(goto_model);
281279

@@ -292,7 +290,6 @@ int goto_instrument_parse_optionst::doit()
292290
if(cmdline.isset("show-local-bitvector-analysis"))
293291
{
294292
do_indirect_call_and_rtti_removal();
295-
do_partial_inlining();
296293
parameter_assignments(goto_model);
297294

298295
// recalculate numbers, etc.
@@ -316,7 +313,6 @@ int goto_instrument_parse_optionst::doit()
316313
if(cmdline.isset("show-custom-bitvector-analysis"))
317314
{
318315
do_indirect_call_and_rtti_removal();
319-
do_partial_inlining();
320316
do_remove_returns();
321317
parameter_assignments(goto_model);
322318

@@ -341,7 +337,6 @@ int goto_instrument_parse_optionst::doit()
341337
if(cmdline.isset("show-escape-analysis"))
342338
{
343339
do_indirect_call_and_rtti_removal();
344-
do_partial_inlining();
345340
do_remove_returns();
346341
parameter_assignments(goto_model);
347342

@@ -358,7 +353,6 @@ int goto_instrument_parse_optionst::doit()
358353
if(cmdline.isset("custom-bitvector-analysis"))
359354
{
360355
do_indirect_call_and_rtti_removal();
361-
do_partial_inlining();
362356
do_remove_returns();
363357
parameter_assignments(goto_model);
364358

@@ -388,7 +382,6 @@ int goto_instrument_parse_optionst::doit()
388382
if(cmdline.isset("show-points-to"))
389383
{
390384
do_indirect_call_and_rtti_removal();
391-
do_partial_inlining();
392385

393386
// recalculate numbers, etc.
394387
goto_model.goto_functions.update();
@@ -405,7 +398,6 @@ int goto_instrument_parse_optionst::doit()
405398
if(cmdline.isset("show-intervals"))
406399
{
407400
do_indirect_call_and_rtti_removal();
408-
do_partial_inlining();
409401

410402
// recalculate numbers, etc.
411403
goto_model.goto_functions.update();
@@ -434,7 +426,6 @@ int goto_instrument_parse_optionst::doit()
434426
if(cmdline.isset("list-calls-args"))
435427
{
436428
do_indirect_call_and_rtti_removal();
437-
do_partial_inlining();
438429

439430
list_calls_and_arguments(goto_model);
440431

@@ -448,7 +439,6 @@ int goto_instrument_parse_optionst::doit()
448439
if(!cmdline.isset("inline"))
449440
{
450441
do_indirect_call_and_rtti_removal();
451-
do_partial_inlining();
452442

453443
// recalculate numbers, etc.
454444
goto_model.goto_functions.update();
@@ -977,8 +967,6 @@ void goto_instrument_parse_optionst::instrument_goto_program()
977967
if(cmdline.isset("show-custom-bitvector-analysis") ||
978968
cmdline.isset("custom-bitvector-analysis"))
979969
{
980-
do_partial_inlining();
981-
982970
status() << "Propagating Constants" << eom;
983971
constant_propagator_ait constant_propagator_ai(goto_model);
984972
remove_skip(goto_model);
@@ -987,7 +975,6 @@ void goto_instrument_parse_optionst::instrument_goto_program()
987975
if(cmdline.isset("escape-analysis"))
988976
{
989977
do_indirect_call_and_rtti_removal();
990-
do_partial_inlining();
991978
do_remove_returns();
992979
parameter_assignments(goto_model);
993980

@@ -1082,9 +1069,7 @@ void goto_instrument_parse_optionst::instrument_goto_program()
10821069
if(cmdline.isset("partial-inline"))
10831070
{
10841071
do_indirect_call_and_rtti_removal();
1085-
1086-
status() << "Partial inlining" << eom;
1087-
goto_partial_inline(goto_model, get_message_handler(), true);
1072+
do_partial_inlining();
10881073

10891074
goto_model.goto_functions.update();
10901075
goto_model.goto_functions.compute_loop_numbers();
@@ -1172,7 +1157,6 @@ void goto_instrument_parse_optionst::instrument_goto_program()
11721157
cmdline.isset("concurrency"))
11731158
{
11741159
do_indirect_call_and_rtti_removal();
1175-
do_partial_inlining();
11761160

11771161
status() << "Pointer Analysis" << eom;
11781162
value_set_analysist value_set_analysis(ns);

‎src/goto-programs/Makefile

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -23,6 +23,7 @@ SRC = basic_blocks.cpp \
2323
goto_program_template.cpp \
2424
goto_trace.cpp \
2525
graphml_witness.cpp \
26+
instrument_preconditions.cpp \
2627
interpreter.cpp \
2728
interpreter_evaluate.cpp \
2829
json_goto_trace.cpp \

‎src/goto-programs/builtin_functions.cpp

Lines changed: 18 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -1113,7 +1113,8 @@ void goto_convertt::do_function_call_symbol(
11131113
throw 0;
11141114
}
11151115
}
1116-
else if(identifier==CPROVER_PREFIX "assert")
1116+
else if(identifier==CPROVER_PREFIX "assert" ||
1117+
identifier==CPROVER_PREFIX "precondition")
11171118
{
11181119
if(arguments.size()!=2)
11191120
{
@@ -1123,16 +1124,28 @@ void goto_convertt::do_function_call_symbol(
11231124
throw 0;
11241125
}
11251126

1127+
bool is_precondition=
1128+
identifier==CPROVER_PREFIX "precondition";
1129+
11261130
const irep_idt description=
11271131
get_string_constant(arguments[1]);
11281132

11291133
goto_programt::targett t=dest.add_instruction(ASSERT);
11301134
t->guard=arguments[0];
11311135
t->source_location=function.source_location();
1132-
t->source_location.set(
1133-
"user-provided",
1134-
!function.source_location().is_built_in());
1135-
t->source_location.set_property_class(ID_assertion);
1136+
1137+
if(is_precondition)
1138+
{
1139+
t->source_location.set_property_class(ID_precondition);
1140+
}
1141+
else
1142+
{
1143+
t->source_location.set(
1144+
"user-provided",
1145+
!function.source_location().is_built_in());
1146+
t->source_location.set_property_class(ID_assertion);
1147+
}
1148+
11361149
t->source_location.set_comment(description);
11371150

11381151
// let's double-check the type of the argument

0 commit comments

Comments
 (0)