Skip to content

value_sets now have function identifiers [blocks: #3126] #3865

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 1 commit into from
Jan 30, 2019
Merged

value_sets now have function identifiers [blocks: #3126] #3865

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
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
100 changes: 59 additions & 41 deletions src/analyses/flow_insensitive_analysis.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -53,12 +53,12 @@ void flow_insensitive_analysis_baset::operator()(
fixedpoint(goto_functions);
}

void flow_insensitive_analysis_baset::operator()(
const goto_programt &goto_program)
void flow_insensitive_analysis_baset::
operator()(const irep_idt &function_id, const goto_programt &goto_program)
{
initialize(goto_program);
goto_functionst goto_functions;
fixedpoint(goto_program, goto_functions);
fixedpoint(function_id, goto_program, goto_functions);
Copy link
Member

Choose a reason for hiding this comment

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

What are the goto_functions used for?

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

They are used to resolve function calls in do_function_call_rec (though in this case it will just fail to resolve any function calls). That said, I have cleaned up the patch so that this change doesn't even show up anymore, because it was only an artefact of reordering functions in the file.

}

void flow_insensitive_analysis_baset::output(
Expand All @@ -69,14 +69,14 @@ void flow_insensitive_analysis_baset::output(
{
out << "////\n" << "//// Function: " << f_it->first << "\n////\n\n";

output(f_it->second.body, f_it->first, out);
output(f_it->first, f_it->second.body, out);
}
}

void flow_insensitive_analysis_baset::output(
const goto_programt &,
const irep_idt &,
std::ostream &out) const
const goto_programt &,
std::ostream &out)
{
get_state().output(ns, out);
}
Expand All @@ -99,6 +99,7 @@ flow_insensitive_analysis_baset::get_next(
}

bool flow_insensitive_analysis_baset::fixedpoint(
const irep_idt &function_id,
const goto_programt &goto_program,
const goto_functionst &goto_functions)
{
Expand All @@ -119,14 +120,15 @@ bool flow_insensitive_analysis_baset::fixedpoint(
{
locationt l=get_next(working_set);

if(visit(l, working_set, goto_program, goto_functions))
if(visit(function_id, l, working_set, goto_program, goto_functions))
new_data=true;
}

return new_data;
}

bool flow_insensitive_analysis_baset::visit(
const irep_idt &function_id,
locationt l,
working_sett &working_set,
const goto_programt &goto_program,
Expand Down Expand Up @@ -157,16 +159,16 @@ bool flow_insensitive_analysis_baset::visit(
// this is a big special case
const code_function_callt &code = to_code_function_call(l->code);

changed=
do_function_call_rec(
l,
code.function(),
code.arguments(),
get_state(),
goto_functions);
changed = do_function_call_rec(
function_id,
l,
code.function(),
code.arguments(),
get_state(),
goto_functions);
}
else
changed = get_state().transform(ns, l, to_l);
changed = get_state().transform(ns, function_id, l, function_id, to_l);

if(changed || !seen(to_l))
{
Expand All @@ -193,6 +195,7 @@ bool flow_insensitive_analysis_baset::visit(
}

bool flow_insensitive_analysis_baset::do_function_call(
const irep_idt &calling_function,
locationt l_call,
const goto_functionst &goto_functions,
const goto_functionst::function_mapt::const_iterator f_it,
Expand Down Expand Up @@ -221,9 +224,15 @@ bool flow_insensitive_analysis_baset::do_function_call(
t->location_number=1;

locationt l_next=l_call; l_next++;
bool new_data=state.transform(ns, l_call, r);
new_data = state.transform(ns, r, t) || new_data;
new_data = state.transform(ns, t, l_next) || new_data;
// do the edge from the call site to the simulated function (the artificial
// return statement that we just generated)
bool new_data =
state.transform(ns, calling_function, l_call, f_it->first, r);
// do the edge from the return to the artificial end-of-function
new_data = state.transform(ns, f_it->first, r, f_it->first, t) || new_data;
Copy link
Contributor

Choose a reason for hiding this comment

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

While you're editing this code, might be sensible to annotate these as "callsite -> head of function" and "callsite -> callsite successor" and so on, explaining the different function names we're passing in

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

Done.

// do edge from (artificial) end of function to instruction after call
new_data =
state.transform(ns, f_it->first, t, calling_function, l_next) || new_data;

return new_data;
}
Expand All @@ -240,7 +249,8 @@ bool flow_insensitive_analysis_baset::do_function_call(
l_begin->function == f_it->first, "function names have to match");

// do the edge from the call site to the beginning of the function
new_data=state.transform(ns, l_call, l_begin);
new_data =
state.transform(ns, calling_function, l_call, f_it->first, l_begin);

// do each function at least once
if(functions_done.find(f_it->first)==
Expand All @@ -254,7 +264,7 @@ bool flow_insensitive_analysis_baset::do_function_call(
if(new_data)
{
// recursive call
fixedpoint(goto_function.body, goto_functions);
fixedpoint(f_it->first, goto_function.body, goto_functions);
new_data=true; // could be reset by fixedpoint
}
}
Expand All @@ -268,13 +278,16 @@ bool flow_insensitive_analysis_baset::do_function_call(
// do edge from end of function to instruction after call
locationt l_next=l_call;
l_next++;
new_data = state.transform(ns, l_end, l_next) || new_data;
new_data =
state.transform(ns, f_it->first, l_end, calling_function, l_next) ||
new_data;
}

return new_data;
}

bool flow_insensitive_analysis_baset::do_function_call_rec(
const irep_idt &calling_function,
locationt l_call,
const exprt &function,
const exprt::operandst &arguments,
Expand All @@ -301,13 +314,8 @@ bool flow_insensitive_analysis_baset::do_function_call_rec(
if(it==goto_functions.function_map.end())
throw "failed to find function "+id2string(identifier);

new_data =
do_function_call(
l_call,
goto_functions,
it,
arguments,
state);
new_data = do_function_call(
calling_function, l_call, goto_functions, it, arguments, state);

recursion_set.erase(identifier);
}
Expand All @@ -316,12 +324,21 @@ bool flow_insensitive_analysis_baset::do_function_call_rec(
const auto &if_expr = to_if_expr(function);

new_data = do_function_call_rec(
l_call, if_expr.true_case(), arguments, state, goto_functions);
calling_function,
l_call,
if_expr.true_case(),
arguments,
state,
goto_functions);

new_data =
do_function_call_rec(
l_call, if_expr.false_case(), arguments, state, goto_functions) ||
new_data;
new_data = do_function_call_rec(
calling_function,
l_call,
if_expr.false_case(),
arguments,
state,
goto_functions) ||
new_data;
}
else if(function.id()==ID_dereference)
{
Expand All @@ -343,13 +360,14 @@ bool flow_insensitive_analysis_baset::do_function_call_rec(

if(it!=goto_functions.function_map.end())
{
new_data =
do_function_call_rec(
l_call,
o.object(),
arguments,
state,
goto_functions) || new_data;
new_data = do_function_call_rec(
calling_function,
l_call,
o.object(),
arguments,
state,
goto_functions) ||
new_data;
}
}
}
Expand Down Expand Up @@ -392,7 +410,7 @@ bool flow_insensitive_analysis_baset::fixedpoint(
const goto_functionst &goto_functions)
{
functions_done.insert(it->first);
return fixedpoint(it->second.body, goto_functions);
return fixedpoint(it->first, it->second.body, goto_functions);
}

void flow_insensitive_analysis_baset::update(const goto_functionst &)
Expand Down
23 changes: 11 additions & 12 deletions src/analyses/flow_insensitive_analysis.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -47,8 +47,10 @@ class flow_insensitive_abstract_domain_baset

virtual bool transform(
const namespacet &ns,
const irep_idt &function_from,
locationt from,
locationt to)=0;
const irep_idt &function_to,
locationt to) = 0;

virtual ~flow_insensitive_abstract_domain_baset()
{
Expand Down Expand Up @@ -126,8 +128,8 @@ class flow_insensitive_analysis_baset

virtual void update(const goto_functionst &goto_functions);

virtual void operator()(
const goto_programt &goto_program);
virtual void
operator()(const irep_idt &function_id, const goto_programt &goto_program);

virtual void operator()(
const goto_functionst &goto_functions);
Expand All @@ -146,20 +148,13 @@ class flow_insensitive_analysis_baset
std::ostream &out);

virtual void output(
const irep_idt &function_id,
const goto_programt &goto_program,
std::ostream &out)
{
output(goto_program, "", out);
}
std::ostream &out);

protected:
const namespacet &ns;

virtual void output(
const goto_programt &goto_program,
const irep_idt &identifier,
std::ostream &out) const;

typedef std::priority_queue<locationt> working_sett;

locationt get_next(working_sett &working_set);
Expand All @@ -173,6 +168,7 @@ class flow_insensitive_analysis_baset

// true = found something new
bool fixedpoint(
const irep_idt &function_id,
const goto_programt &goto_program,
const goto_functionst &goto_functions);

Expand All @@ -185,6 +181,7 @@ class flow_insensitive_analysis_baset

// true = found something new
bool visit(
const irep_idt &function_id,
locationt l,
working_sett &working_set,
const goto_programt &goto_program,
Expand All @@ -206,13 +203,15 @@ class flow_insensitive_analysis_baset

// function calls
bool do_function_call_rec(
const irep_idt &calling_function,
locationt l_call,
const exprt &function,
const exprt::operandst &arguments,
statet &new_state,
const goto_functionst &goto_functions);

bool do_function_call(
const irep_idt &calling_function,
locationt l_call,
const goto_functionst &goto_functions,
const goto_functionst::function_mapt::const_iterator f_it,
Expand Down
2 changes: 1 addition & 1 deletion src/analyses/goto_rw.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -626,7 +626,7 @@ void rw_range_set_value_sett::get_objects_dereference(
size);

exprt object=deref;
dereference(target, object, ns, value_sets);
dereference(function, target, object, ns, value_sets);

auto type_bits = pointer_offset_bits(object.type(), ns);

Expand Down
2 changes: 1 addition & 1 deletion src/goto-instrument/rw_set.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -159,7 +159,7 @@ void _rw_set_loct::read_write_rec(
read_write_rec(*it, r, w, suffix, guard);
}
#else
dereference(target, tmp, ns, value_sets);
dereference(function_id, target, tmp, ns, value_sets);

read_write_rec(tmp, r, w, suffix, guard);
#endif
Expand Down
5 changes: 3 additions & 2 deletions src/goto-symex/precondition.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -113,7 +113,8 @@ void preconditiont::compute_rec(exprt &dest)
// aliasing may happen here

value_setst::valuest expr_set;
value_sets.get_values(target, deref_expr.pointer(), expr_set);
value_sets.get_values(
SSA_step.source.function_id, target, deref_expr.pointer(), expr_set);
std::unordered_set<irep_idt> symbols;

for(value_setst::valuest::const_iterator
Expand All @@ -127,7 +128,7 @@ void preconditiont::compute_rec(exprt &dest)
// may alias!
exprt tmp;
tmp.swap(deref_expr.pointer());
dereference(target, tmp, ns, value_sets);
dereference(SSA_step.source.function_id, target, tmp, ns, value_sets);
deref_expr.swap(tmp);
compute_rec(deref_expr);
}
Expand Down
7 changes: 5 additions & 2 deletions src/pointer-analysis/goto_program_dereference.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -227,7 +227,7 @@ void goto_program_dereferencet::get_value_set(
const exprt &expr,
value_setst::valuest &dest)
{
value_sets.get_values(current_target, expr, dest);
value_sets.get_values(current_function, current_target, expr, dest);
}

/// Remove dereference expressions contained in `expr`.
Expand Down Expand Up @@ -357,9 +357,11 @@ void goto_program_dereferencet::dereference_instruction(

/// Set the current target to `target` and remove derefence from expr.
void goto_program_dereferencet::dereference_expression(
const irep_idt &function_id,
goto_programt::const_targett target,
exprt &expr)
{
current_function = function_id;
current_target=target;
#if 0
valid_local_variables=&target->local_variables;
Expand Down Expand Up @@ -448,6 +450,7 @@ void pointer_checks(
/// Remove dereferences in `expr` using `value_sets` to determine to what
/// objects the pointers may be pointing to.
void dereference(
const irep_idt &function_id,
goto_programt::const_targett target,
exprt &expr,
const namespacet &ns,
Expand All @@ -457,5 +460,5 @@ void dereference(
symbol_tablet new_symbol_table;
goto_program_dereferencet
goto_program_dereference(ns, new_symbol_table, options, value_sets);
goto_program_dereference.dereference_expression(target, expr);
goto_program_dereference.dereference_expression(function_id, target, expr);
}
3 changes: 3 additions & 0 deletions src/pointer-analysis/goto_program_dereference.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -52,6 +52,7 @@ class goto_program_dereferencet:protected dereference_callbackt
void pointer_checks(goto_functionst &goto_functions);

void dereference_expression(
const irep_idt &function_id,
goto_programt::const_targett target,
exprt &expr);

Expand Down Expand Up @@ -93,6 +94,7 @@ class goto_program_dereferencet:protected dereference_callbackt
#if 0
const std::set<irep_idt> *valid_local_variables;
#endif
irep_idt current_function;
goto_programt::const_targett current_target;

/// Unused
Expand All @@ -106,6 +108,7 @@ class goto_program_dereferencet:protected dereference_callbackt
};

void dereference(
const irep_idt &function_id,
goto_programt::const_targett target,
exprt &expr,
const namespacet &,
Expand Down
Loading