Merge pull request #2388 from peterschrammel/improve-jbmc-options

peterschrammel · web-flow · commit 3f255b2f3ec0 · 2018-07-09T18:53:32.000+01:00
Improve JBMC command line options
diff --git a/jbmc/regression/jbmc-strings/StringEquals/test_verify.desc b/jbmc/regression/jbmc-strings/StringEquals/test_verify.desc
@@ -1,6 +1,6 @@
 KNOWNBUG
 Test.class
---refine-strings --string-max-input-length 5 --string-max-length 100 --unwind 10 --function Test.verify --java-throw-runtime-exceptions
+--refine-strings --string-max-input-length 5 --string-max-length 100 --unwind 10 --function Test.verify --throw-runtime-exceptions
 ^EXIT=0$
 ^SIGNAL=0$
 assertion at file Test.java line 60 .* SUCCESS
diff --git a/jbmc/regression/jbmc-strings/StringLastIndexOf/test.desc b/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$
diff --git a/jbmc/regression/jbmc-strings/char_escape/test.desc b/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%\)
diff --git a/jbmc/regression/jbmc/ArithmeticException1/test.desc b/jbmc/regression/jbmc/ArithmeticException1/test.desc
@@ -1,6 +1,6 @@
 CORE
 ArithmeticExceptionTest.class
---java-throw-runtime-exceptions
+--throw-runtime-exceptions
 ^EXIT=10$
 ^SIGNAL=0$
 ^.*assertion at file ArithmeticExceptionTest.java line 8 function.*: FAILURE$
diff --git a/jbmc/regression/jbmc/ArithmeticException2/test.desc b/jbmc/regression/jbmc/ArithmeticException2/test.desc
@@ -1,6 +1,6 @@
 CORE
 ArithmeticExceptionTest.class
---java-throw-runtime-exceptions
+--throw-runtime-exceptions
 ^EXIT=10$
 ^SIGNAL=0$
 ^.*assertion at file ArithmeticExceptionTest.java line 9 function.*: FAILURE$
diff --git a/jbmc/regression/jbmc/ArithmeticException3/test.desc b/jbmc/regression/jbmc/ArithmeticException3/test.desc
@@ -1,6 +1,6 @@
 CORE
 ArithmeticExceptionTest.class
---java-throw-runtime-exceptions
+--throw-runtime-exceptions
 ^EXIT=10$
 ^SIGNAL=0$
 ^.*assertion at file ArithmeticExceptionTest.java line 8 function.*: FAILURE$
diff --git a/jbmc/regression/jbmc/ArithmeticException4/test.desc b/jbmc/regression/jbmc/ArithmeticException4/test.desc
@@ -1,6 +1,6 @@
 CORE
 ArithmeticExceptionTest.class
---java-throw-runtime-exceptions
+--throw-runtime-exceptions
 ^EXIT=10$
 ^SIGNAL=0$
 ^.*assertion at file ArithmeticExceptionTest.java line 9 function.*: FAILURE$
diff --git a/jbmc/regression/jbmc/ArithmeticException5/test.desc b/jbmc/regression/jbmc/ArithmeticException5/test.desc
@@ -1,6 +1,6 @@
 CORE
 ArithmeticExceptionTest.class
---java-throw-runtime-exceptions
+--throw-runtime-exceptions
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL
diff --git a/jbmc/regression/jbmc/ArithmeticException6/test.desc b/jbmc/regression/jbmc/ArithmeticException6/test.desc
@@ -1,6 +1,6 @@
 CORE
 ArithmeticExceptionTest.class
---java-throw-runtime-exceptions --function ArithmeticExceptionTest.main
+--throw-runtime-exceptions --function ArithmeticExceptionTest.main
 ^EXIT=10$
 ^SIGNAL=0$
 ^.*assertion at file ArithmeticExceptionTest.java line 7 function.*: FAILURE$
diff --git a/jbmc/regression/jbmc/ArithmeticException7/test.desc b/jbmc/regression/jbmc/ArithmeticException7/test.desc
@@ -1,6 +1,6 @@
 CORE
 ArithmeticExceptionTest.class
---java-throw-runtime-exceptions
+--throw-runtime-exceptions
 ^EXIT=10$
 ^SIGNAL=0$
 ^.*assertion at file ArithmeticExceptionTest.java line 8 function.*: FAILURE$
diff --git a/jbmc/regression/jbmc/ArrayIndexOutOfBoundsException1/test.desc b/jbmc/regression/jbmc/ArrayIndexOutOfBoundsException1/test.desc
@@ -1,6 +1,6 @@
 CORE
 ArrayIndexOutOfBoundsExceptionTest.class
---java-throw-runtime-exceptions
+--throw-runtime-exceptions
 ^EXIT=10$
 ^SIGNAL=0$
 ^.*assertion at file ArrayIndexOutOfBoundsExceptionTest.java line 8 function.*: FAILURE$
diff --git a/jbmc/regression/jbmc/ArrayIndexOutOfBoundsException2/test.desc b/jbmc/regression/jbmc/ArrayIndexOutOfBoundsException2/test.desc
@@ -1,6 +1,6 @@
 CORE
 ArrayIndexOutOfBoundsExceptionTest.class
---java-throw-runtime-exceptions
+--throw-runtime-exceptions
 ^EXIT=10$
 ^SIGNAL=0$
 ^.*assertion at file ArrayIndexOutOfBoundsExceptionTest.java line 8 function.*: FAILURE$
diff --git a/jbmc/regression/jbmc/ArrayIndexOutOfBoundsException3/test.desc b/jbmc/regression/jbmc/ArrayIndexOutOfBoundsException3/test.desc
@@ -1,6 +1,6 @@
 CORE
 ArrayIndexOutOfBoundsExceptionTest.class
---java-throw-runtime-exceptions
+--throw-runtime-exceptions
 ^EXIT=10$
 ^SIGNAL=0$
 ^.*assertion at file ArrayIndexOutOfBoundsExceptionTest.java line 8 function.*: FAILURE$
diff --git a/jbmc/regression/jbmc/ClassCastException1/test.desc b/jbmc/regression/jbmc/ClassCastException1/test.desc
@@ -1,6 +1,6 @@
 CORE
 ClassCastExceptionTest.class
---java-throw-runtime-exceptions
+--throw-runtime-exceptions
 ^EXIT=10$
 ^SIGNAL=0$
 ^.*assertion at file ClassCastExceptionTest.java line 8 function.*: FAILURE$
diff --git a/jbmc/regression/jbmc/ClassCastException2/test.desc b/jbmc/regression/jbmc/ClassCastException2/test.desc
@@ -1,6 +1,6 @@
 CORE
 ClassCastExceptionTest.class
---java-throw-runtime-exceptions
+--throw-runtime-exceptions
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/jbmc/regression/jbmc/ClassCastException3/test.desc b/jbmc/regression/jbmc/ClassCastException3/test.desc
@@ -1,6 +1,6 @@
 CORE
 ClassCastExceptionTest.class
---java-throw-runtime-exceptions
+--throw-runtime-exceptions
 ^EXIT=10$
 ^SIGNAL=0$
 ^.*assertion at file ClassCastExceptionTest.java line 12 function.*: FAILURE$
diff --git a/jbmc/regression/jbmc/NegativeArraySizeException1/test.desc b/jbmc/regression/jbmc/NegativeArraySizeException1/test.desc
@@ -1,6 +1,6 @@
 CORE
 NegativeArraySizeExceptionTest.class
---java-throw-runtime-exceptions
+--throw-runtime-exceptions
 ^EXIT=10$
 ^SIGNAL=0$
 ^.*assertion at file NegativeArraySizeExceptionTest.java line 7 function.*: FAILURE$
diff --git a/jbmc/regression/jbmc/NegativeArraySizeException2/test.desc b/jbmc/regression/jbmc/NegativeArraySizeException2/test.desc
@@ -1,6 +1,6 @@
 CORE
 NegativeArraySizeExceptionTest.class
---java-throw-runtime-exceptions
+--throw-runtime-exceptions
 ^EXIT=10$
 ^SIGNAL=0$
 ^.*assertion at file NegativeArraySizeExceptionTest.java line 7 function.*: FAILURE$
diff --git a/jbmc/regression/jbmc/NullPointerException2/test.desc b/jbmc/regression/jbmc/NullPointerException2/test.desc
@@ -1,6 +1,6 @@
 CORE
 Test.class
---java-throw-runtime-exceptions
+--throw-runtime-exceptions
 ^EXIT=10$
 ^SIGNAL=0$
 ^.*assertion at file Test.java line 14 function.*: FAILURE$
diff --git a/jbmc/regression/jbmc/NullPointerException3/test.desc b/jbmc/regression/jbmc/NullPointerException3/test.desc
@@ -1,6 +1,6 @@
 CORE
 Test.class
---java-throw-runtime-exceptions
+--throw-runtime-exceptions
 ^EXIT=10$
 ^SIGNAL=0$
 ^.*assertion at file Test.java line 14 function.*: FAILURE$
diff --git a/jbmc/regression/jbmc/NullPointerException4/test.desc b/jbmc/regression/jbmc/NullPointerException4/test.desc
@@ -1,6 +1,6 @@
 CORE
 Test.class
---java-throw-runtime-exceptions
+--throw-runtime-exceptions
 ^EXIT=10$
 ^SIGNAL=0$
 ^.*assertion at file Test.java line 12 function.*: FAILURE$
diff --git a/jbmc/regression/jbmc/annotations1/show_annotation_symbol.desc b/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
diff --git a/jbmc/regression/jbmc/cast_null2/test.desc b/jbmc/regression/jbmc/cast_null2/test.desc
@@ -1,6 +1,6 @@
 CORE
 test.class
---java-throw-runtime-exceptions --function test.main
+--throw-runtime-exceptions --function test.main
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/jbmc/regression/jbmc/coreModels/test.desc b/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$
diff --git a/jbmc/regression/jbmc/exceptions21/test.desc b/jbmc/regression/jbmc/exceptions21/test.desc
@@ -1,6 +1,6 @@
 CORE
 test.class
---function test.f --java-throw-runtime-exceptions
+--function test.f --throw-runtime-exceptions
 ^EXIT=0$
 ^SIGNAL=0$
 VERIFICATION SUCCESSFUL
diff --git a/jbmc/regression/jbmc/exceptions23/test.desc b/jbmc/regression/jbmc/exceptions23/test.desc
@@ -1,6 +1,6 @@
 CORE
 test.class
---java-throw-runtime-exceptions --function test.main
+--throw-runtime-exceptions --function test.main
 ^EXIT=10$
 ^SIGNAL=0$
 VERIFICATION FAILED
diff --git a/jbmc/regression/jbmc/exceptions24/test.desc b/jbmc/regression/jbmc/exceptions24/test.desc
@@ -1,6 +1,6 @@
 CORE
 test.class
---java-throw-runtime-exceptions --function test.main
+--throw-runtime-exceptions --function test.main
 ^EXIT=10$
 ^SIGNAL=0$
 VERIFICATION FAILED
diff --git a/jbmc/regression/jbmc/generic_class_bound1/test.desc b/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
diff --git a/jbmc/regression/jbmc/lambda2/test_no_crash.desc b/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
 --
diff --git a/jbmc/regression/jbmc/lazyloading_synthetic_method_cleanup1/check_clinit_normally_present.desc b/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$
diff --git a/jbmc/regression/jbmc/lazyloading_synthetic_method_cleanup2/check_clinit_normally_present.desc b/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>\(\)
diff --git a/jbmc/regression/jbmc/lazyloading_synthetic_method_cleanup3/check_clinit_normally_present.desc b/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$
diff --git a/jbmc/regression/jbmc/lvt-groovy/test.desc b/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$
 --
diff --git a/jbmc/regression/jbmc/no-main-int-array-maybe-null1/test.desc b/jbmc/regression/jbmc/no-main-int-array-maybe-null1/test.desc
@@ -1,6 +1,6 @@
 CORE
 Main.class
---function Main.main --java-throw-runtime-exceptions
+--function Main.main --throw-runtime-exceptions
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
diff --git a/jbmc/regression/jbmc/package_friendly1/test.desc b/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$
diff --git a/jbmc/regression/jbmc/provide_object_implementation/test.desc b/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$
diff --git a/jbmc/regression/strings-smoke-tests/java_append_string/test_substring.desc b/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$
diff --git a/jbmc/src/java_bytecode/java_bytecode_language.cpp b/jbmc/src/java_bytecode/java_bytecode_language.cpp
@@ -45,32 +45,54 @@ Author: Daniel Kroening, kroening@kroening.com
 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");
-  throw_runtime_exceptions=cmd.isset("java-throw-runtime-exceptions");
+  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");
 
-  if(cmd.isset("java-max-input-array-length"))
-    object_factory_parameters.max_nondet_array_length=
+  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("java-max-input-tree-depth"))
-    object_factory_parameters.max_nondet_tree_depth=
+  }
+  if(cmd.isset("max-nondet-array-length"))
+  {
+    object_factory_parameters.max_nondet_array_length =
+      safe_string2size_t(cmd.get_value("max-nondet-array-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("string-max-input-length"))
-    object_factory_parameters.max_nondet_string_length=
+  }
+  if(cmd.isset("max-nondet-tree-depth"))
+  {
+    object_factory_parameters.max_nondet_tree_depth =
+      safe_string2size_t(cmd.get_value("max-nondet-tree-depth"));
+  }
+
+  if(cmd.isset("string-max-input-length")) // will go away
+  {
+    object_factory_parameters.max_nondet_string_length =
       safe_string2size_t(cmd.get_value("string-max-input-length"));
-  else if(cmd.isset("string-max-length"))
+  }
+  if(cmd.isset("max-nondet-string-length"))
+  {
     object_factory_parameters.max_nondet_string_length =
-      safe_string2size_t(cmd.get_value("string-max-length"));
+      safe_string2size_t(cmd.get_value("max-nondet-string-length"));
+  }
 
   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"))
     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;
diff --git a/jbmc/src/java_bytecode/java_bytecode_language.h b/jbmc/src/java_bytecode/java_bytecode_language.h
diff --git a/jbmc/src/jbmc/jbmc_parse_options.cpp b/jbmc/src/jbmc/jbmc_parse_options.cpp
diff --git a/jbmc/src/jbmc/jbmc_parse_options.h b/jbmc/src/jbmc/jbmc_parse_options.h
diff --git a/jbmc/src/jdiff/jdiff_parse_options.cpp b/jbmc/src/jdiff/jdiff_parse_options.cpp
diff --git a/jbmc/src/jdiff/jdiff_parse_options.h b/jbmc/src/jdiff/jdiff_parse_options.h
diff --git a/jbmc/unit/java-testing-utils/load_java_class.cpp b/jbmc/unit/java-testing-utils/load_java_class.cpp
