cprover
memory_model.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Memory model for partial order concurrency
4 
5 Author: Michael Tautschnig, michael.tautschnig@cs.ox.ac.uk
6 
7 \*******************************************************************/
8 
11 
12 #include "memory_model.h"
13 
14 #include <util/std_expr.h>
15 
18  var_cnt(0)
19 {
20 }
21 
23 {
24 }
25 
27  const std::string &prefix)
28 {
29  return symbol_exprt(
30  "memory_model::choice_"+prefix+std::to_string(var_cnt++),
31  bool_typet());
32 }
33 
35 {
36  // within same thread
37  if(e1->source.thread_nr==e2->source.thread_nr)
38  return numbering[e1]<numbering[e2];
39  else
40  {
41  // in general un-ordered, with exception of thread-spawning
42  return false;
43  }
44 }
45 
47 {
48  // We iterate over all the reads, and
49  // make them match at least one
50  // (internal or external) write.
51 
52  for(address_mapt::const_iterator
53  a_it=address_map.begin();
54  a_it!=address_map.end();
55  a_it++)
56  {
57  const a_rect &a_rec=a_it->second;
58 
59  for(event_listt::const_iterator
60  r_it=a_rec.reads.begin();
61  r_it!=a_rec.reads.end();
62  r_it++)
63  {
64  const event_it r=*r_it;
65 
66  exprt::operandst rf_some_operands;
67  rf_some_operands.reserve(a_rec.writes.size());
68 
69  // this is quadratic in #events per address
70  for(event_listt::const_iterator
71  w_it=a_rec.writes.begin();
72  w_it!=a_rec.writes.end();
73  ++w_it)
74  {
75  const event_it w=*w_it;
76 
77  // rf cannot contradict program order
78  if(po(r, w))
79  continue; // contradicts po
80 
81  bool is_rfi=
82  w->source.thread_nr==r->source.thread_nr;
83 
85 
86  // record the symbol
88  std::make_pair(r, w)]=s;
89 
90  // We rely on the fact that there is at least
91  // one write event that has guard 'true'.
93  and_exprt(w->guard,
94  equal_exprt(r->ssa_lhs, w->ssa_lhs)));
95 
96  // Uses only the write's guard as precondition, read's guard
97  // follows from rf_some
98  add_constraint(equation,
99  read_from, is_rfi?"rfi":"rf", r->source);
100 
101  if(!is_rfi)
102  {
103  // if r reads from w, then w must have happened before r
104  const implies_exprt cond(s, before(w, r));
105  add_constraint(equation,
106  cond, "rf-order", r->source);
107  }
108 
109  rf_some_operands.push_back(s);
110  }
111 
112  // value equals the one of some write
113  exprt rf_some;
114 
115  // uninitialised global symbol like symex_dynamic::dynamic_object*
116  // or *$object
117  if(rf_some_operands.empty())
118  continue;
119  else if(rf_some_operands.size()==1)
120  rf_some=rf_some_operands.front();
121  else
122  {
123  rf_some=or_exprt();
124  rf_some.operands().swap(rf_some_operands);
125  }
126 
127  // Add the read's guard, each of the writes' guards is implied
128  // by each entry in rf_some
129  add_constraint(equation,
130  implies_exprt(r->guard, rf_some), "rf-some", r->source);
131  }
132  }
133 }
partial_order_concurrencyt::event_it
eventst::const_iterator event_it
Definition: partial_order_concurrency.h:27
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
Definition: partial_order_concurrency.cpp:206
partial_order_concurrencyt::a_rect
Definition: partial_order_concurrency.h:48
template_numberingt
Definition: numbering.h:21
and_exprt
Boolean AND.
Definition: std_expr.h:2409
exprt
Base class for all expressions.
Definition: expr.h:54
memory_model_baset::read_from
void read_from(symex_target_equationt &equation)
Definition: memory_model.cpp:46
bool_typet
The Boolean type.
Definition: std_types.h:28
to_string
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
Definition: string_constraint.cpp:53
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:143
memory_model_baset::var_cnt
unsigned var_cnt
Definition: memory_model.h:30
equal_exprt
Equality.
Definition: std_expr.h:1484
partial_order_concurrencyt::before
exprt before(event_it e1, event_it e2, unsigned axioms)
Definition: partial_order_concurrency.cpp:172
partial_order_concurrencyt::a_rect::reads
event_listt reads
Definition: partial_order_concurrency.h:50
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
or_exprt
Boolean OR.
Definition: std_expr.h:2531
memory_model_baset::memory_model_baset
memory_model_baset(const namespacet &_ns)
Definition: memory_model.cpp:16
partial_order_concurrencyt::address_map
address_mapt address_map
Definition: partial_order_concurrency.h:54
memory_model_baset::po
bool po(event_it e1, event_it e2)
Definition: memory_model.cpp:34
exprt::operandst
std::vector< exprt > operandst
Definition: expr.h:57
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:35
memory_model_baset::choice_symbols
choice_symbolst choice_symbols
Definition: memory_model.h:37
memory_model_baset::nondet_bool_symbol
symbol_exprt nondet_bool_symbol(const std::string &prefix)
Definition: memory_model.cpp:26
memory_model_baset::~memory_model_baset
virtual ~memory_model_baset()
Definition: memory_model.cpp:22
partial_order_concurrencyt::a_rect::writes
event_listt writes
Definition: partial_order_concurrency.h:50
implies_exprt
Boolean implication.
Definition: std_expr.h:2485
exprt::operands
operandst & operands()
Definition: expr.h:78
r
static int8_t r
Definition: irep_hash.h:59
memory_model.h
std_expr.h
partial_order_concurrencyt
Definition: partial_order_concurrency.h:19