cprover
partial_order_concurrency.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Add constraints to equation encoding partial orders on events
4 
5 Author: Michael Tautschnig, michael.tautschnig@cs.ox.ac.uk
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_GOTO_SYMEX_PARTIAL_ORDER_CONCURRENCY_H
13 #define CPROVER_GOTO_SYMEX_PARTIAL_ORDER_CONCURRENCY_H
14 
15 #include <util/message.h>
16 
17 #include "symex_target_equation.h"
18 
23 {
24 public:
25  explicit partial_order_concurrencyt(const namespacet &_ns);
27 
28  typedef SSA_stept eventt;
30  typedef eventst::const_iterator event_it;
31 
32  // the name of a clock variable for a shared read/write
33  enum axiomt
34  {
39  };
40 
45  static irep_idt rw_clock_id(
46  event_it e,
47  axiomt axiom=AX_PROPAGATION);
48 
49 protected:
50  const namespacet &ns;
51 
52  typedef std::vector<event_it> event_listt;
53 
54  // lists of reads and writes per address
55  struct a_rect
56  {
58  };
59 
60  typedef std::map<irep_idt, a_rect> address_mapt;
62 
71 
77 
78  // a per-thread numbering of the events
79  typedef std::map<event_it, unsigned> numberingt;
81 
85  static inline irep_idt id(event_it event)
86  {
87  return event->ssa_lhs.get_identifier();
88  }
89 
93  irep_idt address(event_it event) const
94  {
95  return remove_level_2(event->ssa_lhs).get_identifier();
96  }
97 
99 
104  symbol_exprt clock(event_it e, axiomt axiom);
105 
107  void build_clock_type();
108 
114  void add_constraint(
115  symex_target_equationt &equation,
116  const exprt &cond,
117  const std::string &msg,
118  const symex_targett::sourcet &source) const;
119 
128  exprt before(event_it e1, event_it e2, unsigned axioms);
129  virtual exprt before(event_it e1, event_it e2)=0;
130 };
131 
132 #if 0
133 #include <list>
134 #include <map>
135 #include <vector>
136 #include <string>
137 
138 #include "abstract_event_structure.h"
139 
140 class memory_model_baset;
141 
142 class numbered_evtst
143 {
144  typedef abstract_eventt evtt;
145 
146 public:
147  typedef std::vector<evtt const*> ordered_evtst;
148  // NOLINTNEXTLINE(readability/identifiers)
149  typedef ordered_evtst::const_iterator const_iterator;
150  typedef std::map<evtt const*, ordered_evtst::size_type> ordered_evts_mapt;
151 
152  void add_event(const evtt &evt)
153  {
154  const ordered_evtst::size_type offset=ordered_evts.size();
155  ordered_evts.push_back(&evt);
156  if(!ordered_evts_map.insert(std::make_pair(&evt, offset)).second)
157  UNREACHABLE;
158  assert(ordered_evts.size()==ordered_evts_map.size());
159 
160  if(evt.direction==evtt::D_SYNC ||
161  evt.direction==evtt::D_LWSYNC)
162  barriers.insert(barriers.end(), offset);
163  }
164 
165  void add_events(const_iterator first, const_iterator last)
166  {
167  ordered_evts.reserve(ordered_evts.size()+last-first);
168  for( ; first!=last; ++first)
169  add_event(**first);
170  }
171 
172  const_iterator begin() const
173  {
174  return ordered_evts.begin();
175  }
176 
177  const_iterator end() const
178  {
179  return ordered_evts.end();
180  }
181 
182  const_iterator find(const evtt &evt) const
183  {
184  ordered_evts_mapt::const_iterator entry=ordered_evts_map.find(&evt);
185  if(entry==ordered_evts_map.end())
186  return end();
187 
188  return ordered_evts.begin()+entry->second;
189  }
190 
191  std::list<const_iterator> barriers_after(const evtt &evt) const
192  {
193  const_iterator entry=find(evt);
194  if(entry==end())
195  return std::list<const_iterator>();
196 
197  std::list<const_iterator> ret;
198  ordered_evtst::size_type offset=entry-begin();
199  for(std::set<ordered_evtst::size_type>::const_iterator
200  lb=barriers.lower_bound(offset);
201  lb!=barriers.end();
202  ++lb)
203  ret.push_back(ordered_evts.begin()+*lb);
204 
205  return ret;
206  }
207 
208  std::list<const_iterator> barriers_before(const evtt &evt) const
209  {
210  const_iterator entry=find(evt);
211  if(entry==end())
212  return std::list<const_iterator>();
213 
214  std::list<const_iterator> ret;
215  ordered_evtst::size_type offset=entry-begin();
216  for(std::set<ordered_evtst::size_type>::const_iterator
217  ub=barriers.begin();
218  ub!=barriers.end() && *ub<=offset;
219  ++ub)
220  ret.push_back(ordered_evts.begin()+*ub);
221 
222  return ret;
223  }
224 
225 private:
226  ordered_evtst ordered_evts;
227  ordered_evts_mapt ordered_evts_map;
228  std::set<ordered_evtst::size_type> barriers;
229 };
230 
232 {
233 public:
234  // the is-acyclic checks
235  enum acyclict
236  {
237  AC_UNIPROC=0,
238  AC_THINAIR=1,
239  AC_GHB=2,
240  AC_PPC_WS_FENCE=3,
241  AC_N_AXIOMS=4
242  };
243 
244  typedef abstract_eventt evtt;
245  typedef std::map<evtt const*, std::map<evtt const*, exprt> > adj_matrixt;
246  typedef adj_matrixt adj_matricest[AC_N_AXIOMS];
247  typedef std::list<evtt const*> per_valuet;
248  typedef std::map<irep_idt, per_valuet> per_address_mapt;
249  typedef std::vector<numbered_evtst> numbered_per_thread_evtst;
250 
252  memory_model_baset &_memory_model,
253  symex_target_equationt &_target,
254  const namespacet &_ns,
255  messaget &_message);
256 
257  void init(const abstract_events_in_program_ordert &abstract_events_in_po);
258  void add_atomic_sections();
259 
260  // collect all partial orders
261  void add_program_order(adj_matricest &po);
262  void add_read_from(adj_matricest &rf);
263  void add_write_serialisation(adj_matricest &ws);
264  void add_from_read(
265  const adj_matricest &rf,
266  const adj_matricest &ws,
267  adj_matricest &fr);
268  void add_barriers(
269  const adj_matricest &po,
270  const adj_matricest &rf,
271  const adj_matricest &fr);
272 
273  void acyclic();
274 
275  // steps as used in PLDI Power model
276 # define S_COMMIT 0
277 # define S_R_REQ 1
278 # define S_S_ACK 1
279 # define S_PROP(t) ((t+1)<<1)
281  const acyclict check,
282  const evtt &n,
283  const unsigned step) const;
285  const acyclict check,
286  const evtt &n,
287  const unsigned step,
288  const evtt::event_dirt other_dir) const;
289 
290  symbol_exprt fresh_nondet_bool();
291  void add_constraint(
292  exprt &expr,
293  const guardt &guard,
294  const symex_targett::sourcet &source,
295  const std::string &po_name);
296  void add_atomic_sections(const acyclict check);
297  void add_partial_order_constraint(
298  const acyclict check,
299  const std::string &po_name,
300  const evtt &n1,
301  const evtt &n2,
302  const exprt &cond);
303  void add_partial_order_constraint(
304  const acyclict check,
305  const std::string &po_name,
306  const evtt &n1,
307  const unsigned n1_step,
308  const evtt::event_dirt n1_o_d,
309  const evtt &n2,
310  const unsigned n2_step,
311  const evtt::event_dirt n2_o_d,
312  const exprt &cond);
313 
314  const evtt* first_of(const evtt &e1, const evtt &e2) const;
315  const numbered_evtst &get_thread(const evtt &e) const;
316  const numbered_per_thread_evtst &get_all_threads() const
317  {
318  return per_thread_evt_no;
319  }
320 
321  const namespacet &get_ns() const { return ns; }
322  messaget &get_message() { return message; }
323  std::map<std::string, unsigned> num_concurrency_constraints;
324 
325 private:
326  memory_model_baset &memory_model;
327  symex_target_equationt &target;
328  const namespacet &ns;
329  messaget &message;
330 
331  // collect all reads and writes to each address
332  per_address_mapt reads_per_address, writes_per_address;
333 
334  // initialisation events for uninitialised globals
335  std::map<irep_idt, evtt> init_val;
336 
337  // constraints added to the formula
338  const std::string prop_var;
339  unsigned prop_cnt;
340 
341  // number events according to po per thread, including parents
342  numbered_per_thread_evtst per_thread_evt_no;
343 
344  // map between events and (symbolic) integers
345  typet node_type;
346  std::map<evtt const*, unsigned> barrier_id;
347  symbol_exprt node_symbol(
348  const evtt &evt,
349  const std::string &prefix) const;
350  std::vector<std::pair<symbol_exprt, symbol_exprt>>
351  atomic_section_bounds[AC_N_AXIOMS];
352 
353  std::list<exprt> acyclic_constraints[AC_N_AXIOMS];
354  static std::string check_to_string(const acyclict check);
355 
356  // map point-wise order to a single Boolean symbol
357  typedef std::pair<evtt const*, std::pair<unsigned, evtt::event_dirt>>
358  evt_dir_pairt;
359  typedef std::map<std::pair<evt_dir_pairt, evt_dir_pairt>,
360  symbol_exprt> pointwise_mapt;
361  pointwise_mapt edge_cache[AC_N_AXIOMS];
362  typedef std::map<evtt const*,
363  std::list<std::pair<evtt const*, std::pair<exprt, std::string> > > >
364  edge_to_guardt;
365  edge_to_guardt edge_to_guard[AC_N_AXIOMS];
366 
367  void add_sub_clock_rules();
368 
369  typedef std::map<std::pair<irep_idt, irep_idt>, symbol_exprt> clock_mapt;
370  clock_mapt clock_constraint_cache;
371  symbol_exprt add_clock_constraint(
372  const symbol_exprt &n1_sym,
373  const symbol_exprt &n2_sym,
374  const symex_targett::sourcet &source,
375  const std::string &po_name);
376  const symbol_exprt &get_partial_order_constraint(
377  const acyclict check,
378  const std::string &po_name,
379  const evtt &n1,
380  const unsigned n1_step,
381  const evtt::event_dirt n1_o_d,
382  const evtt &n2,
383  const unsigned n2_step,
384  const evtt::event_dirt n2_o_d);
385  void build_partial_order_constraint(
386  const acyclict check,
387  const std::string &po_name,
388  const evtt &n1,
389  const unsigned n1_step,
390  const evtt::event_dirt n1_o_d,
391  const evtt &n2,
392  const unsigned n2_step,
393  const evtt::event_dirt n2_o_d,
394  symbol_exprt &dest);
395 
396  // debugging output
397  std::string event_to_string(const evtt &evt) const;
398  void print_graph(
399  const adj_matrixt &graph,
400  const std::string &edge_label,
401  namespacet const &ns) const;
402 };
403 #endif
404 
405 #endif // CPROVER_GOTO_SYMEX_PARTIAL_ORDER_CONCURRENCY_H
partial_order_concurrencyt::event_it
eventst::const_iterator event_it
Definition: partial_order_concurrency.h:30
messaget
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:155
guard_exprt
Definition: guard_expr.h:27
UNREACHABLE
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:504
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
symex_target_equation.h
Generate Equation using Symbolic Execution.
symex_target_equationt::SSA_stepst
std::list< SSA_stept > SSA_stepst
Definition: symex_target_equation.h:256
partial_order_concurrencyt::add_constraint
void add_constraint(symex_target_equationt &equation, const exprt &cond, const std::string &msg, const symex_targett::sourcet &source) const
Simplify and add a constraint to equation.
Definition: partial_order_concurrency.cpp:202
typet
The type of an expression, extends irept.
Definition: type.h:29
SSA_stept
Single SSA step in the equation.
Definition: ssa_step.h:45
partial_order_concurrencyt::a_rect
Definition: partial_order_concurrency.h:56
partial_order_concurrencyt::before
virtual exprt before(event_it e1, event_it e2)=0
partial_order_concurrencyt::axiomt
axiomt
Definition: partial_order_concurrency.h:34
partial_order_concurrencyt::add_init_writes
void add_init_writes(symex_target_equationt &)
For each shared read event and for each shared write event that appears after spawn or has false guar...
Definition: partial_order_concurrency.cpp:28
exprt
Base class for all expressions.
Definition: expr.h:53
partial_order_concurrencyt::id
static irep_idt id(event_it event)
Produce the symbol ID for an event.
Definition: partial_order_concurrency.h:85
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:82
partial_order_concurrencyt::build_clock_type
void build_clock_type()
Initialize the clock_type so that it can be used to number events.
Definition: partial_order_concurrency.cpp:160
partial_order_concurrencyt::rw_clock_id
static irep_idt rw_clock_id(event_it e, axiomt axiom=AX_PROPAGATION)
Build identifier for the read/write clock variable.
Definition: partial_order_concurrency.cpp:125
partial_order_concurrencyt::~partial_order_concurrencyt
virtual ~partial_order_concurrencyt()
Definition: partial_order_concurrency.cpp:24
partial_order_concurrencyt::ns
const namespacet & ns
Definition: partial_order_concurrency.h:50
partial_order_concurrencyt::AX_NO_THINAIR
@ AX_NO_THINAIR
Definition: partial_order_concurrency.h:36
partial_order_concurrencyt::before
exprt before(event_it e1, event_it e2, unsigned axioms)
Build the partial order constraint for two events: if e1 and e2 are in the same atomic section then c...
Definition: partial_order_concurrency.cpp:168
memory_model_baset
Definition: memory_model.h:18
partial_order_concurrencyt::a_rect::reads
event_listt reads
Definition: partial_order_concurrency.h:57
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
message
static const char * message(const static_verifier_resultt::statust &status)
Makes a status message string from a status.
Definition: static_verifier.cpp:74
partial_order_concurrencyt::AX_OBSERVATION
@ AX_OBSERVATION
Definition: partial_order_concurrency.h:37
partial_order_concurrencyt::build_event_lists
void build_event_lists(symex_target_equationt &)
First call add_init_writes then for each shared read/write (or spawn) populate: 1) the address_map (w...
Definition: partial_order_concurrency.cpp:75
partial_order_concurrencyt::address_map
address_mapt address_map
Definition: partial_order_concurrency.h:61
partial_order_concurrencyt::clock
symbol_exprt clock(event_it e, axiomt axiom)
Produce a clock symbol for some event.
Definition: partial_order_concurrency.cpp:137
symbol_exprt::get_identifier
const irep_idt & get_identifier() const
Definition: std_expr.h:111
partial_order_concurrencyt::numberingt
std::map< event_it, unsigned > numberingt
Definition: partial_order_concurrency.h:79
partial_order_concurrencyt::AX_PROPAGATION
@ AX_PROPAGATION
Definition: partial_order_concurrency.h:38
partial_order_concurrencyt::AX_SC_PER_LOCATION
@ AX_SC_PER_LOCATION
Definition: partial_order_concurrency.h:35
abstract_eventt
Definition: abstract_event.h:23
symex_target_equationt
Inheriting the interface of symex_targett this class represents the SSA form of the input program as ...
Definition: symex_target_equation.h:41
partial_order_concurrencyt::eventst
symex_target_equationt::SSA_stepst eventst
Definition: partial_order_concurrency.h:29
partial_order_concurrencyt::partial_order_concurrencyt
partial_order_concurrencyt(const namespacet &_ns)
Definition: partial_order_concurrency.cpp:19
remove_level_2
ssa_exprt remove_level_2(ssa_exprt ssa)
partial_order_concurrencyt::numbering
numberingt numbering
Definition: partial_order_concurrency.h:80
partial_order_concurrencyt::event_listt
std::vector< event_it > event_listt
Definition: partial_order_concurrency.h:52
partial_order_concurrencyt::a_rect::writes
event_listt writes
Definition: partial_order_concurrency.h:57
partial_order_concurrencyt::address_mapt
std::map< irep_idt, a_rect > address_mapt
Definition: partial_order_concurrency.h:60
symex_targett::sourcet
Identifies source in the context of symbolic execution.
Definition: symex_target.h:38
size_type
unsignedbv_typet size_type()
Definition: c_types.cpp:58
message.h
partial_order_concurrencyt
Base class for implementing memory models via additional constraints for SSA equations.
Definition: partial_order_concurrency.h:23
partial_order_concurrencyt::clock_type
typet clock_type
Definition: partial_order_concurrency.h:98
partial_order_concurrencyt::address
irep_idt address(event_it event) const
Produce an address ID for an event.
Definition: partial_order_concurrency.h:93
partial_order_concurrencyt::eventt
SSA_stept eventt
Definition: partial_order_concurrency.h:28