Error handling cleanup in expr_initializer.cpp (and implied changes)

Author: danpoe

src/ansi-c/ansi_c_entry_point.cpp

@@ -177,8 +177,7 @@ bool ansi_c_entry_point(
     return false; // give up
   }
 
-  if(static_lifetime_init(symbol_table, symbol.location, message_handler))
-    return true;
+  static_lifetime_init(symbol_table, symbol.location, message_handler);
 
   return generate_ansi_c_start_function(symbol, symbol_table, message_handler);
 }

src/ansi-c/c_typecheck_initializer.cpp

@@ -114,12 +114,8 @@ exprt c_typecheck_baset::do_initializer_rec(
       {
         // fill up
         tmp.type()=type;
-        exprt zero=
-          zero_initializer(
-            full_type.subtype(),
-            value.source_location(),
-            *this,
-            get_message_handler());
+        exprt zero =
+          zero_initializer(full_type.subtype(), value.source_location(), *this);
         tmp.operands().resize(integer2size_t(array_size), zero);
       }
     }
@@ -171,12 +167,8 @@ exprt c_typecheck_baset::do_initializer_rec(
       {
         // fill up
         tmp2.type()=type;
-        exprt zero=
-          zero_initializer(
-            full_type.subtype(),
-            value.source_location(),
-            *this,
-            get_message_handler());
+        exprt zero =
+          zero_initializer(full_type.subtype(), value.source_location(), *this);
         tmp2.operands().resize(integer2size_t(array_size), zero);
       }
     }
@@ -399,12 +391,8 @@ exprt::operandst::const_iterator c_typecheck_baset::do_designated_initializer(
             to_array_type(full_type).size().is_nil()))
         {
           // we are willing to grow an incomplete or zero-sized array
-          exprt zero=
-            zero_initializer(
-              full_type.subtype(),
-              value.source_location(),
-              *this,
-              get_message_handler());
+          exprt zero = zero_initializer(
+            full_type.subtype(), value.source_location(), *this);
           dest->operands().resize(integer2size_t(index)+1, zero);
 
           // todo: adjust type!
@@ -466,12 +454,8 @@ exprt::operandst::const_iterator c_typecheck_baset::do_designated_initializer(
         // Note that gcc issues a warning if the union component is switched.
         // Build a union expression from given component.
         union_exprt union_expr(type);
-        union_expr.op()=
-          zero_initializer(
-            component.type(),
-            value.source_location(),
-            *this,
-            get_message_handler());
+        union_expr.op() =
+          zero_initializer(component.type(), value.source_location(), *this);
         union_expr.add_source_location()=value.source_location();
         union_expr.set_component_name(component.get_name());
         *dest=union_expr;
@@ -529,12 +513,8 @@ exprt::operandst::const_iterator c_typecheck_baset::do_designated_initializer(
           union_type.components().front();
 
         union_exprt union_expr(type);
-        union_expr.op()=
-          zero_initializer(
-            component.type(),
-            value.source_location(),
-            *this,
-            get_message_handler());
+        union_expr.op() =
+          zero_initializer(component.type(), value.source_location(), *this);
         union_expr.add_source_location()=value.source_location();
         union_expr.set_component_name(component.get_name());
         *dest=union_expr;
@@ -836,9 +816,7 @@ exprt c_typecheck_baset::do_initializer_list(
      full_type.id()==ID_vector)
   {
     // start with zero everywhere
-    result=
-      zero_initializer(
-        type, value.source_location(), *this, get_message_handler());
+    result = zero_initializer(type, value.source_location(), *this);
   }
   else if(full_type.id()==ID_array)
   {
@@ -851,9 +829,7 @@ exprt c_typecheck_baset::do_initializer_list(
     else
     {
       // start with zero everywhere
-      result=
-        zero_initializer(
-          type, value.source_location(), *this, get_message_handler());
+      result = zero_initializer(type, value.source_location(), *this);
     }
 
     // 6.7.9, 14: An array of character type may be initialized by a character

src/cpp/cpp_typecheck_expr.cpp

@@ -892,12 +892,8 @@ void cpp_typecheckt::typecheck_expr_explicit_typecast(exprt &expr)
   {
     // Default value, e.g., int()
     typecheck_type(expr.type());
-    exprt new_expr=
-      ::zero_initializer(
-        expr.type(),
-        expr.find_source_location(),
-        *this,
-        get_message_handler());
+    exprt new_expr =
+      ::zero_initializer(expr.type(), expr.find_source_location(), *this);
 
     new_expr.add_source_location()=expr.source_location();
     expr=new_expr;

src/cpp/cpp_typecheck_initializer.cpp

@@ -313,9 +313,7 @@ void cpp_typecheckt::zero_initializer(
   }
   else
   {
-    exprt value=
-      ::zero_initializer(
-        final_type, source_location, *this, get_message_handler());
+    exprt value = ::zero_initializer(final_type, source_location, *this);
 
     code_assignt assign;
     assign.lhs()=object;

src/goto-cc/linker_script_merge.cpp

@@ -525,7 +525,7 @@ int linker_script_merget::ls_data2instructions(
     // Push the array initialization to the front now, so that it happens before
     // the initialization of the symbols that point to it.
     namespacet ns(symbol_table);
-    exprt zi=zero_initializer(array_type, array_loc, ns, *message_handler);
+    exprt zi = zero_initializer(array_type, array_loc, ns);
     code_assignt array_assign(array_expr, zi);
     array_assign.add_source_location()=array_loc;
     goto_programt::instructiont array_assign_i;

src/goto-programs/builtin_functions.cpp

@@ -1202,12 +1202,8 @@ void goto_convertt::do_function_call_symbol(
     {
       goto_programt::targett t=dest.add_instruction(ASSIGN);
       t->source_location=function.source_location();
-      exprt zero=
-        zero_initializer(
-          dest_expr.type(),
-          function.source_location(),
-          ns,
-          get_message_handler());
+      exprt zero =
+        zero_initializer(dest_expr.type(), function.source_location(), ns);
       t->code=code_assignt(dest_expr, zero);
     }
   }

src/goto-symex/symex_builtin_functions.cpp

@@ -167,13 +167,8 @@ void goto_symext::symex_allocate(
 
   if(!zero_init.is_zero() && !zero_init.is_false())
   {
-    null_message_handlert null_message;
-    exprt zero_value=
-      zero_initializer(
-        object_type,
-        code.source_location(),
-        ns,
-        null_message);
+    exprt zero_value =
+      zero_initializer(object_type, code.source_location(), ns);
 
     if(zero_value.is_not_nil())
     {

src/linking/static_lifetime_init.cpp

@@ -117,16 +117,10 @@ bool static_lifetime_init(
 
     if(symbol.value.is_nil())
     {
-      try
-      {
-        namespacet ns(symbol_table);
-        rhs=zero_initializer(symbol.type, symbol.location, ns, message_handler);
-        assert(rhs.is_not_nil());
-      }
-      catch(...)
-      {
-        return true;
-      }
+      namespacet ns(symbol_table);
+      rhs = zero_initializer(symbol.type, symbol.location, ns);
+      INVARIANT(
+        rhs.is_not_nil(), "result of zero-initialization must be non-nil");
     }
     else
       rhs=symbol.value;

src/util/expr_initializer.cpp

@@ -23,14 +23,10 @@ Author: Daniel Kroening, [email protected]
 #include "std_expr.h"
 
 template <bool nondet>
-class expr_initializert : public messaget
+class expr_initializert
 {
 public:
-  expr_initializert(
-    const namespacet &_ns,
-    message_handlert &_message_handler):
-    messaget(_message_handler),
-    ns(_ns)
+  expr_initializert(const namespacet &_ns) : ns(_ns)
   {
   }
 
@@ -56,6 +52,10 @@ exprt expr_initializert<nondet>::expr_initializer_rec(
 {
   const irep_idt &type_id=type.id();
 
+  PRECONDITION(
+    type_id != ID_code,
+    source_location.as_string() + ": cannot initialize code type");
+
   if(type_id==ID_unsignedbv ||
      type_id==ID_signedbv ||
      type_id==ID_pointer ||
@@ -119,12 +119,6 @@ exprt expr_initializert<nondet>::expr_initializer_rec(
     result.add_source_location()=source_location;
     return result;
   }
-  else if(type_id==ID_code)
-  {
-    error().source_location=source_location;
-    error() << "cannot initialize code-type" << eom;
-    throw 0;
-  }
   else if(type_id==ID_array)
   {
     const array_typet &array_type=to_array_type(type);
@@ -160,10 +154,15 @@ exprt expr_initializert<nondet>::expr_initializer_rec(
         if(nondet)
           return side_effect_expr_nondett(type, source_location);
 
-        error().source_location=source_location;
-        error() << "failed to zero-initialize array of non-fixed size `"
-                << format(array_type.size()) << "'" << eom;
-        throw 0;
+        std::ostringstream oss;
+        oss << format(array_type.size());
+
+        INVARIANT(
+          false,
+          "non-infinite array size expression must be convertible to an "
+          "integer",
+          source_location.as_string() +
+            ": failed to zero-initialize array of size `" + oss.str() + "'");
       }
 
       DATA_INVARIANT(
@@ -188,10 +187,14 @@ exprt expr_initializert<nondet>::expr_initializer_rec(
       if(nondet)
         return side_effect_expr_nondett(type, source_location);
 
-      error().source_location=source_location;
-      error() << "failed to zero-initialize vector of non-fixed size `"
-              << format(vector_type.size()) << "'" << eom;
-      throw 0;
+      std::ostringstream oss;
+      oss << format(vector_type.size());
+
+      INVARIANT(
+        false,
+        "vector size must be convertible to an integer",
+        source_location.as_string() +
+          ": failed to zero-initialize vector of size `" + oss.str() + "'");
     }
 
     DATA_INVARIANT(
@@ -323,66 +326,29 @@ exprt expr_initializert<nondet>::expr_initializer_rec(
   }
   else
   {
-    error().source_location=source_location;
-    error() << "failed to initialize `" << format(type) << "'" << eom;
-    throw 0;
-  }
-}
-
-exprt zero_initializer(
-  const typet &type,
-  const source_locationt &source_location,
-  const namespacet &ns,
-  message_handlert &message_handler)
-{
-  expr_initializert<false> z_i(ns, message_handler);
-  return z_i(type, source_location);
-}
+    std::ostringstream oss;
+    oss << format(type);
 
-exprt nondet_initializer(
-  const typet &type,
-  const source_locationt &source_location,
-  const namespacet &ns,
-  message_handlert &message_handler)
-{
-  expr_initializert<true> z_i(ns, message_handler);
-  return z_i(type, source_location);
+    PRECONDITION(
+      false,
+      source_location.as_string() + ": cannot initialize " + oss.str() + "'");
+  }
 }
 
 exprt zero_initializer(
   const typet &type,
   const source_locationt &source_location,
   const namespacet &ns)
 {
-  std::ostringstream oss;
-  stream_message_handlert mh(oss);
-
-  try
-  {
-    expr_initializert<false> z_i(ns, mh);
-    return z_i(type, source_location);
-  }
-  catch(int)
-  {
-    throw oss.str();
-  }
+  expr_initializert<false> z_i(ns);
+  return z_i(type, source_location);
 }
 
 exprt nondet_initializer(
   const typet &type,
   const source_locationt &source_location,
   const namespacet &ns)
 {
-  std::ostringstream oss;
-  stream_message_handlert mh(oss);
-
-  try
-  {
-    expr_initializert<true> z_i(ns, mh);
-    return z_i(type, source_location);
-  }
-  catch(int)
-  {
-    throw oss.str();
-  }
+  expr_initializert<true> z_i(ns);
+  return z_i(type, source_location);
 }