Skip to content

Commit 8718e33

Browse files
tautschnigtautschnig
authored
Merge pull request #7708 from remi-delmas-3000/contracts-use-allow-lists
CONTRACTS: `dfcc_is_cprover_symbol` now uses allow lists to match symbols
2 parents ce4c504 + 407914b commit 8718e33

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
@@ -792,7 +792,7 @@ static bool must_check_lhs_from_local_and_tracked(
792792
return true;
793793
}
794794
const auto &id = to_symbol_expr(expr).get_identifier();
795-
if(dfcc_is_cprover_symbol(id))
795+
if(dfcc_is_cprover_static_symbol(id))
796796
{
797797
// Skip the check if we have a single cprover symbol as root object
798798
// 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
@@ -232,7 +232,7 @@ bool dfcc_instrumentt::is_internal_symbol(const irep_idt &id) const
232232
bool dfcc_instrumentt::do_not_instrument(const irep_idt &id) const
233233
{
234234
return !has_prefix(id2string(id), CPROVER_PREFIX "file_local") &&
235-
(dfcc_is_cprover_symbol(id) || is_internal_symbol(id));
235+
(dfcc_is_cprover_function_symbol(id) || is_internal_symbol(id));
236236
}
237237

238238
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)