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 
18 #include <util/replace_expr.h>
19 
20 #include "remove_returns.h"
21 
23  const exprt &src,
24  std::set<dereference_exprt> &dest)
25 {
26  if(src.id()==ID_dereference)
27  dest.insert(to_dereference_expr(src));
28 
29  for(const auto & op : src.operands())
30  collect_deref_expr(op, dest); // recursive call
31 }
32 
33 void mm_io(
34  const exprt &mm_io_r,
35  const exprt &mm_io_w,
36  goto_functionst::goto_functiont &goto_function,
37  const namespacet &ns)
38 {
39  for(goto_programt::instructionst::iterator it=
40  goto_function.body.instructions.begin();
41  it!=goto_function.body.instructions.end();
42  it++)
43  {
44  std::set<dereference_exprt> deref_expr_w, deref_expr_r;
45 
46  if(it->is_assign())
47  {
48  auto &a=to_code_assign(it->code);
49  collect_deref_expr(a.rhs(), deref_expr_r);
50 
51  if(mm_io_r.is_not_nil())
52  {
53  if(deref_expr_r.size()==1)
54  {
55  const dereference_exprt &d=*deref_expr_r.begin();
56  source_locationt source_location=it->source_location;
57  irep_idt function=it->function;
59  const code_typet &ct=to_code_type(mm_io_r.type());
60 
61  irep_idt identifier=to_symbol_expr(mm_io_r).get_identifier();
62  irep_idt r_identifier=id2string(identifier)+RETURN_VALUE_SUFFIX;
63  symbol_exprt return_value(r_identifier, ct.return_type());
64  if_exprt if_expr(integer_address(d.pointer()), return_value, d);
65  replace_expr(d, if_expr, a.rhs());
66 
67  const typet &pt=ct.parameters()[0].type();
68  const typet &st=ct.parameters()[1].type();
69  exprt size=size_of_expr(d.type(), ns);
70  fc.arguments().resize(2);
71  fc.arguments()[0]=typecast_exprt(d.pointer(), pt);
72  fc.arguments()[1]=typecast_exprt(size, st);
73  fc.function()=mm_io_r;
74  goto_function.body.insert_before_swap(it);
75  it->make_function_call(fc);
76  it->source_location=source_location;
77  it->function=function;
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  irep_idt function=it->function;
90  const code_typet &ct=to_code_type(mm_io_w.type());
91  const typet &pt=ct.parameters()[0].type();
92  const typet &st=ct.parameters()[1].type();
93  const typet &vt=ct.parameters()[2].type();
94  exprt size=size_of_expr(d.type(), ns);
95  fc.arguments().resize(3);
96  fc.arguments()[0]=typecast_exprt(d.pointer(), pt);
97  fc.arguments()[1]=typecast_exprt(size, st);
98  fc.arguments()[2]=typecast_exprt(a.rhs(), vt);
99  fc.function()=mm_io_w;
100  goto_function.body.insert_before_swap(it);
101  it->make_function_call(fc);
102  it->source_location=source_location;
103  it->function=function;
104  it++;
105  }
106  }
107  }
108  }
109 }
110 
111 void mm_io(
112  const symbol_tablet &symbol_table,
113  goto_functionst &goto_functions)
114 {
115  const namespacet ns(symbol_table);
116  exprt mm_io_r=nil_exprt(), mm_io_w=nil_exprt();
117 
118  irep_idt id_r=CPROVER_PREFIX "mm_io_r";
119  irep_idt id_w=CPROVER_PREFIX "mm_io_w";
120 
121  auto maybe_symbol=symbol_table.lookup(id_r);
122  if(maybe_symbol)
123  mm_io_r=maybe_symbol->symbol_expr();
124 
125  maybe_symbol=symbol_table.lookup(id_w);
126  if(maybe_symbol)
127  mm_io_w=maybe_symbol->symbol_expr();
128 
129  for(auto & f : goto_functions.function_map)
130  mm_io(mm_io_r, mm_io_w, f.second, ns);
131 }
132 
133 void mm_io(goto_modelt &model)
134 {
135  mm_io(model.symbol_table, model.goto_functions);
136 }
The type of an expression.
Definition: type.h:22
exprt size_of_expr(const typet &type, const namespacet &ns)
semantic type conversion
Definition: std_expr.h:2111
Base type of functions.
Definition: std_types.h:764
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
bool is_not_nil() const
Definition: irep.h:173
#define CPROVER_PREFIX
void collect_deref_expr(const exprt &src, std::set< dereference_exprt > &dest)
Definition: mm_io.cpp:22
const code_typet & to_code_type(const typet &type)
Cast a generic typet to a code_typet.
Definition: std_types.h:993
const irep_idt & get_identifier() const
Definition: std_expr.h:128
The trinary if-then-else operator.
Definition: std_expr.h:3359
function_mapt function_map
typet & type()
Definition: expr.h:56
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:29
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast a generic exprt to a dereference_exprt.
Definition: std_expr.h:3326
const code_assignt & to_code_assign(const codet &code)
Definition: std_code.h:240
Perform Memory-mapped I/O instrumentation.
const irep_idt & id() const
Definition: irep.h:259
bool replace_expr(const exprt &what, const exprt &by, exprt &dest)
class symbol_exprt symbol_expr() const
produces a symbol_exprt for a symbol
Definition: symbol.cpp:111
argumentst & arguments()
Definition: std_code.h:890
The NIL expression.
Definition: std_expr.h:4508
Operator to dereference a pointer.
Definition: std_expr.h:3282
exprt integer_address(const exprt &pointer)
The symbol table.
Definition: symbol_table.h:19
TO_BE_DOCUMENTED.
Definition: namespace.h:74
::goto_functiont goto_functiont
A function call.
Definition: std_code.h:858
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
Definition: std_expr.h:210
Remove function returns.
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:33
Various predicates over pointers in programs.
Pointer Logic.
exprt & function()
Definition: std_code.h:878
Base class for all expressions.
Definition: expr.h:42
exprt & pointer()
Definition: std_expr.h:3305
const parameterst & parameters() const
Definition: std_types.h:905
const source_locationt & source_location() const
Definition: expr.h:125
Expression to hold a symbol (variable)
Definition: std_expr.h:90
#define RETURN_VALUE_SUFFIX
operandst & operands()
Definition: expr.h:66
const symbolt * lookup(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
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:33
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:32
const typet & return_type() const
Definition: std_types.h:895