Skip to content

Commit 1a98e8b

Browse files
author
martin
committed
Add a caller_history argument to ai_historyt::step()
This is similar to a three-way merge in that it allows histories to not only use their state and histories in the next location but also to access the history at the call site. Doing so makes it possible to create "function local" history where all call-sites merge and drop their previous history but it is picked back up on function return. This is needed for managing scalability in some of the more involved histories.
1 parent 7d30335 commit 1a98e8b

File tree

6 files changed

+66
-9
lines changed

6 files changed

+66
-9
lines changed

src/analyses/ai.cpp

Lines changed: 17 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -303,8 +303,14 @@ bool ai_baset::visit(
303303
if(to_l == goto_program.instructions.end())
304304
continue;
305305

306-
new_data |=
307-
visit_edge(function_id, p, function_id, to_l, ns, working_set);
306+
new_data |= visit_edge(
307+
function_id,
308+
p,
309+
function_id,
310+
to_l,
311+
ai_history_baset::no_caller_history,
312+
ns,
313+
working_set); // Local steps so no caller history needed
308314
}
309315
}
310316

@@ -316,11 +322,13 @@ bool ai_baset::visit_edge(
316322
trace_ptrt p,
317323
const irep_idt &to_function_id,
318324
locationt to_l,
325+
trace_ptrt caller_history,
319326
const namespacet &ns,
320327
working_sett &working_set)
321328
{
322329
// Has history taught us not to step here...
323-
auto next = p->step(to_l, *(storage->abstract_traces_before(to_l)));
330+
auto next =
331+
p->step(to_l, *(storage->abstract_traces_before(to_l)), caller_history);
324332
if(next.first == ai_history_baset::step_statust::BLOCKED)
325333
return false;
326334
trace_ptrt to_p = next.second;
@@ -366,6 +374,8 @@ bool ai_baset::visit_edge_function_call(
366374
p_call,
367375
calling_function_id,
368376
l_return,
377+
ai_history_baset::
378+
no_caller_history, // Not needed as we are skipping the function call
369379
ns,
370380
working_set);
371381
}
@@ -439,6 +449,7 @@ bool ai_baset::visit_function_call(
439449
p_call,
440450
calling_function_id,
441451
l_return,
452+
ai_history_baset::no_caller_history, // Would be the same as p_call...
442453
ns,
443454
working_set);
444455
}
@@ -480,6 +491,8 @@ bool ai_recursive_interproceduralt::visit_edge_function_call(
480491
p_call,
481492
callee_function_id,
482493
l_begin,
494+
ai_history_baset::
495+
no_caller_history, // Not needed as p_call already has the info
483496
ns,
484497
catch_working_set);
485498

@@ -525,6 +538,7 @@ bool ai_recursive_interproceduralt::visit_edge_function_call(
525538
p_end,
526539
calling_function_id,
527540
l_return,
541+
p_call, // To allow function-local history
528542
ns,
529543
working_set);
530544
}

src/analyses/ai.h

Lines changed: 6 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -252,7 +252,11 @@ class ai_baset
252252

253253
locationt n = std::next(l);
254254

255-
auto step_return = p->step(n, *(storage->abstract_traces_before(n)));
255+
auto step_return = p->step(
256+
n,
257+
*(storage->abstract_traces_before(n)),
258+
ai_history_baset::no_caller_history);
259+
// Caller history not needed as this is a local step
256260

257261
return storage->abstract_state_before(step_return.second, *domain_factory);
258262
}
@@ -469,6 +473,7 @@ class ai_baset
469473
trace_ptrt p,
470474
const irep_idt &to_function_id,
471475
locationt to_l,
476+
trace_ptrt caller_history,
472477
const namespacet &ns,
473478
working_sett &working_set);
474479

src/analyses/ai_history.cpp

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -27,3 +27,6 @@ xmlt ai_history_baset::output_xml(void) const
2727
xml.data = out.str();
2828
return xml;
2929
}
30+
31+
const ai_history_baset::trace_ptrt ai_history_baset::no_caller_history =
32+
nullptr;

src/analyses/ai_history.h

Lines changed: 15 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -88,11 +88,16 @@ class ai_history_baset
8888
typedef std::pair<step_statust, trace_ptrt> step_returnt;
8989
/// Step creates a new history by advancing the current one to location "to"
9090
/// It is given the set of all other histories that have reached this point.
91+
/// In the case of function call return it is also given the full history of
92+
/// the caller. This allows function-local histories as they can "pick up"
93+
/// the state from before the call when computing the return edge.
9194
///
9295
/// PRECONDITION(to.id_dereferenceable());
9396
/// PRECONDITION(to in goto_program.get_successors(current_location()) ||
9497
/// current_location()->is_function_call() ||
9598
/// current_location()->is_end_function());
99+
/// PRECONDITION(caller_hist == no_caller_history ||
100+
/// current_location()->is_end_function);
96101
///
97102
/// Step may do one of three things :
98103
/// 1. Create a new history object and return a pointer to it
@@ -108,7 +113,12 @@ class ai_history_baset
108113
/// other than the call location) or undesireable (omitting some traces)
109114
/// POSTCONDITION(IMPLIES(result.first == BLOCKED,
110115
/// result.second == nullptr()));
111-
virtual step_returnt step(locationt to, const trace_sett &others) const = 0;
116+
virtual step_returnt step(
117+
locationt to,
118+
const trace_sett &others,
119+
trace_ptrt caller_hist) const = 0;
120+
121+
static const trace_ptrt no_caller_history;
112122

113123
/// The order for history_sett
114124
virtual bool operator<(const ai_history_baset &op) const = 0;
@@ -157,7 +167,10 @@ class ahistoricalt : public ai_history_baset
157167
{
158168
}
159169

160-
step_returnt step(locationt to, const trace_sett &others) const override
170+
step_returnt step(
171+
locationt to,
172+
const trace_sett &others,
173+
trace_ptrt caller_hist) const override
161174
{
162175
trace_ptrt next(new ahistoricalt(to));
163176

src/analyses/call_stack_history.cpp

Lines changed: 21 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -11,8 +11,10 @@ Author: Martin Brain, martin.brain@cs.ox.ac.uk
1111

1212
#include "call_stack_history.h"
1313

14-
ai_history_baset::step_returnt
15-
call_stack_historyt::step(locationt to, const trace_sett &others) const
14+
ai_history_baset::step_returnt call_stack_historyt::step(
15+
locationt to,
16+
const trace_sett &others,
17+
trace_ptrt caller_hist) const
1618
{
1719
DATA_INVARIANT(current_stack != nullptr, "current_stack must exist");
1820

@@ -79,12 +81,29 @@ call_stack_historyt::step(locationt to, const trace_sett &others) const
7981
}
8082
else
8183
{
84+
INVARIANT(
85+
caller_hist != ai_history_baset::no_caller_history,
86+
"return from function should have a caller");
87+
8288
// The expected call return site...
8389
locationt l_caller_return =
8490
std::next(current_stack->caller->current_location);
8591

8692
if(l_caller_return->location_number == to->location_number)
8793
{
94+
INVARIANT(
95+
std::next(caller_hist->current_location())->location_number ==
96+
l_caller_return->location_number,
97+
"caller and caller_hist should be consistent");
98+
// It is tempting to think that...
99+
// INVARIANT(*(current_stack->caller) ==
100+
// *(std::dynamic_pointer_cast<const call_stack_historyt>
101+
// (caller_hist)->current_stack),
102+
// "call stacks should match");
103+
// and that we could just use caller_hist->current_stack here.
104+
// This fails when you hit the recursion limit so that the
105+
// caller_hist has a deep stack but *this has a shallow one.
106+
88107
// ... which is where we are going
89108
next_stack = cse_ptrt(std::make_shared<call_stack_entryt>(
90109
to, current_stack->caller->caller));

src/analyses/call_stack_history.h

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -81,7 +81,10 @@ class call_stack_historyt : public ai_history_baset
8181
{
8282
}
8383

84-
step_returnt step(locationt to, const trace_sett &others) const override;
84+
step_returnt step(
85+
locationt to,
86+
const trace_sett &others,
87+
trace_ptrt caller_hist) const override;
8588

8689
bool operator<(const ai_history_baset &op) const override;
8790
bool operator==(const ai_history_baset &op) const override;

0 commit comments

Comments
 (0)