use optional for unknown pointer offset sizes

Author: Daniel Kroening

src/analyses/goto_rw.cpp

@@ -91,9 +91,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;
 
@@ -166,8 +169,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 ||
@@ -223,15 +227,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);
 }
@@ -252,15 +259,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;
@@ -295,10 +304,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);
@@ -335,17 +347,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)
     {
@@ -394,8 +409,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;
@@ -527,8 +543,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))
@@ -574,8 +593,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);
 }
 
@@ -604,16 +625,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

@@ -3634,9 +3634,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);
@@ -237,9 +237,9 @@ static void add_padding_msvc(struct_typet &type, const namespacet &ns)
       else
       {
         // keep track of offset
-        const mp_integer size = pointer_offset_size(it->type(), ns);
-        if(size >= 1)
-          offset += size;
+        const auto size = pointer_offset_size(it->type(), ns);
+        if(size.has_value() && *size >= 1)
+          offset += *size;
       }
     }
   }
@@ -383,10 +383,10 @@ static void add_padding_gcc(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?
@@ -443,9 +443,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-instrument/count_eloc.cpp

@@ -191,9 +191,9 @@ void print_global_state_size(const goto_modelt &goto_model)
       continue;
     }
 
-    const mp_integer bits = pointer_offset_bits(symbol.type, ns);
-    if(bits > 0)
-      total_size += bits;
+    const auto bits = pointer_offset_bits(symbol.type, ns);
+    if(bits.has_value() && bits.value() > 0)
+      total_size += bits.value();
   }
 
   std::cout << "Total size of global objects: " << total_size << " bits\n";