From e4abae07a437927687e2b1985113350c0d1793af Mon Sep 17 00:00:00 2001 From: Thomas Spriggs Date: Tue, 21 Feb 2023 11:50:52 +0000 Subject: [PATCH 1/9] Separate declarations In order to make the naming pattern easier to spot. --- src/goto-programs/mm_io.cpp | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/src/goto-programs/mm_io.cpp b/src/goto-programs/mm_io.cpp index 2346ff40cbe..96933d33a4e 100644 --- a/src/goto-programs/mm_io.cpp +++ b/src/goto-programs/mm_io.cpp @@ -111,8 +111,9 @@ 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"; From 26b5184e49dedf5940ec8b318278854359bdde08 Mon Sep 17 00:00:00 2001 From: Thomas Spriggs Date: Tue, 21 Feb 2023 11:51:30 +0000 Subject: [PATCH 2/9] Add `const` to mmio identifiers To make it clear that they are not mutated. --- src/goto-programs/mm_io.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/goto-programs/mm_io.cpp b/src/goto-programs/mm_io.cpp index 96933d33a4e..0692a874345 100644 --- a/src/goto-programs/mm_io.cpp +++ b/src/goto-programs/mm_io.cpp @@ -115,8 +115,8 @@ void mm_io(symbol_tablet &symbol_table, goto_functionst &goto_functions) 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) From d7776dbb154d59734b3746a26410d212ea77c4d3 Mon Sep 17 00:00:00 2001 From: Thomas Spriggs Date: Tue, 21 Feb 2023 11:55:42 +0000 Subject: [PATCH 3/9] Replace `maybe_symbol` with specific tighter scoped variables This ensures that the variable is only in scope when it is non-null. --- src/goto-programs/mm_io.cpp | 14 ++++++-------- 1 file changed, 6 insertions(+), 8 deletions(-) diff --git a/src/goto-programs/mm_io.cpp b/src/goto-programs/mm_io.cpp index 0692a874345..3e74f25ce79 100644 --- a/src/goto-programs/mm_io.cpp +++ b/src/goto-programs/mm_io.cpp @@ -118,25 +118,23 @@ void mm_io(symbol_tablet &symbol_table, goto_functionst &goto_functions) 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); From 6b124259854b6cf22872f2bdda517082469a52ce Mon Sep 17 00:00:00 2001 From: Thomas Spriggs Date: Tue, 21 Feb 2023 11:58:33 +0000 Subject: [PATCH 4/9] Invert `is_assign` check To reduce indentation and make it clear that this check filters which instructions the loop operates on. --- src/goto-programs/mm_io.cpp | 102 ++++++++++++++++++------------------ 1 file changed, 51 insertions(+), 51 deletions(-) diff --git a/src/goto-programs/mm_io.cpp b/src/goto-programs/mm_io.cpp index 3e74f25ce79..1d40fd0dcc8 100644 --- a/src/goto-programs/mm_io.cpp +++ b/src/goto-programs/mm_io.cpp @@ -45,64 +45,64 @@ void mm_io( it!=goto_function.body.instructions.end(); it++) { + if(!it->is_assign()) + continue; + std::set deref_expr_w, deref_expr_r; - 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(); + collect_deref_expr(a_rhs, deref_expr_r); - 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++; } } } From 45ea5852bf6a3f3325032e2a9315024a5f996b7d Mon Sep 17 00:00:00 2001 From: Thomas Spriggs Date: Tue, 21 Feb 2023 12:39:52 +0000 Subject: [PATCH 5/9] Declare iterator using `auto` This removes the need for an excessively vebose type, matches C++11 style and is suggested by clang-tidy. --- src/goto-programs/mm_io.cpp | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/src/goto-programs/mm_io.cpp b/src/goto-programs/mm_io.cpp index 1d40fd0dcc8..bedcf5991ed 100644 --- a/src/goto-programs/mm_io.cpp +++ b/src/goto-programs/mm_io.cpp @@ -40,9 +40,8 @@ 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++) { if(!it->is_assign()) From cd98ce20836a05aba550b8b9742395c55fc81b68 Mon Sep 17 00:00:00 2001 From: Thomas Spriggs Date: Tue, 21 Feb 2023 14:11:56 +0000 Subject: [PATCH 6/9] Add documentation of the `mm_io` pass in `mm_io.h` So that there is an overview of the algorithm used and so that the relevant markdown file about the related feature is more easily discoverable. --- src/goto-programs/mm_io.h | 15 +++++++++++++++ 1 file changed, 15 insertions(+) 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 From 20d384130f0b60a9dee4a6f73371c58bed2a9113 Mon Sep 17 00:00:00 2001 From: Thomas Spriggs Date: Tue, 21 Feb 2023 14:14:55 +0000 Subject: [PATCH 7/9] Remove unused `deref_expr_w` variable This helps make it clearer that the dereference writes operation considers only a single write per assignment, rather than a set of writes. --- src/goto-programs/mm_io.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/goto-programs/mm_io.cpp b/src/goto-programs/mm_io.cpp index bedcf5991ed..66896210807 100644 --- a/src/goto-programs/mm_io.cpp +++ b/src/goto-programs/mm_io.cpp @@ -47,7 +47,7 @@ void mm_io( if(!it->is_assign()) continue; - std::set deref_expr_w, deref_expr_r; + std::set deref_expr_r; auto &a_lhs = it->assign_lhs(); auto &a_rhs = it->assign_rhs_nonconst(); From 60e3f91e5b01898485dab786c1ff687536b53b8c Mon Sep 17 00:00:00 2001 From: Thomas Spriggs Date: Tue, 21 Feb 2023 14:24:35 +0000 Subject: [PATCH 8/9] Return result of `collect_deref_expr` function by value This allows for `deref_expr_r` to be made constant, which makes it clear that the set is rebuilt for each assign instruction and is built in one place only. This also makes it clear that the result of the `collect_deref_expr` function is its return value. There is no performance cost to this refactor as Return Value Optimization (RVO) applies in this case. --- src/goto-programs/mm_io.cpp | 14 ++++++-------- 1 file changed, 6 insertions(+), 8 deletions(-) diff --git a/src/goto-programs/mm_io.cpp b/src/goto-programs/mm_io.cpp index 66896210807..1f10e37a7fc 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) +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( @@ -47,11 +47,9 @@ void mm_io( if(!it->is_assign()) continue; - std::set deref_expr_r; - auto &a_lhs = it->assign_lhs(); auto &a_rhs = it->assign_rhs_nonconst(); - collect_deref_expr(a_rhs, deref_expr_r); + const auto deref_expr_r = collect_deref_expr(a_rhs); if(mm_io_r.is_not_nil()) { From 810cc2ad97c89d4adc2dd54bb2844f0aa630324f Mon Sep 17 00:00:00 2001 From: Thomas Spriggs Date: Tue, 21 Feb 2023 15:00:45 +0000 Subject: [PATCH 9/9] Declare `collect_deref_expr` as `static` This makes it clear from reading the `.cpp` file only that this function is not part of the external API and is used within this file only. --- src/goto-programs/mm_io.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/goto-programs/mm_io.cpp b/src/goto-programs/mm_io.cpp index 1f10e37a7fc..6590fc7e4b7 100644 --- a/src/goto-programs/mm_io.cpp +++ b/src/goto-programs/mm_io.cpp @@ -23,7 +23,7 @@ Date: April 2017 #include -std::set collect_deref_expr(const exprt &src) +static std::set collect_deref_expr(const exprt &src) { std::set collected; src.visit_pre([&collected](const exprt &e) {