cprover
partial_order_concurrency.cpp
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 
13 
14 #include <limits>
15 
16 #include <util/arith_tools.h>
17 #include <util/simplify_expr.h>
18 
20  const namespacet &_ns):ns(_ns)
21 {
22 }
23 
25 {
26 }
27 
29  symex_target_equationt &equation)
30 {
31  std::unordered_set<irep_idt> init_done;
32  bool spawn_seen=false;
33 
35 
36  for(eventst::const_iterator
37  e_it=equation.SSA_steps.begin();
38  e_it!=equation.SSA_steps.end();
39  e_it++)
40  {
41  if(e_it->is_spawn())
42  {
43  spawn_seen=true;
44  continue;
45  }
46  else if(!e_it->is_shared_read() &&
47  !e_it->is_shared_write())
48  continue;
49 
50  const irep_idt &a=address(e_it);
51 
52  if(init_done.find(a)!=init_done.end())
53  continue;
54 
55  if(spawn_seen ||
56  e_it->is_shared_read() ||
57  !e_it->guard.is_true())
58  {
59  init_steps.emplace_back(
61  SSA_stept &SSA_step = init_steps.back();
62 
63  SSA_step.guard=true_exprt();
64  // no SSA L2 index, thus nondet value
65  SSA_step.ssa_lhs = remove_level_2(e_it->ssa_lhs);
66  SSA_step.atomic_section_id=0;
67  }
68 
69  init_done.insert(a);
70  }
71 
72  equation.SSA_steps.splice(equation.SSA_steps.begin(), init_steps);
73 }
74 
76  symex_target_equationt &equation,
77  message_handlert &message_handler)
78 {
79  add_init_writes(equation);
80 
81  // a per-thread counter
82  std::map<unsigned, unsigned> counter;
83 
84  for(eventst::const_iterator
85  e_it=equation.SSA_steps.begin();
86  e_it!=equation.SSA_steps.end();
87  e_it++)
88  {
89  if(e_it->is_shared_read() ||
90  e_it->is_shared_write() ||
91  e_it->is_spawn())
92  {
93  unsigned thread_nr=e_it->source.thread_nr;
94 
95  if(!e_it->is_spawn())
96  {
97  a_rect &a_rec=address_map[address(e_it)];
98 
99  if(e_it->is_shared_read())
100  a_rec.reads.push_back(e_it);
101  else // must be write
102  a_rec.writes.push_back(e_it);
103  }
104 
105  // maps an event id to a per-thread counter
106  unsigned cnt=counter[thread_nr]++;
107  numbering[e_it]=cnt;
108  }
109  }
110 
111  messaget log{message_handler};
112  for(address_mapt::const_iterator
113  a_it=address_map.begin();
114  a_it!=address_map.end();
115  a_it++)
116  {
117  const a_rect &a_rec=a_it->second;
118  if(a_rec.reads.empty())
119  continue;
120 
121  log.statistics() << "Shared " << a_it->first << ": " << a_rec.reads.size()
122  << "R/" << a_rec.writes.size() << "W" << messaget::eom;
123  }
124 }
125 
127  event_it event,
128  axiomt axiom)
129 {
130  if(event->is_shared_write())
131  return id2string(id(event))+"$wclk$"+std::to_string(axiom);
132  else if(event->is_shared_read())
133  return id2string(id(event))+"$rclk$"+std::to_string(axiom);
134  else
135  UNREACHABLE;
136 }
137 
139  event_it event,
140  axiomt axiom)
141 {
142  PRECONDITION(!numbering.empty());
143  irep_idt identifier;
144 
145  if(event->is_shared_write())
146  identifier=rw_clock_id(event, axiom);
147  else if(event->is_shared_read())
148  identifier=rw_clock_id(event, axiom);
149  else if(event->is_spawn())
150  {
151  identifier=
152  "t"+std::to_string(event->source.thread_nr+1)+"$"+
153  std::to_string(numbering[event])+"$spwnclk$"+std::to_string(axiom);
154  }
155  else
156  UNREACHABLE;
157 
158  return symbol_exprt(identifier, clock_type);
159 }
160 
162 {
163  PRECONDITION(!numbering.empty());
164 
165  std::size_t width = address_bits(numbering.size());
166  clock_type = unsignedbv_typet(width);
167 }
168 
170  event_it e1, event_it e2, unsigned axioms)
171 {
172  const axiomt axiom_bits[]=
173  {
178  };
179 
180  exprt::operandst ops;
181  ops.reserve(sizeof(axiom_bits)/sizeof(axiomt));
182 
183  for(int i=0; i<int(sizeof(axiom_bits)/sizeof(axiomt)); ++i)
184  {
185  const axiomt ax=axiom_bits[i];
186 
187  if((axioms &ax)==0)
188  continue;
189 
190  if(e1->atomic_section_id!=0 &&
191  e1->atomic_section_id==e2->atomic_section_id)
192  ops.push_back(equal_exprt(clock(e1, ax), clock(e2, ax)));
193  else
194  ops.push_back(
195  binary_relation_exprt(clock(e1, ax), ID_lt, clock(e2, ax)));
196  }
197 
198  POSTCONDITION(!ops.empty());
199 
200  return conjunction(ops);
201 }
202 
204  symex_target_equationt &equation,
205  const exprt &cond,
206  const std::string &msg,
207  const symex_targett::sourcet &source) const
208 {
209  exprt tmp=cond;
210  simplify(tmp, ns);
211 
212  equation.constraint(tmp, msg, source);
213 }
std::size_t address_bits(const mp_integer &size)
ceil(log2(size))
Single SSA step in the equation.
Definition: ssa_step.h:45
unsigned atomic_section_id
Definition: ssa_step.h:169
exprt guard
Definition: ssa_step.h:137
ssa_exprt ssa_lhs
Definition: ssa_step.h:141
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition: std_expr.h:675
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
Equality.
Definition: std_expr.h:1140
Base class for all expressions.
Definition: expr.h:54
std::vector< exprt > operandst
Definition: expr.h:56
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:155
static eomt eom
Definition: message.h:297
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
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...
void build_event_lists(symex_target_equationt &equation, message_handlert &message_handler)
First call add_init_writes then for each shared read/write (or spawn) populate: 1) the address_map (w...
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...
irep_idt address(event_it event) const
Produce an address ID for an event.
symbol_exprt clock(event_it e, axiomt axiom)
Produce a clock symbol for some event.
void build_clock_type()
Initialize the clock_type so that it can be used to number events.
static irep_idt rw_clock_id(event_it e, axiomt axiom=AX_PROPAGATION)
Build identifier for the read/write clock variable.
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.
partial_order_concurrencyt(const namespacet &_ns)
eventst::const_iterator event_it
Expression to hold a symbol (variable)
Definition: std_expr.h:81
Inheriting the interface of symex_targett this class represents the SSA form of the input program as ...
virtual void constraint(const exprt &cond, const std::string &msg, const sourcet &source)
Record a global constraint: there is no guard limiting its scope.
std::list< SSA_stept > SSA_stepst
The Boolean constant true.
Definition: std_expr.h:2717
Fixed-width bit-vector with unsigned binary interpretation.
Definition: std_types.h:1223
const std::string & id2string(const irep_idt &d)
Definition: irep.h:49
Add constraints to equation encoding partial orders on events.
bool simplify(exprt &expr, const namespacet &ns)
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:504
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
#define POSTCONDITION(CONDITION)
Definition: invariant.h:480
ssa_exprt remove_level_2(ssa_exprt ssa)
exprt conjunction(const exprt::operandst &op)
1) generates a conjunction for two or more operands 2) for one operand, returns the operand 3) return...
Definition: std_expr.cpp:41
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
Identifies source in the context of symbolic execution.
Definition: symex_target.h:38