From 0c4c649057db4d7e645c264883c7b5dacca4b016 Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Tue, 23 Aug 2016 09:04:22 +0100 Subject: [PATCH 1/5] Don't use potentially-invalid downcasts to read an object's clsid if possible By using a pointer with a type that corresponds to a real object (at least in Java, where a virtual call against a method of type X guarantees that the instance parameter has at least that type), we make it less likely that a byte-extract opcode is used to retrieve the class-id field. --- .../remove_virtual_functions.cpp | 33 ++++++++++++------- 1 file changed, 22 insertions(+), 11 deletions(-) diff --git a/src/goto-programs/remove_virtual_functions.cpp b/src/goto-programs/remove_virtual_functions.cpp index a0d9f551c2e..0198527bd06 100644 --- a/src/goto-programs/remove_virtual_functions.cpp +++ b/src/goto-programs/remove_virtual_functions.cpp @@ -170,28 +170,39 @@ void remove_virtual_functionst::remove_virtual_function( goto_programt new_code_calls; goto_programt new_code_gotos; + // Get a pointer from which we can extract a clsid. + // If it's already a pointer to an object of some sort, just use it; + // if it's void* then use the parent of all possible candidates, + // which by the nature of get_functions happens to be the last candidate. + + exprt this_expr=code.arguments()[0]; + assert(this_expr.type().id()==ID_pointer && + "Non-pointer this-arg in remove-virtuals?"); + const auto& points_to=this_expr.type().subtype(); + if(points_to==empty_typet()) + { + symbol_typet symbol_type(functions.back().class_id); + this_expr=typecast_exprt(this_expr, pointer_typet(symbol_type)); + } + exprt deref=dereference_exprt(this_expr, this_expr.type().subtype()); + exprt c_id2=build_class_identifier(deref); + for(const auto &fun : functions) { // call function goto_programt::targett t1=new_code_calls.add_instruction(); t1->make_function_call(code); - to_code_function_call(t1->code).function()=fun.symbol_expr; + auto& newcall=to_code_function_call(t1->code); + newcall.function()=fun.symbol_expr; + pointer_typet need_type(symbol_typet(fun.class_id)); + if(newcall.arguments()[0].type()!=need_type) + newcall.arguments()[0].make_typecast(need_type); // goto final goto_programt::targett t3=new_code_calls.add_instruction(); t3->make_goto(t_final, true_exprt()); - exprt this_expr=code.arguments()[0]; - if(this_expr.type().id()!=ID_pointer || - this_expr.type().id()!=ID_struct) - { - symbol_typet symbol_type(fun.class_id); - this_expr=typecast_exprt(this_expr, pointer_typet(symbol_type)); - } - - exprt deref=dereference_exprt(this_expr, this_expr.type().subtype()); exprt c_id1=constant_exprt(fun.class_id, string_typet()); - exprt c_id2=build_class_identifier(deref); goto_programt::targett t4=new_code_gotos.add_instruction(); t4->make_goto(t1, equal_exprt(c_id1, c_id2)); From ef7bdfe5d3a6f91f53ed43590b4db157fc5cd182 Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Fri, 9 Sep 2016 15:00:39 +0100 Subject: [PATCH 2/5] Include child types when creating a virtual function dispatch tree Previously if A had a subtype B which did *not* override a particular function, instances of B would run the default (least-derived) version of the function instead of A's version. --- .../remove_virtual_functions.cpp | 91 +++++++++++++------ 1 file changed, 62 insertions(+), 29 deletions(-) diff --git a/src/goto-programs/remove_virtual_functions.cpp b/src/goto-programs/remove_virtual_functions.cpp index 0198527bd06..0f11bcc0111 100644 --- a/src/goto-programs/remove_virtual_functions.cpp +++ b/src/goto-programs/remove_virtual_functions.cpp @@ -49,6 +49,8 @@ class remove_virtual_functionst typedef std::vector functionst; void get_functions(const exprt &, functionst &); + void get_child_functions_rec(const irep_idt &, const symbol_exprt &, + const irep_idt &, functionst &); exprt get_method(const irep_idt &class_id, const irep_idt &component_name); exprt build_class_identifier(const exprt &); @@ -189,14 +191,22 @@ void remove_virtual_functionst::remove_virtual_function( for(const auto &fun : functions) { - // call function goto_programt::targett t1=new_code_calls.add_instruction(); - 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.class_id)); - if(newcall.arguments()[0].type()!=need_type) - newcall.arguments()[0].make_typecast(need_type); + if(fun.symbol_expr.get_identifier()!=irep_idt()) + { + // 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(newcall.arguments()[0].type()!=need_type) + newcall.arguments()[0].make_typecast(need_type); + } + else + { + // No definition for this type; shouldn't be possible... + t1->make_assertion(false_exprt()); + } // goto final goto_programt::targett t3=new_code_calls.add_instruction(); @@ -235,6 +245,35 @@ void remove_virtual_functionst::remove_virtual_function( target->make_skip(); } +void remove_virtual_functionst::get_child_functions_rec( + const irep_idt &this_id, + const symbol_exprt &last_method_defn, + const irep_idt &component_name, + functionst &functions) +{ + auto findit=class_hierarchy.class_map.find(this_id); + if(findit==class_hierarchy.class_map.end()) + return; + + for(const auto & child : findit->second.children) + { + exprt method=get_method(child, component_name); + functiont function; + function.class_id=child; + if(method.is_not_nil()) + { + function.symbol_expr=to_symbol_expr(method); + function.symbol_expr.set(ID_C_class, child); + } + else { + function.symbol_expr=last_method_defn; + } + functions.push_back(function); + + get_child_functions_rec(child,function.symbol_expr,component_name,functions); + } +} + /*******************************************************************\ Function: remove_virtual_functionst::get_functions @@ -254,23 +293,7 @@ void remove_virtual_functionst::get_functions( const irep_idt class_id=function.get(ID_C_class); const irep_idt component_name=function.get(ID_component_name); assert(!class_id.empty()); - - // iterate over all children, transitively - std::vector children= - class_hierarchy.get_children_trans(class_id); - - for(const auto &child : children) - { - exprt method=get_method(child, component_name); - if(method.is_not_nil()) - { - functiont function; - function.class_id=child; - function.symbol_expr=to_symbol_expr(method); - function.symbol_expr.set(ID_C_class, child); - functions.push_back(function); - } - } + functiont root_function; // Start from current class, go to parents until something // is found. @@ -280,11 +303,9 @@ void remove_virtual_functionst::get_functions( exprt method=get_method(c, component_name); if(method.is_not_nil()) { - functiont function; - function.class_id=c; - function.symbol_expr=to_symbol_expr(method); - function.symbol_expr.set(ID_C_class, c); - functions.push_back(function); + root_function.class_id=c; + root_function.symbol_expr=to_symbol_expr(method); + root_function.symbol_expr.set(ID_C_class, c); break; // abort } @@ -294,6 +315,18 @@ void remove_virtual_functionst::get_functions( if(parents.empty()) break; c=parents.front(); } + + if(root_function.class_id==irep_idt()) + { + // No definition here; this is an abstract function. + root_function.class_id=class_id; + } + + // iterate over all children, transitively + get_child_functions_rec(class_id,root_function.symbol_expr,component_name,functions); + + functions.push_back(root_function); + } /*******************************************************************\ From 381eec4c670dfb05109f05b90c16fb0d1f1dbd0a Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Fri, 9 Sep 2016 15:08:50 +0100 Subject: [PATCH 3/5] Call least-derived virtual function for unknown clsid Previously this would fall through to the first child when e.g. dispatching against a stub type with unknown class hierarchy position, which might assume the `this` pointer to have a more-derived type than it actually does. --- src/goto-programs/remove_virtual_functions.cpp | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/src/goto-programs/remove_virtual_functions.cpp b/src/goto-programs/remove_virtual_functions.cpp index 0f11bcc0111..33ae7554c72 100644 --- a/src/goto-programs/remove_virtual_functions.cpp +++ b/src/goto-programs/remove_virtual_functions.cpp @@ -189,6 +189,7 @@ void remove_virtual_functionst::remove_virtual_function( exprt deref=dereference_exprt(this_expr, this_expr.type().subtype()); exprt c_id2=build_class_identifier(deref); + goto_programt::targett last_function; for(const auto &fun : functions) { goto_programt::targett t1=new_code_calls.add_instruction(); @@ -208,6 +209,8 @@ void remove_virtual_functionst::remove_virtual_function( t1->make_assertion(false_exprt()); } + last_function=t1; + // goto final goto_programt::targett t3=new_code_calls.add_instruction(); t3->make_goto(t_final, true_exprt()); @@ -218,6 +221,11 @@ void remove_virtual_functionst::remove_virtual_function( 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 386aad1dd782d7a6e4a633e939a49ee603da7d4f Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Wed, 14 Dec 2016 10:39:24 +0000 Subject: [PATCH 4/5] Add test for virtual dispatch against child type --- regression/cbmc-java/virtual6/A.class | Bin 0 -> 485 bytes regression/cbmc-java/virtual6/A.java | 40 ++++++++++++++++++++++++ regression/cbmc-java/virtual6/B.class | Bin 0 -> 211 bytes regression/cbmc-java/virtual6/C.class | Bin 0 -> 161 bytes regression/cbmc-java/virtual6/test.desc | 8 +++++ 5 files changed, 48 insertions(+) create mode 100644 regression/cbmc-java/virtual6/A.class create mode 100644 regression/cbmc-java/virtual6/A.java create mode 100644 regression/cbmc-java/virtual6/B.class create mode 100644 regression/cbmc-java/virtual6/C.class create mode 100644 regression/cbmc-java/virtual6/test.desc diff --git a/regression/cbmc-java/virtual6/A.class b/regression/cbmc-java/virtual6/A.class new file mode 100644 index 0000000000000000000000000000000000000000..7fae215b0ebab4360f1f89f106e47a69ae2a3e44 GIT binary patch literal 485 zcmYjMO-lk%6g_V~b=0&pbNq67Sn6qFYBbRv-1p(v0^S$wrfLh$X z5zy+xdsiTS>G^JJGU&LYYp2uaMmz+R1}Ou_^9jXbhs1d~MW9J?F)V!a{^vHJ%fmdK62D3nb)ax$pRo<*QE5?T)d@fMI?FP(dw3SfiW@ zL_ySdW)Saen1Iy?mI^!Sv6s{=QBoD{jrBiI=aj%QtK>~-We_jsQ0`_>n{#MHy)}nH zG^<+fmDkwfkq%Nb``2&mR`n@jd$O9gR@H6&1EE_PObLROm>kR>A|_~OGhl_?KJBYW m;t(kuBaKr^o+FPHveVEOsF+BaNSRpG^&hC5Xq*mo*M0#`3p=m? literal 0 HcmV?d00001 diff --git a/regression/cbmc-java/virtual6/A.java b/regression/cbmc-java/virtual6/A.java new file mode 100644 index 00000000000..a98dc88009d --- /dev/null +++ b/regression/cbmc-java/virtual6/A.java @@ -0,0 +1,40 @@ + +public class A { + + int f() { + return 1; + } + + public void main(int unknown) { + + A a = new A(); + B b = new B(); + C c = new C(); + A callee; + switch(unknown) { + case 1: + callee = a; + break; + case 2: + callee = b; + break; + default: + callee = c; + break; + } + + callee.f(); + + } + +} + +class B extends A { + + int f() { + return 2; + } + +} + +class C extends B {} diff --git a/regression/cbmc-java/virtual6/B.class b/regression/cbmc-java/virtual6/B.class new file mode 100644 index 0000000000000000000000000000000000000000..f810a84fbd64e185c69209a22ec1df9725e8978c GIT binary patch literal 211 zcmYj~y$ZrW5QJy*t1+5h5CS%8VPz>o6a+zR6#GO^IMD=x@u_UA1PdR)hZ5(kT-cr2 z*$?*pdA83qi0h zs&c31+QeQmJf_z)gaen*l${`k#TTY5HZLGZ*P#m49Xud+8iCL0{lb{8hC01L+f;*E O?v3-G>v9Xs1&uFVcNr4^ literal 0 HcmV?d00001 diff --git a/regression/cbmc-java/virtual6/C.class b/regression/cbmc-java/virtual6/C.class new file mode 100644 index 0000000000000000000000000000000000000000..026d126c765345716244e6ad698d0b022ab65ddc GIT binary patch literal 161 zcmX^0Z`VEs1_l!bUM>b^1}=66ZgvJ9Mg}&U%)HDJJ4Oa(4b3n{1{UZ1lvG9rexJ;| zRKL>Pq|~C2#H1Xc2v=}^X;E^jTPBFZ=BSsISeD4cz{0@F$iV0f#7+zf3`{_SL4Xm6 lfiggv4akxO(jXC5t?dkq8^O}-K#~nCr~xE7fIKD!P5_BH7V!W8 literal 0 HcmV?d00001 diff --git a/regression/cbmc-java/virtual6/test.desc b/regression/cbmc-java/virtual6/test.desc new file mode 100644 index 00000000000..8432c7b2303 --- /dev/null +++ b/regression/cbmc-java/virtual6/test.desc @@ -0,0 +1,8 @@ +CORE +A.class +--function A.main --show-goto-functions +^EXIT=0$ +^SIGNAL=0$ +IF "java::C".*THEN GOTO +IF "java::B".*THEN GOTO +IF "java::A".*THEN GOTO From 065bfb9743871c623c32a94d00163a18feda823b Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Wed, 4 Jan 2017 12:58:00 +0000 Subject: [PATCH 5/5] Style and documentation fixes --- .../remove_virtual_functions.cpp | 70 ++++++++++++++----- 1 file changed, 54 insertions(+), 16 deletions(-) diff --git a/src/goto-programs/remove_virtual_functions.cpp b/src/goto-programs/remove_virtual_functions.cpp index 33ae7554c72..4da7d62631b 100644 --- a/src/goto-programs/remove_virtual_functions.cpp +++ b/src/goto-programs/remove_virtual_functions.cpp @@ -7,6 +7,7 @@ Author: Daniel Kroening, kroening@kroening.com \*******************************************************************/ #include +#include #include "class_hierarchy.h" #include "remove_virtual_functions.h" @@ -43,15 +44,23 @@ class remove_virtual_functionst class functiont { public: + functiont() {} + explicit functiont(const irep_idt& _class_id) : + class_id(_class_id) + {} + symbol_exprt symbol_expr; irep_idt class_id; }; typedef std::vector functionst; void get_functions(const exprt &, functionst &); - void get_child_functions_rec(const irep_idt &, const symbol_exprt &, - const irep_idt &, functionst &); - exprt get_method(const irep_idt &class_id, const irep_idt &component_name); + void get_child_functions_rec( + const irep_idt &, const symbol_exprt &, + const irep_idt &, functionst &) const; + exprt get_method( + const irep_idt &class_id, + const irep_idt &component_name) const; exprt build_class_identifier(const exprt &); }; @@ -180,7 +189,7 @@ void remove_virtual_functionst::remove_virtual_function( exprt this_expr=code.arguments()[0]; assert(this_expr.type().id()==ID_pointer && "Non-pointer this-arg in remove-virtuals?"); - const auto& points_to=this_expr.type().subtype(); + const auto &points_to=this_expr.type().subtype(); if(points_to==empty_typet()) { symbol_typet symbol_type(functions.back().class_id); @@ -193,14 +202,14 @@ void remove_virtual_functionst::remove_virtual_function( for(const auto &fun : functions) { goto_programt::targett t1=new_code_calls.add_instruction(); - if(fun.symbol_expr.get_identifier()!=irep_idt()) + if(!fun.symbol_expr.get_identifier().empty()) { // call function t1->make_function_call(code); - auto& newcall=to_code_function_call(t1->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(newcall.arguments()[0].type()!=need_type) + if(!type_eq(newcall.arguments()[0].type(), need_type, ns)) newcall.arguments()[0].make_typecast(need_type); } else @@ -253,11 +262,33 @@ void remove_virtual_functionst::remove_virtual_function( target->make_skip(); } +/*******************************************************************\ + +Function: remove_virtual_functionst::get_child_functions_rec + + Inputs: `this_id`: class name + `last_method_defn`: the most-derived parent of `this_id` + to define the requested function + `component_name`: name of the function searched for + + Outputs: `functions` is assigned a list of {class name, function symbol} + pairs indicating that if `this` is of the given class, then the + call will target the given function. Thus if A <: B <: C and A + and C provide overrides of `f` (but B does not), + get_child_functions_rec("C", C.f, "f") -> [{"C", C.f}, + {"B", C.f}, + {"A", A.f}] + + Purpose: Used by get_functions to track the most-derived parent that + provides an override of a given function. + +\*******************************************************************/ + void remove_virtual_functionst::get_child_functions_rec( const irep_idt &this_id, const symbol_exprt &last_method_defn, const irep_idt &component_name, - functionst &functions) + functionst &functions) const { auto findit=class_hierarchy.class_map.find(this_id); if(findit==class_hierarchy.class_map.end()) @@ -266,19 +297,23 @@ void remove_virtual_functionst::get_child_functions_rec( for(const auto & child : findit->second.children) { exprt method=get_method(child, component_name); - functiont function; - function.class_id=child; + functiont function(child); if(method.is_not_nil()) { function.symbol_expr=to_symbol_expr(method); function.symbol_expr.set(ID_C_class, child); } - else { + else + { function.symbol_expr=last_method_defn; } functions.push_back(function); - get_child_functions_rec(child,function.symbol_expr,component_name,functions); + get_child_functions_rec( + child, + function.symbol_expr, + component_name, + functions); } } @@ -324,17 +359,20 @@ void remove_virtual_functionst::get_functions( c=parents.front(); } - if(root_function.class_id==irep_idt()) + if(root_function.class_id.empty()) { // No definition here; this is an abstract function. root_function.class_id=class_id; } // iterate over all children, transitively - get_child_functions_rec(class_id,root_function.symbol_expr,component_name,functions); + get_child_functions_rec( + class_id, + root_function.symbol_expr, + component_name, + functions); functions.push_back(root_function); - } /*******************************************************************\ @@ -351,7 +389,7 @@ Function: remove_virtual_functionst::get_method exprt remove_virtual_functionst::get_method( const irep_idt &class_id, - const irep_idt &component_name) + const irep_idt &component_name) const { irep_idt id=id2string(class_id)+"."+ id2string(component_name);