cprover
mmio.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Memory-mapped I/O Instrumentation for Goto Programs
4 
5 Author: Daniel Kroening
6 
7 Date: September 2011
8 
9 \*******************************************************************/
10 
13 
14 #include "mmio.h"
15 
17 
18 #include "rw_set.h"
19 
20 #ifdef LOCAL_MAY
22 #endif
23 
24 void mmio(
25  value_setst &value_sets,
26  const symbol_tablet &symbol_table,
27 #ifdef LOCAL_MAY
28  const goto_functionst::goto_functiont &goto_function,
29 #endif
30  goto_programt &goto_program)
31 {
32  namespacet ns(symbol_table);
33 
34 #ifdef LOCAL_MAY
35  local_may_aliast local_may(goto_function);
36 #endif
37 
38  Forall_goto_program_instructions(i_it, goto_program)
39  {
40  goto_programt::instructiont &instruction=*i_it;
41 
42  if(instruction.is_assign())
43  {
44  rw_set_loct rw_set(ns, value_sets, i_it
45 #ifdef LOCAL_MAY
46  , local_may
47 #endif
48  ); // NOLINT(whitespace/parens)
49 
50  if(rw_set.empty())
51  continue;
52 
53  #if 0
54  goto_programt::instructiont original_instruction;
55  original_instruction.swap(instruction);
56  const locationt &location=original_instruction.location;
57 
58  instruction.make_atomic_begin();
59  instruction.location=location;
60  i_it++;
61 
62  // we first perform (non-deterministically) up to 2 writes for
63  // stuff that is potentially read
64  forall_rw_set_entries(e_it, rw_set)
65  if(e_it->second.r)
66  {
67  const shared_bufferst::varst &vars=
68  shared_buffers(e_it->second.object);
69  irep_idt choice0=shared_buffers.choice("0");
70  irep_idt choice1=shared_buffers.choice("1");
71 
72  symbol_exprt choice0_expr=symbol_exprt(choice0, bool_typet());
73  symbol_exprt choice1_expr=symbol_exprt(choice1, bool_typet());
74 
75  symbol_exprt w_buff0_expr=symbol_exprt(vars.w_buff0, vars.type);
76  symbol_exprt w_buff1_expr=symbol_exprt(vars.w_buff1, vars.type);
77 
78  symbol_exprt w_used0_expr=symbol_exprt(vars.w_used0, bool_typet());
79  symbol_exprt w_used1_expr=symbol_exprt(vars.w_used1, bool_typet());
80 
81  const side_effect_nondet_exprt nondet_bool_expr(bool_typet());
82 
83  const and_exprt choice0_rhs(nondet_bool_expr, w_used0_expr);
84  const and_exprt choice1_rhs(nondet_bool_expr, w_used1_expr);
85 
86  // throw 2 Boolean dice
87  shared_buffers.assignment(
88  goto_program, i_it, location, choice0, choice0_rhs);
89  shared_buffers.assignment(
90  goto_program, i_it, location, choice1, choice1_rhs);
91 
92  const symbol_exprt lhs(e_it->second.object, vars.type);
93 
94  const if_exprt value(
95  choice0_expr,
96  w_buff0_expr,
97  if_exprt(choice1_expr, w_buff1_expr, lhs));
98 
99  // write one of the buffer entries
100  shared_buffers.assignment(
101  goto_program, i_it, location, e_it->second.object, value);
102 
103  // update 'used' flags
104  const if_exprt w_used0_rhs(choice0_expr, false_exprt(), w_used0_expr);
105  const and_exprt w_used1_rhs(
106  if_exprt(
107  choice1_expr,
108  false_exprt(),
109  w_used1_expr),
110  w_used0_expr);
111 
112  shared_buffers.assignment(
113  goto_program, i_it, location, vars.w_used0, w_used0_rhs);
114  shared_buffers.assignment(
115  goto_program, i_it, location, vars.w_used1, w_used1_rhs);
116  }
117 
118  // now rotate the write buffers for anything that is written
119  forall_rw_set_entries(e_it, rw_set)
120  if(e_it->second.w)
121  {
122  const shared_bufferst::varst &vars=
123  shared_buffers(e_it->second.object);
124 
125  // w_used1=w_used0; w_used0=true;
126  shared_buffers.assignment(
127  goto_program, i_it, location, vars.w_used1, vars.w_used0);
128  shared_buffers.assignment(
129  goto_program, i_it, location, vars.w_used0, true_exprt());
130 
131  // w_buff1=w_buff0; w_buff0=RHS;
132  shared_buffers.assignment(
133  goto_program, i_it, location, vars.w_buff1, vars.w_buff0);
134  shared_buffers.assignment(
135  goto_program,
136  i_it, location,
137  vars.w_buff0,
138  original_instruction.code.op1());
139  }
140 
141  // ATOMIC_END
142  i_it=goto_program.insert_before(i_it);
143  i_it->make_atomic_end();
144  i_it->location=location;
145  i_it++;
146 
147  i_it--; // the for loop already counts us up
148  #endif
149  }
150  }
151 }
152 
153 void mmio(
154  value_setst &value_sets,
155  goto_modelt &goto_model)
156 {
157  // now instrument
158 
159  Forall_goto_functions(f_it, goto_model.goto_functions)
160  if(f_it->first != INITIALIZE_FUNCTION &&
161  f_it->first!=goto_functionst::entry_point())
162  mmio(value_sets, goto_model.symbol_table,
163 #ifdef LOCAL_MAY
164  f_it->second,
165 #endif
166  f_it->second.body);
167 
168  goto_model.goto_functions.update();
169 }
bool empty() const
Definition: rw_set.h:72
The trinary if-then-else operator.
Definition: std_expr.h:3427
The Boolean type.
Definition: std_types.h:28
void mmio(value_setst &value_sets, const symbol_tablet &symbol_table, goto_programt &goto_program)
Definition: mmio.cpp:24
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:29
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:178
The Boolean constant true.
Definition: std_expr.h:4443
#define INITIALIZE_FUNCTION
Boolean AND.
Definition: std_expr.h:2409
exprt & op1()
Definition: expr.h:87
The symbol table.
Definition: symbol_table.h:19
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
::goto_functiont goto_functiont
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:35
The Boolean constant false.
Definition: std_expr.h:4452
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:72
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
#define Forall_goto_functions(it, functions)
void swap(instructiont &instruction)
Swap two instructions.
Definition: goto_program.h:344
#define Forall_goto_program_instructions(it, program)
Definition: goto_program.h:809
Expression to hold a symbol (variable)
Definition: std_expr.h:143
Memory-mapped I/O Instrumentation for Goto Programs.
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:32
Field-insensitive, location-sensitive may-alias analysis.
Race Detection for Threaded Goto Programs.