Skip to content

Commit 7b8fbc2

Browse files
committed
Refactor mm_io implementation
Use a class to maintain data that remains constant across calls.
1 parent f034dbb commit 7b8fbc2

File tree

1 file changed

+49
-32
lines changed

1 file changed

+49
-32
lines changed

src/goto-programs/mm_io.cpp

Lines changed: 49 additions & 32 deletions
Original file line numberDiff line numberDiff line change
@@ -23,6 +23,48 @@ Date: April 2017
2323

2424
#include <set>
2525

26+
class mm_iot
27+
{
28+
public:
29+
explicit mm_iot(symbol_table_baset &symbol_table);
30+
31+
void mm_io(goto_functionst::goto_functiont &goto_function);
32+
33+
protected:
34+
const irep_idt id_r = CPROVER_PREFIX "mm_io_r";
35+
const irep_idt id_w = CPROVER_PREFIX "mm_io_w";
36+
37+
const namespacet ns;
38+
exprt mm_io_r;
39+
exprt mm_io_r_value;
40+
exprt mm_io_w;
41+
};
42+
43+
mm_iot::mm_iot(symbol_table_baset &symbol_table)
44+
: ns(symbol_table),
45+
mm_io_r(nil_exprt{}),
46+
mm_io_r_value(nil_exprt{}),
47+
mm_io_w(nil_exprt{})
48+
{
49+
if(const auto mm_io_r_symbol = symbol_table.lookup(id_r))
50+
{
51+
mm_io_r = mm_io_r_symbol->symbol_expr();
52+
53+
const auto &value_symbol = get_fresh_aux_symbol(
54+
to_code_type(mm_io_r.type()).return_type(),
55+
id2string(id_r) + "$value",
56+
id2string(id_r) + "$value",
57+
mm_io_r_symbol->location,
58+
mm_io_r_symbol->mode,
59+
symbol_table);
60+
61+
mm_io_r_value = value_symbol.symbol_expr();
62+
}
63+
64+
if(const auto mm_io_w_symbol = symbol_table.lookup(id_w))
65+
mm_io_w = mm_io_w_symbol->symbol_expr();
66+
}
67+
2668
static std::set<dereference_exprt> collect_deref_expr(const exprt &src)
2769
{
2870
std::set<dereference_exprt> collected;
@@ -33,13 +75,12 @@ static std::set<dereference_exprt> collect_deref_expr(const exprt &src)
3375
return collected;
3476
}
3577

36-
void mm_io(
37-
const exprt &mm_io_r,
38-
const exprt &mm_io_r_value,
39-
const exprt &mm_io_w,
40-
goto_functionst::goto_functiont &goto_function,
41-
const namespacet &ns)
78+
void mm_iot::mm_io(goto_functionst::goto_functiont &goto_function)
4279
{
80+
// return early when there is nothing to be done
81+
if(mm_io_r.is_nil() && mm_io_w.is_nil())
82+
return;
83+
4384
for(auto it = goto_function.body.instructions.begin();
4485
it != goto_function.body.instructions.end();
4586
it++)
@@ -107,34 +148,10 @@ void mm_io(
107148

108149
void mm_io(symbol_tablet &symbol_table, goto_functionst &goto_functions)
109150
{
110-
const namespacet ns(symbol_table);
111-
exprt mm_io_r = nil_exprt();
112-
exprt mm_io_r_value = nil_exprt();
113-
exprt mm_io_w = nil_exprt();
114-
115-
const irep_idt id_r = CPROVER_PREFIX "mm_io_r";
116-
const irep_idt id_w = CPROVER_PREFIX "mm_io_w";
117-
118-
if(const auto mm_io_r_symbol = symbol_table.lookup(id_r))
119-
{
120-
mm_io_r = mm_io_r_symbol->symbol_expr();
121-
122-
const auto &value_symbol = get_fresh_aux_symbol(
123-
to_code_type(mm_io_r.type()).return_type(),
124-
id2string(id_r) + "$value",
125-
id2string(id_r) + "$value",
126-
mm_io_r_symbol->location,
127-
mm_io_r_symbol->mode,
128-
symbol_table);
129-
130-
mm_io_r_value = value_symbol.symbol_expr();
131-
}
132-
133-
if(const auto mm_io_w_symbol = symbol_table.lookup(id_w))
134-
mm_io_w = mm_io_w_symbol->symbol_expr();
151+
mm_iot rewrite{symbol_table};
135152

136153
for(auto & f : goto_functions.function_map)
137-
mm_io(mm_io_r, mm_io_r_value, mm_io_w, f.second, ns);
154+
rewrite.mm_io(f.second);
138155
}
139156

140157
void mm_io(goto_modelt &model)

0 commit comments

Comments
 (0)