Skip to content

Fix/correct domain interface #1790

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.

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 9 commits into from
Feb 9, 2018
12 changes: 4 additions & 8 deletions src/analyses/ai.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -365,8 +365,7 @@ bool ai_baset::visit(
// initialize state, if necessary
get_state(to_l);

new_values.transform(
l, to_l, *this, ns, ai_domain_baset::edge_typet::FUNCTION_LOCAL);
new_values.transform(l, to_l, *this, ns);

if(merge(new_values, l, to_l))
have_new_values=true;
Expand Down Expand Up @@ -399,8 +398,7 @@ bool ai_baset::do_function_call(
{
// if we don't have a body, we just do an edige call -> return
std::unique_ptr<statet> tmp_state(make_temporary_state(get_state(l_call)));
tmp_state->transform(
l_call, l_return, *this, ns, ai_domain_baset::edge_typet::FUNCTION_LOCAL);
tmp_state->transform(l_call, l_return, *this, ns);

return merge(*tmp_state, l_call, l_return);
}
Expand All @@ -417,8 +415,7 @@ bool ai_baset::do_function_call(

// do the edge from the call site to the beginning of the function
std::unique_ptr<statet> tmp_state(make_temporary_state(get_state(l_call)));
tmp_state->transform(
l_call, l_begin, *this, ns, ai_domain_baset::edge_typet::CALL);
tmp_state->transform(l_call, l_begin, *this, ns);

bool new_data=false;

Expand All @@ -445,8 +442,7 @@ bool ai_baset::do_function_call(
return false; // function exit point not reachable

std::unique_ptr<statet> tmp_state(make_temporary_state(end_state));
tmp_state->transform(
l_end, l_return, *this, ns, ai_domain_baset::edge_typet::RETURN);
tmp_state->transform(l_end, l_return, *this, ns);

// Propagate those
return merge(*tmp_state, l_end, l_return);
Expand Down
24 changes: 15 additions & 9 deletions src/analyses/ai.h
Original file line number Diff line number Diff line change
Expand Up @@ -31,13 +31,6 @@ class ai_baset;
class ai_domain_baset
{
public:
enum class edge_typet
{
FUNCTION_LOCAL,
CALL,
RETURN,
};

// The constructor is expected to produce 'false'
// or 'bottom'
ai_domain_baset()
Expand All @@ -55,13 +48,21 @@ class ai_domain_baset
// b) there is an edge from the last instruction (END_FUNCTION)
// of the function to the instruction _following_ the call site
// (this also needs to set the LHS, if applicable)
//
// "this" is the domain before the instruction "from"
// "from" is the instruction to be interpretted
// "to" is the next instruction (for GOTO, FUNCTION_CALL, END_FUNCTION)
//
// PRECONDITION(from.is_dereferenceable(), "Must not be _::end()")
// PRECONDITION(to.is_dereferenceable(), "Must not be _::end()")
// PRECONDITION(are_comparable(from,to) ||
// (from->is_function_call() || from->is_end_function())

virtual void transform(
locationt from,
locationt to,
ai_baset &ai,
const namespacet &ns,
edge_typet edge_type) = 0;
const namespacet &ns) = 0;

virtual void output(
std::ostream &out,
Expand Down Expand Up @@ -98,6 +99,11 @@ class ai_domain_baset
//
// This computes the join between "this" and "b".
// Return true if "this" has changed.
// In the usual case, "b" is the updated state after "from"
// and "this" is the state before "to".
//
// PRECONDITION(from.is_dereferenceable(), "Must not be _::end()")
// PRECONDITION(to.is_dereferenceable(), "Must not be _::end()")

// This method allows an expression to be simplified / evaluated using the
// current state. It is used to evaluate assertions and in program
Expand Down
14 changes: 8 additions & 6 deletions src/analyses/constant_propagator.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -45,8 +45,7 @@ void constant_propagator_domaint::transform(
locationt from,
locationt to,
ai_baset &ai,
const namespacet &ns,
ai_domain_baset::edge_typet edge_type)
const namespacet &ns)
{
#ifdef DEBUG
std::cout << "Transform from/to:\n";
Expand Down Expand Up @@ -94,6 +93,8 @@ void constant_propagator_domaint::transform(
{
exprt g;

// Comparing iterators is safe as the target must be within the same list
// of instructions because this is a GOTO.
if(from->get_target()==to)
g=simplify_expr(from->guard, ns);
else
Expand Down Expand Up @@ -122,15 +123,14 @@ void constant_propagator_domaint::transform(
const code_function_callt &function_call=to_code_function_call(from->code);
const exprt &function=function_call.function();

const locationt& next=std::next(from);

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

if(edge_type == ai_domain_baset::edge_typet::FUNCTION_LOCAL)
// Functions with no body
if(from->function == to->function)
{
if(id==CPROVER_PREFIX "set_must" ||
id==CPROVER_PREFIX "get_must" ||
Expand Down Expand Up @@ -178,7 +178,9 @@ void constant_propagator_domaint::transform(
else
{
// unresolved call
INVARIANT(to==next, "Unresolved call can only be approximated if a skip");
INVARIANT(
from->function == to->function,
"Unresolved call can only be approximated if a skip");

if(have_dirty)
values.set_dirty_to_top(cp->dirty, ns);
Expand Down
3 changes: 1 addition & 2 deletions src/analyses/constant_propagator.h
Original file line number Diff line number Diff line change
Expand Up @@ -25,8 +25,7 @@ class constant_propagator_domaint:public ai_domain_baset
locationt from,
locationt to,
ai_baset &ai_base,
const namespacet &ns,
ai_domain_baset::edge_typet edge_type) final override;
const namespacet &ns) final override;

virtual void output(
std::ostream &out,
Expand Down
7 changes: 4 additions & 3 deletions src/analyses/custom_bitvector_analysis.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -269,8 +269,7 @@ void custom_bitvector_domaint::transform(
locationt from,
locationt to,
ai_baset &ai,
const namespacet &ns,
ai_domain_baset::edge_typet edge_type)
const namespacet &ns)
{
// upcast of ai
custom_bitvector_analysist &cba=
Expand Down Expand Up @@ -397,7 +396,7 @@ void custom_bitvector_domaint::transform(
else
{
// only if there is an actual call, i.e., we have a body
if(edge_type != ai_domain_baset::edge_typet::FUNCTION_LOCAL)
if(from->function != to->function)
{
const code_typet &code_type=
to_code_type(ns.lookup(identifier).type);
Expand Down Expand Up @@ -520,6 +519,8 @@ void custom_bitvector_domaint::transform(
{
exprt guard=instruction.guard;

// Comparing iterators is safe as the target must be within the same list
// of instructions because this is a GOTO.
if(to!=from->get_target())
guard.make_not();

Expand Down
9 changes: 3 additions & 6 deletions src/analyses/custom_bitvector_analysis.h
Original file line number Diff line number Diff line change
Expand Up @@ -23,12 +23,9 @@ class custom_bitvector_analysist;
class custom_bitvector_domaint:public ai_domain_baset
{
public:
void transform(
locationt from,
locationt to,
ai_baset &ai,
const namespacet &ns,
ai_domain_baset::edge_typet edge_type) final override;
void
transform(locationt from, locationt to, ai_baset &ai, const namespacet &ns)
final override;

void output(
std::ostream &out,
Expand Down
8 changes: 3 additions & 5 deletions src/analyses/dependence_graph.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -187,24 +187,22 @@ void dep_graph_domaint::transform(
goto_programt::const_targett from,
goto_programt::const_targett to,
ai_baset &ai,
const namespacet &ns,
ai_domain_baset::edge_typet edge_type)
const namespacet &ns)
{
dependence_grapht *dep_graph=dynamic_cast<dependence_grapht*>(&ai);
assert(dep_graph!=nullptr);

// propagate control dependencies across function calls
if(from->is_function_call())
{
const goto_programt::const_targett next = std::next(from);

if(edge_type == ai_domain_baset::edge_typet::FUNCTION_LOCAL)
if(from->function == to->function)
{
control_dependencies(from, to, *dep_graph);
}
else
{
// edge to function entry point
const goto_programt::const_targett next = std::next(from);

dep_graph_domaint *s=
dynamic_cast<dep_graph_domaint*>(&(dep_graph->get_state(next)));
Expand Down
3 changes: 1 addition & 2 deletions src/analyses/dependence_graph.h
Original file line number Diff line number Diff line change
Expand Up @@ -83,8 +83,7 @@ class dep_graph_domaint:public ai_domain_baset
goto_programt::const_targett from,
goto_programt::const_targett to,
ai_baset &ai,
const namespacet &ns,
ai_domain_baset::edge_typet edge_type) final override;
const namespacet &ns) final override;

void output(
std::ostream &out,
Expand Down
3 changes: 1 addition & 2 deletions src/analyses/escape_analysis.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -165,8 +165,7 @@ void escape_domaint::transform(
locationt from,
locationt to,
ai_baset &ai,
const namespacet &ns,
ai_domain_baset::edge_typet /*edge_type*/)
const namespacet &ns)
{
if(has_values.is_false())
return;
Expand Down
9 changes: 3 additions & 6 deletions src/analyses/escape_analysis.h
Original file line number Diff line number Diff line change
Expand Up @@ -28,12 +28,9 @@ class escape_domaint:public ai_domain_baset
{
}

void transform(
locationt from,
locationt to,
ai_baset &ai,
const namespacet &ns,
ai_domain_baset::edge_typet edge_type) final override;
void
transform(locationt from, locationt to, ai_baset &ai, const namespacet &ns)
final override;

void output(
std::ostream &out,
Expand Down
3 changes: 1 addition & 2 deletions src/analyses/global_may_alias.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -79,8 +79,7 @@ void global_may_alias_domaint::transform(
locationt from,
locationt to,
ai_baset &ai,
const namespacet &ns,
ai_domain_baset::edge_typet /*edge_type*/)
const namespacet &ns)
{
if(has_values.is_false())
return;
Expand Down
9 changes: 3 additions & 6 deletions src/analyses/global_may_alias.h
Original file line number Diff line number Diff line change
Expand Up @@ -28,12 +28,9 @@ class global_may_alias_domaint:public ai_domain_baset
{
}

void transform(
locationt from,
locationt to,
ai_baset &ai,
const namespacet &ns,
ai_domain_baset::edge_typet edge_type) final override;
void
transform(locationt from, locationt to, ai_baset &ai, const namespacet &ns)
final override;

void output(
std::ostream &out,
Expand Down
16 changes: 10 additions & 6 deletions src/analyses/interval_domain.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -59,8 +59,7 @@ void interval_domaint::transform(
locationt from,
locationt to,
ai_baset &ai,
const namespacet &ns,
ai_domain_baset::edge_typet /*edge_type*/)
const namespacet &ns)
{
const goto_programt::instructiont &instruction=*from;
switch(instruction.type)
Expand All @@ -79,12 +78,17 @@ void interval_domaint::transform(

case GOTO:
{
// Comparing iterators is safe as the target must be within the same list
// of instructions because this is a GOTO.
locationt next=from;
next++;
if(next==to)
assume(not_exprt(instruction.guard), ns);
else
assume(instruction.guard, ns);
if(from->get_target() != next) // If equal then a skip
{
if(next == to)
assume(not_exprt(instruction.guard), ns);
else
assume(instruction.guard, ns);
}
}
break;

Expand Down
9 changes: 3 additions & 6 deletions src/analyses/interval_domain.h
Original file line number Diff line number Diff line change
Expand Up @@ -32,12 +32,9 @@ class interval_domaint:public ai_domain_baset
{
}

void transform(
locationt from,
locationt to,
ai_baset &ai,
const namespacet &ns,
ai_domain_baset::edge_typet edge_type) final override;
void
transform(locationt from, locationt to, ai_baset &ai, const namespacet &ns)
final override;

void output(
std::ostream &out,
Expand Down
5 changes: 3 additions & 2 deletions src/analyses/invariant_set_domain.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -17,13 +17,14 @@ void invariant_set_domaint::transform(
locationt from_l,
locationt to_l,
ai_baset &ai,
const namespacet &ns,
ai_domain_baset::edge_typet /*edge_type*/)
const namespacet &ns)
{
switch(from_l->type)
{
case GOTO:
{
// Comparing iterators is safe as the target must be within the same list
// of instructions because this is a GOTO.
exprt tmp(from_l->guard);

goto_programt::const_targett next=from_l;
Expand Down
3 changes: 1 addition & 2 deletions src/analyses/invariant_set_domain.h
Original file line number Diff line number Diff line change
Expand Up @@ -56,8 +56,7 @@ class invariant_set_domaint:public ai_domain_baset
locationt from_l,
locationt to_l,
ai_baset &ai,
const namespacet &ns,
ai_domain_baset::edge_typet edge_type) final override;
const namespacet &ns) final override;

void make_top() final override
{
Expand Down
9 changes: 3 additions & 6 deletions src/analyses/is_threaded.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -48,12 +48,9 @@ class is_threaded_domaint:public ai_domain_baset
old_is_threaded!=is_threaded;
}

void transform(
locationt from,
locationt to,
ai_baset &ai,
const namespacet &ns,
ai_domain_baset::edge_typet /*edge_type*/) final override
void
transform(locationt from, locationt to, ai_baset &ai, const namespacet &ns)
final override
{
// assert(reachable);

Expand Down
Loading