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

Author: dcattaruzza

.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
 

regression/cbmc-java/coreModels/test.class

@@ -0,0 +1,9 @@
+CORE
+test.class
+--show-symbol-table
+^EXIT=0$
+^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

regression/cbmc-java/coreModels/test.desc

@@ -0,0 +1,10 @@
+import org.cprover.CProver;
+class test
+{
+  public static void main(String[] args)
+  {
+    int i=CProver.nondetInt();
+    assert(i!=0);
+  }
+}
+

regression/cbmc-java/coreModels/test.java

@@ -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$

regression/jbmc-strings/java_append_char/test.desc

@@ -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)
 

src/java_bytecode/CMakeLists.txt

@@ -38,8 +38,18 @@ include ../common
 
 CLEANFILES = java_bytecode$(LIBEXT)
 
+clean : clean_library
+
+.PHONY: clean_library
+clean_library :
+	$(MAKE) clean -C library
+
 all: java_bytecode$(LIBEXT)
 
+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)

src/java_bytecode/Makefile

@@ -42,6 +42,7 @@ Author: Daniel Kroening, [email protected]
 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"))
@@ -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
+  // 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

src/java_bytecode/java_bytecode_language.cpp

@@ -24,6 +24,7 @@ Author: Daniel Kroening, [email protected]
 #include <java_bytecode/select_pointer_type.h>
 
 #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, [email protected]
   "(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

src/java_bytecode/java_bytecode_language.h

@@ -19,6 +19,15 @@ Author: Daniel Kroening, [email protected]
 #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<irep_idt> &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;
+}