diff --git a/src/goto-programs/mm_io.cpp b/src/goto-programs/mm_io.cpp index 2346ff40cbe..6590fc7e4b7 100644 --- a/src/goto-programs/mm_io.cpp +++ b/src/goto-programs/mm_io.cpp @@ -23,14 +23,14 @@ Date: April 2017 #include -void collect_deref_expr( - const exprt &src, - std::set &dest) +static std::set collect_deref_expr(const exprt &src) { - src.visit_pre([&dest](const exprt &e) { + std::set collected; + src.visit_pre([&collected](const exprt &e) { if(e.id() == ID_dereference) - dest.insert(to_dereference_expr(e)); + collected.insert(to_dereference_expr(e)); }); + return collected; } void mm_io( @@ -40,69 +40,66 @@ void mm_io( goto_functionst::goto_functiont &goto_function, const namespacet &ns) { - for(goto_programt::instructionst::iterator it= - goto_function.body.instructions.begin(); - it!=goto_function.body.instructions.end(); + for(auto it = goto_function.body.instructions.begin(); + it != goto_function.body.instructions.end(); it++) { - std::set deref_expr_w, deref_expr_r; + if(!it->is_assign()) + continue; - if(it->is_assign()) - { - auto &a_lhs = it->assign_lhs(); - auto &a_rhs = it->assign_rhs_nonconst(); - collect_deref_expr(a_rhs, deref_expr_r); + auto &a_lhs = it->assign_lhs(); + auto &a_rhs = it->assign_rhs_nonconst(); + const auto deref_expr_r = collect_deref_expr(a_rhs); - if(mm_io_r.is_not_nil()) + if(mm_io_r.is_not_nil()) + { + if(deref_expr_r.size() == 1) { - if(deref_expr_r.size()==1) - { - const dereference_exprt &d=*deref_expr_r.begin(); - source_locationt source_location = it->source_location(); - const code_typet &ct=to_code_type(mm_io_r.type()); - - if_exprt if_expr( - integer_address(d.pointer()), - typecast_exprt::conditional_cast(mm_io_r_value, d.type()), - d); - replace_expr(d, if_expr, a_rhs); - - const typet &pt=ct.parameters()[0].type(); - const typet &st=ct.parameters()[1].type(); - auto size_opt = size_of_expr(d.type(), ns); - CHECK_RETURN(size_opt.has_value()); - auto call = goto_programt::make_function_call( - mm_io_r_value, - mm_io_r, - {typecast_exprt(d.pointer(), pt), - typecast_exprt(size_opt.value(), st)}, - source_location); - goto_function.body.insert_before_swap(it, call); - it++; - } + const dereference_exprt &d = *deref_expr_r.begin(); + source_locationt source_location = it->source_location(); + const code_typet &ct = to_code_type(mm_io_r.type()); + + if_exprt if_expr( + integer_address(d.pointer()), + typecast_exprt::conditional_cast(mm_io_r_value, d.type()), + d); + replace_expr(d, if_expr, a_rhs); + + const typet &pt = ct.parameters()[0].type(); + const typet &st = ct.parameters()[1].type(); + auto size_opt = size_of_expr(d.type(), ns); + CHECK_RETURN(size_opt.has_value()); + auto call = goto_programt::make_function_call( + mm_io_r_value, + mm_io_r, + {typecast_exprt(d.pointer(), pt), + typecast_exprt(size_opt.value(), st)}, + source_location); + goto_function.body.insert_before_swap(it, call); + it++; } + } - if(mm_io_w.is_not_nil()) + if(mm_io_w.is_not_nil()) + { + if(a_lhs.id() == ID_dereference) { - if(a_lhs.id() == ID_dereference) - { - const dereference_exprt &d = to_dereference_expr(a_lhs); - source_locationt source_location = it->source_location(); - const code_typet &ct=to_code_type(mm_io_w.type()); - const typet &pt=ct.parameters()[0].type(); - const typet &st=ct.parameters()[1].type(); - const typet &vt=ct.parameters()[2].type(); - auto size_opt = size_of_expr(d.type(), ns); - CHECK_RETURN(size_opt.has_value()); - const code_function_callt fc( - mm_io_w, - {typecast_exprt(d.pointer(), pt), - typecast_exprt(size_opt.value(), st), - typecast_exprt(a_rhs, vt)}); - goto_function.body.insert_before_swap(it); - *it = goto_programt::make_function_call(fc, source_location); - it++; - } + const dereference_exprt &d = to_dereference_expr(a_lhs); + source_locationt source_location = it->source_location(); + const code_typet &ct = to_code_type(mm_io_w.type()); + const typet &pt = ct.parameters()[0].type(); + const typet &st = ct.parameters()[1].type(); + const typet &vt = ct.parameters()[2].type(); + auto size_opt = size_of_expr(d.type(), ns); + CHECK_RETURN(size_opt.has_value()); + const code_function_callt fc( + mm_io_w, + {typecast_exprt(d.pointer(), pt), + typecast_exprt(size_opt.value(), st), + typecast_exprt(a_rhs, vt)}); + goto_function.body.insert_before_swap(it); + *it = goto_programt::make_function_call(fc, source_location); + it++; } } } @@ -111,31 +108,30 @@ void mm_io( void mm_io(symbol_tablet &symbol_table, goto_functionst &goto_functions) { const namespacet ns(symbol_table); - exprt mm_io_r = nil_exprt(), mm_io_r_value = nil_exprt(), - mm_io_w = nil_exprt(); + exprt mm_io_r = nil_exprt(); + exprt mm_io_r_value = nil_exprt(); + exprt mm_io_w = nil_exprt(); - irep_idt id_r=CPROVER_PREFIX "mm_io_r"; - irep_idt id_w=CPROVER_PREFIX "mm_io_w"; + const irep_idt id_r = CPROVER_PREFIX "mm_io_r"; + const irep_idt id_w = CPROVER_PREFIX "mm_io_w"; - auto maybe_symbol=symbol_table.lookup(id_r); - if(maybe_symbol) + if(const auto mm_io_r_symbol = symbol_table.lookup(id_r)) { - mm_io_r=maybe_symbol->symbol_expr(); + mm_io_r = mm_io_r_symbol->symbol_expr(); const auto &value_symbol = get_fresh_aux_symbol( to_code_type(mm_io_r.type()).return_type(), id2string(id_r) + "$value", id2string(id_r) + "$value", - maybe_symbol->location, - maybe_symbol->mode, + mm_io_r_symbol->location, + mm_io_r_symbol->mode, symbol_table); mm_io_r_value = value_symbol.symbol_expr(); } - maybe_symbol=symbol_table.lookup(id_w); - if(maybe_symbol) - mm_io_w=maybe_symbol->symbol_expr(); + if(const auto mm_io_w_symbol = symbol_table.lookup(id_w)) + mm_io_w = mm_io_w_symbol->symbol_expr(); for(auto & f : goto_functions.function_map) mm_io(mm_io_r, mm_io_r_value, mm_io_w, f.second, ns); diff --git a/src/goto-programs/mm_io.h b/src/goto-programs/mm_io.h index 86f55c46323..54d60b1ed93 100644 --- a/src/goto-programs/mm_io.h +++ b/src/goto-programs/mm_io.h @@ -10,6 +10,21 @@ Date: April 2017 /// \file /// Perform Memory-mapped I/O instrumentation +/// +/// \details +/// In the case where a modelling function named `__CPROVER_mm_io_r` exists in +/// the symbol table, this pass will insert calls to this function before +/// pointer dereference reads. Only the case where there is a single dereference +/// on the right hand side of an assignment is included in the set of +/// dereference reads. +/// +/// In the case where a modelling function named +/// `__CPROVER_mm_io_w` exists in the symbol table, this pass will insert calls +/// to this function before all pointer dereference writes. All pointer +/// dereference writes are assumed to be on the left hand side of assignments. +/// +/// For details as to how and why this is used see the "Device behavior" section +/// of modeling-mmio.md #ifndef CPROVER_GOTO_PROGRAMS_MM_IO_H #define CPROVER_GOTO_PROGRAMS_MM_IO_H