cprover
shared_buffers.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: 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 <map>
14 #include <set>
15 
17 #include <util/namespace.h>
18 #include <util/cprover_prefix.h>
19 #include <util/prefix.h>
20 #include <util/message.h>
21 
22 #include "wmm.h"
23 
24 class symbol_tablet;
25 class goto_functionst;
26 class value_setst;
27 
29 {
30 public:
31  shared_bufferst(symbol_tablet &_symbol_table, unsigned _nb_threads,
32  messaget &_message):
33  symbol_table(_symbol_table),
34  nb_threads(_nb_threads+1),
35  uniq(0),
36  cav11(false),
37  message(_message)
38  {
39  }
40 
42  {
43  if(model!=TSO)
44  throw "sorry, CAV11 only available for TSO";
45  cav11 = true;
46  }
47 
48  /* instrumentation of a variable */
49  class varst
50  {
51  public:
52  // Older stuff has the higher index.
53  // Shared buffer.
55 
56  // Are those places empty?
58 
59  // Delays write buffer flush: just to make some swaps between mem and buff
60  // -- this is to model lhs := rhs with rhs reading in the buffer without
61  // affecting the memory (Note: we model lhs := rhs by rhs := ..., then
62  // lhs := rhs)
65 
66  // Thread: Was it me who wrote at this place?
67  std::vector<irep_idt> r_buff0_thds, r_buff1_thds;
68 
69  // for delayed read:
72 
74  };
75 
76  typedef std::map<irep_idt, varst> var_mapt;
78 
79  /* instructions in violation cycles (to instrument): */
80  // variables in the cycles
81  std::set<irep_idt> cycles;
82  // events instrumented: var->locations in the code
83  std::multimap<irep_idt, source_locationt> cycles_loc;
84  // events in cycles: var->locations (for read instrumentations)
85  std::multimap<irep_idt, source_locationt> cycles_r_loc;
86 
87  const varst &operator()(const irep_idt &object);
88 
89  void add_initialization_code(goto_functionst &goto_functions);
90 
91  void delay_read(
92  goto_programt &goto_program,
94  const source_locationt &source_location,
95  const irep_idt &read_object,
96  const irep_idt &write_object);
97 
98  void flush_read(
99  goto_programt &goto_program,
101  const source_locationt &source_location,
102  const irep_idt &write_object);
103 
104  void write(
105  goto_programt &goto_program,
107  const source_locationt &source_location,
108  const irep_idt &object,
109  goto_programt::instructiont &original_instruction,
110  const unsigned current_thread);
111 
112  void det_flush(
113  goto_programt &goto_program,
115  const source_locationt &source_location,
116  const irep_idt &object,
117  const unsigned current_thread);
118 
119  void nondet_flush(
120  const irep_idt &function_id,
121  goto_programt &goto_program,
123  const source_locationt &source_location,
124  const irep_idt &object,
125  const unsigned current_thread,
126  const bool tso_pso_rmo);
127 
128  void assignment(
129  goto_programt &goto_program,
131  const source_locationt &source_location,
132  const irep_idt &id_lhs,
133  const exprt &rhs);
134 
136  goto_programt &goto_program,
138  const source_locationt &source_location,
139  const irep_idt &id_lhs,
140  const irep_idt &id_rhs)
141  {
143  assignment(goto_program, t, source_location, id_lhs,
144  ns.lookup(id_rhs).symbol_expr());
145  }
146 
147  bool track(const irep_idt &id) const
148  {
150 
151  const symbolt &symbol=ns.lookup(id);
152  if(symbol.is_thread_local)
153  return false;
155  return false;
156 
157  return true;
158  }
159 
160  irep_idt choice(const irep_idt &function_id, const std::string &suffix)
161  {
162  const auto maybe_symbol = symbol_table.lookup(function_id);
163  const std::string function_base_name =
164  maybe_symbol
165  ? id2string(maybe_symbol->base_name)
166  : "main";
167  return add(function_base_name+"_weak_choice",
168  function_base_name+"_weak_choice", suffix, bool_typet());
169  }
170 
171  bool is_buffered(
172  const namespacet&,
173  const symbol_exprt&,
174  bool is_write);
175 
177  const symbol_exprt&,
178  bool is_write);
179 
181  value_setst &value_sets,
183  goto_programt &goto_program,
184  memory_modelt model,
185  goto_functionst &goto_functions);
186 
187  void affected_by_delay(
188  value_setst &value_sets,
189  goto_functionst &goto_functions);
190 
192  {
193  protected:
197 
198  /* for thread marking (dynamic) */
199  unsigned current_thread;
200  unsigned coming_from;
201  unsigned max_thread;
202 
203  /* data propagated through the CFG */
204  std::set<irep_idt> past_writes;
205 
206  public:
207  cfg_visitort(shared_bufferst &_shared, symbol_tablet &_symbol_table,
208  goto_functionst &_goto_functions)
209  :shared_buffers(_shared), symbol_table(_symbol_table),
210  goto_functions(_goto_functions)
211  {
212  current_thread = 0;
213  coming_from = 0;
214  max_thread = 0;
215  }
216 
217  void weak_memory(
218  value_setst &value_sets,
219  const irep_idt &function_id,
220  memory_modelt model);
221  };
222 
223 protected:
225 
226  // number of threads interfering
227  unsigned nb_threads;
228 
229  // instrumentations (not to be instrumented again)
230  std::set<irep_idt> instrumentations;
231 
232  // variables (non necessarily shared) affected by reads delay
233 public:
234  std::set<irep_idt> affected_by_delay_set;
235 
236 protected:
237  // for fresh variables
238  unsigned uniq;
239 
240  std::string unique();
241 
242  bool cav11;
243 
244  /* message */
246 
247  irep_idt add(
248  const irep_idt &object,
249  const irep_idt &base_name,
250  const std::string &suffix,
251  const typet &type,
252  bool added_as_instrumentation);
253 
255  const irep_idt &object,
256  const irep_idt &base_name,
257  const std::string &suffix,
258  const typet &type)
259  {
260  return add(object, base_name, suffix, type, true);
261  }
262 
263  /* inserting a non-instrumenting, fresh variable */
265  const irep_idt &object,
266  const irep_idt &base_name,
267  const std::string &suffix,
268  const typet &type)
269  {
270  return add(object, base_name, suffix, type, false);
271  }
272 
273  void add_initialization(goto_programt &goto_program);
274 };
275 
276 #endif // CPROVER_GOTO_INSTRUMENT_WMM_SHARED_BUFFERS_H
messaget
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:155
shared_bufferst::write
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
Definition: shared_buffers.cpp:282
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
shared_bufferst::cfg_visitort::symbol_table
symbol_tablet & symbol_table
Definition: shared_buffers.h:195
TSO
@ TSO
Definition: wmm.h:20
symbol_tablet
The symbol table.
Definition: symbol_table.h:20
shared_bufferst::det_flush
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)
Definition: shared_buffers.cpp:341
shared_bufferst::varst::w_buff1_used
irep_idt w_buff1_used
Definition: shared_buffers.h:57
shared_bufferst::set_cav11
void set_cav11(memory_modelt model)
Definition: shared_buffers.h:41
shared_bufferst::is_buffered_in_general
bool is_buffered_in_general(const symbol_exprt &, bool is_write)
Definition: shared_buffers.cpp:980
shared_bufferst
Definition: shared_buffers.h:29
typet
The type of an expression, extends irept.
Definition: type.h:29
shared_bufferst::varst::read_delayed
irep_idt read_delayed
Definition: shared_buffers.h:70
shared_bufferst::varst::r_buff0_thds
std::vector< irep_idt > r_buff0_thds
Definition: shared_buffers.h:67
shared_bufferst::cycles_r_loc
std::multimap< irep_idt, source_locationt > cycles_r_loc
Definition: shared_buffers.h:85
shared_bufferst::cfg_visitort::goto_functions
goto_functionst & goto_functions
Definition: shared_buffers.h:196
prefix.h
shared_bufferst::symbol_table
class symbol_tablet & symbol_table
Definition: shared_buffers.h:224
shared_bufferst::weak_memory
void weak_memory(value_setst &value_sets, symbol_tablet &symbol_table, goto_programt &goto_program, memory_modelt model, goto_functionst &goto_functions)
shared_bufferst::assignment
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)
Definition: shared_buffers.h:135
exprt
Base class for all expressions.
Definition: expr.h:53
shared_bufferst::cfg_visitort::max_thread
unsigned max_thread
Definition: shared_buffers.h:201
bool_typet
The Boolean type.
Definition: std_types.h:37
shared_bufferst::cycles_loc
std::multimap< irep_idt, source_locationt > cycles_loc
Definition: shared_buffers.h:83
shared_bufferst::add
irep_idt add(const irep_idt &object, const irep_idt &base_name, const std::string &suffix, const typet &type, bool added_as_instrumentation)
add a new var for instrumenting the input var
Definition: shared_buffers.cpp:85
shared_bufferst::add_initialization_code
void add_initialization_code(goto_functionst &goto_functions)
Definition: shared_buffers.cpp:139
shared_bufferst::cfg_visitort::current_thread
unsigned current_thread
Definition: shared_buffers.h:199
shared_bufferst::add_fresh_var
irep_idt add_fresh_var(const irep_idt &object, const irep_idt &base_name, const std::string &suffix, const typet &type)
Definition: shared_buffers.h:264
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:82
namespace.h
shared_bufferst::assignment
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
Definition: shared_buffers.cpp:154
shared_bufferst::varst::flush_delayed
irep_idt flush_delayed
Definition: shared_buffers.h:64
shared_bufferst::choice
irep_idt choice(const irep_idt &function_id, const std::string &suffix)
Definition: shared_buffers.h:160
shared_bufferst::var_map
var_mapt var_map
Definition: shared_buffers.h:77
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
shared_bufferst::is_buffered
bool is_buffered(const namespacet &, const symbol_exprt &, bool is_write)
Definition: shared_buffers.cpp:946
symbolt::is_thread_local
bool is_thread_local
Definition: symbol.h:65
namespacet::lookup
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:140
shared_bufferst::message
messaget & message
Definition: shared_buffers.h:245
shared_bufferst::shared_bufferst
shared_bufferst(symbol_tablet &_symbol_table, unsigned _nb_threads, messaget &_message)
Definition: shared_buffers.h:31
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
shared_bufferst::varst::w_buff1
irep_idt w_buff1
Definition: shared_buffers.h:54
shared_bufferst::cav11
bool cav11
Definition: shared_buffers.h:242
shared_bufferst::varst::w_buff0_used
irep_idt w_buff0_used
Definition: shared_buffers.h:57
shared_bufferst::affected_by_delay_set
std::set< irep_idt > affected_by_delay_set
Definition: shared_buffers.h:234
shared_bufferst::cfg_visitort::weak_memory
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
Definition: shared_buffers.cpp:1061
shared_bufferst::unique
std::string unique()
returns a unique id (for fresh variables)
Definition: shared_buffers.cpp:21
shared_bufferst::cycles
std::set< irep_idt > cycles
Definition: shared_buffers.h:81
shared_bufferst::add
irep_idt add(const irep_idt &object, const irep_idt &base_name, const std::string &suffix, const typet &type)
Definition: shared_buffers.h:254
shared_bufferst::cfg_visitort::cfg_visitort
cfg_visitort(shared_bufferst &_shared, symbol_tablet &_symbol_table, goto_functionst &_goto_functions)
Definition: shared_buffers.h:207
cprover_prefix.h
shared_bufferst::cfg_visitort::past_writes
std::set< irep_idt > past_writes
Definition: shared_buffers.h:204
memory_modelt
memory_modelt
Definition: wmm.h:18
shared_bufferst::delay_read
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)
Definition: shared_buffers.cpp:193
goto_program.h
Concrete Goto Program.
source_locationt
Definition: source_location.h:20
shared_bufferst::cfg_visitort::shared_buffers
shared_bufferst & shared_buffers
Definition: shared_buffers.h:194
shared_bufferst::nondet_flush
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
Definition: shared_buffers.cpp:447
shared_bufferst::var_mapt
std::map< irep_idt, varst > var_mapt
Definition: shared_buffers.h:76
shared_bufferst::instrumentations
std::set< irep_idt > instrumentations
Definition: shared_buffers.h:230
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:23
value_setst
Definition: value_sets.h:22
shared_bufferst::cfg_visitort::coming_from
unsigned coming_from
Definition: shared_buffers.h:200
shared_bufferst::varst::type
typet type
Definition: shared_buffers.h:73
symbolt
Symbol table entry.
Definition: symbol.h:28
CPROVER_PREFIX
#define CPROVER_PREFIX
Definition: cprover_prefix.h:14
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
shared_bufferst::varst::w_buff0
irep_idt w_buff0
Definition: shared_buffers.h:54
shared_bufferst::varst::r_buff1_thds
std::vector< irep_idt > r_buff1_thds
Definition: shared_buffers.h:67
symbol_table_baset::lookup
const symbolt * lookup(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
Definition: symbol_table_base.h:95
has_prefix
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
shared_bufferst::flush_read
void flush_read(goto_programt &goto_program, goto_programt::targett &t, const source_locationt &source_location, const irep_idt &write_object)
flushes read (POWER)
Definition: shared_buffers.cpp:242
shared_bufferst::track
bool track(const irep_idt &id) const
Definition: shared_buffers.h:147
shared_bufferst::operator()
const varst & operator()(const irep_idt &object)
instruments the variable
Definition: shared_buffers.cpp:28
shared_bufferst::cfg_visitort
Definition: shared_buffers.h:192
wmm.h
memory models
message.h
shared_bufferst::uniq
unsigned uniq
Definition: shared_buffers.h:238
shared_bufferst::varst::read_delayed_var
irep_idt read_delayed_var
Definition: shared_buffers.h:71
shared_bufferst::varst::mem_tmp
irep_idt mem_tmp
Definition: shared_buffers.h:63
goto_programt::instructiont
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:179
shared_bufferst::varst
Definition: shared_buffers.h:50
shared_bufferst::nb_threads
unsigned nb_threads
Definition: shared_buffers.h:227
shared_bufferst::affected_by_delay
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...
Definition: shared_buffers.cpp:1022
goto_programt::targett
instructionst::iterator targett
Definition: goto_program.h:579
shared_bufferst::add_initialization
void add_initialization(goto_programt &goto_program)
Definition: shared_buffers.cpp:110