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