cprover
mm_io.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Perform Memory-mapped I/O instrumentation
4
5Author: Daniel Kroening
6
7Date: April 2017
8
9\*******************************************************************/
10
13
14#include "mm_io.h"
15
16#include <util/fresh_symbol.h>
17#include <util/pointer_expr.h>
20#include <util/replace_expr.h>
21
22#include "goto_model.h"
23#include "remove_returns.h"
24
25#include <set>
26
28 const exprt &src,
29 std::set<dereference_exprt> &dest)
30{
31 src.visit_pre([&dest](const exprt &e) {
32 if(e.id() == ID_dereference)
33 dest.insert(to_dereference_expr(e));
34 });
35}
36
37void mm_io(
38 const exprt &mm_io_r,
39 const exprt &mm_io_r_value,
40 const exprt &mm_io_w,
42 const namespacet &ns)
43{
44 for(goto_programt::instructionst::iterator it=
45 goto_function.body.instructions.begin();
46 it!=goto_function.body.instructions.end();
47 it++)
48 {
49 std::set<dereference_exprt> deref_expr_w, deref_expr_r;
50
51 if(it->is_assign())
52 {
53 auto &a_lhs = it->assign_lhs();
54 auto &a_rhs = it->assign_rhs_nonconst();
55 collect_deref_expr(a_rhs, deref_expr_r);
56
57 if(mm_io_r.is_not_nil())
58 {
59 if(deref_expr_r.size()==1)
60 {
61 const dereference_exprt &d=*deref_expr_r.begin();
62 source_locationt source_location = it->source_location();
63 const code_typet &ct=to_code_type(mm_io_r.type());
64
65 if_exprt if_expr(integer_address(d.pointer()), mm_io_r_value, 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());
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++;
80 }
81 }
82
83 if(mm_io_w.is_not_nil())
84 {
85 if(a_lhs.id() == ID_dereference)
86 {
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++;
103 }
104 }
105 }
106 }
107}
108
109void mm_io(symbol_tablet &symbol_table, goto_functionst &goto_functions)
110{
111 const namespacet ns(symbol_table);
112 exprt mm_io_r = nil_exprt(), mm_io_r_value = nil_exprt(),
113 mm_io_w = nil_exprt();
114
115 irep_idt id_r=CPROVER_PREFIX "mm_io_r";
116 irep_idt id_w=CPROVER_PREFIX "mm_io_w";
117
118 auto maybe_symbol=symbol_table.lookup(id_r);
119 if(maybe_symbol)
120 {
121 mm_io_r=maybe_symbol->symbol_expr();
122
123 const auto &value_symbol = get_fresh_aux_symbol(
124 to_code_type(mm_io_r.type()).return_type(),
125 id2string(id_r) + "$value",
126 id2string(id_r) + "$value",
127 maybe_symbol->location,
128 maybe_symbol->mode,
129 symbol_table);
130
131 mm_io_r_value = value_symbol.symbol_expr();
132 }
133
134 maybe_symbol=symbol_table.lookup(id_w);
135 if(maybe_symbol)
136 mm_io_w=maybe_symbol->symbol_expr();
137
138 for(auto & f : goto_functions.function_map)
139 mm_io(mm_io_r, mm_io_r_value, mm_io_w, f.second, ns);
140}
141
142void mm_io(goto_modelt &model)
143{
144 mm_io(model.symbol_table, model.goto_functions);
145}
codet representation of a function call statement.
Base type of functions.
Definition: std_types.h:539
const parameterst & parameters() const
Definition: std_types.h:655
const typet & return_type() const
Definition: std_types.h:645
Operator to dereference a pointer.
Definition: pointer_expr.h:648
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
Base class for all expressions.
Definition: expr.h:54
void visit_pre(std::function< void(exprt &)>)
Definition: expr.cpp:245
typet & type()
Return the type of the expression.
Definition: expr.h:82
A collection of goto functions.
function_mapt function_map
::goto_functiont goto_functiont
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:30
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:33
static instructiont make_function_call(const code_function_callt &_code, const source_locationt &l=source_locationt::nil())
Create a function call instruction.
The trinary if-then-else operator.
Definition: std_expr.h:2226
bool is_not_nil() const
Definition: irep.h:380
const irep_idt & id() const
Definition: irep.h:396
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
The NIL expression.
Definition: std_expr.h:2874
const symbolt * lookup(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
The symbol table.
Definition: symbol_table.h:14
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition: symbol.cpp:121
Semantic type conversion.
Definition: std_expr.h:1920
The type of an expression, extends irept.
Definition: type.h:29
#define CPROVER_PREFIX
symbolt & get_fresh_aux_symbol(const typet &type, const std::string &name_prefix, const std::string &basename_prefix, const source_locationt &source_location, const irep_idt &symbol_mode, const namespacet &ns, symbol_table_baset &symbol_table)
Installs a fresh-named symbol with respect to the given namespace ns with the requested name pattern ...
Fresh auxiliary symbol creation.
Symbol Table + CFG.
const std::string & id2string(const irep_idt &d)
Definition: irep.h:47
void mm_io(const exprt &mm_io_r, const exprt &mm_io_r_value, const exprt &mm_io_w, goto_functionst::goto_functiont &goto_function, const namespacet &ns)
Definition: mm_io.cpp:37
void collect_deref_expr(const exprt &src, std::set< dereference_exprt > &dest)
Definition: mm_io.cpp:27
Perform Memory-mapped I/O instrumentation.
API to expression classes for Pointers.
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
Definition: pointer_expr.h:704
optionalt< exprt > size_of_expr(const typet &type, const namespacet &ns)
Pointer Logic.
exprt integer_address(const exprt &pointer)
Various predicates over pointers in programs.
Replace function returns by assignments to global variables.
bool replace_expr(const exprt &what, const exprt &by, exprt &dest)
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:495
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:744