From a4d3881d271c02a4ba426a34a6b78cc6a549b6cf Mon Sep 17 00:00:00 2001 From: Owen Date: Thu, 14 Mar 2019 08:31:14 +0000 Subject: [PATCH 1/6] Make symbol_table parameter non-const We will add a symbol to it, so it cannot be const. --- src/goto-programs/remove_virtual_functions.cpp | 10 +++++----- src/goto-programs/remove_virtual_functions.h | 4 ++-- 2 files changed, 7 insertions(+), 7 deletions(-) diff --git a/src/goto-programs/remove_virtual_functions.cpp b/src/goto-programs/remove_virtual_functions.cpp index 7a57cc7dc1..894c741f6a 100644 --- a/src/goto-programs/remove_virtual_functions.cpp +++ b/src/goto-programs/remove_virtual_functions.cpp @@ -23,7 +23,7 @@ class remove_virtual_functionst { public: remove_virtual_functionst( - const symbol_table_baset &_symbol_table, + symbol_table_baset &_symbol_table, const class_hierarchyt &_class_hierarchy); void operator()(goto_functionst &goto_functions); @@ -40,7 +40,7 @@ public: protected: const namespacet ns; - const symbol_table_baset &symbol_table; + symbol_table_baset &symbol_table; const class_hierarchyt &class_hierarchy; @@ -64,7 +64,7 @@ protected: }; remove_virtual_functionst::remove_virtual_functionst( - const symbol_table_baset &_symbol_table, + symbol_table_baset &_symbol_table, const class_hierarchyt &_class_hierarchy) : ns(_symbol_table), symbol_table(_symbol_table), @@ -588,7 +588,7 @@ void remove_virtual_functionst::operator()(goto_functionst &functions) /// Remove virtual function calls from all functions in the specified /// list and replace them with their most derived implementations void remove_virtual_functions( - const symbol_table_baset &symbol_table, + symbol_table_baset &symbol_table, goto_functionst &goto_functions) { class_hierarchyt class_hierarchy; @@ -665,7 +665,7 @@ goto_programt::targett remove_virtual_function( void collect_virtual_function_callees( const exprt &function, - const symbol_table_baset &symbol_table, + symbol_table_baset &symbol_table, const class_hierarchyt &class_hierarchy, dispatch_table_entriest &overridden_functions) { diff --git a/src/goto-programs/remove_virtual_functions.h b/src/goto-programs/remove_virtual_functions.h index 69b8f243ca..5614cafc41 100644 --- a/src/goto-programs/remove_virtual_functions.h +++ b/src/goto-programs/remove_virtual_functions.h @@ -30,7 +30,7 @@ void remove_virtual_functions( goto_modelt &goto_model); void remove_virtual_functions( - const symbol_table_baset &symbol_table, + symbol_table_baset &symbol_table, goto_functionst &goto_functions); /// Remove virtual functions from one function. @@ -112,7 +112,7 @@ goto_programt::targett remove_virtual_function( /// overridden functions will be stored. void collect_virtual_function_callees( const exprt &function, - const symbol_tablet &symbol_table, + symbol_tablet &symbol_table, const class_hierarchyt &class_hierarchy, dispatch_table_entriest &overridden_functions); From c6ea853f8c82a06d6d5f2831c43b1deb2b3795d7 Mon Sep 17 00:00:00 2001 From: Owen Date: Thu, 14 Mar 2019 08:32:45 +0000 Subject: [PATCH 2/6] Use temp variable for `this` in dispatch tables This is so that value-set filtering in symex will filter elements which don't have the correct class identifier out of the value-set for `this`. --- .../remove_virtual_functions.cpp | 37 ++++++++++++++++--- 1 file changed, 32 insertions(+), 5 deletions(-) diff --git a/src/goto-programs/remove_virtual_functions.cpp b/src/goto-programs/remove_virtual_functions.cpp index 894c741f6a..1a0960018a 100644 --- a/src/goto-programs/remove_virtual_functions.cpp +++ b/src/goto-programs/remove_virtual_functions.cpp @@ -12,6 +12,7 @@ Author: Daniel Kroening, kroening@kroening.com #include +#include #include #include "class_identifier.h" @@ -168,7 +169,6 @@ goto_programt::targett remove_virtual_functionst::remove_virtual_function( INVARIANT( target->is_function_call(), "remove_virtual_function must target a FUNCTION_CALL instruction"); - const code_function_callt &code = target->get_function_call(); goto_programt::targett next_target = std::next(target); @@ -199,7 +199,36 @@ goto_programt::targett remove_virtual_functionst::remove_virtual_function( const auto &vcall_source_loc=target->source_location; - // the final target is a skip + // TODO: only make a temporary when argument_for_this contains a dereference + + // Create a temporary for the `this` argument. This is so that value-set + // filtering in symex will reduce the value-set for `this` to those with the + // correct class identifier. + goto_programt new_code_for_this_argument; + + const code_function_callt &original_code = target->get_function_call(); + exprt argument_for_this = original_code.arguments()[0]; + symbolt &temporary_for_this = get_fresh_aux_symbol( + argument_for_this.type(), + "remove_virtual_functions", // TODO: pass function name in to use here? + "this_argument", + vcall_source_loc, + ID_java, //TODO: get this from somewhere + symbol_table); + const symbol_exprt this_expr = temporary_for_this.symbol_expr(); + const typet &this_type = this_expr.type(); + + new_code_for_this_argument.add( + goto_programt::make_decl(this_expr, vcall_source_loc)); + new_code_for_this_argument.add( + goto_programt::make_assignment( + this_expr, argument_for_this, vcall_source_loc)); + + // Adjust the function call to use \p temporary_for_this as its first argument + code_function_callt code(original_code); + code.arguments()[0] = this_expr; + + // Create a skip as the final target for each branch to jump to at the end goto_programt final_skip; goto_programt::targett t_final = @@ -210,9 +239,6 @@ goto_programt::targett remove_virtual_functionst::remove_virtual_function( goto_programt new_code_calls; goto_programt new_code_gotos; - exprt this_expr=code.arguments()[0]; - - const typet &this_type=this_expr.type(); INVARIANT(this_type.id() == ID_pointer, "this parameter must be a pointer"); INVARIANT( this_type.subtype() != empty_typet(), @@ -321,6 +347,7 @@ goto_programt::targett remove_virtual_functionst::remove_virtual_function( goto_programt new_code; // patch them all together + new_code.destructive_append(new_code_for_this_argument); new_code.destructive_append(new_code_gotos); new_code.destructive_append(new_code_calls); new_code.destructive_append(final_skip); From 0589328df0d016d17503e01caa97aa865ce35ca8 Mon Sep 17 00:00:00 2001 From: Owen Date: Thu, 14 Mar 2019 10:10:36 +0000 Subject: [PATCH 3/6] Only create temp var for this arg if needed If the this argument doesn't contain a dereference then value-set filtering will work on it even without creating a temporary variable --- .../remove_virtual_functions.cpp | 86 +++++++++++++------ 1 file changed, 60 insertions(+), 26 deletions(-) diff --git a/src/goto-programs/remove_virtual_functions.cpp b/src/goto-programs/remove_virtual_functions.cpp index 1a0960018a..ef026bd69a 100644 --- a/src/goto-programs/remove_virtual_functions.cpp +++ b/src/goto-programs/remove_virtual_functions.cpp @@ -12,6 +12,8 @@ Author: Daniel Kroening, kroening@kroening.com #include +#include +#include #include #include @@ -145,6 +147,55 @@ static void create_static_function_call( } } +/// If \p argument_for_this contains a dereference then create a temporary +/// variable for it and use that instead +/// \param [in,out] argument_for_this: The first argument of the function call +/// \param symbol_table: The symbol table to add the new symbol to +/// \param vcall_source_loc: The source location of the function call, which is +/// used for new instructions that are added +/// \param [out] new_code_for_this_argument: New instructions are added here +static void process_this_argument( + exprt &argument_for_this, + symbol_table_baset &symbol_table, + const source_locationt &vcall_source_loc, + goto_programt &new_code_for_this_argument) +{ + if(has_subexpr(argument_for_this, ID_dereference)) + { + // Create a temporary for the `this` argument. This is so that + // \ref goto_symext::try_filter_value_sets can reduce the value-set for + // `this` to those elements with the correct class identifier. + symbolt &temp_symbol = get_fresh_aux_symbol( + argument_for_this.type(), + "remove_virtual_functions", // TODO: pass function name in to use here? + "this_argument", + vcall_source_loc, + ID_java, //TODO: get this from somewhere + symbol_table); + const symbol_exprt temp_var_for_this = temp_symbol.symbol_expr(); + + new_code_for_this_argument.add( + goto_programt::make_decl(temp_var_for_this, vcall_source_loc)); + new_code_for_this_argument.add( + goto_programt::make_assignment( + temp_var_for_this, argument_for_this, vcall_source_loc)); + + // Add null check for temp_var_for_this, as the old one won't work any more. We should + // really use java_bytecode_instrumentt::check_null_dereference(), but it is + // in jbmc rather than cbmc. Or we could use create_fatal_assertion(), but it + // returns a code_blockt, which is a bit inconvenient. + const notequal_exprt null_check( + temp_var_for_this, + null_pointer_exprt(to_pointer_type(temp_var_for_this.type()))); + new_code_for_this_argument.add( + goto_programt::make_assertion(null_check, vcall_source_loc)); + new_code_for_this_argument.add( + goto_programt::make_assumption(null_check, vcall_source_loc)); + + argument_for_this = temp_var_for_this; + } +} + /// Replace virtual function call with a static function call /// Achieved by substituting a virtual function with its most derived /// implementation. If there's a type mismatch between implementation @@ -199,34 +250,16 @@ goto_programt::targett remove_virtual_functionst::remove_virtual_function( const auto &vcall_source_loc=target->source_location; - // TODO: only make a temporary when argument_for_this contains a dereference - - // Create a temporary for the `this` argument. This is so that value-set - // filtering in symex will reduce the value-set for `this` to those with the - // correct class identifier. + code_function_callt code(target->get_function_call()); goto_programt new_code_for_this_argument; - const code_function_callt &original_code = target->get_function_call(); - exprt argument_for_this = original_code.arguments()[0]; - symbolt &temporary_for_this = get_fresh_aux_symbol( - argument_for_this.type(), - "remove_virtual_functions", // TODO: pass function name in to use here? - "this_argument", + process_this_argument( + code.arguments()[0], + symbol_table, vcall_source_loc, - ID_java, //TODO: get this from somewhere - symbol_table); - const symbol_exprt this_expr = temporary_for_this.symbol_expr(); - const typet &this_type = this_expr.type(); + new_code_for_this_argument); - new_code_for_this_argument.add( - goto_programt::make_decl(this_expr, vcall_source_loc)); - new_code_for_this_argument.add( - goto_programt::make_assignment( - this_expr, argument_for_this, vcall_source_loc)); - - // Adjust the function call to use \p temporary_for_this as its first argument - code_function_callt code(original_code); - code.arguments()[0] = this_expr; + const exprt &this_expr = code.arguments()[0]; // Create a skip as the final target for each branch to jump to at the end goto_programt final_skip; @@ -239,9 +272,10 @@ goto_programt::targett remove_virtual_functionst::remove_virtual_function( goto_programt new_code_calls; goto_programt new_code_gotos; - INVARIANT(this_type.id() == ID_pointer, "this parameter must be a pointer"); INVARIANT( - this_type.subtype() != empty_typet(), + this_expr.type().id() == ID_pointer, "this parameter must be a pointer"); + INVARIANT( + this_expr.type().subtype() != empty_typet(), "this parameter must not be a void pointer"); // So long as `this` is already not `void*` typed, the second parameter From d7cfc9dbf7f2973e9c852eee03e7671c3f52ec5b Mon Sep 17 00:00:00 2001 From: Owen Date: Sat, 16 Mar 2019 09:25:07 +0000 Subject: [PATCH 4/6] Use correct function identifier in symbol name --- ...ove_virtual_functions_without_fallback.cpp | 10 +++++ .../remove_virtual_functions.cpp | 37 +++++++++++++++---- src/goto-programs/remove_virtual_functions.h | 2 + 3 files changed, 42 insertions(+), 7 deletions(-) diff --git a/jbmc/unit/java_bytecode/goto-programs/remove_virtual_functions_without_fallback.cpp b/jbmc/unit/java_bytecode/goto-programs/remove_virtual_functions_without_fallback.cpp index 4c15e0976c..d6eae20730 100644 --- a/jbmc/unit/java_bytecode/goto-programs/remove_virtual_functions_without_fallback.cpp +++ b/jbmc/unit/java_bytecode/goto-programs/remove_virtual_functions_without_fallback.cpp @@ -116,6 +116,12 @@ SCENARIO( { symbol_tablet symbol_table = load_java_class( "VirtualFunctionsTestParent", "./java_bytecode/goto-programs/"); + const irep_idt test_program_id = "java::testProgram:()V"; + symbolt test_program_symbol{}; + test_program_symbol.mode = ID_java; + test_program_symbol.name = test_program_id; + test_program_symbol.base_name = test_program_id; + symbol_table.insert(test_program_symbol); namespacet ns(symbol_table); goto_programt test_program; @@ -147,6 +153,7 @@ SCENARIO( remove_virtual_function( symbol_table, + test_program_id, test_program, virtual_call_inst, dispatch_table, @@ -178,6 +185,7 @@ SCENARIO( remove_virtual_function( symbol_table, + test_program_id, test_program, virtual_call_inst, dispatch_table, @@ -220,6 +228,7 @@ SCENARIO( remove_virtual_function( symbol_table, + test_program_id, test_program, virtual_call_inst, dispatch_table, @@ -271,6 +280,7 @@ SCENARIO( remove_virtual_function( symbol_table, + test_program_id, test_program, virtual_call_inst, dispatch_table, diff --git a/src/goto-programs/remove_virtual_functions.cpp b/src/goto-programs/remove_virtual_functions.cpp index ef026bd69a..cb4f15621b 100644 --- a/src/goto-programs/remove_virtual_functions.cpp +++ b/src/goto-programs/remove_virtual_functions.cpp @@ -31,9 +31,12 @@ public: void operator()(goto_functionst &goto_functions); - bool remove_virtual_functions(goto_programt &goto_program); + bool remove_virtual_functions( + const irep_idt &function_id, + goto_programt &goto_program); goto_programt::targett remove_virtual_function( + const irep_idt &function_id, goto_programt &goto_program, goto_programt::targett target, const dispatch_table_entriest &functions, @@ -48,6 +51,7 @@ protected: const class_hierarchyt &class_hierarchy; goto_programt::targett remove_virtual_function( + const irep_idt &function_id, goto_programt &goto_program, goto_programt::targett target); typedef std::function< @@ -77,12 +81,15 @@ remove_virtual_functionst::remove_virtual_functionst( /// Replace specified virtual function call with a static call to its /// most derived implementation +/// \param function_id: The identifier of the function we are currently +/// analysing /// \param [in,out] goto_program: GOTO program to modify /// \param target: iterator to a function in the supplied GOTO program /// to replace. Must point to a virtual function call. /// \return Returns a pointer to the statement in the supplied GOTO /// program after replaced function call goto_programt::targett remove_virtual_functionst::remove_virtual_function( + const irep_idt &function_id, goto_programt &goto_program, goto_programt::targett target) { @@ -100,6 +107,7 @@ goto_programt::targett remove_virtual_functionst::remove_virtual_function( get_functions(function, functions); return remove_virtual_function( + function_id, goto_program, target, functions, @@ -149,12 +157,15 @@ static void create_static_function_call( /// If \p argument_for_this contains a dereference then create a temporary /// variable for it and use that instead +/// \param function_id: The identifier of the function we are currently +/// analysing /// \param [in,out] argument_for_this: The first argument of the function call /// \param symbol_table: The symbol table to add the new symbol to /// \param vcall_source_loc: The source location of the function call, which is /// used for new instructions that are added /// \param [out] new_code_for_this_argument: New instructions are added here static void process_this_argument( + const irep_idt &function_id, exprt &argument_for_this, symbol_table_baset &symbol_table, const source_locationt &vcall_source_loc, @@ -167,10 +178,10 @@ static void process_this_argument( // `this` to those elements with the correct class identifier. symbolt &temp_symbol = get_fresh_aux_symbol( argument_for_this.type(), - "remove_virtual_functions", // TODO: pass function name in to use here? + id2string(function_id), "this_argument", vcall_source_loc, - ID_java, //TODO: get this from somewhere + symbol_table.lookup_ref(function_id).mode, symbol_table); const symbol_exprt temp_var_for_this = temp_symbol.symbol_expr(); @@ -201,6 +212,8 @@ static void process_this_argument( /// implementation. If there's a type mismatch between implementation /// and the instance type or if fallback_action is set to /// ASSUME_FALSE, then function is substituted with a call to ASSUME(false) +/// \param function_id: The identifier of the function we are currently +/// analysing /// \param [in,out] goto_program: GOTO program to modify /// \param target: Iterator to the GOTO instruction in the supplied /// GOTO program to be removed. Must point to a function call @@ -212,6 +225,7 @@ static void process_this_argument( /// \return Returns a pointer to the statement in the supplied GOTO /// program after replaced function call goto_programt::targett remove_virtual_functionst::remove_virtual_function( + const irep_idt &function_id, goto_programt &goto_program, goto_programt::targett target, const dispatch_table_entriest &functions, @@ -254,6 +268,7 @@ goto_programt::targett remove_virtual_functionst::remove_virtual_function( goto_programt new_code_for_this_argument; process_this_argument( + function_id, code.arguments()[0], symbol_table, vcall_source_loc, @@ -595,6 +610,7 @@ exprt remove_virtual_functionst::get_method( /// them with calls to their most derived implementations. Returns /// true if at least one function has been replaced. bool remove_virtual_functionst::remove_virtual_functions( + const irep_idt &function_id, goto_programt &goto_program) { bool did_something=false; @@ -610,7 +626,7 @@ bool remove_virtual_functionst::remove_virtual_functions( if(code.function().id()==ID_virtual_function) { - target = remove_virtual_function(goto_program, target); + target = remove_virtual_function(function_id, goto_program, target); did_something=true; continue; } @@ -636,9 +652,10 @@ void remove_virtual_functionst::operator()(goto_functionst &functions) f_it!=functions.function_map.end(); f_it++) { + const irep_idt &function_id = f_it->first; goto_programt &goto_program=f_it->second.body; - if(remove_virtual_functions(goto_program)) + if(remove_virtual_functions(function_id, goto_program)) did_something=true; } @@ -671,7 +688,8 @@ void remove_virtual_functions(goto_model_functiont &function) class_hierarchyt class_hierarchy; class_hierarchy(function.get_symbol_table()); remove_virtual_functionst rvf(function.get_symbol_table(), class_hierarchy); - rvf.remove_virtual_functions(function.get_goto_function().body); + rvf.remove_virtual_functions( + function.get_function_id(), function.get_goto_function().body); } /// Replace virtual function call with a static function call @@ -680,6 +698,8 @@ void remove_virtual_functions(goto_model_functiont &function) /// and the instance type or if fallback_action is set to /// ASSUME_FALSE, then function is substituted with a call to ASSUME(false) /// \param symbol_table: Symbol table +/// \param function_id: The identifier of the function we are currently +/// analysing /// \param [in,out] goto_program: GOTO program to modify /// \param instruction: Iterator to the GOTO instruction in the supplied /// GOTO program to be removed. Must point to a function call @@ -692,6 +712,7 @@ void remove_virtual_functions(goto_model_functiont &function) /// program after replaced function call goto_programt::targett remove_virtual_function( symbol_tablet &symbol_table, + const irep_idt &function_id, goto_programt &goto_program, goto_programt::targett instruction, const dispatch_table_entriest &dispatch_table, @@ -702,7 +723,7 @@ goto_programt::targett remove_virtual_function( remove_virtual_functionst rvf(symbol_table, class_hierarchy); goto_programt::targett next = rvf.remove_virtual_function( - goto_program, instruction, dispatch_table, fallback_action); + function_id, goto_program, instruction, dispatch_table, fallback_action); goto_program.update(); @@ -711,6 +732,7 @@ goto_programt::targett remove_virtual_function( goto_programt::targett remove_virtual_function( goto_modelt &goto_model, + const irep_idt &function_id, goto_programt &goto_program, goto_programt::targett instruction, const dispatch_table_entriest &dispatch_table, @@ -718,6 +740,7 @@ goto_programt::targett remove_virtual_function( { return remove_virtual_function( goto_model.symbol_table, + function_id, goto_program, instruction, dispatch_table, diff --git a/src/goto-programs/remove_virtual_functions.h b/src/goto-programs/remove_virtual_functions.h index 5614cafc41..1f97f81206 100644 --- a/src/goto-programs/remove_virtual_functions.h +++ b/src/goto-programs/remove_virtual_functions.h @@ -90,6 +90,7 @@ typedef std::map dispatch_table_entries_mapt; goto_programt::targett remove_virtual_function( goto_modelt &goto_model, + const irep_idt &function_id, goto_programt &goto_program, goto_programt::targett instruction, const dispatch_table_entriest &dispatch_table, @@ -97,6 +98,7 @@ goto_programt::targett remove_virtual_function( goto_programt::targett remove_virtual_function( symbol_tablet &symbol_table, + const irep_idt &function_id, goto_programt &goto_program, goto_programt::targett instruction, const dispatch_table_entriest &dispatch_table, From 3e1d0d0dc7577ad8751e80e76dbd0b9f5a562ab1 Mon Sep 17 00:00:00 2001 From: Owen Date: Sun, 17 Mar 2019 07:57:44 +0000 Subject: [PATCH 5/6] Copy directly preceding ASSUMEs Copy directly preceding ASSUMEs, changing the argument for `this` to the new temporary variable for `this`. This is mainly aimed at null checks, to make the local safe pointer analysis work. We stop as soon as we find an instruction that is not an ASSERT or ASSUME. --- .../remove_virtual_functions.cpp | 81 ++++++++++++++++--- 1 file changed, 70 insertions(+), 11 deletions(-) diff --git a/src/goto-programs/remove_virtual_functions.cpp b/src/goto-programs/remove_virtual_functions.cpp index cb4f15621b..da97a81717 100644 --- a/src/goto-programs/remove_virtual_functions.cpp +++ b/src/goto-programs/remove_virtual_functions.cpp @@ -155,10 +155,70 @@ static void create_static_function_call( } } +/// Duplicate ASSUME instructions involving \p argument_for_this for +/// \p temp_var_for_this. We only look at the ASSERT and ASSUME instructions +/// which directly precede the virtual function call. This is mainly aimed at +/// null checks, because \ref local_safe_pointerst would otherwise lose track +/// of known-not-null pointers due to the newly introduced assignment. +/// \param goto_program: The goto program containing the virtual function call +/// \param instr_it: Iterator to the virtual function call in \p goto_program +/// \param argument_for_this: The original expression for the this argument of +/// the virtual function call +/// \param temp_var_for_this: The new expression for the this argument of the +/// virtual function call +/// \return A goto program consisting of all the amended asserts and assumes +static goto_programt analyse_checks_directly_preceding_function_call( + const goto_programt &goto_program, + goto_programt::const_targett instr_it, + const exprt &argument_for_this, + const symbol_exprt &temp_var_for_this) +{ + goto_programt checks_directly_preceding_function_call; + + while(instr_it != goto_program.instructions.cbegin()) + { + instr_it = std::prev(instr_it); + + if(instr_it->type == ASSERT) + { + continue; + } + + if(instr_it->type != ASSUME) + { + break; + } + + exprt guard = instr_it->get_condition(); + + bool changed = false; + for(auto expr_it = guard.depth_begin(); expr_it != guard.depth_end(); + ++expr_it) + { + if(*expr_it == argument_for_this) + { + expr_it.mutate() = temp_var_for_this; + changed = true; + } + } + + if(changed) + { + checks_directly_preceding_function_call.insert_before( + checks_directly_preceding_function_call.instructions.cbegin(), + goto_programt::make_assumption(guard)); + } + } + + return checks_directly_preceding_function_call; +} + /// If \p argument_for_this contains a dereference then create a temporary /// variable for it and use that instead /// \param function_id: The identifier of the function we are currently /// analysing +/// \param goto_program: The goto program containing the virtual function call +/// \param target: Iterator to the virtual function call in \p goto_program /// \param [in,out] argument_for_this: The first argument of the function call /// \param symbol_table: The symbol table to add the new symbol to /// \param vcall_source_loc: The source location of the function call, which is @@ -166,6 +226,8 @@ static void create_static_function_call( /// \param [out] new_code_for_this_argument: New instructions are added here static void process_this_argument( const irep_idt &function_id, + const goto_programt &goto_program, + const goto_programt::targett target, exprt &argument_for_this, symbol_table_baset &symbol_table, const source_locationt &vcall_source_loc, @@ -191,17 +253,12 @@ static void process_this_argument( goto_programt::make_assignment( temp_var_for_this, argument_for_this, vcall_source_loc)); - // Add null check for temp_var_for_this, as the old one won't work any more. We should - // really use java_bytecode_instrumentt::check_null_dereference(), but it is - // in jbmc rather than cbmc. Or we could use create_fatal_assertion(), but it - // returns a code_blockt, which is a bit inconvenient. - const notequal_exprt null_check( - temp_var_for_this, - null_pointer_exprt(to_pointer_type(temp_var_for_this.type()))); - new_code_for_this_argument.add( - goto_programt::make_assertion(null_check, vcall_source_loc)); - new_code_for_this_argument.add( - goto_programt::make_assumption(null_check, vcall_source_loc)); + goto_programt checks_directly_preceding_function_call = + analyse_checks_directly_preceding_function_call( + goto_program, target, argument_for_this, temp_var_for_this); + + new_code_for_this_argument.destructive_append( + checks_directly_preceding_function_call); argument_for_this = temp_var_for_this; } @@ -269,6 +326,8 @@ goto_programt::targett remove_virtual_functionst::remove_virtual_function( process_this_argument( function_id, + goto_program, + target, code.arguments()[0], symbol_table, vcall_source_loc, From 77075e680bbdee84c3f2528426700c7b8717e4ef Mon Sep 17 00:00:00 2001 From: Owen Date: Tue, 19 Mar 2019 09:13:47 +0000 Subject: [PATCH 6/6] Test temp var for this argument in virtual function calls A temporary variable should be created for the `this` argument of a virtual function call when there is a dispatch table and the `this` argument involves a dereference. --- .../A.class | Bin 0 -> 292 bytes .../AContainer.class | Bin 0 -> 273 bytes .../B.class | Bin 0 -> 277 bytes .../Main.class | Bin 0 -> 708 bytes .../Main.java | 30 ++++++++++++++++++ .../test_one_candidate.desc | 12 +++++++ .../test_two_candidates_no_derefs.desc | 13 ++++++++ .../test_two_candidates_with_derefs.desc | 14 ++++++++ 8 files changed, 69 insertions(+) create mode 100644 jbmc/regression/jbmc/virtual_temp_var_for_this_argument/A.class create mode 100644 jbmc/regression/jbmc/virtual_temp_var_for_this_argument/AContainer.class create mode 100644 jbmc/regression/jbmc/virtual_temp_var_for_this_argument/B.class create mode 100644 jbmc/regression/jbmc/virtual_temp_var_for_this_argument/Main.class create mode 100644 jbmc/regression/jbmc/virtual_temp_var_for_this_argument/Main.java create mode 100644 jbmc/regression/jbmc/virtual_temp_var_for_this_argument/test_one_candidate.desc create mode 100644 jbmc/regression/jbmc/virtual_temp_var_for_this_argument/test_two_candidates_no_derefs.desc create mode 100644 jbmc/regression/jbmc/virtual_temp_var_for_this_argument/test_two_candidates_with_derefs.desc diff --git a/jbmc/regression/jbmc/virtual_temp_var_for_this_argument/A.class b/jbmc/regression/jbmc/virtual_temp_var_for_this_argument/A.class new file mode 100644 index 0000000000000000000000000000000000000000..c9cbb14f58c6a3122bac141d26403eba6461b8ea GIT binary patch literal 292 zcmZ9G%?`mp6ot>NQmTHRz|v2m8#^KqiB+*6_R|`SRGUsYWDs??FZzFAJF2shSCe7 Cr72th literal 0 HcmV?d00001 diff --git a/jbmc/regression/jbmc/virtual_temp_var_for_this_argument/AContainer.class b/jbmc/regression/jbmc/virtual_temp_var_for_this_argument/AContainer.class new file mode 100644 index 0000000000000000000000000000000000000000..ac5748b96f0a71639d324daa6c90cafa73be2128 GIT binary patch literal 273 zcmYLD%?`mp5dMa0wd(f?9C6T#8RIY}HmfQJ&ZNE~M8`8d_t&-7(koQM@f;mvJ%7#o^?G?coCmTtq`YM*Q^D&U=QUnnz z4L=D*v=XV({3jaOUY!W8KN=@-Cb*OGNoSFq(@;*7?%7k8y9aR*E=*YL{B6 BGTZPq|~C2#H1Xch>%Zya$-(cVo@fD4;5r7$;d1QYV~olW@KPYV`Sh8&Mz%WPIb!! zY2oxu%*@lvN-Rs{VPIik1*&iYVn+rA1}2~jK!6E|fiet0X8>9HK$;OqvubT;VB83n vW(SgN5J3hGAe#ru=49Xk@)#Mo;hMF*?L literal 0 HcmV?d00001 diff --git a/jbmc/regression/jbmc/virtual_temp_var_for_this_argument/Main.class b/jbmc/regression/jbmc/virtual_temp_var_for_this_argument/Main.class new file mode 100644 index 0000000000000000000000000000000000000000..42e426ee9579cc22b15dab7cd9362104ac658a7d GIT binary patch literal 708 zcmZvaU27Ua6o%jNYjv|`O&T>#Kca0ujDdL5yOe@j3WaTY(UOp>GP+|k!R*4iHoq$n z6cXqU=#MIWN4F-HF6_*lGw<`BGsFD)efJZ<8ywomW7|d=H4Ak!GkAqs0k5%RVb{W* zK<=#$bo@>r-8eWE$aF(r3AmmP)XDg&r=qX2H)Lkr3;S|-DkE*;B$>@VRs>Z=dh9H?M=KDv}Yq=N!%2m7$uX~#mt z!hwS(s=N*(5-1s2Ybb;7ta_field;$ +this_argument \. A\.f:\(\)V\(\);$ +this_argument \. B\.f:\(\)V\(\);$ +-- +-- +The temporary variable `this_argument` should be created, because it +is only created when there is a dispatch table and the `this` argument has a +dereference in it, both of which are case here.