Skip to content

Commit 656ddfa

Browse files
qinhepingqinheping
committed
Detect loop locals with goto_rw in DFCC
1 parent 20a1ecf commit 656ddfa

File tree

12 files changed

+185
-56
lines changed

12 files changed

+185
-56
lines changed

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

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,8 @@
11
void foo()
22
{
3-
int nondet_var;
4-
int __VERIFIER_var;
5-
int __CPROVER_var;
3+
int nondet_var = nondet_int();
4+
int __VERIFIER_var = nondet_int();
5+
int __CPROVER_var = nondet_int();
66
for(int i = 10; i > 0; i--)
77
// clang-format off
88
__CPROVER_assigns(i)

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

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,8 @@
11
void foo()
22
{
3-
int nondet_var;
4-
int __VERIFIER_var;
5-
int __CPROVER_var;
3+
int nondet_var = nondet_int();
4+
int __VERIFIER_var = nondet_int();
5+
int __CPROVER_var = nondet_int();
66
for(int i = 10; i > 0; i--)
77
// clang-format off
88
__CPROVER_assigns(i,nondet_var, __VERIFIER_var, __CPROVER_var)

‎regression/contracts-dfcc/invar_loop-entry_check/main.c

Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -12,7 +12,7 @@ void main()
1212
x1 = &z1;
1313

1414
while(y1 > 0)
15-
__CPROVER_loop_invariant(*x1 == __CPROVER_loop_entry(*x1))
15+
__CPROVER_loop_invariant(y1 >= 0 && *x1 == __CPROVER_loop_entry(*x1))
1616
{
1717
--y1;
1818
*x1 = *x1 + 1;
@@ -24,7 +24,7 @@ void main()
2424
x2 = z2;
2525

2626
while(y2 > 0)
27-
__CPROVER_loop_invariant(x2 == __CPROVER_loop_entry(x2))
27+
__CPROVER_loop_invariant(y2 >= 0 && x2 == __CPROVER_loop_entry(x2))
2828
{
2929
--y2;
3030
x2 = x2 + 1;
@@ -34,11 +34,12 @@ void main()
3434

3535
int y3;
3636
s s0, s1, *s2 = &s0;
37+
s0.n = nondet_int();
3738
s2->n = malloc(sizeof(int));
3839
s1.n = s2->n;
3940

4041
while(y3 > 0)
41-
__CPROVER_loop_invariant(s2->n == __CPROVER_loop_entry(s2->n))
42+
__CPROVER_loop_invariant(y3 >= 0 && s2->n == __CPROVER_loop_entry(s2->n))
4243
{
4344
--y3;
4445
s0.n = s0.n + 1;

‎regression/contracts-dfcc/invar_loop-entry_check/test.desc

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -11,10 +11,10 @@ main.c
1111
^\[main.loop_invariant_base.\d+] line 26 Check invariant before entry for loop .*: SUCCESS$
1212
^\[main.loop_invariant_step.\d+] line 26 Check invariant after step for loop .*: SUCCESS$
1313
^\[main.loop_step_unwinding.\d+] line 26 Check step was unwound for loop .*: SUCCESS$
14-
^\[main.loop_assigns.\d+] line 40 Check assigns clause inclusion for loop .*: SUCCESS$
15-
^\[main.loop_invariant_base.\d+] line 40 Check invariant before entry for loop .*: SUCCESS$
16-
^\[main.loop_invariant_step.\d+] line 40 Check invariant after step for loop .*: SUCCESS$
17-
^\[main.loop_step_unwinding.\d+] line 40 Check step was unwound for loop .*: SUCCESS$
14+
^\[main.loop_assigns.\d+] line 41 Check assigns clause inclusion for loop .*: SUCCESS$
15+
^\[main.loop_invariant_base.\d+] line 41 Check invariant before entry for loop .*: SUCCESS$
16+
^\[main.loop_invariant_step.\d+] line 41 Check invariant after step for loop .*: SUCCESS$
17+
^\[main.loop_step_unwinding.\d+] line 41 Check step was unwound for loop .*: SUCCESS$
1818
^\[main\.assertion\.\d+\] .* assertion \*x1 == z1: SUCCESS$
1919
^\[main\.assertion\.\d+\] .* assertion x2 == z2: SUCCESS$
2020
^\[main.assigns.\d+\] .* Check that y1 is assignable: SUCCESS$

‎regression/contracts-dfcc/invar_loop-entry_fail/main.c

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,7 @@ void main()
66
x = z;
77

88
while(y > 0)
9-
__CPROVER_loop_invariant(x == __CPROVER_loop_entry(x))
9+
__CPROVER_loop_invariant(y >= 0 && x == __CPROVER_loop_entry(x))
1010
{
1111
--y;
1212
x = x + 1;

‎regression/contracts-dfcc/loop_assigns_inference-02/main.c

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -10,11 +10,14 @@ void main()
1010
void foo()
1111
{
1212
int *b = malloc(SIZE * sizeof(int));
13+
int *j;
1314
for(unsigned i = 0; i < SIZE; i++)
1415
// clang-format off
1516
__CPROVER_loop_invariant(i <= SIZE)
1617
// clang-format on
1718
{
19+
j = malloc(SIZE * sizeof(int));
1820
b[i] = 1;
21+
free(j);
1922
}
2023
}

‎regression/contracts-dfcc/loop_assigns_inference-02/test.desc

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -3,12 +3,12 @@ main.c
33
--no-malloc-may-fail --dfcc main --apply-loop-contracts
44
^EXIT=0$
55
^SIGNAL=0$
6-
^\[foo.loop_assigns.\d+\] line 13 Check assigns clause inclusion for loop .*: SUCCESS$
7-
^\[foo.loop_assigns.\d+\] line 13 Check assigns clause inclusion for loop .*: SUCCESS$
8-
^\[foo.loop_invariant_base.\d+\] line 13 Check invariant before entry for loop .*: SUCCESS$
9-
^\[foo.loop_invariant_base.\d+\] line 13 Check invariant before entry for loop .*: SUCCESS$
10-
^\[foo.loop_invariant_step.\d+\] line 13 Check invariant after step for loop .*: SUCCESS$
11-
^\[foo.loop_step_unwinding.\d+\] line 13 Check step was unwound for loop .*: SUCCESS$
6+
^\[foo.loop_assigns.\d+\] line 14 Check assigns clause inclusion for loop .*: SUCCESS$
7+
^\[foo.loop_assigns.\d+\] line 14 Check assigns clause inclusion for loop .*: SUCCESS$
8+
^\[foo.loop_invariant_base.\d+\] line 14 Check invariant before entry for loop .*: SUCCESS$
9+
^\[foo.loop_invariant_base.\d+\] line 14 Check invariant before entry for loop .*: SUCCESS$
10+
^\[foo.loop_invariant_step.\d+\] line 14 Check invariant after step for loop .*: SUCCESS$
11+
^\[foo.loop_step_unwinding.\d+\] line 14 Check step was unwound for loop .*: SUCCESS$
1212
^\[foo.assigns.\d+\] .* Check that i is assignable: SUCCESS$
1313
^\[foo.assigns.\d+\] .* Check that b\[(.*)i\] is assignable: SUCCESS$
1414
^VERIFICATION SUCCESSFUL$

‎regression/contracts-dfcc/loop_assigns_inference-03/main.c

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -7,7 +7,7 @@ void main()
77
int b[SIZE];
88
for(unsigned i = 0; i < SIZE; i++)
99
// clang-format off
10-
__CPROVER_loop_invariant(i <= SIZE)
10+
__CPROVER_loop_invariant((i == 0 || b[0] == 1) && i <= SIZE)
1111
// clang-format on
1212
{
1313
b[i] = 1;

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

Lines changed: 24 additions & 24 deletions
Original file line numberDiff line numberDiff line change
@@ -253,26 +253,6 @@ static bool is_assigned(dirtyt &dirty, const irep_idt &ident, assignst assigns)
253253
return false;
254254
}
255255

256-
/// Collect identifiers that are local to this loop only
257-
/// (excluding nested loop).
258-
static std::unordered_set<irep_idt> gen_loop_locals_set(
259-
const dfcc_loop_nesting_grapht &loop_nesting_graph,
260-
const std::size_t loop_id)
261-
{
262-
std::unordered_set<irep_idt> loop_locals;
263-
for(const auto &target : loop_nesting_graph[loop_id].instructions)
264-
{
265-
auto loop_id_opt = dfcc_get_loop_id(target);
266-
if(
267-
target->is_decl() && loop_id_opt.has_value() &&
268-
loop_id_opt.value() == loop_id)
269-
{
270-
loop_locals.insert(target->decl_symbol().get_identifier());
271-
}
272-
}
273-
return loop_locals;
274-
}
275-
276256
/// Compute subset of locals that must be tracked in the loop's write set.
277257
/// A local must be tracked if it is dirty or if it may be assigned by one
278258
/// of the inner loops.
@@ -329,6 +309,7 @@ static struct contract_clausest default_loop_contract_clauses(
329309
const dfcc_loop_nesting_grapht &loop_nesting_graph,
330310
const std::size_t loop_id,
331311
const irep_idt &function_id,
312+
goto_functiont &goto_function,
332313
local_may_aliast &local_may_alias,
333314
const bool check_side_effect,
334315
message_handlert &message_handler,
@@ -381,7 +362,7 @@ static struct contract_clausest default_loop_contract_clauses(
381362
{
382363
// infer assigns clause targets if none given
383364
auto inferred = dfcc_infer_loop_assigns(
384-
local_may_alias, loop.instructions, loop.head->source_location(), ns);
365+
local_may_alias, goto_function, loop, message_handler, ns);
385366
log.warning() << "No assigns clause provided for loop " << function_id
386367
<< "." << loop.latch->loop_number << " at "
387368
<< loop.head->source_location() << ". The inferred set {";
@@ -416,6 +397,7 @@ static dfcc_loop_infot gen_dfcc_loop_info(
416397
const dfcc_loop_nesting_grapht &loop_nesting_graph,
417398
const std::size_t loop_id,
418399
const irep_idt &function_id,
400+
goto_functiont &goto_function,
419401
const std::map<std::size_t, dfcc_loop_infot> &loop_info_map,
420402
dirtyt &dirty,
421403
local_may_aliast &local_may_alias,
@@ -424,20 +406,37 @@ static dfcc_loop_infot gen_dfcc_loop_info(
424406
dfcc_libraryt &library,
425407
symbol_table_baset &symbol_table)
426408
{
427-
std::unordered_set<irep_idt> loop_locals =
428-
gen_loop_locals_set(loop_nesting_graph, loop_id);
409+
const namespacet ns(symbol_table);
410+
std::unordered_set<irep_idt> loop_locals = gen_loop_locals_set(
411+
function_id,
412+
goto_function,
413+
loop_nesting_graph[loop_id],
414+
message_handler,
415+
ns);
416+
417+
// Exclude locals of inner nested loops.
418+
for(const auto &inner_loop : loop_nesting_graph.get_predecessors(loop_id))
419+
{
420+
INVARIANT(
421+
loop_info_map.find(inner_loop) != loop_info_map.end(),
422+
"DFCC should gen_dfcc_loop_info for inner loops first.");
423+
for(const auto &inner_local : loop_info_map.at(inner_loop).local)
424+
{
425+
loop_locals.erase(inner_local);
426+
}
427+
}
429428

430429
std::unordered_set<irep_idt> loop_tracked = gen_tracked_set(
431430
loop_nesting_graph.get_predecessors(loop_id),
432431
loop_locals,
433432
dirty,
434433
loop_info_map);
435434

436-
const namespacet ns(symbol_table);
437435
struct contract_clausest contract_clauses = default_loop_contract_clauses(
438436
loop_nesting_graph,
439437
loop_id,
440438
function_id,
439+
goto_function,
441440
local_may_alias,
442441
check_side_effect,
443442
message_handler,
@@ -559,6 +558,7 @@ dfcc_cfg_infot::dfcc_cfg_infot(
559558
loop_nesting_graph,
560559
loop_id,
561560
function_id,
561+
goto_function,
562562
loop_info_map,
563563
dirty,
564564
local_may_alias,

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

Lines changed: 114 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -13,6 +13,7 @@ Author: Remi Delmas, [email protected]
1313
#include <util/pointer_expr.h>
1414
#include <util/std_code.h>
1515

16+
#include <analyses/goto_rw.h>
1617
#include <goto-instrument/contracts/utils.h>
1718
#include <goto-instrument/havoc_utils.h>
1819

@@ -46,23 +47,127 @@ depends_on(const exprt &expr, std::unordered_set<irep_idt> identifiers)
4647
return false;
4748
}
4849

50+
/// Collect identifiers that are local to this loop.
51+
/// A identifier is or is equivalent to a loop local if
52+
/// 1. it is declared inside the loop, or
53+
/// 2. there is no write or read of it outside the loop.
54+
/// 3. it is not used in loop contracts.
55+
std::unordered_set<irep_idt> gen_loop_locals_set(
56+
const irep_idt &function_id,
57+
goto_functiont &goto_function,
58+
const dfcc_loop_nesting_graph_nodet &loop_node,
59+
message_handlert &message_handler,
60+
const namespacet &ns)
61+
{
62+
std::unordered_set<irep_idt> loop_locals;
63+
std::unordered_set<irep_idt> non_loop_locals;
64+
65+
const auto &loop = loop_node.instructions;
66+
67+
// All identifiers declared outside the loop.
68+
std::unordered_set<irep_idt> non_loop_decls;
69+
// Ranges of all read/write outside the loop.
70+
rw_range_sett non_loop_rw_range_set(ns, message_handler);
71+
72+
Forall_goto_program_instructions(i_it, goto_function.body)
73+
{
74+
// All variables declared in loops are loop locals.
75+
if(i_it->is_decl() && loop.contains(i_it))
76+
{
77+
loop_locals.insert(i_it->decl_symbol().get_identifier());
78+
}
79+
// Record all other declared variables and their ranges.
80+
else if(i_it->is_decl())
81+
{
82+
non_loop_decls.insert(i_it->decl_symbol().get_identifier());
83+
}
84+
// Record all writing/reading outside the loop.
85+
else if(
86+
(i_it->is_assign() || i_it->is_function_call()) && !loop.contains(i_it))
87+
{
88+
goto_rw(function_id, i_it, non_loop_rw_range_set);
89+
}
90+
}
91+
92+
// Check if declared variables are loop locals.
93+
for(const auto &decl_id : non_loop_decls)
94+
{
95+
bool is_loop_local = true;
96+
// No write to the declared variable.
97+
for(const auto &writing_rw : non_loop_rw_range_set.get_w_set())
98+
{
99+
if(decl_id == writing_rw.first)
100+
{
101+
is_loop_local = false;
102+
break;
103+
}
104+
}
105+
106+
// No read to the declared variable.
107+
for(const auto &writing_rw : non_loop_rw_range_set.get_r_set())
108+
{
109+
if(decl_id == writing_rw.first)
110+
{
111+
is_loop_local = false;
112+
break;
113+
}
114+
}
115+
116+
const auto latch_target = loop_node.latch;
117+
118+
// Loop locals are not used in loop contracts.
119+
for(const auto &id :
120+
find_symbol_identifiers(get_loop_assigns(latch_target)))
121+
{
122+
if(decl_id == id)
123+
{
124+
is_loop_local = false;
125+
break;
126+
}
127+
}
128+
129+
for(const auto &id :
130+
find_symbol_identifiers(get_loop_invariants(latch_target)))
131+
{
132+
if(decl_id == id)
133+
{
134+
is_loop_local = false;
135+
break;
136+
}
137+
}
138+
139+
for(const auto &id :
140+
find_symbol_identifiers(get_loop_decreases(latch_target)))
141+
{
142+
if(decl_id == id)
143+
{
144+
is_loop_local = false;
145+
break;
146+
}
147+
}
148+
149+
// Collect all loop locals.
150+
if(is_loop_local)
151+
loop_locals.insert(decl_id);
152+
}
153+
154+
return loop_locals;
155+
}
156+
49157
assignst dfcc_infer_loop_assigns(
50158
const local_may_aliast &local_may_alias,
51-
const loopt &loop_instructions,
52-
const source_locationt &loop_head_location,
159+
goto_functiont &goto_function,
160+
const dfcc_loop_nesting_graph_nodet &loop,
161+
message_handlert &message_handler,
53162
const namespacet &ns)
54163
{
55164
// infer
56165
assignst assigns;
57-
infer_loop_assigns(local_may_alias, loop_instructions, assigns);
166+
infer_loop_assigns(local_may_alias, loop.instructions, assigns);
58167

59168
// compute locals
60-
std::unordered_set<irep_idt> loop_locals;
61-
for(const auto &target : loop_instructions)
62-
{
63-
if(target->is_decl())
64-
loop_locals.insert(target->decl_symbol().get_identifier());
65-
}
169+
std::unordered_set<irep_idt> loop_locals =
170+
gen_loop_locals_set(irep_idt(), goto_function, loop, message_handler, ns);
66171

67172
// widen or drop targets that depend on loop-locals or are non-constant,
68173
// ie. depend on other locations assigned by the loop.

0 commit comments

Comments
 (0)