Upstream slice functions #2758

nmanthey · 2018-08-20T06:50:15Z

This change allows to slice based on functions remaining reachable. This slicing allows to reduce the search space to a user chosen subset of the prorgam.

kroening · 2018-08-20T07:31:20Z

(I'll get someone to produce a set of tests)

nmanthey · 2018-08-20T18:45:07Z

I can certainly add a test case here, I just learned from #2748 that I can show the goto-program to compare it in the test case.

xbauch · 2018-09-26T14:27:54Z

3 small fixes:

option parser ignored colon-separated list
running slicer multiple times broke an invariant about end-function nodes
on test was called with wrong options

smowton · 2018-09-27T08:47:00Z

regression/goto-instrument/fp-reachability-slice1/test.desc

+--fp-reachability-slice c
+^EXIT=0$
+^SIGNAL=0$
+--


This is a bit easy to pass at the moment, especially if the precise pretty-printing of "dead f" were to change. Suggest adding some positive requirements too, to make the test more robust.

smowton · 2018-09-27T08:47:16Z

regression/goto-instrument/fp-reachability-slice2/test.desc

+--fp-reachability-slice a,c
+^EXIT=0$
+^SIGNAL=0$
+dead d;


(for comparison, this is better)

smowton · 2018-09-27T08:47:32Z

regression/goto-instrument/fp-reachability-slice3/test.desc

+main.c
+--fp-reachability-slice b,c
+^EXIT=0$
+^SIGNAL=0$


No meaningful positive conditions

smowton · 2018-09-27T08:49:41Z

src/goto-instrument/reachability_slicer.cpp

-        stack.emplace_back(edge.first, true);
-        stack.emplace_back(
-          cfg.entry_map[std::prev(node.PC)], caller_is_known);
+        if(std::prev(node.PC)->is_function_call())


Comment about when this might be false?

It really shouldn't happen, but something broke in the slicer during multiple calls and the cfg-predecessor of a successor-of-callsite was not a function call. Now that a new slicer is created it does not happen, so I replaced it back with the original invariant.

smowton · 2018-09-27T08:51:10Z

src/goto-instrument/reachability_slicer.cpp

        if(
          !e.reaches_assertion && !e.reachable_from_assertion &&
          !i_it->is_end_function())
          i_it->make_assumption(false_exprt());
+        e.reaches_assertion = e.reachable_from_assertion = false;


Comment in-inline about why these are reset here?

(It looks like the slicer might be run more than once, in which case perhaps it should be reset before use, rather than upon executing the transformation?)

It seems that slicer is not really supposed to be called multiple times; or it would require a much more thorough resetting that just the reachability flags. I changed the code to build a new slicer before every call.

smowton · 2018-09-27T08:51:26Z

src/goto-instrument/reachability_slicer.cpp

+  goto_modelt &goto_model,
+  const std::string &functions_list)
+{
+  reachability_slicert s;


This (and the following) were renamed as suggested. Thanks.

smowton · 2018-09-27T08:51:42Z

src/goto-instrument/reachability_slicer.cpp

+{
+  reachability_slicert s;
+
+  std::istringstream multiple_functions(functions_list);


multiple_functions->functions_stream?

smowton · 2018-09-27T08:52:03Z

src/goto-instrument/reachability_slicer.cpp

+  std::string single_function;
+  while(std::getline(multiple_functions, single_function, ','))
+  {
+    in_function_criteriont p(single_function);


p->matching_criterion?

kroening · 2018-09-27T10:57:56Z

This is nearly there; it needs a bit of commit squashing, i.e., the tests should come with the code that is tested.

smowton

Thanks for the prompt fixes!

This criterion marks all instructions of a given function as slicer starting point. This is useful when the slicing does not aim at properties, but path that hit a certain function.

This slicer keeps any function in the program, in case it is backward or forward reachable from the target function. The analysis can be repeated for multiple functions. Note: This implementation cannot deal with order of function calls, e.g. if functions a,b and c should be kept, then a path that has a, which calls c, which calls b will also be kept. However, path where not all functions will be called, will be dropped.

allredj

This PR failed Diffblue compatibility checks (cbmc commit: ed85c7f).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/86137585
Status will be re-evaluated on next push.
Please contact @peterschrammel, @thk123, or @allredj for support.

Common spurious failures:

the cbmc commit has disappeared in the mean time (e.g. in a force-push)
the author is not in the list of contributors (e.g. first-time contributors).

peterschrammel

A couple of nitpicks

peterschrammel · 2018-09-27T16:38:12Z

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -1610,6 +1619,9 @@ void goto_instrument_parse_optionst::help()
    " --render-cluster-function    clusterises the dot by functions\n"
    "\n"
    "Slicing:\n"
+    " --fp-reachability-slice <f>  remove instructions that cannot appear on a\n" // NOLINT(*)


--fp-reachability-slice f
The list of functions has to be given as a comma-separated list f.

Shouldn't this use HELP_REACHABILITY_SLICER from below?

It seems that this help macro is for CBMC options, e.g. --reachability-slice-fb is not a valid option for goto-instrument.

peterschrammel · 2018-09-27T16:42:46Z

src/goto-instrument/reachability_slicer.cpp

+{
+  std::istringstream functions_stream(functions_list);
+  std::string single_function;
+  while(std::getline(functions_stream, single_function, ','))


It would be better to provide the splitting as a list<string> cmdlinet::get_comma_separated_values(string) function.

peterschrammel · 2018-09-27T16:46:14Z

src/goto-instrument/reachability_slicer.h

+
+#define HELP_REACHABILITY_SLICER                                               \
+  " --fp-reachability-slice <f>  remove instructions that cannot appear on a " \
+  "trace that visits all given functions. The list of functions has to be "    \


The text help text should be broken after 80 chars and properly aligned (e.g. trace should start below remove).

peterschrammel · 2018-09-27T16:46:48Z

src/goto-instrument/reachability_slicer.cpp

+/// Perform reachability slicing on goto_model for selected functions.
+/// \param goto_model Goto program to slice
+/// \param functions_list The functions relevant for the slicing (i.e. starting
+/// point for the search in the cfg). Anything that is reachable in the CFG


allredj

This PR failed Diffblue compatibility checks (cbmc commit: bfe3dd2).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/86266130
Status will be re-evaluated on next push.
Please contact @peterschrammel, @thk123, or @allredj for support.

Common spurious failures:

the cbmc commit has disappeared in the mean time (e.g. in a force-push)
the author is not in the list of contributors (e.g. first-time contributors).

peterschrammel · 2018-10-01T15:39:45Z

src/goto-instrument/reachability_slicer.h

+
+#define HELP_REACHABILITY_SLICER                                               \
+  " --fp-reachability-slice f    remove instructions that cannot appear on a " \
+  "trace\n                              that visits all given functions. The " \


The layout looks a bit odd. Since clang-format is already off for this section, I'm sure you can make this nicer manually.

This commit adds the command line argument handling for the function path slicer. To keep all possible exeuction traces that hit both function a and b, an example invocation could look as follows: goto-instrument --fp-reachability-slice a,b input output Note, any trace that touches only a, but not b, will not be kept in the program.

allredj

Passed Diffblue compatibility checks (cbmc commit: d86701c).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/86571560

nmanthey requested review from chrisr-diffblue, martin-cs and peterschrammel as code owners August 20, 2018 06:50

kroening approved these changes Aug 20, 2018

View reviewed changes

nmanthey force-pushed the upstream-slice-functions branch from f9edad3 to 392cdf5 Compare August 22, 2018 07:45

nmanthey force-pushed the upstream-slice-functions branch from 392cdf5 to 19f303a Compare September 11, 2018 07:28

nmanthey requested review from pkesseli, smowton and tautschnig as code owners September 26, 2018 14:20

xbauch force-pushed the upstream-slice-functions branch from 78cabc8 to 3091abd Compare September 26, 2018 15:14

smowton reviewed Sep 27, 2018

View reviewed changes

smowton approved these changes Sep 27, 2018

View reviewed changes

Petr Bauch added 2 commits September 27, 2018 12:24

slicer: add function slicer criterion

92793ca

This criterion marks all instructions of a given function as slicer starting point. This is useful when the slicing does not aim at properties, but path that hit a certain function.

xbauch force-pushed the upstream-slice-functions branch from 424e30e to ed85c7f Compare September 27, 2018 11:27

allredj reviewed Sep 27, 2018

View reviewed changes

peterschrammel reviewed Sep 27, 2018

View reviewed changes

allredj reviewed Sep 28, 2018

View reviewed changes

peterschrammel approved these changes Oct 1, 2018

View reviewed changes

xbauch force-pushed the upstream-slice-functions branch from bfe3dd2 to d86701c Compare October 2, 2018 07:42

xbauch merged commit 744f918 into diffblue:develop Oct 2, 2018

allredj reviewed Oct 2, 2018

View reviewed changes

Upstream slice functions #2758

Upstream slice functions #2758

Uh oh!

Conversation

nmanthey commented Aug 20, 2018

Uh oh!

kroening commented Aug 20, 2018

Uh oh!

nmanthey commented Aug 20, 2018

Uh oh!

xbauch commented Sep 26, 2018

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

kroening commented Sep 27, 2018

Uh oh!

smowton left a comment

Choose a reason for hiding this comment

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

peterschrammel left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!