Encode integer addresses together with pointer object/offset

Instead of encoding pointers with the same bit width a pointer on a
given platform has, just widen the bit-blasted encoding to include both
the previous object/offset encoding as well as an (integer) address. The
encoding is thus also trivially extended to handle larger numbers of
objects and offsets of the same width as the address.

Furthermore clean up the code to encapsulate encoding properly, and make
in-code layout of pointer encoding more natural (it's now object,
offset, integer-address).

Fixes: diffblue#436
Fixes: diffblue#311
Fixes: diffblue#94

Author: tautschnig

src/solvers/flattening/bv_pointers.cpp

@@ -1160,6 +1160,179 @@ void bv_pointerst::do_postponed(
     UNREACHABLE;
 }
 
+void bv_pointerst::encode_object_bounds(bounds_mapt &dest)
+{
+  const auto &objects = pointer_logic.objects;
+  std::size_t number = 0;
+
+  const bvt null_pointer = pointer_bits.at(pointer_logic.get_null_object());
+  const bvt &invalid_object =
+    pointer_bits.at(pointer_logic.get_invalid_object());
+
+  bvt conj;
+  conj.reserve(objects.size());
+
+  for(const exprt &expr : objects)
+  {
+    const auto size_expr = size_of_expr(expr.type(), ns);
+
+    if(!size_expr.has_value())
+    {
+      ++number;
+      continue;
+    }
+
+    bvt size_bv = convert_bv(*size_expr);
+
+    // NULL, INVALID have no size
+    DATA_INVARIANT(
+      number != pointer_logic.get_null_object(),
+      "NULL object cannot have a size");
+    DATA_INVARIANT(
+      number != pointer_logic.get_invalid_object(),
+      "INVALID object cannot have a size");
+
+    bvt object_bv;
+    encode(number, object_bv);
+
+    // prepare comparison over integers
+    bvt bv = object_bv;
+    address_bv(bv, pointer_type(expr.type()));
+    DATA_INVARIANT(
+      bv.size() == null_pointer.size(),
+      "NULL pointer encoding does not have matching width");
+    DATA_INVARIANT(
+      bv.size() == invalid_object.size(),
+      "INVALID pointer encoding does not have matching width");
+    DATA_INVARIANT(
+      size_bv.size() == bv.size(),
+      "pointer encoding does not have matching width");
+
+    // NULL, INVALID must not be within object bounds
+    literalt null_lower_bound = bv_utils.rel(
+      null_pointer, ID_lt, bv, bv_utilst::representationt::UNSIGNED);
+
+    literalt inv_obj_lower_bound = bv_utils.rel(
+      invalid_object, ID_lt, bv, bv_utilst::representationt::UNSIGNED);
+
+    // compute the upper bound with the side effect of enforcing the
+    // object addresses not to wrap around/overflow
+    bvt obj_upper_bound = bv_utils.add_sub_no_overflow(
+      bv, size_bv, false, bv_utilst::representationt::UNSIGNED);
+
+    literalt null_upper_bound = bv_utils.rel(
+      null_pointer,
+      ID_ge,
+      obj_upper_bound,
+      bv_utilst::representationt::UNSIGNED);
+
+    literalt inv_obj_upper_bound = bv_utils.rel(
+      invalid_object,
+      ID_ge,
+      obj_upper_bound,
+      bv_utilst::representationt::UNSIGNED);
+
+    // store bounds for re-use
+    dest.insert({number, {bv, obj_upper_bound}});
+
+    conj.push_back(prop.lor(null_lower_bound, null_upper_bound));
+    conj.push_back(prop.lor(inv_obj_lower_bound, inv_obj_upper_bound));
+
+    ++number;
+  }
+
+  if(!conj.empty())
+    prop.l_set_to_true(prop.land(conj));
+}
+
+void bv_pointerst::do_postponed_typecast(
+  const postponedt &postponed,
+  const bounds_mapt &bounds)
+{
+  if(postponed.expr.id() != ID_typecast)
+    return;
+
+  const pointer_typet &type = to_pointer_type(postponed.expr.type());
+  const std::size_t bits = boolbv_width.get_offset_width(type) +
+                           boolbv_width.get_object_width(type) +
+                           boolbv_width.get_address_width(type);
+
+  // given an integer (possibly representing an address) postponed.op,
+  // compute the object and offset that it may refer to
+  bvt saved_bv = postponed.op;
+
+  bvt conj, oob_conj;
+  conj.reserve(bounds.size() + 3);
+  oob_conj.reserve(bounds.size());
+
+  for(const auto &bounds_entry : bounds)
+  {
+    std::size_t number = bounds_entry.first;
+
+    // pointer must be within object bounds
+    const bvt &lb = bounds_entry.second.first;
+    const bvt &ub = bounds_entry.second.second;
+
+    literalt lower_bound =
+      bv_utils.rel(saved_bv, ID_ge, lb, bv_utilst::representationt::UNSIGNED);
+
+    literalt upper_bound =
+      bv_utils.rel(saved_bv, ID_lt, ub, bv_utilst::representationt::UNSIGNED);
+
+    // compute the offset within the object, and the corresponding
+    // pointer bv
+    bvt offset = bv_utils.sub(saved_bv, lb);
+
+    bvt bv;
+    encode(number, bv);
+    object_bv(bv, type);
+    DATA_INVARIANT(
+      offset.size() == boolbv_width.get_offset_width(type),
+      "pointer encoding does not have matching width");
+    bv.insert(bv.end(), offset.begin(), offset.end());
+    bv.insert(bv.end(), saved_bv.begin(), saved_bv.end());
+    DATA_INVARIANT(
+      bv.size() == bits, "pointer encoding does not have matching width");
+
+    // if the integer address is within the object bounds, return an
+    // adjusted offset
+    literalt in_bounds = prop.land(lower_bound, upper_bound);
+    conj.push_back(prop.limplies(in_bounds, bv_utils.equal(bv, postponed.bv)));
+    oob_conj.push_back(!in_bounds);
+  }
+
+  // append integer address as both offset and address
+  bvt invalid_bv, null_bv;
+  encode(pointer_logic.get_invalid_object(), invalid_bv);
+  object_bv(invalid_bv, type);
+  invalid_bv.insert(invalid_bv.end(), saved_bv.begin(), saved_bv.end());
+  invalid_bv.insert(invalid_bv.end(), saved_bv.begin(), saved_bv.end());
+  encode(pointer_logic.get_null_object(), null_bv);
+  object_bv(null_bv, type);
+  null_bv.insert(null_bv.end(), saved_bv.begin(), saved_bv.end());
+  null_bv.insert(null_bv.end(), saved_bv.begin(), saved_bv.end());
+
+  // NULL is always NULL
+  conj.push_back(prop.limplies(
+    bv_utils.equal(saved_bv, pointer_bits.at(pointer_logic.get_null_object())),
+    bv_utils.equal(null_bv, postponed.bv)));
+
+  // INVALID is always INVALID
+  conj.push_back(prop.limplies(
+    bv_utils.equal(
+      saved_bv, pointer_bits.at(pointer_logic.get_invalid_object())),
+    bv_utils.equal(invalid_bv, postponed.bv)));
+
+  // one of the objects or NULL or INVALID with an offset
+  conj.push_back(prop.limplies(
+    prop.land(oob_conj),
+    prop.lor(
+      bv_utils.equal(null_bv, postponed.bv),
+      bv_utils.equal(invalid_bv, postponed.bv))));
+
+  prop.l_set_to_true(prop.land(conj));
+}
+
 void bv_pointerst::post_process()
 {
   // post-processing arrays may yield further objects, do this first
@@ -1169,7 +1342,19 @@ void bv_pointerst::post_process()
       it=postponed_list.begin();
       it!=postponed_list.end();
       it++)
-    do_postponed(*it);
+    do_postponed_non_typecast(*it);
+
+  if(need_address_bounds)
+  {
+    // make sure NULL and INVALID are unique addresses
+    bounds_mapt bounds;
+    encode_object_bounds(bounds);
+
+    for(postponed_listt::const_iterator it = postponed_list.begin();
+        it != postponed_list.end();
+        it++)
+      do_postponed_typecast(*it, bounds);
+  }
 
   // Clear the list to avoid re-doing in case of incremental usage.
   postponed_list.clear();

src/solvers/smt2/smt2_conv.cpp

@@ -235,10 +235,9 @@ void smt2_convt::define_object_size(
   PRECONDITION(expr.id() == ID_object_size);
   const exprt &ptr = to_unary_expr(expr).op();
   std::size_t size_width = boolbv_width(expr.type());
-  std::size_t pointer_width = boolbv_width(ptr.type());
   std::size_t number = 0;
-  std::size_t h=pointer_width-1;
-  std::size_t l=pointer_width-config.bv_encoding.object_bits;
+  std::size_t object_bits =
+    boolbv_width.get_object_width(to_pointer_type(ptr.type()));
 
   for(const auto &o : pointer_logic.objects)
   {
@@ -256,11 +255,11 @@ void smt2_convt::define_object_size(
     }
 
     out << "(assert (=> (= "
-        << "((_ extract " << h << " " << l << ") ";
+        << "((_ extract " << object_bits - 1 << " 0) ";
     convert_expr(ptr);
-    out << ") (_ bv" << number << " " << config.bv_encoding.object_bits << "))"
-        << "(= " << id << " (_ bv" << *object_size << " " << size_width
-        << "))))\n";
+    out << ") (_ bv" << number << " " << object_bits << "))"
+        << "(= " << id << " (_ bv" << object_size->to_ulong() << " "
+        << size_width << "))))\n";
 
     ++number;
   }
@@ -593,10 +592,14 @@ exprt smt2_convt::parse_rec(const irept &src, const typet &type)
     mp_integer v = numeric_cast_v<mp_integer>(bv_expr);
 
     // split into object and offset
-    mp_integer pow=power(2, width-config.bv_encoding.object_bits);
+    std::size_t object_bits =
+      boolbv_width.get_object_width(to_pointer_type(type));
+    std::size_t offset_bits =
+      boolbv_width.get_offset_width(to_pointer_type(type));
+    mp_integer pow = power(2, object_bits);
     pointer_logict::pointert ptr;
-    ptr.object = numeric_cast_v<std::size_t>(v / pow);
-    ptr.offset=v%pow;
+    ptr.object = numeric_cast_v<std::size_t>(v % pow);
+    ptr.offset = (v % power(2, object_bits + offset_bits)) / pow;
     return pointer_logic.pointer_expr(ptr, to_pointer_type(type));
   }
   else if(type.id()==ID_struct)
@@ -639,12 +642,18 @@ void smt2_convt::convert_address_of_rec(
      expr.id()==ID_string_constant ||
      expr.id()==ID_label)
   {
-    out
-      << "(concat (_ bv"
-      << pointer_logic.add_object(expr) << " "
-      << config.bv_encoding.object_bits << ")"
-      << " (_ bv0 "
-      << boolbv_width(result_type)-config.bv_encoding.object_bits << "))";
+    std::string addr =
+      expr.id() == ID_symbol
+        ? expr.get_string(ID_identifier) + "$address"
+        : "(_ bv0 " +
+            std::to_string(boolbv_width.get_address_width(result_type)) + ")";
+
+    out << "(concat "
+        << "(concat "
+        << "(_ bv" << pointer_logic.add_object(expr) << " "
+        << boolbv_width.get_object_width(result_type) << ") "
+        << "(_ bv0 " << boolbv_width.get_offset_width(result_type) << ")) "
+        << addr << ")";
   }
   else if(expr.id()==ID_index)
   {
@@ -1485,23 +1494,21 @@ void smt2_convt::convert_expr(const exprt &expr)
       op.type().id() == ID_pointer,
       "operand of pointer offset expression shall be of pointer type");
 
+    std::size_t object_bits =
+      boolbv_width.get_object_width(to_pointer_type(op.type()));
     std::size_t offset_bits =
-      boolbv_width(op.type()) - config.bv_encoding.object_bits;
-    std::size_t result_width=boolbv_width(expr.type());
-
-    // max extract width
-    if(offset_bits>result_width)
-      offset_bits=result_width;
+      boolbv_width.get_offset_width(to_pointer_type(op.type()));
+    std::size_t ext = boolbv_width(expr.type()) - offset_bits;
 
-    // too few bits?
-    if(result_width>offset_bits)
-      out << "((_ zero_extend " << result_width-offset_bits << ") ";
+    if(ext > 0)
+      out << "((_ zero_extend " << ext << ") ";
 
-    out << "((_ extract " << offset_bits-1 << " 0) ";
+    out << "((_ extract " << object_bits + offset_bits - 1 << " " << object_bits
+        << ") ";
     convert_expr(op);
     out << ")";
 
-    if(result_width>offset_bits)
+    if(ext > 0)
       out << ")"; // zero_extend
   }
   else if(expr.id()==ID_pointer_object)
@@ -1512,15 +1519,14 @@ void smt2_convt::convert_expr(const exprt &expr)
       op.type().id() == ID_pointer,
       "pointer object expressions should be of pointer type");
 
-    std::size_t ext=boolbv_width(expr.type())-config.bv_encoding.object_bits;
-    std::size_t pointer_width = boolbv_width(op.type());
+    std::size_t object_bits =
+      boolbv_width.get_object_width(to_pointer_type(op.type()));
+    std::size_t ext = boolbv_width(expr.type()) - object_bits;
 
     if(ext>0)
       out << "((_ zero_extend " << ext << ") ";
 
-    out << "((_ extract "
-        << pointer_width-1 << " "
-        << pointer_width-config.bv_encoding.object_bits << ") ";
+    out << "((_ extract " << object_bits - 1 << " 0) ";
     convert_expr(op);
     out << ")";
 
@@ -1533,14 +1539,13 @@ void smt2_convt::convert_expr(const exprt &expr)
   }
   else if(expr.id() == ID_is_invalid_pointer)
   {
-    const auto &op = to_unary_expr(expr).op();
-    std::size_t pointer_width = boolbv_width(op.type());
-    out << "(= ((_ extract "
-        << pointer_width-1 << " "
-        << pointer_width-config.bv_encoding.object_bits << ") ";
-    convert_expr(op);
-    out << ") (_ bv" << pointer_logic.get_invalid_object()
-        << " " << config.bv_encoding.object_bits << "))";
+    std::size_t object_bits = boolbv_width.get_object_width(
+      to_pointer_type(to_unary_expr(expr).op().type()));
+
+    out << "(= ((_ extract " << object_bits - 1 << " 0) ";
+    convert_expr(to_unary_expr(expr).op());
+    out << ") (_ bv" << pointer_logic.get_invalid_object() << " " << object_bits
+        << "))";
   }
   else if(expr.id()==ID_string_constant)
   {
@@ -3013,30 +3018,28 @@ void smt2_convt::convert_is_dynamic_object(const unary_exprt &expr)
   std::vector<std::size_t> dynamic_objects;
   pointer_logic.get_dynamic_objects(dynamic_objects);
 
+  std::size_t object_bits =
+    boolbv_width.get_object_width(to_pointer_type(expr.op().type()));
+
   if(dynamic_objects.empty())
     out << "false";
   else
   {
-    std::size_t pointer_width = boolbv_width(expr.op().type());
-
-    out << "(let ((?obj ((_ extract "
-        << pointer_width-1 << " "
-        << pointer_width-config.bv_encoding.object_bits << ") ";
+    out << "(let ((?obj ((_ extract " << object_bits << " 0) ";
     convert_expr(expr.op());
     out << "))) ";
 
     if(dynamic_objects.size()==1)
     {
-      out << "(= (_ bv" << dynamic_objects.front()
-          << " " << config.bv_encoding.object_bits << ") ?obj)";
+      out << "(= (_ bv" << dynamic_objects.front() << " " << object_bits
+          << ") ?obj)";
     }
     else
     {
       out << "(or";
 
       for(const auto &object : dynamic_objects)
-        out << " (= (_ bv" << object
-            << " " << config.bv_encoding.object_bits << ") ?obj)";
+        out << " (= (_ bv" << object << " " << object_bits << ") ?obj)";
 
       out << ")"; // or
     }