Skip to content

Commit d2beb39

Browse files
danpoedanpoe
committed
json log for unwinding
1 parent 580d54c commit d2beb39

File tree

7 files changed

+136
-18
lines changed

7 files changed

+136
-18
lines changed

‎regression/goto-instrument-unwind/Makefile

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -21,9 +21,10 @@ tests.log: ../test.pl
2121
clean:
2222
@for dir in *; do \
2323
if [ -d "$$dir" ]; then \
24-
rm $$dir/*.txt $$dir/*.dot $$dir/*.gb $$dir/*.out; \
24+
rm -f $$dir/*.txt $$dir/*.dot $$dir/*.gb $$dir/*.out; \
2525
fi; \
26-
done;
26+
done;
27+
rm -f tests.log
2728

2829
show:
2930
@for dir in *; do \

‎regression/goto-instrument-unwind/unwind-log1/main.c

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,6 @@
1+
2+
int main()
3+
{
4+
int i;
5+
for(i = 0; i < 10; i++) {}
6+
}

‎regression/goto-instrument-unwind/unwind-log1/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+
"--unwind 10 --unwinding-assertions --log -"
4+
^SIGNAL=0$
5+
^VERIFICATION SUCCESSFUL$
6+
--
7+
^warning: ignoring

‎src/goto-instrument/goto_instrument_parse_options.cpp

Lines changed: 22 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -191,6 +191,28 @@ int goto_instrument_parse_optionst::doit()
191191

192192
goto_functions.update();
193193
goto_functions.compute_loop_numbers();
194+
195+
if(cmdline.isset("log"))
196+
{
197+
std::string filename=cmdline.get_value("log");
198+
199+
bool have_file=!filename.empty() && filename!="-";
200+
201+
std::ofstream of;
202+
203+
if(have_file)
204+
{
205+
of.open(filename);
206+
if(!of)
207+
throw "failed to open file "+filename;
208+
goto_unwind.show_log_json(of);
209+
of.close();
210+
}
211+
else
212+
{
213+
goto_unwind.show_log_json(std::cout);
214+
}
215+
}
194216
}
195217
}
196218

‎src/goto-instrument/goto_instrument_parse_options.h

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -33,6 +33,7 @@ Author: Daniel Kroening, [email protected]
3333
"(minimum-interference)" \
3434
"(mm):(my-events)" \
3535
"(unwind):(unwindset):(unwinding-assertions)(partial-loops)(rest-loops)" \
36+
"(log):" \
3637
"(max-var):(max-po-trans):(ignore-arrays)" \
3738
"(cfg-kill)(no-dependencies)(force-loop-duplication)" \
3839
"(call-graph)" \

‎src/goto-instrument/unwind.cpp

Lines changed: 52 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -72,10 +72,10 @@ Function: copy_segment
7272
void goto_unwindt::copy_segment(
7373
const goto_programt::const_targett start,
7474
const goto_programt::const_targett end, // exclusive
75-
goto_programt &goto_program) const // result
75+
goto_programt &goto_program) // result
7676
{
7777
assert(start->location_number<end->location_number);
78-
assert(goto_program.instructions.empty());
78+
assert(goto_program.empty());
7979

8080
// build map for branch targets inside the loop
8181
typedef std::map<goto_programt::const_targett, unsigned> target_mapt;
@@ -95,6 +95,7 @@ void goto_unwindt::copy_segment(
9595
{
9696
goto_programt::targett t_new=goto_program.add_instruction();
9797
*t_new=*t;
98+
unwind_log.insert(t_new, t->location_number);
9899
target_vector.push_back(t_new); // store copied instruction
99100
}
100101

@@ -139,7 +140,7 @@ void goto_unwindt::unwind(
139140
const goto_programt::const_targett loop_head,
140141
const goto_programt::const_targett loop_exit,
141142
const unsigned k,
142-
const unwind_strategyt unwind_strategy) const
143+
const unwind_strategyt unwind_strategy)
143144
{
144145
std::vector<goto_programt::targett> iteration_points;
145146
unwind(goto_program, loop_head, loop_exit, k, unwind_strategy,
@@ -164,7 +165,7 @@ void goto_unwindt::unwind(
164165
const goto_programt::const_targett loop_exit,
165166
const unsigned k,
166167
const unwind_strategyt unwind_strategy,
167-
std::vector<goto_programt::targett> &iteration_points) const
168+
std::vector<goto_programt::targett> &iteration_points)
168169
{
169170
assert(iteration_points.empty());
170171
assert(loop_head->location_number<loop_exit->location_number);
@@ -178,6 +179,7 @@ void goto_unwindt::unwind(
178179
t->make_skip();
179180
t->source_location=loop_head->source_location;
180181
t->function=loop_head->function;
182+
unwind_log.insert(t, loop_head->location_number);
181183
}
182184
else if(unwind_strategy==REST)
183185
{
@@ -214,9 +216,10 @@ void goto_unwindt::unwind(
214216

215217
new_t->source_location=loop_head->source_location;
216218
new_t->function=loop_head->function;
219+
unwind_log.insert(new_t, loop_head->location_number);
217220
}
218221

219-
assert(!rest_program.instructions.empty());
222+
assert(!rest_program.empty());
220223

221224
// to be filled with copies of the loop body
222225
goto_programt copies;
@@ -233,6 +236,7 @@ void goto_unwindt::unwind(
233236
if(!t_before->is_goto() || !t_before->guard.is_true())
234237
{
235238
goto_programt::targett t_goto=goto_program.insert_before(loop_exit);
239+
unwind_log.insert(t_goto, loop_exit->location_number);
236240

237241
t_goto->make_goto(get_mutable(goto_program, loop_exit));
238242
t_goto->source_location=loop_exit->source_location;
@@ -243,6 +247,8 @@ void goto_unwindt::unwind(
243247
// add a skip before the loop exit
244248

245249
goto_programt::targett t_skip=goto_program.insert_before(loop_exit);
250+
unwind_log.insert(t_skip, loop_exit->location_number);
251+
246252
t_skip->make_skip();
247253
t_skip->source_location=loop_head->source_location;
248254
t_skip->function=loop_head->function;
@@ -282,6 +288,8 @@ void goto_unwindt::unwind(
282288
// insert skip for loop body
283289

284290
goto_programt::targett t_skip=goto_program.insert_before(loop_head);
291+
unwind_log.insert(t_skip, loop_head->location_number);
292+
285293
t_skip->make_skip();
286294
t_skip->source_location=loop_head->source_location;
287295
t_skip->function=loop_head->function;
@@ -310,9 +318,6 @@ void goto_unwindt::unwind(
310318

311319
// now insert copies before loop_exit
312320
goto_program.destructive_insert(loop_exit, copies);
313-
314-
// update it all (except loop numbers)
315-
goto_program.update();
316321
}
317322

318323
/*******************************************************************\
@@ -366,7 +371,7 @@ void goto_unwindt::unwind(
366371
goto_programt &goto_program,
367372
const unwind_sett &unwind_set,
368373
const int k,
369-
const unwind_strategyt unwind_strategy) const
374+
const unwind_strategyt unwind_strategy)
370375
{
371376
assert(k>=-1);
372377

@@ -415,7 +420,7 @@ void goto_unwindt::operator()(
415420
goto_functionst &goto_functions,
416421
const unwind_sett &unwind_set,
417422
const int k,
418-
const unwind_strategyt unwind_strategy) const
423+
const unwind_strategyt unwind_strategy)
419424
{
420425
assert(k>=-1);
421426

@@ -434,3 +439,40 @@ void goto_unwindt::operator()(
434439
goto_program.compute_loop_numbers();
435440
}
436441
}
442+
443+
/*******************************************************************\
444+
445+
Function: show_log_json
446+
447+
Inputs:
448+
449+
Outputs:
450+
451+
Purpose:
452+
453+
\*******************************************************************/
454+
455+
// call after calling goto_functions.update()!
456+
void goto_unwindt::unwind_logt::show_log_json(std::ostream &out) const
457+
{
458+
json_objectt json_result;
459+
json_arrayt &json_unwound=json_result["unwound"].make_array();
460+
461+
for(location_mapt::const_iterator it=location_map.begin();
462+
it!=location_map.end(); it++)
463+
{
464+
json_objectt &object=json_unwound.push_back().make_object();
465+
466+
goto_programt::const_targett target=it->first;
467+
unsigned location_number=it->second;
468+
469+
470+
object["original_location_number"]=json_numbert(i2string(
471+
location_number));
472+
object["new_location_number"]=json_numbert(i2string(
473+
target->location_number));
474+
}
475+
476+
out << json_result;
477+
out << "\n";
478+
}

‎src/goto-instrument/unwind.h

Lines changed: 45 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -10,6 +10,9 @@ Author: Daniel Kroening, [email protected]
1010
#ifndef CPROVER_UNWIND_H
1111
#define CPROVER_UNWIND_H
1212

13+
#include <util/i2string.h>
14+
#include <util/json.h>
15+
#include <util/json_expr.h>
1316
#include <goto-programs/goto_program.h>
1417

1518
// -1: do not unwind loop
@@ -29,30 +32,30 @@ class goto_unwindt
2932
const goto_programt::const_targett loop_head,
3033
const goto_programt::const_targett loop_exit,
3134
const unsigned k, // bound for given loop
32-
const unwind_strategyt unwind_strategy) const;
35+
const unwind_strategyt unwind_strategy);
3336

3437
void unwind(
3538
goto_programt &goto_program,
3639
const goto_programt::const_targett loop_head,
3740
const goto_programt::const_targett loop_exit,
3841
const unsigned k, // bound for given loop
3942
const unwind_strategyt unwind_strategy,
40-
std::vector<goto_programt::targett> &iteration_points) const;
43+
std::vector<goto_programt::targett> &iteration_points);
4144

4245
// unwind function
4346

4447
void unwind(
4548
goto_programt &goto_program,
4649
const unwind_sett &unwind_set,
4750
const int k=-1, // -1: no global bound
48-
const unwind_strategyt unwind_strategy=PARTIAL) const;
51+
const unwind_strategyt unwind_strategy=PARTIAL);
4952

5053
// unwind all functions
5154

5255
void operator()(
5356
goto_functionst &goto_functions,
5457
const unsigned k, // global bound
55-
const unwind_strategyt unwind_strategy=PARTIAL) const
58+
const unwind_strategyt unwind_strategy=PARTIAL)
5659
{
5760
const unwind_sett unwind_set;
5861
operator()(goto_functions, unwind_set, (int)k, unwind_strategy);
@@ -62,9 +65,45 @@ class goto_unwindt
6265
goto_functionst &goto_functions,
6366
const unwind_sett &unwind_set,
6467
const int k=-1, // -1: no global bound
65-
const unwind_strategyt unwind_strategy=PARTIAL) const;
68+
const unwind_strategyt unwind_strategy=PARTIAL);
69+
70+
// unwind log
71+
72+
void show_log_json(std::ostream &out) const
73+
{
74+
unwind_log.show_log_json(out);
75+
}
76+
77+
// log for each copied instruction the location number of the
78+
// original instruction it came from; new instructions are
79+
// associated with the location of the backedge
80+
struct unwind_logt
81+
{
82+
// call after calling goto_functions.update()!
83+
void show_log_json(std::ostream &out) const;
84+
85+
// remove entries that refer to the given goto program
86+
void cleanup(const goto_programt &goto_program)
87+
{
88+
forall_goto_program_instructions(it, goto_program)
89+
location_map.erase(it);
90+
}
91+
92+
void insert(
93+
const goto_programt::const_targett target,
94+
const unsigned location_number)
95+
{
96+
assert(location_map.find(target)==location_map.end());
97+
location_map[target]=location_number;
98+
}
99+
100+
typedef std::map<goto_programt::const_targett, unsigned> location_mapt;
101+
location_mapt location_map;
102+
};
66103

67104
protected:
105+
unwind_logt unwind_log;
106+
68107
int get_k(
69108
const irep_idt func,
70109
const unsigned loop_id,
@@ -75,7 +114,7 @@ class goto_unwindt
75114
void copy_segment(
76115
const goto_programt::const_targett start,
77116
const goto_programt::const_targett end, // exclusive
78-
goto_programt &goto_program) const; // result
117+
goto_programt &goto_program); // result
79118

80119
goto_programt::targett get_mutable(
81120
goto_programt &goto_program,

0 commit comments

Comments
 (0)