Single-path symex checker [blocks: #3976] #3969

peterschrammel · 2019-01-27T23:16:56Z

Implements the --paths variant of using goto-symex.

Each commit message has a non-empty body, explaining why the change was made.
Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
My commit message includes data points confirming performance improvements (if claimed).
My PR is restricted to a single feature or bugfix.
White-space or formatting changes outside the feature-related changed lines are in commits of their own.

allredj

🚫
This PR failed Diffblue compatibility checks (cbmc commit: 0420c96).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/98863639
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).

The incompatibility may have been introduced by an earlier PR. In that case merging this
PR should be avoided unless it fixes the current incompatibility.

allredj

✔️
Passed Diffblue compatibility checks (cbmc commit: f94473b).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/99520817

tautschnig · 2019-02-02T16:41:06Z

src/goto-checker/bmc_util.h

@@ -69,6 +69,12 @@ void slice(
  const optionst &,
  ui_message_handlert &);

+void output_coverage_report(


Documentation would be appreciated. I think the cov_out parameter is the one needing it the most, notably the aspect that an empty string will mean that nothing happens. How about:

/// Output a coverage report as generated by \ref symex_coveraget if \p cov_out is non-empty. /// \param cov_out: file to write the report to; no report is generated if this is empty /// \param goto_model: goto model to build the coverage report for /// \param symex: symbolic execution run to report coverage for /// \param ui_message_handler: status/warning message handler

tautschnig · 2019-02-02T16:47:49Z

src/goto-checker/bmc_util.cpp

+{
+  // add a partial ordering, if required
+  // We won't be able to decide any properties by adding this,
+  // but we'd like to see the entire SSA.


Does this comment still make sense? I recall requesting it, but now that this is more generic I don't think it's appropriate anymore.

tautschnig · 2019-02-02T16:49:12Z

src/goto-checker/bmc_util.cpp

+    return goto_model.get_goto_function(id);
+  };
+
+  // perform symbolic execution


Comments don't always add value: I think it's pretty clear what the next line does, and this just makes it sound like something surprising would happen?

tautschnig · 2019-02-02T16:54:13Z

src/goto-checker/bmc_util.cpp

+    [&goto_model](
+      const irep_idt &id) -> const goto_functionst::goto_functiont & {
+    return goto_model.get_goto_function(id);
+  };


Should we maybe tweak the goto_symext interface a bit? Looking at get_function_from_goto_functions (symex_main.cpp) we now define this helper function multiple times.

tautschnig · 2019-02-02T16:56:29Z

src/goto-checker/bmc_util.cpp

@@ -336,3 +336,25 @@ void perform_symex(

  postprocess_equation(symex, equation, options, ns, ui_message_handler);
 }
+
+void perform_symex(


I'm confused. It seems two commits now introduce the same. They actually do, the lines above already contain the same code.

Yes, that's exactly the problem. The goto-symex interface is broken in this respect. We should have a function that returns a path_storaget::patht for the initial state at the entry point; and then we can resume from that... and everything becomes nice and uniform.

That should be fixable?

Yes, but I'll go ahead with the current version for now and clean up the goto-symex interface later this week. #4071

tautschnig · 2019-02-02T17:17:22Z

src/goto-checker/Makefile

@@ -7,6 +7,7 @@ SRC = bmc_util.cpp \
      goto_verifier.cpp \
      multi_path_symex_checker.cpp \
      multi_path_symex_only_checker.cpp \
+      single_path_symex_only_checker.cpp \


Lexicographic sorting, please. Applies again in a later commit (introducing single_path_symex_checker.cpp).

tautschnig · 2019-02-02T17:18:59Z

src/cbmc/cbmc_parse_options.cpp

+        options, ui_message_handler, goto_model);
+    }
+
+    (void)(*verifier)();


Seems like an unnecessary dance, can't we just run each of them in the branches above?

tautschnig · 2019-02-02T17:20:45Z

src/cbmc/cbmc_parse_options.cpp

    }
+
+    (void)(*verifier)();


Again, seems unnecessary. Just call each of them in the branches above.

tautschnig · 2019-02-02T17:22:25Z

jbmc/src/jbmc/jbmc_parse_options.cpp

      }
+
+      (void)(*verifier)();


Just call each of them in the branches above.

tautschnig · 2019-02-02T17:22:37Z

jbmc/src/jbmc/jbmc_parse_options.cpp

+          options, ui_message_handler, goto_model);
+      }
+
+      (void)(*verifier)();


Just call each of them.

As introduced into bmct in eb0b86b.

Allows us to remove set_message_handler() calls on solvers in other parts of the code.

Reduces code duplication across goto checkers.

Better provide it as a utility than hiding it inside a class. Reduces code duplication across goto checkers.

Copied from bmct. Going to be used by single_path_symex_checkert.

Utility function to set all UNKNOWN properties to PASS when the verification algorithm has finished. Corresponds to the current behaviour of CBMC replying 'successful' when the given bounds have been reached.

Provides functionality close to solvers/prop/cover_goals but without callbacks. It allows us to iteratively get all counterexamples for a set of properties on a fixed equation. This is used as a component by multi-path and single-path symex checkers.

Replaces the path_explorert variant of bmct. The current implementation of this is overly complicated because path_explorert distinguishes the first run of goto-symex from the following ones. To drastically simplify the code goto-symex/symex_bmc needs to be refactored so that all runs can be handled uniformly (e.g. push entry point into work list and then 'resume' from there). See also single_path_symex_checkert.

We can now use single_path_symex_only_checkert instead of bmct.

Extends single_path_symex_only_checkert with calling the solver and returning traces.

We can now use single_path_symex_checkert instead of bmct.

JBMC requires further setup of symex_bmct.

We can now use single_path_symex_checkert instead of bmct.

allredj

✔️
Passed Diffblue compatibility checks (cbmc commit: 1f9f475).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/99702092

peterschrammel added work in progress do not review dependent - do not merge Goto-checker labels Jan 27, 2019

peterschrammel self-assigned this Jan 27, 2019

peterschrammel requested review from cesaro, chrisr-diffblue, cristina-david, kroening, NathanJPhillips, pkesseli, smowton, tautschnig and thk123 as code owners January 27, 2019 23:16

peterschrammel force-pushed the single-path-symex-checker branch from 08989a3 to b59a98e Compare January 28, 2019 14:29

peterschrammel changed the title ~~[WIP] Single-path symex checker [depends: 3796]~~ [WIP] Single-path symex checker [depends: 3968] Jan 28, 2019

peterschrammel force-pushed the single-path-symex-checker branch 2 times, most recently from b9af1f9 to 0420c96 Compare January 28, 2019 17:37

allredj reviewed Jan 28, 2019

View reviewed changes

peterschrammel mentioned this pull request Jan 28, 2019

Make tests pass with single-path symbolic execution [depends-on: #3969, blocks: #3976] #3960

Closed

3 tasks

peterschrammel removed do not review work in progress labels Jan 29, 2019

peterschrammel changed the title ~~[WIP] Single-path symex checker [depends: 3968]~~ Single-path symex checker [depends: 3968] Jan 29, 2019

tautschnig changed the title ~~Single-path symex checker [depends: 3968]~~ Single-path symex checker [depends-on: #3968, blocks: #3976] Feb 1, 2019

tautschnig added the blocker label Feb 1, 2019

peterschrammel changed the title ~~Single-path symex checker [depends-on: #3968, blocks: #3976]~~ Single-path symex checker [blocks: #3976] Feb 1, 2019

peterschrammel force-pushed the single-path-symex-checker branch from 0420c96 to f94473b Compare February 2, 2019 15:13

peterschrammel removed the dependent - do not merge label Feb 2, 2019

allredj reviewed Feb 2, 2019

View reviewed changes

tautschnig approved these changes Feb 2, 2019

View reviewed changes

tautschnig assigned smowton Feb 2, 2019

smowton approved these changes Feb 4, 2019

View reviewed changes

peterschrammel mentioned this pull request Feb 4, 2019

Refactor handling of entry point in goto-symex #4071

Closed

peterschrammel force-pushed the single-path-symex-checker branch from f94473b to e9a0a6f Compare February 4, 2019 16:33

peterschrammel added 11 commits February 4, 2019 18:31

Add SSA validation

26bbcc6

As introduced into bmct in eb0b86b.

Set message handler in solver factory

cbcff00

Allows us to remove set_message_handler() calls on solvers in other parts of the code.

Use in,out for in/out params in doxygen

36ef9ee

Factor out output_coverage_report into bmc_util

6ca7fbf

Reduces code duplication across goto checkers.

Factor out perform_symex into bmc_util

0be41fb

Better provide it as a utility than hiding it inside a class. Reduces code duplication across goto checkers.

Add perform_symex for resuming from state

23150a4

Copied from bmct. Going to be used by single_path_symex_checkert.

Set final status of UNKNOWN properties

8f7ffc4

Utility function to set all UNKNOWN properties to PASS when the verification algorithm has finished. Corresponds to the current behaviour of CBMC replying 'successful' when the given bounds have been reached.

Use goto verifier for --paths with show-vcc and -program-only in CBMC

258b7a9

We can now use single_path_symex_only_checkert instead of bmct.

Add single-path symex checker

a588d80

Extends single_path_symex_only_checkert with calling the solver and returning traces.

peterschrammel force-pushed the single-path-symex-checker branch from e9a0a6f to 96fec16 Compare February 4, 2019 18:31

peterschrammel added 3 commits February 4, 2019 21:54

Use goto verifier for --paths in CBMC

fbaa9ea

We can now use single_path_symex_checkert instead of bmct.

Single-path goto checker for Java requires preprocessing

8f3f02c

JBMC requires further setup of symex_bmct.

Use goto verifier for --paths in JBMC

1f9f475

We can now use single_path_symex_checkert instead of bmct.

peterschrammel force-pushed the single-path-symex-checker branch from 96fec16 to 1f9f475 Compare February 4, 2019 21:54

peterschrammel merged commit 4315c29 into diffblue:develop Feb 4, 2019

peterschrammel deleted the single-path-symex-checker branch February 4, 2019 23:00

allredj reviewed Feb 4, 2019

View reviewed changes

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Single-path symex checker [blocks: #3976] #3969

Single-path symex checker [blocks: #3976] #3969

peterschrammel commented Jan 27, 2019 •

edited

Loading

allredj left a comment

allredj left a comment

tautschnig Feb 2, 2019

tautschnig Feb 2, 2019

tautschnig Feb 2, 2019

tautschnig Feb 2, 2019

tautschnig Feb 2, 2019

peterschrammel Feb 2, 2019 •

edited

Loading

tautschnig Feb 2, 2019

peterschrammel Feb 4, 2019

tautschnig Feb 2, 2019

tautschnig Feb 2, 2019

tautschnig Feb 2, 2019

tautschnig Feb 2, 2019

tautschnig Feb 2, 2019

allredj left a comment

Single-path symex checker [blocks: #3976] #3969

Single-path symex checker [blocks: #3976] #3969

Conversation

peterschrammel commented Jan 27, 2019 • edited Loading

allredj left a comment

Choose a reason for hiding this comment

allredj left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

peterschrammel Feb 2, 2019 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

allredj left a comment

Choose a reason for hiding this comment

peterschrammel commented Jan 27, 2019 •

edited

Loading

peterschrammel Feb 2, 2019 •

edited

Loading