From 28c6477e0e7d8409dcf065c13c1ecf05276a0c95 Mon Sep 17 00:00:00 2001
From: thk123 <thomas@diffblue.com>
Date: Thu, 8 Mar 2018 14:04:00 +0000
Subject: [PATCH 1/2] Adding utility for getting symbols out of the symbol
 table

---
 unit/testing-utils/require_symbol.cpp | 23 +++++++++++++++++++++++
 unit/testing-utils/require_symbol.h   | 26 ++++++++++++++++++++++++++
 2 files changed, 49 insertions(+)
 create mode 100644 unit/testing-utils/require_symbol.cpp
 create mode 100644 unit/testing-utils/require_symbol.h

diff --git a/unit/testing-utils/require_symbol.cpp b/unit/testing-utils/require_symbol.cpp
new file mode 100644
index 00000000000..fcac85b593f
--- /dev/null
+++ b/unit/testing-utils/require_symbol.cpp
@@ -0,0 +1,23 @@
+/*******************************************************************\
+
+ Module: Unit test utilities
+
+ Author: DiffBlue Limited. All rights reserved.
+
+\*******************************************************************/
+
+#include "require_symbol.h"
+#include "catch.hpp"
+
+/// Verify whether a given identifier is found in the symbol table and return it
+/// \param symbol_table: The symbol table to look in
+/// \param symbol_identifier: The name of the symbol
+const symbolt &require_symbol::require_symbol_exists(
+  const symbol_tablet &symbol_table,
+  const irep_idt &symbol_identifier)
+{
+  const symbolt *found_symbol = symbol_table.lookup(symbol_identifier);
+  INFO("Looking for symbol: " + id2string(symbol_identifier));
+  REQUIRE(found_symbol != nullptr);
+  return *found_symbol;
+}
diff --git a/unit/testing-utils/require_symbol.h b/unit/testing-utils/require_symbol.h
new file mode 100644
index 00000000000..4523636e17f
--- /dev/null
+++ b/unit/testing-utils/require_symbol.h
@@ -0,0 +1,26 @@
+/*******************************************************************\
+
+ Module: Unit test utilities
+
+ Author: DiffBlue Limited. All rights reserved.
+
+\*******************************************************************/
+
+#ifndef CPROVER_TESTING_UTILS_REQUIRE_SYMBOL_H
+#define CPROVER_TESTING_UTILS_REQUIRE_SYMBOL_H
+
+#include <util/symbol.h>
+#include <util/symbol_table.h>
+
+/// \file
+/// Helper functions for getting symbols from the symbol table during unit tests
+
+// NOLINTNEXTLINE(readability/namespace)
+namespace require_symbol
+{
+const symbolt &require_symbol_exists(
+  const symbol_tablet &symbol_table,
+  const irep_idt &symbol_identifier);
+}
+
+#endif // CPROVER_TESTING_UTILS_REQUIRE_SYMBOL_H

From e1961d854d6daf42229566d950f36dc6bb53f0e3 Mon Sep 17 00:00:00 2001
From: thk123 <thomas@diffblue.com>
Date: Thu, 8 Mar 2018 14:06:14 +0000
Subject: [PATCH 2/2] Adding unit tests for verifying the behaviour of lazy
 methods on lambdas

---
 .../ci_lazy_methods/lazy_load_lambdas.cpp     | 239 ++++++++++++++++++
 .../ExternalLambdaAccessor.class              | Bin 0 -> 1864 bytes
 .../ExternalLambdaAccessor.java               |  39 +++
 .../lambda_examples/ExternalLambdas.class     | Bin 0 -> 3838 bytes
 4 files changed, 278 insertions(+)
 create mode 100644 unit/java_bytecode/ci_lazy_methods/lazy_load_lambdas.cpp
 create mode 100644 unit/java_bytecode/java_bytecode_parser/lambda_examples/ExternalLambdaAccessor.class
 create mode 100644 unit/java_bytecode/java_bytecode_parser/lambda_examples/ExternalLambdaAccessor.java
 create mode 100644 unit/java_bytecode/java_bytecode_parser/lambda_examples/ExternalLambdas.class

diff --git a/unit/java_bytecode/ci_lazy_methods/lazy_load_lambdas.cpp b/unit/java_bytecode/ci_lazy_methods/lazy_load_lambdas.cpp
new file mode 100644
index 00000000000..67d993a3304
--- /dev/null
+++ b/unit/java_bytecode/ci_lazy_methods/lazy_load_lambdas.cpp
@@ -0,0 +1,239 @@
+/*******************************************************************\
+
+ Module: Unit tests for parsing generic classes
+
+ Author: DiffBlue Limited. All rights reserved.
+
+\*******************************************************************/
+
+#include <testing-utils/catch.hpp>
+#include <testing-utils/load_java_class.h>
+#include <testing-utils/require_symbol.h>
+
+SCENARIO(
+  "Lazy load lambda methods",
+  "[core][java_bytecode][ci_lazy_methods][lambdas][!mayfail]")
+{
+  GIVEN("A class with some locally declared lambdas")
+  {
+    const symbol_tablet symbol_table = load_java_class_lazy(
+      "LocalLambdas",
+      "./java_bytecode/java_bytecode_parser/lambda_examples/",
+      "LocalLambdas.test");
+
+    THEN("Then the lambdas should be loaded")
+    {
+      std::string lambda_name_prefix = "java::LocalLambdas.lambda$test$";
+      require_symbol::require_symbol_exists(
+        symbol_table, lambda_name_prefix + "0:()V");
+
+      require_symbol::require_symbol_exists(
+        symbol_table,
+        lambda_name_prefix + "1:(ILjava/lang/Object;LDummyGeneric;)V");
+
+      require_symbol::require_symbol_exists(
+        symbol_table,
+        lambda_name_prefix + "2:([I[Ljava/lang/Object;[LDummyGeneric;)V");
+
+      require_symbol::require_symbol_exists(
+        symbol_table, lambda_name_prefix + "3:()I");
+
+      require_symbol::require_symbol_exists(
+        symbol_table, lambda_name_prefix + "4:()Ljava/lang/Object;");
+
+      require_symbol::require_symbol_exists(
+        symbol_table, lambda_name_prefix + "5:()LDummyGeneric;");
+
+      require_symbol::require_symbol_exists(
+        symbol_table, lambda_name_prefix + "6:()[I");
+
+      require_symbol::require_symbol_exists(
+        symbol_table, lambda_name_prefix + "7:()[Ljava/lang/Object;");
+
+      require_symbol::require_symbol_exists(
+        symbol_table, lambda_name_prefix + "8:()[LDummyGeneric;");
+
+      require_symbol::require_symbol_exists(
+        symbol_table, lambda_name_prefix + "9:(I)I");
+
+      require_symbol::require_symbol_exists(
+        symbol_table,
+        lambda_name_prefix + "10:(Ljava/lang/Object;)Ljava/lang/Object;");
+
+      require_symbol::require_symbol_exists(
+        symbol_table, lambda_name_prefix + "11:(LDummyGeneric;)LDummyGeneric;");
+    }
+  }
+  GIVEN("A class with some member lambdas")
+  {
+    const symbol_tablet symbol_table = load_java_class_lazy(
+      "MemberLambdas",
+      "./java_bytecode/java_bytecode_parser/lambda_examples/",
+      "MemberLambdas.test");
+
+    THEN("Then the lambdas should be loaded")
+    {
+      std::string lambda_name_prefix = "java::MemberLambdas.lambda$new$";
+      require_symbol::require_symbol_exists(
+        symbol_table, lambda_name_prefix + "0:()V");
+
+      require_symbol::require_symbol_exists(
+        symbol_table,
+        lambda_name_prefix + "1:(ILjava/lang/Object;LDummyGeneric;)V");
+
+      require_symbol::require_symbol_exists(
+        symbol_table,
+        lambda_name_prefix + "2:([I[Ljava/lang/Object;[LDummyGeneric;)V");
+
+      require_symbol::require_symbol_exists(
+        symbol_table, lambda_name_prefix + "3:()I");
+
+      require_symbol::require_symbol_exists(
+        symbol_table, lambda_name_prefix + "4:()Ljava/lang/Object;");
+
+      require_symbol::require_symbol_exists(
+        symbol_table, lambda_name_prefix + "5:()LDummyGeneric;");
+
+      require_symbol::require_symbol_exists(
+        symbol_table, lambda_name_prefix + "6:()[I");
+
+      require_symbol::require_symbol_exists(
+        symbol_table, lambda_name_prefix + "7:()[Ljava/lang/Object;");
+
+      require_symbol::require_symbol_exists(
+        symbol_table, lambda_name_prefix + "8:()[LDummyGeneric;");
+
+      require_symbol::require_symbol_exists(
+        symbol_table, lambda_name_prefix + "9:()I");
+
+      require_symbol::require_symbol_exists(
+        symbol_table, lambda_name_prefix + "10:()Ljava/lang/Object;");
+
+      require_symbol::require_symbol_exists(
+        symbol_table, lambda_name_prefix + "11:()LDummyGeneric;");
+    }
+  }
+  GIVEN("A class with some static lambdas")
+  {
+    const symbol_tablet symbol_table = load_java_class_lazy(
+      "StaticLambdas",
+      "./java_bytecode/java_bytecode_parser/lambda_examples/",
+      "StaticLambdas.test");
+
+    THEN("Then the lambdas should be loaded")
+    {
+      std::string lambda_name_prefix = "java::StaticLambdas.lambda$static$";
+      require_symbol::require_symbol_exists(
+        symbol_table, lambda_name_prefix + "0:()V");
+
+      require_symbol::require_symbol_exists(
+        symbol_table,
+        lambda_name_prefix + "1:(ILjava/lang/Object;LDummyGeneric;)V");
+
+      require_symbol::require_symbol_exists(
+        symbol_table,
+        lambda_name_prefix + "2:([I[Ljava/lang/Object;[LDummyGeneric;)V");
+
+      require_symbol::require_symbol_exists(
+        symbol_table, lambda_name_prefix + "3:()I");
+
+      require_symbol::require_symbol_exists(
+        symbol_table, lambda_name_prefix + "4:()Ljava/lang/Object;");
+
+      require_symbol::require_symbol_exists(
+        symbol_table, lambda_name_prefix + "5:()LDummyGeneric;");
+
+      require_symbol::require_symbol_exists(
+        symbol_table, lambda_name_prefix + "6:()[I");
+
+      require_symbol::require_symbol_exists(
+        symbol_table, lambda_name_prefix + "7:()[Ljava/lang/Object;");
+
+      require_symbol::require_symbol_exists(
+        symbol_table, lambda_name_prefix + "8:()[LDummyGeneric;");
+
+      require_symbol::require_symbol_exists(
+        symbol_table, lambda_name_prefix + "9:()I");
+
+      require_symbol::require_symbol_exists(
+        symbol_table, lambda_name_prefix + "10:()Ljava/lang/Object;");
+
+      require_symbol::require_symbol_exists(
+        symbol_table, lambda_name_prefix + "11:()LDummyGeneric;");
+    }
+  }
+  GIVEN("A class with some outer member lambdas")
+  {
+    const symbol_tablet symbol_table = load_java_class_lazy(
+      "OuterMemberLambdas$Inner",
+      "./java_bytecode/java_bytecode_parser/lambda_examples/",
+      "OuterMemberLambdas$Inner.test");
+
+    THEN("Then the lambdas should be loaded")
+    {
+      std::string lambda_name_prefix =
+        "java::OuterMemberLambdas$Inner.lambda$new$";
+
+      require_symbol::require_symbol_exists(
+        symbol_table, lambda_name_prefix + "0:()I");
+
+      require_symbol::require_symbol_exists(
+        symbol_table, lambda_name_prefix + "1:()Ljava/lang/Object;");
+
+      require_symbol::require_symbol_exists(
+        symbol_table, lambda_name_prefix + "2:()LDummyGeneric;");
+    }
+  }
+}
+
+SCENARIO(
+  "Lazy load lambda methods in seperate class",
+  "[core][java_bytecode][ci_lazy_methods][lambdas][!mayfail]")
+{
+  const symbol_tablet symbol_table = load_java_class_lazy(
+    "ExternalLambdaAccessor",
+    "./java_bytecode/java_bytecode_parser/lambda_examples/",
+    "ExternalLambdaAccessor.test");
+
+  THEN("Then the lambdas should be loaded")
+  {
+    std::string lambda_name_prefix = "java::ExternalLambdas.lambda$new$";
+    require_symbol::require_symbol_exists(
+      symbol_table, lambda_name_prefix + "0:()V");
+
+    require_symbol::require_symbol_exists(
+      symbol_table,
+      lambda_name_prefix + "1:(ILjava/lang/Object;LDummyGeneric;)V");
+
+    require_symbol::require_symbol_exists(
+      symbol_table,
+      lambda_name_prefix + "2:([I[Ljava/lang/Object;[LDummyGeneric;)V");
+
+    require_symbol::require_symbol_exists(
+      symbol_table, lambda_name_prefix + "3:()I");
+
+    require_symbol::require_symbol_exists(
+      symbol_table, lambda_name_prefix + "4:()Ljava/lang/Object;");
+
+    require_symbol::require_symbol_exists(
+      symbol_table, lambda_name_prefix + "5:()LDummyGeneric;");
+
+    require_symbol::require_symbol_exists(
+      symbol_table, lambda_name_prefix + "6:()[I");
+
+    require_symbol::require_symbol_exists(
+      symbol_table, lambda_name_prefix + "7:()[Ljava/lang/Object;");
+
+    require_symbol::require_symbol_exists(
+      symbol_table, lambda_name_prefix + "8:()[LDummyGeneric;");
+
+    require_symbol::require_symbol_exists(
+      symbol_table, lambda_name_prefix + "9:()I");
+
+    require_symbol::require_symbol_exists(
+      symbol_table, lambda_name_prefix + "10:()Ljava/lang/Object;");
+
+    require_symbol::require_symbol_exists(
+      symbol_table, lambda_name_prefix + "11:()LDummyGeneric;");
+  }
+}
diff --git a/unit/java_bytecode/java_bytecode_parser/lambda_examples/ExternalLambdaAccessor.class b/unit/java_bytecode/java_bytecode_parser/lambda_examples/ExternalLambdaAccessor.class
new file mode 100644
index 0000000000000000000000000000000000000000..7b4ae9aaa020ff99b6906f9786ca7cf96fd82e33
GIT binary patch
literal 1864
zcmaJ>>r&G|6#f<qfoA2RfLzK&1>54KDtM!yA~(^f2nu2qO~V4gHtnP>12g{97jniK
zraI#T_!vHj<JqK*CN1X2<~x@?=X~EL`}6m=9{?th52FuJ1+g$15N)9)u3`)qCAy^I
zGOkFJP;nL4B)YC*91{}VP;nEtB)YBQ4kjf^s+hvGM0Zu(!+nWnR6M|}M00YPm&<~J
zMFkHTnx;(4EZ$`}5sR-egl2PFf}u?_E%CIJO$+;lp3acxl$JB}%$jbS(yll|#a*+&
z(4);C6oqZ+8BNcoxAYmq5QRd{PEx(1C=?kORp<z06(}5D&6R9JESR!IfBh;~_Vj(7
zqaP8P%b!x<Si&O(k2y3%IG*6Cf@jiL=6H@31*_6{!SNDn3f86Ziem$>6{Mu`hT|<Z
z6}*$idk!6G1%@=XI0Uv8>_}sm!^EC~57NkRWU<C!;WbANn+)ClsjBoD+U4kpjBf2D
zo~8GMK}zs~nayW}D-=Vkw)&4vitvAJ24((07^Nbqqvmy6&sO(!Xv@+RB)jXPt!)7p
z!$@pN3yzS~=1SS@;i9mFZ5l~==<T{~>xa(nYW;3)#`F1_bk_4TL}RI?RBf+RZL=<0
z6ic?XY@1oLXzqJT^l2+jz_fPUA-oKt)^l9U`EHjODpgm+wy=d|9ADMTs8iL8F?7b_
zwQLxM-Qj7*)x4np!7PZaijr03&INhYWK!qh0H2y1Iux3~cTx;}Zg)=@=P0Uuhk||m
zY1DKe(A1wm|7t9rA}K3fJTd;?#h+HEi$8%*in`R3cJz2@eG^23JZrRb(rJ>>0N?tF
zbTP?^0#Zi;QoAb8>UsKh>1V8jJ#K+;^ms15Oq@k8-Tv}v09}BH&^ka?g5HeYjble(
zU!3qDtxb-z3qyptn}A^|0<_?qxA_-BPVDn{G;AE<#N)BA2$j*uK%hxstPCY2aWj*+
z#lhh+REBl(@-j}ksI`nX7qyqs;i6MzoOV%X8C@>w_V%9f_V&1Y|IR*%R+_UH%|y6^
xs1DG)aazYQh-qT9NKBp+mlQD(I8Qh02o5odPq^UmZN^86j8GjqU0NG(;Sb&7_z3_2

literal 0
HcmV?d00001

diff --git a/unit/java_bytecode/java_bytecode_parser/lambda_examples/ExternalLambdaAccessor.java b/unit/java_bytecode/java_bytecode_parser/lambda_examples/ExternalLambdaAccessor.java
new file mode 100644
index 00000000000..bdeaa7e4c48
--- /dev/null
+++ b/unit/java_bytecode/java_bytecode_parser/lambda_examples/ExternalLambdaAccessor.java
@@ -0,0 +1,39 @@
+class ExternalLambdas
+{
+  int memberPrimitive;
+  Object memberReference;
+  DummyGeneric<Integer> memberSpecalisedGeneric;
+
+  public SimpleLambda simpleLambda = () -> { /*NOP*/ };
+  public ParameterLambda paramLambda = (int primitive, Object reference, DummyGeneric<Integer> specalisedGeneric) -> {};
+  public ArrayParameterLambda arrayParamLambda = (int[] primitive, Object[] reference, DummyGeneric<Integer>[] specalisedGeneric) -> {};
+  public ReturningLambdaPrimitive returnPrimitiveLambda = () -> { return 1; };
+  public ReturningLambdaReference returnReferenceLambda = () -> { return null; };
+  public ReturningLambdaSpecalisedGeneric returningSpecalisedGenericLambda = () -> { return null; };
+  public ReturningLambdaPrimitiveArray returnPrimitiveArrayLambda = () -> { return null; };
+  public ReturningLambdaReferenceArray returnReferenceArrayLambda = () -> { return null; };
+  public ReturningLambdaSpecalisedGenericArray returningSpecalisedGenericArrayLambda = () -> { return null; };
+  public ReturningLambdaPrimitive returnPrimitiveLambdaCapture = () -> { return memberPrimitive; };
+  public ReturningLambdaReference returnReferenceLambdaCapture = () -> { return memberReference; };
+  public ReturningLambdaSpecalisedGeneric returningSpecalisedGenericLambdaCapture = () -> { return memberSpecalisedGeneric; };
+}
+
+public class ExternalLambdaAccessor
+{
+  public static void test()
+  {
+    ExternalLambdas e = new ExternalLambdas();
+    e.simpleLambda.Execute();
+    e.paramLambda.Execute(4, null, null);
+    e.arrayParamLambda.Execute(null, null, null);
+    e.returnPrimitiveLambda.Execute();
+    e.returnReferenceLambda.Execute();
+    e.returningSpecalisedGenericLambda.Execute();
+    e.returnPrimitiveArrayLambda.Execute();
+    e.returnReferenceArrayLambda.Execute();
+    e.returningSpecalisedGenericArrayLambda.Execute();
+    e.returnPrimitiveLambdaCapture.Execute();
+    e.returnReferenceLambdaCapture.Execute();
+    e.returningSpecalisedGenericLambdaCapture.Execute();
+  }
+}
diff --git a/unit/java_bytecode/java_bytecode_parser/lambda_examples/ExternalLambdas.class b/unit/java_bytecode/java_bytecode_parser/lambda_examples/ExternalLambdas.class
new file mode 100644
index 0000000000000000000000000000000000000000..06e1b460efe8a7d7fa3386fa202564560f7dadeb
GIT binary patch
literal 3838
zcmbVO`F9gl6#k|y4NYHZ8uo%vO0j7bO4*@+Ld#MNiw)vZ6{qP?29imfObd12_kG{@
zT~tsIMaBIWkH<gB<9BD$X);ME$DH%#eeb^SF7M{PJM-7S=gtFIg+IesfP+!u!5Ulw
zBMJ?N1({J)ASEarMJ2L=ZjGV}j-cTvrr@}s(I~2MhoC#72;m+<_eL=l4+wfNiW)pD
z=#ePGcudgaQPko|K~Kr!X?Z*&k7q-8E`;Yb)TfQ~fMM^m&9v#5BZda8*O&GghYZ`W
zl9Wc{NAwZBBc)qI9eW3k7)hr~!)#AEku{Qf%FG#qI}FRP&7_8D@t)yydNjW#wI*Q>
zS-LZ9)7Ijm&5Z??do9NpGVHF+)KEDyolO~WJv}g}i^W92n)|g`-PY4%+YRx3vNRmS
z_C#bvblcWPUHKSoR(y*uE8@<y4F+fVc^Fe@jQ6=4rZwb=d<GrlmHaeKsN^%K)Z}@h
z!IHd<={E<RmN03jF%YqPurUh@gBJX-UD~+1AK8V~i)mC}GVv*jEVTv$DLKkmK=T9V
z@s851XT74yZ~K7+wp%BTC%~-UXj-PTSwm&4?SO`=?#v)-vOaEF#-3rh3;Xqflw0u`
zR`mhhHf5a`Ryl{woQ8(@w&SccOHX;mbIeFx%B|EE%Q)83*~#jQwH4KQkg{CE3{uKm
zD^*}=y&EU5WT9{!BZ#&22hA5!*0MT<GKu*$OaN&C`>TuHttwuwEMBhA&>HLSE#oQ>
zpk%uyJKkt2#BGf|-eabhvB8t(O500)z;tm$OnytOxAf@6`I2x7GsgcToX8B@Nn^Vy
z|Np$=zj#YBY2<PldzoZZVIwy2FW#ETI624Gv%3xFaAq)9UyT<c*u?2Yg_rQMLMvhs
z^i%MP2wqiaLwf`X3SJYz>k60Q@(6ZP@P-K9R9K2-5p1X6EfKt}(1GO<^ic4Q2;Nob
z#EJ;^Q1G4z-d9+ORT0D~_&@|7Dy+tu2zF8MkqACkSc`S_A$%gMPZic<8CRdl>T`t+
zSkBc6S$(0<g%t{m(W0;j%?b<A#M@Dv3*LZ8u&~1T5?_V+YB{MPwC%W&9CnyQxdcUh
zTNtM_Os729ux0CO4Rg5V_Jnf#-)NZ6{l1BMve-CXmg6^$F5#S!5-G7$(wkiFw;C3e
zasv%jjGiq^^c{PRPKe)WXe+f?;(c7<dksrtB|WDkem^ER?sFHX<j3bK{h(p>MR+QS
zwJU@l6@J363O8bt!VTzG=tDx`YV1_lhwTb`(W9^%dlarhT%i}c6n4n&Hree)kA~*)
zvNEla%u%DmYp}du`XN2(Wb9GC`T3e3TZQnuhU$1Gb96Y%``l~s1Ef2p=W+&%^zT?f
z6Uf{1Zt70m8cZ3v7EiIOfR=D<zM2aqMT+}Jv&R41^juz8xA1k4ciXL}QVG*BnBYJ7
z+AYaXx$|gPaA6*rScMDtC0ftH8_p->y1O&)KEF(t5Le(*BDOGMmMq%cnGMUG*{9r@
z?a7_lmE4)l$er1P+?lP%o!NBUneE1%*=RV|aj==v{$`?o=u_kDw4a66evT`gK_x+z
zfGGsk0zw2+1=J9P1=JEK0d)k^1k@8m1T+xvtNRS5w-e0}G*i$lL9+$T5j6J{{Z`-#
zKG(QW@zuz$>^eG{#V_lH^b_OPbSK?xptPG_;>_PQbaD_4FzMq;>MAdOY{6C_QXyrX
zKU)W9Iop)>(`Y<N;5n;yg@wvfd}UsYGRpIU$_)jc$CY`t$|%o25%3%-qa2pYnOAOf
z<72d%xYgVQc`?^V!g7-*<xL}x*M3r79eL~#lkyaKY$%iRYRO~w3G%8W1BK@ZlgCz-
z=Scxn3S+z;yyMomiE8pTv7i6E{4^ZEwR{S?4%efC#@PHOGd49~tVwLS#+rR&Ev_-P
z)4Z{{E+-#Z;Q>O7=_YPg;AZ^7IZTD~_zgc}E^guaHdduh&H$1ef(~JbL(mZ%<q%{c
p!y(8<jziE0j&TUO4YzX$x(j!62)YmVa|p8Vkgxlwuloc>{sY8glmGw#

literal 0
HcmV?d00001