Skip to content

Commit aec6269

Browse files
thomasspriggsthomasspriggs
authored
Merge pull request #7553 from thomasspriggs/tas/mmio_cleanup
Refactor and add documentation for `mmio` goto-program pass
2 parents 761facf + 810cc2a commit aec6269

File tree

2 files changed

+83
-72
lines changed

2 files changed

+83
-72
lines changed

‎src/goto-programs/mm_io.cpp‎

Lines changed: 68 additions & 72 deletions
Original file line numberDiff line numberDiff line change
@@ -23,14 +23,14 @@ Date: April 2017
2323

2424
#include <set>
2525

26-
void collect_deref_expr(
27-
const exprt &src,
28-
std::set<dereference_exprt> &dest)
26+
static std::set<dereference_exprt> collect_deref_expr(const exprt &src)
2927
{
30-
src.visit_pre([&dest](const exprt &e) {
28+
std::set<dereference_exprt> collected;
29+
src.visit_pre([&collected](const exprt &e) {
3130
if(e.id() == ID_dereference)
32-
dest.insert(to_dereference_expr(e));
31+
collected.insert(to_dereference_expr(e));
3332
});
33+
return collected;
3434
}
3535

3636
void mm_io(
@@ -40,69 +40,66 @@ void mm_io(
4040
goto_functionst::goto_functiont &goto_function,
4141
const namespacet &ns)
4242
{
43-
for(goto_programt::instructionst::iterator it=
44-
goto_function.body.instructions.begin();
45-
it!=goto_function.body.instructions.end();
43+
for(auto it = goto_function.body.instructions.begin();
44+
it != goto_function.body.instructions.end();
4645
it++)
4746
{
48-
std::set<dereference_exprt> deref_expr_w, deref_expr_r;
47+
if(!it->is_assign())
48+
continue;
4949

50-
if(it->is_assign())
51-
{
52-
auto &a_lhs = it->assign_lhs();
53-
auto &a_rhs = it->assign_rhs_nonconst();
54-
collect_deref_expr(a_rhs, deref_expr_r);
50+
auto &a_lhs = it->assign_lhs();
51+
auto &a_rhs = it->assign_rhs_nonconst();
52+
const auto deref_expr_r = collect_deref_expr(a_rhs);
5553

56-
if(mm_io_r.is_not_nil())
54+
if(mm_io_r.is_not_nil())
55+
{
56+
if(deref_expr_r.size() == 1)
5757
{
58-
if(deref_expr_r.size()==1)
59-
{
60-
const dereference_exprt &d=*deref_expr_r.begin();
61-
source_locationt source_location = it->source_location();
62-
const code_typet &ct=to_code_type(mm_io_r.type());
63-
64-
if_exprt if_expr(
65-
integer_address(d.pointer()),
66-
typecast_exprt::conditional_cast(mm_io_r_value, d.type()),
67-
d);
68-
replace_expr(d, if_expr, a_rhs);
69-
70-
const typet &pt=ct.parameters()[0].type();
71-
const typet &st=ct.parameters()[1].type();
72-
auto size_opt = size_of_expr(d.type(), ns);
73-
CHECK_RETURN(size_opt.has_value());
74-
auto call = goto_programt::make_function_call(
75-
mm_io_r_value,
76-
mm_io_r,
77-
{typecast_exprt(d.pointer(), pt),
78-
typecast_exprt(size_opt.value(), st)},
79-
source_location);
80-
goto_function.body.insert_before_swap(it, call);
81-
it++;
82-
}
58+
const dereference_exprt &d = *deref_expr_r.begin();
59+
source_locationt source_location = it->source_location();
60+
const code_typet &ct = to_code_type(mm_io_r.type());
61+
62+
if_exprt if_expr(
63+
integer_address(d.pointer()),
64+
typecast_exprt::conditional_cast(mm_io_r_value, d.type()),
65+
d);
66+
replace_expr(d, if_expr, a_rhs);
67+
68+
const typet &pt = ct.parameters()[0].type();
69+
const typet &st = ct.parameters()[1].type();
70+
auto size_opt = size_of_expr(d.type(), ns);
71+
CHECK_RETURN(size_opt.has_value());
72+
auto call = goto_programt::make_function_call(
73+
mm_io_r_value,
74+
mm_io_r,
75+
{typecast_exprt(d.pointer(), pt),
76+
typecast_exprt(size_opt.value(), st)},
77+
source_location);
78+
goto_function.body.insert_before_swap(it, call);
79+
it++;
8380
}
81+
}
8482

85-
if(mm_io_w.is_not_nil())
83+
if(mm_io_w.is_not_nil())
84+
{
85+
if(a_lhs.id() == ID_dereference)
8686
{
87-
if(a_lhs.id() == ID_dereference)
88-
{
89-
const dereference_exprt &d = to_dereference_expr(a_lhs);
90-
source_locationt source_location = it->source_location();
91-
const code_typet &ct=to_code_type(mm_io_w.type());
92-
const typet &pt=ct.parameters()[0].type();
93-
const typet &st=ct.parameters()[1].type();
94-
const typet &vt=ct.parameters()[2].type();
95-
auto size_opt = size_of_expr(d.type(), ns);
96-
CHECK_RETURN(size_opt.has_value());
97-
const code_function_callt fc(
98-
mm_io_w,
99-
{typecast_exprt(d.pointer(), pt),
100-
typecast_exprt(size_opt.value(), st),
101-
typecast_exprt(a_rhs, vt)});
102-
goto_function.body.insert_before_swap(it);
103-
*it = goto_programt::make_function_call(fc, source_location);
104-
it++;
105-
}
87+
const dereference_exprt &d = to_dereference_expr(a_lhs);
88+
source_locationt source_location = it->source_location();
89+
const code_typet &ct = to_code_type(mm_io_w.type());
90+
const typet &pt = ct.parameters()[0].type();
91+
const typet &st = ct.parameters()[1].type();
92+
const typet &vt = ct.parameters()[2].type();
93+
auto size_opt = size_of_expr(d.type(), ns);
94+
CHECK_RETURN(size_opt.has_value());
95+
const code_function_callt fc(
96+
mm_io_w,
97+
{typecast_exprt(d.pointer(), pt),
98+
typecast_exprt(size_opt.value(), st),
99+
typecast_exprt(a_rhs, vt)});
100+
goto_function.body.insert_before_swap(it);
101+
*it = goto_programt::make_function_call(fc, source_location);
102+
it++;
106103
}
107104
}
108105
}
@@ -111,31 +108,30 @@ void mm_io(
111108
void mm_io(symbol_tablet &symbol_table, goto_functionst &goto_functions)
112109
{
113110
const namespacet ns(symbol_table);
114-
exprt mm_io_r = nil_exprt(), mm_io_r_value = nil_exprt(),
115-
mm_io_w = nil_exprt();
111+
exprt mm_io_r = nil_exprt();
112+
exprt mm_io_r_value = nil_exprt();
113+
exprt mm_io_w = nil_exprt();
116114

117-
irep_idt id_r=CPROVER_PREFIX "mm_io_r";
118-
irep_idt id_w=CPROVER_PREFIX "mm_io_w";
115+
const irep_idt id_r = CPROVER_PREFIX "mm_io_r";
116+
const irep_idt id_w = CPROVER_PREFIX "mm_io_w";
119117

120-
auto maybe_symbol=symbol_table.lookup(id_r);
121-
if(maybe_symbol)
118+
if(const auto mm_io_r_symbol = symbol_table.lookup(id_r))
122119
{
123-
mm_io_r=maybe_symbol->symbol_expr();
120+
mm_io_r = mm_io_r_symbol->symbol_expr();
124121

125122
const auto &value_symbol = get_fresh_aux_symbol(
126123
to_code_type(mm_io_r.type()).return_type(),
127124
id2string(id_r) + "$value",
128125
id2string(id_r) + "$value",
129-
maybe_symbol->location,
130-
maybe_symbol->mode,
126+
mm_io_r_symbol->location,
127+
mm_io_r_symbol->mode,
131128
symbol_table);
132129

133130
mm_io_r_value = value_symbol.symbol_expr();
134131
}
135132

136-
maybe_symbol=symbol_table.lookup(id_w);
137-
if(maybe_symbol)
138-
mm_io_w=maybe_symbol->symbol_expr();
133+
if(const auto mm_io_w_symbol = symbol_table.lookup(id_w))
134+
mm_io_w = mm_io_w_symbol->symbol_expr();
139135

140136
for(auto & f : goto_functions.function_map)
141137
mm_io(mm_io_r, mm_io_r_value, mm_io_w, f.second, ns);

‎src/goto-programs/mm_io.h‎

Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -10,6 +10,21 @@ Date: April 2017
1010

1111
/// \file
1212
/// Perform Memory-mapped I/O instrumentation
13+
///
14+
/// \details
15+
/// In the case where a modelling function named `__CPROVER_mm_io_r` exists in
16+
/// the symbol table, this pass will insert calls to this function before
17+
/// pointer dereference reads. Only the case where there is a single dereference
18+
/// on the right hand side of an assignment is included in the set of
19+
/// dereference reads.
20+
///
21+
/// In the case where a modelling function named
22+
/// `__CPROVER_mm_io_w` exists in the symbol table, this pass will insert calls
23+
/// to this function before all pointer dereference writes. All pointer
24+
/// dereference writes are assumed to be on the left hand side of assignments.
25+
///
26+
/// For details as to how and why this is used see the "Device behavior" section
27+
/// of modeling-mmio.md
1328

1429
#ifndef CPROVER_GOTO_PROGRAMS_MM_IO_H
1530
#define CPROVER_GOTO_PROGRAMS_MM_IO_H

0 commit comments

Comments
 (0)