cprover
mm_io.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Perform Memory-mapped I/O instrumentation
4 
5 Author: Daniel Kroening
6 
7 Date: 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 
37 void mm_io(
38  const exprt &mm_io_r,
39  const exprt &mm_io_r_value,
40  const exprt &mm_io_w,
41  goto_functionst::goto_functiont &goto_function,
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 
109 void 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 
142 void 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 typet & return_type() const
Definition: std_types.h:645
const parameterst & parameters() const
Definition: std_types.h:655
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