Merge pull request #3057 from tautschnig/expr_init-fix

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

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

@@ -2951,8 +2951,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());