Compact propositional encoding of OBJECT_SIZE(ptr)

For each OBJECT_SIZE expression to be encoded by the propositional
back-end we previously created a select statement over all objects,
mapping a match to the object's size. This would yield a number of
constraints linear in the number of objects times the number of
OBJECT_SIZE expressions.

For a particular benchmark at hand these were 2047 OBJECT_SIZE
expressions over 1669 objects. Post-processing exceeded 30GB of memory
after several minutes of constructing constraints.

For programs that number of distinct object sizes will be small. In the
above benchmark there are only 8 distinct object sizes (over those 1669
objects). The new encoding groups objects by size by forming a
disjunction of the object identifiers. BDDs are used to compute compact
representations of these disjunctions.

With this new approach, post-processing on the above benchmark completes
in less than 10 seconds and memory never exceeds 3GB.

While at it, use the same trick for compacting the encoding of
IS_DYNAMIC_OBJECT(ptr).

Author: tautschnig

src/solvers/flattening/bv_pointers.cpp

@@ -18,6 +18,10 @@ Author: Daniel Kroening, [email protected]
 #include <util/pointer_expr.h>
 #include <util/pointer_offset_size.h>
 #include <util/pointer_predicates.h>
+#include <util/replace_expr.h>
+
+#include <solvers/prop/bdd_expr.h>
+#include <solvers/prop/literal_expr.h>
 
 /// Map bytes according to the configured endianness. The key difference to
 /// endianness_mapt is that bv_endianness_mapt is aware of the bit-level
@@ -898,112 +902,214 @@ bvt bv_pointerst::add_addr(const exprt &expr)
   return encode(a, type);
 }
 
-void bv_pointerst::do_postponed(
-  const postponedt &postponed)
+std::pair<exprt, exprt> bv_pointerst::prepare_postponed_is_dynamic_object(
+  std::vector<symbol_exprt> &placeholders) const
 {
-  if(postponed.expr.id() == ID_is_dynamic_object)
+  PRECONDITION(placeholders.empty());
+
+  const auto &objects = pointer_logic.objects;
+  std::size_t number = 0;
+
+  exprt::operandst dynamic_objects_ops, not_dynamic_objects_ops;
+  dynamic_objects_ops.reserve(objects.size());
+  not_dynamic_objects_ops.reserve(objects.size());
+
+  for(auto it = objects.cbegin(); it != objects.cend(); ++it, ++number)
   {
-    const auto &type =
-      to_pointer_type(to_unary_expr(postponed.expr).op().type());
-    const auto &objects = pointer_logic.objects;
-    std::size_t number=0;
+    const exprt &expr = *it;
 
-    for(auto it = objects.cbegin(); it != objects.cend(); ++it, ++number)
+    // only compare object part
+    pointer_typet pt = pointer_type(expr.type());
+    bvt bv = object_literals(encode(number, pt), pt);
+
+    exprt::operandst conjuncts;
+    conjuncts.reserve(bv.size());
+    placeholders.reserve(bv.size());
+    for(std::size_t i = 0; i < bv.size(); ++i)
     {
-      const exprt &expr=*it;
+      if(placeholders.size() <= i)
+        placeholders.push_back(symbol_exprt{std::to_string(i), bool_typet{}});
+
+      POSTCONDITION(bv[i].is_constant());
+      if(bv[i].is_true())
+        conjuncts.emplace_back(placeholders[i]);
+      else
+        conjuncts.emplace_back(not_exprt{placeholders[i]});
+    }
 
-      bool is_dynamic=pointer_logic.is_dynamic_object(expr);
+    if(pointer_logic.is_dynamic_object(expr))
+      dynamic_objects_ops.push_back(conjunction(conjuncts));
+    else
+      not_dynamic_objects_ops.push_back(conjunction(conjuncts));
+  }
 
-      // only compare object part
-      pointer_typet pt = pointer_type(expr.type());
-      bvt bv = object_literals(encode(number, pt), type);
+  exprt dynamic_objects = disjunction(dynamic_objects_ops);
+  exprt not_dynamic_objects = disjunction(not_dynamic_objects_ops);
 
-      bvt saved_bv = object_literals(postponed.op, type);
+  bdd_exprt bdd_converter;
+  bddt dyn_bdd = bdd_converter.from_expr(dynamic_objects);
+  bddt not_dyn_bdd = bdd_converter.from_expr(not_dynamic_objects);
 
-      POSTCONDITION(bv.size()==saved_bv.size());
-      PRECONDITION(postponed.bv.size()==1);
+  return {bdd_converter.as_expr(dyn_bdd), bdd_converter.as_expr(not_dyn_bdd)};
+}
 
-      literalt l1=bv_utils.equal(bv, saved_bv);
-      literalt l2=postponed.bv.front();
+std::unordered_map<exprt, exprt, irep_hash>
+bv_pointerst::prepare_postponed_object_size(
+  std::vector<symbol_exprt> &placeholders) const
+{
+  PRECONDITION(placeholders.empty());
 
-      if(!is_dynamic)
-        l2=!l2;
+  const auto &objects = pointer_logic.objects;
+  std::size_t number = 0;
 
-      prop.l_set_to_true(prop.limplies(l1, l2));
-    }
-  }
-  else if(
-    const auto postponed_object_size =
-      expr_try_dynamic_cast<object_size_exprt>(postponed.expr))
+  std::unordered_map<exprt, exprt::operandst, irep_hash> per_size_object_ops;
+
+  for(auto it = objects.cbegin(); it != objects.cend(); ++it, ++number)
   {
-    const auto &type = to_pointer_type(postponed_object_size->pointer().type());
-    const auto &objects = pointer_logic.objects;
-    std::size_t number=0;
+    const exprt &expr = *it;
+
+    if(expr.id() != ID_symbol && expr.id() != ID_string_constant)
+      continue;
 
-    for(auto it = objects.cbegin(); it != objects.cend(); ++it, ++number)
+    const auto size_expr = size_of_expr(expr.type(), ns);
+    if(!size_expr.has_value())
+      continue;
+
+    // only compare object part
+    pointer_typet pt = pointer_type(expr.type());
+    bvt bv = object_literals(encode(number, pt), pt);
+
+    exprt::operandst conjuncts;
+    conjuncts.reserve(bv.size());
+    placeholders.reserve(bv.size());
+    for(std::size_t i = 0; i < bv.size(); ++i)
     {
-      const exprt &expr=*it;
+      if(placeholders.size() <= i)
+        placeholders.push_back(symbol_exprt{std::to_string(i), bool_typet{}});
+
+      POSTCONDITION(bv[i].is_constant());
+      if(bv[i].is_true())
+        conjuncts.emplace_back(placeholders[i]);
+      else
+        conjuncts.emplace_back(not_exprt{placeholders[i]});
+    }
 
-      if(expr.id() != ID_symbol && expr.id() != ID_string_constant)
-        continue;
+    per_size_object_ops[size_expr.value()].push_back(conjunction(conjuncts));
+  }
 
-      const auto size_expr = size_of_expr(expr.type(), ns);
+  std::unordered_map<exprt, exprt, irep_hash> result;
+  for(const auto &size_entry : per_size_object_ops)
+  {
+    exprt all_objects_this_size = disjunction(size_entry.second);
+    bdd_exprt bdd_converter;
+    bddt bdd = bdd_converter.from_expr(all_objects_this_size);
 
-      if(!size_expr.has_value())
-        continue;
+    result.emplace(size_entry.first, bdd_converter.as_expr(bdd));
+  }
 
-      const exprt object_size = typecast_exprt::conditional_cast(
-        size_expr.value(), postponed_object_size->type());
+  return result;
+}
 
-      // only compare object part
-      pointer_typet pt = pointer_type(expr.type());
-      bvt bv = object_literals(encode(number, pt), type);
+void bv_pointerst::finish_eager_conversion()
+{
+  // post-processing arrays may yield further objects, do this first
+  SUB::finish_eager_conversion();
 
-      bvt saved_bv = object_literals(postponed.op, type);
+  // it would seem nicer to use `optionalt` here, but GCC >= 12 produces
+  // spurious warnings about accessing uninitialized objects
+  std::pair<exprt, exprt> is_dynamic_expr = {nil_exprt{}, nil_exprt{}};
+  std::vector<symbol_exprt> is_dynamic_placeholders;
 
-      bvt size_bv = convert_bv(object_size);
+  std::unordered_map<exprt, exprt, irep_hash> object_sizes;
+  std::vector<symbol_exprt> object_size_placeholders;
 
-      POSTCONDITION(bv.size()==saved_bv.size());
-      PRECONDITION(postponed.bv.size()>=1);
-      PRECONDITION(size_bv.size() == postponed.bv.size());
+  for(const postponedt &postponed : postponed_list)
+  {
+    if(postponed.expr.id() == ID_is_dynamic_object)
+    {
+      if(is_dynamic_expr.first.is_nil())
+        is_dynamic_expr =
+          prepare_postponed_is_dynamic_object(is_dynamic_placeholders);
 
-      literalt l1=bv_utils.equal(bv, saved_bv);
-      if(l1.is_true())
+      const auto &type =
+        to_pointer_type(to_unary_expr(postponed.expr).op().type());
+      bvt saved_bv = object_literals(postponed.op, type);
+      POSTCONDITION(saved_bv.size() == is_dynamic_placeholders.size());
+      replace_mapt replacements;
+      for(std::size_t i = 0; i < saved_bv.size(); ++i)
       {
-        for(std::size_t i = 0; i < postponed.bv.size(); ++i)
-          prop.set_equal(postponed.bv[i], size_bv[i]);
-        break;
+        replacements.emplace(
+          is_dynamic_placeholders[i], literal_exprt{saved_bv[i]});
       }
-      else if(l1.is_false())
+      exprt is_dyn = is_dynamic_expr.first;
+      replace_expr(replacements, is_dyn);
+      exprt is_not_dyn = is_dynamic_expr.second;
+      replace_expr(replacements, is_not_dyn);
+
+      PRECONDITION(postponed.bv.size() == 1);
+      prop.l_set_to_true(
+        prop.limplies(convert_bv(is_dyn)[0], postponed.bv.front()));
+      prop.l_set_to_true(
+        prop.limplies(convert_bv(is_not_dyn)[0], !postponed.bv.front()));
+    }
+    else if(
+      const auto postponed_object_size =
+        expr_try_dynamic_cast<object_size_exprt>(postponed.expr))
+    {
+      if(object_sizes.empty())
+        object_sizes = prepare_postponed_object_size(object_size_placeholders);
+
+      // we might not have any usable objects
+      if(object_size_placeholders.empty())
         continue;
+
+      const auto &type =
+        to_pointer_type(postponed_object_size->pointer().type());
+      bvt saved_bv = object_literals(postponed.op, type);
+      POSTCONDITION(saved_bv.size() == object_size_placeholders.size());
+      replace_mapt replacements;
+      for(std::size_t i = 0; i < saved_bv.size(); ++i)
+      {
+        replacements.emplace(
+          object_size_placeholders[i], literal_exprt{saved_bv[i]});
+      }
+
+      for(const auto &object_size_entry : object_sizes)
+      {
+        const exprt object_size = typecast_exprt::conditional_cast(
+          object_size_entry.first, postponed_object_size->type());
+        bvt size_bv = convert_bv(object_size);
+        POSTCONDITION(size_bv.size() == postponed.bv.size());
+
+        exprt all_objects_this_size = object_size_entry.second;
+        replace_expr(replacements, all_objects_this_size);
+
+        literalt l1 = convert_bv(all_objects_this_size)[0];
+        if(l1.is_true())
+        {
+          for(std::size_t i = 0; i < postponed.bv.size(); ++i)
+            prop.set_equal(postponed.bv[i], size_bv[i]);
+          break;
+        }
+        else if(l1.is_false())
+          continue;
 #define COMPACT_OBJECT_SIZE_EQ
 #ifndef COMPACT_OBJECT_SIZE_EQ
-      literalt l2=bv_utils.equal(postponed.bv, size_bv);
+        literalt l2 = bv_utils.equal(postponed.bv, size_bv);
 
-      prop.l_set_to_true(prop.limplies(l1, l2));
+        prop.l_set_to_true(prop.limplies(l1, l2));
 #else
-      for(std::size_t i = 0; i < postponed.bv.size(); ++i)
-      {
-        prop.lcnf({!l1, !postponed.bv[i], size_bv[i]});
-        prop.lcnf({!l1, postponed.bv[i], !size_bv[i]});
-      }
+        for(std::size_t i = 0; i < postponed.bv.size(); ++i)
+        {
+          prop.lcnf({!l1, !postponed.bv[i], size_bv[i]});
+          prop.lcnf({!l1, postponed.bv[i], !size_bv[i]});
+        }
 #endif
+      }
     }
+    else
+      UNREACHABLE;
   }
-  else
-    UNREACHABLE;
-}
-
-void bv_pointerst::finish_eager_conversion()
-{
-  // post-processing arrays may yield further objects, do this first
-  SUB::finish_eager_conversion();
-
-  for(postponed_listt::const_iterator
-      it=postponed_list.begin();
-      it!=postponed_list.end();
-      it++)
-    do_postponed(*it);
 
   // Clear the list to avoid re-doing in case of incremental usage.
   postponed_list.clear();

src/solvers/flattening/bv_pointers.h

@@ -92,7 +92,11 @@ class bv_pointerst:public boolbvt
   typedef std::list<postponedt> postponed_listt;
   postponed_listt postponed_list;
 
-  void do_postponed(const postponedt &postponed);
+  std::pair<exprt, exprt> prepare_postponed_is_dynamic_object(
+    std::vector<symbol_exprt> &placeholders) const;
+
+  std::unordered_map<exprt, exprt, irep_hash>
+  prepare_postponed_object_size(std::vector<symbol_exprt> &placeholders) const;
 
   /// Given a pointer encoded in \p bv, extract the literals identifying the
   /// object that the pointer points to.