From 08861320aeeebcb270245049838479d3aba56e28 Mon Sep 17 00:00:00 2001 From: Joel Allred Date: Mon, 30 Jul 2018 17:06:03 +0100 Subject: [PATCH 1/2] Add replace_all string utility Utility to search and replace strings inside a string. --- src/util/string_utils.cpp | 13 +++++++++++++ src/util/string_utils.h | 2 ++ 2 files changed, 15 insertions(+) diff --git a/src/util/string_utils.cpp b/src/util/string_utils.cpp index dc889684205..95cab42bbb8 100644 --- a/src/util/string_utils.cpp +++ b/src/util/string_utils.cpp @@ -148,3 +148,16 @@ std::string escape(const std::string &s) return result; } + +void replace_all( + std::string &str, + const std::string &from, + const std::string &to) +{ + size_t start_pos = 0; + while((start_pos = str.find(from, start_pos)) != std::string::npos) + { + str.replace(start_pos, from.length(), to); + start_pos += to.length(); + } +} diff --git a/src/util/string_utils.h b/src/util/string_utils.h index dbd7e634a52..17936ede3de 100644 --- a/src/util/string_utils.h +++ b/src/util/string_utils.h @@ -67,4 +67,6 @@ Stream &join_strings( /// programming language. std::string escape(const std::string &); +void replace_all(std::string &, const std::string &, const std::string &); + #endif From caed4f914842ea41af8d610b1ac9767a4a0829d4 Mon Sep 17 00:00:00 2001 From: Joel Allred Date: Mon, 30 Jul 2018 17:10:24 +0100 Subject: [PATCH 2/2] Add --java-load-containing-class-only option Add option to only load the class (and inner classes) that contain the method under test. --- .../load-containing-class-only/External.class | Bin 0 -> 504 bytes .../load-containing-class-only/External.java | 8 ++++ .../load-containing-class-only/Test.class | Bin 0 -> 270 bytes .../jbmc/load-containing-class-only/Test.java | 7 ++++ .../jbmc/load-containing-class-only/test.desc | 10 +++++ .../java_bytecode/java_bytecode_language.cpp | 38 +++++++++++++++--- .../java_bytecode/java_bytecode_language.h | 3 ++ .../java_bytecode/java_class_loader_limit.cpp | 9 ++++- 8 files changed, 68 insertions(+), 7 deletions(-) create mode 100644 jbmc/regression/jbmc/load-containing-class-only/External.class create mode 100644 jbmc/regression/jbmc/load-containing-class-only/External.java create mode 100644 jbmc/regression/jbmc/load-containing-class-only/Test.class create mode 100644 jbmc/regression/jbmc/load-containing-class-only/Test.java create mode 100644 jbmc/regression/jbmc/load-containing-class-only/test.desc diff --git a/jbmc/regression/jbmc/load-containing-class-only/External.class b/jbmc/regression/jbmc/load-containing-class-only/External.class new file mode 100644 index 0000000000000000000000000000000000000000..0937ccb2dc46bcfa1f34ac2078b61ddaf943c728 GIT binary patch literal 504 zcmYLF%TB^j6r9rsg;L&#_`tYufi7f2ToI!|OiX+%Feb7q?F}i`V%lQ-7Jk5u8#R$c z6W#k!#?uP2xaXeCnVB>9e*e6G0%&4GhlX+rDwZ@+ykIi3^l6Xg2#6+vl_Y(dDKI-WQm-}Z%n8IgHB5MfL@A!NFtY2BQe zce7ctWw|pKy*nEFmN<4IO{Vh@3g0u`-JyAJ8qkq8kVJ}5jev%0dV|K{JXpu~M?N7r z7im~Cu#OrbzhGbVhr;3@xdqgA`E7)XEds|E_P-y8497g+hxM?@U!(C?QN9`_;7;bl zfj}_0tMN^It28iy=KcF8a z-pSG#=HA13G5@FIAAo0ED@a@^^brOa1Q-gmU$Qc@GXekZ{#8KE_irQ+uCtOhhxeGO z$ixLR(o$_3*GfR`_J=B=W#$xZ>Y6J1^q89uqtQY;z(`{Z#i^)C4V*MBOqou%aZU*r zbrzqNs?rqPnUcjVeEyp|9zQODK)~pRw{XnE55zYEj`DP}!(G0Lx3f+f4v@d_zAl`S JwH|XG^cm%?DYpOs literal 0 HcmV?d00001 diff --git a/jbmc/regression/jbmc/load-containing-class-only/Test.java b/jbmc/regression/jbmc/load-containing-class-only/Test.java new file mode 100644 index 00000000000..2e584ae9b2d --- /dev/null +++ b/jbmc/regression/jbmc/load-containing-class-only/Test.java @@ -0,0 +1,7 @@ +class Test { + + public static int test() { + return External.get(); + } + +} diff --git a/jbmc/regression/jbmc/load-containing-class-only/test.desc b/jbmc/regression/jbmc/load-containing-class-only/test.desc new file mode 100644 index 00000000000..191446f062e --- /dev/null +++ b/jbmc/regression/jbmc/load-containing-class-only/test.desc @@ -0,0 +1,10 @@ +CORE +Test.class +--function Test.test --load-containing-class-only +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring +-- +Check that External.class is not loaded when using --load-containing-class-only diff --git a/jbmc/src/java_bytecode/java_bytecode_language.cpp b/jbmc/src/java_bytecode/java_bytecode_language.cpp index 663eab78563..4d8014d746e 100644 --- a/jbmc/src/java_bytecode/java_bytecode_language.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_language.cpp @@ -10,15 +10,16 @@ Author: Daniel Kroening, kroening@kroening.com #include -#include -#include -#include +#include #include +#include #include +#include #include #include -#include -#include +#include +#include +#include #include @@ -124,7 +125,32 @@ void java_bytecode_languaget::get_language_options(const cmdlinet &cmd) std::back_inserter(extra_methods), build_load_method_by_regex); - if(cmd.isset("java-cp-include-files")) + if(cmd.isset("load-containing-class-only")) + { + const std::string function_to_analyse = cmd.get_value("function"); + const std::size_t first_dollar_index = + function_to_analyse.find_first_of('$'); + const std::size_t last_dot_index = function_to_analyse.find_last_of('.'); + std::string class_name = function_to_analyse; + if(first_dollar_index != std::string::npos) + class_name = class_name.substr(0, first_dollar_index); + else + class_name = class_name.substr(0, last_dot_index); + replace_all(class_name, ".", "\\/"); + java_cp_include_files = class_name + + "(\\$.*)?\\.class|" + "java\\/.*|" + "javax\\/.*|" + "sun\\/.*|" + "org\\/cprover\\/.*|" + "com\\/diffblue\\/annotation\\/.*"; + + if(cmd.isset("java-cp-include-files")) + warning() << "--java-cp-include-files ignored due to " + "--load-containing-class-only" + << eom; + } + else if(cmd.isset("java-cp-include-files")) { java_cp_include_files=cmd.get_value("java-cp-include-files"); // load file list from JSON file diff --git a/jbmc/src/java_bytecode/java_bytecode_language.h b/jbmc/src/java_bytecode/java_bytecode_language.h index 20885ed689c..81a48063c57 100644 --- a/jbmc/src/java_bytecode/java_bytecode_language.h +++ b/jbmc/src/java_bytecode/java_bytecode_language.h @@ -38,6 +38,7 @@ Author: Daniel Kroening, kroening@kroening.com "(java-max-input-tree-depth):" /* will go away */ \ "(max-nondet-tree-depth):" \ "(java-max-vla-length):" \ + "(load-containing-class-only)" \ "(java-cp-include-files):" \ "(lazy-methods)" /* will go away */ \ "(no-lazy-methods)" \ @@ -59,6 +60,8 @@ Author: Daniel Kroening, kroening@kroening.com " never initialize reference-typed parameter to the\n" /* NOLINT(*) */ \ " entry point with null\n" /* NOLINT(*) */ \ " --java-max-vla-length N limit the length of user-code-created arrays\n" /* NOLINT(*) */ \ + " --load-containing-class-only only load the class containing the " \ + " method under test and the library classes" \ " --java-cp-include-files r regexp or JSON list of files to load\n" \ " (with '@' prefix)\n" \ " --no-lazy-methods load and translate all methods given on\n" \ diff --git a/jbmc/src/java_bytecode/java_class_loader_limit.cpp b/jbmc/src/java_bytecode/java_class_loader_limit.cpp index c04e9caa4c2..1bca3fc9f77 100644 --- a/jbmc/src/java_bytecode/java_class_loader_limit.cpp +++ b/jbmc/src/java_bytecode/java_class_loader_limit.cpp @@ -24,7 +24,11 @@ void java_class_loader_limitt::setup_class_load_limit( // '@' signals file reading with list of class files to load use_regex_match = java_cp_include_files[0] != '@'; if(use_regex_match) + { regex_matcher=std::regex(java_cp_include_files); + debug() << "Limit loading to classes matching : " << java_cp_include_files + << eom; + } else { assert(java_cp_include_files.length()>1); @@ -54,7 +58,10 @@ bool java_class_loader_limitt::load_class_file(const std::string &file_name) if(use_regex_match) { std::smatch string_matches; - return std::regex_match(file_name, string_matches, regex_matcher); + if(std::regex_match(file_name, string_matches, regex_matcher)) + return true; + debug() << file_name + " discarded since not matching loader regexp" << eom; + return false; } else // load .class file only if it is in the match set