Merge pull request #2670 from mgudemann/feature/multi_object_input_parameter

[TG-4331] Support multiple types for input parameters for entry point function

Author: Matthias Güdemann

jbmc/src/java_bytecode/Makefile

@@ -35,6 +35,7 @@ SRC = bytecode_info.cpp \
       java_utils.cpp \
       load_method_by_regex.cpp \
       mz_zip_archive.cpp \
+      nondet.cpp \
       remove_exceptions.cpp \
       remove_instanceof.cpp \
       remove_java_new.cpp \

jbmc/src/java_bytecode/java_entry_point.cpp

@@ -22,6 +22,8 @@ Author: Daniel Kroening, [email protected]
 #include "java_object_factory.h"
 #include "java_string_literals.h"
 #include "java_utils.h"
+#include "nondet.h"
+#include <util/fresh_symbol.h>
 
 #define JAVA_MAIN_METHOD "main:([Ljava/lang/String;)V"
 
@@ -317,17 +319,92 @@ exprt::operandst java_build_arguments(
 
     parameters.function_id = goto_functionst::entry_point();
 
-    // generate code to allocate and non-deterministicaly initialize the
-    // argument
-    main_arguments[param_number] = object_factory(
-      p.type(),
-      base_name,
-      init_code,
-      symbol_table,
-      parameters,
-      allocation_typet::LOCAL,
-      function.location,
-      pointer_type_selector);
+    namespacet ns(symbol_table);
+
+    // Generate code to allocate and non-deterministicaly initialize the
+    // argument, if the argument has different possible object types (e.g., from
+    // casts in the function body), then choose one in a non-deterministic way.
+    const auto alternatives =
+      pointer_type_selector.get_parameter_alternative_types(
+        function.name, p.get_identifier(), ns);
+    if(alternatives.empty())
+    {
+      main_arguments[param_number] = object_factory(
+        p.type(),
+        base_name,
+        init_code,
+        symbol_table,
+        parameters,
+        allocation_typet::LOCAL,
+        function.location,
+        pointer_type_selector);
+    }
+    else
+    {
+      INVARIANT(!is_this, "We cannot have different types for `this` here");
+      // create a non-deterministic switch between all possible values for the
+      // type of the parameter.
+      code_switcht code_switch;
+
+      // the idea is to get a new symbol for the parameter value `tmp`
+
+      // then add a non-deterministic switch over all possible input types,
+      // construct the object type at hand and assign to `tmp`
+
+      // switch(...)
+      // {
+      //   case obj1:
+      //     tmp_expr = object_factory(...)
+      //     param = tmp_expr
+      //     break
+      //   ...
+      // }
+      // method(..., param, ...)
+      //
+
+      const symbolt result_symbol = get_fresh_aux_symbol(
+        p.type(),
+        id2string(function.name),
+        "nondet_parameter_" + std::to_string(param_number),
+        function.location,
+        ID_java,
+        symbol_table);
+      main_arguments[param_number] = result_symbol.symbol_expr();
+
+      std::vector<codet> cases(alternatives.size());
+      const auto initialize_parameter = [&](const symbol_typet &type) {
+        code_blockt init_code_for_type;
+        exprt init_expr_for_parameter = object_factory(
+          java_reference_type(type),
+          id2string(base_name) + "_alternative_" +
+            id2string(type.get_identifier()),
+          init_code_for_type,
+          symbol_table,
+          parameters,
+          allocation_typet::DYNAMIC,
+          function.location,
+          pointer_type_selector);
+        init_code_for_type.add(
+          code_assignt(
+            result_symbol.symbol_expr(),
+            typecast_exprt(init_expr_for_parameter, p.type())));
+        return init_code_for_type;
+      };
+
+      std::transform(
+        alternatives.begin(),
+        alternatives.end(),
+        cases.begin(),
+        initialize_parameter);
+
+      init_code.add(
+        generate_nondet_switch(
+          id2string(function.name) + "_" + std::to_string(param_number),
+          cases,
+          java_int_type(),
+          function.location,
+          symbol_table));
+    }
 
     // record as an input
     codet input(ID_input);

jbmc/src/java_bytecode/nondet.cpp

@@ -0,0 +1,131 @@
+/*******************************************************************\
+
+Module: Non-deterministic object init and choice for JBMC
+
+ Author: Diffblue Ltd.
+
+\*******************************************************************/
+
+#include "nondet.h"
+
+#include <java_bytecode/java_types.h>
+#include <util/arith_tools.h>
+#include <util/c_types.h>
+#include <util/fresh_symbol.h>
+#include <util/symbol.h>
+
+/// Gets a fresh nondet choice in range (min_value, max_value). GOTO generated
+/// resembles:
+/// ```
+/// int_type name_prefix::nondet_int = NONDET(int_type)
+/// ASSUME(name_prefix::nondet_int >= min_value)
+/// ASSUME(name_prefix::nondet_int <= max_value)
+/// ```
+/// \param min_value: Minimum value (inclusive) of returned int.
+/// \param max_value: Maximum value (inclusive) of returned int.
+/// \param name_prefix: Prefix for the fresh symbol name generated.
+/// \param int_type: The type of the int used to non-deterministically choose
+///   one of the switch cases.
+/// \param source_location: The location to mark the generated int with.
+/// \param symbol_table: The global symbol table.
+/// \param instructions [out]: Output instructions are written to
+///   'instructions'. These declare, nondet-initialise and range-constrain (with
+///   assume statements) a fresh integer.
+/// \return Returns a symbol expression for the resulting integer.
+symbol_exprt generate_nondet_int(
+  const int64_t min_value,
+  const int64_t max_value,
+  const std::string &name_prefix,
+  const typet &int_type,
+  const source_locationt &source_location,
+  symbol_table_baset &symbol_table,
+  code_blockt &instructions)
+{
+  PRECONDITION(min_value < max_value);
+
+  // Declare a symbol for the non deterministic integer.
+  const symbol_exprt &nondet_symbol = get_fresh_aux_symbol(
+                                        int_type,
+                                        name_prefix,
+                                        "nondet_int",
+                                        source_location,
+                                        ID_java,
+                                        symbol_table)
+                                        .symbol_expr();
+  instructions.add(code_declt(nondet_symbol));
+
+  // Assign the symbol any non deterministic integer value.
+  //   int_type name_prefix::nondet_int = NONDET(int_type)
+  instructions.add(
+    code_assignt(nondet_symbol, side_effect_expr_nondett(int_type)));
+
+  // Constrain the non deterministic integer with a lower bound of `min_value`.
+  //   ASSUME(name_prefix::nondet_int >= min_value)
+  instructions.add(
+    code_assumet(
+      binary_predicate_exprt(
+        nondet_symbol, ID_ge, from_integer(min_value, int_type))));
+
+  // Constrain the non deterministic integer with an upper bound of `max_value`.
+  //   ASSUME(name_prefix::nondet_int <= max_value)
+  instructions.add(
+    code_assumet(
+      binary_predicate_exprt(
+        nondet_symbol, ID_le, from_integer(max_value, int_type))));
+
+  return nondet_symbol;
+}
+
+/// Pick nondeterministically between imperative actions 'switch_cases'.
+/// \param name_prefix: Name prefix for fresh symbols
+/// \param switch_cases: List of codet objects to execute in each switch case.
+/// \param int_type: The type of the int used to non-deterministically choose
+///   one of the switch cases.
+/// \param source_location: The location to mark the generated int with.
+/// \param symbol_table: The global symbol table.
+/// \return Returns a nondet-switch choosing between switch_cases. The resulting
+///   switch block has no default case.
+code_blockt generate_nondet_switch(
+  const irep_idt &name_prefix,
+  const alternate_casest &switch_cases,
+  const typet &int_type,
+  const source_locationt &source_location,
+  symbol_table_baset &symbol_table)
+{
+  PRECONDITION(!switch_cases.empty());
+
+  if(switch_cases.size() == 1)
+    return code_blockt({switch_cases[0]});
+
+  code_switcht result_switch;
+  code_blockt result_block;
+
+  const symbol_exprt &switch_value = generate_nondet_int(
+    0,
+    switch_cases.size() - 1,
+    id2string(name_prefix),
+    int_type,
+    source_location,
+    symbol_table,
+    result_block);
+
+  result_switch.value() = switch_value;
+
+  code_blockt switch_block;
+  int64_t case_number = 0;
+  for(const auto &switch_case : switch_cases)
+  {
+    code_blockt this_block;
+    this_block.add(switch_case);
+    this_block.add(code_breakt());
+    code_switch_caset this_case;
+    this_case.case_op() = from_integer(case_number, switch_value.type());
+    this_case.code() = this_block;
+    switch_block.move(this_case);
+    ++case_number;
+  }
+
+  result_switch.body() = switch_block;
+  result_block.move(result_switch);
+  return result_block;
+}

jbmc/src/java_bytecode/nondet.h

@@ -0,0 +1,34 @@
+/*******************************************************************\
+
+ Module: Non-deterministic object init and choice for JBMC
+
+ Author: Diffblue Ltd.
+
+\*******************************************************************/
+
+#ifndef CPROVER_JAVA_BYTECODE_NONDET_H
+#define CPROVER_JAVA_BYTECODE_NONDET_H
+
+#include <util/std_code.h>
+#include <util/std_expr.h>
+#include <util/symbol_table.h>
+
+symbol_exprt generate_nondet_int(
+  int64_t min_value,
+  int64_t max_value,
+  const std::string &name_prefix,
+  const typet &int_type,
+  const source_locationt &source_location,
+  symbol_table_baset &symbol_table,
+  code_blockt &instructions);
+
+typedef std::vector<codet> alternate_casest;
+
+code_blockt generate_nondet_switch(
+  const irep_idt &name_prefix,
+  const alternate_casest &switch_cases,
+  const typet &int_type,
+  const source_locationt &source_location,
+  symbol_table_baset &symbol_table);
+
+#endif // CPROVER_JAVA_BYTECODE_NONDET_H

jbmc/src/java_bytecode/select_pointer_type.cpp

@@ -223,3 +223,11 @@ select_pointer_typet::get_recursively_instantiated_type(
   visited.erase(parameter_name);
   return inst_val;
 }
+
+std::set<symbol_typet> select_pointer_typet::get_parameter_alternative_types(
+  const irep_idt &function_name,
+  const irep_idt &parameter_name,
+  const namespacet &ns) const
+{
+  return {};
+}

jbmc/src/java_bytecode/select_pointer_type.h

@@ -42,6 +42,11 @@ class select_pointer_typet
       &generic_parameter_specialization_map,
     const namespacet &ns) const;
 
+  virtual std::set<symbol_typet> get_parameter_alternative_types(
+    const irep_idt &function_name,
+    const irep_idt &parameter_name,
+    const namespacet &ns) const;
+
   pointer_typet specialize_generics(
     const pointer_typet &pointer_type,
     const generic_parameter_specialization_mapt