From 6f240093a82e807c24a2fdba7879b5150c974191 Mon Sep 17 00:00:00 2001 From: Kareem Khazem Date: Thu, 12 Apr 2018 16:14:14 +0100 Subject: [PATCH 1/3] Can now test for an option being set in optionst There was previously no public interface to check whether an option had been set in an optionst object; this meant that clients were instead using the isset() method of cmdlinet. This change allows us to set the options from the cmdlinet near the beginning of the front-end, and not refer to the cmdlinet afterward. --- src/util/options.cpp | 5 +++++ src/util/options.h | 3 +++ 2 files changed, 8 insertions(+) diff --git a/src/util/options.cpp b/src/util/options.cpp index bd952760a4c..5671e7ed281 100644 --- a/src/util/options.cpp +++ b/src/util/options.cpp @@ -57,6 +57,11 @@ unsigned int optionst::get_unsigned_int_option(const std::string &option) const return value.empty()?0:safe_string2unsigned(value); } +bool optionst::is_set(const std::string &option) const +{ + return option_map.find(option) != option_map.end(); +} + const std::string optionst::get_option(const std::string &option) const { option_mapt::const_iterator it= diff --git a/src/util/options.h b/src/util/options.h index 1a558a37331..741157740e6 100644 --- a/src/util/options.h +++ b/src/util/options.h @@ -28,6 +28,9 @@ class optionst unsigned int get_unsigned_int_option(const std::string &option) const; const value_listt &get_list_option(const std::string &option) const; + /// N.B. opts.is_set("foo") does not imply opts.get_bool_option("foo") + bool is_set(const std::string &option) const; + void set_option(const std::string &option, const bool value); void set_option(const std::string &option, const int value); void set_option(const std::string &option, const unsigned value); From 751a88275a2ac0a0798bd156990ad3dc70d4765d Mon Sep 17 00:00:00 2001 From: Kareem Khazem Date: Wed, 11 Apr 2018 15:31:49 +0100 Subject: [PATCH 2/3] Factor out default CBMC options to static method CBMC parse options that have default values are all set in a single place---a static method that may also be called from any client that needs to emulate CBMC's default options (e.g. unit tests). Previous to this commit, there were a lot of if(cmdline.isset("no-foo")) options.set_option("foo", false); else options.set_option("foo", true); This commit removes all the else cases. --- src/cbmc/cbmc_parse_options.cpp | 71 ++++++++++++++++++--------------- src/cbmc/cbmc_parse_options.h | 6 +++ 2 files changed, 44 insertions(+), 33 deletions(-) diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index 100c83c2abf..42739bafb12 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -85,6 +85,28 @@ ::cbmc_parse_optionst::cbmc_parse_optionst( { } +void cbmc_parse_optionst::set_default_options(optionst &options) +{ + // Default true + options.set_option("assertions", true); + options.set_option("assumptions", true); + options.set_option("built-in-assertions", true); + options.set_option("pretty-names", true); + options.set_option("propagation", true); + options.set_option("sat-preprocessor", true); + options.set_option("simplify", true); + options.set_option("simplify-if", true); + + // Default false + options.set_option("partial-loops", false); + options.set_option("slice-formula", false); + options.set_option("stop-on-fail", false); + options.set_option("unwinding-assertions", false); + + // Other + options.set_option("arrays-uf", "auto"); +} + void cbmc_parse_optionst::eval_verbosity() { // this is our default verbosity @@ -108,6 +130,8 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options) exit(CPROVER_EXIT_USAGE_ERROR); } + cbmc_parse_optionst::set_default_options(options); + if(cmdline.isset("paths")) options.set_option("paths", true); @@ -143,15 +167,11 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options) if(cmdline.isset("no-simplify")) options.set_option("simplify", false); - else - options.set_option("simplify", true); if(cmdline.isset("stop-on-fail") || cmdline.isset("dimacs") || cmdline.isset("outfile")) options.set_option("stop-on-fail", true); - else - options.set_option("stop-on-fail", false); if(cmdline.isset("trace") || cmdline.isset("stop-on-fail")) @@ -184,8 +204,6 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options) // constant propagation if(cmdline.isset("no-propagation")) options.set_option("propagation", false); - else - options.set_option("propagation", true); // all checks supported by goto_check PARSE_OPTIONS_GOTO_CHECK(cmdline, options); @@ -193,34 +211,29 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options) // check assertions if(cmdline.isset("no-assertions")) options.set_option("assertions", false); - else - options.set_option("assertions", true); // use assumptions if(cmdline.isset("no-assumptions")) options.set_option("assumptions", false); - else - options.set_option("assumptions", true); // magic error label if(cmdline.isset("error-label")) options.set_option("error-label", cmdline.get_values("error-label")); // generate unwinding assertions - if(cmdline.isset("cover")) - options.set_option("unwinding-assertions", false); - else + if(cmdline.isset("unwinding-assertions")) + options.set_option("unwinding-assertions", true); + + if(cmdline.isset("partial-loops")) + options.set_option("partial-loops", true); + + if(options.is_set("cover") && options.get_bool_option("unwinding-assertions")) { - options.set_option( - "unwinding-assertions", - cmdline.isset("unwinding-assertions")); + error() << "--cover and --unwinding-assertions " + << "must not be given together" << eom; + exit(CPROVER_EXIT_USAGE_ERROR); } - // generate unwinding assumptions otherwise - options.set_option( - "partial-loops", - cmdline.isset("partial-loops")); - if(options.get_bool_option("partial-loops") && options.get_bool_option("unwinding-assertions")) { @@ -230,22 +243,17 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options) } // remove unused equations - options.set_option( - "slice-formula", - cmdline.isset("slice-formula")); + if(cmdline.isset("slice-formula")) + options.set_option("slice-formula", true); // simplify if conditions and branches if(cmdline.isset("no-simplify-if")) options.set_option("simplify-if", false); - else - options.set_option("simplify-if", true); if(cmdline.isset("arrays-uf-always")) options.set_option("arrays-uf", "always"); else if(cmdline.isset("arrays-uf-never")) options.set_option("arrays-uf", "never"); - else - options.set_option("arrays-uf", "auto"); if(cmdline.isset("dimacs")) options.set_option("dimacs", true); @@ -387,12 +395,9 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options) if(cmdline.isset("no-sat-preprocessor")) options.set_option("sat-preprocessor", false); - else - options.set_option("sat-preprocessor", true); - options.set_option( - "pretty-names", - !cmdline.isset("no-pretty-names")); + if(cmdline.isset("no-pretty-names")) + options.set_option("pretty-names", false); if(cmdline.isset("outfile")) options.set_option("outfile", cmdline.get_value("outfile")); diff --git a/src/cbmc/cbmc_parse_options.h b/src/cbmc/cbmc_parse_options.h index 9a47b4eed2c..3b243321074 100644 --- a/src/cbmc/cbmc_parse_options.h +++ b/src/cbmc/cbmc_parse_options.h @@ -91,6 +91,12 @@ class cbmc_parse_optionst: const char **argv, const std::string &extra_options); + /// \brief Set the options that have default values + /// + /// This function can be called from clients that wish to emulate CBMC's + /// default behaviour, for example unit tests. + static void set_default_options(optionst &); + protected: goto_modelt goto_model; ui_message_handlert ui_message_handler; From 014d15186bdbca531801f4ec12cd60f31d2e224c Mon Sep 17 00:00:00 2001 From: Kareem Khazem Date: Wed, 11 Apr 2018 16:36:19 +0100 Subject: [PATCH 3/3] Factor out getting & processing goto-model CBMC's methods for getting a goto-model from a source file, and processing that goto-model to be ready for bounded model checking, are now static so that they can be called from clients that wish to set up a goto-model the same way that CBMC does. --- src/cbmc/bmc.h | 3 +- src/cbmc/cbmc_parse_options.cpp | 174 ++++++++++++++++++-------------- src/cbmc/cbmc_parse_options.h | 11 +- 3 files changed, 108 insertions(+), 80 deletions(-) diff --git a/src/cbmc/bmc.h b/src/cbmc/bmc.h index d4feb6847e0..994a3b10be3 100644 --- a/src/cbmc/bmc.h +++ b/src/cbmc/bmc.h @@ -321,7 +321,8 @@ class path_explorert : public bmct " (use --show-loops to get the loop IDs)\n" \ " --show-vcc show the verification conditions\n" \ " --slice-formula remove assignments unrelated to property\n" \ - " --unwinding-assertions generate unwinding assertions\n" \ + " --unwinding-assertions generate unwinding assertions (cannot be\n" \ + " used with --cover or --partial-loops)\n" \ " --partial-loops permit paths with partial loops\n" \ " --no-pretty-names do not simplify identifiers\n" \ " --graphml-witness filename write the witness in GraphML format to " \ diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index 42739bafb12..c3b88a93bd7 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -97,13 +97,7 @@ void cbmc_parse_optionst::set_default_options(optionst &options) options.set_option("simplify", true); options.set_option("simplify-if", true); - // Default false - options.set_option("partial-loops", false); - options.set_option("slice-formula", false); - options.set_option("stop-on-fail", false); - options.set_option("unwinding-assertions", false); - - // Other + // Other default options.set_option("arrays-uf", "auto"); } @@ -132,6 +126,28 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options) cbmc_parse_optionst::set_default_options(options); + if(cmdline.isset("cover") && cmdline.isset("unwinding-assertions")) + { + error() << "--cover and --unwinding-assertions must not be given together" + << eom; + exit(CPROVER_EXIT_USAGE_ERROR); + } + + if(cmdline.isset("partial-loops") && cmdline.isset("unwinding-assertions")) + { + error() << "--partial-loops and --unwinding-assertions must not be given " + << "together" << eom; + exit(CPROVER_EXIT_USAGE_ERROR); + } + + if(cmdline.isset("reachability-slice") && + cmdline.isset("reachability-slice-fb")) + { + error() << "--reachability-slice and --reachability-slice-fb must not be " + << "given together" << eom; + exit(CPROVER_EXIT_USAGE_ERROR); + } + if(cmdline.isset("paths")) options.set_option("paths", true); @@ -165,6 +181,24 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options) if(cmdline.isset("cpp11")) config.cpp.set_cpp11(); + if(cmdline.isset("property")) + options.set_option("property", cmdline.get_values("property")); + + if(cmdline.isset("drop-unused-functions")) + options.set_option("drop-unused-functions", true); + + if(cmdline.isset("string-abstraction")) + options.set_option("string-abstraction", true); + + if(cmdline.isset("reachability-slice-fb")) + options.set_option("reachability-slice-fb", true); + + if(cmdline.isset("reachability-slice")) + options.set_option("reachability-slice", true); + + if(cmdline.isset("nondet-static")) + options.set_option("nondet-static", true); + if(cmdline.isset("no-simplify")) options.set_option("simplify", false); @@ -227,21 +261,6 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options) if(cmdline.isset("partial-loops")) options.set_option("partial-loops", true); - if(options.is_set("cover") && options.get_bool_option("unwinding-assertions")) - { - error() << "--cover and --unwinding-assertions " - << "must not be given together" << eom; - exit(CPROVER_EXIT_USAGE_ERROR); - } - - if(options.get_bool_option("partial-loops") && - options.get_bool_option("unwinding-assertions")) - { - error() << "--partial-loops and --unwinding-assertions " - << "must not be given together" << eom; - exit(CPROVER_EXIT_USAGE_ERROR); - } - // remove unused equations if(cmdline.isset("slice-formula")) options.set_option("slice-formula", true); @@ -532,7 +551,8 @@ int cbmc_parse_optionst::doit() return CPROVER_EXIT_SUCCESS; } - int get_goto_program_ret=get_goto_program(options); + int get_goto_program_ret = + get_goto_program(goto_model, options, cmdline, *this, ui_message_handler); if(get_goto_program_ret!=-1) return get_goto_program_ret; @@ -585,17 +605,21 @@ bool cbmc_parse_optionst::set_properties() } int cbmc_parse_optionst::get_goto_program( - const optionst &options) + goto_modelt &goto_model, + const optionst &options, + const cmdlinet &cmdline, + messaget &log, + ui_message_handlert &ui_message_handler) { if(cmdline.args.empty()) { - error() << "Please provide a program to verify" << eom; + log.error() << "Please provide a program to verify" << log.eom; return CPROVER_EXIT_INCORRECT_TASK; } try { - goto_model=initialize_goto_model(cmdline, get_message_handler()); + goto_model = initialize_goto_model(cmdline, ui_message_handler); if(cmdline.isset("show-symbol-table")) { @@ -603,7 +627,7 @@ int cbmc_parse_optionst::get_goto_program( return CPROVER_EXIT_SUCCESS; } - if(process_goto_program(options)) + if(cbmc_parse_optionst::process_goto_program(goto_model, options, log)) return CPROVER_EXIT_INTERNAL_ERROR; // show it? @@ -620,36 +644,36 @@ int cbmc_parse_optionst::get_goto_program( { show_goto_functions( goto_model, - get_message_handler(), + ui_message_handler, ui_message_handler.get_ui(), cmdline.isset("list-goto-functions")); return CPROVER_EXIT_SUCCESS; } - status() << config.object_bits_info() << eom; + log.status() << config.object_bits_info() << log.eom; } catch(const char *e) { - error() << e << eom; + log.error() << e << log.eom; return CPROVER_EXIT_EXCEPTION; } catch(const std::string &e) { - error() << e << eom; + log.error() << e << log.eom; return CPROVER_EXIT_EXCEPTION; } catch(int e) { - error() << "Numeric exception : " << e << eom; + log.error() << "Numeric exception : " << e << log.eom; return CPROVER_EXIT_EXCEPTION; } catch(const std::bad_alloc &) { - error() << "Out of memory" << eom; + log.error() << "Out of memory" << log.eom; return CPROVER_EXIT_INTERNAL_OUT_OF_MEMORY; } @@ -714,7 +738,9 @@ void cbmc_parse_optionst::preprocessing() } bool cbmc_parse_optionst::process_goto_program( - const optionst &options) + goto_modelt &goto_model, + const optionst &options, + messaget &log) { try { @@ -723,17 +749,17 @@ bool cbmc_parse_optionst::process_goto_program( remove_asm(goto_model); // add the library - link_to_library(goto_model, get_message_handler()); + link_to_library(goto_model, log.get_message_handler()); - if(cmdline.isset("string-abstraction")) - string_instrumentation(goto_model, get_message_handler()); + if(options.get_bool_option("string-abstraction")) + string_instrumentation(goto_model, log.get_message_handler()); // remove function pointers - status() << "Removal of function pointers and virtual functions" << eom; + log.status() << "Removal of function pointers and virtual functions" << eom; remove_function_pointers( - get_message_handler(), + log.get_message_handler(), goto_model, - cmdline.isset("pointer-check")); + options.get_bool_option("pointer-check")); // remove catch and throw (introduces instanceof) remove_exceptions(goto_model); @@ -749,7 +775,7 @@ bool cbmc_parse_optionst::process_goto_program( rewrite_union(goto_model); // add generic checks - status() << "Generic Property Instrumentation" << eom; + log.status() << "Generic Property Instrumentation" << eom; goto_check(options, goto_model); // checks don't know about adjusted float expressions @@ -757,19 +783,18 @@ bool cbmc_parse_optionst::process_goto_program( // ignore default/user-specified initialization // of variables with static lifetime - if(cmdline.isset("nondet-static")) + if(options.get_bool_option("nondet-static")) { - status() << "Adding nondeterministic initialization " - "of static/global variables" << eom; + log.status() << "Adding nondeterministic initialization " + "of static/global variables" + << eom; nondet_static(goto_model); } - if(cmdline.isset("string-abstraction")) + if(options.get_bool_option("string-abstraction")) { - status() << "String Abstraction" << eom; - string_abstraction( - goto_model, - get_message_handler()); + log.status() << "String Abstraction" << eom; + string_abstraction(goto_model, log.get_message_handler()); } // add failed symbols @@ -782,11 +807,11 @@ bool cbmc_parse_optionst::process_goto_program( // add loop ids goto_model.goto_functions.compute_loop_numbers(); - if(cmdline.isset("drop-unused-functions")) + if(options.get_bool_option("drop-unused-functions")) { // Entry point will have been set before and function pointers removed - status() << "Removing unused functions" << eom; - remove_unused_functions(goto_model, get_message_handler()); + log.status() << "Removing unused functions" << eom; + remove_unused_functions(goto_model, log.get_message_handler()); } // remove skips such that trivial GOTOs are deleted and not considered @@ -794,9 +819,9 @@ bool cbmc_parse_optionst::process_goto_program( remove_skip(goto_model); // instrument cover goals - if(cmdline.isset("cover")) + if(options.is_set("cover")) { - if(instrument_cover_goals(options, goto_model, get_message_handler())) + if(instrument_cover_goals(options, goto_model, log.get_message_handler())) return true; } @@ -808,37 +833,32 @@ bool cbmc_parse_optionst::process_goto_program( label_properties(goto_model); // reachability slice? - if(cmdline.isset("reachability-slice-fb")) + if(options.get_bool_option("reachability-slice-fb")) { - if(cmdline.isset("reachability-slice")) - { - error() << "--reachability-slice and --reachability-slice-fb " - << "must not be given together" << eom; - return true; - } - - status() << "Performing a forwards-backwards reachability slice" << eom; - if(cmdline.isset("property")) - reachability_slicer(goto_model, cmdline.get_values("property"), true); + log.status() << "Performing a forwards-backwards reachability slice" + << eom; + if(options.is_set("property")) + reachability_slicer( + goto_model, options.get_list_option("property"), true); else reachability_slicer(goto_model, true); } - if(cmdline.isset("reachability-slice")) + if(options.get_bool_option("reachability-slice")) { - status() << "Performing a reachability slice" << eom; - if(cmdline.isset("property")) - reachability_slicer(goto_model, cmdline.get_values("property")); + log.status() << "Performing a reachability slice" << eom; + if(options.is_set("property")) + reachability_slicer(goto_model, options.get_list_option("property")); else reachability_slicer(goto_model); } // full slice? - if(cmdline.isset("full-slice")) + if(options.get_bool_option("full-slice")) { - status() << "Performing a full slice" << eom; - if(cmdline.isset("property")) - property_slicer(goto_model, cmdline.get_values("property")); + log.status() << "Performing a full slice" << eom; + if(options.is_set("property")) + property_slicer(goto_model, options.get_list_option("property")); else full_slicer(goto_model); } @@ -849,25 +869,25 @@ bool cbmc_parse_optionst::process_goto_program( catch(const char *e) { - error() << e << eom; + log.error() << e << eom; return true; } catch(const std::string &e) { - error() << e << eom; + log.error() << e << eom; return true; } catch(int e) { - error() << "Numeric exception : " << e << eom; + log.error() << "Numeric exception : " << e << eom; return true; } catch(const std::bad_alloc &) { - error() << "Out of memory" << eom; + log.error() << "Out of memory" << eom; exit(CPROVER_EXIT_INTERNAL_OUT_OF_MEMORY); return true; } diff --git a/src/cbmc/cbmc_parse_options.h b/src/cbmc/cbmc_parse_options.h index 3b243321074..8f27472d97c 100644 --- a/src/cbmc/cbmc_parse_options.h +++ b/src/cbmc/cbmc_parse_options.h @@ -97,6 +97,15 @@ class cbmc_parse_optionst: /// default behaviour, for example unit tests. static void set_default_options(optionst &); + static bool process_goto_program(goto_modelt &, const optionst &, messaget &); + + static int get_goto_program( + goto_modelt &, + const optionst &, + const cmdlinet &, + messaget &, + ui_message_handlert &); + protected: goto_modelt goto_model; ui_message_handlert ui_message_handler; @@ -105,8 +114,6 @@ class cbmc_parse_optionst: void register_languages(); void get_command_line_options(optionst &); void preprocessing(); - int get_goto_program(const optionst &); - bool process_goto_program(const optionst &); bool set_properties(); };