Skip to content

Commit 0e367f8

Browse files
viktormalikviktormalik
authored
Merge pull request #146 from FrNecas/instrumentation
Enable and improve GOTO instrumentation
2 parents 3d71891 + 19f4ffb commit 0e367f8

29 files changed

+203
-71
lines changed

‎.gitignore

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -13,6 +13,7 @@ src/config.inc
1313
# regression/test files
1414
*.out
1515
tests.log
16+
instrumented.goto
1617

1718
# files stored by editors
1819
*~

‎regression/Makefile

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -8,7 +8,8 @@ DIRS = \
88
invariants \
99
heap \
1010
heap-data \
11-
memsafety
11+
memsafety \
12+
instrumentation
1213

1314
test:
1415
$(foreach var,$(DIRS), make -C $(var) test || exit 1;)

‎regression/instrumentation/Makefile

Lines changed: 21 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,21 @@
1+
default: tests.log
2+
3+
OUTPUT_GOTO = instrumented.goto
4+
FLAGS = --verbosity 10 --instrument-output $(OUTPUT_GOTO)
5+
6+
test:
7+
@../test.pl -p -c "../../../src/2ls/2ls $(FLAGS)"
8+
9+
tests.log: ../test.pl
10+
@../test.pl -p -c "../../../src/2ls/2ls $(FLAGS)"
11+
12+
show:
13+
@for dir in *; do \
14+
if [ -d "$$dir" ]; then \
15+
vim -o "$$dir/*.c" "$$dir/*.out"; \
16+
fi; \
17+
done;
18+
19+
clean:
20+
@rm -f *.log
21+
@for dir in *; do rm -f $$dir/*.out $$dir/$(OUTPUT_GOTO); done;

‎regression/instrumentation/intervals/main.c

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
void main()
2+
{
3+
int x = 0;
4+
5+
while(x<10)
6+
{
7+
++x;
8+
assert(x<=10);
9+
}
10+
11+
assert(x==10);
12+
}
13+

‎regression/instrumentation/intervals/test.desc

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE
2+
main.c
3+
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^VERIFICATION SUCCESSFUL$
7+
^\s*ASSUME x <= 10 // invariant generated by 2LS$
8+
^\s*ASSUME -\(\(signed __CPROVER_bitvector\[33\]\)x\) <= -1 // invariant generated by 2LS$

‎regression/instrumentation/octagons/main.c

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,16 @@
1+
#include <assert.h>
2+
3+
void main()
4+
{
5+
int x = 0;
6+
unsigned y = 0;
7+
8+
while(x<10 && y<20)
9+
{
10+
++x;
11+
++y;
12+
}
13+
14+
int z=x+y;
15+
assert(z<=20);
16+
}

‎regression/instrumentation/octagons/test.desc

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
CORE
2+
main.c
3+
--octagons
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^\*\* 0 of 1 failed$
7+
^\s*ASSUME \(signed __CPROVER_bitvector\[34\]\)-\(\(signed __CPROVER_bitvector\[33\]\)x\) - \(signed __CPROVER_bitvector\[34\]\)y <= -2 // invariant generated by 2LS$
8+
^\s*ASSUME \(signed __CPROVER_bitvector\[34\]\)x \+ \(signed __CPROVER_bitvector\[34\]\)y <= 20 // invariant generated by 2LS$
9+
^\s*ASSUME \(signed __CPROVER_bitvector\[34\]\)x - \(signed __CPROVER_bitvector\[34\]\)y <= 0 // invariant generated by 2LS$
10+
^\s*ASSUME \(signed __CPROVER_bitvector\[34\]\)y - \(signed __CPROVER_bitvector\[34\]\)x <= 0 // invariant generated by 2LS$
11+
^\s*ASSUME x <= 10 // invariant generated by 2LS$
12+
^\s*ASSUME -\(\(signed __CPROVER_bitvector\[33\]\)x\) <= -1 // invariant generated by 2LS$
13+
^\s*ASSUME y <= 10u // invariant generated by 2LS$
14+
^\s*ASSUME -\(\(signed __CPROVER_bitvector\[33\]\)y\) <= -1 // invariant generated by 2LS$

‎regression/instrumentation/pointers/main.c

Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,15 @@
1+
typedef struct data {
2+
struct data *next;
3+
int content;
4+
} Data;
5+
6+
void main() {
7+
Data x1 = {0,};
8+
Data x2 = {&x1,};
9+
Data x3 = {&x2,};
10+
Data *curr = &x3;
11+
while (curr) {
12+
assert(curr->content == 0);
13+
curr = curr->next;
14+
}
15+
}

‎regression/instrumentation/pointers/test.desc

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
CORE
2+
main.c
3+
--heap
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^VERIFICATION SUCCESSFUL$
7+
^\s*ASSUME curr == \(\(struct data \*\)NULL\) \|\| curr == &x1 \|\| curr == &x2 // invariant generated by 2LS$

‎regression/instrumentation/zones/main.c

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
void main()
2+
{
3+
int x=0, y=0;
4+
for(; x<100; x++)
5+
{
6+
for(y=0; y<=x; y++);
7+
}
8+
assert(x==100);
9+
assert(y==100);
10+
}

‎regression/instrumentation/zones/test.desc

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
CORE
2+
main.c
3+
--zones
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^VERIFICATION SUCCESSFUL$
7+
^\s*ASSUME y <= 100 // invariant generated by 2LS$
8+
^\s*ASSUME -\(\(signed __CPROVER_bitvector\[33\]\)y\) <= -1 // invariant generated by 2LS$
9+
^\s*ASSUME \(signed __CPROVER_bitvector\[33\]\)x - \(signed __CPROVER_bitvector\[33\]\)y <= 0 // invariant generated by 2LS$
10+
^\s*ASSUME \(signed __CPROVER_bitvector\[33\]\)y - \(signed __CPROVER_bitvector\[33\]\)x <= 99 // invariant generated by 2LS$
11+
^\s*ASSUME x <= 100 // invariant generated by 2LS$
12+
^\s*ASSUME -\(\(signed __CPROVER_bitvector\[33\]\)x\) <= -1 // invariant generated by 2LS$

‎src/2ls/2ls_parse_options.cpp

Lines changed: 11 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -232,12 +232,9 @@ void twols_parse_optionst::get_command_line_options(optionst &options)
232232
}
233233
}
234234

235-
// Heap domain requires full program inlining and usage of symbolic paths
235+
// Heap domain requires full program inlining
236236
if(cmdline.isset("heap"))
237-
{
238237
options.set_option("inline", true);
239-
options.set_option("sympath", true);
240-
}
241238

242239
// use incremental assertion checks
243240
if(cmdline.isset("non-incremental"))
@@ -401,6 +398,12 @@ int twols_parse_optionst::doit()
401398
if(get_goto_program(options, goto_model))
402399
return 6;
403400

401+
if(cmdline.isset("heap") && dynamic_memory_detected)
402+
{
403+
// Only use sympath domain if dynamic memory is used
404+
options.set_option("sympath", true);
405+
}
406+
404407
const namespacet ns(goto_model.symbol_table);
405408

406409
if(cmdline.isset("show-stats"))
@@ -691,7 +694,9 @@ int twols_parse_optionst::doit()
691694

692695
if(cmdline.isset("instrument-output"))
693696
{
694-
checker->instrument_and_output(goto_model);
697+
checker->instrument_and_output(
698+
goto_model,
699+
ui_message_handler.get_verbosity());
695700
}
696701

697702
return retval;
@@ -1561,6 +1566,7 @@ void twols_parse_optionst::help()
15611566
" --no-assumptions ignore user assumptions\n"
15621567
" --inline inline all functions into main\n"
15631568
" --inline-partial nr inline functions smaller than the given nr of instructions\n" // NOLINT(*)
1569+
" --instrument-output outfile instrument GOTO code with invariants and export it to outfile\n" // NOLINT(*)
15641570
"\n"
15651571
"Backend options:\n"
15661572
" --all-functions check each function as entry point\n"

‎src/2ls/2ls_parse_options.h

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -52,7 +52,7 @@ class optionst;
5252
"(enum-solver)(binsearch-solver)(arrays)"\
5353
"(string-abstraction)(no-arch)(arch):(floatbv)(fixedbv)" \
5454
"(round-to-nearest)(round-to-plus-inf)(round-to-minus-inf)(round-to-zero)" \
55-
"(inline)(inline-main)(inline-partial):" \
55+
"(inline)(inline-main)(inline-partial):(instrument-output):" \
5656
"(context-sensitive)(termination)(nontermination)" \
5757
"(lexicographic-ranking-function):(monolithic-ranking-function)" \
5858
"(max-inner-ranking-iterations):" \

‎src/2ls/horn_encoding.cpp

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -25,6 +25,7 @@ class horn_encodingt
2525
const optionst &_options,
2626
std::ostream &_out):
2727
goto_functions(_goto_model.goto_functions),
28+
symbol_table(_goto_model.symbol_table),
2829
ns(_goto_model.symbol_table),
2930
options(_options),
3031
out(_out),
@@ -36,6 +37,7 @@ class horn_encodingt
3637

3738
protected:
3839
const goto_functionst &goto_functions;
40+
const symbol_tablet &symbol_table;
3941
const namespacet ns;
4042
const optionst &options;
4143
std::ostream &out;
@@ -63,7 +65,7 @@ void horn_encodingt::translate(
6365
";\n";
6466

6567
// compute SSA
66-
local_SSAt local_SSA(f_it->second, ns, options, "");
68+
local_SSAt local_SSA(f_it->second, symbol_table, options, "");
6769

6870
const goto_programt &body=f_it->second.body;
6971

‎src/2ls/instrument_goto.cpp

Lines changed: 11 additions & 30 deletions
Original file line numberDiff line numberDiff line change
@@ -81,29 +81,17 @@ extern void purify_identifiers(exprt &expr);
8181

8282
void instrument_gotot::instrument_body(
8383
const local_SSAt &SSA,
84+
const symbol_exprt &guard,
8485
const exprt &expr,
8586
goto_functionst::goto_functiont &function)
8687
{
87-
// expected format (/\_j g_j)=> inv
88-
const exprt &impl=expr.op0();
89-
exprt inv=expr.op1(); // copy
90-
91-
std::cout << "Invariant " << from_expr(inv) << std::endl;
88+
// copy the invariant so that it isn't changed by purify_identifiers
89+
exprt inv=expr;
90+
std::cout << "Invariant " << from_expr(SSA.ns, "", inv) << std::endl;
9291

9392
purify_identifiers(inv);
9493

95-
local_SSAt::locationt loc;
96-
if(impl.id()==ID_symbol)
97-
{
98-
loc=find_loop_by_guard(SSA, to_symbol_expr(impl));
99-
}
100-
else if(impl.id()==ID_and)
101-
{
102-
assert(impl.op0().id()==ID_symbol);
103-
loc=find_loop_by_guard(SSA, to_symbol_expr(impl.op0()));
104-
}
105-
else
106-
assert(false);
94+
auto loc=find_loop_by_guard(SSA, guard);
10795

10896
Forall_goto_program_instructions(it, function.body)
10997
{
@@ -138,21 +126,14 @@ void instrument_gotot::instrument_function(
138126
if(summary.fw_invariant.is_true())
139127
return;
140128

141-
// expected format /\_i g_i=> inv_i
142-
if(summary.fw_invariant.id()==ID_implies)
129+
std::vector<domaint::guard_invariant> inv=
130+
summary.fw_domain_ptr->get_guards_and_invariants(*summary.fw_value_ptr);
131+
for(auto const &guard_invariant : inv)
143132
{
144-
instrument_body(SSA, summary.fw_invariant, function);
133+
const symbol_exprt &guard=to_symbol_expr(guard_invariant.first);
134+
exprt invariant=guard_invariant.second;
135+
instrument_body(SSA, guard, invariant, function);
145136
}
146-
else if(summary.fw_invariant.id()==ID_and)
147-
{
148-
for(unsigned i=0; i<summary.fw_invariant.operands().size(); i++)
149-
{
150-
assert(summary.fw_invariant.operands()[i].id()==ID_implies);
151-
instrument_body(SSA, summary.fw_invariant.operands()[i], function);
152-
}
153-
}
154-
else
155-
assert(false);
156137
}
157138

158139
void instrument_gotot::operator()(goto_modelt &goto_model)

‎src/2ls/instrument_goto.h

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -46,7 +46,8 @@ class instrument_gotot:public messaget
4646

4747
void instrument_body(
4848
const local_SSAt &SSA,
49-
const exprt &expr,
49+
const symbol_exprt &guard,
50+
const exprt &inv,
5051
goto_functionst::goto_functiont &function);
5152

5253
void instrument_instruction(

‎src/2ls/show.cpp

Lines changed: 5 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -169,16 +169,16 @@ void show_guards(
169169
void show_ssa(
170170
const goto_functionst::goto_functiont &goto_function,
171171
bool simplify,
172-
const namespacet &ns,
172+
const symbol_tablet &symbol_table,
173173
const optionst &options,
174174
std::ostream &out)
175175
{
176176
if(!goto_function.body_available())
177177
return;
178178

179-
unwindable_local_SSAt local_SSA(goto_function, ns, options);
179+
unwindable_local_SSAt local_SSA(goto_function, symbol_table, options);
180180
if(simplify)
181-
::simplify(local_SSA, ns);
181+
::simplify(local_SSA, local_SSA.ns);
182182
local_SSA.output_verbose(out);
183183
}
184184

@@ -190,8 +190,6 @@ void show_ssa(
190190
std::ostream &out,
191191
message_handlert &message_handler)
192192
{
193-
const namespacet ns(goto_model.symbol_table);
194-
195193
if(!function.empty())
196194
{
197195
out << ">>>> Function " << function << "\n";
@@ -200,7 +198,7 @@ void show_ssa(
200198
if(f_it==goto_model.goto_functions.function_map.end())
201199
out << "function " << function << " not found\n";
202200
else
203-
show_ssa(f_it->second, simplify, ns, options, out);
201+
show_ssa(f_it->second, simplify, goto_model.symbol_table, options, out);
204202
}
205203
else
206204
{
@@ -213,7 +211,7 @@ void show_ssa(
213211

214212
out << ">>>> Function " << f_it->first << "\n";
215213

216-
show_ssa(f_it->second, simplify, ns, options, out);
214+
show_ssa(f_it->second, simplify, goto_model.symbol_table, options, out);
217215

218216
out << "\n";
219217
}

‎src/2ls/summary_checker_ai.cpp

Lines changed: 1 addition & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -15,9 +15,7 @@ Author: Peter Schrammel
1515
property_checkert::resultt summary_checker_ait::operator()(
1616
const goto_modelt &goto_model)
1717
{
18-
const namespacet ns(goto_model.symbol_table);
19-
20-
SSA_functions(goto_model, ns);
18+
SSA_functions(goto_model, goto_model.symbol_table);
2119

2220
ssa_unwinder.init(false, false);
2321

‎src/2ls/summary_checker_base.cpp

Lines changed: 8 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -44,7 +44,7 @@ Author: Peter Schrammel
4444

4545
void summary_checker_baset::SSA_functions(
4646
const goto_modelt &goto_model,
47-
const namespacet &ns)
47+
const symbol_tablet &symbol_table)
4848
{
4949
// compute SSA for all the functions
5050
forall_goto_functions(f_it, goto_model.goto_functions)
@@ -55,14 +55,14 @@ void summary_checker_baset::SSA_functions(
5555
continue;
5656
status() << "Computing SSA of " << f_it->first << messaget::eom;
5757

58-
ssa_db.create(f_it->first, f_it->second, ns);
58+
ssa_db.create(f_it->first, f_it->second, symbol_table);
5959
local_SSAt &SSA=ssa_db.get(f_it->first);
6060

6161
// simplify, if requested
6262
if(simplify)
6363
{
6464
status() << "Simplifying" << messaget::eom;
65-
::simplify(SSA, ns);
65+
::simplify(SSA, SSA.ns);
6666
}
6767

6868
SSA.output(debug()); debug() << eom;
@@ -495,10 +495,14 @@ bool summary_checker_baset::is_spurious(
495495

496496
/// instruments the code with the inferred information and outputs it to a goto-
497497
/// binary
498-
void summary_checker_baset::instrument_and_output(goto_modelt &goto_model)
498+
void summary_checker_baset::instrument_and_output(
499+
goto_modelt &goto_model,
500+
unsigned verbosity)
499501
{
500502
instrument_gotot instrument_goto(options, ssa_db, summary_db);
501503
instrument_goto(goto_model);
504+
if(verbosity==10)
505+
goto_model.output(std::cout);
502506
std::string filename=options.get_option("instrument-output");
503507
status() << "Writing instrumented goto-binary " << filename << eom;
504508
write_goto_binary(

0 commit comments

Comments
 (0)