Merge pull request diffblue#4280 from thomasspriggs/tas/entry_point

Parameterise usage of `java_build_arguments` to allow replacing this function only

Author: thomasspriggs

jbmc/src/java_bytecode/java_bytecode_language.cpp

@@ -862,7 +862,15 @@ bool java_bytecode_languaget::generate_support_functions(
     assert_uncaught_exceptions,
     object_factory_parameters,
     get_pointer_type_selector(),
-    string_refinement_enabled);
+    string_refinement_enabled,
+    [&](const symbolt &function, symbol_table_baset &symbol_table) {
+      return java_build_arguments(
+        function,
+        symbol_table,
+        assume_inputs_non_null,
+        object_factory_parameters,
+        get_pointer_type_selector());
+    });
 }
 
 /// Uses a simple context-insensitive ('ci') analysis to determine which methods

jbmc/src/java_bytecode/java_entry_point.cpp

@@ -28,6 +28,19 @@ Author: Daniel Kroening, [email protected]
 
 #define JAVA_MAIN_METHOD "main:([Ljava/lang/String;)V"
 
+static optionalt<codet> record_return_value(
+  const symbolt &function,
+  const symbol_table_baset &symbol_table);
+
+static code_blockt record_pointer_parameters(
+  const symbolt &function,
+  const std::vector<exprt> &arguments,
+  const symbol_table_baset &symbol_table);
+
+static codet record_exception(
+  const symbolt &function,
+  const symbol_table_baset &symbol_table);
+
 static void create_initialize(symbol_table_baset &symbol_table)
 {
   // If __CPROVER_initialize already exists, replace it. It may already exist
@@ -72,22 +85,6 @@ static bool should_init_symbol(const symbolt &sym)
   return is_java_string_literal_id(sym.name);
 }
 
-/// Get the symbol name of java.lang.Class' initializer method. This method
-/// should initialize a Class instance with known properties of the type it
-/// represents, such as its name, whether it is abstract, or an enumeration,
-/// etc. The method may or may not exist in any particular symbol table; it is
-/// up to the caller to check.
-/// The method's Java signature is:
-/// void cproverInitializeClassLiteral(
-///   String name,
-///   boolean isAnnotation,
-///   boolean isArray,
-///   boolean isInterface,
-///   boolean isSynthetic,
-///   boolean isLocalClass,
-///   boolean isMemberClass,
-///   boolean isEnum);
-/// \return Class initializer method's symbol name.
 irep_idt get_java_class_literal_initializer_signature()
 {
   static irep_idt signature =
@@ -294,18 +291,8 @@ bool is_java_main(const symbolt &function)
   return named_main && is_static && has_correct_type && public_access;
 }
 
-///  Extends \p init_code with code that allocates the objects used as test
-///  arguments for the function under test (\p function) and
-///  non-deterministically initializes them.
-///
-///  All the code generated by this function goes to __CPROVER__start, just
-///  before the call to the method under test.
-///
-///  \returns A std::vector of symbol_exprt, one per parameter of \p function,
-///  containing the objects that can be used as arguments for \p function.
-exprt::operandst java_build_arguments(
+std::pair<code_blockt, std::vector<exprt>> java_build_arguments(
   const symbolt &function,
-  code_blockt &init_code,
   symbol_table_baset &symbol_table,
   bool assume_init_pointers_not_null,
   java_object_factory_parameterst object_factory_parameters,
@@ -314,6 +301,7 @@ exprt::operandst java_build_arguments(
   const java_method_typet::parameterst &parameters =
     to_java_method_type(function.type).parameters();
 
+  code_blockt init_code;
   exprt::operandst main_arguments;
   main_arguments.resize(parameters.size());
 
@@ -444,83 +432,98 @@ exprt::operandst java_build_arguments(
     init_code.add(std::move(input));
   }
 
-  return main_arguments;
+  return make_pair(init_code, main_arguments);
 }
 
-void java_record_outputs(
+/// Mark return value, pointer type parameters and the exception as outputs.
+static code_blockt java_record_outputs(
   const symbolt &function,
   const exprt::operandst &main_arguments,
-  code_blockt &init_code,
   symbol_table_baset &symbol_table)
 {
-  const java_method_typet::parameterst &parameters =
-    to_java_method_type(function.type).parameters();
+  code_blockt init_code;
 
-  exprt::operandst result;
-  result.reserve(parameters.size()+1);
+  if(auto return_value = record_return_value(function, symbol_table))
+  {
+    init_code.add(std::move(*return_value));
+  }
 
-  bool has_return_value =
-    to_java_method_type(function.type).return_type() != java_void_type();
+  init_code.append(
+    record_pointer_parameters(function, main_arguments, symbol_table));
 
-  if(has_return_value)
-  {
-    // record return value
-    codet output(ID_output);
-    output.operands().resize(2);
+  init_code.add(record_exception(function, symbol_table));
 
-    const symbolt &return_symbol=
-      *symbol_table.lookup(JAVA_ENTRY_POINT_RETURN_SYMBOL);
+  return init_code;
+}
 
-    output.op0()=
-      address_of_exprt(
-        index_exprt(
-          string_constantt(return_symbol.base_name),
-          from_integer(0, index_type())));
-    output.op1()=return_symbol.symbol_expr();
-    output.add_source_location()=function.location;
+static optionalt<codet> record_return_value(
+  const symbolt &function,
+  const symbol_table_baset &symbol_table)
+{
+  if(to_java_method_type(function.type).return_type() == java_void_type())
+    return {};
 
-    init_code.add(std::move(output));
-  }
+  const symbolt &return_symbol =
+    *symbol_table.lookup(JAVA_ENTRY_POINT_RETURN_SYMBOL);
 
-  for(std::size_t param_number=0;
-      param_number<parameters.size();
+  codet output(ID_output);
+  output.operands().resize(2);
+  output.op0() = address_of_exprt(index_exprt(
+    string_constantt(return_symbol.base_name), from_integer(0, index_type())));
+  output.op1() = return_symbol.symbol_expr();
+  output.add_source_location() = function.location;
+  return output;
+}
+
+static code_blockt record_pointer_parameters(
+  const symbolt &function,
+  const std::vector<exprt> &arguments,
+  const symbol_table_baset &symbol_table)
+{
+  const java_method_typet::parameterst &parameters =
+    to_java_method_type(function.type).parameters();
+
+  code_blockt init_code;
+
+  for(std::size_t param_number = 0; param_number < parameters.size();
       param_number++)
   {
-    const symbolt &p_symbol=
+    const symbolt &p_symbol =
       *symbol_table.lookup(parameters[param_number].get_identifier());
 
-    if(p_symbol.type.id()==ID_pointer)
-    {
-      // record as an output
-      codet output(ID_output);
-      output.operands().resize(2);
-      output.op0()=
-        address_of_exprt(
-          index_exprt(
-            string_constantt(p_symbol.base_name),
-            from_integer(0, index_type())));
-      output.op1()=main_arguments[param_number];
-      output.add_source_location()=function.location;
-
-      init_code.add(std::move(output));
-    }
+    if(!can_cast_type<pointer_typet>(p_symbol.type))
+      continue;
+
+    codet output(ID_output);
+    output.operands().resize(2);
+    output.op0() = address_of_exprt(index_exprt(
+      string_constantt(p_symbol.base_name), from_integer(0, index_type())));
+    output.op1() = arguments[param_number];
+    output.add_source_location() = function.location;
+
+    init_code.add(std::move(output));
   }
+  return init_code;
+}
 
+static codet record_exception(
+  const symbolt &function,
+  const symbol_table_baset &symbol_table)
+{
   // record exceptional return variable as output
   codet output(ID_output);
   output.operands().resize(2);
 
   // retrieve the exception variable
-  const symbolt exc_symbol=*symbol_table.lookup(
-    JAVA_ENTRY_POINT_EXCEPTION_SYMBOL);
+  const symbolt &exc_symbol =
+    symbol_table.lookup_ref(JAVA_ENTRY_POINT_EXCEPTION_SYMBOL);
 
   output.op0()=address_of_exprt(
     index_exprt(string_constantt(exc_symbol.base_name),
                 from_integer(0, index_type())));
   output.op1()=exc_symbol.symbol_expr();
   output.add_source_location()=function.location;
-
-  init_code.add(std::move(output));
+  return output;
 }
 
 main_function_resultt get_main_symbol(
@@ -580,40 +583,6 @@ main_function_resultt get_main_symbol(
   }
 }
 
-/// Given the \p symbol_table and the \p main_class to test, this function
-/// generates a new function __CPROVER__start that calls the method under tests.
-///
-/// If __CPROVER__start is already in the `symbol_table`, it silently returns.
-/// Otherwise it finds the method under test using `get_main_symbol` and
-/// constructs a body for __CPROVER__start which does as follows:
-///
-/// 1. Allocates and initializes the parameters of the method under test.
-/// 2. Call it and save its return variable in the variable 'return'.
-/// 3. Declare variable 'return' as an output variable (codet with id
-///    ID_output), together with other objects possibly altered by the execution
-///    the method under test (in `java_record_outputs`)
-///
-/// When \p assume_init_pointers_not_null is false, the generated parameter
-/// initialization code will non-deterministically set input parameters to
-/// either null or a stack-allocated object. Observe that the null/non-null
-/// setting only applies to the parameter itself, and is not propagated to other
-/// pointers that it might be necessary to initialize in the object tree rooted
-/// at the parameter.
-/// Parameter \p max_nondet_array_length provides the maximum length for an
-/// array used as part of the input to the method under test, and
-/// \p max_nondet_tree_depth defines the maximum depth of the object tree
-/// created for such inputs. This maximum depth is used **in conjunction** with
-/// the so-called "recursive type set" (see field `recursive_set` in class
-/// java_object_factoryt) to bound the depth of the object tree for the
-/// parameter. Only when
-/// - the depth of the tree is >= max_nondet_tree_depth **AND**
-/// - the type of the object under initialization is already found in the
-///   recursive set
-/// then that object is not initalized and the reference pointing to it is
-/// (deterministically) set to null. This is a source of underapproximation in
-/// our approach to test generation, and should perhaps be fixed in the future.
-///
-/// \return true if error occurred on entry point search
 bool java_entry_point(
   symbol_table_baset &symbol_table,
   const irep_idt &main_class,
@@ -622,7 +591,8 @@ bool java_entry_point(
   bool assert_uncaught_exceptions,
   const java_object_factory_parameterst &object_factory_parameters,
   const select_pointer_typet &pointer_type_selector,
-  bool string_refinement_enabled)
+  bool string_refinement_enabled,
+  const build_argumentst &build_arguments)
 {
   // check if the entry point is already there
   if(symbol_table.symbols.find(goto_functionst::entry_point())!=
@@ -653,31 +623,20 @@ bool java_entry_point(
     symbol,
     symbol_table,
     message_handler,
-    assume_init_pointers_not_null,
     assert_uncaught_exceptions,
     object_factory_parameters,
-    pointer_type_selector);
+    pointer_type_selector,
+    build_arguments);
 }
 
-/// Generate a _start function for a specific function. See
-/// java_entry_point for more details.
-/// \param symbol: The symbol representing the function to call
-/// \param symbol_table: Global symbol table
-/// \param message_handler: Where to write output to
-/// \param assume_init_pointers_not_null: When creating pointers, assume they
-///   always take a non-null value.
-/// \param assert_uncaught_exceptions: Add an uncaught-exception check
-/// \param object_factory_parameters: Parameters for creation of arguments
-/// \param pointer_type_selector: Logic for substituting types of pointers
-/// \return true if error occurred on entry point search, false otherwise
 bool generate_java_start_function(
   const symbolt &symbol,
   symbol_table_baset &symbol_table,
   message_handlert &message_handler,
-  bool assume_init_pointers_not_null,
   bool assert_uncaught_exceptions,
   const java_object_factory_parameterst &object_factory_parameters,
-  const select_pointer_typet &pointer_type_selector)
+  const select_pointer_typet &pointer_type_selector,
+  const build_argumentst &build_arguments)
 {
   messaget message(message_handler);
   code_blockt init_code;
@@ -744,15 +703,10 @@ bool generate_java_start_function(
 
   // create code that allocates the objects used as test arguments and
   // non-deterministically initializes them
-  exprt::operandst main_arguments=
-    java_build_arguments(
-      symbol,
-      init_code,
-      symbol_table,
-      assume_init_pointers_not_null,
-      object_factory_parameters,
-      pointer_type_selector);
-  call_main.arguments()=main_arguments;
+  const std::pair<code_blockt, std::vector<exprt>> main_arguments =
+    build_arguments(symbol, symbol_table);
+  init_code.append(main_arguments.first);
+  call_main.arguments() = main_arguments.second;
 
   // Create target labels for the toplevel exception handler:
   code_labelt toplevel_catch("toplevel_catch", code_skipt());
@@ -791,8 +745,9 @@ bool generate_java_start_function(
   // Converge normal and exceptional return:
   init_code.add(std::move(after_catch));
 
-  // declare certain (which?) variables as test outputs
-  java_record_outputs(symbol, main_arguments, init_code, symbol_table);
+  // Mark return value, pointer type parameters and the exception as outputs.
+  init_code.append(
+    java_record_outputs(symbol, main_arguments.second, symbol_table));
 
   // add uncaught-exception check if requested
   if(assert_uncaught_exceptions)