JBMC Java Core models library #1735

dcattaruzza · 2018-01-15T14:20:22Z

We aim at internalizing a portion of the model-library by turning the jar into an include file.
This will enable us to load the corresponding buffer (or any we need henceforth) from an include file in a similar fashion as we load from a jar file.
Currently this only applies to org.cprover.CProver, and later we'll add other java sources.

tautschnig · 2018-01-15T14:45:14Z

What is a "core model"? The commit message of the second commit has a lot of text, but I'm failing to understand it right at the beginning.

dcattaruzza · 2018-01-15T14:52:14Z

Core models are java class models that are included in the cbmc executable (ie in the core of the analysis). Currently all of our models exist in the model library. The idea is to make a subset of these available with open source jbmc, packaged directly in the executable

tautschnig

I don't claim I need to understand each and every thing, but it really scares me when a commit message sounds innocent (though unclear), but then some core bits of the code are changed as well.

tautschnig · 2018-01-15T14:46:13Z

regression/cbmc-java/coreModels/test.desc

+^SIGNAL=0$
+^Symbol\s*\.*\: java\:\:org\.cprover\.CProver\.\<clinit\>\:\(\)V$
+--
+tests that the core models are  being loaded by checking if the static initializer for the CProver class was


This is missing a second --, unless you really want the test to check that that text does not appear in the output.

tautschnig · 2018-01-15T14:47:08Z

src/java_bytecode/Makefile

+JAR := jar
+JARFLAGS := -cf
+
+.NOTPARALLEL: core-models.jar


Java classes compile together, meaning two javac calls in this make may trigger the same .java compile for an auxiliary class. This avoids the race condition

tautschnig · 2018-01-15T14:47:47Z

src/java_bytecode/java_bytecode_language.cpp

@@ -206,6 +207,24 @@ bool java_bytecode_languaget::typecheck(
  if(string_refinement_enabled)
    string_preprocess.initialize_conversion_table();

+  // Must load java.lang.Object first to avoid stubbing
+  // FIXME: its unclear if this ordering has to be done
+  // here or hard coded inside the classloader.


File an issue to track this?

@dcattaruzza Unless @tautschnig or @peterschrammel think it's better to move this code to the class loader, I propose to leave this code here and update the comment above to say that "This ordering could alternatively be enforced by moving the code below to the class loader."

tautschnig · 2018-01-15T14:58:04Z

src/java_bytecode/java_class_loader.cpp

@@ -74,38 +83,76 @@ 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(


Why does the class loader need to be rewritten when the commit message says this is about putting stuff in a library file?

the class loader needs to load from the internal file buffer

peterschrammel · 2018-01-15T22:12:52Z

src/java_bytecode/jar_file.cpp

+/// to a jar file.
+jar_filet::jar_filet(
+  java_class_loader_limitt &limit,
+  const void *pMem,


no camel case

Also, it would be nice to use a parameter name that is actually descriptive.

peterschrammel · 2018-01-15T22:14:25Z

src/java_bytecode/mz_zip_archive.h

+  /// \param pMem pointer to the memory buffer
+  /// \param size size of the buffer
+  /// \throw Throws std::runtime_error if file cannot be opened
+  explicit mz_zip_archivet(const void *pMem, size_t size);


remove explicit

peterschrammel · 2018-01-15T22:14:39Z

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);
  }
+
+  explicit mz_zip_archive_statet(const void *pMem, size_t size):


remove explicit

peterschrammel · 2018-01-15T22:15:15Z

src/java_bytecode/mz_zip_archive.cpp

+    mz_zip_archive({ })
+  {
+    if(MZ_TRUE!=mz_zip_reader_init_mem(this, pMem, size, 0))
+      throw std::runtime_error("MZT: Could not load data from memory");


Does the user know what MZT is?

MZT is as existing messages in this file.
Do you want these changed?

@dcattaruzza I think it's a good idea to change that message to something more readable, yes. Have a look to the other messages as well.

peterschrammel · 2018-01-15T22:19:23Z

src/java_bytecode/Makefile

+java_class_loader.o: java_core_models.inc java_class_loader.cpp
+	$(CXX) -c $(CP_CXXFLAGS) -o $@ java_class_loader.cpp
+
+java_core_models.inc: converter core-models.jar


This doesn't work on Windows.

@dcattaruzza Appveyor is faling, is it due to this? I think it's not. The idea of compiling multiple files into an .inc file works for the C library, so it should work for the Java class library.

As far as I can tell, Appveyor fails because of shell find -name *.java does not find the java files.
I'm investigating.

Still you should be using $(EXEEXT) here.

peterschrammel · 2018-01-15T22:31:32Z

The commits are a bit mixed up, which makes it hard to review. I suggest the following split:

refactor existing class loader (to make it easy to choose between loading from external or internal jar file later on)
extend class loader to be able to read from internal jar (not using this functionality yet)
jar file converter
add embedded jar file global and use functionality of 2 to wire everything together (should only require minimal changes to the class loader)

dcattaruzza · 2018-01-16T08:40:52Z

@peterschrammel do you mean split the commits or the PR? because I started by doing a smaller PR in the lines of what you're saying and had to include the rest to provide a regression test (the test on the jar buffer is the core models loading) @tautschnig request.

peterschrammel · 2018-01-16T08:46:27Z

Yes, split the commits. I suggest to add the end-to-end regression tests as part of 4 or in a separate commit 5.

cesaro

Remarks and proposal for new commit message

cesaro · 2018-01-16T10:37:23Z

src/java_bytecode/mz_zip_archive.cpp

+    mz_zip_archive({ })
+  {
+    if(MZ_TRUE!=mz_zip_reader_init_mem(this, pMem, size, 0))
+      throw std::runtime_error("MZT: Could not load data from memory");


@dcattaruzza I think it's a good idea to change that message to something more readable, yes. Have a look to the other messages as well.

cesaro · 2018-01-16T10:37:46Z

src/java_bytecode/mz_zip_archive.cpp

@@ -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 *pMem, size_t size):


cesaro · 2018-01-16T10:54:11Z

.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


Please rephrase the commit message as follows:

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

cesaro · 2018-01-16T10:57:32Z

src/java_bytecode/CMakeLists.txt

+
+add_library(java_bytecode ${c_sources} ${sources} ${headers} )
+add_dependencies(java_bytecode core_models_files)
+target_sources(java_bytecode PUBLIC ${sources} ${headers})


@dcattaruzza I remember running twice cmake and it rebuilding for a second time the .jar file, which it should be constructed only once. Has this been fixed?

cesaro · 2018-01-16T10:59:02Z

src/java_bytecode/Makefile

+java_class_loader.o: java_core_models.inc java_class_loader.cpp
+	$(CXX) -c $(CP_CXXFLAGS) -o $@ java_class_loader.cpp
+
+java_core_models.inc: converter core-models.jar


@dcattaruzza Appveyor is faling, is it due to this? I think it's not. The idea of compiling multiple files into an .inc file works for the C library, so it should work for the Java class library.

cesaro · 2018-01-16T11:05:53Z

src/java_bytecode/java_bytecode_language.cpp

@@ -206,6 +207,24 @@ bool java_bytecode_languaget::typecheck(
  if(string_refinement_enabled)
    string_preprocess.initialize_conversion_table();

+  // Must load java.lang.Object first to avoid stubbing
+  // FIXME: its unclear if this ordering has to be done
+  // here or hard coded inside the classloader.


@dcattaruzza Unless @tautschnig or @peterschrammel think it's better to move this code to the class loader, I propose to leave this code here and update the comment above to say that "This ordering could alternatively be enforced by moving the code below to the class loader."

cesaro · 2018-01-16T11:07:09Z

src/java_bytecode/java_bytecode_language.h

-  " --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 the internally provided core models\n"           /* NOLINT(*) */ \


Better: "don't load internally provided models for core classes in the Java Class Library"

Degiorgio · 2018-01-25T18:22:13Z

@peterschrammel done

peterschrammel · 2018-01-25T23:14:18Z

src/java_bytecode/java_bytecode_language.h

-  " --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(*) */ \


use // clang-format off

@peterschrammel just to clarify: I should replace the /* NOLINT(*) */ with // clang-format off ? should this be done for all options or just the one added?

peterschrammel · 2018-01-25T23:15:23Z

LGTM modulo making clang-format happy

cesaro · 2018-01-26T00:03:53Z

@Degiorgio please check that the corresponding TG pointer bump (1406) is correctly pointing to the tip of this PR

tautschnig · 2018-01-26T08:11:43Z

src/java_bytecode/Makefile

@@ -38,8 +38,18 @@ include ../common

 CLEANFILES = java_bytecode$(LIBEXT)

+clean : clean_library


Is there a whitespace after clean? I'm not sure what make's semantics of this are, but I'd rather avoid it. The same seems the be true of the clean_library goal.

tautschnig · 2018-01-26T08:13:09Z

src/java_bytecode/Makefile

+
+.PHONY: clean_library
+clean_library :
+	$(MAKE) clean -C library


Please move all of the above changes below the declaration of the all goal so that all remains the default goal.

tautschnig · 2018-01-26T08:17:00Z

src/java_bytecode/java_class_loader.h

+  /// 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,


No camelcase, please.

tautschnig · 2018-01-26T08:17:41Z

src/java_bytecode/library/Makefile

-	$(JAVAC) $(JFLAGS) $(all_javas)
+.SUFFIXES: .java .class
+
+$(BINARY_DIR)/%.class : $(SOURCE_DIR)/%.java $(BINARY_DIR)


No space before :

tautschnig · 2018-01-26T08:18:18Z

src/java_bytecode/library/Makefile

+clean_ :
+	$(RM) -Rf $(BINARY_DIR)
+
+all: java_core_models.inc


Please make the all goal the first one in this file to make it the default.

tautschnig · 2018-01-26T08:19:02Z

src/java_bytecode/library/Makefile

+all: java_core_models.inc
+
+converter$(EXEEXT): converter.cpp
+	$(CXX) $(CP_CXXFLAGS) -o $@ $<


Please use $(LINKNATIVE) instead of $(CXX) ....

tautschnig · 2018-01-26T08:20:49Z

src/java_bytecode/library/Makefile

+
+java_core_models.inc: converter$(EXEEXT) core-models.jar
+	./converter$(EXEEXT) JAVA_CORE_MODELS core-models.jar > $@
+###############################################################################


I don't think this line is of much value. In other Makefiles, it provides some separation of somewhat "common" rules from very local ones, but using it as the very last line seems pointless.

tautschnig · 2018-01-26T08:22:25Z