pointer_offset_size functions now use optional

This reminds the user of these functionst that they might return an error.

Author: Daniel Kroening

jbmc/src/java_bytecode/remove_java_new.cpp

@@ -86,12 +86,12 @@ goto_programt::targett remove_java_newt::lower_java_new(
   typet object_type = rhs.type().subtype();
 
   // build size expression
-  exprt object_size = size_of_expr(object_type, ns);
-  CHECK_RETURN(object_size.is_not_nil());
+  const auto object_size = size_of_expr(object_type, ns);
+  CHECK_RETURN(object_size.has_value());
 
   // we produce a malloc side-effect, which stays
   side_effect_exprt malloc_expr(ID_allocate, rhs.type(), location);
-  malloc_expr.copy_to_operands(object_size);
+  malloc_expr.copy_to_operands(*object_size);
   // could use true and get rid of the code below
   malloc_expr.copy_to_operands(false_exprt());
   *target =
@@ -138,12 +138,12 @@ goto_programt::targett remove_java_newt::lower_java_new_array(
   PRECONDITION(ns.follow(object_type).id() == ID_struct);
 
   // build size expression
-  exprt object_size = size_of_expr(object_type, ns);
-  CHECK_RETURN(!object_size.is_nil());
+  const auto object_size = size_of_expr(object_type, ns);
+  CHECK_RETURN(object_size.has_value());
 
   // we produce a malloc side-effect, which stays
   side_effect_exprt malloc_expr(ID_allocate, rhs.type(), location);
-  malloc_expr.copy_to_operands(object_size);
+  malloc_expr.copy_to_operands(*object_size);
   // code use true and get rid of the code below
   malloc_expr.copy_to_operands(false_exprt());
 

src/analyses/goto_check.cpp

@@ -1056,8 +1056,10 @@ void goto_checkt::pointer_validity_check(
 
   const exprt &pointer=expr.pointer();
 
-  auto conditions =
-    address_check(pointer, size_of_expr(expr.type(), ns));
+  auto size_of_expr_opt = size_of_expr(expr.type(), ns);
+  CHECK_RETURN(size_of_expr_opt.has_value());
+
+  auto conditions = address_check(pointer, size_of_expr_opt.value());
 
   for(const auto &c : conditions)
   {
@@ -1329,12 +1331,11 @@ void goto_checkt::bounds_check(
       expr,
       guard);
 
-    exprt type_size=size_of_expr(ode.root_object().type(), ns);
-    if(type_size.is_not_nil())
-      type_matches_size=
-        equal_exprt(
-          size,
-          typecast_exprt(type_size, size.type()));
+    auto type_size_opt = size_of_expr(ode.root_object().type(), ns);
+
+    if(type_size_opt.has_value())
+      type_matches_size =
+        equal_exprt(size, typecast_exprt(type_size_opt.value(), size.type()));
   }
 
   const exprt &size=array_type.id()==ID_array ?
@@ -1360,12 +1361,14 @@ void goto_checkt::bounds_check(
     // that member, it behaves as if that member were replaced with the longest
     // array (with the same element type) that would not make the structure
     // larger than the object being accessed; [...]
-    const exprt type_size = size_of_expr(ode.root_object().type(), ns);
+    const auto type_size_opt = size_of_expr(ode.root_object().type(), ns);
+    CHECK_RETURN(type_size_opt.has_value());
 
     binary_relation_exprt inequality(
-      typecast_exprt::conditional_cast(ode.offset(), type_size.type()),
+      typecast_exprt::conditional_cast(
+        ode.offset(), type_size_opt.value().type()),
       ID_lt,
-      type_size);
+      type_size_opt.value());
 
     add_guarded_claim(
       implies_exprt(type_matches_size, inequality),
@@ -1542,10 +1545,9 @@ void goto_checkt::check_rec(const exprt &expr, guardt &guard, bool address)
 
     // we rewrite s->member into *(s+member_offset)
     // to avoid requiring memory safety of the entire struct
+    auto member_offset_opt = member_offset_expr(member, ns);
 
-    exprt member_offset=member_offset_expr(member, ns);
-
-    if(member_offset.is_not_nil())
+    if(member_offset_opt.has_value())
     {
       pointer_typet new_pointer_type = to_pointer_type(deref.pointer().type());
       new_pointer_type.subtype() = expr.type();
@@ -1557,7 +1559,8 @@ void goto_checkt::check_rec(const exprt &expr, guardt &guard, bool address)
       const exprt new_address = typecast_exprt(
         plus_exprt(
           char_pointer,
-          typecast_exprt::conditional_cast(member_offset, pointer_diff_type())),
+          typecast_exprt::conditional_cast(
+            member_offset_opt.value(), pointer_diff_type())),
         char_pointer.type());
 
       const exprt new_address_casted =

src/ansi-c/c_typecheck_expr.cpp

@@ -609,21 +609,20 @@ void c_typecheck_baset::typecheck_expr_builtin_offsetof(exprt &expr)
 
           if(type.id()==ID_struct)
           {
-            exprt o=
-              member_offset_expr(
-                to_struct_type(type), component_name, *this);
+            auto o_opt =
+              member_offset_expr(to_struct_type(type), component_name, *this);
 
-            if(o.is_nil())
+            if(!o_opt.has_value())
             {
               error().source_location = expr.source_location();
               error() << "offsetof failed to determine offset of `"
                       << component_name << "'" << eom;
               throw 0;
             }
 
-            o = typecast_exprt::conditional_cast(o, size_type());
-
-            result=plus_exprt(result, o);
+            result = plus_exprt(
+              result,
+              typecast_exprt::conditional_cast(o_opt.value(), size_type()));
           }
 
           type=struct_union_type.get_component(component_name).type();
@@ -643,20 +642,21 @@ void c_typecheck_baset::typecheck_expr_builtin_offsetof(exprt &expr)
               {
                 if(type.id()==ID_struct)
                 {
-                  exprt o = member_offset_expr(
+                  auto o_opt = member_offset_expr(
                     to_struct_type(type), c.get_name(), *this);
 
-                  if(o.is_nil())
+                  if(!o_opt.has_value())
                   {
                     error().source_location = expr.source_location();
                     error() << "offsetof failed to determine offset of `"
                             << component_name << "'" << eom;
                     throw 0;
                   }
 
-                  o = typecast_exprt::conditional_cast(o, size_type());
-
-                  result=plus_exprt(result, o);
+                  result = plus_exprt(
+                    result,
+                    typecast_exprt::conditional_cast(
+                      o_opt.value(), size_type()));
                 }
 
                 typet tmp = follow(c.type());
@@ -695,11 +695,18 @@ void c_typecheck_baset::typecheck_expr_builtin_offsetof(exprt &expr)
       // still need to typecheck index
       typecheck_expr(index);
 
-      exprt sub_size=size_of_expr(type.subtype(), *this);
+      auto sub_size_opt = size_of_expr(type.subtype(), *this);
+
+      if(!sub_size_opt.has_value())
+      {
+        error().source_location = expr.source_location();
+        error() << "offsetof failed to determine array element size" << eom;
+        throw 0;
+      }
 
       index = typecast_exprt::conditional_cast(index, size_type());
 
-      result=plus_exprt(result, mult_exprt(sub_size, index));
+      result = plus_exprt(result, mult_exprt(sub_size_opt.value(), index));
 
       typet tmp=type.subtype();
       type=tmp;
@@ -966,18 +973,20 @@ void c_typecheck_baset::typecheck_expr_sizeof(exprt &expr)
   {
     // This is a gcc extension.
     // https://gcc.gnu.org/onlinedocs/gcc-4.8.0/gcc/Pointer-Arith.html
-    new_expr = size_of_expr(char_type(), *this);
+    new_expr = from_integer(1, size_type());
   }
   else
   {
-    new_expr = size_of_expr(type, *this);
+    auto size_of_opt = size_of_expr(type, *this);
 
-    if(new_expr.is_nil())
+    if(!size_of_opt.has_value())
     {
       error().source_location = expr.source_location();
       error() << "type has no size: " << to_string(type) << eom;
       throw 0;
     }
+
+    new_expr = size_of_opt.value();
   }
 
   new_expr.swap(expr);

src/ansi-c/c_typecheck_type.cpp

@@ -693,11 +693,19 @@ void c_typecheck_baset::typecheck_vector_type(typet &type)
   }
 
   // the subtype must have constant size
-  exprt sub_size_expr = size_of_expr(subtype, *this);
+  auto sub_size_expr_opt = size_of_expr(subtype, *this);
 
-  simplify(sub_size_expr, *this);
+  if(!sub_size_expr_opt.has_value())
+  {
+    error().source_location = source_location;
+    error() << "failed to determine size of vector base type `"
+            << to_string(subtype) << "'" << eom;
+    throw 0;
+  }
+
+  simplify(sub_size_expr_opt.value(), *this);
 
-  const auto sub_size = numeric_cast<mp_integer>(sub_size_expr);
+  const auto sub_size = numeric_cast<mp_integer>(sub_size_expr_opt.value());
 
   if(!sub_size.has_value())
   {

src/ansi-c/expr2c.cpp

@@ -1863,12 +1863,13 @@ std::string expr2ct::convert_constant(
       if(src.find(ID_C_c_sizeof_type).is_not_nil() &&
          sizeof_nesting==0)
       {
-        const exprt sizeof_expr = build_sizeof_expr(to_constant_expr(src), ns);
+        const auto sizeof_expr_opt =
+          build_sizeof_expr(to_constant_expr(src), ns);
 
-        if(sizeof_expr.is_not_nil())
+        if(sizeof_expr_opt.has_value())
         {
           ++sizeof_nesting;
-          dest=convert(sizeof_expr)+" /*"+dest+"*/ ";
+          dest = convert(sizeof_expr_opt.value()) + " /*" + dest + "*/ ";
           --sizeof_nesting;
         }
       }

src/cpp/cpp_typecheck_expr.cpp

@@ -823,10 +823,14 @@ void cpp_typecheckt::typecheck_expr_new(exprt &expr)
 
   // we add the size of the object for convenience of the
   // runtime library
+  auto size_of_opt = size_of_expr(expr.type().subtype(), *this);
 
-  exprt &sizeof_expr=static_cast<exprt &>(expr.add(ID_sizeof));
-  sizeof_expr=size_of_expr(expr.type().subtype(), *this);
-  sizeof_expr.add(ID_C_c_sizeof_type)=expr.type().subtype();
+  if(size_of_opt.has_value())
+  {
+    auto &sizeof_expr = static_cast<exprt &>(expr.add(ID_sizeof));
+    sizeof_expr = size_of_opt.value();
+    sizeof_expr.add(ID_C_c_sizeof_type) = expr.type().subtype();
+  }
 }
 
 static exprt collect_comma_expression(const exprt &src)

src/cpp/cpp_typecheck_initializer.cpp

@@ -266,9 +266,10 @@ void cpp_typecheckt::zero_initializer(
       if(component.type().id()==ID_code)
         continue;
 
-      exprt component_size=size_of_expr(component.type(), *this);
+      auto component_size_opt = size_of_expr(component.type(), *this);
 
-      const auto size_int = numeric_cast<mp_integer>(component_size);
+      const auto size_int =
+        numeric_cast<mp_integer>(component_size_opt.value_or(nil_exprt()));
       if(size_int.has_value())
       {
         if(*size_int > max_comp_size)

src/goto-programs/mm_io.cpp

@@ -65,10 +65,12 @@ void mm_io(
 
           const typet &pt=ct.parameters()[0].type();
           const typet &st=ct.parameters()[1].type();
-          exprt size=size_of_expr(d.type(), ns);
+          auto size_opt = size_of_expr(d.type(), ns);
+          CHECK_RETURN(size_opt.has_value());
           const code_function_callt fc(
             mm_io_r,
-            {typecast_exprt(d.pointer(), pt), typecast_exprt(size, st)});
+            {typecast_exprt(d.pointer(), pt),
+             typecast_exprt(size_opt.value(), st)});
           goto_function.body.insert_before_swap(it);
           *it = goto_programt::make_function_call(fc, source_location);
           it++;
@@ -85,11 +87,12 @@ void mm_io(
           const typet &pt=ct.parameters()[0].type();
           const typet &st=ct.parameters()[1].type();
           const typet &vt=ct.parameters()[2].type();
-          exprt size=size_of_expr(d.type(), ns);
+          auto size_opt = size_of_expr(d.type(), ns);
+          CHECK_RETURN(size_opt.has_value());
           const code_function_callt fc(
             mm_io_w,
             {typecast_exprt(d.pointer(), pt),
-             typecast_exprt(size, st),
+             typecast_exprt(size_opt.value(), st),
              typecast_exprt(a.rhs(), vt)});
           goto_function.body.insert_before_swap(it);
           *it = goto_programt::make_function_call(fc, source_location);

src/goto-symex/symex_clean_expr.cpp

@@ -79,15 +79,15 @@ process_array_expr(exprt &expr, bool do_simplify, const namespacet &ns)
     {
       if(expr.type().id() != ID_array)
       {
-        exprt array_size = size_of_expr(expr.type(), ns);
+        auto array_size = size_of_expr(expr.type(), ns);
+        CHECK_RETURN(array_size.has_value());
         if(do_simplify)
-          simplify(array_size, ns);
-        expr =
-          byte_extract_exprt(
-            byte_extract_id(),
-            expr,
-            from_integer(0, index_type()),
-            array_typet(char_type(), array_size));
+          simplify(array_size.value(), ns);
+        expr = byte_extract_exprt(
+          byte_extract_id(),
+          expr,
+          from_integer(0, index_type()),
+          array_typet(char_type(), array_size.value()));
       }
 
       // given an array type T[N], i.e., an array of N elements of type T, and a
@@ -99,8 +99,10 @@ process_array_expr(exprt &expr, bool do_simplify, const namespacet &ns)
 
       exprt new_offset =
         typecast_exprt::conditional_cast(ode.offset(), array_size_type);
+      auto subtype_size_opt = size_of_expr(subtype, ns);
+      CHECK_RETURN(subtype_size_opt.has_value());
       exprt subtype_size = typecast_exprt::conditional_cast(
-        size_of_expr(subtype, ns), array_size_type);
+        subtype_size_opt.value(), array_size_type);
       new_offset = div_exprt(new_offset, subtype_size);
       minus_exprt new_size(prev_array_type.size(), new_offset);
       if(do_simplify)

src/goto-symex/symex_other.cpp

@@ -205,14 +205,14 @@ void goto_symext::symex_other(
     // byte array
     if(array_expr.type().id() != ID_array)
     {
-      exprt array_size = size_of_expr(array_expr.type(), ns);
-      do_simplify(array_size);
-      array_expr =
-        byte_extract_exprt(
-          byte_extract_id(),
-          array_expr,
-          from_integer(0, index_type()),
-          array_typet(char_type(), array_size));
+      auto array_size = size_of_expr(array_expr.type(), ns);
+      CHECK_RETURN(array_size.has_value());
+      do_simplify(array_size.value());
+      array_expr = byte_extract_exprt(
+        byte_extract_id(),
+        array_expr,
+        from_integer(0, index_type()),
+        array_typet(char_type(), array_size.value()));
     }
 
     const array_typet &array_type = to_array_type(array_expr.type());

src/pointer-analysis/value_set_dereference.cpp

@@ -440,15 +440,15 @@ value_set_dereferencet::valuet value_set_dereferencet::build_reference_to(
     else
     {
       // try to build a member/index expression - do not use byte_extract
-      exprt subexpr = get_subexpression_at_offset(
+      auto subexpr = get_subexpression_at_offset(
         root_object_subexpression, o.offset(), dereference_type, ns);
-      if(subexpr.is_not_nil())
-        simplify(subexpr, ns);
-      if(subexpr.is_not_nil() && subexpr.id() != byte_extract_id())
+      if(subexpr.has_value())
+        simplify(subexpr.value(), ns);
+      if(subexpr.has_value() && subexpr.value().id() != byte_extract_id())
       {
         // Successfully found a member, array index, or combination thereof
         // that matches the desired type and offset:
-        result.value = subexpr;
+        result.value = subexpr.value();
         return result;
       }