Skip to content

Commit 529d7a5

Browse files
martinmartin
authored andcommitted
Thread a single history through all initialisation and fixedpoints
This is needed to support histories that carry information across function calls. It requires some changes to the internal API in ai_baset but should not give any changes to the results computed.
1 parent b472724 commit 529d7a5

File tree

2 files changed

+43
-31
lines changed

2 files changed

+43
-31
lines changed

src/analyses/ai.cpp

Lines changed: 26 additions & 18 deletions
Original file line numberDiff line numberDiff line change
@@ -157,22 +157,27 @@ xmlt ai_baset::output_xml(
157157
return function_body;
158158
}
159159

160-
void ai_baset::entry_state(const goto_functionst &goto_functions)
160+
ai_baset::trace_ptrt
161+
ai_baset::entry_state(const goto_functionst &goto_functions)
161162
{
162163
// find the 'entry function'
163164

164165
goto_functionst::function_mapt::const_iterator
165166
f_it=goto_functions.function_map.find(goto_functions.entry_point());
166167

167168
if(f_it!=goto_functions.function_map.end())
168-
entry_state(f_it->second.body);
169+
return entry_state(f_it->second.body);
170+
171+
// It is not clear if this is even a well-structured goto_functionst object
172+
return nullptr;
169173
}
170174

171-
void ai_baset::entry_state(const goto_programt &goto_program)
175+
ai_baset::trace_ptrt ai_baset::entry_state(const goto_programt &goto_program)
172176
{
173177
// The first instruction of 'goto_program' is the entry point
174178
trace_ptrt p = history_factory->epoch(goto_program.instructions.begin());
175179
get_state(p).make_entry();
180+
return p;
176181
}
177182

178183
void ai_baset::initialize(
@@ -218,19 +223,16 @@ ai_baset::trace_ptrt ai_baset::get_next(working_sett &working_set)
218223
}
219224

220225
bool ai_baset::fixedpoint(
226+
trace_ptrt start_trace,
221227
const irep_idt &function_id,
222228
const goto_programt &goto_program,
223229
const goto_functionst &goto_functions,
224230
const namespacet &ns)
225231
{
226-
working_sett working_set;
232+
PRECONDITION(start_trace != nullptr);
227233

228-
// Put the first location in the working set
229-
if(!goto_program.empty())
230-
{
231-
put_in_working_set(
232-
working_set, history_factory->bang(goto_program.instructions.begin()));
233-
}
234+
working_sett working_set;
235+
put_in_working_set(working_set, start_trace);
234236

235237
bool new_data=false;
236238

@@ -247,14 +249,15 @@ bool ai_baset::fixedpoint(
247249
}
248250

249251
void ai_baset::fixedpoint(
252+
trace_ptrt start_trace,
250253
const goto_functionst &goto_functions,
251254
const namespacet &ns)
252255
{
253-
goto_functionst::function_mapt::const_iterator
254-
f_it=goto_functions.function_map.find(goto_functions.entry_point());
256+
goto_functionst::function_mapt::const_iterator f_it =
257+
goto_functions.function_map.find(goto_functions.entry_point());
255258

256-
if(f_it!=goto_functions.function_map.end())
257-
fixedpoint(f_it->first, f_it->second.body, goto_functions, ns);
259+
if(f_it != goto_functions.function_map.end())
260+
fixedpoint(start_trace, f_it->first, f_it->second.body, goto_functions, ns);
258261
}
259262

260263
bool ai_baset::visit(
@@ -469,7 +472,7 @@ bool ai_recursive_interproceduralt::visit_edge_function_call(
469472
{
470473
locationt l_begin = callee.instructions.begin();
471474

472-
working_sett ignore_working_set; // Redundant; fixpoint will add l_begin
475+
working_sett catch_working_set; // The trace from the next fixpoint
473476

474477
// Do the edge from the call site to the beginning of the function
475478
bool new_data = visit_edge(
@@ -478,11 +481,16 @@ bool ai_recursive_interproceduralt::visit_edge_function_call(
478481
callee_function_id,
479482
l_begin,
480483
ns,
481-
ignore_working_set);
484+
catch_working_set);
482485

483486
// do we need to do/re-do the fixedpoint of the body?
484487
if(new_data)
485-
fixedpoint(callee_function_id, callee, goto_functions, ns);
488+
fixedpoint(
489+
get_next(catch_working_set),
490+
callee_function_id,
491+
callee,
492+
goto_functions,
493+
ns);
486494
}
487495

488496
// This is the edge from function end to return site.
@@ -493,7 +501,7 @@ bool ai_recursive_interproceduralt::visit_edge_function_call(
493501
l_end->is_end_function(),
494502
"The last instruction of a goto_program must be END_FUNCTION");
495503

496-
// Construct a history from a location
504+
// Find the histories for a location
497505
auto traces = storage->abstract_traces_before(l_end);
498506

499507
bool new_data = false;

src/analyses/ai.h

Lines changed: 17 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -147,8 +147,8 @@ class ai_baset
147147
{
148148
goto_functionst goto_functions;
149149
initialize(function_id, goto_program);
150-
entry_state(goto_program);
151-
fixedpoint(function_id, goto_program, goto_functions, ns);
150+
trace_ptrt p = entry_state(goto_program);
151+
fixedpoint(p, function_id, goto_program, goto_functions, ns);
152152
finalize();
153153
}
154154

@@ -158,8 +158,8 @@ class ai_baset
158158
const namespacet &ns)
159159
{
160160
initialize(goto_functions);
161-
entry_state(goto_functions);
162-
fixedpoint(goto_functions, ns);
161+
trace_ptrt p = entry_state(goto_functions);
162+
fixedpoint(p, goto_functions, ns);
163163
finalize();
164164
}
165165

@@ -168,8 +168,8 @@ class ai_baset
168168
{
169169
const namespacet ns(goto_model.get_symbol_table());
170170
initialize(goto_model.get_goto_functions());
171-
entry_state(goto_model.get_goto_functions());
172-
fixedpoint(goto_model.get_goto_functions(), ns);
171+
trace_ptrt p = entry_state(goto_model.get_goto_functions());
172+
fixedpoint(p, goto_model.get_goto_functions(), ns);
173173
finalize();
174174
}
175175

@@ -181,8 +181,8 @@ class ai_baset
181181
{
182182
goto_functionst goto_functions;
183183
initialize(function_id, goto_function);
184-
entry_state(goto_function.body);
185-
fixedpoint(function_id, goto_function.body, goto_functions, ns);
184+
trace_ptrt p = entry_state(goto_function.body);
185+
fixedpoint(p, function_id, goto_function.body, goto_functions, ns);
186186
finalize();
187187
}
188188

@@ -378,11 +378,11 @@ class ai_baset
378378

379379
/// Set the abstract state of the entry location of a single function to the
380380
/// entry state required by the analysis
381-
void entry_state(const goto_programt &goto_program);
381+
trace_ptrt entry_state(const goto_programt &goto_program);
382382

383383
/// Set the abstract state of the entry location of a whole program to the
384384
/// entry state required by the analysis
385-
void entry_state(const goto_functionst &goto_functions);
385+
trace_ptrt entry_state(const goto_functionst &goto_functions);
386386

387387
/// Output the abstract states for a single function as JSON
388388
/// \param ns: The namespace
@@ -420,13 +420,16 @@ class ai_baset
420420
/// Run the fixedpoint algorithm until it reaches a fixed point
421421
/// \return True if we found something new
422422
virtual bool fixedpoint(
423+
trace_ptrt starting_trace,
423424
const irep_idt &function_id,
424425
const goto_programt &goto_program,
425426
const goto_functionst &goto_functions,
426427
const namespacet &ns);
427428

428-
virtual void
429-
fixedpoint(const goto_functionst &goto_functions, const namespacet &ns);
429+
virtual void fixedpoint(
430+
trace_ptrt starting_trace,
431+
const goto_functionst &goto_functions,
432+
const namespacet &ns);
430433

431434
/// Perform one step of abstract interpretation from trace t
432435
/// Depending on the instruction type it may compute a number of "edges"
@@ -660,10 +663,11 @@ class concurrency_aware_ait:public ait<domainT>
660663
using working_sett = ai_baset::working_sett;
661664

662665
void fixedpoint(
666+
ai_baset::trace_ptrt start_trace,
663667
const goto_functionst &goto_functions,
664668
const namespacet &ns) override
665669
{
666-
ai_baset::fixedpoint(goto_functions, ns);
670+
ai_baset::fixedpoint(start_trace, goto_functions, ns);
667671

668672
is_threadedt is_threaded(goto_functions);
669673

0 commit comments

Comments
 (0)