From 46cbec68a54c3e2ff16cc7922ffdb9d474252f12 Mon Sep 17 00:00:00 2001 From: Thomas Kiley Date: Fri, 29 Sep 2017 14:28:05 +0100 Subject: [PATCH 1/2] Created utility function for loading a class file To catch mistakes where the working directory is wrongly set verify that the class has been loaded. --- unit/Makefile | 1 + .../convert_abstract_class.cpp | 71 ++++--------------- unit/src/java_bytecode/load_java_class.cpp | 67 +++++++++++++++++ unit/src/java_bytecode/load_java_class.h | 22 ++++++ 4 files changed, 105 insertions(+), 56 deletions(-) create mode 100644 unit/src/java_bytecode/load_java_class.cpp create mode 100644 unit/src/java_bytecode/load_java_class.h diff --git a/unit/Makefile b/unit/Makefile index a9f4da75522..dfeb41376e1 100644 --- a/unit/Makefile +++ b/unit/Makefile @@ -3,6 +3,7 @@ # Source files for test utilities SRC = src/expr/require_expr.cpp \ src/ansi-c/c_to_expr.cpp \ + src/java_bytecode/load_java_class.cpp \ unit_tests.cpp \ catch_example.cpp \ util/expr_iterator.cpp \ diff --git a/unit/java_bytecode/java_bytecode_convert_class/convert_abstract_class.cpp b/unit/java_bytecode/java_bytecode_convert_class/convert_abstract_class.cpp index 71f39dfc937..c4ecf4a0943 100644 --- a/unit/java_bytecode/java_bytecode_convert_class/convert_abstract_class.cpp +++ b/unit/java_bytecode/java_bytecode_convert_class/convert_abstract_class.cpp @@ -15,39 +15,18 @@ #include #include #include +#include SCENARIO("java_bytecode_convert_abstract_class", "[core][java_bytecode][java_bytecode_convert_class]") { - std::unique_ptrjava_lang(new_java_bytecode_language()); - - // Configure the path loading - cmdlinet command_line; - command_line.set( - "java-cp-include-files", - "./java_bytecode/java_bytecode_convert_class"); - config.java.classpath.push_back( - "./java_bytecode/java_bytecode_convert_class"); - - // Configure the language - null_message_handlert message_handler; - java_lang->get_language_options(command_line); - java_lang->set_message_handler(message_handler); - - std::istringstream java_code_stream("ignored"); - GIVEN("Some class files in the class path") { WHEN("Parsing an interface") { - java_lang->parse(java_code_stream, "I.class"); - - symbol_tablet new_symbol_table; - java_lang->typecheck(new_symbol_table, ""); + const symbol_tablet &new_symbol_table= + load_java_class("I", "./java_bytecode/java_bytecode_convert_class"); - java_lang->final(new_symbol_table); - - REQUIRE(new_symbol_table.has_symbol("java::I")); THEN("The symbol type should be abstract") { const symbolt &class_symbol=new_symbol_table.lookup("java::I"); @@ -61,14 +40,8 @@ SCENARIO("java_bytecode_convert_abstract_class", } WHEN("Parsing an abstract class") { - java_lang->parse(java_code_stream, "A.class"); - - symbol_tablet new_symbol_table; - java_lang->typecheck(new_symbol_table, ""); - - java_lang->final(new_symbol_table); - - REQUIRE(new_symbol_table.has_symbol("java::A")); + const symbol_tablet &new_symbol_table= + load_java_class("A", "./java_bytecode/java_bytecode_convert_class"); THEN("The symbol type should be abstract") { const symbolt &class_symbol=new_symbol_table.lookup("java::A"); @@ -82,14 +55,8 @@ SCENARIO("java_bytecode_convert_abstract_class", } WHEN("Passing a concrete class") { - java_lang->parse(java_code_stream, "C.class"); - - symbol_tablet new_symbol_table; - java_lang->typecheck(new_symbol_table, ""); - - java_lang->final(new_symbol_table); - - REQUIRE(new_symbol_table.has_symbol("java::C")); + const symbol_tablet &new_symbol_table= + load_java_class("C", "./java_bytecode/java_bytecode_convert_class"); THEN("The symbol type should not be abstract") { const symbolt &class_symbol=new_symbol_table.lookup("java::C"); @@ -103,14 +70,10 @@ SCENARIO("java_bytecode_convert_abstract_class", } WHEN("Passing a concrete class that implements an interface") { - java_lang->parse(java_code_stream, "Implementor.class"); - - symbol_tablet new_symbol_table; - java_lang->typecheck(new_symbol_table, ""); - - java_lang->final(new_symbol_table); - - REQUIRE(new_symbol_table.has_symbol("java::Implementor")); + const symbol_tablet &new_symbol_table= + load_java_class( + "Implementor", + "./java_bytecode/java_bytecode_convert_class"); THEN("The symbol type should not be abstract") { const symbolt &class_symbol= @@ -125,14 +88,10 @@ SCENARIO("java_bytecode_convert_abstract_class", } WHEN("Passing a concrete class that extends an abstract class") { - java_lang->parse(java_code_stream, "Extendor.class"); - - symbol_tablet new_symbol_table; - java_lang->typecheck(new_symbol_table, ""); - - java_lang->final(new_symbol_table); - - REQUIRE(new_symbol_table.has_symbol("java::Extendor")); + const symbol_tablet &new_symbol_table= + load_java_class( + "Extendor", + "./java_bytecode/java_bytecode_convert_class"); THEN("The symbol type should not be abstract") { const symbolt &class_symbol= diff --git a/unit/src/java_bytecode/load_java_class.cpp b/unit/src/java_bytecode/load_java_class.cpp new file mode 100644 index 00000000000..bfcb662ffa2 --- /dev/null +++ b/unit/src/java_bytecode/load_java_class.cpp @@ -0,0 +1,67 @@ +/*******************************************************************\ + + Module: Unit test utilities + + Author: DiffBlue Limited. All rights reserved. + +\*******************************************************************/ + +#include "load_java_class.h" +#include +#include + +#include +#include +#include + +#include + +/// Go through the process of loading, typechecking and finalising loading a +/// specific class file to build the symbol table. +/// \param java_class_name: The name of the class file to load. It should not +/// include the .class extension. +/// \param class_path: The path to load the class from. Should be relative to +/// the unit directory. +/// \return The symbol table that is generated by parsing this file. +symbol_tablet load_java_class( + const std::string &java_class_name, + const std::string &class_path) +{ + // We don't expect the .class suffix to allow us to check the name of the + // class + PRECONDITION(!has_suffix(java_class_name, ".class")); + + // Configure the path loading + cmdlinet command_line; + command_line.set("java-cp-include-files", class_path); + config.java.classpath.clear(); + config.java.classpath.push_back(class_path); + + symbol_tablet new_symbol_table; + + std::unique_ptrjava_lang(new_java_bytecode_language()); + + std::istringstream java_code_stream("ignored"); + null_message_handlert message_handler; + + // Configure the language, load the class files + java_lang->get_language_options(command_line); + java_lang->set_message_handler(message_handler); + java_lang->parse(java_code_stream, java_class_name + ".class"); + java_lang->typecheck(new_symbol_table, ""); + java_lang->final(new_symbol_table); + + // Verify that the class was loaded + const std::string class_symbol_name="java::"+java_class_name; + REQUIRE(new_symbol_table.has_symbol(class_symbol_name)); + const symbolt &class_symbol=new_symbol_table.lookup(class_symbol_name); + REQUIRE(class_symbol.is_type); + const typet &class_type=class_symbol.type; + REQUIRE(class_type.id()==ID_struct); + + // if this fails it indicates the class was not loaded + // Check your working directory and the class path is correctly configured + // as this often indicates that one of these is wrong. + REQUIRE_FALSE(class_type.get_bool(ID_incomplete_class)); + return new_symbol_table; +} diff --git a/unit/src/java_bytecode/load_java_class.h b/unit/src/java_bytecode/load_java_class.h new file mode 100644 index 00000000000..ecfb703dd89 --- /dev/null +++ b/unit/src/java_bytecode/load_java_class.h @@ -0,0 +1,22 @@ +/*******************************************************************\ + + Module: Unit test utilities + + Author: DiffBlue Limited. All rights reserved. + +\*******************************************************************/ + +/// \file +/// Utility for loading and parsing a specified java class file, returning +/// the symbol table generated by this. + +#ifndef CPROVER_SRC_JAVA_BYTECODE_LOAD_JAVA_CLASS_H +#define CPROVER_SRC_JAVA_BYTECODE_LOAD_JAVA_CLASS_H + +#include + +symbol_tablet load_java_class( + const std::string &java_class_name, + const std::string &class_path); + +#endif // CPROVER_SRC_JAVA_BYTECODE_LOAD_JAVA_CLASS_H From 774bfdb867a41f3ac1e3d2b83d3cac212d03001c Mon Sep 17 00:00:00 2001 From: Thomas Kiley Date: Mon, 2 Oct 2017 11:38:29 +0100 Subject: [PATCH 2/2] Correcting type in the extendor class --- .../java_bytecode_convert_class/A.class | Bin 222 -> 274 bytes .../java_bytecode_convert_class/C.class | Bin 261 -> 331 bytes .../ExampleClasses.java | 2 +- .../java_bytecode_convert_class/Extender.class | Bin 0 -> 306 bytes .../java_bytecode_convert_class/Extendor.class | Bin 229 -> 0 bytes .../Implementor.class | Bin 266 -> 346 bytes .../convert_abstract_class.cpp | 4 ++-- 7 files changed, 3 insertions(+), 3 deletions(-) create mode 100644 unit/java_bytecode/java_bytecode_convert_class/Extender.class delete mode 100644 unit/java_bytecode/java_bytecode_convert_class/Extendor.class diff --git a/unit/java_bytecode/java_bytecode_convert_class/A.class b/unit/java_bytecode/java_bytecode_convert_class/A.class index 9684f38ea7c0655906c7480bacda17ebfeb1e5aa..274b7b65272af73bcef727310130aa9b6df79822 100644 GIT binary patch delta 132 zcmcb|IEhL0)W2Q(7#J8#7=*bPm>C4v83frGgeHm_DG2%GCnx5FB^G5SCgr4tfCxqg zmXeIjVnzmLA4ltnu9;5y42(d?z`&}toq=&9kio>j2_)ITf@}<2KsFCV0RuOX#lXVA Qz{|i66lG-K1FPl-04~}Sw*UYD delta 81 zcmbQlbdOQ=)W2Q(7#J8#7zDT&m>GE48Ti;4_$P`QP0UO;kY!*5LIws_t?dkq8-WZ) Z22LQ!1{P#vVPN25Uff$?3=9k=48mLt%nSnT41(+oLK8)e6oh>8lM{2o5{ohulX6l+Km;QL zOG!p%F(U)BkF)he*TQ0b21X!cU|`kS&cL`4$Y5gN1d?oEL0$$fAe#rGfPovx0s&qI fcAy9ckfja8Ak7#Wg^@HeLNzin@Bx)FG4KNbC#n?@ delta 112 zcmX@j)XF4!>ff$?3=9k=3<6vX%nZEj41DYi{1ZiuCT8aQ%Q7$mAp--e)^-NQjX(w? l11FGV0}Jv3SzHY4KsE=EB?*=Vsz6sJ3{=1klw@My0RWXT3cLUS diff --git a/unit/java_bytecode/java_bytecode_convert_class/ExampleClasses.java b/unit/java_bytecode/java_bytecode_convert_class/ExampleClasses.java index a7816923faa..2207fd1cef0 100644 --- a/unit/java_bytecode/java_bytecode_convert_class/ExampleClasses.java +++ b/unit/java_bytecode/java_bytecode_convert_class/ExampleClasses.java @@ -19,7 +19,7 @@ void concreteMethod() { } } -class Extendor extends A { +class Extender extends A { void method() { } diff --git a/unit/java_bytecode/java_bytecode_convert_class/Extender.class b/unit/java_bytecode/java_bytecode_convert_class/Extender.class new file mode 100644 index 0000000000000000000000000000000000000000..415a0300eca450293065867b5823581e3165c066 GIT binary patch literal 306 zcmZXOOKZYF6ot>#Xl#79P;lq6D(J?YQYfOU&`pc`(Ok%sJS2(Y-*P2%(I3zsReC2r z5FD7f_nf)knfd+u{sAyX+d&Zx8%-N6LV2nqoxKu@FTEwfn#CRyny!xceH*Sg`BbYw zoJTiat6-@TZS>i+GGC_z$DQvpjyz5#5*Tvk$DX(!@itlWLL2;PzE|NU;8~#3l+)pt z+Nl~Wln9jzOrSS(QIPMMRgf(MkVxr9Qb}s5e*_)!Yg^88Za$+TeeE=W2RNdD>J=V{ RGVmSPxdG`6k_4I8>;ExHFbMzv literal 0 HcmV?d00001 diff --git a/unit/java_bytecode/java_bytecode_convert_class/Extendor.class b/unit/java_bytecode/java_bytecode_convert_class/Extendor.class deleted file mode 100644 index 3986820feeea621ea71741958a4c6fbd15c82d7f..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 229 zcmZ9Fy9&Z!424g6w^khlp@ZP44o;3DNYP1L6!*XO2P?fuFVfd?5*&O0A4*I+I2cII z;p8KEf1WP@b98N}Xq#|MbO^>GOu}MGP{)%aLG#i;5_;P(k-IYXWp)sL#EB8h;+zHq zd!LrsNp8YA?XN2lUnA*7BF|+$yNH``pg|{C>#C4RkY)s0VFZQ0)}?SW06xiX$V#mG e^Z~lFA(%XkCLFM{eyH1QnfS+ChFiQ;V1EJZy&~uU diff --git a/unit/java_bytecode/java_bytecode_convert_class/Implementor.class b/unit/java_bytecode/java_bytecode_convert_class/Implementor.class index 1c85bca08aeb00b65dbb54105ca7402d7a804f28..86d236765fdc6a5673ccc6ebf8879071f64974ba 100644 GIT binary patch delta 194 zcmeBTy2T`M>ff$?3=9k=48mLt%nbbO3_E0Qm=6>~*C>yqkrA$u7pRff$?3=9k=3<6vX%nUs247}_NeC!PT6D71J=2iO3GB5%m0|Tqpb_T|c mKn5cN2asd~3(5dVPB5DtC?*M(1*$+-CJ$7`1(alB;06G@WD5lV diff --git a/unit/java_bytecode/java_bytecode_convert_class/convert_abstract_class.cpp b/unit/java_bytecode/java_bytecode_convert_class/convert_abstract_class.cpp index c4ecf4a0943..e8932306ee9 100644 --- a/unit/java_bytecode/java_bytecode_convert_class/convert_abstract_class.cpp +++ b/unit/java_bytecode/java_bytecode_convert_class/convert_abstract_class.cpp @@ -90,12 +90,12 @@ SCENARIO("java_bytecode_convert_abstract_class", { const symbol_tablet &new_symbol_table= load_java_class( - "Extendor", + "Extender", "./java_bytecode/java_bytecode_convert_class"); THEN("The symbol type should not be abstract") { const symbolt &class_symbol= - new_symbol_table.lookup("java::Extendor"); + new_symbol_table.lookup("java::Extender"); const typet &symbol_type=class_symbol.type; REQUIRE(symbol_type.id()==ID_struct);