Move cbmc_solvers as solver_factory to new goto-checker module [blocks: 3564, 3565] #3557

peterschrammel · 2018-12-10T23:05:27Z

First of a series of PRs relating to #2883

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.
[n/a] 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).
[n/a] 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: 57c66e2).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/94355641
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 · 2018-12-12T09:19:04Z

TG bump is passing

romainbrenguier · 2018-12-14T11:18:08Z

src/goto-checker/solver_factory.cpp

      options.get_unsigned_int_option("max-node-refinement");

-  info.refine_arrays=options.get_bool_option("refine-arrays");
-  info.refine_arithmetic=options.get_bool_option("refine-arithmetic");


some formatting changes unrelated to the commit are mixed here

Now the split should be correct. Please re-check.

romainbrenguier · 2018-12-14T11:39:11Z

src/goto-checker/solver_factory.h

@@ -50,19 +50,18 @@ class cbmc_solverst
    {
    }

-    explicit solvert(std::unique_ptr<prop_convt> p):prop_conv_ptr(std::move(p))
+    explicit solvert(std::unique_ptr<prop_convt> p)


Not directly related to this PR but I find it a bit strange that the product of the factory is defined in the factory itself. And it seems also this should have been factory functions rather than a factory class as most fields are constant and I guess it's only used to produce one solver.

Noted here: #3574

allredj

🚫
This PR failed Diffblue compatibility checks (cbmc commit: 5af9fed).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/94870273
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 · 2018-12-17T09:55:58Z

src/cbmc/bmc.cpp

        opts,
        symbol_table,
        ui,
        ui.get_ui() == ui_message_handlert::uit::XML_UI);
-      std::unique_ptr<cbmc_solverst::solvert> cbmc_solver;
+      std::unique_ptr<solver_factoryt::solvert> cbmc_solver;
      cbmc_solver = solvers.get_solver();


⛏️ assignment could be on same line as declaration

allredj

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

tautschnig

Looks great to me, just more cleanup-wishlist-requests.

tautschnig · 2018-12-17T12:18:11Z

src/cbmc/bmc.cpp

        opts,
        symbol_table,
        ui,
        ui.get_ui() == ui_message_handlert::uit::XML_UI);
-      std::unique_ptr<cbmc_solverst::solvert> cbmc_solver;
+      std::unique_ptr<solver_factoryt::solvert> cbmc_solver;


As this is also done below: assign directly in the declaration.

tautschnig · 2018-12-17T12:22:01Z

src/goto-checker/solver_factory.h

-#ifndef CPROVER_CBMC_CBMC_SOLVERS_H
-#define CPROVER_CBMC_CBMC_SOLVERS_H
+#ifndef CPROVER_GOTO_CHECKER_SOLVER_FACTORY_H
+#define CPROVER_GOTO_CHECKER_SOLVER_FACTORY_H


Wishlist, possibly to be done in a separate PR: could a lot of includes be purged from the header file and the implementation of several methods be moved to the .cpp file? Really nothing needs to be inlined for performance reasons. With such a move we would eventually end up with a clean and readable interface.

This is the first step of introducing the goto-checker module which will hold the language-agnostic BMC classes.

allredj

🚫
This PR failed Diffblue compatibility checks (cbmc commit: 700d7bb).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/95012430
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 10, 2018 23:05

peterschrammel force-pushed the solver-factory branch 7 times, most recently from 6eacff3 to 57c66e2 Compare December 11, 2018 14:09

allredj reviewed Dec 11, 2018

View reviewed changes

peterschrammel mentioned this pull request Dec 12, 2018

New goto checker interfaces [blocks: 3579] #3564

Merged

7 tasks

peterschrammel added the blocker label Dec 12, 2018

peterschrammel mentioned this pull request Dec 12, 2018

Proposal: introduce a goto-checker module [blocks: #2212, #3268] #2883

Closed

peterschrammel assigned romainbrenguier Dec 12, 2018

peterschrammel changed the title ~~Move cbmc_solvers as solver_factory to new goto-checker module~~ Move cbmc_solvers as solver_factory to new goto-checker module [blocks 3564] Dec 12, 2018

romainbrenguier suggested changes Dec 14, 2018

View reviewed changes

romainbrenguier reviewed Dec 14, 2018

View reviewed changes

peterschrammel mentioned this pull request Dec 15, 2018

Improve design of solver_factoryt #3574

Closed

peterschrammel force-pushed the solver-factory branch 2 times, most recently from b5b62e8 to 5af9fed Compare December 15, 2018 16:19

allredj reviewed Dec 15, 2018

View reviewed changes

peterschrammel changed the title ~~Move cbmc_solvers as solver_factory to new goto-checker module [blocks 3564]~~ Move cbmc_solvers as solver_factory to new goto-checker module [blocks: 3564, 3565] Dec 16, 2018

peterschrammel added the Goto-checker label Dec 16, 2018

romainbrenguier approved these changes Dec 17, 2018

View reviewed changes

peterschrammel force-pushed the solver-factory branch from 5af9fed to 699fcc2 Compare December 17, 2018 10:46

peterschrammel assigned smowton, tautschnig and kroening Dec 17, 2018

allredj approved these changes Dec 17, 2018

View reviewed changes

allredj reviewed 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 approved these changes Dec 17, 2018

View reviewed changes

tautschnig unassigned smowton Dec 17, 2018

peterschrammel added 2 commits December 17, 2018 17:58

Move cbmc_solvers as solver_factory to goto-checker module

bac549b

This is the first step of introducing the goto-checker module which will hold the language-agnostic BMC classes.

Clang-format

700d7bb

peterschrammel force-pushed the solver-factory branch from 699fcc2 to 700d7bb Compare December 17, 2018 17:58

peterschrammel merged commit 8065b10 into diffblue:develop Dec 17, 2018

peterschrammel deleted the solver-factory branch December 17, 2018 18:34

allredj reviewed Dec 17, 2018

View reviewed changes

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

Move cbmc_solvers as solver_factory to new goto-checker module [blocks: 3564, 3565] #3557

Move cbmc_solvers as solver_factory to new goto-checker module [blocks: 3564, 3565] #3557

Uh oh!

peterschrammel commented Dec 10, 2018 •

edited

Loading

Uh oh!

allredj left a comment

Uh oh!

peterschrammel commented Dec 12, 2018

Uh oh!

romainbrenguier Dec 14, 2018

Uh oh!

peterschrammel Dec 15, 2018

Uh oh!

romainbrenguier Dec 14, 2018

Uh oh!

peterschrammel Dec 15, 2018

Uh oh!

allredj left a comment

Uh oh!

romainbrenguier Dec 17, 2018

Uh oh!

peterschrammel Dec 17, 2018

Uh oh!

allredj left a comment

Uh oh!

tautschnig left a comment

Uh oh!

tautschnig Dec 17, 2018

Uh oh!

tautschnig Dec 17, 2018

Uh oh!

peterschrammel Dec 17, 2018

Uh oh!

allredj left a comment

Uh oh!

Uh oh!

Move cbmc_solvers as solver_factory to new goto-checker module [blocks: 3564, 3565] #3557

Move cbmc_solvers as solver_factory to new goto-checker module [blocks: 3564, 3565] #3557

Uh oh!

Conversation

peterschrammel commented Dec 10, 2018 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

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

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

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

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

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

peterschrammel commented Dec 10, 2018 •

edited

Loading