Pointers now come with a width

Author: kroening

src/ansi-c/ansi_c_convert_type.cpp

@@ -16,7 +16,6 @@ Author: Daniel Kroening, [email protected]
 #include <util/c_types.h>
 #include <util/namespace.h>
 #include <util/simplify_expr.h>
-#include <util/config.h>
 #include <util/arith_tools.h>
 #include <util/std_types.h>
 
@@ -219,8 +218,7 @@ void ansi_c_convert_typet::read_rec(const typet &type)
   else if(type.id()==ID_pointer)
   {
     // pointers have a width, much like integers
-    pointer_typet tmp=to_pointer_type(type);
-    tmp.set_width(config.ansi_c.pointer_width);
+    pointer_typet tmp=pointer_type(to_pointer_type(type).subtype());
     other.push_back(tmp);
   }
   else

src/ansi-c/c_preprocess.cpp

@@ -25,6 +25,7 @@ Author: Daniel Kroening, [email protected]
 
 #include <util/c_types.h>
 #include <util/config.h>
+#include <util/invariant.h>
 #include <util/message.h>
 #include <util/tempfile.h>
 #include <util/unicode.h>
@@ -430,14 +431,17 @@ bool c_preprocess_visual_studio(
     command_file << "/D__CPROVER__" << "\n";
     command_file << "/D__WORDSIZE=" << config.ansi_c.pointer_width << "\n";
 
-    if(config.ansi_c.pointer_width==64)
+    if(pointer_diff_type()==signed_long_long_int_type())
     {
       command_file << "\"/D__PTRDIFF_TYPE__=long long int\""  << "\n";
       // yes, both _WIN32 and _WIN64 get defined
       command_file << "/D_WIN64" << "\n";
     }
     else
     {
+      DATA_INVARIANT(
+        pointer_diff_type()==signed_int_type(),
+        "Pointer difference expected to be int typed");
       command_file << "/D__PTRDIFF_TYPE__=int" << "\n";
       command_file << "/U_WIN64" << "\n";
     }

src/ansi-c/padding.cpp

@@ -73,20 +73,15 @@ mp_integer alignment(const typet &type, const namespacet &ns)
           type.id()==ID_signedbv ||
           type.id()==ID_fixedbv ||
           type.id()==ID_floatbv ||
-          type.id()==ID_c_bool)
+          type.id()==ID_c_bool ||
+          type.id()==ID_pointer)
   {
-    std::size_t width=to_bitvector_type(type).get_width();
-    result=width%8?width/8+1:width/8;
+    result=pointer_offset_size(type, ns);
   }
   else if(type.id()==ID_c_enum)
     result=alignment(type.subtype(), ns);
   else if(type.id()==ID_c_enum_tag)
     result=alignment(ns.follow_tag(to_c_enum_tag_type(type)), ns);
-  else if(type.id()==ID_pointer)
-  {
-    std::size_t width=config.ansi_c.pointer_width;
-    result=width%8?width/8+1:width/8;
-  }
   else if(type.id()==ID_symbol)
     result=alignment(ns.follow(type), ns);
   else if(type.id()==ID_c_bit_field)

src/cpp/cpp_typecheck_type.cpp

@@ -14,7 +14,6 @@ Author: Daniel Kroening, [email protected]
 #include <util/source_location.h>
 #include <util/simplify_expr.h>
 #include <util/c_types.h>
-#include <util/config.h>
 
 #include <ansi-c/c_qualifiers.h>
 
@@ -83,7 +82,7 @@ void cpp_typecheckt::typecheck_type(typet &type)
     typecheck_type(type.subtype());
 
     // we add a width, much like with integers
-    to_pointer_type(type).set_width(config.ansi_c.pointer_width);
+    type=pointer_type(type.subtype());
 
     // Check if it is a pointer-to-member
     if(type.find("to-member").is_not_nil())

src/goto-instrument/accelerate/polynomial_accelerator.cpp

@@ -37,7 +37,6 @@ Author: Matt Lewis
 #include <util/simplify_expr.h>
 #include <util/replace_expr.h>
 #include <util/arith_tools.h>
-#include <util/config.h>
 
 #include "accelerator.h"
 #include "util.h"
@@ -345,9 +344,7 @@ bool polynomial_acceleratort::fit_polynomial_sliced(
     return false;
   }
 
-  unsigned width=to_bitvector_type(var.type()).get_width();
-  if(var.type().id()==ID_pointer)
-    width=config.ansi_c.pointer_width;
+  std::size_t width=to_bitvector_type(var.type()).get_width();
   assert(width>0);
 
   for(std::vector<expr_listt>::iterator it=parameters.begin();

src/solvers/flattening/boolbv_update.cpp

@@ -12,7 +12,6 @@ Author: Daniel Kroening, [email protected]
 #include <util/std_expr.h>
 #include <util/arith_tools.h>
 #include <util/base_type.h>
-#include <util/config.h>
 #include <util/pointer_offset_size.h>
 
 #include <util/c_types.h>

src/solvers/flattening/boolbv_width.cpp

@@ -11,7 +11,7 @@ Author: Daniel Kroening, [email protected]
 #include <algorithm>
 
 #include <util/arith_tools.h>
-#include <util/config.h>
+#include <util/invariant.h>
 #include <util/std_types.h>
 
 boolbv_widtht::boolbv_widtht(const namespacet &_ns):ns(_ns)
@@ -193,10 +193,10 @@ const boolbv_widtht::entryt &boolbv_widtht::get_entry(const typet &type) const
   {
     // no width
   }
-  else if(type_id==ID_pointer ||
-          type_id==ID_reference)
+  else if(type_id==ID_pointer)
   {
-    entry.total_width=config.ansi_c.pointer_width;
+    entry.total_width=to_pointer_type(type).get_width();
+    DATA_INVARIANT(entry.total_width!=0, "pointer must have width");
   }
   else if(type_id==ID_symbol)
     entry=get_entry(ns.follow(type));

src/solvers/flattening/bv_pointers.cpp

@@ -96,8 +96,9 @@ bv_pointerst::bv_pointerst(
   pointer_logic(_ns)
 {
   object_bits=config.bv_encoding.object_bits;
-  offset_bits=config.ansi_c.pointer_width-object_bits;
-  bits=config.ansi_c.pointer_width;
+  std::size_t pointer_width=boolbv_width(pointer_type(void_type()));
+  offset_bits=pointer_width-object_bits;
+  bits=pointer_width;
 }
 
 bool bv_pointerst::convert_address_of_rec(
@@ -220,7 +221,7 @@ bvt bv_pointerst::convert_pointer_type(const exprt &expr)
     throw "convert_pointer_type got non-pointer type";
 
   // make sure the config hasn't been changed
-  assert(bits==config.ansi_c.pointer_width);
+  assert(bits==boolbv_width(expr.type()));
 
   if(expr.id()==ID_symbol)
   {

src/util/pointer_offset_size.cpp

@@ -11,15 +11,13 @@ Author: Daniel Kroening, [email protected]
 
 #include "pointer_offset_size.h"
 
-#include <cassert>
-
 #include "c_types.h"
 #include "expr.h"
+#include "invariant.h"
 #include "arith_tools.h"
 #include "std_types.h"
 #include "std_expr.h"
 #include "expr_util.h"
-#include "config.h"
 #include "simplify_expr.h"
 #include "namespace.h"
 #include "symbol.h"
@@ -103,14 +101,15 @@ mp_integer member_offset_bits(
   return offset;
 }
 
+/// Compute the size of a type in bytes, rounding up to full bytes
 mp_integer pointer_offset_size(
   const typet &type,
   const namespacet &ns)
 {
   mp_integer bits=pointer_offset_bits(type, ns);
   if(bits==-1)
     return -1;
-  return bits/8+(((bits%8)==0)?0:1);
+  return bits+7/8;
 }
 
 mp_integer pointer_offset_bits(
@@ -234,7 +233,7 @@ mp_integer pointer_offset_bits(
     if(type.get_bool(ID_C_ptr32))
       return 32;
 
-    return config.ansi_c.pointer_width;
+    return to_bitvector_type(type).get_width();
   }
   else if(type.id()==ID_symbol)
   {
@@ -495,7 +494,7 @@ exprt size_of_expr(
     if(type.get_bool(ID_C_ptr32))
       return from_integer(4, size_type());
 
-    std::size_t width=config.ansi_c.pointer_width;
+    std::size_t width=to_bitvector_type(type).get_width();
     std::size_t bytes=width/8;
     if(bytes*8!=width)
       bytes++;
@@ -531,12 +530,13 @@ mp_integer compute_pointer_offset(
   }
   else if(expr.id()==ID_index)
   {
-    assert(expr.operands().size()==2);
+    const index_exprt &index_expr=to_index_expr(expr);
+    const typet &array_type=ns.follow(index_expr.array().type());
+    DATA_INVARIANT(
+      array_type.id()==ID_array,
+      "index into array expected, found "+array_type.id_string());
 
-    const typet &array_type=ns.follow(expr.op0().type());
-    assert(array_type.id()==ID_array);
-
-    mp_integer o=compute_pointer_offset(expr.op0(), ns);
+    mp_integer o=compute_pointer_offset(index_expr.array(), ns);
 
     if(o!=-1)
     {
@@ -545,29 +545,27 @@ mp_integer compute_pointer_offset(
 
       mp_integer i;
 
-      if(sub_size>0 && !to_integer(expr.op1(), i))
+      if(sub_size>0 && !to_integer(index_expr.index(), i))
         return o+i*sub_size;
     }
 
     // don't know
   }
   else if(expr.id()==ID_member)
   {
-    assert(expr.operands().size()==1);
-    const typet &type=ns.follow(expr.op0().type());
-
-    assert(type.id()==ID_struct ||
-           type.id()==ID_union);
+    const member_exprt &member_expr=to_member_expr(expr);
+    const exprt &op=member_expr.struct_op();
+    const struct_union_typet &type=to_struct_union_type(ns.follow(op.type()));
 
-    mp_integer o=compute_pointer_offset(expr.op0(), ns);
+    mp_integer o=compute_pointer_offset(op, ns);
 
     if(o!=-1)
     {
       if(type.id()==ID_union)
         return o;
 
       return o+member_offset(
-        to_struct_type(type), expr.get(ID_component_name), ns);
+        to_struct_type(type), member_expr.get_component_name(), ns);
     }
   }
   else if(expr.id()==ID_string_constant)
@@ -594,8 +592,10 @@ exprt build_sizeof_expr(
      (type_size==0 && val>0))
     return nil_exprt();
 
-  assert(address_bits(val+1)<=config.ansi_c.pointer_width);
   const typet t(size_type());
+  DATA_INVARIANT(
+    address_bits(val+1)<=pointer_offset_bits(t, ns),
+    "sizeof value does not fit size_type");
 
   mp_integer remainder=0;
   if(type_size!=0)

src/util/simplify_expr.cpp

@@ -204,7 +204,8 @@ bool simplify_exprt::simplify_typecast(exprt &expr)
      expr.op0().id()==ID_typecast &&
      expr.op0().operands().size()==1 &&
      (op_type.id()==ID_signedbv || op_type.id()==ID_unsignedbv) &&
-     to_bitvector_type(op_type).get_width()>=config.ansi_c.pointer_width)
+     to_bitvector_type(op_type).get_width()>=
+     to_bitvector_type(expr_type).get_width())
   {
     exprt tmp=expr.op0().op0();
     expr.op0().swap(tmp);