From 0c26a53595098bf6eec4e290c01604f5ca7f940b Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Fri, 1 Jun 2018 17:13:04 +0100 Subject: [PATCH 1/5] let_count_idt is now a struct --- src/solvers/smt2/smt2_conv.cpp | 8 ++++---- src/solvers/smt2/smt2_conv.h | 17 +++++++++++++---- 2 files changed, 17 insertions(+), 8 deletions(-) diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp index dfd55665af1..ae9501f5743 100644 --- a/src/solvers/smt2/smt2_conv.cpp +++ b/src/solvers/smt2/smt2_conv.cpp @@ -4759,12 +4759,12 @@ exprt smt2_convt::letify_rec( exprt current=let_order[i]; assert(map.find(current)!=map.end()); - if(map.find(current)->second.firstsecond.count < LET_COUNT) return letify_rec(expr, let_order, map, i+1); let_exprt let; - let.symbol() = map.find(current)->second.second; + let.symbol() = map.find(current)->second.let_symbol; let.value() = substitute_let(current, map); let.where() = letify_rec(expr, let_order, map, i+1); @@ -4781,7 +4781,7 @@ void smt2_convt::collect_bindings( if(it!=map.end()) { let_count_idt &count_id=it->second; - ++(count_id.first); + ++(count_id.count); return; } @@ -4797,7 +4797,7 @@ void smt2_convt::collect_bindings( symbol_exprt let= symbol_exprt("_let_"+std::to_string(++let_id_count), expr.type()); - map.insert(std::make_pair(expr, std::make_pair(1, let))); + map.insert(std::make_pair(expr, let_count_idt(1, let))); let_order.push_back(expr); } diff --git a/src/solvers/smt2/smt2_conv.h b/src/solvers/smt2/smt2_conv.h index 41d8564050b..520b79ac209 100644 --- a/src/solvers/smt2/smt2_conv.h +++ b/src/solvers/smt2/smt2_conv.h @@ -170,7 +170,17 @@ class smt2_convt:public prop_convt void find_symbols_rec(const typet &type, std::set &recstack); // letification - typedef std::pair let_count_idt; + struct let_count_idt + { + let_count_idt(std::size_t _count, const symbol_exprt &_let_symbol) + : count(_count), let_symbol(_let_symbol) + { + } + + std::size_t count; + symbol_exprt let_symbol; + }; + typedef std::unordered_map seen_expressionst; unsigned let_id_count; static const unsigned LET_COUNT=2; @@ -185,10 +195,9 @@ class smt2_convt:public prop_convt void operator()(exprt &expr) { seen_expressionst::const_iterator it=let_map.find(expr); - if(it!=let_map.end() && - it->second.first>=LET_COUNT) + if(it != let_map.end() && it->second.count >= LET_COUNT) { - symbol_exprt symb=it->second.second; + const symbol_exprt &symb = it->second.let_symbol; expr=symb; } } From 45436ce4eb208770980eb44ac092392d16eae88a Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Fri, 1 Jun 2018 17:15:08 +0100 Subject: [PATCH 2/5] use std::size_t for container sizes --- src/solvers/smt2/smt2_conv.cpp | 18 +++++++++--------- src/solvers/smt2/smt2_conv.h | 8 ++++---- 2 files changed, 13 insertions(+), 13 deletions(-) diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp index ae9501f5743..0cd206a36df 100644 --- a/src/solvers/smt2/smt2_conv.cpp +++ b/src/solvers/smt2/smt2_conv.cpp @@ -287,24 +287,24 @@ constant_exprt smt2_convt::parse_literal( src.get_sub()[0].id()=="_" && src.get_sub()[1].id()=="+oo") // (_ +oo e s) { - unsigned e=unsafe_string2unsigned(src.get_sub()[2].id_string()); - unsigned s=unsafe_string2unsigned(src.get_sub()[3].id_string()); + std::size_t e = unsafe_string2size_t(src.get_sub()[2].id_string()); + std::size_t s = unsafe_string2size_t(src.get_sub()[3].id_string()); return ieee_floatt::plus_infinity(ieee_float_spect(s, e)).to_expr(); } else if(src.get_sub().size()==4 && src.get_sub()[0].id()=="_" && src.get_sub()[1].id()=="-oo") // (_ -oo e s) { - unsigned e=unsafe_string2unsigned(src.get_sub()[2].id_string()); - unsigned s=unsafe_string2unsigned(src.get_sub()[3].id_string()); + std::size_t e = unsafe_string2size_t(src.get_sub()[2].id_string()); + std::size_t s = unsafe_string2size_t(src.get_sub()[3].id_string()); return ieee_floatt::minus_infinity(ieee_float_spect(s, e)).to_expr(); } else if(src.get_sub().size()==4 && src.get_sub()[0].id()=="_" && src.get_sub()[1].id()=="NaN") // (_ NaN e s) { - unsigned e=unsafe_string2unsigned(src.get_sub()[2].id_string()); - unsigned s=unsafe_string2unsigned(src.get_sub()[3].id_string()); + std::size_t e = unsafe_string2size_t(src.get_sub()[2].id_string()); + std::size_t s = unsafe_string2size_t(src.get_sub()[3].id_string()); return ieee_floatt::NaN(ieee_float_spect(s, e)).to_expr(); } @@ -4333,7 +4333,7 @@ void smt2_convt::find_symbols(const exprt &expr) << " -> " << type2id(expr.type()) << "\n" << "(define-fun " << function << " ("; - for(unsigned i=0; i &let_order, const seen_expressionst &map, - unsigned i) + std::size_t i) { if(i>=let_order.size()) return substitute_let(expr, map); diff --git a/src/solvers/smt2/smt2_conv.h b/src/solvers/smt2/smt2_conv.h index 520b79ac209..5d7d10490d8 100644 --- a/src/solvers/smt2/smt2_conv.h +++ b/src/solvers/smt2/smt2_conv.h @@ -182,8 +182,8 @@ class smt2_convt:public prop_convt }; typedef std::unordered_map seen_expressionst; - unsigned let_id_count; - static const unsigned LET_COUNT=2; + std::size_t let_id_count; + static const std::size_t LET_COUNT = 2; class let_visitort:public expr_visitort { @@ -208,7 +208,7 @@ class smt2_convt:public prop_convt exprt &expr, std::vector &let_order, const seen_expressionst &map, - unsigned i); + std::size_t i); void collect_bindings( exprt &expr, @@ -303,7 +303,7 @@ class smt2_convt:public prop_convt smt2_identifierst smt2_identifiers; // Boolean part - unsigned no_boolean_variables; + std::size_t no_boolean_variables; std::vector boolean_assignment; }; From da0adfe9ca323d450b29ad3128e123262f5b7753 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Fri, 1 Jun 2018 18:13:33 +0100 Subject: [PATCH 3/5] bugfix: irep_hash_containert now keeps a copy of the contained ireps --- src/util/irep_hash_container.cpp | 6 ++++-- src/util/irep_hash_container.h | 11 ++++++++--- 2 files changed, 12 insertions(+), 5 deletions(-) diff --git a/src/util/irep_hash_container.cpp b/src/util/irep_hash_container.cpp index c72d2315928..dc79d098670 100644 --- a/src/util/irep_hash_container.cpp +++ b/src/util/irep_hash_container.cpp @@ -21,13 +21,15 @@ size_t irep_hash_container_baset::number(const irept &irep) ptr_hasht::const_iterator it=ptr_hash.find(&irep.read()); if(it!=ptr_hash.end()) - return it->second; + return it->second.number; packedt packed; pack(irep, packed); size_t id=numbering.number(packed); - ptr_hash[&irep.read()]=id; + auto &irep_entry = ptr_hash[&irep.read()]; + irep_entry.number = id; + irep_entry.irep = irep; return id; } diff --git a/src/util/irep_hash_container.h b/src/util/irep_hash_container.h index 65342ba99b1..a154ba557f0 100644 --- a/src/util/irep_hash_container.h +++ b/src/util/irep_hash_container.h @@ -14,10 +14,9 @@ Author: Daniel Kroening, kroening@kroening.com #include +#include "irep.h" #include "numbering.h" -class irept; - class irep_hash_container_baset { public: @@ -46,7 +45,13 @@ class irep_hash_container_baset } }; - typedef std::unordered_map + struct irep_entryt + { + std::size_t number; + irept irep; // copy to keep addresses stable + }; + + typedef std::unordered_map ptr_hasht; ptr_hasht ptr_hash; From 9a0ffae21af6aedd8e71ecb2b1a8f754511a01e8 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Fri, 1 Jun 2018 17:41:59 +0100 Subject: [PATCH 4/5] added irep_hash_mapt --- src/util/irep_hash_container.h | 87 ++++++++++++++++++++++++++++++++++ 1 file changed, 87 insertions(+) diff --git a/src/util/irep_hash_container.h b/src/util/irep_hash_container.h index a154ba557f0..003ee96339b 100644 --- a/src/util/irep_hash_container.h +++ b/src/util/irep_hash_container.h @@ -92,4 +92,91 @@ class irep_full_hash_containert: } }; +template +class irep_hash_mapt +{ +protected: + using mapt = std::map; + +public: + using key_type = Key; + using mapped_type = T; + using value_type = std::pair; + using const_iterator = typename mapt::const_iterator; + using iterator = typename mapt::iterator; + + const_iterator find(const Key &key) const + { + return map.find(hash_container.number(key)); + } + + iterator find(const Key &key) + { + return map.find(hash_container.number(key)); + } + + const_iterator begin() const + { + return map.begin(); + } + + iterator begin() + { + return map.begin(); + } + + const_iterator end() const + { + return map.end(); + } + + iterator end() + { + return map.end(); + } + + void clear() + { + hash_container.clear(); + map.clear(); + } + + std::size_t size() const + { + return map.size(); + } + + bool empty() const + { + return map.empty(); + } + + T &operator[](const Key &key) + { + const std::size_t i = hash_container.number(key); + return map[i]; + } + + std::pair insert(const value_type &value) + { + const std::size_t i = hash_container.number(value.first); + return map.emplace(i, value.second); + } + + void erase(iterator it) + { + map.erase(it); + } + + void swap(irep_hash_mapt &other) + { + std::swap(hash_container, other.hash_container); + std::swap(map, other.map); + } + +protected: + mutable irep_hash_containert hash_container; + mapt map; +}; + #endif // CPROVER_UTIL_IREP_HASH_CONTAINER_H From 022846af6e3199c5b12612216ddd3f7cfa8fd6e2 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Fri, 1 Jun 2018 18:14:19 +0100 Subject: [PATCH 5/5] letify: use irep_hash_mapt when hashing is expensive Fixes: #344 Fixes: #1944 --- regression/cbmc/Float-smt2-1/main.c | 10 ++++++++++ regression/cbmc/Float-smt2-1/test.desc | 8 ++++++++ src/solvers/smt2/smt2_conv.h | 9 +++++++++ 3 files changed, 27 insertions(+) create mode 100644 regression/cbmc/Float-smt2-1/main.c create mode 100644 regression/cbmc/Float-smt2-1/test.desc diff --git a/regression/cbmc/Float-smt2-1/main.c b/regression/cbmc/Float-smt2-1/main.c new file mode 100644 index 00000000000..23881f378d7 --- /dev/null +++ b/regression/cbmc/Float-smt2-1/main.c @@ -0,0 +1,10 @@ +#include + +int main (void) { +float f; + + assert(f * f > 28); + + return 0; +} + diff --git a/regression/cbmc/Float-smt2-1/test.desc b/regression/cbmc/Float-smt2-1/test.desc new file mode 100644 index 00000000000..be435602af4 --- /dev/null +++ b/regression/cbmc/Float-smt2-1/test.desc @@ -0,0 +1,8 @@ +CORE smt-backend +main.c +--smt2 +^EXIT=10$ +^SIGNAL=0$ +-- +Tests a floating-point operation encoding for SMT2 without --fpa. +Owing to heavy use of sharing, this requires sharing-aware hashing. diff --git a/src/solvers/smt2/smt2_conv.h b/src/solvers/smt2/smt2_conv.h index 5d7d10490d8..e89363f4338 100644 --- a/src/solvers/smt2/smt2_conv.h +++ b/src/solvers/smt2/smt2_conv.h @@ -16,6 +16,10 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#ifndef HASH_CODE +#include +#endif + #include #include #include @@ -181,7 +185,12 @@ class smt2_convt:public prop_convt symbol_exprt let_symbol; }; +#ifdef HASH_CODE typedef std::unordered_map seen_expressionst; +#else + typedef irep_hash_mapt seen_expressionst; +#endif + std::size_t let_id_count; static const std::size_t LET_COUNT = 2;