Skip to content

Commit 7163b6f

Browse files
SaswatPadhiArenBabikian
authored andcommitted
Fixed side-effect checking for invariant contracts
Moved side-effect checking on invariant contracts to goto-instrument. Since invariant contracts are expanded to multiple assertions (and assumptions) around the loop, it is cleaner to expand them only when they are enforced.
1 parent c6a8eef commit 7163b6f

File tree

5 files changed

+78
-30
lines changed

5 files changed

+78
-30
lines changed
Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,15 @@
1+
#include <assert.h>
2+
3+
int main()
4+
{
5+
unsigned N, *a = malloc(sizeof(unsigned int));
6+
7+
*a = 0;
8+
while(*a < N)
9+
__CPROVER_loop_invariant((0 <= *a) && (*a <= N))
10+
{
11+
++(*a);
12+
}
13+
14+
assert(*a == N);
15+
}
Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
CORE
2+
main.c
3+
--enforce-all-contracts
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^\[main.1\] .* Check loop invariant before entry: SUCCESS$
7+
^\[main.2\] .* Check that loop invariant is preserved: SUCCESS$
8+
^\[main.assertion.1\] .* assertion \*a == N: SUCCESS$
9+
^VERIFICATION SUCCESSFUL$
10+
--
11+
This test checks that C expressions are correctly converted to logic
12+
when enforcing loop invariant annotations.

src/goto-instrument/code_contracts.cpp

Lines changed: 43 additions & 23 deletions
Original file line numberDiff line numberDiff line change
@@ -17,6 +17,7 @@ Date: February 2016
1717

1818
#include <analyses/local_may_alias.h>
1919

20+
#include <goto-programs/goto_convert_class.h>
2021
#include <goto-programs/remove_skip.h>
2122

2223
#include <linking/static_lifetime_init.h>
@@ -74,9 +75,11 @@ exprt get_size(const typet &type, const namespacet &ns, messaget &log)
7475

7576
static void check_apply_invariants(
7677
goto_functionst::goto_functiont &goto_function,
78+
goto_convertt &converter,
7779
const local_may_aliast &local_may_alias,
7880
const goto_programt::targett loop_head,
79-
const loopt &loop)
81+
const loopt &loop,
82+
const irep_idt &mode)
8083
{
8184
PRECONDITION(!loop.empty());
8285

@@ -94,16 +97,18 @@ static void check_apply_invariants(
9497
if(invariant.is_nil())
9598
return;
9699

97-
// change H: loop; E: ...
100+
// change
101+
// H: loop;
102+
// E: ...
98103
// to
99-
// H: assert(invariant);
100-
// havoc;
101-
// assume(invariant);
102-
// if(guard) goto E:
103-
// loop;
104-
// assert(invariant);
105-
// assume(false);
106-
// E: ...
104+
// H: assert(invariant);
105+
// havoc;
106+
// assume(invariant);
107+
// if(guard) goto E:
108+
// loop;
109+
// assert(invariant);
110+
// assume(false);
111+
// E: ...
107112

108113
// find out what can get changed in the loop
109114
modifiest modifies;
@@ -114,17 +119,20 @@ static void check_apply_invariants(
114119

115120
// assert the invariant
116121
{
117-
goto_programt::targett a = havoc_code.add(
118-
goto_programt::make_assertion(invariant, loop_head->source_location));
119-
a->source_location.set_comment("Check loop invariant before entry");
122+
auto assertion = code_assertt(invariant);
123+
assertion.add_source_location().swap(loop_head->source_location);
124+
converter.goto_convert(assertion, havoc_code, mode);
125+
havoc_code.instructions.back().source_location.set_comment(
126+
"Check loop invariant before entry");
120127
}
121128

122129
// havoc variables being written to
123130
build_havoc_code(loop_head, modifies, havoc_code);
124131

125132
// assume the invariant
126-
havoc_code.add(
127-
goto_programt::make_assumption(invariant, loop_head->source_location));
133+
auto assumption = code_assumet(invariant);
134+
assumption.add_source_location().swap(loop_head->source_location);
135+
converter.goto_convert(assumption, havoc_code, mode);
128136

129137
// non-deterministically skip the loop if it is a do-while loop
130138
if(!loop_head->is_goto())
@@ -140,11 +148,14 @@ static void check_apply_invariants(
140148

141149
// assert the invariant at the end of the loop body
142150
{
143-
goto_programt::instructiont a =
144-
goto_programt::make_assertion(invariant, loop_end->source_location);
145-
a.source_location.set_comment("Check that loop invariant is preserved");
146-
goto_function.body.insert_before_swap(loop_end, a);
147-
++loop_end;
151+
auto assertion = code_assertt(invariant);
152+
assertion.add_source_location().swap(loop_end->source_location);
153+
converter.goto_convert(assertion, havoc_code, mode);
154+
havoc_code.instructions.back().source_location.set_comment(
155+
"Check that loop invariant is preserved");
156+
auto offset = havoc_code.instructions.size();
157+
goto_function.body.insert_before_swap(loop_end, havoc_code);
158+
std::advance(loop_end, offset);
148159
}
149160

150161
// change the back edge into assume(false) or assume(guard)
@@ -359,15 +370,24 @@ bool code_contractst::apply_function_contract(
359370
}
360371

361372
void code_contractst::apply_loop_contract(
373+
const irep_idt &function_name,
362374
goto_functionst::goto_functiont &goto_function)
363375
{
364376
local_may_aliast local_may_alias(goto_function);
365377
natural_loops_mutablet natural_loops(goto_function.body);
366378

379+
// setup goto_convertt to convert C expressions to logic
380+
goto_convertt converter(symbol_table, log.get_message_handler());
381+
367382
// iterate over the (natural) loops in the function
368383
for(const auto &loop : natural_loops.loop_map)
369384
check_apply_invariants(
370-
goto_function, local_may_alias, loop.first, loop.second);
385+
goto_function,
386+
converter,
387+
local_may_alias,
388+
loop.first,
389+
loop.second,
390+
symbol_table.lookup_ref(function_name).mode);
371391
}
372392

373393
const symbolt &code_contractst::new_tmp_symbol(
@@ -964,7 +984,7 @@ bool code_contractst::enforce_contracts()
964984
if(has_contract(goto_function.first))
965985
funs_to_enforce.insert(id2string(goto_function.first));
966986
else
967-
apply_loop_contract(goto_function.second);
987+
apply_loop_contract(goto_function.first, goto_function.second);
968988
}
969989
return enforce_contracts(funs_to_enforce);
970990
}
@@ -984,7 +1004,7 @@ bool code_contractst::enforce_contracts(
9841004
<< messaget::eom;
9851005
continue;
9861006
}
987-
apply_loop_contract(goto_function->second);
1007+
apply_loop_contract(goto_function->first, goto_function->second);
9881008

9891009
if(!has_contract(fun))
9901010
{

src/goto-instrument/code_contracts.h

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -155,6 +155,9 @@ class code_contractst
155155
std::vector<exprt> &aliasable_references);
156156

157157
void apply_loop_contract(goto_functionst::goto_functiont &goto_function);
158+
void apply_loop_contract(
159+
const irep_idt &function_name,
160+
goto_functionst::goto_functiont &goto_function);
158161

159162
/// \brief Does the named function have a contract?
160163
bool has_contract(const irep_idt);

src/goto-programs/goto_convert.cpp

Lines changed: 5 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -868,13 +868,11 @@ void goto_convertt::convert_loop_invariant(
868868
if(invariant.is_nil())
869869
return;
870870

871-
goto_programt no_sideeffects;
872-
clean_expr(invariant, no_sideeffects, mode);
873-
874-
INVARIANT_WITH_DIAGNOSTICS(
875-
no_sideeffects.instructions.empty(),
876-
"loop invariant is not side-effect free",
877-
code.find_source_location());
871+
// Loop contracts are expanded to assertions (and assumptions)
872+
// at multiple code points around a loop.
873+
// Rather than performing `clean_expr` during compilation,
874+
// we convert the invariant to logic at these various code points
875+
// only when they are enforced (using goto-instrument).
878876

879877
PRECONDITION(loop->is_goto());
880878
loop->guard.add(ID_C_spec_loop_invariant).swap(invariant);

0 commit comments

Comments
 (0)