From c56dbfdbe77ae655e43162f475505de6771a2315 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Tue, 5 Feb 2019 15:53:48 +0000 Subject: [PATCH] use new goto_programt::instructiont API This increases type safety when accessing or construcing instructions of goto programs. --- jbmc/src/java_bytecode/remove_exceptions.cpp | 4 +- src/assembler/remove_asm.cpp | 135 +++++++++--------- src/goto-analyzer/static_simplifier.cpp | 4 +- src/goto-analyzer/taint_analysis.cpp | 4 +- src/goto-instrument/accelerate/accelerate.cpp | 12 +- src/goto-instrument/count_eloc.cpp | 2 +- src/goto-programs/cfg.h | 6 +- src/goto-programs/goto_program.h | 6 +- src/goto-symex/symex_dead.cpp | 2 +- src/goto-symex/symex_decl.cpp | 4 +- src/goto-symex/symex_function_call.cpp | 2 +- src/goto-symex/symex_main.cpp | 5 +- src/goto-symex/symex_other.cpp | 2 +- .../goto_program_dereference.cpp | 20 +-- src/pointer-analysis/value_set_domain_fi.cpp | 3 +- 15 files changed, 107 insertions(+), 104 deletions(-) diff --git a/jbmc/src/java_bytecode/remove_exceptions.cpp b/jbmc/src/java_bytecode/remove_exceptions.cpp index 654b02dd988..94a0b873533 100644 --- a/jbmc/src/java_bytecode/remove_exceptions.cpp +++ b/jbmc/src/java_bytecode/remove_exceptions.cpp @@ -432,7 +432,7 @@ bool remove_exceptionst::instrument_function_call( goto_programt::targett next_it=instr_it; next_it++; - code_function_callt &function_call=to_code_function_call(instr_it->code); + code_function_callt &function_call = instr_it->get_function_call(); DATA_INVARIANT( function_call.function().id()==ID_symbol, "identified expected to be a symbol"); @@ -493,7 +493,7 @@ void remove_exceptionst::instrument_exceptions( { if(instr_it->is_decl()) { - code_declt decl=to_code_decl(instr_it->code); + code_declt decl = instr_it->get_decl(); locals.push_back(decl.symbol()); } // Is it a handler push/pop or catch landing-pad? diff --git a/src/assembler/remove_asm.cpp b/src/assembler/remove_asm.cpp index 22c6a6f604d..e98457eeddb 100644 --- a/src/assembler/remove_asm.cpp +++ b/src/assembler/remove_asm.cpp @@ -107,9 +107,8 @@ void remove_asmt::gcc_asm_function_call( code_function_callt function_call(std::move(fkt), std::move(arguments)); - goto_programt::targett call = dest.add_instruction(FUNCTION_CALL); - call->code = function_call; - call->source_location = code.source_location(); + dest.add( + goto_programt::make_function_call(function_call, code.source_location())); // do we have it? if(!symbol_table.has_symbol(function_identifier)) @@ -157,9 +156,8 @@ void remove_asmt::msc_asm_function_call( code_function_callt function_call(fkt); - goto_programt::targett call = dest.add_instruction(FUNCTION_CALL); - call->code = function_call; - call->source_location = code.source_location(); + dest.add( + goto_programt::make_function_call(function_call, code.source_location())); // do we have it? if(!symbol_table.has_symbol(function_identifier)) @@ -194,7 +192,7 @@ void remove_asmt::process_instruction( goto_programt::instructiont &instruction, goto_programt &dest) { - const code_asmt &code = to_code_asm(instruction.code); + const code_asmt &code = to_code_asm(instruction.get_other()); const irep_idt &flavor = code.get_flavor(); @@ -271,14 +269,15 @@ void remove_asmt::process_instruction_gcc( goto_programt::targett ab = tmp_dest.add_instruction(ATOMIC_BEGIN); ab->source_location = code.source_location(); - goto_programt::targett t = tmp_dest.add_instruction(OTHER); - t->source_location = code.source_location(); - t->code = codet(ID_fence); - t->code.add_source_location() = code.source_location(); - t->code.set(ID_WWfence, true); - t->code.set(ID_RRfence, true); - t->code.set(ID_RWfence, true); - t->code.set(ID_WRfence, true); + codet code_fence(ID_fence); + code_fence.add_source_location() = code.source_location(); + code_fence.set(ID_WWfence, true); + code_fence.set(ID_RRfence, true); + code_fence.set(ID_RWfence, true); + code_fence.set(ID_WRfence, true); + + tmp_dest.add( + goto_programt::make_other(code_fence, code.source_location())); } if(command == "fstcw" || command == "fnstcw" || command == "fldcw") // x86 @@ -292,62 +291,67 @@ void remove_asmt::process_instruction_gcc( } else if(command == ID_sync) // Power { - goto_programt::targett t = tmp_dest.add_instruction(OTHER); - t->source_location = code.source_location(); - t->code = codet(ID_fence); - t->code.add_source_location() = code.source_location(); - t->code.set(ID_WWfence, true); - t->code.set(ID_RRfence, true); - t->code.set(ID_RWfence, true); - t->code.set(ID_WRfence, true); - t->code.set(ID_WWcumul, true); - t->code.set(ID_RWcumul, true); - t->code.set(ID_RRcumul, true); - t->code.set(ID_WRcumul, true); + codet code_fence(ID_fence); + code_fence.add_source_location() = code.source_location(); + code_fence.set(ID_WWfence, true); + code_fence.set(ID_RRfence, true); + code_fence.set(ID_RWfence, true); + code_fence.set(ID_WRfence, true); + code_fence.set(ID_WWcumul, true); + code_fence.set(ID_RWcumul, true); + code_fence.set(ID_RRcumul, true); + code_fence.set(ID_WRcumul, true); + + tmp_dest.add( + goto_programt::make_other(code_fence, code.source_location())); } else if(command == ID_lwsync) // Power { - goto_programt::targett t = tmp_dest.add_instruction(OTHER); - t->source_location = code.source_location(); - t->code = codet(ID_fence); - t->code.add_source_location() = code.source_location(); - t->code.set(ID_WWfence, true); - t->code.set(ID_RRfence, true); - t->code.set(ID_RWfence, true); - t->code.set(ID_WWcumul, true); - t->code.set(ID_RWcumul, true); - t->code.set(ID_RRcumul, true); + codet code_fence(ID_fence); + code_fence.add_source_location() = code.source_location(); + code_fence.set(ID_WWfence, true); + code_fence.set(ID_RRfence, true); + code_fence.set(ID_RWfence, true); + code_fence.set(ID_WWcumul, true); + code_fence.set(ID_RWcumul, true); + code_fence.set(ID_RRcumul, true); + + tmp_dest.add( + goto_programt::make_other(code_fence, code.source_location())); } else if(command == ID_isync) // Power { - goto_programt::targett t = tmp_dest.add_instruction(OTHER); - t->source_location = code.source_location(); - t->code = codet(ID_fence); - t->code.add_source_location() = code.source_location(); + codet code_fence(ID_fence); + code_fence.add_source_location() = code.source_location(); + + tmp_dest.add( + goto_programt::make_other(code_fence, code.source_location())); // doesn't do anything by itself, // needs to be combined with branch } else if(command == "dmb" || command == "dsb") // ARM { - goto_programt::targett t = tmp_dest.add_instruction(OTHER); - t->source_location = code.source_location(); - t->code = codet(ID_fence); - t->code.add_source_location() = code.source_location(); - t->code.set(ID_WWfence, true); - t->code.set(ID_RRfence, true); - t->code.set(ID_RWfence, true); - t->code.set(ID_WRfence, true); - t->code.set(ID_WWcumul, true); - t->code.set(ID_RWcumul, true); - t->code.set(ID_RRcumul, true); - t->code.set(ID_WRcumul, true); + codet code_fence(ID_fence); + code_fence.add_source_location() = code.source_location(); + code_fence.set(ID_WWfence, true); + code_fence.set(ID_RRfence, true); + code_fence.set(ID_RWfence, true); + code_fence.set(ID_WRfence, true); + code_fence.set(ID_WWcumul, true); + code_fence.set(ID_RWcumul, true); + code_fence.set(ID_RRcumul, true); + code_fence.set(ID_WRcumul, true); + + tmp_dest.add( + goto_programt::make_other(code_fence, code.source_location())); } else if(command == "isb") // ARM { - goto_programt::targett t = tmp_dest.add_instruction(OTHER); - t->source_location = code.source_location(); - t->code = codet(ID_fence); - t->code.add_source_location() = code.source_location(); + codet code_fence(ID_fence); + code_fence.add_source_location() = code.source_location(); + + tmp_dest.add( + goto_programt::make_other(code_fence, code.source_location())); // doesn't do anything by itself, // needs to be combined with branch } @@ -436,14 +440,15 @@ void remove_asmt::process_instruction_msc( goto_programt::targett ab = tmp_dest.add_instruction(ATOMIC_BEGIN); ab->source_location = code.source_location(); - goto_programt::targett t = tmp_dest.add_instruction(OTHER); - t->source_location = code.source_location(); - t->code = codet(ID_fence); - t->code.add_source_location() = code.source_location(); - t->code.set(ID_WWfence, true); - t->code.set(ID_RRfence, true); - t->code.set(ID_RWfence, true); - t->code.set(ID_WRfence, true); + codet code_fence(ID_fence); + code_fence.add_source_location() = code.source_location(); + code_fence.set(ID_WWfence, true); + code_fence.set(ID_RRfence, true); + code_fence.set(ID_RWfence, true); + code_fence.set(ID_WRfence, true); + + tmp_dest.add( + goto_programt::make_other(code_fence, code.source_location())); } if(command == "fstcw" || command == "fnstcw" || command == "fldcw") // x86 diff --git a/src/goto-analyzer/static_simplifier.cpp b/src/goto-analyzer/static_simplifier.cpp index 8bc555d88e6..7ff249b5639 100644 --- a/src/goto-analyzer/static_simplifier.cpp +++ b/src/goto-analyzer/static_simplifier.cpp @@ -95,7 +95,7 @@ bool static_simplifier( } else if(i_it->is_assign()) { - code_assignt &assign=to_code_assign(i_it->code); + code_assignt &assign = i_it->get_assign(); // Simplification needs to be aware of which side of the // expression it is handling as: @@ -115,7 +115,7 @@ bool static_simplifier( } else if(i_it->is_function_call()) { - code_function_callt &fcall=to_code_function_call(i_it->code); + code_function_callt &fcall = i_it->get_function_call(); bool unchanged = ai.abstract_state_before(i_it)->ai_simplify(fcall.function(), ns); diff --git a/src/goto-analyzer/taint_analysis.cpp b/src/goto-analyzer/taint_analysis.cpp index d65f562c86c..06229c2a189 100644 --- a/src/goto-analyzer/taint_analysis.cpp +++ b/src/goto-analyzer/taint_analysis.cpp @@ -73,8 +73,8 @@ void taint_analysist::instrument( { case FUNCTION_CALL: { - const code_function_callt &function_call= - to_code_function_call(instruction.code); + const code_function_callt &function_call = + instruction.get_function_call(); const exprt &function=function_call.function(); if(function.id()==ID_symbol) diff --git a/src/goto-instrument/accelerate/accelerate.cpp b/src/goto-instrument/accelerate/accelerate.cpp index 62948970db2..222ac3f26a6 100644 --- a/src/goto-instrument/accelerate/accelerate.cpp +++ b/src/goto-instrument/accelerate/accelerate.cpp @@ -257,8 +257,8 @@ void acceleratet::make_overflow_loc( } goto_programt::targett t=program.insert_after(loop_header); - t->make_assignment(); - t->code=code_assignt(overflow_var, false_exprt()); + *t = + goto_programt::make_assignment(code_assignt(overflow_var, false_exprt())); t->swap(*loop_header); loop.insert(t); overflow_locs[loop_header].push_back(t); @@ -360,8 +360,8 @@ void acceleratet::add_dirty_checks() it!=dirty_vars_map.end(); ++it) { - goto_programt::instructiont assign(ASSIGN); - assign.code=code_assignt(it->second, false_exprt()); + goto_programt::instructiont assign = + goto_programt::make_assignment(code_assignt(it->second, false_exprt())); program.insert_before_swap(program.instructions.begin(), assign); } @@ -384,8 +384,8 @@ void acceleratet::add_dirty_checks() if(dirty_var!=dirty_vars_map.end()) { - goto_programt::instructiont clear_flag(ASSIGN); - clear_flag.code=code_assignt(dirty_var->second, false_exprt()); + goto_programt::instructiont clear_flag = goto_programt::make_assignment( + code_assignt(dirty_var->second, false_exprt())); program.insert_before_swap(it, clear_flag); } } diff --git a/src/goto-instrument/count_eloc.cpp b/src/goto-instrument/count_eloc.cpp index f7626e0e15e..33bb6519585 100644 --- a/src/goto-instrument/count_eloc.cpp +++ b/src/goto-instrument/count_eloc.cpp @@ -164,7 +164,7 @@ void print_global_state_size(const goto_modelt &goto_model) { if(ins.is_assign()) { - const code_assignt &code_assign = to_code_assign(ins.code); + const code_assignt &code_assign = ins.get_assign(); object_descriptor_exprt ode; ode.build(code_assign.lhs(), ns); diff --git a/src/goto-programs/cfg.h b/src/goto-programs/cfg.h index db4a75c8939..2b0fc80d0fc 100644 --- a/src/goto-programs/cfg.h +++ b/src/goto-programs/cfg.h @@ -288,8 +288,7 @@ void cfg_baset::compute_edges_function_call( goto_programt::const_targett next_PC, entryt &entry) { - const exprt &function= - to_code_function_call(instruction.code).function(); + const exprt &function = instruction.get_function_call().function(); if(function.id()!=ID_symbol) return; @@ -339,8 +338,7 @@ void procedure_local_cfg_baset::compute_edges_function_call( goto_programt::const_targett next_PC, typename cfg_baset::entryt &entry) { - const exprt &function= - to_code_function_call(instruction.code).function(); + const exprt &function = instruction.get_function_call().function(); if(function.id()!=ID_symbol) return; diff --git a/src/goto-programs/goto_program.h b/src/goto-programs/goto_program.h index 2733b39ad8d..c36e7a5a50b 100644 --- a/src/goto-programs/goto_program.h +++ b/src/goto-programs/goto_program.h @@ -826,9 +826,11 @@ class goto_programt static_cast(get_nil_irep()), l, ASSUME, g, {}); } - static instructiont make_other(const codet &_code) + static instructiont make_other( + const codet &_code, + const source_locationt &l = source_locationt::nil()) { - return instructiont(_code, source_locationt::nil(), OTHER, nil_exprt(), {}); + return instructiont(_code, l, OTHER, nil_exprt(), {}); } static instructiont make_decl( diff --git a/src/goto-symex/symex_dead.cpp b/src/goto-symex/symex_dead.cpp index b6350245753..d72933a2e78 100644 --- a/src/goto-symex/symex_dead.cpp +++ b/src/goto-symex/symex_dead.cpp @@ -21,7 +21,7 @@ void goto_symext::symex_dead(statet &state) { const goto_programt::instructiont &instruction=*state.source.pc; - const code_deadt &code = to_code_dead(instruction.code); + const code_deadt &code = instruction.get_dead(); // We increase the L2 renaming to make these non-deterministic. // We also prevent propagation of old values. diff --git a/src/goto-symex/symex_decl.cpp b/src/goto-symex/symex_decl.cpp index 028e547b763..529c7aceb9e 100644 --- a/src/goto-symex/symex_decl.cpp +++ b/src/goto-symex/symex_decl.cpp @@ -23,13 +23,13 @@ void goto_symext::symex_decl(statet &state) { const goto_programt::instructiont &instruction=*state.source.pc; - const codet &code = instruction.code; + const auto &code = instruction.get_decl(); // two-operand decl not supported here // we handle the decl with only one operand PRECONDITION(code.operands().size() == 1); - symex_decl(state, to_code_decl(code).symbol()); + symex_decl(state, code.symbol()); } void goto_symext::symex_decl(statet &state, const symbol_exprt &expr) diff --git a/src/goto-symex/symex_function_call.cpp b/src/goto-symex/symex_function_call.cpp index 21124d39c59..2889fc1e039 100644 --- a/src/goto-symex/symex_function_call.cpp +++ b/src/goto-symex/symex_function_call.cpp @@ -447,7 +447,7 @@ void goto_symext::return_assignment(statet &state) const goto_programt::instructiont &instruction=*state.source.pc; PRECONDITION(instruction.is_return()); - const code_returnt &code=to_code_return(instruction.code); + const code_returnt &code = instruction.get_return(); target.location(state.guard.as_expr(), state.source); diff --git a/src/goto-symex/symex_main.cpp b/src/goto-symex/symex_main.cpp index ab8ea636581..58164a9aa27 100644 --- a/src/goto-symex/symex_main.cpp +++ b/src/goto-symex/symex_main.cpp @@ -440,7 +440,7 @@ void goto_symext::symex_step( case ASSIGN: if(!state.guard.is_false()) - symex_assign(state, to_code_assign(instruction.code)); + symex_assign(state, instruction.get_assign()); symex_transition(state); break; @@ -448,8 +448,7 @@ void goto_symext::symex_step( case FUNCTION_CALL: if(!state.guard.is_false()) { - code_function_callt deref_code= - to_code_function_call(instruction.code); + code_function_callt deref_code = instruction.get_function_call(); if(deref_code.lhs().is_not_nil()) clean_expr(deref_code.lhs(), state, true); diff --git a/src/goto-symex/symex_other.cpp b/src/goto-symex/symex_other.cpp index 4ed1c3eaa7f..ad5fb0ff0c6 100644 --- a/src/goto-symex/symex_other.cpp +++ b/src/goto-symex/symex_other.cpp @@ -79,7 +79,7 @@ void goto_symext::symex_other( { const goto_programt::instructiont &instruction=*state.source.pc; - const codet &code = instruction.code; + const codet &code = instruction.get_other(); const irep_idt &statement=code.get_statement(); diff --git a/src/pointer-analysis/goto_program_dereference.cpp b/src/pointer-analysis/goto_program_dereference.cpp index a029883ffe7..3b786cb2a0f 100644 --- a/src/pointer-analysis/goto_program_dereference.cpp +++ b/src/pointer-analysis/goto_program_dereference.cpp @@ -305,17 +305,16 @@ void goto_program_dereferencet::dereference_instruction( if(i.is_assign()) { - if(i.code.operands().size()!=2) - throw "assignment expects two operands"; + auto &assignment = i.get_assign(); dereference_expr( - i.code.op0(), checks_only, value_set_dereferencet::modet::WRITE); + assignment.lhs(), checks_only, value_set_dereferencet::modet::WRITE); dereference_expr( - i.code.op1(), checks_only, value_set_dereferencet::modet::READ); + assignment.rhs(), checks_only, value_set_dereferencet::modet::READ); } else if(i.is_function_call()) { - code_function_callt &function_call = to_code_function_call(i.code); + code_function_callt &function_call = i.get_function_call(); if(function_call.lhs().is_not_nil()) dereference_expr( @@ -332,24 +331,25 @@ void goto_program_dereferencet::dereference_instruction( } else if(i.is_return()) { - Forall_operands(it, i.code) + Forall_operands(it, i.get_return()) dereference_expr(*it, checks_only, value_set_dereferencet::modet::READ); } else if(i.is_other()) { - const irep_idt &statement = i.get_other().get_statement(); + auto &code = i.get_other(); + const irep_idt &statement = code.get_statement(); if(statement==ID_expression) { - if(i.code.operands().size()!=1) + if(code.operands().size() != 1) throw "expression expects one operand"; dereference_expr( - i.code.op0(), checks_only, value_set_dereferencet::modet::READ); + code.op0(), checks_only, value_set_dereferencet::modet::READ); } else if(statement==ID_printf) { - for(auto &op : i.get_other().operands()) + for(auto &op : code.operands()) dereference_expr(op, checks_only, value_set_dereferencet::modet::READ); } } diff --git a/src/pointer-analysis/value_set_domain_fi.cpp b/src/pointer-analysis/value_set_domain_fi.cpp index 12702e046a1..f22acab380f 100644 --- a/src/pointer-analysis/value_set_domain_fi.cpp +++ b/src/pointer-analysis/value_set_domain_fi.cpp @@ -48,8 +48,7 @@ bool value_set_domain_fit::transform( case FUNCTION_CALL: { - const code_function_callt &code= - to_code_function_call(from_l->code); + const code_function_callt &code = from_l->get_function_call(); value_set.do_function_call(function_to, code.arguments(), ns); }