diff --git a/regression/goto-diff/java-properties/new.jar b/regression/goto-diff/java-properties/new.jar new file mode 100644 index 00000000000..d77d86e9ce3 Binary files /dev/null and b/regression/goto-diff/java-properties/new.jar differ diff --git a/regression/goto-diff/java-properties/new/Test.java b/regression/goto-diff/java-properties/new/Test.java new file mode 100644 index 00000000000..c7153bf65b1 --- /dev/null +++ b/regression/goto-diff/java-properties/new/Test.java @@ -0,0 +1,19 @@ +public class Test { + + private static Test static_test = null; + private Test test = new Test(); + + public Test() { + } + + public int foo(int x) { + if (x > 10) { + return x; + } else { + return x * 10; + } + } + + public void newfun() { + } +} diff --git a/regression/goto-diff/java-properties/old.jar b/regression/goto-diff/java-properties/old.jar new file mode 100644 index 00000000000..273b209df38 Binary files /dev/null and b/regression/goto-diff/java-properties/old.jar differ diff --git a/regression/goto-diff/java-properties/old/Test.java b/regression/goto-diff/java-properties/old/Test.java new file mode 100644 index 00000000000..793c46b6000 --- /dev/null +++ b/regression/goto-diff/java-properties/old/Test.java @@ -0,0 +1,19 @@ +public class Test { + + private static Test static_test = new Test(); + private Test test = null; + + public Test() { + } + + public int foo(int x) { + if (x > 10) { + return x; + } else { + return x * 10; + } + } + + public void obsolete() { + } +} diff --git a/regression/goto-diff/java-properties/test.desc b/regression/goto-diff/java-properties/test.desc new file mode 100644 index 00000000000..a615e2bf421 --- /dev/null +++ b/regression/goto-diff/java-properties/test.desc @@ -0,0 +1,10 @@ +CORE +new.jar +old.jar --json-ui --show-properties --cover location +// Enable multi-line checking +activate-multi-line-match +EXIT=0 +SIGNAL=0 + "deletedFunctions": \[\n {\n "name": "java::Test\.obsolete:\(\)V",\n "properties": \[\n {\n "class": "coverage",\n "coveredLines": "18",\n "description": "block 1",\n "expression": "false",\n "name": "java::Test\.obsolete:\(\)V\.coverage\.1",\n "sourceLocation": {\n "bytecodeIndex": "0",\n "file": "Test\.java",\n "function": "java::Test\.obsolete:\(\)V",\n "line": "18"\n }\n }\n ],\n "sourceLocation": {\n "file": "Test\.java",\n "function": "java::Test\.obsolete:\(\)V",\n "line": "18"\n }\n }\n ],\n "modifiedFunctions": \[\n {\n "name": "java::Test\.:\(\)V",\n "properties": \[\n {\n "class": "coverage",\n "coveredLines": "6",\n "description": "block 1",\n "expression": "false",\n "name": "java::Test\.:\(\)V\.coverage\.1",\n "sourceLocation": {\n "bytecodeIndex": "1",\n "file": "Test\.java",\n "function": "java::Test\.:\(\)V",\n "line": "6"\n }\n },\n {\n "class": "coverage",\n "coveredLines": "4",\n "description": "block 2",\n "expression": "false",\n "name": "java::Test\.:\(\)V\.coverage\.2",\n "sourceLocation": {\n "bytecodeIndex": "3",\n "file": "Test\.java",\n "function": "java::Test\.:\(\)V",\n "line": "4"\n }\n },\n {\n "class": "coverage",\n "coveredLines": "4",\n "description": "block 3",\n "expression": "false",\n "name": "java::Test\.:\(\)V\.coverage\.3",\n "sourceLocation": {\n "bytecodeIndex": "5",\n "file": "Test\.java",\n "function": "java::Test\.:\(\)V",\n "line": "4"\n }\n },\n {\n "class": "coverage",\n "coveredLines": "4,7",\n "description": "block 4",\n "expression": "false",\n "name": "java::Test\.:\(\)V\.coverage\.4",\n "sourceLocation": {\n "bytecodeIndex": "6",\n "file": "Test\.java",\n "function": "java::Test\.:\(\)V",\n "line": "4"\n }\n }\n ],\n "sourceLocation": {\n "file": "Test\.java",\n "function": "java::Test\.:\(\)V",\n "line": "6"\n }\n },\n {\n "name": "java::Test\.:\(\)V",\n "properties": \[\n {\n "class": "coverage",\n "coveredLines": "3",\n "description": "block 1",\n "expression": "false",\n "name": "java::Test\.:\(\)V\.coverage\.1",\n "sourceLocation": {\n "bytecodeIndex": "1",\n "file": "Test\.java",\n "function": "java::Test\.:\(\)V",\n "line": "3"\n }\n }\n ],\n "sourceLocation": {\n "file": "Test\.java",\n "function": "java::Test\.:\(\)V",\n "line": "3"\n }\n }\n ],\n "newFunctions": \[\n {\n "name": "java::Test\.newfun:\(\)V",\n "properties": \[\n {\n "class": "coverage",\n "coveredLines": "18",\n "description": "block 1",\n "expression": "false",\n "name": "java::Test\.newfun:\(\)V\.coverage\.1",\n "sourceLocation": {\n "bytecodeIndex": "0",\n "file": "Test\.java",\n "function": "java::Test\.newfun:\(\)V",\n "line": "18"\n }\n }\n ],\n "sourceLocation": {\n "file": "Test\.java",\n "function": "java::Test\.newfun:\(\)V",\n "line": "18"\n }\n }\n ],\n +-- +^warning: ignoring diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index 3496c6bf8ec..1048b322a0f 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -534,7 +534,8 @@ int cbmc_parse_optionst::doit() if(cmdline.isset("show-claims") || // will go away cmdline.isset("show-properties")) // use this one { - show_properties(goto_model, ui_message_handler.get_ui()); + show_properties( + goto_model, get_message_handler(), ui_message_handler.get_ui()); return CPROVER_EXIT_SUCCESS; } @@ -923,7 +924,7 @@ void cbmc_parse_optionst::help() " cbmc file.c ... source file names\n" "\n" "Analysis options:\n" - " --show-properties show the properties, but don't run analysis\n" // NOLINT(*) + HELP_SHOW_PROPERTIES " --symex-coverage-report f generate a Cobertura XML coverage report in f\n" // NOLINT(*) " --property id only check one specific property\n" " --stop-on-fail stop analysis once a failed property is detected\n" // NOLINT(*) diff --git a/src/cbmc/cbmc_parse_options.h b/src/cbmc/cbmc_parse_options.h index 658c552c22e..c5fe31e6b88 100644 --- a/src/cbmc/cbmc_parse_options.h +++ b/src/cbmc/cbmc_parse_options.h @@ -53,9 +53,9 @@ class optionst; "(aig)(16)(32)(64)(LP64)(ILP64)(LLP64)(ILP32)(LP32)" \ "(little-endian)(big-endian)" \ OPT_SHOW_GOTO_FUNCTIONS \ + OPT_SHOW_PROPERTIES \ "(show-loops)" \ "(show-symbol-table)(show-parse-tree)(show-vcc)" \ - "(show-claims)(claim):(show-properties)" \ "(drop-unused-functions)" \ "(property):(stop-on-fail)(trace)" \ "(error-label):(verbosity):(no-library)" \ @@ -72,7 +72,7 @@ class optionst; "(graphml-witness):" \ "(localize-faults)(localize-faults-method):" \ OPT_GOTO_TRACE \ - "(fixedbv)(floatbv)(all-claims)(all-properties)" // legacy, and will eventually disappear // NOLINT(whitespace/line_length) + "(claim):(show-claims)(fixedbv)(floatbv)(all-claims)(all-properties)" // legacy, and will eventually disappear // NOLINT(whitespace/line_length) // clang-format on class cbmc_parse_optionst: diff --git a/src/clobber/clobber_parse_options.cpp b/src/clobber/clobber_parse_options.cpp index 3f36a615272..fa04de3bed2 100644 --- a/src/clobber/clobber_parse_options.cpp +++ b/src/clobber/clobber_parse_options.cpp @@ -150,7 +150,7 @@ int clobber_parse_optionst::doit() if(cmdline.isset("show-properties")) { - show_properties(goto_model, get_ui()); + show_properties(goto_model, get_message_handler(), get_ui()); return 0; } diff --git a/src/clobber/clobber_parse_options.h b/src/clobber/clobber_parse_options.h index eb543f60138..2cbdd3c5523 100644 --- a/src/clobber/clobber_parse_options.h +++ b/src/clobber/clobber_parse_options.h @@ -19,23 +19,27 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include #include class goto_functionst; class optionst; +// clang-format off #define CLOBBER_OPTIONS \ "(depth):(context-bound):(unwind):" \ OPT_GOTO_CHECK \ OPT_SHOW_GOTO_FUNCTIONS \ + OPT_SHOW_PROPERTIES \ "(no-assertions)(no-assumptions)" \ "(error-label):(verbosity):(no-library)" \ "(version)" \ "(string-abstraction)" \ - "(show-locs)(show-vcc)(show-properties)(show-trace)" \ + "(show-locs)(show-vcc)(show-trace)" \ "(property):" \ JAVA_BYTECODE_LANGUAGE_OPTIONS +// clang-format on class clobber_parse_optionst: public parse_options_baset, diff --git a/src/goto-analyzer/goto_analyzer_parse_options.cpp b/src/goto-analyzer/goto_analyzer_parse_options.cpp index 2e4a97b3b0e..e686facd388 100644 --- a/src/goto-analyzer/goto_analyzer_parse_options.cpp +++ b/src/goto-analyzer/goto_analyzer_parse_options.cpp @@ -592,7 +592,7 @@ int goto_analyzer_parse_optionst::perform_analysis(const optionst &options) if(cmdline.isset("show-properties")) { - show_properties(goto_model, get_ui()); + show_properties(goto_model, get_message_handler(), get_ui()); return CPROVER_EXIT_SUCCESS; } @@ -815,6 +815,7 @@ void goto_analyzer_parse_optionst::help() std::cout << " * *\n"; + // clang-format off std::cout << "* * Daniel Kroening, DiffBlue * *\n" "* * kroening@kroening.com * *\n" @@ -898,8 +899,7 @@ void goto_analyzer_parse_optionst::help() " --show-parse-tree show parse tree\n" " --show-symbol-table show symbol table\n" HELP_SHOW_GOTO_FUNCTIONS - // NOLINTNEXTLINE(whitespace/line_length) - " --show-properties show the properties, but don't run analysis\n" + HELP_SHOW_PROPERTIES "\n" "Program instrumentation options:\n" HELP_GOTO_CHECK @@ -908,4 +908,5 @@ void goto_analyzer_parse_optionst::help() " --version show version and exit\n" HELP_TIMESTAMP "\n"; + // clang-format on } diff --git a/src/goto-analyzer/goto_analyzer_parse_options.h b/src/goto-analyzer/goto_analyzer_parse_options.h index d47f4ae91d3..ab1ff8b90cf 100644 --- a/src/goto-analyzer/goto_analyzer_parse_options.h +++ b/src/goto-analyzer/goto_analyzer_parse_options.h @@ -109,6 +109,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include #include #include @@ -119,6 +120,7 @@ class bmct; class goto_functionst; class optionst; +// clang-format off #define GOTO_ANALYSER_OPTIONS \ OPT_FUNCTIONS \ "D:I:(std89)(std99)(std11)" \ @@ -126,10 +128,11 @@ class optionst; "(16)(32)(64)(LP64)(ILP64)(LLP64)(ILP32)(LP32)" \ "(little-endian)(big-endian)" \ OPT_SHOW_GOTO_FUNCTIONS \ + OPT_SHOW_PROPERTIES \ OPT_GOTO_CHECK \ "(show-loops)" \ "(show-symbol-table)(show-parse-tree)" \ - "(show-properties)(show-reachable-properties)(property):" \ + "(show-reachable-properties)(property):" \ "(verbosity):(version)" \ "(gcc)(arch):" \ "(taint):(show-taint)" \ @@ -147,6 +150,7 @@ class optionst; "(location-sensitive)(concurrent)" \ "(no-simplify-slicing)" \ JAVA_BYTECODE_LANGUAGE_OPTIONS +// clang-format on class goto_analyzer_parse_optionst: public parse_options_baset, diff --git a/src/goto-diff/CMakeLists.txt b/src/goto-diff/CMakeLists.txt index 39f4bf011ec..2839634244c 100644 --- a/src/goto-diff/CMakeLists.txt +++ b/src/goto-diff/CMakeLists.txt @@ -13,6 +13,7 @@ target_link_libraries(goto-diff-lib linking big-int pointer-analysis + goto-instrument-lib goto-programs assembler analyses diff --git a/src/goto-diff/Makefile b/src/goto-diff/Makefile index 986085eb307..22304c2a5b7 100644 --- a/src/goto-diff/Makefile +++ b/src/goto-diff/Makefile @@ -15,6 +15,18 @@ OBJ += ../ansi-c/ansi-c$(LIBEXT) \ ../goto-programs/goto-programs$(LIBEXT) \ ../assembler/assembler$(LIBEXT) \ ../pointer-analysis/pointer-analysis$(LIBEXT) \ + ../goto-instrument/cover$(OBJEXT) \ + ../goto-instrument/cover_basic_blocks$(OBJEXT) \ + ../goto-instrument/cover_filter$(OBJEXT) \ + ../goto-instrument/cover_instrument_branch$(OBJEXT) \ + ../goto-instrument/cover_instrument_condition$(OBJEXT) \ + ../goto-instrument/cover_instrument_decision$(OBJEXT) \ + ../goto-instrument/cover_instrument_location$(OBJEXT) \ + ../goto-instrument/cover_instrument_mcdc$(OBJEXT) \ + ../goto-instrument/cover_instrument_other$(OBJEXT) \ + ../goto-instrument/cover_util$(OBJEXT) \ + ../goto-symex/adjust_float_expressions$(OBJEXT) \ + ../goto-symex/rewrite_union$(OBJEXT) \ ../analyses/analyses$(LIBEXT) \ ../langapi/langapi$(LIBEXT) \ ../xmllang/xmllang$(LIBEXT) \ diff --git a/src/goto-diff/goto_diff.h b/src/goto-diff/goto_diff.h index 23a65221358..0c637363e20 100644 --- a/src/goto-diff/goto_diff.h +++ b/src/goto-diff/goto_diff.h @@ -19,43 +19,57 @@ Author: Peter Schrammel #include +class optionst; + class goto_difft:public messaget { public: - explicit goto_difft( + goto_difft( const goto_modelt &_goto_model1, const goto_modelt &_goto_model2, - message_handlert &_message_handler - ) - : - messaget(_message_handler), - goto_model1(_goto_model1), - goto_model2(_goto_model2), - ui(ui_message_handlert::uit::PLAIN), - total_functions_count(0) - {} + const optionst &_options, + message_handlert &_message_handler) + : messaget(_message_handler), + goto_model1(_goto_model1), + goto_model2(_goto_model2), + options(_options), + ui(ui_message_handlert::uit::PLAIN), + total_functions_count(0) + { + } virtual bool operator()()=0; void set_ui(ui_message_handlert::uit _ui) { ui=_ui; } - virtual std::ostream &output_functions(std::ostream &out) const; + virtual void output_functions() const; protected: const goto_modelt &goto_model1; const goto_modelt &goto_model2; + const optionst &options; ui_message_handlert::uit ui; unsigned total_functions_count; typedef std::set irep_id_sett; irep_id_sett new_functions, modified_functions, deleted_functions; - void convert_function_group( + void output_function_group( + const std::string &group_name, + const irep_id_sett &function_group, + const goto_modelt &goto_model) const; + void output_function( + const irep_idt &function_name, + const goto_modelt &goto_model) const; + + void convert_function_group_json( json_arrayt &result, - const irep_id_sett &function_group) const; - void convert_function( + const irep_id_sett &function_group, + const goto_modelt &goto_model) const; + void convert_function_json( json_objectt &result, - const irep_idt &function_name) const; + const irep_idt &function_name, + const goto_modelt &goto_model) const; }; #endif // CPROVER_GOTO_DIFF_GOTO_DIFF_H diff --git a/src/goto-diff/goto_diff_base.cpp b/src/goto-diff/goto_diff_base.cpp index 32b6b2949af..49f79b9858d 100644 --- a/src/goto-diff/goto_diff_base.cpp +++ b/src/goto-diff/goto_diff_base.cpp @@ -11,40 +11,26 @@ Author: Peter Schrammel #include "goto_diff.h" +#include + #include +#include -std::ostream &goto_difft::output_functions(std::ostream &out) const +/// Output diff result +void goto_difft::output_functions() const { - namespacet ns1(goto_model1.symbol_table); - namespacet ns2(goto_model2.symbol_table); switch(ui) { case ui_message_handlert::uit::PLAIN: { - out << "total number of functions: " << total_functions_count << "\n"; - out << "new functions:\n"; - for(irep_id_sett::const_iterator it=new_functions.begin(); - it!=new_functions.end(); ++it) - { - const symbolt &symbol = ns2.lookup(*it); - out << " " << symbol.location.get_file() << ": " << *it << "\n"; - } - - out << "modified functions:\n"; - for(irep_id_sett::const_iterator it=modified_functions.begin(); - it!=modified_functions.end(); ++it) - { - const symbolt &symbol = ns2.lookup(*it); - out << " " << symbol.location.get_file() << ": " << *it << "\n"; - } - - out << "deleted functions:\n"; - for(irep_id_sett::const_iterator it=deleted_functions.begin(); - it!=deleted_functions.end(); ++it) - { - const symbolt &symbol = ns1.lookup(*it); - out << " " << symbol.location.get_file() << ": " << *it << "\n"; - } + result() << "total number of functions: " << total_functions_count + << '\n'; + output_function_group("new functions", new_functions, goto_model2); + output_function_group( + "modified functions", modified_functions, goto_model2); + output_function_group( + "deleted functions", deleted_functions, goto_model1); + result() << eom; break; } case ui_message_handlert::uit::JSON_UI: @@ -52,54 +38,115 @@ std::ostream &goto_difft::output_functions(std::ostream &out) const json_objectt json_result; json_result["totalNumberOfFunctions"]= json_stringt(std::to_string(total_functions_count)); - convert_function_group - (json_result["newFunctions"].make_array(), new_functions); - convert_function_group( - json_result["modifiedFunctions"].make_array(), modified_functions); - convert_function_group( - json_result["deletedFunctions"].make_array(), deleted_functions); - out << ",\n" << json_result; + convert_function_group_json( + json_result["newFunctions"].make_array(), new_functions, goto_model2); + convert_function_group_json( + json_result["modifiedFunctions"].make_array(), + modified_functions, + goto_model2); + convert_function_group_json( + json_result["deletedFunctions"].make_array(), + deleted_functions, + goto_model1); + result() << json_result; break; } case ui_message_handlert::uit::XML_UI: { - out << "not supported yet"; + error() << "XML output not supported yet" << eom; } } - return out; } -void goto_difft::convert_function_group( - json_arrayt &result, - const irep_id_sett &function_group) const +/// Output group of functions in plain text format +/// \param group_name: the name of the group, e.g. "modified functions" +/// \param function_group: set of function ids in the group +/// \param goto_model: the goto model +void goto_difft::output_function_group( + const std::string &group_name, + const irep_id_sett &function_group, + const goto_modelt &goto_model) const { - for(irep_id_sett::const_iterator it=function_group.begin(); - it!=function_group.end(); ++it) + result() << group_name << ":\n"; + for(const auto &function_name : function_group) { - convert_function(result.push_back(jsont()).make_object(), *it); + output_function(function_name, goto_model); } } -void goto_difft::convert_function( - json_objectt &result, - const irep_idt &function_name) const +/// Output function information in plain text format +/// \param function_name: the function id +/// \param goto_model: the goto model +void goto_difft::output_function( + const irep_idt &function_name, + const goto_modelt &goto_model) const +{ + namespacet ns(goto_model.symbol_table); + const symbolt &symbol = ns.lookup(function_name); + + result() << " " << symbol.location.get_file() << ": " << function_name + << '\n'; + + if(options.get_bool_option("show-properties")) + { + const auto goto_function_it = + goto_model.goto_functions.function_map.find(function_name); + CHECK_RETURN( + goto_function_it != goto_model.goto_functions.function_map.end()); + const goto_programt &goto_program = goto_function_it->second.body; + + for(const auto &ins : goto_program.instructions) + { + if(!ins.is_assert()) + continue; + + const source_locationt &source_location = ins.source_location; + irep_idt property_id = source_location.get_property_id(); + result() << " " << property_id << '\n'; + } + } +} + +/// Convert a function group to JSON +/// \param result: the JSON array to be populated +/// \param function_group: set of function ids in the group +/// \param goto_model: the goto model +void goto_difft::convert_function_group_json( + json_arrayt &result, + const irep_id_sett &function_group, + const goto_modelt &goto_model) const { - // the function may be in goto_model1 or goto_model2 - if( - goto_model1.goto_functions.function_map.find(function_name) != - goto_model1.goto_functions.function_map.end()) + for(const auto &function_name : function_group) { - const symbolt &symbol = - namespacet(goto_model1.symbol_table).lookup(function_name); - result["sourceLocation"] = json(symbol.location); + convert_function_json( + result.push_back(jsont()).make_object(), function_name, goto_model); } - else if( - goto_model2.goto_functions.function_map.find(function_name) != - goto_model2.goto_functions.function_map.end()) +} + +/// Convert function information to JSON +/// \param result: the JSON object to be populated +/// \param function_name: the function id +/// \param goto_model: the goto model +void goto_difft::convert_function_json( + json_objectt &result, + const irep_idt &function_name, + const goto_modelt &goto_model) const +{ + namespacet ns(goto_model.symbol_table); + const symbolt &symbol = ns.lookup(function_name); + + result["name"] = json_stringt(id2string(function_name)); + result["sourceLocation"] = json(symbol.location); + + if(options.get_bool_option("show-properties")) { - const symbolt &symbol = - namespacet(goto_model2.symbol_table).lookup(function_name); - result["sourceLocation"] = json(symbol.location); + const auto goto_function_it = + goto_model.goto_functions.function_map.find(function_name); + CHECK_RETURN( + goto_function_it != goto_model.goto_functions.function_map.end()); + const goto_programt &goto_program = goto_function_it->second.body; + + convert_properties_json( + result["properties"].make_array(), ns, function_name, goto_program); } - result["name"]=json_stringt(id2string(function_name)); } diff --git a/src/goto-diff/goto_diff_parse_options.cpp b/src/goto-diff/goto_diff_parse_options.cpp index 87e8c98e5d2..232ebf029b3 100644 --- a/src/goto-diff/goto_diff_parse_options.cpp +++ b/src/goto-diff/goto_diff_parse_options.cpp @@ -20,16 +20,23 @@ Author: Peter Schrammel #include #include #include +#include #include #include +#include +#include #include +#include +#include #include +#include #include #include #include #include +#include #include #include #include @@ -39,8 +46,15 @@ Author: Peter Schrammel #include #include +#include +#include + +#include + #include +#include + #include #include @@ -99,7 +113,7 @@ void goto_diff_parse_optionst::get_command_line_options(optionst &options) options.set_option("show-vcc", true); if(cmdline.isset("cover")) - options.set_option("cover", cmdline.get_value("cover")); + parse_cover_options(cmdline, options); if(cmdline.isset("mm")) options.set_option("mm", cmdline.get_value("mm")); @@ -122,22 +136,8 @@ void goto_diff_parse_optionst::get_command_line_options(optionst &options) if(cmdline.isset("cpp11")) config.cpp.set_cpp11(); - if(cmdline.isset("no-simplify")) - options.set_option("simplify", false); - else - options.set_option("simplify", true); - - if(cmdline.isset("all-claims") || // will go away - cmdline.isset("all-properties")) // use this one - options.set_option("all-properties", true); - else - options.set_option("all-properties", false); - - if(cmdline.isset("unwind")) - options.set_option("unwind", cmdline.get_value("unwind")); - - if(cmdline.isset("depth")) - options.set_option("depth", cmdline.get_value("depth")); + // all checks supported by goto_check + PARSE_OPTIONS_GOTO_CHECK(cmdline, options); if(cmdline.isset("debug-level")) options.set_option("debug-level", cmdline.get_value("debug-level")); @@ -236,6 +236,8 @@ void goto_diff_parse_optionst::get_command_line_options(optionst &options) << " must not be given together" << eom; exit(1); } + + options.set_option("show-properties", cmdline.isset("show-properties")); } /// invoke main modules @@ -244,7 +246,7 @@ int goto_diff_parse_optionst::doit() if(cmdline.isset("version")) { std::cout << CBMC_VERSION << '\n'; - return 0; + return CPROVER_EXIT_SUCCESS; } // @@ -266,7 +268,7 @@ int goto_diff_parse_optionst::doit() if(cmdline.args.size()!=2) { error() << "Please provide two programs to compare" << eom; - return 6; + return CPROVER_EXIT_INCORRECT_TASK; } goto_modelt goto_model1, goto_model2; @@ -284,7 +286,7 @@ int goto_diff_parse_optionst::doit() { show_loop_ids(get_ui(), goto_model1); show_loop_ids(get_ui(), goto_model2); - return true; + return CPROVER_EXIT_SUCCESS; } if( @@ -301,17 +303,13 @@ int goto_diff_parse_optionst::doit() get_message_handler(), ui_message_handler.get_ui(), cmdline.isset("list-goto-functions")); - return 0; + return CPROVER_EXIT_SUCCESS; } if(cmdline.isset("change-impact") || cmdline.isset("forward-impact") || cmdline.isset("backward-impact")) { - // Workaround to avoid deps not propagating between return and end_func - remove_returns(goto_model1); - remove_returns(goto_model2); - impact_modet impact_mode= cmdline.isset("forward-impact") ? impact_modet::FORWARD : @@ -324,7 +322,7 @@ int goto_diff_parse_optionst::doit() impact_mode, cmdline.isset("compact-output")); - return 0; + return CPROVER_EXIT_SUCCESS; } if(cmdline.isset("unified") || @@ -334,15 +332,15 @@ int goto_diff_parse_optionst::doit() u(); u.output(std::cout); - return 0; + return CPROVER_EXIT_SUCCESS; } - syntactic_difft sd(goto_model1, goto_model2, get_message_handler()); + syntactic_difft sd(goto_model1, goto_model2, options, get_message_handler()); sd.set_ui(get_ui()); sd(); - sd.output_functions(std::cout); + sd.output_functions(); - return 0; + return CPROVER_EXIT_SUCCESS; } int goto_diff_parse_optionst::get_goto_program( @@ -359,7 +357,7 @@ int goto_diff_parse_optionst::get_goto_program( goto_model.symbol_table, goto_model.goto_functions, languages.get_message_handler())) - return 6; + return CPROVER_EXIT_INCORRECT_TASK; config.set(cmdline); @@ -380,7 +378,7 @@ int goto_diff_parse_optionst::get_goto_program( if(languages.parse() || languages.typecheck() || languages.final()) - return 6; + return CPROVER_EXIT_INCORRECT_TASK; // we no longer need any parse trees or language files languages.clear_parse(); @@ -393,6 +391,9 @@ int goto_diff_parse_optionst::get_goto_program( goto_model.goto_functions, ui_message_handler); + if(process_goto_program(options, goto_model)) + return CPROVER_EXIT_INTERNAL_ERROR; + // if we had a second argument then we will handle it next if(arg2!="") cmdline.args[0]=arg2; @@ -405,46 +406,72 @@ bool goto_diff_parse_optionst::process_goto_program( const optionst &options, goto_modelt &goto_model) { - symbol_tablet &symbol_table = goto_model.symbol_table; - goto_functionst &goto_functions = goto_model.goto_functions; - try { - namespacet ns(symbol_table); - // Remove inline assembler; this needs to happen before // adding the library. remove_asm(goto_model); // add the library - link_to_library(symbol_table, goto_functions, ui_message_handler); + link_to_library(goto_model, get_message_handler()); // remove function pointers - status() << "Function Pointer Removal" << eom; + status() << "Removal of function pointers and virtual functions" << eom; remove_function_pointers( - get_message_handler(), - symbol_table, - goto_functions, - cmdline.isset("pointer-check")); + get_message_handler(), goto_model, cmdline.isset("pointer-check")); - // do partial inlining - status() << "Partial Inlining" << eom; - goto_partial_inline(goto_functions, ns, ui_message_handler); + // Java virtual functions -> explicit dispatch tables: + remove_virtual_functions(goto_model); + // remove catch and throw + remove_exceptions(goto_model); + // Java instanceof -> clsid comparison: + remove_instanceof(goto_model); + + mm_io(goto_model); + + // instrument library preconditions + instrument_preconditions(goto_model); // remove returns, gcc vectors, complex - remove_returns(symbol_table, goto_functions); - remove_vector(symbol_table, goto_functions); - remove_complex(symbol_table, goto_functions); + remove_returns(goto_model); + remove_vector(goto_model); + remove_complex(goto_model); + rewrite_union(goto_model); + + // add generic checks + status() << "Generic Property Instrumentation" << eom; + goto_check(options, goto_model); - // add failed symbols - // needs to be done before pointer analysis - add_failed_symbols(symbol_table); + // checks don't know about adjusted float expressions + adjust_float_expressions(goto_model); // recalculate numbers, etc. - goto_functions.update(); + goto_model.goto_functions.update(); // add loop ids - goto_functions.compute_loop_numbers(); + goto_model.goto_functions.compute_loop_numbers(); + + // remove skips such that trivial GOTOs are deleted and not considered + // for coverage annotation: + remove_skip(goto_model); + + // instrument cover goals + if(cmdline.isset("cover")) + { + if(instrument_cover_goals(options, goto_model, get_message_handler())) + return true; + } + + // label the assertions + // This must be done after adding assertions and + // before using the argument of the "property" option. + // Do not re-label after using the property slicer because + // this would cause the property identifiers to change. + label_properties(goto_model); + + // remove any skips introduced since coverage instrumentation + remove_skip(goto_model); + goto_model.goto_functions.update(); } catch(const char *e) @@ -459,14 +486,16 @@ bool goto_diff_parse_optionst::process_goto_program( return true; } - catch(int) + catch(int e) { + error() << "Numeric exception: " << e << eom; return true; } catch(const std::bad_alloc &) { error() << "Out of memory" << eom; + exit(CPROVER_EXIT_INTERNAL_OUT_OF_MEMORY); return true; } @@ -476,6 +505,7 @@ bool goto_diff_parse_optionst::process_goto_program( /// display command line help void goto_diff_parse_optionst::help() { + // clang-format off std::cout << "\n" // NOLINTNEXTLINE(whitespace/line_length) @@ -490,6 +520,7 @@ void goto_diff_parse_optionst::help() "\n" "Diff options:\n" HELP_SHOW_GOTO_FUNCTIONS + HELP_SHOW_PROPERTIES " --syntactic do syntactic diff (default)\n" " -u | --unified output unified diff\n" " --change-impact | \n" @@ -498,9 +529,15 @@ void goto_diff_parse_optionst::help() " --backward-impact output unified diff with forward&backward/forward/backward dependencies\n" " --compact-output output dependencies in compact mode\n" "\n" + "Program instrumentation options:\n" + HELP_GOTO_CHECK + " --cover CC create test-suite with coverage criterion CC\n" // NOLINT(*) + "Java Bytecode frontend options:\n" + JAVA_BYTECODE_LANGUAGE_OPTIONS_HELP "Other options:\n" " --version show version and exit\n" " --json-ui use JSON-formatted output\n" HELP_TIMESTAMP "\n"; + // clang-format on } diff --git a/src/goto-diff/goto_diff_parse_options.h b/src/goto-diff/goto_diff_parse_options.h index 8eb8e58f1c2..48dcb89aa43 100644 --- a/src/goto-diff/goto_diff_parse_options.h +++ b/src/goto-diff/goto_diff_parse_options.h @@ -12,25 +12,33 @@ Author: Peter Schrammel #ifndef CPROVER_GOTO_DIFF_GOTO_DIFF_PARSE_OPTIONS_H #define CPROVER_GOTO_DIFF_GOTO_DIFF_PARSE_OPTIONS_H +#include + #include #include #include #include #include +#include #include "goto_diff_languages.h" class goto_modelt; class optionst; +// clang-format off #define GOTO_DIFF_OPTIONS \ "(json-ui)" \ OPT_SHOW_GOTO_FUNCTIONS \ + OPT_SHOW_PROPERTIES \ + OPT_GOTO_CHECK \ + "(cover):" \ "(verbosity):(version)" \ OPT_TIMESTAMP \ "u(unified)(change-impact)(forward-impact)(backward-impact)" \ "(compact-output)" +// clang-format on class goto_diff_parse_optionst: public parse_options_baset, diff --git a/src/goto-diff/syntactic_diff.h b/src/goto-diff/syntactic_diff.h index 8496eb8165e..b5a2b3216e2 100644 --- a/src/goto-diff/syntactic_diff.h +++ b/src/goto-diff/syntactic_diff.h @@ -16,12 +16,13 @@ Author: Peter Schrammel class syntactic_difft:public goto_difft { - public: - explicit syntactic_difft( +public: + syntactic_difft( const goto_modelt &_goto_model1, const goto_modelt &_goto_model2, - message_handlert &_message_handler): - goto_difft(_goto_model1, _goto_model2, _message_handler) + const optionst &_options, + message_handlert &_message_handler) + : goto_difft(_goto_model1, _goto_model2, _options, _message_handler) { } diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp index a98acd741f6..796a47ae508 100644 --- a/src/goto-instrument/goto_instrument_parse_options.cpp +++ b/src/goto-instrument/goto_instrument_parse_options.cpp @@ -532,7 +532,7 @@ int goto_instrument_parse_optionst::doit() cmdline.isset("show-properties")) { const namespacet ns(goto_model.symbol_table); - show_properties(goto_model, get_ui()); + show_properties(goto_model, get_message_handler(), get_ui()); return CPROVER_EXIT_SUCCESS; } @@ -1452,6 +1452,7 @@ void goto_instrument_parse_optionst::instrument_goto_program() /// display command line help void goto_instrument_parse_optionst::help() { + // clang-format off std::cout << "\n" "* * Goto-Instrument " CBMC_VERSION " - Copyright (C) 2008-2013 * *\n" // NOLINT(*) @@ -1475,7 +1476,7 @@ void goto_instrument_parse_optionst::help() "\n" "Diagnosis:\n" " --show-loops show the loops in the program\n" - " --show-properties show the properties\n" + HELP_SHOW_PROPERTIES " --show-symbol-table show symbol table\n" " --list-symbols list symbols with type information\n" HELP_SHOW_GOTO_FUNCTIONS @@ -1570,4 +1571,5 @@ void goto_instrument_parse_optionst::help() " --json-ui use JSON-formatted output\n" HELP_TIMESTAMP "\n"; + // clang-format on } diff --git a/src/goto-instrument/goto_instrument_parse_options.h b/src/goto-instrument/goto_instrument_parse_options.h index 19acc24b44f..77e69dded9f 100644 --- a/src/goto-instrument/goto_instrument_parse_options.h +++ b/src/goto-instrument/goto_instrument_parse_options.h @@ -18,10 +18,12 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include #include #include +// clang-format off #define GOTO_INSTRUMENT_OPTIONS \ "(all)" \ "(document-claims-latex)(document-claims-html)" \ @@ -51,6 +53,7 @@ Author: Daniel Kroening, kroening@kroening.com "(stack-depth):(nondet-static)" \ "(function-enter):(function-exit):(branch):" \ OPT_SHOW_GOTO_FUNCTIONS \ + OPT_SHOW_PROPERTIES \ "(drop-unused-functions)" \ "(show-value-sets)" \ "(show-global-may-alias)" \ @@ -64,7 +67,7 @@ Author: Daniel Kroening, kroening@kroening.com OPT_REMOVE_CONST_FUNCTION_POINTERS \ "(print-internal-representation)" \ "(remove-function-pointers)" \ - "(show-claims)(show-properties)(property):" \ + "(show-claims)(property):" \ "(show-symbol-table)(show-points-to)(show-rw-set)" \ "(cav11)" \ OPT_TIMESTAMP \ @@ -81,8 +84,8 @@ Author: Daniel Kroening, kroening@kroening.com "(show-threaded)(list-calls-args)(print-path-lengths)" \ "(undefined-function-is-assume-false)" \ "(remove-function-body):"\ - "(splice-call):" \ - + "(splice-call):" +// clang-format on class goto_instrument_parse_optionst: public parse_options_baset, diff --git a/src/goto-programs/show_properties.cpp b/src/goto-programs/show_properties.cpp index 3393923ca75..6df2f69bf33 100644 --- a/src/goto-programs/show_properties.cpp +++ b/src/goto-programs/show_properties.cpp @@ -46,13 +46,14 @@ optionalt find_property( return { }; } - void show_properties( const namespacet &ns, const irep_idt &identifier, + message_handlert &message_handler, ui_message_handlert::uit ui, const goto_programt &goto_program) { + messaget msg(message_handler); for(const auto &ins : goto_program.instructions) { if(!ins.is_assert()) @@ -83,7 +84,7 @@ void show_properties( xml_property.new_element("expression").data= from_expr(ns, identifier, ins.guard); - std::cout << xml_property << '\n'; + msg.result() << xml_property; } break; @@ -92,14 +93,13 @@ void show_properties( break; case ui_message_handlert::uit::PLAIN: - std::cout << "Property " << property_id << ":\n"; + msg.result() << "Property " << property_id << ":\n"; - std::cout << " " << ins.source_location << '\n' - << " " << description << '\n' - << " " << from_expr(ns, identifier, ins.guard) - << '\n'; + msg.result() << " " << ins.source_location << '\n' + << " " << description << '\n' + << " " << from_expr(ns, identifier, ins.guard) << '\n'; - std::cout << '\n'; + msg.result() << messaget::eom; break; default: @@ -108,8 +108,7 @@ void show_properties( } } - -void show_properties_json( +void convert_properties_json( json_arrayt &json_properties, const namespacet &ns, const irep_idt &identifier, @@ -147,43 +146,43 @@ void show_properties_json( void show_properties_json( const namespacet &ns, + message_handlert &message_handler, const goto_functionst &goto_functions) { + messaget msg(message_handler); json_arrayt json_properties; for(const auto &fct : goto_functions.function_map) if(!fct.second.is_inlined()) - show_properties_json( - json_properties, - ns, - fct.first, - fct.second.body); + convert_properties_json(json_properties, ns, fct.first, fct.second.body); json_objectt json_result; json_result["properties"] = json_properties; - std::cout << ",\n" << json_result; + msg.result() << json_result; } void show_properties( const namespacet &ns, + message_handlert &message_handler, ui_message_handlert::uit ui, const goto_functionst &goto_functions) { if(ui == ui_message_handlert::uit::JSON_UI) - show_properties_json(ns, goto_functions); + show_properties_json(ns, message_handler, goto_functions); else for(const auto &fct : goto_functions.function_map) if(!fct.second.is_inlined()) - show_properties(ns, fct.first, ui, fct.second.body); + show_properties(ns, fct.first, message_handler, ui, fct.second.body); } void show_properties( const goto_modelt &goto_model, + message_handlert &message_handler, ui_message_handlert::uit ui) { const namespacet ns(goto_model.symbol_table); if(ui == ui_message_handlert::uit::JSON_UI) - show_properties_json(ns, goto_model.goto_functions); + show_properties_json(ns, message_handler, goto_model.goto_functions); else - show_properties(ns, ui, goto_model.goto_functions); + show_properties(ns, message_handler, ui, goto_model.goto_functions); } diff --git a/src/goto-programs/show_properties.h b/src/goto-programs/show_properties.h index 145a195fa8d..ce4cb341c25 100644 --- a/src/goto-programs/show_properties.h +++ b/src/goto-programs/show_properties.h @@ -18,14 +18,26 @@ Author: Daniel Kroening, kroening@kroening.com class namespacet; class goto_modelt; class symbol_tablet; +class goto_programt; class goto_functionst; +class message_handlert; + +// clang-format off +#define OPT_SHOW_PROPERTIES \ + "(show-properties)" + +#define HELP_SHOW_PROPERTIES \ + " --show-properties show the properties, but don't run analysis\n" // NOLINT(*) +// clang-format on void show_properties( const goto_modelt &, + message_handlert &message_handler, ui_message_handlert::uit ui); void show_properties( const namespacet &ns, + message_handlert &message_handler, ui_message_handlert::uit ui, const goto_functionst &goto_functions); @@ -40,4 +52,15 @@ optionalt find_property( const irep_idt &property, const goto_functionst &goto_functions); +/// \brief Collects the properties in the goto program into a `json_arrayt` +/// \param json_properties: JSON array to hold the properties +/// \param ns: namespace +/// \param identifier: function id of the goto program +/// \param goto_program: the goto program +void convert_properties_json( + json_arrayt &json_properties, + const namespacet &ns, + const irep_idt &identifier, + const goto_programt &goto_program); + #endif // CPROVER_GOTO_PROGRAMS_SHOW_PROPERTIES_H diff --git a/src/jbmc/jbmc_parse_options.cpp b/src/jbmc/jbmc_parse_options.cpp index dc45b4830ed..65075e12abf 100644 --- a/src/jbmc/jbmc_parse_options.cpp +++ b/src/jbmc/jbmc_parse_options.cpp @@ -484,7 +484,8 @@ int jbmc_parse_optionst::doit() if(cmdline.isset("show-properties")) { - show_properties(goto_model, ui_message_handler.get_ui()); + show_properties( + goto_model, get_message_handler(), ui_message_handler.get_ui()); return 0; // should contemplate EX_OK from sysexits.h } @@ -877,6 +878,7 @@ void jbmc_parse_optionst::help() std::cout << " * *\n"; + // clang-format off std::cout << "* * Daniel Kroening, Edmund Clarke * *\n" "* * Carnegie Mellon University, Computer Science Department * *\n" @@ -888,7 +890,7 @@ void jbmc_parse_optionst::help() " jbmc class name of class to be checked\n" "\n" "Analysis options:\n" - " --show-properties show the properties, but don't run analysis\n" // NOLINT(*) + HELP_SHOW_PROPERTIES " --symex-coverage-report f generate a Cobertura XML coverage report in f\n" // NOLINT(*) " --property id only check one specific property\n" " --stop-on-fail stop analysis once a failed property is detected\n" // NOLINT(*) @@ -961,4 +963,5 @@ void jbmc_parse_optionst::help() " --verbosity # verbosity level\n" HELP_TIMESTAMP "\n"; + // clang-format on } diff --git a/src/jbmc/jbmc_parse_options.h b/src/jbmc/jbmc_parse_options.h index 362011b8f33..c2793540805 100644 --- a/src/jbmc/jbmc_parse_options.h +++ b/src/jbmc/jbmc_parse_options.h @@ -22,6 +22,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include #include @@ -55,7 +56,7 @@ class optionst; OPT_SHOW_GOTO_FUNCTIONS \ "(show-loops)" \ "(show-symbol-table)(show-parse-tree)(show-vcc)" \ - "(show-properties)" \ + OPT_SHOW_PROPERTIES \ "(drop-unused-functions)" \ "(property):(stop-on-fail)(trace)" \ "(verbosity):" \