Make --lazy-methods and --refine-strings default

These options are always required in practical
use cases. They can be disabled with --no-lazy-methods
and --no-refine-strings if needed for regression tests.

Author: peterschrammel

jbmc/regression/jbmc-strings/StringLastIndexOf/test.desc

@@ -1,6 +1,6 @@
 CORE
 Test.class
---function Test.check --refine-strings --string-max-length 100
+--function Test.check --refine-strings --string-max-input-length 100
 ^EXIT=10$
 ^SIGNAL=0$
 assertion at file Test.java line 11 .* SUCCESS$

jbmc/regression/jbmc-strings/char_escape/test.desc

@@ -3,4 +3,4 @@ Test.class
 --refine-strings --function Test.test --cover location --trace --json-ui
 ^EXIT=0$
 ^SIGNAL=0$
-20 of 23 covered \(87.0%\)|30 of 44 covered \(68.2%\)
+20 of 22 covered \(90.9%\)|30 of 44 covered \(68.2%\)

jbmc/regression/jbmc/annotations1/show_annotation_symbol.desc

@@ -1,6 +1,6 @@
 CORE
 annotations.class
---verbosity 10 --show-symbol-table --function annotations.main
+--no-lazy-methods --verbosity 10 --show-symbol-table --function annotations.main
 ^EXIT=0$
 ^SIGNAL=0$
 ^Type\.\.\.\.\.\.\.\.: @java::ClassAnnotation struct annotations

jbmc/regression/jbmc/coreModels/test.desc

@@ -1,6 +1,6 @@
 CORE
 test.class
---show-symbol-table --cp ../../../src/java_bytecode/library/core-models.jar:.
+--no-lazy-methods --no-refine-strings --show-symbol-table --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
 ^EXIT=0$
 ^SIGNAL=0$
 ^Symbol\s*\.*\: java\:\:org\.cprover\.CProver\.\<init\>\:\(\)V$

jbmc/regression/jbmc/generic_class_bound1/test.desc

@@ -1,6 +1,6 @@
 CORE symex-driven-lazy-loading-expected-failure
 Gn.class
---cover location
+--cover location --no-lazy-methods --no-refine-strings
 ^EXIT=0$
 ^SIGNAL=0$
 .*file Gn.java line 6 function java::Gn.\<init\>:\(\)V bytecode-index 1 block .: FAILED

jbmc/regression/jbmc/lambda2/test_no_crash.desc

@@ -1,6 +1,6 @@
 CORE symex-driven-lazy-loading-expected-failure
 SymStream.class
---verbosity 10 --show-goto-functions
+--no-lazy-methods --verbosity 10 --show-goto-functions
 ^EXIT=0
 ^SIGNAL=0
 --

jbmc/regression/jbmc/lazyloading_synthetic_method_cleanup1/check_clinit_normally_present.desc

@@ -1,6 +1,6 @@
 CORE symex-driven-lazy-loading-expected-failure
 Test.class
---show-goto-functions --function Test.main
+--no-lazy-methods --show-goto-functions --function Test.main
 java::Unused::clinit_wrapper
 Unused\.<clinit>\(\)
 ^EXIT=0$

jbmc/regression/jbmc/lazyloading_synthetic_method_cleanup2/check_clinit_normally_present.desc

@@ -1,6 +1,6 @@
 CORE symex-driven-lazy-loading-expected-failure
 Test.class
---show-goto-functions --function Test.main
+--no-lazy-methods --show-goto-functions --function Test.main
 java::Unused1::clinit_wrapper
 java::Unused2::clinit_wrapper
 Unused2\.<clinit>\(\)

jbmc/regression/jbmc/lazyloading_synthetic_method_cleanup3/check_clinit_normally_present.desc

@@ -1,6 +1,6 @@
 CORE symex-driven-lazy-loading-expected-failure
 Test.class
---show-goto-functions --function Test.main
+--no-lazy-methods --show-goto-functions --function Test.main
 java::Opaque\.<clinit>:\(\)V
 java::Opaque::clinit_wrapper
 ^EXIT=0$

jbmc/regression/jbmc/lvt-groovy/test.desc

@@ -1,6 +1,6 @@
 CORE symex-driven-lazy-loading-expected-failure
 DetectSplitPackagesTask.class
---show-symbol-table
+--show-symbol-table --no-lazy-methods --no-refine-strings
 ^EXIT=0$
 ^SIGNAL=0$
 --

jbmc/regression/jbmc/package_friendly1/test.desc

@@ -1,6 +1,6 @@
 CORE symex-driven-lazy-loading-expected-failure
 main.class
---java-load-class package_friendly1 --java-load-class package_friendly2 --show-goto-functions
+--no-lazy-methods --java-load-class package_friendly1 --java-load-class package_friendly2 --show-goto-functions
 ^main[.]main[\(].*[\)].*$
 ^package_friendly2[.]operation2[\(][\)].*$
 ^EXIT=0$

jbmc/regression/jbmc/provide_object_implementation/test.desc

@@ -1,6 +1,6 @@
 CORE symex-driven-lazy-loading-expected-failure
 java/lang/Object.class
-
+--no-lazy-methods
 ^EXIT=6$
 ^SIGNAL=0$
 ^the program has no entry point$

jbmc/regression/strings-smoke-tests/java_append_string/test_substring.desc

@@ -1,6 +1,6 @@
 CORE
 test_append_string.class
---refine-strings  --string-max-length 10 --function test_append_string.check --java-assume-inputs-non-null
+--refine-strings  --string-max-input-length 10 --function test_append_string.check --java-assume-inputs-non-null
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion.*\].* line 22.* SUCCESS$

jbmc/src/java_bytecode/java_bytecode_language.cpp

@@ -45,7 +45,7 @@ Author: Daniel Kroening, [email protected]
 void java_bytecode_languaget::get_language_options(const cmdlinet &cmd)
 {
   assume_inputs_non_null=cmd.isset("java-assume-inputs-non-null");
-  string_refinement_enabled=cmd.isset("refine-strings");
+  string_refinement_enabled = !cmd.isset("no-refine-strings");
   throw_runtime_exceptions=cmd.isset("java-throw-runtime-exceptions");
   assert_uncaught_exceptions = !cmd.isset("disable-uncaught-exception-check");
   throw_assertion_error = cmd.isset("throw-assertion-error");
@@ -70,7 +70,7 @@ void java_bytecode_languaget::get_language_options(const cmdlinet &cmd)
       safe_string2size_t(cmd.get_value("java-max-vla-length"));
   if(cmd.isset("symex-driven-lazy-loading"))
     lazy_methods_mode=LAZY_METHODS_MODE_EXTERNAL_DRIVER;
-  else if(cmd.isset("lazy-methods"))
+  else if(!cmd.isset("no-lazy-methods"))
     lazy_methods_mode=LAZY_METHODS_MODE_CONTEXT_INSENSITIVE;
   else
     lazy_methods_mode=LAZY_METHODS_MODE_EAGER;

jbmc/src/java_bytecode/java_bytecode_language.h

@@ -36,7 +36,8 @@ Author: Daniel Kroening, [email protected]
   "(java-max-input-tree-depth):" \
   "(java-max-vla-length):" \
   "(java-cp-include-files):" \
-  "(lazy-methods)" \
+  "(lazy-methods)"                 /* will go away */ \
+  "(no-lazy-methods)" \
   "(lazy-methods-extra-entry-point):" \
   "(java-load-class):" \
   "(java-no-load-class):"
@@ -55,10 +56,12 @@ Author: Daniel Kroening, [email protected]
   "                                  the object\n"                                               /* NOLINT(*) */ \
   " --java-max-vla-length            limit the length of user-code-created arrays\n"             /* NOLINT(*) */ \
   " --java-cp-include-files          regexp or JSON list of files to load (with '@' prefix)\n"   /* NOLINT(*) */ \
-  " --lazy-methods                   only translate methods that appear to be reachable from\n"  /* NOLINT(*) */ \
-  "                                  the --function entry point or main class\n"                 /* NOLINT(*) */ \
+  " --no-lazy-methods                load and translate all methods given on the command line\n" /* NOLINT(*) */ \
+  "                                  and in --classpath\n"                                       /* NOLINT(*) */ \
+  "                                  Default is to load methods that appear to be\n"  /* NOLINT(*) */ \
+  "                                  reachable from the --function entry point or main class\n"       /* NOLINT(*) */ \
   "                                  Note --show-symbol-table/goto-functions/properties output\n"/* NOLINT(*) */ \
-  "                                  will be restricted to loaded methods in this case\n"        /* NOLINT(*) */ \
+  "                                  are restricted to loaded methods by default\n"        /* NOLINT(*) */ \
   " --lazy-methods-extra-entry-point METHODNAME\n"                                               /* NOLINT(*) */ \
   "                                  treat METHODNAME as a possible program entry point for\n"   /* NOLINT(*) */ \
   "                                  the purpose of lazy method loading\n"                       /* NOLINT(*) */ \

jbmc/src/jbmc/jbmc_parse_options.cpp

@@ -242,7 +242,7 @@ void jbmc_parse_optionst::get_command_line_options(optionst &options)
     options.set_option("refine-arithmetic", true);
   }
 
-  if(cmdline.isset("refine-strings"))
+  if(!cmdline.isset("no-refine-strings"))
   {
     options.set_option("refine-strings", true);
     options.set_option("string-printable", cmdline.isset("string-printable"));
@@ -1140,7 +1140,7 @@ void jbmc_parse_optionst::help()
     " --yices                      use Yices\n"
     " --z3                         use Z3\n"
     " --refine                     use refinement procedure (experimental)\n"
-    " --refine-strings             use string refinement (experimental)\n"
+    " --no-refine-strings          turn off string refinement\n"
     " --string-printable           add constraint that strings are printable (experimental)\n" // NOLINT(*)
     " --string-max-length          add constraint on the length of strings\n" // NOLINT(*)
     " --string-max-input-length    add constraint on the length of input strings\n" // NOLINT(*)

jbmc/src/jbmc/jbmc_parse_options.h

@@ -55,7 +55,8 @@ class optionst;
   "(no-sat-preprocessor)" \
   "(beautify)" \
   "(dimacs)(refine)(max-node-refinement):(refine-arrays)(refine-arithmetic)"\
-  "(refine-strings)" \
+  "(refine-strings)" /* will go away */ \
+  "(no-refine-strings)" \
   "(string-printable)" \
   "(string-max-length):" \
   "(string-max-input-length):" \

jbmc/src/jdiff/jdiff_parse_options.cpp

@@ -88,6 +88,12 @@ void jdiff_parse_optionst::get_command_line_options(optionst &options)
     exit(1);
   }
 
+  // TODO: improve this when language front ends have been
+  //   disentangled from command line parsing
+  // we always require these options
+  cmdline.set("no-lazy-methods");
+  cmdline.set("no-refine-strings");
+
   if(cmdline.isset("cover"))
     parse_cover_options(cmdline, options);
 

jbmc/src/jdiff/jdiff_parse_options.h

@@ -35,6 +35,8 @@ class optionst;
   OPT_GOTO_CHECK \
   "(cover):" \
   "(verbosity):(version)" \
+  "(no-lazy-methods)" /* should go away */ \
+  "(no-refine-strings)" /* should go away */ \
   OPT_TIMESTAMP \
   "u(unified)(change-impact)(forward-impact)(backward-impact)" \
   "(compact-output)"

jbmc/unit/java-testing-utils/load_java_class.cpp

@@ -38,17 +38,10 @@ symbol_tablet load_java_class_lazy(
   const std::string &class_path,
   const std::string &main)
 {
-  free_form_cmdlinet lazy_command_line;
-  lazy_command_line.add_flag("lazy-methods");
-
   register_language(new_java_bytecode_language);
 
   return load_java_class(
-    java_class_name,
-    class_path,
-    main,
-    get_language_from_mode(ID_java),
-    lazy_command_line);
+    java_class_name, class_path, main, get_language_from_mode(ID_java));
 }
 
 /// Go through the process of loading, type-checking and finalising loading a
@@ -65,10 +58,18 @@ symbol_tablet load_java_class(
   const std::string &class_path,
   const std::string &main)
 {
+  free_form_cmdlinet command_line;
+  command_line.add_flag("no-lazy-methods");
+  command_line.add_flag("no-refine-strings");
+
   register_language(new_java_bytecode_language);
 
   return load_java_class(
-    java_class_name, class_path, main, get_language_from_mode(ID_java));
+    java_class_name,
+    class_path,
+    main,
+    get_language_from_mode(ID_java),
+    command_line);
 }
 
 /// Go through the process of loading, type-checking and finalising loading a
@@ -161,7 +162,9 @@ symbol_tablet load_java_class(
   const std::string &main,
   std::unique_ptr<languaget> &&java_lang)
 {
-  cmdlinet command_line;
+  free_form_cmdlinet command_line;
+  command_line.add_flag("no-lazy-methods");
+  command_line.add_flag("no-refine-strings");
   // TODO(tkiley): This doesn't do anything as "java-cp-include-files" is an
   // TODO(tkiley): unknown argument. This could be changed by using the
   // TODO(tkiley): free_form_cmdlinet however this causes some tests to fail.