From 126e90ae08a91cc1716c540c83e98a2e1a39056b Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Sat, 10 Mar 2018 10:30:31 +0000 Subject: [PATCH] Remove virtual functions: fix no-fallback-function mode Changes since the assume-false-if-no-match mode was introduced had broken it, so this also adds unit tests to ensure that the assume-false mode continues to work in future. --- src/goto-programs/goto_program.h | 9 + .../remove_virtual_functions.cpp | 89 +++-- src/goto-programs/remove_virtual_functions.h | 7 + unit/Makefile | 1 + .../VirtualFunctionsTestChild1.class | Bin 0 -> 279 bytes .../VirtualFunctionsTestChild2.class | Bin 0 -> 279 bytes .../VirtualFunctionsTestGrandchild.class | Bin 0 -> 240 bytes .../VirtualFunctionsTestParent.class | Bin 0 -> 404 bytes .../VirtualFunctionsTestParent.java | 28 ++ ...ove_virtual_functions_without_fallback.cpp | 309 ++++++++++++++++++ .../virtual_functions.cpp | 11 +- 11 files changed, 407 insertions(+), 47 deletions(-) create mode 100644 unit/goto-programs/VirtualFunctionsTestChild1.class create mode 100644 unit/goto-programs/VirtualFunctionsTestChild2.class create mode 100644 unit/goto-programs/VirtualFunctionsTestGrandchild.class create mode 100644 unit/goto-programs/VirtualFunctionsTestParent.class create mode 100644 unit/goto-programs/VirtualFunctionsTestParent.java create mode 100644 unit/goto-programs/remove_virtual_functions_without_fallback.cpp diff --git a/src/goto-programs/goto_program.h b/src/goto-programs/goto_program.h index ebb77a46eae..aa53dfd97d8 100644 --- a/src/goto-programs/goto_program.h +++ b/src/goto-programs/goto_program.h @@ -593,6 +593,15 @@ class goto_programt return end_function; } + const_targett get_end_function() const + { + PRECONDITION(!instructions.empty()); + const auto end_function=std::prev(instructions.end()); + DATA_INVARIANT(end_function->is_end_function(), + "goto program ends on END_FUNCTION"); + return end_function; + } + /// Copy a full goto program, preserving targets void copy_from(const goto_programt &src); diff --git a/src/goto-programs/remove_virtual_functions.cpp b/src/goto-programs/remove_virtual_functions.cpp index a964d156569..fad271b0d27 100644 --- a/src/goto-programs/remove_virtual_functions.cpp +++ b/src/goto-programs/remove_virtual_functions.cpp @@ -178,7 +178,8 @@ void remove_virtual_functionst::remove_virtual_function( // So long as `this` is already not `void*` typed, the second parameter // is ignored: - exprt c_id2=get_class_identifier_field(this_expr, symbol_typet(), ns); + exprt this_class_identifier = + get_class_identifier_field(this_expr, symbol_typet(), ns); // If instructed, add an ASSUME(FALSE) to handle the case where we don't // match any expected type: @@ -191,16 +192,12 @@ void remove_virtual_functionst::remove_virtual_function( // get initial identifier for grouping INVARIANT(!functions.empty(), "Function dispatch table cannot be empty."); - auto last_id = functions.back().symbol_expr.get_identifier(); - // record class_ids for disjunction - std::set class_ids; std::map calls; // Note backwards iteration, to get the fallback candidate first. for(auto it=functions.crbegin(), itend=functions.crend(); it!=itend; ++it) { const auto &fun=*it; - class_ids.insert(fun.class_id); auto insertit=calls.insert( {fun.symbol_expr.get_identifier(), goto_programt::targett()}); @@ -232,49 +229,36 @@ void remove_virtual_functionst::remove_virtual_function( t3->make_goto(t_final, true_exprt()); } - // Emit target if end of dispatch table is reached or if the next element is - // dispatched to another function call. Assumes entries in the functions - // variable to be sorted for the identifier of the function to be called. - auto l_it = std::next(it); - bool next_emit_target = - (l_it == functions.crend()) || - l_it->symbol_expr.get_identifier() != fun.symbol_expr.get_identifier(); - - // The root function call is done via fall-through, so nothing to emit - // explicitly for this. - if(next_emit_target && fun.symbol_expr == last_function_symbol) + // Fall through to the default callee if possible: + if(fallback_action == + virtual_dispatch_fallback_actiont::CALL_LAST_FUNCTION && + fun.symbol_expr == last_function_symbol) { - class_ids.clear(); + // Nothing to do } - - // If this calls the fallback function we just fall through. - // Otherwise branch to the right call: - if(fallback_action!=virtual_dispatch_fallback_actiont::CALL_LAST_FUNCTION || - fun.symbol_expr!=last_function_symbol) + else { - // create a disjunction of class_ids to test - if(next_emit_target && fun.symbol_expr != last_function_symbol) + const constant_exprt fun_class_identifier(fun.class_id, string_typet()); + const equal_exprt class_id_test( + fun_class_identifier, this_class_identifier); + + // If the previous GOTO goes to the same callee, join it + // (e.g. turning IF x GOTO y into IF x || z GOTO y) + if(it != functions.crbegin() && + std::prev(it)->symbol_expr == fun.symbol_expr) { - exprt::operandst or_ops; - for(const auto &id : class_ids) - { - const constant_exprt c_id1(id, string_typet()); - const equal_exprt class_id_test(c_id1, c_id2); - or_ops.push_back(class_id_test); - } - - goto_programt::targett t4 = new_code_gotos.add_instruction(); - t4->source_location = vcall_source_loc; - t4->make_goto(insertit.first->second, disjunction(or_ops)); - - last_id = fun.symbol_expr.get_identifier(); - class_ids.clear(); + INVARIANT( + !new_code_gotos.empty(), + "a dispatch table entry has been processed already, " + "which should have created a GOTO"); + new_code_gotos.instructions.back().guard = + or_exprt(new_code_gotos.instructions.back().guard, class_id_test); } - // record class_id - else if(next_emit_target) + else { - last_id = fun.symbol_expr.get_identifier(); - class_ids.clear(); + goto_programt::targett new_goto = new_code_gotos.add_instruction(); + new_goto->source_location = vcall_source_loc; + new_goto->make_goto(insertit.first->second, class_id_test); } } } @@ -555,20 +539,35 @@ void remove_virtual_functions(goto_model_functiont &function) } void remove_virtual_function( - goto_modelt &goto_model, + symbol_tablet &symbol_table, goto_programt &goto_program, goto_programt::targett instruction, const dispatch_table_entriest &dispatch_table, virtual_dispatch_fallback_actiont fallback_action) { class_hierarchyt class_hierarchy; - class_hierarchy(goto_model.symbol_table); - remove_virtual_functionst rvf(goto_model.symbol_table, class_hierarchy); + class_hierarchy(symbol_table); + remove_virtual_functionst rvf(symbol_table, class_hierarchy); rvf.remove_virtual_function( goto_program, instruction, dispatch_table, fallback_action); } +void remove_virtual_function( + goto_modelt &goto_model, + goto_programt &goto_program, + goto_programt::targett instruction, + const dispatch_table_entriest &dispatch_table, + virtual_dispatch_fallback_actiont fallback_action) +{ + remove_virtual_function( + goto_model.symbol_table, + goto_program, + instruction, + dispatch_table, + fallback_action); +} + void collect_virtual_function_callees( const exprt &function, const symbol_table_baset &symbol_table, diff --git a/src/goto-programs/remove_virtual_functions.h b/src/goto-programs/remove_virtual_functions.h index c242f52c852..43bd0f2fea8 100644 --- a/src/goto-programs/remove_virtual_functions.h +++ b/src/goto-programs/remove_virtual_functions.h @@ -66,6 +66,13 @@ void remove_virtual_function( const dispatch_table_entriest &dispatch_table, virtual_dispatch_fallback_actiont fallback_action); +void remove_virtual_function( + symbol_tablet &symbol_table, + goto_programt &goto_program, + goto_programt::targett instruction, + const dispatch_table_entriest &dispatch_table, + virtual_dispatch_fallback_actiont fallback_action); + /// Given a function expression representing a virtual method of a class, /// the function computes all overridden methods of that virtual method. /// \param function: The virtual function expression for which the overridden diff --git a/unit/Makefile b/unit/Makefile index 50cca33c851..540410f56c1 100644 --- a/unit/Makefile +++ b/unit/Makefile @@ -19,6 +19,7 @@ SRC += unit_tests.cpp \ goto-programs/goto_trace_output.cpp \ goto-programs/class_hierarchy_output.cpp \ goto-programs/class_hierarchy_graph.cpp \ + goto-programs/remove_virtual_functions_without_fallback.cpp \ java_bytecode/java_bytecode_convert_class/convert_abstract_class.cpp \ java_bytecode/java_bytecode_parse_generics/parse_generic_class.cpp \ java_bytecode/java_object_factory/gen_nondet_string_init.cpp \ diff --git a/unit/goto-programs/VirtualFunctionsTestChild1.class b/unit/goto-programs/VirtualFunctionsTestChild1.class new file mode 100644 index 0000000000000000000000000000000000000000..5fe7f15c25da4ebd3f279a197b47b6b137b13239 GIT binary patch literal 279 zcmZ{ePYVH26vfXSe}*xJEhUy%C}k-dWhE)He>0vujW;#k_+D1Z!Uyo7^mgRuXD+rR5?y`Z8V%KV*k?1ZNc` zaUf?ZHQE~$n?!`OLWq~+wBWn|y@)q- literal 0 HcmV?d00001 diff --git a/unit/goto-programs/VirtualFunctionsTestChild2.class b/unit/goto-programs/VirtualFunctionsTestChild2.class new file mode 100644 index 0000000000000000000000000000000000000000..23d141e6412be205d6f57d6b34f6139251673321 GIT binary patch literal 279 zcmZ{ePYVH26vfXS!!Z7Bq$sh(!a|m^nVOZPOtXJ@@-*Jmc;kCnDGMLKhmwo35V!6< zw{w2o?(KfL0vMsrXl7liKH&$Ai2_e(%g#_D+*OE}3DlKQ}ekqecEF*SkLvR;y znyjR+o<=)ViAhD|r+Q^ntPg=an7K%#HiMlwiV|#O3C&-aw^h-4_$PedKnE88`7Dc@ nZ-JlXt;I^L+5Q=H;)USw%)QJS&-@2%yiz8eJ#*l&^rSKs@-eh()( +#include + +#include +#include + +/// Try to resolve a classid comparison `expr`, assuming that any accessed +/// classid has value `actual_class_id` +exprt resolve_classid_test( + const exprt &expr, + const irep_idt &actual_class_id, + const namespacet &ns) +{ + if(expr.id() == ID_or || expr.id() == ID_and) + { + exprt resolved = expr; + for(exprt &op : resolved.operands()) + op = resolve_classid_test(op, actual_class_id, ns); + simplify(resolved, ns); + return resolved; + } + + if(expr.op0().id() == ID_constant && expr.op1().id() != ID_constant) + { + exprt swapped = expr; + std::swap(swapped.op0(), swapped.op1()); + return resolve_classid_test(swapped, actual_class_id, ns); + } + + if(expr.op0().id() == ID_member && + to_member_expr(expr.op0()).get_component_name() == "@class_identifier" && + expr.op1().id() == ID_constant && + expr.op1().type().id() == ID_string) + { + exprt resolved = expr; + resolved.op0() = constant_exprt(actual_class_id, expr.op1().type()); + simplify(resolved, ns); + return resolved; + } + + return expr; +} + +static bool is_call_to( + goto_programt::const_targett inst, const irep_idt &callee) +{ + if(!inst->is_function_call()) + return false; + const exprt &callee_expr = to_code_function_call(inst->code).function(); + if(callee_expr.id() != ID_symbol) + return false; + return to_symbol_expr(callee_expr).get_identifier() == callee; +} + +static bool is_assume_false(goto_programt::const_targett inst) +{ + return inst->is_assume() && inst->guard.is_false(); +} + +/// Interpret `program`, resolving classid comparisons assuming any actual +/// callee has class `actual_class_id`, returning the first instruction we +/// arrive at which is neither a SKIP, nor a GOTO that can be resolved in this +/// way. +static goto_programt::const_targett interpret_classid_comparison( + const goto_programt &program, + const irep_idt &actual_class_id, + const namespacet &ns) +{ + REQUIRE(!program.instructions.empty()); + goto_programt::const_targett pc = program.instructions.begin(); + + while(pc != program.instructions.end()) + { + if(pc->type == GOTO) + { + exprt guard = pc->guard; + guard = resolve_classid_test(guard, actual_class_id, ns); + if(guard.is_true()) + { + REQUIRE(pc->targets.begin() != pc->targets.end()); + pc = *(pc->targets.begin()); + } + else if(guard.is_false()) + ++pc; + else + { + // Can't resolve the test, so exit here: + return pc; + } + } + else if(pc->type == SKIP) + { + ++pc; + } + else + { + return pc; + } + } + + return program.get_end_function(); +} + +SCENARIO( + "Remove virtual functions without a fallback function", + "[core][goto-programs][remove_virtual_functions]") +{ + symbol_tablet symbol_table = + load_java_class("VirtualFunctionsTestParent", "goto-programs/"); + namespacet ns(symbol_table); + + goto_programt test_program; + auto virtual_call_inst = test_program.add_instruction(FUNCTION_CALL); + + const symbolt &callee_symbol = + symbol_table.lookup_ref("java::VirtualFunctionsTestParent.f:()V"); + + exprt callee(ID_virtual_function, callee_symbol.type); + callee.set(ID_identifier, callee_symbol.name); + callee.set(ID_C_class, "java::VirtualFunctionsTestParent"); + callee.set(ID_component_name, "f:()V"); + + code_function_callt call; + call.function() = callee; + // Specific argument doesn't matter, so just pass an appropriately typed + // null pointer: + call.arguments().push_back( + null_pointer_exprt( + to_pointer_type(to_code_type(callee.type()).parameters()[0].type()))); + virtual_call_inst->code = call; + + test_program.add_instruction(END_FUNCTION); + + WHEN("Resolving virtual callsite to a single callee") + { + dispatch_table_entriest dispatch_table; + dispatch_table.emplace_back("java::VirtualFunctionsTestParent"); + dispatch_table.back().symbol_expr = callee_symbol.symbol_expr(); + + remove_virtual_function( + symbol_table, + test_program, + virtual_call_inst, + dispatch_table, + virtual_dispatch_fallback_actiont::ASSUME_FALSE); + + THEN("One class should call the target, others should assume false") + { + REQUIRE( + is_call_to( + interpret_classid_comparison( + test_program, "java::VirtualFunctionsTestParent", ns), + "java::VirtualFunctionsTestParent.f:()V")); + REQUIRE( + is_assume_false( + interpret_classid_comparison( + test_program, "java::NoSuchClass", ns))); + } + } + + WHEN("Resolving virtual callsite with two possible callees") + { + dispatch_table_entriest dispatch_table; + dispatch_table.emplace_back("java::VirtualFunctionsTestParent"); + dispatch_table.back().symbol_expr = callee_symbol.symbol_expr(); + dispatch_table.emplace_back("java::VirtualFunctionsTestChild1"); + dispatch_table.back().symbol_expr = + symbol_table.lookup_ref("java::VirtualFunctionsTestChild1.f:()V") + .symbol_expr(); + + remove_virtual_function( + symbol_table, + test_program, + virtual_call_inst, + dispatch_table, + virtual_dispatch_fallback_actiont::ASSUME_FALSE); + + THEN("Each class should call its respective target, " + "others should assume false") + { + REQUIRE( + is_call_to( + interpret_classid_comparison( + test_program, "java::VirtualFunctionsTestParent", ns), + "java::VirtualFunctionsTestParent.f:()V")); + REQUIRE( + is_call_to( + interpret_classid_comparison( + test_program, "java::VirtualFunctionsTestChild1", ns), + "java::VirtualFunctionsTestChild1.f:()V")); + REQUIRE( + is_assume_false( + interpret_classid_comparison( + test_program, "java::NoSuchClass", ns))); + } + } + + WHEN("Resolving virtual callsite with three callees, " + "two of which share a target") + { + dispatch_table_entriest dispatch_table; + dispatch_table.emplace_back("java::VirtualFunctionsTestParent"); + dispatch_table.back().symbol_expr = callee_symbol.symbol_expr(); + dispatch_table.emplace_back("java::VirtualFunctionsTestChild1"); + dispatch_table.back().symbol_expr = + symbol_table.lookup_ref("java::VirtualFunctionsTestChild1.f:()V") + .symbol_expr(); + dispatch_table.emplace_back("java::VirtualFunctionsTestGrandchild"); + dispatch_table.back().symbol_expr = + symbol_table.lookup_ref("java::VirtualFunctionsTestChild1.f:()V") + .symbol_expr(); + + remove_virtual_function( + symbol_table, + test_program, + virtual_call_inst, + dispatch_table, + virtual_dispatch_fallback_actiont::ASSUME_FALSE); + + THEN("Each class should call its respective target, " + "others should assume false") + { + REQUIRE( + is_call_to( + interpret_classid_comparison( + test_program, "java::VirtualFunctionsTestParent", ns), + "java::VirtualFunctionsTestParent.f:()V")); + REQUIRE( + is_call_to( + interpret_classid_comparison( + test_program, "java::VirtualFunctionsTestChild1", ns), + "java::VirtualFunctionsTestChild1.f:()V")); + REQUIRE( + is_call_to( + interpret_classid_comparison( + test_program, "java::VirtualFunctionsTestGrandchild", ns), + "java::VirtualFunctionsTestChild1.f:()V")); + REQUIRE( + is_assume_false( + interpret_classid_comparison( + test_program, "java::NoSuchClass", ns))); + } + } + + WHEN("Resolving virtual callsite with four callees, two sharing a target " + "with different-targeted callees on either side (i.e. [A, B, B, C])") + { + dispatch_table_entriest dispatch_table; + dispatch_table.emplace_back("java::VirtualFunctionsTestParent"); + dispatch_table.back().symbol_expr = callee_symbol.symbol_expr(); + dispatch_table.emplace_back("java::VirtualFunctionsTestChild1"); + dispatch_table.back().symbol_expr = + symbol_table.lookup_ref("java::VirtualFunctionsTestChild1.f:()V") + .symbol_expr(); + dispatch_table.emplace_back("java::VirtualFunctionsTestGrandchild"); + dispatch_table.back().symbol_expr = + symbol_table.lookup_ref("java::VirtualFunctionsTestChild1.f:()V") + .symbol_expr(); + dispatch_table.emplace_back("java::VirtualFunctionsTestChild2"); + dispatch_table.back().symbol_expr = + symbol_table.lookup_ref("java::VirtualFunctionsTestChild2.f:()V") + .symbol_expr(); + + remove_virtual_function( + symbol_table, + test_program, + virtual_call_inst, + dispatch_table, + virtual_dispatch_fallback_actiont::ASSUME_FALSE); + + THEN("Each class should call its respective target, " + "others should assume false") + { + REQUIRE( + is_call_to( + interpret_classid_comparison( + test_program, "java::VirtualFunctionsTestParent", ns), + "java::VirtualFunctionsTestParent.f:()V")); + REQUIRE( + is_call_to( + interpret_classid_comparison( + test_program, "java::VirtualFunctionsTestChild1", ns), + "java::VirtualFunctionsTestChild1.f:()V")); + REQUIRE( + is_call_to( + interpret_classid_comparison( + test_program, "java::VirtualFunctionsTestGrandchild", ns), + "java::VirtualFunctionsTestChild1.f:()V")); + REQUIRE( + is_call_to( + interpret_classid_comparison( + test_program, "java::VirtualFunctionsTestChild2", ns), + "java::VirtualFunctionsTestChild2.f:()V")); + REQUIRE( + is_assume_false( + interpret_classid_comparison( + test_program, "java::NoSuchClass", ns))); + } + } +} diff --git a/unit/java_bytecode/java_virtual_functions/virtual_functions.cpp b/unit/java_bytecode/java_virtual_functions/virtual_functions.cpp index dd19b115df8..c0565c31202 100644 --- a/unit/java_bytecode/java_virtual_functions/virtual_functions.cpp +++ b/unit/java_bytecode/java_virtual_functions/virtual_functions.cpp @@ -92,11 +92,18 @@ SCENARIO( REQUIRE( (disjunction.op0().id() == ID_equal && disjunction.op1().id() == ID_equal)); - const equal_exprt &eq_expr0 = + equal_exprt eq_expr0 = to_equal_expr(disjunction.op0()); - const equal_exprt &eq_expr1 = + equal_exprt eq_expr1 = to_equal_expr(disjunction.op1()); + if(eq_expr0.op0().id() == ID_constant && + to_constant_expr(eq_expr0.op0()).get_value() == "java::O") + { + // Allow either order of the D and O comparisons: + std::swap(eq_expr0, eq_expr1); + } + check_function_call( eq_expr0, "java::D",