pointer encoding

Author: kroening

src/solvers/flattening/bv_pointers.cpp

@@ -91,33 +91,79 @@ std::size_t bv_pointerst::get_address_width(const pointer_typet &type) const
 }
 
 bvt bv_pointerst::object_literals(const bvt &bv, const pointer_typet &type)
-  const
 {
-  const std::size_t offset_width = get_offset_width(type);
-  const std::size_t object_width = get_object_width(type);
-  PRECONDITION(bv.size() >= offset_width + object_width);
+  const auto width = type.get_width();
+  PRECONDITION(width == bv.size());
+
+  const auto result = prop.new_variables(width);
 
-  return bvt(
-    bv.begin() + offset_width, bv.begin() + offset_width + object_width);
+  for(std::size_t i = 0; i < numbered_pointers.size(); i++)
+  {
+    auto cond = bv_utils.equal(
+      bv,
+      bv_utilst::concatenate(
+        bv_utilst::build_constant(i, width - 1), {const_literal(true)}));
+    bv_utils.cond_implies_equal(
+      cond,
+      bv_utilst::zero_extension(numbered_pointers[i].first, width),
+      result);
+  }
+
+  // the top bit distinguishes 'object only' vs. 'table encoded'
+  return bv_utils.select(bv.back(), bv_utils.zeros(width), result);
 }
 
 bvt bv_pointerst::offset_literals(const bvt &bv, const pointer_typet &type)
-  const
 {
-  const std::size_t offset_width = get_offset_width(type);
-  PRECONDITION(bv.size() >= offset_width);
+  const auto width = type.get_width();
+  PRECONDITION(width == bv.size());
+
+  const auto result = prop.new_variables(width);
 
-  return bvt(bv.begin(), bv.begin() + offset_width);
+  for(std::size_t i = 0; i < numbered_pointers.size(); i++)
+  {
+    auto cond = bv_utils.equal(
+      bv,
+      bv_utilst::concatenate(
+        bv_utilst::build_constant(i, width - 1), {const_literal(true)}));
+    bv_utils.cond_implies_equal(
+      cond,
+      bv_utilst::sign_extension(numbered_pointers[i].second, width),
+      result);
+  }
+
+  // the top bit distinguishes 'object only' vs. 'table encoded'
+  return bv_utils.select(bv.back(), bv_utils.zeros(width), result);
 }
 
-bvt bv_pointerst::object_offset_encoding(const bvt &object, const bvt &offset)
+bvt bv_pointerst::object_offset_encoding(
+  const bvt &object,
+  const bvt &offset,
+  const pointer_typet &type)
 {
-  bvt result;
-  result.reserve(offset.size() + object.size());
-  result.insert(result.end(), offset.begin(), offset.end());
-  result.insert(result.end(), object.begin(), object.end());
+  const auto width = type.get_width();
 
-  return result;
+  // is the offset zero?
+  if(std::find_if_not(offset.begin(), offset.end(), [](literalt l) {
+       return l == const_literal(false);
+     }) != offset.end())
+  {
+    // offset is not zero, add to the pointer table
+    auto number = numbered_pointers.size();
+    numbered_pointers.emplace_back(object, offset);
+
+    // Encode the table index.
+    // Also set top bit to distinguish from object-only pointers.
+    return bv_utilst::concatenate(
+      bv_utilst::build_constant(number, width - 1), {const_literal(true)});
+  }
+  else
+  {
+    // Offset is zero, just zero-extend object number.
+    // Top bit is zero to indicate object-only pointer.
+    return bv_utilst::concatenate(
+      bv_utilst::zero_extension(object, width - 1), {const_literal(false)});
+  }
 }
 
 literalt bv_pointerst::convert_rest(const exprt &expr)
@@ -794,42 +840,49 @@ exprt bv_pointerst::bv_get_rec(
   bvt value_bv(bv.begin() + offset, bv.begin() + offset + bits);
 
   std::string value = bits_to_string(prop, value_bv);
-  std::string value_addr = bits_to_string(prop, object_literals(value_bv, pt));
-  std::string value_offset =
-    bits_to_string(prop, offset_literals(value_bv, pt));
-
   // we treat these like bit-vector constants, but with
   // some additional annotation
-
   const irep_idt bvrep = make_bvrep(bits, [&value](std::size_t i) {
     return value[value.size() - 1 - i] == '1';
   });
 
   constant_exprt result(bvrep, type);
 
   pointer_logict::pointert pointer;
-  pointer.object =
-    numeric_cast_v<std::size_t>(binary2integer(value_addr, false));
-  pointer.offset=binary2integer(value_offset, true);
+
+  // Top bit set?
+  if(value.front() == '1')
+  {
+    // It's a pointer into the table.
+    std::string value_addr =
+      bits_to_string(prop, object_literals(value_bv, pt));
+    std::string value_offset =
+      bits_to_string(prop, offset_literals(value_bv, pt));
+
+    pointer.object =
+      numeric_cast_v<std::size_t>(binary2integer(value_addr, false));
+    pointer.offset = binary2integer(value_offset, true);
+  }
+  else
+  {
+    // It's an object only, offset is zero.
+    pointer.object = numeric_cast_v<std::size_t>(binary2integer(value, false));
+    pointer.offset = 0;
+  }
 
   return annotated_pointer_constant_exprt{
     bvrep, pointer_logic.pointer_expr(pointer, pt)};
 }
 
 bvt bv_pointerst::encode(std::size_t addr, const pointer_typet &type) const
 {
-  const std::size_t offset_bits = get_offset_width(type);
-  const std::size_t object_bits = get_object_width(type);
-
-  bvt zero_offset(offset_bits, const_literal(false));
+  const auto width = type.get_width();
 
-  // set variable part
-  bvt object;
-  object.reserve(object_bits);
-  for(std::size_t i=0; i<object_bits; i++)
-    object.push_back(const_literal((addr & (std::size_t(1) << i)) != 0));
+  auto object = bv_utilst::build_constant(addr, width - 1);
 
-  return object_offset_encoding(object, zero_offset);
+  // Offset is zero, just zero-extend object number.
+  // Top bit is zero to indicate object-only pointer.
+  return bv_utilst::concatenate(object, {const_literal(false)});
 }
 
 bvt bv_pointerst::offset_arithmetic(
@@ -884,7 +937,7 @@ bvt bv_pointerst::offset_arithmetic(
 
   bvt bv_tmp = bv_utils.add(offset_bv, bv_index);
 
-  return object_offset_encoding(object_literals(bv, type), bv_tmp);
+  return object_offset_encoding(object_literals(bv, type), bv_tmp, type);
 }
 
 bvt bv_pointerst::add_addr(const exprt &expr)

src/solvers/flattening/bv_pointers.h

@@ -94,21 +94,28 @@ class bv_pointerst:public boolbvt
   /// \param bv: Encoded pointer
   /// \param type: Type of the encoded pointer
   /// \return Vector of literals identifying the object part of \p bv
-  bvt object_literals(const bvt &bv, const pointer_typet &type) const;
+  bvt object_literals(const bvt &bv, const pointer_typet &type);
 
   /// Given a pointer encoded in \p bv, extract the literals representing the
   /// offset into an object that the pointer points to.
   /// \param bv: Encoded pointer
   /// \param type: Type of the encoded pointer
   /// \return Vector of literals identifying the offset part of \p bv
-  bvt offset_literals(const bvt &bv, const pointer_typet &type) const;
+  bvt offset_literals(const bvt &bv, const pointer_typet &type);
 
   /// Construct a pointer encoding from given encodings of \p object and \p
   /// offset.
   /// \param object: Encoded object
   /// \param offset: Encoded offset
+  /// \param type: Type of the encoded pointer
   /// \return Pointer encoding
-  static bvt object_offset_encoding(const bvt &object, const bvt &offset);
+  bvt object_offset_encoding(
+    const bvt &object,
+    const bvt &offset,
+    const pointer_typet &type);
+
+  /// Table that maps a 'pointer number' to its object/offset pair
+  std::vector<std::pair<bvt, bvt>> numbered_pointers;
 };
 
 #endif // CPROVER_SOLVERS_FLATTENING_BV_POINTERS_H