From 7b04a044ab6d948364fc584623efa0f5f48a627f Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Wed, 14 Dec 2016 11:22:40 +0000 Subject: [PATCH 1/3] Use remove_instanceof in driver programs This adds a remove_instanceof call wherever there was an existing remove_virtual_functions call. --- src/cbmc/cbmc_parse_options.cpp | 4 ++++ src/goto-analyzer/goto_analyzer_parse_options.cpp | 4 ++++ src/goto-programs/remove_instanceof.cpp | 6 ++++++ src/goto-programs/remove_instanceof.h | 2 ++ src/symex/symex_parse_options.cpp | 4 ++++ 5 files changed, 20 insertions(+) diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index 87a9c969981..d09b544c678 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -22,6 +22,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #include #include #include @@ -884,7 +885,10 @@ bool cbmc_parse_optionst::process_goto_program( symbol_table, goto_functions, cmdline.isset("pointer-check")); + // Java virtual functions -> explicit dispatch tables: remove_virtual_functions(symbol_table, goto_functions); + // Java instanceof -> clsid comparison: + remove_instanceof(symbol_table, goto_functions); // full slice? if(cmdline.isset("full-slice")) diff --git a/src/goto-analyzer/goto_analyzer_parse_options.cpp b/src/goto-analyzer/goto_analyzer_parse_options.cpp index 8b36f6e71a4..9e9c4a180bb 100644 --- a/src/goto-analyzer/goto_analyzer_parse_options.cpp +++ b/src/goto-analyzer/goto_analyzer_parse_options.cpp @@ -19,6 +19,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #include #include #include @@ -380,7 +381,10 @@ bool goto_analyzer_parse_optionst::process_goto_program( // remove function pointers status() << "Removing function pointers and virtual functions" << eom; remove_function_pointers(goto_model, cmdline.isset("pointer-check")); + // Java virtual functions -> explicit dispatch tables: remove_virtual_functions(goto_model); + // Java instanceof -> clsid comparison: + remove_instanceof(goto_model); // do partial inlining status() << "Partial Inlining" << eom; diff --git a/src/goto-programs/remove_instanceof.cpp b/src/goto-programs/remove_instanceof.cpp index 7930a67f4c2..ee7f5979332 100644 --- a/src/goto-programs/remove_instanceof.cpp +++ b/src/goto-programs/remove_instanceof.cpp @@ -276,3 +276,9 @@ void remove_instanceof( remove_instanceoft rem(symbol_table, goto_functions); rem.lower_instanceof(); } + +void remove_instanceof(goto_modelt &goto_model) +{ + remove_instanceof( + goto_model.symbol_table, goto_model.goto_functions); +} diff --git a/src/goto-programs/remove_instanceof.h b/src/goto-programs/remove_instanceof.h index 6adf67b3dd8..7b4682ba9bf 100644 --- a/src/goto-programs/remove_instanceof.h +++ b/src/goto-programs/remove_instanceof.h @@ -11,10 +11,12 @@ Author: Chris Smowton, chris.smowton@diffblue.com #include #include "goto_functions.h" +#include "goto_model.h" void remove_instanceof( symbol_tablet &symbol_table, goto_functionst &goto_functions); +void remove_instanceof(goto_modelt &model); #endif diff --git a/src/symex/symex_parse_options.cpp b/src/symex/symex_parse_options.cpp index 9930d9cf43a..148f5b646d1 100644 --- a/src/symex/symex_parse_options.cpp +++ b/src/symex/symex_parse_options.cpp @@ -32,6 +32,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #include #include @@ -361,7 +362,10 @@ bool symex_parse_optionst::process_goto_program(const optionst &options) // remove stuff remove_complex(goto_model); remove_vector(goto_model); + // Java virtual functions -> explicit dispatch tables: remove_virtual_functions(goto_model); + // Java instanceof -> clsid comparison: + remove_instanceof(goto_model); rewrite_union(goto_model); adjust_float_expressions(goto_model); From be331e5fdb6e508c13c0fd27164d02d88cfe48f3 Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Thu, 2 Feb 2017 10:28:18 +0000 Subject: [PATCH 2/3] Add instanceof test cases The first five of these are split up pieces of the existing instanceof1, and the final two are new. The first three (testing array and primitive classids) don't work at present; those dealing with ordinary reference types (3-7) do. --- .../cbmc-java/instanceof1/instanceof1.class | Bin 775 -> 535 bytes .../cbmc-java/instanceof1/instanceof1.java | 12 ------------ .../cbmc-java/instanceof2/instanceof2.class | Bin 0 -> 597 bytes .../cbmc-java/instanceof2/instanceof2.java | 7 +++++++ regression/cbmc-java/instanceof2/test.desc | 8 ++++++++ .../cbmc-java/instanceof3/instanceof3.class | Bin 0 -> 560 bytes .../cbmc-java/instanceof3/instanceof3.java | 7 +++++++ regression/cbmc-java/instanceof3/test.desc | 8 ++++++++ .../cbmc-java/instanceof4/instanceof4.class | Bin 0 -> 564 bytes .../cbmc-java/instanceof4/instanceof4.java | 7 +++++++ regression/cbmc-java/instanceof4/test.desc | 8 ++++++++ .../cbmc-java/instanceof5/instanceof5.class | Bin 0 -> 577 bytes .../cbmc-java/instanceof5/instanceof5.java | 8 ++++++++ regression/cbmc-java/instanceof5/test.desc | 8 ++++++++ regression/cbmc-java/instanceof6/A.class | Bin 0 -> 186 bytes regression/cbmc-java/instanceof6/B.class | Bin 0 -> 171 bytes .../cbmc-java/instanceof6/instanceof6.class | Bin 0 -> 633 bytes .../cbmc-java/instanceof6/instanceof6.java | 15 +++++++++++++++ regression/cbmc-java/instanceof6/test.desc | 8 ++++++++ regression/cbmc-java/instanceof7/A.class | Bin 0 -> 186 bytes regression/cbmc-java/instanceof7/B.class | Bin 0 -> 171 bytes .../cbmc-java/instanceof7/instanceof7.class | Bin 0 -> 633 bytes .../cbmc-java/instanceof7/instanceof7.java | 15 +++++++++++++++ regression/cbmc-java/instanceof7/test.desc | 8 ++++++++ 24 files changed, 107 insertions(+), 12 deletions(-) create mode 100644 regression/cbmc-java/instanceof2/instanceof2.class create mode 100644 regression/cbmc-java/instanceof2/instanceof2.java create mode 100644 regression/cbmc-java/instanceof2/test.desc create mode 100644 regression/cbmc-java/instanceof3/instanceof3.class create mode 100644 regression/cbmc-java/instanceof3/instanceof3.java create mode 100644 regression/cbmc-java/instanceof3/test.desc create mode 100644 regression/cbmc-java/instanceof4/instanceof4.class create mode 100644 regression/cbmc-java/instanceof4/instanceof4.java create mode 100644 regression/cbmc-java/instanceof4/test.desc create mode 100644 regression/cbmc-java/instanceof5/instanceof5.class create mode 100644 regression/cbmc-java/instanceof5/instanceof5.java create mode 100644 regression/cbmc-java/instanceof5/test.desc create mode 100644 regression/cbmc-java/instanceof6/A.class create mode 100644 regression/cbmc-java/instanceof6/B.class create mode 100644 regression/cbmc-java/instanceof6/instanceof6.class create mode 100644 regression/cbmc-java/instanceof6/instanceof6.java create mode 100644 regression/cbmc-java/instanceof6/test.desc create mode 100644 regression/cbmc-java/instanceof7/A.class create mode 100644 regression/cbmc-java/instanceof7/B.class create mode 100644 regression/cbmc-java/instanceof7/instanceof7.class create mode 100644 regression/cbmc-java/instanceof7/instanceof7.java create mode 100644 regression/cbmc-java/instanceof7/test.desc diff --git a/regression/cbmc-java/instanceof1/instanceof1.class b/regression/cbmc-java/instanceof1/instanceof1.class index 8d68b98063b413b0689fd44f3879f4ed1888a913..31bd4c733f4127c7e1ba7e2a941c1bf5b5594f63 100644 GIT binary patch delta 300 zcmYL@y-EW?6otQ;oy;V&t8Uip8h>IN2q*|^W#cp0S&AswL{NJ>trrVnUqG-^!GMBd z>r411;++AtnRDiH&v)*%y*1;{@0T~AX5Eu8=wT@xm1D_c7&wNWWmcN)v*v!I>q#@Z z^qQ~DN|ByS&o2(9hexN!TaML?HAXjAs=l;>0+kQLuDI}%D2hznNK}b-CNtE77{#2t zHV%~p=2;LQR(H^GT0Np$ipd8_OZtl0pV4^_Ssk-pRDhI1$=M5ys+98nUuhjV&@b#W auEm)Ohx{IpN0iQX!k(lrXF%rbYq<$nN8t{Qkw_`I{cFpdV|3d$O z&thT|Ni@9rn~d?!RM<+$Br|vJJ#+3kcYgi({sX`oR$SP)k%x<$9Je@TT{!wahk1_M zIV^D8;aGHW7fTG~B@xFmN>muc&r~crec5GTdkonP6{zG1gWXtu%iwH1qrp@-6e?h-HQu)l#F1F-i=emKP9hcb*7d`wb|U~3(2}3j-oK)xaZ+M9+1CD zRpWQ-4ET?3ES8}#(VnB>VHr(^nY77^Adx*8k>{P=H``R2aJ<#0K@xQ_g_{&jrYmC= z$?k%*cS?@E$vy8WXPk0GQ}D? zf<+4$oWL5Q)I5VdMBx<9?g*KmCRsT__KLK|^2^wADR+kaMD`RmF|pQ|euaw1DZQ3v z8ENz2MqriBhvaUPT)iWK`&3OxZiT8IGSyn8`Wv$xRpd~+@VjP=0W&4{8wx{k=QAAp WE3CA^xpz&Jf#p5b6S{8t*Z%@NzMmfe diff --git a/regression/cbmc-java/instanceof1/instanceof1.java b/regression/cbmc-java/instanceof1/instanceof1.java index c21806a7389..600b8da230e 100644 --- a/regression/cbmc-java/instanceof1/instanceof1.java +++ b/regression/cbmc-java/instanceof1/instanceof1.java @@ -2,18 +2,6 @@ class instanceof1 { public static void main(String[] args) { - // absolutely everything is an Object assert args instanceof Object; - assert int.class instanceof Object; - - // args is an array - assert args instanceof Object[]; - - // string literals are strings - assert "" instanceof String; - - // need a negative example, too - Object o=new Object(); - assert ! (o instanceof String); } }; diff --git a/regression/cbmc-java/instanceof2/instanceof2.class b/regression/cbmc-java/instanceof2/instanceof2.class new file mode 100644 index 0000000000000000000000000000000000000000..c56c25e1934f3ec4f2172c2a2b55f74130c6baf7 GIT binary patch literal 597 zcmYjOO;6iE5Pf4iapD+AfIwQlKMs@wNGP|YRS{6B5?@jfQsA_4mS|~MBirG}6GB?gk4D(+gDm14z4;fIx%2=xDrYe zrq<5)FU5`6>y@nxmti@61QU(d3mX)?&t?Wfn7!gYEBwZ}|SjGyWk`cb^MD`>j zos;(Q9zVUau+!(wG}v(lPfKjID`OSO?pr%{m<-}{Q)gJ@g**HKRIZuXIkWk&74R-N zo8w3vbL&r_J5C6reCN|5F=Y&8&JFZ4th8FYhc(3HJ?uYlhA90+uKk4kZ^O1yw#Shr x`J3~oaAt$1QNZ|H*Lo@hRL0#$6ozn}TR8RutW4u|0>jV2^1qrnC(;&^{{e%ObUOe5 literal 0 HcmV?d00001 diff --git a/regression/cbmc-java/instanceof2/instanceof2.java b/regression/cbmc-java/instanceof2/instanceof2.java new file mode 100644 index 00000000000..dfda558a120 --- /dev/null +++ b/regression/cbmc-java/instanceof2/instanceof2.java @@ -0,0 +1,7 @@ +class instanceof2 +{ + public static void main(String[] args) + { + assert int.class instanceof Object; + } +}; diff --git a/regression/cbmc-java/instanceof2/test.desc b/regression/cbmc-java/instanceof2/test.desc new file mode 100644 index 00000000000..5e10735840b --- /dev/null +++ b/regression/cbmc-java/instanceof2/test.desc @@ -0,0 +1,8 @@ +KNOWNBUG +instanceof2.class + +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/regression/cbmc-java/instanceof3/instanceof3.class b/regression/cbmc-java/instanceof3/instanceof3.class new file mode 100644 index 0000000000000000000000000000000000000000..b89a0754f2801bf0b8d3131d192c44a8761f09d9 GIT binary patch literal 560 zcmYk2%TB^T6o&t43x!gZiy+=vxIh-NkR8ToP*)M*wi)#5`YD6a@?F6&)0Un%8Vz_yWw zMPvSlA9s7giJA=MNyFXWE%t-J4;V84XeO3ztYDRTObkB|T4<7L_30M0i7P@G2=@<3 z3q(VDphKLaLf1^uby>EoMkA%uN0Wk9CACbEQB2gH!R|>gOw&IZCmC60kR`23o6zEH z=>ggZ`Pv8c5i+kZ&YqEYS6(glS`-P0B2jXrbg&}LkpJu1h%rDepL~Kjf@$2r&>x{q S7{C3MKLO3&QBxM;7PH^3uWSAQ literal 0 HcmV?d00001 diff --git a/regression/cbmc-java/instanceof3/instanceof3.java b/regression/cbmc-java/instanceof3/instanceof3.java new file mode 100644 index 00000000000..2f2f4e64a58 --- /dev/null +++ b/regression/cbmc-java/instanceof3/instanceof3.java @@ -0,0 +1,7 @@ +class instanceof3 +{ + public static void main(String[] args) + { + assert args instanceof Object[]; + } +}; diff --git a/regression/cbmc-java/instanceof3/test.desc b/regression/cbmc-java/instanceof3/test.desc new file mode 100644 index 00000000000..f04f943dc4d --- /dev/null +++ b/regression/cbmc-java/instanceof3/test.desc @@ -0,0 +1,8 @@ +KNOWNBUG +instanceof3.class + +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/regression/cbmc-java/instanceof4/instanceof4.class b/regression/cbmc-java/instanceof4/instanceof4.class new file mode 100644 index 0000000000000000000000000000000000000000..98ea9b305454aceaee94aa9bc7e8932e7fa2401d GIT binary patch literal 564 zcmZ9I%TB^j5QhKL0tZS}1g&_##09#L4Lga^cv*Q_U`*82p&ZFUY)xBy7+%1&nnE z8AQtW!aWs=dRsOa*abtXsyr2KF_@*bGls;j-;fMrhsu-3otwH0PIWUCZiMm}oYLiC zOWcWaTX@ZKEee#^+|N!rGHh~&?Fl+ zMr>HfGJxv;=?ukTYNx-&eh~NpL-rSqW6{PEmj5tL>MiL;w9t^T+ooI4CJh;?KsE+Q zS|I9Bfevv&98Py7L%E{1Mv+M$IVFpu6wT91evw@7fjv+_Bj}%slZ>P}j8m*zt1#m1 z)FX^83VHJbi7v9QNS^nQde>qj7F+ZZ5e{MU6q#TS(kKjuR$>k?p6AahXmBpNN*Bv74@URJ(}R|w|R^gbcA9yBGPx2k-((>`m+a8DO=;!G%?FfeskJrNgT zz9szQ`C1$*|9D9^cGqIzoo!A@NxW!}N;zb^1}=66ZgvJ9Mg}&U%)HDJJ4Oa(4b3n{1{UZ1lvG9rexJ;| zRKL>Pq|~C2#H1Xc2v=}^X;E^jTPBDjkeOFpl9-pAnxAH-mz7wS$iu+Gz{<$L=m?Yp z@%3{O^V0SGld@8iOBfUwn1D8d03#3s6#{8CAWIfVgG5-hwlgqp1WU66Nj9(`H<082 I@|YMn0nG6r!2kdN literal 0 HcmV?d00001 diff --git a/regression/cbmc-java/instanceof6/B.class b/regression/cbmc-java/instanceof6/B.class new file mode 100644 index 0000000000000000000000000000000000000000..aabe922764087c6ec2ba3f888a811e7ff0d84cdf GIT binary patch literal 171 zcmX^0Z`VEs1_l!bUM>b^1}=66ZgvJ9Mg}&U%)HDJJ4Oa(4b3n{1{UZ1lvG9rexJ;| zRKL>Pq|~C2#H1Xc2v=}^X;E^jTPBDjkeOFpl9-pAnxAH-mz7wS$iu+Gz{<$L=mf-$ v3_!~+4ZNb^1}=66ZgvJ9Mg}&U%)HDJJ4Oa(4b3n{1{UZ1lvG9rexJ;| zRKL>Pq|~C2#H1Xc2v=}^X;E^jTPBDjkeOFpl9-pAnxAH_mz7wS$iu+Gz{<$L=m?Yp z@%3{O^V0SGld@8iOBfUwn1D8d03#3s6#{8CAWIfVgG5-hwlgqp1WU66Nj9(`H<082 I@|YMn0nJn(!Tb^1}=66ZgvJ9Mg}&U%)HDJJ4Oa(4b3n{1{UZ1lvG9rexJ;| zRKL>Pq|~C2#H1Xc2v=}^X;E^jTPBDjkeOFpl9-pAnxAH_mz7wS$iu+Gz{<$L=mf-$ v3o1c)K=0b;E9^-%F)jS28{ySPNMfVLSAUZ+p1T3ohkIvoX6DS9ncsiE{Q$6myB_LjOI-C(vi6z>7wsBqxGpj0 zL0a&Jhntv}xFs;NsM1s?nTezHiAhy&p!))1PoT18B9lE7aF&+e2)NsEUkgljO{8~* zCq13Kw#f{fC=&@Zm-f3y>YZ8}sOWGl$PyDBZrZ|$AXDM-OZ7I-m$)rZ-3kY1CInhVm(IELr%4hg0`>puB^G=v;tpAh zf>*sG9cI+L-|cL2m?E-0;2tnujHU$aRW2-ZR&fJc_83L`8!Ix&Y0gRoM6`-!=+aax}Q-QVRps2 z{|oL1)W?v-t3S_R*TSO$w%tm3w+0VR323wLI`91)Rm>8pq4Wpq5|^6 Date: Fri, 3 Feb 2017 10:47:29 +0000 Subject: [PATCH 3/3] goto-instrument: remove virt calls and RTTI This adds remove_virtual_functions and remove_instanceof calls to goto-instrument mirroring the situation in all other driver programs that use remove_function_pointers already. --- .../goto_instrument_parse_options.cpp | 59 ++++++++++--------- .../goto_instrument_parse_options.h | 2 +- 2 files changed, 32 insertions(+), 29 deletions(-) diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp index 52c65c3ce37..b69d286a467 100644 --- a/src/goto-instrument/goto_instrument_parse_options.cpp +++ b/src/goto-instrument/goto_instrument_parse_options.cpp @@ -17,6 +17,8 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include +#include #include #include #include @@ -246,7 +248,7 @@ int goto_instrument_parse_optionst::doit() if(cmdline.isset("show-value-sets")) { - do_function_pointer_removal(); + do_indirect_call_and_rtti_removal(); do_partial_inlining(); // recalculate numbers, etc. @@ -263,7 +265,7 @@ int goto_instrument_parse_optionst::doit() if(cmdline.isset("show-global-may-alias")) { - do_function_pointer_removal(); + do_indirect_call_and_rtti_removal(); do_partial_inlining(); do_remove_returns(); parameter_assignments(symbol_table, goto_functions); @@ -281,7 +283,7 @@ int goto_instrument_parse_optionst::doit() if(cmdline.isset("show-local-bitvector-analysis")) { - do_function_pointer_removal(); + do_indirect_call_and_rtti_removal(); do_partial_inlining(); parameter_assignments(symbol_table, goto_functions); @@ -305,7 +307,7 @@ int goto_instrument_parse_optionst::doit() if(cmdline.isset("show-custom-bitvector-analysis")) { - do_function_pointer_removal(); + do_indirect_call_and_rtti_removal(); do_partial_inlining(); do_remove_returns(); parameter_assignments(symbol_table, goto_functions); @@ -331,7 +333,7 @@ int goto_instrument_parse_optionst::doit() if(cmdline.isset("show-escape-analysis")) { - do_function_pointer_removal(); + do_indirect_call_and_rtti_removal(); do_partial_inlining(); do_remove_returns(); parameter_assignments(symbol_table, goto_functions); @@ -351,7 +353,7 @@ int goto_instrument_parse_optionst::doit() if(cmdline.isset("custom-bitvector-analysis")) { - do_function_pointer_removal(); + do_indirect_call_and_rtti_removal(); do_partial_inlining(); do_remove_returns(); parameter_assignments(symbol_table, goto_functions); @@ -382,7 +384,7 @@ int goto_instrument_parse_optionst::doit() if(cmdline.isset("show-points-to")) { - do_function_pointer_removal(); + do_indirect_call_and_rtti_removal(); do_partial_inlining(); // recalculate numbers, etc. @@ -399,7 +401,7 @@ int goto_instrument_parse_optionst::doit() if(cmdline.isset("show-intervals")) { - do_function_pointer_removal(); + do_indirect_call_and_rtti_removal(); do_partial_inlining(); // recalculate numbers, etc. @@ -433,7 +435,7 @@ int goto_instrument_parse_optionst::doit() if(!cmdline.isset("inline")) { - do_function_pointer_removal(); + do_indirect_call_and_rtti_removal(); do_partial_inlining(); // recalculate numbers, etc. @@ -460,7 +462,7 @@ int goto_instrument_parse_optionst::doit() if(cmdline.isset("show-reaching-definitions")) { - do_function_pointer_removal(); + do_indirect_call_and_rtti_removal(); const namespacet ns(symbol_table); reaching_definitions_analysist rd_analysis(ns); @@ -483,7 +485,7 @@ int goto_instrument_parse_optionst::doit() if(cmdline.isset("show-dependence-graph")) { - do_function_pointer_removal(); + do_indirect_call_and_rtti_removal(); const namespacet ns(symbol_table); dependence_grapht dependence_graph(ns); @@ -674,7 +676,7 @@ int goto_instrument_parse_optionst::doit() if(cmdline.isset("accelerate")) { - do_function_pointer_removal(); + do_indirect_call_and_rtti_removal(); namespacet ns(symbol_table); @@ -757,7 +759,7 @@ int goto_instrument_parse_optionst::doit() /*******************************************************************\ -Function: goto_instrument_parse_optionst::do_function_pointer_removal +Function: goto_instrument_parse_optionst::do_indirect_call_and_rtti_removal Inputs: @@ -767,9 +769,10 @@ Function: goto_instrument_parse_optionst::do_function_pointer_removal \*******************************************************************/ -void goto_instrument_parse_optionst::do_function_pointer_removal() +void goto_instrument_parse_optionst::do_indirect_call_and_rtti_removal( + bool force) { - if(function_pointer_removal_done) + if(function_pointer_removal_done && !force) return; function_pointer_removal_done=true; @@ -779,6 +782,10 @@ void goto_instrument_parse_optionst::do_function_pointer_removal() symbol_table, goto_functions, cmdline.isset("pointer-check")); + status() << "Virtual function removal" << eom; + remove_virtual_functions(symbol_table, goto_functions); + status() << "Java instanceof removal" << eom; + remove_instanceof(symbol_table, goto_functions); } /*******************************************************************\ @@ -954,7 +961,7 @@ void goto_instrument_parse_optionst::instrument_goto_program() // now do full inlining, if requested if(cmdline.isset("inline")) { - do_function_pointer_removal(); + do_indirect_call_and_rtti_removal(); if(cmdline.isset("show-custom-bitvector-analysis") || cmdline.isset("custom-bitvector-analysis")) @@ -980,7 +987,7 @@ void goto_instrument_parse_optionst::instrument_goto_program() if(cmdline.isset("escape-analysis")) { - do_function_pointer_removal(); + do_indirect_call_and_rtti_removal(); do_partial_inlining(); do_remove_returns(); parameter_assignments(symbol_table, goto_functions); @@ -1009,14 +1016,14 @@ void goto_instrument_parse_optionst::instrument_goto_program() // replace function pointers, if explicitly requested if(cmdline.isset("remove-function-pointers")) - do_function_pointer_removal(); + do_indirect_call_and_rtti_removal(); if(cmdline.isset("function-inline")) { std::string function=cmdline.get_value("function-inline"); assert(!function.empty()); - do_function_pointer_removal(); + do_indirect_call_and_rtti_removal(); status() << "Inlining calls of function `" << function << "'" << eom; @@ -1067,7 +1074,7 @@ void goto_instrument_parse_optionst::instrument_goto_program() if(cmdline.isset("partial-inline")) { - do_function_pointer_removal(); + do_indirect_call_and_rtti_removal(); status() << "Partial inlining" << eom; goto_partial_inline(goto_functions, ns, ui_message_handler, true); @@ -1079,11 +1086,7 @@ void goto_instrument_parse_optionst::instrument_goto_program() // now do full inlining, if requested if(cmdline.isset("inline")) { - status() << "Function Pointer Removal" << eom; - remove_function_pointers( - symbol_table, - goto_functions, - cmdline.isset("pointer-check")); + do_indirect_call_and_rtti_removal(/*force=*/true); if(cmdline.isset("show-custom-bitvector-analysis") || cmdline.isset("custom-bitvector-analysis")) @@ -1099,7 +1102,7 @@ void goto_instrument_parse_optionst::instrument_goto_program() if(cmdline.isset("constant-propagator")) { - do_function_pointer_removal(); + do_indirect_call_and_rtti_removal(); status() << "Propagating Constants" << eom; @@ -1161,7 +1164,7 @@ void goto_instrument_parse_optionst::instrument_goto_program() cmdline.isset("isr") || cmdline.isset("concurrency")) { - do_function_pointer_removal(); + do_indirect_call_and_rtti_removal(); do_partial_inlining(); status() << "Pointer Analysis" << eom; @@ -1400,7 +1403,7 @@ void goto_instrument_parse_optionst::instrument_goto_program() // full slice? if(cmdline.isset("full-slice")) { - do_function_pointer_removal(); + do_indirect_call_and_rtti_removal(); status() << "Performing a full slice" << eom; if(cmdline.isset("property")) diff --git a/src/goto-instrument/goto_instrument_parse_options.h b/src/goto-instrument/goto_instrument_parse_options.h index c8c992f23e7..1d74bd94dbf 100644 --- a/src/goto-instrument/goto_instrument_parse_options.h +++ b/src/goto-instrument/goto_instrument_parse_options.h @@ -96,7 +96,7 @@ class goto_instrument_parse_optionst: void eval_verbosity(); - void do_function_pointer_removal(); + void do_indirect_call_and_rtti_removal(bool force=false); void do_partial_inlining(); void do_remove_returns();