diff --git a/regression/contracts/assigns_enforce_04/test.desc b/regression/contracts/assigns_enforce_04/test.desc index b1a24463b4d..2e1caa26893 100644 --- a/regression/contracts/assigns_enforce_04/test.desc +++ b/regression/contracts/assigns_enforce_04/test.desc @@ -3,12 +3,6 @@ main.c --enforce-contract f1 ^EXIT=0$ ^SIGNAL=0$ -^\[f1.\d+\] line \d+ Check that x2 is assignable: SUCCESS$ -^\[f1.\d+\] line \d+ Check that y2 is assignable: SUCCESS$ -^\[f1.\d+\] line \d+ Check that z2 is assignable: SUCCESS$ -^\[f2.\d+\] line \d+ Check that x3 is assignable: SUCCESS$ -^\[f2.\d+\] line \d+ Check that y3 is assignable: SUCCESS$ -^\[f2.\d+\] line \d+ Check that z3 is assignable: SUCCESS$ ^\[f3.\d+\] line \d+ Check that \*x3 is assignable: SUCCESS$ ^\[f3.\d+\] line \d+ Check that \*y3 is assignable: SUCCESS$ ^\[f3.\d+\] line \d+ Check that \*z3 is assignable: SUCCESS$ diff --git a/regression/contracts/assigns_enforce_05/test.desc b/regression/contracts/assigns_enforce_05/test.desc index 6c7363f88d0..97352a948f2 100644 --- a/regression/contracts/assigns_enforce_05/test.desc +++ b/regression/contracts/assigns_enforce_05/test.desc @@ -3,7 +3,6 @@ main.c --enforce-contract f1 --enforce-contract f2 --enforce-contract f3 ^EXIT=0$ ^SIGNAL=0$ -^\[f1.1\] line \d+ .*: SUCCESS$ ^VERIFICATION SUCCESSFUL$ -- -- diff --git a/regression/contracts/assigns_enforce_18/test.desc b/regression/contracts/assigns_enforce_18/test.desc index 011006f19c6..355b7179170 100644 --- a/regression/contracts/assigns_enforce_18/test.desc +++ b/regression/contracts/assigns_enforce_18/test.desc @@ -7,7 +7,6 @@ main.c ^\[bar.\d+\] line \d+ Check that \*b is assignable: SUCCESS$ ^\[baz.\d+\] line \d+ Check that POINTER_OBJECT\(\(void \*\)c\) is assignable: FAILURE$ ^\[baz.\d+\] line \d+ Check that \*a is assignable: SUCCESS$ -^\[foo.\d+\] line \d+ Check that a is assignable: SUCCESS$ ^\[foo.\d+\] line \d+ Check that yp is assignable: SUCCESS$ ^\[foo.\d+\] line \d+ Check that z is assignable: SUCCESS$ ^\[foo.\d+\] line \d+ Check that \*xp is assignable: SUCCESS$ diff --git a/regression/contracts/assigns_enforce_21/test.desc b/regression/contracts/assigns_enforce_21/test.desc index 7b629e00d6f..7e2b828b342 100644 --- a/regression/contracts/assigns_enforce_21/test.desc +++ b/regression/contracts/assigns_enforce_21/test.desc @@ -6,9 +6,6 @@ main.c main.c function bar ^\[bar.\d+\] line \d+ Check that \*y is assignable: SUCCESS$ ^\[bar.\d+\] line \d+ Check that x is assignable: FAILURE$ -^\[baz.\d+\] line \d+ Check that w is assignable: SUCCESS$ -^\[foo.\d+\] line \d+ Check that w is assignable: SUCCESS$ -^\[foo.\d+\] line \d+ Check that z is assignable: SUCCESS$ ^VERIFICATION FAILED$ -- -- diff --git a/regression/contracts/assigns_enforce_free_dead/test.desc b/regression/contracts/assigns_enforce_free_dead/test.desc index 616e2b670ab..612466d051d 100644 --- a/regression/contracts/assigns_enforce_free_dead/test.desc +++ b/regression/contracts/assigns_enforce_free_dead/test.desc @@ -10,7 +10,6 @@ main.c ^\[foo.\d+\] line \d+ Check that a is assignable: SUCCESS$ ^\[foo.\d+\] line \d+ Check that q is assignable: SUCCESS$ ^\[foo.\d+\] line \d+ Check that w is assignable: SUCCESS$ -^\[foo.\d+\] line \d+ Check that x is assignable: SUCCESS$ ^\[foo.\d+\] line \d+ Check that y is assignable: SUCCESS$ ^\[foo.\d+\] line \d+ Check that z is assignable: SUCCESS$ ^\[foo.\d+\] line \d+ Check that POINTER_OBJECT\(\(void \*\)z\) is assignable: SUCCESS$ @@ -25,7 +24,6 @@ main.c ^\[foo.\d+\] line \d+ Check that a is assignable: FAILURE$ ^\[foo.\d+\] line \d+ Check that q is assignable: FAILURE$ ^\[foo.\d+\] line \d+ Check that w is assignable: FAILURE$ -^\[foo.\d+\] line \d+ Check that x is assignable: FAILURE$ ^\[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$ diff --git a/regression/contracts/assigns_enforce_structs_04/test.desc b/regression/contracts/assigns_enforce_structs_04/test.desc index 24300267705..3de0bffb9ca 100644 --- a/regression/contracts/assigns_enforce_structs_04/test.desc +++ b/regression/contracts/assigns_enforce_structs_04/test.desc @@ -6,7 +6,6 @@ main.c ^\[f1.\d+\] line \d+ Check that p->y is assignable: FAILURE$ ^\[f2.\d+\] line \d+ Check that p->x is assignable: FAILURE$ ^\[f3.\d+\] line \d+ Check that p->y is assignable: SUCCESS$ -^\[f4.\d+\] line \d+ Check that p is assignable: SUCCESS$ ^VERIFICATION FAILED$ -- -- diff --git a/regression/contracts/assigns_enforce_subfunction_calls/test.desc b/regression/contracts/assigns_enforce_subfunction_calls/test.desc index c4ffcabe76d..9411d1e4536 100644 --- a/regression/contracts/assigns_enforce_subfunction_calls/test.desc +++ b/regression/contracts/assigns_enforce_subfunction_calls/test.desc @@ -3,28 +3,15 @@ main.c --enforce-contract foo ^EXIT=10$ ^SIGNAL=0$ -^main.c function bar$ -^\[bar.1\] line \d+ Check that x is assignable: SUCCESS$ -^\[bar.2\] line \d+ Check that y is assignable: SUCCESS$ -^\[bar.3\] line \d+ Check that x is assignable: SUCCESS$ -^\[bar.4\] line \d+ Check that y is assignable: SUCCESS$ ^main.c function baz$ ^\[baz.1\] line \d+ Check that \*x is assignable: SUCCESS$ ^\[baz.2\] line \d+ Check that \*x is assignable: SUCCESS$ ^\[baz.3\] line \d+ Check that \*x is assignable: FAILURE$ ^\[baz.4\] line \d+ Check that \*x is assignable: FAILURE$ ^main.c function foo$ -^\[foo.1\] line \d+ Check that x is assignable: SUCCESS$ -^\[foo.2\] line \d+ Check that y is assignable: SUCCESS$ ^\[foo.assertion.1\] line \d+ foo.x.set: SUCCESS$ -^\[foo.3\] line \d+ Check that x is assignable: SUCCESS$ -^\[foo.4\] line \d+ Check that y is assignable: SUCCESS$ ^\[foo.assertion.2\] line \d+ foo.local.set: SUCCESS$ -^\[foo.5\] line \d+ Check that x is assignable: SUCCESS$ -^\[foo.6\] line \d+ Check that y is assignable: SUCCESS$ ^\[foo.assertion.3\] line \d+ foo.y.set: SUCCESS$ -^\[foo.7\] line \d+ Check that x is assignable: SUCCESS$ -^\[foo.8\] line \d+ Check that y is assignable: SUCCESS$ ^\[foo.assertion.4\] line \d+ foo.z.set: SUCCESS$ ^VERIFICATION FAILED$ -- diff --git a/regression/contracts/assigns_function_pointer/test.desc b/regression/contracts/assigns_function_pointer/test.desc index 4795e9d620b..0dcf7242f4a 100644 --- a/regression/contracts/assigns_function_pointer/test.desc +++ b/regression/contracts/assigns_function_pointer/test.desc @@ -3,7 +3,6 @@ main.c --enforce-contract bar ^EXIT=0$ ^SIGNAL=0$ -^\[bar.1\] line \d+ Check that fun\_ptr is assignable: SUCCESS$ ^\[main.assertion.\d+\] line \d+ assertion x \=\= 0: SUCCESS$ ^\[main.assertion.\d+\] line \d+ assertion x \=\= 1: SUCCESS$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/contracts/assigns_type_checking_valid_cases/test.desc b/regression/contracts/assigns_type_checking_valid_cases/test.desc index e7c22c65b59..1592a4973c2 100644 --- a/regression/contracts/assigns_type_checking_valid_cases/test.desc +++ b/regression/contracts/assigns_type_checking_valid_cases/test.desc @@ -3,13 +3,9 @@ main.c --enforce-contract foo1 --enforce-contract foo2 --enforce-contract foo3 --enforce-contract foo4 --enforce-contract foo5 --enforce-contract foo6 --enforce-contract foo7 --enforce-contract foo8 --enforce-contract foo9 --enforce-contract foo10 _ --pointer-primitive-check ^EXIT=0$ ^SIGNAL=0$ -^\[foo1.\d+\] line \d+ Check that a is assignable: SUCCESS$ ^\[foo10.\d+\] line \d+ Check that buffer->len is assignable: SUCCESS$ ^\[foo10.\d+\] line \d+ Check that buffer->aux\.allocated is assignable: SUCCESS$ -^\[foo2.\d+\] line \d+ Check that b is assignable: SUCCESS$ -^\[foo3.\d+\] line \d+ Check that b is assignable: SUCCESS$ ^\[foo3.\d+\] line \d+ Check that y is assignable: SUCCESS$ -^\[foo4.\d+\] line \d+ Check that b is assignable: SUCCESS$ ^\[foo4.\d+\] line \d+ Check that \*c is assignable: SUCCESS$ ^\[foo4.\d+\] line \d+ Check that \*x is assignable: SUCCESS$ ^\[foo5.\d+\] line \d+ Check that buffer.data is assignable: SUCCESS$ @@ -28,7 +24,6 @@ main.c ^\[foo8.\d+\] line \d+ Check that array\[\(.* int\)7\] is assignable: SUCCESS$ ^\[foo8.\d+\] line \d+ Check that array\[\(.* int\)8\] is assignable: SUCCESS$ ^\[foo8.\d+\] line \d+ Check that array\[\(.* int\)9\] is assignable: SUCCESS$ -^\[foo9.\d+\] line \d+ Check that array is assignable: SUCCESS$ ^VERIFICATION SUCCESSFUL$ -- Checks whether CBMC parses correctly all standard cases for assigns clauses. diff --git a/regression/contracts/assigns_validity_pointer_01/test.desc b/regression/contracts/assigns_validity_pointer_01/test.desc index 149013fd7a7..905c8e2e27a 100644 --- a/regression/contracts/assigns_validity_pointer_01/test.desc +++ b/regression/contracts/assigns_validity_pointer_01/test.desc @@ -8,7 +8,6 @@ SUCCESS // bar ASSERT \*foo::x > 0 IF ¬\(\*foo::x = 3\) THEN GOTO \d -IF ¬\(.*0.* = NULL\) THEN GOTO \d ASSIGN .*::tmp_if_expr := \(\*\(.*0.*\) = 5 \? true : false\) ASSIGN .*::tmp_if_expr\$\d := .*::tmp_if_expr \? true : false ASSUME .*::tmp_if_expr\$\d diff --git a/regression/contracts/assigns_validity_pointer_02/test.desc b/regression/contracts/assigns_validity_pointer_02/test.desc index c8730036836..4035fc12118 100644 --- a/regression/contracts/assigns_validity_pointer_02/test.desc +++ b/regression/contracts/assigns_validity_pointer_02/test.desc @@ -7,8 +7,6 @@ main.c ^\[bar.\d+\] line \d+ Check that \*x is assignable: SUCCESS$ ^\[bar.\d+\] line \d+ Check that \*y is assignable: SUCCESS$ ^\[baz.\d+\] line \d+ Check that \*z is assignable: SUCCESS$ -^\[foo.\d+\] line \d+ Check that x is assignable: SUCCESS$ -^\[foo.\d+\] line \d+ Check that y is assignable: SUCCESS$ ^\[foo.\d+\] line \d+ Check that \*x is assignable: SUCCESS$ ^VERIFICATION SUCCESSFUL$ -- diff --git a/regression/contracts/function_check_02/main.c b/regression/contracts/function_check_02/main.c index 7960696b6d1..18be2525d8e 100644 --- a/regression/contracts/function_check_02/main.c +++ b/regression/contracts/function_check_02/main.c @@ -15,10 +15,16 @@ int initialize(int *arr) ) // clang-format on { - for(int i = 0; i < 10; i++) - { - arr[i] = i; - } + arr[0] = 0; + arr[1] = 1; + arr[2] = 2; + arr[3] = 3; + arr[4] = 4; + arr[5] = 5; + arr[6] = 6; + arr[7] = 7; + arr[8] = 8; + arr[9] = 9; return 0; } diff --git a/regression/contracts/history-pointer-enforce-10/main.c b/regression/contracts/history-pointer-enforce-10/main.c index 5421773d9bb..475bc47b411 100644 --- a/regression/contracts/history-pointer-enforce-10/main.c +++ b/regression/contracts/history-pointer-enforce-10/main.c @@ -23,7 +23,7 @@ void bar(struct pair *p) __CPROVER_assigns(p->y) p->y = (p->y + 5); } -void baz(struct pair p) __CPROVER_assigns(p) +void baz(struct pair p) __CPROVER_assigns() __CPROVER_ensures(p == __CPROVER_old(p)) { struct pair pp = p; diff --git a/regression/contracts/history-pointer-enforce-10/test.desc b/regression/contracts/history-pointer-enforce-10/test.desc index a3ad4b4cb9c..e8359a34c9e 100644 --- a/regression/contracts/history-pointer-enforce-10/test.desc +++ b/regression/contracts/history-pointer-enforce-10/test.desc @@ -7,8 +7,6 @@ main.c ^\[postcondition.\d+\] file main.c line \d+ Check ensures clause: SUCCESS$ ^\[postcondition.\d+\] file main.c line \d+ Check ensures clause: SUCCESS$ ^\[bar.\d+\] line \d+ Check that p->y is assignable: SUCCESS$ -^\[baz.\d+\] line \d+ Check that p is assignable: SUCCESS$ -^\[baz.\d+\] line \d+ Check that p is assignable: SUCCESS$ ^\[foo.\d+\] line \d+ Check that \*p->y is assignable: SUCCESS$ ^\[foo.\d+\] line \d+ Check that z is assignable: SUCCESS$ ^\[main.assertion.\d+\] line \d+ assertion \*\(p->y\) == 7: SUCCESS$ @@ -19,3 +17,5 @@ main.c This test checks that history variables are supported for structs, symbols, and struct members. By using the --enforce-contract flag, the postcondition (with history variable) is asserted. In this case, this assertion should pass. +Note: A function is always authorized to assign the variables that store +its arguments, there is no need to mention them in the assigns clause. diff --git a/regression/contracts/loop-freeness-check/main.c b/regression/contracts/loop-freeness-check/main.c new file mode 100644 index 00000000000..3840c6dcaec --- /dev/null +++ b/regression/contracts/loop-freeness-check/main.c @@ -0,0 +1,16 @@ +int foo(int *arr) + // clang-format off + __CPROVER_assigns(__CPROVER_POINTER_OBJECT(arr)) +// clang-format off +{ + for(int i = 0; i < 10; i++) + arr[i] = i; + + return 0; +} + +int main() +{ + int arr[10]; + foo(arr); +} diff --git a/regression/contracts/loop-freeness-check/test.desc b/regression/contracts/loop-freeness-check/test.desc new file mode 100644 index 00000000000..a1dc7477d0c --- /dev/null +++ b/regression/contracts/loop-freeness-check/test.desc @@ -0,0 +1,13 @@ +CORE +main.c +--enforce-contract foo +^--- begin invariant violation report ---$ +^Invariant check failed$ +^Condition: is_loop_free\(.*\) +^Reason: Loops remain in function 'foo', assigns clause checking instrumentation cannot be applied\.$ +^EXIT=(127|134)$ +^SIGNAL=0$ +-- +-- +This test checks that loops that remain in the program when attempting to +instrument assigns clauses are detected and trigger an INVARIANT. diff --git a/regression/contracts/quantifiers-exists-ensures-enforce/main.c b/regression/contracts/quantifiers-exists-ensures-enforce/main.c index 1194c2968de..bfdc2e43d77 100644 --- a/regression/contracts/quantifiers-exists-ensures-enforce/main.c +++ b/regression/contracts/quantifiers-exists-ensures-enforce/main.c @@ -7,10 +7,16 @@ int f1(int *arr) }) // clang-format on { - for(int i = 0; i < 10; i++) - { - arr[i] = i; - } + arr[0] = 0; + arr[1] = 1; + arr[2] = 2; + arr[3] = 3; + arr[4] = 4; + arr[5] = 5; + arr[6] = 6; + arr[7] = 7; + arr[8] = 8; + arr[9] = 9; return 0; } @@ -24,10 +30,16 @@ int f2(int *arr) }) // clang-format on { - for(int i = 0; i < 10; i++) - { - arr[i] = 0; - } + arr[0] = 0; + arr[1] = 1; + arr[2] = 2; + arr[3] = 3; + arr[4] = 4; + arr[5] = 5; + arr[6] = 6; + arr[7] = 7; + arr[8] = 8; + arr[9] = 9; return 0; } diff --git a/regression/contracts/quantifiers-exists-requires-enforce/main.c b/regression/contracts/quantifiers-exists-requires-enforce/main.c index 7985f57de3b..c74bbfbb009 100644 --- a/regression/contracts/quantifiers-exists-requires-enforce/main.c +++ b/regression/contracts/quantifiers-exists-requires-enforce/main.c @@ -1,7 +1,7 @@ #include #include -#define MAX_LEN 64 +#define MAX_LEN 10 // clang-format off bool f1(int *arr, int len) @@ -18,11 +18,27 @@ bool f1(int *arr, int len) // clang-format on { bool found_four = false; - for(int i = 0; i <= MAX_LEN; i++) - { - if(i < len) - found_four |= (arr[i] == 4); - } + if(0 < len) + found_four |= (arr[0] == 4); + if(1 < len) + found_four |= (arr[1] == 4); + if(2 < len) + found_four |= (arr[2] == 4); + if(3 < len) + found_four |= (arr[3] == 4); + if(4 < len) + found_four |= (arr[4] == 4); + if(5 < len) + found_four |= (arr[5] == 4); + if(6 < len) + found_four |= (arr[6] == 4); + if(7 < len) + found_four |= (arr[7] == 4); + if(8 < len) + found_four |= (arr[8] == 4); + + if(9 < len) + found_four |= (arr[9] == 4); // clang-format off return (len > 0 ==> found_four); diff --git a/regression/contracts/quantifiers-forall-ensures-enforce/main.c b/regression/contracts/quantifiers-forall-ensures-enforce/main.c index cceba46be58..3e6335ab1f3 100644 --- a/regression/contracts/quantifiers-forall-ensures-enforce/main.c +++ b/regression/contracts/quantifiers-forall-ensures-enforce/main.c @@ -1,6 +1,6 @@ #include -#define MAX_LEN 16 +#define MAX_LEN 10 // clang-format off int f1(int *arr, int len) @@ -12,11 +12,27 @@ int f1(int *arr, int len) }) // clang-format on { - for(int i = 0; i < MAX_LEN; i++) - { - if(i < len) - arr[i] = 0; - } + if(0 < len) + arr[0] = 0; + if(1 < len) + arr[1] = 0; + if(2 < len) + arr[2] = 0; + if(3 < len) + arr[3] = 0; + if(4 < len) + arr[4] = 0; + if(5 < len) + arr[5] = 0; + if(6 < len) + arr[6] = 0; + if(7 < len) + arr[7] = 0; + if(8 < len) + arr[8] = 0; + if(9 < len) + arr[9] = 0; + return 0; } diff --git a/regression/contracts/quantifiers-forall-ensures-enforce/test.desc b/regression/contracts/quantifiers-forall-ensures-enforce/test.desc index 87a1b4d333e..b5a17935c58 100644 --- a/regression/contracts/quantifiers-forall-ensures-enforce/test.desc +++ b/regression/contracts/quantifiers-forall-ensures-enforce/test.desc @@ -4,10 +4,11 @@ main.c ^EXIT=0$ ^SIGNAL=0$ ^\[postcondition.\d+\] file main.c line \d+ Check ensures clause: SUCCESS$ -^\[f1.\d+\] line \d+ Check that arr\[\(.*\)i\] is assignable: SUCCESS$ +^\[f1.\d+\] line \d+ Check that arr\[\(.*\)\d\] is assignable: SUCCESS$ ^VERIFICATION SUCCESSFUL$ -- ^warning: ignoring +^\[f1.\d+\] line \d+ Check that arr\[\(.*\)\d\] is assignable: FAILURE$ -- The purpose of this test is to ensure that we can safely use __CPROVER_forall within positive contexts (enforced ENSURES clauses). diff --git a/regression/contracts/quantifiers-forall-requires-enforce/main.c b/regression/contracts/quantifiers-forall-requires-enforce/main.c index fe0da19e0ca..2040549f0f4 100644 --- a/regression/contracts/quantifiers-forall-requires-enforce/main.c +++ b/regression/contracts/quantifiers-forall-requires-enforce/main.c @@ -12,8 +12,16 @@ bool f1(int *arr) // clang-format on { bool is_identity = true; - for(int i = 0; i < 10; ++i) - is_identity &= (arr[i] == i); + is_identity &= (arr[0] == 0); + is_identity &= (arr[1] == 1); + is_identity &= (arr[2] == 2); + is_identity &= (arr[3] == 3); + is_identity &= (arr[4] == 4); + is_identity &= (arr[5] == 5); + is_identity &= (arr[6] == 6); + is_identity &= (arr[7] == 7); + is_identity &= (arr[8] == 8); + is_identity &= (arr[9] == 9); return is_identity; } diff --git a/regression/contracts/quantifiers-nested-01/main.c b/regression/contracts/quantifiers-nested-01/main.c index 2e1d0667115..f44da69dd13 100644 --- a/regression/contracts/quantifiers-nested-01/main.c +++ b/regression/contracts/quantifiers-nested-01/main.c @@ -11,10 +11,16 @@ int f1(int *arr) }) // clang-format on { - for(int i = 0; i < 10; i++) - { - arr[i] = i; - } + arr[0] = 0; + arr[1] = 1; + arr[2] = 2; + arr[3] = 3; + arr[4] = 4; + arr[5] = 5; + arr[6] = 6; + arr[7] = 7; + arr[8] = 8; + arr[9] = 9; return 0; } diff --git a/regression/contracts/quantifiers-nested-03/main.c b/regression/contracts/quantifiers-nested-03/main.c index e7bf048ddcf..ca586ae9f3e 100644 --- a/regression/contracts/quantifiers-nested-03/main.c +++ b/regression/contracts/quantifiers-nested-03/main.c @@ -10,10 +10,16 @@ __CPROVER_assigns(__CPROVER_POINTER_OBJECT(arr)) ) // clang-format on { - for(int i = 0; i < 10; i++) - { - arr[i] = i; - } + arr[0] = 0; + arr[1] = 1; + arr[2] = 2; + arr[3] = 3; + arr[4] = 4; + arr[5] = 5; + arr[6] = 6; + arr[7] = 7; + arr[8] = 8; + arr[9] = 9; return 0; } diff --git a/regression/contracts/test_aliasing_ensure_indirect/main.c b/regression/contracts/test_aliasing_ensure_indirect/main.c index bac705ee9e3..48980440764 100644 --- a/regression/contracts/test_aliasing_ensure_indirect/main.c +++ b/regression/contracts/test_aliasing_ensure_indirect/main.c @@ -2,7 +2,7 @@ #include #include -void bar(int *z) __CPROVER_assigns(z) +void bar(int *z) __CPROVER_assigns() __CPROVER_ensures(__CPROVER_is_fresh(z, sizeof(int))) { z = malloc(sizeof(*z)); diff --git a/regression/contracts/test_aliasing_ensure_indirect/test.desc b/regression/contracts/test_aliasing_ensure_indirect/test.desc index 69df6b6065c..4c9575dddb9 100644 --- a/regression/contracts/test_aliasing_ensure_indirect/test.desc +++ b/regression/contracts/test_aliasing_ensure_indirect/test.desc @@ -4,7 +4,6 @@ main.c ^EXIT=0$ ^SIGNAL=0$ \[postcondition.\d+\] file main.c line \d+ Check ensures clause: SUCCESS -\[bar.\d+\] line \d+ Check that z is assignable: SUCCESS \[foo.\d+\] line \d+ Check that \*x is assignable: SUCCESS \[main.assertion.\d+\] line \d+ assertion \!\(n \< 4\): SUCCESS ^VERIFICATION SUCCESSFUL$ diff --git a/src/goto-instrument/contracts/contracts.cpp b/src/goto-instrument/contracts/contracts.cpp index 325ed89226a..d0df3a38cb8 100644 --- a/src/goto-instrument/contracts/contracts.cpp +++ b/src/goto-instrument/contracts/contracts.cpp @@ -309,7 +309,13 @@ void code_contractst::check_apply_loop_contracts( // Perform write set instrumentation on the entire loop. check_frame_conditions( - function_name, goto_function.body, loop_head, loop_end, loop_assigns); + function_name, + goto_function.body, + loop_head, + loop_end, + loop_assigns, + // do not skip checks on function parameter assignments + false); havoc_assigns_targetst havoc_gen(to_havoc, ns); havoc_gen.append_full_havoc_code( @@ -1122,7 +1128,9 @@ bool code_contractst::check_frame_conditions_function(const irep_idt &function) return true; } - if(check_for_looped_mallocs(function_obj->second.body)) + auto &function_body = function_obj->second.body; + + if(check_for_looped_mallocs(function_body)) { return true; } @@ -1136,21 +1144,24 @@ bool code_contractst::check_frame_conditions_function(const irep_idt &function) function, symbol_table); - // detect and add static local variables + // Detect and add static local variables assigns.add_static_locals_to_write_set(goto_functions, function); // 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()); - auto instruction_it = function_obj->second.body.instructions.begin(); + auto instruction_it = function_body.instructions.begin(); for(const auto &car : assigns.get_write_set()) { auto snapshot_instructions = car.generate_snapshot_instructions(); insert_before_swap_and_advance( - function_obj->second.body, instruction_it, snapshot_instructions); + function_body, instruction_it, snapshot_instructions); }; + // Restore internal coherence in the programs + goto_functions.update(); + // Full inlining of the function body // Inlining is performed so that function calls to a same function // occurring under different write sets get instrumented specifically @@ -1162,16 +1173,26 @@ bool code_contractst::check_frame_conditions_function(const irep_idt &function) decorated.get_recursive_function_warnings_count() == 0, "Recursive functions found during inlining"); - // restore internal invariants + // Clean up possible fake loops that are due to `IF 0!=0 GOTO i` instructions + simplify_gotos(function_body, ns); + + // Restore internal coherence in the programs goto_functions.update(); + INVARIANT( + is_loop_free(function_body, ns, log), + "Loops remain in function '" + id2string(function) + + "', assigns clause checking instrumentation cannot be applied."); + // Insert write set inclusion checks. check_frame_conditions( - function_obj->first, - function_obj->second.body, + function, + function_body, instruction_it, - function_obj->second.body.instructions.end(), - assigns); + function_body.instructions.end(), + assigns, + // skip checks on function parameter assignments + true); return false; } @@ -1181,7 +1202,8 @@ void code_contractst::check_frame_conditions( goto_programt &body, goto_programt::targett instruction_it, const goto_programt::targett &instruction_end, - assigns_clauset &assigns) + assigns_clauset &assigns, + bool skip_parameter_assigns) { for(; instruction_it != instruction_end; ++instruction_it) { @@ -1189,6 +1211,12 @@ void code_contractst::check_frame_conditions( if(pragmas.find(CONTRACT_PRAGMA_DISABLE_ASSIGNS_CHECK) != pragmas.end()) continue; + if(skip_parameter_assigns && is_parameter_assign(instruction_it, ns)) + continue; + + if(is_auxiliary_decl_dead_or_assign(instruction_it, ns)) + continue; + // Do not instrument this instruction again in the future, // since we are going to instrument it now below. add_pragma_disable_assigns_check(*instruction_it); diff --git a/src/goto-instrument/contracts/contracts.h b/src/goto-instrument/contracts/contracts.h index 6514aada79e..957b4a19d9a 100644 --- a/src/goto-instrument/contracts/contracts.h +++ b/src/goto-instrument/contracts/contracts.h @@ -132,7 +132,8 @@ class code_contractst goto_programt &, goto_programt::targett, const goto_programt::targett &, - assigns_clauset &); + assigns_clauset &, + bool skip_parameter_assigns); /// Inserts an assertion into the goto program to ensure that /// an expression is within the assignable memory frame. diff --git a/src/goto-instrument/contracts/utils.cpp b/src/goto-instrument/contracts/utils.cpp index 95185dd4dd1..d616619e357 100644 --- a/src/goto-instrument/contracts/utils.cpp +++ b/src/goto-instrument/contracts/utils.cpp @@ -10,9 +10,13 @@ Date: September 2021 #include "utils.h" +#include #include +#include +#include #include #include +#include goto_programt::instructiont & add_pragma_disable_assigns_check(goto_programt::instructiont &instr) @@ -163,3 +167,118 @@ void disable_pointer_checks(source_locationt &source_location) source_location.add_pragma("disable:pointer-primitive-check"); source_location.add_pragma("disable:pointer-overflow-check"); } + +bool is_parameter_assign( + const goto_programt::targett &instruction_it, + namespacet &ns) +{ + optionalt sym = {}; + + // extract symbol + if(instruction_it->is_assign()) + { + const auto &lhs = instruction_it->assign_lhs(); + if(can_cast_expr(lhs)) + sym = to_symbol_expr(lhs); + } + + // check condition + if(sym.has_value()) + return ns.lookup(sym.value().get_identifier()).is_parameter; + + return false; +} + +bool is_auxiliary_decl_dead_or_assign( + const goto_programt::targett &instruction_it, + namespacet &ns) +{ + optionalt sym = {}; + + // extract symbol + if(instruction_it->is_decl()) + sym = instruction_it->decl_symbol(); + else if(instruction_it->is_dead()) + sym = instruction_it->dead_symbol(); + else if(instruction_it->is_assign()) + { + const auto &lhs = instruction_it->assign_lhs(); + if(can_cast_expr(lhs)) + sym = to_symbol_expr(lhs); + } + + // check condition + if(sym.has_value()) + return ns.lookup(sym.value().get_identifier()).is_auxiliary; + + return false; +} + +void simplify_gotos(goto_programt &goto_program, namespacet &ns) +{ + for(auto &instruction : goto_program.instructions) + { + if(instruction.is_goto()) + { + const auto &condition = instruction.get_condition(); + const auto &simplified = simplify_expr(condition, ns); + if(simplified.is_false()) + instruction.turn_into_skip(); + } + } +} + +bool is_loop_free( + const goto_programt &goto_program, + namespacet &ns, + messaget &log) +{ + // create cfg from instruction list + cfg_baset cfg; + cfg(goto_program); + + // check that all nodes are there + INVARIANT( + goto_program.instructions.size() == cfg.size(), + "Instruction list vs CFG size mismatch."); + + // compute SCCs + using idxt = graph_nodet::node_indext; + std::vector node_to_scc(cfg.size(), -1); + auto nof_sccs = cfg.SCCs(node_to_scc); + + // compute size of each SCC + std::vector scc_size(nof_sccs, 0); + for(auto scc : node_to_scc) + { + INVARIANT( + 0 <= scc && scc < nof_sccs, "Could not determine SCC for instruction"); + scc_size[scc]++; + } + + // Check they are all of size 1 + bool all_size_one = true; + + for(size_t scc_id = 0; scc_id < nof_sccs; scc_id++) + { + auto size = scc_size[scc_id]; + if(size > 1) + { + all_size_one = false; + + // print offending loops + log.error() << "--- Found loop of size " << size << " ---" + << messaget::eom; + for(idxt node_id = 0; node_id < cfg.size(); node_id++) + { + if(node_to_scc[node_id] == scc_id) + { + const auto &pc = cfg[node_id].PC; + goto_program.output_instruction(ns, "", log.error(), *pc); + log.error() << messaget::eom; + } + } + } + } + return all_size_one; +} diff --git a/src/goto-instrument/contracts/utils.h b/src/goto-instrument/contracts/utils.h index 1614ce023a3..cf90b00db0a 100644 --- a/src/goto-instrument/contracts/utils.h +++ b/src/goto-instrument/contracts/utils.h @@ -17,6 +17,8 @@ Date: September 2021 #include +#include + #define CONTRACT_PRAGMA_DISABLE_ASSIGNS_CHECK "contracts:disable:assigns-check" /// \brief A class that overrides the low-level havocing functions in the base @@ -112,7 +114,7 @@ void insert_before_swap_and_advance( /// \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: Suffix to use to generate the unique name -/// \param is_auxiliary: Do not print symbol in traces if true (default = false) +/// \param is_auxiliary: Do not print symbol in traces if true (default = true) /// \return The new symbolt object. const symbolt &new_tmp_symbol( const typet &type, @@ -120,9 +122,32 @@ const symbolt &new_tmp_symbol( const irep_idt &mode, symbol_table_baset &symtab, std::string suffix = "tmp_cc", - bool is_auxiliary = false); + bool is_auxiliary = true); /// Add disable pragmas for all pointer checks on the given location void disable_pointer_checks(source_locationt &source_location); +/// Returns true iff the instruction is a `DECL x`, `DEAD x`, +/// or `ASSIGN x := expr` where `x` has the `is_parameter` flag set. +bool is_parameter_assign( + const goto_programt::targett &instruction_it, + namespacet &ns); + +/// Returns true iff the instruction is a `DECL x`, `DEAD x`, +/// or `ASSIGN x := expr` where `x` has the `is_auxiliary` flag set. +bool is_auxiliary_decl_dead_or_assign( + const goto_programt::targett &instruction_it, + namespacet &ns); + +/// Turns goto instructions `IF cond GOTO label` where the condition +/// statically simplifies to `false` into SKIP instructions. +void simplify_gotos(goto_programt &goto_program, namespacet &ns); + +/// Returns true iff the given program is loop-free, +/// i.e. if each SCC of its CFG contains a single element. +bool is_loop_free( + const goto_programt &goto_program, + namespacet &ns, + messaget &log); + #endif // CPROVER_GOTO_INSTRUMENT_CONTRACTS_UTILS_H