Skip to content

Feature/context sensitive ait merge 2 #2622

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 5 commits into from
Aug 2, 2018
Merged

Feature/context sensitive ait merge 2 #2622

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
afe32b7
Refactor the methods that access "the abstract domain at a location".
Jul 24, 2018
1fe0796
Convert various older domains to use the more recent ait API.
Jan 16, 2018
e65f027
Add comments to the abstract interpreter interface.
Jul 24, 2018
773bc86
Convert various comments, asserts and throws into invariants.
Jul 24, 2018
28ba192
Strengthen the invariant on what are acceptable function calls.
Jul 26, 2018
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
87 changes: 25 additions & 62 deletions src/analyses/ai.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -15,8 +15,9 @@ Author: Daniel Kroening, kroening@kroening.com
#include <memory>
#include <sstream>

#include <util/std_expr.h>
#include <util/invariant.h>
#include <util/std_code.h>
#include <util/std_expr.h>

#include "is_threaded.h"

Expand Down Expand Up @@ -50,7 +51,7 @@ void ai_baset::output(
out << "**** " << i_it->location_number << " "
<< i_it->source_location << "\n";

find_state(i_it).output(out, *this, ns);
abstract_state_before(i_it)->output(out, *this, ns);
out << "\n";
#if 1
goto_program.output_instruction(ns, identifier, out, *i_it);
Expand Down Expand Up @@ -101,7 +102,8 @@ jsont ai_baset::output_json(
json_numbert(std::to_string(i_it->location_number));
location["sourceLocation"]=
json_stringt(i_it->source_location.as_string());
location["abstractState"]=find_state(i_it).output_json(*this, ns);
location["abstractState"] =
abstract_state_before(i_it)->output_json(*this, ns);

// Ideally we need output_instruction_json
std::ostringstream out;
Expand Down Expand Up @@ -162,7 +164,7 @@ xmlt ai_baset::output_xml(
"source_location",
i_it->source_location.as_string());

location.new_element(find_state(i_it).output_xml(*this, ns));
location.new_element(abstract_state_before(i_it)->output_xml(*this, ns));

// Ideally we need output_instruction_xml
std::ostringstream out;
Expand Down Expand Up @@ -219,7 +221,7 @@ void ai_baset::finalize()
ai_baset::locationt ai_baset::get_next(
working_sett &working_set)
{
assert(!working_set.empty());
PRECONDITION(!working_set.empty());

working_sett::iterator i=working_set.begin();
locationt l=i->second;
Expand Down Expand Up @@ -247,6 +249,7 @@ bool ai_baset::fixedpoint(
{
locationt l=get_next(working_set);

// goto_program is really only needed for iterator manipulation
if(visit(l, working_set, goto_program, goto_functions, ns))
new_data=true;
}
Expand Down Expand Up @@ -322,6 +325,8 @@ bool ai_baset::do_function_call(
// initialize state, if necessary
get_state(l_return);

PRECONDITION(l_call->is_function_call());

const goto_functionst::goto_functiont &goto_function=
f_it->second;

Expand Down Expand Up @@ -387,69 +392,27 @@ bool ai_baset::do_function_call_rec(
const goto_functionst &goto_functions,
const namespacet &ns)
{
assert(!goto_functions.function_map.empty());
PRECONDITION(!goto_functions.function_map.empty());

// This is quite a strong assumption on the well-formedness of the program.
// It means function pointers must be removed before use.
DATA_INVARIANT(
function.id() == ID_symbol,
"Function pointers and indirect calls must be removed before analysis.");

bool new_data=false;

if(function.id()==ID_symbol)
{
const irep_idt &identifier = to_symbol_expr(function).get_identifier();
const irep_idt &identifier = to_symbol_expr(function).get_identifier();

goto_functionst::function_mapt::const_iterator it=
goto_functions.function_map.find(identifier);
goto_functionst::function_mapt::const_iterator it =
goto_functions.function_map.find(identifier);

if(it==goto_functions.function_map.end())
throw "failed to find function "+id2string(identifier);
DATA_INVARIANT(
it != goto_functions.function_map.end(),
"Function " + id2string(identifier) + "not in function map");

new_data=do_function_call(
l_call, l_return,
goto_functions,
it,
arguments,
ns);
}
else if(function.id()==ID_if)
{
if(function.operands().size()!=3)
throw "if has three operands";

bool new_data1=
do_function_call_rec(
l_call, l_return,
function.op1(),
arguments,
goto_functions,
ns);

bool new_data2=
do_function_call_rec(
l_call, l_return,
function.op2(),
arguments,
goto_functions,
ns);

if(new_data1 || new_data2)
new_data=true;
}
else if(function.id()==ID_dereference)
{
// We can't really do this here -- we rely on
// these being removed by some previous analysis.
}
else if(function.id() == ID_null_object)
{
// ignore, can't be a function
}
else if(function.id()==ID_member || function.id()==ID_index)
{
// ignore, can't be a function
}
else
{
throw "unexpected function_call argument: "+
function.id_string();
}
new_data =
do_function_call(l_call, l_return, goto_functions, it, arguments, ns);

return new_data;
}
Expand Down
38 changes: 30 additions & 8 deletions src/analyses/ai.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -25,6 +25,8 @@ Author: Daniel Kroening, kroening@kroening.com

#include "ai_domain.h"

/// The basic interface of an abstract interpreter. This should be enough
/// to create, run and query an abstract interpreter.
// don't use me -- I am just a base class
// use ait instead
class ai_baset
Expand All @@ -41,6 +43,7 @@ class ai_baset
{
}

/// Running the interpreter
void operator()(
const goto_programt &goto_program,
const namespacet &ns)
Expand Down Expand Up @@ -82,17 +85,26 @@ class ai_baset
finalize();
}

/// Accessing individual domains at particular locations
/// (without needing to know what kind of domain or history is used)
/// A pointer to a copy as the method should be const and
/// there are some non-trivial cases including merging domains, etc.
/// Intended for users of the abstract interpreter; don't use internally.

/// Returns the abstract state before the given instruction
virtual const ai_domain_baset & abstract_state_before(
goto_programt::const_targett t) const = 0;
/// PRECONDITION(l is dereferenceable)
virtual std::unique_ptr<statet> abstract_state_before(locationt l) const = 0;
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'm wondering whether this shouldn't use optional?

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

What would be the use-case for it not returning anything?

Copy link
Member

@peterschrammel peterschrammel Jul 26, 2018 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Why can't it just return a const ref? I'm unsure where the return value comes from.

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

In this case it could and used to return a constant ref. However if we are going to break the 1-to-1 link between location and domain (which is the whole point of this patch set) then we have to be able to support cases where the abstract interpreter may not have the domain and may have to compute it in this function. For example : merging all of the different contexts that reach this point or dynamically recomputing the domain from the last merge point. That's why the API needs to change.


/// Returns the abstract state after the given instruction
virtual const ai_domain_baset & abstract_state_after(
goto_programt::const_targett t) const
virtual std::unique_ptr<statet> abstract_state_after(locationt l) const
{
return abstract_state_before(std::next(t));
/// PRECONDITION(l is dereferenceable && std::next(l) is dereferenceable)
/// Check relies on a DATA_INVARIANT of goto_programs
INVARIANT(!l->is_end_function(), "No state after the last instruction");
return abstract_state_before(std::next(l));
}

/// Resets the domain
virtual void clear()
{
}
Expand Down Expand Up @@ -237,6 +249,9 @@ class ai_baset
const goto_functionst &goto_functions,
const namespacet &ns);

// Visit performs one step of abstract interpretation from location l
// Depending on the instruction type it may compute a number of "edges"
// or applications of the abstract transformer
// true = found something new
bool visit(
locationt l,
Expand Down Expand Up @@ -304,10 +319,17 @@ class ait:public ai_baset
return it->second;
}

const ai_domain_baset & abstract_state_before(
goto_programt::const_targett t) const override
std::unique_ptr<statet> abstract_state_before(locationt t) const override
{
return (*this)[t];
typename state_mapt::const_iterator it = state_map.find(t);
if(it == state_map.end())
{
std::unique_ptr<statet> d = util_make_unique<domainT>();
CHECK_RETURN(d->is_bottom());
return d;
}

return util_make_unique<domainT>(it->second);
}

void clear() override
Expand Down
20 changes: 11 additions & 9 deletions src/analyses/constant_propagator.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -592,43 +592,45 @@ void constant_propagator_ait::replace(
{
Forall_goto_program_instructions(it, goto_function.body)
{
state_mapt::iterator s_it=state_map.find(it);
// Works because this is a location (but not history) sensitive domain
const constant_propagator_domaint &d = (*this)[it];

if(s_it==state_map.end())
if(d.is_bottom())
continue;

replace_types_rec(s_it->second.values.replace_const, it->code);
replace_types_rec(s_it->second.values.replace_const, it->guard);
replace_types_rec(d.values.replace_const, it->code);
replace_types_rec(d.values.replace_const, it->guard);

if(it->is_goto() || it->is_assume() || it->is_assert())
{
s_it->second.partial_evaluate(it->guard, ns);
d.partial_evaluate(it->guard, ns);
}
else if(it->is_assign())
{
exprt &rhs=to_code_assign(it->code).rhs();
s_it->second.partial_evaluate(rhs, ns);
d.partial_evaluate(rhs, ns);

if(rhs.id()==ID_constant)
rhs.add_source_location()=it->code.op0().source_location();
}
else if(it->is_function_call())
{
exprt &function = to_code_function_call(it->code).function();
s_it->second.partial_evaluate(function, ns);
d.partial_evaluate(function, ns);

exprt::operandst &args=
to_code_function_call(it->code).arguments();

for(auto &arg : args)
{
s_it->second.partial_evaluate(arg, ns);
d.partial_evaluate(arg, ns);
}
}
else if(it->is_other())
{
if(it->code.get_statement()==ID_expression)
{
s_it->second.partial_evaluate(it->code, ns);
d.partial_evaluate(it->code, ns);
}
}
}
Expand Down
4 changes: 2 additions & 2 deletions src/analyses/dependence_graph.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -307,9 +307,9 @@ void dependence_grapht::add_dep(
goto_programt::const_targett from,
goto_programt::const_targett to)
{
const node_indext n_from=state_map[from].get_node_id();
const node_indext n_from = (*this)[from].get_node_id();
assert(n_from<size());
const node_indext n_to=state_map[to].get_node_id();
const node_indext n_to = (*this)[to].get_node_id();
assert(n_to<size());

// add_edge is redundant as the subsequent operations also insert
Expand Down
8 changes: 4 additions & 4 deletions src/analyses/invariant_propagation.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -206,7 +206,7 @@ void invariant_propagationt::initialize(const goto_programt &goto_program)

forall_goto_program_instructions(it, goto_program)
{
invariant_sett &s=state_map[it].invariant_set;
invariant_sett &s = (*this)[it].invariant_set;

if(it==goto_program.instructions.begin())
s.make_true();
Expand Down Expand Up @@ -243,11 +243,11 @@ void invariant_propagationt::simplify(goto_programt &goto_program)
continue;

// find invariant set
state_mapt::const_iterator s_it=state_map.find(i_it);
if(s_it==state_map.end())
const auto &d = (*this)[i_it];
if(d.is_bottom())
continue;

const invariant_sett &invariant_set=s_it->second.invariant_set;
const invariant_sett &invariant_set = d.invariant_set;

exprt simplified_guard(i_it->guard);

Expand Down
26 changes: 13 additions & 13 deletions src/goto-analyzer/static_simplifier.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -65,8 +65,8 @@ bool static_simplifier(

if(i_it->is_assert())
{
bool unchanged=
ai.abstract_state_before(i_it).ai_simplify(i_it->guard, ns);
bool unchanged =
ai.abstract_state_before(i_it)->ai_simplify(i_it->guard, ns);

if(unchanged)
unmodified.asserts++;
Expand All @@ -75,8 +75,8 @@ bool static_simplifier(
}
else if(i_it->is_assume())
{
bool unchanged=
ai.abstract_state_before(i_it).ai_simplify(i_it->guard, ns);
bool unchanged =
ai.abstract_state_before(i_it)->ai_simplify(i_it->guard, ns);

if(unchanged)
unmodified.assumes++;
Expand All @@ -85,8 +85,8 @@ bool static_simplifier(
}
else if(i_it->is_goto())
{
bool unchanged=
ai.abstract_state_before(i_it).ai_simplify(i_it->guard, ns);
bool unchanged =
ai.abstract_state_before(i_it)->ai_simplify(i_it->guard, ns);

if(unchanged)
unmodified.gotos++;
Expand All @@ -102,11 +102,11 @@ bool static_simplifier(
// <i=0, j=1> i=j
// should simplify to i=1, not to 0=1.

bool unchanged_lhs=
ai.abstract_state_before(i_it).ai_simplify_lhs(assign.lhs(), ns);
bool unchanged_lhs =
ai.abstract_state_before(i_it)->ai_simplify_lhs(assign.lhs(), ns);

bool unchanged_rhs=
ai.abstract_state_before(i_it).ai_simplify(assign.rhs(), ns);
bool unchanged_rhs =
ai.abstract_state_before(i_it)->ai_simplify(assign.rhs(), ns);

if(unchanged_lhs && unchanged_rhs)
unmodified.assigns++;
Expand All @@ -117,13 +117,13 @@ bool static_simplifier(
{
code_function_callt &fcall=to_code_function_call(i_it->code);

bool unchanged=
ai.abstract_state_before(i_it).ai_simplify(fcall.function(), ns);
bool unchanged =
ai.abstract_state_before(i_it)->ai_simplify(fcall.function(), ns);

exprt::operandst &args=fcall.arguments();

for(auto &o : args)
unchanged&=ai.abstract_state_before(i_it).ai_simplify(o, ns);
unchanged &= ai.abstract_state_before(i_it)->ai_simplify(o, ns);

if(unchanged)
unmodified.function_calls++;
Expand Down
Loading