SMT2: Efficient Letification

regression/cbmc/Float-smt2-1/main.c

@@ -0,0 +1,10 @@
+#include <assert.h>
+
+int main (void) {
+float f;
+
+    assert(f * f > 28);
+
+    return 0;
+}
+

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.

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<expr.operands().size(); i++)
+      for(std::size_t i = 0; i < expr.operands().size(); i++)
       {
         if(i!=0)
           out << " ";
@@ -4347,7 +4347,7 @@ void smt2_convt::find_symbols(const exprt &expr)
       out << ' ';
 
       exprt tmp1=expr;
-      for(unsigned i=0; i<tmp1.operands().size(); i++)
+      for(std::size_t i = 0; i < tmp1.operands().size(); i++)
         tmp1.operands()[i]=
           smt2_symbolt("op"+std::to_string(i), tmp1.operands()[i].type());
 
@@ -4751,20 +4751,20 @@ exprt smt2_convt::letify_rec(
   exprt &expr,
   std::vector<exprt> &let_order,
   const seen_expressionst &map,
-  unsigned i)
+  std::size_t i)
 {
   if(i>=let_order.size())
     return substitute_let(expr, map);
 
   exprt current=let_order[i];
   assert(map.find(current)!=map.end());
 
-  if(map.find(current)->second.first<LET_COUNT)
+  if(map.find(current)->second.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);
 }

src/solvers/smt2/smt2_conv.h

@@ -16,6 +16,10 @@ Author: Daniel Kroening, [email protected]
 #include <util/std_expr.h>
 #include <util/byte_operators.h>
 
+#ifndef HASH_CODE
+#include <util/irep_hash_container.h>
+#endif
+
 #include <solvers/prop/prop_conv.h>
 #include <solvers/flattening/boolbv_width.h>
 #include <solvers/flattening/pointer_logic.h>
@@ -170,10 +174,25 @@ class smt2_convt:public prop_convt
   void find_symbols_rec(const typet &type, std::set<irep_idt> &recstack);
 
   // letification
-  typedef std::pair<unsigned, symbol_exprt> 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;
+  };
+
+#ifdef HASH_CODE
   typedef std::unordered_map<exprt, let_count_idt, irep_hash> seen_expressionst;
-  unsigned let_id_count;
-  static const unsigned LET_COUNT=2;
+#else
+  typedef irep_hash_mapt<exprt, let_count_idt> seen_expressionst;
+#endif
+
+  std::size_t let_id_count;
+  static const std::size_t LET_COUNT = 2;
 
   class let_visitort:public expr_visitort
   {
@@ -185,10 +204,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;
       }
     }
@@ -199,7 +217,7 @@ class smt2_convt:public prop_convt
     exprt &expr,
     std::vector<exprt> &let_order,
     const seen_expressionst &map,
-    unsigned i);
+    std::size_t i);
 
   void collect_bindings(
     exprt &expr,
@@ -294,7 +312,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<bool> boolean_assignment;
 };
 

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;
 }

src/util/irep_hash_container.h

@@ -14,10 +14,9 @@ Author: Daniel Kroening, [email protected]
 
 #include <vector>
 
+#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<const void *, std::size_t, pointer_hasht>
+  struct irep_entryt
+  {
+    std::size_t number;
+    irept irep; // copy to keep addresses stable
+  };
+
+  typedef std::unordered_map<const void *, irep_entryt, pointer_hasht>
     ptr_hasht;
   ptr_hasht ptr_hash;
 
@@ -87,4 +92,91 @@ class irep_full_hash_containert:
   }
 };
 
+template <typename Key, typename T>
+class irep_hash_mapt
+{
+protected:
+  using mapt = std::map<std::size_t, T>;
+
+public:
+  using key_type = Key;
+  using mapped_type = T;
+  using value_type = std::pair<const Key, T>;
+  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<iterator, bool> 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<Key, T> &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