forked from diffblue/cbmc
-
Notifications
You must be signed in to change notification settings - Fork 0
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Make convert_java_nondet more general
- Loading branch information
Owen
committed
Jul 13, 2018
1 parent
3c2e55e
commit 6d9e805
Showing
2 changed files
with
192 additions
and
71 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
|
|
@@ -22,90 +22,141 @@ Author: Reuben Thomas, [email protected] | |
|
|
||
| #include "java_object_factory.h" // gen_nondet_init | ||
|
|
||
| /// Returns true if `expr` is a nondet pointer that isn't a function pointer or | ||
| /// a void* pointer as these can be meaningfully non-det initalized. | ||
| static bool is_nondet_pointer(exprt expr) | ||
| { | ||
| // If the expression type doesn't have a subtype then I guess it's primitive | ||
| // and we do not want to convert it. If the type is a ptr-to-void or a | ||
| // function pointer then we also do not want to convert it. | ||
| const typet &type = expr.type(); | ||
| const bool non_void_non_function_pointer = type.id() == ID_pointer && | ||
| type.subtype().id() != ID_empty && | ||
| type.subtype().id() != ID_code; | ||
| return can_cast_expr<side_effect_expr_nondett>(expr) && | ||
| non_void_non_function_pointer; | ||
| } | ||
|
|
||
| /// Populate `instructions` with goto instructions to nondet init | ||
| /// `aux_symbol_expr` | ||
| static goto_programt get_gen_nondet_init_instructions( | ||
| const symbol_exprt &aux_symbol_expr, | ||
| const source_locationt &source_loc, | ||
| symbol_table_baset &symbol_table, | ||
| message_handlert &message_handler, | ||
| const object_factory_parameterst &object_factory_parameters, | ||
| const irep_idt &mode) | ||
| { | ||
| code_blockt gen_nondet_init_code; | ||
| const bool skip_classid = true; | ||
| gen_nondet_init( | ||
| aux_symbol_expr, | ||
| gen_nondet_init_code, | ||
| symbol_table, | ||
| source_loc, | ||
| skip_classid, | ||
| allocation_typet::DYNAMIC, | ||
| object_factory_parameters, | ||
| update_in_placet::NO_UPDATE_IN_PLACE); | ||
|
|
||
| goto_programt instructions; | ||
| goto_convert( | ||
| gen_nondet_init_code, symbol_table, instructions, message_handler, mode); | ||
| return instructions; | ||
| } | ||
|
|
||
| /// Checks an instruction to see whether it contains an assignment from | ||
| /// side_effect_expr_nondet. If so, replaces the instruction with a range of | ||
| /// instructions to properly nondet-initialize the lhs. | ||
| /// \param goto_program: The goto program to modify. | ||
| /// \param target: One of the steps in that goto program. | ||
| /// \param symbol_table: The global symbol table. | ||
| /// \param message_handler: Handles logging. | ||
| /// \param max_nondet_array_length: Maximum size of new nondet arrays. | ||
| /// \return The next instruction to process with this function. | ||
| static goto_programt::targett insert_nondet_init_code( | ||
| /// \param object_factory_parameters: Parameters for the generation of nondet | ||
| /// objects. | ||
| /// \param mode: Language mode | ||
| /// \return The next instruction to process with this function and a boolean | ||
| /// indicating whether any changes were made to the goto program. | ||
| static std::pair<goto_programt::targett, bool> insert_nondet_init_code( | ||
| goto_programt &goto_program, | ||
| const goto_programt::targett &target, | ||
| symbol_table_baset &symbol_table, | ||
| message_handlert &message_handler, | ||
| object_factory_parameterst object_factory_parameters, | ||
| const irep_idt &mode) | ||
| { | ||
| // Return if the instruction isn't an assignment | ||
| const auto next_instr=std::next(target); | ||
| if(!target->is_assign()) | ||
| { | ||
| return next_instr; | ||
| } | ||
| const auto next_instr = std::next(target); | ||
|
|
||
| // Return if the rhs of the assignment isn't a side effect expression | ||
| const auto &assign=to_code_assign(target->code); | ||
| if(assign.rhs().id()!=ID_side_effect) | ||
| // We only expect to find nondets in the rhs of an assignments, and in return | ||
| // statements if remove_returns has not been run, but we do a more general | ||
| // check on all operands in case this changes | ||
| for(exprt &op : target->code.operands()) | ||
| { | ||
| return next_instr; | ||
| } | ||
| if(!is_nondet_pointer(op)) | ||
| { | ||
| continue; | ||
| } | ||
|
|
||
| // Return if the rhs isn't nondet | ||
| const auto &side_effect=to_side_effect_expr(assign.rhs()); | ||
| if(side_effect.get_statement()!=ID_nondet) | ||
| { | ||
| return next_instr; | ||
| } | ||
| const auto &nondet_expr = to_side_effect_expr_nondet(op); | ||
|
|
||
| const auto lhs=assign.lhs(); | ||
| // If the lhs type doesn't have a subtype then I guess it's primitive and | ||
| // we want to bail out now | ||
| if(!lhs.type().has_subtype()) | ||
| { | ||
| return next_instr; | ||
| } | ||
| if(!nondet_expr.get_nullable()) | ||
| object_factory_parameters.max_nonnull_tree_depth = 1; | ||
|
|
||
| // Although, if the type is a ptr-to-void then we also want to bail | ||
| if(lhs.type().subtype().id()==ID_empty || | ||
| lhs.type().subtype().id()==ID_code) | ||
| { | ||
| return next_instr; | ||
| } | ||
| const source_locationt &source_loc = target->source_location; | ||
|
|
||
| // Check whether the nondet object may be null | ||
| if(!to_side_effect_expr_nondet(side_effect).get_nullable()) | ||
| object_factory_parameters.max_nonnull_tree_depth = 1; | ||
| // Get the symbol to nondet-init | ||
| const auto source_loc=target->source_location; | ||
| // Currently the code looks like this | ||
| // target: instruction containing op | ||
| // When we are done it will look like this | ||
| // target : declare aux_symbol | ||
| // . <gen_nondet_init_instructions - many lines> | ||
| // . <gen_nondet_init_instructions - many lines> | ||
| // . <gen_nondet_init_instructions - many lines> | ||
| // target2: instruction containing op, with op replaced by aux_symbol | ||
| // dead aux_symbol | ||
|
|
||
| // Erase the nondet assignment | ||
| target->make_skip(); | ||
| symbolt &aux_symbol = get_fresh_aux_symbol( | ||
| op.type(), | ||
| id2string(goto_programt::get_function_id(goto_program)), | ||
| "nondet_tmp", | ||
| source_loc, | ||
| ID_java, | ||
| symbol_table); | ||
|
|
||
| // Generate nondet init code | ||
| code_blockt init_code; | ||
| gen_nondet_init( | ||
| lhs, | ||
| init_code, | ||
| symbol_table, | ||
| source_loc, | ||
| true, | ||
| allocation_typet::DYNAMIC, | ||
| object_factory_parameters, | ||
| update_in_placet::NO_UPDATE_IN_PLACE); | ||
| const symbol_exprt aux_symbol_expr = aux_symbol.symbol_expr(); | ||
| op = aux_symbol_expr; | ||
|
|
||
| // Convert this code into goto instructions | ||
| goto_programt new_instructions; | ||
| goto_convert( | ||
| init_code, symbol_table, new_instructions, message_handler, mode); | ||
| // Insert an instruction declaring `aux_symbol` before `target`, being | ||
| // careful to preserve jumps to `target` | ||
| goto_programt::instructiont decl_aux_symbol; | ||
| decl_aux_symbol.make_decl(code_declt(aux_symbol_expr)); | ||
| decl_aux_symbol.source_location = source_loc; | ||
| goto_program.insert_before_swap(target, decl_aux_symbol); | ||
|
|
||
| // Insert the new instructions into the instruction list | ||
| goto_program.destructive_insert(next_instr, new_instructions); | ||
| goto_program.update(); | ||
| // Keep track of the new location of the instruction containing op. | ||
| const goto_programt::targett target2 = std::next(target); | ||
|
|
||
| return next_instr; | ||
| goto_programt gen_nondet_init_instructions = | ||
| get_gen_nondet_init_instructions( | ||
| aux_symbol_expr, | ||
| source_loc, | ||
| symbol_table, | ||
| message_handler, | ||
| object_factory_parameters, | ||
| mode); | ||
| goto_program.destructive_insert(target2, gen_nondet_init_instructions); | ||
|
|
||
| goto_programt::targett dead_aux_symbol = goto_program.insert_after(target2); | ||
| dead_aux_symbol->make_dead(); | ||
| dead_aux_symbol->code = code_deadt(aux_symbol_expr); | ||
| dead_aux_symbol->source_location = source_loc; | ||
|
|
||
| // In theory target could have more than one operand which should be | ||
| // replaced by convert_nondet, so we return target2 so that it | ||
| // will be checked again | ||
| return std::make_pair(target2, true); | ||
| } | ||
|
|
||
| return std::make_pair(next_instr, false); | ||
| } | ||
|
|
||
| /// For each instruction in the goto program, checks if it is an assignment from | ||
|
|
@@ -114,25 +165,35 @@ static goto_programt::targett insert_nondet_init_code( | |
| /// \param goto_program: The goto program to modify. | ||
| /// \param symbol_table: The global symbol table. | ||
| /// \param message_handler: Handles logging. | ||
| /// \param max_nondet_array_length: Maximum size of new nondet arrays. | ||
| /// \param object_factory_parameters: Parameters for the generation of nondet | ||
| /// objects. | ||
| /// \param mode: Language mode | ||
| void convert_nondet( | ||
| goto_programt &goto_program, | ||
| symbol_table_baset &symbol_table, | ||
| message_handlert &message_handler, | ||
| const object_factory_parameterst &object_factory_parameters, | ||
| const irep_idt &mode) | ||
| { | ||
| for(auto instruction_iterator=goto_program.instructions.begin(), | ||
| end=goto_program.instructions.end(); | ||
| instruction_iterator!=end;) | ||
| bool changed = false; | ||
| auto instruction_iterator = goto_program.instructions.begin(); | ||
|
|
||
| while(instruction_iterator != goto_program.instructions.end()) | ||
| { | ||
| instruction_iterator = insert_nondet_init_code( | ||
| auto ret = insert_nondet_init_code( | ||
| goto_program, | ||
| instruction_iterator, | ||
| symbol_table, | ||
| message_handler, | ||
| object_factory_parameters, | ||
| mode); | ||
| instruction_iterator = ret.first; | ||
| changed |= ret.second; | ||
| } | ||
|
|
||
| if(changed) | ||
| { | ||
| goto_program.update(); | ||
| } | ||
| } | ||
|
|
||
|
|
||
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters