From 04f2faf291961355018a413dc24e1126cdce9c2d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Matthias=20G=C3=BCdemann?= Date: Tue, 5 Dec 2017 11:55:21 +0100 Subject: [PATCH 1/3] Mark GOTO instructions with unresolved virtual calls --- src/goto-programs/remove_virtual_functions.cpp | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/goto-programs/remove_virtual_functions.cpp b/src/goto-programs/remove_virtual_functions.cpp index d4bc305929b..776f928bf5b 100644 --- a/src/goto-programs/remove_virtual_functions.cpp +++ b/src/goto-programs/remove_virtual_functions.cpp @@ -192,6 +192,9 @@ void remove_virtual_functionst::remove_virtual_function( { // No definition for this type; shouldn't be possible... t1->make_assertion(false_exprt()); + t1->source_location.set_comment( + ("cannot find calls for " + + id2string(code.function().get(ID_identifier)))); } insertit.first->second=t1; // goto final From 2b6dc8bf4b7909b2ae92080b3d3ef11a42cd8c97 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Matthias=20G=C3=BCdemann?= Date: Tue, 2 Jan 2018 17:19:58 +0100 Subject: [PATCH 2/3] Resolve concrete function call if no implementation is found --- .../remove_virtual_functions.cpp | 59 +++++++++++++++---- 1 file changed, 47 insertions(+), 12 deletions(-) diff --git a/src/goto-programs/remove_virtual_functions.cpp b/src/goto-programs/remove_virtual_functions.cpp index 776f928bf5b..8179258d149 100644 --- a/src/goto-programs/remove_virtual_functions.cpp +++ b/src/goto-programs/remove_virtual_functions.cpp @@ -8,6 +8,7 @@ Author: Daniel Kroening, kroening@kroening.com /// \file /// Remove Virtual Function (Method) Calls +#include #include "remove_virtual_functions.h" #include "class_hierarchy.h" @@ -47,15 +48,20 @@ class remove_virtual_functionst goto_programt::targett target); void get_functions(const exprt &, dispatch_table_entriest &); + typedef std::function< + resolve_concrete_function_callt::concrete_function_callt( + const irep_idt &, + const irep_idt &)> + function_call_resolvert; void get_child_functions_rec( const irep_idt &, const symbol_exprt &, const irep_idt &, dispatch_table_entriest &, - std::set &visited) const; - exprt get_method( - const irep_idt &class_id, - const irep_idt &component_name) const; + std::set &visited, + const function_call_resolvert &) const; + exprt + get_method(const irep_idt &class_id, const irep_idt &component_name) const; }; remove_virtual_functionst::remove_virtual_functionst( @@ -194,7 +200,8 @@ void remove_virtual_functionst::remove_virtual_function( t1->make_assertion(false_exprt()); t1->source_location.set_comment( ("cannot find calls for " + - id2string(code.function().get(ID_identifier)))); + id2string(code.function().get(ID_identifier)) + " dispatching " + + id2string(fun.class_id))); } insertit.first->second=t1; // goto final @@ -250,6 +257,7 @@ void remove_virtual_functionst::remove_virtual_function( /// `last_method_defn`: the most-derived parent of `this_id` to define the /// requested function /// `component_name`: name of the function searched for +/// `resolve_function_call`: function to resolve abstract method call /// \return `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 @@ -260,7 +268,8 @@ void remove_virtual_functionst::get_child_functions_rec( const symbol_exprt &last_method_defn, const irep_idt &component_name, dispatch_table_entriest &functions, - std::set &visited) const + std::set &visited, + const function_call_resolvert &resolve_function_call) const { auto findit=class_hierarchy.class_map.find(this_id); if(findit==class_hierarchy.class_map.end()) @@ -281,6 +290,21 @@ void remove_virtual_functionst::get_child_functions_rec( { function.symbol_expr=last_method_defn; } + if(function.symbol_expr == symbol_exprt()) + { + const resolve_concrete_function_callt::concrete_function_callt + &resolved_call = resolve_function_call(child, component_name); + if(resolved_call.is_valid()) + { + function.class_id = resolved_call.get_class_identifier(); + const symbolt &called_symbol = + symbol_table.lookup_ref(resolved_call.get_virtual_method_name()); + + function.symbol_expr = called_symbol.symbol_expr(); + function.symbol_expr.set( + ID_C_class, resolved_call.get_class_identifier()); + } + } functions.push_back(function); get_child_functions_rec( @@ -288,7 +312,8 @@ void remove_virtual_functionst::get_child_functions_rec( function.symbol_expr, component_name, functions, - visited); + visited, + resolve_function_call); } } @@ -297,21 +322,30 @@ void remove_virtual_functionst::get_functions( dispatch_table_entriest &functions) { const irep_idt class_id=function.get(ID_C_class); + const std::string class_id_string(id2string(class_id)); const irep_idt component_name=function.get(ID_component_name); + const std::string component_name_string(id2string(component_name)); INVARIANT(!class_id.empty(), "All virtual functions must have a class"); resolve_concrete_function_callt get_virtual_call_target( symbol_table, class_hierarchy); - const resolve_concrete_function_callt::concrete_function_callt & - resolved_call=get_virtual_call_target(class_id, component_name); + const function_call_resolvert resolve_function_call = + [&get_virtual_call_target]( + const irep_idt &class_id, const irep_idt &component_name) { + return get_virtual_call_target(class_id, component_name); + }; + + const resolve_concrete_function_callt::concrete_function_callt + &resolved_call = get_virtual_call_target(class_id, component_name); + dispatch_table_entryt root_function; if(resolved_call.is_valid()) { root_function.class_id=resolved_call.get_class_identifier(); - const symbolt &called_symbol= - *symbol_table.lookup(resolved_call.get_virtual_method_name()); + const symbolt &called_symbol = + symbol_table.lookup_ref(resolved_call.get_virtual_method_name()); root_function.symbol_expr=called_symbol.symbol_expr(); root_function.symbol_expr.set( @@ -330,7 +364,8 @@ void remove_virtual_functionst::get_functions( root_function.symbol_expr, component_name, functions, - visited); + visited, + resolve_function_call); if(root_function.symbol_expr!=symbol_exprt()) functions.push_back(root_function); From 3365054dbe8d9e5c6c4311e51e4da5a9a0a36328 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Matthias=20G=C3=BCdemann?= Date: Wed, 3 Jan 2018 18:53:47 +0100 Subject: [PATCH 3/3] Add regression test --- .../AbstractList$Itr.class | Bin 0 -> 752 bytes .../AbstractList.class | Bin 0 -> 1443 bytes .../AbstractList.java | 42 ++++++++++++++++++ .../ArrayList$Itr.class | Bin 0 -> 731 bytes .../ArrayList$ListItr.class | Bin 0 -> 689 bytes .../removed_virtual_functions/ArrayList.class | Bin 0 -> 831 bytes .../removed_virtual_functions/ArrayList.java | 31 +++++++++++++ .../ArrayListEquals.class | Bin 0 -> 670 bytes .../ArrayListEquals.java | 11 +++++ .../removed_virtual_functions/Iterator.class | Bin 0 -> 238 bytes .../removed_virtual_functions/Iterator.java | 4 ++ .../removed_virtual_functions/List.class | Bin 0 -> 287 bytes .../removed_virtual_functions/List.java | 4 ++ .../ListIterator.class | Bin 0 -> 299 bytes .../ListIterator.java | 5 +++ .../removed_virtual_functions/test.desc | 6 +++ 16 files changed, 103 insertions(+) create mode 100644 regression/cbmc-java/removed_virtual_functions/AbstractList$Itr.class create mode 100644 regression/cbmc-java/removed_virtual_functions/AbstractList.class create mode 100644 regression/cbmc-java/removed_virtual_functions/AbstractList.java create mode 100644 regression/cbmc-java/removed_virtual_functions/ArrayList$Itr.class create mode 100644 regression/cbmc-java/removed_virtual_functions/ArrayList$ListItr.class create mode 100644 regression/cbmc-java/removed_virtual_functions/ArrayList.class create mode 100644 regression/cbmc-java/removed_virtual_functions/ArrayList.java create mode 100644 regression/cbmc-java/removed_virtual_functions/ArrayListEquals.class create mode 100644 regression/cbmc-java/removed_virtual_functions/ArrayListEquals.java create mode 100644 regression/cbmc-java/removed_virtual_functions/Iterator.class create mode 100644 regression/cbmc-java/removed_virtual_functions/Iterator.java create mode 100644 regression/cbmc-java/removed_virtual_functions/List.class create mode 100644 regression/cbmc-java/removed_virtual_functions/List.java create mode 100644 regression/cbmc-java/removed_virtual_functions/ListIterator.class create mode 100644 regression/cbmc-java/removed_virtual_functions/ListIterator.java create mode 100644 regression/cbmc-java/removed_virtual_functions/test.desc diff --git a/regression/cbmc-java/removed_virtual_functions/AbstractList$Itr.class b/regression/cbmc-java/removed_virtual_functions/AbstractList$Itr.class new file mode 100644 index 0000000000000000000000000000000000000000..d9513c3a088ff6cf1c819c0bfa6d5f8231f989df GIT binary patch literal 752 zcma)3%Sr<=6g`=#opv1i^8M_?B5ehA;Z7-tC{zYrw777W)}T}BR5GdPKe^C_2rm2p zKT5ors&wi`hD>r#&OPTO`S^T$2e6BB5++t`#IR~1Z=qnJ$Pic8UQpg)NVx~?KuO+F zt{131+S&JfPt_T+mFQOWoFR7DzZ48<*Ym~c;HE8Pi?@4(f@_{wU2y*!!)cz53R$#k%Ifskm2UQ>k81LO(2K zDpj}3@A!6)`&Zj%?XKwP!zG*EmCw~cQsjwBm2?=2e~E5G3CUGohEBw>oBe_8h+|Km zH9LA^TiV4z9F~IwN*2}`GNS~2G=j#%FeH9V!sv9l&S)D7^lULuOt4Hw>(gtRG!jS> zYSZcj27Q2C+k645y~217Ig=U-ch-oTheNePJsO=thURPp$x+2HjhS!VI?bAGn2+=~ zq4nY+QX0`R{%C1rs5Of@^4A%Ewb;{`*2cfI=BdlT0;L$P7O@l}%Sh8~Qz{c{NWu65 D*4c;m literal 0 HcmV?d00001 diff --git a/regression/cbmc-java/removed_virtual_functions/AbstractList.class b/regression/cbmc-java/removed_virtual_functions/AbstractList.class new file mode 100644 index 0000000000000000000000000000000000000000..80474322ce5f275c94323ed6f2f3a0ec2d662473 GIT binary patch literal 1443 zcmZWo+fEZv6kTUJ)1hT3El{*xKoqsKK;lSBn;3y?db{kD%$$?8%T7|Dzd88rem$YL zDRNOLJh8Zrjh4^^>~3GLu3hc3lYLC zrh2B=dQ~y=EIu5~?wPO6MBXgyBpz<>Sve;;vL&DtCuG-cKIxeh5Jf5$LjtWYDi+-y zwkFWqlZ#l#_pcW#rJVJ^mb`@; zsTr5u80bcjvubnx>xD$bzJ< ziT9-3v`{qDMwY&7me;H|j=PQIKrOhJK62RlMp7N(z8er+ctE9OS3EJSXbG!+hM}+?_3Ae(08SVQ5u>y zJAmdniXFqd8vh3E1iHZ5=m|Om-eGpErX*;nX=*$2?oL#Uo3KCHSEpFtP(F3vdsodg9)QIMW68yjT#6V&E7{WKeS%!zMt z=1(~&$xw<7%wdS1t3*rFbB&rLyHXp4)P`x}e;Chj9XHtYAU1K6n#bid#>^^4lv*`Y zj;tC#@-IHd_&DtY@aY|A26SX+{zk><47=C!7X+K_*sF%W$c3T E7h9DGw*UYD literal 0 HcmV?d00001 diff --git a/regression/cbmc-java/removed_virtual_functions/AbstractList.java b/regression/cbmc-java/removed_virtual_functions/AbstractList.java new file mode 100644 index 00000000000..d4c8baf09f5 --- /dev/null +++ b/regression/cbmc-java/removed_virtual_functions/AbstractList.java @@ -0,0 +1,42 @@ +public abstract class AbstractList + implements List +{ + public Iterator iterator() { + return new Itr(); + } + + public ListIterator listIterator() { + return listIterator(0); + } + + public boolean equals(Object o) { + if (o == this) + return true; + if (!(o instanceof List)) + return false; + + ListIterator e1 = listIterator(); + ListIterator e2 = ((List) o).listIterator(); + while (e1.hasNext() && e2.hasNext()) { + E o1 = e1.next(); + Object o2 = e2.next(); + if (!(o1==null ? o2==null : o1.equals(o2))) + return false; + } + return !(e1.hasNext() || e2.hasNext()); + } + + private class Itr implements Iterator { + Itr() { + } + + public boolean hasNext() { + return false; + } + + public E next() { + return null; + } + + } +} diff --git a/regression/cbmc-java/removed_virtual_functions/ArrayList$Itr.class b/regression/cbmc-java/removed_virtual_functions/ArrayList$Itr.class new file mode 100644 index 0000000000000000000000000000000000000000..13a922d28f78a7b8e36a34b33f8b10a713adb8ed GIT binary patch literal 731 zcma)(%}&BV6ot>UNTF1y2>$<|vY?oN3wIh4Lo~rOxX`$8H{b+nu$XBv@=h*vVN6{3 z06vuQPEi!yn5Lb%XU=^0Oy}+WH^F?!T-4gPQw|b;x-F}<*&bjnd{VB#2o>3Qa#WIo^W;-B1ja4$QU{nJ!MJH-RLn zCe4na(F2&}?I*DEGqlIZlTuo=k|*yREUGQqqtt2GG|o&YS*jRjk^AJ7SCIj}$}MzcjMManWVG@6u3#~RYmJ^+?H Be@XxV literal 0 HcmV?d00001 diff --git a/regression/cbmc-java/removed_virtual_functions/ArrayList$ListItr.class b/regression/cbmc-java/removed_virtual_functions/ArrayList$ListItr.class new file mode 100644 index 0000000000000000000000000000000000000000..1914266e79e0fc9ffa9e22ca539a3d1ad4898d5f GIT binary patch literal 689 zcmZ9JO-tlJ5Qg7Q#)&h@==klr>-T_PARfGp42UQUgk?by)?2HMwv35%GNS*FvZF4cp8XbVh##XjDBqGyZJy_3UcYrClTuVwPb zsCylE*~4AmI1{KG>#InnUBgk`Y?QU{0IJO}rzj)S*koMJQ$3Em=0Y85`_7U6qPB13 zy$n!>7ho7G9##d$`q9t#2-FHK-@#xH0ta_&S6u1mV~Ibl1a1VPUbmh2FCBivs8Fr) z_Lsg(>u+woKx}UPgY!(+h0k*&53xL8a*Zc2odJA$b$Tqs7{;kh@E#Cql^P~#1*Vvt zw`tMZnBzY2%<1J!sb|!@(&&N!+?=n*H%6RVKg%1Zi9$tFb_0aP0O27@Y z5~v1g8mYrXW?7U8cwwArTd4HnG}e9U+MS_5>2Puu32cUO8oi%hjv{p`M+q~Ha59$3 zP^#F>XUUTO9Fw*d4wRBthS?QpE-SCT%+w!{{O!>ux_B zj54j{SQ{_7*4mmc^G_yIHI9yBb1)ml-rpKh6>F#p)QfB@-;gqe*W6E0;O=ks;n^Fd zzjuo5at@7PSDL@T% z#>P_S9%lmgvBj^*;EvhIsQq7XKJB^JaKCfrV! extends AbstractList + implements List +{ + public ListIterator listIterator() { + return new ListItr(0); + } + public ListIterator listIterator(int index) { + return new ListItr(index); + } + private class ListItr extends Itr implements ListIterator { + ListItr(int index) { + super(); + } + + public boolean hasPrevious() { + return false; + } + } + + private class Itr implements Iterator { + Itr() { + } + + public boolean hasNext() { + return false; + } + public E next() { + return null; + } + } +} diff --git a/regression/cbmc-java/removed_virtual_functions/ArrayListEquals.class b/regression/cbmc-java/removed_virtual_functions/ArrayListEquals.class new file mode 100644 index 0000000000000000000000000000000000000000..13472296078dc579e9210dd9e614dbf541851613 GIT binary patch literal 670 zcmZuu+fEu$6kTT+7(~2{K($syeSy}LwCNj!q%mz`GPVyG6MZ|3Cpa)2>@YO(5BdxJ z2VVM85>5I6ev>h-Goye_=V7nC*WPFC%iP{y{{`>?yE$aAVc}H{1~#3N5%%cm~oX>G&l${(`k%b-&` z3?kK0VZF(23#~}Hy(4)U55`3W=2~7SkkK&Y@Ov{e{9i&3mTUEgp{qW7df&o7E4|f? z^RSSm^dy%@89O}Jgh=)mSf0-LwcS;2#EYo-HUh=U%oa(uUOmGO()>&MGaz&$+Brrw zq9CSUk0E}?=^Sk)CV5Hv`J{ljz=$`;5=HdmpTrcga0BCXjMUMa{XZ~&A#ILQBl0G+ zmQB=tmLn`v*`}v;%gNhEU8*p l1) { + ArrayList al = new ArrayList(); + if(l1.equals(al)) + return 1; + else + return 0; + } + +} diff --git a/regression/cbmc-java/removed_virtual_functions/Iterator.class b/regression/cbmc-java/removed_virtual_functions/Iterator.class new file mode 100644 index 0000000000000000000000000000000000000000..b75d211c3b63fbb68cb335d2f0e749eefff7a3d4 GIT binary patch literal 238 zcmX^0Z`VEs1_l!bK6VBkb_QNX2KJ1^V!zai5=I7Q4b3P<29`W9M?^!@Co8cmQ9ma! zFJ0e1DJwO(#F~+TGdMFnFR`SwD3y_cRYNnx6)2`*<7$Pe)(%sMk%22XzqBYh)h#mz zsGrxfB(*59B)>=xWDz3+2aM0iAb@T)8zTcF0~65Y3=B*xK&LXWFfagVRt7epI6Fv` PfdhykEKUY4un0E*QD`;Q literal 0 HcmV?d00001 diff --git a/regression/cbmc-java/removed_virtual_functions/Iterator.java b/regression/cbmc-java/removed_virtual_functions/Iterator.java new file mode 100644 index 00000000000..a67327494f8 --- /dev/null +++ b/regression/cbmc-java/removed_virtual_functions/Iterator.java @@ -0,0 +1,4 @@ +public interface Iterator { + boolean hasNext(); + E next(); +} diff --git a/regression/cbmc-java/removed_virtual_functions/List.class b/regression/cbmc-java/removed_virtual_functions/List.class new file mode 100644 index 0000000000000000000000000000000000000000..e16c33ebb51d2d52ac0adbdd15af2e774431e592 GIT binary patch literal 287 zcmX^0Z`VEs1_l!bK6VBkb_QNX2A-VE;u6o2)S|?a{31pM0S!$bA0!cLMh4E{%=Em( zlG377Mg~zdX`2vNYdfGCK@Cp~ePZZhFvS`+u2w!-iDilUIf;4c`u<5-smUeQc9=qp z3|ztarA5i9Zkahi%Q-;~(*tQ_WMBcYfzCxYhK-Sdk%0;5MFs{Y7DfhU1{NTn6~tp; U1M}J8d=8)(M23@r3#@`00Q+@BoB#j- literal 0 HcmV?d00001 diff --git a/regression/cbmc-java/removed_virtual_functions/List.java b/regression/cbmc-java/removed_virtual_functions/List.java new file mode 100644 index 00000000000..b3cd2e3e6d5 --- /dev/null +++ b/regression/cbmc-java/removed_virtual_functions/List.java @@ -0,0 +1,4 @@ +public interface List { + ListIterator listIterator(); + ListIterator listIterator(int index); +} diff --git a/regression/cbmc-java/removed_virtual_functions/ListIterator.class b/regression/cbmc-java/removed_virtual_functions/ListIterator.class new file mode 100644 index 0000000000000000000000000000000000000000..203568c50e23432296f85a967b34c6f3778d21f7 GIT binary patch literal 299 zcmZWkNeaS15Ue)QaW{gGNG|3g2rAwbgrI_+yp1wwLP%gT5#Q#)2lyzl-9YrvRCiTZ zFW1}o0-%SsKvSS4;1I+?W^;8i1k3d{gc{dNt&U-uX9PQWN*&h=B6*a4ER(&z*hXq+ zhJ?y0+$YlHS`mt_x1KQ9A58}Tz2ko>m>H#|N%e?*V|G?oX|8u_8pb@X9fX extends Iterator { + boolean hasNext(); + boolean hasPrevious(); + E next(); +} diff --git a/regression/cbmc-java/removed_virtual_functions/test.desc b/regression/cbmc-java/removed_virtual_functions/test.desc new file mode 100644 index 00000000000..36b47b39757 --- /dev/null +++ b/regression/cbmc-java/removed_virtual_functions/test.desc @@ -0,0 +1,6 @@ +CORE +ArrayListEquals.class +--lazy-methods --java-max-vla-length 48 --unwind 8 --java-unwind-enum-static --trace --cover location --function ArrayListEquals.check2 --show-goto-functions +e2 . ArrayList\$Itr.hasNext:\(\)Z\(\); +-- +e2 . ListIterator.hasNext:\(\)Z\(\);