From 8c633e08e004bcc97134a07858ed365ff5c2f2c5 Mon Sep 17 00:00:00 2001 From: Martin Brain Date: Thu, 8 Sep 2016 07:58:26 +0100 Subject: [PATCH 01/13] Add XML and JSON output to the base of both domains and analysis. --- src/analyses/ai.cpp | 152 ++++++++++++++++++++++++++++++++++++++++++++ src/analyses/ai.h | 88 +++++++++++++++++++++++++ 2 files changed, 240 insertions(+) diff --git a/src/analyses/ai.cpp b/src/analyses/ai.cpp index 552649d6009..d1ad335b082 100644 --- a/src/analyses/ai.cpp +++ b/src/analyses/ai.cpp @@ -82,6 +82,158 @@ void ai_baset::output( /*******************************************************************\ +Function: ai_baset::output_json + + Inputs: The namespace and goto_functions + + Outputs: The JSON object + + Purpose: Output the domains for the whole program as JSON + +\*******************************************************************/ + +jsont ai_baset::output_json( + const namespacet &ns, + const goto_functionst &goto_functions) const +{ + json_objectt result; + + forall_goto_functions(f_it, goto_functions) + { + if(f_it->second.body_available()) + { + result[id2string(f_it->first)]= + output_json(ns, f_it->second.body, f_it->first); + } + else + { + result[id2string(f_it->first)]=json_arrayt(); + } + } + + return result; +} + +/*******************************************************************\ + +Function: ai_baset::output_json + + Inputs: The namespace, goto_program and it's identifier + + Outputs: The JSON object + + Purpose: Output the domains for a single function as JSON + +\*******************************************************************/ + +jsont ai_baset::output_json( + const namespacet &ns, + const goto_programt &goto_program, + const irep_idt &identifier) const +{ + json_arrayt contents; + + forall_goto_program_instructions(i_it, goto_program) + { + json_objectt location; + location["location_number"]= + json_numbert(std::to_string(i_it->location_number)); + location["source_location"]= + json_stringt(i_it->source_location.as_string()); + location["domain"]=find_state(i_it).output_json(*this, ns); + + // Ideally we need output_instruction_json + std::ostringstream out; + goto_program.output_instruction(ns, identifier, out, i_it); + location["instruction"]=json_stringt(out.str()); + + contents.push_back(location); + } + + return contents; +} + +/*******************************************************************\ + +Function: ai_baset::output_xml + + Inputs: The namespace and goto_functions + + Outputs: The XML object + + Purpose: Output the domains for the whole program as XML + +\*******************************************************************/ + +xmlt ai_baset::output_xml( + const namespacet &ns, + const goto_functionst &goto_functions) const +{ + xmlt program("program"); + + forall_goto_functions(f_it, goto_functions) + { + xmlt function("function"); + function.set_attribute("name", id2string(f_it->first)); + function.set_attribute( + "body_available", + f_it->second.body_available() ? "true" : "false"); + + if(f_it->second.body_available()) + { + function.new_element(output_xml(ns, f_it->second.body, f_it->first)); + } + + program.new_element(function); + } + + return program; +} + +/*******************************************************************\ + +Function: ai_baset::output_xml + + Inputs: The namespace, goto_program and it's identifier + + Outputs: The XML object + + Purpose: Output the domains for a single function as XML + +\*******************************************************************/ + +xmlt ai_baset::output_xml( + const namespacet &ns, + const goto_programt &goto_program, + const irep_idt &identifier) const +{ + xmlt function_body; + + forall_goto_program_instructions(i_it, goto_program) + { + xmlt location; + location.set_attribute( + "location_number", + std::to_string(i_it->location_number)); + location.set_attribute( + "source_location", + i_it->source_location.as_string()); + + location.new_element(find_state(i_it).output_xml(*this, ns)); + + // Ideally we need output_instruction_xml + std::ostringstream out; + goto_program.output_instruction(ns, identifier, out, i_it); + location.set_attribute("instruction", out.str()); + + function_body.new_element(location); + } + + return function_body; +} + +/*******************************************************************\ + Function: ai_baset::entry_state Inputs: diff --git a/src/analyses/ai.h b/src/analyses/ai.h index 10a9831d1c5..db2027ed919 100644 --- a/src/analyses/ai.h +++ b/src/analyses/ai.h @@ -11,6 +11,10 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include + +#include +#include #include @@ -53,6 +57,27 @@ class ai_domain_baset { } + virtual jsont output_json( + const ai_baset &ai, + const namespacet &ns) const + { + std::ostringstream out; + output(out, ai, ns); + json_stringt json(out.str()); + return json; + } + + virtual xmlt output_xml( + const ai_baset &ai, + const namespacet &ns) const + { + std::ostringstream out; + output(out, ai, ns); + xmlt xml("domain"); + xml.data=out.str(); + return xml; + } + // no states virtual void make_bottom()=0; @@ -157,6 +182,58 @@ class ai_baset output(ns, goto_function.body, "", out); } + + virtual jsont output_json( + const namespacet &ns, + const goto_functionst &goto_functions) const; + + jsont output_json( + const goto_modelt &goto_model) const + { + const namespacet ns(goto_model.symbol_table); + return output_json(ns, goto_model.goto_functions); + } + + jsont output_json( + const namespacet &ns, + const goto_programt &goto_program) const + { + return output_json(ns, goto_program, ""); + } + + jsont output_json( + const namespacet &ns, + const goto_functionst::goto_functiont &goto_function) const + { + return output_json(ns, goto_function.body, ""); + } + + + virtual xmlt output_xml( + const namespacet &ns, + const goto_functionst &goto_functions) const; + + xmlt output_xml( + const goto_modelt &goto_model) const + { + const namespacet ns(goto_model.symbol_table); + return output_xml(ns, goto_model.goto_functions); + } + + xmlt output_xml( + const namespacet &ns, + const goto_programt &goto_program) const + { + return output_xml(ns, goto_program, ""); + } + + xmlt output_xml( + const namespacet &ns, + const goto_functionst::goto_functiont &goto_function) const + { + return output_xml(ns, goto_function.body, ""); + } + protected: // overload to add a factory virtual void initialize(const goto_programt &); @@ -172,6 +249,17 @@ class ai_baset const irep_idt &identifier, std::ostream &out) const; + virtual jsont output_json( + const namespacet &ns, + const goto_programt &goto_program, + const irep_idt &identifier) const; + + virtual xmlt output_xml( + const namespacet &ns, + const goto_programt &goto_program, + const irep_idt &identifier) const; + + // the work-queue is sorted by location number typedef std::map working_sett; From 63c956438fc417e00e328845c6a04b82f9ad0e1f Mon Sep 17 00:00:00 2001 From: Martin Brain Date: Thu, 8 Sep 2016 08:05:42 +0100 Subject: [PATCH 02/13] Make evaluation and/or simplification of conditions a domain operation. --- src/analyses/ai.h | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/src/analyses/ai.h b/src/analyses/ai.h index db2027ed919..574f84eadaf 100644 --- a/src/analyses/ai.h +++ b/src/analyses/ai.h @@ -15,6 +15,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include #include @@ -94,6 +95,17 @@ class ai_domain_baset // // This computes the join between "this" and "b". // Return true if "this" has changed. + + // This method allows an expression to be simplified / evaluated using the + // current value of the domain. It is used to evaluate assertions and in + // program simplification + virtual exprt domain_simplify( + const exprt &condition, + const namespacet &ns, + const bool lhs=false) const + { + return condition; + } }; // don't use me -- I am just a base class From 0f25befdf4aca5cbf57f7c920ec969c9e16f44f3 Mon Sep 17 00:00:00 2001 From: martin Date: Fri, 16 Dec 2016 16:39:29 +0000 Subject: [PATCH 03/13] Implement domain_simplify for intervals. --- src/analyses/interval_domain.cpp | 70 +++++++++++++++++++++++++++++--- src/analyses/interval_domain.h | 12 +++++- 2 files changed, 76 insertions(+), 6 deletions(-) diff --git a/src/analyses/interval_domain.cpp b/src/analyses/interval_domain.cpp index 0d5ca3d80aa..a75f1bf4964 100644 --- a/src/analyses/interval_domain.cpp +++ b/src/analyses/interval_domain.cpp @@ -127,7 +127,7 @@ void interval_domaint::transform( /*******************************************************************\ -Function: interval_domaint::merge +Function: interval_domaint::join Inputs: @@ -137,10 +137,8 @@ Function: interval_domaint::merge \*******************************************************************/ -bool interval_domaint::merge( - const interval_domaint &b, - locationt from, - locationt to) +bool interval_domaint::join( + const interval_domaint &b) { if(b.bottom) return false; if(bottom) { *this=b; return true; } @@ -498,3 +496,65 @@ exprt interval_domaint::make_expression(const symbol_exprt &src) const else return true_exprt(); } + +/*******************************************************************\ + +Function: interval_domaint::domain_simplify + + Inputs: The expression to simplify. + + Outputs: A simplified version of the expression. + + Purpose: Uses the domain to simplify a given expression using context-specific information. + +\*******************************************************************/ + +exprt interval_domaint::domain_simplify( + const exprt &condition, + const namespacet &ns, + const bool lhs) const +{ + if(lhs) + { + // For now do not simplify the left hand side of assignments + return condition; + } + + interval_domaint d(*this); + + // merge intervals to properly handle conjunction + if(condition.id()==ID_and) + { + interval_domaint a; + a.make_top(); + a.assume(condition, ns); + +#ifdef DEBUG + a.output(std::cout, interval_analysis, ns); + d.output(std::cout, interval_analysis, ns); +#endif + + if(!a.join(d)) + { + exprt e; + e.make_true(); + return e; + } + } + else if(condition.id()==ID_symbol) + { + // TODO: we have to handle symbol expression + } + else + { + d.assume(not_exprt(condition), ns); + if(d.is_bottom()) + { + exprt e; + e.make_true(); + return e; + } + } + + return condition; +} diff --git a/src/analyses/interval_domain.h b/src/analyses/interval_domain.h index f9ffd291b12..572fc6082a0 100644 --- a/src/analyses/interval_domain.h +++ b/src/analyses/interval_domain.h @@ -40,10 +40,15 @@ class interval_domaint:public ai_domain_baset const ai_baset &ai, const namespacet &ns) const override final; + bool join(const interval_domaint &b); + bool merge( const interval_domaint &b, locationt from, - locationt to); + locationt to) + { + return join(b); + } // no states void make_bottom() override final @@ -85,6 +90,11 @@ class interval_domaint:public ai_domain_baset return bottom; } + virtual exprt domain_simplify( + const exprt &condition, + const namespacet &ns, + const bool lhs=false) const; + protected: bool bottom; From 901cc7cc8834a930b8ba33a7c24148500dccab38 Mon Sep 17 00:00:00 2001 From: martin Date: Thu, 15 Dec 2016 20:05:53 +0000 Subject: [PATCH 04/13] Add utility function to tell is a program is threaded or not. --- src/analyses/is_threaded.h | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/src/analyses/is_threaded.h b/src/analyses/is_threaded.h index 931baabb7db..5ed932d1732 100644 --- a/src/analyses/is_threaded.h +++ b/src/analyses/is_threaded.h @@ -29,6 +29,11 @@ class is_threadedt return is_threaded_set.find(t)!=is_threaded_set.end(); } + bool operator()(void) const + { + return !is_threaded_set.empty(); + } + protected: typedef std::set is_threaded_sett; is_threaded_sett is_threaded_set; From 486433dd3e6330411458bbdde5e121eb5fbf28ea Mon Sep 17 00:00:00 2001 From: martin Date: Fri, 16 Dec 2016 16:42:27 +0000 Subject: [PATCH 05/13] Refactor goto-analyzer so that task, analysis, domain and output can be picked independently. --- src/goto-analyzer/Makefile | 1 + .../goto_analyzer_parse_options.cpp | 176 ++++++++++- .../goto_analyzer_parse_options.h | 7 +- src/goto-analyzer/static_analyzer.cpp | 203 ++++++------- src/goto-analyzer/static_analyzer.h | 3 +- src/goto-analyzer/static_show_domain.cpp | 87 ++++++ src/goto-analyzer/static_show_domain.h | 26 ++ src/goto-analyzer/static_simplifier.cpp | 284 ++++++++++++++++++ src/goto-analyzer/static_simplifier.h | 26 ++ 9 files changed, 691 insertions(+), 122 deletions(-) create mode 100644 src/goto-analyzer/static_show_domain.cpp create mode 100644 src/goto-analyzer/static_show_domain.h create mode 100644 src/goto-analyzer/static_simplifier.cpp create mode 100644 src/goto-analyzer/static_simplifier.h diff --git a/src/goto-analyzer/Makefile b/src/goto-analyzer/Makefile index bfeac69abba..b2561494e33 100644 --- a/src/goto-analyzer/Makefile +++ b/src/goto-analyzer/Makefile @@ -1,5 +1,6 @@ SRC = goto_analyzer_main.cpp goto_analyzer_parse_options.cpp \ taint_parser.cpp taint_analysis.cpp static_analyzer.cpp \ + static_show_domain.cpp static_simplifier.cpp \ unreachable_instructions.cpp OBJ += ../ansi-c/ansi-c$(LIBEXT) \ diff --git a/src/goto-analyzer/goto_analyzer_parse_options.cpp b/src/goto-analyzer/goto_analyzer_parse_options.cpp index 4b29d4b8548..ae444610524 100644 --- a/src/goto-analyzer/goto_analyzer_parse_options.cpp +++ b/src/goto-analyzer/goto_analyzer_parse_options.cpp @@ -30,6 +30,8 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include +#include #include #include @@ -46,6 +48,8 @@ Author: Daniel Kroening, kroening@kroening.com #include "taint_analysis.h" #include "unreachable_instructions.h" #include "static_analyzer.h" +#include "static_show_domain.h" +#include "static_simplifier.h" /*******************************************************************\ @@ -169,6 +173,100 @@ void goto_analyzer_parse_optionst::get_command_line_options(optionst &options) if(cmdline.isset("error-label")) options.set_option("error-label", cmdline.get_values("error-label")); #endif + + + // Output format choice + options.set_option("text", false); + options.set_option("json", false); + options.set_option("xml", false); + options.set_option("outfile", "-"); + + if(cmdline.isset("text")) + { + options.set_option("text", true); + options.set_option("outfile", cmdline.get_value("text")); + } + else if(cmdline.isset("json")) + { + options.set_option("json", true); + options.set_option("outfile", cmdline.get_value("json")); + } + else if(cmdline.isset("xml")) + { + options.set_option("xml", true); + options.set_option("outfile", cmdline.get_value("xml")); + } + else + { + options.set_option("text", true); + } + + + // Task options + options.set_option( "show", false); + options.set_option( "verify", false); + options.set_option("simplify", false); + + if(cmdline.isset("show") || + cmdline.isset("show-intervals") || + cmdline.isset("show-non-null")) + options.set_option("show", true); + else if(cmdline.isset("verify")) + options.set_option("verify", true); + else if(cmdline.isset("simplify")) + { + options.set_option("simplify", true); + options.set_option("outfile", cmdline.get_value("simplify")); + } + + if(!(options.get_bool_option("show") || + options.get_bool_option("verify") || + options.get_bool_option("simplify"))) + { + status() << "Task defaults to --show" << eom; + options.set_option("show", true); + } + + + // Abstract interpreter choice + options.set_option("flow-sensitive", false); + options.set_option("concurrent", false); + + if(cmdline.isset("flow-sensitive")) + options.set_option("flow-sensitive", true); + else if(cmdline.isset("concurrent")) + options.set_option("concurrent", true); + else + { + is_threadedt is_threaded(goto_model.goto_functions); + bool contains_concurrent_code=is_threaded(); + + options.set_option("flow-sensitive", !contains_concurrent_code); + options.set_option("concurrent", contains_concurrent_code); + } + + + // Domain choice + options.set_option("constants", false); + options.set_option("intervals", false); + options.set_option("non-null", false); + + if(cmdline.isset("intervals") || + cmdline.isset("show-intervals")) + options.set_option("intervals", true); + else if(cmdline.isset("non-null") || + cmdline.isset("show-non-null")) + options.set_option("non-null", true); + else if(cmdline.isset("constants")) + options.set_option("constants", true); + + if(!(options.get_bool_option("constants") || + options.get_bool_option("intervals") || + options.get_bool_option("non-null"))) + { + status() << "Domain defaults to --constants" << eom; + options.set_option("constants", true); + } } /*******************************************************************\ @@ -229,8 +327,12 @@ int goto_analyzer_parse_optionst::doit() else { std::string json_file=cmdline.get_value("json"); - bool result= - taint_analysis(goto_model, taint_file, get_message_handler(), false, json_file); + bool result=taint_analysis( + goto_model, + taint_file, + get_message_handler(), + false, + json_file); return result?10:0; } } @@ -293,17 +395,47 @@ int goto_analyzer_parse_optionst::doit() return 0; } - if(cmdline.isset("non-null") || - cmdline.isset("intervals")) + + // Output file factory + std::ostream *out; + const std::string outfile=options.get_option("outfile"); + if(outfile=="-") + out=&std::cout; + else { - optionst options; - options.set_option("json", cmdline.get_value("json")); - options.set_option("xml", cmdline.get_value("xml")); - bool result= - static_analyzer(goto_model, options, get_message_handler()); - return result?10:0; + out=new std::ofstream(outfile); + if(!*out) + { + error() << "Failed to open output file `" + << outfile << "'" << eom; + return 6; + } } + + // Run the analysis + bool result=true; + if(options.get_bool_option("show")) + result=static_show_domain(goto_model, options, get_message_handler(), *out); + + else if(options.get_bool_option("verify")) + result= static_analyzer(goto_model, options, get_message_handler(), *out); + + else if(options.get_bool_option("simplify")) + result= static_simplifier(goto_model, options, get_message_handler(), *out); + else + { + error() << "No task given" << eom; + return 6; + } + + if(out!=&std::cout) + delete out; + + return result?10:0; + + + // Final defensive error case error() << "no analysis option given -- consider reading --help" << eom; return 6; @@ -477,17 +609,29 @@ void goto_analyzer_parse_optionst::help() " goto-analyzer [-h] [--help] show help\n" " goto-analyzer file.c ... source file names\n" "\n" - "Analyses:\n" + "Task options:\n" + " --show display the abstract domains\n" + " --verify use the abstract domains to check assertions\n" + " --simplify file_name use the abstract domains to simplify the program\n" "\n" - " --taint file_name perform taint analysis using rules in given file\n" - " --unreachable-instructions list dead code\n" - " --intervals interval analysis\n" - " --non-null non-null analysis\n" + "Abstract interpreter options:\n" + " --flow-sensitive use flow-sensitive abstract interpreter\n" + " --concurrent use concurrent abstract interpreter\n" + "\n" + "Domain options:\n" + " --constants constant abstraction\n" + " --intervals interval abstraction\n" + " --non-null non-null abstraction\n" "\n" - "Analysis options:\n" + "Output options:\n" + " --text file_name output results in plain text to given file\n" " --json file_name output results in JSON format to given file\n" " --xml file_name output results in XML format to given file\n" "\n" + "Other analyses:\n" + " --taint file_name perform taint analysis using rules in given file\n" + " --unreachable-instructions list dead code\n" + "\n" "C/C++ frontend options:\n" " -I path set include path (C/C++)\n" " -D macro define preprocessor macro (C/C++)\n" diff --git a/src/goto-analyzer/goto_analyzer_parse_options.h b/src/goto-analyzer/goto_analyzer_parse_options.h index 19b44c21910..368af800c13 100644 --- a/src/goto-analyzer/goto_analyzer_parse_options.h +++ b/src/goto-analyzer/goto_analyzer_parse_options.h @@ -33,10 +33,13 @@ class optionst; "(gcc)(arch):" \ "(taint):(show-taint)" \ "(show-local-may-alias)" \ - "(json):(xml):" \ + "(json):(xml):(text):" \ "(unreachable-instructions)" \ "(intervals)(show-intervals)" \ - "(non-null)(show-non-null)" + "(non-null)(show-non-null)" \ + "(constants)" \ + "(show)(verify)(simplify):" \ + "(flow-sensitive)(concurrent)" class goto_analyzer_parse_optionst: public parse_options_baset, diff --git a/src/goto-analyzer/static_analyzer.cpp b/src/goto-analyzer/static_analyzer.cpp index f4f6c5cff33..65eb3bf8d20 100644 --- a/src/goto-analyzer/static_analyzer.cpp +++ b/src/goto-analyzer/static_analyzer.cpp @@ -8,25 +8,28 @@ Author: Daniel Kroening, kroening@kroening.com #include -#include #include #include #include +#include #include "static_analyzer.h" +template class static_analyzert:public messaget { public: static_analyzert( const goto_modelt &_goto_model, const optionst &_options, - message_handlert &_message_handler): + message_handlert &_message_handler, + std::ostream &_out): messaget(_message_handler), goto_functions(_goto_model.goto_functions), ns(_goto_model.symbol_table), - options(_options) + options(_options), + out(_out) { } @@ -36,38 +39,38 @@ class static_analyzert:public messaget const goto_functionst &goto_functions; const namespacet ns; const optionst &options; + std::ostream &out; // analyses - ait interval_analysis; + analyzerT domain; void plain_text_report(); - void json_report(const std::string &); - void xml_report(const std::string &); - - tvt eval(goto_programt::const_targett); + void json_report(); + void xml_report(); }; /*******************************************************************\ -Function: static_analyzert::operator() +Function: static_analyzert::operator() - Inputs: + Inputs: None. - Outputs: + Outputs: false on success, true on failure. - Purpose: + Purpose: Run the analysis, check the assertions and report in the correct format. \*******************************************************************/ -bool static_analyzert::operator()() +template +bool static_analyzert::operator()() { - status() << "performing interval analysis" << eom; - interval_analysis(goto_functions, ns); + status() << "Performing analysis" << eom; + domain(goto_functions, ns); - if(!options.get_option("json").empty()) - json_report(options.get_option("json")); - else if(!options.get_option("xml").empty()) - xml_report(options.get_option("xml")); + if(options.get_bool_option("json")) + json_report(); + else if(options.get_bool_option("xml")) + xml_report(); else plain_text_report(); @@ -76,38 +79,18 @@ bool static_analyzert::operator()() /*******************************************************************\ -Function: static_analyzert::eval +Function: static_analyzert::plain_text_report - Inputs: + Inputs: None. - Outputs: + Outputs: Text report via out. - Purpose: + Purpose: Check the assertions and give results as text. \*******************************************************************/ -tvt static_analyzert::eval(goto_programt::const_targett t) -{ - exprt guard=t->guard; - interval_domaint d=interval_analysis[t]; - d.assume(not_exprt(guard), ns); - if(d.is_bottom()) return tvt(true); - return tvt::unknown(); -} - -/*******************************************************************\ - -Function: static_analyzert::plain_text_report - - Inputs: - - Outputs: - - Purpose: - -\*******************************************************************/ - -void static_analyzert::plain_text_report() +template +void static_analyzert::plain_text_report() { unsigned pass=0, fail=0, unknown=0; @@ -124,7 +107,7 @@ void static_analyzert::plain_text_report() { if(!i_it->is_assert()) continue; - tvt r=eval(i_it); + exprt simplified=domain[i_it].domain_simplify(i_it->guard, ns); result() << '[' << i_it->source_location.get_property_id() << ']' << ' '; @@ -133,48 +116,43 @@ void static_analyzert::plain_text_report() if(!i_it->source_location.get_comment().empty()) result() << ", " << i_it->source_location.get_comment(); result() << ": "; - if(r.is_true()) - result() << "SUCCESS"; - else if(r.is_false()) - result() << "FAILURE"; + if(simplified.is_true()) + { result() << "SUCCESS"; pass++; } + else if(simplified.is_false()) + { result() << "FAILURE (if reachable)"; fail++; } else - result() << "UNKNOWN"; + { result() << "UNKNOWN"; unknown++; } result() << eom; - if(r.is_true()) - pass++; - else if(r.is_false()) - fail++; - else - unknown++; } status() << '\n'; } - - status() << "SUMMARY: " << pass << " pass, " << fail << " fail, " + status() << "SUMMARY: " << pass << " pass, " << fail << " fail if reachable, " << unknown << " unknown\n"; } /*******************************************************************\ -Function: static_analyzert::json_report +Function: static_analyzert::json_report - Inputs: + Inputs: None. - Outputs: + Outputs: JSON report via out. - Purpose: + Purpose: Check the assertions and give results as JSON. \*******************************************************************/ -void static_analyzert::json_report(const std::string &file_name) +template +void static_analyzert::json_report() { json_arrayt json_result; forall_goto_functions(f_it, goto_functions) { - if(!f_it->second.body.has_assertion()) continue; + if(!f_it->second.body.has_assertion()) + continue; if(f_it->first=="__actual_thread_spawn") continue; @@ -183,14 +161,14 @@ void static_analyzert::json_report(const std::string &file_name) { if(!i_it->is_assert()) continue; - tvt r=eval(i_it); + exprt simplified=domain[i_it].domain_simplify(i_it->guard, ns); json_objectt &j=json_result.push_back().make_object(); - if(r.is_true()) + if(simplified.is_true()) j["status"]=json_stringt("SUCCESS"); - else if(r.is_false()) - j["status"]=json_stringt("FAILURE"); + else if(simplified.is_false()) + j["status"]=json_stringt("FAILURE (if reachable)"); else j["status"]=json_stringt("UNKNOWN"); @@ -200,32 +178,24 @@ void static_analyzert::json_report(const std::string &file_name) i_it->source_location.get_comment())); } } - - std::ofstream out(file_name); - if(!out) - { - error() << "failed to open JSON output file `" - << file_name << "'" << eom; - return; - } - - status() << "Writing report to `" << file_name << "'" << eom; + status() << "Writing JSON report" << eom; out << json_result; } /*******************************************************************\ -Function: static_analyzert::xml_report +Function: static_analyzert::xml_report - Inputs: + Inputs: None. - Outputs: + Outputs: XML report via out. - Purpose: + Purpose: Check the assertions and give results as XML. \*******************************************************************/ -void static_analyzert::xml_report(const std::string &file_name) +template +void static_analyzert::xml_report() { xmlt xml_result; @@ -240,14 +210,14 @@ void static_analyzert::xml_report(const std::string &file_name) { if(!i_it->is_assert()) continue; - tvt r=eval(i_it); + exprt simplified=domain[i_it].domain_simplify(i_it->guard, ns); xmlt &x=xml_result.new_element("result"); - if(r.is_true()) + if(simplified.is_true()) x.set_attribute("status", "SUCCESS"); - else if(r.is_false()) - x.set_attribute("status", "FAILURE"); + else if(simplified.is_false()) + x.set_attribute("status", "FAILURE (if reachable)"); else x.set_attribute("status", "UNKNOWN"); @@ -257,15 +227,7 @@ void static_analyzert::xml_report(const std::string &file_name) } } - std::ofstream out(file_name); - if(!out) - { - error() << "failed to open XML output file `" - << file_name << "'" << eom; - return; - } - - status() << "Writing report to `" << file_name << "'" << eom; + status() << "Writing XML report" << eom; out << xml_result; } @@ -273,21 +235,56 @@ void static_analyzert::xml_report(const std::string &file_name) Function: static_analyzer - Inputs: + Inputs: The goto_model to check, options giving the domain and output, + the message handler and output stream. - Outputs: + Outputs: Report via out. - Purpose: + Purpose: Runs the analyzer, check assertions and generate a report. \*******************************************************************/ bool static_analyzer( const goto_modelt &goto_model, const optionst &options, - message_handlert &message_handler) + message_handlert &message_handler, + std::ostream &out) { - return static_analyzert( - goto_model, options, message_handler)(); + if(options.get_bool_option("flow-sensitive")) + { + if(options.get_bool_option("constants")) + return static_analyzert > + (goto_model, options, message_handler, out)(); + + else if(options.get_bool_option("intervals")) + return static_analyzert > + (goto_model, options, message_handler, out)(); + + // else if(options.get_bool_option("non-null")) + // return static_analyzert > + // (goto_model, options, message_handler, out)(); + } + else if(options.get_bool_option("concurrent")) + { + // Constant and interval don't have merge_shared yet +#if 0 + if(options.get_bool_option("constants")) + return static_analyzert > + (goto_model, options, message_handler, out)(); + + else if(options.get_bool_option("intervals")) + return static_analyzert > + (goto_model, options, message_handler, out)(); + + // else if(options.get_bool_option("non-null")) + // return static_analyzert > + // (goto_model, options, message_handler, out)(); +#endif + } + + messaget m(message_handler); + m.status() << "Task / Interpreter / Domain combination not supported" << messaget::eom; + return true; } /*******************************************************************\ diff --git a/src/goto-analyzer/static_analyzer.h b/src/goto-analyzer/static_analyzer.h index 3d964a2964a..0b158624e72 100644 --- a/src/goto-analyzer/static_analyzer.h +++ b/src/goto-analyzer/static_analyzer.h @@ -20,7 +20,8 @@ Author: Daniel Kroening, kroening@kroening.com bool static_analyzer( const goto_modelt &, const optionst &, - message_handlert &); + message_handlert &, + std::ostream &); void show_intervals( const goto_modelt &, diff --git a/src/goto-analyzer/static_show_domain.cpp b/src/goto-analyzer/static_show_domain.cpp new file mode 100644 index 00000000000..a3a2616c152 --- /dev/null +++ b/src/goto-analyzer/static_show_domain.cpp @@ -0,0 +1,87 @@ +/*******************************************************************\ + +Module: + +Author: Martin Brain, martin.brain@cs.ox.ac.uk + +\*******************************************************************/ + +#include + +#include +#include +#include + +#include +#include + +#include "static_show_domain.h" + +/*******************************************************************\ + +Function: static_show_domain + + Inputs: The goto_model to analyze, options giving the domain and output, + the message handler and output stream. + + Outputs: The abstract domain via out. + + Purpose: Runs the analyzer and then prints out the domain. + +\*******************************************************************/ + +bool static_show_domain( + const goto_modelt &goto_model, + const optionst &options, + message_handlert &message_handler, + std::ostream &out) +{ + ai_baset *domain=NULL; + + if(options.get_bool_option("flow-sensitive")) + { + if(options.get_bool_option("constants")) + domain=new ait(); + + else if(options.get_bool_option("intervals")) + domain=new ait(); + + // else if(options.get_bool_option("non-null")) + // domain=new ait(); + } + else if(options.get_bool_option("concurrent")) + { + // Constant and interval don't have merge_shared yet +#if 0 + if(options.get_bool_option("constants")) + domain=new concurrency_aware_ait(); + + else if(options.get_bool_option("intervals")) + domain=new concurrency_aware_ait(); + + // else if(options.get_bool_option("non-null")) + // domain=new concurrency_aware_ait(); +#endif + } + + if(domain==NULL) + { + messaget m(message_handler); + m.status() << "Task / Interpreter / Domain combination not supported" + << messaget::eom; + return true; + } + + // status() << "Performing analysis" << eom; + (*domain)(goto_model); + + if(options.get_bool_option("json")) + out << domain->output_json(goto_model); + else if(options.get_bool_option("xml")) + out << domain->output_xml(goto_model); + else + domain->output(goto_model, out); + + delete domain; + return false; +} diff --git a/src/goto-analyzer/static_show_domain.h b/src/goto-analyzer/static_show_domain.h new file mode 100644 index 00000000000..3f0e7da3680 --- /dev/null +++ b/src/goto-analyzer/static_show_domain.h @@ -0,0 +1,26 @@ +/*******************************************************************\ + +Module: + +Author: Martin Brain, martin.brain@cs.ox.ac.uk + +\*******************************************************************/ + +#ifndef CPROVER_GOTO_ANALYZER_STATIC_SHOW_DOMAIN_H +#define CPROVER_GOTO_ANALYZER_STATIC_SHOW_DOMAIN_H + +#include + +#include +#include +#include + +#include + +bool static_show_domain( + const goto_modelt &, + const optionst &, + message_handlert &, + std::ostream &); + +#endif diff --git a/src/goto-analyzer/static_simplifier.cpp b/src/goto-analyzer/static_simplifier.cpp new file mode 100644 index 00000000000..fe7118563e3 --- /dev/null +++ b/src/goto-analyzer/static_simplifier.cpp @@ -0,0 +1,284 @@ +/*******************************************************************\ + +Module: + +Author: Lucas Cordeiro, lucas.cordeiro@cs.ox.ac.uk + +\*******************************************************************/ + +// #define DEBUG + +#ifdef DEBUG +#include +#endif + +#include + +#include + +#include +#include + +#include "static_simplifier.h" + +template +class static_simplifiert:public messaget +{ +public: + static_simplifiert( + goto_modelt &_goto_model, + const optionst &_options, + message_handlert &_message_handler, + std::ostream &_out): + messaget(_message_handler), + goto_functions(_goto_model.goto_functions), + ns(_goto_model.symbol_table), + options(_options), + out(_out) + { + } + + bool operator()(void); + +protected: + goto_functionst &goto_functions; + const namespacet ns; + const optionst &options; + std::ostream &out; + + // analyses + analyzerT domain; + + void simplify_program(void); + unsigned simplify_guard(goto_programt::instructionst::iterator &i_it); +}; + +/*******************************************************************\ + +Function: static_simplifiert::operator() + + Inputs: None. + + Outputs: false on success, true on failure. + + Purpose: Run the analysis, check the assertions and report in the correct format. + +\*******************************************************************/ + +template +bool static_simplifiert::operator()(void) +{ + status() << "Performing analysis" << eom; + domain(goto_functions, ns); + + status() << "Simplifying program" << eom; + simplify_program(); + + status() << "Writing goto binary" << eom; + return write_goto_binary(out, ns.get_symbol_table(), goto_functions); +} + + +/*******************************************************************\ + +Function: static_simplifiert::simplify_guard + + Inputs: An iterator pointing to an instruction. + + Outputs: 1 if simplified, 0 if not. + + Purpose: Simplifies the instruction's guard using the information in the abstract domain. + +\*******************************************************************/ + +template +unsigned static_simplifiert::simplify_guard( + goto_programt::instructionst::iterator &i_it) +{ + exprt simplified=domain[i_it].domain_simplify(i_it->guard, ns); + unsigned return_value=(simplified==i_it->guard) ? 0 : 1; + i_it->guard=simplified; + return return_value; +} + +/*******************************************************************\ + +Function: static_simplifiert::simplify_program + + Inputs: None. + + Outputs: None. + + Purpose: Simplifies the program using the information in the abstract domain. + +\*******************************************************************/ + +template +void static_simplifiert::simplify_program() +{ + struct counterst + { + unsigned asserts; + unsigned assumes; + unsigned gotos; + unsigned assigns; + unsigned function_calls; + }; + + counterst simplified={0, 0, 0, 0, 0}; + counterst unmodified={0, 0, 0, 0, 0}; + + Forall_goto_functions(f_it, goto_functions) + { + Forall_goto_program_instructions(i_it, f_it->second.body) + { + if(i_it->is_assert()) + { + unsigned result=simplify_guard(i_it); + simplified.asserts+=result; + unmodified.asserts+=(1-result); + } + else if(i_it->is_assume()) + { + unsigned result=simplify_guard(i_it); + simplified.assumes+=result; + unmodified.assumes+=(1-result); + } + else if(i_it->is_goto()) + { + unsigned result=simplify_guard(i_it); + simplified.gotos+=result; + unmodified.gotos+=(1-result); + } + else if(i_it->is_assign()) + { + code_assignt assign(to_code_assign(i_it->code)); + + /* + ** Simplification needs to be aware of which side of the + ** expression it is handling as: + ** i=j + ** should simplify to i=1, not to 0=1. + */ + + exprt simp_lhs=domain[i_it].domain_simplify(assign.lhs(), ns, true); + exprt simp_rhs=domain[i_it].domain_simplify(assign.rhs(), ns, false); + + unsigned result=(simp_lhs==assign.lhs() && + simp_rhs==assign.rhs()) ? 0 : 1; + simplified.assigns+=result; + unmodified.assigns+=(1-result); + + assign.lhs()=simp_lhs; + assign.rhs()=simp_rhs; + i_it->code=assign; + } + else if(i_it->is_function_call()) + { + unsigned result=0; + code_function_callt fcall(to_code_function_call(i_it->code)); + + exprt new_function=domain[i_it].domain_simplify(fcall.function(), ns); + result|=(new_function==fcall.function()) ? 0 : 1; + fcall.function()=new_function; + + exprt::operandst &args=fcall.arguments(); + + for(exprt::operandst::iterator o_it=args.begin(); + o_it!=args.end(); + ++o_it) + { + exprt new_arg=domain[i_it].domain_simplify(*o_it, ns); + result|=(new_arg==*o_it) ? 0 : 1; + *o_it=new_arg; + } + + i_it->code=fcall; + + simplified.function_calls+=result; + unmodified.function_calls+=(1-result); + } + } + } + + // Make sure the references are correct. + goto_functions.update(); + + + status() << "SIMPLIFIED: " + << " assert: " << simplified.asserts + << ", assume: " << simplified.assumes + << ", goto: " << simplified.gotos + << ", assigns: " << simplified.assigns + << ", function calls: " << simplified.function_calls + << "\n" + << "UNMODIFIED: " + << " assert: " << unmodified.asserts + << ", assume: " << unmodified.assumes + << ", goto: " << unmodified.gotos + << ", assigns: " << unmodified.assigns + << ", function calls: " << unmodified.function_calls + << eom; + + return; +} + + + + +/*******************************************************************\ + +Function: static_simplifier + + Inputs: The goto_model to analyze and simplify, options giving the domain, + the message handler and output stream. + + Outputs: The simplified goto binary via out. + + Purpose: Runs the analyzer, simplifies and then outputs. + +\*******************************************************************/ + +bool static_simplifier( + goto_modelt &goto_model, + const optionst &options, + message_handlert &message_handler, + std::ostream &out) +{ + if(options.get_bool_option("flow-sensitive")) + { + if(options.get_bool_option("constants")) + return static_simplifiert > + (goto_model, options, message_handler, out)(); + + else if(options.get_bool_option("intervals")) + return static_simplifiert > + (goto_model, options, message_handler, out)(); + + // else if(options.get_bool_option("non-null")) + // return static_simplifiert > + // (goto_model, options, message_handler, out)(); + } + else if(options.get_bool_option("concurrent")) + { + // Constant and interval don't have merge_shared yet +#if 0 + if(options.get_bool_option("constants")) + return static_simplifiert > + (goto_model, options, message_handler, out)(); + + else if(options.get_bool_option("intervals")) + return static_simplifiert > + (goto_model, options, message_handler, out)(); + + // else if(options.get_bool_option("non-null")) + // return static_simplifiert > + // (goto_model, options, message_handler, out)(); +#endif + } + + messaget m(message_handler); + m.status() << "Task / Interpreter / Domain combination not supported" + << messaget::eom; + return true; +} diff --git a/src/goto-analyzer/static_simplifier.h b/src/goto-analyzer/static_simplifier.h new file mode 100644 index 00000000000..c9d4e156b7a --- /dev/null +++ b/src/goto-analyzer/static_simplifier.h @@ -0,0 +1,26 @@ +/*******************************************************************\ + +Module: + +Author: Lucas Cordeiro, lucas.cordeiro@cs.ox.ac.uk + +\*******************************************************************/ + +#ifndef CPROVER_GOTO_ANALYZER_STATIC_SIMPLIFIER_H +#define CPROVER_GOTO_ANALYZER_STATIC_SIMPLIFIER_H + +#include + +#include +#include +#include + +#include + +bool static_simplifier( + goto_modelt &, + const optionst &, + message_handlert &, + std::ostream &); + +#endif From 3945129c9213930d4e87a992484d08337bfedaa4 Mon Sep 17 00:00:00 2001 From: Martin Brain Date: Fri, 9 Sep 2016 08:07:36 +0100 Subject: [PATCH 06/13] Remove the special case handling of --show-intervals. The option string --show --intervals is more flexible, --show-intervals is now an alias. --- .../goto_analyzer_parse_options.cpp | 6 ------ src/goto-analyzer/static_analyzer.cpp | 21 ------------------- src/goto-analyzer/static_analyzer.h | 4 ---- 3 files changed, 31 deletions(-) diff --git a/src/goto-analyzer/goto_analyzer_parse_options.cpp b/src/goto-analyzer/goto_analyzer_parse_options.cpp index ae444610524..9ead2c6ff2d 100644 --- a/src/goto-analyzer/goto_analyzer_parse_options.cpp +++ b/src/goto-analyzer/goto_analyzer_parse_options.cpp @@ -389,12 +389,6 @@ int goto_analyzer_parse_optionst::doit() if(set_properties()) return 7; - if(cmdline.isset("show-intervals")) - { - show_intervals(goto_model, std::cout); - return 0; - } - // Output file factory std::ostream *out; diff --git a/src/goto-analyzer/static_analyzer.cpp b/src/goto-analyzer/static_analyzer.cpp index 65eb3bf8d20..f3a12ae604b 100644 --- a/src/goto-analyzer/static_analyzer.cpp +++ b/src/goto-analyzer/static_analyzer.cpp @@ -286,24 +286,3 @@ bool static_analyzer( m.status() << "Task / Interpreter / Domain combination not supported" << messaget::eom; return true; } - -/*******************************************************************\ - -Function: show_intervals - - Inputs: - - Outputs: - - Purpose: - -\*******************************************************************/ - -void show_intervals( - const goto_modelt &goto_model, - std::ostream &out) -{ - ait interval_analysis; - interval_analysis(goto_model); - interval_analysis.output(goto_model, out); -} diff --git a/src/goto-analyzer/static_analyzer.h b/src/goto-analyzer/static_analyzer.h index 0b158624e72..fc320ad734b 100644 --- a/src/goto-analyzer/static_analyzer.h +++ b/src/goto-analyzer/static_analyzer.h @@ -23,8 +23,4 @@ bool static_analyzer( message_handlert &, std::ostream &); -void show_intervals( - const goto_modelt &, - std::ostream &); - #endif // CPROVER_GOTO_ANALYZER_STATIC_ANALYZER_H From d09a25d41f8b5003b8988d238d32c255007ba6ab Mon Sep 17 00:00:00 2001 From: martin Date: Mon, 19 Dec 2016 20:07:52 +0000 Subject: [PATCH 07/13] Lucas' fixes and improvements to the interval domain. --- src/analyses/interval_domain.cpp | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/analyses/interval_domain.cpp b/src/analyses/interval_domain.cpp index a75f1bf4964..39bc3274a91 100644 --- a/src/analyses/interval_domain.cpp +++ b/src/analyses/interval_domain.cpp @@ -148,7 +148,9 @@ bool interval_domaint::join( for(int_mapt::iterator it=int_map.begin(); it!=int_map.end(); ) // no it++ { - const int_mapt::const_iterator b_it=b.int_map.begin(); + //search for the variable that needs to be merged + //containers have different size and variable order + const int_mapt::const_iterator b_it=b.int_map.find(it->first); if(b_it==b.int_map.end()) { it=int_map.erase(it); From 311f442d4ff0e04f0f4e08d5270a84628c7fbd2a Mon Sep 17 00:00:00 2001 From: martin Date: Mon, 19 Dec 2016 20:08:15 +0000 Subject: [PATCH 08/13] Lucas' fixes and improvements to the constant domain. --- src/analyses/constant_propagator.cpp | 208 +++++++++++++++++++++++---- src/analyses/constant_propagator.h | 6 + 2 files changed, 187 insertions(+), 27 deletions(-) diff --git a/src/analyses/constant_propagator.cpp b/src/analyses/constant_propagator.cpp index c7d5879d858..41819730640 100644 --- a/src/analyses/constant_propagator.cpp +++ b/src/analyses/constant_propagator.cpp @@ -20,6 +20,61 @@ Author: Peter Schrammel /*******************************************************************\ +Function: concatenate_array_id + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +exprt concatenate_array_id( + const exprt &array, const exprt &index, + const typet &type) +{ + std::string a, idx, identifier; + a = array.get_string(ID_identifier); + + if (index.id()==ID_typecast) + idx = index.op0().get_string(ID_value); + else + idx = index.get_string(ID_value); + + mp_integer i=string2integer(idx); + identifier=a+"["+integer2string(i)+"]"; + symbol_exprt new_expr(identifier, type); + + return new_expr; +} + +/*******************************************************************\ + +Function: concatenate_array_id + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +exprt concatenate_array_id( + const exprt &array, const mp_integer &index, + const typet &type) +{ + std::string a, identifier; + a = array.get_string(ID_identifier); + identifier=a+"["+integer2string(index)+"]"; + symbol_exprt new_expr(identifier, type); + + return new_expr; +} + +/*******************************************************************\ + Function: constant_propagator_domaint::assign_rec Inputs: @@ -35,6 +90,7 @@ void constant_propagator_domaint::assign_rec( const exprt &lhs, const exprt &rhs, const namespacet &ns) { + const typet & lhs_type = ns.follow(lhs.type()); const typet & rhs_type = ns.follow(rhs.type()); #ifdef DEBUG @@ -42,7 +98,28 @@ void constant_propagator_domaint::assign_rec( << " := " << from_type(ns, "", rhs_type) << std::endl; #endif - if(lhs.id()==ID_symbol && rhs_type.id()!=ID_array + if(lhs.id()==ID_symbol && rhs.id()==ID_if) + { + exprt cond=rhs.op0(); + assert(cond.operands().size()==2); + if(values.is_constant(cond.op0()) + && values.is_constant(cond.op1())) + { + if(cond.op0().id()==ID_index) + { + exprt index=cond.op0(); + exprt new_expr=concatenate_array_id(index.op0(), index.op1(), index.type()); + values.replace_const(new_expr); + cond.op0()=new_expr; + cond = simplify_expr(cond,ns); + } + else + assert(0); + + assign(values, to_symbol_expr(lhs), cond, ns); + } + } + else if(lhs.id()==ID_symbol && rhs_type.id()!=ID_array && rhs_type.id()!=ID_struct && rhs_type.id()!=ID_union) { @@ -51,6 +128,27 @@ void constant_propagator_domaint::assign_rec( else values.set_to_top(to_symbol_expr(lhs)); } + else if(lhs.id()==ID_symbol && lhs_type.id()==ID_array + && rhs_type.id()==ID_array) + { + exprt new_expr; + mp_integer idx=0; + forall_operands(it, rhs) + { + new_expr=concatenate_array_id(lhs, idx, it->type()); + assign(values, to_symbol_expr(new_expr), *it, ns); + idx = idx +1; + } + } + else if (lhs.id()==ID_index) + { + if (values.is_constant(lhs.op1()) + && values.is_constant(rhs)) + { + exprt new_expr=concatenate_array_id(lhs.op0(), lhs.op1(), rhs.type()); + assign(values, to_symbol_expr(new_expr), rhs, ns); + } + } #if 0 else //TODO: could make field or array element-sensitive { @@ -106,12 +204,22 @@ void constant_propagator_domaint::transform( else if(from->is_goto()) { exprt g; + if(from->get_target()==to) g = simplify_expr(from->guard, ns); else g = simplify_expr(not_exprt(from->guard), ns); - two_way_propagate_rec(g, ns); + if (g.is_false()) + values.set_to_bottom(); + else + { + //TODO: we need to support widening! + if (g.is_constant()) + values.set_to_top(); + else + two_way_propagate_rec(g, ns); + } } else if(from->is_dead()) { @@ -141,6 +249,7 @@ void constant_propagator_domaint::transform( else values.set_to_top(); } + #ifdef DEBUG std::cout << "after:\n"; output(std::cout,ai,ns); @@ -226,6 +335,30 @@ void constant_propagator_domaint::assign( /*******************************************************************\ +Function: constant_propagator_domaint::is_array_constant + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +bool constant_propagator_domaint::valuest::is_array_constant(const exprt &expr) const +{ + exprt new_expr = concatenate_array_id(expr.op0(), + expr.op1(), expr.type()); + + if (replace_const.expr_map.find(to_symbol_expr(new_expr).get_identifier()) == + replace_const.expr_map.end()) + return false; + + return true; +} + +/*******************************************************************\ + Function: constant_propagator_domaint::valuest::is_constant Inputs: @@ -251,6 +384,9 @@ bool constant_propagator_domaint::valuest::is_constant(const exprt &expr) const replace_const.expr_map.end()) return false; + if (expr.id()==ID_index) + return is_array_constant(expr); + if(expr.id()==ID_address_of) return is_constant_address_of(to_address_of_expr(expr).object()); @@ -400,38 +536,25 @@ bool constant_propagator_domaint::valuest::merge(const valuest &src) it!=replace_const.expr_map.end(); ) // no it++ { - if(src.replace_const.expr_map.find(it->first) == - src.replace_const.expr_map.end()) + const replace_symbolt::expr_mapt::const_iterator + b_it=src.replace_const.expr_map.find(it->first); + + if(b_it==src.replace_const.expr_map.end()) { //cannot use set_to_top here - replace_const.expr_map.erase(it++); + replace_const.expr_map.erase(it); changed = true; + break; } - else ++it; - } - - for(const auto &src_replace_pair : src.replace_const.expr_map) - { - replace_symbolt::expr_mapt::iterator c_it= - replace_const.expr_map.find(src_replace_pair.first); - - if(c_it!=replace_const.expr_map.end()) + else { - // values are different, set to top - if(c_it->second!=src_replace_pair.second) - { - changed=set_to_top(src_replace_pair.first); - assert(changed); - } + const exprt previous=it->second; + replace_const.expr_map[b_it->first]=b_it->second; + if (it->second != previous) changed = true; + + it++; } - // is not in "this", ignore - else { } } - -#ifdef DEBUG - std::cout << "merged: " << changed << '\n'; -#endif - return changed; } @@ -520,6 +643,34 @@ void constant_propagator_ait::replace( /*******************************************************************\ +Function: constant_propagator_ait::replace_array_symbol + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +void constant_propagator_ait::replace_array_symbol(exprt &expr) +{ + if (expr.id()==ID_index) + expr = concatenate_array_id(expr.op0(), + expr.op1(), expr.type()); + + Forall_operands(it, expr) + { + if (it->id()==ID_equal) + replace_array_symbol(it->op0()); + else if (it->id()==ID_index) + replace_array_symbol(expr.op0()); + } + +} + +/*******************************************************************\ + Function: constant_propagator_ait::replace Inputs: @@ -546,6 +697,7 @@ void constant_propagator_ait::replace( if(it->is_goto() || it->is_assume() || it->is_assert()) { + replace_array_symbol(it->guard); s_it->second.values.replace_const(it->guard); it->guard = simplify_expr(it->guard, ns); } @@ -554,6 +706,8 @@ void constant_propagator_ait::replace( exprt &rhs = to_code_assign(it->code).rhs(); s_it->second.values.replace_const(rhs); rhs = simplify_expr(rhs, ns); + if (rhs.id()==ID_constant) + rhs.add_source_location()=it->code.op0().source_location(); } else if(it->is_function_call()) { diff --git a/src/analyses/constant_propagator.h b/src/analyses/constant_propagator.h index 026bc96f970..d98e9cf744e 100644 --- a/src/analyses/constant_propagator.h +++ b/src/analyses/constant_propagator.h @@ -55,6 +55,7 @@ class constant_propagator_domaint:public ai_domain_baset } bool is_constant(const exprt &expr) const; + bool is_array_constant(const exprt &expr) const; bool is_constant_address_of(const exprt &expr) const; bool set_to_top(const irep_idt &id); @@ -68,6 +69,7 @@ class constant_propagator_domaint:public ai_domain_baset replace_const.clear(); is_bottom = false; } + }; valuest values; @@ -109,6 +111,9 @@ class constant_propagator_ait:public ait protected: friend class constant_propagator_domaint; + void replace_array_symbol( + exprt &expr); + void replace( goto_functionst::goto_functiont &, const namespacet &); @@ -120,6 +125,7 @@ class constant_propagator_ait:public ait void replace_types_rec( const replace_symbolt &replace_const, exprt &expr); + }; #endif // CPROVER_ANALYSES_CONSTANT_PROPAGATOR_H From a8b5fc53e1980342138360a44aab05abe619b6e0 Mon Sep 17 00:00:00 2001 From: Martin Brain Date: Fri, 9 Sep 2016 09:02:20 +0100 Subject: [PATCH 09/13] Implement domain_simplify for the constant domain. --- src/analyses/constant_propagator.cpp | 26 ++++++++++++++++++++++++++ src/analyses/constant_propagator.h | 1 + 2 files changed, 27 insertions(+) diff --git a/src/analyses/constant_propagator.cpp b/src/analyses/constant_propagator.cpp index 41819730640..fb23adbccea 100644 --- a/src/analyses/constant_propagator.cpp +++ b/src/analyses/constant_propagator.cpp @@ -335,6 +335,32 @@ void constant_propagator_domaint::assign( /*******************************************************************\ +Function: constant_propagator_domaint::domain_simplify + + Inputs: The condition to simplify and its namespace. + + Outputs: The simplified condition. + + Purpose: Simplify the condition given context-sensitive knowledge from the domain. + +\*******************************************************************/ + +exprt constant_propagator_domaint::domain_simplify (const exprt &condition, + const namespacet &ns, + const bool lhs) const +{ + if (lhs) { + // For now do not simplify the left hand sides of assignments + return condition; + } else { + exprt e(condition); + values.replace_const(e); + return simplify_expr(e, ns); + } +} + +/*******************************************************************\ + Function: constant_propagator_domaint::is_array_constant Inputs: diff --git a/src/analyses/constant_propagator.h b/src/analyses/constant_propagator.h index d98e9cf744e..81c02d6b9ba 100644 --- a/src/analyses/constant_propagator.h +++ b/src/analyses/constant_propagator.h @@ -22,6 +22,7 @@ class constant_propagator_domaint:public ai_domain_baset void make_bottom() override final { values.set_to_bottom(); } void make_entry() override final { values.set_to_top(); } bool merge(const constant_propagator_domaint &, locationt, locationt); + virtual exprt domain_simplify (const exprt &condition, const namespacet &ns, const bool lhs = false) const; struct valuest { From 8f465ed002c6f5ac1cc7393e372450455267d970 Mon Sep 17 00:00:00 2001 From: Martin Brain Date: Fri, 9 Sep 2016 08:19:26 +0100 Subject: [PATCH 10/13] Lucas' rather fantastic regression tests with flags and status updated to match the refactoring. Where the current precision is insufficient, the tests are marked FUTURE. --- regression/goto-analyzer/Makefile | 6 ++ .../constant_propagation1.c | 14 ++++ .../constant_propagation_01/test.desc | 9 +++ .../constant_propagation_02.c | 13 +++ .../constant_propagation_02/original | 3 + .../constant_propagation_02/simplified | 81 +++++++++++++++++++ .../constant_propagation_02/test.desc | 9 +++ .../constant_propagation_03.c | 13 +++ .../constant_propagation_03/test.desc | 9 +++ .../constant_propagation_04.c | 13 +++ .../constant_propagation_04/test.desc | 9 +++ .../constant_propagation_05.c | 13 +++ .../constant_propagation_05/test.desc | 8 ++ .../constant_propagation_06.c | 30 +++++++ .../constant_propagation_06/test.desc | 15 ++++ .../constant_propagation_07.c | 14 ++++ .../constant_propagation_07/test.desc | 8 ++ .../constant_propagation_08.c | 16 ++++ .../constant_propagation_08/test.desc | 10 +++ .../constant_propagation_09.c | 14 ++++ .../constant_propagation_09/test.desc | 9 +++ .../constant_propagation_10.c | 25 ++++++ .../constant_propagation_10/test.desc | 9 +++ .../constant_propagation_11.c | 17 ++++ .../constant_propagation_11/test.desc | 9 +++ .../constant_propagation_12.c | 13 +++ .../constant_propagation_12/test.desc | 9 +++ .../constant_propagation_13.c | 14 ++++ .../constant_propagation_13/test.desc | 8 ++ .../constant_propagation_14.c | 13 +++ .../constant_propagation_14/test.desc | 9 +++ .../constant_propagation_15.c | 13 +++ .../constant_propagation_15/test.desc | 9 +++ .../constant_propagation_16.c | 13 +++ .../constant_propagation_16/test.desc | 8 ++ .../constant_propagation_17.c | 16 ++++ .../constant_propagation_17/test.desc | 9 +++ .../constant_propagation_18.c | 13 +++ .../constant_propagation_18/test.desc | 8 ++ .../goto-analyzer/intervals1/intervals1.c | 4 +- regression/goto-analyzer/intervals1/test.desc | 2 +- .../goto-analyzer/intervals10/intervals10.c | 21 +++++ .../goto-analyzer/intervals10/test.desc | 12 +++ .../goto-analyzer/intervals11/intervals11.c | 43 ++++++++++ .../goto-analyzer/intervals11/test.desc | 9 +++ .../goto-analyzer/intervals12/intervals12.c | 16 ++++ .../goto-analyzer/intervals12/test.desc | 9 +++ .../goto-analyzer/intervals2/intervals2.c | 6 +- regression/goto-analyzer/intervals2/test.desc | 2 +- regression/goto-analyzer/intervals3/test.desc | 2 +- regression/goto-analyzer/intervals4/test.desc | 2 +- regression/goto-analyzer/intervals5/test.desc | 2 +- regression/goto-analyzer/intervals6/test.desc | 6 +- regression/goto-analyzer/intervals7/test.desc | 6 +- .../goto-analyzer/intervals8/intervals8.c | 9 +++ regression/goto-analyzer/intervals8/test.desc | 8 ++ .../goto-analyzer/intervals9/intervals9.c | 12 +++ regression/goto-analyzer/intervals9/test.desc | 8 ++ 58 files changed, 694 insertions(+), 16 deletions(-) create mode 100644 regression/goto-analyzer/constant_propagation_01/constant_propagation1.c create mode 100644 regression/goto-analyzer/constant_propagation_01/test.desc create mode 100644 regression/goto-analyzer/constant_propagation_02/constant_propagation_02.c create mode 100644 regression/goto-analyzer/constant_propagation_02/original create mode 100644 regression/goto-analyzer/constant_propagation_02/simplified create mode 100644 regression/goto-analyzer/constant_propagation_02/test.desc create mode 100644 regression/goto-analyzer/constant_propagation_03/constant_propagation_03.c create mode 100644 regression/goto-analyzer/constant_propagation_03/test.desc create mode 100644 regression/goto-analyzer/constant_propagation_04/constant_propagation_04.c create mode 100644 regression/goto-analyzer/constant_propagation_04/test.desc create mode 100644 regression/goto-analyzer/constant_propagation_05/constant_propagation_05.c create mode 100644 regression/goto-analyzer/constant_propagation_05/test.desc create mode 100644 regression/goto-analyzer/constant_propagation_06/constant_propagation_06.c create mode 100644 regression/goto-analyzer/constant_propagation_06/test.desc create mode 100644 regression/goto-analyzer/constant_propagation_07/constant_propagation_07.c create mode 100644 regression/goto-analyzer/constant_propagation_07/test.desc create mode 100644 regression/goto-analyzer/constant_propagation_08/constant_propagation_08.c create mode 100644 regression/goto-analyzer/constant_propagation_08/test.desc create mode 100644 regression/goto-analyzer/constant_propagation_09/constant_propagation_09.c create mode 100644 regression/goto-analyzer/constant_propagation_09/test.desc create mode 100644 regression/goto-analyzer/constant_propagation_10/constant_propagation_10.c create mode 100644 regression/goto-analyzer/constant_propagation_10/test.desc create mode 100644 regression/goto-analyzer/constant_propagation_11/constant_propagation_11.c create mode 100644 regression/goto-analyzer/constant_propagation_11/test.desc create mode 100644 regression/goto-analyzer/constant_propagation_12/constant_propagation_12.c create mode 100644 regression/goto-analyzer/constant_propagation_12/test.desc create mode 100644 regression/goto-analyzer/constant_propagation_13/constant_propagation_13.c create mode 100644 regression/goto-analyzer/constant_propagation_13/test.desc create mode 100644 regression/goto-analyzer/constant_propagation_14/constant_propagation_14.c create mode 100644 regression/goto-analyzer/constant_propagation_14/test.desc create mode 100644 regression/goto-analyzer/constant_propagation_15/constant_propagation_15.c create mode 100644 regression/goto-analyzer/constant_propagation_15/test.desc create mode 100644 regression/goto-analyzer/constant_propagation_16/constant_propagation_16.c create mode 100644 regression/goto-analyzer/constant_propagation_16/test.desc create mode 100644 regression/goto-analyzer/constant_propagation_17/constant_propagation_17.c create mode 100644 regression/goto-analyzer/constant_propagation_17/test.desc create mode 100644 regression/goto-analyzer/constant_propagation_18/constant_propagation_18.c create mode 100644 regression/goto-analyzer/constant_propagation_18/test.desc create mode 100644 regression/goto-analyzer/intervals10/intervals10.c create mode 100644 regression/goto-analyzer/intervals10/test.desc create mode 100644 regression/goto-analyzer/intervals11/intervals11.c create mode 100644 regression/goto-analyzer/intervals11/test.desc create mode 100644 regression/goto-analyzer/intervals12/intervals12.c create mode 100644 regression/goto-analyzer/intervals12/test.desc create mode 100644 regression/goto-analyzer/intervals8/intervals8.c create mode 100644 regression/goto-analyzer/intervals8/test.desc create mode 100644 regression/goto-analyzer/intervals9/intervals9.c create mode 100644 regression/goto-analyzer/intervals9/test.desc diff --git a/regression/goto-analyzer/Makefile b/regression/goto-analyzer/Makefile index 5701431a37e..2c534c8749a 100644 --- a/regression/goto-analyzer/Makefile +++ b/regression/goto-analyzer/Makefile @@ -12,3 +12,9 @@ show: vim -o "$$dir/*.java" "$$dir/*.out"; \ fi; \ done; + +clean: + find . -name *.*~ | xargs rm -f + find . -name *.out | xargs rm -f + find . -name *.goto | xargs rm -f + rm -f tests.log diff --git a/regression/goto-analyzer/constant_propagation_01/constant_propagation1.c b/regression/goto-analyzer/constant_propagation_01/constant_propagation1.c new file mode 100644 index 00000000000..801a21535a9 --- /dev/null +++ b/regression/goto-analyzer/constant_propagation_01/constant_propagation1.c @@ -0,0 +1,14 @@ +#include + +int main() +{ + int i, j=20; + + if (j==20) + { + int x=1,y=2,z; + z=x+y; + assert(z==3); + } + +} diff --git a/regression/goto-analyzer/constant_propagation_01/test.desc b/regression/goto-analyzer/constant_propagation_01/test.desc new file mode 100644 index 00000000000..7e9cac6056b --- /dev/null +++ b/regression/goto-analyzer/constant_propagation_01/test.desc @@ -0,0 +1,9 @@ +CORE +constant_propagation1.c +--constants --simplify out.goto +^EXIT=0$ +^SIGNAL=0$ +^SIMPLIFIED: assert: 1, assume: 0, goto: 2, assigns: 5, function calls: 0$ +^UNMODIFIED: assert: 0, assume: 0, goto: 0, assigns: 12, function calls: 2$ +-- +^warning: ignoring diff --git a/regression/goto-analyzer/constant_propagation_02/constant_propagation_02.c b/regression/goto-analyzer/constant_propagation_02/constant_propagation_02.c new file mode 100644 index 00000000000..ff139437bd8 --- /dev/null +++ b/regression/goto-analyzer/constant_propagation_02/constant_propagation_02.c @@ -0,0 +1,13 @@ +#include + +int main() +{ + int i=0, j=2; + + if (i==0) + { + i++; + j++; + } + assert(j!=3); +} diff --git a/regression/goto-analyzer/constant_propagation_02/original b/regression/goto-analyzer/constant_propagation_02/original new file mode 100644 index 00000000000..13a9e245c81 --- /dev/null +++ b/regression/goto-analyzer/constant_propagation_02/original @@ -0,0 +1,3 @@ +Task defaults to --show +Domain defaults to --constants +GOTO-ANALYSER version 5.5 64-bit x86_64 linux diff --git a/regression/goto-analyzer/constant_propagation_02/simplified b/regression/goto-analyzer/constant_propagation_02/simplified new file mode 100644 index 00000000000..6c722a607de --- /dev/null +++ b/regression/goto-analyzer/constant_propagation_02/simplified @@ -0,0 +1,81 @@ +Reading GOTO program from `out.goto' +^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + +main /* main */ + // 0 file constant_propagation_02.c line 5 function main + signed int i; + // 1 file constant_propagation_02.c line 5 function main + i = 0; + // 2 file constant_propagation_02.c line 5 function main + signed int j; + // 3 file constant_propagation_02.c line 5 function main + j = 2; + // 4 file constant_propagation_02.c line 7 function main + IF FALSE THEN GOTO 1 + // 5 file constant_propagation_02.c line 9 function main + 0 = 1; + // 6 file constant_propagation_02.c line 10 function main + 2 = 3; + // 7 no location + 1: SKIP + // 8 file constant_propagation_02.c line 12 function main + ASSERT FALSE // assertion j!=3 + // 9 file constant_propagation_02.c line 12 function main + GOTO 2 + // 10 file constant_propagation_02.c line 12 function main + (void)0; + // 11 no location + 2: SKIP + // 12 file constant_propagation_02.c line 13 function main + dead j; + // 13 file constant_propagation_02.c line 13 function main + dead i; + // 14 file constant_propagation_02.c line 13 function main + main#return_value = NONDET(signed int); + // 15 file constant_propagation_02.c line 13 function main + END_FUNCTION +^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + +_start /* _start */ + // 16 no location + __CPROVER_initialize(); + // 17 file constant_propagation_02.c line 3 + main(); + // 18 file constant_propagation_02.c line 3 + return' = main#return_value; + // 19 file constant_propagation_02.c line 3 + dead main#return_value; + // 20 file constant_propagation_02.c line 3 + OUTPUT("return", return'); + // 21 no location + END_FUNCTION +^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + +__CPROVER_initialize /* __CPROVER_initialize */ + // 22 no location + // Labels: __CPROVER_HIDE + SKIP + // 23 file line 39 + __CPROVER_dead_object = NULL; + // 24 file line 38 + __CPROVER_deallocated = NULL; + // 25 file line 42 + __CPROVER_malloc_is_new_array = FALSE; + // 26 file line 40 + __CPROVER_malloc_object = NULL; + // 27 file line 41 + __CPROVER_malloc_size = 0ul; + // 28 file line 43 + __CPROVER_memory_leak = NULL; + // 29 file line 31 + __CPROVER_next_thread_id = 0ul; + // 30 file line 85 + __CPROVER_pipe_count = 0u; + // 31 file line 65 + __CPROVER_rounding_mode = 0; + // 32 file line 29 + __CPROVER_thread_id = 0ul; + // 33 file line 30 + __CPROVER_threads_exited = ARRAY_OF(FALSE); + // 34 no location + END_FUNCTION diff --git a/regression/goto-analyzer/constant_propagation_02/test.desc b/regression/goto-analyzer/constant_propagation_02/test.desc new file mode 100644 index 00000000000..635f7dcf620 --- /dev/null +++ b/regression/goto-analyzer/constant_propagation_02/test.desc @@ -0,0 +1,9 @@ +CORE +constant_propagation_02.c +--constants --simplify out.goto +^EXIT=0$ +^SIGNAL=0$ +^SIMPLIFIED: assert: 1, assume: 0, goto: 2, assigns: 6, function calls: 0$ +^UNMODIFIED: assert: 0, assume: 0, goto: 0, assigns: 11, function calls: 2$ +-- +^warning: ignoring diff --git a/regression/goto-analyzer/constant_propagation_03/constant_propagation_03.c b/regression/goto-analyzer/constant_propagation_03/constant_propagation_03.c new file mode 100644 index 00000000000..f08f6020d82 --- /dev/null +++ b/regression/goto-analyzer/constant_propagation_03/constant_propagation_03.c @@ -0,0 +1,13 @@ +#include + +int main() +{ + int i=0, j=2; + + if (i==0) + { + i++; + j++; + } + assert(j==3); +} diff --git a/regression/goto-analyzer/constant_propagation_03/test.desc b/regression/goto-analyzer/constant_propagation_03/test.desc new file mode 100644 index 00000000000..37962658987 --- /dev/null +++ b/regression/goto-analyzer/constant_propagation_03/test.desc @@ -0,0 +1,9 @@ +CORE +constant_propagation_03.c +--constants --simplify out.goto +^EXIT=0$ +^SIGNAL=0$ +^SIMPLIFIED: assert: 1, assume: 0, goto: 2, assigns: 6, function calls: 0$ +^UNMODIFIED: assert: 0, assume: 0, goto: 0, assigns: 11, function calls: 2$ +-- +^warning: ignoring diff --git a/regression/goto-analyzer/constant_propagation_04/constant_propagation_04.c b/regression/goto-analyzer/constant_propagation_04/constant_propagation_04.c new file mode 100644 index 00000000000..ca003ccd2b8 --- /dev/null +++ b/regression/goto-analyzer/constant_propagation_04/constant_propagation_04.c @@ -0,0 +1,13 @@ +#include + +int main() +{ + int i=0, j=2; + + if (i<50) + { + i++; + j++; + } + assert(j==3); +} diff --git a/regression/goto-analyzer/constant_propagation_04/test.desc b/regression/goto-analyzer/constant_propagation_04/test.desc new file mode 100644 index 00000000000..2b23ac224f7 --- /dev/null +++ b/regression/goto-analyzer/constant_propagation_04/test.desc @@ -0,0 +1,9 @@ +CORE +constant_propagation_04.c +--constants --simplify out.goto +^EXIT=0$ +^SIGNAL=0$ +^SIMPLIFIED: assert: 1, assume: 0, goto: 2, assigns: 6, function calls: 0$ +^UNMODIFIED: assert: 0, assume: 0, goto: 0, assigns: 11, function calls: 2$ +-- +^warning: ignoring diff --git a/regression/goto-analyzer/constant_propagation_05/constant_propagation_05.c b/regression/goto-analyzer/constant_propagation_05/constant_propagation_05.c new file mode 100644 index 00000000000..037fbbe0632 --- /dev/null +++ b/regression/goto-analyzer/constant_propagation_05/constant_propagation_05.c @@ -0,0 +1,13 @@ +#include + +int main() +{ + int i=0, j=2; + + if (i<50) + { + i++; + j++; + } + assert(j!=3); +} diff --git a/regression/goto-analyzer/constant_propagation_05/test.desc b/regression/goto-analyzer/constant_propagation_05/test.desc new file mode 100644 index 00000000000..84712b085da --- /dev/null +++ b/regression/goto-analyzer/constant_propagation_05/test.desc @@ -0,0 +1,8 @@ +CORE +constant_propagation_05.c +--constants --verify +^EXIT=0$ +^SIGNAL=0$ +^\[main.assertion.1\] file constant_propagation_05.c line 12 function main, assertion j!=3: FAILURE (if reachable)$ +-- +^warning: ignoring diff --git a/regression/goto-analyzer/constant_propagation_06/constant_propagation_06.c b/regression/goto-analyzer/constant_propagation_06/constant_propagation_06.c new file mode 100644 index 00000000000..d1d29427250 --- /dev/null +++ b/regression/goto-analyzer/constant_propagation_06/constant_propagation_06.c @@ -0,0 +1,30 @@ +#include + +int main() +{ + int i, j=20; + + if(i>=20) + assert(i>=10); // success + + if(i>=10 && i<=20) + assert(i!=30); // success + + if(i>=10 && i<=20) + assert(i!=15); // fails + + if(i<1 && i>10) + assert(0); // success + + if(i>=10 && j>=i) + assert(j>=10); // success + + if(i>=j) + assert(i>=j); // unknown + + if(i>10) + assert(i>=11); // success + + if(i<=100 && j=10: SUCCESS$ +^\[main.assertion.2\] file constant_propagation_06.c line 11 function main, assertion i!=30: SUCCESS$ +^\[main.assertion.3\] file constant_propagation_06.c line 14 function main, assertion i!=15: UNKNOWN$ +^\[main.assertion.4\] file constant_propagation_06.c line 17 function main, assertion 0: SUCCESS$ +^\[main.assertion.5\] file constant_propagation_06.c line 20 function main, assertion j>=10: SUCCESS$ +^\[main.assertion.6\] file constant_propagation_06.c line 23 function main, assertion i>=j: UNKNOWN$ +^\[main.assertion.7\] file constant_propagation_06.c line 26 function main, assertion i>=11: SUCCESS$ +^\[main.assertion.8\] file constant_propagation_06.c line 29 function main, assertion j<100: SUCCESS$ +-- +^warning: ignoring diff --git a/regression/goto-analyzer/constant_propagation_07/constant_propagation_07.c b/regression/goto-analyzer/constant_propagation_07/constant_propagation_07.c new file mode 100644 index 00000000000..40b04edfdd0 --- /dev/null +++ b/regression/goto-analyzer/constant_propagation_07/constant_propagation_07.c @@ -0,0 +1,14 @@ +#include + +int main() +{ + int i=0, j=2; + + while (i<50) + { + i++; + j++; + } + assert(i<51); +} + diff --git a/regression/goto-analyzer/constant_propagation_07/test.desc b/regression/goto-analyzer/constant_propagation_07/test.desc new file mode 100644 index 00000000000..7494eafcd54 --- /dev/null +++ b/regression/goto-analyzer/constant_propagation_07/test.desc @@ -0,0 +1,8 @@ +CORE +constant_propagation_07.c +--constants --verify +^EXIT=0$ +^SIGNAL=0$ +^\[main.assertion.1\] file constant_propagation_07.c line 12 function main, assertion i<51: UNKNOWN$ +-- +^warning: ignoring diff --git a/regression/goto-analyzer/constant_propagation_08/constant_propagation_08.c b/regression/goto-analyzer/constant_propagation_08/constant_propagation_08.c new file mode 100644 index 00000000000..3909e3889e4 --- /dev/null +++ b/regression/goto-analyzer/constant_propagation_08/constant_propagation_08.c @@ -0,0 +1,16 @@ +#include + +int main() +{ + int i=0, j=2; + + while (i<=50) + { + i++; + j++; + } + assert(i<50); + assert(i<51); + assert(i<52); +} + diff --git a/regression/goto-analyzer/constant_propagation_08/test.desc b/regression/goto-analyzer/constant_propagation_08/test.desc new file mode 100644 index 00000000000..994c2c532df --- /dev/null +++ b/regression/goto-analyzer/constant_propagation_08/test.desc @@ -0,0 +1,10 @@ +FUTURE +constant_propagation_08.c +--intervals --verify +^EXIT=0$ +^SIGNAL=0$ +^\[main.assertion.1\] file constant_propagation_08.c line 12 function main, assertion i<50: UNKNOWN$ +^\[main.assertion.2\] file constant_propagation_08.c line 13 function main, assertion i<51: UNKNOWN$ +^\[main.assertion.3\] file constant_propagation_08.c line 14 function main, assertion i<52: SUCCESS$ +-- +^warning: ignoring diff --git a/regression/goto-analyzer/constant_propagation_09/constant_propagation_09.c b/regression/goto-analyzer/constant_propagation_09/constant_propagation_09.c new file mode 100644 index 00000000000..002e9063228 --- /dev/null +++ b/regression/goto-analyzer/constant_propagation_09/constant_propagation_09.c @@ -0,0 +1,14 @@ +#include + +int main() +{ + int i=0, j=2; + + while (i<=50) + { + i++; + j++; + } + assert(j<52); +} + diff --git a/regression/goto-analyzer/constant_propagation_09/test.desc b/regression/goto-analyzer/constant_propagation_09/test.desc new file mode 100644 index 00000000000..8cb0ec6a003 --- /dev/null +++ b/regression/goto-analyzer/constant_propagation_09/test.desc @@ -0,0 +1,9 @@ +CORE +constant_propagation_09.c +--intervals --verify +^EXIT=0$ +^SIGNAL=0$ +******** Function main +^\[main.assertion.1\] file constant_propagation_09.c line 12 function main, assertion j<52: UNKNOWN$ +-- +^warning: ignoring diff --git a/regression/goto-analyzer/constant_propagation_10/constant_propagation_10.c b/regression/goto-analyzer/constant_propagation_10/constant_propagation_10.c new file mode 100644 index 00000000000..169f7965b9d --- /dev/null +++ b/regression/goto-analyzer/constant_propagation_10/constant_propagation_10.c @@ -0,0 +1,25 @@ +#include +int main() +{ + signed int i; + signed int j; + i = 0; + if(!(i >= 2)) + { + j = j + 1; + i = i + 1; + if(!(i >= 2)) + { + j = j + 1; + i = i + 1; + if(!(i >= 2)) + { + j = j + 1; + i = i + 1; + } + assert(!(i < 2)); + } + } + return 0; +} + diff --git a/regression/goto-analyzer/constant_propagation_10/test.desc b/regression/goto-analyzer/constant_propagation_10/test.desc new file mode 100644 index 00000000000..7b78521a13d --- /dev/null +++ b/regression/goto-analyzer/constant_propagation_10/test.desc @@ -0,0 +1,9 @@ +CORE +constant_propagation_10.c +--constants --simplify out.goto +^EXIT=0$ +^SIGNAL=0$ +^SIMPLIFIED: assert: 1, assume: 0, goto: 4, assigns: 10, function calls: 0$ +^UNMODIFIED: assert: 0, assume: 0, goto: 1, assigns: 10, function calls: 2$ +-- +^warning: ignoring diff --git a/regression/goto-analyzer/constant_propagation_11/constant_propagation_11.c b/regression/goto-analyzer/constant_propagation_11/constant_propagation_11.c new file mode 100644 index 00000000000..3022a4f0f19 --- /dev/null +++ b/regression/goto-analyzer/constant_propagation_11/constant_propagation_11.c @@ -0,0 +1,17 @@ +#include +int main() +{ + int a[2]; + int i; + i = 0; + + if (i==0) + a[0]=1; + else + a[1]=2; + + assert(a[0]==1 || a[1]==2); + + return 0; +} + diff --git a/regression/goto-analyzer/constant_propagation_11/test.desc b/regression/goto-analyzer/constant_propagation_11/test.desc new file mode 100644 index 00000000000..7c849326cf6 --- /dev/null +++ b/regression/goto-analyzer/constant_propagation_11/test.desc @@ -0,0 +1,9 @@ +FUTURE +constant_propagation_11.c +--constants --simplify out.goto +^EXIT=0$ +^SIGNAL=0$ +^SIMPLIFIED: assert: 1, assume: 0, goto: 2, assigns: 5, function calls: 0$ +^UNMODIFIED: assert: 0, assume: 0, goto: 4, assigns: 13, function calls: 2$ +-- +^warning: ignoring diff --git a/regression/goto-analyzer/constant_propagation_12/constant_propagation_12.c b/regression/goto-analyzer/constant_propagation_12/constant_propagation_12.c new file mode 100644 index 00000000000..55ea9ac7fc2 --- /dev/null +++ b/regression/goto-analyzer/constant_propagation_12/constant_propagation_12.c @@ -0,0 +1,13 @@ +#include +int main() +{ + int a[2]={0,0}; + + if (a[0]==0) + a[0]=1; + + assert(a[0]==0); + + return 0; +} + diff --git a/regression/goto-analyzer/constant_propagation_12/test.desc b/regression/goto-analyzer/constant_propagation_12/test.desc new file mode 100644 index 00000000000..ca5803363ad --- /dev/null +++ b/regression/goto-analyzer/constant_propagation_12/test.desc @@ -0,0 +1,9 @@ +FUTURE +constant_propagation_12.c +--constants --simplify out.goto +^EXIT=0$ +^SIGNAL=0$ +^SIMPLIFIED: assert: 1, assume: 0, goto: 3, assigns: 4, function calls: 0$ +^UNMODIFIED: assert: 0, assume: 0, goto: 0, assigns: 11, function calls: 2$ +-- +^warning: ignoring diff --git a/regression/goto-analyzer/constant_propagation_13/constant_propagation_13.c b/regression/goto-analyzer/constant_propagation_13/constant_propagation_13.c new file mode 100644 index 00000000000..ac5933e9177 --- /dev/null +++ b/regression/goto-analyzer/constant_propagation_13/constant_propagation_13.c @@ -0,0 +1,14 @@ +#include +int main() +{ + int a[2]={0,0}; + int i, y; + + if (a[0]==0) + a[0]=1; + + assert(a[0]==2); + + return 0; +} + diff --git a/regression/goto-analyzer/constant_propagation_13/test.desc b/regression/goto-analyzer/constant_propagation_13/test.desc new file mode 100644 index 00000000000..22f10d125e3 --- /dev/null +++ b/regression/goto-analyzer/constant_propagation_13/test.desc @@ -0,0 +1,8 @@ +FUTURE +constant_propagation_13.c +--constants --verify +^EXIT=0$ +^SIGNAL=0$ +^\[main.assertion.1\] file constant_propagation_13.c line 10 function main, assertion a\[0\]==2: FAILURE$ +-- +^warning: ignoring diff --git a/regression/goto-analyzer/constant_propagation_14/constant_propagation_14.c b/regression/goto-analyzer/constant_propagation_14/constant_propagation_14.c new file mode 100644 index 00000000000..124d1e30a20 --- /dev/null +++ b/regression/goto-analyzer/constant_propagation_14/constant_propagation_14.c @@ -0,0 +1,13 @@ +#include +int main() +{ + int a[2]={0,0}; + + if (a[0]==0) + a[0]=1; + + assert(a[0]==1 /*|| a[0]==2*/); + + return 0; +} + diff --git a/regression/goto-analyzer/constant_propagation_14/test.desc b/regression/goto-analyzer/constant_propagation_14/test.desc new file mode 100644 index 00000000000..a39a1f66cda --- /dev/null +++ b/regression/goto-analyzer/constant_propagation_14/test.desc @@ -0,0 +1,9 @@ +FUTURE +constant_propagation_14.c +--constants --simplify out.goto +^EXIT=0$ +^SIGNAL=0$ +^SIMPLIFIED: assert: 1, assume: 0, goto: 0$ +^UNKNOWN: assert: 0, assume: 0, goto: 0$ +-- +^warning: ignoring diff --git a/regression/goto-analyzer/constant_propagation_15/constant_propagation_15.c b/regression/goto-analyzer/constant_propagation_15/constant_propagation_15.c new file mode 100644 index 00000000000..9a7e7692d62 --- /dev/null +++ b/regression/goto-analyzer/constant_propagation_15/constant_propagation_15.c @@ -0,0 +1,13 @@ +#include +int main() +{ + int i=0, y; + + if (i==0) + y=1; + + assert(y==1); + + return 0; +} + diff --git a/regression/goto-analyzer/constant_propagation_15/test.desc b/regression/goto-analyzer/constant_propagation_15/test.desc new file mode 100644 index 00000000000..20d36183eb0 --- /dev/null +++ b/regression/goto-analyzer/constant_propagation_15/test.desc @@ -0,0 +1,9 @@ +FUTURE +constant_propagation_15.c +--constants --simplify out.goto +^EXIT=0$ +^SIGNAL=0$ +^SIMPLIFIED: assert: 1, assume: 0, goto: 1, assigns: 4, function calls: 0$ +^UNMODIFIED: assert: 0, assume: 0, goto: 2, assigns: 11, function calls: 2$ +-- +^warning: ignoring diff --git a/regression/goto-analyzer/constant_propagation_16/constant_propagation_16.c b/regression/goto-analyzer/constant_propagation_16/constant_propagation_16.c new file mode 100644 index 00000000000..102cfd7f812 --- /dev/null +++ b/regression/goto-analyzer/constant_propagation_16/constant_propagation_16.c @@ -0,0 +1,13 @@ +#include +int main() +{ + int i=0, y; + + if (i==0) + y=1; + + assert(y==0); + + return 0; +} + diff --git a/regression/goto-analyzer/constant_propagation_16/test.desc b/regression/goto-analyzer/constant_propagation_16/test.desc new file mode 100644 index 00000000000..b56c871deb4 --- /dev/null +++ b/regression/goto-analyzer/constant_propagation_16/test.desc @@ -0,0 +1,8 @@ +FUTURE +constant_propagation_16.c +--constants --verify +^EXIT=0$ +^SIGNAL=0$ +^\[main.assertion.1\] file constant_propagation_16.c line 9 function main, assertion y==0: FAILURE (if reachable)$ +-- +^warning: ignoring diff --git a/regression/goto-analyzer/constant_propagation_17/constant_propagation_17.c b/regression/goto-analyzer/constant_propagation_17/constant_propagation_17.c new file mode 100644 index 00000000000..8b426fe84b5 --- /dev/null +++ b/regression/goto-analyzer/constant_propagation_17/constant_propagation_17.c @@ -0,0 +1,16 @@ +#include +int main() +{ + int a[2]={0,0}; + + if (a[0]==0) + a[0]=1; + else + a[0]=2; + + assert(a[0]==1 || a[0]==2); + assert(a[0]==1 && a[0]==2); + + return 0; +} + diff --git a/regression/goto-analyzer/constant_propagation_17/test.desc b/regression/goto-analyzer/constant_propagation_17/test.desc new file mode 100644 index 00000000000..acecb91eb0a --- /dev/null +++ b/regression/goto-analyzer/constant_propagation_17/test.desc @@ -0,0 +1,9 @@ +FUTURE +constant_propagation_17.c +--constants --verify +^EXIT=0$ +^SIGNAL=0$ +^\[main.assertion.1\] file constant_propagation_17.c line 11 function main, assertion a\[0\]==1 || a\[0\]==2: SUCCESS$ +^\[main.assertion.2\] file constant_propagation_17.c line 12 function main, assertion a\[0\]==1 && a\[0\]==2: FAILURE$ +-- +^warning: ignoring diff --git a/regression/goto-analyzer/constant_propagation_18/constant_propagation_18.c b/regression/goto-analyzer/constant_propagation_18/constant_propagation_18.c new file mode 100644 index 00000000000..6639f9b5c81 --- /dev/null +++ b/regression/goto-analyzer/constant_propagation_18/constant_propagation_18.c @@ -0,0 +1,13 @@ +#include +int main() +{ + int a[2]={0,0}; + + if (a[0]==0) + a[0]=1; + + assert(a[0]==2); + + return 0; +} + diff --git a/regression/goto-analyzer/constant_propagation_18/test.desc b/regression/goto-analyzer/constant_propagation_18/test.desc new file mode 100644 index 00000000000..7ea74c4d264 --- /dev/null +++ b/regression/goto-analyzer/constant_propagation_18/test.desc @@ -0,0 +1,8 @@ +FUTURE +constant_propagation_18.c +--constants --verify +^EXIT=0$ +^SIGNAL=0$ +^\[main.assertion.1\] file constant_propagation_18.c line 9 function main, assertion a\[0\]==2: FAILURE$ +-- +^warning: ignoring diff --git a/regression/goto-analyzer/intervals1/intervals1.c b/regression/goto-analyzer/intervals1/intervals1.c index a797452b198..cdec490fe6d 100644 --- a/regression/goto-analyzer/intervals1/intervals1.c +++ b/regression/goto-analyzer/intervals1/intervals1.c @@ -2,8 +2,8 @@ int main() { - int i, j; - + int i, j=20; + if(i>=20) assert(i>=10); diff --git a/regression/goto-analyzer/intervals1/test.desc b/regression/goto-analyzer/intervals1/test.desc index 3e81f14023a..7aca700f7a5 100644 --- a/regression/goto-analyzer/intervals1/test.desc +++ b/regression/goto-analyzer/intervals1/test.desc @@ -1,6 +1,6 @@ CORE intervals1.c ---intervals +--intervals --verify ^EXIT=0$ ^SIGNAL=0$ ^\[main.assertion.1\] file intervals1.c line 8 function main, assertion i>=10: SUCCESS$ diff --git a/regression/goto-analyzer/intervals10/intervals10.c b/regression/goto-analyzer/intervals10/intervals10.c new file mode 100644 index 00000000000..b27cc6f2001 --- /dev/null +++ b/regression/goto-analyzer/intervals10/intervals10.c @@ -0,0 +1,21 @@ +#include + +int main() +{ + int i, j; + + if(i<=100 && j100); // fails + + if(i<=100 && j100: FAILURE (if reachable)$ +^\[main.assertion.4\] file intervals10.c line 17 function main, assertion j<99: UNKNOWN$ +^\[main.assertion.5\] file intervals10.c line 20 function main, assertion j==100: FAILURE (if reachable)$ +-- +^warning: ignoring diff --git a/regression/goto-analyzer/intervals11/intervals11.c b/regression/goto-analyzer/intervals11/intervals11.c new file mode 100644 index 00000000000..2f061cd554d --- /dev/null +++ b/regression/goto-analyzer/intervals11/intervals11.c @@ -0,0 +1,43 @@ +#include +const int xLen = 10; +const int Alen = 2; +const int Blen = 1; +float nondet_float(); +int main() { + float A[] = {1.0f,-0.5f}; + float B[] = {1.0f}; + int i,j; + float x[xLen]; + float x_aux[xLen]; + float y[xLen]; + float y_aux[xLen]; + float total=0; + for (i=0;i=-1 && x[i]<=1); + x_aux[i]=0; + y_aux[i]=0; + } + for(i=0;i=1;j--) + x_aux[j] = x_aux[j-1]; + x_aux[0] = x[i]; + /* Num, x values */ + for (j = 0; j < Blen; j++) { + y[i] = y[i] + B[j]*x_aux[j]; + assert(y[i]>=-1.0f && y[i]<=1.0f); //success + } + /* Den, y values */ + for(j=0;j=-1.0f && y[i]<=1.0f); //fails + } + /* Update past y values */ + for(j=Alen-2;j>=1;j--) + y_aux[j] = y_aux[j-1]; + y_aux[0] = y[i]; + } +} + diff --git a/regression/goto-analyzer/intervals11/test.desc b/regression/goto-analyzer/intervals11/test.desc new file mode 100644 index 00000000000..039cbffbeb0 --- /dev/null +++ b/regression/goto-analyzer/intervals11/test.desc @@ -0,0 +1,9 @@ +FUTURE +intervals11.c +--intervals --verify +^EXIT=0$ +^SIGNAL=0$ +^\[main.assertion.1\] file intervals11.c line 30 function main, assertion y\[i\]>=-1.0f && y\[i\]<=1.0f: UNKNOWN$ +^\[main.assertion.2\] file intervals11.c line 35 function main, assertion y\[i\]>=-1.0f && y\[i\]<=1.0f: UNKNOWN$ +-- +^warning: ignoring diff --git a/regression/goto-analyzer/intervals12/intervals12.c b/regression/goto-analyzer/intervals12/intervals12.c new file mode 100644 index 00000000000..15d865adf80 --- /dev/null +++ b/regression/goto-analyzer/intervals12/intervals12.c @@ -0,0 +1,16 @@ +#include + +int main (void) { + int i; + int j; + + if (i <= 0 && j < i) + assert(j < 0); + + if (j < i && i <= 0) + assert(j < 0); + + return 0; +} + + diff --git a/regression/goto-analyzer/intervals12/test.desc b/regression/goto-analyzer/intervals12/test.desc new file mode 100644 index 00000000000..59a724c28b5 --- /dev/null +++ b/regression/goto-analyzer/intervals12/test.desc @@ -0,0 +1,9 @@ +FUTURE +intervals12.c +--intervals --verify +^EXIT=0$ +^SIGNAL=0$ +^[main.assertion.1] file intervals12.c line 8 function main, assertion j < 0: SUCCESS$ +^[main.assertion.2] file intervals12.c line 11 function main, assertion j < 0: SUCCESS$ +-- +^warning: ignoring diff --git a/regression/goto-analyzer/intervals2/intervals2.c b/regression/goto-analyzer/intervals2/intervals2.c index d1eaf25240e..d542854bb6a 100644 --- a/regression/goto-analyzer/intervals2/intervals2.c +++ b/regression/goto-analyzer/intervals2/intervals2.c @@ -2,10 +2,10 @@ int main(){ int x; - if (x > 0) { - if (x < 20) { + if (x > 0 && x < 20) { + //if (x < 20) { assert(x > -10 && x < 100); - } + //} } return 0; } diff --git a/regression/goto-analyzer/intervals2/test.desc b/regression/goto-analyzer/intervals2/test.desc index 0c017f6b333..3341c4cd069 100644 --- a/regression/goto-analyzer/intervals2/test.desc +++ b/regression/goto-analyzer/intervals2/test.desc @@ -1,6 +1,6 @@ CORE intervals2.c ---intervals +--intervals --verify ^EXIT=0$ ^SIGNAL=0$ ^\[main.assertion.1\] file intervals2.c line 7 function main, assertion x > -10 && x < 100: SUCCESS$ diff --git a/regression/goto-analyzer/intervals3/test.desc b/regression/goto-analyzer/intervals3/test.desc index 5db07df08a4..dceec17bc81 100644 --- a/regression/goto-analyzer/intervals3/test.desc +++ b/regression/goto-analyzer/intervals3/test.desc @@ -1,6 +1,6 @@ CORE intervals3.c ---intervals +--intervals --verify ^EXIT=0$ ^SIGNAL=0$ ^\[main.assertion.1\] file intervals3.c line 7 function main, assertion x > -10 || x < 100: SUCCESS$ diff --git a/regression/goto-analyzer/intervals4/test.desc b/regression/goto-analyzer/intervals4/test.desc index 9f56ff02403..92724fd69ee 100644 --- a/regression/goto-analyzer/intervals4/test.desc +++ b/regression/goto-analyzer/intervals4/test.desc @@ -1,6 +1,6 @@ CORE intervals4.c ---intervals +--intervals --verify ^EXIT=0$ ^SIGNAL=0$ ^\[main.assertion.1\] file intervals4.c line 9 function main, assertion i >= 1 && i <= 2: SUCCESS$ diff --git a/regression/goto-analyzer/intervals5/test.desc b/regression/goto-analyzer/intervals5/test.desc index 42554724e2d..0213e7b3297 100644 --- a/regression/goto-analyzer/intervals5/test.desc +++ b/regression/goto-analyzer/intervals5/test.desc @@ -1,6 +1,6 @@ CORE intervals5.c ---intervals +--intervals --verify ^EXIT=0$ ^SIGNAL=0$ ^\[main.assertion.1\] file intervals5.c line 9 function main, assertion i >= 1 || i <= 2: SUCCESS$ diff --git a/regression/goto-analyzer/intervals6/test.desc b/regression/goto-analyzer/intervals6/test.desc index 14fd64f33dd..6e36b7948d2 100644 --- a/regression/goto-analyzer/intervals6/test.desc +++ b/regression/goto-analyzer/intervals6/test.desc @@ -1,8 +1,8 @@ -CORE +FUTURE intervals6.c ---intervals +--intervals --verify ^EXIT=0$ ^SIGNAL=0$ -^\[main.assertion.1\] file intervals6.c line 7 function main, assertion x < -10 || x > 100: UNKNOWN$ +^\[main.assertion.1\] file intervals6.c line 7 function main, assertion x < -10 || x > 100: FAILURE (if reachable)$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/intervals7/test.desc b/regression/goto-analyzer/intervals7/test.desc index aeeb24bd0a9..6a42b4a30ec 100644 --- a/regression/goto-analyzer/intervals7/test.desc +++ b/regression/goto-analyzer/intervals7/test.desc @@ -1,8 +1,8 @@ -CORE +FUTURE intervals7.c ---intervals +--intervals --verify ^EXIT=0$ ^SIGNAL=0$ -^\[main.assertion.1\] file intervals7.c line 7 function main, assertion x < -10 && x > 100: UNKNOWN$ +^\[main.assertion.1\] file intervals7.c line 7 function main, assertion x < -10 && x > 100: FAILURE (if reachable)$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/intervals8/intervals8.c b/regression/goto-analyzer/intervals8/intervals8.c new file mode 100644 index 00000000000..4128ac07ce5 --- /dev/null +++ b/regression/goto-analyzer/intervals8/intervals8.c @@ -0,0 +1,9 @@ +#include + +int main(){ + int x; + if (x > 0 && x < 20) { + assert(x < -10 && x < 100); + } + return 0; +} diff --git a/regression/goto-analyzer/intervals8/test.desc b/regression/goto-analyzer/intervals8/test.desc new file mode 100644 index 00000000000..7500059a717 --- /dev/null +++ b/regression/goto-analyzer/intervals8/test.desc @@ -0,0 +1,8 @@ +FUTURE +intervals8.c +--intervals --verify +^EXIT=0$ +^SIGNAL=0$ +^\[main.assertion.1\] file intervals8.c line 6 function main, assertion x < -10 && x < 100: FAILURE (if reachable)$ +-- +^warning: ignoring diff --git a/regression/goto-analyzer/intervals9/intervals9.c b/regression/goto-analyzer/intervals9/intervals9.c new file mode 100644 index 00000000000..27739c7aa28 --- /dev/null +++ b/regression/goto-analyzer/intervals9/intervals9.c @@ -0,0 +1,12 @@ +#include + +int main() +{ + int i; + + if(i>0) + if(i<3) + assert(i>=1 && i<=2); + + return 0; +} diff --git a/regression/goto-analyzer/intervals9/test.desc b/regression/goto-analyzer/intervals9/test.desc new file mode 100644 index 00000000000..33f92abcdb2 --- /dev/null +++ b/regression/goto-analyzer/intervals9/test.desc @@ -0,0 +1,8 @@ +CORE +intervals9.c +--intervals --verify +^EXIT=0$ +^SIGNAL=0$ +^\[main.assertion.1\] file intervals9.c line 9 function main, assertion i>=1 && i<=2: SUCCESS$ +-- +^warning: ignoring From 1b2209776052a4c38b4a7f986875bb2676d225ad Mon Sep 17 00:00:00 2001 From: martin Date: Tue, 1 Nov 2016 11:01:59 +0000 Subject: [PATCH 11/13] Add output_json to the dependence_graph abstract domain. --- src/analyses/dependence_graph.cpp | 50 +++++++++++++++++++ .../goto_analyzer_parse_options.cpp | 20 ++++++-- .../goto_analyzer_parse_options.h | 5 +- src/goto-analyzer/static_show_domain.cpp | 28 ++++++++--- 4 files changed, 91 insertions(+), 12 deletions(-) diff --git a/src/analyses/dependence_graph.cpp b/src/analyses/dependence_graph.cpp index ddabac0c522..77eb8187b18 100644 --- a/src/analyses/dependence_graph.cpp +++ b/src/analyses/dependence_graph.cpp @@ -11,6 +11,8 @@ Date: August 2013 #include +#include + #include "goto_rw.h" #include "dependence_graph.h" @@ -329,6 +331,54 @@ void dep_graph_domaint::output( } } +/*******************************************************************\ + +Function: dep_graph_domaint::output_json + + Inputs: The abstract interpreter and the namespace. + + Outputs: The domain, formatted as a JSON object. + + Purpose: Outputs the current value of the domain. + +\*******************************************************************/ + + +jsont dep_graph_domaint::output_json( + const ai_baset &ai, + const namespacet &ns) const +{ + json_arrayt graph; + + for(dep_graph_domaint::depst::const_iterator cdi=control_deps.begin(); + cdi!=control_deps.end(); + ++cdi) + { + json_objectt &link=graph.push_back().make_object(); + link["location_number"]= + json_numbert(std::to_string((*cdi)->location_number)); + link["source_location"]= + json_stringt((*cdi)->source_location.as_string()); + link["type"]=json_stringt("control"); + } + + for(dep_graph_domaint::depst::const_iterator ddi=data_deps.begin(); + ddi!=data_deps.end(); + ++ddi) + { + json_objectt &link=graph.push_back().make_object(); + link["location_number"]= + json_numbert(std::to_string((*ddi)->location_number)); + link["source_location"]= + json_stringt((*ddi)->source_location.as_string()); + link["type"]=json_stringt("data"); + } + + return graph; +} + + + /*******************************************************************\ Function: dependence_grapht::add_dep diff --git a/src/goto-analyzer/goto_analyzer_parse_options.cpp b/src/goto-analyzer/goto_analyzer_parse_options.cpp index 9ead2c6ff2d..0ca03a99071 100644 --- a/src/goto-analyzer/goto_analyzer_parse_options.cpp +++ b/src/goto-analyzer/goto_analyzer_parse_options.cpp @@ -179,6 +179,7 @@ void goto_analyzer_parse_optionst::get_command_line_options(optionst &options) options.set_option("text", false); options.set_option("json", false); options.set_option("xml", false); + options.set_option("dot", false); options.set_option("outfile", "-"); if(cmdline.isset("text")) @@ -196,6 +197,11 @@ void goto_analyzer_parse_optionst::get_command_line_options(optionst &options) options.set_option("xml", true); options.set_option("outfile", cmdline.get_value("xml")); } + else if (cmdline.isset("dot")) + { + options.set_option("dot", true); + options.set_option("outfile", cmdline.get_value("dot")); + } else { options.set_option("text", true); @@ -250,6 +256,7 @@ void goto_analyzer_parse_optionst::get_command_line_options(optionst &options) options.set_option("constants", false); options.set_option("intervals", false); options.set_option("non-null", false); + options.set_option("dependence-graph", false); if(cmdline.isset("intervals") || cmdline.isset("show-intervals")) @@ -259,10 +266,13 @@ void goto_analyzer_parse_optionst::get_command_line_options(optionst &options) options.set_option("non-null", true); else if(cmdline.isset("constants")) options.set_option("constants", true); - - if(!(options.get_bool_option("constants") || - options.get_bool_option("intervals") || - options.get_bool_option("non-null"))) + else if (cmdline.isset("dependence-graph")) + options.set_option("dependence-graph", true); + + if (!(options.get_bool_option("constants") || + options.get_bool_option("intervals") || + options.get_bool_option("non-null") || + options.get_bool_option("dependence-graph"))) { status() << "Domain defaults to --constants" << eom; options.set_option("constants", true); @@ -616,11 +626,13 @@ void goto_analyzer_parse_optionst::help() " --constants constant abstraction\n" " --intervals interval abstraction\n" " --non-null non-null abstraction\n" + " --dependence-graph dependency relation between instructions\n" "\n" "Output options:\n" " --text file_name output results in plain text to given file\n" " --json file_name output results in JSON format to given file\n" " --xml file_name output results in XML format to given file\n" + " --dot file_name output results in DOT format to given file\n" "\n" "Other analyses:\n" " --taint file_name perform taint analysis using rules in given file\n" diff --git a/src/goto-analyzer/goto_analyzer_parse_options.h b/src/goto-analyzer/goto_analyzer_parse_options.h index 368af800c13..3feff9f7b27 100644 --- a/src/goto-analyzer/goto_analyzer_parse_options.h +++ b/src/goto-analyzer/goto_analyzer_parse_options.h @@ -33,12 +33,13 @@ class optionst; "(gcc)(arch):" \ "(taint):(show-taint)" \ "(show-local-may-alias)" \ - "(json):(xml):(text):" \ + "(json):(xml):(text):(dot):" \ "(unreachable-instructions)" \ "(intervals)(show-intervals)" \ "(non-null)(show-non-null)" \ "(constants)" \ - "(show)(verify)(simplify):" \ + "(dependence-graph)" \ + "(show)(verify)(simplify):" \ "(flow-sensitive)(concurrent)" class goto_analyzer_parse_optionst: diff --git a/src/goto-analyzer/static_show_domain.cpp b/src/goto-analyzer/static_show_domain.cpp index a3a2616c152..7ad61565a40 100644 --- a/src/goto-analyzer/static_show_domain.cpp +++ b/src/goto-analyzer/static_show_domain.cpp @@ -14,6 +14,7 @@ Author: Martin Brain, martin.brain@cs.ox.ac.uk #include #include +#include #include "static_show_domain.h" @@ -36,18 +37,23 @@ bool static_show_domain( message_handlert &message_handler, std::ostream &out) { - ai_baset *domain=NULL; - + ai_baset *domain = NULL; + namespacet ns(goto_model.symbol_table); + if(options.get_bool_option("flow-sensitive")) { if(options.get_bool_option("constants")) - domain=new ait(); + domain = new ait(); else if(options.get_bool_option("intervals")) - domain=new ait(); + domain = new ait(); + + //else if(options.get_bool_option("non-null")) + // domain = new ait(); + + else if(options.get_bool_option("dependence-graph")) + domain = new dependence_grapht(ns); - // else if(options.get_bool_option("non-null")) - // domain=new ait(); } else if(options.get_bool_option("concurrent")) { @@ -75,10 +81,20 @@ bool static_show_domain( // status() << "Performing analysis" << eom; (*domain)(goto_model); + if(options.get_bool_option("json")) out << domain->output_json(goto_model); else if(options.get_bool_option("xml")) out << domain->output_xml(goto_model); + else if(options.get_bool_option("dot") && options.get_bool_option("dependence-graph")) + { + dependence_grapht *d = dynamic_cast(domain); + assert(d != NULL); + + out << "digraph g {\n"; + d->output_dot(out); + out << "}\n"; + } else domain->output(goto_model, out); From 964d30b931cff7ab10cd9e9c35ce201a47a3b874 Mon Sep 17 00:00:00 2001 From: martin Date: Fri, 16 Dec 2016 17:34:25 +0000 Subject: [PATCH 12/13] Add utility function for remove_unreachable. --- .../goto_analyzer_parse_options.cpp | 2 ++ .../goto_analyzer_parse_options.h | 5 +++-- src/goto-analyzer/static_simplifier.cpp | 18 ++++++++++++++++++ src/goto-programs/remove_unreachable.cpp | 7 +++++++ src/goto-programs/remove_unreachable.h | 1 + 5 files changed, 31 insertions(+), 2 deletions(-) diff --git a/src/goto-analyzer/goto_analyzer_parse_options.cpp b/src/goto-analyzer/goto_analyzer_parse_options.cpp index 0ca03a99071..dd2fbcd6daf 100644 --- a/src/goto-analyzer/goto_analyzer_parse_options.cpp +++ b/src/goto-analyzer/goto_analyzer_parse_options.cpp @@ -233,6 +233,8 @@ void goto_analyzer_parse_optionst::get_command_line_options(optionst &options) options.set_option("show", true); } + // For development allow slicing to be disabled in the simplify task + options.set_option("simplify-slicing", !(cmdline.isset("no-simplify-slicing"))); // Abstract interpreter choice options.set_option("flow-sensitive", false); diff --git a/src/goto-analyzer/goto_analyzer_parse_options.h b/src/goto-analyzer/goto_analyzer_parse_options.h index 3feff9f7b27..2f9c813d7d3 100644 --- a/src/goto-analyzer/goto_analyzer_parse_options.h +++ b/src/goto-analyzer/goto_analyzer_parse_options.h @@ -39,8 +39,9 @@ class optionst; "(non-null)(show-non-null)" \ "(constants)" \ "(dependence-graph)" \ - "(show)(verify)(simplify):" \ - "(flow-sensitive)(concurrent)" + "(show)(verify)(simplify):" \ + "(flow-sensitive)(concurrent)" \ + "(no-simplify-slicing)" class goto_analyzer_parse_optionst: public parse_options_baset, diff --git a/src/goto-analyzer/static_simplifier.cpp b/src/goto-analyzer/static_simplifier.cpp index fe7118563e3..66797d1f11f 100644 --- a/src/goto-analyzer/static_simplifier.cpp +++ b/src/goto-analyzer/static_simplifier.cpp @@ -19,6 +19,9 @@ Author: Lucas Cordeiro, lucas.cordeiro@cs.ox.ac.uk #include #include +#include +#include + #include "static_simplifier.h" template @@ -74,6 +77,21 @@ bool static_simplifiert::operator()(void) status() << "Simplifying program" << eom; simplify_program(); + // Remove obviously unreachable things and (now) unconditional branches + if (options.get_bool_option("simplify-slicing")) + { + status() << "Removing unreachable instructions" << eom; + + remove_skip(goto_functions); // Removes goto false + goto_functions.update(); + + remove_unreachable(goto_functions); // Convert unreachable to skips + goto_functions.update(); + + remove_skip(goto_functions); // Remove all of the new skips + goto_functions.update(); + } + status() << "Writing goto binary" << eom; return write_goto_binary(out, ns.get_symbol_table(), goto_functions); } diff --git a/src/goto-programs/remove_unreachable.cpp b/src/goto-programs/remove_unreachable.cpp index 38f8e93974a..bbf43acefbb 100644 --- a/src/goto-programs/remove_unreachable.cpp +++ b/src/goto-programs/remove_unreachable.cpp @@ -57,3 +57,10 @@ void remove_unreachable(goto_programt &goto_program) it->make_skip(); } } + +void remove_unreachable(goto_functionst &goto_functions) +{ + Forall_goto_functions(f_it, goto_functions) + remove_unreachable(f_it->second.body); +} + diff --git a/src/goto-programs/remove_unreachable.h b/src/goto-programs/remove_unreachable.h index 694cd8c0af8..4fd423641f1 100644 --- a/src/goto-programs/remove_unreachable.h +++ b/src/goto-programs/remove_unreachable.h @@ -12,5 +12,6 @@ Author: Daniel Kroening, kroening@kroening.com #include "goto_functions.h" void remove_unreachable(goto_programt &goto_program); +void remove_unreachable(goto_functionst &goto_functions); #endif // CPROVER_GOTO_PROGRAMS_REMOVE_UNREACHABLE_H From 143310189563d4dd16b9140dc271ba9cd1545f72 Mon Sep 17 00:00:00 2001 From: martin Date: Mon, 19 Dec 2016 19:32:54 +0000 Subject: [PATCH 13/13] Catch exceptions thrown in doit(). --- .../goto_analyzer_parse_options.cpp | 219 ++++++++++++------ 1 file changed, 150 insertions(+), 69 deletions(-) diff --git a/src/goto-analyzer/goto_analyzer_parse_options.cpp b/src/goto-analyzer/goto_analyzer_parse_options.cpp index dd2fbcd6daf..9ef471116ef 100644 --- a/src/goto-analyzer/goto_analyzer_parse_options.cpp +++ b/src/goto-analyzer/goto_analyzer_parse_options.cpp @@ -295,98 +295,112 @@ Function: goto_analyzer_parse_optionst::doit int goto_analyzer_parse_optionst::doit() { - if(cmdline.isset("version")) + try { - std::cout << CBMC_VERSION << std::endl; - return 0; - } + if(cmdline.isset("version")) + { + std::cout << CBMC_VERSION << std::endl; + return 0; + } - // - // command line options - // + // + // command line options + // + + optionst options; + get_command_line_options(options); + eval_verbosity(); - optionst options; - get_command_line_options(options); - eval_verbosity(); + // + // Print a banner + // + status() << "GOTO-ANALYSER version " CBMC_VERSION " " + << sizeof(void *)*8 << "-bit " + << config.this_architecture() << " " + << config.this_operating_system() << eom; - // - // Print a banner - // - status() << "GOTO-ANALYSER version " CBMC_VERSION " " - << sizeof(void *)*8 << "-bit " - << config.this_architecture() << " " - << config.this_operating_system() << eom; + register_languages(); - register_languages(); + goto_model.set_message_handler(get_message_handler()); - goto_model.set_message_handler(get_message_handler()); + if(goto_model(cmdline.args)) + return 6; - if(goto_model(cmdline.args)) - return 6; + if(process_goto_program(options)) + return 6; - if(process_goto_program(options)) - return 6; + if(cmdline.isset("taint")) + { + std::string taint_file=cmdline.get_value("taint"); - if(cmdline.isset("taint")) - { - std::string taint_file=cmdline.get_value("taint"); + if(cmdline.isset("show-taint")) + { + taint_analysis(goto_model, taint_file, get_message_handler(), true, ""); + return 0; + } + else + { + std::string json_file=cmdline.get_value("json"); + bool result=taint_analysis( + goto_model, + taint_file, + get_message_handler(), + false, + json_file); + return result?10:0; + } + } - if(cmdline.isset("show-taint")) + if(cmdline.isset("unreachable-instructions")) { - taint_analysis(goto_model, taint_file, get_message_handler(), true, ""); + const std::string json_file=cmdline.get_value("json"); + + if(json_file.empty()) + unreachable_instructions(goto_model, false, std::cout); + else if(json_file=="-") + unreachable_instructions(goto_model, true, std::cout); + else + { + std::ofstream ofs(json_file); + if(!ofs) + { + error() << "Failed to open json output `" + << json_file << "'" << eom; + return 6; + } + + unreachable_instructions(goto_model, true, ofs); + } + return 0; } - else - { - std::string json_file=cmdline.get_value("json"); - bool result=taint_analysis( - goto_model, - taint_file, - get_message_handler(), - false, - json_file); - return result?10:0; - } - } - - if(cmdline.isset("unreachable-instructions")) - { - const std::string json_file=cmdline.get_value("json"); - if(json_file.empty()) - unreachable_instructions(goto_model, false, std::cout); - else if(json_file=="-") - unreachable_instructions(goto_model, true, std::cout); - else + if(cmdline.isset("show-local-may-alias")) { - std::ofstream ofs(json_file); - if(!ofs) + namespacet ns(goto_model.symbol_table); + + forall_goto_functions(it, goto_model.goto_functions) { - error() << "Failed to open json output `" - << json_file << "'" << eom; - return 6; + std::cout << ">>>>\n"; + std::cout << ">>>> " << it->first << '\n'; + std::cout << ">>>>\n"; + local_may_aliast local_may_alias(it->second); + local_may_alias.output(std::cout, it->second, ns); + std::cout << '\n'; } - unreachable_instructions(goto_model, true, ofs); + return 0; } - return 0; - } - - if(cmdline.isset("show-local-may-alias")) - { - namespacet ns(goto_model.symbol_table); + label_properties(goto_model); - forall_goto_functions(it, goto_model.goto_functions) + if(cmdline.isset("show-properties")) { - std::cout << ">>>>\n"; - std::cout << ">>>> " << it->first << '\n'; - std::cout << ">>>>\n"; - local_may_aliast local_may_alias(it->second); - local_may_alias.output(std::cout, it->second, ns); - std::cout << '\n'; + show_properties(goto_model, get_ui()); + return 0; } +<<<<<<< HEAD return 0; } @@ -415,10 +429,30 @@ int goto_analyzer_parse_optionst::doit() error() << "Failed to open output file `" << outfile << "'" << eom; return 6; +======= + if(set_properties()) + return 7; + + + // Output file factory + std::ostream *out; + const std::string outfile = options.get_option("outfile"); + if (outfile == "-") + out = &std::cout; + else + { + out = new std::ofstream(outfile); + if(!*out) + { + error() << "Failed to open output file `" + << outfile << "'" << eom; + return 6; + } +>>>>>>> 1f65b1a... Catch exceptions thrown in doit(). } - } +<<<<<<< HEAD // Run the analysis bool result=true; if(options.get_bool_option("show")) @@ -441,10 +475,57 @@ int goto_analyzer_parse_optionst::doit() return result?10:0; +======= + // Run the analysis + bool result = true; + if (options.get_bool_option("show")) + result = static_show_domain(goto_model, options, get_message_handler(), *out); + + else if (options.get_bool_option("verify")) + result = static_analyzer(goto_model, options, get_message_handler(), *out); + + else if (options.get_bool_option("simplify")) + result = static_simplifier(goto_model, options, get_message_handler(), *out); + else + { + error() << "No task given" << eom; + return 6; + } + + if (out != &std::cout) + delete out; + + return result?10:0; + +>>>>>>> 1f65b1a... Catch exceptions thrown in doit(). // Final defensive error case error() << "no analysis option given -- consider reading --help" << eom; return 6; + } + catch(const char *e) + { + error() << e << eom; + return 6; + } + + catch(const std::string e) + { + error() << e << eom; + return 6; + } + + catch(int x) + { + return x; + } + + catch(std::bad_alloc) + { + error() << "Out of memory" << eom; + return 6; + } + } /*******************************************************************\