From 9091faa9550baa90fb63bca54f25f7717aaeec72 Mon Sep 17 00:00:00 2001 From: reuk Date: Wed, 22 Nov 2017 13:47:33 +0000 Subject: [PATCH 01/16] Use stdlib debug mode in Travis --- .travis.yml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/.travis.yml b/.travis.yml index 8b1e9c98a0f..305cd75273f 100644 --- a/.travis.yml +++ b/.travis.yml @@ -65,7 +65,9 @@ jobs: before_install: - mkdir bin ; ln -s /usr/bin/gcc-5 bin/gcc # env: COMPILER=g++-5 SAN_FLAGS="-fsanitize=undefined -fno-sanitize-recover -fno-omit-frame-pointer" - env: COMPILER="ccache g++-5" + env: + - COMPILER="ccache g++-5" + - EXTRA_CXXFLAGS="-D_GLIBCXX_DEBUG" # OS X using g++ - stage: Test different OS/CXX/Flags From f8e38fb130e2a4a03a21b2f8836f602ad07d487f Mon Sep 17 00:00:00 2001 From: reuk Date: Thu, 23 Nov 2017 11:38:00 +0000 Subject: [PATCH 02/16] Add edge type parameter to ai transform method --- 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, 61 insertions(+), 25 deletions(-) diff --git a/src/analyses/ai.cpp b/src/analyses/ai.cpp index dedb2da9a3c..d76391c6446 100644 --- a/src/analyses/ai.cpp +++ b/src/analyses/ai.cpp @@ -365,7 +365,8 @@ bool ai_baset::visit( // initialize state, if necessary get_state(to_l); - new_values.transform(l, to_l, *this, ns); + new_values.transform( + l, to_l, *this, ns, ai_domain_baset::edge_typet::FUNCTION_LOCAL); if(merge(new_values, l, to_l)) have_new_values=true; @@ -398,7 +399,8 @@ 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); + tmp_state->transform( + l_call, l_return, *this, ns, ai_domain_baset::edge_typet::FUNCTION_LOCAL); return merge(*tmp_state, l_call, l_return); } @@ -415,7 +417,8 @@ 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); + tmp_state->transform( + l_call, l_begin, *this, ns, ai_domain_baset::edge_typet::CALL); bool new_data=false; @@ -442,7 +445,8 @@ 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); + tmp_state->transform( + l_end, l_return, *this, ns, ai_domain_baset::edge_typet::RETURN); // Propagate those return merge(*tmp_state, l_end, l_return); diff --git a/src/analyses/ai.h b/src/analyses/ai.h index a09e43f699f..5b99be3d507 100644 --- a/src/analyses/ai.h +++ b/src/analyses/ai.h @@ -31,6 +31,13 @@ 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() @@ -53,7 +60,8 @@ class ai_domain_baset locationt from, locationt to, ai_baset &ai, - const namespacet &ns)=0; + const namespacet &ns, + edge_typet edge_type) = 0; virtual void output( std::ostream &out, diff --git a/src/analyses/constant_propagator.cpp b/src/analyses/constant_propagator.cpp index e95417f4934..230d2b1dd1b 100644 --- a/src/analyses/constant_propagator.cpp +++ b/src/analyses/constant_propagator.cpp @@ -45,7 +45,8 @@ void constant_propagator_domaint::transform( locationt from, locationt to, ai_baset &ai, - const namespacet &ns) + const namespacet &ns, + ai_domain_baset::edge_typet /*edge_type*/) { #ifdef DEBUG std::cout << "Transform from/to:\n"; diff --git a/src/analyses/constant_propagator.h b/src/analyses/constant_propagator.h index 0fc4796e8b7..1431783f918 100644 --- a/src/analyses/constant_propagator.h +++ b/src/analyses/constant_propagator.h @@ -25,7 +25,8 @@ class constant_propagator_domaint:public ai_domain_baset locationt from, locationt to, ai_baset &ai_base, - const namespacet &ns) final override; + const namespacet &ns, + ai_domain_baset::edge_typet edge_type) 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 16c3fad0c4f..e86efba1524 100644 --- a/src/analyses/custom_bitvector_analysis.cpp +++ b/src/analyses/custom_bitvector_analysis.cpp @@ -269,7 +269,8 @@ void custom_bitvector_domaint::transform( locationt from, locationt to, ai_baset &ai, - const namespacet &ns) + const namespacet &ns, + ai_domain_baset::edge_typet /*edge_type*/) { // upcast of ai custom_bitvector_analysist &cba= diff --git a/src/analyses/custom_bitvector_analysis.h b/src/analyses/custom_bitvector_analysis.h index 4896d768cb7..e64a83e585c 100644 --- a/src/analyses/custom_bitvector_analysis.h +++ b/src/analyses/custom_bitvector_analysis.h @@ -27,7 +27,8 @@ class custom_bitvector_domaint:public ai_domain_baset locationt from, locationt to, ai_baset &ai, - const namespacet &ns) final override; + const namespacet &ns, + ai_domain_baset::edge_typet edge_type) final override; void output( std::ostream &out, diff --git a/src/analyses/dependence_graph.cpp b/src/analyses/dependence_graph.cpp index 5f1bae158bc..af9a3aed953 100644 --- a/src/analyses/dependence_graph.cpp +++ b/src/analyses/dependence_graph.cpp @@ -187,7 +187,8 @@ void dep_graph_domaint::transform( goto_programt::const_targett from, goto_programt::const_targett to, ai_baset &ai, - const namespacet &ns) + const namespacet &ns, + ai_domain_baset::edge_typet /*edge_type*/) { 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 30b97108776..97f7548e0f7 100644 --- a/src/analyses/dependence_graph.h +++ b/src/analyses/dependence_graph.h @@ -83,7 +83,8 @@ 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 override; + const namespacet &ns, + ai_domain_baset::edge_typet edge_type) final override; void output( std::ostream &out, diff --git a/src/analyses/escape_analysis.cpp b/src/analyses/escape_analysis.cpp index 507df39f770..5b4585d421b 100644 --- a/src/analyses/escape_analysis.cpp +++ b/src/analyses/escape_analysis.cpp @@ -165,7 +165,8 @@ void escape_domaint::transform( locationt from, locationt to, ai_baset &ai, - const namespacet &ns) + const namespacet &ns, + ai_domain_baset::edge_typet /*edge_type*/) { if(has_values.is_false()) return; diff --git a/src/analyses/escape_analysis.h b/src/analyses/escape_analysis.h index 52de2b5dfc8..0020859bf8f 100644 --- a/src/analyses/escape_analysis.h +++ b/src/analyses/escape_analysis.h @@ -32,7 +32,8 @@ class escape_domaint:public ai_domain_baset locationt from, locationt to, ai_baset &ai, - const namespacet &ns) final override; + const namespacet &ns, + ai_domain_baset::edge_typet edge_type) final override; void output( std::ostream &out, diff --git a/src/analyses/global_may_alias.cpp b/src/analyses/global_may_alias.cpp index 82c1f5a72dc..32f4f32589b 100644 --- a/src/analyses/global_may_alias.cpp +++ b/src/analyses/global_may_alias.cpp @@ -79,7 +79,8 @@ void global_may_alias_domaint::transform( locationt from, locationt to, ai_baset &ai, - const namespacet &ns) + const namespacet &ns, + ai_domain_baset::edge_typet /*edge_type*/) { if(has_values.is_false()) return; diff --git a/src/analyses/global_may_alias.h b/src/analyses/global_may_alias.h index a5e1b0cd49a..5ab40edbe57 100644 --- a/src/analyses/global_may_alias.h +++ b/src/analyses/global_may_alias.h @@ -32,7 +32,8 @@ class global_may_alias_domaint:public ai_domain_baset locationt from, locationt to, ai_baset &ai, - const namespacet &ns) final override; + const namespacet &ns, + ai_domain_baset::edge_typet edge_type) final override; void output( std::ostream &out, diff --git a/src/analyses/interval_domain.cpp b/src/analyses/interval_domain.cpp index 5f1b9a314b5..649e24b8a60 100644 --- a/src/analyses/interval_domain.cpp +++ b/src/analyses/interval_domain.cpp @@ -59,7 +59,8 @@ void interval_domaint::transform( locationt from, locationt to, ai_baset &ai, - const namespacet &ns) + const namespacet &ns, + ai_domain_baset::edge_typet /*edge_type*/) { const goto_programt::instructiont &instruction=*from; switch(instruction.type) diff --git a/src/analyses/interval_domain.h b/src/analyses/interval_domain.h index 7702990d53d..16dc3cbdd7b 100644 --- a/src/analyses/interval_domain.h +++ b/src/analyses/interval_domain.h @@ -36,7 +36,8 @@ class interval_domaint:public ai_domain_baset locationt from, locationt to, ai_baset &ai, - const namespacet &ns) final override; + const namespacet &ns, + ai_domain_baset::edge_typet edge_type) final override; void output( std::ostream &out, diff --git a/src/analyses/invariant_set_domain.cpp b/src/analyses/invariant_set_domain.cpp index 3132591eb42..d7e3800786b 100644 --- a/src/analyses/invariant_set_domain.cpp +++ b/src/analyses/invariant_set_domain.cpp @@ -17,7 +17,8 @@ void invariant_set_domaint::transform( locationt from_l, locationt to_l, ai_baset &ai, - const namespacet &ns) + const namespacet &ns, + ai_domain_baset::edge_typet /*edge_type*/) { switch(from_l->type) { diff --git a/src/analyses/invariant_set_domain.h b/src/analyses/invariant_set_domain.h index 367e987c709..59e29b4efa6 100644 --- a/src/analyses/invariant_set_domain.h +++ b/src/analyses/invariant_set_domain.h @@ -56,7 +56,8 @@ class invariant_set_domaint:public ai_domain_baset locationt from_l, locationt to_l, ai_baset &ai, - const namespacet &ns) final override; + const namespacet &ns, + ai_domain_baset::edge_typet edge_type) final override; void make_top() final override { diff --git a/src/analyses/is_threaded.cpp b/src/analyses/is_threaded.cpp index 54a3fa2d70d..2910bf3c629 100644 --- a/src/analyses/is_threaded.cpp +++ b/src/analyses/is_threaded.cpp @@ -52,7 +52,8 @@ class is_threaded_domaint:public ai_domain_baset locationt from, locationt to, ai_baset &ai, - const namespacet &ns) final override + const namespacet &ns, + ai_domain_baset::edge_typet /*edge_type*/) final override { // assert(reachable); diff --git a/src/analyses/reaching_definitions.cpp b/src/analyses/reaching_definitions.cpp index c3242849511..48b2f81f16f 100644 --- a/src/analyses/reaching_definitions.cpp +++ b/src/analyses/reaching_definitions.cpp @@ -59,7 +59,8 @@ void rd_range_domaint::transform( locationt from, locationt to, ai_baset &ai, - const namespacet &ns) + const namespacet &ns, + ai_domain_baset::edge_typet /*edge_type*/) { reaching_definitions_analysist *rd= dynamic_cast(&ai); diff --git a/src/analyses/reaching_definitions.h b/src/analyses/reaching_definitions.h index e218eb19bca..499b4064967 100644 --- a/src/analyses/reaching_definitions.h +++ b/src/analyses/reaching_definitions.h @@ -117,7 +117,8 @@ class rd_range_domaint:public ai_domain_baset locationt from, locationt to, ai_baset &ai, - const namespacet &ns) final override; + const namespacet &ns, + ai_domain_baset::edge_typet edge_type) final override; void output( std::ostream &out, diff --git a/src/analyses/uninitialized_domain.cpp b/src/analyses/uninitialized_domain.cpp index 4f92eaebd49..5310f0ffcb0 100644 --- a/src/analyses/uninitialized_domain.cpp +++ b/src/analyses/uninitialized_domain.cpp @@ -20,7 +20,8 @@ void uninitialized_domaint::transform( locationt from, locationt to, ai_baset &ai, - const namespacet &ns) + const namespacet &ns, + ai_domain_baset::edge_typet /*edge_type*/) { if(has_values.is_false()) return; diff --git a/src/analyses/uninitialized_domain.h b/src/analyses/uninitialized_domain.h index 45a9d085c99..afc0b71fed7 100644 --- a/src/analyses/uninitialized_domain.h +++ b/src/analyses/uninitialized_domain.h @@ -33,7 +33,8 @@ class uninitialized_domaint:public ai_domain_baset locationt from, locationt to, ai_baset &ai, - const namespacet &ns) final override; + const namespacet &ns, + ai_domain_baset::edge_typet edge_type) 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 c8ea9dae2d2..004ae391a60 100644 --- a/unit/analyses/ai/ai_simplify_lhs.cpp +++ b/unit/analyses/ai/ai_simplify_lhs.cpp @@ -25,7 +25,12 @@ class constant_simplification_mockt:public ai_domain_baset { public: - void transform(locationt, locationt, ai_baset &, const namespacet &) override + void transform( + locationt, + locationt, + ai_baset &, + const namespacet &, + ai_domain_baset::edge_typet) override {} void make_bottom() override {} From 394c42d015793e5d435f5f0d32bf691d2d02db94 Mon Sep 17 00:00:00 2001 From: reuk Date: Wed, 22 Nov 2017 11:33:55 +0000 Subject: [PATCH 03/16] Fix iterator comparison bug in reaching_definitions.cpp --- src/analyses/reaching_definitions.cpp | 12 +++++------- src/analyses/reaching_definitions.h | 3 ++- 2 files changed, 7 insertions(+), 8 deletions(-) diff --git a/src/analyses/reaching_definitions.cpp b/src/analyses/reaching_definitions.cpp index 48b2f81f16f..02cdfa4dd2c 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); + transform_function_call(ns, from, to, *rd, edge_type); // cleanup parameters else if(from->is_end_function()) transform_end_function(ns, from, to, *rd); @@ -170,15 +170,13 @@ void rd_range_domaint::transform_function_call( const namespacet &ns, locationt from, locationt to, - reaching_definitions_analysist &rd) + reaching_definitions_analysist &rd, + ai_domain_baset::edge_typet edge_type) { 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(edge_type != ai_domain_baset::edge_typet::FUNCTION_LOCAL) { for(valuest::iterator it=values.begin(); it!=values.end(); diff --git a/src/analyses/reaching_definitions.h b/src/analyses/reaching_definitions.h index 499b4064967..ce112c1ed66 100644 --- a/src/analyses/reaching_definitions.h +++ b/src/analyses/reaching_definitions.h @@ -218,7 +218,8 @@ class rd_range_domaint:public ai_domain_baset const namespacet &ns, locationt from, locationt to, - reaching_definitions_analysist &rd); + reaching_definitions_analysist &rd, + ai_domain_baset::edge_typet edge_type); void transform_end_function( const namespacet &ns, locationt from, From e0605b70c359832fa1c274eb6f8d9242dff52953 Mon Sep 17 00:00:00 2001 From: reuk Date: Wed, 22 Nov 2017 11:52:03 +0000 Subject: [PATCH 04/16] Fix iterator equality check bug in dependence_graph.cpp --- src/analyses/dependence_graph.cpp | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) diff --git a/src/analyses/dependence_graph.cpp b/src/analyses/dependence_graph.cpp index af9a3aed953..6d691528ca8 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,10 +196,9 @@ void dep_graph_domaint::transform( // propagate control dependencies across function calls if(from->is_function_call()) { - goto_programt::const_targett next=from; - ++next; + const goto_programt::const_targett next = std::next(from); - if(next==to) + if(edge_type == ai_domain_baset::edge_typet::FUNCTION_LOCAL) { control_dependencies(from, to, *dep_graph); } From af314f588b13b1aa1f04d0c7e35f836b851f723f Mon Sep 17 00:00:00 2001 From: reuk Date: Thu, 23 Nov 2017 10:28:41 +0000 Subject: [PATCH 05/16] Fix iterator equality check bug in custom_bitvector_analysis.cpp --- src/analyses/custom_bitvector_analysis.cpp | 7 ++----- 1 file changed, 2 insertions(+), 5 deletions(-) diff --git a/src/analyses/custom_bitvector_analysis.cpp b/src/analyses/custom_bitvector_analysis.cpp index e86efba1524..0b45099302b 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,11 +396,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(edge_type != ai_domain_baset::edge_typet::FUNCTION_LOCAL) { const code_typet &code_type= to_code_type(ns.lookup(identifier).type); From 6297085f09c4147eea16bba00455d240a3a95496 Mon Sep 17 00:00:00 2001 From: reuk Date: Wed, 22 Nov 2017 10:33:38 +0000 Subject: [PATCH 06/16] Fix iterator comparison bug in expr_iterator --- src/util/expr_iterator.h | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/util/expr_iterator.h b/src/util/expr_iterator.h index be228bcfba4..3fa9ee89860 100644 --- a/src/util/expr_iterator.h +++ b/src/util/expr_iterator.h @@ -53,7 +53,10 @@ struct depth_iterator_expr_statet final inline bool operator==( const depth_iterator_expr_statet &left, const depth_iterator_expr_statet &right) -{ return left.it==right.it && left.expr.get()==right.expr.get(); } +{ + return distance(left.it, left.end) == distance(right.it, right.end) && + left.expr.get() == right.expr.get(); +} /// Depth first search iterator base - iterates over supplied expression /// and all its operands recursively. From 8de0ea351b7bea044cc2228dd814d4806f368cff Mon Sep 17 00:00:00 2001 From: reuk Date: Wed, 22 Nov 2017 11:47:37 +0000 Subject: [PATCH 07/16] Fix iterator equality check bug in ai.h --- src/analyses/ai.h | 4 +++- src/goto-programs/goto_program_template.h | 11 +++++++++++ 2 files changed, 14 insertions(+), 1 deletion(-) diff --git a/src/analyses/ai.h b/src/analyses/ai.h index 5b99be3d507..99d1b130345 100644 --- a/src/analyses/ai.h +++ b/src/analyses/ai.h @@ -409,7 +409,9 @@ class ait:public ai_baset } protected: - typedef std::unordered_map state_mapt; + typedef std:: + unordered_map + state_mapt; state_mapt state_map; // this one creates states, if need be diff --git a/src/goto-programs/goto_program_template.h b/src/goto-programs/goto_program_template.h index 264cf77c77c..772dee7d982 100644 --- a/src/goto-programs/goto_program_template.h +++ b/src/goto-programs/goto_program_template.h @@ -810,4 +810,15 @@ struct const_target_hash_templatet { return t->location_number; } }; +/// Functor to check whether iterators from different collections point at the +/// same object. +struct pointee_address_equalt +{ + template + bool operator()(const A &a, const B &b) const + { + return &(*a) == &(*b); + } +}; + #endif // CPROVER_GOTO_PROGRAMS_GOTO_PROGRAM_TEMPLATE_H From 82d42e57fcd535a04fd33013ce36de5448e41861 Mon Sep 17 00:00:00 2001 From: reuk Date: Wed, 22 Nov 2017 12:32:55 +0000 Subject: [PATCH 08/16] Fix expr iterator mutation bug --- src/util/expr_iterator.h | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/src/util/expr_iterator.h b/src/util/expr_iterator.h index 3fa9ee89860..1c43c953d69 100644 --- a/src/util/expr_iterator.h +++ b/src/util/expr_iterator.h @@ -102,8 +102,12 @@ class depth_iterator_baset depth_iterator_t &next_sibling_or_parent() { PRECONDITION(!m_stack.empty()); - m_stack.back().it=m_stack.back().end; - ++(*this); + m_stack.pop_back(); + if(!m_stack.empty()) + { + ++m_stack.back().it; + return ++(*this); + } return this->downcast(); } From 60ef5aa41f509800f2dfa0ef1dc7809727855029 Mon Sep 17 00:00:00 2001 From: reuk Date: Wed, 22 Nov 2017 14:05:09 +0000 Subject: [PATCH 09/16] Fix use-after-free in c_typecheck_initializer.cpp --- src/ansi-c/c_typecheck_initializer.cpp | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/ansi-c/c_typecheck_initializer.cpp b/src/ansi-c/c_typecheck_initializer.cpp index 4f2804e1521..da5a1ce073c 100644 --- a/src/ansi-c/c_typecheck_initializer.cpp +++ b/src/ansi-c/c_typecheck_initializer.cpp @@ -591,9 +591,9 @@ exprt::operandst::const_iterator c_typecheck_baset::do_designated_initializer( if(dest->operands().empty()) { warning().source_location=value.find_source_location(); - warning() << "initialisation of " << full_type.id() - << " requires initializer list, found " - << value.id() << " instead" << eom; + warning() << "initialisation of " << dest_type.id() + << " requires initializer list, found " << value.id() + << " instead" << eom; // in case of a variable-length array consume all remaining // initializer elements From 18656b2aa37fd8f7fb3eb2eb4aeb513802523954 Mon Sep 17 00:00:00 2001 From: reuk Date: Wed, 22 Nov 2017 14:53:23 +0000 Subject: [PATCH 10/16] Fix iterator equality check bug in graphml_witness.cpp --- src/goto-programs/graphml_witness.cpp | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/src/goto-programs/graphml_witness.cpp b/src/goto-programs/graphml_witness.cpp index 9c2c8d2f51c..e316b00ccba 100644 --- a/src/goto-programs/graphml_witness.cpp +++ b/src/goto-programs/graphml_witness.cpp @@ -18,6 +18,8 @@ Author: Daniel Kroening #include #include +#include + void graphml_witnesst::remove_l0_l1(exprt &expr) { if(expr.id()==ID_symbol) @@ -241,10 +243,10 @@ void graphml_witnesst::operator()(const goto_tracet &goto_trace) continue; } - goto_tracet::stepst::const_iterator next=it; - for(++next; - next!=goto_trace.steps.end() && - (step_to_node[next->step_nr]==sink || it->pc==next->pc); + auto next = std::next(it); + for(; next != goto_trace.steps.end() && + (step_to_node[next->step_nr] == sink || + pointee_address_equalt{}(it->pc, next->pc)); // NOLINT ++next) { // advance From c44ed8c8e94e5623cd57548876335d332f7fd096 Mon Sep 17 00:00:00 2001 From: reuk Date: Wed, 22 Nov 2017 15:42:10 +0000 Subject: [PATCH 11/16] Avoid dereferencing past-the-end iterator in cover.cpp --- src/goto-instrument/cover.cpp | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/goto-instrument/cover.cpp b/src/goto-instrument/cover.cpp index d76afe03b71..6d7f6f387b9 100644 --- a/src/goto-instrument/cover.cpp +++ b/src/goto-instrument/cover.cpp @@ -1553,7 +1553,10 @@ void instrument_cover_goals( remove_repetition(controlling); // for now, we restrict to the case of a single ''decision''; // however, this is not true, e.g., ''? :'' operator. - minimize_mcdc_controlling(controlling, *decisions.begin()); + if(!decisions.empty()) + { + minimize_mcdc_controlling(controlling, *decisions.begin()); + } for(const auto &p : controlling) { From 194ac7cf1703788dae2693e36677c456ae506f41 Mon Sep 17 00:00:00 2001 From: reuk Date: Wed, 22 Nov 2017 18:10:30 +0000 Subject: [PATCH 12/16] Fix null dereference bug in cpp_typecheck_compound_type.cpp --- src/cpp/cpp_typecheck_compound_type.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/cpp/cpp_typecheck_compound_type.cpp b/src/cpp/cpp_typecheck_compound_type.cpp index bb5b9d5a912..3757c8cead1 100644 --- a/src/cpp/cpp_typecheck_compound_type.cpp +++ b/src/cpp/cpp_typecheck_compound_type.cpp @@ -1271,7 +1271,7 @@ void cpp_typecheckt::typecheck_member_function( method_qualifier); } - if(value.id()=="cpp_not_typechecked") + if(value.id() == "cpp_not_typechecked" && value.has_operands()) move_member_initializers(initializers, type, value.op0()); else move_member_initializers(initializers, type, value); From 47933cbf3fb040f92263e8799239e8667c4f9416 Mon Sep 17 00:00:00 2001 From: reuk Date: Thu, 23 Nov 2017 14:06:33 +0000 Subject: [PATCH 13/16] Fix heap use-after-free in string_refinement.cpp --- src/solvers/refinement/string_refinement.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/solvers/refinement/string_refinement.cpp b/src/solvers/refinement/string_refinement.cpp index c25bc90d32d..0b48caff4c3 100644 --- a/src/solvers/refinement/string_refinement.cpp +++ b/src/solvers/refinement/string_refinement.cpp @@ -1808,7 +1808,7 @@ static void initial_index_set( while(!to_process.empty()) { - const exprt &cur = to_process.back(); + const exprt cur = to_process.back(); to_process.pop_back(); if(cur.id() == ID_index && is_char_type(cur.type())) { From ef929ea867b949266e53c60856839411a3f82c5a Mon Sep 17 00:00:00 2001 From: reuk Date: Thu, 23 Nov 2017 14:51:17 +0000 Subject: [PATCH 14/16] Fix iterator equality check bug in constant_propagator.cpp --- 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 230d2b1dd1b..c4174dc8f91 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(to==next) + if(edge_type == ai_domain_baset::edge_typet::FUNCTION_LOCAL) { if(id==CPROVER_PREFIX "set_must" || id==CPROVER_PREFIX "get_must" || From 991d2b7719839c72591166a55977b54a0579dc04 Mon Sep 17 00:00:00 2001 From: reuk Date: Fri, 24 Nov 2017 15:33:28 +0000 Subject: [PATCH 15/16] Fix goto program hash function The hash function for goto program targets previously dereferenced the target and returned the instruction's location number. However, in some circumstances the location number of an instruction might be modified. If some unordered_map/set is using an iterator to a modified instruction as a key, then the collection invariants will be broken, leading to undefined behaviour. This patch switches to using instruction addresses as hash values, allowing any field in the instruction to be modified without affecting the hash result. --- src/goto-programs/goto_program_template.h | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/goto-programs/goto_program_template.h b/src/goto-programs/goto_program_template.h index 772dee7d982..fd48166b0b7 100644 --- a/src/goto-programs/goto_program_template.h +++ b/src/goto-programs/goto_program_template.h @@ -807,7 +807,10 @@ struct const_target_hash_templatet { std::size_t operator()( const typename goto_program_templatet::const_targett t) const - { return t->location_number; } + { + using hash_typet = decltype(&(*t)); + return std::hash{}(&(*t)); + } }; /// Functor to check whether iterators from different collections point at the From d423c65705b81ecf8b7e724a627836ab3a03e49e Mon Sep 17 00:00:00 2001 From: reuk Date: Fri, 24 Nov 2017 17:08:28 +0000 Subject: [PATCH 16/16] Mark tests which fail due to invariant violations There was an issue in cover.cpp where the begin() of an empty vector was dereferenced. To avoid this case, we add an INVARIANT which checks that the vector has at least one element. However, this causes some of the tests to fail, so these have been marked KNOWNBUG. --- regression/cbmc-cover/built-ins7/test.desc | 5 ++++- regression/cbmc-cover/mcdc1/test.desc | 5 ++++- regression/cbmc-cover/mcdc10/test.desc | 5 ++++- regression/cbmc-cover/mcdc11/test.desc | 5 ++++- regression/cbmc-cover/mcdc12/test.desc | 5 ++++- regression/cbmc-cover/mcdc13/test.desc | 5 ++++- regression/cbmc-cover/mcdc14/test.desc | 5 ++++- regression/cbmc-cover/mcdc2/test.desc | 5 ++++- regression/cbmc-cover/mcdc3/test.desc | 5 ++++- regression/cbmc-cover/mcdc4/test.desc | 5 ++++- regression/cbmc-cover/mcdc5/test.desc | 5 ++++- regression/cbmc-cover/mcdc6/test.desc | 5 ++++- regression/cbmc-cover/mcdc7/test.desc | 5 ++++- regression/cbmc-cover/mcdc8/test.desc | 5 ++++- regression/cbmc-cover/mcdc9/test.desc | 5 ++++- src/goto-instrument/cover.cpp | 6 ++---- 16 files changed, 62 insertions(+), 19 deletions(-) diff --git a/regression/cbmc-cover/built-ins7/test.desc b/regression/cbmc-cover/built-ins7/test.desc index cea40c3340e..bcffa040ad5 100644 --- a/regression/cbmc-cover/built-ins7/test.desc +++ b/regression/cbmc-cover/built-ins7/test.desc @@ -1,4 +1,4 @@ -CORE +KNOWNBUG main.c --cover mcdc --unwind 5 ^EXIT=0$ @@ -7,3 +7,6 @@ main.c -- ^warning: ignoring ^\[.*