From bd907a4c9ec8d3b75f6cf88de3a06623c4d3214c Mon Sep 17 00:00:00 2001 From: thk123 Date: Tue, 29 May 2018 15:34:34 +0100 Subject: [PATCH 1/4] Diversified the test for multiple fields Though this wasn't the problem, makes the tests more robust as more than one type used in specialising the same generic type. --- .../goto_program_generics/BWrapper.class | Bin 0 -> 315 bytes .../GenericFields$MultipleGenericFields.class | Bin 778 -> 833 bytes .../goto_program_generics/GenericFields.java | 4 ++-- .../goto_program_generics/GenericHelper.java | 8 ++++++++ .../generic_parameters_test.cpp | 4 ++-- 5 files changed, 12 insertions(+), 4 deletions(-) create mode 100644 jbmc/unit/java_bytecode/goto_program_generics/BWrapper.class diff --git a/jbmc/unit/java_bytecode/goto_program_generics/BWrapper.class b/jbmc/unit/java_bytecode/goto_program_generics/BWrapper.class new file mode 100644 index 0000000000000000000000000000000000000000..879bbc45300db45ea0aa05346634ea029837062e GIT binary patch literal 315 zcmXw!y-veG5QJwh#!ig$Lx40ilt~KG(19otDNtBYfQ*#xY)){Iv7^J`y(kb81rNYO zA;ux-bU)wh%xdrZ=kp7|DFz`t?6uH9Kfr!~1A(O63xR)b3tL?Xyy0S$@S2qmM$nCI zVXoKDsd0BY&8hU`GShjYovnE*dexJC5rpyd-s#oKxHExD**d%}*Df=2yNObeJWPJ1v^+r+%d3KluBIeulcCbqt{JE*NNz76AH{H7=h2AfFqczL` literal 0 HcmV?d00001 diff --git a/jbmc/unit/java_bytecode/goto_program_generics/GenericFields$MultipleGenericFields.class b/jbmc/unit/java_bytecode/goto_program_generics/GenericFields$MultipleGenericFields.class index c7fbb48fb8d95b1ecabc2b6304207ee01fcafe17..f66f5b82b6b0e39624c1b8fc7fb337a63ab87f26 100644 GIT binary patch delta 393 zcmX|+y-osA5QV?Hz~0^Uf(r=#pez0>{-S7NRxRvINTf5d)5OM#@B;L9gv!S-fyTmU z>$~_0#<}ZiacAb7nKNhZll$SGety5c0WD5^0+s?MShm%Q&nj!0b)Os?mf6&7`FJ!m zJDS}=vs10KZ+ds#?nCdaeVJDAMLg(#otG#ZricuNyk^g^&w;|bO2-UM4h`ebFvbNjwwZ$;>?13* delta 356 zcmYL@OHKko5Qe`Q!@O*8P(&03eBc8_W8%h*OO0`(E7wM60WpS*2XOC>Z~~9uf|$54 zajBQ^0N%m)_h3RgUDeh9UtiUS_v9UX{l2{ehwO(0)FMLa_SFbkWzApQPQJlWuZ% z`#?j;P?M*0g}}k+<&sxa*QAbPG%VB5#91kGs*dG#m7`XBgwuM(eaSo}MNb~Yn^!E4 zT{O!qsx%(ymdYrUfk4jQzq}s>^Z~SEwjQ J(gHSFfIsv8AzuIh diff --git a/jbmc/unit/java_bytecode/goto_program_generics/GenericFields.java b/jbmc/unit/java_bytecode/goto_program_generics/GenericFields.java index b83152c95b4..92f1f848513 100644 --- a/jbmc/unit/java_bytecode/goto_program_generics/GenericFields.java +++ b/jbmc/unit/java_bytecode/goto_program_generics/GenericFields.java @@ -11,10 +11,10 @@ public void foo() { class MultipleGenericFields { Wrapper field_input1; - Wrapper field_input2; + Wrapper field_input2; public void foo() { field_input1.field.i = 10; - field_input2.field.i = 20; + field_input2.field.b = true; } } diff --git a/jbmc/unit/java_bytecode/goto_program_generics/GenericHelper.java b/jbmc/unit/java_bytecode/goto_program_generics/GenericHelper.java index fb7c9e73e0d..332c68a6cb6 100644 --- a/jbmc/unit/java_bytecode/goto_program_generics/GenericHelper.java +++ b/jbmc/unit/java_bytecode/goto_program_generics/GenericHelper.java @@ -6,6 +6,14 @@ public IWrapper(int ii) { } } +// boolean wrapper +class BWrapper { + public boolean b; + public BWrapper(boolean bb) { + b = bb; + } +} + // simple generic class class Wrapper { public T field; diff --git a/jbmc/unit/java_bytecode/goto_program_generics/generic_parameters_test.cpp b/jbmc/unit/java_bytecode/goto_program_generics/generic_parameters_test.cpp index 14b61f44c01..ec6a994a918 100644 --- a/jbmc/unit/java_bytecode/goto_program_generics/generic_parameters_test.cpp +++ b/jbmc/unit/java_bytecode/goto_program_generics/generic_parameters_test.cpp @@ -136,13 +136,13 @@ SCENARIO( {}, entry_point_code); - THEN("Object 'field_input1' has field 'field' of type IWrapper") + THEN("Object 'field_input2' has field 'field' of type BWrapper") { require_goto_statements::require_struct_component_assignment( field_input2_name, {}, "field", - "java::IWrapper", + "java::BWrapper", {}, entry_point_code); } From 1f9a5c47d6d551e2d8639a44ace1358d01693062 Mon Sep 17 00:00:00 2001 From: thk123 Date: Wed, 30 May 2018 09:40:54 +0100 Subject: [PATCH 2/4] Adding test about the type --- .../generic_parameters_test.cpp | 15 +++++++++++++++ 1 file changed, 15 insertions(+) diff --git a/jbmc/unit/java_bytecode/goto_program_generics/generic_parameters_test.cpp b/jbmc/unit/java_bytecode/goto_program_generics/generic_parameters_test.cpp index ec6a994a918..9d7b1633b35 100644 --- a/jbmc/unit/java_bytecode/goto_program_generics/generic_parameters_test.cpp +++ b/jbmc/unit/java_bytecode/goto_program_generics/generic_parameters_test.cpp @@ -102,6 +102,21 @@ SCENARIO( require_goto_statements::require_entry_point_argument_assignment( "this", entry_point_code); + THEN("Type of multiple generic fields should be right") + { + const typet &class_type = + symbol_table.lookup_ref("java::GenericFields$MultipleGenericFields") + .type; + + const auto &component = require_type::require_component( + to_java_class_type(class_type), "field_input2"); + + const java_generic_typet &type = + require_type::require_java_generic_type(component.type()); + require_type::require_pointer( + type.generic_type_arguments()[0], symbol_typet{"java::BWrapper"}); + } + THEN("Object 'this' has field 'field_input1' of type Wrapper") { const auto &field_input1_name = From 0c874bf6c1a0c97cd85fee5d0c91a1891c2c077f Mon Sep 17 00:00:00 2001 From: thk123 Date: Wed, 30 May 2018 15:52:43 +0100 Subject: [PATCH 3/4] Don't have generic type variables as a comment The symex_target_equation will merge two types who differ only in generic specialisation losing the specialisation information. This ensures that information is kept. --- src/util/irep_ids.def | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/util/irep_ids.def b/src/util/irep_ids.def index 2706e179ee7..c7b233c17ab 100644 --- a/src/util/irep_ids.def +++ b/src/util/irep_ids.def @@ -655,7 +655,7 @@ IREP_ID_TWO(C_java_implicitly_generic_class_type, #java_implicitly_generic_class IREP_ID_TWO(C_java_generic_symbol, #java_generic_symbol) IREP_ID_TWO(generic_types, #generic_types) IREP_ID_TWO(implicit_generic_types, #implicit_generic_types) -IREP_ID_TWO(type_variables, #type_variables) +IREP_ID_ONE(type_variables) IREP_ID_TWO(java_lambda_method_handle_index, lambda_method_handle_index) IREP_ID_TWO(java_lambda_method_handles, lambda_method_handles) IREP_ID_ONE(havoc_object) From e1398bc314782c296e945ed8c8aee6bae10d8aa6 Mon Sep 17 00:00:00 2001 From: thk123 Date: Wed, 30 May 2018 17:33:29 +0100 Subject: [PATCH 4/4] Add tests for generic type erasure Ensure that moving generic type information out of a comment doesn't cause type errors. --- jbmc/regression/CMakeLists.txt | 1 + jbmc/regression/Makefile | 1 + jbmc/regression/jbmc-generics/CMakeLists.txt | 10 +++++ jbmc/regression/jbmc-generics/Makefile | 36 ++++++++++++++++++ .../jbmc-generics/type_erasure/BWrapper.class | Bin 0 -> 266 bytes .../jbmc-generics/type_erasure/Gen.class | Bin 0 -> 406 bytes .../jbmc-generics/type_erasure/IWrapper.class | Bin 0 -> 266 bytes .../type_erasure/TestClass.class | Bin 0 -> 1226 bytes .../jbmc-generics/type_erasure/TestClass.java | 34 +++++++++++++++++ .../jbmc-generics/type_erasure/test.desc | 6 +++ .../type_erasure/test_function_input.desc | 10 +++++ 11 files changed, 98 insertions(+) create mode 100644 jbmc/regression/jbmc-generics/CMakeLists.txt create mode 100644 jbmc/regression/jbmc-generics/Makefile create mode 100644 jbmc/regression/jbmc-generics/type_erasure/BWrapper.class create mode 100644 jbmc/regression/jbmc-generics/type_erasure/Gen.class create mode 100644 jbmc/regression/jbmc-generics/type_erasure/IWrapper.class create mode 100644 jbmc/regression/jbmc-generics/type_erasure/TestClass.class create mode 100644 jbmc/regression/jbmc-generics/type_erasure/TestClass.java create mode 100644 jbmc/regression/jbmc-generics/type_erasure/test.desc create mode 100644 jbmc/regression/jbmc-generics/type_erasure/test_function_input.desc diff --git a/jbmc/regression/CMakeLists.txt b/jbmc/regression/CMakeLists.txt index 487dd801c66..65da4bee9a9 100644 --- a/jbmc/regression/CMakeLists.txt +++ b/jbmc/regression/CMakeLists.txt @@ -11,3 +11,4 @@ add_subdirectory(janalyzer-taint) add_subdirectory(jbmc-concurrency) add_subdirectory(jbmc-inheritance) add_subdirectory(jbmc-cover) +add_subdirectory(jbmc-generics) diff --git a/jbmc/regression/Makefile b/jbmc/regression/Makefile index 7e607532891..0d85532780a 100644 --- a/jbmc/regression/Makefile +++ b/jbmc/regression/Makefile @@ -9,6 +9,7 @@ DIRS = janalzyer-taint \ jbmc-strings \ jdiff \ string-smoke-tests \ + jbmc-generics \ # Empty last line # Tests under goto-gcc cannot be run on Windows, so appveyor.yml unlinks diff --git a/jbmc/regression/jbmc-generics/CMakeLists.txt b/jbmc/regression/jbmc-generics/CMakeLists.txt new file mode 100644 index 00000000000..fa345944621 --- /dev/null +++ b/jbmc/regression/jbmc-generics/CMakeLists.txt @@ -0,0 +1,10 @@ +add_test_pl_tests( + "$" +) + +add_test_pl_profile( + "jbmc-symex-driven-lazy-loading" + "$ --symex-driven-lazy-loading" + "-C;-X;symex-driven-lazy-loading-expected-failure;-s;symex-driven-loading" + "CORE" +) diff --git a/jbmc/regression/jbmc-generics/Makefile b/jbmc/regression/jbmc-generics/Makefile new file mode 100644 index 00000000000..81024778e07 --- /dev/null +++ b/jbmc/regression/jbmc-generics/Makefile @@ -0,0 +1,36 @@ +default: tests.log + +include ../../src/config.inc + +test: + @../$(CPROVER_DIR)/regression/test.pl -p -c ../../../src/jbmc/jbmc + @../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -s symex-driven-loading + +tests.log: ../$(CPROVER_DIR)/regression/test.pl + @../$(CPROVER_DIR)/regression/test.pl -p -c ../../../src/jbmc/jbmc + @../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -s symex-driven-loading + +show: + @for dir in *; do \ + if [ -d "$$dir" ]; then \ + vim -o "$$dir/*.java" "$$dir/*.out"; \ + fi; \ + done; + +clean: + find -name '*.out' -execdir $(RM) '{}' \; + find -name '*.gb' -execdir $(RM) '{}' \; + $(RM) tests.log + +%.class: %.java ../../src/org.cprover.jar + javac -g -cp ../../src/org.cprover.jar:. $< + +nondet_java_files := $(shell find . -name "Nondet*.java") +nondet_class_files := $(patsubst %.java, %.class, $(nondet_java_files)) + +.PHONY: nondet-class-files +nondet-class-files: $(nondet_class_files) + +.PHONY: clean-nondet-class-files +clean-nondet-class-files: + -rm $(nondet_class_files) diff --git a/jbmc/regression/jbmc-generics/type_erasure/BWrapper.class b/jbmc/regression/jbmc-generics/type_erasure/BWrapper.class new file mode 100644 index 0000000000000000000000000000000000000000..2fbcfaf51ec254202a3fe8a6dbf482c1a51b7100 GIT binary patch literal 266 zcmXwzJ#NB45QX3P7aRu@PCyA1xJj2NMUbd0Qp6%sy0uxsB4b-?lY6C#M8N?#6k^sQ z#XP@_GG#yIE!i{2~na-xjG&)sZ)^^ zOh!qSi()ObGWiajcBdLbki36sQP)zxaQLi_I+sgjwg#ze+C?FnX1*6cB7_H@(EA@J z3=NJ8QEuapY%lW`V_5tr!0*9<+c}s$&OJ_X*8$wwALy5Xg+8mt80-Spu=6e+*qK9* HtQH10L3%Ki literal 0 HcmV?d00001 diff --git a/jbmc/regression/jbmc-generics/type_erasure/Gen.class b/jbmc/regression/jbmc-generics/type_erasure/Gen.class new file mode 100644 index 0000000000000000000000000000000000000000..e1b49e488fdb78e2f6f59cc308281788290f2751 GIT binary patch literal 406 zcmZWlyH3ME5S;as7?T78p`{EIq@e=K5{d+k1x2j%XLAY{85`MWBtDA@iGmN{qY!%` z6d}#-%-rnW?tXoLd;++@aR3{KK8}2h2&4&7x)d*BQi^IZxzCrf&{u@sOf4#*yG9c1 zEMvusRi$*obbLA|IMe!p-v+6wS-z3_S|e1Vh24Qn>!PR|98a+ zEWQZ9$AANuqsPpG&j_ZJbHM1Dvr*i$chDOH8@n96l}HE~hrb5wq0elvp$wT>>(={- HR_x#hx9d^# literal 0 HcmV?d00001 diff --git a/jbmc/regression/jbmc-generics/type_erasure/IWrapper.class b/jbmc/regression/jbmc-generics/type_erasure/IWrapper.class new file mode 100644 index 0000000000000000000000000000000000000000..49cd865379d8fd07bc640dd0944a529f4e922375 GIT binary patch literal 266 zcmXwz%?`m(5QWcFwbZ{Su*5<)cEm;^ku)p_>)X2FO0{xZ-pfj2;Q>69m@6#i$_QRC-)eC_OFiPSN-sK+GiA2wYnkQKSY+AYD6XOk2QH!XA15>o_G6Lk z{bhKRQH~BQ{uAK$V59hTFngR!ocwPGDE9B58v_evR);Y|c&yc*udp+RYOEIOA3u{Y Al>h($ literal 0 HcmV?d00001 diff --git a/jbmc/regression/jbmc-generics/type_erasure/TestClass.class b/jbmc/regression/jbmc-generics/type_erasure/TestClass.class new file mode 100644 index 0000000000000000000000000000000000000000..3d24d025188f6dc226eb988f6e98ab66be188bdc GIT binary patch literal 1226 zcmZuvT~8B16g|^!yZu<86bcCPAt07*p^6nvN>D&ir04?#B5&Jv1BmHlsy?);My_ZU1jN38f5|FY&a!|vKD#TRtd$F< zKu^{xna^ska;Ci_lLeyLa^5KJ8nz|(O;B+Tt*SscyJJ?JwIVq(0-D3kdaaa~Y$P!R zeA&lli6N2WpBEUoc-h;^`GvhQaVfj8XB(A@X=j#ssEMt1VqM#gk$<^mRNO+?34vHA z?VjZvZj>rDhlR&o^7bNS2Dhz)lHt^BD%0Bu7nmERbkNF!fu(%0*|5-dxn}3hbxXFV zyVZgDBjb&sp&LEyDb;Au&?PV=;Z)Hm9i&#yNAbwE%eID_xTRqMw^>%}78Pj?cd#fB zX&-!^J2LZ>BnFwMGK^(9c}}vDV?A%=Qx7 zID_ZKDZHC{_9K*IL=yTtgwNn3=>L}3YJkZ^2k1h5N&N)saXVEOptuE$L8aeAx(Gr< zMoB-;0v0fUCm3`Kn;>}rD?|pF8^V1I(G$$mafO}-!^8(@8(AaVHDXtZjdB--_cumW zjPd)0ey%a*j#fyrNFFS$J0a|>&ZG+_0I^@kx95FopjCIf0ZXU8_M-$hw`?@ zVYV5p@fvHH!Wb6Ge2?6lm~81IcT=DA8v3MnQC}lA;top2&h;tqEcWw$Io3%kn`(_N k?dAf#(clR}$555`P`sa@Tz&(xQ9gLI2lAy%yLVmx3#e4-q5uE@ literal 0 HcmV?d00001 diff --git a/jbmc/regression/jbmc-generics/type_erasure/TestClass.java b/jbmc/regression/jbmc-generics/type_erasure/TestClass.java new file mode 100644 index 00000000000..a698eb6aec5 --- /dev/null +++ b/jbmc/regression/jbmc-generics/type_erasure/TestClass.java @@ -0,0 +1,34 @@ +class Gen { + public T t; +} + +class IWrapper { + public int i; +} + +class BWrapper { + public boolean b; +} + +class TestClass { + static void testFunction() { + Gen a = new Gen<>(); + Gen b = a; + assert(b == a); + Gen c; + c = b; + assert(c == b); + assert(c.equals(a)); + } + + static void testFunctionWithInput(Gen a, Gen b, Gen c) { + if(a != null && b != null && c != null && + a.t != null && b.t != null && c.t != null) + { + b = a; + assert(b == a); + a = c; + assert(a == c); + } + } +} diff --git a/jbmc/regression/jbmc-generics/type_erasure/test.desc b/jbmc/regression/jbmc-generics/type_erasure/test.desc new file mode 100644 index 00000000000..97346d61f0c --- /dev/null +++ b/jbmc/regression/jbmc-generics/type_erasure/test.desc @@ -0,0 +1,6 @@ +CORE +TestClass.class +--function TestClass.testFunction --classpath ../../../src/java_bytecode/library/core-models.jar:. +EXIT=0 +SIGNAL=0 +VERIFICATION SUCCESSFUL diff --git a/jbmc/regression/jbmc-generics/type_erasure/test_function_input.desc b/jbmc/regression/jbmc-generics/type_erasure/test_function_input.desc new file mode 100644 index 00000000000..61b04394178 --- /dev/null +++ b/jbmc/regression/jbmc-generics/type_erasure/test_function_input.desc @@ -0,0 +1,10 @@ +CORE +TestClass.class +--function TestClass.testFunctionWithInput +EXIT=0 +SIGNAL=0 +VERIFICATION SUCCESSFUL +-- +-- +Adding the core models causes a exception in convert_struct relating to the +`monitorCount` component. See diffblue/cbmc#2307