Skip to content

Commit 7954845

Browse files
author
Remi Delmas
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 6f175c5 commit 7954845

File tree

8 files changed

+217
-8
lines changed

8 files changed

+217
-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 --enforce-contract foo --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 --enforce-contract foo --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
@@ -795,7 +795,7 @@ static bool must_check_lhs_from_local_and_tracked(
795795
return true;
796796
}
797797
const auto &id = to_symbol_expr(expr).get_identifier();
798-
if(dfcc_is_cprover_symbol(id))
798+
if(dfcc_is_cprover_static_symbol(id))
799799
{
800800
// Skip the check if we have a single cprover symbol as root object
801801
// 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: 134 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -14,9 +14,140 @@ 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 std::unordered_set<irep_idt> function_symbols;
20+
static std::unordered_set<irep_idt> static_symbols;
21+
22+
static void init_function_symbols()
23+
{
24+
// the set of all CPROVER symbols that we know of
25+
if(function_symbols.empty())
26+
{
27+
function_symbols.insert(CPROVER_PREFIX "_start");
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()
118+
{
119+
if(static_symbols.empty())
120+
{
121+
static_symbols.insert(CPROVER_PREFIX "pipe_offset");
122+
static_symbols.insert(CPROVER_PREFIX "pipes");
123+
static_symbols.insert(CPROVER_PREFIX "rounding_mode");
124+
static_symbols.insert(CPROVER_PREFIX "deallocated");
125+
static_symbols.insert(CPROVER_PREFIX "dead_object");
126+
static_symbols.insert(CPROVER_PREFIX "fpu_control_word");
127+
static_symbols.insert(CPROVER_PREFIX "jsa_jump_buffer");
128+
static_symbols.insert(CPROVER_PREFIX
129+
"malloc_failure_mode_assert_then_assume");
130+
static_symbols.insert(CPROVER_PREFIX "malloc_failure_mode_return_null");
131+
static_symbols.insert(CPROVER_PREFIX "malloc_is_new_array");
132+
static_symbols.insert(CPROVER_PREFIX "max_malloc_size");
133+
static_symbols.insert(CPROVER_PREFIX "memory_leak");
134+
}
135+
}
136+
137+
bool dfcc_is_cprover_function_symbol(const irep_idt &id)
138+
{
139+
init_function_symbols();
140+
std::string str = id2string(id);
141+
return function_symbols.find(id) != function_symbols.end() ||
142+
// nondet functions
143+
has_prefix(str, "__VERIFIER") || has_prefix(str, "nondet");
144+
}
145+
146+
bool dfcc_is_cprover_static_symbol(const irep_idt &id)
18147
{
148+
init_static_symbols();
19149
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");
150+
return static_symbols.find(id) != static_symbols.end() ||
151+
// auto objects from pointer derefs
152+
has_suffix(str, "$object");
22153
}

‎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 know 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)