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,9 @@ void rw_range_sett::get_objects_shift(
 {
   const exprt simp_distance=simplify_expr(shift.distance(), ns);
 
-  range_spect src_size=
-    to_range_spect(pointer_offset_bits(shift.op().type(), ns));
+  auto op_bits = pointer_offset_bits(shift.op().type(), ns);
+
+  range_spect src_size = op_bits.has_value() ? to_range_spect(*op_bits) : -1;
 
   mp_integer dist;
   if(range_start==-1 ||
@@ -224,15 +228,18 @@ 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);
 
-  if(offset!=-1)
-    offset+=range_start;
+  range_spect offset;
+
+  if(offset_bits.has_value())
+  {
+    offset = to_range_spect(*offset_bits);
+    offset += range_start;
+  }
+  else
+    offset = -1;
 
   get_objects_rec(mode, expr.struct_op(), offset, size);
 }
@@ -253,15 +260,17 @@ 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);
+
+    sub_size = subtype_bits.has_value() ? to_range_spect(*subtype_bits) : -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);
+
+    sub_size = subtype_bits.has_value() ? to_range_spect(*subtype_bits) : -1;
   }
   else
     return;
@@ -296,10 +305,13 @@ 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);
 
-  if(sub_size==-1)
+  range_spect sub_size;
+
+  if(subtype_bits.has_value())
+    sub_size = to_range_spect(*subtype_bits);
+  else
   {
     forall_operands(it, expr)
       get_objects_rec(mode, *it, 0, -1);
@@ -336,17 +348,20 @@ void rw_range_sett::get_objects_struct(
   const struct_typet &struct_type=
     to_struct_type(ns.follow(expr.type()));
 
-  range_spect full_size=
-    to_range_spect(pointer_offset_bits(struct_type, ns));
+  auto struct_bits = pointer_offset_bits(struct_type, ns);
+
+  range_spect full_size =
+    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)
   {
-    range_spect sub_size=
-      to_range_spect(pointer_offset_bits(it->type(), ns));
+    auto it_bits = pointer_offset_bits(it->type(), ns);
+
+    range_spect sub_size = it_bits.has_value() ? to_range_spect(*it_bits) : -1;
 
     if(offset==-1)
     {
@@ -395,8 +410,9 @@ void rw_range_sett::get_objects_typecast(
 {
   const exprt &op=tc.op();
 
-  range_spect new_size=
-    to_range_spect(pointer_offset_bits(op.type(), ns));
+  auto op_bits = pointer_offset_bits(op.type(), ns);
+
+  range_spect new_size = op_bits.has_value() ? to_range_spect(*op_bits) : -1;
 
   if(range_start==-1)
     new_size=-1;
@@ -528,8 +544,11 @@ void rw_range_sett::get_objects_rec(
   {
     const symbol_exprt &symbol=to_symbol_expr(expr);
     const irep_idt identifier=symbol.get_identifier();
-    range_spect full_size=
-      to_range_spect(pointer_offset_bits(symbol.type(), ns));
+
+    auto symbol_bits = pointer_offset_bits(symbol.type(), ns);
+
+    range_spect full_size =
+      symbol_bits.has_value() ? to_range_spect(*symbol_bits) : -1;
 
     if(full_size==0 ||
        (full_size>0 && range_start>=full_size))
@@ -575,8 +594,10 @@ void rw_range_sett::get_objects_rec(
 
 void rw_range_sett::get_objects_rec(get_modet mode, const exprt &expr)
 {
-  range_spect size=
-    to_range_spect(pointer_offset_bits(expr.type(), ns));
+  auto expr_bits = pointer_offset_bits(expr.type(), ns);
+
+  range_spect size = expr_bits.has_value() ? to_range_spect(*expr_bits) : -1;
+
   get_objects_rec(mode, expr, 0, size);
 }
 
@@ -605,16 +626,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,11 @@ 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())
+        gen(from, identifier, 0, to_range_spect(*param_bits));
+      else
+        gen(from, identifier, 0, -1);
     }
   }
   else

src/ansi-c/expr2c.cpp

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

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

@@ -86,9 +86,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

@@ -51,12 +51,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)
           {
@@ -92,13 +92,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 "

src/goto-programs/interpreter_evaluate.cpp

@@ -162,12 +162,12 @@ bool interpretert::byte_offset_to_memory_offset(
     {
       const mp_integer comp_offset = member_offset(st, comp.get_name(), ns);
 
-      const mp_integer component_byte_size =
+      auto component_byte_size =
         pointer_offset_size(comp.type(), ns);
-      if(component_byte_size<0)
+      if(!component_byte_size.has_value())
         return true;
 
-      if(comp_offset + component_byte_size > offset)
+      if(comp_offset + *component_byte_size > offset)
       {
         mp_integer subtype_result;
         bool ret=byte_offset_to_memory_offset(
@@ -189,25 +189,30 @@ bool interpretert::byte_offset_to_memory_offset(
   else if(source_type.id()==ID_array)
   {
     const auto &at=to_array_type(source_type);
+
     mp_vectort array_size_vec;
     evaluate(at.size(), array_size_vec);
+
     if(array_size_vec.size()!=1)
       return true;
+
     mp_integer array_size=array_size_vec[0];
-    mp_integer elem_size_bytes=pointer_offset_size(at.subtype(), ns);
-    if(elem_size_bytes<=0)
+    auto elem_size_bytes = pointer_offset_size(at.subtype(), ns);
+    if(!elem_size_bytes.has_value() || *elem_size_bytes == 0)
       return true;
+
     mp_integer elem_size_leaves;
     if(count_type_leaves(at.subtype(), elem_size_leaves))
       return true;
-    mp_integer this_idx=offset/elem_size_bytes;
+
+    mp_integer this_idx = offset / (*elem_size_bytes);
     if(this_idx>=array_size_vec[0])
       return true;
+
     mp_integer subtype_result;
-    bool ret=byte_offset_to_memory_offset(
-      at.subtype(),
-      offset%elem_size_bytes,
-      subtype_result);
+    bool ret = byte_offset_to_memory_offset(
+      at.subtype(), offset % (*elem_size_bytes), subtype_result);
+
     result=subtype_result+(elem_size_leaves*this_idx);
     return ret;
   }
@@ -259,26 +264,31 @@ bool interpretert::memory_offset_to_byte_offset(
   else if(source_type.id()==ID_array)
   {
     const auto &at=to_array_type(source_type);
+
     mp_vectort array_size_vec;
     evaluate(at.size(), array_size_vec);
     if(array_size_vec.size()!=1)
       return true;
-    mp_integer elem_size=pointer_offset_size(at.subtype(), ns);
-    if(elem_size==-1)
+
+    auto elem_size = pointer_offset_size(at.subtype(), ns);
+    if(!elem_size.has_value())
       return true;
+
     mp_integer elem_count;
     if(count_type_leaves(at.subtype(), elem_count))
       return true;
+
     mp_integer this_idx=full_cell_offset/elem_count;
     if(this_idx>=array_size_vec[0])
       return true;
+
     mp_integer subtype_result;
     bool ret=
       memory_offset_to_byte_offset(
         at.subtype(),
         full_cell_offset%elem_count,
         subtype_result);
-    result=subtype_result+(elem_size*this_idx);
+    result = subtype_result + ((*elem_size) * this_idx);
     return ret;
   }
   else