Skip to content

Reachability slicer: split cfg walks into two phases #3218

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

Reachability slicer: split cfg walks into two phases #3218

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
a9363da
Reachability slicer: split cfg walks into two phases
smowton Oct 12, 2018
0d8e3c1
Constify slicing_criteriont::operator()
smowton Oct 23, 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
23 changes: 23 additions & 0 deletions regression/cbmc/reachability-slice-interproc2/main.c
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,23 @@
void b();

void c()
{
__CPROVER_assert(0, "");
b();
}

void b()
{
a();
c();
}

void a()
{
c();
}

int main()
{
a();
}
8 changes: 8 additions & 0 deletions regression/cbmc/reachability-slice-interproc2/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,8 @@
CORE
main.c
--reachability-slice --show-goto-functions
^EXIT=0$
^SIGNAL=0$
main\(\)
--
^warning: ignoring
Copy link
Member

Choose a reason for hiding this comment

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

Can you check that b is not in the slice?

Copy link
Contributor Author

Choose a reason for hiding this comment

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

No, it is in the slice, since it calls c.

Copy link
Member

Choose a reason for hiding this comment

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

Ah, I see, the forward walk is not used in the way I assumed.

Copy link
Member

Choose a reason for hiding this comment

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

Is there a test that actually slices away something?

Copy link
Contributor Author

Choose a reason for hiding this comment

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

The original cbmc/reachability-slice has two tests looking for slicing. These new ones were particularly looking for over-slicing since that's the bug @polgreen / @tautschnig encountered.

19 changes: 19 additions & 0 deletions regression/cbmc/reachability-slice-interproc3/main.c
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,19 @@
void intermediate();
void root();

int main()
{
intermediate();
return 1;
}

void intermediate()
{
root();
}

void root()
{
__CPROVER_assert(0, "");
intermediate();
}
8 changes: 8 additions & 0 deletions regression/cbmc/reachability-slice-interproc3/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,8 @@
CORE
main.c
--reachability-slice-fb --show-goto-functions
^EXIT=0$
^SIGNAL=0$
main#return_value = 1;
--
^warning: ignoring
4 changes: 2 additions & 2 deletions src/goto-instrument/full_slicer.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -284,7 +284,7 @@ static bool implicit(goto_programt::const_targett target)
void full_slicert::operator()(
goto_functionst &goto_functions,
const namespacet &ns,
slicing_criteriont &criterion)
const slicing_criteriont &criterion)
{
// build the CFG data structure
cfg(goto_functions);
Expand Down Expand Up @@ -367,7 +367,7 @@ void full_slicert::operator()(
void full_slicer(
goto_functionst &goto_functions,
const namespacet &ns,
slicing_criteriont &criterion)
const slicing_criteriont &criterion)
{
full_slicert()(goto_functions, ns, criterion);
}
Expand Down
4 changes: 2 additions & 2 deletions src/goto-instrument/full_slicer.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -33,12 +33,12 @@ class slicing_criteriont
{
public:
virtual ~slicing_criteriont();
virtual bool operator()(goto_programt::const_targett)=0;
virtual bool operator()(goto_programt::const_targett) const = 0;
};

void full_slicer(
goto_functionst &goto_functions,
const namespacet &ns,
slicing_criteriont &criterion);
const slicing_criteriont &criterion);

#endif // CPROVER_GOTO_INSTRUMENT_FULL_SLICER_H
8 changes: 4 additions & 4 deletions src/goto-instrument/full_slicer_class.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -41,7 +41,7 @@ class full_slicert
void operator()(
goto_functionst &goto_functions,
const namespacet &ns,
slicing_criteriont &criterion);
const slicing_criteriont &criterion);

protected:
struct cfg_nodet
Expand Down Expand Up @@ -107,7 +107,7 @@ class full_slicert
class assert_criteriont:public slicing_criteriont
{
public:
virtual bool operator()(goto_programt::const_targett target)
virtual bool operator()(goto_programt::const_targett target) const
{
return target->is_assert();
}
Expand All @@ -121,7 +121,7 @@ class in_function_criteriont : public slicing_criteriont
{
}

virtual bool operator()(goto_programt::const_targett target)
virtual bool operator()(goto_programt::const_targett target) const
{
return target->function == target_function;
}
Expand All @@ -139,7 +139,7 @@ class properties_criteriont:public slicing_criteriont
{
}

virtual bool operator()(goto_programt::const_targett target)
virtual bool operator()(goto_programt::const_targett target) const
{
if(!target->is_assert())
return false;
Expand Down
Loading