Add --load-containing-class-only option #2633

allredj · 2018-07-30T16:36:39Z

Add option to only load the class (and inner classes) that contain the method under test.

Utility to search and replace strings inside a string.

tautschnig · 2018-07-30T16:51:30Z

jbmc/src/java_bytecode/java_bytecode_language.h

@@ -38,7 +38,8 @@ Author: Daniel Kroening, [email protected]
  "(java-max-input-tree-depth):" /* will go away */ \
  "(max-nondet-tree-depth):" \
  "(java-max-vla-length):" \
-  "(java-cp-include-files):" \
+  "(load-containing-class-only)" \
+  "(java-cp-include-files)" \


Missing : (unless you really wanted to change the syntax here, which isn't reflected in the code.

Typo. Fixed.

tautschnig · 2018-07-30T16:52:24Z

jbmc/src/java_bytecode/java_bytecode_language.h

@@ -59,6 +60,8 @@ Author: Daniel Kroening, [email protected]
  "                              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" \


How does this differ from lazy loading? Obviously I'm not a Java expert, but as a mere user I'm pretty confused by this vast array of options.

Lazy-loading will load all the classes that are needed to analyse the program. This option is more aggressive as it will cut out anything that leaves the class that contains the method under test. It's a wild over-approximation but it's an easy way of analysing blocks that would otherwise be intractable by jbmc.

Hmm, there is all the work that @hannes-steffenhagen-diffblue has done (7952f2c and related commits). Is doing it on a by-class level a much better approach for Java? Also, without your explanation above I would not have guess the semantics of this new option.

@tautschnig The documentation is a bit sparse, I can easily agree with that. It's mostly the fault of the --help string format which we don't want to make to heavy. Where would a good place be to write an extended description?
At this point it's not clear how well a per-class approach would work. It's an experimental feature (I will document is as such).

Is doing it on a by-class level a much better approach for Java?

Unfortunately, it's more complicated than that due to Java's compiler-generated methods, inner classes, etc.

Near-duplicate of test-gen's single-function-only option? Perhaps both should be generalised into a function whitelist?

tautschnig · 2018-07-30T16:52:58Z

src/cbmc/cbmc_parse_options.h

@@ -54,6 +54,7 @@ class optionst;
  "(string-max-input-length):" \
  "(aig)(16)(32)(64)(LP64)(ILP64)(LLP64)(ILP32)(LP32)" \
  "(little-endian)(big-endian)" \
+  "(load-containing-class-only)" \


Why is this being added to CBMC?!

Mistake. Will remove.

allredj · 2018-07-30T16:58:22Z

jbmc/src/java_bytecode/java_bytecode_language.cpp

+                            "javax\\/.*|"
+                            "sun\\/.*|"
+                            "org\\/cprover\\/.*|"
+                            "com\\/diffblue\\/annotation\\/.*";


This is obviously not great. Please suggest ways of making this more general.

Not actually making it more general, but you might do (javax|sun|org\\/cprover|com\\/diffblue\\/annotation)\\/.*

These hard-coded values make the option a bit misleading (it is not only loading the containing class). Maybe these could be added through java-cp-include-files as additional files to include (that have to be given explicitly) on the command line.

@romainbrenguier That might indeed be better. Will try that.

Add option to only load the class (and inner classes) that contain the method under test.

allredj

Passed Diffblue compatibility checks (cbmc commit: caed4f9).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/80402350

romainbrenguier · 2018-07-31T07:26:41Z

jbmc/regression/jbmc/load-containing-class-only/test.desc

+--
+^warning: ignoring
+--
+Check that External.class is not loaded when using --load-containing-class-only


May be good to have a test that shows the opposite is true without the option.

romainbrenguier · 2018-07-31T07:29:03Z

jbmc/src/java_bytecode/java_bytecode_language.cpp

-  if(cmd.isset("java-cp-include-files"))
+  if(cmd.isset("load-containing-class-only"))
+  {
+    const std::string function_to_analyse = cmd.get_value("function");


This assumes --function is set in the command line

romainbrenguier · 2018-07-31T07:30:26Z

jbmc/src/java_bytecode/java_bytecode_language.cpp

+    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);


It doesn't seem to handle the case where there is no dot.

romainbrenguier · 2018-07-31T07:31:53Z

jbmc/src/java_bytecode/java_bytecode_language.cpp

+    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;


No need to copy function_to_analyse here, it can be used in the substr call instead.

romainbrenguier · 2018-07-31T07:36:03Z

jbmc/src/java_bytecode/java_bytecode_language.cpp

+                            "javax\\/.*|"
+                            "sun\\/.*|"
+                            "org\\/cprover\\/.*|"
+                            "com\\/diffblue\\/annotation\\/.*";


These hard-coded values make the option a bit misleading (it is not only loading the containing class). Maybe these could be added through java-cp-include-files as additional files to include (that have to be given explicitly) on the command line.

romainbrenguier · 2018-07-31T07:50:28Z

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 &);


Keeping the name of the parameters could be nice.

romainbrenguier · 2018-07-31T07:51:39Z

src/util/string_utils.cpp

@@ -148,3 +148,16 @@ std::string escape(const std::string &s)

  return result;
 }
+
+void replace_all(


Documentation would be nice.

romainbrenguier · 2018-07-31T07:52:36Z

src/util/string_utils.cpp

+  const std::string &to)
+{
+  size_t start_pos = 0;
+  while((start_pos = str.find(from, start_pos)) != std::string::npos)


A for-loop maybe clearer.

smowton · 2018-07-31T09:13:17Z

jbmc/src/java_bytecode/java_bytecode_language.cpp

+    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);


There always should be one in a Java function ID (but make an INVARIANT)

smowton · 2018-07-31T09:14:17Z

jbmc/src/java_bytecode/java_bytecode_language.cpp

+    replace_all(class_name, ".", "\\/");
+    java_cp_include_files = class_name +
+                            "(\\$.*)?\\.class|"
+                            "java\\/.*|"


I don't think / needs escaping?

Loading all inner classes is a bit weird, should they only be inners of the desired class?

smowton · 2018-07-31T09:16:47Z

jbmc/src/java_bytecode/java_class_loader_limit.cpp

    regex_matcher=std::regex(java_cp_include_files);
+    debug() << "Limit loading to classes matching : " << java_cp_include_files


Class-loading is limited to...

allredj · 2018-07-31T10:19:23Z

Moving the core functionality out of jbmc as it is not very relevant to verification. Replacement PR: #2640

Add replace_all string utility

0886132

Utility to search and replace strings inside a string.

allredj self-assigned this Jul 30, 2018

allredj requested review from peterschrammel, forejtv and romainbrenguier July 30, 2018 16:36

allredj requested review from cesaro, cristina-david, kroening, mgudemann, NathanJPhillips, pkesseli, smowton, tautschnig and thk123 as code owners July 30, 2018 16:36

tautschnig requested changes Jul 30, 2018

View reviewed changes

allredj commented Jul 30, 2018

View reviewed changes

Add --java-load-containing-class-only option

caed4f9

Add option to only load the class (and inner classes) that contain the method under test.

allredj force-pushed the load-containing-class-only branch from 8c435e1 to caed4f9 Compare July 30, 2018 17:04

allredj commented Jul 30, 2018

View reviewed changes

romainbrenguier reviewed Jul 31, 2018

View reviewed changes

smowton reviewed Jul 31, 2018

View reviewed changes

allredj mentioned this pull request Jul 31, 2018

Class loading utils #2640

Merged

allredj closed this Jul 31, 2018

allredj deleted the load-containing-class-only branch July 31, 2018 10:19

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Add --load-containing-class-only option #2633

Add --load-containing-class-only option #2633

allredj commented Jul 30, 2018

tautschnig Jul 30, 2018

allredj Jul 30, 2018

tautschnig Jul 30, 2018

allredj Jul 30, 2018

tautschnig Jul 30, 2018

allredj Jul 31, 2018

peterschrammel Jul 31, 2018 •

edited

Loading

smowton Jul 31, 2018

tautschnig Jul 30, 2018

allredj Jul 30, 2018

allredj Jul 30, 2018

tautschnig Jul 30, 2018

romainbrenguier Jul 31, 2018

allredj Jul 31, 2018

allredj left a comment

romainbrenguier Jul 31, 2018

romainbrenguier Jul 31, 2018

romainbrenguier Jul 31, 2018

romainbrenguier Jul 31, 2018

romainbrenguier Jul 31, 2018

romainbrenguier Jul 31, 2018

romainbrenguier Jul 31, 2018

romainbrenguier Jul 31, 2018

smowton Jul 31, 2018

smowton Jul 31, 2018

smowton Jul 31, 2018

smowton Jul 31, 2018

allredj commented Jul 31, 2018

		regex_matcher=std::regex(java_cp_include_files);
		debug() << "Limit loading to classes matching : " << java_cp_include_files

Add --load-containing-class-only option #2633

Add --load-containing-class-only option #2633

Conversation

allredj commented Jul 30, 2018

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

peterschrammel Jul 31, 2018 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

allredj left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

allredj commented Jul 31, 2018

peterschrammel Jul 31, 2018 •

edited

Loading