Implement the new pointer encoding for SMT1/2 back ends

Author: tautschnig

src/solvers/smt1/smt1_conv.cpp

@@ -145,20 +145,22 @@ exprt smt1_convt::ce_value(
   else if(type.id()==ID_pointer)
   {
     assert(value.size()==boolbv_width(type));
+    std::size_t object_bits=pointer_logic.get_object_width();
+    std::size_t offset_bits=pointer_logic.get_offset_width();
 
     constant_exprt result(type);
-    result.set_value(value);
+    result.set_value(value.substr(0, object_bits+offset_bits));
 
     // add the elaborated expression as operand
 
     pointer_logict::pointert p;
-    p.object=integer2unsigned(
-      binary2integer(
-        value.substr(0, config.bv_encoding.object_bits), false));
+    p.object=
+      integer2size_t(
+        binary2integer(value.substr(0, object_bits), false));
 
     p.offset=
       binary2integer(
-        value.substr(config.bv_encoding.object_bits, std::string::npos), true);
+        value.substr(object_bits, offset_bits), true);
 
     result.copy_to_operands(
       pointer_logic.pointer_expr(p, to_pointer_type(type)));
@@ -261,13 +263,18 @@ void smt1_convt::convert_address_of_rec(
      expr.id()==ID_string_constant ||
      expr.id()==ID_label)
   {
+    std::string addr=
+      expr.id()==ID_symbol?
+      expr.get_string(ID_identifier)+"$address":
+      "bv0["+std::to_string(pointer_logic.get_address_width())+"]";
+
     out
+      << "(concat "
       << "(concat"
-      << " bv" << pointer_logic.add_object(expr) << "["
-      << config.bv_encoding.object_bits << "]"
-      << " bv0["
-      << boolbv_width(result_type)-config.bv_encoding.object_bits << "]"
-      << ")";
+      << " bv" << pointer_logic.add_object(expr)
+      << "[" << pointer_logic.get_object_width() << "]"
+      << " bv0[" << pointer_logic.get_offset_width() << "]"
+      << ") " << addr << ")";
   }
   else if(expr.id()==ID_index)
   {
@@ -893,33 +900,26 @@ void smt1_convt::convert_expr(const exprt &expr, bool bool_as_bv)
   {
     assert(expr.operands().size()==1);
     assert(expr.op0().type().id()==ID_pointer);
-    std::size_t op_width=boolbv_width(expr.op0().type());
-    out << "(zero_extend[" << config.bv_encoding.object_bits << "] (extract["
-        << (op_width-1-config.bv_encoding.object_bits)
-        << ":0] ";
+    std::size_t object_bits=pointer_logic.get_object_width();
+    std::size_t offset_bits=pointer_logic.get_offset_width();
+    out << "(extract["
+        << object_bits+offset_bits-1 << ":"
+        << object_bits << "] ";
     convert_expr(expr.op0(), true);
-    out << "))";
-    assert(boolbv_width(expr.type())==op_width);
+    out << ")";
+    DATA_INVARIANT(
+      boolbv_width(expr.type()) == offset_bits, "offset encoding mismatch");
   }
   else if(expr.id()==ID_pointer_object)
   {
     assert(expr.operands().size()==1);
     assert(expr.op0().type().id()==ID_pointer);
-    std::size_t op_width=boolbv_width(expr.op0().type());
-    signed int ext=boolbv_width(expr.type())-config.bv_encoding.object_bits;
-
-    if(ext>0)
-      out << "(zero_extend[" << ext << "] ";
-
-    out << "(extract["
-        << (op_width-1)
-        << ":"
-        << op_width-1-config.bv_encoding.object_bits << "] ";
+    std::size_t object_bits=pointer_logic.get_object_width();
+    out << "(extract[" << object_bits-1 << ":0] ";
     convert_expr(expr.op0(), true);
     out << ")";
-
-    if(ext>0)
-      out << ")";
+    DATA_INVARIANT(
+      boolbv_width(expr.type()) == object_bits, "object encoding mismatch");
   }
   else if(expr.id()=="is_dynamic_object")
   {
@@ -931,17 +931,15 @@ void smt1_convt::convert_expr(const exprt &expr, bool bool_as_bv)
 
     assert(expr.operands().size()==1);
     assert(expr.op0().type().id()==ID_pointer);
-    std::size_t op_width=boolbv_width(expr.op0().type());
+    std::size_t object_bits=pointer_logic.get_object_width();
 
     // this may have to be converted
     from_bool_begin(type, bool_as_bv);
 
-    out << "(= (extract["
-        << (op_width-1)
-        << ":" << op_width-config.bv_encoding.object_bits << "] ";
+    out << "(= (extract[" << object_bits-1 << ":0] ";
     convert_expr(expr.op0(), true);
     out << ") bv" << pointer_logic.get_invalid_object()
-        << "[" << config.bv_encoding.object_bits << "])";
+        << "[" << object_bits << "])";
 
     // this may have to be converted
     from_bool_end(type, bool_as_bv);
@@ -1856,12 +1854,14 @@ void smt1_convt::convert_constant(
     if(value==ID_NULL)
     {
       assert(boolbv_width(expr.type())!=0);
-      out << "(concat"
+      out << "(concat "
+          << "(concat"
           << " bv" << pointer_logic.get_null_object()
-          << "[" << config.bv_encoding.object_bits << "]"
-          << " bv0[" << boolbv_width(expr.type())-config.bv_encoding.object_bits
-          << "]"
-          << ")"; // concat
+          << "[" << pointer_logic.get_object_width() << "]"
+          << " bv0[" << pointer_logic.get_offset_width() << "]"
+          << ") "
+          << "bv0[" << pointer_logic.get_address_width() << "]"
+          << ")";
     }
     else
       throw "unknown pointer constant: "+id2string(value);
@@ -1937,7 +1937,7 @@ void smt1_convt::convert_is_dynamic_object(
 
   assert(expr.operands().size()==1);
   assert(expr.op0().type().id()==ID_pointer);
-  std::size_t op_width=boolbv_width(expr.op0().type());
+  std::size_t object_bits=pointer_logic.get_object_width();
 
   // this may have to be converted
   from_bool_begin(expr.type(), bool_as_bv);
@@ -1948,24 +1948,22 @@ void smt1_convt::convert_is_dynamic_object(
   {
     // let is only allowed in formulas
 
-    out << "(let (?obj (extract["
-        << (op_width-1)
-        << ":" << op_width-config.bv_encoding.object_bits << "] ";
+    out << "(let (?obj (extract[" << object_bits-1 << ":0] ";
     convert_expr(expr.op0(), true);
     out << ")) ";
 
     if(dynamic_objects.size()==1)
     {
       out << "(= bv" << dynamic_objects.front()
-          << "[" << config.bv_encoding.object_bits << "] ?obj)";
+          << "[" << object_bits << "] ?obj)";
     }
     else
     {
       out << "(or";
 
       for(const auto &obj : dynamic_objects)
         out << " (= bv" << obj
-            << "[" << config.bv_encoding.object_bits << "] ?obj)";
+            << "[" << object_bits << "] ?obj)";
 
       out << ")"; // or
     }
@@ -2847,6 +2845,14 @@ void smt1_convt::find_symbols(const exprt &expr)
         convert_type(type);
         out << "))" << "\n";
       }
+
+      std::string address_id=id2string(identifier)+"$address";
+
+      out << ":extrafuns(("
+          << convert_identifier(address_id)
+          << " ";
+      convert_type(size_type());
+      out << "))\n";
     }
   }
   else if(expr.id()==ID_array_of)

src/solvers/smt2/smt2_conv.cpp

@@ -138,34 +138,28 @@ void smt2_convt::define_object_size(
   const exprt &expr)
 {
   assert(expr.id()==ID_object_size);
-  const exprt &ptr = expr.op0();
-  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;
+  const exprt &ptr=expr.op0();
+  std::size_t size_width=boolbv_width(expr.type());
+  std::size_t number=0;
+  std::size_t object_bits=pointer_logic.get_object_width();
 
   for(const auto &o : pointer_logic.objects)
   {
-    const typet &type = ns.follow(o.type());
-    exprt size_expr = size_of_expr(type, ns);
-    mp_integer object_size;
+    const typet &type=ns.follow(o.type());
+    mp_integer object_size=pointer_offset_size(type, ns);
 
-    if(o.id()!=ID_symbol ||
-       size_expr.is_nil() ||
-       to_integer(size_expr, object_size))
+    if(o.id()!=ID_symbol || object_size<=0)
     {
       ++number;
       continue;
     }
 
     out << "(assert (implies (= " <<
-      "((_ extract " << h << " " << l << ") ";
+      "((_ extract " << object_bits-1 << " 0) ";
     convert_expr(ptr);
-    out << ") (_ bv" << number << " "
-        << config.bv_encoding.object_bits << "))"
-        << "(= " << id << " (_ bv" << object_size.to_ulong() << " "
-        << size_width << "))))\n";
+    out << ") (_ bv" << number << " " << object_bits << "))" <<
+      "(= " << id << " (_ bv" << object_size.to_ulong() << " " <<
+      size_width << "))))\n";
 
     ++number;
   }
@@ -456,10 +450,12 @@ exprt smt2_convt::parse_rec(const irept &src, const typet &_type)
     to_integer(bv_expr, v);
 
     // split into object and offset
-    mp_integer pow=power(2, width-config.bv_encoding.object_bits);
+    std::size_t object_bits=pointer_logic.get_object_width();
+    std::size_t offset_bits=pointer_logic.get_offset_width();
+    mp_integer pow=power(2, object_bits);
     pointer_logict::pointert ptr;
-    ptr.object=integer2size_t(v/pow);
-    ptr.offset=v%pow;
+    ptr.object=integer2size_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)
@@ -487,12 +483,18 @@ void smt2_convt::convert_address_of_rec(
      expr.id()==ID_string_constant ||
      expr.id()==ID_label)
   {
+    std::string addr=
+      expr.id()==ID_symbol?
+      expr.get_string(ID_identifier)+"$address":
+      "(_ bv0 "+std::to_string(pointer_logic.get_address_width())+")";
+
     out
-      << "(concat (_ bv"
-      << pointer_logic.add_object(expr) << " "
-      << config.bv_encoding.object_bits << ")"
-      << " (_ bv0 "
-      << boolbv_width(result_type)-config.bv_encoding.object_bits << "))";
+      << "(concat "
+      << "(concat "
+      << "(_ bv" << pointer_logic.add_object(expr)
+      << " " << pointer_logic.get_object_width() << ") "
+      << "(_ bv0 " << pointer_logic.get_offset_width() << ")) "
+      << addr << ")";
   }
   else if(expr.id()==ID_index)
   {
@@ -1312,38 +1314,32 @@ void smt2_convt::convert_expr(const exprt &expr)
   {
     assert(expr.operands().size()==1);
     assert(expr.op0().type().id()==ID_pointer);
-    std::size_t offset_bits=
-      boolbv_width(expr.op0().type())-config.bv_encoding.object_bits;
-    std::size_t result_width=boolbv_width(expr.type());
+    std::size_t object_bits=pointer_logic.get_object_width();
+    std::size_t offset_bits=pointer_logic.get_offset_width();
+    std::size_t ext=boolbv_width(expr.type())-offset_bits;
 
-    // max extract width
-    if(offset_bits>result_width)
-      offset_bits=result_width;
-
-    // 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(expr.op0());
     out << ")";
 
-    if(result_width>offset_bits)
+    if(ext>0)
       out << ")"; // zero_extend
   }
   else if(expr.id()==ID_pointer_object)
   {
     assert(expr.operands().size()==1);
     assert(expr.op0().type().id()==ID_pointer);
-    std::size_t ext=boolbv_width(expr.type())-config.bv_encoding.object_bits;
-    std::size_t pointer_width=boolbv_width(expr.op0().type());
+    std::size_t object_bits=pointer_logic.get_object_width();
+    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(expr.op0());
     out << ")";
 
@@ -1357,14 +1353,12 @@ void smt2_convt::convert_expr(const exprt &expr)
   else if(expr.id()==ID_invalid_pointer)
   {
     assert(expr.operands().size()==1);
+    std::size_t object_bits=pointer_logic.get_object_width();
 
-    std::size_t pointer_width=boolbv_width(expr.op0().type());
-    out << "(= ((_ extract "
-        << pointer_width-1 << " "
-        << pointer_width-config.bv_encoding.object_bits << ") ";
+    out << "(= ((_ extract " << object_bits-1 << " 0) ";
     convert_expr(expr.op0());
     out << ") (_ bv" << pointer_logic.get_invalid_object()
-        << " " << config.bv_encoding.object_bits << "))";
+        << " " << object_bits << "))";
   }
   else if(expr.id()=="pointer_object_has_type")
   {
@@ -2721,31 +2715,28 @@ void smt2_convt::convert_is_dynamic_object(const exprt &expr)
   pointer_logic.get_dynamic_objects(dynamic_objects);
 
   assert(expr.operands().size()==1);
+  std::size_t object_bits=pointer_logic.get_object_width();
 
   if(dynamic_objects.empty())
     out << "false";
   else
   {
-    std::size_t pointer_width=boolbv_width(expr.op0().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.op0());
     out << "))) ";
 
     if(dynamic_objects.size()==1)
     {
       out << "(= (_ bv" << dynamic_objects.front()
-          << " " << config.bv_encoding.object_bits << ") ?obj)";
+          << " " << object_bits << ") ?obj)";
     }
     else
     {
       out << "(or";
 
       for(const auto &object : dynamic_objects)
         out << " (= (_ bv" << object
-            << " " << config.bv_encoding.object_bits << ") ?obj)";
+            << " " << object_bits << ") ?obj)";
 
       out << ")"; // or
     }