diff --git a/doc/cprover-manual/properties.md b/doc/cprover-manual/properties.md index 40f9c10eede..3f37e580807 100644 --- a/doc/cprover-manual/properties.md +++ b/doc/cprover-manual/properties.md @@ -134,21 +134,64 @@ As all of these checks apply across the entire input program, we may wish to disable them for selected statements in the program. For example, unsigned overflows can be expected and acceptable in certain instructions even when elsewhere we do not expect them. As of version 5.12, CBMC supports selectively -disabling automatically generated properties. To disable property generation, -use `#pragma CPROVER check disable ""`, which remains in effect -until a `#pragma CPROVER check pop` (to re-enable all properties -disabled before or since the last `#pragma CPROVER check push`) is provided. +disabling or enabling automatically generated properties using pragmas. + + +CPROVER pragmas are handled using a stack: +- `#pragma CPROVER check push` pushes a new level on the pragma stack +- `#pragma CPROVER check disable ""` adds a disable pragma at the top of the stack +- `#pragma CPROVER check enable ""` adds a enable pragma at the top of the stack +- an `enable` or `disable` pragma for a given check present at the top level of the stack shadows other pragmas for the same in lower levels of the stack +- adding both `enable` and `disable` pragmas for a same check in a same level of the stack creates a PARSING_ERROR. +- `#pragma CPROVER check pop` pops a level in the stack and restores the state of pragmas at the sub level + For example, for unsigned overflow checks, use + +``` +unsigned foo(unsigned x) +{ +#pragma CPROVER check push +#pragma CPROVER check enable "unsigned-overflow" + x = x + 1; // immediately follows the pragma, unsigned overflow check apply here +#pragma CPROVER check pop + x = x + 2; // unsigned overflow checks do not apply here +``` + +``` +unsigned foo(unsigned x) +{ +#pragma CPROVER check push +#pragma CPROVER check enable "unsigned-overflow" +#pragma CPROVER check enable "signed-overflow" + x = x + 1; // unsigned and signed overflow check apply here +#pragma CPROVER check push +#pragma CPROVER check disable "unsigned-overflow" + x = x + 2; // only signed overflow check apply here +#pragma CPROVER check pop + x = x + 3; // unsigned and signed overflow check apply here +#pragma CPROVER check pop + x = x + 2; // unsigned overflow checks do not apply here +``` + ``` unsigned foo(unsigned x) { #pragma CPROVER check push +#pragma CPROVER check enable "unsigned-overflow" +#pragma CPROVER check enable "signed-overflow" + x = x + 1; // unsigned and signed overflow check apply here +#pragma CPROVER check push #pragma CPROVER check disable "unsigned-overflow" - x = x + 1; // immediately follows the pragma, no unsigned overflow check here +#pragma CPROVER check enable "unsigned-overflow" + // PARSING_ERROR ... Found enable and disable pragmas for unsigned-overflow-check + x = x + 2; +#pragma CPROVER check pop + x = x + 3; #pragma CPROVER check pop - x = x + 2; // unsigned overflow checks are generated here + x = x + 2; ``` + #### Flag --nan-check limitations Please note that `--nan-check` flag is adding not-a-number checks only for diff --git a/jbmc/src/janalyzer/janalyzer_parse_options.cpp b/jbmc/src/janalyzer/janalyzer_parse_options.cpp index ca98361eafc..d07f4770ab6 100644 --- a/jbmc/src/janalyzer/janalyzer_parse_options.cpp +++ b/jbmc/src/janalyzer/janalyzer_parse_options.cpp @@ -705,7 +705,11 @@ void janalyzer_parse_optionst::process_goto_function( // add generic checks goto_check( - function.get_function_id(), function.get_goto_function(), ns, options); + function.get_function_id(), + function.get_goto_function(), + ns, + options, + log.get_message_handler()); } bool janalyzer_parse_optionst::can_generate_function_body(const irep_idt &name) diff --git a/jbmc/src/jbmc/jbmc_parse_options.cpp b/jbmc/src/jbmc/jbmc_parse_options.cpp index af93b90a4f2..254a78bdc5a 100644 --- a/jbmc/src/jbmc/jbmc_parse_options.cpp +++ b/jbmc/src/jbmc/jbmc_parse_options.cpp @@ -812,7 +812,11 @@ void jbmc_parse_optionst::process_goto_function( // add generic checks goto_check( - function.get_function_id(), function.get_goto_function(), ns, options); + function.get_function_id(), + function.get_goto_function(), + ns, + options, + log.get_message_handler()); // Replace Java new side effects remove_java_new( diff --git a/jbmc/src/jdiff/jdiff_parse_options.cpp b/jbmc/src/jdiff/jdiff_parse_options.cpp index b193091ffee..9ea27ba96dd 100644 --- a/jbmc/src/jdiff/jdiff_parse_options.cpp +++ b/jbmc/src/jdiff/jdiff_parse_options.cpp @@ -278,7 +278,7 @@ bool jdiff_parse_optionst::process_goto_program( // add generic checks log.status() << "Generic Property Instrumentation" << messaget::eom; - goto_check(options, goto_model); + goto_check(options, goto_model, log.get_message_handler()); // checks don't know about adjusted float expressions adjust_float_expressions(goto_model); diff --git a/regression/cbmc/pragma_cprover_enable1/main.c b/regression/cbmc/pragma_cprover_enable1/main.c new file mode 100644 index 00000000000..2ff377a7225 --- /dev/null +++ b/regression/cbmc/pragma_cprover_enable1/main.c @@ -0,0 +1,16 @@ +int main() +{ + int x; + int y[1]; + +#pragma CPROVER check push +#pragma CPROVER check enable "bounds" +#pragma CPROVER check enable "signed-overflow" + // generate assertions for the following statement + x = x + y[1]; + // pop all annotations +#pragma CPROVER check pop + // but do not generate assertions for this one + x = y[1]; + return x; +} diff --git a/regression/cbmc/pragma_cprover_enable1/test.desc b/regression/cbmc/pragma_cprover_enable1/test.desc new file mode 100644 index 00000000000..21dd47970f0 --- /dev/null +++ b/regression/cbmc/pragma_cprover_enable1/test.desc @@ -0,0 +1,12 @@ +CORE +main.c + +^\[main\.array_bounds\.1\] line \d+ array 'y' upper bound.*FAILURE$ +^\[main\.overflow\.1\] line \d+ arithmetic overflow on signed.*FAILURE$ +^\*\* 2 of 2 failed +^VERIFICATION FAILED$ +^EXIT=10$ +^SIGNAL=0$ +-- +-- +Checks that we can selectively activate checks using pragmas. \ No newline at end of file diff --git a/regression/cbmc/pragma_cprover_enable2/main.c b/regression/cbmc/pragma_cprover_enable2/main.c new file mode 100644 index 00000000000..42c740fa295 --- /dev/null +++ b/regression/cbmc/pragma_cprover_enable2/main.c @@ -0,0 +1,24 @@ +int foo(int x) +{ + return x; +} + +int main() +{ + int m, n; + +#pragma CPROVER check push +#pragma CPROVER check enable "signed-overflow" + // generate assertions for the following statements + int x = m = n + n; + ++n; + n++; + n += 1; + foo(x + n); + // pop all annotations +#pragma CPROVER check pop + // but do not generate assertions for these + x = n + n; + foo(x + n); + return x; +} diff --git a/regression/cbmc/pragma_cprover_enable2/test.desc b/regression/cbmc/pragma_cprover_enable2/test.desc new file mode 100644 index 00000000000..9ddbded4bb7 --- /dev/null +++ b/regression/cbmc/pragma_cprover_enable2/test.desc @@ -0,0 +1,14 @@ +CORE +main.c + +^\[main\.overflow\.1\] line 13 arithmetic overflow on signed \+ in n \+ n: FAILURE$ +^\[main\.overflow\.2\] line 14 arithmetic overflow on signed \+ in n \+ 1: FAILURE$ +^\[main\.overflow\.3\] line 15 arithmetic overflow on signed \+ in n \+ 1: FAILURE$ +^\[main\.overflow\.4\] line 16 arithmetic overflow on signed \+ in n \+ 1: FAILURE$ +^\[main\.overflow\.5\] line 17 arithmetic overflow on signed \+ in x \+ n: FAILURE$ +^\*\* 5 of 5 failed +^VERIFICATION FAILED$ +^EXIT=10$ +^SIGNAL=0$ +-- +^warning: ignoring diff --git a/regression/cbmc/pragma_cprover_enable3/main.c b/regression/cbmc/pragma_cprover_enable3/main.c new file mode 100644 index 00000000000..b58963e731c --- /dev/null +++ b/regression/cbmc/pragma_cprover_enable3/main.c @@ -0,0 +1,20 @@ +#include + +int main() +{ + char *p = malloc(sizeof(*p)); + char *q; + +#pragma CPROVER check push +#pragma CPROVER check enable "pointer-primitive" + // generate checks for the following statements and fail + if(__CPROVER_same_object(p, q)) + { + } +#pragma CPROVER check pop + + // but do not generate checks on the following statements + if(__CPROVER_same_object(p, q)) + { + } +} diff --git a/regression/cbmc/pragma_cprover_enable3/test.desc b/regression/cbmc/pragma_cprover_enable3/test.desc new file mode 100644 index 00000000000..0b807ce400d --- /dev/null +++ b/regression/cbmc/pragma_cprover_enable3/test.desc @@ -0,0 +1,18 @@ +CORE +main.c + +^main.c function main$ +^\[main.pointer_primitives.\d+\] line 11 pointer invalid in POINTER_OBJECT\(\(const void \*\)p\): SUCCESS$ +^\[main.pointer_primitives.\d+\] line 11 deallocated dynamic object in POINTER_OBJECT\(\(const void \*\)p\): SUCCESS$ +^\[main.pointer_primitives.\d+\] line 11 dead object in POINTER_OBJECT\(\(const void \*\)p\): SUCCESS$ +^\[main.pointer_primitives.\d+\] line 11 pointer outside object bounds in POINTER_OBJECT\(\(const void \*\)p\): SUCCESS$ +^\[main.pointer_primitives.\d+\] line 11 pointer invalid in POINTER_OBJECT\(\(const void \*\)q\): FAILURE$ +^\[main.pointer_primitives.\d+\] line 11 deallocated dynamic object in POINTER_OBJECT\(\(const void \*\)q\): SUCCESS$ +^\[main.pointer_primitives.\d+\] line 11 dead object in POINTER_OBJECT\(\(const void \*\)q\): SUCCESS$ +^\[main.pointer_primitives.\d+\] line 11 pointer outside object bounds in POINTER_OBJECT\(\(const void \*\)q\): FAILURE$ +^VERIFICATION FAILED$ +^EXIT=10$ +^SIGNAL=0$ +-- +^\[main.pointer_primitives.\d+\] line 17 +-- \ No newline at end of file diff --git a/regression/cbmc/pragma_cprover_enable_disable_global_off/main.c b/regression/cbmc/pragma_cprover_enable_disable_global_off/main.c new file mode 100644 index 00000000000..31c7360121e --- /dev/null +++ b/regression/cbmc/pragma_cprover_enable_disable_global_off/main.c @@ -0,0 +1,42 @@ +#include + +int main() +{ + char *p = malloc(sizeof(*p)); + char *q; + +#pragma CPROVER check push +#pragma CPROVER check enable "pointer-primitive" + // must generate checks + if(__CPROVER_same_object(p, q)) + { + } +#pragma CPROVER check push +#pragma CPROVER check disable "pointer-primitive" + // must not generate checks + if(__CPROVER_same_object(p, q)) + { + } +#pragma CPROVER check push +#pragma CPROVER check enable "pointer-primitive" + // must generate checks + if(__CPROVER_same_object(p, q)) + { + } +#pragma CPROVER check pop + // must not generate generate checks + if(__CPROVER_same_object(p, q)) + { + } +#pragma CPROVER check pop + // must generate generate checks + if(__CPROVER_same_object(p, q)) + { + } +#pragma CPROVER check pop + // must not generate generate checks + if(__CPROVER_same_object(p, q)) + { + } + return 0; +} diff --git a/regression/cbmc/pragma_cprover_enable_disable_global_off/test.desc b/regression/cbmc/pragma_cprover_enable_disable_global_off/test.desc new file mode 100644 index 00000000000..61e93992e7d --- /dev/null +++ b/regression/cbmc/pragma_cprover_enable_disable_global_off/test.desc @@ -0,0 +1,36 @@ +CORE +main.c + +^main.c function main$ +^\[main.pointer_primitives.\d+\] line 11 pointer invalid in POINTER_OBJECT\(\(const void \*\)p\): SUCCESS$ +^\[main.pointer_primitives.\d+\] line 11 deallocated dynamic object in POINTER_OBJECT\(\(const void \*\)p\): SUCCESS$ +^\[main.pointer_primitives.\d+\] line 11 dead object in POINTER_OBJECT\(\(const void \*\)p\): SUCCESS$ +^\[main.pointer_primitives.\d+\] line 11 pointer outside object bounds in POINTER_OBJECT\(\(const void \*\)p\): SUCCESS$ +^\[main.pointer_primitives.\d+\] line 11 pointer invalid in POINTER_OBJECT\(\(const void \*\)q\): FAILURE$ +^\[main.pointer_primitives.\d+\] line 11 deallocated dynamic object in POINTER_OBJECT\(\(const void \*\)q\): SUCCESS$ +^\[main.pointer_primitives.\d+\] line 11 dead object in POINTER_OBJECT\(\(const void \*\)q\): SUCCESS$ +^\[main.pointer_primitives.\d+\] line 11 pointer outside object bounds in POINTER_OBJECT\(\(const void \*\)q\): FAILURE$ +^\[main.pointer_primitives.\d+\] line 23 pointer invalid in POINTER_OBJECT\(\(const void \*\)p\): SUCCESS$ +^\[main.pointer_primitives.\d+\] line 23 deallocated dynamic object in POINTER_OBJECT\(\(const void \*\)p\): SUCCESS$ +^\[main.pointer_primitives.\d+\] line 23 dead object in POINTER_OBJECT\(\(const void \*\)p\): SUCCESS$ +^\[main.pointer_primitives.\d+\] line 23 pointer outside object bounds in POINTER_OBJECT\(\(const void \*\)p\): SUCCESS$ +^\[main.pointer_primitives.\d+\] line 23 pointer invalid in POINTER_OBJECT\(\(const void \*\)q\): FAILURE$ +^\[main.pointer_primitives.\d+\] line 23 deallocated dynamic object in POINTER_OBJECT\(\(const void \*\)q\): SUCCESS$ +^\[main.pointer_primitives.\d+\] line 23 dead object in POINTER_OBJECT\(\(const void \*\)q\): SUCCESS$ +^\[main.pointer_primitives.\d+\] line 23 pointer outside object bounds in POINTER_OBJECT\(\(const void \*\)q\): FAILURE$ +^\[main.pointer_primitives.\d+\] line 33 pointer invalid in POINTER_OBJECT\(\(const void \*\)p\): SUCCESS$ +^\[main.pointer_primitives.\d+\] line 33 deallocated dynamic object in POINTER_OBJECT\(\(const void \*\)p\): SUCCESS$ +^\[main.pointer_primitives.\d+\] line 33 dead object in POINTER_OBJECT\(\(const void \*\)p\): SUCCESS$ +^\[main.pointer_primitives.\d+\] line 33 pointer outside object bounds in POINTER_OBJECT\(\(const void \*\)p\): SUCCESS$ +^\[main.pointer_primitives.\d+\] line 33 pointer invalid in POINTER_OBJECT\(\(const void \*\)q\): FAILURE$ +^\[main.pointer_primitives.\d+\] line 33 deallocated dynamic object in POINTER_OBJECT\(\(const void \*\)q\): SUCCESS$ +^\[main.pointer_primitives.\d+\] line 33 dead object in POINTER_OBJECT\(\(const void \*\)q\): SUCCESS$ +^\[main.pointer_primitives.\d+\] line 33 pointer outside object bounds in POINTER_OBJECT\(\(const void \*\)q\): FAILURE$ +^VERIFICATION FAILED$ +^EXIT=10$ +^SIGNAL=0$ +-- +^\[main.pointer_primitives.\d+\] line 17 +^\[main.pointer_primitives.\d+\] line 28 +^\[main.pointer_primitives.\d+\] line 38 +-- diff --git a/regression/cbmc/pragma_cprover_enable_disable_global_on/main.c b/regression/cbmc/pragma_cprover_enable_disable_global_on/main.c new file mode 100644 index 00000000000..c4ad7887ccb --- /dev/null +++ b/regression/cbmc/pragma_cprover_enable_disable_global_on/main.c @@ -0,0 +1,42 @@ +#include + +int main() +{ + char *p = malloc(sizeof(*p)); + char *q; + +#pragma CPROVER check push +#pragma CPROVER check enable "pointer-primitive" + // must generate checks + if(__CPROVER_same_object(p, q)) + { + } +#pragma CPROVER check push +#pragma CPROVER check disable "pointer-primitive" + // must not generate checks + if(__CPROVER_same_object(p, q)) + { + } +#pragma CPROVER check push +#pragma CPROVER check enable "pointer-primitive" + // must generate checks + if(__CPROVER_same_object(p, q)) + { + } +#pragma CPROVER check pop + // must not generate generate checks + if(__CPROVER_same_object(p, q)) + { + } +#pragma CPROVER check pop + // must generate generate checks + if(__CPROVER_same_object(p, q)) + { + } +#pragma CPROVER check pop + // must generate generate checks + if(__CPROVER_same_object(p, q)) + { + } + return 0; +} diff --git a/regression/cbmc/pragma_cprover_enable_disable_global_on/test.desc b/regression/cbmc/pragma_cprover_enable_disable_global_on/test.desc new file mode 100644 index 00000000000..4c960997d8d --- /dev/null +++ b/regression/cbmc/pragma_cprover_enable_disable_global_on/test.desc @@ -0,0 +1,43 @@ +CORE +main.c +--pointer-primitive-check +^main.c function main$ +^\[main.pointer_primitives.\d+\] line 11 pointer invalid in POINTER_OBJECT\(\(const void \*\)p\): SUCCESS$ +^\[main.pointer_primitives.\d+\] line 11 deallocated dynamic object in POINTER_OBJECT\(\(const void \*\)p\): SUCCESS$ +^\[main.pointer_primitives.\d+\] line 11 dead object in POINTER_OBJECT\(\(const void \*\)p\): SUCCESS$ +^\[main.pointer_primitives.\d+\] line 11 pointer outside object bounds in POINTER_OBJECT\(\(const void \*\)p\): SUCCESS$ +^\[main.pointer_primitives.\d+\] line 11 pointer invalid in POINTER_OBJECT\(\(const void \*\)q\): FAILURE$ +^\[main.pointer_primitives.\d+\] line 11 deallocated dynamic object in POINTER_OBJECT\(\(const void \*\)q\): SUCCESS$ +^\[main.pointer_primitives.\d+\] line 11 dead object in POINTER_OBJECT\(\(const void \*\)q\): SUCCESS$ +^\[main.pointer_primitives.\d+\] line 11 pointer outside object bounds in POINTER_OBJECT\(\(const void \*\)q\): FAILURE$ +^\[main.pointer_primitives.\d+\] line 23 pointer invalid in POINTER_OBJECT\(\(const void \*\)p\): SUCCESS$ +^\[main.pointer_primitives.\d+\] line 23 deallocated dynamic object in POINTER_OBJECT\(\(const void \*\)p\): SUCCESS$ +^\[main.pointer_primitives.\d+\] line 23 dead object in POINTER_OBJECT\(\(const void \*\)p\): SUCCESS$ +^\[main.pointer_primitives.\d+\] line 23 pointer outside object bounds in POINTER_OBJECT\(\(const void \*\)p\): SUCCESS$ +^\[main.pointer_primitives.\d+\] line 23 pointer invalid in POINTER_OBJECT\(\(const void \*\)q\): FAILURE$ +^\[main.pointer_primitives.\d+\] line 23 deallocated dynamic object in POINTER_OBJECT\(\(const void \*\)q\): SUCCESS$ +^\[main.pointer_primitives.\d+\] line 23 dead object in POINTER_OBJECT\(\(const void \*\)q\): SUCCESS$ +^\[main.pointer_primitives.\d+\] line 23 pointer outside object bounds in POINTER_OBJECT\(\(const void \*\)q\): FAILURE$ +^\[main.pointer_primitives.\d+\] line 33 pointer invalid in POINTER_OBJECT\(\(const void \*\)p\): SUCCESS$ +^\[main.pointer_primitives.\d+\] line 33 deallocated dynamic object in POINTER_OBJECT\(\(const void \*\)p\): SUCCESS$ +^\[main.pointer_primitives.\d+\] line 33 dead object in POINTER_OBJECT\(\(const void \*\)p\): SUCCESS$ +^\[main.pointer_primitives.\d+\] line 33 pointer outside object bounds in POINTER_OBJECT\(\(const void \*\)p\): SUCCESS$ +^\[main.pointer_primitives.\d+\] line 33 pointer invalid in POINTER_OBJECT\(\(const void \*\)q\): FAILURE$ +^\[main.pointer_primitives.\d+\] line 33 deallocated dynamic object in POINTER_OBJECT\(\(const void \*\)q\): SUCCESS$ +^\[main.pointer_primitives.\d+\] line 33 dead object in POINTER_OBJECT\(\(const void \*\)q\): SUCCESS$ +^\[main.pointer_primitives.\d+\] line 33 pointer outside object bounds in POINTER_OBJECT\(\(const void \*\)q\): FAILURE$ +^\[main.pointer_primitives.\d+\] line 38 pointer invalid in POINTER_OBJECT\(\(const void \*\)p\): SUCCESS$ +^\[main.pointer_primitives.\d+\] line 38 deallocated dynamic object in POINTER_OBJECT\(\(const void \*\)p\): SUCCESS$ +^\[main.pointer_primitives.\d+\] line 38 dead object in POINTER_OBJECT\(\(const void \*\)p\): SUCCESS$ +^\[main.pointer_primitives.\d+\] line 38 pointer outside object bounds in POINTER_OBJECT\(\(const void \*\)p\): SUCCESS$ +^\[main.pointer_primitives.\d+\] line 38 pointer invalid in POINTER_OBJECT\(\(const void \*\)q\): FAILURE$ +^\[main.pointer_primitives.\d+\] line 38 deallocated dynamic object in POINTER_OBJECT\(\(const void \*\)q\): SUCCESS$ +^\[main.pointer_primitives.\d+\] line 38 dead object in POINTER_OBJECT\(\(const void \*\)q\): SUCCESS$ +^\[main.pointer_primitives.\d+\] line 38 pointer outside object bounds in POINTER_OBJECT\(\(const void \*\)q\): FAILURE$ +^VERIFICATION FAILED$ +^EXIT=10$ +^SIGNAL=0$ +-- +^\[main.pointer_primitives.\d+\] line 17 +^\[main.pointer_primitives.\d+\] line 28 +-- diff --git a/regression/cbmc/pragma_cprover_enable_disable_multiple/main.c b/regression/cbmc/pragma_cprover_enable_disable_multiple/main.c new file mode 100644 index 00000000000..8e277c6cfcf --- /dev/null +++ b/regression/cbmc/pragma_cprover_enable_disable_multiple/main.c @@ -0,0 +1,17 @@ +#include + +int main() +{ + char *p = malloc(sizeof(*p)); + char *q; + +#pragma CPROVER check push +#pragma CPROVER check enable "pointer-overflow" +#pragma CPROVER check enable "pointer-overflow" // should not print an error message +#pragma CPROVER check push +#pragma CPROVER check disable "pointer-primitive" +#pragma CPROVER check enable "pointer-primitive" // should print an error message +#pragma CPROVER check pop +#pragma CPROVER check pop + return 0; +} diff --git a/regression/cbmc/pragma_cprover_enable_disable_multiple/test.desc b/regression/cbmc/pragma_cprover_enable_disable_multiple/test.desc new file mode 100644 index 00000000000..25e1f24a2c9 --- /dev/null +++ b/regression/cbmc/pragma_cprover_enable_disable_multiple/test.desc @@ -0,0 +1,10 @@ +CORE +main.c + +^file main.c line \d+ function main: Found enable and disable pragmas for pointer-primitive-check +^PARSING ERROR$ +^EXIT=6$ +^SIGNAL=0$ +-- +^file main.c line \d+ function main: Found enable and disable pragmas for pointer-overflow-check +-- diff --git a/regression/contracts/assigns_enforce_arrays_05/test.desc b/regression/contracts/assigns_enforce_arrays_05/test.desc index 4a485acff3f..4fe133f4914 100644 --- a/regression/contracts/assigns_enforce_arrays_05/test.desc +++ b/regression/contracts/assigns_enforce_arrays_05/test.desc @@ -1,6 +1,6 @@ CORE main.c ---enforce-contract assigns_ptr --enforce-contract assigns_range +--enforce-contract assigns_range ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/regression/contracts/assigns_enforce_free_dead/test.desc b/regression/contracts/assigns_enforce_free_dead/test.desc index 425e9705f27..616e2b670ab 100644 --- a/regression/contracts/assigns_enforce_free_dead/test.desc +++ b/regression/contracts/assigns_enforce_free_dead/test.desc @@ -29,7 +29,9 @@ main.c ^\[foo.\d+\] line \d+ Check that y is assignable: FAILURE$ ^\[foo.\d+\] line \d+ Check that z is assignable: FAILURE$ ^\[foo.\d+\] line \d+ Check that POINTER_OBJECT\(\(void \*\)z\) is assignable: FAILURE$ -^.*tmp_cc\$\d+.*: FAILURE$ +^.*__car_valid.*: FAILURE$ +^.*__car_lb.*: FAILURE$ +^.*__car_ub.*: FAILURE$ -- Checks that invalidated CARs are correctly tracked on `free` and `DEAD`. @@ -40,4 +42,4 @@ We also check (using positive regex matches above) that `**p` should be assignable in one case and should not be assignable in the other. Finally, we check that there should be no "internal" assertion failures -on `tmp_cc` variables used to track CARs. +on `__car_valid`, `__car_ub`, `__car_lb` variables used to track CARs. diff --git a/regression/contracts/assigns_enforce_havoc_object/functions.txt b/regression/contracts/assigns_enforce_havoc_object/functions.txt new file mode 100644 index 00000000000..08364b2d66f --- /dev/null +++ b/regression/contracts/assigns_enforce_havoc_object/functions.txt @@ -0,0 +1 @@ +Reading GOTO program from '__CPROVER_file_local_s2n_hash_c_s2n_evp_hash_reset_with_contracts_harness.c.goto' diff --git a/regression/contracts/assigns_enforce_havoc_object/main.c b/regression/contracts/assigns_enforce_havoc_object/main.c new file mode 100644 index 00000000000..1b1a56639b2 --- /dev/null +++ b/regression/contracts/assigns_enforce_havoc_object/main.c @@ -0,0 +1,47 @@ +#include +#include + +int x = 0; +typedef struct stc { + int i; + int j; +} stc; + +typedef struct stb { + stc *c; +} stb; + +typedef struct sta { + union { + stb *b; + int i; + int j; + } u; +} sta; + +int nondet_int(); + +void bar(sta *a) +{ + if (nondet_bool()) return; + __CPROVER_havoc_object(a->u.b->c); + return; +} + +void foo(sta *a) __CPROVER_assigns(__CPROVER_POINTER_OBJECT(a->u.b->c)) +{ + bar(a); + a->u.i = 2; + return; +} + +int main() +{ + stc *c = malloc(sizeof(*c)); + stb *b = malloc(sizeof(*b)); + sta *a = malloc(sizeof(*a)); + b->c = c; + a->u.b = b; + foo(a); + return 0; +} diff --git a/regression/contracts/assigns_enforce_havoc_object/test.desc b/regression/contracts/assigns_enforce_havoc_object/test.desc new file mode 100644 index 00000000000..03b6d7b14f0 --- /dev/null +++ b/regression/contracts/assigns_enforce_havoc_object/test.desc @@ -0,0 +1,11 @@ +CORE +main.c +--enforce-contract foo +^EXIT=10$ +^SIGNAL=0$ +^\[bar\.\d+\] line \d+ Check that \*a\->u\.b\->c is assignable: SUCCESS$ +^\[foo\.\d+\] line \d+ Check that a\->u\.i is assignable: FAILURE$ +^VERIFICATION FAILED$ +-- +-- +Checks wether contract enforcement works with arguments to __CPROVER_havoc_object. diff --git a/regression/contracts/assigns_enforce_statics/main.c b/regression/contracts/assigns_enforce_statics/main.c index 92f6f44afab..d21bf932134 100644 --- a/regression/contracts/assigns_enforce_statics/main.c +++ b/regression/contracts/assigns_enforce_statics/main.c @@ -1,15 +1,18 @@ #include #include -static int x; +static int x = 0; void foo() __CPROVER_assigns(x) { int *y = &x; - static int x; + static int x = 0; + + // should pass (assigns local x) x++; + // should fail (assigns global x) (*y)++; } diff --git a/regression/contracts/assigns_enforce_statics_subfunctions/main.c b/regression/contracts/assigns_enforce_statics_subfunctions/main.c new file mode 100644 index 00000000000..3b637dd2f59 --- /dev/null +++ b/regression/contracts/assigns_enforce_statics_subfunctions/main.c @@ -0,0 +1,31 @@ +#include +#include + +static int x; +static int xx; + +void foo() +{ + int *y = &x; + int *yy = &xx; + + static int x; + // must pass (modifies local static) + x++; + + // must pass (modifies assignable global static ) + (*y)++; + + // must fail (modifies non-assignable global static) + (*yy)++; +} + +void bar() __CPROVER_assigns(x) +{ + foo(); +} + +int main() +{ + bar(); +} diff --git a/regression/contracts/assigns_enforce_statics_subfunctions/test.desc b/regression/contracts/assigns_enforce_statics_subfunctions/test.desc new file mode 100644 index 00000000000..1a0a5abce0e --- /dev/null +++ b/regression/contracts/assigns_enforce_statics_subfunctions/test.desc @@ -0,0 +1,14 @@ +CORE +main.c +--enforce-contract bar _ --pointer-primitive-check +^EXIT=10$ +^SIGNAL=0$ +^\[foo.\d+\] line \d+ Check that y is assignable: SUCCESS$ +^\[foo.\d+\] line \d+ Check that foo\$\$1\$\$x is assignable: SUCCESS$ +^\[foo.\d+\] line \d+ Check that \*y is assignable: SUCCESS$ +^\[foo.\d+\] line \d+ Check that \*yy is assignable: FAILURE$ +^VERIFICATION FAILED$ +-- +-- +Checks whether static local and global variables are correctly tracked +in assigns clause verification, accross subfunction calls. diff --git a/regression/contracts/quantifiers-forall-ensures-enforce/main.c b/regression/contracts/quantifiers-forall-ensures-enforce/main.c index db97d407e56..cceba46be58 100644 --- a/regression/contracts/quantifiers-forall-ensures-enforce/main.c +++ b/regression/contracts/quantifiers-forall-ensures-enforce/main.c @@ -23,7 +23,7 @@ int f1(int *arr, int len) int main() { int len; - __CPROVER_assume(0 <= len && len <= MAX_LEN); + __CPROVER_assume(0 < len && len <= MAX_LEN); int *arr = malloc(len * sizeof(int)); f1(arr, len); diff --git a/src/analyses/goto_check.cpp b/src/analyses/goto_check.cpp index 1bdb812a092..c05290c4f94 100644 --- a/src/analyses/goto_check.cpp +++ b/src/analyses/goto_check.cpp @@ -25,6 +25,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #include #include #include @@ -48,9 +49,9 @@ class goto_checkt public: goto_checkt( const namespacet &_ns, - const optionst &_options): - ns(_ns), - local_bitvector_analysis(nullptr) + const optionst &_options, + message_handlert &_message_handler) + : ns(_ns), local_bitvector_analysis(nullptr), log(_message_handler) { no_enum_check = false; enable_bounds_check=_options.get_bool_option("bounds-check"); @@ -99,6 +100,8 @@ class goto_checkt std::unique_ptr local_bitvector_analysis; goto_programt::const_targett current_target; guard_managert guard_manager; + messaget log; + bool no_enum_check; /// Check an address-of expression: @@ -289,12 +292,6 @@ class goto_checkt void goto_checkt::collect_allocations( const goto_functionst &goto_functions) { - if( - !enable_pointer_check && !enable_bounds_check && - !enable_pointer_overflow_check) - { - return; - } for(const auto &gf_entry : goto_functions.function_map) { @@ -1853,27 +1850,42 @@ optionalt goto_checkt::rw_ok_check(exprt expr) /// Set a Boolean flag to a new value (via `set_flag`) and restore the previous /// value when the entire object goes out of scope. +/// Tracks flags to allow detecting double sets class flag_resett { public: - /// Store the current value of \p flag and then set its value to \p new_value. - void set_flag(bool &flag, bool new_value) + /// \brief Store the current value of \p flag and + /// then set its value to \p new_value. + /// \returns true if the flag was already seen before + bool set_flag(bool &flag, bool new_value) { + bool already_seen = seen(flag); + seen_flags.insert(&flag); if(flag != new_value) { flags_to_reset.emplace_back(&flag, flag); flag = new_value; } + return already_seen; } - /// Restore the values of all flags that have been modified via `set_flag`. + /// \brief True iff flag has already been seen by \ref set_flag + bool seen(bool &flag) + { + return seen_flags.find(&flag) != seen_flags.end(); + } + + /// \brief Restore the values of all flags that have been + /// modified via `set_flag`. ~flag_resett() { + seen_flags.clear(); for(const auto &flag_pair : flags_to_reset) *flag_pair.first = flag_pair.second; } private: + std::unordered_set seen_flags; std::list> flags_to_reset; }; @@ -1892,7 +1904,6 @@ void goto_checkt::goto_check( util_make_unique(goto_function, ns); goto_programt &goto_program=goto_function.body; - Forall_goto_program_instructions(it, goto_program) { current_target = it; @@ -1902,32 +1913,64 @@ void goto_checkt::goto_check( const auto &pragmas = i.source_location().get_pragmas(); for(const auto &d : pragmas) { + bool seen = false; if(d.first == "disable:bounds-check") - flag_resetter.set_flag(enable_bounds_check, false); + seen = flag_resetter.set_flag(enable_bounds_check, false); else if(d.first == "disable:pointer-check") - flag_resetter.set_flag(enable_pointer_check, false); + seen = flag_resetter.set_flag(enable_pointer_check, false); else if(d.first == "disable:memory-leak-check") - flag_resetter.set_flag(enable_memory_leak_check, false); + seen = flag_resetter.set_flag(enable_memory_leak_check, false); else if(d.first == "disable:div-by-zero-check") - flag_resetter.set_flag(enable_div_by_zero_check, false); + seen = flag_resetter.set_flag(enable_div_by_zero_check, false); else if(d.first == "disable:enum-range-check") - flag_resetter.set_flag(enable_enum_range_check, false); + seen = flag_resetter.set_flag(enable_enum_range_check, false); else if(d.first == "disable:signed-overflow-check") - flag_resetter.set_flag(enable_signed_overflow_check, false); + seen = flag_resetter.set_flag(enable_signed_overflow_check, false); else if(d.first == "disable:unsigned-overflow-check") - flag_resetter.set_flag(enable_unsigned_overflow_check, false); + seen = flag_resetter.set_flag(enable_unsigned_overflow_check, false); else if(d.first == "disable:pointer-overflow-check") - flag_resetter.set_flag(enable_pointer_overflow_check, false); + seen = flag_resetter.set_flag(enable_pointer_overflow_check, false); else if(d.first == "disable:float-overflow-check") - flag_resetter.set_flag(enable_float_overflow_check, false); + seen = flag_resetter.set_flag(enable_float_overflow_check, false); else if(d.first == "disable:conversion-check") - flag_resetter.set_flag(enable_conversion_check, false); + seen = flag_resetter.set_flag(enable_conversion_check, false); else if(d.first == "disable:undefined-shift-check") - flag_resetter.set_flag(enable_undefined_shift_check, false); + seen = flag_resetter.set_flag(enable_undefined_shift_check, false); else if(d.first == "disable:nan-check") - flag_resetter.set_flag(enable_nan_check, false); + seen = flag_resetter.set_flag(enable_nan_check, false); else if(d.first == "disable:pointer-primitive-check") - flag_resetter.set_flag(enable_pointer_primitive_check, false); + seen = flag_resetter.set_flag(enable_pointer_primitive_check, false); + else if(d.first == "enable:bounds-check") + seen = flag_resetter.set_flag(enable_bounds_check, true); + else if(d.first == "enable:pointer-check") + seen = flag_resetter.set_flag(enable_pointer_check, true); + else if(d.first == "enable:memory-leak-check") + seen = flag_resetter.set_flag(enable_memory_leak_check, true); + else if(d.first == "enable:div-by-zero-check") + seen = flag_resetter.set_flag(enable_div_by_zero_check, true); + else if(d.first == "enable:enum-range-check") + seen = flag_resetter.set_flag(enable_enum_range_check, true); + else if(d.first == "enable:signed-overflow-check") + seen = flag_resetter.set_flag(enable_signed_overflow_check, true); + else if(d.first == "enable:unsigned-overflow-check") + seen = flag_resetter.set_flag(enable_unsigned_overflow_check, true); + else if(d.first == "enable:pointer-overflow-check") + seen = flag_resetter.set_flag(enable_pointer_overflow_check, true); + else if(d.first == "enable:float-overflow-check") + seen = flag_resetter.set_flag(enable_float_overflow_check, true); + else if(d.first == "enable:conversion-check") + seen = flag_resetter.set_flag(enable_conversion_check, true); + else if(d.first == "enable:undefined-shift-check") + seen = flag_resetter.set_flag(enable_undefined_shift_check, true); + else if(d.first == "enable:nan-check") + seen = flag_resetter.set_flag(enable_nan_check, true); + else if(d.first == "enable:pointer-primitive-check") + seen = flag_resetter.set_flag(enable_pointer_primitive_check, true); + + INVARIANT( + !seen, + "Found enable and disable pragmas for " + id2string(d.first) + + " at \n" + i.source_location().pretty()); } new_code.clear(); @@ -2378,18 +2421,20 @@ void goto_check( const irep_idt &function_identifier, goto_functionst::goto_functiont &goto_function, const namespacet &ns, - const optionst &options) + const optionst &options, + message_handlert &message_handler) { - goto_checkt goto_check(ns, options); + goto_checkt goto_check(ns, options, message_handler); goto_check.goto_check(function_identifier, goto_function); } void goto_check( const namespacet &ns, const optionst &options, - goto_functionst &goto_functions) + goto_functionst &goto_functions, + message_handlert &message_handler) { - goto_checkt goto_check(ns, options); + goto_checkt goto_check(ns, options, message_handler); goto_check.collect_allocations(goto_functions); @@ -2401,8 +2446,9 @@ void goto_check( void goto_check( const optionst &options, - goto_modelt &goto_model) + goto_modelt &goto_model, + message_handlert &message_handler) { const namespacet ns(goto_model.symbol_table); - goto_check(ns, options, goto_model.goto_functions); + goto_check(ns, options, goto_model.goto_functions, message_handler); } diff --git a/src/analyses/goto_check.h b/src/analyses/goto_check.h index 58f4a20696f..f214cfbdc4d 100644 --- a/src/analyses/goto_check.h +++ b/src/analyses/goto_check.h @@ -17,21 +17,25 @@ Author: Daniel Kroening, kroening@kroening.com class goto_modelt; class namespacet; class optionst; +class message_handlert; void goto_check( const namespacet &ns, const optionst &options, - goto_functionst &goto_functions); + goto_functionst &goto_functions, + message_handlert &message_handler); void goto_check( const irep_idt &function_identifier, goto_functionst::goto_functiont &goto_function, const namespacet &ns, - const optionst &options); + const optionst &options, + message_handlert &message_handler); void goto_check( const optionst &options, - goto_modelt &goto_model); + goto_modelt &goto_model, + message_handlert &message_handler); #define OPT_GOTO_CHECK \ "(bounds-check)(pointer-check)(memory-leak-check)" \ diff --git a/src/ansi-c/ansi_c_parser.cpp b/src/ansi-c/ansi_c_parser.cpp index 61d2825e662..66ad625b2e9 100644 --- a/src/ansi-c/ansi_c_parser.cpp +++ b/src/ansi-c/ansi_c_parser.cpp @@ -19,21 +19,18 @@ ansi_c_id_classt ansi_c_parsert::lookup( bool label) { // labels and tags have a separate name space - const irep_idt scope_name= - tag?"tag-"+id2string(base_name): - label?"label-"+id2string(base_name): - base_name; + const irep_idt scope_name = + tag ? "tag-" + id2string(base_name) + : label ? "label-" + id2string(base_name) : base_name; - for(scopest::const_reverse_iterator it=scopes.rbegin(); - it!=scopes.rend(); + for(scopest::const_reverse_iterator it = scopes.rbegin(); it != scopes.rend(); it++) { - scopet::name_mapt::const_iterator n_it= - it->name_map.find(scope_name); + scopet::name_mapt::const_iterator n_it = it->name_map.find(scope_name); - if(n_it!=it->name_map.end()) + if(n_it != it->name_map.end()) { - identifier=n_it->second.prefixed_name; + identifier = n_it->second.prefixed_name; return n_it->second.id_class; } } @@ -42,33 +39,30 @@ ansi_c_id_classt ansi_c_parsert::lookup( // If it's a tag, we will add to current scope. if(tag) { - ansi_c_identifiert &i= - current_scope().name_map[scope_name]; - i.id_class=ansi_c_id_classt::ANSI_C_TAG; - i.prefixed_name=current_scope().prefix+id2string(scope_name); - i.base_name=base_name; - identifier=i.prefixed_name; + ansi_c_identifiert &i = current_scope().name_map[scope_name]; + i.id_class = ansi_c_id_classt::ANSI_C_TAG; + i.prefixed_name = current_scope().prefix + id2string(scope_name); + i.base_name = base_name; + identifier = i.prefixed_name; return ansi_c_id_classt::ANSI_C_TAG; } - identifier=base_name; + identifier = base_name; return ansi_c_id_classt::ANSI_C_UNKNOWN; } void ansi_c_parsert::add_tag_with_body(irept &tag) { - const std::string scope_name= - "tag-"+tag.get_string(ID_C_base_name); + const std::string scope_name = "tag-" + tag.get_string(ID_C_base_name); - irep_idt prefixed_name=current_scope().prefix+scope_name; + irep_idt prefixed_name = current_scope().prefix + scope_name; - if(prefixed_name!=tag.get(ID_identifier)) + if(prefixed_name != tag.get(ID_identifier)) { // re-defined in a deeper scope - ansi_c_identifiert &identifier= - current_scope().name_map[scope_name]; - identifier.id_class=ansi_c_id_classt::ANSI_C_TAG; - identifier.prefixed_name=prefixed_name; + ansi_c_identifiert &identifier = current_scope().name_map[scope_name]; + identifier.id_class = ansi_c_id_classt::ANSI_C_TAG; + identifier.prefixed_name = prefixed_name; tag.set(ID_identifier, prefixed_name); } } @@ -81,21 +75,18 @@ int yyansi_cerror(const std::string &error) return 0; } -void ansi_c_parsert::add_declarator( - exprt &declaration, - irept &declarator) +void ansi_c_parsert::add_declarator(exprt &declaration, irept &declarator) { assert(declarator.is_not_nil()); - ansi_c_declarationt &ansi_c_declaration= - to_ansi_c_declaration(declaration); + ansi_c_declarationt &ansi_c_declaration = to_ansi_c_declaration(declaration); ansi_c_declaratort new_declarator; new_declarator.build(declarator); - irep_idt base_name=new_declarator.get_base_name(); + irep_idt base_name = new_declarator.get_base_name(); - bool is_member=ansi_c_declaration.get_is_member(); - bool is_parameter=ansi_c_declaration.get_is_parameter(); + bool is_member = ansi_c_declaration.get_is_member(); + bool is_parameter = ansi_c_declaration.get_is_parameter(); if(is_member) { @@ -113,39 +104,35 @@ void ansi_c_parsert::add_declarator( if(!base_name.empty()) { c_storage_spect c_storage_spec(ansi_c_declaration.type()); - bool is_typedef=c_storage_spec.is_typedef; - bool is_extern=c_storage_spec.is_extern; + bool is_typedef = c_storage_spec.is_typedef; + bool is_extern = c_storage_spec.is_extern; - bool force_root_scope=false; + bool force_root_scope = false; // Functions always go into global scope, unless // declared as a parameter or are typedefs. - if(new_declarator.type().id()==ID_code && - !is_parameter && - !is_typedef) - force_root_scope=true; + if(new_declarator.type().id() == ID_code && !is_parameter && !is_typedef) + force_root_scope = true; // variables marked as 'extern' always go into global scope if(is_extern) - force_root_scope=true; + force_root_scope = true; - ansi_c_id_classt id_class=is_typedef? - ansi_c_id_classt::ANSI_C_TYPEDEF: - ansi_c_id_classt::ANSI_C_SYMBOL; + ansi_c_id_classt id_class = is_typedef ? ansi_c_id_classt::ANSI_C_TYPEDEF + : ansi_c_id_classt::ANSI_C_SYMBOL; - scopet &scope= - force_root_scope?root_scope():current_scope(); + scopet &scope = force_root_scope ? root_scope() : current_scope(); // set the final name - irep_idt prefixed_name=force_root_scope? - base_name: - current_scope().prefix+id2string(base_name); + irep_idt prefixed_name = force_root_scope + ? base_name + : current_scope().prefix + id2string(base_name); new_declarator.set_name(prefixed_name); // add to scope - ansi_c_identifiert &identifier=scope.name_map[base_name]; - identifier.id_class=id_class; - identifier.prefixed_name=prefixed_name; + ansi_c_identifiert &identifier = scope.name_map[base_name]; + identifier.id_class = id_class; + identifier.prefixed_name = prefixed_name; if(force_root_scope) current_scope().name_map[base_name] = identifier; @@ -156,13 +143,12 @@ void ansi_c_parsert::add_declarator( ansi_c_id_classt ansi_c_parsert::get_class(const typet &type) { - if(type.id()==ID_typedef) + if(type.id() == ID_typedef) return ansi_c_id_classt::ANSI_C_TYPEDEF; - else if(type.id()==ID_struct || - type.id()==ID_union || - type.id()==ID_c_enum) + else if( + type.id() == ID_struct || type.id() == ID_union || type.id() == ID_c_enum) return ansi_c_id_classt::ANSI_C_TAG; - else if(type.id()==ID_merged_type) + else if(type.id() == ID_merged_type) { for(const typet &subtype : to_type_with_subtypes(type).subtypes()) { @@ -175,3 +161,56 @@ ansi_c_id_classt ansi_c_parsert::get_class(const typet &type) return ansi_c_id_classt::ANSI_C_SYMBOL; } + +bool ansi_c_parsert::pragma_cprover_empty() +{ + return pragma_cprover_stack.empty(); +} + +void ansi_c_parsert::pragma_cprover_push() +{ + std::map empty; + pragma_cprover_stack.push_back(std::move(empty)); +} + +void ansi_c_parsert::pragma_cprover_pop() +{ + pragma_cprover_stack.pop_back(); +} + +void ansi_c_parsert::pragma_cprover_add_check(irep_idt name, bool enabled) +{ + if(pragma_cprover_stack.empty()) + pragma_cprover_push(); + + pragma_cprover_stack.back()[name] = enabled; +} + +bool ansi_c_parsert::pragma_cprover_clash(irep_idt name, bool enabled) +{ + auto top = pragma_cprover_stack.back(); + auto found = top.find(name); + return found != top.end() && found->second != enabled; +} + +void ansi_c_parsert::set_pragma_cprover() +{ + // handle enable/disable shadowing + // by bottom-to-top flattening + std::map flattened; + + for(const auto &pragma_set : pragma_cprover_stack) + for(const auto &pragma : pragma_set) + flattened[pragma.first] = pragma.second; + + source_location.remove(ID_pragma); + + for(const auto &pragma : flattened) + { + std::string check_name = id2string(pragma.first); + std::string full_name = pragma.second + ? std::string("enable:") + check_name + : std::string("disable:") + check_name; + source_location.add_pragma(full_name); + } +} diff --git a/src/ansi-c/ansi_c_parser.h b/src/ansi-c/ansi_c_parser.h index 2427a8b15a3..ea5f140d171 100644 --- a/src/ansi-c/ansi_c_parser.h +++ b/src/ansi-c/ansi_c_parser.h @@ -6,21 +6,21 @@ Author: Daniel Kroening, kroening@kroening.com \*******************************************************************/ - #ifndef CPROVER_ANSI_C_ANSI_C_PARSER_H #define CPROVER_ANSI_C_ANSI_C_PARSER_H +#include #include -#include #include +#include #include "ansi_c_parse_tree.h" #include "ansi_c_scope.h" int yyansi_cparse(); -class ansi_c_parsert:public parsert +class ansi_c_parsert : public parsert { public: ansi_c_parse_treet parse_tree; @@ -39,7 +39,7 @@ class ansi_c_parsert:public parsert virtual bool parse() override { - return yyansi_cparse()!=0; + return yyansi_cparse() != 0; } virtual void clear() override @@ -48,12 +48,12 @@ class ansi_c_parsert:public parsert parse_tree.clear(); // scanner state - tag_following=false; - asm_block_following=false; - parenthesis_counter=0; + tag_following = false; + asm_block_following = false; + parenthesis_counter = 0; string_literal.clear(); pragma_pack.clear(); - pragma_cprover.clear(); + pragma_cprover_stack.clear(); // set up global scope scopes.clear(); @@ -66,7 +66,7 @@ class ansi_c_parsert:public parsert unsigned parenthesis_counter; std::string string_literal; std::list pragma_pack; - std::list> pragma_cprover; + std::list> pragma_cprover_stack; typedef configt::ansi_ct::flavourt modet; modet mode; @@ -107,7 +107,13 @@ class ansi_c_parsert:public parsert return scopes.back(); } - enum class decl_typet { TAG, MEMBER, PARAMETER, OTHER }; + enum class decl_typet + { + TAG, + MEMBER, + PARAMETER, + OTHER + }; // convert a declarator and then add it to existing an declaration void add_declarator(exprt &declaration, irept &declarator); @@ -117,20 +123,20 @@ class ansi_c_parsert:public parsert void copy_item(const ansi_c_declarationt &declaration) { - assert(declaration.id()==ID_declaration); + assert(declaration.id() == ID_declaration); parse_tree.items.push_back(declaration); } void new_scope(const std::string &prefix) { - const scopet ¤t=current_scope(); + const scopet ¤t = current_scope(); scopes.push_back(scopet()); - scopes.back().prefix=current.prefix+prefix; + scopes.back().prefix = current.prefix + prefix; } ansi_c_id_classt lookup( const irep_idt &base_name, // in - irep_idt &identifier, // out + irep_idt &identifier, // out bool tag, bool label); @@ -143,15 +149,25 @@ class ansi_c_parsert:public parsert return identifier; } - void set_pragma_cprover() - { - source_location.remove(ID_pragma); - for(const auto &pragma_set : pragma_cprover) - { - for(const auto &pragma : pragma_set) - source_location.add_pragma(pragma); - } - } + /// \brief True iff the CPROVER pragma stack is empty + bool pragma_cprover_empty(); + + /// \brief Pushes an empty level in the CPROVER pragma stack + void pragma_cprover_push(); + + /// \brief Pops a level in the CPROVER pragma stack + void pragma_cprover_pop(); + + /// \brief Adds a check to the CPROVER pragma stack + void pragma_cprover_add_check(irep_idt name, bool enabled); + + /// Returns true the same check with different polarity + /// is already present at top of the stack + bool pragma_cprover_clash(irep_idt name, bool enabled); + + /// \brief Tags \ref source_location with + /// the current CPROVER pragma stack + void set_pragma_cprover(); }; extern ansi_c_parsert ansi_c_parser; diff --git a/src/ansi-c/scanner.l b/src/ansi-c/scanner.l index 295988fdf6f..100ff57c1eb 100644 --- a/src/ansi-c/scanner.l +++ b/src/ansi-c/scanner.l @@ -238,6 +238,7 @@ pointer_primitive "pointer-primitive" memory_check ("bounds"|"pointer"|"memory_leak") overflow_check ("signed"|"unsigned"|"pointer"|"float")"-overflow" named_check ["]({arith_check}|{enum_check}|{memory_check}|{overflow_check}|{pointer_primitive})["] +enable_or_disable ("enable"|"disable") %x GRAMMAR %x COMMENT1 @@ -402,29 +403,33 @@ void ansi_c_scanner_init() /* CProver specific pragmas: hint to disable named checks */ {ws}"check"{ws}"push" { - PARSER.pragma_cprover.push_back({}); + PARSER.pragma_cprover_push(); } {ws}"check"{ws}"pop" { - if(!PARSER.pragma_cprover.empty()) + if(!PARSER.pragma_cprover_empty()) { - PARSER.pragma_cprover.pop_back(); + PARSER.pragma_cprover_pop(); PARSER.set_pragma_cprover(); } } -{ws}"check"{ws}"disable"{ws}{named_check} { +{ws}"check"{ws}{enable_or_disable}{ws}{named_check} { std::string tmp(yytext); + bool enable = tmp.find("enable")!=std::string::npos; std::string::size_type p = tmp.find('"') + 1; - std::string value = - std::string("disable:") + + std::string check_name = std::string(tmp, p, tmp.size() - p - 1) + std::string("-check"); - if(PARSER.pragma_cprover.empty()) - PARSER.pragma_cprover.push_back({value}); - else - PARSER.pragma_cprover.back().insert(value); + bool clash = PARSER.pragma_cprover_clash(check_name, enable); + if(clash) + { + yyansi_cerror( + "Found enable and disable pragmas for " + + id2string(check_name)); + return TOK_SCANNER_ERROR; + } + PARSER.pragma_cprover_add_check(check_name, enable); PARSER.set_pragma_cprover(); } - . { yyansi_cerror("Unsupported #pragma CPROVER"); return TOK_SCANNER_ERROR; diff --git a/src/goto-instrument/contracts/assigns.cpp b/src/goto-instrument/contracts/assigns.cpp index c79354e9621..48b12c5f1f3 100644 --- a/src/goto-instrument/contracts/assigns.cpp +++ b/src/goto-instrument/contracts/assigns.cpp @@ -41,15 +41,17 @@ static const slicet normalize_to_slice(const exprt &expr, const namespacet &ns) size.has_value(), "`sizeof` must always be computable on l-value assigns clause targets."); - return {typecast_exprt::conditional_cast( - address_of_exprt{expr}, pointer_type(char_type())), - typecast_exprt::conditional_cast(size.value(), signed_size_type())}; + return { + typecast_exprt::conditional_cast( + address_of_exprt{expr}, pointer_type(char_type())), + typecast_exprt::conditional_cast(size.value(), signed_size_type())}; } UNREACHABLE; } const symbolt assigns_clauset::conditional_address_ranget::generate_new_symbol( + const std::string &prefix, const typet &type, const source_locationt &location) const { @@ -57,7 +59,8 @@ const symbolt assigns_clauset::conditional_address_ranget::generate_new_symbol( type, location, parent.symbol_table.lookup_ref(parent.function_name).mode, - parent.symbol_table); + parent.symbol_table, + prefix); } assigns_clauset::conditional_address_ranget::conditional_address_ranget( @@ -68,54 +71,87 @@ assigns_clauset::conditional_address_ranget::conditional_address_ranget( parent(parent), slice(normalize_to_slice(expr, parent.ns)), validity_condition_var( - generate_new_symbol(bool_typet(), location).symbol_expr()), + generate_new_symbol("__car_valid", bool_typet(), location).symbol_expr()), lower_bound_address_var( - generate_new_symbol(slice.first.type(), location).symbol_expr()), + generate_new_symbol("__car_lb", slice.first.type(), location) + .symbol_expr()), upper_bound_address_var( - generate_new_symbol(slice.first.type(), location).symbol_expr()) + generate_new_symbol("__car_ub", slice.first.type(), location) + .symbol_expr()) { } +// clang-format off +/// \brief Generates and returns snapshot instructions for source_expr. +/// +/// ``` +/// DECL bool __car_valid +/// DECL char *__car_lb +/// DECL char *__car_ub +/// ASSIGN __car_lb := NULL +/// ASSIGN __car_ub := NULL +/// ASSIGN __car_valid := all_dereferences_are_valid(source_expr) & rw_ok(&(source_expr), size) +/// IF !__car_valid GOTO END_SNAPSHOT +/// ASSIGN __car_lb := &(source_expr) +/// ASSIGN __car_ub := &(source_expr) + size-1 +/// END_SNAPSHOT: SKIP +/// ``` +// clang-format on goto_programt assigns_clauset::conditional_address_ranget::generate_snapshot_instructions() const { goto_programt instructions; - - instructions.add(goto_programt::make_decl(validity_condition_var, location)); - instructions.add(goto_programt::make_decl(lower_bound_address_var, location)); - instructions.add(goto_programt::make_decl(upper_bound_address_var, location)); + // adding pragmas to the location to selectively disable checks + // where it is sound to do so + source_locationt location_no_checks = location; + location_no_checks.add_pragma("disable:pointer-check"); + location_no_checks.add_pragma("disable:pointer-primitive-check"); + location_no_checks.add_pragma("disable:pointer-overflow-check"); + + instructions.add( + goto_programt::make_decl(validity_condition_var, location_no_checks)); + instructions.add( + goto_programt::make_decl(lower_bound_address_var, location_no_checks)); + instructions.add( + goto_programt::make_decl(upper_bound_address_var, location_no_checks)); instructions.add(goto_programt::make_assignment( lower_bound_address_var, null_pointer_exprt{to_pointer_type(slice.first.type())}, - location)); + location_no_checks)); instructions.add(goto_programt::make_assignment( upper_bound_address_var, null_pointer_exprt{to_pointer_type(slice.first.type())}, - location)); + location_no_checks)); + + // check validity + const auto validity_check_expr = and_exprt{ + all_dereferences_are_valid(source_expr, parent.ns), + w_ok_exprt{slice.first, slice.second}}; + instructions.add(goto_programt::make_assignment( + validity_condition_var, validity_check_expr, location_no_checks)); + // jump here if validity_check_expr is false goto_programt skip_program; const auto skip_target = skip_program.add(goto_programt::make_skip(location)); - const auto validity_check_expr = - and_exprt{all_dereferences_are_valid(source_expr, parent.ns), - w_ok_exprt{slice.first, slice.second}}; - instructions.add(goto_programt::make_assignment( - validity_condition_var, validity_check_expr, location)); - instructions.add(goto_programt::make_goto( - skip_target, not_exprt{validity_condition_var}, location)); + skip_target, not_exprt{validity_condition_var}, location_no_checks)); instructions.add(goto_programt::make_assignment( - lower_bound_address_var, slice.first, location)); + lower_bound_address_var, slice.first, location_no_checks)); + + source_locationt location_overflow_check = location; + location_overflow_check.add_pragma("enable:pointer-overflow-check"); instructions.add(goto_programt::make_assignment( upper_bound_address_var, - minus_exprt{plus_exprt{slice.first, slice.second}, - from_integer(1, slice.second.type())}, - location)); - + minus_exprt{ + plus_exprt{slice.first, slice.second}, + from_integer(1, slice.second.type())}, + // activate pointer-overflow checks to guard against overflow on this addition + location_overflow_check)); instructions.destructive_append(skip_program); return instructions; } @@ -127,11 +163,14 @@ assigns_clauset::conditional_address_ranget::generate_unsafe_inclusion_check( return conjunction( {validity_condition_var, same_object(lower_bound_address_var, lhs.lower_bound_address_var), - same_object(lhs.upper_bound_address_var, upper_bound_address_var), - less_than_or_equal_exprt{lower_bound_address_var, - lhs.lower_bound_address_var}, - less_than_or_equal_exprt{lhs.upper_bound_address_var, - upper_bound_address_var}}); + // redudant now that we guard against pointer overflow + // same_object(lhs.upper_bound_address_var, upper_bound_address_var), + less_than_or_equal_exprt{ + pointer_offset(lower_bound_address_var), + pointer_offset(lhs.lower_bound_address_var)}, + less_than_or_equal_exprt{ + pointer_offset(lhs.upper_bound_address_var), + pointer_offset(upper_bound_address_var)}}); } assigns_clauset::assigns_clauset( diff --git a/src/goto-instrument/contracts/assigns.h b/src/goto-instrument/contracts/assigns.h index bdc97ead1d9..1cd2eb64af4 100644 --- a/src/goto-instrument/contracts/assigns.h +++ b/src/goto-instrument/contracts/assigns.h @@ -61,7 +61,9 @@ class assigns_clauset generate_unsafe_inclusion_check(const conditional_address_ranget &) const; const symbolt - generate_new_symbol(const typet &, const source_locationt &) const; + generate_new_symbol( + const std::string &prefix, + const typet &, const source_locationt &) const; friend class assigns_clauset; }; diff --git a/src/goto-instrument/contracts/contracts.cpp b/src/goto-instrument/contracts/contracts.cpp index 6b1724a4c4f..9db6a0e6a3d 100644 --- a/src/goto-instrument/contracts/contracts.cpp +++ b/src/goto-instrument/contracts/contracts.cpp @@ -15,6 +15,8 @@ Date: February 2016 #include #include +#include +#include #include @@ -677,6 +679,11 @@ void code_contractst::instrument_call_statement( } else if(callee_name == "free") { + source_locationt &source_location_no_checks = instruction_it->source_location_nonconst(); + source_location_no_checks.add_pragma("disable:pointer-check"); + source_location_no_checks.add_pragma("disable:pointer-primitive-check"); + source_location_no_checks.add_pragma("disable:pointer-overflow-check"); + const auto free_car = add_inclusion_check( body, assigns, @@ -687,9 +694,9 @@ void code_contractst::instrument_call_statement( goto_programt alias_checking_instructions, skip_program; alias_checking_instructions.add(goto_programt::make_goto( skip_program.add( - goto_programt::make_skip(instruction_it->source_location())), + goto_programt::make_skip(source_location_no_checks)), not_exprt{free_car.validity_condition_var}, - instruction_it->source_location())); + source_location_no_checks)); // Since the argument to free may be an "alias" (but not identical) // to existing CARs' source_expr, structural equality wouldn't work. @@ -702,14 +709,15 @@ void code_contractst::instrument_call_statement( const auto object_validity_var_addr = new_tmp_symbol( pointer_type(bool_typet{}), - instruction_it->source_location(), + source_location_no_checks, symbol_table.lookup_ref(function).mode, - symbol_table) + symbol_table, + "__car_valid") .symbol_expr(); write_set_validity_addrs.insert(object_validity_var_addr); alias_checking_instructions.add(goto_programt::make_decl( - object_validity_var_addr, instruction_it->source_location())); + object_validity_var_addr, source_location_no_checks)); // if the CAR was defined on the same_object as the one being `free`d, // record its validity variable's address, otherwise record NULL alias_checking_instructions.add(goto_programt::make_assignment( @@ -721,7 +729,7 @@ void code_contractst::instrument_call_statement( free_car.lower_bound_address_var, w_car.lower_bound_address_var)}, address_of_exprt{w_car.validity_condition_var}, null_pointer_exprt{to_pointer_type(object_validity_var_addr.type())}}, - instruction_it->source_location())); + source_location_no_checks)); } alias_checking_instructions.destructive_append(skip_program); @@ -736,9 +744,9 @@ void code_contractst::instrument_call_statement( skip_program.clear(); invalidation_instructions.add(goto_programt::make_goto( skip_program.add( - goto_programt::make_skip(instruction_it->source_location())), + goto_programt::make_skip(source_location_no_checks)), not_exprt{free_car.validity_condition_var}, - instruction_it->source_location())); + source_location_no_checks)); // invalidate all recorded CAR validity variables for(const auto &w_car_validity_addr : write_set_validity_addrs) @@ -746,13 +754,13 @@ void code_contractst::instrument_call_statement( goto_programt w_car_skip_program; invalidation_instructions.add(goto_programt::make_goto( w_car_skip_program.add( - goto_programt::make_skip(instruction_it->source_location())), + goto_programt::make_skip(source_location_no_checks)), null_pointer(w_car_validity_addr), - instruction_it->source_location())); + source_location_no_checks)); invalidation_instructions.add(goto_programt::make_assignment( dereference_exprt{w_car_validity_addr}, false_exprt{}, - instruction_it->source_location())); + source_location_no_checks)); invalidation_instructions.destructive_append(w_car_skip_program); } @@ -844,6 +852,9 @@ bool code_contractst::check_frame_conditions_function(const irep_idt &function) return true; } + // Full inlining of the function body + goto_function_inline(goto_functions, function, ns, log.get_message_handler()); + // Get assigns clause for function const symbolt &target = ns.lookup(function); assigns_clauset assigns( @@ -853,17 +864,12 @@ bool code_contractst::check_frame_conditions_function(const irep_idt &function) function, symbol_table); - // Adds formal parameters to write set + // Add formal parameters to write set for(const auto ¶m : to_code_type(target.type).parameters()) assigns.add_to_write_set(ns.lookup(param.get_identifier()).symbol_expr()); - // Adds local static declarations to write set - for(const auto &sym_pair : symbol_table) - { - const auto &sym = sym_pair.second; - if(sym.is_static_lifetime && sym.location.get_function() == function) - assigns.add_to_write_set(sym.symbol_expr()); - } + // Detect local static variables and add them to the write set + find_static_locals(function_obj->second, assigns); auto instruction_it = function_obj->second.body.instructions.begin(); for(const auto &car : assigns.get_write_set()) @@ -886,8 +892,6 @@ void code_contractst::check_frame_conditions( goto_programt::targett &instruction_it, assigns_clauset &assigns) { - goto_function_inline(goto_functions, function, ns, log.get_message_handler()); - for(; instruction_it != body.instructions.end(); ++instruction_it) { if(instruction_it->is_decl()) @@ -916,6 +920,10 @@ void code_contractst::check_frame_conditions( else if(instruction_it->is_dead()) { const auto &symbol = instruction_it->dead_symbol(); + source_locationt &source_location_no_checks = instruction_it->source_location_nonconst(); + source_location_no_checks.add_pragma("disable:pointer-check"); + source_location_no_checks.add_pragma("disable:pointer-primitive-check"); + source_location_no_checks.add_pragma("disable:pointer-overflow-check"); // CAR equality and hash are defined on source_expr alone, // therefore this temporary CAR should be "found" const auto &symbol_car = assigns.get_write_set().find( @@ -962,10 +970,14 @@ code_contractst::add_inclusion_check( program, instruction_it, snapshot_instructions); goto_programt assertion; - assertion.add(goto_programt::make_assertion( - assigns.generate_inclusion_check(car), instruction_it->source_location())); - assertion.instructions.back().source_location_nonconst().set_comment( + source_locationt source_location = instruction_it->source_location_nonconst(); + source_location.add_pragma("disable:pointer-check"); + source_location.add_pragma("disable:pointer-primitive-check"); + source_location.add_pragma("disable:pointer-overflow-check"); + source_location.set_comment( "Check that " + from_expr(ns, expr.id(), expr) + " is assignable"); + assertion.add(goto_programt::make_assertion( + assigns.generate_inclusion_check(car), source_location)); insert_before_swap_and_advance(program, instruction_it, assertion); return car; @@ -1260,3 +1272,63 @@ bool code_contractst::enforce_contracts(const std::set &to_enforce) } return fail; } + +void code_contractst::find_static_locals( + const goto_functiont &function, + assigns_clauset &assigns) +{ + find_symbols_sett tmp_set; + + // find symbols in all possible places + forall_goto_program_instructions(inst, function.body) + { + // this covers ASSERT/ASSUME and guarded instructions + if(inst->has_condition()) + find_symbols(inst->condition(), tmp_set, true, false); + + if(inst->is_assign()) + { + if(inst->assign_lhs().is_not_nil()) + find_symbols(inst->assign_lhs(), tmp_set, true, false); + + if(inst->assign_rhs().is_not_nil()) + find_symbols(inst->assign_rhs(), tmp_set, true, false); + } + + if(inst->is_set_return_value()) + find_symbols(inst->return_value(), tmp_set, true, false); + + if(inst->is_function_call()) + { + if(inst->call_lhs().is_not_nil()) + find_symbols(inst->call_lhs(), tmp_set, true, false); + + // we DO NOT recurse into function calls + find_symbols(inst->call_function(), tmp_set, true, false); + + forall_expr(e_it, inst->call_arguments()) + { + find_symbols(*e_it, tmp_set, true, false); + } + } + + if(inst->is_other()) + find_symbols(inst->get_other(), tmp_set, true, false); + } + + // filter symbols with static lifetime and non-empty function attribute + // and add them to the assigns clause + for(auto it = tmp_set.begin(); it != tmp_set.end(); it++) + { + symbolt sym = ns.lookup(*it); + bool is_local_static = + sym.is_static_lifetime && !sym.location.get_function().empty(); + if(is_local_static) + assigns.add_to_write_set(sym.symbol_expr()); + } + + // clear set + tmp_set.clear(); + + return; +} diff --git a/src/goto-instrument/contracts/contracts.h b/src/goto-instrument/contracts/contracts.h index bd79f6e3b7c..24339b76336 100644 --- a/src/goto-instrument/contracts/contracts.h +++ b/src/goto-instrument/contracts/contracts.h @@ -210,6 +210,29 @@ class code_contractst codet &expression, source_locationt location, const irep_idt &mode); + + + /// Finds static local symbols that occur in the body of the given function and adds them to the the write set of `assigns`. + /// + /// @param function the function to search local static symbols in + /// @param assigns assigns clause where search results are added + /// + /// A symbol is considered a static local symbol iff: + /// - it has a static lifetime annotation + /// - its source location has a non-empty function attribute + /// + /// Symbol occurrences are searched in: + /// - ASSERT/ASSUME conditions + /// - ASSIGN lhs and rhs + /// - FUNCTION_CALL function, lhs and operands + /// - SET_RETURN_VALUE instructions + /// - OTHER code. + /// + /// The search does *not*: + /// - recurse into FUNCTION_CALL + /// - test DECL or DEAD symbols (because local statics are never DECL'd or DEAD'd for being static). + /// - test attributes of GOTO, SET_RETURN_VALUE, THREAD*, ATOMIC*, THROW, CATCH instructions + void find_static_locals(const goto_functiont &function, assigns_clauset &assigns); }; #endif // CPROVER_GOTO_INSTRUMENT_CONTRACTS_CONTRACTS_H diff --git a/src/goto-instrument/contracts/utils.cpp b/src/goto-instrument/contracts/utils.cpp index b1c199229d5..68b0b9a0605 100644 --- a/src/goto-instrument/contracts/utils.cpp +++ b/src/goto-instrument/contracts/utils.cpp @@ -127,12 +127,13 @@ const symbolt &new_tmp_symbol( const typet &type, const source_locationt &location, const irep_idt &mode, - symbol_table_baset &symtab) + symbol_table_baset &symtab, + std::string suffix) { return get_fresh_aux_symbol( type, - id2string(location.get_function()) + "::tmp_cc", - "tmp_cc", + id2string(location.get_function()) + "::", + suffix, location, mode, symtab); diff --git a/src/goto-instrument/contracts/utils.h b/src/goto-instrument/contracts/utils.h index 3be8c8f965d..8090bc71473 100644 --- a/src/goto-instrument/contracts/utils.h +++ b/src/goto-instrument/contracts/utils.h @@ -91,15 +91,22 @@ void insert_before_swap_and_advance( /// \brief Adds a new temporary symbol to the symbol table. /// +/// The unique name is generated as: +/// ``` +/// "location.function() + "::" + suffix + "$" + uid +/// ``` +/// /// \param type: The type of the new symbol. /// \param location: The source location for the new symbol. /// \param mode: The mode for the new symbol, e.g. ID_C, ID_java. /// \param symtab: The symbol table to which the new symbol is to be added. +/// \param suffix: base suffix used to generate the unique name. /// \return The new symbolt object. const symbolt &new_tmp_symbol( const typet &type, const source_locationt &location, const irep_idt &mode, - symbol_table_baset &symtab); + symbol_table_baset &symtab, + std::string suffix = "tmp_cc"); #endif // CPROVER_GOTO_INSTRUMENT_CONTRACTS_UTILS_H diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp index 8bc4ff2b7a7..a7230c723d6 100644 --- a/src/goto-instrument/goto_instrument_parse_options.cpp +++ b/src/goto-instrument/goto_instrument_parse_options.cpp @@ -1332,7 +1332,7 @@ void goto_instrument_parse_optionst::instrument_goto_program() } // add generic checks, if needed - goto_check(options, goto_model); + goto_check(options, goto_model, log.get_message_handler()); // check for uninitalized local variables if(cmdline.isset("uninitialized-check")) diff --git a/src/goto-programs/process_goto_program.cpp b/src/goto-programs/process_goto_program.cpp index 68121ab9335..0252e121125 100644 --- a/src/goto-programs/process_goto_program.cpp +++ b/src/goto-programs/process_goto_program.cpp @@ -66,7 +66,7 @@ bool process_goto_program( // add generic checks log.status() << "Generic Property Instrumentation" << messaget::eom; - goto_check(options, goto_model); + goto_check(options, goto_model, log.get_message_handler()); // checks don't know about adjusted float expressions adjust_float_expressions(goto_model);