From 5912a041d73f09282c8f2845a5393a1f93d3e59e Mon Sep 17 00:00:00 2001 From: thk123 Date: Tue, 6 Mar 2018 17:13:19 +0000 Subject: [PATCH 1/3] Refactored java_load_class to allow specifying different cmd line args This will allow adding a lazy version. Don't set flags on optiont that take the default value anyway --- unit/testing-utils/Makefile | 1 + unit/testing-utils/free_form_cmdline.cpp | 35 ++++++++++++++++++++++++ unit/testing-utils/free_form_cmdline.h | 27 ++++++++++++++++++ unit/testing-utils/load_java_class.cpp | 22 ++++++++++++--- unit/testing-utils/load_java_class.h | 8 ++++++ 5 files changed, 89 insertions(+), 4 deletions(-) create mode 100644 unit/testing-utils/free_form_cmdline.cpp create mode 100644 unit/testing-utils/free_form_cmdline.h diff --git a/unit/testing-utils/Makefile b/unit/testing-utils/Makefile index 45ccd69ec7b..659842f178f 100644 --- a/unit/testing-utils/Makefile +++ b/unit/testing-utils/Makefile @@ -1,5 +1,6 @@ SRC = \ c_to_expr.cpp \ + free_form_cmdline.cpp \ load_java_class.cpp \ require_expr.cpp \ require_goto_statements.cpp \ diff --git a/unit/testing-utils/free_form_cmdline.cpp b/unit/testing-utils/free_form_cmdline.cpp new file mode 100644 index 00000000000..3b310f4d139 --- /dev/null +++ b/unit/testing-utils/free_form_cmdline.cpp @@ -0,0 +1,35 @@ +/*******************************************************************\ + + Module: Unit test utilities + + Author: DiffBlue Limited. + +\*******************************************************************/ + +#include "free_form_cmdline.h" + +/// Create a command line option that can be set +/// \param flag_name: The name of the command line option to support +void free_form_cmdlinet::create_flag(const std::string &flag_name) +{ + optiont option; + option.optstring = flag_name; + options.push_back(option); +} + +/// Equivalent to specifying --flag for the command line +/// \param flag: The name of the flag to specify +void free_form_cmdlinet::add_flag(std::string flag) +{ + create_flag(flag); + set(flag); +} + +/// Equivalent to specifying --flag value +/// \param flag: The name of the flag to specify +/// \param value: The value to the set the command line option to +void free_form_cmdlinet::add_option(std::string flag, std::string value) +{ + create_flag(flag); + set(flag, value); +} diff --git a/unit/testing-utils/free_form_cmdline.h b/unit/testing-utils/free_form_cmdline.h new file mode 100644 index 00000000000..040099d3cd7 --- /dev/null +++ b/unit/testing-utils/free_form_cmdline.h @@ -0,0 +1,27 @@ +/*******************************************************************\ + + Module: Unit test utilities + + Author: DiffBlue Limited. + +\*******************************************************************/ + +#ifndef CPROVER_TESTING_UTILS_FREE_FORM_CMDLINE_H +#define CPROVER_TESTING_UTILS_FREE_FORM_CMDLINE_H + +#include + +/// An implementation of cmdlinet to be used in tests. It does not require +/// specifying exactly what flags are supported and instead allows setting any +/// flag +class free_form_cmdlinet : public cmdlinet +{ +public: + void add_flag(std::string flag); + void add_option(std::string flag, std::string value); + +private: + void create_flag(const std::string &flag_name); +}; + +#endif // CPROVER_TESTING_UTILS_FREE_FORM_CMDLINE_H diff --git a/unit/testing-utils/load_java_class.cpp b/unit/testing-utils/load_java_class.cpp index 38ef466e8f2..f4f1bcd10e2 100644 --- a/unit/testing-utils/load_java_class.cpp +++ b/unit/testing-utils/load_java_class.cpp @@ -7,11 +7,11 @@ \*******************************************************************/ #include "load_java_class.h" +#include "free_form_cmdline.h" #include #include #include -#include #include #include @@ -51,7 +51,8 @@ symbol_tablet load_java_class( const std::string &java_class_name, const std::string &class_path, const std::string &main, - std::unique_ptr &&java_lang) + std::unique_ptr &&java_lang, + const cmdlinet &command_line) { // We expect the name of the class without the .class suffix to allow us to // check it @@ -66,8 +67,6 @@ symbol_tablet load_java_class( message_handler); // 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); config.main = main; @@ -109,3 +108,18 @@ symbol_tablet load_java_class( REQUIRE_FALSE(class_type.get_bool(ID_incomplete_class)); return std::move(maybe_goto_model->symbol_table); } + +symbol_tablet load_java_class( + const std::string &java_class_name, + const std::string &class_path, + const std::string &main, + std::unique_ptr &&java_lang) +{ + cmdlinet command_line; + // TODO(tkiley): This doesn't do anything as "java-cp-include-files" is an + // TODO(tkiley): unknown argument. This could be changed by using the + // TODO(tkiley): free_form_cmdlinet + command_line.set("java-cp-include-files", class_path); + return load_java_class( + java_class_name, class_path, main, std::move(java_lang), command_line); +} diff --git a/unit/testing-utils/load_java_class.h b/unit/testing-utils/load_java_class.h index 01cd3bfda16..6011f3b4ad2 100644 --- a/unit/testing-utils/load_java_class.h +++ b/unit/testing-utils/load_java_class.h @@ -18,6 +18,7 @@ #include #include +#include symbol_tablet load_java_class( const std::string &java_class_name, @@ -30,4 +31,11 @@ symbol_tablet load_java_class( const std::string &main, std::unique_ptr &&java_lang); +symbol_tablet load_java_class( + const std::string &java_class_name, + const std::string &class_path, + const std::string &main, + std::unique_ptr &&java_lang, + const cmdlinet &command_line); + #endif // CPROVER_TESTING_UTILS_LOAD_JAVA_CLASS_H From 72fc31e542b31db75a5d27f32e75280e180bdb24 Mon Sep 17 00:00:00 2001 From: thk123 Date: Tue, 6 Mar 2018 17:14:02 +0000 Subject: [PATCH 2/3] Add lazy version of load_java_class This can be used to test the lazy behaviour of bytecode parsing --- unit/testing-utils/load_java_class.cpp | 26 ++++++++++++++++++++++++++ unit/testing-utils/load_java_class.h | 5 +++++ 2 files changed, 31 insertions(+) diff --git a/unit/testing-utils/load_java_class.cpp b/unit/testing-utils/load_java_class.cpp index f4f1bcd10e2..d6164cc6667 100644 --- a/unit/testing-utils/load_java_class.cpp +++ b/unit/testing-utils/load_java_class.cpp @@ -18,6 +18,32 @@ #include +/// Go through the process of loading, type-checking and finalising loading a +/// specific class file to build the symbol table. The functions are converted +/// using ci_lazy_methods (equivalent to passing --lazy-methods to JBMC) +/// \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. +/// \param main: The name of the main function or "" to use the default +/// behaviour to find a main function. +/// \return The symbol table that is generated by parsing this file. +symbol_tablet load_java_class_lazy( + const std::string &java_class_name, + const std::string &class_path, + const std::string &main) +{ + free_form_cmdlinet lazy_command_line; + lazy_command_line.add_flag("lazy-methods"); + + return load_java_class( + java_class_name, + class_path, + main, + new_java_bytecode_language(), + lazy_command_line); +} + /// Go through the process of loading, type-checking 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 diff --git a/unit/testing-utils/load_java_class.h b/unit/testing-utils/load_java_class.h index 6011f3b4ad2..0a29a2304aa 100644 --- a/unit/testing-utils/load_java_class.h +++ b/unit/testing-utils/load_java_class.h @@ -38,4 +38,9 @@ symbol_tablet load_java_class( std::unique_ptr &&java_lang, const cmdlinet &command_line); +symbol_tablet load_java_class_lazy( + const std::string &java_class_name, + const std::string &class_path, + const std::string &main); + #endif // CPROVER_TESTING_UTILS_LOAD_JAVA_CLASS_H From 3864e6cfd2c59662f1d0adefff7bf80e3ad118ac Mon Sep 17 00:00:00 2001 From: thk123 Date: Tue, 6 Mar 2018 17:29:42 +0000 Subject: [PATCH 3/3] Updating comment with relevant JIRA ticket --- unit/testing-utils/load_java_class.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/unit/testing-utils/load_java_class.cpp b/unit/testing-utils/load_java_class.cpp index d6164cc6667..82521b9eff6 100644 --- a/unit/testing-utils/load_java_class.cpp +++ b/unit/testing-utils/load_java_class.cpp @@ -144,7 +144,8 @@ symbol_tablet load_java_class( cmdlinet command_line; // TODO(tkiley): This doesn't do anything as "java-cp-include-files" is an // TODO(tkiley): unknown argument. This could be changed by using the - // TODO(tkiley): free_form_cmdlinet + // TODO(tkiley): free_form_cmdlinet however this causes some tests to fail. + // TODO(tkiley): TG-2708 to investigate and fix command_line.set("java-cp-include-files", class_path); return load_java_class( java_class_name, class_path, main, std::move(java_lang), command_line);