Skip to content

Commit d46627d

Browse files
Merge pull request #6947 from remi-delmas-3000/cfg-info-loops
CONTRACTS: detect and handle locals in assigns clause checking for loops
2 parents 240daac + 00959cc commit d46627d

File tree

13 files changed

+350
-286
lines changed

13 files changed

+350
-286
lines changed
Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
#include <stdlib.h>
2+
3+
int main()
4+
{
5+
unsigned char *i = malloc(5);
6+
7+
while(i != i + 5)
8+
__CPROVER_loop_invariant(1 == 1)
9+
{
10+
const char lower = *i++;
11+
}
12+
}
Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
CORE
2+
main.c
3+
--apply-loop-contracts
4+
^\[main.assigns.\d+\].*line 10 Check that i is assignable: SUCCESS$
5+
^EXIT=0$
6+
^SIGNAL=0$
7+
^VERIFICATION SUCCESSFUL$
8+
--
9+
--
10+
Checks that loop local variables do not cause explicit checks
Lines changed: 28 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,28 @@
1+
static void foo()
2+
{
3+
unsigned i;
4+
5+
for(i = 0; i < 16; i++)
6+
__CPROVER_loop_invariant(1 == 1)
7+
{
8+
int v = 1;
9+
}
10+
}
11+
12+
static void bar()
13+
{
14+
unsigned i;
15+
16+
for(i = 0; i < 16; i++)
17+
__CPROVER_loop_invariant(1 == 1)
18+
{
19+
int v = 1;
20+
}
21+
}
22+
23+
int main()
24+
{
25+
bar();
26+
foo();
27+
foo();
28+
}
Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
CORE
2+
main.c
3+
--apply-loop-contracts
4+
^\[bar.assigns.\d+\].*Check that i is assignable: SUCCESS$
5+
^\[foo.assigns.\d+\].*Check that i is assignable: SUCCESS$
6+
^EXIT=0$
7+
^SIGNAL=0$
8+
^VERIFICATION SUCCESSFUL$
9+
--
10+
--
11+
Checks that loop local variables do not cause explicit checks

regression/contracts/invar_check_nested_loops/test.desc

Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -9,9 +9,10 @@ main.c
99
^\[main\.\d+\] .* Check loop invariant before entry: SUCCESS$
1010
^\[main\.\d+\] .* Check that loop invariant is preserved: SUCCESS$
1111
^\[main\.\d+\] .* Check decreases clause on loop iteration: SUCCESS$
12-
^\[main.assigns.\d+] .* line 23 Check that s is assignable: SUCCESS$
13-
^\[main.assigns.\d+] .* line 24 Check that a is assignable: SUCCESS$
14-
^\[main.assigns.\d+] .* line 27 Check that s is assignable: SUCCESS$
12+
^\[main\.assigns\.\d+\].*line 17 Check that s is assignable: SUCCESS$
13+
^\[main\.assigns\.\d+\].*line 23 Check that s is assignable: SUCCESS$
14+
^\[main\.assigns\.\d+\].*line 24 Check that a is assignable: SUCCESS$
15+
^\[main\.assigns\.\d+\].*line 27 Check that s is assignable: SUCCESS$
1516
^\[main\.assertion.\d+\] .* assertion s == n: SUCCESS$
1617
^VERIFICATION SUCCESSFUL$
1718
--

regression/contracts/loop_guard_with_side_effects/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,6 @@ main.c
44
\[check.assigns\.\d+\] line \d+ Check that \*j is assignable: SUCCESS$
55
\[check.overflow\.\d+\] line \d+ arithmetic overflow on unsigned \+ in \*j \+ 1u: SUCCESS
66
\[check.overflow\.\d+\] line \d+ arithmetic overflow on unsigned \+ in \*j \+ 1u: SUCCESS
7-
\[check.assigns\.\d+\] line \d+ Check that return_value_check is assignable: SUCCESS$
87
\[main\.\d+\] line \d+ Check loop invariant before entry: SUCCESS$
98
\[main\.\d+\] line \d+ Check that loop invariant is preserved: SUCCESS$
109
\[main.assigns\.\d+\] line \d+ Check that i is assignable: SUCCESS$
@@ -16,6 +15,7 @@ main.c
1615
\[main.assertion\.\d+\] line \d+ assertion j == k \+ 1: SUCCESS$
1716
^EXIT=0$
1817
^SIGNAL=0$
18+
^VERIFICATION SUCCESSFUL$
1919
--
2020
--
2121
This test demonstrates a case where the loop guard has side effects.

regression/contracts/loop_guard_with_side_effects_fail/test.desc

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2,7 +2,6 @@ CORE
22
main.c
33
--apply-loop-contracts _ --unsigned-overflow-check
44
\[check.assigns\.\d+\] line \d+ Check that \*j is assignable: FAILURE$
5-
\[check.assigns\.\d+\] line \d+ Check that return_value_check is assignable: SUCCESS$
65
\[main\.\d+\] line \d+ Check loop invariant before entry: SUCCESS$
76
\[main\.\d+\] line \d+ Check that loop invariant is preserved: SUCCESS$
87
\[main.assigns\.\d+\] line \d+ Check that i is assignable: SUCCESS$
Lines changed: 197 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,197 @@
1+
/*******************************************************************\
2+
3+
Module: CFG-based information for assigns clause checking simplification
4+
5+
Author: Remi Delmas
6+
7+
Date: June 2022
8+
9+
\*******************************************************************/
10+
11+
/// \file
12+
/// Classes providing CFG-based information about symbols to guide
13+
/// simplifications in function and loop assigns clause checking
14+
15+
#ifndef CPROVER_GOTO_INSTRUMENT_CONTRACTS_CFG_INFO_H
16+
#define CPROVER_GOTO_INSTRUMENT_CONTRACTS_CFG_INFO_H
17+
18+
#include <goto-programs/goto_convert_class.h>
19+
20+
#include <util/byte_operators.h>
21+
#include <util/expr_cast.h>
22+
#include <util/message.h>
23+
24+
#include <goto-programs/goto_model.h>
25+
26+
#include <analyses/dirty.h>
27+
#include <analyses/locals.h>
28+
#include <goto-instrument/havoc_utils.h>
29+
#include <goto-instrument/loop_utils.h>
30+
31+
#include <set>
32+
#include <vector>
33+
34+
/// Stores information about a goto function computed from its CFG.
35+
///
36+
/// The methods of this class provide information about identifiers
37+
/// to allow simplifying assigns clause checking assertions.
38+
class cfg_infot
39+
{
40+
public:
41+
/// Returns true iff `ident` is locally declared.
42+
virtual bool is_local(const irep_idt &ident) const = 0;
43+
44+
/// Returns true iff the given `ident` is either non-locally declared
45+
/// or is locally-declared but dirty.
46+
virtual bool is_not_local_or_dirty_local(const irep_idt &ident) const = 0;
47+
48+
/// Returns true iff `expr` is an access to a locally declared symbol
49+
/// and does not contain `dereference` or `address_of` operations.
50+
bool is_local_composite_access(const exprt &expr) const
51+
{
52+
// case-splitting on the lhs structure copied from symex_assignt::assign_rec
53+
if(expr.id() == ID_symbol)
54+
{
55+
return is_local(to_symbol_expr(expr).get_identifier());
56+
}
57+
else if(expr.id() == ID_index)
58+
{
59+
return is_local_composite_access(to_index_expr(expr).array());
60+
}
61+
else if(expr.id() == ID_member)
62+
{
63+
const typet &type = to_member_expr(expr).struct_op().type();
64+
if(
65+
type.id() == ID_struct || type.id() == ID_struct_tag ||
66+
type.id() == ID_union || type.id() == ID_union_tag)
67+
{
68+
return is_local_composite_access(to_member_expr(expr).compound());
69+
}
70+
else
71+
{
72+
throw unsupported_operation_exceptiont(
73+
"is_local_composite_access: unexpected assignment to member of '" +
74+
type.id_string() + "'");
75+
}
76+
}
77+
else if(expr.id() == ID_if)
78+
{
79+
return is_local_composite_access(to_if_expr(expr).true_case()) &&
80+
is_local_composite_access(to_if_expr(expr).false_case());
81+
}
82+
else if(expr.id() == ID_typecast)
83+
{
84+
return is_local_composite_access(to_typecast_expr(expr).op());
85+
}
86+
else if(
87+
expr.id() == ID_byte_extract_little_endian ||
88+
expr.id() == ID_byte_extract_big_endian)
89+
{
90+
return is_local_composite_access(to_byte_extract_expr(expr).op());
91+
}
92+
else if(expr.id() == ID_complex_real)
93+
{
94+
return is_local_composite_access(to_complex_real_expr(expr).op());
95+
}
96+
else if(expr.id() == ID_complex_imag)
97+
{
98+
return is_local_composite_access(to_complex_imag_expr(expr).op());
99+
}
100+
else
101+
{
102+
// matches ID_address_of, ID_dereference, etc.
103+
return false;
104+
}
105+
}
106+
};
107+
108+
// For goto_functions
109+
class function_cfg_infot : public cfg_infot
110+
{
111+
public:
112+
explicit function_cfg_infot(const goto_functiont &_goto_function)
113+
: dirty_analysis(_goto_function), locals(_goto_function)
114+
{
115+
parameters.insert(
116+
_goto_function.parameter_identifiers.begin(),
117+
_goto_function.parameter_identifiers.end());
118+
}
119+
120+
/// Returns true iff `ident` is a local or parameter of the goto_function.
121+
bool is_local(const irep_idt &ident) const override
122+
{
123+
return locals.is_local(ident) ||
124+
(parameters.find(ident) != parameters.end());
125+
}
126+
127+
/// Returns true iff the given `ident` is either not a goto_function local
128+
/// or is a local that is dirty.
129+
bool is_not_local_or_dirty_local(const irep_idt &ident) const override
130+
{
131+
if(is_local(ident))
132+
return dirty_analysis.get_dirty_ids().find(ident) !=
133+
dirty_analysis.get_dirty_ids().end();
134+
else
135+
return true;
136+
}
137+
138+
private:
139+
const dirtyt dirty_analysis;
140+
const localst locals;
141+
std::unordered_set<irep_idt> parameters;
142+
};
143+
144+
// For a loop in a goto_function
145+
class loop_cfg_infot : public cfg_infot
146+
{
147+
public:
148+
loop_cfg_infot(goto_functiont &_goto_function, const loopt &loop)
149+
: dirty_analysis(_goto_function)
150+
{
151+
for(const auto &t : loop)
152+
{
153+
if(t->is_decl())
154+
locals.insert(t->decl_symbol().get_identifier());
155+
}
156+
}
157+
158+
/// Returns true iff `ident` is a loop local.
159+
bool is_local(const irep_idt &ident) const override
160+
{
161+
return locals.find(ident) != locals.end();
162+
}
163+
164+
/// Returns true iff the given `ident` is either not a loop local
165+
/// or is a loop local that is dirty.
166+
bool is_not_local_or_dirty_local(const irep_idt &ident) const override
167+
{
168+
if(is_local(ident))
169+
return dirty_analysis.get_dirty_ids().find(ident) !=
170+
dirty_analysis.get_dirty_ids().end();
171+
else
172+
return true;
173+
}
174+
175+
void erase_locals(std::set<exprt> &exprs)
176+
{
177+
auto it = exprs.begin();
178+
while(it != exprs.end())
179+
{
180+
if(
181+
it->id() == ID_symbol && is_local(to_symbol_expr(*it).get_identifier()))
182+
{
183+
it = exprs.erase(it);
184+
}
185+
else
186+
{
187+
it++;
188+
}
189+
}
190+
}
191+
192+
private:
193+
const dirtyt dirty_analysis;
194+
std::unordered_set<irep_idt> locals;
195+
};
196+
197+
#endif

0 commit comments

Comments
 (0)