cprover
Loading...
Searching...
No Matches
mmio.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Memory-mapped I/O Instrumentation for Goto Programs
4
5Author: Daniel Kroening
6
7Date: 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
24static 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
159void 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:2125
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:3077
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.
const goto_instruction_codet & code() const
Get the code represented by this instruction.
void swap(instructiont &instruction)
Swap two instructions.
A generic container class for the GOTO intermediate representation of one function.
The trinary if-then-else operator.
Definition std_expr.h:2375
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.
The Boolean constant true.
Definition std_expr.h:3068
#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