Add JANALYZER tool

Author: peterschrammel

CMakeLists.txt

@@ -81,6 +81,8 @@ set_target_properties(
     java_bytecode
     jbmc
     jbmc-lib
+    janalyzer
+    janalyzer-lib
     jdiff
     jdiff-lib
     java-testing-utils

jbmc/src/CMakeLists.txt

@@ -16,4 +16,5 @@ endmacro(generic_includes)
 add_subdirectory(miniz)
 add_subdirectory(java_bytecode)
 add_subdirectory(jbmc)
+add_subdirectory(janalyzer)
 add_subdirectory(jdiff)

jbmc/src/Makefile

@@ -1,9 +1,9 @@
-DIRS = jbmc jdiff java_bytecode miniz
+DIRS = janalyzer jbmc jdiff java_bytecode miniz
 
 include config.inc
 
 .PHONY: all
-all: jbmc.dir jdiff.dir
+all: janalyzer.dir jbmc.dir jdiff.dir
 
 # building cbmc proper
 .PHONY: cprover.dir
@@ -13,6 +13,9 @@ cprover.dir:
 .PHONY: java_bytecode.dir
 java_bytecode.dir: miniz.dir
 
+.PHONY: janalyzer.dir
+janalyzer.dir: java_bytecode.dir cprover.dir
+
 .PHONY: jbmc.dir
 jbmc.dir: java_bytecode.dir cprover.dir
 

jbmc/src/janalyzer/CMakeLists.txt

@@ -0,0 +1,26 @@
+# Library
+file(GLOB_RECURSE sources "*.cpp" "*.h")
+list(REMOVE_ITEM sources
+    ${CMAKE_CURRENT_SOURCE_DIR}/janalyzer_main.cpp
+)
+add_library(janalyzer-lib ${sources})
+
+generic_includes(janalyzer-lib)
+
+target_link_libraries(janalyzer-lib
+    ansi-c
+    java_bytecode
+    linking
+    big-int
+    goto-analyzer-lib
+    goto-programs
+    analyses
+    pointer-analysis
+    langapi
+    json
+    util
+)
+
+# Executable
+add_executable(janalyzer janalyzer_main.cpp)
+target_link_libraries(janalyzer janalyzer-lib)

jbmc/src/janalyzer/Makefile

@@ -0,0 +1,49 @@
+SRC = janalyzer_main.cpp \
+      janalyzer_parse_options.cpp \
+      # Empty last line
+
+OBJ += ../$(CPROVER_DIR)/src/ansi-c/ansi-c$(LIBEXT) \
+      ../java_bytecode/java_bytecode$(LIBEXT) \
+      ../$(CPROVER_DIR)/src/linking/linking$(LIBEXT) \
+      ../$(CPROVER_DIR)/src/big-int/big-int$(LIBEXT) \
+      ../$(CPROVER_DIR)/src/goto-programs/goto-programs$(LIBEXT) \
+      ../$(CPROVER_DIR)/src/analyses/analyses$(LIBEXT) \
+      ../$(CPROVER_DIR)/src/pointer-analysis/pointer-analysis$(LIBEXT) \
+      ../$(CPROVER_DIR)/src/langapi/langapi$(LIBEXT) \
+      ../$(CPROVER_DIR)/src/json/json$(LIBEXT) \
+      ../$(CPROVER_DIR)/src/util/util$(LIBEXT) \
+      ..//miniz/miniz$(OBJEXT) \
+      ../$(CPROVER_DIR)/src/goto-analyzer/static_show_domain$(OBJEXT) \
+      ../$(CPROVER_DIR)/src/goto-analyzer/static_simplifier$(OBJEXT) \
+      ../$(CPROVER_DIR)/src/goto-analyzer/static_verifier$(OBJEXT) \
+      ../$(CPROVER_DIR)/src/goto-analyzer/taint_analysis$(OBJEXT) \
+      ../$(CPROVER_DIR)/src/goto-analyzer/taint_parser$(OBJEXT) \
+      ../$(CPROVER_DIR)/src/goto-analyzer/unreachable_instructions$(OBJEXT) \
+      # Empty last line
+
+INCLUDES= -I .. -I ../$(CPROVER_DIR)/src
+
+LIBS =
+
+include ../config.inc
+include ../$(CPROVER_DIR)/src/config.inc
+include ../$(CPROVER_DIR)/src/common
+
+CLEANFILES = janalyzer$(EXEEXT)
+
+all: janalyzer$(EXEEXT)
+
+ifneq ($(wildcard ../jsil/Makefile),)
+  OBJ += ../jsil/jsil$(LIBEXT)
+  CP_CXXFLAGS += -DHAVE_JSIL
+endif
+
+###############################################################################
+
+janalyzer$(EXEEXT): $(OBJ)
+	$(LINKBIN)
+
+.PHONY: janalyzer-mac-signed
+
+janalyzer-mac-signed: janalyzer$(EXEEXT)
+	strip janalyzer$(EXEEXT) ; codesign -v -s $(OSX_IDENTITY) janalyzer$(EXEEXT)

jbmc/src/janalyzer/README.md

@@ -0,0 +1,8 @@
+\ingroup module_hidden
+\defgroup janalyzer janalyzer
+
+# Folder janalyzer
+
+`janalyzer/` is a tool performing static analyses on Java
+programs. It provides a Java front end for many of the static analyses
+in the \ref analyses directory.

jbmc/src/janalyzer/janalyzer_main.cpp

@@ -0,0 +1,29 @@
+/*******************************************************************\
+
+Module: JANALYZER Main Module
+
+Author: Peter Schrammel
+
+\*******************************************************************/
+
+/// \file
+/// JANALYZER Main Module
+
+#include "janalyzer_parse_options.h"
+
+#include <util/unicode.h>
+
+#ifdef _MSC_VER
+int wmain(int argc, const wchar_t **argv_wide)
+{
+  auto vec = narrow_argv(argc, argv_wide);
+  auto narrow = to_c_str_array(std::begin(vec), std::end(vec));
+  auto argv = narrow.data();
+#else
+int main(int argc, const char **argv)
+{
+#endif
+  janalyzer_parse_optionst parse_options(argc, argv);
+
+  return parse_options.main();
+}