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/A.class b/unit/java_bytecode/java_bytecode_convert_class/A.class index 9684f38ea7c..274b7b65272 100644 Binary files a/unit/java_bytecode/java_bytecode_convert_class/A.class and b/unit/java_bytecode/java_bytecode_convert_class/A.class differ diff --git a/unit/java_bytecode/java_bytecode_convert_class/C.class b/unit/java_bytecode/java_bytecode_convert_class/C.class index 70de87e848a..f4cd56ed19e 100644 Binary files a/unit/java_bytecode/java_bytecode_convert_class/C.class and b/unit/java_bytecode/java_bytecode_convert_class/C.class differ 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 00000000000..415a0300eca Binary files /dev/null and b/unit/java_bytecode/java_bytecode_convert_class/Extender.class differ 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 3986820feee..00000000000 Binary files a/unit/java_bytecode/java_bytecode_convert_class/Extendor.class and /dev/null differ diff --git a/unit/java_bytecode/java_bytecode_convert_class/Implementor.class b/unit/java_bytecode/java_bytecode_convert_class/Implementor.class index 1c85bca08ae..86d236765fd 100644 Binary files a/unit/java_bytecode/java_bytecode_convert_class/Implementor.class and b/unit/java_bytecode/java_bytecode_convert_class/Implementor.class differ 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..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 @@ -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,18 +88,14 @@ 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( + "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); 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