Move Java unit tests

Author: peterschrammel

jbmc/unit/CMakeLists.txt

@@ -0,0 +1,52 @@
+file(GLOB_RECURSE sources "*.cpp" "*.h")
+list(APPEND sources  ${CBMC_SOURCE_DIR}/../unit/unit_tests.cpp)
+
+file(GLOB_RECURSE java-testing_utils "java-testing-utils/*.cpp" "java-testing-utils/*.h")
+
+list(REMOVE_ITEM sources
+    # Don't build
+    ${CMAKE_CURRENT_SOURCE_DIR}/sharing_map.cpp
+    ${CMAKE_CURRENT_SOURCE_DIR}/elf_reader.cpp
+    ${CMAKE_CURRENT_SOURCE_DIR}/smt2_parser.cpp
+    ${CMAKE_CURRENT_SOURCE_DIR}/json.cpp
+    ${CMAKE_CURRENT_SOURCE_DIR}/cpp_parser.cpp
+    ${CMAKE_CURRENT_SOURCE_DIR}/osx_fat_reader.cpp
+    ${CMAKE_CURRENT_SOURCE_DIR}/unicode.cpp
+    ${CMAKE_CURRENT_SOURCE_DIR}/wp.cpp
+    ${CMAKE_CURRENT_SOURCE_DIR}/cpp_scanner.cpp
+    ${CMAKE_CURRENT_SOURCE_DIR}/float_utils.cpp
+    ${CMAKE_CURRENT_SOURCE_DIR}/ieee_float.cpp
+
+    # Will be built into a separate library and linked
+    ${java-testing_utils}
+
+    # Intended to fail to compile
+    ${CMAKE_CURRENT_SOURCE_DIR}/util/expr_cast/expr_undefined_casts.cpp
+)
+
+add_subdirectory(java-testing-utils)
+
+add_executable(java-unit ${sources})
+target_include_directories(java-unit
+    PUBLIC
+    ${CBMC_BINARY_DIR}
+    ${CBMC_SOURCE_DIR}
+    ${CBMC_SOURCE_DIR}/../unit
+    ${CMAKE_CURRENT_SOURCE_DIR}
+)
+target_link_libraries(java-unit
+        java-testing-utils
+        testing-utils
+        ansi-c
+        solvers
+        goto-programs
+        goto-instrument-lib
+        cbmc-lib
+)
+
+add_test(
+    NAME java-unit
+    COMMAND $<TARGET_FILE:java-unit>
+    WORKING_DIRECTORY ${CMAKE_CURRENT_SOURCE_DIR}
+)
+set_tests_properties(java-unit PROPERTIES LABELS "CORE;CBMC")

jbmc/unit/Makefile

@@ -0,0 +1,119 @@
+.PHONY: all cprover.dir jprover.dir testing-utils.dir java-testing-utils.dir test
+
+# Source files for test utilities
+SRC = $(CPROVER_DIR)/unit/unit_tests.cpp \
+      # Empty last line
+
+# Test source files
+SRC += java_bytecode/goto-programs/class_hierarchy_output.cpp \
+       java_bytecode/goto-programs/class_hierarchy_graph.cpp \
+       java_bytecode/goto-programs/remove_virtual_functions_without_fallback.cpp \
+       java_bytecode/java_bytecode_convert_class/convert_abstract_class.cpp \
+       java_bytecode/java_bytecode_convert_method/convert_invoke_dynamic.cpp \
+       java_bytecode/java_bytecode_parse_generics/parse_generic_class.cpp \
+       java_bytecode/java_object_factory/gen_nondet_string_init.cpp \
+       java_bytecode/java_bytecode_parse_lambdas/java_bytecode_parse_lambda_method_table.cpp \
+       java_bytecode/java_bytecode_parse_lambdas/java_bytecode_convert_class_lambda_method_handles.cpp \
+       java_bytecode/java_string_library_preprocess/convert_exprt_to_string_exprt.cpp \
+       java_bytecode/java_types/erase_type_arguments.cpp \
+       java_bytecode/java_types/generic_type_index.cpp \
+       java_bytecode/java_types/java_generic_symbol_type.cpp \
+       java_bytecode/java_types/java_type_from_string.cpp \
+       java_bytecode/java_utils_test.cpp \
+       java_bytecode/inherited_static_fields/inherited_static_fields.cpp \
+       pointer-analysis/custom_value_set_analysis.cpp \
+       solvers/refinement/string_constraint_instantiation/instantiate_not_contains.cpp \
+       solvers/refinement/string_refinement/dependency_graph.cpp \
+       solvers/refinement/string_refinement/string_symbol_resolution.cpp \
+       util/expr_iterator.cpp \
+       util/has_subtype.cpp \
+       util/parameter_indices.cpp \
+       util/simplify_expr.cpp \
+       java_bytecode/java_virtual_functions/virtual_functions.cpp \
+       java_bytecode/java_bytecode_parse_generics/parse_generic_superclasses.cpp \
+       # Empty last line
+
+INCLUDES= -I ../src/ -I. -I $(CPROVER_DIR)/src -I $(CPROVER_DIR)/unit
+
+include ../src/config.inc
+include $(CPROVER_DIR)/src/config.inc
+include $(CPROVER_DIR)/src/common
+
+cprover.dir:
+	$(MAKE) $(MAKEARGS) -C $(CPROVER_DIR)/src
+
+jprover.dir:
+	$(MAKE) $(MAKEARGS) -C ../src
+
+cprover-testing-utils.dir:
+	$(MAKE) $(MAKEARGS) -C $(CPROVER_DIR)/unit/testing-utils
+
+java-testing-utils.dir:
+	$(MAKE) $(MAKEARGS) -C java-testing-utils
+
+# We need to link bmc.o to the unit test, so here's everything it depends on...
+BMC_DEPS =$(CPROVER_DIR)/src/cbmc/all_properties$(OBJEXT) \
+          $(CPROVER_DIR)/src/cbmc/bmc$(OBJEXT) \
+          $(CPROVER_DIR)/src/cbmc/bmc_cover$(OBJEXT) \
+          $(CPROVER_DIR)/src/cbmc/bv_cbmc$(OBJEXT) \
+          $(CPROVER_DIR)/src/cbmc/cbmc_dimacs$(OBJEXT) \
+          $(CPROVER_DIR)/src/cbmc/cbmc_languages$(OBJEXT) \
+          $(CPROVER_DIR)/src/cbmc/cbmc_parse_options$(OBJEXT) \
+          $(CPROVER_DIR)/src/cbmc/cbmc_solvers$(OBJEXT) \
+          $(CPROVER_DIR)/src/cbmc/counterexample_beautification$(OBJEXT) \
+          $(CPROVER_DIR)/src/cbmc/fault_localization$(OBJEXT) \
+          $(CPROVER_DIR)/src/cbmc/show_vcc$(OBJEXT) \
+          $(CPROVER_DIR)/src/cbmc/symex_bmc$(OBJEXT) \
+          $(CPROVER_DIR)/src/cbmc/symex_coverage$(OBJEXT) \
+          $(CPROVER_DIR)/src/cbmc/xml_interface$(OBJEXT) \
+          $(CPROVER_DIR)/src/jsil/expr2jsil$(OBJEXT) \
+          $(CPROVER_DIR)/src/jsil/jsil_convert$(OBJEXT) \
+          $(CPROVER_DIR)/src/jsil/jsil_entry_point$(OBJEXT) \
+          $(CPROVER_DIR)/src/jsil/jsil_internal_additions$(OBJEXT) \
+          $(CPROVER_DIR)/src/jsil/jsil_language$(OBJEXT) \
+          $(CPROVER_DIR)/src/jsil/jsil_lex.yy$(OBJEXT) \
+          $(CPROVER_DIR)/src/jsil/jsil_parser$(OBJEXT) \
+          $(CPROVER_DIR)/src/jsil/jsil_parse_tree$(OBJEXT) \
+          $(CPROVER_DIR)/src/jsil/jsil_typecheck$(OBJEXT) \
+          $(CPROVER_DIR)/src/jsil/jsil_types$(OBJEXT) \
+          $(CPROVER_DIR)/src/jsil/jsil_y.tab$(OBJEXT) \
+          # Empty last line
+
+CPROVER_LIBS =../src/java_bytecode/java_bytecode$(LIBEXT) \
+              ../src/miniz/miniz$(OBJEXT) \
+              $(CPROVER_DIR)/src/ansi-c/ansi-c$(LIBEXT) \
+              $(CPROVER_DIR)/src/cpp/cpp$(LIBEXT) \
+              $(CPROVER_DIR)/src/json/json$(LIBEXT) \
+              $(CPROVER_DIR)/src/linking/linking$(LIBEXT) \
+              $(CPROVER_DIR)/src/util/util$(LIBEXT) \
+              $(CPROVER_DIR)/src/big-int/big-int$(LIBEXT) \
+              $(CPROVER_DIR)/src/goto-programs/goto-programs$(LIBEXT) \
+              $(CPROVER_DIR)/src/goto-instrument/goto-instrument$(LIBEXT) \
+              $(CPROVER_DIR)/src/pointer-analysis/pointer-analysis$(LIBEXT) \
+              $(CPROVER_DIR)/src/langapi/langapi$(LIBEXT) \
+              $(CPROVER_DIR)/src/assembler/assembler$(LIBEXT) \
+              $(CPROVER_DIR)/src/analyses/analyses$(LIBEXT) \
+              $(CPROVER_DIR)/src/solvers/solvers$(LIBEXT) \
+              $(BMC_DEPS) \
+              # Empty last line
+
+OBJ += $(CPROVER_LIBS) \
+       $(CPROVER_DIR)/unit/testing-utils/testing-utils$(LIBEXT) \
+       java-testing-utils/java-testing-utils$(LIBEXT)
+
+TESTS = unit_tests$(EXEEXT) \
+        # Empty last line
+
+CLEANFILES = $(TESTS)
+
+all: cprover.dir cprover-testing-utils.dir jprover.dir java-testing-utils.dir
+	$(MAKE) $(MAKEARGS) $(TESTS)
+
+test: all
+	$(foreach test,$(TESTS), (echo Running: $(test); ./$(test)) &&) true
+
+
+###############################################################################
+
+unit_tests$(EXEEXT): $(OBJ)
+	$(LINKBIN)

jbmc/unit/java-testing-utils/CMakeLists.txt

@@ -0,0 +1,11 @@
+file(GLOB_RECURSE sources "*.cpp" "*.h")
+add_library(java-testing-utils ${sources})
+target_link_libraries(java-testing-utils
+    util
+    java_bytecode
+)
+target_include_directories(java-testing-utils
+    PUBLIC
+    ${CMAKE_CURRENT_SOURCE_DIR}/..
+    ${CBMC_SOURCE_DIR}/../unit
+)

jbmc/unit/java-testing-utils/Makefile

@@ -0,0 +1,20 @@
+SRC = \
+  load_java_class.cpp \
+  require_goto_statements.cpp \
+  require_parse_tree.cpp \
+  require_type.cpp \
+  # Empty last line (please keep above list sorted!)
+
+INCLUDES = -I .. -I . -I ../../src -I ../$(CPROVER_DIR)/src -I ../$(CPROVER_DIR)/unit
+
+include ../../src/config.inc
+include ../$(CPROVER_DIR)/src/config.inc
+include ../$(CPROVER_DIR)/src/common
+
+CLEANFILES = java-testing-utils$(LIBEXT)
+
+.PHONY: all
+all: java-testing-utils$(LIBEXT)
+
+java-testing-utils$(LIBEXT): $(OBJ)
+	$(LINKLIB)

unit/testing-utils/load_java_class.cpp renamed to jbmc/unit/java-testing-utils/load_java_class.cpp

@@ -7,7 +7,8 @@
 \*******************************************************************/
 
 #include "load_java_class.h"
-#include "free_form_cmdline.h"
+
+#include <testing-utils/free_form_cmdline.h>
 #include <testing-utils/catch.hpp>
 #include <iostream>
 

unit/testing-utils/load_java_class.h renamed to jbmc/unit/java-testing-utils/load_java_class.h

@@ -7,7 +7,8 @@
 \*******************************************************************/
 
 #include "require_goto_statements.h"
-#include "catch.hpp"
+
+#include <testing-utils/catch.hpp>
 
 #include <algorithm>
 #include <util/expr_iterator.h>

unit/testing-utils/require_goto_statements.cpp renamed to jbmc/unit/java-testing-utils/require_goto_statements.cpp

@@ -13,7 +13,8 @@
 #define CPROVER_JAVA_TESTING_UTILS_REQUIRE_PARSE_TREE_H
 
 #include <java_bytecode/java_bytecode_parse_tree.h>
-#include "catch.hpp"
+
+#include <testing-utils/catch.hpp>
 
 // NOLINTNEXTLINE(readability/namespace)
 namespace require_parse_tree

unit/testing-utils/require_goto_statements.h renamed to jbmc/unit/java-testing-utils/require_goto_statements.h

@@ -7,7 +7,7 @@
 \*******************************************************************/
 
 #include <testing-utils/catch.hpp>
-#include <testing-utils/load_java_class.h>
+#include <java-testing-utils/load_java_class.h>
 #include <testing-utils/require_symbol.h>
 
 SCENARIO(

unit/testing-utils/require_parse_tree.cpp renamed to jbmc/unit/java-testing-utils/require_parse_tree.cpp

@@ -7,7 +7,7 @@
 \*******************************************************************/
 
 #include <testing-utils/catch.hpp>
-#include <testing-utils/load_java_class.h>
+#include <java-testing-utils/load_java_class.h>
 
 #include <goto-programs/class_hierarchy.h>
 
@@ -31,7 +31,7 @@ SCENARIO(
   "[core][goto-programs][class_hierarchy_graph]")
 {
   symbol_tablet symbol_table =
-    load_java_class("HierarchyTest", "goto-programs/");
+    load_java_class("HierarchyTest", "./java_bytecode/goto-programs/");
   class_hierarchy_grapht hierarchy;
   hierarchy.populate(symbol_table);
 

unit/testing-utils/require_parse_tree.h renamed to jbmc/unit/java-testing-utils/require_parse_tree.h

@@ -7,7 +7,7 @@
 \*******************************************************************/
 
 #include <testing-utils/catch.hpp>
-#include <testing-utils/load_java_class.h>
+#include <java-testing-utils/load_java_class.h>
 
 #include <goto-programs/class_hierarchy.h>
 
@@ -40,7 +40,7 @@ SCENARIO(
   "[core][goto-programs][class_hierarchy]")
 {
   symbol_tablet symbol_table =
-    load_java_class("HierarchyTest", "goto-programs/");
+    load_java_class("HierarchyTest", "./java_bytecode/goto-programs/");
   class_hierarchyt hierarchy;
 
   std::stringstream output_stream;

unit/testing-utils/require_type.cpp renamed to jbmc/unit/java-testing-utils/require_type.cpp

@@ -8,7 +8,7 @@
 \*******************************************************************/
 
 #include <testing-utils/catch.hpp>
-#include <testing-utils/load_java_class.h>
+#include <java-testing-utils/load_java_class.h>
 
 #include <util/simplify_expr.h>
 #include <goto-programs/remove_virtual_functions.h>
@@ -114,8 +114,8 @@ SCENARIO(
   "Remove virtual functions without a fallback function",
   "[core][goto-programs][remove_virtual_functions]")
 {
-  symbol_tablet symbol_table =
-    load_java_class("VirtualFunctionsTestParent", "goto-programs/");
+  symbol_tablet symbol_table = load_java_class(
+    "VirtualFunctionsTestParent", "./java_bytecode/goto-programs/");
   namespacet ns(symbol_table);
 
   goto_programt test_program;

unit/testing-utils/require_type.h renamed to jbmc/unit/java-testing-utils/require_type.h

@@ -6,10 +6,10 @@
 
 \*******************************************************************/
 #include <testing-utils/catch.hpp>
-#include <testing-utils/load_java_class.h>
-#include <testing-utils/require_goto_statements.h>
+#include <java-testing-utils/load_java_class.h>
+#include <java-testing-utils/require_goto_statements.h>
 #include <util/config.h>
-#include <testing-utils/require_type.h>
+#include <java-testing-utils/require_type.h>
 #include <testing-utils/require_symbol.h>
 
 // NOTE: To inspect these tests at any point, use expr2java.
@@ -27,7 +27,7 @@ SCENARIO(
   {
     const symbol_tablet &symbol_table = load_java_class(
       "SuperclassInst",
-      "./goto-programs/goto_program_generics",
+      "./java_bytecode/goto_program_generics",
       "SuperclassInst.foo");
 
     WHEN("The method input argument is created in the entry point function")
@@ -68,7 +68,7 @@ SCENARIO(
   {
     const symbol_tablet &symbol_table = load_java_class(
       "SuperclassInst2",
-      "./goto-programs/goto_program_generics",
+      "./java_bytecode/goto_program_generics",
       "SuperclassInst2.foo");
 
     WHEN("The method input argument is created in the entry point function")
@@ -99,7 +99,7 @@ SCENARIO(
   {
     const symbol_tablet &symbol_table = load_java_class(
       "SuperclassInst3",
-      "./goto-programs/goto_program_generics",
+      "./java_bytecode/goto_program_generics",
       "SuperclassInst3.foo");
 
     WHEN("The method input argument is created in the entry point function")
@@ -142,7 +142,7 @@ SCENARIO(
   {
     const symbol_tablet &symbol_table = load_java_class(
       "SuperclassUninstTest",
-      "./goto-programs/goto_program_generics",
+      "./java_bytecode/goto_program_generics",
       "SuperclassUninstTest.foo");
 
     WHEN("The method input argument is created in the entry point function")
@@ -187,7 +187,7 @@ SCENARIO(
   {
     const symbol_tablet &symbol_table = load_java_class(
       "SuperclassMixedTest",
-      "./goto-programs/goto_program_generics",
+      "./java_bytecode/goto_program_generics",
       "SuperclassMixedTest.foo");
 
     WHEN("The method input argument is created in the entry point function")
@@ -240,7 +240,7 @@ SCENARIO(
   {
     const symbol_tablet &symbol_table = load_java_class(
       "SuperclassInnerInst",
-      "./goto-programs/goto_program_generics",
+      "./java_bytecode/goto_program_generics",
       "SuperclassInnerInst.foo");
 
     WHEN("The method input argument is created in the entry point function")
@@ -309,7 +309,7 @@ SCENARIO(
   {
     const symbol_tablet &symbol_table = load_java_class(
       "SuperclassInnerUninstTest",
-      "./goto-programs/goto_program_generics",
+      "./java_bytecode/goto_program_generics",
       "SuperclassInnerUninstTest.foo");
 
     WHEN("The method input argument is created in the entry point function")
@@ -425,7 +425,7 @@ SCENARIO(
   {
     const symbol_tablet &symbol_table = load_java_class(
       "SuperclassUnsupported",
-      "./goto-programs/goto_program_generics",
+      "./java_bytecode/goto_program_generics",
       "SuperclassUnsupported.foo");
 
     THEN("The struct for UnsupportedWrapper1 is complete and non-generic")
@@ -474,7 +474,7 @@ SCENARIO(
   {
     const symbol_tablet &symbol_table = load_java_class(
       "SuperclassOpaque",
-      "./goto-programs/goto_program_generics",
+      "./java_bytecode/goto_program_generics",
       "SuperclassOpaque.foo");
 
     THEN("The struct for OpaqueWrapper is incomplete and not-generic")