From 02080c85177a96cc6a71f90865b1393f14b6be11 Mon Sep 17 00:00:00 2001 From: Martin Brain Date: Thu, 8 Sep 2016 08:05:42 +0100 Subject: [PATCH 01/24] Make evaluation and/or simplification of conditions/expressions an ai 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 2894cde3b10..64ead3a941f 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 92d684f804996a4b3651df041e6eee66244305ce Mon Sep 17 00:00:00 2001 From: martin Date: Fri, 16 Dec 2016 16:39:29 +0000 Subject: [PATCH 02/24] Implement domain_simplify for intervals. --- src/analyses/interval_domain.cpp | 70 +++++++++++++++++++++++++++++--- src/analyses/interval_domain.h | 14 ++++++- 2 files changed, 77 insertions(+), 7 deletions(-) diff --git a/src/analyses/interval_domain.cpp b/src/analyses/interval_domain.cpp index 1faf8c52364..5a2a493283a 100644 --- a/src/analyses/interval_domain.cpp +++ b/src/analyses/interval_domain.cpp @@ -129,7 +129,7 @@ void interval_domaint::transform( /*******************************************************************\ -Function: interval_domaint::merge +Function: interval_domaint::join Inputs: @@ -139,10 +139,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; @@ -527,3 +525,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 7e95c65e9de..c7ae0896739 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 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() final @@ -85,7 +90,12 @@ class interval_domaint:public ai_domain_baset return bottom; } -private: + virtual exprt domain_simplify( + const exprt &condition, + const namespacet &ns, + const bool lhs=false) const; + +protected: bool bottom; typedef std::map int_mapt; From 07b147be93d8659764175b2fd33489e88cb5b773 Mon Sep 17 00:00:00 2001 From: martin Date: Fri, 16 Dec 2016 16:42:27 +0000 Subject: [PATCH 03/24] Refactor goto-analyzer so that task, analysis, domain and output can be picked independently. --- src/goto-analyzer/Makefile | 2 + .../goto_analyzer_parse_options.cpp | 183 +++++++++-- .../goto_analyzer_parse_options.h | 7 +- src/goto-analyzer/static_analyzer.cpp | 201 ++++++------- 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, 694 insertions(+), 125 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 9eb45165f9c..f582145e85e 100644 --- a/src/goto-analyzer/Makefile +++ b/src/goto-analyzer/Makefile @@ -4,6 +4,8 @@ SRC = goto_analyzer_main.cpp \ taint_analysis.cpp \ taint_parser.cpp \ unreachable_instructions.cpp \ + static_simplifier.cpp \ + static_show_domain.cpp \ # Empty last line 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 5f889ff99d7..61272492bf8 100644 --- a/src/goto-analyzer/goto_analyzer_parse_options.cpp +++ b/src/goto-analyzer/goto_analyzer_parse_options.cpp @@ -32,6 +32,8 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include +#include #include #include @@ -48,6 +50,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" /*******************************************************************\ @@ -174,6 +178,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); + } } /*******************************************************************\ @@ -234,9 +332,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; } } @@ -347,17 +448,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; @@ -533,8 +664,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" + // NOLINTNEXTLINE(whitespace/line_length) + " --verify use the abstract domains to check assertions\n" + // NOLINTNEXTLINE(whitespace/line_length) + " --simplify file_name use the abstract domains to simplify the program\n" + "\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" + "Output options:\n" + " --text file_name output results in plain text to given file\n" + // NOLINTNEXTLINE(whitespace/line_length) + " --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" // NOLINTNEXTLINE(whitespace/line_length) " --taint file_name perform taint analysis using rules in given file\n" " --unreachable-instructions list dead code\n" @@ -542,13 +694,6 @@ void goto_analyzer_parse_optionst::help() " --unreachable-functions list functions unreachable from the entry point\n" // NOLINTNEXTLINE(whitespace/line_length) " --reachable-functions list functions reachable from the entry point\n" - " --intervals interval analysis\n" - " --non-null non-null analysis\n" - "\n" - "Analysis options:\n" - // NOLINTNEXTLINE(whitespace/line_length) - " --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" "C/C++ frontend options:\n" " -I path set include path (C/C++)\n" diff --git a/src/goto-analyzer/goto_analyzer_parse_options.h b/src/goto-analyzer/goto_analyzer_parse_options.h index a72dd9ca76a..c5b06e58004 100644 --- a/src/goto-analyzer/goto_analyzer_parse_options.h +++ b/src/goto-analyzer/goto_analyzer_parse_options.h @@ -38,11 +38,14 @@ class optionst; "(gcc)(arch):" \ "(taint):(show-taint)" \ "(show-local-may-alias)" \ - "(json):(xml):" \ + "(json):(xml):(text):" \ "(unreachable-instructions)(unreachable-functions)" \ "(reachable-functions)" \ "(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 1168cff1a73..47a6fb8282a 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,39 +79,18 @@ bool static_analyzert::operator()() /*******************************************************************\ -Function: static_analyzert::eval - - Inputs: - - Outputs: - - Purpose: - -\*******************************************************************/ - -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 +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. \*******************************************************************/ -void static_analyzert::plain_text_report() +template +void static_analyzert::plain_text_report() { unsigned pass=0, fail=0, unknown=0; @@ -127,7 +109,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() << ']' << ' '; @@ -136,42 +118,36 @@ 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; @@ -188,14 +164,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"); @@ -205,32 +181,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; @@ -247,14 +215,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"); @@ -265,15 +233,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; } @@ -281,21 +241,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 603dae2ed1cb94dc444a001f99090e5d79879c0e Mon Sep 17 00:00:00 2001 From: Martin Brain Date: Fri, 9 Sep 2016 08:07:36 +0100 Subject: [PATCH 04/24] 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 61272492bf8..ba28c1f487e 100644 --- a/src/goto-analyzer/goto_analyzer_parse_options.cpp +++ b/src/goto-analyzer/goto_analyzer_parse_options.cpp @@ -442,12 +442,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 47a6fb8282a..c586daad4ee 100644 --- a/src/goto-analyzer/static_analyzer.cpp +++ b/src/goto-analyzer/static_analyzer.cpp @@ -292,24 +292,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 b316e28c3aadf57d2c8b2b5126f68df5ccb4f105 Mon Sep 17 00:00:00 2001 From: Martin Brain Date: Fri, 9 Sep 2016 09:02:20 +0100 Subject: [PATCH 05/24] 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 6735d558cc3..bd2b4dab22a 100644 --- a/src/analyses/constant_propagator.cpp +++ b/src/analyses/constant_propagator.cpp @@ -333,6 +333,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 0766b458f7d..a48bcf0c8a8 100644 --- a/src/analyses/constant_propagator.h +++ b/src/analyses/constant_propagator.h @@ -29,6 +29,7 @@ class constant_propagator_domaint:public ai_domain_baset void make_bottom() final { values.set_to_bottom(); } void make_entry() 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 c089455daa012ac39bcb6436f47a27f193e0c96d Mon Sep 17 00:00:00 2001 From: martin Date: Tue, 1 Nov 2016 11:01:59 +0000 Subject: [PATCH 06/24] 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 | 3 +- src/goto-analyzer/static_show_domain.cpp | 28 ++++++++--- 4 files changed, 90 insertions(+), 11 deletions(-) diff --git a/src/analyses/dependence_graph.cpp b/src/analyses/dependence_graph.cpp index 93588e209a7..93a73165650 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" @@ -345,6 +347,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 ba28c1f487e..4ceea891a17 100644 --- a/src/goto-analyzer/goto_analyzer_parse_options.cpp +++ b/src/goto-analyzer/goto_analyzer_parse_options.cpp @@ -184,6 +184,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")) @@ -201,6 +202,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); @@ -255,6 +261,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")) @@ -264,10 +271,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); @@ -673,12 +683,14 @@ 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" // NOLINTNEXTLINE(whitespace/line_length) " --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" // NOLINTNEXTLINE(whitespace/line_length) diff --git a/src/goto-analyzer/goto_analyzer_parse_options.h b/src/goto-analyzer/goto_analyzer_parse_options.h index c5b06e58004..4e3118e2456 100644 --- a/src/goto-analyzer/goto_analyzer_parse_options.h +++ b/src/goto-analyzer/goto_analyzer_parse_options.h @@ -38,12 +38,13 @@ class optionst; "(gcc)(arch):" \ "(taint):(show-taint)" \ "(show-local-may-alias)" \ - "(json):(xml):(text):" \ + "(json):(xml):(text):(dot):" \ "(unreachable-instructions)(unreachable-functions)" \ "(reachable-functions)" \ "(intervals)(show-intervals)" \ "(non-null)(show-non-null)" \ "(constants)" \ + "(dependence-graph)" \ "(show)(verify)(simplify):" \ "(flow-sensitive)(concurrent)" 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 39e9d9fd2433df210f8f910cf92a5cc853afed50 Mon Sep 17 00:00:00 2001 From: martin Date: Fri, 16 Dec 2016 17:34:25 +0000 Subject: [PATCH 07/24] Add utility function for remove_unreachable. --- .../goto_analyzer_parse_options.cpp | 2 ++ .../goto_analyzer_parse_options.h | 3 ++- src/goto-analyzer/static_simplifier.cpp | 18 ++++++++++++++++++ src/goto-programs/remove_unreachable.cpp | 7 +++++++ src/goto-programs/remove_unreachable.h | 1 + 5 files changed, 30 insertions(+), 1 deletion(-) diff --git a/src/goto-analyzer/goto_analyzer_parse_options.cpp b/src/goto-analyzer/goto_analyzer_parse_options.cpp index 4ceea891a17..9a101b5a51e 100644 --- a/src/goto-analyzer/goto_analyzer_parse_options.cpp +++ b/src/goto-analyzer/goto_analyzer_parse_options.cpp @@ -238,6 +238,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 4e3118e2456..d7d8c18fccc 100644 --- a/src/goto-analyzer/goto_analyzer_parse_options.h +++ b/src/goto-analyzer/goto_analyzer_parse_options.h @@ -46,7 +46,8 @@ class optionst; "(constants)" \ "(dependence-graph)" \ "(show)(verify)(simplify):" \ - "(flow-sensitive)(concurrent)" + "(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 14f92e97be1..8c87f205e96 100644 --- a/src/goto-programs/remove_unreachable.cpp +++ b/src/goto-programs/remove_unreachable.cpp @@ -55,3 +55,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 1a0e40c00f0ec2b9576077fdbd3fae72b9a50ecb Mon Sep 17 00:00:00 2001 From: martin Date: Mon, 19 Dec 2016 19:32:54 +0000 Subject: [PATCH 08/24] Catch exceptions thrown in doit() in goto analyzer. --- .../goto_analyzer_parse_options.cpp | 334 ++++++++++-------- 1 file changed, 185 insertions(+), 149 deletions(-) diff --git a/src/goto-analyzer/goto_analyzer_parse_options.cpp b/src/goto-analyzer/goto_analyzer_parse_options.cpp index 9a101b5a51e..2c0756d43a1 100644 --- a/src/goto-analyzer/goto_analyzer_parse_options.cpp +++ b/src/goto-analyzer/goto_analyzer_parse_options.cpp @@ -300,204 +300,240 @@ 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-ANALYZER 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)) - return 6; + goto_functionst::function_mapt::const_iterator f_it= + goto_model.goto_functions.function_map.find( + goto_functionst::entry_point()); - if(process_goto_program(options)) - return 6; + if(f_it==goto_model.goto_functions.function_map.end()) + { + error() << "Entry point not found" << eom; + return 6; + } - if(cmdline.isset("taint")) - { - std::string taint_file=cmdline.get_value("taint"); + if(process_goto_program(options)) + return 6; + + status() << "Starting analysis" << eom; - if(cmdline.isset("show-taint")) + if(cmdline.isset("taint")) { - taint_analysis(goto_model, taint_file, get_message_handler(), true, ""); - return 0; + 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; + } } - else + + if(cmdline.isset("unreachable-instructions")) { - 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; - } - } + const std::string json_file=cmdline.get_value("json"); - 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 + { + std::ofstream ofs(json_file); + if(!ofs) + { + error() << "Failed to open json output `" + << json_file << "'" << eom; + return 6; + } + + unreachable_instructions(goto_model, true, ofs); + } - if(json_file.empty()) - unreachable_instructions(goto_model, false, std::cout); - else if(json_file=="-") - unreachable_instructions(goto_model, true, std::cout); - else + return 0; + } + + if(cmdline.isset("unreachable-functions")) { - std::ofstream ofs(json_file); - if(!ofs) + const std::string json_file=cmdline.get_value("json"); + + if(json_file.empty()) + unreachable_functions(goto_model, false, std::cout); + else if(json_file=="-") + unreachable_functions(goto_model, true, std::cout); + else { - error() << "Failed to open json output `" - << json_file << "'" << eom; - return 6; + std::ofstream ofs(json_file); + if(!ofs) + { + error() << "Failed to open json output `" + << json_file << "'" << eom; + return 6; + } + + unreachable_functions(goto_model, true, ofs); } - unreachable_instructions(goto_model, true, ofs); + return 0; } - return 0; - } + if(cmdline.isset("reachable-functions")) + { + const std::string json_file=cmdline.get_value("json"); - if(cmdline.isset("unreachable-functions")) - { - const std::string json_file=cmdline.get_value("json"); + if(json_file.empty()) + reachable_functions(goto_model, false, std::cout); + else if(json_file=="-") + reachable_functions(goto_model, true, std::cout); + else + { + std::ofstream ofs(json_file); + if(!ofs) + { + error() << "Failed to open json output `" + << json_file << "'" << eom; + return 6; + } + + reachable_functions(goto_model, true, ofs); + } - if(json_file.empty()) - unreachable_functions(goto_model, false, std::cout); - else if(json_file=="-") - unreachable_functions(goto_model, true, std::cout); - else + return 0; + } + + 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_functions(goto_model, true, ofs); + return 0; } - return 0; - } + label_properties(goto_model); - if(cmdline.isset("reachable-functions")) - { - const std::string json_file=cmdline.get_value("json"); + if(cmdline.isset("show-properties")) + { + show_properties(goto_model, get_ui()); + return 0; + } - if(json_file.empty()) - reachable_functions(goto_model, false, std::cout); - else if(json_file=="-") - reachable_functions(goto_model, true, std::cout); + 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 { - std::ofstream ofs(json_file); - if(!ofs) + if(options.get_bool_option("simplify")) + out=new std::ofstream(outfile, std::ios::binary); + else + out=new std::ofstream(outfile); + + if(!*out) { - error() << "Failed to open json output `" - << json_file << "'" << eom; + error() << "Failed to open output file `" << outfile << "'" << eom; return 6; } - - reachable_functions(goto_model, true, ofs); } - return 0; - } - - if(cmdline.isset("show-local-may-alias")) - { - namespacet ns(goto_model.symbol_table); - - forall_goto_functions(it, goto_model.goto_functions) + // 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 { - 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'; + error() << "No task given" << eom; + return 6; } - return 0; - } - - label_properties(goto_model); + if(out!=&std::cout) + delete out; - if(cmdline.isset("show-properties")) + return result?10:0; + } + catch(const char *e) { - show_properties(goto_model, get_ui()); - return 0; + error() << e << 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 + catch(const std::string e) { - out=new std::ofstream(outfile); - if(!*out) - { - error() << "Failed to open output file `" - << outfile << "'" << eom; - return 6; - } + error() << e << 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 + catch(int x) + { + return x; + } + catch(std::bad_alloc) { - error() << "No task given" << eom; + error() << "Out of memory" << 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; } /*******************************************************************\ From 1a4a859985f3bc39caf0b91ceca93d02e5423af6 Mon Sep 17 00:00:00 2001 From: Daniel Poetzl Date: Sun, 22 Jan 2017 12:01:45 +0000 Subject: [PATCH 09/24] Fix merging issues in goto analyzer --- src/analyses/dependence_graph.h | 6 +++++- src/goto-analyzer/goto_analyzer_parse_options.cpp | 1 + 2 files changed, 6 insertions(+), 1 deletion(-) diff --git a/src/analyses/dependence_graph.h b/src/analyses/dependence_graph.h index 8b627dd36b0..70ae0df5ac4 100644 --- a/src/analyses/dependence_graph.h +++ b/src/analyses/dependence_graph.h @@ -93,7 +93,11 @@ class dep_graph_domaint:public ai_domain_baset const ai_baset &ai, const namespacet &ns) const final; - void make_top() final + jsont output_json( + const ai_baset &ai, + const namespacet &ns) const; + + void make_top() final override { assert(node_id!=std::numeric_limits::max()); diff --git a/src/goto-analyzer/goto_analyzer_parse_options.cpp b/src/goto-analyzer/goto_analyzer_parse_options.cpp index 2c0756d43a1..12fb67bf968 100644 --- a/src/goto-analyzer/goto_analyzer_parse_options.cpp +++ b/src/goto-analyzer/goto_analyzer_parse_options.cpp @@ -25,6 +25,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #include #include #include From 5b66759741567e3ebb997a4108521d0381eca32a Mon Sep 17 00:00:00 2001 From: Daniel Poetzl Date: Wed, 25 Jan 2017 20:25:17 +0000 Subject: [PATCH 10/24] Fix whitespace to match coding guidelines --- .../goto_analyzer_parse_options.cpp | 64 ++++++++----------- src/goto-analyzer/static_analyzer.cpp | 28 +++++--- src/goto-analyzer/static_show_domain.cpp | 24 +++---- src/goto-analyzer/static_simplifier.cpp | 45 ++++++------- 4 files changed, 78 insertions(+), 83 deletions(-) diff --git a/src/goto-analyzer/goto_analyzer_parse_options.cpp b/src/goto-analyzer/goto_analyzer_parse_options.cpp index 12fb67bf968..318b0a65161 100644 --- a/src/goto-analyzer/goto_analyzer_parse_options.cpp +++ b/src/goto-analyzer/goto_analyzer_parse_options.cpp @@ -1,6 +1,6 @@ /*******************************************************************\ -Module: Goto-Analyser Command Line Option Processing +Module: Goto-Analyzer Command Line Option Processing Author: Daniel Kroening, kroening@kroening.com @@ -142,7 +142,7 @@ void goto_analyzer_parse_optionst::get_command_line_options(optionst &options) exit(1); } - #if 0 +#if 0 if(cmdline.isset("c89")) config.ansi_c.set_c89(); @@ -160,9 +160,9 @@ void goto_analyzer_parse_optionst::get_command_line_options(optionst &options) if(cmdline.isset("cpp11")) config.cpp.set_cpp11(); - #endif +#endif - #if 0 +#if 0 // check assertions if(cmdline.isset("no-assertions")) options.set_option("assertions", false); @@ -178,8 +178,7 @@ void goto_analyzer_parse_optionst::get_command_line_options(optionst &options) // magic error label if(cmdline.isset("error-label")) options.set_option("error-label", cmdline.get_values("error-label")); - #endif - +#endif // Output format choice options.set_option("text", false); @@ -213,15 +212,14 @@ void goto_analyzer_parse_optionst::get_command_line_options(optionst &options) options.set_option("text", true); } - // Task options - options.set_option( "show", false); - options.set_option( "verify", false); + 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")) + cmdline.isset("show-intervals") || + cmdline.isset("show-non-null")) options.set_option("show", true); else if(cmdline.isset("verify")) options.set_option("verify", true); @@ -231,16 +229,18 @@ void goto_analyzer_parse_optionst::get_command_line_options(optionst &options) options.set_option("outfile", cmdline.get_value("simplify")); } - if(!(options.get_bool_option("show") || - options.get_bool_option("verify") || - options.get_bool_option("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); } // For development allow slicing to be disabled in the simplify task - options.set_option("simplify-slicing", !(cmdline.isset("no-simplify-slicing"))); + options.set_option( + "simplify-slicing", + !(cmdline.isset("no-simplify-slicing"))); // Abstract interpreter choice options.set_option("flow-sensitive", false); @@ -251,14 +251,7 @@ void goto_analyzer_parse_optionst::get_command_line_options(optionst &options) 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); - } - + options.set_option("flow-sensitive", true); // Domain choice options.set_option("constants", false); @@ -277,10 +270,10 @@ void goto_analyzer_parse_optionst::get_command_line_options(optionst &options) 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"))) + 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); @@ -556,19 +549,16 @@ bool goto_analyzer_parse_optionst::set_properties() if(cmdline.isset("property")) ::set_properties(goto_model, cmdline.get_values("property")); } - catch(const char *e) { error() << e << eom; return true; } - catch(const std::string e) { error() << e << eom; return true; } - catch(int) { return true; @@ -649,24 +639,20 @@ bool goto_analyzer_parse_optionst::process_goto_program( return true; } } - catch(const char *e) { error() << e << eom; return true; } - catch(const std::string e) { error() << e << eom; return true; } - catch(int) { return true; } - catch(std::bad_alloc) { error() << "Out of memory" << eom; @@ -692,7 +678,7 @@ void goto_analyzer_parse_optionst::help() { std::cout << "\n" - "* * GOTO-ANALYSER " CBMC_VERSION " - Copyright (C) 2016 "; + "* * GOTO-ANALYZER " CBMC_VERSION " - Copyright (C) 2016 "; std::cout << "(" << (sizeof(void *)*8) << "-bit version)"; @@ -719,10 +705,10 @@ void goto_analyzer_parse_optionst::help() " --concurrent use concurrent abstract interpreter\n" "\n" "Domain options:\n" - " --constants constant abstraction\n" - " --intervals interval abstraction\n" - " --non-null non-null abstraction\n" - " --dependence-graph dependency relation between instructions\n" + " --constants constant domain\n" + " --intervals interval domain\n" + " --non-null non-null domain\n" + " --dependence-graph data and control dependencies between instructions\n" // NOLINT(*) "\n" "Output options:\n" " --text file_name output results in plain text to given file\n" diff --git a/src/goto-analyzer/static_analyzer.cpp b/src/goto-analyzer/static_analyzer.cpp index c586daad4ee..0bf4a030970 100644 --- a/src/goto-analyzer/static_analyzer.cpp +++ b/src/goto-analyzer/static_analyzer.cpp @@ -57,7 +57,8 @@ Function: static_analyzert::operator() Outputs: false on success, true on failure. - Purpose: Run the analysis, check the assertions and report in the correct format. + Purpose: Run the analysis, check the assertions and report in the + correct format. \*******************************************************************/ @@ -115,21 +116,31 @@ void static_analyzert::plain_text_report() << ']' << ' '; result() << i_it->source_location; + if(!i_it->source_location.get_comment().empty()) result() << ", " << i_it->source_location.get_comment(); + result() << ": "; + if(simplified.is_true()) - { result() << "SUCCESS"; pass++; } + { + result() << "SUCCESS"; pass++; + } else if(simplified.is_false()) - { result() << "FAILURE (if reachable)"; fail++; } + { + result() << "FAILURE (if reachable)"; fail++; + } else - { result() << "UNKNOWN"; unknown++; } - result() << eom; + { + result() << "UNKNOWN"; unknown++; + } + result() << eom; } status() << '\n'; } + status() << "SUMMARY: " << pass << " pass, " << fail << " fail if reachable, " << unknown << " unknown\n"; } @@ -229,7 +240,8 @@ void static_analyzert::xml_report() x.set_attribute("file", id2string(i_it->source_location.get_file())); x.set_attribute("line", id2string(i_it->source_location.get_line())); x.set_attribute( - "description", id2string(i_it->source_location.get_comment())); + "description", + id2string(i_it->source_location.get_comment())); } } @@ -259,11 +271,11 @@ bool static_analyzer( if(options.get_bool_option("flow-sensitive")) { if(options.get_bool_option("constants")) - return static_analyzert > + return static_analyzert> (goto_model, options, message_handler, out)(); else if(options.get_bool_option("intervals")) - return static_analyzert > + return static_analyzert> (goto_model, options, message_handler, out)(); // else if(options.get_bool_option("non-null")) diff --git a/src/goto-analyzer/static_show_domain.cpp b/src/goto-analyzer/static_show_domain.cpp index 7ad61565a40..8d24c522eb6 100644 --- a/src/goto-analyzer/static_show_domain.cpp +++ b/src/goto-analyzer/static_show_domain.cpp @@ -43,27 +43,21 @@ bool static_show_domain( 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(); - - //else if(options.get_bool_option("non-null")) - // domain = new ait(); - + domain=new ait(); else if(options.get_bool_option("dependence-graph")) - domain = new dependence_grapht(ns); - + domain=new dependence_grapht(ns); } 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(); + domain=new concurrency_aware_ait(); else if(options.get_bool_option("intervals")) - domain=new concurrency_aware_ait(); + domain=new concurrency_aware_ait(); // else if(options.get_bool_option("non-null")) // domain=new concurrency_aware_ait(); @@ -86,10 +80,11 @@ bool static_show_domain( 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")) + else if(options.get_bool_option("dot") && + options.get_bool_option("dependence-graph")) { - dependence_grapht *d = dynamic_cast(domain); - assert(d != NULL); + dependence_grapht *d=dynamic_cast(domain); + assert(d!=NULL); out << "digraph g {\n"; d->output_dot(out); @@ -99,5 +94,6 @@ bool static_show_domain( domain->output(goto_model, out); delete domain; + return false; } diff --git a/src/goto-analyzer/static_simplifier.cpp b/src/goto-analyzer/static_simplifier.cpp index 66797d1f11f..ce5bd8c511d 100644 --- a/src/goto-analyzer/static_simplifier.cpp +++ b/src/goto-analyzer/static_simplifier.cpp @@ -14,13 +14,12 @@ Author: Lucas Cordeiro, lucas.cordeiro@cs.ox.ac.uk #include -#include - #include #include #include #include +#include #include "static_simplifier.h" @@ -64,7 +63,8 @@ Function: static_simplifiert::operator() Outputs: false on success, true on failure. - Purpose: Run the analysis, check the assertions and report in the correct format. + Purpose: Run the analysis, check the assertions and report in the + correct format. \*******************************************************************/ @@ -78,7 +78,7 @@ bool static_simplifiert::operator()(void) simplify_program(); // Remove obviously unreachable things and (now) unconditional branches - if (options.get_bool_option("simplify-slicing")) + if(options.get_bool_option("simplify-slicing")) { status() << "Removing unreachable instructions" << eom; @@ -105,7 +105,8 @@ Function: static_simplifiert::simplify_guard Outputs: 1 if simplified, 0 if not. - Purpose: Simplifies the instruction's guard using the information in the abstract domain. + Purpose: Simplifies the instruction's guard using the information in + the abstract domain. \*******************************************************************/ @@ -114,7 +115,7 @@ 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; + unsigned return_value=(simplified==i_it->guard)?0:1; i_it->guard=simplified; return return_value; } @@ -127,7 +128,8 @@ Function: static_simplifiert::simplify_program Outputs: None. - Purpose: Simplifies the program using the information in the abstract domain. + Purpose: Simplifies the program using the information in the abstract + domain. \*******************************************************************/ @@ -173,17 +175,18 @@ void static_simplifiert::simplify_program() 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. + 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; + simp_rhs==assign.rhs())?0:1; + simplified.assigns+=result; unmodified.assigns+=(1-result); @@ -222,7 +225,6 @@ void static_simplifiert::simplify_program() // Make sure the references are correct. goto_functions.update(); - status() << "SIMPLIFIED: " << " assert: " << simplified.asserts << ", assume: " << simplified.assumes @@ -241,15 +243,12 @@ void static_simplifiert::simplify_program() return; } - - - /*******************************************************************\ Function: static_simplifier - Inputs: The goto_model to analyze and simplify, options giving the domain, - the message handler and output stream. + 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. @@ -266,11 +265,11 @@ bool static_simplifier( if(options.get_bool_option("flow-sensitive")) { if(options.get_bool_option("constants")) - return static_simplifiert > + return static_simplifiert> (goto_model, options, message_handler, out)(); else if(options.get_bool_option("intervals")) - return static_simplifiert > + return static_simplifiert> (goto_model, options, message_handler, out)(); // else if(options.get_bool_option("non-null")) @@ -282,8 +281,9 @@ bool static_simplifier( // 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)(); + return static_simplifiert< + concurrency_aware_ait> + (goto_model, options, message_handler, out)(); else if(options.get_bool_option("intervals")) return static_simplifiert > @@ -298,5 +298,6 @@ bool static_simplifier( messaget m(message_handler); m.status() << "Task / Interpreter / Domain combination not supported" << messaget::eom; + return true; } From a2209290ac29dc4a295ea0e66be760ee2eb04387 Mon Sep 17 00:00:00 2001 From: Daniel Poetzl Date: Wed, 25 Jan 2017 20:47:53 +0000 Subject: [PATCH 11/24] Fix constant propagator Four additional regression tests are not expected to work at present which are now marked as FUTURE. --- .../constant_propagation_10.c | 2 +- src/analyses/constant_propagator.cpp | 563 +++++++++--------- src/analyses/constant_propagator.h | 124 ++-- src/analyses/interval_domain.cpp | 4 +- src/analyses/replace_symbol_ext.cpp | 20 +- .../goto_analyzer_parse_options.cpp | 8 +- src/goto-analyzer/static_analyzer.cpp | 9 +- src/goto-analyzer/static_show_domain.cpp | 2 +- 8 files changed, 378 insertions(+), 354 deletions(-) diff --git a/regression/goto-analyzer/constant_propagation_10/constant_propagation_10.c b/regression/goto-analyzer/constant_propagation_10/constant_propagation_10.c index 169f7965b9d..f0dea39a424 100644 --- a/regression/goto-analyzer/constant_propagation_10/constant_propagation_10.c +++ b/regression/goto-analyzer/constant_propagation_10/constant_propagation_10.c @@ -4,7 +4,7 @@ int main() signed int i; signed int j; i = 0; - if(!(i >= 2)) + if(!(i >= 2)) { j = j + 1; i = i + 1; diff --git a/src/analyses/constant_propagator.cpp b/src/analyses/constant_propagator.cpp index bd2b4dab22a..325e6f30589 100644 --- a/src/analyses/constant_propagator.cpp +++ b/src/analyses/constant_propagator.cpp @@ -18,61 +18,6 @@ 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: @@ -85,73 +30,23 @@ Function: constant_propagator_domaint::assign_rec void constant_propagator_domaint::assign_rec( valuest &values, - const exprt &lhs, const exprt &rhs, + 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()); + if(lhs.id()!=ID_symbol) + return; -#ifdef DEBUG - std::cout << "assign: " << from_expr(ns, "", lhs) - << " := " << from_type(ns, "", rhs_type) << std::endl; -#endif + const symbol_exprt &s=to_symbol_expr(lhs); - 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); + exprt tmp=rhs; + values.replace_const(tmp); + tmp=simplify_expr(tmp, ns); - 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) - { - if(values.is_constant(rhs)) - assign(values, to_symbol_expr(lhs), rhs, ns); - 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 - { - } -#endif + if(tmp.is_constant()) + values.set_to(s, tmp); + else + values.set_to_top(s); } /*******************************************************************\ @@ -172,16 +67,24 @@ void constant_propagator_domaint::transform( ai_baset &ai, const namespacet &ns) { - #ifdef DEBUG +#ifdef DEBUG + std::cout << "Transform from/to:\n"; std::cout << from->location_number << " --> " << to->location_number << '\n'; - #endif +#endif #ifdef DEBUG - std::cout << "before:\n"; + std::cout << "Before:\n"; output(std::cout, ai, ns); #endif + const constant_propagator_ait *cp= + dynamic_cast(&ai); + bool have_dirty=cp!=NULL; + + if(values.is_bottom) + return; + if(from->is_decl()) { const code_declt &code_decl=to_code_decl(from->code); @@ -191,8 +94,8 @@ void constant_propagator_domaint::transform( else if(from->is_assign()) { const code_assignt &assignment=to_code_assign(from->code); - const exprt &lhs = assignment.lhs(); - const exprt &rhs = assignment.rhs(); + const exprt &lhs=assignment.lhs(); + const exprt &rhs=assignment.rhs(); assign_rec(values, lhs, rhs, ns); } else if(from->is_assume()) @@ -204,19 +107,15 @@ void constant_propagator_domaint::transform( exprt g; if(from->get_target()==to) - g = simplify_expr(from->guard, ns); + g=simplify_expr(from->guard, ns); else - g = simplify_expr(not_exprt(from->guard), ns); + g=simplify_expr(not_exprt(from->guard), ns); - if (g.is_false()) + 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); + two_way_propagate_rec(g, ns); } } else if(from->is_dead()) @@ -226,35 +125,102 @@ void constant_propagator_domaint::transform( } else if(from->is_function_call()) { - const exprt &function=to_code_function_call(from->code).function(); + const code_function_callt &function_call=to_code_function_call(from->code); + const exprt &function=function_call.function(); + + locationt next=from; + next++; if(function.id()==ID_symbol) { - const irep_idt &identifier=to_symbol_expr(function).get_identifier(); - - if(identifier=="__CPROVER_set_must" || - identifier=="__CPROVER_get_must" || - identifier=="__CPROVER_set_may" || - identifier=="__CPROVER_get_may" || - identifier=="__CPROVER_cleanup" || - identifier=="__CPROVER_clear_may" || - identifier=="__CPROVER_clear_must") + // called function identifier + const symbol_exprt &symbol_expr=to_symbol_expr(function); + const irep_idt id=symbol_expr.get_identifier(); + + if(to==next) { + if(id=="__CPROVER_set_must" || + id=="__CPROVER_get_must" || + id=="__CPROVER_set_may" || + id=="__CPROVER_get_may" || + id=="__CPROVER_cleanup" || + id=="__CPROVER_clear_may" || + id=="__CPROVER_clear_must") + { + // no effect on constants + } + else + { + if(have_dirty) + values.set_dirty_to_top(cp->dirty, ns); + else + values.set_to_top(); + } } else - values.set_to_top(); + { + // we have an actual call + + // parameters of called function + const symbolt &symbol=ns.lookup(id); + const code_typet &code_type=to_code_type(symbol.type); + const code_typet::parameterst ¶meters=code_type.parameters(); + + const code_function_callt::argumentst &arguments + =function_call.arguments(); + + unsigned n=std::min(arguments.size(), parameters.size()); + + for(unsigned i=0; idirty, ns); + else + values.set_to_top(); + } + } + else if(from->is_end_function()) + { + // erase parameters + + const irep_idt id=from->function; + const symbolt &symbol=ns.lookup(id); + + const code_typet &type=to_code_type(symbol.type); + + typedef code_typet::parameterst parameterst; + const parameterst ¶meters=type.parameters(); + + for(parameterst::const_iterator it=parameters.begin(); + it!=parameters.end(); it++) + { + // normal parameter + const irep_idt par=it->get_identifier(); + + // this erases the parameter from the map + values.set_to_top(par); + } } #ifdef DEBUG - std::cout << "after:\n"; + std::cout << "After:\n"; output(std::cout, ai, ns); #endif } - /*******************************************************************\ Function: constant_propagator_domaint::two_way_propagate_rec @@ -274,7 +240,8 @@ bool constant_propagator_domaint::two_way_propagate_rec( #ifdef DEBUG std::cout << "two_way_propagate_rec: " << from_expr(ns, "", expr) << '\n'; #endif - bool change = false; + + bool change=false; if(expr.id()==ID_and) { @@ -291,44 +258,22 @@ bool constant_propagator_domaint::two_way_propagate_rec( } else if(expr.id()==ID_equal) { - const exprt &lhs = expr.op0(); - const exprt &rhs = expr.op1(); + const exprt &lhs=expr.op0(); + const exprt &rhs=expr.op1(); // two-way propagation valuest copy_values = values; assign_rec(copy_values, lhs, rhs, ns); if(!values.is_constant(rhs) || values.is_constant(lhs)) - assign_rec(values, rhs, lhs, ns); + assign_rec(values, rhs, lhs, ns); change = values.meet(copy_values); } #ifdef DEBUG std::cout << "two_way_propagate_rec: " << change << '\n'; #endif - return change; -} - -/*******************************************************************\ - -Function: constant_propagator_domaint::assign - - Inputs: - Outputs: - - Purpose: - -\*******************************************************************/ - -void constant_propagator_domaint::assign( - valuest &dest, - const symbol_exprt &lhs, - exprt rhs, - const namespacet &ns) const -{ - values.replace_const(rhs); - rhs = simplify_expr(rhs, ns); - dest.set_to(lhs, rhs); + return change; } /*******************************************************************\ @@ -339,18 +284,23 @@ Function: constant_propagator_domaint::domain_simplify Outputs: The simplified condition. - Purpose: Simplify the condition given context-sensitive knowledge from the domain. + 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 +exprt constant_propagator_domaint::domain_simplify( + const exprt &condition, + const namespacet &ns, + const bool lhs) const { - if (lhs) { + if(lhs) + { // For now do not simplify the left hand sides of assignments return condition; - } else { + } + else + { exprt e(condition); values.replace_const(e); return simplify_expr(e, ns); @@ -359,30 +309,6 @@ exprt constant_propagator_domaint::domain_simplify (const exprt &condition, /*******************************************************************\ -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: @@ -404,12 +330,12 @@ bool constant_propagator_domaint::valuest::is_constant(const exprt &expr) const return false; if(expr.id()==ID_symbol) - if(replace_const.expr_map.find(to_symbol_expr(expr).get_identifier()) == + if(replace_const.expr_map.find(to_symbol_expr(expr).get_identifier())== replace_const.expr_map.end()) return false; - if (expr.id()==ID_index) - return is_array_constant(expr); + if(expr.id()==ID_index) + return false; if(expr.id()==ID_address_of) return is_constant_address_of(to_address_of_expr(expr).object()); @@ -460,25 +386,57 @@ Function: constant_propagator_domaint::valuest::set_to_top Outputs: - Purpose: Do not call this when iterating over replace_const.expr_map! + Purpose: Do not call when iterating over replace_const.expr_map! \*******************************************************************/ bool constant_propagator_domaint::valuest::set_to_top(const irep_idt &id) { - bool result = false; - - replace_symbolt::expr_mapt::iterator r_it = - replace_const.expr_map.find(id); + replace_symbolt::expr_mapt::iterator r_it + =replace_const.expr_map.find(id); - if(r_it != replace_const.expr_map.end()) + if(r_it!=replace_const.expr_map.end()) { assert(!is_bottom); replace_const.expr_map.erase(r_it); - result = true; + return true; } - return result; + return false; +} + +/*******************************************************************\ + +Function: constant_propagator_domaint::valuest::set_dirty_to_top + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +void constant_propagator_domaint::valuest::set_dirty_to_top( + const dirtyt &dirty, + const namespacet &ns) +{ + typedef replace_symbol_extt::expr_mapt expr_mapt; + expr_mapt &expr_map=replace_const.expr_map; + + for(expr_mapt::iterator it=expr_map.begin(); + it!=expr_map.end();) + { + const irep_idt id=it->first; + + const symbolt &symbol=ns.lookup(id); + + if((!symbol.is_procedure_local() || dirty(id)) && + !symbol.type.get_bool(ID_C_constant)) + it=expr_map.erase(it); + else + it++; + } } /*******************************************************************\ @@ -500,11 +458,26 @@ void constant_propagator_domaint::valuest::output( out << "const map:\n"; if(is_bottom) + { out << " bottom\n"; + assert(replace_const.expr_map.empty()); + return; + } - for(const auto &replace_pair : replace_const.expr_map) - out << ' ' << replace_pair.first << "=" - << from_expr(ns, "", replace_pair.second) << '\n'; + assert(!is_bottom); + if(replace_const.expr_map.empty()) + { + out << "top\n"; + return; + } + + for(replace_symbolt::expr_mapt::const_iterator + it=replace_const.expr_map.begin(); + it!=replace_const.expr_map.end(); + ++it) + { + out << ' ' << it->first << "=" << from_expr(ns, "", it->second) << '\n'; + } } /*******************************************************************\ @@ -541,6 +514,10 @@ Function: constant_propagator_domaint::valuest::merge bool constant_propagator_domaint::valuest::merge(const valuest &src) { + // dummy + const symbol_tablet symbol_table; + const namespacet ns(symbol_table); + // nothing to do if(src.is_bottom) return false; @@ -548,38 +525,64 @@ bool constant_propagator_domaint::valuest::merge(const valuest &src) // just copy if(is_bottom) { - replace_const = src.replace_const; - is_bottom = src.is_bottom; + assert(!src.is_bottom); + replace_const=src.replace_const; // copy + is_bottom=false; return true; } - bool changed = false; + assert(!is_bottom && !src.is_bottom); - // set everything to top that is not in src - for(replace_symbolt::expr_mapt::const_iterator - it=replace_const.expr_map.begin(); - it!=replace_const.expr_map.end(); - ) // no it++ + bool changed=false; + + replace_symbol_extt::expr_mapt &expr_map=replace_const.expr_map; + const replace_symbol_extt::expr_mapt &src_expr_map=src.replace_const.expr_map; + + // handle top + if(src_expr_map.empty()) + { + // change if it was not top + changed=!expr_map.empty(); + + set_to_top(); + assert(expr_map.empty()); + assert(!is_bottom); + + return changed; + } + + // remove those that are + // - different in src + // - do not exist in src + for(replace_symbolt::expr_mapt::iterator it=expr_map.begin(); + it!=expr_map.end();) { - const replace_symbolt::expr_mapt::const_iterator - b_it=src.replace_const.expr_map.find(it->first); + const irep_idt id=it->first; + const exprt &expr=it->second; + + replace_symbolt::expr_mapt::const_iterator s_it; + s_it=src_expr_map.find(id); - if(b_it==src.replace_const.expr_map.end()) + if(s_it!=src_expr_map.end()) { - //cannot use set_to_top here - replace_const.expr_map.erase(it); - changed = true; - break; + // check value + const exprt &src_expr=s_it->second; + + if(expr!=src_expr) + { + it=expr_map.erase(it); + changed=true; + } + else + it++; } else { - const exprt previous=it->second; - replace_const.expr_map[b_it->first]=b_it->second; - if (it->second != previous) changed = true; - - it++; + it=expr_map.erase(it); + changed=true; } } + return changed; } @@ -602,24 +605,27 @@ bool constant_propagator_domaint::valuest::meet(const valuest &src) bool changed = false; - for(const auto &src_replace_pair : src.replace_const.expr_map) + for(replace_symbolt::expr_mapt::const_iterator + it=src.replace_const.expr_map.begin(); + it!=src.replace_const.expr_map.end(); + ++it) { - replace_symbolt::expr_mapt::iterator c_it= - replace_const.expr_map.find(src_replace_pair.first); + replace_symbolt::expr_mapt::iterator + c_it = replace_const.expr_map.find(it->first); if(c_it!=replace_const.expr_map.end()) { - if(c_it->second!=src_replace_pair.second) + if(c_it->second!=it->second) { set_to_bottom(); - changed=true; + changed = true; break; } } else { - set_to(src_replace_pair.first, src_replace_pair.second); - changed=true; + set_to(it->first, it->second); + changed = true; } } @@ -643,7 +649,31 @@ bool constant_propagator_domaint::merge( locationt from, locationt to) { - return values.merge(other.values); + const symbol_tablet symbol_table; + const namespacet ns(symbol_table); + +#if 0 + if(to->is_skip()) + { + std::cout << "This:\n"; + values.output(std::cout, ns); + std::cout << "Other:\n"; + other.values.output(std::cout, ns); + } +#endif + + bool b; + b=values.merge(other.values); + +#if 0 + if(to->is_skip()) + { + std::cout << "Merge result:\n"; + values.output(std::cout, ns); + } +#endif + + return b; } /*******************************************************************\ @@ -668,34 +698,6 @@ 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: @@ -712,9 +714,9 @@ void constant_propagator_ait::replace( { Forall_goto_program_instructions(it, goto_function.body) { - state_mapt::iterator s_it = state_map.find(it); + state_mapt::iterator s_it=state_map.find(it); - if(s_it == state_map.end()) + if(s_it==state_map.end()) continue; replace_types_rec(s_it->second.values.replace_const, it->code); @@ -722,16 +724,15 @@ 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); } else if(it->is_assign()) { - exprt &rhs = to_code_assign(it->code).rhs(); + 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=simplify_expr(rhs, ns); + if(rhs.id()==ID_constant) rhs.add_source_location()=it->code.op0().source_location(); } else if(it->is_function_call()) @@ -740,14 +741,14 @@ void constant_propagator_ait::replace( to_code_function_call(it->code).function()); simplify_expr(to_code_function_call(it->code).function(), ns); - exprt::operandst &args = + exprt::operandst &args= to_code_function_call(it->code).arguments(); - for(exprt::operandst::iterator o_it = args.begin(); - o_it != args.end(); ++o_it) + for(exprt::operandst::iterator o_it=args.begin(); + o_it!=args.end(); ++o_it) { s_it->second.values.replace_const(*o_it); - *o_it = simplify_expr(*o_it, ns); + *o_it=simplify_expr(*o_it, ns); } } else if(it->is_other()) diff --git a/src/analyses/constant_propagator.h b/src/analyses/constant_propagator.h index a48bcf0c8a8..3f2d6921160 100644 --- a/src/analyses/constant_propagator.h +++ b/src/analyses/constant_propagator.h @@ -9,90 +9,119 @@ Author: Peter Schrammel #ifndef CPROVER_ANALYSES_CONSTANT_PROPAGATOR_H #define CPROVER_ANALYSES_CONSTANT_PROPAGATOR_H +#include + #include "ai.h" +#include "dirty.h" #include "replace_symbol_ext.h" class constant_propagator_domaint:public ai_domain_baset { public: - void transform( - locationt, - locationt, - ai_baset &, - const namespacet &) final; - void output( - std::ostream &, - const ai_baset &, - const namespacet &) const final; - void make_top() final { values.set_to_top(); } - void make_bottom() final { values.set_to_bottom(); } - void make_entry() 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; + virtual void transform( + locationt from, + locationt to, + ai_baset &ai_base, + const namespacet &ns); + + virtual void output( + std::ostream &out, + const ai_baset &ai_base, + const namespacet &ns) const; + + bool merge( + const constant_propagator_domaint &other, + locationt from, + locationt to); + + virtual exprt domain_simplify( + const exprt &condition, + const namespacet &ns, + const bool lhs=false) const; + + virtual void make_bottom() + { + values.set_to_bottom(); + } + + virtual void make_top() + { + values.set_to_top(); + } + + virtual void make_entry() + { + make_top(); + } struct valuest { public: - valuest():is_bottom(true) { } + valuest():is_bottom(true) {} // maps variables to constants replace_symbol_extt replace_const; bool is_bottom; - void output(std::ostream &, const namespacet &) const; - bool merge(const valuest &src); bool meet(const valuest &src); - void set_to_bottom() + // set whole state + + inline void set_to_bottom() { replace_const.clear(); - is_bottom = true; + is_bottom=true; } - void set_to(const irep_idt &lhs_id, const exprt &rhs_val) + inline void set_to_top() { - replace_const.expr_map[lhs_id] = rhs_val; - is_bottom = false; + replace_const.clear(); + is_bottom=false; } - void set_to(const symbol_exprt &lhs, const exprt &rhs_val) + // set single identifier + + inline void set_to(const irep_idt &lhs, const exprt &rhs) { - set_to(lhs.get_identifier(), rhs_val); + replace_const.expr_map[lhs]=rhs; + is_bottom=false; } - 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); + inline void set_to(const symbol_exprt &lhs, const exprt &rhs) + { + set_to(lhs.get_identifier(), rhs); + } bool set_to_top(const symbol_exprt &expr) { return set_to_top(expr.get_identifier()); } - void set_to_top() + bool set_to_top(const irep_idt &id); + + void set_dirty_to_top(const dirtyt &dirty, const namespacet &ns); + + 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 is_empty() const { - replace_const.clear(); - is_bottom = false; + assert(replace_const.type_map.empty()); + return replace_const.expr_map.empty(); } + void output(std::ostream &out, const namespacet &ns) const; }; valuest values; -private: - void assign( - valuest &dest, - const symbol_exprt &lhs, - exprt rhs, - const namespacet &ns) const; - +protected: void assign_rec( valuest &values, - const exprt &lhs, - const exprt &rhs, + const exprt &lhs, const exprt &rhs, const namespacet &ns); bool two_way_propagate_rec( @@ -103,9 +132,14 @@ class constant_propagator_domaint:public ai_domain_baset class constant_propagator_ait:public ait { public: + explicit constant_propagator_ait(const goto_functionst &goto_functions) : + dirty(goto_functions) + { + } + constant_propagator_ait( goto_functionst &goto_functions, - const namespacet &ns) + const namespacet &ns) : dirty(goto_functions) { operator()(goto_functions, ns); replace(goto_functions, ns); @@ -113,18 +147,17 @@ class constant_propagator_ait:public ait constant_propagator_ait( goto_functionst::goto_functiont &goto_function, - const namespacet &ns) + const namespacet &ns) : dirty(goto_function) { operator()(goto_function, ns); replace(goto_function, ns); } + dirtyt dirty; + protected: friend class constant_propagator_domaint; - void replace_array_symbol( - exprt &expr); - void replace( goto_functionst::goto_functiont &, const namespacet &); @@ -136,7 +169,6 @@ class constant_propagator_ait:public ait void replace_types_rec( const replace_symbolt &replace_const, exprt &expr); - }; #endif // CPROVER_ANALYSES_CONSTANT_PROPAGATOR_H diff --git a/src/analyses/interval_domain.cpp b/src/analyses/interval_domain.cpp index 5a2a493283a..4965501d9d6 100644 --- a/src/analyses/interval_domain.cpp +++ b/src/analyses/interval_domain.cpp @@ -155,8 +155,8 @@ bool interval_domaint::join( for(int_mapt::iterator it=int_map.begin(); it!=int_map.end(); ) // no it++ { - //search for the variable that needs to be merged - //containers have different size and variable order + // 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()) { diff --git a/src/analyses/replace_symbol_ext.cpp b/src/analyses/replace_symbol_ext.cpp index 568ea45e090..11c7c163edb 100644 --- a/src/analyses/replace_symbol_ext.cpp +++ b/src/analyses/replace_symbol_ext.cpp @@ -25,7 +25,7 @@ Function: replace_symbol_extt::replace bool replace_symbol_extt::replace(exprt &dest) const { - bool result=true; + bool result=true; // nothing changed // first look at type @@ -38,20 +38,7 @@ bool replace_symbol_extt::replace(exprt &dest) const if(!have_to_replace(dest)) return result; - // do not replace object in address_of expressions - if(dest.id()==ID_address_of) - { - const exprt &object = to_address_of_expr(dest).object(); - if(object.id()==ID_symbol) - { - expr_mapt::const_iterator it= - expr_map.find(object.get(ID_identifier)); - - if(it!=expr_map.end()) - return false; - } - } - else if(dest.id()==ID_symbol) + if(dest.id()==ID_symbol) { expr_mapt::const_iterator it= expr_map.find(dest.get(ID_identifier)); @@ -77,7 +64,8 @@ bool replace_symbol_extt::replace(exprt &dest) const const irept &va_arg_type=dest.find(ID_C_va_arg_type); if(va_arg_type.is_not_nil() && - !replace_symbolt::replace(static_cast(dest.add(ID_C_va_arg_type)))) + !replace_symbolt::replace( + static_cast(dest.add(ID_C_va_arg_type)))) result=false; return result; diff --git a/src/goto-analyzer/goto_analyzer_parse_options.cpp b/src/goto-analyzer/goto_analyzer_parse_options.cpp index 318b0a65161..f77e74500e6 100644 --- a/src/goto-analyzer/goto_analyzer_parse_options.cpp +++ b/src/goto-analyzer/goto_analyzer_parse_options.cpp @@ -202,7 +202,7 @@ 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")) + else if(cmdline.isset("dot")) { options.set_option("dot", true); options.set_option("outfile", cmdline.get_value("dot")); @@ -267,10 +267,10 @@ 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); - else if (cmdline.isset("dependence-graph")) + else if(cmdline.isset("dependence-graph")) options.set_option("dependence-graph", true); - - if (!(options.get_bool_option("constants") || + + if(!(options.get_bool_option("constants") || options.get_bool_option("intervals") || options.get_bool_option("non-null") || options.get_bool_option("dependence-graph"))) diff --git a/src/goto-analyzer/static_analyzer.cpp b/src/goto-analyzer/static_analyzer.cpp index 0bf4a030970..0dec55a54de 100644 --- a/src/goto-analyzer/static_analyzer.cpp +++ b/src/goto-analyzer/static_analyzer.cpp @@ -287,8 +287,9 @@ bool static_analyzer( // 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)(); + return static_analyzert> + (goto_model, options, message_handler, out)(); else if(options.get_bool_option("intervals")) return static_analyzert > @@ -301,6 +302,8 @@ bool static_analyzer( } messaget m(message_handler); - m.status() << "Task / Interpreter / Domain combination not supported" << messaget::eom; + m.status() << "Task / Interpreter / Domain combination not supported" + << messaget::eom; + return true; } diff --git a/src/goto-analyzer/static_show_domain.cpp b/src/goto-analyzer/static_show_domain.cpp index 8d24c522eb6..412c45e2bc2 100644 --- a/src/goto-analyzer/static_show_domain.cpp +++ b/src/goto-analyzer/static_show_domain.cpp @@ -39,7 +39,7 @@ bool static_show_domain( { ai_baset *domain = NULL; namespacet ns(goto_model.symbol_table); - + if(options.get_bool_option("flow-sensitive")) { if(options.get_bool_option("constants")) From cfd909d7289543319461d082347eba9d082fcf0c Mon Sep 17 00:00:00 2001 From: Daniel Poetzl Date: Mon, 30 Jan 2017 18:29:21 +0000 Subject: [PATCH 12/24] disable two-way propagation for now --- src/analyses/constant_propagator.cpp | 14 +++++++++----- 1 file changed, 9 insertions(+), 5 deletions(-) diff --git a/src/analyses/constant_propagator.cpp b/src/analyses/constant_propagator.cpp index 325e6f30589..d8f342c52a8 100644 --- a/src/analyses/constant_propagator.cpp +++ b/src/analyses/constant_propagator.cpp @@ -82,8 +82,7 @@ void constant_propagator_domaint::transform( dynamic_cast(&ai); bool have_dirty=cp!=NULL; - if(values.is_bottom) - return; + assert(!values.is_bottom); if(from->is_decl()) { @@ -116,6 +115,7 @@ void constant_propagator_domaint::transform( else { two_way_propagate_rec(g, ns); + assert(!values.is_bottom); // for now } } else if(from->is_dead()) @@ -215,6 +215,8 @@ void constant_propagator_domaint::transform( } } + assert(from->is_goto() || !values.is_bottom); + #ifdef DEBUG std::cout << "After:\n"; output(std::cout, ai, ns); @@ -243,6 +245,7 @@ bool constant_propagator_domaint::two_way_propagate_rec( bool change=false; +#if 0 if(expr.id()==ID_and) { // need a fixed point here to get the most out of it @@ -252,7 +255,7 @@ bool constant_propagator_domaint::two_way_propagate_rec( forall_operands(it, expr) if(two_way_propagate_rec(*it, ns)) - change = true; + change=true; } while(change); } @@ -262,12 +265,13 @@ bool constant_propagator_domaint::two_way_propagate_rec( const exprt &rhs=expr.op1(); // two-way propagation - valuest copy_values = values; + valuest copy_values=values; assign_rec(copy_values, lhs, rhs, ns); if(!values.is_constant(rhs) || values.is_constant(lhs)) assign_rec(values, rhs, lhs, ns); - change = values.meet(copy_values); + change=values.meet(copy_values); } +#endif #ifdef DEBUG std::cout << "two_way_propagate_rec: " << change << '\n'; From 8ca0691e176f471d67fcbb3df820d186d772f13b Mon Sep 17 00:00:00 2001 From: Daniel Poetzl Date: Fri, 3 Feb 2017 12:33:14 +0000 Subject: [PATCH 13/24] regression test changes --- regression/Makefile | 8 ++ .../{constant_propagation1.c => main.c} | 0 .../constant_propagation_01/test.desc | 10 +-- .../{constant_propagation_02.c => main.c} | 0 .../constant_propagation_02/original | 3 - .../constant_propagation_02/simplified | 81 ------------------- .../constant_propagation_02/test.desc | 10 +-- .../{constant_propagation_03.c => main.c} | 0 .../constant_propagation_03/test.desc | 8 +- .../{constant_propagation_04.c => main.c} | 0 .../constant_propagation_04/test.desc | 8 +- .../{constant_propagation_05.c => main.c} | 0 .../constant_propagation_05/test.desc | 4 +- .../main.c} | 0 .../constant_propagation_06/test.desc | 15 +--- .../main.c} | 0 .../constant_propagation_07/test.desc | 7 +- .../main.c} | 0 .../constant_propagation_08/test.desc | 9 +-- .../main.c} | 0 .../constant_propagation_09/test.desc | 8 +- .../main.c} | 0 .../constant_propagation_10/test.desc | 7 +- .../main.c} | 0 .../constant_propagation_11/test.desc | 8 +- .../main.c} | 0 .../constant_propagation_12/test.desc | 8 +- .../main.c} | 0 .../constant_propagation_13/test.desc | 4 +- .../main.c} | 0 .../constant_propagation_14/test.desc | 8 +- .../main.c} | 0 .../constant_propagation_15/test.desc | 7 +- .../constant_propagation_16/test.desc | 8 -- .../constant_propagation_17/test.desc | 9 --- .../constant_propagation_18/test.desc | 8 -- regression/goto-analyzer/intervals1/test.desc | 15 ---- .../goto-analyzer/intervals10/test.desc | 12 --- .../goto-analyzer/intervals11/test.desc | 9 --- .../goto-analyzer/intervals12/test.desc | 9 --- regression/goto-analyzer/intervals2/test.desc | 8 -- regression/goto-analyzer/intervals3/test.desc | 8 -- regression/goto-analyzer/intervals4/test.desc | 8 -- regression/goto-analyzer/intervals5/test.desc | 8 -- regression/goto-analyzer/intervals6/test.desc | 8 -- regression/goto-analyzer/intervals7/test.desc | 8 -- regression/goto-analyzer/intervals8/test.desc | 8 -- regression/goto-analyzer/intervals9/test.desc | 8 -- .../intervals1.c => intervals_01/main.c} | 0 .../goto-analyzer/intervals_01/test.desc | 15 ++++ .../intervals2.c => intervals_02/main.c} | 2 - .../goto-analyzer/intervals_02/test.desc | 8 ++ .../intervals3.c => intervals_03/main.c} | 0 .../goto-analyzer/intervals_03/test.desc | 8 ++ .../intervals4.c => intervals_04/main.c} | 0 .../goto-analyzer/intervals_04/test.desc | 8 ++ .../intervals5.c => intervals_05/main.c} | 0 .../goto-analyzer/intervals_05/test.desc | 8 ++ .../intervals6.c => intervals_06/main.c} | 0 .../goto-analyzer/intervals_06/test.desc | 8 ++ .../intervals7.c => intervals_07/main.c} | 0 .../goto-analyzer/intervals_07/test.desc | 8 ++ .../intervals8.c => intervals_08/main.c} | 0 .../goto-analyzer/intervals_08/test.desc | 8 ++ .../intervals9.c => intervals_09/main.c} | 0 .../goto-analyzer/intervals_09/test.desc | 8 ++ .../intervals10.c => intervals_10/main.c} | 0 .../goto-analyzer/intervals_10/test.desc | 12 +++ .../intervals11.c => intervals_11/main.c} | 0 .../goto-analyzer/intervals_11/test.desc | 9 +++ .../intervals12.c => intervals_12/main.c} | 0 .../goto-analyzer/intervals_12/test.desc | 9 +++ .../main.c} | 0 .../goto-analyzer/intervals_13/test.desc | 15 ++++ .../main.c} | 0 .../goto-analyzer/intervals_14/test.desc | 10 +++ .../main.c} | 0 .../goto-analyzer/intervals_15/test.desc | 8 ++ regression/goto-instrument-wmm-core/Makefile | 1 + 79 files changed, 207 insertions(+), 285 deletions(-) rename regression/goto-analyzer/constant_propagation_01/{constant_propagation1.c => main.c} (100%) rename regression/goto-analyzer/constant_propagation_02/{constant_propagation_02.c => main.c} (100%) delete mode 100644 regression/goto-analyzer/constant_propagation_02/original delete mode 100644 regression/goto-analyzer/constant_propagation_02/simplified rename regression/goto-analyzer/constant_propagation_03/{constant_propagation_03.c => main.c} (100%) rename regression/goto-analyzer/constant_propagation_04/{constant_propagation_04.c => main.c} (100%) rename regression/goto-analyzer/constant_propagation_05/{constant_propagation_05.c => main.c} (100%) rename regression/goto-analyzer/{constant_propagation_07/constant_propagation_07.c => constant_propagation_06/main.c} (100%) rename regression/goto-analyzer/{constant_propagation_10/constant_propagation_10.c => constant_propagation_07/main.c} (100%) rename regression/goto-analyzer/{constant_propagation_11/constant_propagation_11.c => constant_propagation_08/main.c} (100%) rename regression/goto-analyzer/{constant_propagation_12/constant_propagation_12.c => constant_propagation_09/main.c} (100%) rename regression/goto-analyzer/{constant_propagation_13/constant_propagation_13.c => constant_propagation_10/main.c} (100%) rename regression/goto-analyzer/{constant_propagation_14/constant_propagation_14.c => constant_propagation_11/main.c} (100%) rename regression/goto-analyzer/{constant_propagation_15/constant_propagation_15.c => constant_propagation_12/main.c} (100%) rename regression/goto-analyzer/{constant_propagation_16/constant_propagation_16.c => constant_propagation_13/main.c} (100%) rename regression/goto-analyzer/{constant_propagation_17/constant_propagation_17.c => constant_propagation_14/main.c} (100%) rename regression/goto-analyzer/{constant_propagation_18/constant_propagation_18.c => constant_propagation_15/main.c} (100%) delete mode 100644 regression/goto-analyzer/constant_propagation_16/test.desc delete mode 100644 regression/goto-analyzer/constant_propagation_17/test.desc delete mode 100644 regression/goto-analyzer/constant_propagation_18/test.desc delete mode 100644 regression/goto-analyzer/intervals1/test.desc delete mode 100644 regression/goto-analyzer/intervals10/test.desc delete mode 100644 regression/goto-analyzer/intervals11/test.desc delete mode 100644 regression/goto-analyzer/intervals12/test.desc delete mode 100644 regression/goto-analyzer/intervals2/test.desc delete mode 100644 regression/goto-analyzer/intervals3/test.desc delete mode 100644 regression/goto-analyzer/intervals4/test.desc delete mode 100644 regression/goto-analyzer/intervals5/test.desc delete mode 100644 regression/goto-analyzer/intervals6/test.desc delete mode 100644 regression/goto-analyzer/intervals7/test.desc delete mode 100644 regression/goto-analyzer/intervals8/test.desc delete mode 100644 regression/goto-analyzer/intervals9/test.desc rename regression/goto-analyzer/{intervals1/intervals1.c => intervals_01/main.c} (100%) create mode 100644 regression/goto-analyzer/intervals_01/test.desc rename regression/goto-analyzer/{intervals2/intervals2.c => intervals_02/main.c} (80%) create mode 100644 regression/goto-analyzer/intervals_02/test.desc rename regression/goto-analyzer/{intervals3/intervals3.c => intervals_03/main.c} (100%) create mode 100644 regression/goto-analyzer/intervals_03/test.desc rename regression/goto-analyzer/{intervals4/intervals4.c => intervals_04/main.c} (100%) create mode 100644 regression/goto-analyzer/intervals_04/test.desc rename regression/goto-analyzer/{intervals5/intervals5.c => intervals_05/main.c} (100%) create mode 100644 regression/goto-analyzer/intervals_05/test.desc rename regression/goto-analyzer/{intervals6/intervals6.c => intervals_06/main.c} (100%) create mode 100644 regression/goto-analyzer/intervals_06/test.desc rename regression/goto-analyzer/{intervals7/intervals7.c => intervals_07/main.c} (100%) create mode 100644 regression/goto-analyzer/intervals_07/test.desc rename regression/goto-analyzer/{intervals8/intervals8.c => intervals_08/main.c} (100%) create mode 100644 regression/goto-analyzer/intervals_08/test.desc rename regression/goto-analyzer/{intervals9/intervals9.c => intervals_09/main.c} (100%) create mode 100644 regression/goto-analyzer/intervals_09/test.desc rename regression/goto-analyzer/{intervals10/intervals10.c => intervals_10/main.c} (100%) create mode 100644 regression/goto-analyzer/intervals_10/test.desc rename regression/goto-analyzer/{intervals11/intervals11.c => intervals_11/main.c} (100%) create mode 100644 regression/goto-analyzer/intervals_11/test.desc rename regression/goto-analyzer/{intervals12/intervals12.c => intervals_12/main.c} (100%) create mode 100644 regression/goto-analyzer/intervals_12/test.desc rename regression/goto-analyzer/{constant_propagation_06/constant_propagation_06.c => intervals_13/main.c} (100%) create mode 100644 regression/goto-analyzer/intervals_13/test.desc rename regression/goto-analyzer/{constant_propagation_08/constant_propagation_08.c => intervals_14/main.c} (100%) create mode 100644 regression/goto-analyzer/intervals_14/test.desc rename regression/goto-analyzer/{constant_propagation_09/constant_propagation_09.c => intervals_15/main.c} (100%) create mode 100644 regression/goto-analyzer/intervals_15/test.desc diff --git a/regression/Makefile b/regression/Makefile index 296f583cc5e..fef85ccc958 100644 --- a/regression/Makefile +++ b/regression/Makefile @@ -12,3 +12,11 @@ DIRS = ansi-c \ test: $(foreach var,$(DIRS), $(MAKE) -C $(var) test || exit 1;) + +clean: + @for dir in *; do \ + if [ -d "$$dir" ]; then \ + $(MAKE) -C "$$dir" clean; \ + fi; \ + done; + diff --git a/regression/goto-analyzer/constant_propagation_01/constant_propagation1.c b/regression/goto-analyzer/constant_propagation_01/main.c similarity index 100% rename from regression/goto-analyzer/constant_propagation_01/constant_propagation1.c rename to regression/goto-analyzer/constant_propagation_01/main.c diff --git a/regression/goto-analyzer/constant_propagation_01/test.desc b/regression/goto-analyzer/constant_propagation_01/test.desc index 1eb849c3c7a..f5aa9da5608 100644 --- a/regression/goto-analyzer/constant_propagation_01/test.desc +++ b/regression/goto-analyzer/constant_propagation_01/test.desc @@ -1,9 +1,9 @@ -FUTURE -constant_propagation1.c ---constants --simplify out.goto +CORE +main.c +--constants --simplify out.gb ^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$ +^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/main.c similarity index 100% rename from regression/goto-analyzer/constant_propagation_02/constant_propagation_02.c rename to regression/goto-analyzer/constant_propagation_02/main.c diff --git a/regression/goto-analyzer/constant_propagation_02/original b/regression/goto-analyzer/constant_propagation_02/original deleted file mode 100644 index 13a9e245c81..00000000000 --- a/regression/goto-analyzer/constant_propagation_02/original +++ /dev/null @@ -1,3 +0,0 @@ -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 deleted file mode 100644 index 6c722a607de..00000000000 --- a/regression/goto-analyzer/constant_propagation_02/simplified +++ /dev/null @@ -1,81 +0,0 @@ -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 index 20cc5fcf86e..a7074d70c31 100644 --- a/regression/goto-analyzer/constant_propagation_02/test.desc +++ b/regression/goto-analyzer/constant_propagation_02/test.desc @@ -1,9 +1,9 @@ -FUTURE -constant_propagation_02.c ---constants --simplify out.goto +CORE +main.c +--constants --simplify out.gb ^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$ +^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/main.c similarity index 100% rename from regression/goto-analyzer/constant_propagation_03/constant_propagation_03.c rename to regression/goto-analyzer/constant_propagation_03/main.c diff --git a/regression/goto-analyzer/constant_propagation_03/test.desc b/regression/goto-analyzer/constant_propagation_03/test.desc index 2225c1a666e..ffe6d41d638 100644 --- a/regression/goto-analyzer/constant_propagation_03/test.desc +++ b/regression/goto-analyzer/constant_propagation_03/test.desc @@ -1,9 +1,9 @@ FUTURE -constant_propagation_03.c ---constants --simplify out.goto +main.c +--constants --simplify out.gb ^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$ +^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/main.c similarity index 100% rename from regression/goto-analyzer/constant_propagation_04/constant_propagation_04.c rename to regression/goto-analyzer/constant_propagation_04/main.c diff --git a/regression/goto-analyzer/constant_propagation_04/test.desc b/regression/goto-analyzer/constant_propagation_04/test.desc index 2510b3f8a5e..ffe6d41d638 100644 --- a/regression/goto-analyzer/constant_propagation_04/test.desc +++ b/regression/goto-analyzer/constant_propagation_04/test.desc @@ -1,9 +1,9 @@ FUTURE -constant_propagation_04.c ---constants --simplify out.goto +main.c +--constants --simplify out.gb ^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$ +^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/main.c similarity index 100% rename from regression/goto-analyzer/constant_propagation_05/constant_propagation_05.c rename to regression/goto-analyzer/constant_propagation_05/main.c diff --git a/regression/goto-analyzer/constant_propagation_05/test.desc b/regression/goto-analyzer/constant_propagation_05/test.desc index ddb22cc3616..e53a7f39396 100644 --- a/regression/goto-analyzer/constant_propagation_05/test.desc +++ b/regression/goto-analyzer/constant_propagation_05/test.desc @@ -1,8 +1,8 @@ FUTURE -constant_propagation_05.c +main.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)$ +^\[main.assertion.1\] file main.c line 12 function main, assertion j!=3: FAILURE (if reachable)$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/constant_propagation_07/constant_propagation_07.c b/regression/goto-analyzer/constant_propagation_06/main.c similarity index 100% rename from regression/goto-analyzer/constant_propagation_07/constant_propagation_07.c rename to regression/goto-analyzer/constant_propagation_06/main.c diff --git a/regression/goto-analyzer/constant_propagation_06/test.desc b/regression/goto-analyzer/constant_propagation_06/test.desc index 2c2596fe092..48616565f04 100644 --- a/regression/goto-analyzer/constant_propagation_06/test.desc +++ b/regression/goto-analyzer/constant_propagation_06/test.desc @@ -1,15 +1,8 @@ -FUTURE -constant_propagation_06.c ---intervals --verify +CORE +main.c +--constants --verify ^EXIT=0$ ^SIGNAL=0$ -^\[main.assertion.1\] file constant_propagation_06.c line 8 function main, assertion i>=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$ +^\[main.assertion.1\] file main.c line 12 function main, assertion i<51: UNKNOWN$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/constant_propagation_10/constant_propagation_10.c b/regression/goto-analyzer/constant_propagation_07/main.c similarity index 100% rename from regression/goto-analyzer/constant_propagation_10/constant_propagation_10.c rename to regression/goto-analyzer/constant_propagation_07/main.c diff --git a/regression/goto-analyzer/constant_propagation_07/test.desc b/regression/goto-analyzer/constant_propagation_07/test.desc index 615893d4f78..c4b03cd8738 100644 --- a/regression/goto-analyzer/constant_propagation_07/test.desc +++ b/regression/goto-analyzer/constant_propagation_07/test.desc @@ -1,8 +1,9 @@ FUTURE -constant_propagation_07.c ---constants --verify +main.c +--constants --simplify out.gb ^EXIT=0$ ^SIGNAL=0$ -^\[main.assertion.1\] file constant_propagation_07.c line 12 function main, assertion i<51: UNKNOWN$ +^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_08/main.c similarity index 100% rename from regression/goto-analyzer/constant_propagation_11/constant_propagation_11.c rename to regression/goto-analyzer/constant_propagation_08/main.c diff --git a/regression/goto-analyzer/constant_propagation_08/test.desc b/regression/goto-analyzer/constant_propagation_08/test.desc index 994c2c532df..07a97596c15 100644 --- a/regression/goto-analyzer/constant_propagation_08/test.desc +++ b/regression/goto-analyzer/constant_propagation_08/test.desc @@ -1,10 +1,9 @@ FUTURE -constant_propagation_08.c ---intervals --verify +main.c +--constants --simplify out.gb ^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$ +^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_09/main.c similarity index 100% rename from regression/goto-analyzer/constant_propagation_12/constant_propagation_12.c rename to regression/goto-analyzer/constant_propagation_09/main.c diff --git a/regression/goto-analyzer/constant_propagation_09/test.desc b/regression/goto-analyzer/constant_propagation_09/test.desc index 6a1b75f0c1b..eebfe27dd49 100644 --- a/regression/goto-analyzer/constant_propagation_09/test.desc +++ b/regression/goto-analyzer/constant_propagation_09/test.desc @@ -1,9 +1,9 @@ FUTURE -constant_propagation_09.c ---intervals --verify +main.c +--constants --simplify out.gb ^EXIT=0$ ^SIGNAL=0$ -******** Function main -^\[main.assertion.1\] file constant_propagation_09.c line 12 function main, assertion j<52: UNKNOWN$ +^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_10/main.c similarity index 100% rename from regression/goto-analyzer/constant_propagation_13/constant_propagation_13.c rename to regression/goto-analyzer/constant_propagation_10/main.c diff --git a/regression/goto-analyzer/constant_propagation_10/test.desc b/regression/goto-analyzer/constant_propagation_10/test.desc index 52d98cb611b..9662c38cf04 100644 --- a/regression/goto-analyzer/constant_propagation_10/test.desc +++ b/regression/goto-analyzer/constant_propagation_10/test.desc @@ -1,9 +1,8 @@ FUTURE -constant_propagation_10.c ---constants --simplify out.goto +main.c +--constants --verify ^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$ +^\[main.assertion.1\] file main.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_11/main.c similarity index 100% rename from regression/goto-analyzer/constant_propagation_14/constant_propagation_14.c rename to regression/goto-analyzer/constant_propagation_11/main.c diff --git a/regression/goto-analyzer/constant_propagation_11/test.desc b/regression/goto-analyzer/constant_propagation_11/test.desc index 7c849326cf6..4e9c8715429 100644 --- a/regression/goto-analyzer/constant_propagation_11/test.desc +++ b/regression/goto-analyzer/constant_propagation_11/test.desc @@ -1,9 +1,9 @@ FUTURE -constant_propagation_11.c ---constants --simplify out.goto +main.c +--constants --simplify out.gb ^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$ +^Simplified: assert: 1, assume: 0, goto: 0$ +^Unmodified: 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_12/main.c similarity index 100% rename from regression/goto-analyzer/constant_propagation_15/constant_propagation_15.c rename to regression/goto-analyzer/constant_propagation_12/main.c diff --git a/regression/goto-analyzer/constant_propagation_12/test.desc b/regression/goto-analyzer/constant_propagation_12/test.desc index ca5803363ad..208b235ccd5 100644 --- a/regression/goto-analyzer/constant_propagation_12/test.desc +++ b/regression/goto-analyzer/constant_propagation_12/test.desc @@ -1,9 +1,9 @@ FUTURE -constant_propagation_12.c ---constants --simplify out.goto +main.c +--constants --simplify out.gb ^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$ +^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_13/main.c similarity index 100% rename from regression/goto-analyzer/constant_propagation_16/constant_propagation_16.c rename to regression/goto-analyzer/constant_propagation_13/main.c diff --git a/regression/goto-analyzer/constant_propagation_13/test.desc b/regression/goto-analyzer/constant_propagation_13/test.desc index 22f10d125e3..66d18c7ab67 100644 --- a/regression/goto-analyzer/constant_propagation_13/test.desc +++ b/regression/goto-analyzer/constant_propagation_13/test.desc @@ -1,8 +1,8 @@ FUTURE -constant_propagation_13.c +main.c --constants --verify ^EXIT=0$ ^SIGNAL=0$ -^\[main.assertion.1\] file constant_propagation_13.c line 10 function main, assertion a\[0\]==2: FAILURE$ +^\[main.assertion.1\] file main.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_14/main.c similarity index 100% rename from regression/goto-analyzer/constant_propagation_17/constant_propagation_17.c rename to regression/goto-analyzer/constant_propagation_14/main.c diff --git a/regression/goto-analyzer/constant_propagation_14/test.desc b/regression/goto-analyzer/constant_propagation_14/test.desc index a39a1f66cda..5f104bfa09c 100644 --- a/regression/goto-analyzer/constant_propagation_14/test.desc +++ b/regression/goto-analyzer/constant_propagation_14/test.desc @@ -1,9 +1,9 @@ FUTURE -constant_propagation_14.c ---constants --simplify out.goto +main.c +--constants --verify ^EXIT=0$ ^SIGNAL=0$ -^SIMPLIFIED: assert: 1, assume: 0, goto: 0$ -^UNKNOWN: assert: 0, assume: 0, goto: 0$ +^\[main.assertion.1\] file main.c line 11 function main, assertion a\[0\]==1 || a\[0\]==2: SUCCESS$ +^\[main.assertion.2\] file main.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_15/main.c similarity index 100% rename from regression/goto-analyzer/constant_propagation_18/constant_propagation_18.c rename to regression/goto-analyzer/constant_propagation_15/main.c diff --git a/regression/goto-analyzer/constant_propagation_15/test.desc b/regression/goto-analyzer/constant_propagation_15/test.desc index 20d36183eb0..a1ce84cc89c 100644 --- a/regression/goto-analyzer/constant_propagation_15/test.desc +++ b/regression/goto-analyzer/constant_propagation_15/test.desc @@ -1,9 +1,8 @@ FUTURE -constant_propagation_15.c ---constants --simplify out.goto +main.c +--constants --verify ^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$ +^\[main.assertion.1\] file main.c line 9 function main, assertion a\[0\]==2: FAILURE$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/constant_propagation_16/test.desc b/regression/goto-analyzer/constant_propagation_16/test.desc deleted file mode 100644 index b56c871deb4..00000000000 --- a/regression/goto-analyzer/constant_propagation_16/test.desc +++ /dev/null @@ -1,8 +0,0 @@ -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/test.desc b/regression/goto-analyzer/constant_propagation_17/test.desc deleted file mode 100644 index acecb91eb0a..00000000000 --- a/regression/goto-analyzer/constant_propagation_17/test.desc +++ /dev/null @@ -1,9 +0,0 @@ -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/test.desc b/regression/goto-analyzer/constant_propagation_18/test.desc deleted file mode 100644 index 7ea74c4d264..00000000000 --- a/regression/goto-analyzer/constant_propagation_18/test.desc +++ /dev/null @@ -1,8 +0,0 @@ -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/test.desc b/regression/goto-analyzer/intervals1/test.desc deleted file mode 100644 index 5a9802eeb20..00000000000 --- a/regression/goto-analyzer/intervals1/test.desc +++ /dev/null @@ -1,15 +0,0 @@ -KNOWNBUG -intervals1.c ---intervals --verify -^EXIT=0$ -^SIGNAL=0$ -^\[main.assertion.1\] file intervals1.c line 8 function main, assertion i>=10: SUCCESS$ -^\[main.assertion.2\] file intervals1.c line 11 function main, assertion i!=30: SUCCESS$ -^\[main.assertion.3\] file intervals1.c line 14 function main, assertion i!=15: UNKNOWN$ -^\[main.assertion.4\] file intervals1.c line 17 function main, assertion 0: SUCCESS$ -^\[main.assertion.5\] file intervals1.c line 20 function main, assertion j>=10: SUCCESS$ -^\[main.assertion.6\] file intervals1.c line 23 function main, assertion i>=j: UNKNOWN$ -^\[main.assertion.7\] file intervals1.c line 26 function main, assertion i>=11: SUCCESS$ -^\[main.assertion.8\] file intervals1.c line 29 function main, assertion j<100: SUCCESS$ --- -^warning: ignoring diff --git a/regression/goto-analyzer/intervals10/test.desc b/regression/goto-analyzer/intervals10/test.desc deleted file mode 100644 index 794198505f1..00000000000 --- a/regression/goto-analyzer/intervals10/test.desc +++ /dev/null @@ -1,12 +0,0 @@ -FUTURE -intervals10.c ---intervals --verify -^EXIT=0$ -^SIGNAL=0$ -^\[main.assertion.1\] file intervals10.c line 8 function main, assertion j<=100: SUCCESS$ -^\[main.assertion.2\] file intervals10.c line 11 function main, assertion j<101: SUCCESS$ -^\[main.assertion.3\] file intervals10.c line 14 function main, assertion j>100: 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/test.desc b/regression/goto-analyzer/intervals11/test.desc deleted file mode 100644 index 039cbffbeb0..00000000000 --- a/regression/goto-analyzer/intervals11/test.desc +++ /dev/null @@ -1,9 +0,0 @@ -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/test.desc b/regression/goto-analyzer/intervals12/test.desc deleted file mode 100644 index 59a724c28b5..00000000000 --- a/regression/goto-analyzer/intervals12/test.desc +++ /dev/null @@ -1,9 +0,0 @@ -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/test.desc b/regression/goto-analyzer/intervals2/test.desc deleted file mode 100644 index 65aae030db1..00000000000 --- a/regression/goto-analyzer/intervals2/test.desc +++ /dev/null @@ -1,8 +0,0 @@ -KNOWNBUG -intervals2.c ---intervals --verify -^EXIT=0$ -^SIGNAL=0$ -^\[main.assertion.1\] file intervals2.c line 7 function main, assertion x > -10 && x < 100: SUCCESS$ --- -^warning: ignoring diff --git a/regression/goto-analyzer/intervals3/test.desc b/regression/goto-analyzer/intervals3/test.desc deleted file mode 100644 index 69ded2182ee..00000000000 --- a/regression/goto-analyzer/intervals3/test.desc +++ /dev/null @@ -1,8 +0,0 @@ -KNOWNBUG -intervals3.c ---intervals --verify -^EXIT=0$ -^SIGNAL=0$ -^\[main.assertion.1\] file intervals3.c line 7 function main, assertion x > -10 || x < 100: SUCCESS$ --- -^warning: ignoring diff --git a/regression/goto-analyzer/intervals4/test.desc b/regression/goto-analyzer/intervals4/test.desc deleted file mode 100644 index 2b725180e3f..00000000000 --- a/regression/goto-analyzer/intervals4/test.desc +++ /dev/null @@ -1,8 +0,0 @@ -KNOWNBUG -intervals4.c ---intervals --verify -^EXIT=0$ -^SIGNAL=0$ -^\[main.assertion.1\] file intervals4.c line 9 function main, assertion i >= 1 && i <= 2: SUCCESS$ --- -^warning: ignoring diff --git a/regression/goto-analyzer/intervals5/test.desc b/regression/goto-analyzer/intervals5/test.desc deleted file mode 100644 index eb64fbc13d1..00000000000 --- a/regression/goto-analyzer/intervals5/test.desc +++ /dev/null @@ -1,8 +0,0 @@ -KNOWNBUG -intervals5.c ---intervals --verify -^EXIT=0$ -^SIGNAL=0$ -^\[main.assertion.1\] file intervals5.c line 9 function main, assertion i >= 1 || i <= 2: SUCCESS$ --- -^warning: ignoring diff --git a/regression/goto-analyzer/intervals6/test.desc b/regression/goto-analyzer/intervals6/test.desc deleted file mode 100644 index 6e36b7948d2..00000000000 --- a/regression/goto-analyzer/intervals6/test.desc +++ /dev/null @@ -1,8 +0,0 @@ -FUTURE -intervals6.c ---intervals --verify -^EXIT=0$ -^SIGNAL=0$ -^\[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 deleted file mode 100644 index 6a42b4a30ec..00000000000 --- a/regression/goto-analyzer/intervals7/test.desc +++ /dev/null @@ -1,8 +0,0 @@ -FUTURE -intervals7.c ---intervals --verify -^EXIT=0$ -^SIGNAL=0$ -^\[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/test.desc b/regression/goto-analyzer/intervals8/test.desc deleted file mode 100644 index 7500059a717..00000000000 --- a/regression/goto-analyzer/intervals8/test.desc +++ /dev/null @@ -1,8 +0,0 @@ -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/test.desc b/regression/goto-analyzer/intervals9/test.desc deleted file mode 100644 index 37c33b97288..00000000000 --- a/regression/goto-analyzer/intervals9/test.desc +++ /dev/null @@ -1,8 +0,0 @@ -KNOWNBUG -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 diff --git a/regression/goto-analyzer/intervals1/intervals1.c b/regression/goto-analyzer/intervals_01/main.c similarity index 100% rename from regression/goto-analyzer/intervals1/intervals1.c rename to regression/goto-analyzer/intervals_01/main.c diff --git a/regression/goto-analyzer/intervals_01/test.desc b/regression/goto-analyzer/intervals_01/test.desc new file mode 100644 index 00000000000..db689e5d1ad --- /dev/null +++ b/regression/goto-analyzer/intervals_01/test.desc @@ -0,0 +1,15 @@ +CORE +main.c +--intervals --verify +^EXIT=0$ +^SIGNAL=0$ +^\[main.assertion.1\] file main.c line 8 function main, assertion i>=10: SUCCESS$ +^\[main.assertion.2\] file main.c line 11 function main, assertion i!=30: SUCCESS$ +^\[main.assertion.3\] file main.c line 14 function main, assertion i!=15: UNKNOWN$ +^\[main.assertion.4\] file main.c line 17 function main, assertion 0: SUCCESS$ +^\[main.assertion.5\] file main.c line 20 function main, assertion j>=10: SUCCESS$ +^\[main.assertion.6\] file main.c line 23 function main, assertion i>=j: UNKNOWN$ +^\[main.assertion.7\] file main.c line 26 function main, assertion i>=11: SUCCESS$ +^\[main.assertion.8\] file main.c line 29 function main, assertion j<100: SUCCESS$ +-- +^warning: ignoring diff --git a/regression/goto-analyzer/intervals2/intervals2.c b/regression/goto-analyzer/intervals_02/main.c similarity index 80% rename from regression/goto-analyzer/intervals2/intervals2.c rename to regression/goto-analyzer/intervals_02/main.c index d542854bb6a..755d36df82c 100644 --- a/regression/goto-analyzer/intervals2/intervals2.c +++ b/regression/goto-analyzer/intervals_02/main.c @@ -3,9 +3,7 @@ int main(){ int x; if (x > 0 && x < 20) { - //if (x < 20) { assert(x > -10 && x < 100); - //} } return 0; } diff --git a/regression/goto-analyzer/intervals_02/test.desc b/regression/goto-analyzer/intervals_02/test.desc new file mode 100644 index 00000000000..9dfc850cf6b --- /dev/null +++ b/regression/goto-analyzer/intervals_02/test.desc @@ -0,0 +1,8 @@ +KNOWNBUG +main.c +--intervals --verify +^EXIT=0$ +^SIGNAL=0$ +^\[main.assertion.1\] file main.c line 7 function main, assertion x > -10 && x < 100: SUCCESS$ +-- +^warning: ignoring diff --git a/regression/goto-analyzer/intervals3/intervals3.c b/regression/goto-analyzer/intervals_03/main.c similarity index 100% rename from regression/goto-analyzer/intervals3/intervals3.c rename to regression/goto-analyzer/intervals_03/main.c diff --git a/regression/goto-analyzer/intervals_03/test.desc b/regression/goto-analyzer/intervals_03/test.desc new file mode 100644 index 00000000000..f901ea41a56 --- /dev/null +++ b/regression/goto-analyzer/intervals_03/test.desc @@ -0,0 +1,8 @@ +CORE +main.c +--intervals --verify +^EXIT=0$ +^SIGNAL=0$ +^\[main.assertion.1\] file main.c line 7 function main, assertion x > -10 || x < 100: SUCCESS$ +-- +^warning: ignoring diff --git a/regression/goto-analyzer/intervals4/intervals4.c b/regression/goto-analyzer/intervals_04/main.c similarity index 100% rename from regression/goto-analyzer/intervals4/intervals4.c rename to regression/goto-analyzer/intervals_04/main.c diff --git a/regression/goto-analyzer/intervals_04/test.desc b/regression/goto-analyzer/intervals_04/test.desc new file mode 100644 index 00000000000..91550585968 --- /dev/null +++ b/regression/goto-analyzer/intervals_04/test.desc @@ -0,0 +1,8 @@ +KNOWNBUG +main.c +--intervals --verify +^EXIT=0$ +^SIGNAL=0$ +^\[main.assertion.1\] file main.c line 9 function main, assertion i >= 1 && i <= 2: SUCCESS$ +-- +^warning: ignoring diff --git a/regression/goto-analyzer/intervals5/intervals5.c b/regression/goto-analyzer/intervals_05/main.c similarity index 100% rename from regression/goto-analyzer/intervals5/intervals5.c rename to regression/goto-analyzer/intervals_05/main.c diff --git a/regression/goto-analyzer/intervals_05/test.desc b/regression/goto-analyzer/intervals_05/test.desc new file mode 100644 index 00000000000..3c4e162000b --- /dev/null +++ b/regression/goto-analyzer/intervals_05/test.desc @@ -0,0 +1,8 @@ +CORE +main.c +--intervals --verify +^EXIT=0$ +^SIGNAL=0$ +^\[main.assertion.1\] file main.c line 9 function main, assertion i >= 1 || i <= 2: SUCCESS$ +-- +^warning: ignoring diff --git a/regression/goto-analyzer/intervals6/intervals6.c b/regression/goto-analyzer/intervals_06/main.c similarity index 100% rename from regression/goto-analyzer/intervals6/intervals6.c rename to regression/goto-analyzer/intervals_06/main.c diff --git a/regression/goto-analyzer/intervals_06/test.desc b/regression/goto-analyzer/intervals_06/test.desc new file mode 100644 index 00000000000..facd3285898 --- /dev/null +++ b/regression/goto-analyzer/intervals_06/test.desc @@ -0,0 +1,8 @@ +FUTURE +main.c +--intervals --verify +^EXIT=0$ +^SIGNAL=0$ +^\[main.assertion.1\] file main.c line 7 function main, assertion x < -10 || x > 100: FAILURE (if reachable)$ +-- +^warning: ignoring diff --git a/regression/goto-analyzer/intervals7/intervals7.c b/regression/goto-analyzer/intervals_07/main.c similarity index 100% rename from regression/goto-analyzer/intervals7/intervals7.c rename to regression/goto-analyzer/intervals_07/main.c diff --git a/regression/goto-analyzer/intervals_07/test.desc b/regression/goto-analyzer/intervals_07/test.desc new file mode 100644 index 00000000000..557063f4e33 --- /dev/null +++ b/regression/goto-analyzer/intervals_07/test.desc @@ -0,0 +1,8 @@ +FUTURE +main.c +--intervals --verify +^EXIT=0$ +^SIGNAL=0$ +^\[main.assertion.1\] file main.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/intervals_08/main.c similarity index 100% rename from regression/goto-analyzer/intervals8/intervals8.c rename to regression/goto-analyzer/intervals_08/main.c diff --git a/regression/goto-analyzer/intervals_08/test.desc b/regression/goto-analyzer/intervals_08/test.desc new file mode 100644 index 00000000000..4cf9f8f7def --- /dev/null +++ b/regression/goto-analyzer/intervals_08/test.desc @@ -0,0 +1,8 @@ +FUTURE +main.c +--intervals --verify +^EXIT=0$ +^SIGNAL=0$ +^\[main.assertion.1\] file main.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/intervals_09/main.c similarity index 100% rename from regression/goto-analyzer/intervals9/intervals9.c rename to regression/goto-analyzer/intervals_09/main.c diff --git a/regression/goto-analyzer/intervals_09/test.desc b/regression/goto-analyzer/intervals_09/test.desc new file mode 100644 index 00000000000..1ea84fe57dc --- /dev/null +++ b/regression/goto-analyzer/intervals_09/test.desc @@ -0,0 +1,8 @@ +CORE +main.c +--intervals --verify +^EXIT=0$ +^SIGNAL=0$ +^\[main.assertion.1\] file main.c line 9 function main, assertion i>=1 && i<=2: SUCCESS$ +-- +^warning: ignoring diff --git a/regression/goto-analyzer/intervals10/intervals10.c b/regression/goto-analyzer/intervals_10/main.c similarity index 100% rename from regression/goto-analyzer/intervals10/intervals10.c rename to regression/goto-analyzer/intervals_10/main.c diff --git a/regression/goto-analyzer/intervals_10/test.desc b/regression/goto-analyzer/intervals_10/test.desc new file mode 100644 index 00000000000..239032bf55f --- /dev/null +++ b/regression/goto-analyzer/intervals_10/test.desc @@ -0,0 +1,12 @@ +FUTURE +main.c +--intervals --verify +^EXIT=0$ +^SIGNAL=0$ +^\[main.assertion.1\] file main.c line 8 function main, assertion j<=100: SUCCESS$ +^\[main.assertion.2\] file main.c line 11 function main, assertion j<101: SUCCESS$ +^\[main.assertion.3\] file main.c line 14 function main, assertion j>100: FAILURE (if reachable)$ +^\[main.assertion.4\] file main.c line 17 function main, assertion j<99: UNKNOWN$ +^\[main.assertion.5\] file main.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/intervals_11/main.c similarity index 100% rename from regression/goto-analyzer/intervals11/intervals11.c rename to regression/goto-analyzer/intervals_11/main.c diff --git a/regression/goto-analyzer/intervals_11/test.desc b/regression/goto-analyzer/intervals_11/test.desc new file mode 100644 index 00000000000..691bd1c1314 --- /dev/null +++ b/regression/goto-analyzer/intervals_11/test.desc @@ -0,0 +1,9 @@ +FUTURE +main.c +--intervals --verify +^EXIT=0$ +^SIGNAL=0$ +^\[main.assertion.1\] file main.c line 30 function main, assertion y\[i\]>=-1.0f && y\[i\]<=1.0f: UNKNOWN$ +^\[main.assertion.2\] file main.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/intervals_12/main.c similarity index 100% rename from regression/goto-analyzer/intervals12/intervals12.c rename to regression/goto-analyzer/intervals_12/main.c diff --git a/regression/goto-analyzer/intervals_12/test.desc b/regression/goto-analyzer/intervals_12/test.desc new file mode 100644 index 00000000000..bdb98e27d7e --- /dev/null +++ b/regression/goto-analyzer/intervals_12/test.desc @@ -0,0 +1,9 @@ +FUTURE +main.c +--intervals --verify +^EXIT=0$ +^SIGNAL=0$ +^[main.assertion.1] file main.c line 8 function main, assertion j < 0: SUCCESS$ +^[main.assertion.2] file main.c line 11 function main, assertion j < 0: SUCCESS$ +-- +^warning: ignoring diff --git a/regression/goto-analyzer/constant_propagation_06/constant_propagation_06.c b/regression/goto-analyzer/intervals_13/main.c similarity index 100% rename from regression/goto-analyzer/constant_propagation_06/constant_propagation_06.c rename to regression/goto-analyzer/intervals_13/main.c diff --git a/regression/goto-analyzer/intervals_13/test.desc b/regression/goto-analyzer/intervals_13/test.desc new file mode 100644 index 00000000000..db689e5d1ad --- /dev/null +++ b/regression/goto-analyzer/intervals_13/test.desc @@ -0,0 +1,15 @@ +CORE +main.c +--intervals --verify +^EXIT=0$ +^SIGNAL=0$ +^\[main.assertion.1\] file main.c line 8 function main, assertion i>=10: SUCCESS$ +^\[main.assertion.2\] file main.c line 11 function main, assertion i!=30: SUCCESS$ +^\[main.assertion.3\] file main.c line 14 function main, assertion i!=15: UNKNOWN$ +^\[main.assertion.4\] file main.c line 17 function main, assertion 0: SUCCESS$ +^\[main.assertion.5\] file main.c line 20 function main, assertion j>=10: SUCCESS$ +^\[main.assertion.6\] file main.c line 23 function main, assertion i>=j: UNKNOWN$ +^\[main.assertion.7\] file main.c line 26 function main, assertion i>=11: SUCCESS$ +^\[main.assertion.8\] file main.c line 29 function main, assertion j<100: SUCCESS$ +-- +^warning: ignoring diff --git a/regression/goto-analyzer/constant_propagation_08/constant_propagation_08.c b/regression/goto-analyzer/intervals_14/main.c similarity index 100% rename from regression/goto-analyzer/constant_propagation_08/constant_propagation_08.c rename to regression/goto-analyzer/intervals_14/main.c diff --git a/regression/goto-analyzer/intervals_14/test.desc b/regression/goto-analyzer/intervals_14/test.desc new file mode 100644 index 00000000000..58b2daef2fe --- /dev/null +++ b/regression/goto-analyzer/intervals_14/test.desc @@ -0,0 +1,10 @@ +FUTURE +main.c +--intervals --verify +^EXIT=0$ +^SIGNAL=0$ +^\[main.assertion.1\] file main.c line 12 function main, assertion i<50: UNKNOWN$ +^\[main.assertion.2\] file main.c line 13 function main, assertion i<51: UNKNOWN$ +^\[main.assertion.3\] file main.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/intervals_15/main.c similarity index 100% rename from regression/goto-analyzer/constant_propagation_09/constant_propagation_09.c rename to regression/goto-analyzer/intervals_15/main.c diff --git a/regression/goto-analyzer/intervals_15/test.desc b/regression/goto-analyzer/intervals_15/test.desc new file mode 100644 index 00000000000..21eb7254c54 --- /dev/null +++ b/regression/goto-analyzer/intervals_15/test.desc @@ -0,0 +1,8 @@ +CORE +main.c +--intervals --verify +^EXIT=0$ +^SIGNAL=0$ +^\[main.assertion.1\] file main.c line 12 function main, assertion j<52: UNKNOWN$ +-- +^warning: ignoring diff --git a/regression/goto-instrument-wmm-core/Makefile b/regression/goto-instrument-wmm-core/Makefile index 85c17bf622b..6684274289d 100644 --- a/regression/goto-instrument-wmm-core/Makefile +++ b/regression/goto-instrument-wmm-core/Makefile @@ -31,3 +31,4 @@ show: vim -o "$$dir/*.c" "$$dir/*.out"; \ fi; \ done; + From f678bd8ae00e6a29e588c1acb1062b0edd16feba Mon Sep 17 00:00:00 2001 From: Daniel Poetzl Date: Fri, 3 Feb 2017 13:44:37 +0000 Subject: [PATCH 14/24] Addressing goto analyzer review comments --- .../constant_propagation_05/test.desc | 2 +- .../constant_propagation_06/test.desc | 2 +- .../constant_propagation_10/test.desc | 2 +- .../constant_propagation_13/test.desc | 2 +- .../constant_propagation_14/test.desc | 4 +- .../constant_propagation_15/test.desc | 2 +- regression/goto-analyzer/intervals_01/main.c | 2 +- .../goto-analyzer/intervals_01/test.desc | 16 +- .../goto-analyzer/intervals_02/test.desc | 2 +- .../goto-analyzer/intervals_03/test.desc | 2 +- .../goto-analyzer/intervals_04/test.desc | 2 +- .../goto-analyzer/intervals_05/test.desc | 2 +- .../goto-analyzer/intervals_06/test.desc | 2 +- .../goto-analyzer/intervals_07/test.desc | 2 +- .../goto-analyzer/intervals_08/test.desc | 2 +- .../goto-analyzer/intervals_09/test.desc | 2 +- .../goto-analyzer/intervals_10/test.desc | 10 +- .../goto-analyzer/intervals_11/test.desc | 4 +- .../goto-analyzer/intervals_12/test.desc | 4 +- .../goto-analyzer/intervals_13/test.desc | 16 +- .../goto-analyzer/intervals_14/test.desc | 6 +- .../goto-analyzer/intervals_15/test.desc | 2 +- regression/goto-instrument-wmm-core/Makefile | 1 - src/analyses/ai.cpp | 46 ++++++ src/analyses/ai.h | 30 +--- src/analyses/constant_propagator.cpp | 155 +++++++----------- src/analyses/constant_propagator.h | 15 +- src/analyses/dependence_graph.cpp | 27 ++- src/analyses/interval_domain.cpp | 25 +-- src/analyses/interval_domain.h | 4 +- src/analyses/replace_symbol_ext.cpp | 72 -------- src/analyses/replace_symbol_ext.h | 20 --- .../goto_analyzer_parse_options.cpp | 4 +- src/goto-analyzer/static_analyzer.cpp | 40 +++-- src/goto-analyzer/static_show_domain.cpp | 17 +- src/goto-analyzer/static_show_domain.h | 1 - src/goto-analyzer/static_simplifier.cpp | 123 ++++++-------- src/goto-analyzer/static_simplifier.h | 1 - src/goto-programs/remove_unreachable.cpp | 1 - src/util/replace_symbol.cpp | 74 +++++++-- src/util/replace_symbol.h | 5 +- 41 files changed, 342 insertions(+), 409 deletions(-) delete mode 100644 src/analyses/replace_symbol_ext.cpp delete mode 100644 src/analyses/replace_symbol_ext.h diff --git a/regression/goto-analyzer/constant_propagation_05/test.desc b/regression/goto-analyzer/constant_propagation_05/test.desc index e53a7f39396..e84fdb08b4f 100644 --- a/regression/goto-analyzer/constant_propagation_05/test.desc +++ b/regression/goto-analyzer/constant_propagation_05/test.desc @@ -3,6 +3,6 @@ main.c --constants --verify ^EXIT=0$ ^SIGNAL=0$ -^\[main.assertion.1\] file main.c line 12 function main, assertion j!=3: FAILURE (if reachable)$ +^\[main.assertion.1\] file main.c line 12 function main, assertion j!=3: Failure (if reachable)$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/constant_propagation_06/test.desc b/regression/goto-analyzer/constant_propagation_06/test.desc index 48616565f04..da9d7778bbf 100644 --- a/regression/goto-analyzer/constant_propagation_06/test.desc +++ b/regression/goto-analyzer/constant_propagation_06/test.desc @@ -3,6 +3,6 @@ main.c --constants --verify ^EXIT=0$ ^SIGNAL=0$ -^\[main.assertion.1\] file main.c line 12 function main, assertion i<51: UNKNOWN$ +^\[main.assertion.1\] file main.c line 12 function main, assertion i<51: Unknown$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/constant_propagation_10/test.desc b/regression/goto-analyzer/constant_propagation_10/test.desc index 9662c38cf04..527325b84bb 100644 --- a/regression/goto-analyzer/constant_propagation_10/test.desc +++ b/regression/goto-analyzer/constant_propagation_10/test.desc @@ -3,6 +3,6 @@ main.c --constants --verify ^EXIT=0$ ^SIGNAL=0$ -^\[main.assertion.1\] file main.c line 10 function main, assertion a\[0\]==2: FAILURE$ +^\[main.assertion.1\] file main.c line 10 function main, assertion a\[0\]==2: Failure$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/constant_propagation_13/test.desc b/regression/goto-analyzer/constant_propagation_13/test.desc index 66d18c7ab67..2d2e078a424 100644 --- a/regression/goto-analyzer/constant_propagation_13/test.desc +++ b/regression/goto-analyzer/constant_propagation_13/test.desc @@ -3,6 +3,6 @@ main.c --constants --verify ^EXIT=0$ ^SIGNAL=0$ -^\[main.assertion.1\] file main.c line 9 function main, assertion y==0: FAILURE (if reachable)$ +^\[main.assertion.1\] file main.c line 9 function main, assertion y==0: Failure (if reachable)$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/constant_propagation_14/test.desc b/regression/goto-analyzer/constant_propagation_14/test.desc index 5f104bfa09c..fc3be910670 100644 --- a/regression/goto-analyzer/constant_propagation_14/test.desc +++ b/regression/goto-analyzer/constant_propagation_14/test.desc @@ -3,7 +3,7 @@ main.c --constants --verify ^EXIT=0$ ^SIGNAL=0$ -^\[main.assertion.1\] file main.c line 11 function main, assertion a\[0\]==1 || a\[0\]==2: SUCCESS$ -^\[main.assertion.2\] file main.c line 12 function main, assertion a\[0\]==1 && a\[0\]==2: FAILURE$ +^\[main.assertion.1\] file main.c line 11 function main, assertion a\[0\]==1 || a\[0\]==2: Success$ +^\[main.assertion.2\] file main.c line 12 function main, assertion a\[0\]==1 && a\[0\]==2: Failure$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/constant_propagation_15/test.desc b/regression/goto-analyzer/constant_propagation_15/test.desc index a1ce84cc89c..aba11ba0c06 100644 --- a/regression/goto-analyzer/constant_propagation_15/test.desc +++ b/regression/goto-analyzer/constant_propagation_15/test.desc @@ -3,6 +3,6 @@ main.c --constants --verify ^EXIT=0$ ^SIGNAL=0$ -^\[main.assertion.1\] file main.c line 9 function main, assertion a\[0\]==2: FAILURE$ +^\[main.assertion.1\] file main.c line 9 function main, assertion a\[0\]==2: Failure$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/intervals_01/main.c b/regression/goto-analyzer/intervals_01/main.c index cdec490fe6d..ce6294d362c 100644 --- a/regression/goto-analyzer/intervals_01/main.c +++ b/regression/goto-analyzer/intervals_01/main.c @@ -3,7 +3,7 @@ int main() { int i, j=20; - + if(i>=20) assert(i>=10); diff --git a/regression/goto-analyzer/intervals_01/test.desc b/regression/goto-analyzer/intervals_01/test.desc index db689e5d1ad..e90c4aaeda6 100644 --- a/regression/goto-analyzer/intervals_01/test.desc +++ b/regression/goto-analyzer/intervals_01/test.desc @@ -3,13 +3,13 @@ main.c --intervals --verify ^EXIT=0$ ^SIGNAL=0$ -^\[main.assertion.1\] file main.c line 8 function main, assertion i>=10: SUCCESS$ -^\[main.assertion.2\] file main.c line 11 function main, assertion i!=30: SUCCESS$ -^\[main.assertion.3\] file main.c line 14 function main, assertion i!=15: UNKNOWN$ -^\[main.assertion.4\] file main.c line 17 function main, assertion 0: SUCCESS$ -^\[main.assertion.5\] file main.c line 20 function main, assertion j>=10: SUCCESS$ -^\[main.assertion.6\] file main.c line 23 function main, assertion i>=j: UNKNOWN$ -^\[main.assertion.7\] file main.c line 26 function main, assertion i>=11: SUCCESS$ -^\[main.assertion.8\] file main.c line 29 function main, assertion j<100: SUCCESS$ +^\[main.assertion.1\] file main.c line 8 function main, assertion i>=10: Success$ +^\[main.assertion.2\] file main.c line 11 function main, assertion i!=30: Success$ +^\[main.assertion.3\] file main.c line 14 function main, assertion i!=15: Unknown$ +^\[main.assertion.4\] file main.c line 17 function main, assertion 0: Success$ +^\[main.assertion.5\] file main.c line 20 function main, assertion j>=10: Success$ +^\[main.assertion.6\] file main.c line 23 function main, assertion i>=j: Unknown$ +^\[main.assertion.7\] file main.c line 26 function main, assertion i>=11: Success$ +^\[main.assertion.8\] file main.c line 29 function main, assertion j<100: Success$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/intervals_02/test.desc b/regression/goto-analyzer/intervals_02/test.desc index 9dfc850cf6b..fa4f926287f 100644 --- a/regression/goto-analyzer/intervals_02/test.desc +++ b/regression/goto-analyzer/intervals_02/test.desc @@ -3,6 +3,6 @@ main.c --intervals --verify ^EXIT=0$ ^SIGNAL=0$ -^\[main.assertion.1\] file main.c line 7 function main, assertion x > -10 && x < 100: SUCCESS$ +^\[main.assertion.1\] file main.c line 7 function main, assertion x > -10 && x < 100: Success$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/intervals_03/test.desc b/regression/goto-analyzer/intervals_03/test.desc index f901ea41a56..79042c334de 100644 --- a/regression/goto-analyzer/intervals_03/test.desc +++ b/regression/goto-analyzer/intervals_03/test.desc @@ -3,6 +3,6 @@ main.c --intervals --verify ^EXIT=0$ ^SIGNAL=0$ -^\[main.assertion.1\] file main.c line 7 function main, assertion x > -10 || x < 100: SUCCESS$ +^\[main.assertion.1\] file main.c line 7 function main, assertion x > -10 || x < 100: Success$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/intervals_04/test.desc b/regression/goto-analyzer/intervals_04/test.desc index 91550585968..5bb03255f37 100644 --- a/regression/goto-analyzer/intervals_04/test.desc +++ b/regression/goto-analyzer/intervals_04/test.desc @@ -3,6 +3,6 @@ main.c --intervals --verify ^EXIT=0$ ^SIGNAL=0$ -^\[main.assertion.1\] file main.c line 9 function main, assertion i >= 1 && i <= 2: SUCCESS$ +^\[main.assertion.1\] file main.c line 9 function main, assertion i >= 1 && i <= 2: Success$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/intervals_05/test.desc b/regression/goto-analyzer/intervals_05/test.desc index 3c4e162000b..5c9af29a2b1 100644 --- a/regression/goto-analyzer/intervals_05/test.desc +++ b/regression/goto-analyzer/intervals_05/test.desc @@ -3,6 +3,6 @@ main.c --intervals --verify ^EXIT=0$ ^SIGNAL=0$ -^\[main.assertion.1\] file main.c line 9 function main, assertion i >= 1 || i <= 2: SUCCESS$ +^\[main.assertion.1\] file main.c line 9 function main, assertion i >= 1 || i <= 2: Success$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/intervals_06/test.desc b/regression/goto-analyzer/intervals_06/test.desc index facd3285898..2dc8d29a3b6 100644 --- a/regression/goto-analyzer/intervals_06/test.desc +++ b/regression/goto-analyzer/intervals_06/test.desc @@ -3,6 +3,6 @@ main.c --intervals --verify ^EXIT=0$ ^SIGNAL=0$ -^\[main.assertion.1\] file main.c line 7 function main, assertion x < -10 || x > 100: FAILURE (if reachable)$ +^\[main.assertion.1\] file main.c line 7 function main, assertion x < -10 || x > 100: Failure (if reachable)$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/intervals_07/test.desc b/regression/goto-analyzer/intervals_07/test.desc index 557063f4e33..aa3962f39de 100644 --- a/regression/goto-analyzer/intervals_07/test.desc +++ b/regression/goto-analyzer/intervals_07/test.desc @@ -3,6 +3,6 @@ main.c --intervals --verify ^EXIT=0$ ^SIGNAL=0$ -^\[main.assertion.1\] file main.c line 7 function main, assertion x < -10 && x > 100: FAILURE (if reachable)$ +^\[main.assertion.1\] file main.c line 7 function main, assertion x < -10 && x > 100: Failure (if reachable)$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/intervals_08/test.desc b/regression/goto-analyzer/intervals_08/test.desc index 4cf9f8f7def..7b83ecd0f21 100644 --- a/regression/goto-analyzer/intervals_08/test.desc +++ b/regression/goto-analyzer/intervals_08/test.desc @@ -3,6 +3,6 @@ main.c --intervals --verify ^EXIT=0$ ^SIGNAL=0$ -^\[main.assertion.1\] file main.c line 6 function main, assertion x < -10 && x < 100: FAILURE (if reachable)$ +^\[main.assertion.1\] file main.c line 6 function main, assertion x < -10 && x < 100: Failure (if reachable)$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/intervals_09/test.desc b/regression/goto-analyzer/intervals_09/test.desc index 1ea84fe57dc..8145fc369ca 100644 --- a/regression/goto-analyzer/intervals_09/test.desc +++ b/regression/goto-analyzer/intervals_09/test.desc @@ -3,6 +3,6 @@ main.c --intervals --verify ^EXIT=0$ ^SIGNAL=0$ -^\[main.assertion.1\] file main.c line 9 function main, assertion i>=1 && i<=2: SUCCESS$ +^\[main.assertion.1\] file main.c line 9 function main, assertion i>=1 && i<=2: Success$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/intervals_10/test.desc b/regression/goto-analyzer/intervals_10/test.desc index 239032bf55f..468ce13a550 100644 --- a/regression/goto-analyzer/intervals_10/test.desc +++ b/regression/goto-analyzer/intervals_10/test.desc @@ -3,10 +3,10 @@ main.c --intervals --verify ^EXIT=0$ ^SIGNAL=0$ -^\[main.assertion.1\] file main.c line 8 function main, assertion j<=100: SUCCESS$ -^\[main.assertion.2\] file main.c line 11 function main, assertion j<101: SUCCESS$ -^\[main.assertion.3\] file main.c line 14 function main, assertion j>100: FAILURE (if reachable)$ -^\[main.assertion.4\] file main.c line 17 function main, assertion j<99: UNKNOWN$ -^\[main.assertion.5\] file main.c line 20 function main, assertion j==100: FAILURE (if reachable)$ +^\[main.assertion.1\] file main.c line 8 function main, assertion j<=100: Success$ +^\[main.assertion.2\] file main.c line 11 function main, assertion j<101: Success$ +^\[main.assertion.3\] file main.c line 14 function main, assertion j>100: Failure (if reachable)$ +^\[main.assertion.4\] file main.c line 17 function main, assertion j<99: Unknown$ +^\[main.assertion.5\] file main.c line 20 function main, assertion j==100: Failure (if reachable)$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/intervals_11/test.desc b/regression/goto-analyzer/intervals_11/test.desc index 691bd1c1314..799ad36f64f 100644 --- a/regression/goto-analyzer/intervals_11/test.desc +++ b/regression/goto-analyzer/intervals_11/test.desc @@ -3,7 +3,7 @@ main.c --intervals --verify ^EXIT=0$ ^SIGNAL=0$ -^\[main.assertion.1\] file main.c line 30 function main, assertion y\[i\]>=-1.0f && y\[i\]<=1.0f: UNKNOWN$ -^\[main.assertion.2\] file main.c line 35 function main, assertion y\[i\]>=-1.0f && y\[i\]<=1.0f: UNKNOWN$ +^\[main.assertion.1\] file main.c line 30 function main, assertion y\[i\]>=-1.0f && y\[i\]<=1.0f: Unknown$ +^\[main.assertion.2\] file main.c line 35 function main, assertion y\[i\]>=-1.0f && y\[i\]<=1.0f: Unknown$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/intervals_12/test.desc b/regression/goto-analyzer/intervals_12/test.desc index bdb98e27d7e..ffdf46857de 100644 --- a/regression/goto-analyzer/intervals_12/test.desc +++ b/regression/goto-analyzer/intervals_12/test.desc @@ -3,7 +3,7 @@ main.c --intervals --verify ^EXIT=0$ ^SIGNAL=0$ -^[main.assertion.1] file main.c line 8 function main, assertion j < 0: SUCCESS$ -^[main.assertion.2] file main.c line 11 function main, assertion j < 0: SUCCESS$ +^[main.assertion.1] file main.c line 8 function main, assertion j < 0: Success$ +^[main.assertion.2] file main.c line 11 function main, assertion j < 0: Success$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/intervals_13/test.desc b/regression/goto-analyzer/intervals_13/test.desc index db689e5d1ad..e90c4aaeda6 100644 --- a/regression/goto-analyzer/intervals_13/test.desc +++ b/regression/goto-analyzer/intervals_13/test.desc @@ -3,13 +3,13 @@ main.c --intervals --verify ^EXIT=0$ ^SIGNAL=0$ -^\[main.assertion.1\] file main.c line 8 function main, assertion i>=10: SUCCESS$ -^\[main.assertion.2\] file main.c line 11 function main, assertion i!=30: SUCCESS$ -^\[main.assertion.3\] file main.c line 14 function main, assertion i!=15: UNKNOWN$ -^\[main.assertion.4\] file main.c line 17 function main, assertion 0: SUCCESS$ -^\[main.assertion.5\] file main.c line 20 function main, assertion j>=10: SUCCESS$ -^\[main.assertion.6\] file main.c line 23 function main, assertion i>=j: UNKNOWN$ -^\[main.assertion.7\] file main.c line 26 function main, assertion i>=11: SUCCESS$ -^\[main.assertion.8\] file main.c line 29 function main, assertion j<100: SUCCESS$ +^\[main.assertion.1\] file main.c line 8 function main, assertion i>=10: Success$ +^\[main.assertion.2\] file main.c line 11 function main, assertion i!=30: Success$ +^\[main.assertion.3\] file main.c line 14 function main, assertion i!=15: Unknown$ +^\[main.assertion.4\] file main.c line 17 function main, assertion 0: Success$ +^\[main.assertion.5\] file main.c line 20 function main, assertion j>=10: Success$ +^\[main.assertion.6\] file main.c line 23 function main, assertion i>=j: Unknown$ +^\[main.assertion.7\] file main.c line 26 function main, assertion i>=11: Success$ +^\[main.assertion.8\] file main.c line 29 function main, assertion j<100: Success$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/intervals_14/test.desc b/regression/goto-analyzer/intervals_14/test.desc index 58b2daef2fe..20a01bf3e12 100644 --- a/regression/goto-analyzer/intervals_14/test.desc +++ b/regression/goto-analyzer/intervals_14/test.desc @@ -3,8 +3,8 @@ main.c --intervals --verify ^EXIT=0$ ^SIGNAL=0$ -^\[main.assertion.1\] file main.c line 12 function main, assertion i<50: UNKNOWN$ -^\[main.assertion.2\] file main.c line 13 function main, assertion i<51: UNKNOWN$ -^\[main.assertion.3\] file main.c line 14 function main, assertion i<52: SUCCESS$ +^\[main.assertion.1\] file main.c line 12 function main, assertion i<50: Unknown$ +^\[main.assertion.2\] file main.c line 13 function main, assertion i<51: Unknown$ +^\[main.assertion.3\] file main.c line 14 function main, assertion i<52: Success$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/intervals_15/test.desc b/regression/goto-analyzer/intervals_15/test.desc index 21eb7254c54..7d3bae09250 100644 --- a/regression/goto-analyzer/intervals_15/test.desc +++ b/regression/goto-analyzer/intervals_15/test.desc @@ -3,6 +3,6 @@ main.c --intervals --verify ^EXIT=0$ ^SIGNAL=0$ -^\[main.assertion.1\] file main.c line 12 function main, assertion j<52: UNKNOWN$ +^\[main.assertion.1\] file main.c line 12 function main, assertion j<52: Unknown$ -- ^warning: ignoring diff --git a/regression/goto-instrument-wmm-core/Makefile b/regression/goto-instrument-wmm-core/Makefile index 6684274289d..85c17bf622b 100644 --- a/regression/goto-instrument-wmm-core/Makefile +++ b/regression/goto-instrument-wmm-core/Makefile @@ -31,4 +31,3 @@ show: vim -o "$$dir/*.c" "$$dir/*.out"; \ fi; \ done; - diff --git a/src/analyses/ai.cpp b/src/analyses/ai.cpp index 45d4b83c92c..dc60f04067f 100644 --- a/src/analyses/ai.cpp +++ b/src/analyses/ai.cpp @@ -8,6 +8,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include #include #include @@ -18,6 +19,51 @@ Author: Daniel Kroening, kroening@kroening.com /*******************************************************************\ +Function: ai_domain_baset::output_json + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +jsont ai_domain_baset::output_json( + const ai_baset &ai, + const namespacet &ns) const +{ + std::ostringstream out; + output(out, ai, ns); + json_stringt json(out.str()); + return json; +} + +/*******************************************************************\ + +Function: ai_domain_baset::output_xml + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +xmlt ai_domain_baset::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; +} + +/*******************************************************************\ + Function: ai_baset::output Inputs: diff --git a/src/analyses/ai.h b/src/analyses/ai.h index 64ead3a941f..0ec78e13b21 100644 --- a/src/analyses/ai.h +++ b/src/analyses/ai.h @@ -11,7 +11,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include #include #include @@ -60,24 +59,11 @@ 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; - } + const namespacet &ns) const; 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; - } + const namespacet &ns) const; // no states virtual void make_bottom()=0; @@ -97,14 +83,16 @@ class ai_domain_baset // 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, + // current state. It is used to evaluate assertions and in program + // simplification + + // return true if unchanged + virtual bool ai_simplify( + exprt &condition, const namespacet &ns, const bool lhs=false) const { - return condition; + return true; } }; diff --git a/src/analyses/constant_propagator.cpp b/src/analyses/constant_propagator.cpp index d8f342c52a8..1cf928ac069 100644 --- a/src/analyses/constant_propagator.cpp +++ b/src/analyses/constant_propagator.cpp @@ -1,6 +1,6 @@ /*******************************************************************\ -Module: Constant Propagation +Module: Constant propagation Author: Peter Schrammel @@ -13,6 +13,7 @@ Author: Peter Schrammel #include #include #include +#include #include "constant_propagator.h" @@ -41,7 +42,7 @@ void constant_propagator_domaint::assign_rec( exprt tmp=rhs; values.replace_const(tmp); - tmp=simplify_expr(tmp, ns); + simplify(tmp, ns); if(tmp.is_constant()) values.set_to(s, tmp); @@ -139,13 +140,13 @@ void constant_propagator_domaint::transform( if(to==next) { - if(id=="__CPROVER_set_must" || - id=="__CPROVER_get_must" || - id=="__CPROVER_set_may" || - id=="__CPROVER_get_may" || - id=="__CPROVER_cleanup" || - id=="__CPROVER_clear_may" || - id=="__CPROVER_clear_must") + if(id==CPROVER_PREFIX "set_must" || + id==CPROVER_PREFIX "get_must" || + id==CPROVER_PREFIX "set_may" || + id==CPROVER_PREFIX "get_may" || + id==CPROVER_PREFIX "cleanup" || + id==CPROVER_PREFIX "clear_may" || + id==CPROVER_PREFIX "clear_must") { // no effect on constants } @@ -166,17 +167,19 @@ void constant_propagator_domaint::transform( const code_typet &code_type=to_code_type(symbol.type); const code_typet::parameterst ¶meters=code_type.parameters(); - const code_function_callt::argumentst &arguments - =function_call.arguments(); + const code_function_callt::argumentst &arguments= + function_call.arguments(); - unsigned n=std::min(arguments.size(), parameters.size()); - - for(unsigned i=0; iget_identifier(), arg.type()); + assign_rec(values, parameter_expr, arg, ns); - assign_rec(values, parameter_expr, arguments[i], ns); + ++p_it; } } } @@ -201,18 +204,8 @@ void constant_propagator_domaint::transform( const code_typet &type=to_code_type(symbol.type); - typedef code_typet::parameterst parameterst; - const parameterst ¶meters=type.parameters(); - - for(parameterst::const_iterator it=parameters.begin(); - it!=parameters.end(); it++) - { - // normal parameter - const irep_idt par=it->get_identifier(); - - // this erases the parameter from the map - values.set_to_top(par); - } + for(const auto ¶m : type.parameters()) + values.set_to_top(param.get_identifier()); } assert(from->is_goto() || !values.is_bottom); @@ -245,6 +238,7 @@ bool constant_propagator_domaint::two_way_propagate_rec( bool change=false; + // this seems to be buggy at present #if 0 if(expr.id()==ID_and) { @@ -282,32 +276,35 @@ bool constant_propagator_domaint::two_way_propagate_rec( /*******************************************************************\ -Function: constant_propagator_domaint::domain_simplify +Function: constant_propagator_domaint::simplify Inputs: The condition to simplify and its namespace. Outputs: The simplified condition. Purpose: Simplify the condition given context-sensitive knowledge - from the domain. + from the abstract state. \*******************************************************************/ -exprt constant_propagator_domaint::domain_simplify( - const exprt &condition, +bool constant_propagator_domaint::ai_simplify( + exprt &condition, const namespacet &ns, const bool lhs) const { if(lhs) { // For now do not simplify the left hand sides of assignments - return condition; + return true; } else { - exprt e(condition); - values.replace_const(e); - return simplify_expr(e, ns); + bool b; + + b=values.replace_const.replace(condition); + b&=simplify(condition, ns); + + return b; } } @@ -396,17 +393,12 @@ Function: constant_propagator_domaint::valuest::set_to_top bool constant_propagator_domaint::valuest::set_to_top(const irep_idt &id) { - replace_symbolt::expr_mapt::iterator r_it - =replace_const.expr_map.find(id); + replace_symbolt::expr_mapt::size_type n_erased= + replace_const.expr_map.erase(id); - if(r_it!=replace_const.expr_map.end()) - { - assert(!is_bottom); - replace_const.expr_map.erase(r_it); - return true; - } + assert(n_erased==0 || !is_bottom); - return false; + return n_erased>0; } /*******************************************************************\ @@ -425,7 +417,7 @@ void constant_propagator_domaint::valuest::set_dirty_to_top( const dirtyt &dirty, const namespacet &ns) { - typedef replace_symbol_extt::expr_mapt expr_mapt; + typedef replace_symbolt::expr_mapt expr_mapt; expr_mapt &expr_map=replace_const.expr_map; for(expr_mapt::iterator it=expr_map.begin(); @@ -475,12 +467,9 @@ void constant_propagator_domaint::valuest::output( return; } - for(replace_symbolt::expr_mapt::const_iterator - it=replace_const.expr_map.begin(); - it!=replace_const.expr_map.end(); - ++it) + for(const auto &p : replace_const.expr_map) { - out << ' ' << it->first << "=" << from_expr(ns, "", it->second) << '\n'; + out << ' ' << p.first << "=" << from_expr(ns, "", p.second) << '\n'; } } @@ -518,10 +507,6 @@ Function: constant_propagator_domaint::valuest::merge bool constant_propagator_domaint::valuest::merge(const valuest &src) { - // dummy - const symbol_tablet symbol_table; - const namespacet ns(symbol_table); - // nothing to do if(src.is_bottom) return false; @@ -539,8 +524,8 @@ bool constant_propagator_domaint::valuest::merge(const valuest &src) bool changed=false; - replace_symbol_extt::expr_mapt &expr_map=replace_const.expr_map; - const replace_symbol_extt::expr_mapt &src_expr_map=src.replace_const.expr_map; + replace_symbolt::expr_mapt &expr_map=replace_const.expr_map; + const replace_symbolt::expr_mapt &src_expr_map=src.replace_const.expr_map; // handle top if(src_expr_map.empty()) @@ -549,8 +534,6 @@ bool constant_propagator_domaint::valuest::merge(const valuest &src) changed=!expr_map.empty(); set_to_top(); - assert(expr_map.empty()); - assert(!is_bottom); return changed; } @@ -607,29 +590,26 @@ bool constant_propagator_domaint::valuest::meet(const valuest &src) if(src.is_bottom || is_bottom) return false; - bool changed = false; + bool changed=false; - for(replace_symbolt::expr_mapt::const_iterator - it=src.replace_const.expr_map.begin(); - it!=src.replace_const.expr_map.end(); - ++it) + for(const auto &m : src.replace_const.expr_map) { replace_symbolt::expr_mapt::iterator - c_it = replace_const.expr_map.find(it->first); + c_it=replace_const.expr_map.find(m.first); if(c_it!=replace_const.expr_map.end()) { - if(c_it->second!=it->second) + if(c_it->second!=m.second) { set_to_bottom(); - changed = true; + changed=true; break; } } else { - set_to(it->first, it->second); - changed = true; + set_to(m.first, m.second); + changed=true; } } @@ -653,31 +633,7 @@ bool constant_propagator_domaint::merge( locationt from, locationt to) { - const symbol_tablet symbol_table; - const namespacet ns(symbol_table); - -#if 0 - if(to->is_skip()) - { - std::cout << "This:\n"; - values.output(std::cout, ns); - std::cout << "Other:\n"; - other.values.output(std::cout, ns); - } -#endif - - bool b; - b=values.merge(other.values); - -#if 0 - if(to->is_skip()) - { - std::cout << "Merge result:\n"; - values.output(std::cout, ns); - } -#endif - - return b; + return values.merge(other.values); } /*******************************************************************\ @@ -729,13 +685,13 @@ void constant_propagator_ait::replace( if(it->is_goto() || it->is_assume() || it->is_assert()) { s_it->second.values.replace_const(it->guard); - it->guard = simplify_expr(it->guard, ns); + simplify(it->guard, ns); } else if(it->is_assign()) { exprt &rhs=to_code_assign(it->code).rhs(); s_it->second.values.replace_const(rhs); - rhs=simplify_expr(rhs, ns); + simplify(rhs, ns); if(rhs.id()==ID_constant) rhs.add_source_location()=it->code.op0().source_location(); } @@ -743,7 +699,8 @@ void constant_propagator_ait::replace( { s_it->second.values.replace_const( to_code_function_call(it->code).function()); - simplify_expr(to_code_function_call(it->code).function(), ns); + + simplify(to_code_function_call(it->code).function(), ns); exprt::operandst &args= to_code_function_call(it->code).arguments(); @@ -752,7 +709,7 @@ void constant_propagator_ait::replace( o_it!=args.end(); ++o_it) { s_it->second.values.replace_const(*o_it); - *o_it=simplify_expr(*o_it, ns); + simplify(*o_it, ns); } } else if(it->is_other()) diff --git a/src/analyses/constant_propagator.h b/src/analyses/constant_propagator.h index 3f2d6921160..c1791dd9cae 100644 --- a/src/analyses/constant_propagator.h +++ b/src/analyses/constant_propagator.h @@ -9,13 +9,12 @@ Author: Peter Schrammel #ifndef CPROVER_ANALYSES_CONSTANT_PROPAGATOR_H #define CPROVER_ANALYSES_CONSTANT_PROPAGATOR_H -#include +#include +#include #include "ai.h" #include "dirty.h" -#include "replace_symbol_ext.h" - class constant_propagator_domaint:public ai_domain_baset { public: @@ -35,8 +34,8 @@ class constant_propagator_domaint:public ai_domain_baset locationt from, locationt to); - virtual exprt domain_simplify( - const exprt &condition, + virtual bool ai_simplify( + exprt &condition, const namespacet &ns, const bool lhs=false) const; @@ -61,7 +60,7 @@ class constant_propagator_domaint:public ai_domain_baset valuest():is_bottom(true) {} // maps variables to constants - replace_symbol_extt replace_const; + replace_symbolt replace_const; bool is_bottom; bool merge(const valuest &src); @@ -141,6 +140,8 @@ class constant_propagator_ait:public ait goto_functionst &goto_functions, const namespacet &ns) : dirty(goto_functions) { + assert(false); + operator()(goto_functions, ns); replace(goto_functions, ns); } @@ -149,6 +150,8 @@ class constant_propagator_ait:public ait goto_functionst::goto_functiont &goto_function, const namespacet &ns) : dirty(goto_function) { + assert(false); + operator()(goto_function, ns); replace(goto_function, ns); } diff --git a/src/analyses/dependence_graph.cpp b/src/analyses/dependence_graph.cpp index 93a73165650..686aecf6b4d 100644 --- a/src/analyses/dependence_graph.cpp +++ b/src/analyses/dependence_graph.cpp @@ -12,6 +12,7 @@ Date: August 2013 #include #include +#include #include "goto_rw.h" @@ -359,42 +360,34 @@ Function: dep_graph_domaint::output_json \*******************************************************************/ - 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) + for(const auto &cd : control_deps) { 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["locationNumber"]= + json_numbert(std::to_string(cd->location_number)); + link["sourceLocation"]=json(cd->source_location); link["type"]=json_stringt("control"); } - for(dep_graph_domaint::depst::const_iterator ddi=data_deps.begin(); - ddi!=data_deps.end(); - ++ddi) + for(const auto &dd : data_deps) { 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["locationNumber"]= + json_numbert(std::to_string(dd->location_number)); + link["sourceLocation"]=json(dd->source_location); + json_stringt(dd->source_location.as_string()); link["type"]=json_stringt("data"); } return graph; } - - /*******************************************************************\ Function: dependence_grapht::add_dep diff --git a/src/analyses/interval_domain.cpp b/src/analyses/interval_domain.cpp index 4965501d9d6..43d80acd78d 100644 --- a/src/analyses/interval_domain.cpp +++ b/src/analyses/interval_domain.cpp @@ -528,25 +528,28 @@ exprt interval_domaint::make_expression(const symbol_exprt &src) const /*******************************************************************\ -Function: interval_domaint::domain_simplify +Function: interval_domaint::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. + Purpose: Uses the abstract state to simplify a given expression + using context-specific information. \*******************************************************************/ -exprt interval_domaint::domain_simplify( - const exprt &condition, +bool interval_domaint::ai_simplify( + exprt &condition, const namespacet &ns, const bool lhs) const { + bool unchanged=true; + if(lhs) { // For now do not simplify the left hand side of assignments - return condition; + return true; } interval_domaint d(*this); @@ -565,9 +568,8 @@ exprt interval_domaint::domain_simplify( if(!a.join(d)) { - exprt e; - e.make_true(); - return e; + unchanged=condition.is_true(); + condition.make_true(); } } else if(condition.id()==ID_symbol) @@ -579,11 +581,10 @@ exprt interval_domaint::domain_simplify( d.assume(not_exprt(condition), ns); if(d.is_bottom()) { - exprt e; - e.make_true(); - return e; + unchanged=condition.is_true(); + condition.make_true(); } } - return condition; + return unchanged; } diff --git a/src/analyses/interval_domain.h b/src/analyses/interval_domain.h index c7ae0896739..237f4912752 100644 --- a/src/analyses/interval_domain.h +++ b/src/analyses/interval_domain.h @@ -90,8 +90,8 @@ class interval_domaint:public ai_domain_baset return bottom; } - virtual exprt domain_simplify( - const exprt &condition, + virtual bool ai_simplify( + exprt &condition, const namespacet &ns, const bool lhs=false) const; diff --git a/src/analyses/replace_symbol_ext.cpp b/src/analyses/replace_symbol_ext.cpp deleted file mode 100644 index 11c7c163edb..00000000000 --- a/src/analyses/replace_symbol_ext.cpp +++ /dev/null @@ -1,72 +0,0 @@ -/*******************************************************************\ - -Module: Modified expression replacement for constant propagator - -Author: Peter Schrammel - -\*******************************************************************/ - -#include -#include - -#include "replace_symbol_ext.h" - -/*******************************************************************\ - -Function: replace_symbol_extt::replace - - Inputs: - - Outputs: - - Purpose: does not replace object in address_of expressions - -\*******************************************************************/ - -bool replace_symbol_extt::replace(exprt &dest) const -{ - bool result=true; // nothing changed - - // first look at type - - if(have_to_replace(dest.type())) - if(!replace_symbolt::replace(dest.type())) - result=false; - - // now do expression itself - - if(!have_to_replace(dest)) - return result; - - if(dest.id()==ID_symbol) - { - expr_mapt::const_iterator it= - expr_map.find(dest.get(ID_identifier)); - - if(it!=expr_map.end()) - { - dest=it->second; - return false; - } - } - - Forall_operands(it, dest) - if(!replace(*it)) - result=false; - - const irept &c_sizeof_type=dest.find(ID_C_c_sizeof_type); - - if(c_sizeof_type.is_not_nil() && - !replace_symbolt::replace( - static_cast(dest.add(ID_C_c_sizeof_type)))) - result=false; - - const irept &va_arg_type=dest.find(ID_C_va_arg_type); - - if(va_arg_type.is_not_nil() && - !replace_symbolt::replace( - static_cast(dest.add(ID_C_va_arg_type)))) - result=false; - - return result; -} diff --git a/src/analyses/replace_symbol_ext.h b/src/analyses/replace_symbol_ext.h deleted file mode 100644 index 5a2152db17f..00000000000 --- a/src/analyses/replace_symbol_ext.h +++ /dev/null @@ -1,20 +0,0 @@ -/*******************************************************************\ - -Module: Modified expression replacement for constant propagator - -Author: Peter Schrammel - -\*******************************************************************/ - -#ifndef CPROVER_ANALYSES_REPLACE_SYMBOL_EXT_H -#define CPROVER_ANALYSES_REPLACE_SYMBOL_EXT_H - -#include - -class replace_symbol_extt:public replace_symbolt -{ -public: - virtual bool replace(exprt &dest) const; -}; - -#endif // CPROVER_ANALYSES_REPLACE_SYMBOL_EXT_H diff --git a/src/goto-analyzer/goto_analyzer_parse_options.cpp b/src/goto-analyzer/goto_analyzer_parse_options.cpp index f77e74500e6..363680604a7 100644 --- a/src/goto-analyzer/goto_analyzer_parse_options.cpp +++ b/src/goto-analyzer/goto_analyzer_parse_options.cpp @@ -678,7 +678,7 @@ void goto_analyzer_parse_optionst::help() { std::cout << "\n" - "* * GOTO-ANALYZER " CBMC_VERSION " - Copyright (C) 2016 "; + "* * GOTO-ANALYZER " CBMC_VERSION " - Copyright (C) 2017 "; std::cout << "(" << (sizeof(void *)*8) << "-bit version)"; @@ -702,7 +702,7 @@ void goto_analyzer_parse_optionst::help() "\n" "Abstract interpreter options:\n" " --flow-sensitive use flow-sensitive abstract interpreter\n" - " --concurrent use concurrent abstract interpreter\n" + " --concurrent use concurrency-aware abstract interpreter\n" "\n" "Domain options:\n" " --constants constant domain\n" diff --git a/src/goto-analyzer/static_analyzer.cpp b/src/goto-analyzer/static_analyzer.cpp index 0dec55a54de..e00eefc6050 100644 --- a/src/goto-analyzer/static_analyzer.cpp +++ b/src/goto-analyzer/static_analyzer.cpp @@ -9,6 +9,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include #include #include @@ -16,7 +17,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "static_analyzer.h" -template +template class static_analyzert:public messaget { public: @@ -110,7 +111,8 @@ void static_analyzert::plain_text_report() if(!i_it->is_assert()) continue; - exprt simplified=domain[i_it].domain_simplify(i_it->guard, ns); + exprt e(i_it->guard); + domain[i_it].ai_simplify(e, ns); result() << '[' << i_it->source_location.get_property_id() << ']' << ' '; @@ -122,17 +124,20 @@ void static_analyzert::plain_text_report() result() << ": "; - if(simplified.is_true()) + if(e.is_true()) { - result() << "SUCCESS"; pass++; + result() << "Success"; + pass++; } - else if(simplified.is_false()) + else if(e.is_false()) { - result() << "FAILURE (if reachable)"; fail++; + result() << "Failure (if reachable)"; + fail++; } else { - result() << "UNKNOWN"; unknown++; + result() << "Unknown"; + unknown++; } result() << eom; @@ -141,7 +146,7 @@ void static_analyzert::plain_text_report() status() << '\n'; } - status() << "SUMMARY: " << pass << " pass, " << fail << " fail if reachable, " + status() << "Summary: " << pass << " pass, " << fail << " fail if reachable, " << unknown << " unknown\n"; } @@ -175,21 +180,19 @@ void static_analyzert::json_report() if(!i_it->is_assert()) continue; - exprt simplified=domain[i_it].domain_simplify(i_it->guard, ns); + exprt e(i_it->guard); + domain[i_it].ai_simplify(e, ns); json_objectt &j=json_result.push_back().make_object(); - if(simplified.is_true()) + if(e.is_true()) j["status"]=json_stringt("SUCCESS"); - else if(simplified.is_false()) + else if(e.is_false()) j["status"]=json_stringt("FAILURE (if reachable)"); else j["status"]=json_stringt("UNKNOWN"); - j["file"]=json_stringt(id2string(i_it->source_location.get_file())); - j["line"]=json_numbert(id2string(i_it->source_location.get_line())); - j["description"]=json_stringt(id2string( - i_it->source_location.get_comment())); + j["sourceLocation"]=json(i_it->source_location); } } status() << "Writing JSON report" << eom; @@ -226,13 +229,14 @@ void static_analyzert::xml_report() if(!i_it->is_assert()) continue; - exprt simplified=domain[i_it].domain_simplify(i_it->guard, ns); + exprt e(i_it->guard); + domain[i_it].ai_simplify(e, ns); xmlt &x=xml_result.new_element("result"); - if(simplified.is_true()) + if(e.is_true()) x.set_attribute("status", "SUCCESS"); - else if(simplified.is_false()) + else if(e.is_false()) x.set_attribute("status", "FAILURE (if reachable)"); else x.set_attribute("status", "UNKNOWN"); diff --git a/src/goto-analyzer/static_show_domain.cpp b/src/goto-analyzer/static_show_domain.cpp index 412c45e2bc2..036290e0d1d 100644 --- a/src/goto-analyzer/static_show_domain.cpp +++ b/src/goto-analyzer/static_show_domain.cpp @@ -6,7 +6,14 @@ Author: Martin Brain, martin.brain@cs.ox.ac.uk \*******************************************************************/ +//#define DEBUG + +#ifdef DEBUG +#include +#endif + #include +#include #include #include @@ -37,13 +44,17 @@ bool static_show_domain( message_handlert &message_handler, std::ostream &out) { - ai_baset *domain = NULL; + ai_baset *domain=nullptr; + 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(); + domain=new constant_propagator_ait(goto_model.goto_functions); + } else if(options.get_bool_option("intervals")) domain=new ait(); else if(options.get_bool_option("dependence-graph")) @@ -64,7 +75,7 @@ bool static_show_domain( #endif } - if(domain==NULL) + if(domain==nullptr) { messaget m(message_handler); m.status() << "Task / Interpreter / Domain combination not supported" diff --git a/src/goto-analyzer/static_show_domain.h b/src/goto-analyzer/static_show_domain.h index 3f0e7da3680..bedb1e7faed 100644 --- a/src/goto-analyzer/static_show_domain.h +++ b/src/goto-analyzer/static_show_domain.h @@ -12,7 +12,6 @@ Author: Martin Brain, martin.brain@cs.ox.ac.uk #include #include -#include #include #include diff --git a/src/goto-analyzer/static_simplifier.cpp b/src/goto-analyzer/static_simplifier.cpp index ce5bd8c511d..f1ac76189f7 100644 --- a/src/goto-analyzer/static_simplifier.cpp +++ b/src/goto-analyzer/static_simplifier.cpp @@ -52,7 +52,7 @@ class static_simplifiert:public messaget analyzerT domain; void simplify_program(void); - unsigned simplify_guard(goto_programt::instructionst::iterator &i_it); + bool simplify_guard(goto_programt::instructionst::iterator &i_it); }; /*******************************************************************\ @@ -96,30 +96,6 @@ bool static_simplifiert::operator()(void) 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 @@ -138,6 +114,13 @@ void static_simplifiert::simplify_program() { struct counterst { + counterst() : + asserts(0), + assumes(0), + gotos(0), + assigns(0), + function_calls(0) {} + unsigned asserts; unsigned assumes; unsigned gotos; @@ -145,8 +128,8 @@ void static_simplifiert::simplify_program() unsigned function_calls; }; - counterst simplified={0, 0, 0, 0, 0}; - counterst unmodified={0, 0, 0, 0, 0}; + counterst simplified; + counterst unmodified; Forall_goto_functions(f_it, goto_functions) { @@ -154,70 +137,66 @@ void static_simplifiert::simplify_program() { if(i_it->is_assert()) { - unsigned result=simplify_guard(i_it); - simplified.asserts+=result; - unmodified.asserts+=(1-result); + bool unchanged=domain[i_it].ai_simplify(i_it->guard, ns); + + if(unchanged) + unmodified.asserts++; + else + simplified.asserts++; } else if(i_it->is_assume()) { - unsigned result=simplify_guard(i_it); - simplified.assumes+=result; - unmodified.assumes+=(1-result); + bool unchanged=domain[i_it].ai_simplify(i_it->guard, ns); + + if(unchanged) + unmodified.assumes++; + else + simplified.assumes++; } else if(i_it->is_goto()) { - unsigned result=simplify_guard(i_it); - simplified.gotos+=result; - unmodified.gotos+=(1-result); + bool unchanged=domain[i_it].ai_simplify(i_it->guard, ns); + + if(unchanged) + unmodified.gotos++; + else + simplified.gotos++; } else if(i_it->is_assign()) { - code_assignt assign(to_code_assign(i_it->code)); + 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. - */ + // 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); + bool unchanged_lhs= + domain[i_it].ai_simplify(assign.lhs(), ns, true); - unsigned result=(simp_lhs==assign.lhs() && - simp_rhs==assign.rhs())?0:1; + bool unchanged_rhs= + domain[i_it].ai_simplify(assign.rhs(), ns, false); - simplified.assigns+=result; - unmodified.assigns+=(1-result); - - assign.lhs()=simp_lhs; - assign.rhs()=simp_rhs; - i_it->code=assign; + if(unchanged_lhs && unchanged_rhs) + unmodified.assigns++; + else + simplified.assigns++; } else if(i_it->is_function_call()) { - unsigned result=0; - code_function_callt fcall(to_code_function_call(i_it->code)); + 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; + bool unchanged=domain[i_it].ai_simplify(fcall.function(), ns); 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; + for(auto &o : args) + unchanged&=domain[i_it].ai_simplify(o, ns); - simplified.function_calls+=result; - unmodified.function_calls+=(1-result); + if(unchanged) + unmodified.function_calls++; + else + simplified.function_calls++; } } } @@ -225,14 +204,14 @@ void static_simplifiert::simplify_program() // Make sure the references are correct. goto_functions.update(); - status() << "SIMPLIFIED: " + status() << "Simplified: " << " assert: " << simplified.asserts << ", assume: " << simplified.assumes << ", goto: " << simplified.gotos << ", assigns: " << simplified.assigns << ", function calls: " << simplified.function_calls << "\n" - << "UNMODIFIED: " + << "Unmodified: " << " assert: " << unmodified.asserts << ", assume: " << unmodified.assumes << ", goto: " << unmodified.gotos diff --git a/src/goto-analyzer/static_simplifier.h b/src/goto-analyzer/static_simplifier.h index c9d4e156b7a..61bb77dad1d 100644 --- a/src/goto-analyzer/static_simplifier.h +++ b/src/goto-analyzer/static_simplifier.h @@ -12,7 +12,6 @@ Author: Lucas Cordeiro, lucas.cordeiro@cs.ox.ac.uk #include #include -#include #include #include diff --git a/src/goto-programs/remove_unreachable.cpp b/src/goto-programs/remove_unreachable.cpp index 8c87f205e96..ac6df4261a8 100644 --- a/src/goto-programs/remove_unreachable.cpp +++ b/src/goto-programs/remove_unreachable.cpp @@ -61,4 +61,3 @@ void remove_unreachable(goto_functionst &goto_functions) Forall_goto_functions(f_it, goto_functions) remove_unreachable(f_it->second.body); } - diff --git a/src/util/replace_symbol.cpp b/src/util/replace_symbol.cpp index 4dce48d8b93..c81a80fe7cc 100644 --- a/src/util/replace_symbol.cpp +++ b/src/util/replace_symbol.cpp @@ -74,9 +74,11 @@ Function: replace_symbolt::replace \*******************************************************************/ -bool replace_symbolt::replace(exprt &dest) const +bool replace_symbolt::replace( + exprt &dest, + const bool replace_with_const) const { - bool result=true; + bool result=true; // unchanged // first look at type @@ -89,33 +91,75 @@ bool replace_symbolt::replace(exprt &dest) const if(!have_to_replace(dest)) return result; - if(dest.id()==ID_symbol) + if(dest.id()==ID_member) + { + member_exprt &me=to_member_expr(dest); + + if(!replace(me.struct_op(), replace_with_const)) + result=false; + } + else if(dest.id()==ID_index) + { + index_exprt &ie=to_index_expr(dest); + + if(!replace(ie.array(), replace_with_const)) + result=false; + + if(!replace(ie.index())) + result=false; + } + else if(dest.id()==ID_address_of) + { + address_of_exprt &aoe=to_address_of_expr(dest); + + if(!replace(aoe.object(), false)) + result=false; + } + else if(dest.id()==ID_symbol) { + const symbol_exprt &s=to_symbol_expr(dest); + expr_mapt::const_iterator it= - expr_map.find(dest.get(ID_identifier)); + expr_map.find(s.get_identifier()); if(it!=expr_map.end()) { - dest=it->second; + const exprt &e=it->second; + + if(!replace_with_const && e.is_constant()) + return true; + + dest=e; + return false; } } - - Forall_operands(it, dest) - if(!replace(*it)) - result=false; + else + { + Forall_operands(it, dest) + if(!replace(*it)) + result=false; + } const irept &c_sizeof_type=dest.find(ID_C_c_sizeof_type); - if(c_sizeof_type.is_not_nil() && - !replace(static_cast(dest.add(ID_C_c_sizeof_type)))) - result=false; + if(c_sizeof_type.is_not_nil()) + { + typet &type=static_cast(dest.add(ID_C_c_sizeof_type)); + + if(!replace(type)) + result=false; + } const irept &va_arg_type=dest.find(ID_C_va_arg_type); - if(va_arg_type.is_not_nil() && - !replace(static_cast(dest.add(ID_C_va_arg_type)))) - result=false; + if(va_arg_type.is_not_nil()) + { + typet &type=static_cast(dest.add(ID_C_va_arg_type)); + + if(!replace(type)) + result=false; + } return result; } diff --git a/src/util/replace_symbol.h b/src/util/replace_symbol.h index f26c8eb067a..29b70a6f102 100644 --- a/src/util/replace_symbol.h +++ b/src/util/replace_symbol.h @@ -37,7 +37,10 @@ class replace_symbolt type_map.insert(std::pair(identifier, type)); } - virtual bool replace(exprt &dest) const; + virtual bool replace( + exprt &dest, + const bool replace_with_const=true) const; + virtual bool replace(typet &dest) const; void operator()(exprt &dest) const From 3e69c765700c9a0c156d80847a355f8543997bf7 Mon Sep 17 00:00:00 2001 From: Daniel Poetzl Date: Fri, 10 Feb 2017 12:34:54 +0000 Subject: [PATCH 15/24] option to ignore unresolved functions in the constant propagator --- src/analyses/constant_propagator.cpp | 32 +++++++++++++------ src/analyses/constant_propagator.h | 8 +++-- .../goto_analyzer_parse_options.cpp | 3 ++ .../goto_analyzer_parse_options.h | 3 +- src/goto-analyzer/static_show_domain.cpp | 6 ++-- 5 files changed, 38 insertions(+), 14 deletions(-) diff --git a/src/analyses/constant_propagator.cpp b/src/analyses/constant_propagator.cpp index 1cf928ac069..9e608aed82d 100644 --- a/src/analyses/constant_propagator.cpp +++ b/src/analyses/constant_propagator.cpp @@ -81,7 +81,15 @@ void constant_propagator_domaint::transform( const constant_propagator_ait *cp= dynamic_cast(&ai); - bool have_dirty=cp!=NULL; + + bool have_dirty=false; + bool ignore_unresolved_calls=false; + + if(cp!=nullptr) + { + have_dirty=true; + ignore_unresolved_calls=cp->ignore_unresolved_calls; + } assert(!values.is_bottom); @@ -152,10 +160,13 @@ void constant_propagator_domaint::transform( } else { - if(have_dirty) - values.set_dirty_to_top(cp->dirty, ns); - else - values.set_to_top(); + if(!ignore_unresolved_calls) + { + if(have_dirty) + values.set_dirty_to_top(cp->dirty, ns); + else + values.set_to_top(); + } } } else @@ -189,10 +200,13 @@ void constant_propagator_domaint::transform( assert(to==next); - if(have_dirty) - values.set_dirty_to_top(cp->dirty, ns); - else - values.set_to_top(); + if(!ignore_unresolved_calls) + { + if(have_dirty) + values.set_dirty_to_top(cp->dirty, ns); + else + values.set_to_top(); + } } } else if(from->is_end_function()) diff --git a/src/analyses/constant_propagator.h b/src/analyses/constant_propagator.h index c1791dd9cae..b1be918cdee 100644 --- a/src/analyses/constant_propagator.h +++ b/src/analyses/constant_propagator.h @@ -131,8 +131,11 @@ class constant_propagator_domaint:public ai_domain_baset class constant_propagator_ait:public ait { public: - explicit constant_propagator_ait(const goto_functionst &goto_functions) : - dirty(goto_functions) + explicit constant_propagator_ait( + const goto_functionst &goto_functions, + const bool ignore_unresolved_calls=false) : + dirty(goto_functions), + ignore_unresolved_calls(ignore_unresolved_calls) { } @@ -157,6 +160,7 @@ class constant_propagator_ait:public ait } dirtyt dirty; + bool ignore_unresolved_calls; protected: friend class constant_propagator_domaint; diff --git a/src/goto-analyzer/goto_analyzer_parse_options.cpp b/src/goto-analyzer/goto_analyzer_parse_options.cpp index 363680604a7..9111dbb9507 100644 --- a/src/goto-analyzer/goto_analyzer_parse_options.cpp +++ b/src/goto-analyzer/goto_analyzer_parse_options.cpp @@ -278,6 +278,9 @@ void goto_analyzer_parse_optionst::get_command_line_options(optionst &options) status() << "Domain defaults to --constants" << eom; options.set_option("constants", true); } + + if(cmdline.isset("ignore-unresolved-calls")) + options.set_option("ignore-unresolved-calls", true); } /*******************************************************************\ diff --git a/src/goto-analyzer/goto_analyzer_parse_options.h b/src/goto-analyzer/goto_analyzer_parse_options.h index d7d8c18fccc..36fca9b9d8c 100644 --- a/src/goto-analyzer/goto_analyzer_parse_options.h +++ b/src/goto-analyzer/goto_analyzer_parse_options.h @@ -47,7 +47,8 @@ class optionst; "(dependence-graph)" \ "(show)(verify)(simplify):" \ "(flow-sensitive)(concurrent)" \ - "(no-simplify-slicing)" + "(no-simplify-slicing)" \ + "(ignore-unresolved-calls)" class goto_analyzer_parse_optionst: public parse_options_baset, diff --git a/src/goto-analyzer/static_show_domain.cpp b/src/goto-analyzer/static_show_domain.cpp index 036290e0d1d..bf576f5a55c 100644 --- a/src/goto-analyzer/static_show_domain.cpp +++ b/src/goto-analyzer/static_show_domain.cpp @@ -52,8 +52,10 @@ bool static_show_domain( { if(options.get_bool_option("constants")) { - //domain=new ait(); - domain=new constant_propagator_ait(goto_model.goto_functions); + domain= + new constant_propagator_ait( + goto_model.goto_functions, + options.get_bool_option("ignore-unresolved-calls")); } else if(options.get_bool_option("intervals")) domain=new ait(); From 3202ac7b9a315653e46317ccace6296bc8edafbe Mon Sep 17 00:00:00 2001 From: Daniel Poetzl Date: Fri, 10 Feb 2017 12:51:25 +0000 Subject: [PATCH 16/24] use ai function output in goto-instrument --- .../goto_instrument_parse_options.cpp | 25 ++----------------- 1 file changed, 2 insertions(+), 23 deletions(-) diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp index 66421b2e1e1..a30fdd4c92a 100644 --- a/src/goto-instrument/goto_instrument_parse_options.cpp +++ b/src/goto-instrument/goto_instrument_parse_options.cpp @@ -507,17 +507,7 @@ int goto_instrument_parse_optionst::doit() reaching_definitions_analysist rd_analysis(ns); rd_analysis(goto_functions, ns); - forall_goto_functions(f_it, goto_functions) - { - if(f_it->second.body_available()) - { - std::cout << "////" << std::endl; - std::cout << "//// Function: " << f_it->first << std::endl; - std::cout << "////" << std::endl; - std::cout << std::endl; - rd_analysis.output(ns, f_it->second.body, std::cout); - } - } + rd_analysis.output(ns, goto_functions, std::cout); return 0; } @@ -530,18 +520,7 @@ int goto_instrument_parse_optionst::doit() dependence_grapht dependence_graph(ns); dependence_graph(goto_functions, ns); - forall_goto_functions(f_it, goto_functions) - { - if(f_it->second.body_available()) - { - std::cout << "////" << std::endl; - std::cout << "//// Function: " << f_it->first << std::endl; - std::cout << "////" << std::endl; - std::cout << std::endl; - dependence_graph.output(ns, f_it->second.body, std::cout); - } - } - + dependence_graph.output(ns, goto_functions, std::cout); dependence_graph.output_dot(std::cout); return 0; From e73e0dc352edafa406b3027f0151834505f4dddc Mon Sep 17 00:00:00 2001 From: Daniel Poetzl Date: Wed, 15 Feb 2017 17:09:53 +0000 Subject: [PATCH 17/24] more status output --- src/analyses/ai.cpp | 4 ++-- src/goto-analyzer/static_analyzer.cpp | 8 ++++++-- src/goto-analyzer/static_show_domain.cpp | 7 +++++-- src/goto-analyzer/static_simplifier.cpp | 6 ++++-- 4 files changed, 17 insertions(+), 8 deletions(-) diff --git a/src/analyses/ai.cpp b/src/analyses/ai.cpp index dc60f04067f..9efb4d8a241 100644 --- a/src/analyses/ai.cpp +++ b/src/analyses/ai.cpp @@ -57,7 +57,7 @@ xmlt ai_domain_baset::output_xml( { std::ostringstream out; output(out, ai, ns); - xmlt xml("domain"); + xmlt xml("abstract_state"); xml.data=out.str(); return xml; } @@ -185,7 +185,7 @@ jsont ai_baset::output_json( json_numbert(std::to_string(i_it->location_number)); location["sourceLocation"]= json_stringt(i_it->source_location.as_string()); - location["domain"]=find_state(i_it).output_json(*this, ns); + location["abstractState"]=find_state(i_it).output_json(*this, ns); // Ideally we need output_instruction_json std::ostringstream out; diff --git a/src/goto-analyzer/static_analyzer.cpp b/src/goto-analyzer/static_analyzer.cpp index e00eefc6050..9d23ee81407 100644 --- a/src/goto-analyzer/static_analyzer.cpp +++ b/src/goto-analyzer/static_analyzer.cpp @@ -66,9 +66,11 @@ Function: static_analyzert::operator() template bool static_analyzert::operator()() { - status() << "Performing analysis" << eom; + status() << "Computing abstract states" << eom; domain(goto_functions, ns); + status() << "Checking assertions" << eom; + if(options.get_bool_option("json")) json_report(); else if(options.get_bool_option("xml")) @@ -272,6 +274,9 @@ bool static_analyzer( message_handlert &message_handler, std::ostream &out) { + messaget m(message_handler); + m.status() << "Selecting abstract domain" << messaget::eom; + if(options.get_bool_option("flow-sensitive")) { if(options.get_bool_option("constants")) @@ -305,7 +310,6 @@ bool static_analyzer( #endif } - messaget m(message_handler); m.status() << "Task / Interpreter / Domain combination not supported" << messaget::eom; diff --git a/src/goto-analyzer/static_show_domain.cpp b/src/goto-analyzer/static_show_domain.cpp index bf576f5a55c..62139b8efc3 100644 --- a/src/goto-analyzer/static_show_domain.cpp +++ b/src/goto-analyzer/static_show_domain.cpp @@ -47,6 +47,9 @@ bool static_show_domain( ai_baset *domain=nullptr; namespacet ns(goto_model.symbol_table); + messaget m(message_handler); + + m.status() << "Selecting abstract domain" << messaget::eom; if(options.get_bool_option("flow-sensitive")) { @@ -79,15 +82,15 @@ bool static_show_domain( if(domain==nullptr) { - messaget m(message_handler); m.status() << "Task / Interpreter / Domain combination not supported" << messaget::eom; return true; } - // status() << "Performing analysis" << eom; + m.status() << "Computing abstract states" << messaget::eom; (*domain)(goto_model); + m.status() << "Outputting abstract states" << messaget::eom; if(options.get_bool_option("json")) out << domain->output_json(goto_model); diff --git a/src/goto-analyzer/static_simplifier.cpp b/src/goto-analyzer/static_simplifier.cpp index f1ac76189f7..b28e7501c0a 100644 --- a/src/goto-analyzer/static_simplifier.cpp +++ b/src/goto-analyzer/static_simplifier.cpp @@ -71,7 +71,7 @@ Function: static_simplifiert::operator() template bool static_simplifiert::operator()(void) { - status() << "Performing analysis" << eom; + status() << "Computing abstract states" << eom; domain(goto_functions, ns); status() << "Simplifying program" << eom; @@ -241,6 +241,9 @@ bool static_simplifier( message_handlert &message_handler, std::ostream &out) { + messaget m(message_handler); + m.status() << "Selecting abstract domain" << messaget::eom; + if(options.get_bool_option("flow-sensitive")) { if(options.get_bool_option("constants")) @@ -274,7 +277,6 @@ bool static_simplifier( #endif } - messaget m(message_handler); m.status() << "Task / Interpreter / Domain combination not supported" << messaget::eom; From fce4f71578665fdc08c8e9253dd81e06a473abbf Mon Sep 17 00:00:00 2001 From: Daniel Poetzl Date: Wed, 15 Feb 2017 17:16:02 +0000 Subject: [PATCH 18/24] constant propagator fix --- src/analyses/ai.h | 7 +++---- src/analyses/constant_propagator.cpp | 4 +++- 2 files changed, 6 insertions(+), 5 deletions(-) diff --git a/src/analyses/ai.h b/src/analyses/ai.h index 0ec78e13b21..5f64b52f1b3 100644 --- a/src/analyses/ai.h +++ b/src/analyses/ai.h @@ -40,9 +40,9 @@ class ai_domain_baset // how function calls are treated: // a) there is an edge from each call site to the function head - // b) there is an edge from the last instruction (END_FUNCTION) - // of the function to the instruction _following_ the call site - // (this also needs to set the LHS, if applicable) + // b) there is an edge from the last instruction (END_FUNCTION) of + // the function to the instruction _following_ the call site (this + // also needs to set the LHS, if applicable) virtual void transform( locationt from, @@ -208,7 +208,6 @@ class ai_baset return output_json(ns, goto_function.body, ""); } - virtual xmlt output_xml( const namespacet &ns, const goto_functionst &goto_functions) const; diff --git a/src/analyses/constant_propagator.cpp b/src/analyses/constant_propagator.cpp index 9e608aed82d..e90c0e6e979 100644 --- a/src/analyses/constant_propagator.cpp +++ b/src/analyses/constant_propagator.cpp @@ -91,7 +91,9 @@ void constant_propagator_domaint::transform( ignore_unresolved_calls=cp->ignore_unresolved_calls; } - assert(!values.is_bottom); + //assert(!values.is_bottom); + if(values.is_bottom) + return; if(from->is_decl()) { From 1ef5df065dc768d64d58a9727174a6011f035f85 Mon Sep 17 00:00:00 2001 From: Daniel Poetzl Date: Fri, 17 Feb 2017 16:22:32 +0000 Subject: [PATCH 19/24] add is_bottom() and is_top() to ai_domain_baset --- regression/Makefile | 1 - .../constant_propagation_16/main.c | 13 ++++++ .../constant_propagation_16/test.desc | 7 +++ src/analyses/ai.cpp | 7 ++- src/analyses/ai.h | 6 +++ src/analyses/constant_propagator.cpp | 6 ++- src/analyses/constant_propagator.h | 44 +++++++++++++------ src/analyses/custom_bitvector_analysis.h | 22 +++++++--- src/analyses/dependence_graph.h | 30 ++++++++++--- src/analyses/escape_analysis.h | 22 +++++++--- src/analyses/global_may_alias.h | 22 +++++++--- src/analyses/interval_domain.h | 29 +++++++----- src/analyses/invariant_set_domain.h | 20 ++++++--- src/analyses/is_threaded.cpp | 20 +++++++-- src/analyses/reaching_definitions.h | 26 ++++++++--- src/analyses/uninitialized_domain.h | 20 +++++++-- src/goto-analyzer/static_show_domain.cpp | 2 +- src/util/replace_symbol.h | 5 +++ 18 files changed, 233 insertions(+), 69 deletions(-) create mode 100644 regression/goto-analyzer/constant_propagation_16/main.c create mode 100644 regression/goto-analyzer/constant_propagation_16/test.desc diff --git a/regression/Makefile b/regression/Makefile index fef85ccc958..71e3494e073 100644 --- a/regression/Makefile +++ b/regression/Makefile @@ -19,4 +19,3 @@ clean: $(MAKE) -C "$$dir" clean; \ fi; \ done; - diff --git a/regression/goto-analyzer/constant_propagation_16/main.c b/regression/goto-analyzer/constant_propagation_16/main.c new file mode 100644 index 00000000000..22fbac6a427 --- /dev/null +++ b/regression/goto-analyzer/constant_propagation_16/main.c @@ -0,0 +1,13 @@ + +void func() +{ + while(1) {} +} + +int main() +{ + func(); + + 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..ef4ab9321a2 --- /dev/null +++ b/regression/goto-analyzer/constant_propagation_16/test.desc @@ -0,0 +1,7 @@ +CORE +main.c +--show --constants +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring diff --git a/src/analyses/ai.cpp b/src/analyses/ai.cpp index 9efb4d8a241..36991b63c96 100644 --- a/src/analyses/ai.cpp +++ b/src/analyses/ai.cpp @@ -572,7 +572,12 @@ bool ai_baset::do_function_call( assert(l_end->is_end_function()); // do edge from end of function to instruction after call - std::unique_ptr tmp_state(make_temporary_state(get_state(l_end))); + const statet &end_state=get_state(l_end); + + if(end_state.is_bottom()) + return false; // function exit point not reachable + + std::unique_ptr tmp_state(make_temporary_state(end_state)); tmp_state->transform(l_end, l_return, *this, ns); // Propagate those diff --git a/src/analyses/ai.h b/src/analyses/ai.h index 5f64b52f1b3..d7393c8d9ef 100644 --- a/src/analyses/ai.h +++ b/src/analyses/ai.h @@ -75,6 +75,12 @@ class ai_domain_baset // a reasonable entry-point state virtual void make_entry()=0; + virtual bool is_bottom() const=0; + + // the analysis doesn't use this, + // and domains may refuse to implement it. + virtual bool is_top() const=0; + // also add // // bool merge(const T &b, locationt from, locationt to); diff --git a/src/analyses/constant_propagator.cpp b/src/analyses/constant_propagator.cpp index e90c0e6e979..81d3fbb062c 100644 --- a/src/analyses/constant_propagator.cpp +++ b/src/analyses/constant_propagator.cpp @@ -79,6 +79,10 @@ void constant_propagator_domaint::transform( output(std::cout, ai, ns); #endif + // When the domain is used with constant_propagator_ait, + // information about dirty variables and config flags are + // available. Otherwise, the below will be null and we use default + // values const constant_propagator_ait *cp= dynamic_cast(&ai); @@ -91,7 +95,7 @@ void constant_propagator_domaint::transform( ignore_unresolved_calls=cp->ignore_unresolved_calls; } - //assert(!values.is_bottom); + // assert(!values.is_bottom); if(values.is_bottom) return; diff --git a/src/analyses/constant_propagator.h b/src/analyses/constant_propagator.h index b1be918cdee..c2118752294 100644 --- a/src/analyses/constant_propagator.h +++ b/src/analyses/constant_propagator.h @@ -22,12 +22,12 @@ class constant_propagator_domaint:public ai_domain_baset locationt from, locationt to, ai_baset &ai_base, - const namespacet &ns); + const namespacet &ns) final override; virtual void output( std::ostream &out, const ai_baset &ai_base, - const namespacet &ns) const; + const namespacet &ns) const override; bool merge( const constant_propagator_domaint &other, @@ -37,23 +37,33 @@ class constant_propagator_domaint:public ai_domain_baset virtual bool ai_simplify( exprt &condition, const namespacet &ns, - const bool lhs=false) const; + const bool lhs=false) const final override; - virtual void make_bottom() + virtual void make_bottom() final override { values.set_to_bottom(); } - virtual void make_top() + virtual void make_top() final override { values.set_to_top(); } - virtual void make_entry() + virtual void make_entry() final override { make_top(); } + virtual bool is_bottom() const final override + { + return values.is_bot(); + } + + virtual bool is_top() const final override + { + return values.is_top(); + } + struct valuest { public: @@ -68,27 +78,37 @@ class constant_propagator_domaint:public ai_domain_baset // set whole state - inline void set_to_bottom() + void set_to_bottom() { replace_const.clear(); is_bottom=true; } - inline void set_to_top() + void set_to_top() { replace_const.clear(); is_bottom=false; } + bool is_bot() const + { + return is_bottom && replace_const.empty(); + } + + bool is_top() const + { + return !is_bottom && replace_const.empty(); + } + // set single identifier - inline void set_to(const irep_idt &lhs, const exprt &rhs) + void set_to(const irep_idt &lhs, const exprt &rhs) { replace_const.expr_map[lhs]=rhs; is_bottom=false; } - inline void set_to(const symbol_exprt &lhs, const exprt &rhs) + void set_to(const symbol_exprt &lhs, const exprt &rhs) { set_to(lhs.get_identifier(), rhs); } @@ -143,8 +163,6 @@ class constant_propagator_ait:public ait goto_functionst &goto_functions, const namespacet &ns) : dirty(goto_functions) { - assert(false); - operator()(goto_functions, ns); replace(goto_functions, ns); } @@ -153,8 +171,6 @@ class constant_propagator_ait:public ait goto_functionst::goto_functiont &goto_function, const namespacet &ns) : dirty(goto_function) { - assert(false); - operator()(goto_function, ns); replace(goto_function, ns); } diff --git a/src/analyses/custom_bitvector_analysis.h b/src/analyses/custom_bitvector_analysis.h index ceb2ba691be..e141988761e 100644 --- a/src/analyses/custom_bitvector_analysis.h +++ b/src/analyses/custom_bitvector_analysis.h @@ -32,32 +32,44 @@ class custom_bitvector_domaint:public ai_domain_baset locationt from, locationt to, ai_baset &ai, - const namespacet &ns) final; + const namespacet &ns) final override; void output( std::ostream &out, const ai_baset &ai, - const namespacet &ns) const final; + const namespacet &ns) const final override; - void make_bottom() final + void make_bottom() final override { may_bits.clear(); must_bits.clear(); has_values=tvt(false); } - void make_top() final + void make_top() final override { may_bits.clear(); must_bits.clear(); has_values=tvt(true); } - void make_entry() final + void make_entry() final override { make_top(); } + bool is_bottom() const final override + { + assert(!has_values.is_false() || (may_bits.empty() && must_bits.empty())); + return has_values.is_false(); + } + + bool is_top() const final override + { + assert(!has_values.is_true() || (may_bits.empty() && must_bits.empty())); + return has_values.is_true(); + } + bool merge( const custom_bitvector_domaint &b, locationt from, diff --git a/src/analyses/dependence_graph.h b/src/analyses/dependence_graph.h index 70ae0df5ac4..e03a78df68e 100644 --- a/src/analyses/dependence_graph.h +++ b/src/analyses/dependence_graph.h @@ -86,16 +86,16 @@ class dep_graph_domaint:public ai_domain_baset goto_programt::const_targett from, goto_programt::const_targett to, ai_baset &ai, - const namespacet &ns) final; + const namespacet &ns) final override; void output( std::ostream &out, const ai_baset &ai, - const namespacet &ns) const final; + const namespacet &ns) const final override; jsont output_json( const ai_baset &ai, - const namespacet &ns) const; + const namespacet &ns) const override; void make_top() final override { @@ -106,7 +106,7 @@ class dep_graph_domaint:public ai_domain_baset data_deps.clear(); } - void make_bottom() final + void make_bottom() final override { assert(node_id!=std::numeric_limits::max()); @@ -115,11 +115,31 @@ class dep_graph_domaint:public ai_domain_baset data_deps.clear(); } - void make_entry() final + void make_entry() final override { make_top(); } + bool is_top() const final override + { + assert(node_id!=std::numeric_limits::max()); + + assert(!has_values.is_true() || + (control_deps.empty() && data_deps.empty())); + + return has_values.is_true(); + } + + bool is_bottom() const final override + { + assert(node_id!=std::numeric_limits::max()); + + assert(!has_values.is_false() || + (control_deps.empty() && data_deps.empty())); + + return has_values.is_false(); + } + void set_node_id(node_indext id) { node_id=id; diff --git a/src/analyses/escape_analysis.h b/src/analyses/escape_analysis.h index 948bed3fea8..834a9031a34 100644 --- a/src/analyses/escape_analysis.h +++ b/src/analyses/escape_analysis.h @@ -37,33 +37,45 @@ class escape_domaint:public ai_domain_baset locationt from, locationt to, ai_baset &ai, - const namespacet &ns) final; + const namespacet &ns) final override; void output( std::ostream &out, const ai_baset &ai, - const namespacet &ns) const final; + const namespacet &ns) const final override; bool merge( const escape_domaint &b, locationt from, locationt to); - void make_bottom() final + void make_bottom() final override { cleanup_map.clear(); aliases.clear(); has_values=tvt(false); } - void make_top() final + void make_top() final override { cleanup_map.clear(); aliases.clear(); has_values=tvt(true); } - void make_entry() final + bool is_bottom() const override final + { + assert(!has_values.is_false() || (cleanup_map.empty() && aliases.empty())); + return has_values.is_false(); + } + + bool is_top() const override final + { + assert(!has_values.is_true() || (cleanup_map.empty() && aliases.empty())); + return has_values.is_true(); + } + + void make_entry() override final { make_top(); } diff --git a/src/analyses/global_may_alias.h b/src/analyses/global_may_alias.h index 2f4a49b2d0a..9ed5b5ed78d 100644 --- a/src/analyses/global_may_alias.h +++ b/src/analyses/global_may_alias.h @@ -37,35 +37,47 @@ class global_may_alias_domaint:public ai_domain_baset locationt from, locationt to, ai_baset &ai, - const namespacet &ns) final; + const namespacet &ns) final override; void output( std::ostream &out, const ai_baset &ai, - const namespacet &ns) const final; + const namespacet &ns) const final override; bool merge( const global_may_alias_domaint &b, locationt from, locationt to); - void make_bottom() final + void make_bottom() final override { aliases.clear(); has_values=tvt(false); } - void make_top() final + void make_top() final override { aliases.clear(); has_values=tvt(true); } - void make_entry() final + void make_entry() final override { make_top(); } + bool is_bottom() const final override + { + assert(!has_values.is_false() || aliases.empty()); + return has_values.is_false(); + } + + bool is_top() const final override + { + assert(!has_values.is_true() || aliases.empty()); + return has_values.is_true(); + } + typedef union_find aliasest; aliasest aliases; diff --git a/src/analyses/interval_domain.h b/src/analyses/interval_domain.h index 237f4912752..d081ea2d9a8 100644 --- a/src/analyses/interval_domain.h +++ b/src/analyses/interval_domain.h @@ -33,12 +33,12 @@ class interval_domaint:public ai_domain_baset locationt from, locationt to, ai_baset &ai, - const namespacet &ns) final; + const namespacet &ns) final override; void output( std::ostream &out, const ai_baset &ai, - const namespacet &ns) const final; + const namespacet &ns) const override; bool join(const interval_domaint &b); @@ -51,7 +51,7 @@ class interval_domaint:public ai_domain_baset } // no states - void make_bottom() final + void make_bottom() final override { int_map.clear(); float_map.clear(); @@ -59,18 +59,30 @@ class interval_domaint:public ai_domain_baset } // all states - void make_top() final + void make_top() final override { int_map.clear(); float_map.clear(); bottom=false; } - void make_entry() final + void make_entry() final override { make_top(); } + bool is_bottom() const override final + { + // assert(!bottom || (int_map.empty() && float_map.empty())); + + return bottom; + } + + bool is_top() const override final + { + return !bottom && int_map.empty() && float_map.empty(); + } + exprt make_expression(const symbol_exprt &) const; void assume(const exprt &, const namespacet &); @@ -85,15 +97,10 @@ class interval_domaint:public ai_domain_baset return src.id()==ID_floatbv; } - bool is_bottom() const - { - return bottom; - } - virtual bool ai_simplify( exprt &condition, const namespacet &ns, - const bool lhs=false) const; + const bool lhs=false) const override final; protected: bool bottom; diff --git a/src/analyses/invariant_set_domain.h b/src/analyses/invariant_set_domain.h index 2e231524cbb..3031ac8d867 100644 --- a/src/analyses/invariant_set_domain.h +++ b/src/analyses/invariant_set_domain.h @@ -41,7 +41,7 @@ class invariant_set_domaint:public ai_domain_baset void output( std::ostream &out, const ai_baset &ai, - const namespacet &ns) const final + const namespacet &ns) const final override { if(has_values.is_known()) out << has_values.to_string() << '\n'; @@ -53,25 +53,35 @@ class invariant_set_domaint:public ai_domain_baset locationt from_l, locationt to_l, ai_baset &ai, - const namespacet &ns) final; + const namespacet &ns) final override; - void make_top() final + void make_top() final override { invariant_set.make_true(); has_values=tvt(true); } - void make_bottom() final + void make_bottom() final override { invariant_set.make_false(); has_values=tvt(false); } - void make_entry() final + void make_entry() final override { invariant_set.make_true(); has_values=tvt(true); } + + bool is_top() const override final + { + return has_values.is_true(); + } + + bool is_bottom() const override final + { + return has_values.is_false(); + } }; #endif // CPROVER_ANALYSES_INVARIANT_SET_DOMAIN_H diff --git a/src/analyses/is_threaded.cpp b/src/analyses/is_threaded.cpp index 905cd6b91ac..8d19315a83b 100644 --- a/src/analyses/is_threaded.cpp +++ b/src/analyses/is_threaded.cpp @@ -48,7 +48,7 @@ class is_threaded_domaint:public ai_domain_baset locationt from, locationt to, ai_baset &ai, - const namespacet &ns) final + const namespacet &ns) final override { // assert(reachable); @@ -59,23 +59,35 @@ class is_threaded_domaint:public ai_domain_baset is_threaded=true; } - void make_bottom() final + void make_bottom() final override { reachable=false; is_threaded=false; } - void make_top() final + void make_top() final override { reachable=true; is_threaded=true; } - void make_entry() final + void make_entry() final override { reachable=true; is_threaded=false; } + + bool is_bottom() const override final + { + assert(reachable || !is_threaded); + + return !reachable; + } + + bool is_top() const override final + { + return reachable && is_threaded; + } }; /*******************************************************************\ diff --git a/src/analyses/reaching_definitions.h b/src/analyses/reaching_definitions.h index a48a271a9a6..a08963bd379 100644 --- a/src/analyses/reaching_definitions.h +++ b/src/analyses/reaching_definitions.h @@ -112,17 +112,17 @@ class rd_range_domaint:public ai_domain_baset locationt from, locationt to, ai_baset &ai, - const namespacet &ns) final; + const namespacet &ns) final override; void output( std::ostream &out, const ai_baset &ai, - const namespacet &ns) const final + const namespacet &ns) const final override { output(out); } - void make_top() final + void make_top() final override { values.clear(); if(bv_container) @@ -130,7 +130,7 @@ class rd_range_domaint:public ai_domain_baset has_values=tvt(true); } - void make_bottom() final + void make_bottom() final override { values.clear(); if(bv_container) @@ -138,11 +138,23 @@ class rd_range_domaint:public ai_domain_baset has_values=tvt(false); } - void make_entry() final + void make_entry() final override { make_top(); } + bool is_top() const override final + { + assert(!has_values.is_true() || values.empty()); + return has_values.is_true(); + } + + bool is_bottom() const override final + { + assert(!has_values.is_false() || values.empty()); + return has_values.is_false(); + } + // returns true iff there is s.th. new bool merge( const rd_range_domaint &other, @@ -248,9 +260,9 @@ class reaching_definitions_analysist: virtual ~reaching_definitions_analysist(); virtual void initialize( - const goto_functionst &goto_functions); + const goto_functionst &goto_functions) override; - virtual statet &get_state(goto_programt::const_targett l) + virtual statet &get_state(goto_programt::const_targett l) override { statet &s=concurrency_aware_ait::get_state(l); diff --git a/src/analyses/uninitialized_domain.h b/src/analyses/uninitialized_domain.h index 6ca27f341b0..7323f08af80 100644 --- a/src/analyses/uninitialized_domain.h +++ b/src/analyses/uninitialized_domain.h @@ -30,30 +30,42 @@ class uninitialized_domaint:public ai_domain_baset locationt from, locationt to, ai_baset &ai, - const namespacet &ns) final; + const namespacet &ns) final override; void output( std::ostream &out, const ai_baset &ai, const namespacet &ns) const final; - void make_top() final + void make_top() final override { uninitialized.clear(); has_values=tvt(true); } - void make_bottom() final + void make_bottom() final override { uninitialized.clear(); has_values=tvt(false); } - void make_entry() final + void make_entry() final override { make_top(); } + bool is_top() const override final + { + assert(!has_values.is_true() || uninitialized.empty()); + return has_values.is_true(); + } + + bool is_bottom() const override final + { + assert(!has_values.is_false() || uninitialized.empty()); + return has_values.is_false(); + } + // returns true iff there is s.th. new bool merge( const uninitialized_domaint &other, diff --git a/src/goto-analyzer/static_show_domain.cpp b/src/goto-analyzer/static_show_domain.cpp index 62139b8efc3..b39e1a244af 100644 --- a/src/goto-analyzer/static_show_domain.cpp +++ b/src/goto-analyzer/static_show_domain.cpp @@ -6,7 +6,7 @@ Author: Martin Brain, martin.brain@cs.ox.ac.uk \*******************************************************************/ -//#define DEBUG +// #define DEBUG #ifdef DEBUG #include diff --git a/src/util/replace_symbol.h b/src/util/replace_symbol.h index 29b70a6f102..8a1e9b8e22e 100644 --- a/src/util/replace_symbol.h +++ b/src/util/replace_symbol.h @@ -59,6 +59,11 @@ class replace_symbolt type_map.clear(); } + bool empty() const + { + return expr_map.empty() && type_map.empty(); + } + replace_symbolt(); virtual ~replace_symbolt(); From ce789eeffc62589ff1528183c07d422d128c2ade Mon Sep 17 00:00:00 2001 From: Daniel Poetzl Date: Wed, 22 Feb 2017 20:37:52 +0000 Subject: [PATCH 20/24] enable failed tests printer for goto-analyzer regression tests --- regression/goto-analyzer/intervals_09/test.desc | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/regression/goto-analyzer/intervals_09/test.desc b/regression/goto-analyzer/intervals_09/test.desc index 8145fc369ca..83776b8ae34 100644 --- a/regression/goto-analyzer/intervals_09/test.desc +++ b/regression/goto-analyzer/intervals_09/test.desc @@ -1,4 +1,4 @@ -CORE +KNOWNBUG main.c --intervals --verify ^EXIT=0$ From 8f4aa80fbc96ca0f33155d0f71ae9625872160bb Mon Sep 17 00:00:00 2001 From: Daniel Poetzl Date: Fri, 24 Feb 2017 16:59:03 +0000 Subject: [PATCH 21/24] enable assertions in is_threadedt --- .../goto-analyzer/constant_propagation_01/main.c | 1 - .../constant_propagation_01/test.desc | 2 +- .../goto-analyzer/constant_propagation_02/main.c | 1 - .../constant_propagation_02/test.desc | 2 +- .../goto-analyzer/constant_propagation_03/main.c | 1 - .../goto-analyzer/constant_propagation_04/main.c | 1 - .../goto-analyzer/constant_propagation_05/main.c | 1 - .../goto-analyzer/constant_propagation_06/main.c | 1 - .../constant_propagation_06/test.desc | 2 +- .../goto-analyzer/constant_propagation_07/main.c | 2 +- .../goto-analyzer/constant_propagation_08/main.c | 2 +- .../goto-analyzer/constant_propagation_09/main.c | 2 +- .../goto-analyzer/constant_propagation_10/main.c | 2 +- .../goto-analyzer/constant_propagation_11/main.c | 2 +- .../goto-analyzer/constant_propagation_12/main.c | 2 +- .../goto-analyzer/constant_propagation_13/main.c | 2 +- .../goto-analyzer/constant_propagation_14/main.c | 2 +- .../goto-analyzer/constant_propagation_15/main.c | 2 +- .../goto-analyzer/constant_propagation_17/main.c | 14 ++++++++++++++ .../constant_propagation_17/test.desc | 8 ++++++++ regression/goto-analyzer/intervals_01/main.c | 1 - regression/goto-analyzer/intervals_01/test.desc | 16 ++++++++-------- regression/goto-analyzer/intervals_02/main.c | 1 - regression/goto-analyzer/intervals_03/main.c | 1 - regression/goto-analyzer/intervals_04/main.c | 1 - regression/goto-analyzer/intervals_05/main.c | 1 - regression/goto-analyzer/intervals_06/main.c | 1 - regression/goto-analyzer/intervals_07/main.c | 1 - regression/goto-analyzer/intervals_08/main.c | 1 - regression/goto-analyzer/intervals_09/main.c | 1 - regression/goto-analyzer/intervals_10/main.c | 1 - regression/goto-analyzer/intervals_11/main.c | 2 +- regression/goto-analyzer/intervals_12/main.c | 1 - regression/goto-analyzer/intervals_13/main.c | 1 - regression/goto-analyzer/intervals_13/test.desc | 16 ++++++++-------- regression/goto-analyzer/intervals_14/main.c | 1 - regression/goto-analyzer/intervals_15/main.c | 1 - regression/goto-analyzer/intervals_15/test.desc | 2 +- regression/goto-analyzer/intervals_16/main.c | 13 +++++++++++++ regression/goto-analyzer/intervals_16/test.desc | 8 ++++++++ src/analyses/is_threaded.cpp | 10 ++-------- 41 files changed, 75 insertions(+), 58 deletions(-) create mode 100644 regression/goto-analyzer/constant_propagation_17/main.c create mode 100644 regression/goto-analyzer/constant_propagation_17/test.desc create mode 100644 regression/goto-analyzer/intervals_16/main.c create mode 100644 regression/goto-analyzer/intervals_16/test.desc diff --git a/regression/goto-analyzer/constant_propagation_01/main.c b/regression/goto-analyzer/constant_propagation_01/main.c index 801a21535a9..6689d8d4562 100644 --- a/regression/goto-analyzer/constant_propagation_01/main.c +++ b/regression/goto-analyzer/constant_propagation_01/main.c @@ -1,4 +1,3 @@ -#include int main() { diff --git a/regression/goto-analyzer/constant_propagation_01/test.desc b/regression/goto-analyzer/constant_propagation_01/test.desc index f5aa9da5608..a4a79f28ab1 100644 --- a/regression/goto-analyzer/constant_propagation_01/test.desc +++ b/regression/goto-analyzer/constant_propagation_01/test.desc @@ -3,7 +3,7 @@ main.c --constants --simplify out.gb ^EXIT=0$ ^SIGNAL=0$ -^Simplified: assert: 1, assume: 0, goto: 2, assigns: 5, function calls: 0$ +^Simplified: assert: 1, assume: 0, goto: 1, 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/main.c b/regression/goto-analyzer/constant_propagation_02/main.c index ff139437bd8..db0c8dc3f3e 100644 --- a/regression/goto-analyzer/constant_propagation_02/main.c +++ b/regression/goto-analyzer/constant_propagation_02/main.c @@ -1,4 +1,3 @@ -#include int main() { diff --git a/regression/goto-analyzer/constant_propagation_02/test.desc b/regression/goto-analyzer/constant_propagation_02/test.desc index a7074d70c31..6a28820a4b0 100644 --- a/regression/goto-analyzer/constant_propagation_02/test.desc +++ b/regression/goto-analyzer/constant_propagation_02/test.desc @@ -3,7 +3,7 @@ main.c --constants --simplify out.gb ^EXIT=0$ ^SIGNAL=0$ -^Simplified: assert: 1, assume: 0, goto: 2, assigns: 6, function calls: 0$ +^Simplified: assert: 1, assume: 0, goto: 1, 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/main.c b/regression/goto-analyzer/constant_propagation_03/main.c index f08f6020d82..09a5434dead 100644 --- a/regression/goto-analyzer/constant_propagation_03/main.c +++ b/regression/goto-analyzer/constant_propagation_03/main.c @@ -1,4 +1,3 @@ -#include int main() { diff --git a/regression/goto-analyzer/constant_propagation_04/main.c b/regression/goto-analyzer/constant_propagation_04/main.c index ca003ccd2b8..2c6c3f39db1 100644 --- a/regression/goto-analyzer/constant_propagation_04/main.c +++ b/regression/goto-analyzer/constant_propagation_04/main.c @@ -1,4 +1,3 @@ -#include int main() { diff --git a/regression/goto-analyzer/constant_propagation_05/main.c b/regression/goto-analyzer/constant_propagation_05/main.c index 037fbbe0632..b740fc135c0 100644 --- a/regression/goto-analyzer/constant_propagation_05/main.c +++ b/regression/goto-analyzer/constant_propagation_05/main.c @@ -1,4 +1,3 @@ -#include int main() { diff --git a/regression/goto-analyzer/constant_propagation_06/main.c b/regression/goto-analyzer/constant_propagation_06/main.c index 40b04edfdd0..6290aa89e6b 100644 --- a/regression/goto-analyzer/constant_propagation_06/main.c +++ b/regression/goto-analyzer/constant_propagation_06/main.c @@ -1,4 +1,3 @@ -#include int main() { diff --git a/regression/goto-analyzer/constant_propagation_06/test.desc b/regression/goto-analyzer/constant_propagation_06/test.desc index da9d7778bbf..77a7349569f 100644 --- a/regression/goto-analyzer/constant_propagation_06/test.desc +++ b/regression/goto-analyzer/constant_propagation_06/test.desc @@ -3,6 +3,6 @@ main.c --constants --verify ^EXIT=0$ ^SIGNAL=0$ -^\[main.assertion.1\] file main.c line 12 function main, assertion i<51: Unknown$ +^\[main.assertion.1\] file main.c line 11 function main, assertion i\s*<\s*51: Unknown$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/constant_propagation_07/main.c b/regression/goto-analyzer/constant_propagation_07/main.c index f0dea39a424..1fb6fee8e15 100644 --- a/regression/goto-analyzer/constant_propagation_07/main.c +++ b/regression/goto-analyzer/constant_propagation_07/main.c @@ -1,4 +1,4 @@ -#include + int main() { signed int i; diff --git a/regression/goto-analyzer/constant_propagation_08/main.c b/regression/goto-analyzer/constant_propagation_08/main.c index 3022a4f0f19..295e23c636d 100644 --- a/regression/goto-analyzer/constant_propagation_08/main.c +++ b/regression/goto-analyzer/constant_propagation_08/main.c @@ -1,4 +1,4 @@ -#include + int main() { int a[2]; diff --git a/regression/goto-analyzer/constant_propagation_09/main.c b/regression/goto-analyzer/constant_propagation_09/main.c index 55ea9ac7fc2..9bd38159f67 100644 --- a/regression/goto-analyzer/constant_propagation_09/main.c +++ b/regression/goto-analyzer/constant_propagation_09/main.c @@ -1,4 +1,4 @@ -#include + int main() { int a[2]={0,0}; diff --git a/regression/goto-analyzer/constant_propagation_10/main.c b/regression/goto-analyzer/constant_propagation_10/main.c index ac5933e9177..217faa4c9a7 100644 --- a/regression/goto-analyzer/constant_propagation_10/main.c +++ b/regression/goto-analyzer/constant_propagation_10/main.c @@ -1,4 +1,4 @@ -#include + int main() { int a[2]={0,0}; diff --git a/regression/goto-analyzer/constant_propagation_11/main.c b/regression/goto-analyzer/constant_propagation_11/main.c index 124d1e30a20..cefa0c479ab 100644 --- a/regression/goto-analyzer/constant_propagation_11/main.c +++ b/regression/goto-analyzer/constant_propagation_11/main.c @@ -1,4 +1,4 @@ -#include + int main() { int a[2]={0,0}; diff --git a/regression/goto-analyzer/constant_propagation_12/main.c b/regression/goto-analyzer/constant_propagation_12/main.c index 9a7e7692d62..a8379b64712 100644 --- a/regression/goto-analyzer/constant_propagation_12/main.c +++ b/regression/goto-analyzer/constant_propagation_12/main.c @@ -1,4 +1,4 @@ -#include + int main() { int i=0, y; diff --git a/regression/goto-analyzer/constant_propagation_13/main.c b/regression/goto-analyzer/constant_propagation_13/main.c index 102cfd7f812..a4307c4d431 100644 --- a/regression/goto-analyzer/constant_propagation_13/main.c +++ b/regression/goto-analyzer/constant_propagation_13/main.c @@ -1,4 +1,4 @@ -#include + int main() { int i=0, y; diff --git a/regression/goto-analyzer/constant_propagation_14/main.c b/regression/goto-analyzer/constant_propagation_14/main.c index 8b426fe84b5..7a659b87c60 100644 --- a/regression/goto-analyzer/constant_propagation_14/main.c +++ b/regression/goto-analyzer/constant_propagation_14/main.c @@ -1,4 +1,4 @@ -#include + int main() { int a[2]={0,0}; diff --git a/regression/goto-analyzer/constant_propagation_15/main.c b/regression/goto-analyzer/constant_propagation_15/main.c index 6639f9b5c81..e3dd672831d 100644 --- a/regression/goto-analyzer/constant_propagation_15/main.c +++ b/regression/goto-analyzer/constant_propagation_15/main.c @@ -1,4 +1,4 @@ -#include + int main() { int a[2]={0,0}; diff --git a/regression/goto-analyzer/constant_propagation_17/main.c b/regression/goto-analyzer/constant_propagation_17/main.c new file mode 100644 index 00000000000..40b04edfdd0 --- /dev/null +++ b/regression/goto-analyzer/constant_propagation_17/main.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_17/test.desc b/regression/goto-analyzer/constant_propagation_17/test.desc new file mode 100644 index 00000000000..76dc0fca897 --- /dev/null +++ b/regression/goto-analyzer/constant_propagation_17/test.desc @@ -0,0 +1,8 @@ +CORE +main.c +--constants --verify +^EXIT=0$ +^SIGNAL=0$ +^\[main.assertion.1\] file main.c line 12 function main, assertion i\s*<\s*51: (Unknown|Failure \(if reachable\))$ +-- +^warning: ignoring diff --git a/regression/goto-analyzer/intervals_01/main.c b/regression/goto-analyzer/intervals_01/main.c index ce6294d362c..aeb37b99e07 100644 --- a/regression/goto-analyzer/intervals_01/main.c +++ b/regression/goto-analyzer/intervals_01/main.c @@ -1,4 +1,3 @@ -#include int main() { diff --git a/regression/goto-analyzer/intervals_01/test.desc b/regression/goto-analyzer/intervals_01/test.desc index e90c4aaeda6..af3180985b5 100644 --- a/regression/goto-analyzer/intervals_01/test.desc +++ b/regression/goto-analyzer/intervals_01/test.desc @@ -3,13 +3,13 @@ main.c --intervals --verify ^EXIT=0$ ^SIGNAL=0$ -^\[main.assertion.1\] file main.c line 8 function main, assertion i>=10: Success$ -^\[main.assertion.2\] file main.c line 11 function main, assertion i!=30: Success$ -^\[main.assertion.3\] file main.c line 14 function main, assertion i!=15: Unknown$ -^\[main.assertion.4\] file main.c line 17 function main, assertion 0: Success$ -^\[main.assertion.5\] file main.c line 20 function main, assertion j>=10: Success$ -^\[main.assertion.6\] file main.c line 23 function main, assertion i>=j: Unknown$ -^\[main.assertion.7\] file main.c line 26 function main, assertion i>=11: Success$ -^\[main.assertion.8\] file main.c line 29 function main, assertion j<100: Success$ +^\[main.assertion.1\] file main.c line 7 function main, assertion i\s*>=\s*10: Success$ +^\[main.assertion.2\] file main.c line 10 function main, assertion i\s*!=\s*30: Success$ +^\[main.assertion.3\] file main.c line 13 function main, assertion i\s*!=\s*15: Unknown$ +^\[main.assertion.4\] file main.c line 16 function main, assertion 0: Success$ +^\[main.assertion.5\] file main.c line 19 function main, assertion j\s*>=\s*10: Success$ +^\[main.assertion.6\] file main.c line 22 function main, assertion i\s*>=\s*j: Unknown$ +^\[main.assertion.7\] file main.c line 25 function main, assertion i\s*>=\s*11: Success$ +^\[main.assertion.8]\ file main.c line 28 function main, assertion j\s*<\s*100: Success$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/intervals_02/main.c b/regression/goto-analyzer/intervals_02/main.c index 755d36df82c..00659353325 100644 --- a/regression/goto-analyzer/intervals_02/main.c +++ b/regression/goto-analyzer/intervals_02/main.c @@ -1,4 +1,3 @@ -#include int main(){ int x; diff --git a/regression/goto-analyzer/intervals_03/main.c b/regression/goto-analyzer/intervals_03/main.c index bbaa3ce4e1e..de8c1eead32 100644 --- a/regression/goto-analyzer/intervals_03/main.c +++ b/regression/goto-analyzer/intervals_03/main.c @@ -1,4 +1,3 @@ -#include int main(){ int x; diff --git a/regression/goto-analyzer/intervals_04/main.c b/regression/goto-analyzer/intervals_04/main.c index 790a5f1379f..1ca11e32143 100644 --- a/regression/goto-analyzer/intervals_04/main.c +++ b/regression/goto-analyzer/intervals_04/main.c @@ -1,4 +1,3 @@ -//#include int main() { diff --git a/regression/goto-analyzer/intervals_05/main.c b/regression/goto-analyzer/intervals_05/main.c index ed19ba71590..2cd79130dc9 100644 --- a/regression/goto-analyzer/intervals_05/main.c +++ b/regression/goto-analyzer/intervals_05/main.c @@ -1,4 +1,3 @@ -//#include int main() { diff --git a/regression/goto-analyzer/intervals_06/main.c b/regression/goto-analyzer/intervals_06/main.c index e93240e7573..0e8a1f37c13 100644 --- a/regression/goto-analyzer/intervals_06/main.c +++ b/regression/goto-analyzer/intervals_06/main.c @@ -1,4 +1,3 @@ -#include int main(){ int x; diff --git a/regression/goto-analyzer/intervals_07/main.c b/regression/goto-analyzer/intervals_07/main.c index c893c413ad5..75da9413b97 100644 --- a/regression/goto-analyzer/intervals_07/main.c +++ b/regression/goto-analyzer/intervals_07/main.c @@ -1,4 +1,3 @@ -#include int main(){ int x; diff --git a/regression/goto-analyzer/intervals_08/main.c b/regression/goto-analyzer/intervals_08/main.c index 4128ac07ce5..3bcb7fe69c7 100644 --- a/regression/goto-analyzer/intervals_08/main.c +++ b/regression/goto-analyzer/intervals_08/main.c @@ -1,4 +1,3 @@ -#include int main(){ int x; diff --git a/regression/goto-analyzer/intervals_09/main.c b/regression/goto-analyzer/intervals_09/main.c index 27739c7aa28..73b8e73dc85 100644 --- a/regression/goto-analyzer/intervals_09/main.c +++ b/regression/goto-analyzer/intervals_09/main.c @@ -1,4 +1,3 @@ -#include int main() { diff --git a/regression/goto-analyzer/intervals_10/main.c b/regression/goto-analyzer/intervals_10/main.c index b27cc6f2001..b245b3f5b7c 100644 --- a/regression/goto-analyzer/intervals_10/main.c +++ b/regression/goto-analyzer/intervals_10/main.c @@ -1,4 +1,3 @@ -#include int main() { diff --git a/regression/goto-analyzer/intervals_11/main.c b/regression/goto-analyzer/intervals_11/main.c index 2f061cd554d..a6496ef764d 100644 --- a/regression/goto-analyzer/intervals_11/main.c +++ b/regression/goto-analyzer/intervals_11/main.c @@ -1,4 +1,4 @@ -#include + const int xLen = 10; const int Alen = 2; const int Blen = 1; diff --git a/regression/goto-analyzer/intervals_12/main.c b/regression/goto-analyzer/intervals_12/main.c index 15d865adf80..506e118f898 100644 --- a/regression/goto-analyzer/intervals_12/main.c +++ b/regression/goto-analyzer/intervals_12/main.c @@ -1,4 +1,3 @@ -#include int main (void) { int i; diff --git a/regression/goto-analyzer/intervals_13/main.c b/regression/goto-analyzer/intervals_13/main.c index d1d29427250..b631969e8f6 100644 --- a/regression/goto-analyzer/intervals_13/main.c +++ b/regression/goto-analyzer/intervals_13/main.c @@ -1,4 +1,3 @@ -#include int main() { diff --git a/regression/goto-analyzer/intervals_13/test.desc b/regression/goto-analyzer/intervals_13/test.desc index e90c4aaeda6..8d9720faf63 100644 --- a/regression/goto-analyzer/intervals_13/test.desc +++ b/regression/goto-analyzer/intervals_13/test.desc @@ -3,13 +3,13 @@ main.c --intervals --verify ^EXIT=0$ ^SIGNAL=0$ -^\[main.assertion.1\] file main.c line 8 function main, assertion i>=10: Success$ -^\[main.assertion.2\] file main.c line 11 function main, assertion i!=30: Success$ -^\[main.assertion.3\] file main.c line 14 function main, assertion i!=15: Unknown$ -^\[main.assertion.4\] file main.c line 17 function main, assertion 0: Success$ -^\[main.assertion.5\] file main.c line 20 function main, assertion j>=10: Success$ -^\[main.assertion.6\] file main.c line 23 function main, assertion i>=j: Unknown$ -^\[main.assertion.7\] file main.c line 26 function main, assertion i>=11: Success$ -^\[main.assertion.8\] file main.c line 29 function main, assertion j<100: Success$ +^\[main.assertion.1\] file main.c line 7 function main, assertion i\s*>=\s*10: Success$ +^\[main.assertion.2\] file main.c line 10 function main, assertion i\s*!=\s*30: Success$ +^\[main.assertion.3\] file main.c line 13 function main, assertion i\s*!=\s*15: Unknown$ +^\[main.assertion.4\] file main.c line 16 function main, assertion 0: Success$ +^\[main.assertion.5\] file main.c line 19 function main, assertion j\s*>=\s*10: Success$ +^\[main.assertion.6\] file main.c line 22 function main, assertion i\s*>=\s*j: Unknown$ +^\[main.assertion.7\] file main.c line 25 function main, assertion i\s*>=\s*11: Success$ +^\[main.assertion.8\] file main.c line 28 function main, assertion j\s*<\s*100: Success$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/intervals_14/main.c b/regression/goto-analyzer/intervals_14/main.c index 3909e3889e4..7e4d53d5e06 100644 --- a/regression/goto-analyzer/intervals_14/main.c +++ b/regression/goto-analyzer/intervals_14/main.c @@ -1,4 +1,3 @@ -#include int main() { diff --git a/regression/goto-analyzer/intervals_15/main.c b/regression/goto-analyzer/intervals_15/main.c index 002e9063228..52ef248b772 100644 --- a/regression/goto-analyzer/intervals_15/main.c +++ b/regression/goto-analyzer/intervals_15/main.c @@ -1,4 +1,3 @@ -#include int main() { diff --git a/regression/goto-analyzer/intervals_15/test.desc b/regression/goto-analyzer/intervals_15/test.desc index 7d3bae09250..e61667afcd4 100644 --- a/regression/goto-analyzer/intervals_15/test.desc +++ b/regression/goto-analyzer/intervals_15/test.desc @@ -3,6 +3,6 @@ main.c --intervals --verify ^EXIT=0$ ^SIGNAL=0$ -^\[main.assertion.1\] file main.c line 12 function main, assertion j<52: Unknown$ +^\[main.assertion.1\] file main.c line 11 function main, assertion j\s*<\s*52: Unknown$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/intervals_16/main.c b/regression/goto-analyzer/intervals_16/main.c new file mode 100644 index 00000000000..52ef248b772 --- /dev/null +++ b/regression/goto-analyzer/intervals_16/main.c @@ -0,0 +1,13 @@ + +int main() +{ + int i=0, j=2; + + while (i<=50) + { + i++; + j++; + } + assert(j<52); +} + diff --git a/regression/goto-analyzer/intervals_16/test.desc b/regression/goto-analyzer/intervals_16/test.desc new file mode 100644 index 00000000000..c23e2bcf4f5 --- /dev/null +++ b/regression/goto-analyzer/intervals_16/test.desc @@ -0,0 +1,8 @@ +CORE +main.c +--intervals --verify +^EXIT=0$ +^SIGNAL=0$ +^\[main.assertion.1\] file main.c line 11 function main, assertion j\s*<\s*52: (Unknown|Failure \(if reachable\))$ +-- +^warning: ignoring diff --git a/src/analyses/is_threaded.cpp b/src/analyses/is_threaded.cpp index 8d19315a83b..9567b343517 100644 --- a/src/analyses/is_threaded.cpp +++ b/src/analyses/is_threaded.cpp @@ -29,10 +29,7 @@ class is_threaded_domaint:public ai_domain_baset locationt from, locationt to) { - // assert(src.reachable); - - if(!src.reachable) - return false; + assert(src.reachable); bool old_reachable=reachable; bool old_is_threaded=is_threaded; @@ -50,10 +47,7 @@ class is_threaded_domaint:public ai_domain_baset ai_baset &ai, const namespacet &ns) final override { - // assert(reachable); - - if(!reachable) - return; + assert(reachable); if(from->is_start_thread()) is_threaded=true; From 58bfe6db6a47dc5e021be762030e7706baa54537 Mon Sep 17 00:00:00 2001 From: Daniel Poetzl Date: Tue, 4 Apr 2017 15:06:50 +0100 Subject: [PATCH 22/24] fixed merging issue --- src/goto-analyzer/goto_analyzer_parse_options.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/goto-analyzer/goto_analyzer_parse_options.cpp b/src/goto-analyzer/goto_analyzer_parse_options.cpp index 9111dbb9507..641f58f6a58 100644 --- a/src/goto-analyzer/goto_analyzer_parse_options.cpp +++ b/src/goto-analyzer/goto_analyzer_parse_options.cpp @@ -324,7 +324,7 @@ int goto_analyzer_parse_optionst::doit() goto_model.set_message_handler(get_message_handler()); - if(goto_model(cmdline.args)) + if(goto_model(cmdline)) return 6; goto_functionst::function_mapt::const_iterator f_it= From fcd0c0a2b1b2c5f44bf843e7aeb5699693a813de Mon Sep 17 00:00:00 2001 From: Daniel Poetzl Date: Wed, 5 Apr 2017 13:48:17 +0100 Subject: [PATCH 23/24] fixed compilation error in debug mode --- src/analyses/interval_domain.cpp | 5 ----- 1 file changed, 5 deletions(-) diff --git a/src/analyses/interval_domain.cpp b/src/analyses/interval_domain.cpp index 43d80acd78d..18befbfe182 100644 --- a/src/analyses/interval_domain.cpp +++ b/src/analyses/interval_domain.cpp @@ -561,11 +561,6 @@ bool interval_domaint::ai_simplify( 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)) { unchanged=condition.is_true(); From e183ffb44925619da76c6d026029e34053c8a0c1 Mon Sep 17 00:00:00 2001 From: Daniel Poetzl Date: Fri, 5 May 2017 13:01:17 +0100 Subject: [PATCH 24/24] fixed merging issue --- src/analyses/Makefile | 1 - 1 file changed, 1 deletion(-) diff --git a/src/analyses/Makefile b/src/analyses/Makefile index 690b119e83c..9be0609687f 100644 --- a/src/analyses/Makefile +++ b/src/analyses/Makefile @@ -22,7 +22,6 @@ SRC = ai.cpp \ locals.cpp \ natural_loops.cpp \ reaching_definitions.cpp \ - replace_symbol_ext.cpp \ static_analysis.cpp \ uninitialized_domain.cpp \ # Empty last line