From 81922468d8ff4e8da8a424a83d9861fa3651a76f Mon Sep 17 00:00:00 2001 From: Owen Jones Date: Mon, 19 Feb 2018 17:57:55 +0000 Subject: [PATCH 1/2] Make remove_virtual_function() consistent If there is more than one possible virtual function, we cast the object to the appropriate type in each case, but if there is only one possibility we don't. This PR makes us cast the object when there is only one possibility as well. Note that just because there is only one possibility, it does not mean that the object already has the correct type. Also, if the object is already the correct type then the cast isn't inserted, in all cases. --- .../remove_virtual_functions.cpp | 42 ++++++++++++------- 1 file changed, 28 insertions(+), 14 deletions(-) diff --git a/src/goto-programs/remove_virtual_functions.cpp b/src/goto-programs/remove_virtual_functions.cpp index 7028d0550ce..7c19e2d2071 100644 --- a/src/goto-programs/remove_virtual_functions.cpp +++ b/src/goto-programs/remove_virtual_functions.cpp @@ -96,6 +96,28 @@ void remove_virtual_functionst::remove_virtual_function( virtual_dispatch_fallback_actiont::CALL_LAST_FUNCTION); } +/// Create a concrete function call to replace a virtual one +/// \param call [in/out]: the function call to update +/// \param function_symbol: the function to be called +/// \param ns: namespace +static void create_static_function_call( + code_function_callt &call, + const symbol_exprt &function_symbol, + const namespacet &ns) +{ + call.function() = function_symbol; + // Cast the `this` pointer to the correct type for the new callee: + const auto &callee_type = + to_code_type(ns.lookup(function_symbol.get_identifier()).type); + const code_typet::parametert *this_param = callee_type.get_this(); + INVARIANT( + this_param != nullptr, + "Virtual function callees must have a `this` argument"); + typet need_type = this_param->type(); + if(!type_eq(call.arguments()[0].type(), need_type, ns)) + call.arguments()[0].make_typecast(need_type); +} + void remove_virtual_functionst::remove_virtual_function( goto_programt &goto_program, goto_programt::targett target, @@ -121,8 +143,10 @@ void remove_virtual_functionst::remove_virtual_function( if(functions.begin()->symbol_expr==symbol_exprt()) target->make_skip(); else - to_code_function_call(target->code).function()= - functions.begin()->symbol_expr; + { + create_static_function_call( + to_code_function_call(target->code), functions.front().symbol_expr, ns); + } return; } @@ -187,18 +211,8 @@ void remove_virtual_functionst::remove_virtual_function( { // call function t1->make_function_call(code); - auto &newcall=to_code_function_call(t1->code); - newcall.function()=fun.symbol_expr; - // Cast the `this` pointer to the correct type for the new callee: - const auto &callee_type= - to_code_type(ns.lookup(fun.symbol_expr.get_identifier()).type); - const code_typet::parametert *this_param = callee_type.get_this(); - INVARIANT( - this_param != nullptr, - "Virtual function callees must have a `this` argument"); - typet need_type=this_param->type(); - if(!type_eq(newcall.arguments()[0].type(), need_type, ns)) - newcall.arguments()[0].make_typecast(need_type); + create_static_function_call( + to_code_function_call(t1->code), fun.symbol_expr, ns); } else { From c9f3ea41c7ade3995e317d9277945ed92e2fd6ed Mon Sep 17 00:00:00 2001 From: Owen Jones Date: Thu, 22 Feb 2018 17:20:54 +0000 Subject: [PATCH 2/2] Test casts in remove_virtual_function() Add a test to check that when we replace virtual function calls with static function calls we cast the class to the appropriate type for the static function call, so the argument for the `this` parameter will have the correct type, and also that when a cast is not needed we will not create one. Different code is run if there is only one possible static function or if there is more than one, so we make sure that we test both of these options. --- .../VirtualFunctions$A.class | Bin 0 -> 395 bytes .../VirtualFunctions$B.class | Bin 0 -> 409 bytes .../VirtualFunctions$C.class | Bin 0 -> 348 bytes .../VirtualFunctions.class | Bin 0 -> 729 bytes .../VirtualFunctions.java | 27 ++++++++++++++++++ .../test.desc | 8 ++++++ 6 files changed, 35 insertions(+) create mode 100644 regression/cbmc-java/remove_virtual_function_typecast/VirtualFunctions$A.class create mode 100644 regression/cbmc-java/remove_virtual_function_typecast/VirtualFunctions$B.class create mode 100644 regression/cbmc-java/remove_virtual_function_typecast/VirtualFunctions$C.class create mode 100644 regression/cbmc-java/remove_virtual_function_typecast/VirtualFunctions.class create mode 100644 regression/cbmc-java/remove_virtual_function_typecast/VirtualFunctions.java create mode 100644 regression/cbmc-java/remove_virtual_function_typecast/test.desc diff --git a/regression/cbmc-java/remove_virtual_function_typecast/VirtualFunctions$A.class b/regression/cbmc-java/remove_virtual_function_typecast/VirtualFunctions$A.class new file mode 100644 index 0000000000000000000000000000000000000000..ad6430af4c8f4d427eb9edef339ca70291cfb874 GIT binary patch literal 395 zcmZ8cO-sW-5Ph@FhmFzJ+Wr8c2S31Eyj6r!CXx{H&Bp)bN$}tg@JET0 zSVS_1c{6X`n_<4bKRy9mU>0G3afnHXLqc$=jdoXr!SP8(@K)7>B8*aP)J^k}D|;{V zl9@?b6|&5v)os5eJ@>3@0xb#gwK2-BN?F&6scD*N>l#_E8&f!4nR>olu=0@*-Bpb( z)LOS|XMNfEM!w1z9{dnfKHHzq`PR7AB&9S@$!)$-g=4C(!x04k*@giB1)p=kUBXC= z{^>jDts94&gO2pD!*%>Cz>q6&z4vE6>w4z;#^9fkwnl+{mJ5uq%NX$@fdj_j5B#u5 AZvX%Q literal 0 HcmV?d00001 diff --git a/regression/cbmc-java/remove_virtual_function_typecast/VirtualFunctions$B.class b/regression/cbmc-java/remove_virtual_function_typecast/VirtualFunctions$B.class new file mode 100644 index 0000000000000000000000000000000000000000..62a2eaef1ce57bb4d8dbd2674f450bb329d0af0e GIT binary patch literal 409 zcmZWkO-sW-5Ph3ZlSW%(>s{!<570|*N}(+jgy2QVeH&L?i5tj=|I3r$!5`p{5?^8w zi3>Y#=FNLE%;(qp2Y?w4L)aMkhAI!$cc((>!lfc_%kH znK&sjnWwVUZM`L(`cYQ`Vkr<^8>7lqE~`qB8YihP>qh45#$>fFOf_9zQu!bd-WE-n zskLs$PWrO*C;1{HIB*Cvh;d;_{cN(le} literal 0 HcmV?d00001 diff --git a/regression/cbmc-java/remove_virtual_function_typecast/VirtualFunctions$C.class b/regression/cbmc-java/remove_virtual_function_typecast/VirtualFunctions$C.class new file mode 100644 index 0000000000000000000000000000000000000000..60b7019fc930c779beca8f12515b06ab7a32e61b GIT binary patch literal 348 zcmZWk%SyvQ6g`t?8)I8z`vF21>Owc}DlQBZgwTzW{WK0Z5+^W8{4ZC6i++F~C7ubc z;=r7H&x3nszJI-D;z|I|2Xvq7(@7=2;2M3vJY{f7>hjB=bE{?r{N+*D#jc0F()y!?dtpx_}UMwEdW dCd72;LrmE@|9HR|j#x8t4+|u8eb!S(euUBkVdTW8Hy^4F`@fHa2W*+Nj&u5{M^oe??J{ zc%e$uAhoeg+Oe@i*A`UMOl8_XkNY=)p9yN+8+EUmp^C1We{$9mlz-|-XUBqKW49+L zdGSRcnCa>$_&vDm2gyIx4@qj>*jHgsCEBe2!%}vwQ=|2Ck_}XNI*9yC$5G0{mVX`i zw}O+#m|AbQ##v_q^IE1SQG$i>gf=&k{zR!`B!8mhQF8vqgTxO`wK>@0Xzz#SmR!tY z&P4-rg4xjsqS2e=C5%SZ`99;YGYRss<>{q7^3u1q=pj3dD slSo#mGaX;?E#IVy@A$zE3s@yDV2#^>QAK`Ji#00zvlgc5UHU32Zy