From d978ef96f9f9a1415a94788f6070efa22b1d1133 Mon Sep 17 00:00:00 2001 From: Cesar Rodriguez Date: Tue, 17 Oct 2017 17:25:07 +0100 Subject: [PATCH 1/4] Folder build/ ignored. This is needed due the to the introduction of cmake, which by convention generates build files in a folder named "build" --- .gitignore | 1 + 1 file changed, 1 insertion(+) 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 From 001c1a22ae159848536c3fdd549fbd2abeb43baf Mon Sep 17 00:00:00 2001 From: Kurt Degiorgio Date: Fri, 3 Nov 2017 11:45:33 +0000 Subject: [PATCH 2/4] ireps of type "ID_atomic_begin" and "ID_atomic_end" will now be properly displayed when the "show-symbol-table" flag is specified. --- src/ansi-c/expr2c.cpp | 6 ++++++ 1 file changed, 6 insertions(+) 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); From 5c3997de8dd75e010146ecc194d371b6060b69af Mon Sep 17 00:00:00 2001 From: Kurt Degiorgio Date: Tue, 24 Oct 2017 12:56:29 +0100 Subject: [PATCH 3/4] Refectors how CBMC interprets a codet thread-block The current use of labels starting with a specific prefix (__CPROVER_ASYNC_) is a viable way to insert concurrency related goto-instructions in the goto program for C programs. However, in the context of a java program, where labels are removed by the compiler this is not possible. In-order to facilitate the support of both C and Java concurrency, this commit does the following change: In 'goto_convertt::convert_label' instead of inserting a codet(ID_start_thread) we insert the actual goto-instructions that would have previously been generated by 'goto_convertt::convert_start_thread' when 'ID_started_thread' is being parsed. --- src/goto-programs/goto_convert.cpp | 103 +++++++++++++++---------- src/goto-programs/goto_convert_class.h | 5 ++ 2 files changed, 69 insertions(+), 39 deletions(-) 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 // From 22afc5c45b1625956c7a41728762dbbec272c6a9 Mon Sep 17 00:00:00 2001 From: Cesar Rodriguez Date: Mon, 30 Oct 2017 18:25:13 +0000 Subject: [PATCH 4/4] Fixes wrong invocation order for static initializers The Java Virtual Machine Specification, section 5.5, p. 359 defines that the static initializers of both the parent class or interfaces of a given class must be invoked **before** the class initializer of the class. They were previously being invoked in the opposite order. Two Regression tests added to enforce this behaviour. --- .../cbmc-java/static_init_order/A.class | Bin 0 -> 276 bytes .../cbmc-java/static_init_order/B.class | Bin 0 -> 261 bytes .../cbmc-java/static_init_order/C.class | Bin 0 -> 272 bytes .../static_init_order/static_init_order.class | Bin 0 -> 726 bytes .../static_init_order/static_init_order.java | 51 +++++++++++++++++ .../cbmc-java/static_init_order/test1.desc | 8 +++ .../cbmc-java/static_init_order/test2.desc | 8 +++ .../java_bytecode_convert_method.cpp | 52 +++++++++++++----- 8 files changed, 106 insertions(+), 13 deletions(-) create mode 100644 regression/cbmc-java/static_init_order/A.class create mode 100644 regression/cbmc-java/static_init_order/B.class create mode 100644 regression/cbmc-java/static_init_order/C.class create mode 100644 regression/cbmc-java/static_init_order/static_init_order.class create mode 100644 regression/cbmc-java/static_init_order/static_init_order.java create mode 100644 regression/cbmc-java/static_init_order/test1.desc create mode 100644 regression/cbmc-java/static_init_order/test2.desc 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 0000000000000000000000000000000000000000..35252a9e67cbb6040ad482d5739376389669ec15 GIT binary patch literal 276 zcmYL@K}*9x5QX2QwXth#V-;_Lcu^~~7muMJ0ihuEpm+_NbdfDFftZ&5t>QuO&>zqr zReW2dF1(%LdvAu>Y=71O?s2BjM9{`DIzGBSLP0CCg{?<|#?9@Upc$7_Bj`Ta!c68L zsi|Idnv)zxS^k$)FXg<-%%gSu{Ik}z%@XG&Wi>U`V5S#3zyVr5P6G6BDv$?3==d<# z#ryC%otdmAj;SRz#w8lO%{`CeFa$ok3s!NY{|#BO;VJx`4P3Kt@1s{cMlV!f@cy%E Px3bTrcT6bGc{ut7w~H!l literal 0 HcmV?d00001 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 0000000000000000000000000000000000000000..e7895d4f84d8fc18ea7e40a9d2f6a428f7107292 GIT binary patch literal 261 zcmX^0Z`VEs1_l!b5iSN61|CiZUIspP27Y!10Y(Nko6Nk-5<5l)W)00SMg|t={FGEi z27aH+yi~u^+@#c^ki?`Mpa_Reat>4_S8#r5QF5wVCP-YYxFoS8GdUh47oT60l3Jvf zl~|U@!@$bG#?Bzf!yv>U%*ep#1jLR&>43&CO^z=ski z!A6Ujxt#9|cW(FVKY(Af9T;d-p`&TTv(X~ZiEBczhAL6{h@f}6D}v#t8%bzRRU&7H zT_Cfi2x2CcVHiJ6XOSMVP>xl>KlZuERk$v)b((Et){n$dxUf-iVZ!2Xe1ccNK`fH( zU>-y=%<;w775%qx4$U(B*otVYiHM3jeZ{fnx zvzSO?6TJJMG``tFdq58}-^};EdGCGS{QC3b6u>4rE<7wrTybHUxa`8lQkj>PGF+@m zTy;@0$eN35xGu3SFt;A0snS`T4AO^j8ua=q5)gX=#jSV{XWIgWR{NEJ-Ay7TFuM~E z)brtop3*N(v4E4QG`k~E-OYmV{j=a>o~I2uI79CWl(xeD8K1kG40Wg;$L4h-&4Mfr z_YJn6=t$|?2f?Sn!z_II=yE;qa053zR52saH0VY@7`)rKe{TGd)`=FVU7(V<<)MYP zfIofqqIaOejJ%(@p0J}S)a`Q^^c1Ny)+(9^u(NDPfRot68fWQo;KFYjOFY>i3w-W1 z-j*2!qtiKo_-YDK=U&W{0%goiN_+epi&%RE>&*!YPe-sBot@6>V-)@QBh-!|4^bJR z#C-Xup|f(j1{|I}{%4hRGgxG{Me2EGD-gfYl30*vQ18-2@9qEea+QU#s(bV=y*j%D zsY+;)ZiQN_7q!OVcnq6)zd)_-en;gH(*6Rw@C|a>!}&;zX9t#d&kXJ|FBTU60(R+r AaR2}S literal 0 HcmV?d00001 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/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();