From c195e63c34dcc4cadb4c92fa19cee842b6a82060 Mon Sep 17 00:00:00 2001 From: reuk Date: Mon, 24 Apr 2017 11:40:33 +0100 Subject: [PATCH 1/3] Remove 'erase' in replace_java_nondet.cpp Erasing a range of instructions from a goto program can cause memory bugs when `goto_program::update` is called. Specifically, if any of the remaining nodes in the program have elements of `targets` which point into the erased range, then the program may attempt an invalid read during the `update` call. To avoid this, I thought of two options: - check through the goto-program for instructions with `target`s that point into the removed range, and remove those `target`s, or - just replace the existing instructions with no-ops. Although I think the first solution is better, I can't think of a good way of doing it with acceptable complexity, so this patch implements the second option. --- src/goto-programs/replace_java_nondet.cpp | 23 ++++++++++++++--------- 1 file changed, 14 insertions(+), 9 deletions(-) diff --git a/src/goto-programs/replace_java_nondet.cpp b/src/goto-programs/replace_java_nondet.cpp index b78a0819cac..1faddf24491 100644 --- a/src/goto-programs/replace_java_nondet.cpp +++ b/src/goto-programs/replace_java_nondet.cpp @@ -215,9 +215,9 @@ Function: check_and_replace_target \*******************************************************************/ -static goto_programt::const_targett check_and_replace_target( +static goto_programt::targett check_and_replace_target( goto_programt &goto_program, - const goto_programt::const_targett &target) + const goto_programt::targett &target) { // Check whether this is a nondet library method, and return if not const auto instr_info=get_nondet_instruction_info(target); @@ -241,7 +241,7 @@ static goto_programt::const_targett check_and_replace_target( to_symbol_expr(next_instr_assign_lhs).get_identifier(); auto &instructions=goto_program.instructions; - const auto end=instructions.cend(); + const auto end=instructions.end(); // Look for an instruction where this name is on the RHS of an assignment const auto matching_assignment=std::find_if( @@ -263,10 +263,15 @@ static goto_programt::const_targett check_and_replace_target( const auto after_matching_assignment=std::next(matching_assignment); assert(after_matching_assignment!=end); - const auto after_erased=goto_program.instructions.erase( - target, after_matching_assignment); + std::for_each( + target, + after_matching_assignment, + [](goto_programt::instructiont &instr) + { + instr.make_skip(); + }); - const auto inserted=goto_program.insert_before(after_erased); + const auto inserted=goto_program.insert_before(after_matching_assignment); inserted->make_assignment(); side_effect_expr_nondett inserted_expr(nondet_var.type()); inserted_expr.set_nullable( @@ -278,7 +283,7 @@ static goto_programt::const_targett check_and_replace_target( goto_program.update(); - return after_erased; + return after_matching_assignment; } /*******************************************************************\ @@ -297,8 +302,8 @@ Function: replace_java_nondet static void replace_java_nondet(goto_programt &goto_program) { - for(auto instruction_iterator=goto_program.instructions.cbegin(), - end=goto_program.instructions.cend(); + for(auto instruction_iterator=goto_program.instructions.begin(), + end=goto_program.instructions.end(); instruction_iterator!=end;) { instruction_iterator=check_and_replace_target( From 6deaa3b899df6f64088bcc789c5fdb19ece07b01 Mon Sep 17 00:00:00 2001 From: reuk Date: Thu, 27 Apr 2017 10:27:37 +0100 Subject: [PATCH 2/3] Remove skip in replace_java_nondet.cpp The changes in replace_java_nondet uncovered a similar 'erase' issue in convert_nondet, which this patch also fixes. --- src/goto-programs/convert_nondet.cpp | 17 ++++++++++------- src/goto-programs/replace_java_nondet.cpp | 4 ++++ 2 files changed, 14 insertions(+), 7 deletions(-) diff --git a/src/goto-programs/convert_nondet.cpp b/src/goto-programs/convert_nondet.cpp index 9e54d70d893..55c52fe8f4b 100644 --- a/src/goto-programs/convert_nondet.cpp +++ b/src/goto-programs/convert_nondet.cpp @@ -9,6 +9,7 @@ Author: Reuben Thomas, reuben.thomas@diffblue.com #include "goto-programs/convert_nondet.h" #include "goto-programs/goto_convert.h" #include "goto-programs/goto_model.h" +#include "goto-programs/remove_skip.h" #include "java_bytecode/java_object_factory.h" // gen_nondet_init @@ -34,9 +35,9 @@ Function: insert_nondet_init_code \*******************************************************************/ -static goto_programt::const_targett insert_nondet_init_code( +static goto_programt::targett insert_nondet_init_code( goto_programt &goto_program, - const goto_programt::const_targett &target, + const goto_programt::targett &target, symbol_tablet &symbol_table, message_handlert &message_handler, size_t max_nondet_array_length) @@ -82,7 +83,7 @@ static goto_programt::const_targett insert_nondet_init_code( const auto source_loc=target->source_location; // Erase the nondet assignment - const auto after_erased=goto_program.instructions.erase(target); + target->make_skip(); // Generate nondet init code code_blockt init_code; @@ -101,10 +102,10 @@ static goto_programt::const_targett insert_nondet_init_code( goto_convert(init_code, symbol_table, new_instructions, message_handler); // Insert the new instructions into the instruction list - goto_program.destructive_insert(after_erased, new_instructions); + goto_program.destructive_insert(next_instr, new_instructions); goto_program.update(); - return after_erased; + return next_instr; } /*******************************************************************\ @@ -129,8 +130,8 @@ static void convert_nondet( message_handlert &message_handler, size_t max_nondet_array_length) { - for(auto instruction_iterator=goto_program.instructions.cbegin(), - end=goto_program.instructions.cend(); + for(auto instruction_iterator=goto_program.instructions.begin(), + end=goto_program.instructions.end(); instruction_iterator!=end;) { instruction_iterator=insert_nondet_init_code( @@ -160,4 +161,6 @@ void convert_nondet( } goto_functions.compute_location_numbers(); + + remove_skip(goto_functions); } diff --git a/src/goto-programs/replace_java_nondet.cpp b/src/goto-programs/replace_java_nondet.cpp index 1faddf24491..b0514d60a7b 100644 --- a/src/goto-programs/replace_java_nondet.cpp +++ b/src/goto-programs/replace_java_nondet.cpp @@ -9,6 +9,7 @@ Author: Reuben Thomas, reuben.thomas@diffblue.com #include "goto-programs/replace_java_nondet.h" #include "goto-programs/goto_convert.h" #include "goto-programs/goto_model.h" +#include "goto-programs/remove_skip.h" #include "util/irep_ids.h" @@ -320,5 +321,8 @@ void replace_java_nondet(goto_functionst &goto_functions) { replace_java_nondet(goto_program.second.body); } + goto_functions.compute_location_numbers(); + + remove_skip(goto_functions); } From d15d84238d4977bcad5995713acda18a90ba5113 Mon Sep 17 00:00:00 2001 From: reuk Date: Thu, 27 Apr 2017 10:39:23 +0100 Subject: [PATCH 3/3] Fix indentation in convert_nondet --- src/goto-programs/convert_nondet.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/goto-programs/convert_nondet.cpp b/src/goto-programs/convert_nondet.cpp index 55c52fe8f4b..e4655716d9b 100644 --- a/src/goto-programs/convert_nondet.cpp +++ b/src/goto-programs/convert_nondet.cpp @@ -132,7 +132,7 @@ static void convert_nondet( { for(auto instruction_iterator=goto_program.instructions.begin(), end=goto_program.instructions.end(); - instruction_iterator!=end;) + instruction_iterator!=end;) { instruction_iterator=insert_nondet_init_code( goto_program,