Skip to content

Commit 269f253

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

File tree

24 files changed

+149
-61
lines changed

24 files changed

+149
-61
lines changed

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

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1,11 +1,11 @@
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
8-
__CPROVER_assigns(i)
8+
__CPROVER_assigns(i)
99
__CPROVER_loop_invariant(0 <= i && i <= 10)
1010
__CPROVER_decreases(i)
1111
// clang-format on

‎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_assigns_opt/main.c

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -17,7 +17,7 @@ int foo()
1717
}
1818
assert(r1 == 0);
1919

20-
int r2, s2 = 1;
20+
int r2 = nondet_int(), s2 = 1;
2121
__CPROVER_assume(r2 >= 0);
2222
while(r2 > 0)
2323
__CPROVER_assigns(r2, s2) __CPROVER_loop_invariant(r2 >= 0 && s2 == 1)

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

Lines changed: 1 addition & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,6 @@
1-
#include <assert.h>
2-
31
int main()
42
{
5-
int r;
3+
int r = nondet_int();
64
__CPROVER_assume(r >= 0);
75

86
while(r > 0)

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

Lines changed: 1 addition & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,6 @@
1-
#include <assert.h>
2-
31
int main()
42
{
5-
int r;
3+
int r = nondet_int();
64
__CPROVER_assume(r >= 0);
75

86
while(r > 0)

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

Lines changed: 1 addition & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,6 @@
1-
#include <assert.h>
2-
31
int main()
42
{
5-
int r;
3+
int r = nondet_int();
64
__CPROVER_assume(r >= 0);
75

86
while(r > 0)

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2,7 +2,7 @@
22

33
int main()
44
{
5-
int r, n, x, y;
5+
int r, n, x = nondet_int(), y = nondet_int();
66
__CPROVER_assume(n > 0 && x == y);
77

88
for(r = 0; r < n; ++r)

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

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -2,7 +2,7 @@
22

33
int main()
44
{
5-
int n, s = 0;
5+
int n = nondet_int(), s = 0;
66
__CPROVER_assume(n >= 0);
77

88
for(int i = 0; i < n; ++i)
@@ -11,7 +11,7 @@ int main()
1111
__CPROVER_decreases(n - i)
1212
// clang-format on
1313
{
14-
int a, b;
14+
int a = nondet_int(), b = nondet_int();
1515
__CPROVER_assume(b >= 0 && a == b);
1616

1717
while(a > 0)

‎regression/contracts-dfcc/invar_check_pointer_modifies-01/main.c

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,7 @@ void main()
66
char *data = malloc(1);
77
*data = 42;
88

9-
unsigned i;
9+
unsigned i = nondet_int();
1010
while(i > 0)
1111
// clang-format off
1212
__CPROVER_loop_invariant(*data == 42)

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -8,7 +8,7 @@ void main()
88
copy = data;
99
*data = 42;
1010

11-
unsigned i;
11+
unsigned i = nondet_int();
1212
while(i > 0)
1313
// clang-format off
1414
__CPROVER_loop_invariant(*data == 42)

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2,7 +2,7 @@
22

33
int main()
44
{
5-
int r;
5+
int r = nondet_int();
66
__CPROVER_assume(r >= 0);
77

88
while(r > 0)

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

Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -8,7 +8,7 @@ typedef struct
88

99
void main()
1010
{
11-
int *x1, y1, z1;
11+
int *x1, y1 = nondet_int(), z1;
1212
x1 = &z1;
1313

1414
while(y1 > 0)
@@ -20,7 +20,7 @@ void main()
2020
}
2121
assert(*x1 == z1);
2222

23-
int x2, y2, z2;
23+
int x2, y2 = nondet_int(), z2;
2424
x2 = z2;
2525

2626
while(y2 > 0)
@@ -32,8 +32,9 @@ void main()
3232
}
3333
assert(x2 == z2);
3434

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

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2,7 +2,7 @@
22

33
void main()
44
{
5-
int x, y, z;
5+
int x = nondet_int(), y = nondet_int(), z = nondet_int();
66
x = z;
77

88
while(y > 0)

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2,7 +2,7 @@
22

33
int main()
44
{
5-
int r;
5+
int r = nondet_int();
66
int s = 1;
77
__CPROVER_assume(r >= 0);
88
while(r > 0)

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2,7 +2,7 @@
22

33
int main()
44
{
5-
int r;
5+
int r = nondet_int();
66
int s = 1;
77
__CPROVER_assume(r >= 0);
88
while(r > 0)

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2,7 +2,7 @@
22

33
int main()
44
{
5-
int r, s = 1;
5+
int r = nondet_int(), s = 1;
66
__CPROVER_assume(r >= 0);
77
while(r > 0)
88
// clang-format off

‎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 & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -12,4 +12,5 @@ void main()
1212
{
1313
b[i] = 1;
1414
}
15+
assert(b[0] = 1);
1516
}

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

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -6,6 +6,9 @@ int foo() __CPROVER_assigns()
66
char buf1[SIZE];
77
char buf2[SIZE];
88
char buf3[SIZE];
9+
buf1[0]= 0;
10+
buf2[0]= 0;
11+
buf3[0]= 0;
912
size_t i = 0;
1013
while(i < SIZE)
1114
// clang-format off

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

Lines changed: 17 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,12 @@ 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,
366+
goto_function,
367+
loop.instructions,
368+
loop.head->source_location(),
369+
message_handler,
370+
ns);
385371
log.warning() << "No assigns clause provided for loop " << function_id
386372
<< "." << loop.latch->loop_number << " at "
387373
<< loop.head->source_location() << ". The inferred set {";
@@ -416,6 +402,7 @@ static dfcc_loop_infot gen_dfcc_loop_info(
416402
const dfcc_loop_nesting_grapht &loop_nesting_graph,
417403
const std::size_t loop_id,
418404
const irep_idt &function_id,
405+
goto_functiont &goto_function,
419406
const std::map<std::size_t, dfcc_loop_infot> &loop_info_map,
420407
dirtyt &dirty,
421408
local_may_aliast &local_may_alias,
@@ -424,20 +411,25 @@ static dfcc_loop_infot gen_dfcc_loop_info(
424411
dfcc_libraryt &library,
425412
symbol_table_baset &symbol_table)
426413
{
427-
std::unordered_set<irep_idt> loop_locals =
428-
gen_loop_locals_set(loop_nesting_graph, loop_id);
414+
const namespacet ns(symbol_table);
415+
std::unordered_set<irep_idt> loop_locals = gen_loop_locals_set(
416+
function_id,
417+
goto_function,
418+
loop_nesting_graph[loop_id].instructions,
419+
message_handler,
420+
ns);
429421

430422
std::unordered_set<irep_idt> loop_tracked = gen_tracked_set(
431423
loop_nesting_graph.get_predecessors(loop_id),
432424
loop_locals,
433425
dirty,
434426
loop_info_map);
435427

436-
const namespacet ns(symbol_table);
437428
struct contract_clausest contract_clauses = default_loop_contract_clauses(
438429
loop_nesting_graph,
439430
loop_id,
440431
function_id,
432+
goto_function,
441433
local_may_alias,
442434
check_side_effect,
443435
message_handler,
@@ -559,6 +551,7 @@ dfcc_cfg_infot::dfcc_cfg_infot(
559551
loop_nesting_graph,
560552
loop_id,
561553
function_id,
554+
goto_function,
562555
loop_info_map,
563556
dirty,
564557
local_may_alias,

0 commit comments

Comments
 (0)