diff --git a/regression/cbmc-java/NullPointer2/test.desc b/regression/cbmc-java/NullPointer2/test.desc index f89103d5f52..3be1eaa44fc 100644 --- a/regression/cbmc-java/NullPointer2/test.desc +++ b/regression/cbmc-java/NullPointer2/test.desc @@ -3,7 +3,7 @@ NullPointer2.class --pointer-check --stop-on-fail ^EXIT=10$ ^SIGNAL=0$ -^ file NullPointer2.java line 9 function java::NullPointer2.main:(\[Ljava/lang/String;)V$ +^ file NullPointer2.java line 9 function java::NullPointer2.main:(\[Ljava/lang/String;)V ^VERIFICATION FAILED$ -- ^warning: ignoring diff --git a/regression/cbmc-java/virtual6/test.desc b/regression/cbmc-java/virtual6/test.desc index 8432c7b2303..5a5a7c7bf3b 100644 --- a/regression/cbmc-java/virtual6/test.desc +++ b/regression/cbmc-java/virtual6/test.desc @@ -5,4 +5,3 @@ A.class ^SIGNAL=0$ IF "java::C".*THEN GOTO IF "java::B".*THEN GOTO -IF "java::A".*THEN GOTO diff --git a/regression/cbmc-java/virtual7/A.class b/regression/cbmc-java/virtual7/A.class new file mode 100644 index 00000000000..c6db5120319 Binary files /dev/null and b/regression/cbmc-java/virtual7/A.class differ diff --git a/regression/cbmc-java/virtual7/B.class b/regression/cbmc-java/virtual7/B.class new file mode 100644 index 00000000000..9676ada0b2f Binary files /dev/null and b/regression/cbmc-java/virtual7/B.class differ diff --git a/regression/cbmc-java/virtual7/C.class b/regression/cbmc-java/virtual7/C.class new file mode 100644 index 00000000000..3c1ddff3a73 Binary files /dev/null and b/regression/cbmc-java/virtual7/C.class differ diff --git a/regression/cbmc-java/virtual7/D.class b/regression/cbmc-java/virtual7/D.class new file mode 100644 index 00000000000..d32bf62bcd5 Binary files /dev/null and b/regression/cbmc-java/virtual7/D.class differ diff --git a/regression/cbmc-java/virtual7/E.class b/regression/cbmc-java/virtual7/E.class new file mode 100644 index 00000000000..582841ed28c Binary files /dev/null and b/regression/cbmc-java/virtual7/E.class differ diff --git a/regression/cbmc-java/virtual7/test.class b/regression/cbmc-java/virtual7/test.class new file mode 100644 index 00000000000..38d77aa50e8 Binary files /dev/null and b/regression/cbmc-java/virtual7/test.class differ diff --git a/regression/cbmc-java/virtual7/test.desc b/regression/cbmc-java/virtual7/test.desc new file mode 100644 index 00000000000..b2b26ecb9ce --- /dev/null +++ b/regression/cbmc-java/virtual7/test.desc @@ -0,0 +1,12 @@ +CORE +test.class +--show-goto-functions +^EXIT=0$ +^SIGNAL=0$ +IF "java::E".*THEN GOTO [12] +IF "java::B".*THEN GOTO [12] +IF "java::D".*THEN GOTO [12] +IF "java::C".*THEN GOTO [12] +-- +IF "java::A".*THEN GOTO +GOTO 4 diff --git a/regression/cbmc-java/virtual7/test.java b/regression/cbmc-java/virtual7/test.java new file mode 100644 index 00000000000..dc2d3043925 --- /dev/null +++ b/regression/cbmc-java/virtual7/test.java @@ -0,0 +1,25 @@ +public class test { + public static void main() { + A[] as = { new A(), new B(), new C(), new D(), new E() }; + as[2].f(); + } +} + +class A { + void f() { } +} + + +class B extends A { + void f() { } +} + +class C extends A { + void f() { } +} + +class D extends C { +} + +class E extends B { +} diff --git a/src/goto-programs/remove_virtual_functions.cpp b/src/goto-programs/remove_virtual_functions.cpp index 56c89dac3f0..da9cce5039f 100644 --- a/src/goto-programs/remove_virtual_functions.cpp +++ b/src/goto-programs/remove_virtual_functions.cpp @@ -104,6 +104,8 @@ void remove_virtual_functionst::remove_virtual_function( const code_function_callt &code= to_code_function_call(target->code); + const auto &vcall_source_loc=target->source_location; + const exprt &function=code.function(); assert(function.id()==ID_virtual_function); assert(!code.arguments().empty()); @@ -121,9 +123,11 @@ void remove_virtual_functionst::remove_virtual_function( if(functions.size()==1) { assert(target->is_function_call()); - to_code_function_call(target->code).function()= - functions.begin()->symbol_expr; - + if(functions.begin()->symbol_expr==symbol_exprt()) + target->make_skip(); + else + to_code_function_call(target->code).function()= + functions.begin()->symbol_expr; return; } @@ -131,6 +135,8 @@ void remove_virtual_functionst::remove_virtual_function( goto_programt final_skip; goto_programt::targett t_final=final_skip.add_instruction(); + t_final->source_location=vcall_source_loc; + t_final->make_skip(); // build the calls and gotos @@ -142,46 +148,57 @@ void remove_virtual_functionst::remove_virtual_function( // If necessary, cast to the last candidate function to // get the object's clsid. By the structure of get_functions, // this is the parent of all other classes under consideration. - symbol_typet suggested_type(functions.back().class_id); + const auto &base_classid=functions.back().class_id; + const auto &base_function_symbol=functions.back().symbol_expr; + symbol_typet suggested_type(base_classid); exprt c_id2=get_class_identifier_field(this_expr, suggested_type, ns); - goto_programt::targett last_function; - for(const auto &fun : functions) + std::map calls; + // Note backwards iteration, to get the least-derived candidate first. + for(auto it=functions.crbegin(), itend=functions.crend(); it!=itend; ++it) { - goto_programt::targett t1=new_code_calls.add_instruction(); - if(!fun.symbol_expr.get_identifier().empty()) + const auto &fun=*it; + auto insertit=calls.insert( + {fun.symbol_expr.get_identifier(), goto_programt::targett()}); + + // Only create one call sequence per possible target: + if(insertit.second) { + goto_programt::targett t1=new_code_calls.add_instruction(); + t1->source_location=vcall_source_loc; + if(!fun.symbol_expr.get_identifier().empty()) + { // call function - t1->make_function_call(code); - auto &newcall=to_code_function_call(t1->code); - newcall.function()=fun.symbol_expr; - pointer_typet need_type(symbol_typet(fun.symbol_expr.get(ID_C_class))); - if(!type_eq(newcall.arguments()[0].type(), need_type, ns)) - newcall.arguments()[0].make_typecast(need_type); + t1->make_function_call(code); + auto &newcall=to_code_function_call(t1->code); + newcall.function()=fun.symbol_expr; + pointer_typet need_type(symbol_typet(fun.symbol_expr.get(ID_C_class))); + if(!type_eq(newcall.arguments()[0].type(), need_type, ns)) + newcall.arguments()[0].make_typecast(need_type); + } + else + { + // No definition for this type; shouldn't be possible... + t1->make_assertion(false_exprt()); + } + insertit.first->second=t1; + // goto final + goto_programt::targett t3=new_code_calls.add_instruction(); + t3->source_location=vcall_source_loc; + t3->make_goto(t_final, true_exprt()); } - else + + // If this calls the base function we just fall through. + // Otherwise branch to the right call: + if(fun.symbol_expr!=base_function_symbol) { - // No definition for this type; shouldn't be possible... - t1->make_assertion(false_exprt()); + exprt c_id1=constant_exprt(fun.class_id, string_typet()); + goto_programt::targett t4=new_code_gotos.add_instruction(); + t4->source_location=vcall_source_loc; + t4->make_goto(insertit.first->second, equal_exprt(c_id1, c_id2)); } - - last_function=t1; - - // goto final - goto_programt::targett t3=new_code_calls.add_instruction(); - t3->make_goto(t_final, true_exprt()); - - exprt c_id1=constant_exprt(fun.class_id, string_typet()); - - goto_programt::targett t4=new_code_gotos.add_instruction(); - t4->make_goto(t1, equal_exprt(c_id1, c_id2)); } - // In any other case (most likely a stub class) call the most basic - // version of the method we know to exist: - goto_programt::targett fallthrough=new_code_gotos.add_instruction(); - fallthrough->make_goto(last_function); - goto_programt new_code; // patch them all together