Adding concurrency to Java

.gitignore

@@ -117,6 +117,7 @@ src/ansi-c/library/converter
 src/ansi-c/library/converter.exe
 src/util/irep_ids_convert
 src/util/irep_ids_convert.exe
+build/
 
 *.pyc
 

regression/cbmc-java/static_init_order/static_init_order.java

@@ -0,0 +1,51 @@
+public class static_init_order
+{
+  // as per the Java Virtual Machine Specification,
+  // section 5.5, p. 35 we expect the static initializer of
+  // the parent class to be called before the static initializer
+  // of the class in question.
+  //
+  // The following tests will verify the aforementioned behaviour.
+
+  public static void test1()
+  {
+    C object2 = new C();
+    B object  = new B();
+    if(object2.x != 20)
+        // order of init is: C.clint, B.clint, A.clint
+        // This should not be reachable as expected order
+        // should be: C.clint, A.clint, B.clint.
+        assert(false);
+  }
+
+  public static void test2()
+  {
+    C object2 = new C();
+    B object  = new B();
+    // Assertion is expected to fail,
+    // as the only way for object2.x
+    // to be assigned a value of 10 is through
+    // the following incorrect ordering of init calls:
+    // C.clint, B.clint, A.clint
+    assert(object2.x == 10);
+  }
+}
+
+class C
+{
+  public static int x = 0;
+}
+
+class A
+{
+  static {
+    C.x=10;
+  }
+}
+
+class B extends A
+{
+  static {
+    C.x=20;
+  }
+}

regression/cbmc-java/static_init_order/test1.desc

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

regression/cbmc-java/static_init_order/test2.desc

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

src/ansi-c/expr2c.cpp

@@ -2968,6 +2968,12 @@ std::string expr2ct::convert_code(
   if(statement=="unlock")
     return convert_code_unlock(src, indent);
 
+  if(statement==ID_atomic_begin)
+    return indent_str(indent)+"__CPROVER_atomic_begin();";
+
+  if(statement==ID_atomic_end)
+    return indent_str(indent)+"__CPROVER_atomic_end();";
+
   if(statement==ID_function_call)
     return convert_code_function_call(to_code_function_call(src), indent);
 

src/goto-programs/goto_convert.cpp

@@ -344,23 +344,33 @@ void goto_convertt::convert_label(
 
   goto_programt tmp;
 
-  // magic thread creation label?
+  // magic thread creation label.
+  // The "__CPROVER_ASYNC_" signals the start of a sequence of instructions
+  // that can be executed in parallel, i.e, a new thread.
   if(has_prefix(id2string(label), "__CPROVER_ASYNC_"))
   {
-    // this is like a START_THREAD
-    codet tmp_code(ID_start_thread);
-    tmp_code.copy_to_operands(code.op0());
-    tmp_code.add_source_location()=code.source_location();
-    convert(tmp_code, tmp);
+    // the body of the thread is expected to be
+    // in the operand.
+    INVARIANT(code.op0().is_not_nil(),
+      "op0 in magic thread creation label is null");
+
+    // replace the magic thread creation label with a
+    // thread block (START_THREAD...END_THREAD).
+    code_blockt thread_body;
+    thread_body.add(to_code(code.op0()));
+    thread_body.add_source_location()=code.source_location();
+    generate_thread_block(thread_body, dest);
   }
   else
+  {
     convert(to_code(code.op0()), tmp);
 
-  goto_programt::targett target=tmp.instructions.begin();
-  dest.destructive_append(tmp);
+    goto_programt::targett target=tmp.instructions.begin();
+    dest.destructive_append(tmp);
 
-  targets.labels.insert({label, {target, targets.destructor_stack}});
-  target->labels.push_front(label);
+    targets.labels.insert({label, {target, targets.destructor_stack}});
+    target->labels.push_front(label);
+  }
 }
 
 void goto_convertt::convert_gcc_local_label(
@@ -1539,39 +1549,14 @@ void goto_convertt::convert_start_thread(
   const codet &code,
   goto_programt &dest)
 {
-  if(code.operands().size()!=1)
-  {
-    error().source_location=code.find_source_location();
-    error() << "start_thread expects one operand" << eom;
-    throw 0;
-  }
-
   goto_programt::targett start_thread=
     dest.add_instruction(START_THREAD);
-
   start_thread->source_location=code.source_location();
+  start_thread->code=code;
 
-  {
-    // start_thread label;
-    // goto tmp;
-    // label: op0-code
-    // end_thread
-    // tmp: skip
-
-    goto_programt::targett goto_instruction=dest.add_instruction(GOTO);
-    goto_instruction->guard=true_exprt();
-    goto_instruction->source_location=code.source_location();
-
-    goto_programt tmp;
-    convert(to_code(code.op0()), tmp);
-    goto_programt::targett end_thread=tmp.add_instruction(END_THREAD);
-    end_thread->source_location=code.source_location();
-
-    start_thread->targets.push_back(tmp.instructions.begin());
-    dest.destructive_append(tmp);
-    goto_instruction->targets.push_back(dest.add_instruction(SKIP));
-    dest.instructions.back().source_location=code.source_location();
-  }
+  // remember it to do target later
+  targets.gotos.push_back(
+    std::make_pair(start_thread, targets.destructor_stack));
 }
 
 void goto_convertt::convert_end_thread(
@@ -2242,3 +2227,43 @@ void goto_convert(
 
   ::goto_convert(to_code(symbol.value), symbol_table, dest, message_handler);
 }
+
+/// Generates the necessary goto-instructions to represent a thread-block.
+/// Specifically, the following instructions are generated:
+///
+/// A: START_THREAD : C
+/// B: GOTO Z
+/// C: SKIP
+/// D: {THREAD BODY}
+/// E: END_THREAD
+/// Z: SKIP
+///
+/// \param thread_body: sequence of codet's that can be executed
+///   in parallel.
+/// \param [out] dest: resulting goto-instructions.
+void goto_convertt::generate_thread_block(
+  const code_blockt &thread_body,
+  goto_programt &dest)
+{
+  goto_programt preamble, body, postamble;
+
+  goto_programt::targett c=body.add_instruction();
+  c->make_skip();
+  convert(thread_body, body);
+
+  goto_programt::targett e=postamble.add_instruction(END_THREAD);
+  e->source_location=thread_body.source_location();
+  goto_programt::targett z=postamble.add_instruction();
+  z->make_skip();
+
+  goto_programt::targett a=preamble.add_instruction(START_THREAD);
+  a->source_location=thread_body.source_location();
+  a->targets.push_back(c);
+  goto_programt::targett b=preamble.add_instruction();
+  b->source_location=thread_body.source_location();
+  b->make_goto(z);
+
+  dest.destructive_append(preamble);
+  dest.destructive_append(body);
+  dest.destructive_append(postamble);
+}

src/goto-programs/goto_convert_class.h

@@ -502,6 +502,11 @@ class goto_convertt:public messaget
     const irep_idt &id,
     std::list<exprt> &dest);
 
+  // START_THREAD; ... END_THREAD;
+  void generate_thread_block(
+    const code_blockt &thread_body,
+    goto_programt &dest);
+
   //
   // misc
   //

src/java_bytecode/java_bytecode_convert_method.cpp

@@ -984,13 +984,33 @@ exprt java_bytecode_convert_methodt::get_or_create_clinit_wrapper(
   if(!class_needs_clinit(classname))
     return static_cast<const exprt &>(get_nil_irep());
 
+  // if the symbol table already contains the clinit_wrapper() function, return
+  // it
   const irep_idt &clinit_wrapper_name=
     id2string(classname)+"::clinit_wrapper";
   auto findit=symbol_table.symbols.find(clinit_wrapper_name);
   if(findit!=symbol_table.symbols.end())
     return findit->second.symbol_expr();
 
-  // Create the wrapper now:
+  // Otherwise, assume that class C extends class C' and implements interfaces
+  // I1, ..., In. We now create the following function (possibly recursively
+  // creating the clinit_wrapper functions for C' and I1, ..., In):
+  //
+  // java::C::clinit_wrapper()
+  // {
+  //   if (java::C::clinit_already_run == false)
+  //   {
+  //     java::C::clinit_already_run = true; // before recursive calls!
+  //
+  //     java::C'::clinit_wrapper();
+  //     java::I1::clinit_wrapper();
+  //     java::I2::clinit_wrapper();
+  //     // ...
+  //     java::In::clinit_wrapper();
+  //
+  //     java::C::<clinit>();
+  //   }
+  // }
   const irep_idt &already_run_name=
     id2string(classname)+"::clinit_already_run";
   symbolt already_run_symbol;
@@ -1009,24 +1029,20 @@ exprt java_bytecode_convert_methodt::get_or_create_clinit_wrapper(
     already_run_symbol.symbol_expr(),
     false_exprt());
 
+  // the entire body of the function is an if-then-else
   code_ifthenelset wrapper_body;
+
+  // add the condition to the if
   wrapper_body.cond()=check_already_run;
+
+  // add the "already-run = false" statement
   code_blockt init_body;
-  // Note already-run is set *before* calling clinit, in order to prevent
-  // recursion in clinit methods.
   code_assignt set_already_run(already_run_symbol.symbol_expr(), true_exprt());
   init_body.move_to_operands(set_already_run);
-  const irep_idt &real_clinit_name=id2string(classname)+".<clinit>:()V";
-  const symbolt &class_symbol=*symbol_table.lookup(classname);
-
-  auto findsymit=symbol_table.symbols.find(real_clinit_name);
-  if(findsymit!=symbol_table.symbols.end())
-  {
-    code_function_callt call_real_init;
-    call_real_init.function()=findsymit->second.symbol_expr();
-    init_body.move_to_operands(call_real_init);
-  }
 
+  // iterate through the base types and add recursive calls to the
+  // clinit_wrapper()
+  const symbolt &class_symbol=*symbol_table.lookup(classname);
   for(const auto &base : to_class_type(class_symbol.type).bases())
   {
     const auto base_name=to_symbol_type(base.type()).get_identifier();
@@ -1038,8 +1054,18 @@ exprt java_bytecode_convert_methodt::get_or_create_clinit_wrapper(
     init_body.move_to_operands(call_base);
   }
 
+  // call java::C::<clinit>(), if the class has one static initializer
+  const irep_idt &real_clinit_name=id2string(classname)+".<clinit>:()V";
+  auto find_sym_it=symbol_table.symbols.find(real_clinit_name);
+  if(find_sym_it!=symbol_table.symbols.end())
+  {
+    code_function_callt call_real_init;
+    call_real_init.function()=find_sym_it->second.symbol_expr();
+    init_body.move_to_operands(call_real_init);
+  }
   wrapper_body.then_case()=init_body;
 
+  // insert symbol in the symbol table
   symbolt wrapper_method_symbol;
   code_typet wrapper_method_type;
   wrapper_method_type.return_type()=void_typet();