Merge pull request #3251 from danpoe/feature/nondet-init-structs

Recursive nondet init of pointers to structs [blocks: #3443]

Author: danpoe

jbmc/src/java_bytecode/Makefile

@@ -26,6 +26,7 @@ SRC = bytecode_info.cpp \
       java_entry_point.cpp \
       java_local_variable_table.cpp \
       java_object_factory.cpp \
+      java_object_factory_parameters.cpp \
       java_pointer_casts.cpp \
       java_qualifiers.cpp \
       java_root_class.cpp \
@@ -35,7 +36,6 @@ SRC = bytecode_info.cpp \
       java_types.cpp \
       java_utils.cpp \
       load_method_by_regex.cpp \
-      object_factory_parameters.cpp \
       mz_zip_archive.cpp \
       remove_exceptions.cpp \
       remove_instanceof.cpp \

jbmc/src/java_bytecode/convert_java_nondet.cpp

@@ -44,7 +44,7 @@ static goto_programt get_gen_nondet_init_instructions(
   const source_locationt &source_loc,
   symbol_table_baset &symbol_table,
   message_handlert &message_handler,
-  const object_factory_parameterst &object_factory_parameters,
+  const java_object_factory_parameterst &object_factory_parameters,
   const irep_idt &mode)
 {
   code_blockt gen_nondet_init_code;
@@ -82,7 +82,7 @@ static std::pair<goto_programt::targett, bool> insert_nondet_init_code(
   const goto_programt::targett &target,
   symbol_table_baset &symbol_table,
   message_handlert &message_handler,
-  object_factory_parameterst object_factory_parameters,
+  java_object_factory_parameterst object_factory_parameters,
   const irep_idt &mode)
 {
   const auto next_instr = std::next(target);
@@ -172,7 +172,7 @@ void convert_nondet(
   goto_programt &goto_program,
   symbol_table_baset &symbol_table,
   message_handlert &message_handler,
-  const object_factory_parameterst &object_factory_parameters,
+  const java_object_factory_parameterst &object_factory_parameters,
   const irep_idt &mode)
 {
   bool changed = false;
@@ -200,10 +200,10 @@ void convert_nondet(
 void convert_nondet(
   goto_model_functiont &function,
   message_handlert &message_handler,
-  const object_factory_parameterst &object_factory_parameters,
+  const java_object_factory_parameterst &object_factory_parameters,
   const irep_idt &mode)
 {
-  object_factory_parameterst parameters = object_factory_parameters;
+  java_object_factory_parameterst parameters = object_factory_parameters;
   parameters.function_id = function.get_function_id();
   convert_nondet(
     function.get_goto_function().body,
@@ -219,7 +219,7 @@ void convert_nondet(
   goto_functionst &goto_functions,
   symbol_table_baset &symbol_table,
   message_handlert &message_handler,
-  const object_factory_parameterst &object_factory_parameters)
+  const java_object_factory_parameterst &object_factory_parameters)
 {
   const namespacet ns(symbol_table);
 
@@ -229,7 +229,7 @@ void convert_nondet(
 
     if(symbol.mode==ID_java)
     {
-      object_factory_parameterst parameters = object_factory_parameters;
+      java_object_factory_parameterst parameters = object_factory_parameters;
       parameters.function_id = f_it.first;
       convert_nondet(
         f_it.second.body,
@@ -248,7 +248,7 @@ void convert_nondet(
 void convert_nondet(
   goto_modelt &goto_model,
   message_handlert &message_handler,
-  const object_factory_parameterst& object_factory_parameters)
+  const java_object_factory_parameterst &object_factory_parameters)
 {
   convert_nondet(
     goto_model.goto_functions,

jbmc/src/java_bytecode/convert_java_nondet.h

@@ -20,7 +20,7 @@ class symbol_table_baset;
 class goto_modelt;
 class goto_model_functiont;
 class message_handlert;
-struct object_factory_parameterst;
+struct java_object_factory_parameterst;
 
 /// Converts side_effect_exprt_nondett expressions using java_object_factory.
 /// For example, NONDET(SomeClass *) may become a nondet choice between a null
@@ -40,12 +40,12 @@ void convert_nondet(
   goto_functionst &goto_functions,
   symbol_table_baset &symbol_table,
   message_handlert &message_handler,
-  const object_factory_parameterst &object_factory_parameters);
+  const java_object_factory_parameterst &object_factory_parameters);
 
 void convert_nondet(
   goto_modelt &,
   message_handlert &,
-  const object_factory_parameterst &object_factory_parameters);
+  const java_object_factory_parameterst &object_factory_parameters);
 
 /// Converts side_effect_exprt_nondett expressions using java_object_factory.
 /// For example, NONDET(SomeClass *) may become a nondet choice between a null
@@ -64,7 +64,7 @@ void convert_nondet(
 void convert_nondet(
   goto_model_functiont &function,
   message_handlert &message_handler,
-  const object_factory_parameterst &object_factory_parameters,
+  const java_object_factory_parameterst &object_factory_parameters,
   const irep_idt &mode);
 
 #endif // CPROVER_JAVA_BYTECODE_CONVERT_NONDET_H

jbmc/src/java_bytecode/java_bytecode_language.h

@@ -13,9 +13,9 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "ci_lazy_methods.h"
 #include "ci_lazy_methods_needed.h"
 #include "java_class_loader.h"
+#include "java_object_factory_parameters.h"
 #include "java_static_initializers.h"
 #include "java_string_library_preprocess.h"
-#include "object_factory_parameters.h"
 #include "select_pointer_type.h"
 #include "synthetic_methods_map.h"
 
@@ -179,7 +179,7 @@ class java_bytecode_languaget:public languaget
   java_class_loadert java_class_loader;
   bool threading_support;
   bool assume_inputs_non_null;      // assume inputs variables to be non-null
-  object_factory_parameterst object_factory_parameters;
+  java_object_factory_parameterst object_factory_parameters;
   size_t max_user_array_length;     // max size for user code created arrays
   method_bytecodet method_bytecode;
   lazy_methods_modet lazy_methods_mode;

jbmc/src/java_bytecode/java_entry_point.cpp

@@ -122,7 +122,7 @@ static void java_static_lifetime_init(
   symbol_table_baset &symbol_table,
   const source_locationt &source_location,
   bool assume_init_pointers_not_null,
-  object_factory_parameterst object_factory_parameters,
+  java_object_factory_parameterst object_factory_parameters,
   const select_pointer_typet &pointer_type_selector,
   bool string_refinement_enabled,
   message_handlert &message_handler)
@@ -218,7 +218,7 @@ static void java_static_lifetime_init(
                                     is_non_null_library_global(sym.name) ||
                                     assume_init_pointers_not_null;
 
-        object_factory_parameterst parameters = object_factory_parameters;
+        java_object_factory_parameterst parameters = object_factory_parameters;
         if(not_allow_null && !is_class_model)
           parameters.min_null_tree_depth = 1;
 
@@ -278,7 +278,7 @@ exprt::operandst java_build_arguments(
   code_blockt &init_code,
   symbol_table_baset &symbol_table,
   bool assume_init_pointers_not_null,
-  object_factory_parameterst object_factory_parameters,
+  java_object_factory_parameterst object_factory_parameters,
   const select_pointer_typet &pointer_type_selector)
 {
   const java_method_typet::parameterst &parameters =
@@ -307,7 +307,7 @@ exprt::operandst java_build_arguments(
     // be null
     bool is_this=(param_number==0) && parameters[param_number].get_this();
 
-    object_factory_parameterst parameters = object_factory_parameters;
+    java_object_factory_parameterst parameters = object_factory_parameters;
     // only pointer must be non-null
     if(assume_init_pointers_not_null || is_this)
       parameters.min_null_tree_depth = 1;
@@ -598,7 +598,7 @@ bool java_entry_point(
   message_handlert &message_handler,
   bool assume_init_pointers_not_null,
   bool assert_uncaught_exceptions,
-  const object_factory_parameterst &object_factory_parameters,
+  const java_object_factory_parameterst &object_factory_parameters,
   const select_pointer_typet &pointer_type_selector,
   bool string_refinement_enabled)
 {
@@ -654,7 +654,7 @@ bool generate_java_start_function(
   message_handlert &message_handler,
   bool assume_init_pointers_not_null,
   bool assert_uncaught_exceptions,
-  const object_factory_parameterst &object_factory_parameters,
+  const java_object_factory_parameterst &object_factory_parameters,
   const select_pointer_typet &pointer_type_selector)
 {
   messaget message(message_handler);

jbmc/src/java_bytecode/java_entry_point.h

@@ -25,7 +25,7 @@ bool java_entry_point(
   class message_handlert &message_handler,
   bool assume_init_pointers_not_null,
   bool assert_uncaught_exceptions,
-  const object_factory_parameterst &object_factory_parameters,
+  const java_object_factory_parameterst &object_factory_parameters,
   const select_pointer_typet &pointer_type_selector,
   bool string_refinement_enabled);
 
@@ -76,7 +76,7 @@ bool generate_java_start_function(
   class message_handlert &message_handler,
   bool assume_init_pointers_not_null,
   bool assert_uncaught_exceptions,
-  const object_factory_parameterst &object_factory_parameters,
+  const java_object_factory_parameterst &object_factory_parameters,
   const select_pointer_typet &pointer_type_selector);
 
 #endif // CPROVER_JAVA_BYTECODE_JAVA_ENTRY_POINT_H

jbmc/src/java_bytecode/java_object_factory.cpp

@@ -30,7 +30,7 @@ class java_object_factoryt
   /// methods in this class.
   const source_locationt &loc;
 
-  const object_factory_parameterst object_factory_parameters;
+  const java_object_factory_parameterst object_factory_parameters;
 
   /// This is employed in conjunction with the depth above. Every time the
   /// non-det generator visits a type, the type is added to this set. We forbid
@@ -83,7 +83,7 @@ class java_object_factoryt
   java_object_factoryt(
     std::vector<const symbolt *> &_symbols_created,
     const source_locationt &loc,
-    const object_factory_parameterst _object_factory_parameters,
+    const java_object_factory_parameterst _object_factory_parameters,
     symbol_table_baset &_symbol_table,
     const select_pointer_typet &pointer_type_selector)
     : symbols_created(_symbols_created),
@@ -1212,7 +1212,7 @@ void java_object_factoryt::gen_nondet_init(
   {
     // types different from pointer or structure:
     // bool, int, float, byte, char, ...
-    exprt rhs = type.id() == ID_c_bool ? get_nondet_bool(type)
+    exprt rhs = type.id() == ID_c_bool ? get_nondet_bool(type, loc)
                                        : side_effect_expr_nondett(type, loc);
     code_assignt assign(expr, rhs);
     assign.add_source_location()=loc;
@@ -1536,7 +1536,7 @@ exprt object_factory(
   const irep_idt base_name,
   code_blockt &init_code,
   symbol_table_baset &symbol_table,
-  object_factory_parameterst parameters,
+  java_object_factory_parameterst parameters,
   allocation_typet alloc_type,
   const source_locationt &loc,
   const select_pointer_typet &pointer_type_selector)
@@ -1629,7 +1629,7 @@ void gen_nondet_init(
   const source_locationt &loc,
   bool skip_classid,
   allocation_typet alloc_type,
-  const object_factory_parameterst &object_factory_parameters,
+  const java_object_factory_parameterst &object_factory_parameters,
   const select_pointer_typet &pointer_type_selector,
   update_in_placet update_in_place)
 {
@@ -1666,7 +1666,7 @@ exprt object_factory(
   const irep_idt base_name,
   code_blockt &init_code,
   symbol_tablet &symbol_table,
-  const object_factory_parameterst &object_factory_parameters,
+  const java_object_factory_parameterst &object_factory_parameters,
   allocation_typet alloc_type,
   const source_locationt &location)
 {
@@ -1690,7 +1690,7 @@ void gen_nondet_init(
   const source_locationt &loc,
   bool skip_classid,
   allocation_typet alloc_type,
-  const object_factory_parameterst &object_factory_parameters,
+  const java_object_factory_parameterst &object_factory_parameters,
   update_in_placet update_in_place)
 {
   select_pointer_typet pointer_type_selector;

jbmc/src/java_bytecode/java_object_factory.h

@@ -94,7 +94,7 @@ exprt object_factory(
   const irep_idt base_name,
   code_blockt &init_code,
   symbol_table_baset &symbol_table,
-  object_factory_parameterst parameters,
+  java_object_factory_parameterst parameters,
   allocation_typet alloc_type,
   const source_locationt &location,
   const select_pointer_typet &pointer_type_selector);
@@ -104,7 +104,7 @@ exprt object_factory(
   const irep_idt base_name,
   code_blockt &init_code,
   symbol_tablet &symbol_table,
-  const object_factory_parameterst &object_factory_parameters,
+  const java_object_factory_parameterst &object_factory_parameters,
   allocation_typet alloc_type,
   const source_locationt &location);
 
@@ -122,7 +122,7 @@ void gen_nondet_init(
   const source_locationt &loc,
   bool skip_classid,
   allocation_typet alloc_type,
-  const object_factory_parameterst &object_factory_parameters,
+  const java_object_factory_parameterst &object_factory_parameters,
   const select_pointer_typet &pointer_type_selector,
   update_in_placet update_in_place);
 
@@ -133,7 +133,7 @@ void gen_nondet_init(
   const source_locationt &loc,
   bool skip_classid,
   allocation_typet alloc_type,
-  const object_factory_parameterst &object_factory_parameters,
+  const java_object_factory_parameterst &object_factory_parameters,
   update_in_placet update_in_place);
 
 exprt allocate_dynamic_object(

jbmc/src/java_bytecode/java_object_factory_parameters.cpp

@@ -0,0 +1,16 @@
+/*******************************************************************\
+
+Module:
+
+Author: Daniel Poetzl
+
+\*******************************************************************/
+
+#include "java_object_factory_parameters.h"
+
+void parse_java_object_factory_options(
+  const cmdlinet &cmdline,
+  optionst &options)
+{
+  parse_object_factory_options(cmdline, options);
+}

jbmc/src/java_bytecode/java_object_factory_parameters.h

@@ -0,0 +1,33 @@
+/*******************************************************************\
+
+Module:
+
+Author: Daniel Poetzl
+
+\*******************************************************************/
+
+#ifndef CPROVER_JAVA_BYTECODE_JAVA_OBJECT_FACTORY_PARAMETERS_H
+#define CPROVER_JAVA_BYTECODE_JAVA_OBJECT_FACTORY_PARAMETERS_H
+
+#include <util/object_factory_parameters.h>
+
+struct java_object_factory_parameterst final : public object_factory_parameterst
+{
+  java_object_factory_parameterst()
+  {
+  }
+
+  explicit java_object_factory_parameterst(const optionst &options)
+    : object_factory_parameterst(options)
+  {
+  }
+};
+
+/// Parse the java object factory parameters from a given command line
+/// \param cmdline Command line
+/// \param [out] options The options object that will be updated
+void parse_java_object_factory_options(
+  const cmdlinet &cmdline,
+  optionst &options);
+
+#endif