cprover
Loading...
Searching...
No Matches
shared_buffers.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
9
10#ifndef CPROVER_GOTO_INSTRUMENT_WMM_SHARED_BUFFERS_H
11#define CPROVER_GOTO_INSTRUMENT_WMM_SHARED_BUFFERS_H
12
13#include <util/cprover_prefix.h>
14#include <util/namespace.h>
15#include <util/prefix.h>
17
19
20#include "wmm.h"
21
22#include <map>
23#include <set>
24
25class goto_functionst;
26class messaget;
27class value_setst;
28
30{
31public:
43
45 {
46 if(model!=TSO)
47 throw "sorry, CAV11 only available for TSO";
48 cav11 = true;
49 }
50
51 /* instrumentation of a variable */
52 class varst
53 {
54 public:
55 // Older stuff has the higher index.
56 // Shared buffer.
58
59 // Are those places empty?
61
62 // Delays write buffer flush: just to make some swaps between mem and buff
63 // -- this is to model lhs := rhs with rhs reading in the buffer without
64 // affecting the memory (Note: we model lhs := rhs by rhs := ..., then
65 // lhs := rhs)
68
69 // Thread: Was it me who wrote at this place?
70 std::vector<irep_idt> r_buff0_thds, r_buff1_thds;
71
72 // for delayed read:
75
77 };
78
79 typedef std::map<irep_idt, varst> var_mapt;
81
82 /* instructions in violation cycles (to instrument): */
83 // variables in the cycles
84 std::set<irep_idt> cycles;
85 // events instrumented: var->locations in the code
86 std::multimap<irep_idt, source_locationt> cycles_loc;
87 // events in cycles: var->locations (for read instrumentations)
88 std::multimap<irep_idt, source_locationt> cycles_r_loc;
89
90 const varst &operator()(const irep_idt &object);
91
92 void add_initialization_code(goto_functionst &goto_functions);
93
94 void delay_read(
95 goto_programt &goto_program,
97 const source_locationt &source_location,
98 const irep_idt &read_object,
99 const irep_idt &write_object);
100
101 void flush_read(
102 goto_programt &goto_program,
104 const source_locationt &source_location,
105 const irep_idt &write_object);
106
107 void write(
108 goto_programt &goto_program,
110 const source_locationt &source_location,
111 const irep_idt &object,
113 const unsigned current_thread);
114
115 void det_flush(
116 goto_programt &goto_program,
118 const source_locationt &source_location,
119 const irep_idt &object,
120 const unsigned current_thread);
121
122 void nondet_flush(
123 const irep_idt &function_id,
124 goto_programt &goto_program,
126 const source_locationt &source_location,
127 const irep_idt &object,
128 const unsigned current_thread,
129 const bool tso_pso_rmo);
130
131 void assignment(
132 goto_programt &goto_program,
134 const source_locationt &source_location,
135 const irep_idt &id_lhs,
136 const exprt &rhs);
137
139 goto_programt &goto_program,
141 const source_locationt &source_location,
142 const irep_idt &id_lhs,
143 const irep_idt &id_rhs)
144 {
146 assignment(goto_program, t, source_location, id_lhs,
147 ns.lookup(id_rhs).symbol_expr());
148 }
149
150 bool track(const irep_idt &id) const
151 {
153
154 const symbolt &symbol=ns.lookup(id);
155 if(symbol.is_thread_local)
156 return false;
158 return false;
159
160 return true;
161 }
162
163 irep_idt choice(const irep_idt &function_id, const std::string &suffix)
164 {
165 const auto maybe_symbol = symbol_table.lookup(function_id);
167 return add(*maybe_symbol, "_weak_choice" + suffix, bool_typet());
168 }
169
170 bool is_buffered(
171 const namespacet&,
172 const symbol_exprt&,
173 bool is_write);
174
176 const symbol_exprt&,
177 bool is_write);
178
180 value_setst &value_sets,
182 goto_programt &goto_program,
183 memory_modelt model,
184 goto_functionst &goto_functions);
185
187 value_setst &value_sets,
188 goto_functionst &goto_functions);
189
191 {
192 protected:
196
197 /* for thread marking (dynamic) */
199 unsigned coming_from;
200 unsigned max_thread;
201
202 /* data propagated through the CFG */
203 std::set<irep_idt> past_writes;
204
205 public:
218
219 void weak_memory(
220 value_setst &value_sets,
221 const irep_idt &function_id,
222 memory_modelt model);
223 };
224
225protected:
227
228 // number of threads interfering
229 unsigned nb_threads;
230
231 // instrumentations (not to be instrumented again)
232 std::set<irep_idt> instrumentations;
233
234 // variables (non necessarily shared) affected by reads delay
235public:
236 std::set<irep_idt> affected_by_delay_set;
237
238protected:
239 // for fresh variables
240 unsigned uniq;
241
242 std::string unique();
243
244 bool cav11;
245
246 /* message */
248
250 const symbolt &object,
251 const std::string &suffix,
252 const typet &type,
254
256 add(const symbolt &object, const std::string &suffix, const typet &type)
257 {
258 return add(object, suffix, type, true);
259 }
260
261 /* inserting a non-instrumenting, fresh variable */
263 const symbolt &object,
264 const std::string &suffix,
265 const typet &type)
266 {
267 return add(object, suffix, type, false);
268 }
269
270 void add_initialization(goto_programt &goto_program);
271};
272
273#endif // CPROVER_GOTO_INSTRUMENT_WMM_SHARED_BUFFERS_H
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:563
The Boolean type.
Definition std_types.h:36
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:39
Base class for all expressions.
Definition expr.h:56
A collection of goto functions.
This class represents an instruction in the GOTO intermediate representation.
A generic container class for the GOTO intermediate representation of one function.
instructionst::iterator targett
Class that provides messages with a built-in verbosity 'level'.
Definition message.h:155
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
symbol_table_baset & symbol_table
void weak_memory(value_setst &value_sets, const irep_idt &function_id, memory_modelt model)
instruments the program for the pairs detected through the CFG
cfg_visitort(shared_bufferst &_shared, symbol_table_baset &_symbol_table, goto_functionst &_goto_functions)
std::set< irep_idt > past_writes
std::vector< irep_idt > r_buff0_thds
std::vector< irep_idt > r_buff1_thds
std::multimap< irep_idt, source_locationt > cycles_loc
const varst & operator()(const irep_idt &object)
instruments the variable
void set_cav11(memory_modelt model)
void nondet_flush(const irep_idt &function_id, goto_programt &goto_program, goto_programt::targett &t, const source_locationt &source_location, const irep_idt &object, const unsigned current_thread, const bool tso_pso_rmo)
instruments read
std::string unique()
returns a unique id (for fresh variables)
void write(goto_programt &goto_program, goto_programt::targett &t, const source_locationt &source_location, const irep_idt &object, goto_programt::instructiont &original_instruction, const unsigned current_thread)
instruments write
void weak_memory(value_setst &value_sets, symbol_table_baset &symbol_table, goto_programt &goto_program, memory_modelt model, goto_functionst &goto_functions)
void affected_by_delay(value_setst &value_sets, goto_functionst &goto_functions)
analysis over the goto-program which computes in affected_by_delay_set the variables (non necessarily...
shared_bufferst(symbol_table_baset &_symbol_table, unsigned _nb_threads, messaget &_message)
void det_flush(goto_programt &goto_program, goto_programt::targett &t, const source_locationt &source_location, const irep_idt &object, const unsigned current_thread)
flush buffers (instruments fence)
irep_idt add_fresh_var(const symbolt &object, const std::string &suffix, const typet &type)
void add_initialization(goto_programt &goto_program)
bool is_buffered_in_general(const symbol_exprt &, bool is_write)
void assignment(goto_programt &goto_program, goto_programt::targett &t, const source_locationt &source_location, const irep_idt &id_lhs, const exprt &rhs)
add an assignment in the goto-program
irep_idt add(const symbolt &object, const std::string &suffix, const typet &type, bool added_as_instrumentation)
add a new var for instrumenting the input var
std::set< irep_idt > affected_by_delay_set
class symbol_table_baset & symbol_table
std::set< irep_idt > cycles
void delay_read(goto_programt &goto_program, goto_programt::targett &t, const source_locationt &source_location, const irep_idt &read_object, const irep_idt &write_object)
delays a read (POWER)
void flush_read(goto_programt &goto_program, goto_programt::targett &t, const source_locationt &source_location, const irep_idt &write_object)
flushes read (POWER)
std::multimap< irep_idt, source_locationt > cycles_r_loc
std::map< irep_idt, varst > var_mapt
irep_idt choice(const irep_idt &function_id, const std::string &suffix)
void add_initialization_code(goto_functionst &goto_functions)
bool track(const irep_idt &id) const
irep_idt add(const symbolt &object, const std::string &suffix, const typet &type)
bool is_buffered(const namespacet &, const symbol_exprt &, bool is_write)
std::set< irep_idt > instrumentations
void assignment(goto_programt &goto_program, goto_programt::targett &t, const source_locationt &source_location, const irep_idt &id_lhs, const irep_idt &id_rhs)
Expression to hold a symbol (variable)
Definition std_expr.h:113
The symbol table base class interface.
Symbol table entry.
Definition symbol.h:28
bool is_thread_local
Definition symbol.h:71
The type of an expression, extends irept.
Definition type.h:29
bool has_prefix(const std::string &s, const std::string &prefix)
Definition converter.cpp:13
#define CPROVER_PREFIX
Concrete Goto Program.
const std::string & id2string(const irep_idt &d)
Definition irep.h:47
#define CHECK_RETURN(CONDITION)
Definition invariant.h:495
Author: Diffblue Ltd.
memory models
memory_modelt
Definition wmm.h:18
@ TSO
Definition wmm.h:20