diff --git a/regression/goto-instrument/data-flow1/main.c b/regression/goto-instrument/data-flow1/main.c new file mode 100644 index 00000000000..1aecb44916d --- /dev/null +++ b/regression/goto-instrument/data-flow1/main.c @@ -0,0 +1,18 @@ +int d=0; + +void f1() +{ + d=1; +} + +int main() +{ + int x=2; + int y=3; + + f1(); + + if(x && y && d) + return 0; +} + diff --git a/regression/goto-instrument/data-flow1/test.desc b/regression/goto-instrument/data-flow1/test.desc new file mode 100644 index 00000000000..e7413631c0f --- /dev/null +++ b/regression/goto-instrument/data-flow1/test.desc @@ -0,0 +1,8 @@ +CORE +main.c +"--show-dependence-graph" +^EXIT=0$ +^SIGNAL=0$ +Data dependencies: .*33.* +-- +^warning: ignoring diff --git a/src/analyses/ai.cpp b/src/analyses/ai.cpp index f98a3f807ae..0e95e233e44 100644 --- a/src/analyses/ai.cpp +++ b/src/analyses/ai.cpp @@ -120,8 +120,7 @@ Function: ai_baset::entry_state void ai_baset::entry_state(const goto_programt &goto_program) { - // The first instruction of 'goto_program' is the entry point, - // and we make that 'top'. + // The first instruction of 'goto_program' is the entry point get_state(goto_program.instructions.begin()).make_entry(); } @@ -226,9 +225,11 @@ bool ai_baset::fixedpoint( { working_sett working_set; - // We will put all locations at least once into the working set. - forall_goto_program_instructions(i_it, goto_program) - put_in_working_set(working_set, i_it); + // Put the first location in the working set + if(!goto_program.empty()) + put_in_working_set( + working_set, + goto_program.instructions.begin()); bool new_data=false; diff --git a/src/analyses/custom_bitvector_analysis.cpp b/src/analyses/custom_bitvector_analysis.cpp index 883ea1ef188..878a7037320 100644 --- a/src/analyses/custom_bitvector_analysis.cpp +++ b/src/analyses/custom_bitvector_analysis.cpp @@ -326,6 +326,8 @@ void custom_bitvector_domaint::transform( ai_baset &ai, const namespacet &ns) { + if(has_values.is_false()) return; + // upcast of ai custom_bitvector_analysist &cba= static_cast(ai); @@ -565,8 +567,11 @@ void custom_bitvector_domaint::output( const ai_baset &ai, const namespacet &ns) const { - if(is_bottom) - out << "BOTTOM\n"; + if(has_values.is_known()) + { + out << has_values.to_string() << '\n'; + return; + } const custom_bitvector_analysist &cba= static_cast(ai); @@ -625,10 +630,10 @@ bool custom_bitvector_domaint::merge( locationt from, locationt to) { - if(b.is_bottom) + if(b.has_values.is_false()) return false; // no change - if(is_bottom) + if(has_values.is_false()) { *this=b; return true; // change @@ -858,7 +863,7 @@ void custom_bitvector_analysist::check( if(!custom_bitvector_domaint::has_get_must_or_may(i_it->guard)) continue; - if(operator[](i_it).is_bottom) continue; + if(operator[](i_it).has_values.is_false()) continue; exprt tmp=eval(i_it->guard, i_it); result=simplify_expr(tmp, ns); diff --git a/src/analyses/custom_bitvector_analysis.h b/src/analyses/custom_bitvector_analysis.h index d964f34f3ec..3cdf0895ddb 100644 --- a/src/analyses/custom_bitvector_analysis.h +++ b/src/analyses/custom_bitvector_analysis.h @@ -10,6 +10,7 @@ Author: Daniel Kroening, kroening@kroening.com #define CPROVER_ANALYSES_CUSTOM_BITVECTOR_ANALYSIS_H #include +#include #include "ai.h" #include "local_may_alias.h" @@ -42,20 +43,19 @@ class custom_bitvector_domaint:public ai_domain_baset { may_bits.clear(); must_bits.clear(); - is_bottom=true; + has_values=tvt(false); } void make_top() final override { - // We don't have a proper top, and refuse to do this. - assert(false); + may_bits.clear(); + must_bits.clear(); + has_values=tvt(true); } void make_entry() final override { - may_bits.clear(); - must_bits.clear(); - is_bottom=false; + make_top(); } bool merge( @@ -90,9 +90,9 @@ class custom_bitvector_domaint:public ai_domain_baset vectorst get_rhs(const exprt &) const; vectorst get_rhs(const irep_idt &) const; - bool is_bottom; + tvt has_values; - custom_bitvector_domaint():is_bottom(true) + custom_bitvector_domaint():has_values(true) { } diff --git a/src/analyses/dependence_graph.cpp b/src/analyses/dependence_graph.cpp index c5ff3153ca5..0114058e0dc 100644 --- a/src/analyses/dependence_graph.cpp +++ b/src/analyses/dependence_graph.cpp @@ -32,7 +32,8 @@ bool dep_graph_domaint::merge( goto_programt::const_targett from, goto_programt::const_targett to) { - bool change=false; + bool changed=has_values.is_false(); + has_values=tvt::unknown(); depst::iterator it=control_deps.begin(); for(depst::const_iterator ito=src.control_deps.begin(); @@ -44,7 +45,7 @@ bool dep_graph_domaint::merge( if(it==control_deps.end() || *ito<*it) { control_deps.insert(it, *ito); - change=true; + changed=true; } else if(it!=control_deps.end()) ++it; @@ -60,13 +61,13 @@ bool dep_graph_domaint::merge( if(it==data_deps.end() || *ito<*it) { data_deps.insert(it, *ito); - change=true; + changed=true; } else if(it!=data_deps.end()) ++it; } - return change; + return changed; } /*******************************************************************\ diff --git a/src/analyses/dependence_graph.h b/src/analyses/dependence_graph.h index e783fae8fda..15c0828fef6 100644 --- a/src/analyses/dependence_graph.h +++ b/src/analyses/dependence_graph.h @@ -13,6 +13,7 @@ Date: August 2013 #define CPROVER_ANALYSES_DEPENDENCE_GRAPH_H #include +#include #include "ai.h" #include "cfg_dominators.h" @@ -70,6 +71,7 @@ class dep_graph_domaint:public ai_domain_baset typedef graph::node_indext node_indext; dep_graph_domaint(): + has_values(false), node_id(std::numeric_limits::max()) { } @@ -89,20 +91,22 @@ class dep_graph_domaint:public ai_domain_baset std::ostream &out, const ai_baset &ai, const namespacet &ns) const final override; - + void make_top() final override { + has_values=tvt(true); node_id=std::numeric_limits::max(); } void make_bottom() final override { + has_values=tvt(false); node_id=std::numeric_limits::max(); } void make_entry() final override { - node_id=std::numeric_limits::max(); + make_top(); } void set_node_id(node_indext id) @@ -117,6 +121,7 @@ class dep_graph_domaint:public ai_domain_baset } protected: + tvt has_values; node_indext node_id; typedef std::set depst; diff --git a/src/analyses/escape_analysis.cpp b/src/analyses/escape_analysis.cpp index 7d610c3198a..711dd35d170 100644 --- a/src/analyses/escape_analysis.cpp +++ b/src/analyses/escape_analysis.cpp @@ -266,6 +266,8 @@ void escape_domaint::transform( ai_baset &ai, const namespacet &ns) { + if(has_values.is_false()) return; + // upcast of ai //escape_analysist &ea= // static_cast(ai); @@ -364,9 +366,9 @@ void escape_domaint::output( const ai_baset &ai, const namespacet &ns) const { - if(is_bottom) + if(has_values.is_known()) { - out << "BOTTOM\n"; + out << has_values.to_string() << '\n'; return; } @@ -422,10 +424,10 @@ bool escape_domaint::merge( locationt from, locationt to) { - if(b.is_bottom) + if(b.has_values.is_false()) return false; // no change - if(is_bottom) + if(has_values.is_false()) { *this=b; return true; // change diff --git a/src/analyses/escape_analysis.h b/src/analyses/escape_analysis.h index c485a01140e..3cccec91a30 100644 --- a/src/analyses/escape_analysis.h +++ b/src/analyses/escape_analysis.h @@ -11,6 +11,7 @@ Author: Daniel Kroening, kroening@kroening.com #define CPROVER_ANALYSES_ESCAPE_ANALYSIS_H #include +#include #include #include "ai.h" @@ -28,7 +29,7 @@ class escape_analysist; class escape_domaint:public ai_domain_baset { public: - escape_domaint():is_bottom(true) + escape_domaint():has_values(false) { } @@ -51,19 +52,20 @@ class escape_domaint:public ai_domain_baset void make_bottom() override final { cleanup_map.clear(); - is_bottom=true; + aliases.clear(); + has_values=tvt(false); } void make_top() override final { - // We don't have a proper top. - assert(false); + cleanup_map.clear(); + aliases.clear(); + has_values=tvt(true); } - + void make_entry() override final { - cleanup_map.clear(); - is_bottom=false; + make_top(); } typedef union_find aliasest; @@ -80,9 +82,9 @@ class escape_domaint:public ai_domain_baset typedef std::map cleanup_mapt; cleanup_mapt cleanup_map; - bool is_bottom; - protected: + tvt has_values; + void assign_lhs_cleanup(const exprt &, const std::set &); void get_rhs_cleanup(const exprt &, std::set &); void assign_lhs_aliases(const exprt &, const std::set &); diff --git a/src/analyses/global_may_alias.cpp b/src/analyses/global_may_alias.cpp index 0e3e190aa29..f89530d3ed8 100644 --- a/src/analyses/global_may_alias.cpp +++ b/src/analyses/global_may_alias.cpp @@ -130,6 +130,8 @@ void global_may_alias_domaint::transform( ai_baset &ai, const namespacet &ns) { + if(has_values.is_false()) return; + const goto_programt::instructiont &instruction=*from; switch(instruction.type) @@ -179,6 +181,12 @@ void global_may_alias_domaint::output( const ai_baset &ai, const namespacet &ns) const { + if(has_values.is_known()) + { + out << has_values.to_string() << '\n'; + return; + } + for(aliasest::const_iterator a_it1=aliases.begin(); a_it1!=aliases.end(); a_it1++) @@ -218,7 +226,8 @@ bool global_may_alias_domaint::merge( locationt from, locationt to) { - bool changed=false; + bool changed=has_values.is_false(); + has_values=tvt::unknown(); // do union for(aliasest::const_iterator it=b.aliases.begin(); diff --git a/src/analyses/global_may_alias.h b/src/analyses/global_may_alias.h index 0b4d178baab..69eaa22404b 100644 --- a/src/analyses/global_may_alias.h +++ b/src/analyses/global_may_alias.h @@ -11,6 +11,7 @@ Author: Daniel Kroening, kroening@kroening.com #define CPROVER_ANALYSES_GLOBAL_MAY_ALIAS_H #include +#include #include #include "ai.h" @@ -28,6 +29,10 @@ class global_may_alias_analysist; class global_may_alias_domaint:public ai_domain_baset { public: + global_may_alias_domaint():has_values(false) + { + } + void transform( locationt from, locationt to, @@ -47,23 +52,26 @@ class global_may_alias_domaint:public ai_domain_baset void make_bottom() final override { aliases.clear(); + has_values=tvt(false); } void make_top() final override { - // We don't have a proper top. - assert(false); + aliases.clear(); + has_values=tvt(true); } void make_entry() final override { - aliases.clear(); + make_top(); } typedef union_find aliasest; aliasest aliases; protected: + tvt has_values; + void assign_lhs_aliases(const exprt &, const std::set &); void get_rhs_aliases(const exprt &, std::set &); void get_rhs_aliases_address_of(const exprt &, std::set &); diff --git a/src/analyses/invariant_set_domain.h b/src/analyses/invariant_set_domain.h index 2190b0503b4..99923f536f9 100644 --- a/src/analyses/invariant_set_domain.h +++ b/src/analyses/invariant_set_domain.h @@ -9,12 +9,19 @@ Author: Daniel Kroening, kroening@kroening.com #ifndef CPROVER_ANALYSES_INVARIANT_SET_DOMAIN_H #define CPROVER_ANALYSES_INVARIANT_SET_DOMAIN_H +#include + #include "ai.h" #include "invariant_set.h" class invariant_set_domaint:public ai_domain_baset { public: + invariant_set_domaint():has_values(false) + { + } + + tvt has_values; invariant_sett invariant_set; // overloading @@ -24,7 +31,11 @@ class invariant_set_domaint:public ai_domain_baset locationt from, locationt to) { - return invariant_set.make_union(other.invariant_set); + bool changed=invariant_set.make_union(other.invariant_set) || + has_values.is_false(); + has_values=tvt::unknown(); + + return changed; } void output( @@ -32,7 +43,10 @@ class invariant_set_domaint:public ai_domain_baset const ai_baset &ai, const namespacet &ns) const override final { - invariant_set.output("", out); + if(has_values.is_known()) + out << has_values.to_string() << '\n'; + else + invariant_set.output("", out); } virtual void transform( @@ -40,20 +54,23 @@ class invariant_set_domaint:public ai_domain_baset locationt to_l, ai_baset &ai, const namespacet &ns) override final; - + void make_top() override final { invariant_set.make_true(); + has_values=tvt(true); } void make_bottom() override final { invariant_set.make_false(); + has_values=tvt(false); } void make_entry() override final { invariant_set.make_true(); + has_values=tvt(true); } }; diff --git a/src/analyses/is_threaded.cpp b/src/analyses/is_threaded.cpp index 0b3df79a553..1c14ad9d424 100644 --- a/src/analyses/is_threaded.cpp +++ b/src/analyses/is_threaded.cpp @@ -34,7 +34,7 @@ class is_threaded_domaint:public ai_domain_baset bool old_reachable=reachable; if(src.reachable) reachable=true; - + bool old_h_s=has_spawn; if(src.has_spawn && (from->is_end_function() || @@ -66,7 +66,7 @@ class is_threaded_domaint:public ai_domain_baset is_threaded=true; } } - + void make_bottom() override final { reachable=has_spawn=is_threaded=false; @@ -76,7 +76,7 @@ class is_threaded_domaint:public ai_domain_baset { reachable=has_spawn=is_threaded=true; } - + void make_entry() override final { reachable=true; diff --git a/src/analyses/reaching_definitions.cpp b/src/analyses/reaching_definitions.cpp index c0cda391b9e..04809464c70 100644 --- a/src/analyses/reaching_definitions.cpp +++ b/src/analyses/reaching_definitions.cpp @@ -679,6 +679,13 @@ Function: rd_range_domaint::output void rd_range_domaint::output(std::ostream &out) const { out << "Reaching definitions:" << std::endl; + + if(has_values.is_known()) + { + out << has_values.to_string() << '\n'; + return; + } + for(valuest::const_iterator it=values.begin(); it!=values.end(); @@ -797,7 +804,8 @@ bool rd_range_domaint::merge( locationt from, locationt to) { - bool more=false; + bool changed=has_values.is_false(); + has_values=tvt::unknown(); valuest::iterator it=values.begin(); for(valuest::const_iterator ito=other.values.begin(); @@ -809,7 +817,7 @@ bool rd_range_domaint::merge( if(it==values.end() || ito->firstfirst) { values.insert(*ito); - more=true; + changed=true; } else if(it!=values.end()) { @@ -817,7 +825,7 @@ bool rd_range_domaint::merge( if(merge_inner(it->second, ito->second)) { - more=true; + changed=true; export_cache.erase(it->first); } @@ -825,7 +833,7 @@ bool rd_range_domaint::merge( } } - return more; + return changed; } /*******************************************************************\ @@ -853,7 +861,8 @@ bool rd_range_domaint::merge_shared( assert(rd!=0); #endif - bool more=false; + bool changed=has_values.is_false(); + has_values=tvt::unknown(); valuest::iterator it=values.begin(); for(valuest::const_iterator ito=other.values.begin(); @@ -871,7 +880,7 @@ bool rd_range_domaint::merge_shared( if(it==values.end() || ito->firstfirst) { values.insert(*ito); - more=true; + changed=true; } else if(it!=values.end()) { @@ -879,7 +888,7 @@ bool rd_range_domaint::merge_shared( if(merge_inner(it->second, ito->second)) { - more=true; + changed=true; export_cache.erase(it->first); } @@ -887,7 +896,7 @@ bool rd_range_domaint::merge_shared( } } - return more; + return changed; } /*******************************************************************\ diff --git a/src/analyses/reaching_definitions.h b/src/analyses/reaching_definitions.h index 0d1d2e36f39..a047e5cd782 100644 --- a/src/analyses/reaching_definitions.h +++ b/src/analyses/reaching_definitions.h @@ -12,6 +12,8 @@ Date: February 2013 #ifndef CPROVER_ANALYSES_REACHING_DEFINITIONS_H #define CPROVER_ANALYSES_REACHING_DEFINITIONS_H +#include + #include "ai.h" #include "goto_rw.h" @@ -44,6 +46,12 @@ class sparse_bitvector_analysist return entry.first->second; } + void clear() + { + value_map.clear(); + values.clear(); + } + protected: typedef typename std::map inner_mapt; std::vector values; @@ -83,6 +91,7 @@ class rd_range_domaint:public ai_domain_baset public: rd_range_domaint(): ai_domain_baset(), + has_values(false), bv_container(0) { } @@ -106,20 +115,24 @@ class rd_range_domaint:public ai_domain_baset { output(out); } - + void make_top() override final { values.clear(); + if(bv_container) bv_container->clear(); + has_values=tvt(true); } void make_bottom() override final { values.clear(); + if(bv_container) bv_container->clear(); + has_values=tvt(false); } void make_entry() override final { - values.clear(); + make_top(); } // returns true iff there is s.th. new @@ -145,6 +158,8 @@ class rd_range_domaint:public ai_domain_baset } protected: + tvt has_values; + sparse_bitvector_analysist *bv_container; typedef std::set values_innert; diff --git a/src/analyses/uninitialized_domain.cpp b/src/analyses/uninitialized_domain.cpp index e0aa7b0c057..36640250fa8 100644 --- a/src/analyses/uninitialized_domain.cpp +++ b/src/analyses/uninitialized_domain.cpp @@ -31,7 +31,7 @@ void uninitialized_domaint::transform( ai_baset &ai, const namespacet &ns) { - if(is_bottom) return; + if(has_values.is_false()) return; switch(from->type) { @@ -98,8 +98,8 @@ void uninitialized_domaint::output( const ai_baset &ai, const namespacet &ns) const { - if(is_bottom) - out << "BOTTOM"; + if(has_values.is_known()) + out << has_values.to_string() << '\n'; else { for(const auto & id : uninitialized) @@ -124,16 +124,16 @@ bool uninitialized_domaint::merge( locationt from, locationt to) { - bool old_is_bottom=is_bottom; - - is_bottom=is_bottom && other.is_bottom; - unsigned old_uninitialized=uninitialized.size(); uninitialized.insert( other.uninitialized.begin(), other.uninitialized.end()); - return old_is_bottom!=is_bottom || - old_uninitialized!=uninitialized.size(); + bool changed= + (has_values.is_false() && !other.has_values.is_false()) || + old_uninitialized!=uninitialized.size(); + has_values=tvt::unknown(); + + return changed; } diff --git a/src/analyses/uninitialized_domain.h b/src/analyses/uninitialized_domain.h index 89943ef8054..93f1f2fd2b8 100644 --- a/src/analyses/uninitialized_domain.h +++ b/src/analyses/uninitialized_domain.h @@ -11,16 +11,16 @@ Date: January 2010 #ifndef CPROVER_ANALYSES_UNINITIALIZED_DOMAIN_H #define CPROVER_ANALYSES_UNINITIALIZED_DOMAIN_H +#include + #include "ai.h" class uninitialized_domaint:public ai_domain_baset { public: - uninitialized_domaint():is_bottom(true) + uninitialized_domaint():has_values(false) { } - - bool is_bottom; // Locals that are declared but may not be initialized typedef std::set uninitializedt; @@ -36,17 +36,17 @@ class uninitialized_domaint:public ai_domain_baset std::ostream &out, const ai_baset &ai, const namespacet &ns) const override final; - + void make_top() override final { - // We don't have a proper 'top', and refuse to do this. - assert(false); + uninitialized.clear(); + has_values=tvt(true); } void make_bottom() override final { uninitialized.clear(); - is_bottom=true; + has_values=tvt(false); } void make_entry() override final @@ -61,6 +61,8 @@ class uninitialized_domaint:public ai_domain_baset locationt to); protected: + tvt has_values; + void assign(const exprt &lhs); };