The sub-size of void* is undefined; use char* as specified in the standard

This patch includes a review of all uses of functions from pointer_offset_size.h
as all of those may return nil or a negative number if the size could not be
determined. Calling sites need to handle those cases as appropriate in a given
context.

Author: tautschnig

regression/cbmc/void_pointer1/main.c

@@ -0,0 +1,12 @@
+char buffer[2];
+int length = 2;
+
+void func(void* buf, int len)
+{
+  while( len-- )
+    *(char *)buf++;
+}
+
+void main(){
+  func(buffer,length);
+}

regression/cbmc/void_pointer1/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--pointer-check
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/cbmc/void_pointer2/main.c

@@ -0,0 +1,12 @@
+char buffer[2];
+int length = 2;
+
+void func(void* buf, int len)
+{
+  while( len-- )
+    *(char *)buf++;
+}
+
+void main(){
+  func(buffer,length);
+}

regression/cbmc/void_pointer2/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--pointer-check --no-simplify --unwind 3
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

src/analyses/goto_rw.cpp

@@ -149,6 +149,7 @@ void rw_range_sett::get_objects_complex(
 
   range_spect sub_size=
     to_range_spect(pointer_offset_bits(op.type().subtype(), ns));
+  assert(sub_size>0);
   range_spect offset=
     (range_start==-1 || expr.id()==ID_complex_real) ? 0 : sub_size;
 

src/ansi-c/c_typecheck_expr.cpp

@@ -1318,8 +1318,8 @@ void c_typecheck_baset::typecheck_expr_typecast(exprt &expr)
     // an integer/float of the same size
     if((expr_type.id()==ID_signedbv ||
         expr_type.id()==ID_unsignedbv) &&
-       pointer_offset_size(expr_type, *this)==
-       pointer_offset_size(op_vector_type, *this))
+       pointer_offset_bits(expr_type, *this)==
+       pointer_offset_bits(op_vector_type, *this))
     {
     }
     else

src/ansi-c/padding.cpp

@@ -339,6 +339,9 @@ void add_padding(union_typet &type, const namespacet &ns)
   mp_integer max_alignment=alignment(type, ns)*8;
   mp_integer size_bits=pointer_offset_bits(type, ns);
 
+  if(size_bits<0)
+    throw "type of unknown size:\n"+type.pretty();
+
   union_typet::componentst &components=type.components();
 
   // Is the union packed?

src/goto-instrument/alignment_checks.cpp

@@ -60,6 +60,9 @@ void print_struct_alignment_problems(
           const namespacet ns(symbol_table);
           mp_integer size=pointer_offset_size(it_type, ns);
 
+          if(size<0)
+            throw "type of unknown size:\n"+it_type.pretty();
+
           cumulated_length+=size;
           // [it_mem;it_next] cannot be covered by an instruction
           if(cumulated_length>config.ansi_c.memory_operand_size)
@@ -99,6 +102,9 @@ void print_struct_alignment_problems(
       const mp_integer size=
         pointer_offset_size(array.subtype(), ns);
 
+      if(size<0)
+        throw "type of unknown size:\n"+it_type.pretty();
+
       if(2*integer2long(size)<=config.ansi_c.memory_operand_size)
       {
         out << "\nWARNING: "

src/pointer-analysis/value_set.cpp

@@ -717,10 +717,23 @@ void value_sett::get_value_set_rec(
 
       if(i_is_set)
       {
-        i*=pointer_offset_size(ptr_operand.type().subtype(), ns);
+        typet pointer_sub_type=ptr_operand.type().subtype();
+        if(pointer_sub_type.id()==ID_empty)
+          pointer_sub_type=char_type();
 
-        if(expr.id()==ID_minus)
-          i.negate();
+        mp_integer size=pointer_offset_size(pointer_sub_type, ns);
+
+        if(size<=0)
+        {
+          i_is_set=false;
+        }
+        else
+        {
+          i*=size;
+
+          if(expr.id()==ID_minus)
+            i.negate();
+        }
       }
 
       get_value_set_rec(
@@ -1155,7 +1168,14 @@ void value_sett::get_reference_set_rec(
         }
         else if(!to_integer(offset, i) &&
                 o.offset_is_zero())
-          o.offset=i*pointer_offset_size(array_type.subtype(), ns);
+        {
+          mp_integer size=pointer_offset_size(array_type.subtype(), ns);
+
+          if(size<=0)
+            o.offset_is_set=false;
+          else
+            o.offset=i*size;
+        }
         else
           o.offset_is_set=false;
 

src/pointer-analysis/value_set_dereference.cpp

@@ -566,6 +566,10 @@ value_set_dereferencet::valuet value_set_dereferencet::build_reference_to(
         // no need to adjust offset
         adjusted_offset=offset;
       }
+      else if(element_size<=0)
+      {
+        throw "unknown or invalid type size of:\n"+dereference_type.pretty();
+      }
       else
       {
         exprt element_size_expr=
@@ -965,7 +969,12 @@ bool value_set_dereferencet::memory_model_bytes(
     // upper bound
     {
       mp_integer from_width=pointer_offset_size(from_type, ns);
+      if(from_width<=0)
+        throw "unknown or invalid type size:\n"+from_type.pretty();
+
       mp_integer to_width=pointer_offset_size(to_type, ns);
+      if(to_width<=0)
+        throw "unknown or invalid type size:\n"+to_type.pretty();
 
       exprt bound=from_integer(from_width-to_width, offset.type());
 

src/solvers/cvc/cvc_conv.cpp

@@ -835,6 +835,7 @@ void cvc_convt::convert_address_of_rec(const exprt &expr)
       to_struct_type(struct_op.type()),
       component_name,
       ns);
+    assert(offset>=0);
 
     typet index_type(ID_unsignedbv);
     index_type.set(ID_width, config.ansi_c.pointer_width);

src/solvers/dplib/dplib_conv.cpp

@@ -218,6 +218,7 @@ void dplib_convt::convert_address_of_rec(const exprt &expr)
 
     mp_integer offset=member_offset(ns,
       to_struct_type(struct_op.type()), component_name);
+    assert(offset>=0);
 
     typet index_type(ID_unsignedbv);
     index_type.set(ID_width, config.ansi_c.pointer_width);

src/solvers/flattening/bv_pointers.cpp

@@ -6,6 +6,7 @@ Author: Daniel Kroening, [email protected]
 
 \*******************************************************************/
 
+#include <util/c_types.h>
 #include <util/config.h>
 #include <util/arith_tools.h>
 #include <util/prefix.h>
@@ -185,6 +186,7 @@ bool bv_pointerst::convert_address_of_rec(
     // get size
     mp_integer size=
       pointer_offset_size(array_type.subtype(), ns);
+    assert(size>0);
 
     offset_arithmetic(bv, size, index);
     assert(bv.size()==bits);
@@ -205,6 +207,7 @@ bool bv_pointerst::convert_address_of_rec(
       mp_integer offset=member_offset(
         to_struct_type(struct_op_type),
         member_expr.get_component_name(), ns);
+      assert(offset>=0);
 
       // add offset
       offset_arithmetic(bv, offset);
@@ -375,7 +378,12 @@ bvt bv_pointerst::convert_pointer_type(const exprt &expr)
         count++;
         bv=convert_bv(*it);
         assert(bv.size()==bits);
-        size=pointer_offset_size(it->type().subtype(), ns);
+
+        typet pointer_sub_type=it->type().subtype();
+        if(pointer_sub_type.id()==ID_empty)
+          pointer_sub_type=char_type();
+        size=pointer_offset_size(pointer_sub_type, ns);
+        assert(size>0);
       }
     }
 
@@ -449,6 +457,7 @@ bvt bv_pointerst::convert_pointer_type(const exprt &expr)
 
     mp_integer element_size=
       pointer_offset_size(expr.op0().type().subtype(), ns);
+    assert(element_size>0);
 
     offset_arithmetic(bv, element_size, neg_op1);
 
@@ -517,6 +526,7 @@ bvt bv_pointerst::convert_bitvector(const exprt &expr)
 
     mp_integer element_size=
       pointer_offset_size(expr.op0().type().subtype(), ns);
+    assert(element_size>0);
 
     if(element_size!=1)
     {

src/solvers/flattening/flatten_byte_operators.cpp

@@ -197,6 +197,8 @@ exprt flatten_byte_update(
 
   mp_integer element_size=
     pointer_offset_size(src.op2().type(), ns);
+  if(element_size<0)
+    throw "byte_update of unknown width:\n"+src.pretty();
 
   const typet &t=ns.follow(src.op0().type());
 
@@ -378,9 +380,9 @@ exprt flatten_byte_update(
           t.id()==ID_pointer)
   {
     // do a shift, mask and OR
-    std::size_t width=integer2size_t(pointer_offset_size(t, ns)*8);
-
-    assert(width!=0);
+    mp_integer type_width=pointer_offset_bits(t, ns);
+    assert(type_width>0);
+    std::size_t width=integer2size_t(type_width);
 
     if(element_size*8>width)
       throw "flatten_byte_update to update element that is too large";

src/solvers/flattening/pointer_logic.cpp

@@ -200,7 +200,7 @@ exprt pointer_logict::object_rec(
     mp_integer size=
       pointer_offset_size(src.type().subtype(), ns);
 
-    if(size==0)
+    if(size<=0)
       return src;
 
     mp_integer index=offset/size;
@@ -234,6 +234,7 @@ exprt pointer_logict::object_rec(
       const typet &subtype=it->type();
 
       mp_integer sub_size=pointer_offset_size(subtype, ns);
+      assert(sub_size>0);
       mp_integer new_offset=current_offset+sub_size;
 
       if(new_offset>offset)

src/solvers/smt1/smt1_conv.cpp

@@ -432,6 +432,7 @@ void smt1_convt::convert_address_of_rec(
         member_expr.get_component_name();
 
       mp_integer offset=member_offset(struct_type, component_name, ns);
+      assert(offset>=0);
 
       typet index_type(ID_unsignedbv);
       index_type.set(ID_width, boolbv_width(result_type));
@@ -2333,6 +2334,7 @@ void smt1_convt::convert_plus(const plus_exprt &expr)
 
       mp_integer element_size=
         pointer_offset_size(expr.type().subtype(), ns);
+      assert(element_size>0);
 
       // adjust width if needed
       if(boolbv_width(i.type())!=boolbv_width(expr.type()))

src/solvers/smt2/smt2_conv.cpp

@@ -694,6 +694,7 @@ void smt2_convt::convert_address_of_rec(
         member_expr.get_component_name();
 
       mp_integer offset=member_offset(struct_type, component_name, ns);
+      assert(offset>=0);
 
       unsignedbv_typet index_type;
       index_type.set_width(boolbv_width(result_type));
@@ -3253,6 +3254,7 @@ void smt2_convt::convert_plus(const plus_exprt &expr)
 
       mp_integer element_size=
         pointer_offset_size(expr.type().subtype(), ns);
+      assert(element_size>0);
 
       out << "(bvadd ";
       convert_expr(p);
@@ -3469,6 +3471,7 @@ void smt2_convt::convert_minus(const minus_exprt &expr)
       // Pointer difference.
       mp_integer element_size=
         pointer_offset_size(expr.op0().type().subtype(), ns);
+      assert(element_size>0);
 
       if(element_size>=2)
         out << "(bvsdiv ";

src/util/pointer_offset_size.cpp

@@ -130,6 +130,8 @@ mp_integer pointer_offset_bits(
   if(type.id()==ID_array)
   {
     mp_integer sub=pointer_offset_bits(type.subtype(), ns);
+    if(sub<0)
+      return -1;
 
     // get size
     const exprt &size=to_array_type(type).size();
@@ -145,6 +147,8 @@ mp_integer pointer_offset_bits(
   else if(type.id()==ID_vector)
   {
     mp_integer sub=pointer_offset_bits(type.subtype(), ns);
+    if(sub<0)
+      return -1;
 
     // get size
     const exprt &size=to_vector_type(type).size();
@@ -160,6 +164,9 @@ mp_integer pointer_offset_bits(
   else if(type.id()==ID_complex)
   {
     mp_integer sub=pointer_offset_bits(type.subtype(), ns);
+    if(sub<0)
+      return -1;
+
     return sub*2;
   }
   else if(type.id()==ID_struct)
@@ -201,6 +208,8 @@ mp_integer pointer_offset_bits(
     {
       const typet &subtype=it->type();
       mp_integer sub_size=pointer_offset_bits(subtype, ns);
+      if(sub_size==-1)
+        return -1;
       if(sub_size>result)
         result=sub_size;
     }
@@ -467,6 +476,11 @@ exprt size_of_expr(
       else
         sub_size=pointer_offset_size(subtype, ns);
 
+      if(sub_size==-1)
+      {
+        result=-1;
+        break;
+      }
       if(sub_size>result)
         result=sub_size;
     }
@@ -566,7 +580,7 @@ mp_integer compute_pointer_offset(
 
       mp_integer i;
 
-      if(sub_size!=0 && !to_integer(expr.op1(), i))
+      if(sub_size>0 && !to_integer(expr.op1(), i))
         return o+i*sub_size;
     }
 

src/util/simplify_expr_pointer.cpp

@@ -383,12 +383,14 @@ bool simplify_exprt::simplify_pointer_offset(exprt &expr)
     if(ptr_expr.size()!=1 || int_expr.empty())
       return true;
 
-    typet pointer_type=ptr_expr.front().type();
+    typet pointer_sub_type=ptr_expr.front().type().subtype();
+    if(pointer_sub_type.id()==ID_empty)
+      pointer_sub_type=char_type();
 
     mp_integer element_size=
-      pointer_offset_size(pointer_type.subtype(), ns);
+      pointer_offset_size(pointer_sub_type, ns);
 
-    if(element_size==0)
+    if(element_size<0)
       return true;
 
     // this might change the type of the pointer!