Merge pull request #970 from diffblue/pointers-with-width

Daniel Kroening · web-flow · commit 8425bf4bb53e · 2017-09-07T08:49:23.000+01:00
Pointers get a width
diff --git a/regression/invariants/driver.cpp b/regression/invariants/driver.cpp
@@ -11,9 +11,11 @@ Author: Chris Smowton, chris.smowton@diffblue.com
 
 #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;
 }
diff --git a/src/ansi-c/ansi_c_convert_type.cpp b/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);
 }
diff --git a/src/ansi-c/c_typecheck_type.cpp b/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));
diff --git a/src/cpp/cpp_typecheck_constructor.cpp b/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;
diff --git a/src/cpp/cpp_typecheck_conversions.cpp b/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;
diff --git a/src/cpp/cpp_typecheck_type.cpp b/src/cpp/cpp_typecheck_type.cpp
@@ -14,6 +14,7 @@ Author: Daniel Kroening, kroening@cs.cmu.edu
 #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())
     {
diff --git a/src/cpp/parse.cpp b/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);
diff --git a/src/goto-symex/symex_builtin_functions.cpp b/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())
diff --git a/src/goto-symex/symex_dead.cpp b/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);
 
diff --git a/src/goto-symex/symex_decl.cpp b/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);
 
diff --git a/src/java_bytecode/java_bytecode_instrument.cpp b/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:
 
diff --git a/src/java_bytecode/java_string_library_preprocess.cpp b/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());
diff --git a/src/java_bytecode/java_types.cpp b/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:
diff --git a/src/path-symex/path_symex.cpp b/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())
diff --git a/src/pointer-analysis/value_set.cpp b/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
diff --git a/src/util/c_types.cpp b/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()
diff --git a/src/util/simplify_expr_pointer.cpp b/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);
diff --git a/src/util/std_expr.h b/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();
diff --git a/src/util/std_types.h b/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)
   {
diff --git a/unit/analyses/does_remove_const/does_expr_lose_const.cpp b/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(
diff --git a/unit/analyses/does_remove_const/does_type_preserve_const_correctness.cpp b/unit/analyses/does_remove_const/does_type_preserve_const_correctness.cpp
diff --git a/unit/analyses/does_remove_const/is_type_at_least_as_const_as.cpp b/unit/analyses/does_remove_const/is_type_at_least_as_const_as.cpp

Original file line number	Diff line number	Diff line change
`@@ -216,6 +216,13 @@ void ansi_c_convert_typet::read_rec(const typet &type)`
`216`	`216`	`{`
`217`	`217`	`c_storage_spec.alias=type.subtype().get(ID_value);`
`218`	`218`	`}`
	`219`	`+ else if(type.id()==ID_pointer)`
	`220`	`+ {`
	`221`	`+ // pointers have a width, much like integers`
	`222`	`+ pointer_typet tmp=to_pointer_type(type);`
	`223`	`+ tmp.set_width(config.ansi_c.pointer_width);`
	`224`	`+ other.push_back(tmp);`
	`225`	`+ }`
`219`	`226`	`else`
`220`	`227`	`other.push_back(type);`
`221`	`228`	`}`
Original file line number	Diff line number	Diff line change
`@@ -1280,11 +1280,8 @@ bool cpp_typecheckt::reference_binding(`
`1280`	`1280`	`if(reference_compatible(expr, type, rank))`
`1281`	`1281`	`{`
`1282`	`1282`	`{`
`1283`		`- address_of_exprt tmp;`
	`1283`	`+ address_of_exprt tmp(expr, reference_type(expr.type()));`
`1284`	`1284`	`tmp.add_source_location()=expr.source_location();`
`1285`		`- tmp.object()=expr;`
`1286`		`- tmp.type()=pointer_type(tmp.op0().type());`
`1287`		`- tmp.type().set(ID_C_reference, true);`
`1288`	`1285`	`new_expr.swap(tmp);`
`1289`	`1286`	`}`
`1290`	`1287`
`@@ -1411,10 +1408,7 @@ bool cpp_typecheckt::reference_binding(`
`1411`	`1408`
`1412`	`1409`	`if(user_defined_conversion_sequence(arg_expr, type.subtype(), new_expr, rank))`
`1413`	`1410`	`{`
`1414`		`- address_of_exprt tmp;`
`1415`		`- tmp.type()=pointer_type(new_expr.type());`
`1416`		`- tmp.object()=new_expr;`
`1417`		`- tmp.type().set(ID_C_reference, true);`
	`1411`	`+ address_of_exprt tmp(new_expr, reference_type(new_expr.type()));`
`1418`	`1412`	`tmp.add_source_location()=new_expr.source_location();`
`1419`	`1413`	`new_expr.swap(tmp);`
`1420`	`1414`	`return true;`
Original file line number	Diff line number	Diff line change
`@@ -3015,7 +3015,7 @@ bool Parser::optPtrOperator(typet &ptrs)`
`3015`	`3015`
`3016`	`3016`	`if(t=='*')`
`3017`	`3017`	`{`
`3018`		`- pointer_typet op;`
	`3018`	`+ typet op(ID_pointer);`
`3019`	`3019`	`cpp_tokent tk;`
`3020`	`3020`	`lex.get_token(tk);`
`3021`	`3021`	`set_location(op, tk);`
Original file line number	Diff line number	Diff line change
`@@ -165,20 +165,20 @@ void goto_symext::symex_malloc(`
`165`	`165`
`166`	`166`	`new_symbol_table.add(value_symbol);`
`167`	`167`
`168`		`- address_of_exprt rhs;`
	`168`	`+ exprt rhs;`
`169`	`169`
`170`	`170`	`if(object_type.id()==ID_array)`
`171`	`171`	`{`
`172`		`- rhs.type()=pointer_type(value_symbol.type.subtype());`
`173`	`172`	`index_exprt index_expr(value_symbol.type.subtype());`
`174`	`173`	`index_expr.array()=value_symbol.symbol_expr();`
`175`	`174`	`index_expr.index()=from_integer(0, index_type());`
`176`		`- rhs.op0()=index_expr;`
	`175`	`+ rhs=address_of_exprt(`
	`176`	`+ index_expr, pointer_type(value_symbol.type.subtype()));`
`177`	`177`	`}`
`178`	`178`	`else`
`179`	`179`	`{`
`180`		`- rhs.op0()=value_symbol.symbol_expr();`
`181`		`- rhs.type()=pointer_type(value_symbol.type);`
	`180`	`+ rhs=address_of_exprt(`
	`181`	`+ value_symbol.symbol_expr(), pointer_type(value_symbol.type));`
`182`	`182`	`}`
`183`	`183`
`184`	`184`	`if(rhs.type()!=lhs.type())`