Skip to content

Dependency graph fix #420

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 2 commits into from
Jan 17, 2017
Merged

Dependency graph fix #420

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
7b899e8
AI framework fix
danpoe Jan 13, 2017
eef9570
Dependence graph fix
danpoe Jan 13, 2017
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
18 changes: 18 additions & 0 deletions regression/goto-instrument/dependence-graph1/main.c
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,18 @@

int x;

void func()
{
int r;

r = x;
}

int main()
{
x = 1;
func();

return 0;
}

7 changes: 7 additions & 0 deletions regression/goto-instrument/dependence-graph1/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,7 @@
CORE
main.c
--show-dependence-graph
^EXIT=0$
^SIGNAL=0$
--
^warning: ignoring
7 changes: 4 additions & 3 deletions src/analyses/ai.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -499,10 +499,11 @@ void ai_baset::sequential_fixedpoint(
const goto_functionst &goto_functions,
const namespacet &ns)
{
// do each function at least once
goto_functionst::function_mapt::const_iterator
f_it=goto_functions.function_map.find(goto_functions.entry_point());

forall_goto_functions(it, goto_functions)
fixedpoint(it->second.body, goto_functions, ns);
if(f_it!=goto_functions.function_map.end())
fixedpoint(f_it->second.body, goto_functions, ns);
Copy link
Collaborator

Choose a reason for hiding this comment

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

How does this change relate to the commit message?

Copy link
Contributor Author

Choose a reason for hiding this comment

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

Ah right. This is a general framework fix as it does not make sense to run the fixpoint on other functions when we don't set the entry state (as discussed with @peterschrammel). Should I make a separate commit or pull request for that?

Copy link
Collaborator

Choose a reason for hiding this comment

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

Apologies for the major delay: Yes, please do move this into a separate commit as it could be contentious for cases where the entry function isn't available (it's not clear to me whether running abstract interpretation considering each function a possible entry point is actually a bad idea).

Copy link
Contributor Author

Choose a reason for hiding this comment

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

I think it would be a useful new feature actually. The existing code though seemed to be a remaining hack from when bottom could be a state of a reachable location.

}

/*******************************************************************\
Expand Down
11 changes: 9 additions & 2 deletions src/analyses/dependence_graph.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -94,14 +94,20 @@ class dep_graph_domaint:public ai_domain_baset

void make_top() final override
{
assert(node_id!=std::numeric_limits<node_indext>::max());

has_values=tvt(true);
node_id=std::numeric_limits<node_indext>::max();
control_deps.clear();
data_deps.clear();
}

void make_bottom() final override
{
assert(node_id!=std::numeric_limits<node_indext>::max());

has_values=tvt(false);
node_id=std::numeric_limits<node_indext>::max();
control_deps.clear();
data_deps.clear();
}

void make_entry() final override
Expand Down Expand Up @@ -161,6 +167,7 @@ class dependence_grapht:

void initialize(const goto_programt &goto_program)
{
ait<dep_graph_domaint>::initialize(goto_program);
post_dominators(goto_program);
}

Expand Down