Goto checkers for Java require further preprocessing

Author: peterschrammel

jbmc/src/java_bytecode/Makefile

@@ -7,6 +7,7 @@ SRC = bytecode_info.cpp \
       generic_parameter_specialization_map_keys.cpp \
       jar_file.cpp \
       jar_pool.cpp \
+      java_bmc_util.cpp \
       java_bytecode_convert_class.cpp \
       java_bytecode_convert_method.cpp \
       java_bytecode_concurrency_instrumentation.cpp \

jbmc/src/java_bytecode/java_bmc_util.cpp

@@ -0,0 +1,41 @@
+/*******************************************************************\
+
+Module: Bounded Model Checking Utils for Java
+
+Author: Daniel Kroening, Peter Schrammel
+
+ \*******************************************************************/
+
+/// \file
+/// Bounded Model Checking Utils for Java
+
+#include "java_bmc_util.h"
+
+#include <goto-checker/symex_bmc.h>
+#include <goto-programs/abstract_goto_model.h>
+#include <java_bytecode/java_enum_static_init_unwind_handler.h>
+
+void java_setup_symex(
+  const optionst &options,
+  abstract_goto_modelt &goto_model,
+  symex_bmct &symex)
+{
+  // unwinds <clinit> loops to number of enum elements
+  if(options.get_bool_option("java-unwind-enum-static"))
+  {
+    // clang-format off
+    // (it asks for the body to be at the same indent level as the parameters
+    //  for some reason)
+    symex.add_loop_unwind_handler(
+      [&goto_model](
+        const goto_symex_statet::call_stackt &context,
+        unsigned loop_num,
+        unsigned unwind,
+        unsigned &max_unwind)
+      { // NOLINT (*)
+        return java_enum_static_init_unwind_handler(
+          context, loop_num, unwind, max_unwind, goto_model.get_symbol_table());
+      });
+    // clang-format on
+  }
+}

jbmc/src/java_bytecode/java_bmc_util.h

@@ -0,0 +1,25 @@
+/*******************************************************************\
+
+Module: Bounded Model Checking Utils for Java
+
+Author: Daniel Kroening, Peter Schrammel
+
+ \*******************************************************************/
+
+/// \file
+/// Bounded Model Checking Utils for Java
+
+#ifndef CPROVER_JAVA_BYTECODE_JAVA_BMC_UTIL_H
+#define CPROVER_JAVA_BYTECODE_JAVA_BMC_UTIL_H
+
+class abstract_goto_modelt;
+class optionst;
+class symex_bmct;
+
+/// Registers Java-specific preprocessing handlers with goto-symex
+void java_setup_symex(
+  const optionst &options,
+  abstract_goto_modelt &goto_model,
+  symex_bmct &symex);
+
+#endif // CPROVER_JAVA_BYTECODE_JAVA_BMC_UTIL_H

jbmc/src/java_bytecode/java_multi_path_symex_only_checker.h

@@ -0,0 +1,33 @@
+/*******************************************************************\
+
+Module: Goto Checker using Bounded Model Checking for Java
+
+Author: Daniel Kroening, Peter Schrammel
+
+ \*******************************************************************/
+
+/// \file
+/// Goto Checker using Bounded Model Checking for Java
+
+#ifndef CPROVER_JAVA_BYTECODE_JAVA_MULTI_PATH_SYMEX_ONLY_CHECKER_H
+#define CPROVER_JAVA_BYTECODE_JAVA_MULTI_PATH_SYMEX_ONLY_CHECKER_H
+
+#include <goto-checker/multi_path_symex_only_checker.h>
+
+#include "java_bmc_util.h"
+
+class java_multi_path_symex_only_checkert
+  : public multi_path_symex_only_checkert
+{
+public:
+  java_multi_path_symex_only_checkert(
+    const optionst &options,
+    ui_message_handlert &ui_message_handler,
+    abstract_goto_modelt &goto_model)
+    : multi_path_symex_only_checkert(options, ui_message_handler, goto_model)
+  {
+    java_setup_symex(options, goto_model, symex);
+  }
+};
+
+#endif // CPROVER_JAVA_BYTECODE_JAVA_MULTI_PATH_SYMEX_ONLY_CHECKER_H