From 39bc7ea72ee5896a5c1a627f79adc7ac6d089886 Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Tue, 30 Jan 2018 23:11:15 +0000 Subject: [PATCH 1/3] 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. --- .../jbmc-strings/StringLastIndexOf/test.desc | 2 +- .../jbmc-strings/char_escape/test.desc | 2 +- .../annotations1/show_annotation_symbol.desc | 2 +- jbmc/regression/jbmc/coreModels/test.desc | 2 +- .../jbmc/generic_class_bound1/test.desc | 2 +- .../jbmc/lambda2/test_no_crash.desc | 2 +- .../check_clinit_normally_present.desc | 2 +- .../check_clinit_normally_present.desc | 2 +- .../check_clinit_normally_present.desc | 2 +- jbmc/regression/jbmc/lvt-groovy/test.desc | 2 +- .../jbmc/package_friendly1/test.desc | 2 +- .../provide_object_implementation/test.desc | 2 +- .../java_append_string/test_substring.desc | 2 +- .../java_bytecode/java_bytecode_language.cpp | 4 ++-- .../java_bytecode/java_bytecode_language.h | 11 +++++---- jbmc/src/jbmc/jbmc_parse_options.cpp | 4 ++-- jbmc/src/jbmc/jbmc_parse_options.h | 3 ++- jbmc/src/jdiff/jdiff_parse_options.cpp | 6 +++++ jbmc/src/jdiff/jdiff_parse_options.h | 2 ++ .../java-testing-utils/load_java_class.cpp | 23 +++++++++++-------- 20 files changed, 47 insertions(+), 32 deletions(-) diff --git a/jbmc/regression/jbmc-strings/StringLastIndexOf/test.desc b/jbmc/regression/jbmc-strings/StringLastIndexOf/test.desc index 4f1852669c0..2e18576f085 100644 --- 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 index 53ab05408c9..fea3171d5b6 100644 --- 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/annotations1/show_annotation_symbol.desc b/jbmc/regression/jbmc/annotations1/show_annotation_symbol.desc index 0735ec2d46d..320f8ac345a 100644 --- 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/coreModels/test.desc b/jbmc/regression/jbmc/coreModels/test.desc index 4bda1b0ed61..9390687e25c 100644 --- 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\.\\:\(\)V$ diff --git a/jbmc/regression/jbmc/generic_class_bound1/test.desc b/jbmc/regression/jbmc/generic_class_bound1/test.desc index d4d425ec194..6f623851472 100644 --- 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.\:\(\)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 index f05242bf10d..0a2a94c84a3 100644 --- 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 index 56fb8f416a6..300b49f25b6 100644 --- 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\.\(\) ^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 index 3bb1dc48487..46ace60fa73 100644 --- 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\.\(\) 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 index a52f8d6cd60..2c0d3865f1e 100644 --- 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\.:\(\)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 index 6f8c52c05ca..d78a7de8454 100644 --- 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/package_friendly1/test.desc b/jbmc/regression/jbmc/package_friendly1/test.desc index e3250bd8d47..efd3f766756 100644 --- 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 index 381ae109d1e..ff8518e73f9 100644 --- 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 index dfddb22d72b..a6272d26347 100644 --- 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 index 76d5b0d839c..6f051e971ee 100644 --- a/jbmc/src/java_bytecode/java_bytecode_language.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_language.cpp @@ -45,7 +45,7 @@ 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"); + 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; diff --git a/jbmc/src/java_bytecode/java_bytecode_language.h b/jbmc/src/java_bytecode/java_bytecode_language.h index 8c3ca46d77a..f900ac2c52d 100644 --- a/jbmc/src/java_bytecode/java_bytecode_language.h +++ b/jbmc/src/java_bytecode/java_bytecode_language.h @@ -36,7 +36,8 @@ Author: Daniel Kroening, kroening@kroening.com "(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, kroening@kroening.com " 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(*) */ \ diff --git a/jbmc/src/jbmc/jbmc_parse_options.cpp b/jbmc/src/jbmc/jbmc_parse_options.cpp index 7d04c553b96..481b181b818 100644 --- a/jbmc/src/jbmc/jbmc_parse_options.cpp +++ b/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(*) diff --git a/jbmc/src/jbmc/jbmc_parse_options.h b/jbmc/src/jbmc/jbmc_parse_options.h index 616b1d1b9d9..177c4f92b57 100644 --- a/jbmc/src/jbmc/jbmc_parse_options.h +++ b/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):" \ diff --git a/jbmc/src/jdiff/jdiff_parse_options.cpp b/jbmc/src/jdiff/jdiff_parse_options.cpp index 877aef28c1b..f22a5d722c5 100644 --- a/jbmc/src/jdiff/jdiff_parse_options.cpp +++ b/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); diff --git a/jbmc/src/jdiff/jdiff_parse_options.h b/jbmc/src/jdiff/jdiff_parse_options.h index b23af102930..e562e55a833 100644 --- a/jbmc/src/jdiff/jdiff_parse_options.h +++ b/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)" diff --git a/jbmc/unit/java-testing-utils/load_java_class.cpp b/jbmc/unit/java-testing-utils/load_java_class.cpp index 29d303a1605..82cab0fd0a0 100644 --- a/jbmc/unit/java-testing-utils/load_java_class.cpp +++ b/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 &&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. From 548baea93463d493a3bfe63f30a5bb6328d6c0ff Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Wed, 31 Jan 2018 16:59:55 +0000 Subject: [PATCH 2/3] Improve naming of command line options Drops the 'java' prefix from the most important java command line options. The prefix is not required anymore since JBMC and CBMC do not share the same command line interface anymore. --- .../java_bytecode/java_bytecode_language.cpp | 36 ++++++++++++++----- .../java_bytecode/java_bytecode_language.h | 12 ++++--- jbmc/src/jbmc/jbmc_parse_options.cpp | 2 +- jbmc/src/jbmc/jbmc_parse_options.h | 3 +- 4 files changed, 38 insertions(+), 15 deletions(-) diff --git a/jbmc/src/java_bytecode/java_bytecode_language.cpp b/jbmc/src/java_bytecode/java_bytecode_language.cpp index 6f051e971ee..8518e40ace8 100644 --- a/jbmc/src/java_bytecode/java_bytecode_language.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_language.cpp @@ -51,18 +51,38 @@ void java_bytecode_languaget::get_language_options(const cmdlinet &cmd) 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")) diff --git a/jbmc/src/java_bytecode/java_bytecode_language.h b/jbmc/src/java_bytecode/java_bytecode_language.h index f900ac2c52d..67c45630e1e 100644 --- a/jbmc/src/java_bytecode/java_bytecode_language.h +++ b/jbmc/src/java_bytecode/java_bytecode_language.h @@ -32,8 +32,10 @@ Author: Daniel Kroening, kroening@kroening.com "(throw-assertion-error)" \ "(java-assume-inputs-non-null)" \ "(java-throw-runtime-exceptions)" \ - "(java-max-input-array-length):" \ - "(java-max-input-tree-depth):" \ + "(java-max-input-array-length):" /* will go away */ \ + "(max-nondet-array-length):" \ + "(java-max-input-tree-depth):" /* will go away */ \ + "(max-nondet-tree-depth):" \ "(java-max-vla-length):" \ "(java-cp-include-files):" \ "(lazy-methods)" /* will go away */ \ @@ -51,9 +53,9 @@ Author: Daniel Kroening, kroening@kroening.com " --java-assume-inputs-non-null never initialize reference-typed parameter to the\n" /* NOLINT(*) */ \ " entry point with null\n" /* NOLINT(*) */ \ " --java-throw-runtime-exceptions make implicit runtime exceptions explicit\n" /* NOLINT(*) */ \ - " --java-max-input-array-length N limit input array size to <= N\n" /* NOLINT(*) */ \ - " --java-max-input-tree-depth N object references are (deterministically) set to null in\n" /* NOLINT(*) */ \ - " the object\n" /* NOLINT(*) */ \ + " --max-nondet-array-length N limit nondet (e.g. input) array size to <= N\n" /* NOLINT(*) */ \ + " --max-nondet-tree-depth N limit size of nondet (e.g. input) object tree;\n" /* NOLINT(*) */ \ + " at level N references are set to null\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(*) */ \ " --no-lazy-methods load and translate all methods given on the command line\n" /* NOLINT(*) */ \ diff --git a/jbmc/src/jbmc/jbmc_parse_options.cpp b/jbmc/src/jbmc/jbmc_parse_options.cpp index 481b181b818..0283c9346f6 100644 --- a/jbmc/src/jbmc/jbmc_parse_options.cpp +++ b/jbmc/src/jbmc/jbmc_parse_options.cpp @@ -1143,7 +1143,7 @@ void jbmc_parse_optionst::help() " --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(*) + " --max-nondet-string-length bound the length of nondet (e.g. input) strings\n" // NOLINT(*) " --outfile filename output formula to given file\n" " --arrays-uf-never never turn arrays into uninterpreted functions\n" // NOLINT(*) " --arrays-uf-always always turn arrays into uninterpreted functions\n" // NOLINT(*) diff --git a/jbmc/src/jbmc/jbmc_parse_options.h b/jbmc/src/jbmc/jbmc_parse_options.h index 177c4f92b57..9f5da915be3 100644 --- a/jbmc/src/jbmc/jbmc_parse_options.h +++ b/jbmc/src/jbmc/jbmc_parse_options.h @@ -59,7 +59,8 @@ class optionst; "(no-refine-strings)" \ "(string-printable)" \ "(string-max-length):" \ - "(string-max-input-length):" \ + "(string-max-input-length):" /* will go away */ \ + "(max-nondet-string-length):" \ "(16)(32)(64)(LP64)(ILP64)(LLP64)(ILP32)(LP32)" \ OPT_SHOW_GOTO_FUNCTIONS \ OPT_SHOW_CLASS_HIERARCHY \ From 0a10bf372d961bc3db72942adf2657f611616ce6 Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Thu, 21 Jun 2018 21:55:41 +0100 Subject: [PATCH 3/3] Drop java prefix from throw-runtime-exceptions option The 'java' prefix is not required anymore since JBMC and CBMC do not share the same command line interface anymore. --- jbmc/regression/jbmc-strings/StringEquals/test_verify.desc | 2 +- jbmc/regression/jbmc/ArithmeticException1/test.desc | 2 +- jbmc/regression/jbmc/ArithmeticException2/test.desc | 2 +- jbmc/regression/jbmc/ArithmeticException3/test.desc | 2 +- jbmc/regression/jbmc/ArithmeticException4/test.desc | 2 +- jbmc/regression/jbmc/ArithmeticException5/test.desc | 2 +- jbmc/regression/jbmc/ArithmeticException6/test.desc | 2 +- jbmc/regression/jbmc/ArithmeticException7/test.desc | 2 +- .../jbmc/ArrayIndexOutOfBoundsException1/test.desc | 2 +- .../jbmc/ArrayIndexOutOfBoundsException2/test.desc | 2 +- .../jbmc/ArrayIndexOutOfBoundsException3/test.desc | 2 +- jbmc/regression/jbmc/ClassCastException1/test.desc | 2 +- jbmc/regression/jbmc/ClassCastException2/test.desc | 2 +- jbmc/regression/jbmc/ClassCastException3/test.desc | 2 +- jbmc/regression/jbmc/NegativeArraySizeException1/test.desc | 2 +- jbmc/regression/jbmc/NegativeArraySizeException2/test.desc | 2 +- jbmc/regression/jbmc/NullPointerException2/test.desc | 2 +- jbmc/regression/jbmc/NullPointerException3/test.desc | 2 +- jbmc/regression/jbmc/NullPointerException4/test.desc | 2 +- jbmc/regression/jbmc/cast_null2/test.desc | 2 +- jbmc/regression/jbmc/exceptions21/test.desc | 2 +- jbmc/regression/jbmc/exceptions23/test.desc | 2 +- jbmc/regression/jbmc/exceptions24/test.desc | 2 +- jbmc/regression/jbmc/no-main-int-array-maybe-null1/test.desc | 2 +- jbmc/src/java_bytecode/java_bytecode_language.cpp | 4 +++- jbmc/src/java_bytecode/java_bytecode_language.h | 5 +++-- 26 files changed, 30 insertions(+), 27 deletions(-) diff --git a/jbmc/regression/jbmc-strings/StringEquals/test_verify.desc b/jbmc/regression/jbmc-strings/StringEquals/test_verify.desc index f13e27ac930..01bf846bfdc 100644 --- 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/ArithmeticException1/test.desc b/jbmc/regression/jbmc/ArithmeticException1/test.desc index e8f7c941fd4..0339ff4f6d5 100644 --- 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 index 00820d86c6e..510065d60f0 100644 --- 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 index e8f7c941fd4..0339ff4f6d5 100644 --- 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 index 00820d86c6e..510065d60f0 100644 --- 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 index d57ec32a9a9..508682718d6 100644 --- 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 index 8cd09de8d51..17a0f6b4323 100644 --- 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 index e8f7c941fd4..0339ff4f6d5 100644 --- 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 index e6216e07c79..2904f44355d 100644 --- 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 index e6216e07c79..2904f44355d 100644 --- 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 index e6216e07c79..2904f44355d 100644 --- 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 index fa84bf185ab..9dd470b881c 100644 --- 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 index c593280efe5..e9be3a9d818 100644 --- 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 index e2188d63898..e6ba629de3a 100644 --- 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 index a203a79a628..3c7006827de 100644 --- 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 index a203a79a628..3c7006827de 100644 --- 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 index e4ad2c5739d..94828524b2f 100644 --- 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 index e4ad2c5739d..94828524b2f 100644 --- 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 index 800755d16bb..8ec1d555381 100644 --- 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/cast_null2/test.desc b/jbmc/regression/jbmc/cast_null2/test.desc index b71b059cd5a..5cce3d56aa5 100644 --- 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/exceptions21/test.desc b/jbmc/regression/jbmc/exceptions21/test.desc index 24040e046e4..ee88ed7a0a2 100644 --- 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 index c99eef557dd..69bf18ce113 100644 --- 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 index a58943b5d28..403750992f2 100644 --- 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/no-main-int-array-maybe-null1/test.desc b/jbmc/regression/jbmc/no-main-int-array-maybe-null1/test.desc index 57b29af8ed2..fa4cca3f657 100644 --- 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/src/java_bytecode/java_bytecode_language.cpp b/jbmc/src/java_bytecode/java_bytecode_language.cpp index 8518e40ace8..663eab78563 100644 --- a/jbmc/src/java_bytecode/java_bytecode_language.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_language.cpp @@ -46,7 +46,9 @@ 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("no-refine-strings"); - throw_runtime_exceptions=cmd.isset("java-throw-runtime-exceptions"); + 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"); diff --git a/jbmc/src/java_bytecode/java_bytecode_language.h b/jbmc/src/java_bytecode/java_bytecode_language.h index 67c45630e1e..9a742b37099 100644 --- a/jbmc/src/java_bytecode/java_bytecode_language.h +++ b/jbmc/src/java_bytecode/java_bytecode_language.h @@ -31,7 +31,8 @@ Author: Daniel Kroening, kroening@kroening.com "(disable-uncaught-exception-check)" \ "(throw-assertion-error)" \ "(java-assume-inputs-non-null)" \ - "(java-throw-runtime-exceptions)" \ + "(java-throw-runtime-exceptions)" /* will go away */ \ + "(throw-runtime-exceptions)" \ "(java-max-input-array-length):" /* will go away */ \ "(max-nondet-array-length):" \ "(java-max-input-tree-depth):" /* will go away */ \ @@ -52,7 +53,7 @@ Author: Daniel Kroening, kroening@kroening.com " at the location of the assert statement\n" /* NOLINT(*) */ \ " --java-assume-inputs-non-null never initialize reference-typed parameter to the\n" /* NOLINT(*) */ \ " entry point with null\n" /* NOLINT(*) */ \ - " --java-throw-runtime-exceptions make implicit runtime exceptions explicit\n" /* NOLINT(*) */ \ + " --throw-runtime-exceptions make implicit runtime exceptions explicit\n" /* NOLINT(*) */ \ " --max-nondet-array-length N limit nondet (e.g. input) array size to <= N\n" /* NOLINT(*) */ \ " --max-nondet-tree-depth N limit size of nondet (e.g. input) object tree;\n" /* NOLINT(*) */ \ " at level N references are set to null\n" /* NOLINT(*) */ \