diff --git a/.gitignore b/.gitignore index f9c16bc3a33..5061a31744a 100644 --- a/.gitignore +++ b/.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 diff --git a/regression/cbmc-java/static_init_order/A.class b/regression/cbmc-java/static_init_order/A.class new file mode 100644 index 00000000000..35252a9e67c Binary files /dev/null and b/regression/cbmc-java/static_init_order/A.class differ diff --git a/regression/cbmc-java/static_init_order/B.class b/regression/cbmc-java/static_init_order/B.class new file mode 100644 index 00000000000..e7895d4f84d Binary files /dev/null and b/regression/cbmc-java/static_init_order/B.class differ diff --git a/regression/cbmc-java/static_init_order/C.class b/regression/cbmc-java/static_init_order/C.class new file mode 100644 index 00000000000..dcf5b9927f0 Binary files /dev/null and b/regression/cbmc-java/static_init_order/C.class differ diff --git a/regression/cbmc-java/static_init_order/static_init_order.class b/regression/cbmc-java/static_init_order/static_init_order.class new file mode 100644 index 00000000000..378088af2e8 Binary files /dev/null and b/regression/cbmc-java/static_init_order/static_init_order.class differ diff --git a/regression/cbmc-java/static_init_order/static_init_order.java b/regression/cbmc-java/static_init_order/static_init_order.java new file mode 100644 index 00000000000..312ccfb8334 --- /dev/null +++ b/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; + } +} diff --git a/regression/cbmc-java/static_init_order/test1.desc b/regression/cbmc-java/static_init_order/test1.desc new file mode 100644 index 00000000000..d80e6850004 --- /dev/null +++ b/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$ +-- diff --git a/regression/cbmc-java/static_init_order/test2.desc b/regression/cbmc-java/static_init_order/test2.desc new file mode 100644 index 00000000000..367eae926c4 --- /dev/null +++ b/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$ +-- diff --git a/src/ansi-c/expr2c.cpp b/src/ansi-c/expr2c.cpp index 2e73a24f7ad..5128b7802b4 100644 --- a/src/ansi-c/expr2c.cpp +++ b/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); diff --git a/src/goto-programs/goto_convert.cpp b/src/goto-programs/goto_convert.cpp index 4234e855cd1..d624b48b45b 100644 --- a/src/goto-programs/goto_convert.cpp +++ b/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); +} diff --git a/src/goto-programs/goto_convert_class.h b/src/goto-programs/goto_convert_class.h index 21fcd1d0140..f6d1ba411f5 100644 --- a/src/goto-programs/goto_convert_class.h +++ b/src/goto-programs/goto_convert_class.h @@ -502,6 +502,11 @@ class goto_convertt:public messaget const irep_idt &id, std::list &dest); + // START_THREAD; ... END_THREAD; + void generate_thread_block( + const code_blockt &thread_body, + goto_programt &dest); + // // misc // diff --git a/src/java_bytecode/java_bytecode_convert_method.cpp b/src/java_bytecode/java_bytecode_convert_method.cpp index fb9b18bd871..31d55841aeb 100644 --- a/src/java_bytecode/java_bytecode_convert_method.cpp +++ b/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(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::(); + // } + // } 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)+".:()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::(), if the class has one static initializer + const irep_idt &real_clinit_name=id2string(classname)+".:()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();