cprover
Loading...
Searching...
No Matches
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
24#include <set>
25
26static std::set<dereference_exprt> collect_deref_expr(const exprt &src)
27{
28 std::set<dereference_exprt> collected;
29 src.visit_pre([&collected](const exprt &e) {
30 if(e.id() == ID_dereference)
32 });
33 return collected;
34}
35
36void mm_io(
37 const exprt &mm_io_r,
38 const exprt &mm_io_r_value,
39 const exprt &mm_io_w,
41 const namespacet &ns)
42{
43 for(auto it = goto_function.body.instructions.begin();
44 it != goto_function.body.instructions.end();
45 it++)
46 {
47 if(!it->is_assign())
48 continue;
49
50 auto &a_lhs = it->assign_lhs();
51 auto &a_rhs = it->assign_rhs_nonconst();
53
54 if(mm_io_r.is_not_nil())
55 {
56 if(deref_expr_r.size() == 1)
57 {
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
65 d);
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());
74 mm_io_r,
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 {
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());
96 mm_io_w,
98 typecast_exprt(size_opt.value(), st),
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
108void mm_io(symbol_tablet &symbol_table, goto_functionst &goto_functions)
109{
110 const namespacet ns(symbol_table);
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
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();
135
136 for(auto & f : goto_functions.function_map)
137 mm_io(mm_io_r, mm_io_r_value, mm_io_w, f.second, ns);
138}
139
140void mm_io(goto_modelt &model)
141{
142 mm_io(model.symbol_table, model.goto_functions);
143}
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:563
goto_instruction_codet representation of a function call statement.
Base type of functions.
Definition std_types.h:539
Operator to dereference a pointer.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:39
Base class for all expressions.
Definition expr.h:56
void visit_pre(std::function< void(exprt &)>)
Definition expr.cpp:227
typet & type()
Return the type of the expression.
Definition expr.h:84
A collection of goto functions.
function_mapt function_map
::goto_functiont goto_functiont
symbol_tablet symbol_table
Symbol table.
Definition goto_model.h:31
goto_functionst goto_functions
GOTO functions.
Definition goto_model.h:34
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:2323
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:3026
const symbolt * lookup(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
The symbol table.
Semantic type conversion.
Definition std_expr.h:2017
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition std_expr.h:2025
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:36
static std::set< dereference_exprt > collect_deref_expr(const exprt &src)
Definition mm_io.cpp:26
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.
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.
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