From 32d49736ead97090375eef16917abda8df883382 Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Tue, 9 Oct 2018 17:48:27 +0100 Subject: [PATCH 1/3] Functions for outputting options This can be used to output the options set at the beginning of an analysis in order to understand the settings. --- src/util/options.cpp | 51 ++++++++++++++++++++++++++++++++++++++++++++ src/util/options.h | 7 ++++++ 2 files changed, 58 insertions(+) diff --git a/src/util/options.cpp b/src/util/options.cpp index 65c805a8b65..c75a02182c1 100644 --- a/src/util/options.cpp +++ b/src/util/options.cpp @@ -11,7 +11,9 @@ Author: Daniel Kroening, kroening@kroening.com #include "options.h" +#include "json.h" #include "string2int.h" +#include "xml.h" void optionst::set_option(const std::string &option, const std::string &value) @@ -84,3 +86,52 @@ const optionst::value_listt &optionst::get_list_option( else return it->second; } + +/// Returns the options as JSON key value pairs +json_objectt optionst::to_json() const +{ + json_objectt json_options; + for(const auto &option_pair : option_map) + { + json_arrayt &values = json_options[option_pair.first].make_array(); + for(const auto &value : option_pair.second) + values.push_back(json_stringt(value)); + } + return json_options; +} + +/// Returns the options in XML format +xmlt optionst::to_xml() const +{ + xmlt xml_options("options"); + for(const auto &option_pair : option_map) + { + xmlt &xml_option = xml_options.new_element("option"); + xml_option.set_attribute("name", option_pair.first); + for(const auto &value : option_pair.second) + { + xmlt &xml_value = xml_option.new_element("value"); + xml_value.data = value; + } + } + return xml_options; +} + +/// Outputs the options to `out` +void optionst::output(std::ostream &out) const +{ + for(const auto &option_pair : option_map) + { + out << option_pair.first << ": "; + bool first = true; + for(const auto &value : option_pair.second) + { + if(first) + first = false; + else + out << ", "; + out << '"' << value << '"'; + } + out << "\n"; + } +} diff --git a/src/util/options.h b/src/util/options.h index 741157740e6..d2e35c8c11c 100644 --- a/src/util/options.h +++ b/src/util/options.h @@ -16,6 +16,9 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +class json_objectt; +class xmlt; + class optionst { public: @@ -55,6 +58,10 @@ class optionst return *this; } + json_objectt to_json() const; + xmlt to_xml() const; + void output(std::ostream &out) const; + protected: option_mapt option_map; const value_listt empty_list; From 5741a43806eaf04f1719c3b03ea9fe5ec84fef50 Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Tue, 9 Oct 2018 21:39:45 +0100 Subject: [PATCH 2/3] Evaluate verbosity before producing output --- jbmc/src/jbmc/jbmc_parse_options.cpp | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/jbmc/src/jbmc/jbmc_parse_options.cpp b/jbmc/src/jbmc/jbmc_parse_options.cpp index 5a2a499eb07..35884eb742e 100644 --- a/jbmc/src/jbmc/jbmc_parse_options.cpp +++ b/jbmc/src/jbmc/jbmc_parse_options.cpp @@ -390,6 +390,9 @@ int jbmc_parse_optionst::doit() return 0; // should contemplate EX_OK from sysexits.h } + eval_verbosity( + cmdline.get_value("verbosity"), messaget::M_STATISTICS, ui_message_handler); + // // command line options // @@ -412,9 +415,6 @@ int jbmc_parse_optionst::doit() return 6; // should contemplate EX_SOFTWARE from sysexits.h } - eval_verbosity( - cmdline.get_value("verbosity"), messaget::M_STATISTICS, ui_message_handler); - // // Print a banner // From 5b8d9a3446cca538878af2d2bce0b723692d2270 Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Tue, 9 Oct 2018 21:44:09 +0100 Subject: [PATCH 3/3] Output options in JBMC --- .../regression/jbmc/output-options/Main.class | Bin 0 -> 340 bytes jbmc/regression/jbmc/output-options/Main.java | 6 +++++ jbmc/regression/jbmc/output-options/test.desc | 23 ++++++++++++++++++ jbmc/src/jbmc/jbmc_parse_options.cpp | 23 ++++++++++++++++++ 4 files changed, 52 insertions(+) create mode 100644 jbmc/regression/jbmc/output-options/Main.class create mode 100644 jbmc/regression/jbmc/output-options/Main.java create mode 100644 jbmc/regression/jbmc/output-options/test.desc diff --git a/jbmc/regression/jbmc/output-options/Main.class b/jbmc/regression/jbmc/output-options/Main.class new file mode 100644 index 0000000000000000000000000000000000000000..bd67b76274fe619b21e77a4bb8cfc4633c607d6a GIT binary patch literal 340 zcmZvWJx;?w5QX3PZ^6WI00}5?K^GE;-5rR`~bk!%g?fqMVcRsyWggDhk zUCk%CDsN;y=889w+7Pzdcj-tz%HCL-VK1vnZH6ZnjIv4=4+A-?{Q~QRFq_WHLS1Of zuMU_$uxJAwd>&{Egx24*>wKh&im>_53hcq*Z`UZ8iubdDB$Dl6q zTCDK>wO%snb8n}Ub{A)EKiPdovzr_qdrvOCe1BTnsp*gvyl$KQA!iYsC4|5l(HCMK I*Ql-04@m_-5C8xG literal 0 HcmV?d00001 diff --git a/jbmc/regression/jbmc/output-options/Main.java b/jbmc/regression/jbmc/output-options/Main.java new file mode 100644 index 00000000000..20c6646fb75 --- /dev/null +++ b/jbmc/regression/jbmc/output-options/Main.java @@ -0,0 +1,6 @@ +public class Main { + public static void main(String[] args) { + for(String arg : args) { + } + } +} diff --git a/jbmc/regression/jbmc/output-options/test.desc b/jbmc/regression/jbmc/output-options/test.desc new file mode 100644 index 00000000000..df330695097 --- /dev/null +++ b/jbmc/regression/jbmc/output-options/test.desc @@ -0,0 +1,23 @@ +CORE symex-driven-lazy-loading-expected-failure +Main.class +--verbosity 10 --unwind 2 --disable-uncaught-exception-check --throw-assertion-error +^VERIFICATION SUCCESSFUL$ +^EXIT=0$ +^SIGNAL=0$ +assertions: "1" +assumptions: "1" +java-threading: "0" +lazy-methods: "1" +propagation: "1" +refine-strings: "1" +sat-preprocessor: "1" +simplify: "1" +simplify-if: "1" +symex-driven-lazy-loading: "0" +throw-assertion-error: "1" +throw-runtime-exceptions: "0" +uncaught-exception-check: "0" +unwind: "2" +-- +-- +Symex-driven lazy loading would expect symex-driven-lazy-loading: "1". diff --git a/jbmc/src/jbmc/jbmc_parse_options.cpp b/jbmc/src/jbmc/jbmc_parse_options.cpp index 35884eb742e..60467ff66de 100644 --- a/jbmc/src/jbmc/jbmc_parse_options.cpp +++ b/jbmc/src/jbmc/jbmc_parse_options.cpp @@ -20,6 +20,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #include #include @@ -422,6 +423,28 @@ int jbmc_parse_optionst::doit() << "-bit " << config.this_architecture() << " " << config.this_operating_system() << eom; + // output the options + switch(ui_message_handler.get_ui()) + { + case ui_message_handlert::uit::PLAIN: + conditional_output(debug(), [&options](messaget::mstreamt &mstream) { + mstream << "\nOptions: \n"; + options.output(mstream); + mstream << messaget::eom; + }); + break; + case ui_message_handlert::uit::JSON_UI: + { + json_objectt json_options; + json_options["options"] = options.to_json(); + debug() << json_options; + break; + } + case ui_message_handlert::uit::XML_UI: + debug() << options.to_xml(); + break; + } + register_language(new_ansi_c_language); register_language(new_java_bytecode_language);