use optionalt<exprt> instead of nil_exprt in expr_initializer

This matches the signature of the external interface.

Author: Daniel Kroening

src/util/expr_initializer.cpp

@@ -26,23 +26,22 @@ class expr_initializert
   {
   }
 
-  exprt operator()(
-    const typet &type,
-    const source_locationt &source_location)
+  optionalt<exprt>
+  operator()(const typet &type, const source_locationt &source_location)
   {
     return expr_initializer_rec(type, source_location);
   }
 
 protected:
   const namespacet &ns;
 
-  exprt expr_initializer_rec(
+  optionalt<exprt> expr_initializer_rec(
     const typet &type,
     const source_locationt &source_location);
 };
 
 template <bool nondet>
-exprt expr_initializert<nondet>::expr_initializer_rec(
+optionalt<exprt> expr_initializert<nondet>::expr_initializer_rec(
   const typet &type,
   const source_locationt &source_location)
 {
@@ -103,12 +102,12 @@ exprt expr_initializert<nondet>::expr_initializer_rec(
       result = side_effect_expr_nondett(type, source_location);
     else
     {
-      exprt sub_zero =
+      auto sub_zero =
         expr_initializer_rec(to_complex_type(type).subtype(), source_location);
-      if(sub_zero.is_nil())
-        return nil_exprt();
+      if(!sub_zero.has_value())
+        return {};
 
-      result = complex_exprt(sub_zero, sub_zero, to_complex_type(type));
+      result = complex_exprt(*sub_zero, *sub_zero, to_complex_type(type));
     }
 
     result.add_source_location()=source_location;
@@ -130,17 +129,16 @@ exprt expr_initializert<nondet>::expr_initializer_rec(
     }
     else
     {
-      exprt tmpval =
-        expr_initializer_rec(array_type.subtype(), source_location);
-      if(tmpval.is_nil())
-        return nil_exprt();
+      auto tmpval = expr_initializer_rec(array_type.subtype(), source_location);
+      if(!tmpval.has_value())
+        return {};
 
       if(array_type.size().id()==ID_infinity)
       {
         if(nondet)
           return side_effect_expr_nondett(type, source_location);
 
-        array_of_exprt value(tmpval, array_type);
+        array_of_exprt value(*tmpval, array_type);
         value.add_source_location()=source_location;
         return std::move(value);
       }
@@ -151,14 +149,15 @@ exprt expr_initializert<nondet>::expr_initializer_rec(
         if(nondet)
           return side_effect_expr_nondett(type, source_location);
         else
-          return nil_exprt();
+          return {};
       }
 
       if(*array_size < 0)
-        return nil_exprt();
+        return {};
 
       array_exprt value({}, array_type);
-      value.operands().resize(numeric_cast_v<std::size_t>(*array_size), tmpval);
+      value.operands().resize(
+        numeric_cast_v<std::size_t>(*array_size), *tmpval);
       value.add_source_location()=source_location;
       return std::move(value);
     }
@@ -167,18 +166,18 @@ exprt expr_initializert<nondet>::expr_initializer_rec(
   {
     const vector_typet &vector_type=to_vector_type(type);
 
-    exprt tmpval = expr_initializer_rec(vector_type.subtype(), source_location);
-    if(tmpval.is_nil())
-      return nil_exprt();
+    auto tmpval = expr_initializer_rec(vector_type.subtype(), source_location);
+    if(!tmpval.has_value())
+      return {};
 
     const mp_integer vector_size =
       numeric_cast_v<mp_integer>(vector_type.size());
 
     if(vector_size < 0)
-      return nil_exprt();
+      return {};
 
     vector_exprt value({}, vector_type);
-    value.operands().resize(numeric_cast_v<std::size_t>(vector_size), tmpval);
+    value.operands().resize(numeric_cast_v<std::size_t>(vector_size), *tmpval);
     value.add_source_location()=source_location;
 
     return std::move(value);
@@ -202,11 +201,11 @@ exprt expr_initializert<nondet>::expr_initializer_rec(
       }
       else
       {
-        const exprt member = expr_initializer_rec(c.type(), source_location);
-        if(member.is_nil())
-          return nil_exprt();
+        const auto member = expr_initializer_rec(c.type(), source_location);
+        if(!member.has_value())
+          return {};
 
-        value.add_to_operands(std::move(member));
+        value.add_to_operands(std::move(*member));
       }
     }
 
@@ -241,62 +240,78 @@ exprt expr_initializert<nondet>::expr_initializer_rec(
       }
     }
 
-    union_exprt value("", nil_exprt(), type);
-    value.add_source_location()=source_location;
-
     if(!found)
     {
       // stupid empty union
+      union_exprt value("", nil_exprt(), type);
+      value.add_source_location() = source_location;
+      return std::move(value);
     }
     else
     {
-      value.set_component_name(component.get_name());
-      value.op()=
+      auto component_value =
         expr_initializer_rec(component.type(), source_location);
-      if(value.op().is_nil())
-        return nil_exprt();
-    }
 
-    return std::move(value);
+      if(!component_value.has_value())
+        return {};
+
+      union_exprt value(component.get_name(), *component_value, type);
+      value.add_source_location() = source_location;
+
+      return std::move(value);
+    }
   }
   else if(type_id == ID_symbol_type)
   {
-    exprt result = expr_initializer_rec(ns.follow(type), source_location);
+    auto result = expr_initializer_rec(ns.follow(type), source_location);
+
+    if(!result.has_value())
+      return {};
+
     // we might have mangled the type for arrays, so keep that
     if(type.id() != ID_array)
-      result.type()=type;
+      result->type() = type;
 
-    return result;
+    return *result;
   }
   else if(type_id==ID_c_enum_tag)
   {
-    exprt result = expr_initializer_rec(
+    auto result = expr_initializer_rec(
       ns.follow_tag(to_c_enum_tag_type(type)), source_location);
 
+    if(!result.has_value())
+      return {};
+
     // use the tag type
-    result.type() = type;
+    result->type() = type;
 
-    return result;
+    return *result;
   }
   else if(type_id==ID_struct_tag)
   {
-    exprt result = expr_initializer_rec(
+    auto result = expr_initializer_rec(
       ns.follow_tag(to_struct_tag_type(type)), source_location);
 
+    if(!result.has_value())
+      return {};
+
     // use the tag type
-    result.type() = type;
+    result->type() = type;
 
-    return result;
+    return *result;
   }
   else if(type_id==ID_union_tag)
   {
-    exprt result = expr_initializer_rec(
+    auto result = expr_initializer_rec(
       ns.follow_tag(to_union_tag_type(type)), source_location);
 
+    if(!result.has_value())
+      return {};
+
     // use the tag type
-    result.type() = type;
+    result->type() = type;
 
-    return result;
+    return *result;
   }
   else if(type_id==ID_string)
   {
@@ -310,7 +325,7 @@ exprt expr_initializert<nondet>::expr_initializer_rec(
     return result;
   }
   else
-    return nil_exprt();
+    return {};
 }
 
 /// Create the equivalent of zero for type `type`.
@@ -324,12 +339,7 @@ optionalt<exprt> zero_initializer(
   const source_locationt &source_location,
   const namespacet &ns)
 {
-  expr_initializert<false> z_i(ns);
-  const exprt result = z_i(type, source_location);
-  if(result.is_nil())
-    return {};
-  else
-    return result;
+  return expr_initializert<false>(ns)(type, source_location);
 }
 
 /// Create a non-deterministic value for type `type`, with all subtypes
@@ -344,10 +354,5 @@ optionalt<exprt> nondet_initializer(
   const source_locationt &source_location,
   const namespacet &ns)
 {
-  expr_initializert<true> z_i(ns);
-  const exprt result = z_i(type, source_location);
-  if(result.is_nil())
-    return {};
-  else
-    return result;
+  return expr_initializert<true>(ns)(type, source_location);
 }