From ed008f99b5925ee645060898df2ae2005308b918 Mon Sep 17 00:00:00 2001 From: Dario Cattaruzza Date: Thu, 16 Nov 2017 13:07:41 +0000 Subject: [PATCH 1/4] Add constructors for having memory-loaded jar files This allows the jar_file class to load from a buffer (c array) as opposed to a file --- src/java_bytecode/jar_file.cpp | 28 ++++++++++++++++++++++++---- src/java_bytecode/jar_file.h | 17 +++++++++++++++-- src/java_bytecode/mz_zip_archive.cpp | 11 +++++++++++ src/java_bytecode/mz_zip_archive.h | 7 +++++++ 4 files changed, 57 insertions(+), 6 deletions(-) diff --git a/src/java_bytecode/jar_file.cpp b/src/java_bytecode/jar_file.cpp index ec690238996..b289f4e2d3a 100644 --- a/src/java_bytecode/jar_file.cpp +++ b/src/java_bytecode/jar_file.cpp @@ -12,10 +12,7 @@ Author: Diffblue Ltd #include #include "java_class_loader_limit.h" -jar_filet::jar_filet( - java_class_loader_limitt &limit, - const std::string &filename): - m_zip_archive(filename) +void jar_filet::initialize_file_index(java_class_loader_limitt &limit) { const size_t file_count=m_zip_archive.get_num_files(); for(size_t index=0; index filenames() const; private: + /// Loads the fileindex (m_name_to_index) with a map of loaded files to + /// indices. + void initialize_file_index(java_class_loader_limitt &limit); + mz_zip_archivet m_zip_archive; - /// Map of filename to the file index in the zip archive + /// Map of filename to the file index in the zip archive. std::unordered_map m_name_to_index; }; diff --git a/src/java_bytecode/mz_zip_archive.cpp b/src/java_bytecode/mz_zip_archive.cpp index f467f4ed739..a193f47e1fb 100644 --- a/src/java_bytecode/mz_zip_archive.cpp +++ b/src/java_bytecode/mz_zip_archive.cpp @@ -25,6 +25,14 @@ class mz_zip_archive_statet final:public mz_zip_archive if(MZ_TRUE!=mz_zip_reader_init_file(this, filename.data(), 0)) throw std::runtime_error("MZT: Could not load a file: "+filename); } + + mz_zip_archive_statet(const void *data, size_t size): + mz_zip_archive({ }) + { + if(MZ_TRUE!=mz_zip_reader_init_mem(this, data, size, 0)) + throw std::runtime_error("MZT: Could not load data from memory"); + } + mz_zip_archive_statet(const mz_zip_archive_statet &)=delete; mz_zip_archive_statet(mz_zip_archive_statet &&)=delete; mz_zip_archive_statet &operator=(const mz_zip_archive_statet &)=delete; @@ -41,6 +49,9 @@ static_assert(sizeof(mz_uint)<=sizeof(size_t), mz_zip_archivet::mz_zip_archivet(const std::string &filename): m_state(new mz_zip_archive_statet(filename)) { } +mz_zip_archivet::mz_zip_archivet(const void *data, size_t size): + m_state(new mz_zip_archive_statet(data, size)) { } + // VS Compatibility mz_zip_archivet::mz_zip_archivet(mz_zip_archivet &&other): m_state(std::move(other.m_state)) { } diff --git a/src/java_bytecode/mz_zip_archive.h b/src/java_bytecode/mz_zip_archive.h index 4e2bbf529d6..d8caf98c455 100644 --- a/src/java_bytecode/mz_zip_archive.h +++ b/src/java_bytecode/mz_zip_archive.h @@ -24,6 +24,13 @@ class mz_zip_archivet final /// \param filename Path of the zip archive /// \throw Throws std::runtime_error if file cannot be opened explicit mz_zip_archivet(const std::string &filename); + + /// Loads a zip buffer + /// \param data pointer to the memory buffer + /// \param size size of the buffer + /// \throw Throws std::runtime_error if file cannot be opened + mz_zip_archivet(const void *data, size_t size); + mz_zip_archivet(const mz_zip_archivet &)=delete; mz_zip_archivet &operator=(const mz_zip_archivet &)=delete; /// Move constructor. Doesn't throw. Leaves other object invalidated. From 34216f5128584d89ae7196fcadd447cf8ca2a485 Mon Sep 17 00:00:00 2001 From: Dario Cattaruzza Date: Tue, 16 Jan 2018 09:14:23 +0000 Subject: [PATCH 2/4] Refactor jar loading --- src/java_bytecode/java_class_loader.cpp | 74 +++++++++++-------------- src/java_bytecode/java_class_loader.h | 8 +++ 2 files changed, 41 insertions(+), 41 deletions(-) diff --git a/src/java_bytecode/java_class_loader.cpp b/src/java_bytecode/java_class_loader.cpp index b3039e9bd69..6749dfbd2e1 100644 --- a/src/java_bytecode/java_class_loader.cpp +++ b/src/java_bytecode/java_class_loader.cpp @@ -74,38 +74,50 @@ void java_class_loadert::set_java_cp_include_files( java_cp_include_files=_java_cp_include_files; } -java_bytecode_parse_treet &java_class_loadert::get_parse_tree( +/// Retrieves a class file from a jar and loads it into the tree +bool java_class_loadert::get_class_file( java_class_loader_limitt &class_loader_limit, - const irep_idt &class_name) + const irep_idt &class_name, + const std::string &jar_file, + java_bytecode_parse_treet &parse_tree) { - java_bytecode_parse_treet &parse_tree=class_map[class_name]; + const auto &jm=jar_map[jar_file]; - // First check given JAR files - for(const auto &jf : jar_files) + auto jm_it=jm.entries.find(class_name); + + if(jm_it!=jm.entries.end()) { - read_jar_file(class_loader_limit, jf); + debug() << "Getting class `" << class_name << "' from JAR " + << jar_file << eom; - const auto &jm=jar_map[jf]; + std::string data=jar_pool(class_loader_limit, jar_file) + .get_entry(jm_it->second.class_file_name); - auto jm_it=jm.entries.find(class_name); + std::istringstream istream(data); - if(jm_it!=jm.entries.end()) - { - debug() << "Getting class `" << class_name << "' from JAR " - << jf << eom; + java_bytecode_parse( + istream, + parse_tree, + get_message_handler()); - std::string data=jar_pool(class_loader_limit, jf) - .get_entry(jm_it->second.class_file_name); + return true; + } + return false; +} - std::istringstream istream(data); - java_bytecode_parse( - istream, - parse_tree, - get_message_handler()); +java_bytecode_parse_treet &java_class_loadert::get_parse_tree( + java_class_loader_limitt &class_loader_limit, + const irep_idt &class_name) +{ + java_bytecode_parse_treet &parse_tree=class_map[class_name]; + // First check given JAR files + for(const auto &jf : jar_files) + { + read_jar_file(class_loader_limit, jf); + if(get_class_file(class_loader_limit, class_name, jf, parse_tree)) return parse_tree; - } } // See if we can find it in the class path @@ -115,28 +127,8 @@ java_bytecode_parse_treet &java_class_loadert::get_parse_tree( if(has_suffix(cp, ".jar")) { read_jar_file(class_loader_limit, cp); - - const auto &jm=jar_map[cp]; - - auto jm_it=jm.entries.find(class_name); - - if(jm_it!=jm.entries.end()) - { - debug() << "Getting class `" << class_name << "' from JAR " - << cp << eom; - - std::string data=jar_pool(class_loader_limit, cp) - .get_entry(jm_it->second.class_file_name); - - std::istringstream istream(data); - - java_bytecode_parse( - istream, - parse_tree, - get_message_handler()); - + if(get_class_file(class_loader_limit, class_name, cp, parse_tree)) return parse_tree; - } } else { diff --git a/src/java_bytecode/java_class_loader.h b/src/java_bytecode/java_class_loader.h index 82e624bbacc..9ffe5ae10b4 100644 --- a/src/java_bytecode/java_class_loader.h +++ b/src/java_bytecode/java_class_loader.h @@ -40,6 +40,14 @@ class java_class_loadert:public messaget void read_jar_file(java_class_loader_limitt &, const irep_idt &); + /// Attempts to load the class from the given jar. + /// Returns true if found and loaded + bool get_class_file( + java_class_loader_limitt &class_loader_limit, + const irep_idt &class_name, + const std::string &jar_file, + java_bytecode_parse_treet &parse_tree); + /// Given a \p class_name (e.g. "java.lang.Thread") try to load the /// corresponding .class file by first scanning all .jar files whose /// pathname is stored in \ref jar_files, and if that doesn't work, then scan From f66288b40452a031792b23b859107ea95301440f Mon Sep 17 00:00:00 2001 From: Dario Cattaruzza Date: Thu, 16 Nov 2017 14:09:16 +0000 Subject: [PATCH 3/4] Internalize core models of the Java Class Library The 'core models' is a set of .class files that model core classes from the Java Class Library, such as java.lang.Object or java.lang.Thread. A minimum is necessary for CBMC to understand, e.g., when a new thread is created. These core classes live in `src/java_bytecode/library`. This commit adds support to compile and pack the core classes into a single jar file, core-models.jar, and a converter program that transforms that .jar file into a C-language array of data that can then be linked into CBMC, thus making the .jar file be present in the data segment of the CBMC ELF. Other modifications: - New option --no-core-models, allowing to disable the loading of the internal core models - make and cmake now compile the core models into a single core-models.jar - Add regression one regression tests ensuring the the core-models.jar is loaded by default --- .gitignore | 3 + regression/cbmc-java/coreModels/test.class | Bin 0 -> 582 bytes regression/cbmc-java/coreModels/test.desc | 9 +++ regression/cbmc-java/coreModels/test.java | 10 +++ .../jbmc-strings/java_append_char/test.desc | 2 +- src/java_bytecode/CMakeLists.txt | 12 ++- src/java_bytecode/Makefile | 10 +++ src/java_bytecode/java_bytecode_language.cpp | 19 +++++ src/java_bytecode/java_bytecode_language.h | 29 +++---- src/java_bytecode/java_class_loader.cpp | 52 +++++++++++++ src/java_bytecode/java_class_loader.h | 29 +++++++ src/java_bytecode/library/CMakeLists.txt | 19 +++++ src/java_bytecode/library/Makefile | 40 ++++++++-- src/java_bytecode/library/converter.cpp | 72 ++++++++++++++++++ 14 files changed, 282 insertions(+), 24 deletions(-) create mode 100644 regression/cbmc-java/coreModels/test.class create mode 100644 regression/cbmc-java/coreModels/test.desc create mode 100644 regression/cbmc-java/coreModels/test.java create mode 100644 src/java_bytecode/library/CMakeLists.txt create mode 100644 src/java_bytecode/library/converter.cpp diff --git a/.gitignore b/.gitignore index 5061a31744a..d9ed44bd1a5 100644 --- a/.gitignore +++ b/.gitignore @@ -45,6 +45,7 @@ src/ansi-c/gcc_builtin_headers_tm.inc src/ansi-c/gcc_builtin_headers_mips.inc src/ansi-c/gcc_builtin_headers_power.inc src/ansi-c/gcc_builtin_headers_ubsan.inc +src/java_bytecode/java_core_models.inc # regression/test files *.out @@ -115,6 +116,8 @@ src/ansi-c/file_converter src/ansi-c/file_converter.exe src/ansi-c/library/converter src/ansi-c/library/converter.exe +src/java_bytecode/converter +src/java_bytecode/converter.exe src/util/irep_ids_convert src/util/irep_ids_convert.exe build/ diff --git a/regression/cbmc-java/coreModels/test.class b/regression/cbmc-java/coreModels/test.class new file mode 100644 index 0000000000000000000000000000000000000000..c4d6e034fe940d6bbc7c5750300a1846a2f7db6c GIT binary patch literal 582 zcmYLG%Wl&^6g^`*cH+88n$R?mrUdAsuppc68lj@lN|nMx3PNgFIrb=;kdCAABp;I> zVBI3M2qf6|n-JoT$wSt7u08j>?%e!XIf0$kKRJoMpU*TW+p4eWbp zGE@)4H04T*M5b><8V)BsW?%ybwZ56q*j!q14yRXCO%iD0e?9X?i$&%UcCo>iCb76Q2ny31up$M>r zz{5d+$7ls8z-Op$xL>afpDC3nGGKrno&{=lkK9N18$=YSfOVDw%WD?taL2 z5|oLIxxSFpK^ZS7+y>g6&|D~0%u}Iwyw;>JdPWBX7@$RC&C{$|xo%uiWz!<_px9J3 zX=k+OUfh9QQ^8QAx10U62vS0sYSY?)KPQ|^2w}9t-g=2q%y`ft9Fcdjh!Krau&6FPe11$b+ AfdBvi literal 0 HcmV?d00001 diff --git a/regression/cbmc-java/coreModels/test.desc b/regression/cbmc-java/coreModels/test.desc new file mode 100644 index 00000000000..22f3976f5d0 --- /dev/null +++ b/regression/cbmc-java/coreModels/test.desc @@ -0,0 +1,9 @@ +CORE +test.class +--show-symbol-table +^EXIT=0$ +^SIGNAL=0$ +^Symbol\s*\.*\: java\:\:org\.cprover\.CProver\.\\:\(\)V$ +-- +-- +tests that the core models are being loaded by checking if the static initializer for the CProver class was diff --git a/regression/cbmc-java/coreModels/test.java b/regression/cbmc-java/coreModels/test.java new file mode 100644 index 00000000000..3be70bc0b84 --- /dev/null +++ b/regression/cbmc-java/coreModels/test.java @@ -0,0 +1,10 @@ +import org.cprover.CProver; +class test +{ + public static void main(String[] args) + { + int i=CProver.nondetInt(); + assert(i!=0); + } +} + diff --git a/regression/jbmc-strings/java_append_char/test.desc b/regression/jbmc-strings/java_append_char/test.desc index d625466d5cf..783301b2d52 100644 --- a/regression/jbmc-strings/java_append_char/test.desc +++ b/regression/jbmc-strings/java_append_char/test.desc @@ -1,6 +1,6 @@ CORE test_append_char.class ---refine-strings --string-max-length 1000 +--refine-strings --string-max-length 1000 --no-core-models ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/src/java_bytecode/CMakeLists.txt b/src/java_bytecode/CMakeLists.txt index b9b8191fd16..60abcd475f0 100644 --- a/src/java_bytecode/CMakeLists.txt +++ b/src/java_bytecode/CMakeLists.txt @@ -1,5 +1,13 @@ -file(GLOB_RECURSE sources "*.cpp" "*.h") -add_library(java_bytecode ${sources}) +get_filename_component(JAVA_CORE_MODELS_INC "library/java_core_models.inc" REALPATH BASE_DIR ${CMAKE_CURRENT_SOURCE_DIR}) +set_source_files_properties("library/java_core_models.inc" GENERATED) + +file(GLOB sources "*.cpp") +file(GLOB_RECURSE headers "*.h") +add_subdirectory(library) + +add_library(java_bytecode ${sources} ${headers} ) +add_dependencies(java_bytecode core_models_files) +target_sources(java_bytecode PUBLIC ${sources} ${headers}) generic_includes(java_bytecode) diff --git a/src/java_bytecode/Makefile b/src/java_bytecode/Makefile index c0cbc6daebd..a3f47de2632 100644 --- a/src/java_bytecode/Makefile +++ b/src/java_bytecode/Makefile @@ -40,6 +40,16 @@ CLEANFILES = java_bytecode$(LIBEXT) all: java_bytecode$(LIBEXT) +clean: clean_library + +.PHONY: clean_library +clean_library: + $(MAKE) clean -C library + +library/java_core_models.inc: + $(MAKE) -C library java_core_models.inc + +java_class_loader$(OBJEXT): library/java_core_models.inc ############################################################################### java_bytecode$(LIBEXT): $(OBJ) diff --git a/src/java_bytecode/java_bytecode_language.cpp b/src/java_bytecode/java_bytecode_language.cpp index 2fb13dc36e2..4c12e0b362f 100644 --- a/src/java_bytecode/java_bytecode_language.cpp +++ b/src/java_bytecode/java_bytecode_language.cpp @@ -42,6 +42,7 @@ Author: Daniel Kroening, kroening@kroening.com void java_bytecode_languaget::get_language_options(const cmdlinet &cmd) { assume_inputs_non_null=cmd.isset("java-assume-inputs-non-null"); + java_class_loader.use_core_models=!cmd.isset("no-core-models"); string_refinement_enabled=cmd.isset("refine-strings"); throw_runtime_exceptions=cmd.isset("java-throw-runtime-exceptions"); if(cmd.isset("java-max-input-array-length")) @@ -267,6 +268,24 @@ bool java_bytecode_languaget::typecheck( if(string_refinement_enabled) string_preprocess.initialize_conversion_table(); + // Must load java.lang.Object first to avoid stubbing + // This ordering could alternatively be enforced by + // moving the code below to the class loader. + java_class_loadert::class_mapt::const_iterator it= + java_class_loader.class_map.find("java.lang.Object"); + if(it!=java_class_loader.class_map.end()) + { + if(java_bytecode_convert_class( + it->second, + symbol_table, + get_message_handler(), + max_user_array_length, + method_bytecode, + lazy_methods_mode, + string_preprocess)) + return true; + } + // first generate a new struct symbol for each class and a new function symbol // for every method for(java_class_loadert::class_mapt::const_iterator diff --git a/src/java_bytecode/java_bytecode_language.h b/src/java_bytecode/java_bytecode_language.h index a637fc5f556..63078525407 100644 --- a/src/java_bytecode/java_bytecode_language.h +++ b/src/java_bytecode/java_bytecode_language.h @@ -24,6 +24,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #define JAVA_BYTECODE_LANGUAGE_OPTIONS /*NOLINT*/ \ + "(no-core-models)" \ "(java-assume-inputs-non-null)" \ "(java-throw-runtime-exceptions)" \ "(java-max-input-array-length):" \ @@ -35,19 +36,21 @@ Author: Daniel Kroening, kroening@kroening.com "(java-load-class):" #define JAVA_BYTECODE_LANGUAGE_OPTIONS_HELP /*NOLINT*/ \ - " --java-assume-inputs-non-null never initialize reference-typed parameter to the\n" \ - " entry point with null\n" \ - " --java-throw-runtime-exceptions make implicit runtime exceptions explicit\n" \ - " --java-max-input-array-length N limit input array size to <= N\n" \ - " --java-max-input-tree-depth N object references are (deterministically) set to null in\n"\ - " the object\n" \ - " --java-max-vla-length limit the length of user-code-created arrays\n" \ - " --java-cp-include-files regexp or JSON list of files to load (with '@' prefix)\n" \ - " --lazy-methods only translate methods that appear to be reachable from\n" \ - " the --function entry point or main class\n" \ - " --lazy-methods-extra-entry-point METHODNAME\n" \ - " treat METHODNAME as a possible program entry point for\n" \ - " the purpose of lazy method loading\n" \ + " --no-core-models don't load internally provided models for core classes in\n"/* NOLINT(*) */ \ + " the Java Class Library\n" /* NOLINT(*) */ \ + " --java-assume-inputs-non-null never initialize reference-typed parameter to the\n" /* NOLINT(*) */ \ + " entry point with null\n" /* NOLINT(*) */ \ + " --java-throw-runtime-exceptions make implicit runtime exceptions explicit\n" /* NOLINT(*) */ \ + " --java-max-input-array-length N limit input array size to <= N\n" /* NOLINT(*) */ \ + " --java-max-input-tree-depth N object references are (deterministically) set to null in\n" /* NOLINT(*) */ \ + " the object\n" /* NOLINT(*) */ \ + " --java-max-vla-length limit the length of user-code-created arrays\n" /* NOLINT(*) */ \ + " --java-cp-include-files regexp or JSON list of files to load (with '@' prefix)\n" /* NOLINT(*) */ \ + " --lazy-methods only translate methods that appear to be reachable from\n" /* NOLINT(*) */ \ + " the --function entry point or main class\n" /* NOLINT(*) */ \ + " --lazy-methods-extra-entry-point METHODNAME\n" /* NOLINT(*) */ \ + " treat METHODNAME as a possible program entry point for\n" /* NOLINT(*) */ \ + " the purpose of lazy method loading\n" /* NOLINT(*) */ \ " A '.*' wildcard is allowed to specify all class members\n" #define MAX_NONDET_ARRAY_LENGTH_DEFAULT 5 diff --git a/src/java_bytecode/java_class_loader.cpp b/src/java_bytecode/java_class_loader.cpp index 6749dfbd2e1..838d47f9970 100644 --- a/src/java_bytecode/java_class_loader.cpp +++ b/src/java_bytecode/java_class_loader.cpp @@ -19,6 +19,15 @@ Author: Daniel Kroening, kroening@kroening.com #include "java_bytecode_parser.h" #include "jar_file.h" +#include "library/java_core_models.inc" + +/// This variable stores the data of the file core-models.jar. The macro +/// JAVA_CORE_MODELS_SIZE is defined in the header java_core_models.inc, which +/// gets generated at compile time by running a small utility (converter.cpp) on +/// actual .jar file. The number of bytes in the variable is +/// JAVA_CORE_MODELS_SIZE, another macro defined in java_core_models.inc. +unsigned char java_core_models[] = { JAVA_CORE_MODELS_DATA }; + java_bytecode_parse_treet &java_class_loadert::operator()( const irep_idt &class_name) { @@ -105,6 +114,26 @@ bool java_class_loadert::get_class_file( return false; } +/// Retrieves a class file from the internal jar and loads it into the tree +bool java_class_loadert::get_internal_class_file( + java_class_loader_limitt &class_loader_limit, + const irep_idt &class_name, + java_bytecode_parse_treet &parse_tree) +{ + // Add internal jar file. The name is used to load it once only and + // reference it later. + std::string core_models="core-models.jar"; + jar_pool(class_loader_limit, + core_models, + java_core_models, + JAVA_CORE_MODELS_SIZE); + + // This does not read from the jar file but from the jar_filet object + // as we've just created it + read_jar_file(class_loader_limit, core_models); + return + get_class_file(class_loader_limit, class_name, core_models, parse_tree); +} java_bytecode_parse_treet &java_class_loadert::get_parse_tree( java_class_loader_limitt &class_loader_limit, @@ -120,6 +149,12 @@ java_bytecode_parse_treet &java_class_loadert::get_parse_tree( return parse_tree; } + if(use_core_models) + { + if(get_internal_class_file(class_loader_limit, class_name, parse_tree)) + return parse_tree; + } + // See if we can find it in the class path for(const auto &cp : config.java.classpath) { @@ -283,3 +318,20 @@ void java_class_loadert::add_load_classes(const std::vector &classes) for(const auto &id : classes) java_load_classes.push_back(id); } + +jar_filet &java_class_loadert::jar_pool( + java_class_loader_limitt &class_loader_limit, + const std::string &buffer_name, + const void *pmem, + size_t size) +{ + const auto it=m_archives.find(buffer_name); + if(it==m_archives.end()) + { + // VS: Can't construct in place + auto file=jar_filet(class_loader_limit, pmem, size); + return m_archives.emplace(buffer_name, std::move(file)).first->second; + } + else + return it->second; +} diff --git a/src/java_bytecode/java_class_loader.h b/src/java_bytecode/java_class_loader.h index 9ffe5ae10b4..0fbacb26a65 100644 --- a/src/java_bytecode/java_class_loader.h +++ b/src/java_bytecode/java_class_loader.h @@ -23,6 +23,12 @@ Author: Daniel Kroening, kroening@kroening.com class java_class_loadert:public messaget { public: + // Default constructor does not use core models + // for backward compatibility of unit tests + java_class_loadert() : + use_core_models(true) + {} + java_bytecode_parse_treet &operator()(const irep_idt &); void set_java_cp_include_files(std::string &); @@ -48,6 +54,13 @@ class java_class_loadert:public messaget const std::string &jar_file, java_bytecode_parse_treet &parse_tree); + /// Attempts to load the class from the internal core models. + /// Returns true if found and loaded + bool get_internal_class_file( + java_class_loader_limitt &class_loader_limit, + const irep_idt &class_name, + java_bytecode_parse_treet &parse_tree); + /// Given a \p class_name (e.g. "java.lang.Thread") try to load the /// corresponding .class file by first scanning all .jar files whose /// pathname is stored in \ref jar_files, and if that doesn't work, then scan @@ -68,6 +81,18 @@ class java_class_loadert:public messaget jar_filet &jar_pool(java_class_loader_limitt &limit, const std::string &filename); + /// Load jar archive(from cache if already loaded) + /// \param limit + /// \param buffer_name name of the original file + /// \param pmem memory pointer to the contents of the file + /// \param size size of the memory buffer + /// Note that this mocks the existence of a file which may + /// or may not exist since the actual data bis retrieved from memory. + jar_filet &jar_pool(java_class_loader_limitt &limit, + const std::string &buffer_name, + const void *pmem, + size_t size); + /// An object of this class represents the information of _a single JAR file_ /// that is relevant for a class loader: a map associating logical class names /// with with handles (struct entryt) that describe one .class file inside the @@ -101,6 +126,10 @@ class java_class_loadert:public messaget /// java_class_loader_limitt::setup_class_load_limit() for further /// information. std::string java_cp_include_files; + + /// Indicates that the core models should be loaded + bool use_core_models; + private: std::map m_archives; std::vector java_load_classes; diff --git a/src/java_bytecode/library/CMakeLists.txt b/src/java_bytecode/library/CMakeLists.txt new file mode 100644 index 00000000000..2321ded87d9 --- /dev/null +++ b/src/java_bytecode/library/CMakeLists.txt @@ -0,0 +1,19 @@ +find_package(Java REQUIRED) +include(UseJava) +set(CMAKE_JAVA_COMPILE_FLAGS -sourcepath "src" -d "classes" -XDignore.symbol.file) +file(GLOB_RECURSE java_sources "*.java") +set(JAR_NAME "core-models") +add_jar(${JAR_NAME} ${java_sources}) +get_filename_component(CORE_MODELS_JAR "core-models.jar" REALPATH BASE_DIR ${CMAKE_CURRENT_SOURCE_DIR}) +get_filename_component(JAVA_CORE_MODELS_INC "java_core_models.inc" REALPATH BASE_DIR ${CMAKE_CURRENT_SOURCE_DIR}) +file(GLOB_RECURSE jars "*.jar") +add_executable(java-converter converter.cpp) + +add_custom_target(core_models_files) +add_dependencies(core_models_files ${JAR_NAME}) +add_custom_command(TARGET core_models_files + PRE_BUILD + COMMAND java-converter JAVA_CORE_MODELS core-models.jar > ${JAVA_CORE_MODELS_INC} + ) + +set_source_files_properties("java_core_models.inc" GENERATED) diff --git a/src/java_bytecode/library/Makefile b/src/java_bytecode/library/Makefile index aa51ec1694a..a191f9fd79b 100644 --- a/src/java_bytecode/library/Makefile +++ b/src/java_bytecode/library/Makefile @@ -1,4 +1,11 @@ -all: org.cprover.jar +.NOTPARALLEL: +#javac compiles multiple classes for each source as it will compile dependent sources. +#Thus we do not allow the make to run concurrently. + +SRC = converter.cpp + +include ../../config.inc +include ../../common SOURCE_DIR := src BINARY_DIR := classes @@ -6,21 +13,38 @@ BINARY_DIR := classes FIND := find JAVAC := javac -JFLAGS := -sourcepath $(SOURCE_DIR) -d $(BINARY_DIR) +JFLAGS := -sourcepath $(SOURCE_DIR) -d $(BINARY_DIR) -XDignore.symbol.file CLASSPATH := SOURCE_DIR -all_javas := $(shell $(FIND) $(SOURCE_DIR) -name '*.java') +ALL_JAVAS := $(wildcard $(SOURCE_DIR)/*/*.java $(SOURCE_DIR)/*/*/*.java $(SOURCE_DIR)/*/*/*/*.java) +ALL_CLASSES := $(patsubst $(SOURCE_DIR)/%.java,$(BINARY_DIR)/%.class,$(ALL_JAVAS)) $(BINARY_DIR): mkdir -p $(BINARY_DIR) -.PHONY: compile -compile: $(BINARY_DIR) - $(JAVAC) $(JFLAGS) $(all_javas) +.SUFFIXES: .java .class + +$(BINARY_DIR)/%.class: $(SOURCE_DIR)/%.java $(BINARY_DIR) + $(JAVAC) $(JFLAGS) $(patsubst $(BINARY_DIR)/%.class,$(SOURCE_DIR)/%.java,$@) JAR := jar JARFLAGS := -cf -org.cprover.jar: compile - $(JAR) $(JARFLAGS) $@ -C $(BINARY_DIR) org +core-models.jar: $(ALL_CLASSES) + $(JAR) $(JARFLAGS) $@ -C $(BINARY_DIR) . + +CLEANFILES = core-models.jar converter$(EXEEXT) java_core_models.inc + +all: java_core_models.inc + +clean: clean_ + +clean_: + $(RM) -Rf $(BINARY_DIR) + +converter$(EXEEXT): converter.cpp + $(LINKNATIVE) + +java_core_models.inc: converter$(EXEEXT) core-models.jar + ./converter$(EXEEXT) JAVA_CORE_MODELS core-models.jar > $@ diff --git a/src/java_bytecode/library/converter.cpp b/src/java_bytecode/library/converter.cpp new file mode 100644 index 00000000000..27d083e02dc --- /dev/null +++ b/src/java_bytecode/library/converter.cpp @@ -0,0 +1,72 @@ +/*******************************************************************\ + +Module: + +Author: Dario Cattaruzza + +Date: November 2017 + +\*******************************************************************/ + +#include +#include +#include +#include +#include + +/// Loads a binary file into a c array and creates c and h files to +/// access it from code. +/// +/// This program takes two arguments, a `name` and a path to a file. It loads +/// the given file (usually a .jar file) and dumps to the standard output a +/// header file with two macros, looking like this: +/// +/// ``` +/// \#define MYNAME_DATA 0x01 0x23 0xf4 0x8e 0x9a +/// \#define MYNAME_SIZE 5 +/// ``` +/// The `name` is used as the prefix for the macros (`MYNAME` in the example +/// above). The output content, when included from a C/C++ file, can be used to +/// define an array initialized to the contents of the file, like this: +/// +/// ``` +/// const char myarray[] = { MYNAME_DATA }; +/// const size_t myarray_size = MYNAME_SIZE; +/// ``` +int main(int argc, char *argv[]) +{ + if(argc<2 || strlen(argv[1])==0) + { + printf("Usage: converter VARNAME JAR_FILE\n\n"); + return 1; + } + + std::size_t size=0; + const char *varname=argv[1]; + + printf("// File automatically generated by " __FILE__ "\n\n"); + + printf("#define %s_DATA \\\n ", varname); + std::ifstream src((argc>2) ? argv[2] : "core-models.jar", + std::ios_base::binary); + std::istream &stream=(argc>2) ? src : std::cin; + if(!stream.eof()) + { + size++; + printf("0x%02x", (unsigned char) stream.get()); + + while(!stream.eof()) + { + printf(", "); + if(size % 16 == 0) + printf("\\\n "); + printf("0x%02x", (unsigned char) stream.get()); + size++; + } + printf("\n"); + } + + std::cout << "\n#define " << varname << "_SIZE " << size << "\n\n"; + src.close(); + return 0; +} From a8e659c3fecd53584fe39de15d2ba60cb8e57157 Mon Sep 17 00:00:00 2001 From: Kurt Degiorgio Date: Thu, 25 Jan 2018 18:07:39 +0000 Subject: [PATCH 4/4] Fixed CMake linker ODR violations caused by a regression-test Including .Cpp file in a regression-test was causing linker issues with CMake, specifically ODR (One Definition Rule) violations. Commit addresses this by modifying the test to include the header file instead. --- src/java_bytecode/java_types.cpp | 4 ---- src/java_bytecode/java_types.h | 4 ++++ unit/java_bytecode/java_utils_test.cpp | 2 +- 3 files changed, 5 insertions(+), 5 deletions(-) diff --git a/src/java_bytecode/java_types.cpp b/src/java_bytecode/java_types.cpp index e9d99e44c85..cf3095f1366 100644 --- a/src/java_bytecode/java_types.cpp +++ b/src/java_bytecode/java_types.cpp @@ -29,10 +29,6 @@ std::vector parse_list_types( const char opening_bracket, const char closing_bracket); -size_t find_closing_semi_colon_for_reference_type( - const std::string src, - size_t starting_point = 0); - typet java_int_type() { return signedbv_typet(32); diff --git a/src/java_bytecode/java_types.h b/src/java_bytecode/java_types.h index 3d3758b5407..925640e5a09 100644 --- a/src/java_bytecode/java_types.h +++ b/src/java_bytecode/java_types.h @@ -82,6 +82,10 @@ std::vector java_generic_type_from_string( typet java_bytecode_promotion(const typet &); exprt java_bytecode_promotion(const exprt &); +size_t find_closing_semi_colon_for_reference_type( + const std::string src, + size_t starting_point = 0); + bool is_java_array_tag(const irep_idt &tag); bool is_valid_java_array(const struct_typet &); diff --git a/unit/java_bytecode/java_utils_test.cpp b/unit/java_bytecode/java_utils_test.cpp index 3f3c7e603a6..e2faf4ff920 100644 --- a/unit/java_bytecode/java_utils_test.cpp +++ b/unit/java_bytecode/java_utils_test.cpp @@ -13,7 +13,7 @@ #include -#include +#include #include SCENARIO("Test that the generic signature delimiter lookup works reliably",