Rip out the heart of bmct [depends: 3557, blocks: 3578, 3580, 3581] #3565

peterschrammel · 2018-12-12T16:11:53Z

This breaks up bmct into reusable pieces with side effects made explicit. Follow up PRs will transform this into a new modular implementation.

Based on #3564
Review only the last 3 commits.

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: bf74357).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/94676355
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

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

romainbrenguier

Moving the functions one by one would make reviewing easier but otherwise looks fine.

romainbrenguier · 2018-12-17T12:19:30Z

jbmc/src/jbmc/Makefile

@@ -40,6 +40,7 @@ OBJ += ../$(CPROVER_DIR)/src/ansi-c/ansi-c$(LIBEXT) \
      ../$(CPROVER_DIR)/src/json/json$(LIBEXT) \
      ../$(CPROVER_DIR)/src/cbmc/all_properties$(OBJEXT) \
      ../$(CPROVER_DIR)/src/cbmc/bmc$(OBJEXT) \
+      ../$(CPROVER_DIR)/src/cbmc/bmc_util$(OBJEXT) \


Typo in commit message? "Factor out bmct building blocks int bmc_util" -> into?

tautschnig

Ok, but I am wondering whether at some point all contents of the cbmc folder will have moved to the goto-checker folder? Is "bounded model checking"-specific code really something that should be placed in there?

smowton

Generally not convinced at the granularity of these methods, especially the ones that just print an informational message before calling another method, or the ones that mess with symex internal state without being members of symex.

smowton · 2018-12-17T14:25:08Z

src/cbmc/bmc_util.cpp

+  message_handlert &message_handler)
+{
+  messaget msg(message_handler);
+  msg.status() << "converting SSA" << messaget::eom;


Might be a good time to improve this rubbish message :) "Converting VCCs to propositional formula"?

Although, this isn't a very useful utility-- print a message then call another public function? Probably just inline this?

smowton · 2018-12-17T14:26:08Z

src/cbmc/bmc_util.cpp

+  ui_message_handlert &ui_message_handler)
+{
+  messaget msg(ui_message_handler);
+  msg.status() << "Building error trace" << messaget::eom;


Similar to the symex case below, this isn't a very useful utility

smowton · 2018-12-17T14:27:09Z

src/cbmc/bmc_util.cpp

+  if(!ns.lookup(INITIALIZE_FUNCTION, init_symbol))
+    symex.language_mode = init_symbol->mode;
+
+  msg.status() << "Starting Bounded Model Checking" << messaget::eom;


Is this message even true? Symex isn't really BMC any more than any of the prior passes were

smowton · 2018-12-17T14:27:30Z

src/cbmc/bmc_util.cpp

+
+  symex.last_source_location.make_nil();
+
+  symex.unwindset.parse_unwind(options.get_option("unwind"));


Move this method onto symex? It exclusively has effects on symex's members

smowton · 2018-12-17T14:29:31Z

src/cbmc/bmc_util.cpp

+}
+
+void slice(
+  symex_bmct &symex,


Const reference?

smowton · 2018-12-17T14:31:35Z

src/cbmc/bmc_util.cpp

+      }
+    }
+  }
+  msg.statistics() << "Generated " << symex.get_total_vccs() << " VCC(s), "


It looks like symex_target_equation is assumed to be bound to symex at this point, such that slicing the target equation has an invisible side-effect on symex (so that get_remaining_vccs() reflects the result of slicing). That suggests moving this onto goto_symext

smowton · 2018-12-17T14:33:31Z

src/cbmc/bmc_util.h

+  prop_convt &,
+  message_handlert &);
+
+void report_failure(ui_message_handlert &);


All these methods now have names that don't specify what they do that clearly, because they're no longer in bmct. Move them into a namespace bmc_utilt?

peterschrammel · 2018-12-17T22:24:04Z

Maybe I was not sufficiently clear about the purpose of this PR: The point of this is to extract from bmct as much as possible so that I can use it "as is" in the new implementations and avoid having to backport changes that happen to bmct in the meanwhile. I am not going to change any functionality here.
One can discuss about the granularity, but this is secondary at this stage - we can easily refactor later and we can even decide that these utilities should get completely absorbed by the new implementation in the end.

smowton

Go on then

This is an intermediate step in order to reuse the building blocks in the new implementation of bmct. The old implementation is functional until it can be replaced by the new one.

allredj

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

peterschrammel requested review from cesaro, chrisr-diffblue, cristina-david, kroening, pkesseli, smowton and tautschnig as code owners December 12, 2018 16:11

peterschrammel added the blocker label Dec 12, 2018

peterschrammel force-pushed the factor-out-bmc-utils branch from f7ad772 to e9d1f38 Compare December 12, 2018 16:18

peterschrammel assigned romainbrenguier Dec 12, 2018

peterschrammel added the do not merge label Dec 12, 2018

peterschrammel force-pushed the factor-out-bmc-utils branch 4 times, most recently from 89555c4 to bf74357 Compare December 13, 2018 16:41

allredj reviewed Dec 13, 2018

View reviewed changes

peterschrammel force-pushed the factor-out-bmc-utils branch from bf74357 to 1561b05 Compare December 16, 2018 16:30

peterschrammel changed the title ~~Factor out bmc utils~~ Factor out bmc utils [depends: 3557] Dec 16, 2018

peterschrammel mentioned this pull request Dec 16, 2018

Split witness output functions into proof and refutation [depends: 3565] #3578

Merged

5 tasks

peterschrammel changed the title ~~Factor out bmc utils [depends: 3557]~~ Factor out bmc utils [depends: 3557, blocks: 3578] Dec 16, 2018

peterschrammel added dependent - do not merge and removed do not merge labels Dec 16, 2018

peterschrammel force-pushed the factor-out-bmc-utils branch from 1561b05 to cd34e43 Compare December 16, 2018 17:02

peterschrammel mentioned this pull request Dec 16, 2018

Move symex-bmc and symex-coverage to goto-checker [blocks: 3583] #3580

Merged

3 tasks

peterschrammel changed the title ~~Factor out bmc utils [depends: 3557, blocks: 3578]~~ Factor out bmc utils [depends: 3557, blocks: 3578, 3581] Dec 16, 2018

peterschrammel changed the title ~~Factor out bmc utils [depends: 3557, blocks: 3578, 3581]~~ Factor out bmc utils [depends: 3557, blocks: 3578, 3580] Dec 16, 2018

peterschrammel mentioned this pull request Dec 16, 2018

Move BMC options and help text to bmc_util [depends: 3565] #3581

Merged

7 tasks

peterschrammel changed the title ~~Factor out bmc utils [depends: 3557, blocks: 3578, 3580]~~ Factor out bmc utils [depends: 3557, blocks: 3578, 3580, 3581] Dec 16, 2018

allredj reviewed Dec 16, 2018

View reviewed changes

peterschrammel changed the title ~~Factor out bmc utils [depends: 3557, blocks: 3578, 3580, 3581]~~ Rip out the heart of bmct [depends: 3557, blocks: 3578, 3580, 3581] Dec 16, 2018

peterschrammel added the Goto-checker label Dec 16, 2018

peterschrammel assigned smowton, tautschnig and kroening Dec 17, 2018

romainbrenguier approved these changes Dec 17, 2018

View reviewed changes

tautschnig approved these changes Dec 17, 2018

View reviewed changes

tautschnig assigned peterschrammel and unassigned tautschnig, kroening and romainbrenguier Dec 17, 2018

smowton reviewed Dec 17, 2018

View reviewed changes

smowton approved these changes Dec 18, 2018

View reviewed changes

tautschnig unassigned smowton Dec 18, 2018

peterschrammel removed the dependent - do not merge label Jan 8, 2019

peterschrammel force-pushed the factor-out-bmc-utils branch from cd34e43 to 04822bd Compare January 8, 2019 22:15

peterschrammel added 2 commits January 8, 2019 22:18

Factor out bmct building blocks into bmc_util

4a710c7

This is an intermediate step in order to reuse the building blocks in the new implementation of bmct. The old implementation is functional until it can be replaced by the new one.

Move bmc_util to goto_checker module

c343989

peterschrammel force-pushed the factor-out-bmc-utils branch from 04822bd to c343989 Compare January 8, 2019 22:18

allredj reviewed Jan 8, 2019

View reviewed changes

peterschrammel merged commit 387834c into diffblue:develop Jan 9, 2019

peterschrammel deleted the factor-out-bmc-utils branch January 9, 2019 13:07


		symex.last_source_location.make_nil();

		symex.unwindset.parse_unwind(options.get_option("unwind"));

Rip out the heart of bmct [depends: 3557, blocks: 3578, 3580, 3581] #3565

Rip out the heart of bmct [depends: 3557, blocks: 3578, 3580, 3581] #3565

Uh oh!

Conversation

peterschrammel commented Dec 12, 2018

Uh oh!

allredj 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!

romainbrenguier left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

tautschnig left a comment

Choose a reason for hiding this comment

Uh oh!

smowton 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!

peterschrammel commented Dec 17, 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!

Uh oh!