Skip to content

Remove 'erase' in replace_java_nondet.cpp, fixes #850 #860

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 3 commits into from
Apr 27, 2017
Merged

Remove 'erase' in replace_java_nondet.cpp, fixes #850 #860

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
c195e63
Remove 'erase' in replace_java_nondet.cpp
reuk Apr 24, 2017
6deaa3b
Remove skip in replace_java_nondet.cpp
reuk Apr 27, 2017
d15d842
Fix indentation in convert_nondet
reuk Apr 27, 2017
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
19 changes: 11 additions & 8 deletions src/goto-programs/convert_nondet.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -9,6 +9,7 @@ Author: Reuben Thomas, [email protected]
#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

Expand All @@ -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)
Expand Down Expand Up @@ -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;
Expand All @@ -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;
}

/*******************************************************************\
Expand All @@ -129,9 +130,9 @@ 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();
instruction_iterator!=end;)
for(auto instruction_iterator=goto_program.instructions.begin(),
end=goto_program.instructions.end();
instruction_iterator!=end;)
{
instruction_iterator=insert_nondet_init_code(
goto_program,
Expand Down Expand Up @@ -160,4 +161,6 @@ void convert_nondet(
}

goto_functions.compute_location_numbers();

remove_skip(goto_functions);
}
27 changes: 18 additions & 9 deletions src/goto-programs/replace_java_nondet.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -9,6 +9,7 @@ Author: Reuben Thomas, [email protected]
#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"

Expand Down Expand Up @@ -215,9 +216,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);
Expand All @@ -241,7 +242,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(
Expand All @@ -263,10 +264,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(
Expand All @@ -278,7 +284,7 @@ static goto_programt::const_targett check_and_replace_target(

goto_program.update();

return after_erased;
return after_matching_assignment;
}

/*******************************************************************\
Expand All @@ -297,8 +303,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(
Expand All @@ -315,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);
}