const namespacet &ns,

const goto_functionst &goto_functions,

std::ostream &out) const

{

for(const auto &gf_entry : goto_functions.function_map)

{

if(gf_entry.second.body_available())

{

out << "////\n";

out << "//// Function: " << gf_entry.first << "\n";

out << "////\n";

out << "\n";

output(ns, gf_entry.first, gf_entry.second.body, out);

}

}

const namespacet &ns,

const irep_idt &function_id,

const goto_programt &goto_program,

std::ostream &out) const

{

(void)function_id; // unused parameter

forall_goto_program_instructions(i_it, goto_program)

{

out << "**** " << i_it->location_number << " " << i_it->source_location()

<< "\n";

abstract_state_before(i_it)->output(out, *this, ns);

out << "\n";

#if 1

i_it->output(out);

out << "\n";

#endif

}

const namespacet &ns,

const goto_functionst &goto_functions) const

{

json_objectt result;

for(const auto &gf_entry : goto_functions.function_map)

{

if(gf_entry.second.body_available())

{

result[id2string(gf_entry.first)] =

output_json(ns, gf_entry.first, gf_entry.second.body);

}

else

{

result[id2string(gf_entry.first)] = json_arrayt();

}

}

return std::move(result);

const namespacet &ns,

const irep_idt &function_id,

const goto_programt &goto_program) const

{

(void)function_id; // unused parameter

json_arrayt contents;

forall_goto_program_instructions(i_it, goto_program)

{

// Ideally we need output_instruction_json

std::ostringstream out;

i_it->output(out);

json_objectt location{

{"locationNumber", json_numbert(std::to_string(i_it->location_number))},

{"sourceLocation", json_stringt(i_it->source_location().as_string())},

{"abstractState", abstract_state_before(i_it)->output_json(*this, ns)},

{"instruction", json_stringt(out.str())}};

contents.push_back(std::move(location));

}

return std::move(contents);

const namespacet &ns,

const goto_functionst &goto_functions) const

{

xmlt program("program");

for(const auto &gf_entry : goto_functions.function_map)

{

xmlt function(

"function",

{{"name", id2string(gf_entry.first)},

{"body_available", gf_entry.second.body_available() ? "true" : "false"}},

{});

if(gf_entry.second.body_available())

{

function.new_element(

output_xml(ns, gf_entry.first, gf_entry.second.body));

}

program.new_element(function);

}

return program;

const namespacet &ns,

const irep_idt &function_id,

const goto_programt &goto_program) const

{

(void)function_id; // unused parameter

xmlt function_body;

forall_goto_program_instructions(i_it, goto_program)

{

xmlt location(

"",

{{"location_number", std::to_string(i_it->location_number)},

{"source_location", i_it->source_location().as_string()}},

{abstract_state_before(i_it)->output_xml(*this, ns)});

// Ideally we need output_instruction_xml

std::ostringstream out;

i_it->output(out);

location.set_attribute("instruction", out.str());

function_body.new_element(location);

}

return function_body;

{

// find the 'entry function'

goto_functionst::function_mapt::const_iterator

f_it=goto_functions.function_map.find(goto_functions.entry_point());

if(f_it!=goto_functions.function_map.end())

return entry_state(f_it->second.body);

// It is not clear if this is even a well-structured goto_functionst object

return nullptr;

{

if(goto_program.empty())

return nullptr;

// The first instruction of 'goto_program' is the entry point

trace_ptrt p = history_factory->epoch(goto_program.instructions.begin());

get_state(p).make_entry();

return p;

const irep_idt &function_id,

const goto_functionst::goto_functiont &goto_function)

{

initialize(function_id, goto_function.body);

{

// Domains are created and set to bottom on access.

// So we do not need to set them to be bottom before hand.

{

for(const auto &gf_entry : goto_functions.function_map)

initialize(gf_entry.first, gf_entry.second);

{

PRECONDITION(!working_set.empty());

static_assert(

std::is_same<

working_sett,

std::set<trace_ptrt, ai_history_baset::compare_historyt>>::value,

"begin must return the minimal entry");

auto first = working_set.begin();

trace_ptrt t = *first;

working_set.erase(first);

return t;

trace_ptrt start_trace,

const irep_idt &function_id,

const goto_programt &goto_program,

const goto_functionst &goto_functions,

const namespacet &ns)

{

PRECONDITION(start_trace != nullptr);

working_sett working_set;

put_in_working_set(working_set, start_trace);

bool new_data=false;

while(!working_set.empty())

{

trace_ptrt p = get_next(working_set);

// goto_program is really only needed for iterator manipulation

if(visit(function_id, p, working_set, goto_program, goto_functions, ns))

new_data=true;

}

return new_data;

trace_ptrt start_trace,

const goto_functionst &goto_functions,

const namespacet &ns)

{

goto_functionst::function_mapt::const_iterator f_it =

goto_functions.function_map.find(goto_functions.entry_point());

if(f_it != goto_functions.function_map.end())

fixedpoint(start_trace, f_it->first, f_it->second.body, goto_functions, ns);

const irep_idt &function_id,

trace_ptrt p,

working_sett &working_set,

const goto_programt &goto_program,

const goto_functionst &goto_functions,

const namespacet &ns)

{

bool new_data=false;

locationt l = p->current_location();

messaget log(message_handler);

log.progress() << "ai_baset::visit " << l->location_number << " in "

<< function_id << messaget::eom;

// Function call and end are special cases

if(l->is_function_call())

{

DATA_INVARIANT(

goto_program.get_successors(l).size() == 1,

"function calls only have one successor");

DATA_INVARIANT(

*(goto_program.get_successors(l).begin()) == std::next(l),

"function call successor / return location must be the next instruction");

new_data = visit_function_call(

function_id, p, working_set, goto_program, goto_functions, ns);

}

else if(l->is_end_function())

{

DATA_INVARIANT(

goto_program.get_successors(l).empty(),

"The end function instruction should have no successors.");

new_data = visit_end_function(

function_id, p, working_set, goto_program, goto_functions, ns);

}

else

{

// Successors can be empty, for example assume(0).

// Successors can contain duplicates, for example GOTO next;

for(const auto &to_l : goto_program.get_successors(l))

{

if(to_l == goto_program.instructions.end())

continue;

new_data |= visit_edge(

function_id,

p,

function_id,

to_l,

ai_history_baset::no_caller_history,

ns,

working_set); // Local steps so no caller history needed

}

}

return new_data;

const irep_idt &function_id,

trace_ptrt p,

const irep_idt &to_function_id,

locationt to_l,

trace_ptrt caller_history,

const namespacet &ns,

working_sett &working_set)

{

messaget log(message_handler);

log.progress() << "ai_baset::visit_edge from "

<< p->current_location()->location_number << " to "

<< to_l->location_number << "... ";

// Has history taught us not to step here...

auto next =

p->step(to_l, *(storage->abstract_traces_before(to_l)), caller_history);

if(next.first == ai_history_baset::step_statust::BLOCKED)

{

log.progress() << "blocked by history" << messaget::eom;

return false;

}

else if(next.first == ai_history_baset::step_statust::NEW)

{

log.progress() << "gives a new history... ";

}

else

{

log.progress() << "merges with existing history... ";

}

trace_ptrt to_p = next.second;

// Abstract domains are mutable so we must copy before we transform

statet &current = get_state(p);

std::unique_ptr<statet> tmp_state(make_temporary_state(current));

statet &new_values = *tmp_state;

// Apply transformer

log.progress() << "applying transformer... ";

new_values.transform(function_id, p, to_function_id, to_p, *this, ns);

// Expanding a domain means that it has to be analysed again

// Likewise if the history insists that it is a new trace

// (assuming it is actually reachable).

log.progress() << "merging... ";

bool return_value = false;

if(

merge(new_values, p, to_p) ||

(next.first == ai_history_baset::step_statust::NEW &&

!new_values.is_bottom()))

{

put_in_working_set(working_set, to_p);

log.progress() << "result queued." << messaget::eom;

return_value = true;

}

else

{

log.progress() << "domain unchanged." << messaget::eom;

}

// Branch because printing some histories and domains can be expensive

// esp. if the output is then just discarded and this is a critical path.

if(message_handler.get_verbosity() >= messaget::message_levelt::M_DEBUG)

{

log.debug() << "p = ";

p->output(log.debug());

log.debug() << messaget::eom;

log.debug() << "current = ";

current.output(log.debug(), *this, ns);

log.debug() << messaget::eom;

log.debug() << "to_p = ";

to_p->output(log.debug());

log.debug() << messaget::eom;

log.debug() << "new_values = ";

new_values.output(log.debug(), *this, ns);

log.debug() << messaget::eom;

}

return return_value;

const irep_idt &calling_function_id,

trace_ptrt p_call,

locationt l_return,

const irep_idt &,

working_sett &working_set,

const goto_programt &,

const goto_functionst &,

const namespacet &ns)

{

messaget log(message_handler);

log.progress() << "ai_baset::visit_edge_function_call from "

<< p_call->current_location()->location_number << " to "

<< l_return->location_number << messaget::eom;

// The default implementation is not interprocedural

// so the effects of the call are approximated but nothing else

return visit_edge(

calling_function_id,

p_call,

calling_function_id,

l_return,

ai_history_baset::

no_caller_history, // Not needed as we are skipping the function call

ns,

working_set);

const irep_idt &calling_function_id,

trace_ptrt p_call,

working_sett &working_set,

const goto_programt &caller,

const goto_functionst &goto_functions,

const namespacet &ns)

{

locationt l_call = p_call->current_location();

PRECONDITION(l_call->is_function_call());

messaget log(message_handler);

log.progress() << "ai_baset::visit_function_call at "

<< l_call->location_number << messaget::eom;

locationt l_return = std::next(l_call);

// operator() allows analysis of a single goto_program independently

// it generates a synthetic goto_functions object for this

if(!goto_functions.function_map.empty())

{

const exprt &callee_expression = l_call->call_function();

if(callee_expression.id() == ID_symbol)

{

const irep_idt &callee_function_id =

to_symbol_expr(callee_expression).get_identifier();

log.progress() << "Calling " << callee_function_id << messaget::eom;

goto_functionst::function_mapt::const_iterator it =

goto_functions.function_map.find(callee_function_id);

DATA_INVARIANT(

it != goto_functions.function_map.end(),

"Function " + id2string(callee_function_id) + "not in function map");

const goto_functionst::goto_functiont &callee_fun = it->second;

if(callee_fun.body_available())

{

return visit_edge_function_call(

calling_function_id,

p_call,

l_return,

callee_function_id,

working_set,

callee_fun.body,

goto_functions,

ns);

}

else

{

// Fall through to the default, body not available, case

}

}

else

{

// Function pointers are not currently supported and must be removed

DATA_INVARIANT(

callee_expression.id() == ID_symbol,

"Function pointers and indirect calls must be removed before "

"analysis.");

}

}

// If the body is not available then we just do the edge from call to return

// in the caller. Domains should over-approximate what the function might do.

return visit_edge(

calling_function_id,

p_call,

calling_function_id,

l_return,

ai_history_baset::no_caller_history, // Would be the same as p_call...

ns,

working_set);

const irep_idt &function_id,

trace_ptrt p,

working_sett &working_set,

const goto_programt &goto_program,

const goto_functionst &goto_functions,

const namespacet &ns)

{

locationt l = p->current_location();

PRECONDITION(l->is_end_function());

messaget log(message_handler);

log.progress() << "ai_baset::visit_end_function " << function_id

<< messaget::eom;

// Do nothing

return false;

const irep_idt &calling_function_id,

trace_ptrt p_call,

locationt l_return,

const irep_idt &callee_function_id,

working_sett &working_set,

const goto_programt &callee,

const goto_functionst &goto_functions,

const namespacet &ns)

{

messaget log(message_handler);

log.progress() << "ai_recursive_interproceduralt::visit_edge_function_call"

<< " from " << p_call->current_location()->location_number

<< " to " << l_return->location_number << messaget::eom;

// This is the edge from call site to function head.

{

locationt l_begin = callee.instructions.begin();

working_sett catch_working_set; // The trace from the next fixpoint

// Do the edge from the call site to the beginning of the function

bool new_data = visit_edge(

calling_function_id,

p_call,

callee_function_id,

l_begin,

ai_history_baset::

no_caller_history, // Not needed as p_call already has the info

ns,

catch_working_set);

log.progress() << "Handle " << callee_function_id << " recursively"

<< messaget::eom;

// do we need to do/re-do the fixedpoint of the body?

if(new_data)

fixedpoint(

get_next(catch_working_set),

callee_function_id,

callee,

goto_functions,

ns);

}

// This is the edge from function end to return site.

{

log.progress() << "Handle return edges" << messaget::eom;

// get location at end of the procedure we have called

locationt l_end = --callee.instructions.end();

DATA_INVARIANT(

l_end->is_end_function(),

"The last instruction of a goto_program must be END_FUNCTION");

// Find the histories for a location

auto traces = storage->abstract_traces_before(l_end);

bool new_data = false;

// The history used may mean there are multiple histories at the end of the

// function. Some of these can be progressed (for example, if the history

// tracks paths within functions), some can't be (for example, not all

// calling contexts will be appropriate). We rely on the history's step,

// called from visit_edge to prune as applicable.

for(auto p_end : *traces)

{

// do edge from end of function to instruction after call

const statet &end_state = get_state(p_end);

if(!end_state.is_bottom())

{

// function exit point reachable in that history

new_data |= visit_edge(

callee_function_id,

p_end,

calling_function_id,

l_return,

p_call, // To allow function-local history

ns,

working_set);

}

}

return new_data;

}