Skip to content

Refactor and add documentation for mmio goto-program pass #7553

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 9 commits into from
Feb 22, 2023
Merged

Refactor and add documentation for mmio goto-program pass #7553

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
9 commits
Select commit Hold shift + click to select a range
e4abae0
Separate declarations
thomasspriggs Feb 21, 2023
26b5184
Add `const` to mmio identifiers
thomasspriggs Feb 21, 2023
d7776db
Replace `maybe_symbol` with specific tighter scoped variables
thomasspriggs Feb 21, 2023
6b12425
Invert `is_assign` check
thomasspriggs Feb 21, 2023
45ea585
Declare iterator using `auto`
thomasspriggs Feb 21, 2023
cd98ce2
Add documentation of the `mm_io` pass in `mm_io.h`
thomasspriggs Feb 21, 2023
20d3841
Remove unused `deref_expr_w` variable
thomasspriggs Feb 21, 2023
60e3f91
Return result of `collect_deref_expr` function by value
thomasspriggs Feb 21, 2023
810cc2a
Declare `collect_deref_expr` as `static`
thomasspriggs Feb 21, 2023
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
140 changes: 68 additions & 72 deletions src/goto-programs/mm_io.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -23,14 +23,14 @@ Date: April 2017

#include <set>

void collect_deref_expr(
const exprt &src,
std::set<dereference_exprt> &dest)
static std::set<dereference_exprt> collect_deref_expr(const exprt &src)
{
src.visit_pre([&dest](const exprt &e) {
std::set<dereference_exprt> 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(
Expand All @@ -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<dereference_exprt> 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++;
}
}
}
Expand All @@ -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);
Expand Down
15 changes: 15 additions & 0 deletions src/goto-programs/mm_io.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down