[TG-3813] Allow specifying specific methods by regex to be loaded by lazy methods #2350

thk123 · 2018-06-12T16:47:48Z

Based on: #2335 ✅
Here we extend the existing option --lazy-methods-extra-entry-point to take a regex (previously allowed .* to be used to specify any method for a given class). This brings it into line with other "work around lazy loading not loading what I want".

I maintained support for automatic descriptor filling (though now it will match all the methods whereas previously it would error). I also keep not requiring the java:: prefix.

mgudemann · 2018-06-13T08:09:58Z

jbmc/regression/jbmc/lazyloading11/test.desc

@@ -1,6 +1,6 @@
 CORE symex-driven-lazy-loading-expected-failure
 test.class
--lazy-methods --verbosity 10 --function test.f --lazy-methods-extra-entry-point 'test.sety:(I)V' --lazy-methods-extra-entry-point 'test.sety:(F)V'
+--lazy-methods --verbosity 10 --function test.f --lazy-methods-extra-entry-point 'test.sety:\(I\)V' --lazy-methods-extra-entry-point 'test.sety:\(F\)V'


are you sure this is needed in the quotes ?

You mean the escaping the brackets? Yes as otherwise it will be used as a regex group rather than matching the brackets (this is essentially what is changing).

mgudemann · 2018-06-13T08:13:46Z

jbmc/src/java_bytecode/ci_lazy_methods_needed.cpp

@@ -43,3 +44,114 @@ bool ci_lazy_methods_neededt::add_needed_class(

  return true;
 }
+
+/// Add to the needed classes all class specified, the replacement type if it
+/// will be replaced, and all feilds it contains.


... fields ...

Though this is a comment for #2335 so will squash into there

mgudemann · 2018-06-13T08:19:32Z

jbmc/src/java_bytecode/load_method_by_regex.cpp

+
+  static const std::string java_prefix = "java::";
+  return descriptor_index == java_prefix.length() - 1 &&
+         has_prefix(pattern, "java::");


what does this check? the prefix check is done above, right?

Yes I worried about that being confusing but couldn't think of a better way - this is checking that if a : is found, it is not the second colon in java::

thk123 · 2018-06-13T08:24:45Z

CI failing for hopefully the reason in #2335 only, needs some unit tests for load_method_by_regext

LAJW

I feel like the class hierarchy in the last two commits could be replaced by lambdas and functions returning lambdas. It would greatly reduce boilerplate.

LAJW · 2018-06-13T10:09:01Z

jbmc/src/java_bytecode/load_extra_methods.h

+  {
+  }
+  std::vector<irep_idt>
+  extra_methods(const symbol_tablet &symbol_table) const override;


This class hierarchy appears to be unnecessary. You could greatly simplify all of that by using lambdas (and maybe higher-order functions to make your life easier).

LAJW · 2018-06-13T10:10:13Z

jbmc/src/java_bytecode/load_method_by_regex.cpp

+    if(symbol.second.is_function())
+    {
+      const std::string symbol_name = id2string(symbol.first);
+      if(std::regex_match(symbol_name, regex))


Combine conditions, flatten the loop? Also this is another single-method-class that could've been replaced by a lambda.

Think is is clearer as two separate checks.

thk123 · 2018-06-13T14:11:32Z

@LAJW repalaced class structure with lambda cac9c7b

thk123 · 2018-06-13T14:33:33Z

jbmc/src/java_bytecode/load_method_by_regex.cpp

@@ -0,0 +1,77 @@
+


This needs adding to a Makefile

thk123 · 2018-06-18T16:18:28Z

TG pointer bump: https://github.com/diffblue/test-gen/pull/1960

mgudemann

LGTM

LAJW · 2018-06-19T13:08:24Z

jbmc/unit/java_bytecode/load_method_by_regex.cpp

@@ -28,8 +19,7 @@ SCENARIO(
    const std::string pattern = "java::com.diffblue.ClassName.methodName";
    WHEN("When calling does_pattern_miss_descriptor")
    {
-      bool result =
-        load_method_by_regex_testt::does_pattern_miss_descriptor(pattern);
+      bool result = does_pattern_miss_descriptor(pattern);


Nit const here and in the rest of this file.

LAJW · 2018-06-19T13:09:10Z

jbmc/src/java_bytecode/java_bytecode_language.cpp

@@ -100,7 +100,7 @@ void java_bytecode_languaget::get_language_options(const cmdlinet &cmd)
    extra_entry_points.end(),
    std::back_inserter(extra_methods),
    [](const std::string &pattern) {
-      return util_make_unique<load_method_by_regext>(pattern);
+      return build_load_method_by_regex(pattern);


Could you put build_load_method_by_regex as an argument of std::transform directly?

LAJW · 2018-06-19T13:09:43Z

jbmc/src/java_bytecode/load_method_by_regex.cpp

+        if(std::regex_match(symbol_name, regex))
+        {
+          matched_methods.push_back(symbol_name);
+        }


The body of this loop could be simplified to:

if(symbol.second.is_function() && std::regex_match(id2string(symbol.first), regex)) matched_methods.push_back(symbol.first);

Sure if you like, not convinced it is any more readable (And I'm not removing braces 🙃 )

LAJW

Some nitpicks about testing utilities. Please squash before merging, so that all these classes disappear.

LAJW · 2018-06-19T13:12:47Z

unit/testing-utils/require_vectors_equal_unordered.h

+template <class T>
+static void require_vectors_equal_unordered(
+  const std::vector<T> actual,
+  const std::vector<T> expected)


Remove static - it's an instruction for the linker that a function has been defined only in this file and nowhere else. While it might work on the first use (used only in one file at the moment), it might potentially break later when there are unresovled externals to an already defined specialization of this template.

Also, could you add & to actual and expected? As it is right now, this function will only work with copyable elements or rvalues. That means if you were testing a vector of unique pointers, it would only work with std::move.

…rder

These method loads can be used to manually load additional methods for ci_lazy_methods

This will allow for loading for example, all constructors or all methods called getSomething. Tests using this require minor modifications when they have specified the descriptor as the brackets must be escaped for the regex. However, the new code handles the case where no descriptor is provided (in which case it will match all overloads) and the case where no java:: prefix has been provided, leaving similar behaviour. Correcting documentation for the extra entry points

allredj

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

@lock

7c1de91 Merge pull request diffblue#2465 from tautschnig/vs-criteria 9480092 Merge pull request diffblue#2437 from tautschnig/vs-empty a025add Merge pull request diffblue#2463 from tautschnig/vs-xref 0f3d345 Remove unused parameter criteria cdb7e52 Merge pull request diffblue#2453 from tautschnig/vs-deprected-uint bb7607d Merge pull request diffblue#2451 from tautschnig/c++-parser a07639d Merge pull request diffblue#2447 from tautschnig/cpp-regression-tests bdac907 Merge pull request diffblue#2459 from tautschnig/cmake-cleanup 261e883 Merge pull request diffblue#2461 from tautschnig/vs-auto 8acbc6c Merge pull request diffblue#2457 from tautschnig/vs-goto-convert bd2547a Merge pull request diffblue#2458 from tautschnig/vs-long-long fbc56db Remove unnecessarily inlined implementations to otherwise empty cpp file 6adcebc Merge pull request diffblue#2456 from tautschnig/vs-reserve a905ac0 Replace lambda by member function reference to silence Visual Studio ce6a297 Use auto to avoid unnecessary signed/unsigned conversion 79ef045 Deprecate get_unsigned_int c528c25 Remove no-longer-existent-files from exclusion lists in CMake files 4c6fc61 Use long-long integer constant as the left-hand side is long long 7dbf60a Remove unused parameters in goto_convert 0482889 Use reserve instead of generating blank strings 5e5e264 Merge pull request diffblue#2441 from tautschnig/vs-concur 8b03ac1 Merge pull request diffblue#2404 from tautschnig/vs-zero-2 18a3070 Merge pull request diffblue#2454 from tautschnig/vs-code-typet 062a886 Merge pull request diffblue#2408 from tautschnig/vs-set-map ccfc4e0 Merge pull request diffblue#2417 from tautschnig/vs-missing-arg 2bf4097 Merge pull request diffblue#2419 from tautschnig/vs-loc-num 7308bf6 Avoid deprecated code_typet() constructor c2a8fb8 Do not use count() when returning a bool 62ec461 Merge pull request diffblue#2360 from smowton/smowton/fix/dont-deref-null-for-class-identifier-v2 5e1f365 C++ parser: actually use parameters dca5b76 Merge pull request diffblue#2413 from tautschnig/vs-cpp-fix ee2421a Test passes 0cf27c6 type_traits requires C++ 11 660ae90 Remove unused parameter from cpp_destructor and fix types 0784f77 Merge pull request diffblue#2125 from smowton/smowton/feature/symex-ignore-null-derefs 001fca0 Merge pull request diffblue#2280 from cesaro/java-concurrency-synchronization 2369df3 Add message handler to remove_instanceof and _exceptions 419bc1b Java instanceof: avoid dereferencing null pointer 9fd3434 Use local-safe-pointers analysis to improve Symex pointer resolution 8078569 Add local-safe-pointers analysis 0062a9c Merge pull request diffblue#2444 from tautschnig/vs-value-set 68ac566 JBMC: Regression tests for synchronized methods c0ee316 JBMC: Support for synchronized methods 7efa7bf JBMC: Regression tests for multi-threaded java programs 4d91aa5 JBMC: Modified the instrumentation of monitorexit/enter instructions 0691f03 JBMC: Zero-initialized 'cproverMonitorCount' component and removed '@lock' field (fixes diffblue#2307) 0b90c17 JBMC: Moved format_classpath.sh to scripts/format_classpath.sh 2a0d2f9 AppVeyor fix: remove existing clones of the java models library. 0c5a497 Merge pull request diffblue#2446 from tautschnig/vs-unlink f4cb6a9 Merge pull request diffblue#2442 from tautschnig/vs-side 5b12b25 Merge pull request diffblue#2445 from tautschnig/vs-simpl 53e35c2 Move side effect out of conditional aab593b Use C++ standard library function instead of POSIX function f5b465d Simplify code to avoid Visual Studio warnings 7621a86 Remove unused parameter in value_set_analysis d50cec0 Remove unused parameter from concurrency_instrumentationt::instrument 475fe20 Merge pull request diffblue#2393 from tautschnig/git-info-cmake-fixes 5cd87c1 Merge pull request diffblue#2436 from tautschnig/vs-zero b4c0e22 Merge pull request diffblue#2410 from tautschnig/vs-deref-type 662d256 Merge pull request diffblue#2431 from tautschnig/vs-with 1aceb6c Merge pull request diffblue#2391 from diffblue/compilation-instructions 7c894e7 Merge pull request diffblue#2402 from tautschnig/vs-no-dummy 822de57 Merge pull request diffblue#2432 from tautschnig/vs-slice a3fe43b Merge pull request diffblue#2427 from tautschnig/vs-read-bin 0ab38e5 Merge pull request diffblue#2433 from tautschnig/vs-is-zero 95396bc Merge pull request diffblue#2438 from tautschnig/vs-partial 551ab81 Merge pull request diffblue#2411 from tautschnig/vs-message-handler 7464904 Merge pull request diffblue#2424 from tautschnig/vs-template 1feaa94 Merge pull request diffblue#2407 from tautschnig/vs-linker 82c7e48 Remove dummy implementations from propt 209d459 Partial-order concurrency: Remove unused parameter 0e3958a Zero-length array warning is C4200 in Visual Studio ed2cf6a Remove unused parameter from float_bvt::is_zero cb54ae5 Remove unused, empty function a5ecfb4 Remove unused parameters in convert_with_* 373636e Remove parameters that read_bin_goto_object_v3 does not use d6bdee6 Merge pull request diffblue#2369 from polgreen/disconnect_unreachable 0498da9 Merge pull request diffblue#2400 from tautschnig/vs-return-type 2eb9156 Merge pull request diffblue#2406 from tautschnig/vs-sizet1 d5ea06f Merge pull request diffblue#2422 from tautschnig/vs-thread-id 609c934 Merge pull request diffblue#2414 from tautschnig/vs-want 9263e43 Merge pull request diffblue#2403 from tautschnig/vs-zero-1 e638f72 CBMC_VERSION: Use generated include files instead of command-line defines 1360f7f CMake refers to Clang on a Mac as AppleClang f27e724 Merge pull request diffblue#2421 from tautschnig/vs-bound ed98fd7 Merge pull request diffblue#2412 from tautschnig/vs-build 16fa26d Merge pull request diffblue#2405 from diffblue/aws-codebuild-jbmc d7dd598 build jbmc on AWS codebuild 001f684 fix compilation instructions 040fd91 Remove unused parameter dereference_type 6ee60cd Do not unnecessarily convert mp_integer to bounded type d605d56 goto-program instruction's location_number is unsigned 9305ebd Remove unused parameter message_handler 4361cc4 goto-instrument/wmm: add missing argument 6256290 Fix return type of nodes_empty 8c2f6e1 Use std::set instead of map as value is never used bd4faad Use std::size_t instead of int to match types at callsites d07d418 Templatize architecture_string to avoid type conversion 9c72f61 Fix type of thread_id to match goto-trace fb512f0 Remove unused paramter in cpp_typecheck_resolvet 2afa919 Explicitly compare int to zero to avoid Visual Studio warning a1be6c8 Remove unused parameter from local_bitvector_analysist::build 4b5677d Bound the number of attempts my_mkstemps tries to compute a file name b8743fa Merge pull request diffblue#2415 from tautschnig/fix-models d7ef0bc Fix coreModels test to match latest java models library 90c56b3 Merge pull request diffblue#2396 from tautschnig/vs-constructor a45e777 Merge pull request diffblue#2397 from tautschnig/vs-indent 38c7889 Merge pull request diffblue#2399 from tautschnig/vs-defined 8324386 Merge pull request diffblue#2401 from tautschnig/vs-make-constant-rec 1c1562e Merge pull request diffblue#2398 from tautschnig/vs-remove-adjust 2bf9de7 Remove empty function make_constant_rec cdb4075 Use defined(...) when testing for defined-ness of macros bef9866 Remove unused function adjust_lhs_object f0ceaf7 expr2c: indent output of code_deadt 576c0a6 Remove constructor declaration that has no implementation 8f6dab8 Merge pull request diffblue#2261 from thk123/bugfix/TG-3652/wrong-generic-type-two-params 262affb Merge pull request diffblue#2350 from thk123/feature/TG-3813/load-specified-methods 122108a Merge pull request diffblue#2387 from diffblue/fix-dist-scripts 1d461c4 version numbers are now followed by git tag 8f93163 increased version number in preparation for release 5.9 8bc9ecf Merge pull request diffblue#2386 from tautschnig/make-version 7b4b8fe Make's file function is only available from 4.2 onwards ca982a5 Merge pull request diffblue#2373 from tautschnig/git-version-output af880a4 Merge pull request diffblue#2382 from tautschnig/missing-dest e149397 Merge pull request diffblue#2384 from tautschnig/quiet-vs 4b124c8 add centered git version to CBMC banner 718e926 Build .release_info files containing the version string 6416372 windowsify compiler options 23455af Print git revision with all --version outputs 7ca835b Added CBMC_VERSION defines to CMake configuration 783fcea Extend lazy-methods-extra-entry-point to support regex methods 1e55404 CI lazy methods take vector of method loaders 2fb9e21 Add utility for checking two vectors are equal without caring about order e1398bc Add tests for generic type erasure 0c874bf Don't have generic type variables as a comment 1f9a5c4 Adding test about the type bd907a4 Diversified the test for multiple fields 6f98511 Merge pull request diffblue#2335 from thk123/bugfix/load-classes-from-opaque-calls ae1535f Do not print version info when linking using Visual Studio 7e7619c Add missing virtual destructor c0dd633 Merge pull request diffblue#2376 from diffblue/gcc_attributes5_KNOWNBUG 3423e44 gcc/clang treat __attribute__((aligned())) differently c509ece Merge pull request diffblue#2379 from tautschnig/fix-bswap e95f59d Don't instantiate abstract types when they are returned from stubs d7d5f63 Disable lazy loading opaque return for symex driven loading 409d892 Don't forcibly instantiate abstract classes a718893 Adding test to ensure methods on return type of opaque function 20645c9 Add classes to needed classes for parameters and returns for opaque calls 9d42bc8 Move method for gathering all instantiated types into ci_lazy_methods_needed b67ae26 Add can_cast_type for symbol_typet 9981fab Correct doxygen documentation 67c056b Unit test for disconnecting unreachable nodes eca3366 Disconnect unreachable nodes in a graph 3126dea Fix bswap_exprt constructor ac02bbc Merge pull request diffblue#2243 from diffblue/no-warning-ptr-array 0ef77c7 Merge pull request diffblue#2377 from diffblue/fix-tests3 b603a63 make test independent of index type 5ca7410 ignore size of arrays on ptr-to-array conversions git-subtree-dir: cbmc git-subtree-split: 7c1de91

thk123 requested review from smowton and LAJW June 12, 2018 16:47

thk123 requested review from cesaro, kroening, mgudemann, peterschrammel and tautschnig as code owners June 12, 2018 16:47

mgudemann reviewed Jun 13, 2018

View reviewed changes

LAJW reviewed Jun 13, 2018

View reviewed changes

thk123 force-pushed the feature/TG-3813/load-specified-methods branch from cac9c7b to 727ab5f Compare June 18, 2018 14:36

thk123 commented Jun 18, 2018

View reviewed changes

thk123 force-pushed the feature/TG-3813/load-specified-methods branch from 727ab5f to 5eefd82 Compare June 18, 2018 15:55

thk123 force-pushed the feature/TG-3813/load-specified-methods branch from 5eefd82 to 60305de Compare June 19, 2018 12:45

mgudemann approved these changes Jun 19, 2018

View reviewed changes

LAJW reviewed Jun 19, 2018

View reviewed changes

LAJW approved these changes Jun 19, 2018

View reviewed changes

thk123 added 2 commits June 21, 2018 14:27

Add utility for checking two vectors are equal without caring about o…

2fb9e21

…rder

CI lazy methods take vector of method loaders

1e55404

These method loads can be used to manually load additional methods for ci_lazy_methods

thk123 force-pushed the feature/TG-3813/load-specified-methods branch from 60305de to 024036b Compare June 21, 2018 13:30

thk123 force-pushed the feature/TG-3813/load-specified-methods branch from 024036b to 783fcea Compare June 21, 2018 15:18

allredj reviewed Jun 21, 2018

View reviewed changes

thk123 merged commit 262affb into diffblue:develop Jun 22, 2018

thk123 deleted the feature/TG-3813/load-specified-methods branch June 22, 2018 06:44

[TG-3813] Allow specifying specific methods by regex to be loaded by lazy methods #2350

[TG-3813] Allow specifying specific methods by regex to be loaded by lazy methods #2350

Uh oh!

Conversation

thk123 commented Jun 12, 2018 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

thk123 commented Jun 13, 2018

Uh oh!

LAJW left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

thk123 commented Jun 13, 2018

Uh oh!

Choose a reason for hiding this comment

Uh oh!

thk123 commented Jun 18, 2018

Uh oh!

mgudemann left a comment

Choose a reason for hiding this comment

Uh oh!

LAJW Jun 19, 2018 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

LAJW Jun 19, 2018 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

LAJW left a comment

Choose a reason for hiding this comment

Uh oh!

LAJW Jun 19, 2018 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

thk123 commented Jun 12, 2018 •

edited

Loading

LAJW Jun 19, 2018 •

edited

Loading

LAJW Jun 19, 2018 •

edited

Loading

LAJW Jun 19, 2018 •

edited

Loading