Skip to content

static_analysist now passes function identifiers to transform() #3130

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
Oct 10, 2018
Merged

static_analysist now passes function identifiers to transform() #3130

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
88 changes: 66 additions & 22 deletions src/analyses/static_analysis.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -66,11 +66,12 @@ void static_analysis_baset::operator()(
}

void static_analysis_baset::operator()(
const irep_idt &function_identifier,
const goto_programt &goto_program)
{
initialize(goto_program);
goto_functionst goto_functions;
fixedpoint(goto_program, goto_functions);
fixedpoint(function_identifier, goto_program, goto_functions);
}

void static_analysis_baset::output(
Expand Down Expand Up @@ -166,6 +167,7 @@ static_analysis_baset::locationt static_analysis_baset::get_next(
}

bool static_analysis_baset::fixedpoint(
const irep_idt &function_identifier,
const goto_programt &goto_program,
const goto_functionst &goto_functions)
{
Expand All @@ -184,14 +186,15 @@ bool static_analysis_baset::fixedpoint(
{
locationt l=get_next(working_set);

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

return new_data;
}

bool static_analysis_baset::visit(
const irep_idt &function_identifier,
locationt l,
working_sett &working_set,
const goto_programt &goto_program,
Expand Down Expand Up @@ -220,14 +223,17 @@ bool static_analysis_baset::visit(
to_code_function_call(l->code);

do_function_call_rec(
l, to_l,
function_identifier,
l,
to_l,
code.function(),
code.arguments(),
new_values,
goto_functions);
}
else
new_values.transform(ns, l, to_l);
new_values.transform(
ns, function_identifier, l, function_identifier, to_l);

statet &other=get_state(to_l);

Expand All @@ -245,7 +251,9 @@ bool static_analysis_baset::visit(
}

void static_analysis_baset::do_function_call(
locationt l_call, locationt l_return,
const irep_idt &calling_function,
locationt l_call,
locationt l_return,
const goto_functionst &goto_functions,
const goto_functionst::function_mapt::const_iterator f_it,
const exprt::operandst &,
Expand All @@ -264,7 +272,7 @@ void static_analysis_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(new_state));
tmp_state->transform(ns, l_call, l_begin);
tmp_state->transform(ns, calling_function, l_call, f_it->first, l_begin);

statet &begin_state=get_state(l_begin);

Expand All @@ -286,7 +294,7 @@ void static_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);
}
}

Expand All @@ -301,7 +309,7 @@ void static_analysis_baset::do_function_call(
// do edge from end of function to instruction after call
std::unique_ptr<statet> tmp_state(
make_temporary_state(end_of_function));
tmp_state->transform(ns, l_end, l_return);
tmp_state->transform(ns, f_it->first, l_end, calling_function, l_return);

// propagate those -- not exceedingly precise, this is,
// as still it contains all the state from the
Expand All @@ -311,12 +319,15 @@ void static_analysis_baset::do_function_call(

{
// effect on current procedure (if any)
new_state.transform(ns, l_call, l_return);
new_state.transform(
ns, calling_function, l_call, calling_function, l_return);
}
}

void static_analysis_baset::do_function_call_rec(
locationt l_call, locationt l_return,
const irep_idt &calling_function,
locationt l_call,
locationt l_return,
const exprt &function,
const exprt::operandst &arguments,
statet &new_state,
Expand Down Expand Up @@ -345,7 +356,9 @@ void static_analysis_baset::do_function_call_rec(
throw "failed to find function "+id2string(identifier);

do_function_call(
l_call, l_return,
calling_function,
l_call,
l_return,
goto_functions,
it,
arguments,
Expand All @@ -361,14 +374,18 @@ void static_analysis_baset::do_function_call_rec(
std::unique_ptr<statet> n2(make_temporary_state(new_state));

do_function_call_rec(
l_call, l_return,
calling_function,
l_call,
l_return,
function.op1(),
arguments,
new_state,
goto_functions);

do_function_call_rec(
l_call, l_return,
calling_function,
l_call,
l_return,
function.op2(),
arguments,
*n2,
Expand All @@ -392,7 +409,13 @@ void static_analysis_baset::do_function_call_rec(
const object_descriptor_exprt &o=to_object_descriptor_expr(value);
std::unique_ptr<statet> n2(make_temporary_state(new_state));
do_function_call_rec(
l_call, l_return, o.object(), arguments, *n2, goto_functions);
calling_function,
l_call,
l_return,
o.object(),
arguments,
*n2,
goto_functions);
merge(new_state, *n2, l_return);
}
}
Expand Down Expand Up @@ -424,7 +447,7 @@ void static_analysis_baset::sequential_fixedpoint(

forall_goto_functions(it, goto_functions)
if(functions_done.insert(it->first).second)
fixedpoint(it->second.body, goto_functions);
fixedpoint(it->first, it->second.body, goto_functions);
}

void static_analysis_baset::concurrent_fixedpoint(
Expand All @@ -442,16 +465,32 @@ void static_analysis_baset::concurrent_fixedpoint(
generate_state(sh_target);
statet &shared_state=get_state(sh_target);

typedef std::list<std::pair<goto_programt const*,
goto_programt::const_targett> > thread_wlt;
struct wl_entryt
{
wl_entryt(
const irep_idt &_function_identifier,
const goto_programt &_goto_program,
locationt _location)
: function_identifier(_function_identifier),
goto_program(&_goto_program),
location(_location)
{
}

irep_idt function_identifier;
const goto_programt *goto_program;
locationt location;
};

typedef std::list<wl_entryt> thread_wlt;
thread_wlt thread_wl;

forall_goto_functions(it, goto_functions)
forall_goto_program_instructions(t_it, it->second.body)
{
if(is_threaded(t_it))
{
thread_wl.push_back(std::make_pair(&(it->second.body), t_it));
thread_wl.push_back(wl_entryt(it->first, it->second.body, t_it));

goto_programt::const_targett l_end=
it->second.body.instructions.end();
Expand All @@ -472,16 +511,21 @@ void static_analysis_baset::concurrent_fixedpoint(
for(const auto &thread : thread_wl)
{
working_sett working_set;
put_in_working_set(working_set, thread.second);
put_in_working_set(working_set, thread.location);

statet &begin_state=get_state(thread.second);
merge(begin_state, shared_state, thread.second);
statet &begin_state = get_state(thread.location);
merge(begin_state, shared_state, thread.location);

while(!working_set.empty())
{
goto_programt::const_targett l=get_next(working_set);

visit(l, working_set, *thread.first, goto_functions);
visit(
thread.function_identifier,
l,
working_set,
*thread.goto_program,
goto_functions);

// the underlying domain must make sure that the final state
// carries all possible values; otherwise we would need to
Expand Down
15 changes: 12 additions & 3 deletions src/analyses/static_analysis.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -58,8 +58,10 @@ class domain_baset

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

virtual void output(
const namespacet &,
Expand Down Expand Up @@ -130,6 +132,7 @@ class static_analysis_baset
virtual void update(const goto_functionst &goto_functions);

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

virtual void operator()(
Expand Down Expand Up @@ -193,6 +196,7 @@ class static_analysis_baset

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

Expand All @@ -206,6 +210,7 @@ class static_analysis_baset

// true = found something new
bool visit(
const irep_idt &function_identifier,
locationt l,
working_sett &working_set,
const goto_programt &goto_program,
Expand Down Expand Up @@ -237,14 +242,18 @@ class static_analysis_baset

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

void do_function_call(
locationt l_call, locationt l_return,
const irep_idt &calling_function,
locationt l_call,
locationt l_return,
const goto_functionst &goto_functions,
const goto_functionst::function_mapt::const_iterator f_it,
const exprt::operandst &arguments,
Expand Down
2 changes: 2 additions & 0 deletions src/pointer-analysis/value_set_domain.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -47,7 +47,9 @@ class value_set_domain_templatet:public domain_baset

virtual void transform(
const namespacet &ns,
const irep_idt &function_from,
locationt from_l,
const irep_idt &function_to,
locationt to_l);

virtual void get_reference_set(
Expand Down
4 changes: 3 additions & 1 deletion src/pointer-analysis/value_set_domain_transform.inc
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -16,7 +16,9 @@ Author: Daniel Kroening, kroening@kroening.com
template<class VST>
void value_set_domain_templatet<VST>::transform(
const namespacet &ns,
const irep_idt &function_from,
locationt from_l,
const irep_idt &function_to,
locationt to_l)
{
switch(from_l->type)
Expand Down Expand Up @@ -51,7 +53,7 @@ void value_set_domain_templatet<VST>::transform(
to_code_function_call(from_l->code);

value_set.do_function_call(
to_l->function, code.arguments(), ns);
function_to, code.arguments(), ns);
}
break;

Expand Down