Re-enable users of {expr,nondet}_initializer to do their own error reporting

With d5535a9 {expr,nondet}_initializer would
fail an invariant when an expression of the chosen type could not be generated.
As user input code can reasonably trigger this case (see included regression
test), the caller should be able to do error handling as appropriate in a given
context.

Author: tautschnig

jbmc/src/java_bytecode/java_bytecode_convert_class.cpp

@@ -708,12 +708,14 @@ void java_bytecode_convert_classt::convert(
       new_symbol.type.set(ID_C_access, ID_default);
 
     const namespacet ns(symbol_table);
-    new_symbol.value=
-      zero_initializer(
-        field_type,
-        class_symbol.location,
-        ns,
-        get_message_handler());
+    const auto value = zero_initializer(field_type, class_symbol.location, ns);
+    if(!value.has_value())
+    {
+      error().source_location = class_symbol.location;
+      error() << "failed to zero-initialize " << f.name << eom;
+      throw 0;
+    }
+    new_symbol.value = *value;
 
     // Load annotations
     if(!f.annotations.empty())

jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

@@ -2955,8 +2955,15 @@ optionalt<exprt> java_bytecode_convert_methodt::convert_invoke_dynamic(
   if(return_type.id() == ID_empty)
     return {};
 
-  return zero_initializer(
-    return_type, location, namespacet(symbol_table), get_message_handler());
+  const auto value =
+    zero_initializer(return_type, location, namespacet(symbol_table));
+  if(!value.has_value())
+  {
+    error().source_location = location;
+    error() << "failed to zero-initialize return type" << eom;
+    throw 0;
+  }
+  return value;
 }
 
 void java_bytecode_convert_methodt::draw_edges_from_ret_to_jsr(

jbmc/src/java_bytecode/java_entry_point.cpp

@@ -193,13 +193,18 @@ static void java_static_lifetime_init(
         // First initialize the object as prior to a constructor:
         namespacet ns(symbol_table);
 
-        exprt zero_object =
-          zero_initializer(
-            sym.type, source_locationt(), ns, message_handler);
+        auto zero_object = zero_initializer(sym.type, source_locationt(), ns);
+        if(!zero_object.has_value())
+        {
+          messaget message(message_handler);
+          message.error() << "failed to zero-initialize " << sym.name
+                          << messaget::eom;
+          throw 0;
+        }
         set_class_identifier(
-          to_struct_expr(zero_object), ns, to_symbol_type(sym.type));
+          to_struct_expr(*zero_object), ns, to_symbol_type(sym.type));
 
-        code_block.add(code_assignt(sym.symbol_expr(), zero_object));
+        code_block.add(code_assignt(sym.symbol_expr(), *zero_object));
 
         // Then call the init function:
         code_block.move(initializer_call);

jbmc/src/java_bytecode/java_object_factory.cpp

@@ -1044,19 +1044,17 @@ void java_object_factoryt::gen_nondet_struct_init(
     // passes can easily recognise leaves no uninitialised state behind.
 
     // This code mirrors the `remove_java_new` pass:
-    null_message_handlert nullout;
-    exprt initial_object =
-      zero_initializer(
-        struct_type, source_locationt(), ns, nullout);
+    auto initial_object = zero_initializer(struct_type, source_locationt(), ns);
+    CHECK_RETURN(initial_object.has_value());
     irep_idt qualified_clsid = "java::" + id2string(class_identifier);
     set_class_identifier(
-      to_struct_expr(initial_object), ns, symbol_typet(qualified_clsid));
+      to_struct_expr(*initial_object), ns, symbol_typet(qualified_clsid));
 
     // If the initialised type is a special-cased String type (one with length
     // and data fields introduced by string-library preprocessing), initialise
     // those fields with nondet values:
     skip_special_string_fields = initialize_nondet_string_fields(
-      to_struct_expr(initial_object),
+      to_struct_expr(*initial_object),
       assignments,
       object_factory_parameters.min_nondet_string_length,
       object_factory_parameters.max_nondet_string_length,
@@ -1065,7 +1063,7 @@ void java_object_factoryt::gen_nondet_struct_init(
       symbol_table,
       object_factory_parameters.string_printable);
 
-    assignments.add(code_assignt(expr, initial_object));
+    assignments.add(code_assignt(expr, *initial_object));
   }
 
   for(const auto &component : components)

jbmc/src/java_bytecode/java_string_literals.cpp

@@ -192,8 +192,10 @@ symbol_exprt get_or_create_string_literal_symbol(
       // Other members of JDK's java.lang.String we don't understand
       // without string-refinement. Just zero-init them; consider using
       // test-gen-like nondet object trees instead.
-      literal_init.copy_to_operands(
-        zero_initializer(comp.type(), string_expr.source_location(), ns));
+      const auto init =
+        zero_initializer(comp.type(), string_expr.source_location(), ns);
+      CHECK_RETURN(init.has_value());
+      literal_init.copy_to_operands(*init);
     }
     new_symbol.value = literal_init;
   }

jbmc/src/java_bytecode/remove_java_new.cpp

@@ -93,12 +93,12 @@ goto_programt::targett remove_java_newt::lower_java_new(
 
   // zero-initialize the object
   dereference_exprt deref(lhs, object_type);
-  exprt zero_object =
-    zero_initializer(object_type, location, ns, get_message_handler());
+  auto zero_object = zero_initializer(object_type, location, ns);
+  CHECK_RETURN(zero_object.has_value());
   set_class_identifier(
-    to_struct_expr(zero_object), ns, to_symbol_type(object_type));
+    to_struct_expr(*zero_object), ns, to_symbol_type(object_type));
   goto_programt::targett t_i = dest.insert_after(target);
-  t_i->make_assignment(code_assignt(deref, zero_object));
+  t_i->make_assignment(code_assignt(deref, *zero_object));
   t_i->source_location = location;
 
   return t_i;
@@ -153,12 +153,12 @@ goto_programt::targett remove_java_newt::lower_java_new_array(
 
   // Init base class:
   dereference_exprt deref(lhs, object_type);
-  exprt zero_object =
-    zero_initializer(object_type, location, ns, get_message_handler());
+  auto zero_object = zero_initializer(object_type, location, ns);
+  CHECK_RETURN(zero_object.has_value());
   set_class_identifier(
-    to_struct_expr(zero_object), ns, to_symbol_type(object_type));
+    to_struct_expr(*zero_object), ns, to_symbol_type(object_type));
   goto_programt::targett t_i = dest.insert_before(next);
-  t_i->make_assignment(code_assignt(deref, zero_object));
+  t_i->make_assignment(code_assignt(deref, *zero_object));
   t_i->source_location = location;
 
   // if it's an array, we need to set the length field
@@ -232,10 +232,11 @@ goto_programt::targett remove_java_newt::lower_java_new_array(
   // zero-initialize the data
   if(!rhs.get_bool(ID_skip_initialize))
   {
-    exprt zero_element = zero_initializer(
-      data.type().subtype(), location, ns, get_message_handler());
+    const auto zero_element =
+      zero_initializer(data.type().subtype(), location, ns);
+    CHECK_RETURN(zero_element.has_value());
     codet array_set(ID_array_set);
-    array_set.copy_to_operands(new_array_data_symbol, zero_element);
+    array_set.copy_to_operands(new_array_data_symbol, *zero_element);
     goto_programt::targett t_d = dest.insert_before(next);
     t_d->make_other(array_set);
     t_d->source_location = location;

regression/ansi-c/array_initialization4/main.c

@@ -0,0 +1,13 @@
+#include <assert.h>
+
+int foo(unsigned n)
+{
+  assert(n > 0);
+  int A[n] = {1};
+  return A[0];
+}
+
+int main()
+{
+  assert(foo(1) == 1);
+}

regression/ansi-c/array_initialization4/test.desc

@@ -0,0 +1,7 @@
+CORE
+main.c
+
+^EXIT=(1|64)$
+^SIGNAL=0$
+--
+^warning: ignoring

src/ansi-c/c_typecheck_initializer.cpp

@@ -114,13 +114,16 @@ 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());
-        tmp.operands().resize(integer2size_t(array_size), zero);
+        const auto zero =
+          zero_initializer(full_type.subtype(), value.source_location(), *this);
+        if(!zero.has_value())
+        {
+          err_location(value);
+          error() << "cannot zero-initialize array with subtype `"
+                  << to_string(full_type.subtype()) << "'" << eom;
+          throw 0;
+        }
+        tmp.operands().resize(integer2size_t(array_size), *zero);
       }
     }
 
@@ -171,13 +174,16 @@ 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());
-        tmp2.operands().resize(integer2size_t(array_size), zero);
+        const auto zero =
+          zero_initializer(full_type.subtype(), value.source_location(), *this);
+        if(!zero.has_value())
+        {
+          err_location(value);
+          error() << "cannot zero-initialize array with subtype `"
+                  << to_string(full_type.subtype()) << "'" << eom;
+          throw 0;
+        }
+        tmp2.operands().resize(integer2size_t(array_size), *zero);
       }
     }
 
@@ -395,13 +401,16 @@ 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());
-          dest->operands().resize(integer2size_t(index)+1, zero);
+          const auto zero = zero_initializer(
+            full_type.subtype(), value.source_location(), *this);
+          if(!zero.has_value())
+          {
+            err_location(value);
+            error() << "cannot zero-initialize array with subtype `"
+                    << to_string(full_type.subtype()) << "'" << eom;
+            throw 0;
+          }
+          dest->operands().resize(integer2size_t(index) + 1, *zero);
 
           // todo: adjust type!
         }
@@ -461,15 +470,17 @@ 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());
+        const auto zero =
+          zero_initializer(component.type(), value.source_location(), *this);
+        if(!zero.has_value())
+        {
+          err_location(value);
+          error() << "cannot zero-initialize union component of type `"
+                  << to_string(component.type()) << "'" << eom;
+          throw 0;
+        }
+        union_exprt union_expr(component.get_name(), *zero, type);
         union_expr.add_source_location()=value.source_location();
-        union_expr.set_component_name(component.get_name());
         *dest=union_expr;
       }
 
@@ -524,15 +535,17 @@ exprt::operandst::const_iterator c_typecheck_baset::do_designated_initializer(
         const union_typet::componentt &component=
           union_type.components().front();
 
-        union_exprt union_expr(type);
-        union_expr.op()=
-          zero_initializer(
-            component.type(),
-            value.source_location(),
-            *this,
-            get_message_handler());
+        const auto zero =
+          zero_initializer(component.type(), value.source_location(), *this);
+        if(!zero.has_value())
+        {
+          err_location(value);
+          error() << "cannot zero-initialize union component of type `"
+                  << to_string(component.type()) << "'" << eom;
+          throw 0;
+        }
+        union_exprt union_expr(component.get_name(), *zero, type);
         union_expr.add_source_location()=value.source_location();
-        union_expr.set_component_name(component.get_name());
         *dest=union_expr;
       }
     }
@@ -830,9 +843,15 @@ 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());
+    const auto zero = zero_initializer(type, value.source_location(), *this);
+    if(!zero.has_value())
+    {
+      err_location(value.source_location());
+      error() << "cannot zero-initialize `" << to_string(full_type) << "'"
+              << eom;
+      throw 0;
+    }
+    result = *zero;
   }
   else if(full_type.id()==ID_array)
   {
@@ -845,9 +864,15 @@ exprt c_typecheck_baset::do_initializer_list(
     else
     {
       // start with zero everywhere
-      result=
-        zero_initializer(
-          type, value.source_location(), *this, get_message_handler());
+      const auto zero = zero_initializer(type, value.source_location(), *this);
+      if(!zero.has_value())
+      {
+        err_location(value.source_location());
+        error() << "cannot zero-initialize `" << to_string(full_type) << "'"
+                << eom;
+        throw 0;
+      }
+      result = *zero;
     }
 
     // 6.7.9, 14: An array of character type may be initialized by a character

src/cpp/cpp_typecheck_expr.cpp

@@ -870,15 +870,18 @@ 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());
-
-    new_expr.add_source_location()=expr.source_location();
-    expr=new_expr;
+    auto new_expr =
+      ::zero_initializer(expr.type(), expr.find_source_location(), *this);
+    if(!new_expr.has_value())
+    {
+      err_location(expr.find_source_location());
+      error() << "cannot zero-initialize `" << to_string(expr.type()) << "'"
+              << eom;
+      throw 0;
+    }
+
+    new_expr->add_source_location() = expr.source_location();
+    expr = *new_expr;
   }
   else if(expr.operands().size()==1)
   {

src/cpp/cpp_typecheck_initializer.cpp

@@ -306,13 +306,16 @@ void cpp_typecheckt::zero_initializer(
   }
   else
   {
-    exprt value=
-      ::zero_initializer(
-        final_type, source_location, *this, get_message_handler());
+    const auto value = ::zero_initializer(final_type, source_location, *this);
+    if(!value.has_value())
+    {
+      err_location(source_location);
+      error() << "cannot zero-initialize `" << to_string(final_type) << "'"
+              << eom;
+      throw 0;
+    }
 
-    code_assignt assign;
-    assign.lhs()=object;
-    assign.rhs()=value;
+    code_assignt assign(object, *value);
     assign.add_source_location()=source_location;
 
     typecheck_expr(assign.op0());