Skip to content

Commit 407914b

Browse files
qinhepingqinheping
committed
CONTRACTS: dfcc_is_cprover_symbol now uses allow lists
The result of `dfcc_is_cprover_symbol` is used to skip frame conditon checks on symbols with special meaning. Before we were matching symbols based on their prefix, which would allow users to skip frame condition checks just by naming their symbols with these prefixes. We now use a closed allow list, and distinguish function symbolds form static var symbols. We add test that show that variables named with __CPROVER, __VERIFIER or nondet prefixes do not bypass frame condition checks.
1 parent fb42722 commit 407914b

File tree

8 files changed

+218
-8
lines changed

8 files changed

+218
-8
lines changed

‎regression/contracts-dfcc/dont_skip_cprover_prefixed_vars_fail/main.c‎

Lines changed: 23 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,23 @@
1+
void foo()
2+
{
3+
int nondet_var;
4+
int __VERIFIER_var;
5+
int __CPROVER_var;
6+
for(int i = 10; i > 0; i--)
7+
// clang-format off
8+
__CPROVER_assigns(i)
9+
__CPROVER_loop_invariant(0 <= i && i <= 10)
10+
__CPROVER_decreases(i)
11+
// clang-format on
12+
{
13+
nondet_var = 0;
14+
__VERIFIER_var = 0;
15+
__CPROVER_var = 0;
16+
}
17+
}
18+
19+
int main()
20+
{
21+
foo();
22+
return 0;
23+
}

‎regression/contracts-dfcc/dont_skip_cprover_prefixed_vars_fail/test.desc‎

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
CORE
2+
main.c
3+
--dfcc main --apply-loop-contracts
4+
^\[foo.assigns.\d+\] line \d+ Check that nondet_var is assignable: FAILURE$
5+
^\[foo.assigns.\d+\] line \d+ Check that __VERIFIER_var is assignable: FAILURE$
6+
^\[foo.assigns.\d+\] line \d+ Check that __CPROVER_var is assignable: FAILURE$
7+
^EXIT=10$
8+
^SIGNAL=0$
9+
^VERIFICATION FAILED$
10+
--
11+
--
12+
This test checks that program variables with special name prefixes
13+
__CPROVER_, __VERIFIER, or nondet do not escape assigns clause checking.

‎regression/contracts-dfcc/dont_skip_cprover_prefixed_vars_pass/main.c‎

Lines changed: 23 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,23 @@
1+
void foo()
2+
{
3+
int nondet_var;
4+
int __VERIFIER_var;
5+
int __CPROVER_var;
6+
for(int i = 10; i > 0; i--)
7+
// clang-format off
8+
__CPROVER_assigns(i,nondet_var, __VERIFIER_var, __CPROVER_var)
9+
__CPROVER_loop_invariant(0 <= i && i <= 10)
10+
__CPROVER_decreases(i)
11+
// clang-format on
12+
{
13+
nondet_var = 0;
14+
__VERIFIER_var = 0;
15+
__CPROVER_var = 0;
16+
}
17+
}
18+
19+
int main()
20+
{
21+
foo();
22+
return 0;
23+
}

‎regression/contracts-dfcc/dont_skip_cprover_prefixed_vars_pass/test.desc‎

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
CORE
2+
main.c
3+
--dfcc main --apply-loop-contracts
4+
^\[foo.assigns.\d+\] line \d+ Check that nondet_var is assignable: SUCCESS$
5+
^\[foo.assigns.\d+\] line \d+ Check that __VERIFIER_var is assignable: SUCCESS$
6+
^\[foo.assigns.\d+\] line \d+ Check that __CPROVER_var is assignable: SUCCESS$
7+
^EXIT=0$
8+
^SIGNAL=0$
9+
^VERIFICATION SUCCESSFUL$
10+
--
11+
--
12+
This test checks that when program variables names have special prefixes
13+
__CPROVER_, __VERIFIER, or nondet, adding them to the write set makes them
14+
assignable.

‎src/goto-instrument/contracts/dynamic-frames/dfcc_cfg_info.cpp‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -794,7 +794,7 @@ static bool must_check_lhs_from_local_and_tracked(
794794
return true;
795795
}
796796
const auto &id = to_symbol_expr(expr).get_identifier();
797-
if(dfcc_is_cprover_symbol(id))
797+
if(dfcc_is_cprover_static_symbol(id))
798798
{
799799
// Skip the check if we have a single cprover symbol as root object
800800
// cprover symbols are used for generic checks instrumentation and are

‎src/goto-instrument/contracts/dynamic-frames/dfcc_instrument.cpp‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -235,7 +235,7 @@ bool dfcc_instrumentt::is_internal_symbol(const irep_idt &id) const
235235
bool dfcc_instrumentt::do_not_instrument(const irep_idt &id) const
236236
{
237237
return !has_prefix(id2string(id), CPROVER_PREFIX "file_local") &&
238-
(dfcc_is_cprover_symbol(id) || is_internal_symbol(id));
238+
(dfcc_is_cprover_function_symbol(id) || is_internal_symbol(id));
239239
}
240240

241241
void dfcc_instrumentt::instrument_harness_function(

‎src/goto-instrument/contracts/dynamic-frames/dfcc_is_cprover_symbol.cpp‎

Lines changed: 135 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -14,9 +14,141 @@ Date: March 2023
1414
#include <util/prefix.h>
1515
#include <util/suffix.h>
1616

17-
bool dfcc_is_cprover_symbol(const irep_idt &id)
17+
#include <unordered_set>
18+
19+
static void
20+
init_function_symbols(std::unordered_set<irep_idt> &function_symbols)
21+
{
22+
// the set of all CPROVER symbols that we know of
23+
if(function_symbols.empty())
24+
{
25+
function_symbols.insert(CPROVER_PREFIX "_start");
26+
function_symbols.insert(CPROVER_PREFIX "array_copy");
27+
function_symbols.insert(CPROVER_PREFIX "array_replace");
28+
function_symbols.insert(CPROVER_PREFIX "array_set");
29+
function_symbols.insert(CPROVER_PREFIX "assert");
30+
function_symbols.insert(CPROVER_PREFIX "assignable");
31+
function_symbols.insert(CPROVER_PREFIX "assume");
32+
function_symbols.insert(CPROVER_PREFIX "contracts_car_create");
33+
function_symbols.insert(CPROVER_PREFIX "contracts_car_set_contains");
34+
function_symbols.insert(CPROVER_PREFIX "contracts_car_set_create");
35+
function_symbols.insert(CPROVER_PREFIX "contracts_car_set_insert");
36+
function_symbols.insert(CPROVER_PREFIX "contracts_car_set_remove");
37+
function_symbols.insert(
38+
CPROVER_PREFIX "contracts_check_replace_ensures_was_freed_preconditions");
39+
function_symbols.insert(CPROVER_PREFIX "contracts_free");
40+
function_symbols.insert(CPROVER_PREFIX "contracts_is_freeable");
41+
function_symbols.insert(CPROVER_PREFIX "contracts_is_fresh");
42+
function_symbols.insert(CPROVER_PREFIX "contracts_link_allocated");
43+
function_symbols.insert(CPROVER_PREFIX "contracts_link_deallocated");
44+
function_symbols.insert(CPROVER_PREFIX "contracts_link_is_fresh");
45+
function_symbols.insert(CPROVER_PREFIX "contracts_obeys_contract");
46+
function_symbols.insert(CPROVER_PREFIX "contracts_obj_set_add");
47+
function_symbols.insert(CPROVER_PREFIX "contracts_obj_set_append");
48+
function_symbols.insert(CPROVER_PREFIX "contracts_obj_set_contains_exact");
49+
function_symbols.insert(CPROVER_PREFIX "contracts_obj_set_contains");
50+
function_symbols.insert(CPROVER_PREFIX "contracts_obj_set_create_append");
51+
function_symbols.insert(CPROVER_PREFIX
52+
"contracts_obj_set_create_indexed_by_object_id");
53+
function_symbols.insert(CPROVER_PREFIX "contracts_obj_set_release");
54+
function_symbols.insert(CPROVER_PREFIX "contracts_obj_set_remove");
55+
function_symbols.insert(CPROVER_PREFIX "contracts_pointer_in_range_dfcc");
56+
function_symbols.insert(CPROVER_PREFIX "contracts_was_freed");
57+
function_symbols.insert(CPROVER_PREFIX "contracts_write_set_add_allocated");
58+
function_symbols.insert(CPROVER_PREFIX "contracts_write_set_add_decl");
59+
function_symbols.insert(CPROVER_PREFIX "contracts_write_set_add_freeable");
60+
function_symbols.insert(
61+
CPROVER_PREFIX
62+
"contracts_write_set_check_allocated_deallocated_is_empty");
63+
function_symbols.insert(CPROVER_PREFIX
64+
"contracts_write_set_check_array_copy");
65+
function_symbols.insert(CPROVER_PREFIX
66+
"contracts_write_set_check_array_replace");
67+
function_symbols.insert(CPROVER_PREFIX
68+
"contracts_write_set_check_array_set");
69+
function_symbols.insert(CPROVER_PREFIX
70+
"contracts_write_set_check_assignment");
71+
function_symbols.insert(
72+
CPROVER_PREFIX "contracts_write_set_check_assigns_clause_inclusion");
73+
function_symbols.insert(CPROVER_PREFIX
74+
"contracts_write_set_check_deallocate");
75+
function_symbols.insert(CPROVER_PREFIX
76+
"contracts_write_set_check_frees_clause_inclusion");
77+
function_symbols.insert(CPROVER_PREFIX
78+
"contracts_write_set_check_havoc_object");
79+
function_symbols.insert(CPROVER_PREFIX "contracts_write_set_create");
80+
function_symbols.insert(CPROVER_PREFIX
81+
"contracts_write_set_deallocate_freeable");
82+
function_symbols.insert(CPROVER_PREFIX
83+
"contracts_write_set_havoc_get_assignable_target");
84+
function_symbols.insert(CPROVER_PREFIX
85+
"contracts_write_set_havoc_object_whole");
86+
function_symbols.insert(CPROVER_PREFIX "contracts_write_set_havoc_slice");
87+
function_symbols.insert(CPROVER_PREFIX
88+
"contracts_write_set_insert_assignable");
89+
function_symbols.insert(CPROVER_PREFIX
90+
"contracts_write_set_insert_object_from");
91+
function_symbols.insert(CPROVER_PREFIX
92+
"contracts_write_set_insert_object_upto");
93+
function_symbols.insert(CPROVER_PREFIX
94+
"contracts_write_set_insert_object_whole");
95+
function_symbols.insert(CPROVER_PREFIX "contracts_write_set_record_dead");
96+
function_symbols.insert(CPROVER_PREFIX
97+
"contracts_write_set_record_deallocated");
98+
function_symbols.insert(CPROVER_PREFIX "contracts_write_set_release");
99+
function_symbols.insert(CPROVER_PREFIX "deallocate");
100+
function_symbols.insert(CPROVER_PREFIX "freeable");
101+
function_symbols.insert(CPROVER_PREFIX "havoc_object");
102+
function_symbols.insert(CPROVER_PREFIX "havoc_slice");
103+
function_symbols.insert(CPROVER_PREFIX "initialize");
104+
function_symbols.insert(CPROVER_PREFIX "is_freeable");
105+
function_symbols.insert(CPROVER_PREFIX "is_fresh");
106+
function_symbols.insert(CPROVER_PREFIX "obeys_contract");
107+
function_symbols.insert(CPROVER_PREFIX "object_from");
108+
function_symbols.insert(CPROVER_PREFIX "object_upto");
109+
function_symbols.insert(CPROVER_PREFIX "object_whole");
110+
function_symbols.insert(CPROVER_PREFIX "pointer_in_range_dfcc");
111+
function_symbols.insert(CPROVER_PREFIX "precondition");
112+
function_symbols.insert(CPROVER_PREFIX "printf");
113+
function_symbols.insert(CPROVER_PREFIX "was_freed");
114+
}
115+
}
116+
117+
static void init_static_symbols(std::unordered_set<irep_idt> &static_symbols)
118+
{
119+
if(static_symbols.empty())
120+
{
121+
static_symbols.insert(CPROVER_PREFIX "dead_object");
122+
static_symbols.insert(CPROVER_PREFIX "deallocated");
123+
static_symbols.insert(CPROVER_PREFIX "fpu_control_word");
124+
static_symbols.insert(CPROVER_PREFIX "jsa_jump_buffer");
125+
static_symbols.insert(CPROVER_PREFIX "malloc_failure_mode_return_null");
126+
static_symbols.insert(CPROVER_PREFIX
127+
"malloc_failure_mode_assert_then_assume");
128+
static_symbols.insert(CPROVER_PREFIX "malloc_is_new_array");
129+
static_symbols.insert(CPROVER_PREFIX "max_malloc_size");
130+
static_symbols.insert(CPROVER_PREFIX "memory_leak");
131+
static_symbols.insert(CPROVER_PREFIX "pipe_offset");
132+
static_symbols.insert(CPROVER_PREFIX "pipes");
133+
static_symbols.insert(CPROVER_PREFIX "rounding_mode");
134+
}
135+
}
136+
137+
bool dfcc_is_cprover_function_symbol(const irep_idt &id)
18138
{
139+
std::unordered_set<irep_idt> function_symbols;
140+
init_function_symbols(function_symbols);
19141
std::string str = id2string(id);
20-
return has_prefix(str, CPROVER_PREFIX) || has_prefix(str, "__VERIFIER") ||
21-
has_prefix(str, "nondet") || has_suffix(str, "$object");
142+
return function_symbols.find(id) != function_symbols.end() ||
143+
// nondet functions
144+
has_prefix(str, "__VERIFIER") || has_prefix(str, "nondet");
145+
}
146+
147+
bool dfcc_is_cprover_static_symbol(const irep_idt &id)
148+
{
149+
std::unordered_set<irep_idt> static_symbols;
150+
init_static_symbols(static_symbols);
151+
return static_symbols.find(id) != static_symbols.end() ||
152+
// auto objects from pointer derefs
153+
has_suffix(id2string(id), "$object");
22154
}

‎src/goto-instrument/contracts/dynamic-frames/dfcc_is_cprover_symbol.h‎

Lines changed: 8 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -15,8 +15,13 @@ Date: March 2023
1515

1616
#include <util/irep.h>
1717

18-
/// \return True iff the id starts with CPROVER_PREFIX, `__VERIFIER`, `nondet`
19-
/// or ends with `$object`.
20-
bool dfcc_is_cprover_symbol(const irep_idt &id);
18+
/// Returns `true` iff id is one of the known CPROVER functions or starts with
19+
/// `__VERIFIER` or `nondet`.
20+
bool dfcc_is_cprover_function_symbol(const irep_idt &id);
21+
22+
/// Returns `true` iff the symbol is one of the known CPROVER static
23+
/// instrumentation variables or ends with `$object` and represents an
24+
/// auto-generated object following a pointer dereference.
25+
bool dfcc_is_cprover_static_symbol(const irep_idt &id);
2126

2227
#endif

0 commit comments

Comments
 (0)