Pointers get a width

regression/invariants/driver.cpp

@@ -11,9 +11,11 @@ Author: Chris Smowton, [email protected]
 
 #include <string>
 #include <sstream>
+
 #include <util/invariant.h>
 #include <util/invariant_utils.h>
 #include <util/std_types.h>
+#include <util/c_types.h>
 
 /// An example of structured invariants-- this contains fields to
 /// describe the error to a catcher, and also produces a human-readable
@@ -86,7 +88,7 @@ int main(int argc, char** argv)
   else if(arg=="data-invariant-string")
     DATA_INVARIANT(false, "Test invariant failure");
   else if(arg=="irep")
-    INVARIANT_WITH_IREP(false, "error with irep", pointer_typet(void_typet()));
+    INVARIANT_WITH_IREP(false, "error with irep", pointer_type(void_typet()));
   else
     return 1;
 }

src/ansi-c/ansi_c_convert_type.cpp

@@ -216,6 +216,13 @@ void ansi_c_convert_typet::read_rec(const typet &type)
   {
     c_storage_spec.alias=type.subtype().get(ID_value);
   }
+  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);
+    other.push_back(tmp);
+  }
   else
     other.push_back(type);
 }

src/ansi-c/c_typecheck_type.cpp

@@ -76,7 +76,10 @@ void c_typecheck_baset::typecheck_type(typet &type)
   else if(type.id()==ID_array)
     typecheck_array_type(to_array_type(type));
   else if(type.id()==ID_pointer)
+  {
     typecheck_type(type.subtype());
+    INVARIANT(!type.get(ID_width).empty(), "pointers must have width");
+  }
   else if(type.id()==ID_struct ||
           type.id()==ID_union)
     typecheck_compound_type(to_struct_union_type(type));

src/cpp/cpp_typecheck_constructor.cpp

@@ -223,8 +223,7 @@ void cpp_typecheckt::default_cpctor(
   cpp_declaratort parameter_tor;
   parameter_tor.add(ID_value).make_nil();
   parameter_tor.set(ID_name, cpp_parameter);
-  parameter_tor.type()=reference_typet();
-  parameter_tor.type().subtype().make_nil();
+  parameter_tor.type()=reference_type(nil_typet());
   parameter_tor.add_source_location()=source_location;
 
   // Parameter declaration
@@ -388,9 +387,8 @@ void cpp_typecheckt::default_assignop(
   declarator_name.get_sub().push_back(irept("="));
 
   declarator_type.id(ID_function_type);
-  declarator_type.subtype()=reference_typet();
+  declarator_type.subtype()=reference_type(nil_typet());
   declarator_type.subtype().add("#qualifier").make_nil();
-  declarator_type.subtype().subtype().make_nil();
 
   exprt &args=static_cast<exprt&>(declarator.type().add(ID_parameters));
   args.add_source_location()=source_location;

src/cpp/cpp_typecheck_conversions.cpp

@@ -1280,11 +1280,8 @@ bool cpp_typecheckt::reference_binding(
     if(reference_compatible(expr, type, rank))
     {
       {
-        address_of_exprt tmp;
+        address_of_exprt tmp(expr, reference_type(expr.type()));
         tmp.add_source_location()=expr.source_location();
-        tmp.object()=expr;
-        tmp.type()=pointer_type(tmp.op0().type());
-        tmp.type().set(ID_C_reference, true);
         new_expr.swap(tmp);
       }
 
@@ -1411,10 +1408,7 @@ bool cpp_typecheckt::reference_binding(
 
   if(user_defined_conversion_sequence(arg_expr, type.subtype(), new_expr, rank))
   {
-    address_of_exprt tmp;
-    tmp.type()=pointer_type(new_expr.type());
-    tmp.object()=new_expr;
-    tmp.type().set(ID_C_reference, true);
+    address_of_exprt tmp(new_expr, reference_type(new_expr.type()));
     tmp.add_source_location()=new_expr.source_location();
     new_expr.swap(tmp);
     return true;

src/cpp/cpp_typecheck_type.cpp

@@ -14,6 +14,7 @@ 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>
 
@@ -81,6 +82,9 @@ void cpp_typecheckt::typecheck_type(typet &type)
     // the pointer might have a qualifier, but do subtype first
     typecheck_type(type.subtype());
 
+    // we add a width, much like with integers
+    to_pointer_type(type).set_width(config.ansi_c.pointer_width);
+
     // Check if it is a pointer-to-member
     if(type.find("to-member").is_not_nil())
     {

src/cpp/parse.cpp

@@ -3015,7 +3015,7 @@ bool Parser::optPtrOperator(typet &ptrs)
 
     if(t=='*')
     {
-      pointer_typet op;
+      typet op(ID_pointer);
       cpp_tokent tk;
       lex.get_token(tk);
       set_location(op, tk);

src/goto-symex/symex_builtin_functions.cpp

@@ -165,20 +165,20 @@ void goto_symext::symex_malloc(
 
   new_symbol_table.add(value_symbol);
 
-  address_of_exprt rhs;
+  exprt rhs;
 
   if(object_type.id()==ID_array)
   {
-    rhs.type()=pointer_type(value_symbol.type.subtype());
     index_exprt index_expr(value_symbol.type.subtype());
     index_expr.array()=value_symbol.symbol_expr();
     index_expr.index()=from_integer(0, index_type());
-    rhs.op0()=index_expr;
+    rhs=address_of_exprt(
+      index_expr, pointer_type(value_symbol.type.subtype()));
   }
   else
   {
-    rhs.op0()=value_symbol.symbol_expr();
-    rhs.type()=pointer_type(value_symbol.type);
+    rhs=address_of_exprt(
+      value_symbol.symbol_expr(), pointer_type(value_symbol.type));
   }
 
   if(rhs.type()!=lhs.type())

src/goto-symex/symex_dead.cpp

@@ -45,12 +45,7 @@ void goto_symext::symex_dead(statet &state)
     exprt rhs;
 
     if(failed.is_not_nil())
-    {
-      address_of_exprt address_of_expr;
-      address_of_expr.object()=failed;
-      address_of_expr.type()=code.op0().type();
-      rhs=address_of_expr;
-    }
+      rhs=address_of_exprt(failed, to_pointer_type(code.op0().type()));
     else
       rhs=exprt(ID_invalid);
 

src/goto-symex/symex_decl.cpp

@@ -60,12 +60,7 @@ void goto_symext::symex_decl(statet &state, const symbol_exprt &expr)
     exprt rhs;
 
     if(failed.is_not_nil())
-    {
-      address_of_exprt address_of_expr;
-      address_of_expr.object()=failed;
-      address_of_expr.type()=expr.type();
-      rhs=address_of_expr;
-    }
+      rhs=address_of_exprt(failed, to_pointer_type(expr.type()));
     else
       rhs=exprt(ID_invalid);
 

src/java_bytecode/java_bytecode_instrument.cpp

@@ -103,8 +103,8 @@ codet java_bytecode_instrumentt::throw_exception(
       get_message_handler());
   }
 
-  pointer_typet exc_ptr_type;
-  exc_ptr_type.subtype()=symbol_typet(exc_class_name);
+  pointer_typet exc_ptr_type=
+    pointer_type(symbol_typet(exc_class_name));
 
   // Allocate and throw an instance of the exception class:
 

src/java_bytecode/java_string_library_preprocess.cpp

@@ -1304,8 +1304,7 @@ exprt java_string_library_preprocesst::get_object_at_index(
 {
   dereference_exprt deref_objs(argv, argv.type().subtype());
   pointer_typet empty_pointer=pointer_type(empty_typet());
-  pointer_typet pointer_of_pointer;
-  pointer_of_pointer.copy_to_subtypes(empty_pointer);
+  pointer_typet pointer_of_pointer=pointer_type(empty_pointer);
   member_exprt data_member(deref_objs, "data", pointer_of_pointer);
   plus_exprt data_pointer_plus_index(
     data_member, from_integer(index, java_int_type()), data_member.type());

src/java_bytecode/java_types.cpp

@@ -67,7 +67,7 @@ typet java_boolean_type()
 
 reference_typet java_reference_type(const typet &subtype)
 {
-  return to_reference_type(reference_type(subtype));
+  return reference_type(subtype);
 }
 
 reference_typet java_lang_object_type()
@@ -246,11 +246,10 @@ typet java_type_from_string(const std::string &src)
           class_name[i]='.';
 
       std::string identifier="java::"+class_name;
+      symbol_typet symbol_type(identifier);
+      symbol_type.set(ID_C_base_name, class_name);
 
-      reference_typet result;
-      result.subtype()=symbol_typet(identifier);
-      result.subtype().set(ID_C_base_name, class_name);
-      return result;
+      return java_reference_type(symbol_type);
     }
 
   default:

src/path-symex/path_symex.cpp

@@ -245,20 +245,20 @@ void path_symext::symex_malloc(
   value_symbol.type.set("#dynamic", true);
   value_symbol.mode=ID_C;
 
-  address_of_exprt rhs;
+  exprt rhs;
 
   if(object_type.id()==ID_array)
   {
-    rhs.type()=pointer_type(value_symbol.type.subtype());
     index_exprt index_expr(value_symbol.type.subtype());
     index_expr.array()=value_symbol.symbol_expr();
     index_expr.index()=from_integer(0, index_type());
-    rhs.op0()=index_expr;
+    rhs=address_of_exprt(
+      index_expr, pointer_type(value_symbol.type.subtype()));
   }
   else
   {
-    rhs.op0()=value_symbol.symbol_expr();
-    rhs.type()=pointer_type(value_symbol.type);
+    rhs=address_of_exprt(
+      value_symbol.symbol_expr(), pointer_type(value_symbol.type));
   }
 
   if(rhs.type()!=lhs.type())

src/pointer-analysis/value_set.cpp

@@ -1523,9 +1523,8 @@ void value_sett::apply_code(
 
       if(failed.is_not_nil())
       {
-        address_of_exprt address_of_expr;
-        address_of_expr.object()=failed;
-        address_of_expr.type()=lhs.type();
+        address_of_exprt address_of_expr(
+          failed, to_pointer_type(lhs.type()));
         assign(lhs, address_of_expr, ns, false, false);
       }
       else

src/util/c_types.cpp

@@ -296,12 +296,12 @@ signedbv_typet pointer_diff_type()
 
 pointer_typet pointer_type(const typet &subtype)
 {
-  return pointer_typet(subtype);
+  return pointer_typet(subtype, config.ansi_c.pointer_width);
 }
 
 reference_typet reference_type(const typet &subtype)
 {
-  return reference_typet(subtype);
+  return reference_typet(subtype, config.ansi_c.pointer_width);
 }
 
 typet void_type()

src/util/simplify_expr_pointer.cpp

@@ -78,7 +78,8 @@ bool simplify_exprt::simplify_address_of_arg(exprt &expr)
         if(!to_integer(expr.op1(), index) &&
            step_size!=-1)
         {
-          pointer_typet pointer_type;
+          pointer_typet pointer_type=
+            to_pointer_type(to_dereference_expr(expr.op0()).pointer().type());
           pointer_type.subtype()=expr.type();
           typecast_exprt typecast_expr(
             from_integer(step_size*index+address, index_type()), pointer_type);
@@ -114,7 +115,8 @@ bool simplify_exprt::simplify_address_of_arg(exprt &expr)
           mp_integer offset=member_offset(struct_type, member, ns);
           if(offset!=-1)
           {
-            pointer_typet pointer_type;
+            pointer_typet pointer_type=
+              to_pointer_type(to_dereference_expr(expr.op0()).pointer().type());
             pointer_type.subtype()=expr.type();
             typecast_exprt typecast_expr(
               from_integer(address+offset, index_type()), pointer_type);

src/util/std_expr.h

@@ -2599,11 +2599,6 @@ class address_of_exprt:public unary_exprt
   {
   }
 
-  address_of_exprt():
-    unary_exprt(ID_address_of, pointer_typet())
-  {
-  }
-
   exprt &object()
   {
     return op0();

src/util/std_types.h

@@ -1367,16 +1367,6 @@ inline c_bit_field_typet &to_c_bit_field_type(typet &type)
 class pointer_typet:public bitvector_typet
 {
 public:
-  pointer_typet():bitvector_typet(ID_pointer)
-  {
-  }
-
-  // this one will go away; use the one with width
-  explicit pointer_typet(const typet &_subtype):
-    bitvector_typet(ID_pointer, _subtype)
-  {
-  }
-
   pointer_typet(const typet &_subtype, std::size_t width):
     bitvector_typet(ID_pointer, _subtype, width)
   {
@@ -1418,18 +1408,6 @@ inline pointer_typet &to_pointer_type(typet &type)
 class reference_typet:public pointer_typet
 {
 public:
-  reference_typet()
-  {
-    set(ID_C_reference, true);
-  }
-
-  // this one will go away; use the one with width
-  explicit reference_typet(const typet &_subtype):
-    pointer_typet(_subtype)
-  {
-    set(ID_C_reference, true);
-  }
-
   reference_typet(const typet &_subtype, std::size_t _width):
     pointer_typet(_subtype, _width)
   {

unit/analyses/does_remove_const/does_expr_lose_const.cpp

@@ -10,15 +10,17 @@
 /// Does Remove Const Unit Tests
 
 #include <catch.hpp>
-#include <analyses/does_remove_const.h>
+
 #include <util/std_expr.h>
 #include <util/std_code.h>
 #include <util/std_types.h>
+#include <util/c_types.h>
+
 #include <ansi-c/c_qualifiers.h>
 #include <goto-programs/goto_program.h>
+#include <analyses/does_remove_const.h>
 #include <analyses/does_remove_const/does_remove_const_util.h>
 
-
 SCENARIO("does_expr_lose_const",
   "[core][analyses][does_remove_const][does_expr_remove_const]")
 {
@@ -43,23 +45,23 @@ SCENARIO("does_expr_lose_const",
     // pointer (can be reassigned)
     //   to int (value can be changed)
     // int *
-    typet pointer_to_int_type=pointer_typet(non_const_primitive_type);
+    typet pointer_to_int_type=pointer_type(non_const_primitive_type);
 
     // const pointer (can't be reassigned)
     //   to int (value can be changed)
     // int * const
-    typet const_pointer_to_int_type=pointer_typet(non_const_primitive_type);
+    typet const_pointer_to_int_type=pointer_type(non_const_primitive_type);
     const_qualifier.write(const_pointer_to_int_type);
 
     // pointer (can be reassigned)
     //   to const int (value can't be changed)
     // const int *
-    typet pointer_to_const_int_type=pointer_typet(const_primitive_type);
+    typet pointer_to_const_int_type=pointer_type(const_primitive_type);
 
     // constant pointer (can't be reassigned)
     //   to const int (value can't be changed)
     // const int * const
-    typet const_pointer_to_const_int_type=pointer_typet(const_primitive_type);
+    typet const_pointer_to_const_int_type=pointer_type(const_primitive_type);
     const_qualifier.write(const_pointer_to_const_int_type);
 
     symbol_exprt const_primitive_symbol(