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/pointer_expr.h>
19 #include <util/replace_expr.h>
20 
21 #include "goto_model.h"
22 #include "remove_returns.h"
23 
24 #include <set>
25 
27  const exprt &src,
28  std::set<dereference_exprt> &dest)
29 {
30  src.visit_pre([&dest](const exprt &e) {
31  if(e.id() == ID_dereference)
32  dest.insert(to_dereference_expr(e));
33  });
34 }
35 
36 void mm_io(
37  const exprt &mm_io_r,
38  const exprt &mm_io_w,
39  goto_functionst::goto_functiont &goto_function,
40  const namespacet &ns)
41 {
42  for(goto_programt::instructionst::iterator it=
43  goto_function.body.instructions.begin();
44  it!=goto_function.body.instructions.end();
45  it++)
46  {
47  std::set<dereference_exprt> deref_expr_w, deref_expr_r;
48 
49  if(it->is_assign())
50  {
51  auto &a_lhs = it->assign_lhs();
52  auto &a_rhs = it->assign_rhs_nonconst();
53  collect_deref_expr(a_rhs, deref_expr_r);
54 
55  if(mm_io_r.is_not_nil())
56  {
57  if(deref_expr_r.size()==1)
58  {
59  const dereference_exprt &d=*deref_expr_r.begin();
60  source_locationt source_location=it->source_location;
61  const code_typet &ct=to_code_type(mm_io_r.type());
62 
63  irep_idt identifier=to_symbol_expr(mm_io_r).get_identifier();
64  auto return_value = return_value_symbol(identifier, ns);
65  if_exprt if_expr(integer_address(d.pointer()), return_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());
72  const code_function_callt fc(
73  mm_io_r,
74  {typecast_exprt(d.pointer(), pt),
75  typecast_exprt(size_opt.value(), st)});
76  goto_function.body.insert_before_swap(it);
77  *it = goto_programt::make_function_call(fc, source_location);
78  it++;
79  }
80  }
81 
82  if(mm_io_w.is_not_nil())
83  {
84  if(a_lhs.id() == ID_dereference)
85  {
86  const dereference_exprt &d = to_dereference_expr(a_lhs);
87  source_locationt source_location=it->source_location;
88  const code_typet &ct=to_code_type(mm_io_w.type());
89  const typet &pt=ct.parameters()[0].type();
90  const typet &st=ct.parameters()[1].type();
91  const typet &vt=ct.parameters()[2].type();
92  auto size_opt = size_of_expr(d.type(), ns);
93  CHECK_RETURN(size_opt.has_value());
94  const code_function_callt fc(
95  mm_io_w,
96  {typecast_exprt(d.pointer(), pt),
97  typecast_exprt(size_opt.value(), st),
98  typecast_exprt(a_rhs, vt)});
99  goto_function.body.insert_before_swap(it);
100  *it = goto_programt::make_function_call(fc, source_location);
101  it++;
102  }
103  }
104  }
105  }
106 }
107 
108 void mm_io(
109  const symbol_tablet &symbol_table,
110  goto_functionst &goto_functions)
111 {
112  const namespacet ns(symbol_table);
113  exprt mm_io_r=nil_exprt(), 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  mm_io_r=maybe_symbol->symbol_expr();
121 
122  maybe_symbol=symbol_table.lookup(id_w);
123  if(maybe_symbol)
124  mm_io_w=maybe_symbol->symbol_expr();
125 
126  for(auto & f : goto_functions.function_map)
127  mm_io(mm_io_r, mm_io_w, f.second, ns);
128 }
129 
130 void mm_io(goto_modelt &model)
131 {
132  mm_io(model.symbol_table, model.goto_functions);
133 }
codet representation of a function call statement.
Definition: std_code.h:1213
Base type of functions.
Definition: std_types.h:539
const parameterst & parameters() const
Definition: std_types.h:655
Operator to dereference a pointer.
Definition: pointer_expr.h:628
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:2172
bool is_not_nil() const
Definition: irep.h:391
const irep_idt & id() const
Definition: irep.h:407
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:2820
const irep_idt & get_identifier() const
Definition: std_expr.h:109
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:1866
The type of an expression, extends irept.
Definition: type.h:28
#define CPROVER_PREFIX
Symbol Table + CFG.
void mm_io(const exprt &mm_io_r, const exprt &mm_io_w, goto_functionst::goto_functiont &goto_function, const namespacet &ns)
Definition: mm_io.cpp:36
void collect_deref_expr(const exprt &src, std::set< dereference_exprt > &dest)
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.
Definition: pointer_expr.h:684
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.
symbol_exprt return_value_symbol(const irep_idt &identifier, const namespacet &ns)
produces the symbol that is used to store the return value of the function with the given identifier
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 symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:189
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:744