[depends: #1333] pointers now come with a width

regression/goto-analyzer/approx-const-fp-array-variable-invalid-cast-const-fp/test.desc

@@ -2,9 +2,9 @@ CORE
 main.c
 --show-goto-functions --verbosity 10 --pointer-check
 ^Removing function pointers and virtual functions$
-^\s*IF fp == \(const void_fp\)f2 THEN GOTO [0-9]$
-^\s*IF fp == \(const void_fp\)f3 THEN GOTO [0-9]$
-^\s*IF fp == \(const void_fp\)f4 THEN GOTO [0-9]$
+^\s*IF fp == \(.*\)f2 THEN GOTO [0-9]$
+^\s*IF fp == \(.*\)f3 THEN GOTO [0-9]$
+^\s*IF fp == \(.*\)f4 THEN GOTO [0-9]$
 ^SIGNAL=0$
 --
 ^warning: ignoring

src/ansi-c/ansi_c_convert_type.cpp

@@ -14,9 +14,9 @@ Author: Daniel Kroening, [email protected]
 #include <cassert>
 
 #include <util/c_types.h>
+#include <util/config.h>
 #include <util/namespace.h>
 #include <util/simplify_expr.h>
-#include <util/config.h>
 #include <util/arith_tools.h>
 #include <util/std_types.h>
 
@@ -221,9 +221,11 @@ void ansi_c_convert_typet::read_rec(const typet &type)
     // We turn ID_frontend_pointer to ID_pointer
     // Pointers have a width, much like integers,
     // which is added here.
-    typet tmp(type);
-    tmp.id(ID_pointer);
-    tmp.set(ID_width, config.ansi_c.pointer_width);
+    pointer_typet tmp(type.subtype(), config.ansi_c.pointer_width);
+    tmp.add_source_location()=type.source_location();
+    const irep_idt typedef_identifier=type.get(ID_C_typedef);
+    if(!typedef_identifier.empty())
+      tmp.set(ID_C_typedef, typedef_identifier);
     other.push_back(tmp);
   }
   else if(type.id()==ID_pointer)

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_convert_type.cpp

@@ -162,9 +162,12 @@ void cpp_convert_typet::read_rec(const typet &type)
   else if(type.id()==ID_frontend_pointer)
   {
     // add width and turn into ID_pointer
-    typet tmp=type;
-    tmp.id(ID_pointer);
-    tmp.set(ID_width, config.ansi_c.pointer_width);
+    pointer_typet tmp(type.subtype(), config.ansi_c.pointer_width);
+    tmp.add_source_location()=type.source_location();
+    if(type.get_bool(ID_C_reference))
+      tmp.set(ID_C_reference, true);
+    if(type.get_bool(ID_C_rvalue_reference))
+      tmp.set(ID_C_rvalue_reference, true);
     other.push_back(tmp);
   }
   else if(type.id()==ID_pointer)

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>
 
@@ -79,12 +78,10 @@ void cpp_typecheckt::typecheck_type(typet &type)
   }
   else if(type.id()==ID_pointer)
   {
-    // the pointer might have a qualifier, but do subtype first
+    // the pointer/reference 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/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/cvc/cvc_conv.cpp

@@ -13,9 +13,9 @@ Author: Daniel Kroening, [email protected]
 #include <string>
 
 #include <util/arith_tools.h>
+#include <util/c_types.h>
 #include <util/std_types.h>
 #include <util/std_expr.h>
-#include <util/config.h>
 #include <util/find_symbols.h>
 #include <util/pointer_offset_size.h>
 #include <util/string2int.h>
@@ -159,8 +159,9 @@ void cvc_convt::convert_constant_expr(const exprt &expr)
     {
       out << "(# object:="
           << pointer_logic.get_null_object()
-          << ", offset:="
-          << bin_zero(config.ansi_c.pointer_width) << " #)";
+          << ", offset:=";
+      convert_expr(from_integer(0, size_type()));
+      out << " #)";
     }
     else
       throw "unknown pointer constant: "+id2string(value);
@@ -176,7 +177,9 @@ void cvc_convt::convert_constant_expr(const exprt &expr)
   }
   else if(expr.type().id()==ID_array)
   {
-    out << "ARRAY (i: " << array_index_type() << "):";
+    out << "ARRAY (i: ";
+    convert_type(index_type());
+    out << "):";
 
     assert(!expr.operands().empty());
 
@@ -188,7 +191,9 @@ void cvc_convt::convert_constant_expr(const exprt &expr)
       else
         out << "\n  ELSIF ";
 
-      out << "i=" << array_index(i) << " THEN ";
+      out << "i=";
+      convert_expr(from_integer(i, index_type()));
+      out << " THEN ";
       convert_array_value(*it);
       i++;
     }
@@ -247,7 +252,7 @@ void cvc_convt::convert_plus_expr(const exprt &expr)
       out << "(LET P: " << cvc_pointer_type() << " = ";
       convert_expr(*p);
       out << " IN P WITH .offset:=BVPLUS("
-          << config.ansi_c.pointer_width
+          << pointer_offset_bits(pointer_type(void_type()), ns)
           << ", P.offset, ";
       convert_expr(*i);
       out << "))";
@@ -487,52 +492,24 @@ void cvc_convt::convert_literal(const literalt l)
     out << ")";
 }
 
-std::string cvc_convt::bin_zero(unsigned bits)
+std::string cvc_convt::cvc_pointer_type() const
 {
-  assert(bits!=0);
-  std::string result="0bin";
-  while(bits!=0)
-  {
-    result+='0';
-    bits--;
-  }
-  return result;
-}
-
-std::string cvc_convt::cvc_pointer_type()
-{
-  assert(config.ansi_c.pointer_width!=0);
-  return "[# object: INT, offset: BITVECTOR("+
-         std::to_string(config.ansi_c.pointer_width)+") #]";
-}
-
-std::string cvc_convt::array_index_type()
-{
-  return std::string("BITVECTOR(")+
-         std::to_string(32)+")";
-}
-
-typet cvc_convt::gen_array_index_type()
-{
-  typet t(ID_signedbv);
-  t.set(ID_width, 32);
-  return t;
-}
-
-std::string cvc_convt::array_index(unsigned i)
-{
-  return "0bin"+integer2binary(i, config.ansi_c.int_width);
+  return
+    "[# object: INT, offset: BITVECTOR("+
+    std::to_string(
+      integer2size_t(
+        pointer_offset_bits(pointer_type(void_type()), ns)))+") #]";
 }
 
 void cvc_convt::convert_array_index(const exprt &expr)
 {
-  if(expr.type()==gen_array_index_type())
+  if(expr.type()==index_type())
   {
     convert_expr(expr);
   }
   else
   {
-    exprt tmp(ID_typecast, gen_array_index_type());
+    exprt tmp(ID_typecast, index_type());
     tmp.copy_to_operands(expr);
     convert_expr(tmp);
   }
@@ -547,8 +524,9 @@ void cvc_convt::convert_address_of_rec(const exprt &expr)
     out
       << "(# object:="
       << pointer_logic.add_object(expr)
-      << ", offset:="
-      << bin_zero(config.ansi_c.pointer_width) << " #)";
+      << ", offset:=";
+    convert_expr(from_integer(0, size_type()));
+    out << " #)";
   }
   else if(expr.id()==ID_index)
   {
@@ -581,7 +559,7 @@ void cvc_convt::convert_address_of_rec(const exprt &expr)
         assert(false);
 
       out << " IN P WITH .offset:=BVPLUS("
-                   << config.ansi_c.pointer_width
+                   << pointer_offset_bits(pointer_type(void_type()), ns)
                    << ", P.offset, ";
       convert_expr(index);
       out << "))";
@@ -609,13 +587,10 @@ void cvc_convt::convert_address_of_rec(const exprt &expr)
       ns);
     assert(offset>=0);
 
-    typet index_type(ID_unsignedbv);
-    index_type.set(ID_width, config.ansi_c.pointer_width);
-
-    exprt index=from_integer(offset, index_type);
+    exprt index=from_integer(offset, size_type());
 
     out << " IN P WITH .offset:=BVPLUS("
-                 << config.ansi_c.pointer_width
+                 << pointer_offset_bits(pointer_type(void_type()), ns)
                  << ", P.offset, ";
     convert_expr(index);
     out << "))";
@@ -1035,7 +1010,9 @@ void cvc_convt::convert_expr(const exprt &expr)
   {
     assert(expr.type().id()==ID_array);
     assert(expr.operands().size()==1);
-    out << "(ARRAY (i: " << array_index_type() << "): ";
+    out << "(ARRAY (i: ";
+    convert_type(index_type());
+    out << "): ";
     convert_array_value(expr.op0());
     out << ")";
   }
@@ -1273,8 +1250,9 @@ void cvc_convt::convert_type(const typet &type)
   {
     const array_typet &array_type=to_array_type(type);
 
-    out << "ARRAY " << array_index_type()
-                 << " OF ";
+    out << "ARRAY ";
+    convert_type(index_type());
+    out << " OF ";
 
     if(array_type.subtype().id()==ID_bool)
       out << "BITVECTOR(1)";

src/solvers/cvc/cvc_conv.h

@@ -79,11 +79,7 @@ class cvc_convt:public prop_convt
   void convert_array_value(const exprt &expr);
   void convert_as_bv(const exprt &expr);
   void convert_array_index(const exprt &expr);
-  static typet gen_array_index_type();
-  static std::string bin_zero(unsigned bits);
-  static std::string array_index_type();
-  static std::string array_index(unsigned i);
-  static std::string cvc_pointer_type();
+  std::string cvc_pointer_type() const;
 };
 
 #endif // CPROVER_SOLVERS_CVC_CVC_CONV_H

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)
@@ -195,7 +195,8 @@ const boolbv_widtht::entryt &boolbv_widtht::get_entry(const typet &type) const
   }
   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);
+  PRECONDITION(bits==boolbv_width(expr.type()));
 
   if(expr.id()==ID_symbol)
   {