diff --git a/doc/man/goto-synthesizer.1 b/doc/man/goto-synthesizer.1 index 346be77c35a..149f839c324 100644 --- a/doc/man/goto-synthesizer.1 +++ b/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 diff --git a/regression/goto-synthesizer/loop_contracts_synthesis_03/test_cadical.desc b/regression/goto-synthesizer/loop_contracts_synthesis_03/test_cadical.desc new file mode 100644 index 00000000000..9b1ab094634 --- /dev/null +++ b/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. diff --git a/src/goto-synthesizer/cegis_verifier.cpp b/src/goto-synthesizer/cegis_verifier.cpp index b6254c56861..97a0058ea9a 100644 --- a/src/goto-synthesizer/cegis_verifier.cpp +++ b/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 cegis_verifiert::get_cause_loop_id( std::list 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 object_sizes; std::unordered_map havoced_values; @@ -588,8 +560,6 @@ optionalt 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 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> checker = util_make_unique< diff --git a/src/goto-synthesizer/cegis_verifier.h b/src/goto-synthesizer/cegis_verifier.h index f156a23663e..481246a6688 100644 --- a/src/goto-synthesizer/cegis_verifier.h +++ b/src/goto-synthesizer/cegis_verifier.h @@ -103,11 +103,14 @@ class cegis_verifiert const invariant_mapt &invariant_candidates, const std::map> &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> &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. diff --git a/src/goto-synthesizer/enumerative_loop_contracts_synthesizer.cpp b/src/goto-synthesizer/enumerative_loop_contracts_synthesizer.cpp index 944aeabfab4..e681bb2fed6 100644 --- a/src/goto-synthesizer/enumerative_loop_contracts_synthesizer.cpp +++ b/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. diff --git a/src/goto-synthesizer/enumerative_loop_contracts_synthesizer.h b/src/goto-synthesizer/enumerative_loop_contracts_synthesizer.h index 49636dfca3e..9dbda380797 100644 --- a/src/goto-synthesizer/enumerative_loop_contracts_synthesizer.h +++ b/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 + #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: diff --git a/src/goto-synthesizer/goto_synthesizer_parse_options.cpp b/src/goto-synthesizer/goto_synthesizer_parse_options.cpp index a4c19ae77b3..8c9b8bce14b 100644 --- a/src/goto-synthesizer/goto_synthesizer_parse_options.cpp +++ b/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" diff --git a/src/goto-synthesizer/goto_synthesizer_parse_options.h b/src/goto-synthesizer/goto_synthesizer_parse_options.h index c9dc3817b0c..94af3d87e6f 100644 --- a/src/goto-synthesizer/goto_synthesizer_parse_options.h +++ b/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 +#include #include #include +#include #include #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; };