use optional for unknown pointer offset sizes

Author: Daniel Kroening

src/analyses/goto_rw.cpp

@@ -92,9 +92,12 @@ void rw_range_sett::get_objects_complex(
   const exprt &op=expr.op0();
   assert(op.type().id()==ID_complex);
 
-  range_spect sub_size=
-    to_range_spect(pointer_offset_bits(op.type().subtype(), ns));
-  assert(sub_size>0);
+  auto subtype_bits=pointer_offset_bits(op.type().subtype(), ns);
+  CHECK_RETURN(subtype_bits.has_value());
+
+  range_spect sub_size=to_range_spect(*subtype_bits);
+  CHECK_RETURN(sub_size>0);
+
   range_spect offset=
     (range_start==-1 || expr.id()==ID_complex_real) ? 0 : sub_size;
 
@@ -167,8 +170,10 @@ void rw_range_sett::get_objects_shift(
 {
   const exprt simp_distance=simplify_expr(shift.distance(), ns);
 
+  auto op_bits=pointer_offset_bits(shift.op().type(), ns);
+
   range_spect src_size=
-    to_range_spect(pointer_offset_bits(shift.op().type(), ns));
+    op_bits.has_value()?to_range_spect(*op_bits):-1;
 
   mp_integer dist;
   if(range_start==-1 ||
@@ -224,12 +229,17 @@ void rw_range_sett::get_objects_member(
 
   const struct_typet &struct_type=to_struct_type(type);
 
-  range_spect offset=
-    to_range_spect(
-      member_offset_bits(
-        struct_type,
-        expr.get_component_name(),
-        ns));
+  auto offset_bits=member_offset_bits(
+    struct_type,
+    expr.get_component_name(),
+    ns);
+
+  range_spect offset;
+
+  if(offset_bits.has_value())
+    offset=to_range_spect(*offset_bits);
+  else
+    offset=-1;
 
   if(offset!=-1)
     offset+=range_start;
@@ -253,15 +263,23 @@ void rw_range_sett::get_objects_index(
   {
     const vector_typet &vector_type=to_vector_type(type);
 
-    sub_size=
-      to_range_spect(pointer_offset_bits(vector_type.subtype(), ns));
+    auto subtype_bits=pointer_offset_bits(vector_type.subtype(), ns);
+
+    if(subtype_bits.has_value())
+      sub_size=to_range_spect(*subtype_bits);
+    else
+      sub_size=-1;
   }
   else if(type.id()==ID_array)
   {
     const array_typet &array_type=to_array_type(type);
 
-    sub_size=
-      to_range_spect(pointer_offset_bits(array_type.subtype(), ns));
+    auto subtype_bits=pointer_offset_bits(array_type.subtype(), ns);
+
+    if(subtype_bits.has_value())
+      sub_size=to_range_spect(*subtype_bits);
+    else
+      sub_size=-1;
   }
   else
     return;
@@ -296,8 +314,14 @@ void rw_range_sett::get_objects_array(
   const array_typet &array_type=
     to_array_type(ns.follow(expr.type()));
 
-  range_spect sub_size=
-    to_range_spect(pointer_offset_bits(array_type.subtype(), ns));
+  auto subtype_bits=pointer_offset_bits(array_type.subtype(), ns);
+
+  range_spect sub_size;
+
+  if(subtype_bits.has_value())
+    sub_size=to_range_spect(*subtype_bits);
+  else
+    sub_size=-1;
 
   if(sub_size==-1)
   {
@@ -336,17 +360,21 @@ void rw_range_sett::get_objects_struct(
   const struct_typet &struct_type=
     to_struct_type(ns.follow(expr.type()));
 
+  auto struct_bits=pointer_offset_bits(struct_type, ns);
+
   range_spect full_size=
-    to_range_spect(pointer_offset_bits(struct_type, ns));
+    struct_bits.has_value()?to_range_spect(*struct_bits):-1;
 
   range_spect offset=0;
   range_spect full_r_s=range_start==-1 ? 0 : range_start;
   range_spect full_r_e=size==-1 || full_size==-1 ? -1 : full_r_s+size;
 
   forall_operands(it, expr)
   {
+    auto it_bits=pointer_offset_bits(it->type(), ns);
+
     range_spect sub_size=
-      to_range_spect(pointer_offset_bits(it->type(), ns));
+      it_bits.has_value()?to_range_spect(*it_bits):-1;
 
     if(offset==-1)
     {
@@ -395,8 +423,10 @@ void rw_range_sett::get_objects_typecast(
 {
   const exprt &op=tc.op();
 
+  auto op_bits=pointer_offset_bits(op.type(), ns);
+
   range_spect new_size=
-    to_range_spect(pointer_offset_bits(op.type(), ns));
+    op_bits.has_value()?to_range_spect(*op_bits):-1;
 
   if(range_start==-1)
     new_size=-1;
@@ -528,8 +558,11 @@ void rw_range_sett::get_objects_rec(
   {
     const symbol_exprt &symbol=to_symbol_expr(expr);
     const irep_idt identifier=symbol.get_identifier();
+
+    auto symbol_bits=pointer_offset_bits(symbol.type(), ns);
+
     range_spect full_size=
-      to_range_spect(pointer_offset_bits(symbol.type(), ns));
+      symbol_bits.has_value()?to_range_spect(*symbol_bits):-1;
 
     if(full_size==0 ||
        (full_size>0 && range_start>=full_size))
@@ -575,8 +608,11 @@ void rw_range_sett::get_objects_rec(
 
 void rw_range_sett::get_objects_rec(get_modet mode, const exprt &expr)
 {
+  auto expr_bits=pointer_offset_bits(expr.type(), ns);
+
   range_spect size=
-    to_range_spect(pointer_offset_bits(expr.type(), ns));
+    expr_bits.has_value()?to_range_spect(*expr_bits):-1;
+
   get_objects_rec(mode, expr, 0, size);
 }
 
@@ -605,16 +641,24 @@ void rw_range_set_value_sett::get_objects_dereference(
   exprt object=deref;
   dereference(target, object, ns, value_sets);
 
-  range_spect new_size=
-    to_range_spect(pointer_offset_bits(object.type(), ns));
+  auto type_bits=pointer_offset_bits(object.type(), ns);
 
-  if(range_start==-1 || new_size<=range_start)
-    new_size=-1;
-  else
+  range_spect new_size;
+
+  if(type_bits.has_value())
   {
-    new_size-=range_start;
-    new_size=std::min(size, new_size);
+    new_size=to_range_spect(*type_bits);
+
+    if(range_start==-1 || new_size<=range_start)
+      new_size=-1;
+    else
+    {
+      new_size-=range_start;
+      new_size=std::min(size, new_size);
+    }
   }
+  else
+    new_size=-1;
 
   // value_set_dereferencet::build_reference_to will turn *p into
   // DYNAMIC_OBJECT(p) ? *p : invalid_objectN

src/analyses/reaching_definitions.cpp

@@ -210,9 +210,12 @@ void rd_range_domaint::transform_function_call(
       if(identifier.empty())
         continue;
 
-      range_spect size=
-        to_range_spect(pointer_offset_bits(param.type(), ns));
-      gen(from, identifier, 0, size);
+      auto param_bits=pointer_offset_bits(param.type(), ns);
+      if(param_bits.has_value())
+      {
+        range_spect size=to_range_spect(*param_bits);
+        gen(from, identifier, 0, size);
+      }
     }
   }
   else

src/ansi-c/expr2c.cpp

@@ -3623,7 +3623,7 @@ std::string expr2ct::convert_with_precedence(
     return convert_function(
       src,
       "__builtin_bswap"+
-      integer2string(pointer_offset_bits(src.op0().type(), ns)),
+      integer2string(*pointer_offset_bits(src.op0().type(), ns)),
       precedence=16);
 
   else if(src.id()==ID_isnormal)

src/ansi-c/padding.cpp

@@ -76,7 +76,7 @@ mp_integer alignment(const typet &type, const namespacet &ns)
           type.id()==ID_c_bool ||
           type.id()==ID_pointer)
   {
-    result=pointer_offset_size(type, ns);
+    result=*pointer_offset_size(type, ns);
   }
   else if(type.id()==ID_c_enum)
     result=alignment(type.subtype(), ns);
@@ -243,10 +243,10 @@ void add_padding(struct_typet &type, const namespacet &ns)
       }
     }
 
-    mp_integer size=pointer_offset_size(it_type, ns);
+    auto size=pointer_offset_size(it_type, ns);
 
-    if(size!=-1)
-      offset+=size;
+    if(size.has_value())
+      offset+=*size;
   }
 
   // any explicit alignment for the struct?
@@ -301,9 +301,9 @@ void add_padding(union_typet &type, const namespacet &ns)
   // check per component, and ignore those without fixed size
   for(const auto &c : type.components())
   {
-    mp_integer s=pointer_offset_bits(c.type(), ns);
-    if(s>0)
-      size_bits=std::max(size_bits, s);
+    auto s=pointer_offset_bits(c.type(), ns);
+    if(s.has_value())
+      size_bits=std::max(size_bits, *s);
   }
 
   // Is the union packed?

src/ansi-c/type2name.cpp

@@ -85,9 +85,9 @@ static std::string pointer_offset_bits_as_string(
   const typet &type,
   const namespacet &ns)
 {
-  mp_integer bits = pointer_offset_bits(type, ns);
-  CHECK_RETURN(bits != -1);
-  return integer2string(bits);
+  auto bits = pointer_offset_bits(type, ns);
+  CHECK_RETURN(bits.has_value());
+  return integer2string(*bits);
 }
 
 static bool parent_is_sym_check=false;

src/goto-instrument/alignment_checks.cpp

@@ -47,12 +47,12 @@ void print_struct_alignment_problems(
         {
           const typet &it_type = it_next->type();
           const namespacet ns(symbol_table);
-          mp_integer size = pointer_offset_size(it_type, ns);
+          auto size = pointer_offset_size(it_type, ns);
 
-          if(size < 0)
+          if(!size.has_value())
             throw "type of unknown size:\n" + it_type.pretty();
 
-          cumulated_length += size;
+          cumulated_length += *size;
           // [it_mem;it_next] cannot be covered by an instruction
           if(cumulated_length > config.ansi_c.memory_operand_size)
           {
@@ -88,13 +88,13 @@ void print_struct_alignment_problems(
       #if 0
       const namespacet ns(symbol_table);
       const array_typet array=to_array_type(symbol_pair.second.type);
-      const mp_integer size=
+      const auto size=
         pointer_offset_size(array.subtype(), ns);
 
-      if(size<0)
+      if(!size.has_value())
         throw "type of unknown size:\n"+it_type.pretty();
 
-      if(2*integer2long(size)<=config.ansi_c.memory_operand_size)
+      if(2*integer2long(*size)<=config.ansi_c.memory_operand_size)
       {
         out << "\nWARNING: "
             << "declaration of an array at "