From ddf6c92561f061d6829fb1886ba7be97614b78fe Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Thu, 16 Nov 2017 23:52:30 +0000 Subject: [PATCH 1/3] Simplify equalities of constants Enables some pruning of virtual function dispatch in goto-symex --- src/util/simplify_expr_int.cpp | 22 ++++++++++++++-------- 1 file changed, 14 insertions(+), 8 deletions(-) diff --git a/src/util/simplify_expr_int.cpp b/src/util/simplify_expr_int.cpp index 995447c1c7e..623a43fdfd2 100644 --- a/src/util/simplify_expr_int.cpp +++ b/src/util/simplify_expr_int.cpp @@ -1215,11 +1215,6 @@ bool simplify_exprt::simplify_inequality(exprt &expr) (expr.id()==ID_equal || expr.id()==ID_notequal)) return simplify_inequality_pointer_object(expr); - // first see if we compare to a constant - - bool op0_is_const=tmp0.is_constant(); - bool op1_is_const=tmp1.is_constant(); - ns.follow_symbol(tmp0.type()); ns.follow_symbol(tmp1.type()); @@ -1229,9 +1224,20 @@ bool simplify_exprt::simplify_inequality(exprt &expr) if(tmp1.type().id()==ID_c_enum_tag) tmp1.type()=ns.follow_tag(to_c_enum_tag_type(tmp1.type())); + const auto tmp0_const = expr_try_dynamic_cast(tmp0); + const auto tmp1_const = expr_try_dynamic_cast(tmp1); + // are _both_ constant? - if(op0_is_const && op1_is_const) + if(tmp0_const && tmp1_const) { + if(expr.id() == ID_equal || expr.id() == ID_notequal) + { + + bool equal = (tmp0_const->get_value() == tmp1_const->get_value()); + expr.make_bool(expr.id() == ID_equal ? equal : !equal); + return false; + } + if(tmp0.type().id()==ID_bool) { bool v0=tmp0.is_true(); @@ -1347,7 +1353,7 @@ bool simplify_exprt::simplify_inequality(exprt &expr) return false; } } - else if(op0_is_const) + else if(tmp0_const) { // we want the constant on the RHS @@ -1366,7 +1372,7 @@ bool simplify_exprt::simplify_inequality(exprt &expr) simplify_inequality_constant(expr); return false; } - else if(op1_is_const) + else if(tmp1_const) { // one is constant return simplify_inequality_constant(expr); From c7d8ea647c1c7ed29d3f7e4fa73e82c37a9e8749 Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Fri, 17 Nov 2017 00:38:57 +0000 Subject: [PATCH 2/3] Tests for simplifying ID_string equalities --- regression/cbmc-java/virtual8/A.class | Bin 0 -> 222 bytes regression/cbmc-java/virtual8/B.class | Bin 0 -> 207 bytes regression/cbmc-java/virtual8/C.class | Bin 0 -> 207 bytes regression/cbmc-java/virtual8/D.class | Bin 0 -> 164 bytes regression/cbmc-java/virtual8/E.class | Bin 0 -> 164 bytes regression/cbmc-java/virtual8/Test.class | Bin 0 -> 354 bytes regression/cbmc-java/virtual8/Test.java | 29 ++++++++++++++++++++ regression/cbmc-java/virtual8/test.desc | 11 ++++++++ regression/cbmc-java/virtual9/A.class | Bin 0 -> 222 bytes regression/cbmc-java/virtual9/B.class | Bin 0 -> 207 bytes regression/cbmc-java/virtual9/C.class | Bin 0 -> 207 bytes regression/cbmc-java/virtual9/D.class | Bin 0 -> 164 bytes regression/cbmc-java/virtual9/E.class | Bin 0 -> 164 bytes regression/cbmc-java/virtual9/Test.class | Bin 0 -> 456 bytes regression/cbmc-java/virtual9/Test.java | 33 +++++++++++++++++++++++ regression/cbmc-java/virtual9/test.desc | 13 +++++++++ 16 files changed, 86 insertions(+) create mode 100644 regression/cbmc-java/virtual8/A.class create mode 100644 regression/cbmc-java/virtual8/B.class create mode 100644 regression/cbmc-java/virtual8/C.class create mode 100644 regression/cbmc-java/virtual8/D.class create mode 100644 regression/cbmc-java/virtual8/E.class create mode 100644 regression/cbmc-java/virtual8/Test.class create mode 100644 regression/cbmc-java/virtual8/Test.java create mode 100644 regression/cbmc-java/virtual8/test.desc create mode 100644 regression/cbmc-java/virtual9/A.class create mode 100644 regression/cbmc-java/virtual9/B.class create mode 100644 regression/cbmc-java/virtual9/C.class create mode 100644 regression/cbmc-java/virtual9/D.class create mode 100644 regression/cbmc-java/virtual9/E.class create mode 100644 regression/cbmc-java/virtual9/Test.class create mode 100644 regression/cbmc-java/virtual9/Test.java create mode 100644 regression/cbmc-java/virtual9/test.desc diff --git a/regression/cbmc-java/virtual8/A.class b/regression/cbmc-java/virtual8/A.class new file mode 100644 index 0000000000000000000000000000000000000000..680ceb8db5c63d43c9afdd4e7e415ccfaa5ba982 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%IB2#Q|3;36=$_KvyONRLlvK IWMbd~0CT4qssI20 literal 0 HcmV?d00001 diff --git a/regression/cbmc-java/virtual8/C.class b/regression/cbmc-java/virtual8/C.class new file mode 100644 index 0000000000000000000000000000000000000000..6391b1ca05c4835b79cb53ba5edb24acb3fba99d 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^jTPBFZ8IoFDqL-CemdL}v!obSNz~}b^1}=66ZgvJ9Mg}&U%)HDJJ4Oa(4b3n{1{UZ1lvG9rexJ;| zRKL>Pq|~C2#H1Xc2v=}^X;E^jTPBFZ8IoFDqL-CemdL}v!obSNz~~CZP7DeROhB_i ofDwp+GC-OQ$dU!pAQ4ur?F@_?!P4wNk_{{<10*?sJSGNC05#hfNdN!< literal 0 HcmV?d00001 diff --git a/regression/cbmc-java/virtual8/Test.class b/regression/cbmc-java/virtual8/Test.class new file mode 100644 index 0000000000000000000000000000000000000000..f90d0ac64b8cfb7dde24b4a84087a8e75f353d93 GIT binary patch literal 354 zcmYL@OH0E*6ot=C(o8c>AHE;pqPtqqZrmwCQM$3{!Xmg#>L@8~3Tfm2a$`loAK;G? z&qS~cb6@k_Gw1u~;|stk4m1?jH8!xRu%+R4`WJWsQ9aUt;ANB4r@a`tEi zjX|2(n_`;Sd>AJaPJ+D1`o!CV-dPDw<1`cKyIGNsY(I5OG_>=@$vA$A4XTI~_6+tB z3FOMaphgu(2%3)RPU7sjdz*~yh$HFoKA}Z#ipD{s;zSrVyF+GSu5^}=R~CXb#;_dn zXD83vp)KY=^bOt$)$sV}BjAZp|5rZd+~KuP_zz12*PVA%R%>;xfR?H}rd(>U_t5+W D6_PB| literal 0 HcmV?d00001 diff --git a/regression/cbmc-java/virtual8/Test.java b/regression/cbmc-java/virtual8/Test.java new file mode 100644 index 00000000000..7d5e5b08396 --- /dev/null +++ b/regression/cbmc-java/virtual8/Test.java @@ -0,0 +1,29 @@ +public class Test { + public static void runF(A x) { + x.f(); + } + + public static void main() { + A y = new D(); + runF(y); + } +} + +class A { + void f() { } +} + + +class B extends A { + void f() { } +} + +class C extends A { + void f() { } +} + +class D extends C { +} + +class E extends B { +} diff --git a/regression/cbmc-java/virtual8/test.desc b/regression/cbmc-java/virtual8/test.desc new file mode 100644 index 00000000000..774005ac03d --- /dev/null +++ b/regression/cbmc-java/virtual8/test.desc @@ -0,0 +1,11 @@ +CORE +Test.class +--program-only +^EXIT=0$ +^SIGNAL=0$ +C\.f +-- +A\.f +B\.f +D\.f +E\.f diff --git a/regression/cbmc-java/virtual9/A.class b/regression/cbmc-java/virtual9/A.class new file mode 100644 index 0000000000000000000000000000000000000000..145301d5c90c1d24d74e775db4de337459e9813e 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%IZA#Q|3;36=$_KvyOPRLlvK IWMbd~0CbxfvH$=8 literal 0 HcmV?d00001 diff --git a/regression/cbmc-java/virtual9/C.class b/regression/cbmc-java/virtual9/C.class new file mode 100644 index 0000000000000000000000000000000000000000..abbca958c2d485ab777a0d38a2d6e43f2f2062bc 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^jTPBFZ8IoFDqL-CemdL}v!obSNz~}sLm>4(#HR2db literal 0 HcmV?d00001 diff --git a/regression/cbmc-java/virtual9/E.class b/regression/cbmc-java/virtual9/E.class new file mode 100644 index 0000000000000000000000000000000000000000..90b2361dc032366210e451a283eb09c614dfa36f GIT binary patch literal 164 zcmX^0Z`VEs1_l!bUM>b^1}=66ZgvJ9Mg}&U%)HDJJ4Oa(4b3n{1{UZ1lvG9rexJ;| zRKL>Pq|~C2#H1Xc2v=}^X;E^jTPBFZ8IoFDqL-CemdL}v!obSNz~~CZP7DeROhB_i ofDwp+GC-OQ$dU!pAQ4ur?F@_?!P4wNk_{}V03pgxtr>J?G4vJ6}JaD*z{`nJ`c^v4dTKJrgR50wohE38qmN*cYe}^s^ug;&X!P z9NrML_Uz6lIw5Sb*L*A!PX06Oi3yd(Ne_&hbzB4rMJh zp)jdJ<7FU^jemKcamm!kZLIVcWS3BH7tq{SSWBch)!m~H2-!(VOiOGF2!5rL-xm0n WWwx#|yUC0J Date: Fri, 17 Nov 2017 16:33:29 +0000 Subject: [PATCH 3/3] Remove obsolete equal/notequal cases in simplify_expr --- src/util/simplify_expr_int.cpp | 42 ++++------------------------------ 1 file changed, 5 insertions(+), 37 deletions(-) diff --git a/src/util/simplify_expr_int.cpp b/src/util/simplify_expr_int.cpp index 623a43fdfd2..4d065f6d49b 100644 --- a/src/util/simplify_expr_int.cpp +++ b/src/util/simplify_expr_int.cpp @@ -1238,32 +1238,12 @@ bool simplify_exprt::simplify_inequality(exprt &expr) return false; } - if(tmp0.type().id()==ID_bool) - { - bool v0=tmp0.is_true(); - bool v1=tmp1.is_true(); - - if(expr.id()==ID_equal) - { - expr.make_bool(v0==v1); - return false; - } - else if(expr.id()==ID_notequal) - { - expr.make_bool(v0!=v1); - return false; - } - } - else if(tmp0.type().id()==ID_fixedbv) + if(tmp0.type().id() == ID_fixedbv) { fixedbvt f0(to_constant_expr(tmp0)); fixedbvt f1(to_constant_expr(tmp1)); - if(expr.id()==ID_notequal) - expr.make_bool(f0!=f1); - else if(expr.id()==ID_equal) - expr.make_bool(f0==f1); - else if(expr.id()==ID_ge) + if(expr.id() == ID_ge) expr.make_bool(f0>=f1); else if(expr.id()==ID_le) expr.make_bool(f0<=f1); @@ -1281,11 +1261,7 @@ bool simplify_exprt::simplify_inequality(exprt &expr) ieee_floatt f0(to_constant_expr(tmp0)); ieee_floatt f1(to_constant_expr(tmp1)); - if(expr.id()==ID_notequal) - expr.make_bool(f0!=f1); - else if(expr.id()==ID_equal) - expr.make_bool(f0==f1); - else if(expr.id()==ID_ge) + if(expr.id() == ID_ge) expr.make_bool(f0>=f1); else if(expr.id()==ID_le) expr.make_bool(f0<=f1); @@ -1308,11 +1284,7 @@ bool simplify_exprt::simplify_inequality(exprt &expr) if(to_rational(tmp1, r1)) return true; - if(expr.id()==ID_notequal) - expr.make_bool(r0!=r1); - else if(expr.id()==ID_equal) - expr.make_bool(r0==r1); - else if(expr.id()==ID_ge) + if(expr.id() == ID_ge) expr.make_bool(r0>=r1); else if(expr.id()==ID_le) expr.make_bool(r0<=r1); @@ -1335,11 +1307,7 @@ bool simplify_exprt::simplify_inequality(exprt &expr) if(to_integer(tmp1, v1)) return true; - if(expr.id()==ID_notequal) - expr.make_bool(v0!=v1); - else if(expr.id()==ID_equal) - expr.make_bool(v0==v1); - else if(expr.id()==ID_ge) + if(expr.id() == ID_ge) expr.make_bool(v0>=v1); else if(expr.id()==ID_le) expr.make_bool(v0<=v1);