Collect complexity statistics of solver queries #5266

hannes-steffenhagen-diffblue · 2020-03-11T15:23:09Z

Introduces a functionality to track and collect the complexity of individual
solver queries. For SAT solvers we collect the number of clauses, literals, and
variables. The functionality matches solver queries to the SSA steps that
produced them. After running the solver, we produce a JSON report that matches
program line to GOTO instruction to SSA step to solver hardness.

At present the collection is command-line optional and only works with the
default SAT solver (minisat2). Extension to other SAT and SMT solvers should be
possible.

Supercedes #5159

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.

Introduces a functionality to track and collect the complexity of individual solver queries. For SAT solvers we collect the number of clauses, literals, and variables. The functionality matches solver queries to the SSA steps that produced them. After running the solver, we produce a JSON report that matches program line to GOTO instruction to SSA step to solver hardness. At present the collection is command-line optional and only works with the default SAT solver (minisat2). Extension to other SAT and SMT solvers should be possible. A simple regression test is included. Note: the solver-hardness structure lives in the minisat2 and is accessible via the interface of hardness-collector (which minisat2 inherits from). Hence to find out if symex should collect the statistics one must try-cast `prop` to `hardness-collector`. `prop` is part of the `solvert` but not directly accessible from `decision-procedure`. So we also had to extend the interface that initialises the SSA conversion (to include `prop` as well).

peterschrammel · 2020-03-11T16:27:39Z

src/goto-checker/bmc_util.cpp


 void convert_symex_target_equation(
  symex_target_equationt &equation,
-  decision_proceduret &decision_procedure,


undo to keep it general

peterschrammel · 2020-03-11T16:27:49Z

src/goto-checker/bmc_util.cpp


-  // convert SSA
-  equation.convert(decision_procedure);
+  equation.convert(property_decider.get_decision_procedure());


undo to keep it general

peterschrammel · 2020-03-11T16:28:02Z

src/goto-checker/bmc_util.cpp

 #include <linking/static_lifetime_init.h>

 #include <solvers/decision_procedure.h>
+#include <solvers/flattening/boolbv.h>


peterschrammel · 2020-03-11T16:28:17Z

src/goto-checker/bmc_util.cpp


-  convert_symex_target_equation(
-    equation, property_decider.get_decision_procedure(), ui_message_handler);
+  convert_symex_target_equation(equation, property_decider, ui_message_handler);


peterschrammel · 2020-03-11T16:28:25Z

src/goto-checker/bmc_util.h

 void convert_symex_target_equation(
  symex_target_equationt &,
-  decision_proceduret &,
+  goto_symex_property_decidert &,


peterschrammel · 2020-03-11T16:30:02Z

src/goto-checker/goto_symex_property_decider.h


 /// Provides management of goal variables that encode properties
-class goto_symex_property_decidert
+class goto_symex_property_decidert : public hardness_collectort


no changes required in this class

peterschrammel · 2020-03-11T16:30:38Z

src/goto-checker/multi_path_symex_checker.cpp

    equation_generated(false),
    property_decider(options, ui_message_handler, equation, ns)
 {
+  if(options.is_set("write-solver-stats-to"))


This should happen in solver_factoryt

peterschrammel · 2020-03-11T16:31:56Z

src/goto-checker/multi_path_symex_checker.cpp

+{
+  if(options.is_set("write-solver-stats-to"))
+  {
+    with_solver_hardness(property_decider, [](solver_hardnesst &hardness) {


pass decision procedure instead of property decider:
with_solver_hardness(property_decider.get_decision_procedure()).produce_report();

peterschrammel · 2020-03-11T16:32:30Z

src/goto-symex/symex_target_equation.cpp


 #include <solvers/decision_procedure.h>
+#include <solvers/hardness_collector.h>
+#include <solvers/prop/prop.h>


no reference to prop in this class

peterschrammel · 2020-03-11T16:35:38Z

src/goto-symex/symex_target_equation.h

 #include "symex_target.h"

 class decision_proceduret;
+class propt;


no changes required in this file

hannes-steffenhagen-diffblue · 2020-03-16T10:19:38Z

src/goto-checker/incremental_goto_checker.h


+  /// Additional reporting that may result from the underlying solver, no-op by
+  /// default.
+  virtual void report()


Since this is just for the hardness stats right now should this be reflected in the name of this method?

I'd say no.

hannes-steffenhagen-diffblue · 2020-03-16T14:48:20Z

regression/solver-hardness/solver-hardness-simple/test.desc

+^\[main.assertion.\d+\] line \d+ assertion a \+ b \< 10: FAILURE$
+^VERIFICATION FAILED$
+^Valid JSON File$
+\"SAT_hardness\": \{(\"Clauses\": \d+|\"Variables\": \d+|\"Literals\": \d+), (\"Clauses\": \d+|\"Variables\": \d+|\"Literals\": \d+), (\"Clauses\": \d+|\"Variables\": \d+|\"Literals\": \d+)\}


As far as tests go this isn’t very exciting, but I couldn’t figure out a good way to put specific values here either; Any changes to symex or solvers would invalidate any test that’s checking for concrete values here.

You could check that there is something non-zero, at least.

peterschrammel

Looks good now. Thanks, @hannes-steffenhagen-diffblue, for cleaning this up!

peterschrammel · 2020-03-16T13:23:08Z

src/goto-checker/incremental_goto_checker.h


+  /// Additional reporting that may result from the underlying solver, no-op by
+  /// default.
+  virtual void report()


I'd say no.

peterschrammel · 2020-03-16T15:38:16Z

regression/solver-hardness/solver-hardness-simple/test.desc

+^\[main.assertion.\d+\] line \d+ assertion a \+ b \< 10: FAILURE$
+^VERIFICATION FAILED$
+^Valid JSON File$
+\"SAT_hardness\": \{(\"Clauses\": \d+|\"Variables\": \d+|\"Literals\": \d+), (\"Clauses\": \d+|\"Variables\": \d+|\"Literals\": \d+), (\"Clauses\": \d+|\"Variables\": \d+|\"Literals\": \d+)\}


You could check that there is something non-zero, at least.

NlightNFotis

Looks good to me.

peterschrammel reviewed Mar 11, 2020

View reviewed changes

hannes-steffenhagen-diffblue force-pushed the feature/solver-hardness branch 3 times, most recently from 025a967 to 6ae064e Compare March 16, 2020 11:09

hannes-steffenhagen-diffblue commented Mar 16, 2020

View reviewed changes

hannes-steffenhagen-diffblue marked this pull request as ready for review March 16, 2020 11:10

hannes-steffenhagen-diffblue requested review from chrisr-diffblue, kroening, martin-cs, romainbrenguier, smowton and tautschnig as code owners March 16, 2020 11:10

hannes-steffenhagen-diffblue mentioned this pull request Mar 16, 2020

Collect complexity statistics of solver queries #5159

Closed

7 tasks

hannes-steffenhagen-diffblue changed the title ~~Feature/solver hardness~~ Collect complexity statistics of solver queries Mar 16, 2020

karkhaz added the aws Bugs or features of importance to AWS CBMC users label Mar 16, 2020

Refactoring hardness collection to not expose prop

fbb2da1

hannes-steffenhagen-diffblue force-pushed the feature/solver-hardness branch from a404049 to fbb2da1 Compare March 16, 2020 14:33

hannes-steffenhagen-diffblue commented Mar 16, 2020

View reviewed changes

peterschrammel approved these changes Mar 16, 2020

View reviewed changes

NlightNFotis approved these changes Mar 17, 2020

View reviewed changes

hannes-steffenhagen-diffblue merged commit 1002ac5 into diffblue:develop Mar 18, 2020

Collect complexity statistics of solver queries #5266

Collect complexity statistics of solver queries #5266

Uh oh!

Conversation

hannes-steffenhagen-diffblue commented Mar 11, 2020 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

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!

Choose a reason for hiding this comment

Uh oh!

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!

NlightNFotis left a comment

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

5 participants

hannes-steffenhagen-diffblue commented Mar 11, 2020 •

edited

Loading