Set language options

Author: peterschrammel

jbmc/src/janalyzer/janalyzer_parse_options.cpp

@@ -77,6 +77,8 @@ void janalyzer_parse_optionst::get_command_line_options(optionst &options)
     exit(CPROVER_EXIT_USAGE_ERROR);
   }
 
+  parse_java_language_options(cmdline, options);
+
   // check assertions
   if(cmdline.isset("no-assertions"))
     options.set_option("assertions", false);
@@ -350,7 +352,7 @@ int janalyzer_parse_optionst::doit()
 
   try
   {
-    goto_model = initialize_goto_model(cmdline, get_message_handler());
+    goto_model = initialize_goto_model(cmdline, get_message_handler(), options);
   }
 
   catch(const char *e)

jbmc/src/java_bytecode/Makefile

@@ -35,6 +35,7 @@ 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/java_bytecode_language.cpp

@@ -10,14 +10,16 @@ Author: Daniel Kroening, [email protected]
 
 #include <string>
 
-#include <util/symbol_table.h>
-#include <util/suffix.h>
-#include <util/config.h>
 #include <util/cmdline.h>
+#include <util/config.h>
 #include <util/expr_iterator.h>
+#include <util/invariant.h>
 #include <util/journalling_symbol_table.h>
+#include <util/options.h>
 #include <util/string2int.h>
-#include <util/invariant.h>
+#include <util/suffix.h>
+#include <util/symbol_table.h>
+
 #include <json/json_parser.h>
 
 #include <goto-programs/class_hierarchy.h>
@@ -39,97 +41,108 @@ Author: Daniel Kroening, [email protected]
 #include "expr2java.h"
 #include "load_method_by_regex.h"
 
-/// Consume options that are java bytecode specific.
-/// \param Command:line options
-/// \return None
-void java_bytecode_languaget::get_language_options(const cmdlinet &cmd)
+/// Parse options that are java bytecode specific.
+/// \param cmd Command line
+/// \param [out] options The options object that will be updated.
+void parse_java_language_options(const cmdlinet &cmd, optionst &options)
 {
-  assume_inputs_non_null=cmd.isset("java-assume-inputs-non-null");
-  string_refinement_enabled = !cmd.isset("no-refine-strings");
-  throw_runtime_exceptions =
-    cmd.isset("java-throw-runtime-exceptions") || // will go away
-    cmd.isset("throw-runtime-exceptions");
-  assert_uncaught_exceptions = !cmd.isset("disable-uncaught-exception-check");
-  throw_assertion_error = cmd.isset("throw-assertion-error");
-  threading_support = cmd.isset("java-threading");
+  options.set_option(
+    "java-assume-inputs-non-null", cmd.isset("java-assume-inputs-non-null"));
+  options.set_option(
+    "throw-runtime-exceptions", cmd.isset("throw-runtime-exceptions"));
+  options.set_option(
+    "uncaught-exception-check", !cmd.isset("disable-uncaught-exception-check"));
+  options.set_option(
+    "throw-assertion-error", cmd.isset("throw-assertion-error"));
+  options.set_option("java-threading", cmd.isset("java-threading"));
 
-  if(cmd.isset("java-max-input-array-length")) // will go away
-  {
-    object_factory_parameters.max_nondet_array_length =
-      safe_string2size_t(cmd.get_value("java-max-input-array-length"));
-  }
-  if(cmd.isset("max-nondet-array-length"))
+  if(cmd.isset("java-max-vla-length"))
   {
-    object_factory_parameters.max_nondet_array_length =
-      safe_string2size_t(cmd.get_value("max-nondet-array-length"));
+    options.set_option(
+      "java-max-vla-length", cmd.get_value("java-max-vla-length"));
   }
 
-  if(cmd.isset("java-max-input-tree-depth")) // will go away
-  {
-    object_factory_parameters.max_nondet_tree_depth =
-      safe_string2size_t(cmd.get_value("java-max-input-tree-depth"));
-  }
-  if(cmd.isset("max-nondet-tree-depth"))
+  options.set_option(
+    "symex-driven-lazy-loading", cmd.isset("symex-driven-lazy-loading"));
+
+  if(cmd.isset("java-load-class"))
+    options.set_option("java-load-class", cmd.get_values("java-load-class"));
+
+  if(cmd.isset("java-no-load-class"))
   {
-    object_factory_parameters.max_nondet_tree_depth =
-      safe_string2size_t(cmd.get_value("max-nondet-tree-depth"));
+    options.set_option(
+      "java-no-load-class", cmd.get_values("java-no-load-class"));
   }
-
-  if(cmd.isset("string-max-input-length")) // will go away
+  if(cmd.isset("lazy-methods-extra-entry-point"))
   {
-    object_factory_parameters.max_nondet_string_length =
-      safe_string2size_t(cmd.get_value("string-max-input-length"));
+    options.set_option(
+      "lazy-methods-extra-entry-point",
+      cmd.get_values("lazy-methods-extra-entry-point"));
   }
-  if(cmd.isset("max-nondet-string-length"))
+  if(cmd.isset("java-cp-include-files"))
   {
-    object_factory_parameters.max_nondet_string_length =
-      safe_string2size_t(cmd.get_value("max-nondet-string-length"));
+    options.set_option(
+      "java-cp-include-files", cmd.get_value("java-cp-include-files"));
   }
+}
 
-  object_factory_parameters.string_printable = cmd.isset("string-printable");
-  if(cmd.isset("java-max-vla-length"))
-    max_user_array_length =
-      safe_string2size_t(cmd.get_value("java-max-vla-length"));
-  if(cmd.isset("symex-driven-lazy-loading"))
+/// Consume options that are java bytecode specific.
+void java_bytecode_languaget::set_language_options(const optionst &options)
+{
+  object_factory_parameters.set(options);
+
+  assume_inputs_non_null =
+    options.get_bool_option("java-assume-inputs-non-null");
+  string_refinement_enabled = options.get_bool_option("refine-strings");
+  throw_runtime_exceptions =
+    options.get_bool_option("throw-runtime-exceptions");
+  assert_uncaught_exceptions =
+    options.get_bool_option("uncaught-exception-check");
+  throw_assertion_error = options.get_bool_option("throw-assertion-error");
+  threading_support = options.get_bool_option("java-threading");
+  max_user_array_length =
+    options.get_unsigned_int_option("java-max-vla-length");
+
+  if(options.get_bool_option("symex-driven-lazy-loading"))
     lazy_methods_mode=LAZY_METHODS_MODE_EXTERNAL_DRIVER;
-  else if(!cmd.isset("no-lazy-methods"))
+  else if(options.get_bool_option("lazy-methods"))
     lazy_methods_mode=LAZY_METHODS_MODE_CONTEXT_INSENSITIVE;
   else
     lazy_methods_mode=LAZY_METHODS_MODE_EAGER;
 
   if(throw_runtime_exceptions)
   {
     java_load_classes.insert(
-        java_load_classes.end(),
-        exception_needed_classes.begin(),
-        exception_needed_classes.end());
+      java_load_classes.end(),
+      exception_needed_classes.begin(),
+      exception_needed_classes.end());
   }
-  if(cmd.isset("java-load-class"))
+
+  if(options.is_set("java-load-class"))
   {
-    const auto &values = cmd.get_values("java-load-class");
+    const auto &load_values = options.get_list_option("java-load-class");
     java_load_classes.insert(
-        java_load_classes.end(), values.begin(), values.end());
+      java_load_classes.end(), load_values.begin(), load_values.end());
   }
-  if(cmd.isset("java-no-load-class"))
+  if(options.is_set("java-no-load-class"))
   {
-    const auto &values = cmd.get_values("java-no-load-class");
-    no_load_classes = {values.begin(), values.end()};
+    const auto &no_load_values = options.get_list_option("java-no-load-class");
+    no_load_classes = {no_load_values.begin(), no_load_values.end()};
   }
-
-  const std::list<std::string> &extra_entry_points=
-    cmd.get_values("lazy-methods-extra-entry-point");
+  const std::list<std::string> &extra_entry_points =
+    options.get_list_option("lazy-methods-extra-entry-point");
   std::transform(
     extra_entry_points.begin(),
     extra_entry_points.end(),
     std::back_inserter(extra_methods),
     build_load_method_by_regex);
-  const auto &new_points = build_extra_entry_points(cmd);
+  const auto &new_points = build_extra_entry_points(options);
   extra_methods.insert(
     extra_methods.end(), new_points.begin(), new_points.end());
 
-  if(cmd.isset("java-cp-include-files"))
+  java_cp_include_files = options.get_option("java-cp-include-files");
+  if(!java_cp_include_files.empty())
   {
-    java_cp_include_files=cmd.get_value("java-cp-include-files");
     // load file list from JSON file
     if(java_cp_include_files[0]=='@')
     {
@@ -144,7 +157,7 @@ void java_bytecode_languaget::get_language_options(const cmdlinet &cmd)
         throw "the JSON file has a wrong format";
       jsont include_files=json_cp_config["jar"];
       if(!include_files.is_array())
-         throw "the JSON file has a wrong format";
+        throw "the JSON file has a wrong format";
 
       // add jars from JSON config file to classpath
       for(const jsont &file_entry : include_files.array)
@@ -160,7 +173,7 @@ void java_bytecode_languaget::get_language_options(const cmdlinet &cmd)
   else
     java_cp_include_files=".*";
 
-  nondet_static = cmd.isset("nondet-static");
+  nondet_static = options.get_bool_option("nondet-static");
 
   language_options_initialized=true;
 }
@@ -1216,8 +1229,7 @@ java_bytecode_languaget::~java_bytecode_languaget()
 /// specifying extra entry points. To provide a regex entry point, the command
 /// line option `--lazy-methods-extra-entry-point` can be used directly.
 std::vector<load_extra_methodst>
-java_bytecode_languaget::build_extra_entry_points(
-  const cmdlinet &command_line) const
+java_bytecode_languaget::build_extra_entry_points(const optionst &options) const
 {
   return {};
 }

jbmc/src/java_bytecode/java_bytecode_language.h

@@ -92,7 +92,7 @@ enum lazy_methods_modet
 class java_bytecode_languaget:public languaget
 {
 public:
-  virtual void get_language_options(const cmdlinet &) override;
+  virtual void set_language_options(const optionst &) override;
 
   virtual bool preprocess(
     std::istream &instream,
@@ -200,7 +200,7 @@ class java_bytecode_languaget:public languaget
 
 private:
   virtual std::vector<load_extra_methodst>
-  build_extra_entry_points(const cmdlinet &command_line) const;
+  build_extra_entry_points(const optionst &) const;
   const std::unique_ptr<const select_pointer_typet> pointer_type_selector;
 
   /// Maps synthetic method names on to the particular type of synthetic method
@@ -217,4 +217,6 @@ class java_bytecode_languaget:public languaget
 
 std::unique_ptr<languaget> new_java_bytecode_language();
 
+void parse_java_language_options(const cmdlinet &cmd, optionst &options);
+
 #endif // CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_LANGUAGE_H

jbmc/src/java_bytecode/java_class_loader_limit.cpp

@@ -13,6 +13,8 @@ Author: Daniel Kroening, [email protected]
 
 #include <json/json_parser.h>
 
+#include <util/invariant.h>
+
 /// Initializes class with either regex matcher or match set. If the string
 /// starts with an `@` it is treated as a path to a JSON file. Otherwise, it is
 /// treated as a regex.
@@ -48,8 +50,9 @@ Author: Daniel Kroening, [email protected]
 void java_class_loader_limitt::setup_class_load_limit(
   const std::string &java_cp_include_files)
 {
-  if(java_cp_include_files.empty())
-    throw "class regexp cannot be empty, `get_language_options` not called?";
+  PRECONDITION(
+    !java_cp_include_files.empty(),
+    "class regexp cannot be empty, `set_language_options` not called?");
 
   // '@' signals file reading with list of class files to load
   use_regex_match = java_cp_include_files[0] != '@';

jbmc/src/java_bytecode/object_factory_parameters.h

@@ -14,6 +14,9 @@ Author: Daniel Kroening, [email protected]
 
 #include <util/irep.h>
 
+class cmdlinet;
+class optionst;
+
 #define MAX_NONDET_ARRAY_LENGTH_DEFAULT 5
 #define MAX_NONDET_STRING_LENGTH \
   static_cast<std::size_t>(std::numeric_limits<std::int32_t>::max())
@@ -23,18 +26,18 @@ Author: Daniel Kroening, [email protected]
 struct object_factory_parameterst final
 {
   /// Maximum value for the non-deterministically-chosen length of an array.
-  size_t max_nondet_array_length=MAX_NONDET_ARRAY_LENGTH_DEFAULT;
+  size_t max_nondet_array_length = MAX_NONDET_ARRAY_LENGTH_DEFAULT;
 
   /// Maximum value for the non-deterministically-chosen length of a string.
-  size_t max_nondet_string_length=MAX_NONDET_STRING_LENGTH;
+  size_t max_nondet_string_length = MAX_NONDET_STRING_LENGTH;
 
   /// Maximum depth for object hierarchy on input.
   /// Used to prevent object factory to loop infinitely during the
   /// generation of code that allocates/initializes data structures of recursive
   /// data types or unbounded depth. We bound the maximum number of times we
   /// dereference a pointer using a 'depth counter'. We set a pointer to null if
   /// such depth becomes >= than this maximum value.
-  size_t max_nondet_tree_depth=MAX_NONDET_TREE_DEPTH;
+  size_t max_nondet_tree_depth = MAX_NONDET_TREE_DEPTH;
 
   /// To force a certain depth of non-null objects.
   /// The default is that objects are 'maybe null' up to the nondet tree depth.
@@ -53,6 +56,11 @@ struct object_factory_parameterst final
 
   /// Function id, used as a prefix for identifiers of temporaries
   irep_idt function_id;
+
+  /// Assigns the parameters from given options
+  void set(const optionst &);
 };
 
+void parse_object_factory_options(const cmdlinet &, optionst &);
+
 #endif