From 0431ce95403440135ae2979f2fbfcd4ca522f10f Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Tue, 1 Nov 2016 14:53:54 +0000 Subject: [PATCH 1/5] Remove virtual functions: shorten dispatch table Previously the dispatch table contained an entry per potential callee type; this reduces that to an entry per *distinct* callee function, which can be much shorter e.g. for java.lang.Object.equals, which every type has by inheritence but is often not overridden. --- .../remove_virtual_functions.cpp | 69 ++++++++++--------- 1 file changed, 38 insertions(+), 31 deletions(-) diff --git a/src/goto-programs/remove_virtual_functions.cpp b/src/goto-programs/remove_virtual_functions.cpp index 56c89dac3f..77ffb074d1 100644 --- a/src/goto-programs/remove_virtual_functions.cpp +++ b/src/goto-programs/remove_virtual_functions.cpp @@ -123,7 +123,6 @@ void remove_virtual_functionst::remove_virtual_function( assert(target->is_function_call()); to_code_function_call(target->code).function()= functions.begin()->symbol_expr; - return; } @@ -142,46 +141,54 @@ void remove_virtual_functionst::remove_virtual_function( // If necessary, cast to the last candidate function to // get the object's clsid. By the structure of get_functions, // this is the parent of all other classes under consideration. - symbol_typet suggested_type(functions.back().class_id); + const auto &base_classid=functions.back().class_id; + const auto &base_function_symbol=functions.back().symbol_expr; + symbol_typet suggested_type(base_classid); exprt c_id2=get_class_identifier_field(this_expr, suggested_type, ns); - goto_programt::targett last_function; - for(const auto &fun : functions) + std::map calls; + // Note backwards iteration, to get the least-derived candidate first. + for(auto it=functions.crbegin(), itend=functions.crend(); it!=itend; ++it) { - goto_programt::targett t1=new_code_calls.add_instruction(); - if(!fun.symbol_expr.get_identifier().empty()) + const auto &fun=*it; + auto insertit=calls.insert( + {fun.symbol_expr.get_identifier(), goto_programt::targett()}); + + // Only create one call sequence per possible target: + if(insertit.second) { + goto_programt::targett t1=new_code_calls.add_instruction(); + if(!fun.symbol_expr.get_identifier().empty()) + { // call function - t1->make_function_call(code); - auto &newcall=to_code_function_call(t1->code); - newcall.function()=fun.symbol_expr; - pointer_typet need_type(symbol_typet(fun.symbol_expr.get(ID_C_class))); - if(!type_eq(newcall.arguments()[0].type(), need_type, ns)) - newcall.arguments()[0].make_typecast(need_type); + t1->make_function_call(code); + auto &newcall=to_code_function_call(t1->code); + newcall.function()=fun.symbol_expr; + pointer_typet need_type(symbol_typet(fun.symbol_expr.get(ID_C_class))); + if(!type_eq(newcall.arguments()[0].type(), need_type, ns)) + newcall.arguments()[0].make_typecast(need_type); + } + else + { + // No definition for this type; shouldn't be possible... + t1->make_assertion(false_exprt()); + } + insertit.first->second=t1; + // goto final + goto_programt::targett t3=new_code_calls.add_instruction(); + t3->make_goto(t_final, true_exprt()); } - else + + // If this calls the base function we just fall through. + // Otherwise branch to the right call: + if(fun.symbol_expr!=base_function_symbol) { - // No definition for this type; shouldn't be possible... - t1->make_assertion(false_exprt()); + exprt c_id1=constant_exprt(fun.class_id, string_typet()); + goto_programt::targett t4=new_code_gotos.add_instruction(); + t4->make_goto(insertit.first->second, equal_exprt(c_id1, c_id2)); } - - last_function=t1; - - // goto final - goto_programt::targett t3=new_code_calls.add_instruction(); - t3->make_goto(t_final, true_exprt()); - - exprt c_id1=constant_exprt(fun.class_id, string_typet()); - - goto_programt::targett t4=new_code_gotos.add_instruction(); - t4->make_goto(t1, equal_exprt(c_id1, c_id2)); } - // In any other case (most likely a stub class) call the most basic - // version of the method we know to exist: - goto_programt::targett fallthrough=new_code_gotos.add_instruction(); - fallthrough->make_goto(last_function); - goto_programt new_code; // patch them all together From e5ff8dcb2c7c48b5557add312bd4db432c328ce5 Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Thu, 3 Nov 2016 09:41:00 +0000 Subject: [PATCH 2/5] If the only dispatch option is abstract, erase the call This can happen if the callee library isn't available and we're not mocking it. --- src/goto-programs/remove_virtual_functions.cpp | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/src/goto-programs/remove_virtual_functions.cpp b/src/goto-programs/remove_virtual_functions.cpp index 77ffb074d1..dccb6c5f23 100644 --- a/src/goto-programs/remove_virtual_functions.cpp +++ b/src/goto-programs/remove_virtual_functions.cpp @@ -121,8 +121,11 @@ void remove_virtual_functionst::remove_virtual_function( if(functions.size()==1) { assert(target->is_function_call()); - to_code_function_call(target->code).function()= - functions.begin()->symbol_expr; + if(functions.begin()->symbol_expr==symbol_exprt()) + target->make_skip(); + else + to_code_function_call(target->code).function()= + functions.begin()->symbol_expr; return; } From 260c8ec9936841a01dbba148f9b96c9c054e401c Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Tue, 31 Jan 2017 16:15:58 +0000 Subject: [PATCH 3/5] Make test more tolerant of formatting differences Side-effect of the virtual function table abbreviation code was to give a callsite a more expressive source_location than before. --- regression/cbmc-java/NullPointer2/test.desc | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/regression/cbmc-java/NullPointer2/test.desc b/regression/cbmc-java/NullPointer2/test.desc index f89103d5f5..3be1eaa44f 100644 --- a/regression/cbmc-java/NullPointer2/test.desc +++ b/regression/cbmc-java/NullPointer2/test.desc @@ -3,7 +3,7 @@ NullPointer2.class --pointer-check --stop-on-fail ^EXIT=10$ ^SIGNAL=0$ -^ file NullPointer2.java line 9 function java::NullPointer2.main:(\[Ljava/lang/String;)V$ +^ file NullPointer2.java line 9 function java::NullPointer2.main:(\[Ljava/lang/String;)V ^VERIFICATION FAILED$ -- ^warning: ignoring From 48f03aa5d665ea5c7cd30e7ad3565cd1841cc12b Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Tue, 31 Jan 2017 16:18:07 +0000 Subject: [PATCH 4/5] Add test for vtable abbreviation Also amend virtual6 whose expected results are now slightly different. --- regression/cbmc-java/virtual6/test.desc | 1 - regression/cbmc-java/virtual7/A.class | Bin 0 -> 222 bytes regression/cbmc-java/virtual7/B.class | Bin 0 -> 207 bytes regression/cbmc-java/virtual7/C.class | Bin 0 -> 207 bytes regression/cbmc-java/virtual7/D.class | Bin 0 -> 164 bytes regression/cbmc-java/virtual7/E.class | Bin 0 -> 164 bytes regression/cbmc-java/virtual7/test.class | Bin 0 -> 371 bytes regression/cbmc-java/virtual7/test.desc | 12 +++++++++++ regression/cbmc-java/virtual7/test.java | 25 +++++++++++++++++++++++ 9 files changed, 37 insertions(+), 1 deletion(-) create mode 100644 regression/cbmc-java/virtual7/A.class create mode 100644 regression/cbmc-java/virtual7/B.class create mode 100644 regression/cbmc-java/virtual7/C.class create mode 100644 regression/cbmc-java/virtual7/D.class create mode 100644 regression/cbmc-java/virtual7/E.class create mode 100644 regression/cbmc-java/virtual7/test.class create mode 100644 regression/cbmc-java/virtual7/test.desc create mode 100644 regression/cbmc-java/virtual7/test.java diff --git a/regression/cbmc-java/virtual6/test.desc b/regression/cbmc-java/virtual6/test.desc index 8432c7b230..5a5a7c7bf3 100644 --- a/regression/cbmc-java/virtual6/test.desc +++ b/regression/cbmc-java/virtual6/test.desc @@ -5,4 +5,3 @@ A.class ^SIGNAL=0$ IF "java::C".*THEN GOTO IF "java::B".*THEN GOTO -IF "java::A".*THEN GOTO diff --git a/regression/cbmc-java/virtual7/A.class b/regression/cbmc-java/virtual7/A.class new file mode 100644 index 0000000000000000000000000000000000000000..c6db51203199b01a76a911c4b7531e7bb162cc1d GIT binary patch literal 222 zcmX^0Z`VEs1_l!bJ}w4k25xo+9(D#^Mg}&U%)HDJJ4Oa(4b3n{1{UZ1lvG9rexJ;| zRKL>Pq|~C2#H1Xc2xA%}16OcPq|~C2#H1Xc2xA%}16Oc2S859_p zfaZe$6A%Ms7=V@lS+YQy5lFLYZD(NI2xKraumedpu%H-_#Q|3;36=$_KvyOKRLlvK IWMbd~0ED9%)c^nh literal 0 HcmV?d00001 diff --git a/regression/cbmc-java/virtual7/C.class b/regression/cbmc-java/virtual7/C.class new file mode 100644 index 0000000000000000000000000000000000000000..3c1ddff3a73a3e87ff98fc3cdb357bd35cce38ad GIT binary patch literal 207 zcmX^0Z`VEs1_l!bJ}w4k25xo+9(D#^Mg}&U%)HDJJ4Oa(4b3n{1{UZ1lvG9rexJ;| zRKL>Pq|~C2#H1Xc2xA%}16Ocb^1}=66ZgvJ9Mg}&U%)HDJJ4Oa(4b3n{1{UZ1lvG9rexJ;| zRKL>Pq|~C2#H1Xc2v=}^X;E^jTPBFZS&~{@qL-CemdL}v!obSNz~}b^1}=66ZgvJ9Mg}&U%)HDJJ4Oa(4b3n{1{UZ1lvG9rexJ;| zRKL>Pq|~C2#H1Xc2v=}^X;E^jTPBFZS&~{@qL-CemdL}v!obSNz~~CZP7DeROhB_i ofDwp+GC-OQ$dU!pAQ4ur?F@_?!P4wNk_{}V0VFwqJSGNC06{+(bpQYW literal 0 HcmV?d00001 diff --git a/regression/cbmc-java/virtual7/test.class b/regression/cbmc-java/virtual7/test.class new file mode 100644 index 0000000000000000000000000000000000000000..38d77aa50e8af9680f4d61ac192b438429eddede GIT binary patch literal 371 zcmYLF%SyvQ6g@YYWRhuY&=2sV z#5-N+z`5t#a}RTe`TqI%0&s*Kg(~V2D+-q3RRv*qO~Ez1uHYHoP*A9w(56H~VvFFO zWO-J!3HILp13`2~Jx!?HWVybb3{yS6PtpN9Vwhw(K}Dm}Bb=Gr_C8_7cFAQ5JBmdK!ODqZr-aK&MzLGMW93J&ETLFcqU)w} Z_>SOzM-?`2k~rpnJ4J=>UgF-u@-HF!Hl_do literal 0 HcmV?d00001 diff --git a/regression/cbmc-java/virtual7/test.desc b/regression/cbmc-java/virtual7/test.desc new file mode 100644 index 0000000000..b2b26ecb9c --- /dev/null +++ b/regression/cbmc-java/virtual7/test.desc @@ -0,0 +1,12 @@ +CORE +test.class +--show-goto-functions +^EXIT=0$ +^SIGNAL=0$ +IF "java::E".*THEN GOTO [12] +IF "java::B".*THEN GOTO [12] +IF "java::D".*THEN GOTO [12] +IF "java::C".*THEN GOTO [12] +-- +IF "java::A".*THEN GOTO +GOTO 4 diff --git a/regression/cbmc-java/virtual7/test.java b/regression/cbmc-java/virtual7/test.java new file mode 100644 index 0000000000..dc2d304392 --- /dev/null +++ b/regression/cbmc-java/virtual7/test.java @@ -0,0 +1,25 @@ +public class test { + public static void main() { + A[] as = { new A(), new B(), new C(), new D(), new E() }; + as[2].f(); + } +} + +class A { + void f() { } +} + + +class B extends A { + void f() { } +} + +class C extends A { + void f() { } +} + +class D extends C { +} + +class E extends B { +} From 3981fb038edf348bac3fddb541a0cf1c968a23b3 Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Wed, 1 Feb 2017 15:17:24 +0000 Subject: [PATCH 5/5] Add source locations to virt calls This confers the source location belonging to a virtual call to the code implementing its expanded vtable. --- src/goto-programs/remove_virtual_functions.cpp | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/src/goto-programs/remove_virtual_functions.cpp b/src/goto-programs/remove_virtual_functions.cpp index dccb6c5f23..da9cce5039 100644 --- a/src/goto-programs/remove_virtual_functions.cpp +++ b/src/goto-programs/remove_virtual_functions.cpp @@ -104,6 +104,8 @@ void remove_virtual_functionst::remove_virtual_function( const code_function_callt &code= to_code_function_call(target->code); + const auto &vcall_source_loc=target->source_location; + const exprt &function=code.function(); assert(function.id()==ID_virtual_function); assert(!code.arguments().empty()); @@ -133,6 +135,8 @@ void remove_virtual_functionst::remove_virtual_function( goto_programt final_skip; goto_programt::targett t_final=final_skip.add_instruction(); + t_final->source_location=vcall_source_loc; + t_final->make_skip(); // build the calls and gotos @@ -161,6 +165,7 @@ void remove_virtual_functionst::remove_virtual_function( if(insertit.second) { goto_programt::targett t1=new_code_calls.add_instruction(); + t1->source_location=vcall_source_loc; if(!fun.symbol_expr.get_identifier().empty()) { // call function @@ -179,6 +184,7 @@ void remove_virtual_functionst::remove_virtual_function( insertit.first->second=t1; // goto final goto_programt::targett t3=new_code_calls.add_instruction(); + t3->source_location=vcall_source_loc; t3->make_goto(t_final, true_exprt()); } @@ -188,6 +194,7 @@ void remove_virtual_functionst::remove_virtual_function( { exprt c_id1=constant_exprt(fun.class_id, string_typet()); goto_programt::targett t4=new_code_gotos.add_instruction(); + t4->source_location=vcall_source_loc; t4->make_goto(insertit.first->second, equal_exprt(c_id1, c_id2)); } }