From db925dec5f0246689ef7618f2aa0723aae418e04 Mon Sep 17 00:00:00 2001 From: martin Date: Fri, 9 Feb 2018 00:01:01 +0000 Subject: [PATCH 1/9] Revert "Fix iterator equality check bug in constant_propagator.cpp" This reverts commit ef929ea867b949266e53c60856839411a3f82c5a. --- src/analyses/constant_propagator.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/analyses/constant_propagator.cpp b/src/analyses/constant_propagator.cpp index c4174dc8f91..230d2b1dd1b 100644 --- a/src/analyses/constant_propagator.cpp +++ b/src/analyses/constant_propagator.cpp @@ -46,7 +46,7 @@ void constant_propagator_domaint::transform( locationt to, ai_baset &ai, const namespacet &ns, - ai_domain_baset::edge_typet edge_type) + ai_domain_baset::edge_typet /*edge_type*/) { #ifdef DEBUG std::cout << "Transform from/to:\n"; @@ -130,7 +130,7 @@ void constant_propagator_domaint::transform( const symbol_exprt &symbol_expr=to_symbol_expr(function); const irep_idt id=symbol_expr.get_identifier(); - if(edge_type == ai_domain_baset::edge_typet::FUNCTION_LOCAL) + if(to==next) { if(id==CPROVER_PREFIX "set_must" || id==CPROVER_PREFIX "get_must" || From 86cadcdda4936287023be2df2dd02cf1c6321e9d Mon Sep 17 00:00:00 2001 From: martin Date: Fri, 9 Feb 2018 00:01:28 +0000 Subject: [PATCH 2/9] Revert "Fix iterator equality check bug in custom_bitvector_analysis.cpp" This reverts commit af314f588b13b1aa1f04d0c7e35f836b851f723f. --- src/analyses/custom_bitvector_analysis.cpp | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/src/analyses/custom_bitvector_analysis.cpp b/src/analyses/custom_bitvector_analysis.cpp index 0b45099302b..e86efba1524 100644 --- a/src/analyses/custom_bitvector_analysis.cpp +++ b/src/analyses/custom_bitvector_analysis.cpp @@ -270,7 +270,7 @@ void custom_bitvector_domaint::transform( locationt to, ai_baset &ai, const namespacet &ns, - ai_domain_baset::edge_typet edge_type) + ai_domain_baset::edge_typet /*edge_type*/) { // upcast of ai custom_bitvector_analysist &cba= @@ -396,8 +396,11 @@ void custom_bitvector_domaint::transform( } else { + goto_programt::const_targett next=from; + ++next; + // only if there is an actual call, i.e., we have a body - if(edge_type != ai_domain_baset::edge_typet::FUNCTION_LOCAL) + if(next!=to) { const code_typet &code_type= to_code_type(ns.lookup(identifier).type); From ac036fd4ebbdd8b6aff2dacf55d29d5a21752d70 Mon Sep 17 00:00:00 2001 From: martin Date: Fri, 9 Feb 2018 00:01:52 +0000 Subject: [PATCH 3/9] Revert "Fix iterator equality check bug in dependence_graph.cpp" This reverts commit e0605b70c359832fa1c274eb6f8d9242dff52953. --- src/analyses/dependence_graph.cpp | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/src/analyses/dependence_graph.cpp b/src/analyses/dependence_graph.cpp index 6d691528ca8..af9a3aed953 100644 --- a/src/analyses/dependence_graph.cpp +++ b/src/analyses/dependence_graph.cpp @@ -188,7 +188,7 @@ void dep_graph_domaint::transform( goto_programt::const_targett to, ai_baset &ai, const namespacet &ns, - ai_domain_baset::edge_typet edge_type) + ai_domain_baset::edge_typet /*edge_type*/) { dependence_grapht *dep_graph=dynamic_cast(&ai); assert(dep_graph!=nullptr); @@ -196,9 +196,10 @@ void dep_graph_domaint::transform( // propagate control dependencies across function calls if(from->is_function_call()) { - const goto_programt::const_targett next = std::next(from); + goto_programt::const_targett next=from; + ++next; - if(edge_type == ai_domain_baset::edge_typet::FUNCTION_LOCAL) + if(next==to) { control_dependencies(from, to, *dep_graph); } From 3ca91bc4cd18677d2c83dd942728963f52908b4e Mon Sep 17 00:00:00 2001 From: martin Date: Fri, 9 Feb 2018 00:02:10 +0000 Subject: [PATCH 4/9] Revert "Fix iterator comparison bug in reaching_definitions.cpp" This reverts commit 394c42d015793e5d435f5f0d32bf691d2d02db94. --- src/analyses/reaching_definitions.cpp | 12 +++++++----- src/analyses/reaching_definitions.h | 3 +-- 2 files changed, 8 insertions(+), 7 deletions(-) diff --git a/src/analyses/reaching_definitions.cpp b/src/analyses/reaching_definitions.cpp index 02cdfa4dd2c..48b2f81f16f 100644 --- a/src/analyses/reaching_definitions.cpp +++ b/src/analyses/reaching_definitions.cpp @@ -60,7 +60,7 @@ void rd_range_domaint::transform( locationt to, ai_baset &ai, const namespacet &ns, - ai_domain_baset::edge_typet edge_type) + ai_domain_baset::edge_typet /*edge_type*/) { reaching_definitions_analysist *rd= dynamic_cast(&ai); @@ -79,7 +79,7 @@ void rd_range_domaint::transform( transform_start_thread(ns, *rd); // do argument-to-parameter assignments else if(from->is_function_call()) - transform_function_call(ns, from, to, *rd, edge_type); + transform_function_call(ns, from, to, *rd); // cleanup parameters else if(from->is_end_function()) transform_end_function(ns, from, to, *rd); @@ -170,13 +170,15 @@ void rd_range_domaint::transform_function_call( const namespacet &ns, locationt from, locationt to, - reaching_definitions_analysist &rd, - ai_domain_baset::edge_typet edge_type) + reaching_definitions_analysist &rd) { const code_function_callt &code=to_code_function_call(from->code); + goto_programt::const_targett next=from; + ++next; + // only if there is an actual call, i.e., we have a body - if(edge_type != ai_domain_baset::edge_typet::FUNCTION_LOCAL) + if(next!=to) { for(valuest::iterator it=values.begin(); it!=values.end(); diff --git a/src/analyses/reaching_definitions.h b/src/analyses/reaching_definitions.h index ce112c1ed66..499b4064967 100644 --- a/src/analyses/reaching_definitions.h +++ b/src/analyses/reaching_definitions.h @@ -218,8 +218,7 @@ class rd_range_domaint:public ai_domain_baset const namespacet &ns, locationt from, locationt to, - reaching_definitions_analysist &rd, - ai_domain_baset::edge_typet edge_type); + reaching_definitions_analysist &rd); void transform_end_function( const namespacet &ns, locationt from, From 1990994d30cfd44492146abab310e7d4ef78bc23 Mon Sep 17 00:00:00 2001 From: martin Date: Fri, 9 Feb 2018 00:02:47 +0000 Subject: [PATCH 5/9] Revert "Add edge type parameter to ai transform method" This reverts commit f8e38fb130e2a4a03a21b2f8836f602ad07d487f. There are a number of problems with commit f8e38fb130e2a4a03a21b2f8836f602ad07d487f : 1. This is a key API and breaks out-of-tree abstract domains. 2. It doesn't take into account the invariants on transform. 3. The extra parameter duplicates information in the arguments and confuses cases; without a body a CALL instruction is not a CALL. 4. It doesn't fix all of the issues in tranform functions. 5. It doesn't fix the corresponding API issues with merge. --- src/analyses/ai.cpp | 12 ++++-------- src/analyses/ai.h | 10 +--------- src/analyses/constant_propagator.cpp | 3 +-- src/analyses/constant_propagator.h | 3 +-- src/analyses/custom_bitvector_analysis.cpp | 3 +-- src/analyses/custom_bitvector_analysis.h | 3 +-- src/analyses/dependence_graph.cpp | 3 +-- src/analyses/dependence_graph.h | 3 +-- src/analyses/escape_analysis.cpp | 3 +-- src/analyses/escape_analysis.h | 3 +-- src/analyses/global_may_alias.cpp | 3 +-- src/analyses/global_may_alias.h | 3 +-- src/analyses/interval_domain.cpp | 3 +-- src/analyses/interval_domain.h | 3 +-- src/analyses/invariant_set_domain.cpp | 3 +-- src/analyses/invariant_set_domain.h | 3 +-- src/analyses/is_threaded.cpp | 3 +-- src/analyses/reaching_definitions.cpp | 3 +-- src/analyses/reaching_definitions.h | 3 +-- src/analyses/uninitialized_domain.cpp | 3 +-- src/analyses/uninitialized_domain.h | 3 +-- unit/analyses/ai/ai_simplify_lhs.cpp | 7 +------ 22 files changed, 25 insertions(+), 61 deletions(-) diff --git a/src/analyses/ai.cpp b/src/analyses/ai.cpp index d76391c6446..dedb2da9a3c 100644 --- a/src/analyses/ai.cpp +++ b/src/analyses/ai.cpp @@ -365,8 +365,7 @@ bool ai_baset::visit( // initialize state, if necessary get_state(to_l); - new_values.transform( - l, to_l, *this, ns, ai_domain_baset::edge_typet::FUNCTION_LOCAL); + new_values.transform(l, to_l, *this, ns); if(merge(new_values, l, to_l)) have_new_values=true; @@ -399,8 +398,7 @@ bool ai_baset::do_function_call( { // if we don't have a body, we just do an edige call -> return std::unique_ptr tmp_state(make_temporary_state(get_state(l_call))); - tmp_state->transform( - l_call, l_return, *this, ns, ai_domain_baset::edge_typet::FUNCTION_LOCAL); + tmp_state->transform(l_call, l_return, *this, ns); return merge(*tmp_state, l_call, l_return); } @@ -417,8 +415,7 @@ bool ai_baset::do_function_call( // do the edge from the call site to the beginning of the function std::unique_ptr tmp_state(make_temporary_state(get_state(l_call))); - tmp_state->transform( - l_call, l_begin, *this, ns, ai_domain_baset::edge_typet::CALL); + tmp_state->transform(l_call, l_begin, *this, ns); bool new_data=false; @@ -445,8 +442,7 @@ bool ai_baset::do_function_call( 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, ai_domain_baset::edge_typet::RETURN); + tmp_state->transform(l_end, l_return, *this, ns); // Propagate those return merge(*tmp_state, l_end, l_return); diff --git a/src/analyses/ai.h b/src/analyses/ai.h index 99d1b130345..c9662a7a342 100644 --- a/src/analyses/ai.h +++ b/src/analyses/ai.h @@ -31,13 +31,6 @@ class ai_baset; class ai_domain_baset { public: - enum class edge_typet - { - FUNCTION_LOCAL, - CALL, - RETURN, - }; - // The constructor is expected to produce 'false' // or 'bottom' ai_domain_baset() @@ -60,8 +53,7 @@ class ai_domain_baset locationt from, locationt to, ai_baset &ai, - const namespacet &ns, - edge_typet edge_type) = 0; + const namespacet &ns)=0; virtual void output( std::ostream &out, diff --git a/src/analyses/constant_propagator.cpp b/src/analyses/constant_propagator.cpp index 230d2b1dd1b..e95417f4934 100644 --- a/src/analyses/constant_propagator.cpp +++ b/src/analyses/constant_propagator.cpp @@ -45,8 +45,7 @@ void constant_propagator_domaint::transform( locationt from, locationt to, ai_baset &ai, - const namespacet &ns, - ai_domain_baset::edge_typet /*edge_type*/) + const namespacet &ns) { #ifdef DEBUG std::cout << "Transform from/to:\n"; diff --git a/src/analyses/constant_propagator.h b/src/analyses/constant_propagator.h index 1431783f918..0fc4796e8b7 100644 --- a/src/analyses/constant_propagator.h +++ b/src/analyses/constant_propagator.h @@ -25,8 +25,7 @@ class constant_propagator_domaint:public ai_domain_baset locationt from, locationt to, ai_baset &ai_base, - const namespacet &ns, - ai_domain_baset::edge_typet edge_type) final override; + const namespacet &ns) final override; virtual void output( std::ostream &out, diff --git a/src/analyses/custom_bitvector_analysis.cpp b/src/analyses/custom_bitvector_analysis.cpp index e86efba1524..16c3fad0c4f 100644 --- a/src/analyses/custom_bitvector_analysis.cpp +++ b/src/analyses/custom_bitvector_analysis.cpp @@ -269,8 +269,7 @@ void custom_bitvector_domaint::transform( locationt from, locationt to, ai_baset &ai, - const namespacet &ns, - ai_domain_baset::edge_typet /*edge_type*/) + const namespacet &ns) { // upcast of ai custom_bitvector_analysist &cba= diff --git a/src/analyses/custom_bitvector_analysis.h b/src/analyses/custom_bitvector_analysis.h index e64a83e585c..4896d768cb7 100644 --- a/src/analyses/custom_bitvector_analysis.h +++ b/src/analyses/custom_bitvector_analysis.h @@ -27,8 +27,7 @@ class custom_bitvector_domaint:public ai_domain_baset locationt from, locationt to, ai_baset &ai, - const namespacet &ns, - ai_domain_baset::edge_typet edge_type) final override; + const namespacet &ns) final override; void output( std::ostream &out, diff --git a/src/analyses/dependence_graph.cpp b/src/analyses/dependence_graph.cpp index af9a3aed953..5f1bae158bc 100644 --- a/src/analyses/dependence_graph.cpp +++ b/src/analyses/dependence_graph.cpp @@ -187,8 +187,7 @@ void dep_graph_domaint::transform( goto_programt::const_targett from, goto_programt::const_targett to, ai_baset &ai, - const namespacet &ns, - ai_domain_baset::edge_typet /*edge_type*/) + const namespacet &ns) { dependence_grapht *dep_graph=dynamic_cast(&ai); assert(dep_graph!=nullptr); diff --git a/src/analyses/dependence_graph.h b/src/analyses/dependence_graph.h index 97f7548e0f7..30b97108776 100644 --- a/src/analyses/dependence_graph.h +++ b/src/analyses/dependence_graph.h @@ -83,8 +83,7 @@ class dep_graph_domaint:public ai_domain_baset goto_programt::const_targett from, goto_programt::const_targett to, ai_baset &ai, - const namespacet &ns, - ai_domain_baset::edge_typet edge_type) final override; + const namespacet &ns) final override; void output( std::ostream &out, diff --git a/src/analyses/escape_analysis.cpp b/src/analyses/escape_analysis.cpp index 90fc7f5f87c..1598b9ededa 100644 --- a/src/analyses/escape_analysis.cpp +++ b/src/analyses/escape_analysis.cpp @@ -165,8 +165,7 @@ void escape_domaint::transform( locationt from, locationt to, ai_baset &ai, - const namespacet &ns, - ai_domain_baset::edge_typet /*edge_type*/) + const namespacet &ns) { if(has_values.is_false()) return; diff --git a/src/analyses/escape_analysis.h b/src/analyses/escape_analysis.h index 0020859bf8f..52de2b5dfc8 100644 --- a/src/analyses/escape_analysis.h +++ b/src/analyses/escape_analysis.h @@ -32,8 +32,7 @@ class escape_domaint:public ai_domain_baset locationt from, locationt to, ai_baset &ai, - const namespacet &ns, - ai_domain_baset::edge_typet edge_type) final override; + const namespacet &ns) final override; void output( std::ostream &out, diff --git a/src/analyses/global_may_alias.cpp b/src/analyses/global_may_alias.cpp index 32f4f32589b..82c1f5a72dc 100644 --- a/src/analyses/global_may_alias.cpp +++ b/src/analyses/global_may_alias.cpp @@ -79,8 +79,7 @@ void global_may_alias_domaint::transform( locationt from, locationt to, ai_baset &ai, - const namespacet &ns, - ai_domain_baset::edge_typet /*edge_type*/) + const namespacet &ns) { if(has_values.is_false()) return; diff --git a/src/analyses/global_may_alias.h b/src/analyses/global_may_alias.h index 5ab40edbe57..a5e1b0cd49a 100644 --- a/src/analyses/global_may_alias.h +++ b/src/analyses/global_may_alias.h @@ -32,8 +32,7 @@ class global_may_alias_domaint:public ai_domain_baset locationt from, locationt to, ai_baset &ai, - const namespacet &ns, - ai_domain_baset::edge_typet edge_type) final override; + const namespacet &ns) final override; void output( std::ostream &out, diff --git a/src/analyses/interval_domain.cpp b/src/analyses/interval_domain.cpp index 649e24b8a60..5f1b9a314b5 100644 --- a/src/analyses/interval_domain.cpp +++ b/src/analyses/interval_domain.cpp @@ -59,8 +59,7 @@ void interval_domaint::transform( locationt from, locationt to, ai_baset &ai, - const namespacet &ns, - ai_domain_baset::edge_typet /*edge_type*/) + const namespacet &ns) { const goto_programt::instructiont &instruction=*from; switch(instruction.type) diff --git a/src/analyses/interval_domain.h b/src/analyses/interval_domain.h index 16dc3cbdd7b..7702990d53d 100644 --- a/src/analyses/interval_domain.h +++ b/src/analyses/interval_domain.h @@ -36,8 +36,7 @@ class interval_domaint:public ai_domain_baset locationt from, locationt to, ai_baset &ai, - const namespacet &ns, - ai_domain_baset::edge_typet edge_type) final override; + const namespacet &ns) final override; void output( std::ostream &out, diff --git a/src/analyses/invariant_set_domain.cpp b/src/analyses/invariant_set_domain.cpp index d7e3800786b..3132591eb42 100644 --- a/src/analyses/invariant_set_domain.cpp +++ b/src/analyses/invariant_set_domain.cpp @@ -17,8 +17,7 @@ void invariant_set_domaint::transform( locationt from_l, locationt to_l, ai_baset &ai, - const namespacet &ns, - ai_domain_baset::edge_typet /*edge_type*/) + const namespacet &ns) { switch(from_l->type) { diff --git a/src/analyses/invariant_set_domain.h b/src/analyses/invariant_set_domain.h index 59e29b4efa6..367e987c709 100644 --- a/src/analyses/invariant_set_domain.h +++ b/src/analyses/invariant_set_domain.h @@ -56,8 +56,7 @@ class invariant_set_domaint:public ai_domain_baset locationt from_l, locationt to_l, ai_baset &ai, - const namespacet &ns, - ai_domain_baset::edge_typet edge_type) final override; + const namespacet &ns) final override; void make_top() final override { diff --git a/src/analyses/is_threaded.cpp b/src/analyses/is_threaded.cpp index 2910bf3c629..54a3fa2d70d 100644 --- a/src/analyses/is_threaded.cpp +++ b/src/analyses/is_threaded.cpp @@ -52,8 +52,7 @@ class is_threaded_domaint:public ai_domain_baset locationt from, locationt to, ai_baset &ai, - const namespacet &ns, - ai_domain_baset::edge_typet /*edge_type*/) final override + const namespacet &ns) final override { // assert(reachable); diff --git a/src/analyses/reaching_definitions.cpp b/src/analyses/reaching_definitions.cpp index 48b2f81f16f..c3242849511 100644 --- a/src/analyses/reaching_definitions.cpp +++ b/src/analyses/reaching_definitions.cpp @@ -59,8 +59,7 @@ void rd_range_domaint::transform( locationt from, locationt to, ai_baset &ai, - const namespacet &ns, - ai_domain_baset::edge_typet /*edge_type*/) + const namespacet &ns) { reaching_definitions_analysist *rd= dynamic_cast(&ai); diff --git a/src/analyses/reaching_definitions.h b/src/analyses/reaching_definitions.h index 499b4064967..e218eb19bca 100644 --- a/src/analyses/reaching_definitions.h +++ b/src/analyses/reaching_definitions.h @@ -117,8 +117,7 @@ class rd_range_domaint:public ai_domain_baset locationt from, locationt to, ai_baset &ai, - const namespacet &ns, - ai_domain_baset::edge_typet edge_type) final override; + const namespacet &ns) final override; void output( std::ostream &out, diff --git a/src/analyses/uninitialized_domain.cpp b/src/analyses/uninitialized_domain.cpp index 5310f0ffcb0..4f92eaebd49 100644 --- a/src/analyses/uninitialized_domain.cpp +++ b/src/analyses/uninitialized_domain.cpp @@ -20,8 +20,7 @@ void uninitialized_domaint::transform( locationt from, locationt to, ai_baset &ai, - const namespacet &ns, - ai_domain_baset::edge_typet /*edge_type*/) + const namespacet &ns) { if(has_values.is_false()) return; diff --git a/src/analyses/uninitialized_domain.h b/src/analyses/uninitialized_domain.h index afc0b71fed7..45a9d085c99 100644 --- a/src/analyses/uninitialized_domain.h +++ b/src/analyses/uninitialized_domain.h @@ -33,8 +33,7 @@ class uninitialized_domaint:public ai_domain_baset locationt from, locationt to, ai_baset &ai, - const namespacet &ns, - ai_domain_baset::edge_typet edge_type) final override; + const namespacet &ns) final override; void output( std::ostream &out, diff --git a/unit/analyses/ai/ai_simplify_lhs.cpp b/unit/analyses/ai/ai_simplify_lhs.cpp index 004ae391a60..c8ea9dae2d2 100644 --- a/unit/analyses/ai/ai_simplify_lhs.cpp +++ b/unit/analyses/ai/ai_simplify_lhs.cpp @@ -25,12 +25,7 @@ class constant_simplification_mockt:public ai_domain_baset { public: - void transform( - locationt, - locationt, - ai_baset &, - const namespacet &, - ai_domain_baset::edge_typet) override + void transform(locationt, locationt, ai_baset &, const namespacet &) override {} void make_bottom() override {} From e3db794d801a29e568362b94b01e006bbe811c39 Mon Sep 17 00:00:00 2001 From: martin Date: Thu, 8 Feb 2018 23:07:14 +0000 Subject: [PATCH 6/9] Whitespace changes to keep clang-format happy. --- src/analyses/ai.h | 2 +- src/analyses/custom_bitvector_analysis.h | 8 +++----- src/analyses/escape_analysis.h | 8 +++----- src/analyses/global_may_alias.h | 8 +++----- src/analyses/interval_domain.h | 8 +++----- src/analyses/is_threaded.cpp | 8 +++----- src/analyses/reaching_definitions.h | 8 +++----- src/analyses/uninitialized_domain.h | 8 +++----- 8 files changed, 22 insertions(+), 36 deletions(-) diff --git a/src/analyses/ai.h b/src/analyses/ai.h index c9662a7a342..ba5ef2e5864 100644 --- a/src/analyses/ai.h +++ b/src/analyses/ai.h @@ -53,7 +53,7 @@ class ai_domain_baset locationt from, locationt to, ai_baset &ai, - const namespacet &ns)=0; + const namespacet &ns) = 0; virtual void output( std::ostream &out, diff --git a/src/analyses/custom_bitvector_analysis.h b/src/analyses/custom_bitvector_analysis.h index 4896d768cb7..4142d6930c1 100644 --- a/src/analyses/custom_bitvector_analysis.h +++ b/src/analyses/custom_bitvector_analysis.h @@ -23,11 +23,9 @@ class custom_bitvector_analysist; class custom_bitvector_domaint:public ai_domain_baset { public: - void transform( - locationt from, - locationt to, - ai_baset &ai, - const namespacet &ns) final override; + void + transform(locationt from, locationt to, ai_baset &ai, const namespacet &ns) + final override; void output( std::ostream &out, diff --git a/src/analyses/escape_analysis.h b/src/analyses/escape_analysis.h index 52de2b5dfc8..bbf05973b13 100644 --- a/src/analyses/escape_analysis.h +++ b/src/analyses/escape_analysis.h @@ -28,11 +28,9 @@ class escape_domaint:public ai_domain_baset { } - void transform( - locationt from, - locationt to, - ai_baset &ai, - const namespacet &ns) final override; + void + transform(locationt from, locationt to, ai_baset &ai, const namespacet &ns) + final override; void output( std::ostream &out, diff --git a/src/analyses/global_may_alias.h b/src/analyses/global_may_alias.h index a5e1b0cd49a..b8f3480bb1c 100644 --- a/src/analyses/global_may_alias.h +++ b/src/analyses/global_may_alias.h @@ -28,11 +28,9 @@ class global_may_alias_domaint:public ai_domain_baset { } - void transform( - locationt from, - locationt to, - ai_baset &ai, - const namespacet &ns) final override; + void + transform(locationt from, locationt to, ai_baset &ai, const namespacet &ns) + final override; void output( std::ostream &out, diff --git a/src/analyses/interval_domain.h b/src/analyses/interval_domain.h index 7702990d53d..f94236861e6 100644 --- a/src/analyses/interval_domain.h +++ b/src/analyses/interval_domain.h @@ -32,11 +32,9 @@ class interval_domaint:public ai_domain_baset { } - void transform( - locationt from, - locationt to, - ai_baset &ai, - const namespacet &ns) final override; + void + transform(locationt from, locationt to, ai_baset &ai, const namespacet &ns) + final override; void output( std::ostream &out, diff --git a/src/analyses/is_threaded.cpp b/src/analyses/is_threaded.cpp index 54a3fa2d70d..c509fcac857 100644 --- a/src/analyses/is_threaded.cpp +++ b/src/analyses/is_threaded.cpp @@ -48,11 +48,9 @@ class is_threaded_domaint:public ai_domain_baset old_is_threaded!=is_threaded; } - void transform( - locationt from, - locationt to, - ai_baset &ai, - const namespacet &ns) final override + void + transform(locationt from, locationt to, ai_baset &ai, const namespacet &ns) + final override { // assert(reachable); diff --git a/src/analyses/reaching_definitions.h b/src/analyses/reaching_definitions.h index e218eb19bca..046dae22863 100644 --- a/src/analyses/reaching_definitions.h +++ b/src/analyses/reaching_definitions.h @@ -113,11 +113,9 @@ class rd_range_domaint:public ai_domain_baset bv_container=&_bv_container; } - void transform( - locationt from, - locationt to, - ai_baset &ai, - const namespacet &ns) final override; + void + transform(locationt from, locationt to, ai_baset &ai, const namespacet &ns) + final override; void output( std::ostream &out, diff --git a/src/analyses/uninitialized_domain.h b/src/analyses/uninitialized_domain.h index 45a9d085c99..2d957d0bbb5 100644 --- a/src/analyses/uninitialized_domain.h +++ b/src/analyses/uninitialized_domain.h @@ -29,11 +29,9 @@ class uninitialized_domaint:public ai_domain_baset typedef std::set uninitializedt; uninitializedt uninitialized; - void transform( - locationt from, - locationt to, - ai_baset &ai, - const namespacet &ns) final override; + void + transform(locationt from, locationt to, ai_baset &ai, const namespacet &ns) + final override; void output( std::ostream &out, From d447c26147f7d6e05057c5540ed95f7f668a1ed4 Mon Sep 17 00:00:00 2001 From: martin Date: Thu, 1 Feb 2018 19:26:31 +0000 Subject: [PATCH 7/9] Document the invariants on iterators arguments to transform and merge. In many, but not all, cases they are comparable. However they should always be dereferenceable. --- src/analyses/ai.h | 14 ++++++++++++++ 1 file changed, 14 insertions(+) diff --git a/src/analyses/ai.h b/src/analyses/ai.h index ba5ef2e5864..dfe5e183a3d 100644 --- a/src/analyses/ai.h +++ b/src/analyses/ai.h @@ -48,6 +48,15 @@ class ai_domain_baset // 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) + // + // "this" is the domain before the instruction "from" + // "from" is the instruction to be interpretted + // "to" is the next instruction (for GOTO, FUNCTION_CALL, END_FUNCTION) + // + // PRECONDITION(from.is_dereferenceable(), "Must not be _::end()") + // PRECONDITION(to.is_dereferenceable(), "Must not be _::end()") + // PRECONDITION(are_comparable(from,to) || + // (from->is_function_call() || from->is_end_function()) virtual void transform( locationt from, @@ -90,6 +99,11 @@ class ai_domain_baset // // This computes the join between "this" and "b". // Return true if "this" has changed. + // In the usual case, "b" is the updated state after "from" + // and "this" is the state before "to". + // + // PRECONDITION(from.is_dereferenceable(), "Must not be _::end()") + // PRECONDITION(to.is_dereferenceable(), "Must not be _::end()") // This method allows an expression to be simplified / evaluated using the // current state. It is used to evaluate assertions and in program From b2fba976d5b5d5f7e8bdb61bbf6a8ca6a0733678 Mon Sep 17 00:00:00 2001 From: martin Date: Tue, 16 Jan 2018 23:57:51 +0000 Subject: [PATCH 8/9] Correct domain transformers so that they meet the preconditions. This will eliminate issues with non-comparable iterators being compared and tidies a few things. --- src/analyses/constant_propagator.cpp | 11 +++++++---- src/analyses/custom_bitvector_analysis.cpp | 7 +++---- src/analyses/dependence_graph.cpp | 6 ++---- src/analyses/interval_domain.cpp | 2 ++ src/analyses/invariant_set_domain.cpp | 2 ++ src/analyses/reaching_definitions.cpp | 5 +---- 6 files changed, 17 insertions(+), 16 deletions(-) diff --git a/src/analyses/constant_propagator.cpp b/src/analyses/constant_propagator.cpp index e95417f4934..fa410762bf2 100644 --- a/src/analyses/constant_propagator.cpp +++ b/src/analyses/constant_propagator.cpp @@ -93,6 +93,8 @@ void constant_propagator_domaint::transform( { exprt g; + // Comparing iterators is safe as the target must be within the same list + // of instructions because this is a GOTO. if(from->get_target()==to) g=simplify_expr(from->guard, ns); else @@ -121,15 +123,14 @@ void constant_propagator_domaint::transform( const code_function_callt &function_call=to_code_function_call(from->code); const exprt &function=function_call.function(); - const locationt& next=std::next(from); - if(function.id()==ID_symbol) { // called function identifier const symbol_exprt &symbol_expr=to_symbol_expr(function); const irep_idt id=symbol_expr.get_identifier(); - if(to==next) + // Functions with no body + if(from->function == to->function) { if(id==CPROVER_PREFIX "set_must" || id==CPROVER_PREFIX "get_must" || @@ -177,7 +178,9 @@ void constant_propagator_domaint::transform( else { // unresolved call - INVARIANT(to==next, "Unresolved call can only be approximated if a skip"); + INVARIANT( + from->function == to->function, + "Unresolved call can only be approximated if a skip"); if(have_dirty) values.set_dirty_to_top(cp->dirty, ns); diff --git a/src/analyses/custom_bitvector_analysis.cpp b/src/analyses/custom_bitvector_analysis.cpp index 16c3fad0c4f..ae452b36002 100644 --- a/src/analyses/custom_bitvector_analysis.cpp +++ b/src/analyses/custom_bitvector_analysis.cpp @@ -395,11 +395,8 @@ void custom_bitvector_domaint::transform( } else { - goto_programt::const_targett next=from; - ++next; - // only if there is an actual call, i.e., we have a body - if(next!=to) + if(from->function != to->function) { const code_typet &code_type= to_code_type(ns.lookup(identifier).type); @@ -522,6 +519,8 @@ void custom_bitvector_domaint::transform( { exprt guard=instruction.guard; + // Comparing iterators is safe as the target must be within the same list + // of instructions because this is a GOTO. if(to!=from->get_target()) guard.make_not(); diff --git a/src/analyses/dependence_graph.cpp b/src/analyses/dependence_graph.cpp index 5f1bae158bc..f4af2913fa0 100644 --- a/src/analyses/dependence_graph.cpp +++ b/src/analyses/dependence_graph.cpp @@ -195,16 +195,14 @@ void dep_graph_domaint::transform( // propagate control dependencies across function calls if(from->is_function_call()) { - goto_programt::const_targett next=from; - ++next; - - if(next==to) + if(from->function == to->function) { control_dependencies(from, to, *dep_graph); } else { // edge to function entry point + const goto_programt::const_targett next = std::next(from); dep_graph_domaint *s= dynamic_cast(&(dep_graph->get_state(next))); diff --git a/src/analyses/interval_domain.cpp b/src/analyses/interval_domain.cpp index 5f1b9a314b5..eff19db4f62 100644 --- a/src/analyses/interval_domain.cpp +++ b/src/analyses/interval_domain.cpp @@ -78,6 +78,8 @@ void interval_domaint::transform( case GOTO: { + // Comparing iterators is safe as the target must be within the same list + // of instructions because this is a GOTO. locationt next=from; next++; if(next==to) diff --git a/src/analyses/invariant_set_domain.cpp b/src/analyses/invariant_set_domain.cpp index 3132591eb42..1e1015eb404 100644 --- a/src/analyses/invariant_set_domain.cpp +++ b/src/analyses/invariant_set_domain.cpp @@ -23,6 +23,8 @@ void invariant_set_domaint::transform( { case GOTO: { + // Comparing iterators is safe as the target must be within the same list + // of instructions because this is a GOTO. exprt tmp(from_l->guard); goto_programt::const_targett next=from_l; diff --git a/src/analyses/reaching_definitions.cpp b/src/analyses/reaching_definitions.cpp index c3242849511..7788835f0db 100644 --- a/src/analyses/reaching_definitions.cpp +++ b/src/analyses/reaching_definitions.cpp @@ -173,11 +173,8 @@ void rd_range_domaint::transform_function_call( { const code_function_callt &code=to_code_function_call(from->code); - goto_programt::const_targett next=from; - ++next; - // only if there is an actual call, i.e., we have a body - if(next!=to) + if(from->function != to->function) { for(valuest::iterator it=values.begin(); it!=values.end(); From d7bb937da011dd6cd6248b938d9713dd1a04f0ab Mon Sep 17 00:00:00 2001 From: martin Date: Wed, 17 Jan 2018 00:21:36 +0000 Subject: [PATCH 9/9] Catch the case when a GOTO instruction is effectively a SKIP. This is rare in usual work-flows as remove_skip should remove this. However if the program has been extensively transformed it could happen. --- src/analyses/interval_domain.cpp | 11 +++++++---- 1 file changed, 7 insertions(+), 4 deletions(-) diff --git a/src/analyses/interval_domain.cpp b/src/analyses/interval_domain.cpp index eff19db4f62..1b237c31f1f 100644 --- a/src/analyses/interval_domain.cpp +++ b/src/analyses/interval_domain.cpp @@ -82,10 +82,13 @@ void interval_domaint::transform( // of instructions because this is a GOTO. locationt next=from; next++; - if(next==to) - assume(not_exprt(instruction.guard), ns); - else - assume(instruction.guard, ns); + if(from->get_target() != next) // If equal then a skip + { + if(next == to) + assume(not_exprt(instruction.guard), ns); + else + assume(instruction.guard, ns); + } } break;