Merge pull request #1718 from cesaro/concurrency-team-small-fixes

Adding concurrency to Java

Author: Thomas Kiley

.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/A.class

@@ -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/B.class

@@ -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/C.class

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

regression/cbmc-java/static_init_order/static_init_order.class

@@ -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);
 

regression/cbmc-java/static_init_order/static_init_order.java

@@ -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);
+}