Merge pull request #4287 from smowton/smowton/fix/missing-enum-non-fatal

Make failed nondet Enum assignment non-fatal

Author: smowton

Diff for: jbmc/src/java_bytecode/convert_java_nondet.cpp

@@ -57,7 +57,8 @@ static goto_programt get_gen_nondet_init_instructions(
     skip_classid,
     lifetimet::DYNAMIC,
     object_factory_parameters,
-    update_in_placet::NO_UPDATE_IN_PLACE);
+    update_in_placet::NO_UPDATE_IN_PLACE,
+    message_handler);
 
   goto_programt instructions;
   goto_convert(

Diff for: jbmc/src/java_bytecode/java_bytecode_language.cpp

@@ -869,7 +869,8 @@ bool java_bytecode_languaget::generate_support_functions(
         symbol_table,
         assume_inputs_non_null,
         object_factory_parameters,
-        get_pointer_type_selector());
+        get_pointer_type_selector(),
+        get_message_handler());
     });
 }
 
@@ -1068,22 +1069,25 @@ bool java_bytecode_languaget::convert_single_method(
           symbol_table,
           nondet_static,
           object_factory_parameters,
-          get_pointer_type_selector());
+          get_pointer_type_selector(),
+          get_message_handler());
       else
         writable_symbol.value = get_clinit_wrapper_body(
           function_id,
           symbol_table,
           nondet_static,
           object_factory_parameters,
-          get_pointer_type_selector());
+          get_pointer_type_selector(),
+          get_message_handler());
       break;
     case synthetic_method_typet::STUB_CLASS_STATIC_INITIALIZER:
       writable_symbol.value =
         stub_global_initializer_factory.get_stub_initializer_body(
           function_id,
           symbol_table,
           object_factory_parameters,
-          get_pointer_type_selector());
+          get_pointer_type_selector(),
+          get_message_handler());
       break;
     }
     // Notify lazy methods of static calls made from the newly generated

Diff for: jbmc/src/java_bytecode/java_entry_point.cpp

@@ -258,7 +258,8 @@ static void java_static_lifetime_init(
           lifetimet::STATIC_GLOBAL,
           parameters,
           pointer_type_selector,
-          update_in_placet::NO_UPDATE_IN_PLACE);
+          update_in_placet::NO_UPDATE_IN_PLACE,
+          message_handler);
       }
       else if(sym.value.is_not_nil())
       {
@@ -296,7 +297,8 @@ std::pair<code_blockt, std::vector<exprt>> java_build_arguments(
   symbol_table_baset &symbol_table,
   bool assume_init_pointers_not_null,
   java_object_factory_parameterst object_factory_parameters,
-  const select_pointer_typet &pointer_type_selector)
+  const select_pointer_typet &pointer_type_selector,
+  message_handlert &message_handler)
 {
   const java_method_typet::parameterst &parameters =
     to_java_method_type(function.type).parameters();
@@ -354,7 +356,8 @@ std::pair<code_blockt, std::vector<exprt>> java_build_arguments(
         factory_parameters,
         lifetimet::AUTOMATIC_LOCAL,
         function.location,
-        pointer_type_selector);
+        pointer_type_selector,
+        message_handler);
     }
     else
     {
@@ -400,7 +403,8 @@ std::pair<code_blockt, std::vector<exprt>> java_build_arguments(
           factory_parameters,
           lifetimet::DYNAMIC,
           function.location,
-          pointer_type_selector);
+          pointer_type_selector,
+          message_handler);
         init_code_for_type.add(
           code_assignt(
             result_symbol.symbol_expr(),

Diff for: jbmc/src/java_bytecode/java_entry_point.h

@@ -169,6 +169,7 @@ bool generate_java_start_function(
 /// \param pointer_type_selector: Means of selecting the type of value
 ///   constructed for reference types which are initialised by the code
 ///   returned.
+/// \param message_handler: log
 /// \returns A pairing of the code to initialise the arguments and a std::vector
 ///   of the expressions for these arguments. The vector contains one element
 ///   per parameter of \p function. The vector of expressions can be used as
@@ -182,6 +183,7 @@ std::pair<code_blockt, std::vector<exprt>> java_build_arguments(
   symbol_table_baset &symbol_table,
   bool assume_init_pointers_not_null,
   java_object_factory_parameterst object_factory_parameters,
-  const select_pointer_typet &pointer_type_selector);
+  const select_pointer_typet &pointer_type_selector,
+  message_handlert &message_handler);
 
 #endif // CPROVER_JAVA_BYTECODE_JAVA_ENTRY_POINT_H

Diff for: jbmc/src/java_bytecode/java_object_factory.cpp

@@ -59,6 +59,9 @@ class java_object_factoryt
 
   allocate_objectst allocate_objects;
 
+  /// Log for reporting warnings and errors in object creation
+  messaget log;
+
   code_assignt get_null_assignment(
     const exprt &expr,
     const pointer_typet &ptr_type);
@@ -84,7 +87,8 @@ class java_object_factoryt
     const source_locationt &loc,
     const java_object_factory_parameterst _object_factory_parameters,
     symbol_table_baset &_symbol_table,
-    const select_pointer_typet &pointer_type_selector)
+    const select_pointer_typet &pointer_type_selector,
+    message_handlert &log)
     : loc(loc),
       object_factory_parameters(_object_factory_parameters),
       symbol_table(_symbol_table),
@@ -94,7 +98,8 @@ class java_object_factoryt
         ID_java,
         loc,
         object_factory_parameters.function_id,
-        symbol_table)
+        symbol_table),
+      log(log)
   {}
 
   void gen_nondet_array_init(
@@ -104,7 +109,7 @@ class java_object_factoryt
     update_in_placet,
     const source_locationt &location);
 
-  void gen_nondet_enum_init(
+  bool gen_nondet_enum_init(
     code_blockt &assignments,
     const exprt &expr,
     const java_class_typet &java_class_type,
@@ -263,8 +268,8 @@ void java_object_factoryt::gen_pointer_target_init(
     }
     if(target_class_type.get_base("java::java.lang.Enum"))
     {
-      gen_nondet_enum_init(assignments, expr, target_class_type, location);
-      return;
+      if(gen_nondet_enum_init(assignments, expr, target_class_type, location))
+        return;
     }
   }
 
@@ -1435,20 +1440,31 @@ void java_object_factoryt::gen_nondet_array_init(
 ///     int i = nondet(int);
 ///     assume(0 < = i < $VALUES.length);
 ///     expr = $VALUES[i];
-/// where $VALUES is a variable generated by the Java compiler that stores
-/// the array that is returned by Enum.values().
-void java_object_factoryt::gen_nondet_enum_init(
+/// where $VALUES is a variable generated by the Java compiler and which gives
+/// the possible values of a particular enum subtype (this is the same array
+/// that is returned by Enum.values()).
+/// This may fail if the $VALUES static field is not present. Ensuring that
+/// field is in the symbol table when this method may be applicable is the
+/// driver program's responsibility: for example, \ref ci_lazy_methods.cpp makes
+/// some effort to retain this field when a stub method might refer to it.
+/// \return true on success
+bool java_object_factoryt::gen_nondet_enum_init(
   code_blockt &assignments,
   const exprt &expr,
   const java_class_typet &java_class_type,
   const source_locationt &location)
 {
   const irep_idt &class_name = java_class_type.get_name();
   const irep_idt values_name = id2string(class_name) + ".$VALUES";
-  INVARIANT(
-    ns.get_symbol_table().has_symbol(values_name),
-    "The $VALUES array (populated by clinit_wrapper) should be in the "
-    "symbol table");
+  if(!ns.get_symbol_table().has_symbol(values_name))
+  {
+    log.warning() << values_name
+                  << " is missing, so the corresponding Enum "
+                     "type will nondet initialised"
+                  << messaget::eom;
+    return false;
+  }
+
   const symbolt &values = ns.lookup(values_name);
 
   // Access members (length and data) of $VALUES array
@@ -1473,6 +1489,8 @@ void java_object_factoryt::gen_nondet_enum_init(
   const dereference_exprt arraycellref(plus);
   code_assignt enum_assign(expr, typecast_exprt(arraycellref, expr.type()));
   assignments.add(enum_assign);
+
+  return true;
 }
 
 static void assert_type_consistency(const code_blockt &assignments)
@@ -1510,7 +1528,8 @@ exprt object_factory(
   java_object_factory_parameterst parameters,
   lifetimet lifetime,
   const source_locationt &loc,
-  const select_pointer_typet &pointer_type_selector)
+  const select_pointer_typet &pointer_type_selector,
+  message_handlert &log)
 {
   irep_idt identifier=id2string(goto_functionst::entry_point())+
     "::"+id2string(base_name);
@@ -1531,10 +1550,7 @@ exprt object_factory(
   CHECK_RETURN(!moving_symbol_failed);
 
   java_object_factoryt state(
-    loc,
-    parameters,
-    symbol_table,
-    pointer_type_selector);
+    loc, parameters, symbol_table, pointer_type_selector, log);
   code_blockt assignments;
   state.gen_nondet_init(
     assignments,
@@ -1587,6 +1603,7 @@ exprt object_factory(
 ///   MAY_UPDATE_IN_PLACE: generate a runtime nondet branch between the NO_
 ///   and MUST_ cases.
 ///   MUST_UPDATE_IN_PLACE: reinitialize an existing object
+/// \param log: used to report object construction warnings and failures
 /// \return `init_code` gets an instruction sequence to initialize or
 ///   reinitialize `expr` and child objects it refers to. `symbol_table` is
 ///   modified with any new symbols created. This includes any necessary
@@ -1600,13 +1617,11 @@ void gen_nondet_init(
   lifetimet lifetime,
   const java_object_factory_parameterst &object_factory_parameters,
   const select_pointer_typet &pointer_type_selector,
-  update_in_placet update_in_place)
+  update_in_placet update_in_place,
+  message_handlert &log)
 {
   java_object_factoryt state(
-    loc,
-    object_factory_parameters,
-    symbol_table,
-    pointer_type_selector);
+    loc, object_factory_parameters, symbol_table, pointer_type_selector, log);
   code_blockt assignments;
   state.gen_nondet_init(
     assignments,
@@ -1634,7 +1649,8 @@ exprt object_factory(
   symbol_tablet &symbol_table,
   const java_object_factory_parameterst &object_factory_parameters,
   lifetimet lifetime,
-  const source_locationt &location)
+  const source_locationt &location,
+  message_handlert &log)
 {
   select_pointer_typet pointer_type_selector;
   return object_factory(
@@ -1645,7 +1661,8 @@ exprt object_factory(
     object_factory_parameters,
     lifetime,
     location,
-    pointer_type_selector);
+    pointer_type_selector,
+    log);
 }
 
 /// Call gen_nondet_init() above with a default (identity) pointer_type_selector
@@ -1657,7 +1674,8 @@ void gen_nondet_init(
   bool skip_classid,
   lifetimet lifetime,
   const java_object_factory_parameterst &object_factory_parameters,
-  update_in_placet update_in_place)
+  update_in_placet update_in_place,
+  message_handlert &log)
 {
   select_pointer_typet pointer_type_selector;
   gen_nondet_init(
@@ -1669,7 +1687,8 @@ void gen_nondet_init(
     lifetime,
     object_factory_parameters,
     pointer_type_selector,
-    update_in_place);
+    update_in_place,
+    log);
 }
 
 /// Adds a call for the given method to the end of `assignments` if the method

Diff for: jbmc/src/java_bytecode/java_object_factory.h

@@ -87,7 +87,8 @@ exprt object_factory(
   java_object_factory_parameterst parameters,
   lifetimet lifetime,
   const source_locationt &location,
-  const select_pointer_typet &pointer_type_selector);
+  const select_pointer_typet &pointer_type_selector,
+  message_handlert &log);
 
 exprt object_factory(
   const typet &type,
@@ -96,7 +97,8 @@ exprt object_factory(
   symbol_tablet &symbol_table,
   const java_object_factory_parameterst &object_factory_parameters,
   lifetimet lifetime,
-  const source_locationt &location);
+  const source_locationt &location,
+  message_handlert &log);
 
 enum class update_in_placet
 {
@@ -114,7 +116,8 @@ void gen_nondet_init(
   lifetimet lifetime,
   const java_object_factory_parameterst &object_factory_parameters,
   const select_pointer_typet &pointer_type_selector,
-  update_in_placet update_in_place);
+  update_in_placet update_in_place,
+  message_handlert &log);
 
 void gen_nondet_init(
   const exprt &expr,
@@ -124,6 +127,7 @@ void gen_nondet_init(
   bool skip_classid,
   lifetimet lifetime,
   const java_object_factory_parameterst &object_factory_parameters,
-  update_in_placet update_in_place);
+  update_in_placet update_in_place,
+  message_handlert &log);
 
 #endif // CPROVER_JAVA_BYTECODE_JAVA_OBJECT_FACTORY_H