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