Merge pull request #7612 from qinheping/different_solver_in_synthesizer

Enable solver options in goto-synthesizer

Author: qinheping

doc/man/goto-synthesizer.1

@@ -29,6 +29,98 @@ specify the output destination of the loop-contracts JSON
 .TP
 \fB\-\-object\-bits\fR n
 number of bits used for object addresses
+.TP
+\fB\-\-sat\-solver\fR solver
+use specified SAT solver
+.TP
+\fB\-\-external\-sat\-solver\fR cmd
+command to invoke SAT solver process
+.TP
+\fB\-\-no\-sat\-preprocessor\fR
+disable the SAT solver's simplifier
+.TP
+\fB\-\-dimacs\fR
+generate CNF in DIMACS format
+.TP
+\fB\-\-beautify\fR
+beautify the counterexample
+(greedy heuristic)
+.TP
+\fB\-\-smt1\fR
+use default SMT1 solver (obsolete)
+.TP
+\fB\-\-smt2\fR
+use default SMT2 solver (Z3)
+.TP
+\fB\-\-bitwuzla\fR
+use Bitwuzla
+.TP
+\fB\-\-boolector\fR
+use Boolector
+.TP
+\fB\-\-cprover\-smt2\fR
+use CPROVER SMT2 solver
+.TP
+\fB\-\-cvc3\fR
+use CVC3
+.TP
+\fB\-\-cvc4\fR
+use CVC4
+.TP
+\fB\-\-cvc5\fR
+use CVC5
+.TP
+\fB\-\-mathsat\fR
+use MathSAT
+.TP
+\fB\-\-yices\fR
+use Yices
+.TP
+\fB\-\-z3\fR
+use Z3
+.TP
+\fB\-\-fpa\fR
+use theory of floating\-point arithmetic
+.TP
+\fB\-\-refine\fR
+use refinement procedure (experimental)
+.TP
+\fB\-\-refine\-arrays\fR
+use refinement for arrays only
+.TP
+\fB\-\-refine\-arithmetic\fR
+refinement of arithmetic expressions only
+.TP
+\fB\-\-max\-node\-refinement\fR
+maximum refinement iterations for
+arithmetic expressions
+.TP
+\fB\-\-incremental\-smt2\-solver\fR \fIcmd\fR
+Use the incremental SMT backend where \fIcmd\fR is the command to invoke the SMT
+solver of choice.
+.br
+Example invocations:
+.br
+  --incremental-smt2-solver 'z3 -smt2 -in' (use the Z3 solver).
+.br
+  --incremental-smt2-solver 'cvc5 --lang=smtlib2.6 --incremental' (use the CVC5 solver).
+.sp
+Note that:
+.br
+The solver name must be in the "PATH" or be an executable with full path.
+.br
+The SMT solver should accept incremental SMTlib v2.6 formatted input from the stdin.
+.br
+The SMT solver should support the QF_AUFBV logic.
+.TP
+\fB\-\-outfile\fR filename
+output formula to given file
+.TP
+\fB\-\-dump\-smt\-formula\fR filename
+output smt incremental formula to the given file
+.TP
+\fB\-\-write\-solver\-stats\-to\fR json\-file
+collect the solver query complexity
 .SS "User-interface options:"
 .TP
 \fB\-\-xml\-ui\fR

regression/goto-synthesizer/loop_contracts_synthesis_03/test_cadical.desc

@@ -0,0 +1,11 @@
+CORE
+main.c
+--pointer-check _ --sat-solver cadical --verbosity 10
+^EXIT=0$
+^SIGNAL=0$
+Solving with CaDiCaL|The specified solver, 'cadical', is not available. The default solver will be used instead.
+^\[main.pointer\_dereference.\d+\] .* SUCCESS$
+^VERIFICATION SUCCESSFUL$
+--
+--
+Check if solver options can be correctly parsed.

src/goto-synthesizer/cegis_verifier.cpp

@@ -81,32 +81,8 @@ get_checked_pointer_from_null_pointer_check(const exprt &violation)
   UNREACHABLE;
 }
 
-optionst cegis_verifiert::get_options()
+void cegis_verifiert::preprocess_goto_model()
 {
-  optionst options;
-
-  // Default options
-  // These options are the same as we run CBMC without any set flag.
-  options.set_option("built-in-assertions", true);
-  options.set_option("propagation", true);
-  options.set_option("simple-slice", true);
-  options.set_option("simplify", true);
-  options.set_option("show-goto-symex-steps", false);
-  options.set_option("show-points-to-sets", false);
-  options.set_option("show-array-constraints", false);
-  options.set_option("built-in-assertions", true);
-  options.set_option("assertions", true);
-  options.set_option("assumptions", true);
-  options.set_option("arrays-uf", "auto");
-  options.set_option("depth", UINT32_MAX);
-  options.set_option("exploration-strategy", "lifo");
-  options.set_option("symex-cache-dereferences", false);
-  options.set_option("rewrite-union", true);
-  options.set_option("self-loops-to-assumptions", true);
-
-  // Generating trace for counterexamples.
-  options.set_option("trace", true);
-
   // Preprocess `goto_model`. Copied from `cbmc_parse_options.cpp`.
   remove_asm(goto_model);
   link_to_library(
@@ -119,7 +95,6 @@ optionst cegis_verifiert::get_options()
 
   remove_skip(goto_model);
   label_properties(goto_model);
-  return options;
 }
 
 cext::violation_typet
@@ -203,7 +178,6 @@ std::list<loop_idt> cegis_verifiert::get_cause_loop_id(
   std::list<loop_idt> result;
 
   // build the dependence graph
-  const namespacet ns(goto_model.symbol_table);
   dependence_grapht dependence_graph(ns);
   dependence_graph(goto_model);
 
@@ -382,8 +356,6 @@ cext cegis_verifiert::build_cex(
   const goto_tracet &goto_trace,
   const source_locationt &loop_entry_loc)
 {
-  const namespacet ns(goto_model.symbol_table);
-
   // Valuations of havoced variables right after havoc instructions.
   std::unordered_map<exprt, mp_integer, irep_hash> object_sizes;
   std::unordered_map<exprt, mp_integer, irep_hash> havoced_values;
@@ -588,8 +560,6 @@ optionalt<cext> cegis_verifiert::verify()
   // 3. construct the formatted counterexample from the violated property and
   //    its trace.
 
-  const namespacet ns(goto_model.symbol_table);
-
   // Store the original functions. We will restore them after the verification.
   for(const auto &fun_entry : goto_model.goto_functions.function_map)
   {
@@ -618,7 +588,7 @@ optionalt<cext> cegis_verifiert::verify()
   // Get the checker same as CBMC api without any flag.
   // TODO: replace the checker with CBMC api once it is implemented.
   ui_message_handlert ui_message_handler(log.get_message_handler());
-  const auto options = get_options();
+  preprocess_goto_model();
   std::unique_ptr<
     all_properties_verifier_with_trace_storaget<multi_path_symex_checkert>>
     checker = util_make_unique<

src/goto-synthesizer/cegis_verifier.h

@@ -103,11 +103,14 @@ class cegis_verifiert
     const invariant_mapt &invariant_candidates,
     const std::map<loop_idt, std::set<exprt>> &assigns_map,
     goto_modelt &goto_model,
+    const optionst &options,
     messaget &log)
     : invariant_candidates(invariant_candidates),
       assigns_map(assigns_map),
       goto_model(goto_model),
-      log(log)
+      options(options),
+      log(log),
+      ns(goto_model.symbol_table)
   {
   }
 
@@ -120,11 +123,6 @@ class cegis_verifiert
   irep_idt target_violation_id;
 
 protected:
-  // Get the options same as using CBMC api without any flag, and
-  // preprocess `goto_model`.
-  // TODO: replace the checker with CBMC api once it is implemented.
-  optionst get_options();
-
   // Compute the cause loops of `violation`.
   // We say a loop is the cause loop if the violated predicate is dependent
   // upon the write set of the loop.
@@ -168,10 +166,15 @@ class cegis_verifiert
     const goto_functiont &function,
     unsigned location_number_of_target);
 
+  /// Preprocess the goto model to prepare for verification.
+  void preprocess_goto_model();
+
   const invariant_mapt &invariant_candidates;
   const std::map<loop_idt, std::set<exprt>> &assigns_map;
   goto_modelt &goto_model;
+  const optionst &options;
   messaget log;
+  const namespacet ns;
 
   /// Map from function names to original functions. It is used to
   /// restore functions with annotated loops to original functions.

src/goto-synthesizer/enumerative_loop_contracts_synthesizer.cpp

@@ -334,7 +334,7 @@ exprt enumerative_loop_contracts_synthesizert::synthesize_strengthening_clause(
 
       // The verifier we use to check current invariant candidates.
       cegis_verifiert verifier(
-        combined_invariant, assigns_map, goto_model, log);
+        combined_invariant, assigns_map, goto_model, options, log);
 
       // A good strengthening clause if
       // 1. all checks pass, or
@@ -367,7 +367,8 @@ invariant_mapt enumerative_loop_contracts_synthesizert::synthesize_all()
     in_invariant_clause_map, pos_invariant_clause_map, neg_guards);
 
   // The verifier we use to check current invariant candidates.
-  cegis_verifiert verifier(combined_invariant, assigns_map, goto_model, log);
+  cegis_verifiert verifier(
+    combined_invariant, assigns_map, goto_model, options, log);
 
   // Set of symbols the violation may be dependent on.
   // We enumerate strengthening clauses built from symbols from the set.

src/goto-synthesizer/enumerative_loop_contracts_synthesizer.h

@@ -14,6 +14,8 @@ Author: Qinheping Hu
 // NOLINTNEXTLINE(whitespace/line_length)
 #define CPROVER_GOTO_SYNTHESIZER_ENUMERATIVE_LOOP_CONTRACTS_SYNTHESIZER_H
 
+#include <util/options.h>
+
 #include "loop_contracts_synthesizer_base.h"
 
 class messaget;
@@ -30,8 +32,10 @@ class enumerative_loop_contracts_synthesizert
 public:
   enumerative_loop_contracts_synthesizert(
     goto_modelt &goto_model,
+    const optionst &options,
     messaget &log)
     : loop_contracts_synthesizer_baset(goto_model, log),
+      options(options),
       ns(goto_model.symbol_table)
   {
   }
@@ -46,6 +50,7 @@ class enumerative_loop_contracts_synthesizert
     return assigns_map;
   }
 
+  const optionst &options;
   namespacet ns;
 
 private:

src/goto-synthesizer/goto_synthesizer_parse_options.cpp

@@ -60,8 +60,11 @@ int goto_synthesizer_parse_optionst::doit()
     configure_gcc(gcc_version);
   }
 
+  // Get options and preprocess `goto_model`.
+  const auto &options = get_options();
+
   // Synthesize loop invariants and annotate them into `goto_model`
-  enumerative_loop_contracts_synthesizert synthesizer(goto_model, log);
+  enumerative_loop_contracts_synthesizert synthesizer(goto_model, options, log);
   const auto &invariant_map = synthesizer.synthesize_all();
   const auto &assigns_map = synthesizer.get_assigns_map();
 
@@ -176,6 +179,37 @@ int goto_synthesizer_parse_optionst::get_goto_program()
   return CPROVER_EXIT_SUCCESS;
 }
 
+optionst goto_synthesizer_parse_optionst::get_options()
+{
+  optionst options;
+
+  // Default options
+  // These options are the same as we run CBMC without any set flag.
+  options.set_option("built-in-assertions", true);
+  options.set_option("propagation", true);
+  options.set_option("simple-slice", true);
+  options.set_option("simplify", true);
+  options.set_option("show-goto-symex-steps", false);
+  options.set_option("show-points-to-sets", false);
+  options.set_option("show-array-constraints", false);
+  options.set_option("built-in-assertions", true);
+  options.set_option("assertions", true);
+  options.set_option("assumptions", true);
+  options.set_option("arrays-uf", "auto");
+  options.set_option("depth", UINT32_MAX);
+  options.set_option("exploration-strategy", "lifo");
+  options.set_option("symex-cache-dereferences", false);
+  options.set_option("rewrite-union", true);
+  options.set_option("self-loops-to-assumptions", true);
+
+  // Generating trace for counterexamples.
+  options.set_option("trace", true);
+
+  parse_solver_options(cmdline, options);
+
+  return options;
+}
+
 /// display command line help
 void goto_synthesizer_parse_optionst::help()
 {
@@ -197,6 +231,7 @@ void goto_synthesizer_parse_optionst::help()
     "\n"
     "Backend options:\n"
     HELP_CONFIG_BACKEND
+    HELP_SOLVER
     "\n"
     "Other options:\n"
     " --version                    show version and exit\n"

src/goto-synthesizer/goto_synthesizer_parse_options.h

@@ -10,10 +10,12 @@ Author: Qinheping Hu
 #define CPROVER_GOTO_SYNTHESIZER_GOTO_SYNTHESIZER_PARSE_OPTIONS_H
 
 #include <util/config.h>
+#include <util/options.h>
 #include <util/parse_options.h>
 
 #include <goto-programs/goto_model.h>
 
+#include <goto-checker/solver_factory.h>
 #include <goto-instrument/contracts/contracts.h>
 
 #include "dump_loop_contracts.h"
@@ -23,6 +25,7 @@ Author: Qinheping Hu
   OPT_DUMP_LOOP_CONTRACTS \
   "(" FLAG_LOOP_CONTRACTS_NO_UNWIND ")" \
   OPT_CONFIG_BACKEND \
+  OPT_SOLVER \
   "(verbosity):(version)(xml-ui)(json-ui)" \
   // empty last line
 
@@ -48,6 +51,10 @@ class goto_synthesizer_parse_optionst : public parse_options_baset
 
   int get_goto_program();
 
+  // Get the options same as using CBMC api without any flags and set any
+  // options specified in the command line.
+  optionst get_options();
+
   goto_modelt goto_model;
 };