Skip to content

Commit 8d491f3

Browse files
qinhepingqinheping
committed
Update CLI for applyin loop contracts with dfcc
1 parent 2aec6a9 commit 8d491f3

File tree

14 files changed

+197
-54
lines changed

14 files changed

+197
-54
lines changed

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

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+
}

‎regression/contracts-dfcc/detect_loop_locals/test.desc

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
CORE
2+
main.c
3+
--dfcc main --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.

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

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+
}

‎regression/contracts-dfcc/detect_loop_locals2/test.desc

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
CORE
2+
main.c
3+
--dfcc main --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-dfcc/invar_assigns_opt/test.desc

Lines changed: 11 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -1,18 +1,18 @@
11
CORE
22
main.c
3-
--dfcc main
3+
--dfcc main --apply-loop-contracts
44
^EXIT=0$
55
^SIGNAL=0$
6-
^\[main.\d+\] .* Check loop invariant before entry: SUCCESS$
7-
^\[main.\d+\] .* Check that loop invariant is preserved: SUCCESS$
8-
^\[main.\d+\] .* Check decreases clause on loop iteration: SUCCESS$
9-
^\[main.assertion.\d+\] .* assertion r1 == 0: SUCCESS$
10-
^\[main.\d+\] .* Check loop invariant before entry: SUCCESS$
11-
^\[main.assigns.\d+\] .* Check that s2 is assignable: SUCCESS$
12-
^\[main.assigns.\d+\] .* Check that r2 is assignable: SUCCESS$
13-
^\[main.\d+\] .* Check that loop invariant is preserved: SUCCESS$
14-
^\[main.\d+\] .* Check decreases clause on loop iteration: SUCCESS$
15-
^\[main.assertion.\d+\] .* assertion r2 == 0: SUCCESS$
6+
^\[foo.\d+\] .* Check loop invariant before entry: SUCCESS$
7+
^\[foo.\d+\] .* Check that loop invariant is preserved: SUCCESS$
8+
^\[foo.\d+\] .* Check decreases clause on loop iteration: SUCCESS$
9+
^\[foo.assertion.\d+\] .* assertion r1 == 0: SUCCESS$
10+
^\[foo.\d+\] .* Check loop invariant before entry: SUCCESS$
11+
^\[foo.assigns.\d+\] .* Check that s2 is assignable: SUCCESS$
12+
^\[foo.assigns.\d+\] .* Check that r2 is assignable: SUCCESS$
13+
^\[foo.\d+\] .* Check that loop invariant is preserved: SUCCESS$
14+
^\[foo.\d+\] .* Check decreases clause on loop iteration: SUCCESS$
15+
^\[foo.assertion.\d+\] .* assertion r2 == 0: SUCCESS$
1616
^VERIFICATION SUCCESSFUL$
1717
--
1818
--

‎regression/contracts-dfcc/loop_assigns-01/test.desc

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -1,13 +1,13 @@
11
CORE
22
main.c
3-
--dfcc main
3+
--dfcc main --apply-loop-contracts
44
^EXIT=10$
55
^SIGNAL=0$
6-
^\[main.\d+\] .* Check loop invariant before entry: SUCCESS$
7-
^\[main.assigns.\d+\] .* Check that i is assignable: SUCCESS$
8-
^\[main.assigns.\d+\] .* Check that b->data\[(.*)i\] is assignable: SUCCESS$
9-
^\[main.\d+\] .* Check that loop invariant is preserved: SUCCESS$
10-
^\[main.assertion.\d+\] .* assertion b->data\[5\] == 0: FAILURE$
6+
^\[foo.\d+\] .* Check loop invariant before entry: SUCCESS$
7+
^\[foo.assigns.\d+\] .* Check that i is assignable: SUCCESS$
8+
^\[foo.assigns.\d+\] .* Check that b->data\[(.*)i\] is assignable: SUCCESS$
9+
^\[foo.\d+\] .* Check that loop invariant is preserved: SUCCESS$
10+
^\[foo.assertion.\d+\] .* assertion b->data\[5\] == 0: FAILURE$
1111
^VERIFICATION FAILED$
1212
--
1313
--

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

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -1,14 +1,14 @@
11
CORE
22
main.c
3-
--dfcc main
3+
--dfcc main --apply-loop-contracts
44
^EXIT=0$
55
^SIGNAL=0$
6-
^\[main.\d+\] .* Check loop invariant before entry: SUCCESS$
7-
^\[main.\d+\] .* Check that loop invariant is preserved: SUCCESS$
8-
^\[main.assigns.\d+\] .* Check that i is assignable: SUCCESS$
9-
^\[main.assigns.\d+\] .* Check that b\[(.*)i\] is assignable: SUCCESS$
6+
^\[foo.\d+\] .* Check loop invariant before entry: SUCCESS$
7+
^\[foo.\d+\] .* Check that loop invariant is preserved: SUCCESS$
8+
^\[foo.assigns.\d+\] .* Check that i is assignable: SUCCESS$
9+
^\[foo.assigns.\d+\] .* Check that b\[(.*)i\] is assignable: SUCCESS$
1010
^VERIFICATION SUCCESSFUL$
1111
--
1212
--
13-
This test checks assigns clauses (i, __CPROVER_POINTER_OBJECT(b)) is inferred,
13+
This test checks assigns clauses (i, __CPROVER_object_whole(b)) is inferred,
1414
and widened correctly.

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

Lines changed: 13 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -121,6 +121,7 @@ void dfcc(
121121
const bool allow_recursive_calls,
122122
const std::set<irep_idt> &to_replace,
123123
const bool apply_loop_contracts,
124+
const bool unwind_transformed_loops,
124125
const std::set<std::string> &to_exclude_from_nondet_static,
125126
message_handlert &message_handler)
126127
{
@@ -137,6 +138,7 @@ void dfcc(
137138
allow_recursive_calls,
138139
to_replace_map,
139140
apply_loop_contracts,
141+
unwind_transformed_loops,
140142
to_exclude_from_nondet_static,
141143
message_handler);
142144
}
@@ -149,6 +151,7 @@ void dfcc(
149151
const bool allow_recursive_calls,
150152
const std::map<irep_idt, irep_idt> &to_replace,
151153
const bool apply_loop_contracts,
154+
const bool unwind_transformed_loops,
152155
const std::set<std::string> &to_exclude_from_nondet_static,
153156
message_handlert &message_handler)
154157
{
@@ -160,6 +163,7 @@ void dfcc(
160163
allow_recursive_calls,
161164
to_replace,
162165
apply_loop_contracts,
166+
unwind_transformed_loops,
163167
message_handler,
164168
to_exclude_from_nondet_static};
165169
}
@@ -172,6 +176,7 @@ dfcct::dfcct(
172176
const bool allow_recursive_calls,
173177
const std::map<irep_idt, irep_idt> &to_replace,
174178
const bool apply_loop_contracts,
179+
const bool unwind_transformed_loops,
175180
message_handlert &message_handler,
176181
const std::set<std::string> &to_exclude_from_nondet_static)
177182
: options(options),
@@ -213,9 +218,16 @@ dfcct::dfcct(
213218
library,
214219
spec_functions,
215220
contract_clauses_codegen),
216-
instrument(goto_model, message_handler, utils, loop_instrument, library),
221+
instrument(
222+
goto_model,
223+
message_handler,
224+
utils,
225+
loop_instrument,
226+
apply_loop_contracts,
227+
library),
217228
max_assigns_clause_size(0)
218229
{
230+
instrument.unwind_transformed_loops = unwind_transformed_loops;
219231
transform_goto_model();
220232
}
221233

‎src/goto-instrument/contracts/dynamic-frames/dfcc.h

Lines changed: 12 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -100,6 +100,8 @@ class invalid_function_contract_pair_exceptiont : public cprover_exception_baset
100100
/// \param allow_recursive_calls Allow the checked function to be recursive
101101
/// \param to_replace set of functions to replace with their contract
102102
/// \param apply_loop_contracts apply loop contract transformations iff true
103+
/// \param unwind_transformed_loops unwind transformed loops after applying loop
104+
/// contracts.
103105
/// \param to_exclude_from_nondet_static set of symbols to exclude when havocing
104106
/// static program symbols.
105107
/// \param message_handler used for debug/warning/error messages
@@ -111,6 +113,7 @@ void dfcc(
111113
const bool allow_recursive_calls,
112114
const std::set<irep_idt> &to_replace,
113115
const bool apply_loop_contracts,
116+
const bool unwind_transformed_loops,
114117
const std::set<std::string> &to_exclude_from_nondet_static,
115118
message_handlert &message_handler);
116119

@@ -129,7 +132,9 @@ void dfcc(
129132
/// \param to_check (function,contract) pair for contract checking
130133
/// \param allow_recursive_calls Allow the checked function to be recursive
131134
/// \param to_replace Functions-to-contract mapping for replacement
132-
/// \param apply_loop_contracts Spply loop contract transformations iff true
135+
/// \param apply_loop_contracts Apply loop contract transformations iff true
136+
/// \param unwind_transformed_loops unwind transformed loops after applying loop
137+
/// contracts.
133138
/// \param to_exclude_from_nondet_static Set of symbols to exclude when havocing
134139
/// static program symbols.
135140
/// \param message_handler used for debug/warning/error messages
@@ -141,6 +146,7 @@ void dfcc(
141146
const bool allow_recursive_calls,
142147
const std::map<irep_idt, irep_idt> &to_replace,
143148
const bool apply_loop_contracts,
149+
const bool unwind_transformed_loops,
144150
const std::set<std::string> &to_exclude_from_nondet_static,
145151
message_handlert &message_handler);
146152

@@ -159,6 +165,8 @@ class dfcct
159165
/// \param to_replace functions-to-contract mapping for replacement
160166
/// \param apply_loop_contracts apply loop contract transformations iff true
161167
/// havocing static program symbols.
168+
/// \param unwind_transformed_loops unwind transformed loops after applying loop
169+
/// contracts.
162170
/// \param message_handler used for debug/warning/error messages
163171
/// \param to_exclude_from_nondet_static set of symbols to exclude when
164172
dfcct(
@@ -169,6 +177,7 @@ class dfcct
169177
const bool allow_recursive_calls,
170178
const std::map<irep_idt, irep_idt> &to_replace,
171179
const bool apply_loop_contracts,
180+
const bool unwind_transformed_loops,
172181
message_handlert &message_handler,
173182
const std::set<std::string> &to_exclude_from_nondet_static);
174183

@@ -194,7 +203,7 @@ class dfcct
194203
/// (replacement mode)
195204
/// - instrument all remaining functions GOTO model
196205
/// - (this includes standard library functions).
197-
/// - specialise the instrumentation functions by unwiding loops they contain
206+
/// - specialise the instrumentation functions by unwinding loops they contain
198207
/// to the maximum size of any assigns clause involved in the model.
199208
void transform_goto_model();
200209

@@ -278,7 +287,7 @@ class dfcct
278287
/// for each instrumented function
279288
///
280289
/// A call to `nondet_static` will re-generate the initialize function with
281-
/// nondet values. The intrumentation statics will not get nondet initialised
290+
/// nondet values. The instrumentation statics will not get nondet initialised
282291
/// by virtue of being tagged with ID_C_no_nondet_initialization.
283292
///
284293
/// However, nondet_static expects instructions to be either function calls

0 commit comments

Comments
 (0)