Deal with virtual function calls with no candidate targets #2074

owen-mc-diffblue · 2018-04-16T14:36:51Z

During virtual method resolution, if a virtual function call has no candidate targets then we add the class it was called on as an instantiated class.

Also tidied up the code in various ways.

tautschnig

Please reconsider the id_sett part as detailed in my comments. I have not looked at the Java part.

tautschnig · 2018-04-16T14:53:47Z

src/util/irep.h

@@ -29,6 +29,8 @@ Author: Daniel Kroening, [email protected]
 #include <list>
 #else
 #include <map>
+#include <unordered_set>


This is in the wrong place for it would not get included when SUB_IS_LIST is set.

tautschnig · 2018-04-16T14:55:38Z

src/util/irep.h

@@ -43,6 +45,7 @@ typedef std::string irep_namet;
 // NOLINTNEXTLINE(readability/identifiers)
 typedef string_hash irep_id_hash;
 #endif
+typedef std::unordered_set<irep_idt, irep_id_hash> id_sett;


It's probably a good idea to introduce a widely visible typedef, but I think this needs to happen in a separate PR: 1) Various places already define an id_sett; 2) those definitions don't always use the same types; 3) the type name should likely make clear that this is an unordered set of IDs.

Okay, for this PR I'll just make it a local typedef, but I might try and make a widely visible one in another PR. For the record it's std::unordered_set<irep_idt, irep_id_hash> 9 times and std::set<cpp_idt *> 2 times. I like that id_sett is short, but I agree that you might assume it wasn't unordered.

Here's a PR for you: #2075

owen-mc-diffblue · 2018-04-16T16:02:50Z

@smowton Please review

smowton

Looks good, but needs tests -- at least the minimal example I gave on Slack please:

public class test {

  interface factory_intf {
    public intf getintf();
  }

  interface intf {
    public void f();
  }

  public static void main(factory_intf i) { i.getintf().f(); }
}

smowton · 2018-04-17T11:07:31Z

src/java_bytecode/ci_lazy_methods.cpp

+
+    any_new_classes = false;
+
+    // Find virtual callsites with no candidate targets, guess that the class


Suggest giving example: if we have invokevirtual A.f and we don't believe either A or any of its children may exist, assume specifically A is somehow instantiated. Note this may result in an abstract class being classified as instantiated, which stands in for some unknown concrete subclass: in this case the called method will be a stub.

owen-mc-diffblue · 2018-04-18T12:48:53Z

@smowton I have added that comment and that test

NathanJPhillips · 2018-04-18T13:22:50Z

src/java_bytecode/ci_lazy_methods.cpp

+        candidate_target_methods,
+        symbol_table);
+
+      if(candidate_target_methods.empty())


I'd invert this with a continue for clarity of control flow.

NathanJPhillips · 2018-04-18T13:23:08Z

src/java_bytecode/ci_lazy_methods.cpp

+
+      if(candidate_target_methods.empty())
+      {
+        any_new_classes = true;


I'd set this at the end after you've done something that adds new classes.

owen-mc-diffblue · 2018-04-18T15:44:18Z

@NathanJPhillips I've addressed your comments. I've also removed the typedef for id_sett and used std::unordered_set<irep_idt> instead, following #2082.

It's slightly easier to read a while loop, and it makes sense to initialise any_new_methods to true because we have already put things into method_worklist2.

Used set instead of vector to remove duplicates, which should prevent investigating the same method multiple times.

Also, use an unordered list instead of a vector so we don't have to deduplicate

During virtual method resolution, if a virtual function call has no candidate targets then we add the class it was called on as an instantiated class.

It should decide that `intf` is instantiated even though (a) it doesn't see a constructor for it and (b) it is an interface. It isn't ideal instantiating an interface, but it stands in for a class which implements the interface.

smowton · 2018-04-19T13:26:45Z

@owen-jones-diffblue test-gen bump?

owen-mc-diffblue · 2018-04-19T13:31:40Z

https://github.com/diffblue/test-gen/pull/1710

id_sett changes removed from this PR

31c47c2 Merge pull request diffblue#2113 from diffblue/java_new_array_data fb3025d Merge pull request diffblue#2107 from thk123/feature/TG-3271/interpreter-tracking-mock-exceptions 32bf48e Merge pull request diffblue#2105 from tautschnig/determinise-test 7254a2a show java_new_array_data side effects 0f1482c Merge pull request diffblue#2094 from smowton/smowton/fix/tmp-object-factory-prefix 3cfec66 Merge pull request diffblue#2106 from diffblue/ptrmember_on_array bf4c39c Merge pull request diffblue#1966 from JohnDumbell/JohnDumbell/Update-Assertion-Validation 74a37c6 Merge pull request diffblue#1988 from tautschnig/cadical 74dc576 Merge pull request diffblue#2003 from tautschnig/bitfield-offset 8916906 Merge pull request diffblue#2008 from tautschnig/section-bug 0bd83ab Extension to interpreter class a0ca0ba fix array->f typechecking e1f4120 Make virtual function resolution independent of string table entry ordering 714ccff Merge pull request diffblue#2072 from danpoe/feature/small-shared-two-way-ptr 16b6c20 Merge pull request diffblue#2046 from thk123/gs_tg2922 04cb909 Merge pull request diffblue#2102 from thk123/formatting/sort-includes-clang-format 7070ba1 Sort includes using clang-format 9874a6b Reformatting touched output function f2a4054 Remove redundant default constructor 54fb9ab Use format rather than from_expr for output 781bf7c Introduce exceptions for all conversion steps. 21997b2 Add documentation to convert_bitvector 015b284 Test demonstrating logging with clause for dealing with Windows 9d41b0c Disable nested exception printing for Windows b866015 Provide the original goto statement in the error a97bc28 Introduce throwing a guard conversion exception 12f25c2 Introduce throwing bv_conversion expection 9bd5222 Convert flatten_byte_extract to use structured exceptions 3207291 Introduce nested exception printing 35c4be7 Small shared two way pointer 7d247da Merge pull request diffblue#2099 from mgudemann/bugfix/build/glucose_syrup 1776a9e Merge pull request diffblue#1950 from romainbrenguier/refactor/prop_conv_straightforward 4147243 Change set_variable_name API to consume irep_idt 2d8be06 Rename `it` to pair in boolbvt::print_assignment 4365c28 Simplify boolbvt::set_to b18109f Make make_(free_)bv_expr return exprt 5724a35 Simplify loop in prop_conv::get 4987f3a Remove useless comments 13e87a9 Simplify dec_solve a0500f6 Use standard algorithm for finding an element ba13c94 Use auto for iterator types 9179571 Remove useless includes a905a07 Replace throws by invariant or preconditions 7db44fc Remove virtual keyword where not needed 990f33e Initialize at declaration instead of construction c1a93b3 Renaming `it` to symbol 8eb20f6 Use ranged for dc799e0 Assert replaced by unreachable c34e073 Add support for CaDiCaL 1bd9efd Merge pull request diffblue#2097 from peterschrammel/java-cleanup-replace a079f46 Clang-format moved file 2eb3714 Move replace_java_nondet to java_bytecode 9a8c292 Remove unnecessary include c8cf100 Remove Java refs from ANSI-C docs 0090952 Merge pull request diffblue#2096 from diffblue/cleanout-java aa3caa3 Fix CMake build for Glucose Syrup 1156930 Merge pull request diffblue#1244 from tautschnig/goto-gcc-at-fix 706e391 Merge pull request diffblue#2093 from owen-jones-diffblue/owen-jones-diffblue/remove_unnecessary_irep_id_hash 290feb4 Merge pull request diffblue#2095 from diffblue/get_json_stream_precondition ac2df21 Merge pull request diffblue#2027 from tautschnig/linking-multiple-conflicts dd0d602 Merge pull request diffblue#2030 from tautschnig/goto-cc-linux-kernel 42e58d4 Merge pull request diffblue#2085 from tautschnig/from_expr-cleanup 692f92d remove dependency on java_bytecode 8c6165d precondition for get_json_stream() e28a662 Remove unused typedef 5626fb7 Merge pull request diffblue#2092 from smowton/smowton/cleanup/diffblue-spelling 4840154 Replace stack by deque and use range-based for loop 987edbe Use range-based for loops 92ac82c Remove redundant irep_id_hash for unordered maps dc2b436 Remove redundant irep_id_hash for sets 5aa2c2d Attribute main function arguments to __CPROVER_start b7ef5af Merge pull request diffblue#2053 from owen-jones-diffblue/owen-jones-diffblue/bugfix/make-callgraph-include-uncalled-functions 252474f String tests: DiffBlue -> Diffblue de1915a Merge pull request diffblue#2074 from owen-jones-diffblue/owen-jones-diffblue/lazy-methods-no-candidate-callees d73f6bc Make directed callgraph include nodes with no edges 2a45e61 Only the top-level section should be considered for renaming 9c66a66 fixup! Support __attribute__((section("x")) e133964 C front-end: Section/ASM renaming also needs to be applied to aliases 0cfc72f Test --call-graph and --reachable-call-graph 1c34d22 Test lazy-loading when there are no candidates 289a439 Deal with virtual function calls with no candidate targets 9347615 Remove incorrect comment 18b1962 Fix order of parameters in function header 82058da Store virtual function calls instead of virtual call-sites 3653550 Use unordered set of irep_ids in ci_lazy_methods c31d43f Remove code duplication 945f885 Rename two variables and make one more local b7d70e7 Replace do-while loop with equally valid while loop 58b990d Use from_{expr,type} matching the language of the expression/type 177c8c1 goto-cc: support thin ar archives, refactoring e80008e goto-cc: support GCC's print-sysroot* options 38e6fa5 Accept the --build-id option in goto-ld f3bbb12 Linking: report multiple conflicts 495f109 Fixing member offset computation in presence of bitfields 5109eab Add @<file> arguments to the original command line 97d556e Update desc file to add pass variables. eea76ec Add a regression test. c14e907 Increase AssertionError arguments allowed from 2 to 3 git-subtree-dir: cbmc git-subtree-split: 31c47c2

owen-mc-diffblue requested review from cesaro, kroening, mgudemann, peterschrammel, smowton, tautschnig and thk123 as code owners April 16, 2018 14:36

tautschnig previously requested changes Apr 16, 2018

View reviewed changes

owen-mc-diffblue force-pushed the owen-jones-diffblue/lazy-methods-no-candidate-callees branch from d884274 to b858e9a Compare April 16, 2018 16:00

owen-mc-diffblue force-pushed the owen-jones-diffblue/lazy-methods-no-candidate-callees branch 2 times, most recently from b1de53e to 7152744 Compare April 17, 2018 08:29

smowton reviewed Apr 17, 2018

View reviewed changes

owen-mc-diffblue force-pushed the owen-jones-diffblue/lazy-methods-no-candidate-callees branch 2 times, most recently from 639617b to 265cef2 Compare April 18, 2018 12:48

NathanJPhillips approved these changes Apr 18, 2018

View reviewed changes

owen-mc-diffblue force-pushed the owen-jones-diffblue/lazy-methods-no-candidate-callees branch from 265cef2 to d7081fa Compare April 18, 2018 15:42

Owen Jones added 9 commits April 19, 2018 09:44

Replace do-while loop with equally valid while loop

b7d70e7

It's slightly easier to read a while loop, and it makes sense to initialise any_new_methods to true because we have already put things into method_worklist2.

Rename two variables and make one more local

945f885

Remove code duplication

c31d43f

Use unordered set of irep_ids in ci_lazy_methods

3653550

Used set instead of vector to remove duplicates, which should prevent investigating the same method multiple times.

Store virtual function calls instead of virtual call-sites

82058da

Also, use an unordered list instead of a vector so we don't have to deduplicate

Fix order of parameters in function header

18b1962

Remove incorrect comment

9347615

Deal with virtual function calls with no candidate targets

289a439

During virtual method resolution, if a virtual function call has no candidate targets then we add the class it was called on as an instantiated class.

Test lazy-loading when there are no candidates

1c34d22

It should decide that `intf` is instantiated even though (a) it doesn't see a constructor for it and (b) it is an interface. It isn't ideal instantiating an interface, but it stands in for a class which implements the interface.

owen-mc-diffblue force-pushed the owen-jones-diffblue/lazy-methods-no-candidate-callees branch from d7081fa to 1c34d22 Compare April 19, 2018 08:44

smowton approved these changes Apr 19, 2018

View reviewed changes

thk123 merged commit de1915a into diffblue:develop Apr 19, 2018

owen-mc-diffblue deleted the owen-jones-diffblue/lazy-methods-no-candidate-callees branch April 19, 2018 14:14

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Deal with virtual function calls with no candidate targets #2074

Deal with virtual function calls with no candidate targets #2074

owen-mc-diffblue commented Apr 16, 2018

tautschnig left a comment

tautschnig Apr 16, 2018

tautschnig Apr 16, 2018

owen-mc-diffblue Apr 16, 2018

NathanJPhillips Apr 16, 2018

owen-mc-diffblue commented Apr 16, 2018

smowton left a comment

smowton Apr 17, 2018

owen-mc-diffblue commented Apr 18, 2018

NathanJPhillips Apr 18, 2018

NathanJPhillips Apr 18, 2018

owen-mc-diffblue commented Apr 18, 2018

smowton commented Apr 19, 2018

owen-mc-diffblue commented Apr 19, 2018


		any_new_classes = false;

		// Find virtual callsites with no candidate targets, guess that the class

Deal with virtual function calls with no candidate targets #2074

Deal with virtual function calls with no candidate targets #2074

Conversation

owen-mc-diffblue commented Apr 16, 2018

tautschnig left a comment

Choose a reason for hiding this comment

tautschnig Apr 16, 2018

Choose a reason for hiding this comment

tautschnig Apr 16, 2018

Choose a reason for hiding this comment

owen-mc-diffblue Apr 16, 2018

Choose a reason for hiding this comment

NathanJPhillips Apr 16, 2018

Choose a reason for hiding this comment

owen-mc-diffblue commented Apr 16, 2018

smowton left a comment

Choose a reason for hiding this comment

smowton Apr 17, 2018

Choose a reason for hiding this comment

owen-mc-diffblue commented Apr 18, 2018

NathanJPhillips Apr 18, 2018

Choose a reason for hiding this comment

NathanJPhillips Apr 18, 2018

Choose a reason for hiding this comment

owen-mc-diffblue commented Apr 18, 2018

smowton commented Apr 19, 2018

owen-mc-diffblue commented Apr 19, 2018