Java object factory: take a message handler

Author: smowton

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(

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

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(),

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

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(
@@ -1517,7 +1522,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);
@@ -1538,10 +1544,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,
@@ -1594,6 +1597,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
@@ -1607,13 +1611,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,
@@ -1641,7 +1643,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(
@@ -1652,7 +1655,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
@@ -1664,7 +1668,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(
@@ -1676,7 +1681,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

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

jbmc/src/java_bytecode/java_static_initializers.cpp

@@ -195,13 +195,15 @@ gen_clinit_eqexpr(const exprt &expr, const clinit_statest state)
 ///   if nondet-static is true)
 /// \param pointer_type_selector: used to choose concrete types for abstract-
 ///   typed globals and fields (only needed if nondet-static is true)
+/// \param message_handler: log
 static void clinit_wrapper_do_recursive_calls(
   symbol_table_baset &symbol_table,
   const irep_idt &class_name,
   code_blockt &init_body,
   const bool nondet_static,
   const 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 symbolt &class_symbol = symbol_table.lookup_ref(class_name);
   for(const auto &base : to_class_type(class_symbol.type).bases())
@@ -265,7 +267,8 @@ static void clinit_wrapper_do_recursive_calls(
         lifetimet::DYNAMIC,
         parameters,
         pointer_type_selector,
-        update_in_placet::NO_UPDATE_IN_PLACE);
+        update_in_placet::NO_UPDATE_IN_PLACE,
+        message_handler);
     }
   }
 }
@@ -447,13 +450,15 @@ static void create_clinit_wrapper_symbols(
 ///   if nondet-static is true)
 /// \param pointer_type_selector: used to choose concrete types for abstract-
 ///   typed globals and fields (only needed if nondet-static is true)
+/// \param message_handler: log output
 /// \return the body of the static initializer wrapper
 code_blockt get_thread_safe_clinit_wrapper_body(
   const irep_idt &function_id,
   symbol_table_baset &symbol_table,
   const bool nondet_static,
   const 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 symbolt &wrapper_method_symbol = symbol_table.lookup_ref(function_id);
   irep_idt class_name = wrapper_method_symbol.type.get(ID_C_class);
@@ -605,7 +610,8 @@ code_blockt get_thread_safe_clinit_wrapper_body(
       init_body,
       nondet_static,
       object_factory_parameters,
-      pointer_type_selector);
+      pointer_type_selector,
+      message_handler);
     function_body.append(init_body);
   }
 
@@ -637,13 +643,15 @@ code_blockt get_thread_safe_clinit_wrapper_body(
 ///   if nondet-static is true)
 /// \param pointer_type_selector: used to choose concrete types for abstract-
 ///   typed globals and fields (only needed if nondet-static is true)
+/// \param message_handler: log output
 /// \return the body of the static initializer wrapper
 code_ifthenelset get_clinit_wrapper_body(
   const irep_idt &function_id,
   symbol_table_baset &symbol_table,
   const bool nondet_static,
   const 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)
 {
   // Assume that class C extends class C' and implements interfaces
   // I1, ..., In. We now create the following function (possibly recursively
@@ -687,7 +695,8 @@ code_ifthenelset get_clinit_wrapper_body(
     init_body,
     nondet_static,
     object_factory_parameters,
-    pointer_type_selector);
+    pointer_type_selector,
+    message_handler);
 
   // the entire body of the function is an if-then-else
   return code_ifthenelset(std::move(check_already_run), std::move(init_body));
@@ -828,12 +837,14 @@ void stub_global_initializer_factoryt::create_stub_global_initializer_symbols(
 ///   the stub globals and objects reachable from them
 /// \param pointer_type_selector: used to choose concrete types for abstract-
 ///   typed globals and fields.
+/// \param message_handler: log output
 /// \return synthetic static initializer body.
 code_blockt stub_global_initializer_factoryt::get_stub_initializer_body(
   const irep_idt &function_id,
   symbol_table_baset &symbol_table,
   const 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 symbolt &stub_initializer_symbol = symbol_table.lookup_ref(function_id);
   irep_idt class_id = stub_initializer_symbol.type.get(ID_C_class);
@@ -875,7 +886,8 @@ code_blockt stub_global_initializer_factoryt::get_stub_initializer_body(
       lifetimet::DYNAMIC,
       parameters,
       pointer_type_selector,
-      update_in_placet::NO_UPDATE_IN_PLACE);
+      update_in_placet::NO_UPDATE_IN_PLACE,
+      message_handler);
   }
 
   return static_init_body;