Skip to content

Commit 4e38322

Browse files
feliperodrifeliperodri
authored
Merge pull request #6345 from feliperodri/fix-contract-replacement
Check subset relationship of assigns clause during replacement
2 parents 4fd1a8d + bb4c90b commit 4e38322

File tree

10 files changed

+133
-56
lines changed

10 files changed

+133
-56
lines changed

‎regression/contracts/assigns_enforce_structs_07/test.desc

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE
1+
KNOWNBUG
22
main.c
33
--enforce-all-contracts _ --pointer-check
44
^EXIT=10$
@@ -12,3 +12,6 @@ main.c
1212
--
1313
Checks whether CBMC properly evaluates write set of members
1414
from invalid objects. In this case, they are not writable.
15+
16+
Bug: We need to check the validity of each dereference
17+
when accessing struct members.

‎regression/contracts/assigns_replace_08/main.c

Lines changed: 19 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,19 @@
1+
#include <stdlib.h>
2+
3+
int x;
4+
int *z = &x;
5+
6+
void bar() __CPROVER_assigns(*z)
7+
{
8+
}
9+
10+
void foo() __CPROVER_assigns()
11+
{
12+
bar();
13+
}
14+
15+
int main()
16+
{
17+
foo();
18+
return 0;
19+
}

‎regression/contracts/assigns_replace_08/test.desc

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,16 @@
1+
CORE
2+
main.c
3+
--enforce-contract foo --replace-call-with-contract bar _ --pointer-primitive-check
4+
^EXIT=10$
5+
^SIGNAL=0$
6+
\[\d+\] file main.c line \d+ Check that bar\'s assigns clause is a subset of foo\'s assigns clause: FAILURE$
7+
\[\d+\] file main.c line \d+ Check that \*z is assignable: FAILURE$
8+
^.* 2 of \d+ failed \(\d+ iteration.*\)$
9+
^VERIFICATION FAILED$
10+
--
11+
\[\d+\] file main.c line \d+ Check that bar\'s assigns clause is a subset of foo\'s assigns clause: SUCCESS$
12+
\[\d+\] file main.c line \d+ Check that \*z is assignable: SUCCESS$
13+
^VERIFICATION SUCCESSFUL$
14+
--
15+
Checks whether CBMC properly evaluates subset relationship on assigns
16+
during replacement.

‎regression/contracts/assigns_validity_pointer_01/main.c

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -17,17 +17,17 @@ void baz() __CPROVER_assigns(*z) __CPROVER_ensures(z == NULL || *z == 7)
1717
*z = 7;
1818
}
1919

20-
void foo(int *x) __CPROVER_assigns(*x) __CPROVER_requires(*x > 0)
20+
void foo(int *x) __CPROVER_assigns(*x, *z) __CPROVER_requires(*x > 0)
2121
__CPROVER_ensures(*x == 3)
2222
{
2323
bar(x, NULL);
24-
z == NULL;
2524
baz();
2625
}
2726

2827
int main()
2928
{
3029
int n;
30+
z = malloc(sizeof(*z));
3131
foo(&n);
3232

3333
assert(n == 3);

‎regression/contracts/assigns_validity_pointer_02/test.desc

Lines changed: 8 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -3,11 +3,16 @@ main.c
33
--enforce-contract foo
44
^EXIT=0$
55
^SIGNAL=0$
6+
^\[postcondition.\d+\] file main.c line \d+ Check ensures clause: SUCCESS$
7+
^\[foo.\d+\] line \d+ Check that bar\'s assigns clause is a subset of foo\'s assigns clause: SUCCESS$
8+
^\[foo.\d+\] line \d+ Check that \*x is assignable: SUCCESS$
9+
^\[foo.\d+\] line \d+ Check that baz\'s assigns clause is a subset of foo\'s assigns clause: SUCCESS$
610
^VERIFICATION SUCCESSFUL$
7-
//^([foo\.1] line 15 assertion: FAILURE)
811
--
9-
\[foo\.1\] line 24 assertion: FAILURE
10-
\[foo\.3\] line 27 assertion: FAILURE
12+
^\[postcondition.\d+\] file main.c line \d+ Check ensures clause: FAILURE$
13+
^\[foo.\d+\] line \d+ Check that bar\'s assigns clause is a subset of foo\'s assigns clause: FAILURE$
14+
^\[foo.\d+\] line \d+ Check that \*x is assignable: FAILURE$
15+
^\[foo.\d+\] line \d+ Check that baz\'s assigns clause is a subset of foo\'s assigns clause: FAILURE$
1116
--
1217
Verification:
1318
This test checks support for a NULL pointer that is assigned to by

‎regression/contracts/assigns_validity_pointer_04/test.desc

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,8 +3,10 @@ main.c
33
--enforce-contract foo --replace-call-with-contract bar --replace-call-with-contract baz _ --pointer-primitive-check
44
^EXIT=10$
55
^SIGNAL=0$
6+
^\[\d+\] file main.c line \d+ Check that bar\'s assigns clause is a subset of foo\'s assigns clause: FAILURE$
7+
^\[\d+\] file main.c line \d+ Check that baz\'s assigns clause is a subset of foo\'s assigns clause: FAILURE$
68
^\[foo.\d+\] line \d+ Check that z is assignable: FAILURE$
7-
^.* 1 of \d+ failed \(\d+ iteration.*\)$
9+
^.* 3 of \d+ failed \(\d+ iteration.*\)$
810
^VERIFICATION FAILED$
911
// bar
1012
ASSERT \*foo::x > 0

‎regression/contracts/test_aliasing_ensure_indirect/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -7,7 +7,7 @@ main.c
77
\[postcondition.\d+\] file main.c line \d+ Check ensures clause: SUCCESS
88
\[bar.\d+\] line \d+ Check that z is assignable: SUCCESS
99
\[foo.\d+\] line \d+ Check that \*x is assignable: SUCCESS
10-
\[foo.\d+\] line \d+ Check that callee's assigns clause is a subset of caller's: SUCCESS
10+
\[foo.\d+\] line \d+ Check that bar\'s assigns clause is a subset of foo\'s assigns clause: SUCCESS
1111
\[main.assertion.\d+\] line \d+ assertion \!\(n \< 4\): SUCCESS
1212
^VERIFICATION SUCCESSFUL$
1313
--

‎src/ansi-c/ansi_c_convert_type.cpp

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -272,6 +272,7 @@ void ansi_c_convert_typet::read_rec(const typet &type)
272272
for(auto &assignment : to_unary_expr(as_expr).op().operands())
273273
assigns.add_to_operands(std::move(assignment));
274274
}
275+
assigns.add_source_location() = as_expr.source_location();
275276
}
276277
else if(type.id() == ID_C_spec_ensures)
277278
{

‎src/goto-instrument/contracts/assigns.cpp

Lines changed: 46 additions & 41 deletions
Original file line numberDiff line numberDiff line change
@@ -43,45 +43,62 @@ exprt assigns_clauset::targett::normalize(const exprt &expr)
4343
exprt assigns_clauset::targett::generate_containment_check(
4444
const address_of_exprt &lhs_address) const
4545
{
46-
exprt::operandst condition;
46+
exprt::operandst address_validity;
47+
exprt::operandst containment_check;
4748

4849
// __CPROVER_w_ok(target, sizeof(target))
49-
condition.push_back(w_ok_exprt(
50+
address_validity.push_back(w_ok_exprt(
5051
address,
5152
size_of_expr(dereference_exprt(address).type(), parent.ns).value()));
5253

54+
// __CPROVER_w_ok(lhs, sizeof(lhs))
55+
address_validity.push_back(w_ok_exprt(
56+
lhs_address,
57+
size_of_expr(dereference_exprt(lhs_address).type(), parent.ns).value()));
58+
5359
// __CPROVER_same_object(lhs, target)
54-
condition.push_back(same_object(lhs_address, address));
60+
containment_check.push_back(same_object(lhs_address, address));
5561

5662
// If assigns target was a dereference, comparing objects is enough
57-
if(id == ID_dereference)
63+
// and the resulting condition will be
64+
// __CPROVER_w_ok(target, sizeof(target))
65+
// && __CPROVER_w_ok(lhs, sizeof(lhs))
66+
// ==> __CPROVER_same_object(lhs, target)
67+
if(id != ID_dereference)
5868
{
59-
return conjunction(condition);
69+
const auto lhs_offset = pointer_offset(lhs_address);
70+
const auto own_offset = pointer_offset(address);
71+
72+
// __CPROVER_offset(lhs) >= __CPROVER_offset(target)
73+
containment_check.push_back(
74+
binary_relation_exprt(lhs_offset, ID_ge, own_offset));
75+
76+
const auto lhs_region = plus_exprt(
77+
typecast_exprt::conditional_cast(
78+
size_of_expr(lhs_address.object().type(), parent.ns).value(),
79+
lhs_offset.type()),
80+
lhs_offset);
81+
82+
const exprt own_region = plus_exprt(
83+
typecast_exprt::conditional_cast(
84+
size_of_expr(address.object().type(), parent.ns).value(),
85+
own_offset.type()),
86+
own_offset);
87+
88+
// (sizeof(lhs) + __CPROVER_offset(lhs)) <=
89+
// (sizeof(target) + __CPROVER_offset(target))
90+
containment_check.push_back(
91+
binary_relation_exprt(lhs_region, ID_le, own_region));
6092
}
6193

62-
const auto lhs_offset = pointer_offset(lhs_address);
63-
const auto own_offset = pointer_offset(address);
64-
65-
// __CPROVER_offset(lhs) >= __CPROVER_offset(target)
66-
condition.push_back(binary_relation_exprt(lhs_offset, ID_ge, own_offset));
67-
68-
const auto lhs_region = plus_exprt(
69-
typecast_exprt::conditional_cast(
70-
size_of_expr(lhs_address.object().type(), parent.ns).value(),
71-
lhs_offset.type()),
72-
lhs_offset);
73-
74-
const exprt own_region = plus_exprt(
75-
typecast_exprt::conditional_cast(
76-
size_of_expr(address.object().type(), parent.ns).value(),
77-
own_offset.type()),
78-
own_offset);
79-
80-
// (sizeof(lhs) + __CPROVER_offset(lhs)) <=
81-
// (sizeof(target) + __CPROVER_offset(target))
82-
condition.push_back(binary_relation_exprt(lhs_region, ID_le, own_region));
83-
84-
return conjunction(condition);
94+
// __CPROVER_w_ok(target, sizeof(target))
95+
// && __CPROVER_w_ok(lhs, sizeof(lhs))
96+
// ==> __CPROVER_same_object(lhs, target)
97+
// && __CPROVER_offset(lhs) >= __CPROVER_offset(target)
98+
// && (sizeof(lhs) + __CPROVER_offset(lhs)) <=
99+
// (sizeof(target) + __CPROVER_offset(target))
100+
return binary_relation_exprt(
101+
conjunction(address_validity), ID_implies, conjunction(containment_check));
85102
}
86103

87104
assigns_clauset::assigns_clauset(
@@ -152,7 +169,6 @@ exprt assigns_clauset::generate_containment_check(const exprt &lhs) const
152169
{
153170
condition.push_back(target.generate_containment_check(lhs_address));
154171
}
155-
156172
for(const auto &target : global_write_set)
157173
{
158174
condition.push_back(target.generate_containment_check(lhs_address));
@@ -174,12 +190,6 @@ exprt assigns_clauset::generate_subset_check(
174190
exprt result = true_exprt();
175191
for(const auto &subtarget : subassigns.global_write_set)
176192
{
177-
// TODO: Optimize the implication generated due to the validity check.
178-
// In some cases, e.g. when `subtarget` is known to be `NULL`,
179-
// the implication can be skipped entirely. See #6105 for more details.
180-
auto validity_check =
181-
w_ok_exprt(subtarget.address, from_integer(0, unsigned_int_type()));
182-
183193
exprt::operandst current_subtarget_found_conditions;
184194
for(const auto &target : global_write_set)
185195
{
@@ -191,12 +201,7 @@ exprt assigns_clauset::generate_subset_check(
191201
current_subtarget_found_conditions.push_back(
192202
target.generate_containment_check(subtarget.address));
193203
}
194-
195-
auto current_subtarget_found = or_exprt(
196-
not_exprt(validity_check),
197-
disjunction(current_subtarget_found_conditions));
198-
199-
result = and_exprt(result, current_subtarget_found);
204+
result = and_exprt(result, disjunction(current_subtarget_found_conditions));
200205
}
201206

202207
return result;

‎src/goto-instrument/contracts/contracts.cpp

Lines changed: 33 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -601,8 +601,31 @@ bool code_contractst::apply_function_contract(
601601
// in the assigns clause.
602602
if(assigns.is_not_nil())
603603
{
604-
assigns_clauset assigns_cause(assigns, log, ns);
605-
auto assigns_havoc = assigns_cause.generate_havoc_code();
604+
assigns_clauset assigns_clause(assigns, log, ns);
605+
606+
// Retrieve assigns clause of the caller function if exists.
607+
const irep_idt &caller_function = target->source_location.get_function();
608+
auto caller_assigns =
609+
to_code_with_contract_type(ns.lookup(caller_function).type).assigns();
610+
611+
if(caller_assigns.is_not_nil())
612+
{
613+
// check subset relationship of assigns clause for called function
614+
assigns_clauset caller_assigns_clause(caller_assigns, log, ns);
615+
goto_programt subset_check_assertion;
616+
subset_check_assertion.add(goto_programt::make_assertion(
617+
caller_assigns_clause.generate_subset_check(assigns_clause),
618+
assigns_clause.location));
619+
subset_check_assertion.instructions.back().source_location.set_comment(
620+
"Check that " + id2string(function) +
621+
"'s assigns clause is a subset of " + id2string(caller_function) +
622+
"'s assigns clause");
623+
insert_before_swap_and_advance(
624+
goto_program, target, subset_check_assertion);
625+
}
626+
627+
// Havoc all targets in global write set
628+
auto assigns_havoc = assigns_clause.generate_havoc_code();
606629

607630
// Insert the non-deterministic assignment immediately before the call site.
608631
insert_before_swap_and_advance(goto_program, target, assigns_havoc);
@@ -772,8 +795,8 @@ void code_contractst::instrument_call_statement(
772795
alias_assertion.instructions.back().source_location.set_comment(
773796
"Check that " + from_expr(ns, alias_expr.id(), alias_expr) +
774797
" is assignable");
775-
program.insert_before_swap(instruction_iterator, alias_assertion);
776-
++instruction_iterator;
798+
insert_before_swap_and_advance(
799+
program, instruction_iterator, alias_assertion);
777800
}
778801

779802
const symbolt &called_symbol = ns.lookup(called_name);
@@ -810,9 +833,12 @@ void code_contractst::instrument_call_statement(
810833
alias_assertion.add(goto_programt::make_assertion(
811834
subset_check, instruction_iterator->source_location));
812835
alias_assertion.instructions.back().source_location.set_comment(
813-
"Check that callee's assigns clause is a subset of caller's");
814-
program.insert_before_swap(instruction_iterator, alias_assertion);
815-
++instruction_iterator;
836+
"Check that " + id2string(called_name) +
837+
"'s assigns clause is a subset of " +
838+
id2string(instruction_iterator->source_location.get_function()) +
839+
"'s assigns clause");
840+
insert_before_swap_and_advance(
841+
program, instruction_iterator, alias_assertion);
816842
}
817843
}
818844

0 commit comments

Comments
 (0)