Added new cmd option to jbmc, 'java-threading'

Setting this option will enable  support for analysing
multi-threaded java programs. For now, this means that a thread-safe
version of clinit_wrapper is generated. This was made opt-in instead
of opt-out as the inclusion of thread-safe clinit wrapper has negative
implications for performance.

Commit also adds appropriate regression tests that use this flag to test
the resulting modifications to the clinit_wrapper

Author: Degiorgio

regression/cbmc-java/static_init1/test1.desc

@@ -0,0 +1,8 @@
+CORE
+static_init.class
+--function static_init.main --java-threading
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/cbmc-java/static_init2/test1.desc

@@ -0,0 +1,8 @@
+CORE
+static_init.class
+--function static_init.main --java-threading
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/cbmc-java/static_init_order/test3.desc

@@ -0,0 +1,7 @@
+CORE
+static_init_order.class
+--function static_init_order.test1 --trace --java-threading
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--

regression/cbmc-java/static_init_order/test4.desc

@@ -0,0 +1,7 @@
+CORE
+static_init_order.class
+--function static_init_order.test2 --java-threading
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--

src/java_bytecode/java_bytecode_language.cpp

@@ -69,6 +69,11 @@ void java_bytecode_languaget::get_language_options(const cmdlinet &cmd)
   else
     lazy_methods_mode=LAZY_METHODS_MODE_EAGER;
 
+  if(cmd.isset("java-threading"))
+    threading_support = true;
+  else
+    threading_support = false;
+
   if(cmd.isset("java-throw-runtime-exceptions"))
   {
     throw_runtime_exceptions = true;
@@ -701,7 +706,8 @@ bool java_bytecode_languaget::typecheck(
   // For each class that will require a static initializer wrapper, create a
   // function named package.classname::clinit_wrapper, and a corresponding
   // global tracking whether it has run or not:
-  create_static_initializer_wrappers(symbol_table, synthetic_methods);
+  create_static_initializer_wrappers(
+    symbol_table, synthetic_methods, threading_support);
 
   // Now incrementally elaborate methods
   // that are reachable from this entry point.
@@ -961,7 +967,11 @@ bool java_bytecode_languaget::convert_single_method(
     switch(synthetic_method_it->second)
     {
     case synthetic_method_typet::STATIC_INITIALIZER_WRAPPER:
-      symbol.value = get_clinit_wrapper_body(function_id, symbol_table);
+      if(threading_support)
+        symbol.value = get_thread_safe_clinit_wrapper_body(
+          function_id, symbol_table);
+      else
+        symbol.value = get_clinit_wrapper_body(function_id, symbol_table);
       break;
     case synthetic_method_typet::STUB_CLASS_STATIC_INITIALIZER:
       symbol.value =

src/java_bytecode/java_bytecode_language.h

@@ -159,6 +159,7 @@ class java_bytecode_languaget:public languaget
   irep_idt main_class;
   std::vector<irep_idt> main_jar_classes;
   java_class_loadert java_class_loader;
+  bool threading_support;
   bool assume_inputs_non_null;      // assume inputs variables to be non-null
   object_factory_parameterst object_factory_parameters;
   size_t max_user_array_length;     // max size for user code created arrays