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 
16 #include <util/cprover_prefix.h>
17 
20 
21 #if 0
22 #include <util/std_expr.h>
23 #include <util/guard.h>
24 #include <util/prefix.h>
25 
27 #endif
28 
29 #include "interrupt.h"
30 #include "rw_set.h"
31 
32 #ifdef LOCAL_MAY
34 #endif
35 
36 void mmio(
37  value_setst &value_sets,
38  const symbol_tablet &symbol_table,
39 #ifdef LOCAL_MAY
40  const goto_functionst::goto_functiont &goto_function,
41 #endif
42  goto_programt &goto_program)
43 {
44  namespacet ns(symbol_table);
45 
46 #ifdef LOCAL_MAY
47  local_may_aliast local_may(goto_function);
48 #endif
49 
50  Forall_goto_program_instructions(i_it, goto_program)
51  {
52  goto_programt::instructiont &instruction=*i_it;
53 
54  if(instruction.is_assign())
55  {
56  rw_set_loct rw_set(ns, value_sets, i_it
57 #ifdef LOCAL_MAY
58  , local_may
59 #endif
60  ); // NOLINT(whitespace/parens)
61 
62  if(rw_set.empty())
63  continue;
64 
65  #if 0
66  goto_programt::instructiont original_instruction;
67  original_instruction.swap(instruction);
68  const locationt &location=original_instruction.location;
69 
70  instruction.make_atomic_begin();
71  instruction.location=location;
72  i_it++;
73 
74  // we first perform (non-deterministically) up to 2 writes for
75  // stuff that is potentially read
76  forall_rw_set_entries(e_it, rw_set)
77  if(e_it->second.r)
78  {
79  const shared_bufferst::varst &vars=
80  shared_buffers(e_it->second.object);
81  irep_idt choice0=shared_buffers.choice("0");
82  irep_idt choice1=shared_buffers.choice("1");
83 
84  symbol_exprt choice0_expr=symbol_exprt(choice0, bool_typet());
85  symbol_exprt choice1_expr=symbol_exprt(choice1, bool_typet());
86 
87  symbol_exprt w_buff0_expr=symbol_exprt(vars.w_buff0, vars.type);
88  symbol_exprt w_buff1_expr=symbol_exprt(vars.w_buff1, vars.type);
89 
90  symbol_exprt w_used0_expr=symbol_exprt(vars.w_used0, bool_typet());
91  symbol_exprt w_used1_expr=symbol_exprt(vars.w_used1, bool_typet());
92 
93  exprt nondet_bool_expr=side_effect_nondet_exprt(bool_typet());
94 
95  exprt choice0_rhs=and_exprt(nondet_bool_expr, w_used0_expr);
96  exprt choice1_rhs=and_exprt(nondet_bool_expr, w_used1_expr);
97 
98  // throw 2 Boolean dice
99  shared_buffers.assignment(
100  goto_program, i_it, location, choice0, choice0_rhs);
101  shared_buffers.assignment(
102  goto_program, i_it, location, choice1, choice1_rhs);
103 
104  exprt lhs=symbol_exprt(e_it->second.object, vars.type);
105 
106  exprt value=
107  if_exprt(choice0_expr, w_buff0_expr,
108  if_exprt(choice1_expr, w_buff1_expr, lhs));
109 
110  // write one of the buffer entries
111  shared_buffers.assignment(
112  goto_program, i_it, location, e_it->second.object, value);
113 
114  // update 'used' flags
115  exprt w_used0_rhs=if_exprt(choice0_expr, false_exprt(), w_used0_expr);
116  exprt w_used1_rhs=
117  and_exprt(
118  if_exprt(
119  choice1_expr,
120  false_exprt(),
121  w_used1_expr),
122  w_used0_expr);
123 
124  shared_buffers.assignment(
125  goto_program, i_it, location, vars.w_used0, w_used0_rhs);
126  shared_buffers.assignment(
127  goto_program, i_it, location, vars.w_used1, w_used1_rhs);
128  }
129 
130  // now rotate the write buffers for anything that is written
131  forall_rw_set_entries(e_it, rw_set)
132  if(e_it->second.w)
133  {
134  const shared_bufferst::varst &vars=
135  shared_buffers(e_it->second.object);
136 
137  // w_used1=w_used0; w_used0=true;
138  shared_buffers.assignment(
139  goto_program, i_it, location, vars.w_used1, vars.w_used0);
140  shared_buffers.assignment(
141  goto_program, i_it, location, vars.w_used0, true_exprt());
142 
143  // w_buff1=w_buff0; w_buff0=RHS;
144  shared_buffers.assignment(
145  goto_program, i_it, location, vars.w_buff1, vars.w_buff0);
146  shared_buffers.assignment(
147  goto_program,
148  i_it, location,
149  vars.w_buff0,
150  original_instruction.code.op1());
151  }
152 
153  // ATOMIC_END
154  i_it=goto_program.insert_before(i_it);
155  i_it->make_atomic_end();
156  i_it->location=location;
157  i_it++;
158 
159  i_it--; // the for loop already counts us up
160  #endif
161  }
162  }
163 }
164 
165 void mmio(
166  value_setst &value_sets,
167  class symbol_tablet &symbol_table,
168  goto_functionst &goto_functions)
169 {
170  // we first figure out which objects are read/written by the ISR
171 
172 
173 
174  // now instrument
175 
176  Forall_goto_functions(f_it, goto_functions)
177  if(f_it->first!=CPROVER_PREFIX "initialize" &&
178  f_it->first!=goto_functionst::entry_point())
179  mmio(value_sets, symbol_table,
180 #ifdef LOCAL_MAY
181  f_it->second,
182 #endif
183  f_it->second.body);
184 
185  goto_functions.update();
186 }
#define CPROVER_PREFIX
bool empty() const
Definition: rw_set.h:72
Goto Programs with Functions.
The trinary if-then-else operator.
Definition: std_expr.h:2771
The proper Booleans.
Definition: std_types.h:33
void mmio(value_setst &value_sets, const symbol_tablet &symbol_table, goto_programt &goto_program)
Definition: mmio.cpp:36
The boolean constant true.
Definition: std_expr.h:3742
boolean AND
Definition: std_expr.h:1852
API to expression classes.
The symbol table.
Definition: symbol_table.h:52
TO_BE_DOCUMENTED.
Definition: namespace.h:62
Guard Data Structure.
goto_function_templatet< goto_programt > goto_functiont
The boolean constant false.
Definition: std_expr.h:3753
Interrupt Instrumentation for Goto Programs.
A specialization of goto_program_templatet over goto programs in which instructions have codet type...
Definition: goto_program.h:24
Base class for all expressions.
Definition: expr.h:46
#define Forall_goto_functions(it, functions)
#define Forall_goto_program_instructions(it, program)
Definition: goto_program.h:73
Expression to hold a symbol (variable)
Definition: std_expr.h:82
Memory-mapped I/O Instrumentation for Goto Programs.
Program Transformation.
Concrete Goto Program.
Field-insensitive, location-sensitive may-alias analysis.
Race Detection for Threaded Goto Programs.