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  src.visit_pre([&dest](const exprt &e) {
27  if(e.id() == ID_dereference)
28  dest.insert(to_dereference_expr(e));
29  });
30 }
31 
32 void mm_io(
33  const exprt &mm_io_r,
34  const exprt &mm_io_w,
35  goto_functionst::goto_functiont &goto_function,
36  const namespacet &ns)
37 {
38  for(goto_programt::instructionst::iterator it=
39  goto_function.body.instructions.begin();
40  it!=goto_function.body.instructions.end();
41  it++)
42  {
43  std::set<dereference_exprt> deref_expr_w, deref_expr_r;
44 
45  if(it->is_assign())
46  {
47  auto a = it->get_assign();
48  collect_deref_expr(a.rhs(), deref_expr_r);
49 
50  if(mm_io_r.is_not_nil())
51  {
52  if(deref_expr_r.size()==1)
53  {
54  const dereference_exprt &d=*deref_expr_r.begin();
55  source_locationt source_location=it->source_location;
56  const code_typet &ct=to_code_type(mm_io_r.type());
57 
58  irep_idt identifier=to_symbol_expr(mm_io_r).get_identifier();
59  auto return_value = return_value_symbol(identifier, ns);
60  if_exprt if_expr(integer_address(d.pointer()), return_value, d);
61  if(!replace_expr(d, if_expr, a.rhs()))
62  it->set_assign(a);
63 
64  const typet &pt=ct.parameters()[0].type();
65  const typet &st=ct.parameters()[1].type();
66  auto size_opt = size_of_expr(d.type(), ns);
67  CHECK_RETURN(size_opt.has_value());
68  const code_function_callt fc(
69  mm_io_r,
70  {typecast_exprt(d.pointer(), pt),
71  typecast_exprt(size_opt.value(), st)});
72  goto_function.body.insert_before_swap(it);
73  *it = goto_programt::make_function_call(fc, source_location);
74  it++;
75  }
76  }
77 
78  if(mm_io_w.is_not_nil())
79  {
80  if(a.lhs().id()==ID_dereference)
81  {
82  const dereference_exprt &d=to_dereference_expr(a.lhs());
83  source_locationt source_location=it->source_location;
84  const code_typet &ct=to_code_type(mm_io_w.type());
85  const typet &pt=ct.parameters()[0].type();
86  const typet &st=ct.parameters()[1].type();
87  const typet &vt=ct.parameters()[2].type();
88  auto size_opt = size_of_expr(d.type(), ns);
89  CHECK_RETURN(size_opt.has_value());
90  const code_function_callt fc(
91  mm_io_w,
92  {typecast_exprt(d.pointer(), pt),
93  typecast_exprt(size_opt.value(), st),
94  typecast_exprt(a.rhs(), vt)});
95  goto_function.body.insert_before_swap(it);
96  *it = goto_programt::make_function_call(fc, source_location);
97  it++;
98  }
99  }
100  }
101  }
102 }
103 
104 void mm_io(
105  const symbol_tablet &symbol_table,
106  goto_functionst &goto_functions)
107 {
108  const namespacet ns(symbol_table);
109  exprt mm_io_r=nil_exprt(), mm_io_w=nil_exprt();
110 
111  irep_idt id_r=CPROVER_PREFIX "mm_io_r";
112  irep_idt id_w=CPROVER_PREFIX "mm_io_w";
113 
114  auto maybe_symbol=symbol_table.lookup(id_r);
115  if(maybe_symbol)
116  mm_io_r=maybe_symbol->symbol_expr();
117 
118  maybe_symbol=symbol_table.lookup(id_w);
119  if(maybe_symbol)
120  mm_io_w=maybe_symbol->symbol_expr();
121 
122  for(auto & f : goto_functions.function_map)
123  mm_io(mm_io_r, mm_io_w, f.second, ns);
124 }
125 
126 void mm_io(goto_modelt &model)
127 {
128  mm_io(model.symbol_table, model.goto_functions);
129 }
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
pointer_offset_size.h
Pointer Logic.
symbol_tablet
The symbol table.
Definition: symbol_table.h:20
CHECK_RETURN
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:496
typet
The type of an expression, extends irept.
Definition: type.h:29
mm_io
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:32
dereference_exprt
Operator to dereference a pointer.
Definition: std_expr.h:2888
if_exprt
The trinary if-then-else operator.
Definition: std_expr.h:2964
pointer_predicates.h
Various predicates over pointers in programs.
exprt
Base class for all expressions.
Definition: expr.h:53
goto_modelt
Definition: goto_model.h:26
goto_functionst::function_map
function_mapt function_map
Definition: goto_functions.h:27
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
goto_programt::make_function_call
static instructiont make_function_call(const code_function_callt &_code, const source_locationt &l=source_locationt::nil())
Create a function call instruction.
Definition: goto_program.h:1049
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:81
code_function_callt
codet representation of a function call statement.
Definition: std_code.h:1183
irept::is_not_nil
bool is_not_nil() const
Definition: irep.h:402
collect_deref_expr
void collect_deref_expr(const exprt &src, std::set< dereference_exprt > &dest)
Definition: mm_io.cpp:22
to_code_type
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:946
mm_io.h
Perform Memory-mapped I/O instrumentation.
symbol_exprt::get_identifier
const irep_idt & get_identifier() const
Definition: std_expr.h:111
nil_exprt
The NIL expression.
Definition: std_expr.h:3973
dereference_exprt::pointer
exprt & pointer()
Definition: std_expr.h:2901
symbolt::symbol_expr
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition: symbol.cpp:122
integer_address
exprt integer_address(const exprt &pointer)
Definition: pointer_predicates.cpp:129
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:177
code_typet
Base type of functions.
Definition: std_types.h:736
irept::id
const irep_idt & id() const
Definition: irep.h:418
code_typet::parameters
const parameterst & parameters() const
Definition: std_types.h:857
remove_returns.h
Replace function returns by assignments to global variables.
source_locationt
Definition: source_location.h:20
goto_functionst::goto_functiont
::goto_functiont goto_functiont
Definition: goto_functions.h:25
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:23
to_dereference_expr
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
Definition: std_expr.h:2944
goto_modelt::goto_functions
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:33
replace_expr
bool replace_expr(const exprt &what, const exprt &by, exprt &dest)
Definition: replace_expr.cpp:12
CPROVER_PREFIX
#define CPROVER_PREFIX
Definition: cprover_prefix.h:14
exprt::visit_pre
void visit_pre(std::function< void(exprt &)>)
Definition: expr.cpp:311
return_value_symbol
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
Definition: remove_returns.cpp:415
symbol_table_baset::lookup
const symbolt * lookup(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
Definition: symbol_table_base.h:95
size_of_expr
optionalt< exprt > size_of_expr(const typet &type, const namespacet &ns)
Definition: pointer_offset_size.cpp:285
replace_expr.h
typecast_exprt
Semantic type conversion.
Definition: std_expr.h:2013
goto_modelt::symbol_table
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:30