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.push_back(symex_target_equationt::SSA_stept());
60  symex_target_equationt::SSA_stept &SSA_step=init_steps.back();
61 
62  SSA_step.guard=true_exprt();
63  // no SSA L2 index, thus nondet value
64  SSA_step.ssa_lhs=e_it->ssa_lhs;
65  SSA_step.ssa_lhs.remove_level_2();
67  SSA_step.atomic_section_id=0;
68  SSA_step.source=e_it->source;
69  }
70 
71  init_done.insert(a);
72  }
73 
74  equation.SSA_steps.splice(equation.SSA_steps.begin(), init_steps);
75 }
76 
78  symex_target_equationt &equation)
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  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  statistics() << "Shared " << a_it->first << ": "
122  << a_rec.reads.size() << "R/"
123  << a_rec.writes.size() << "W" << 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  return "";
139 }
140 
142  event_it event,
143  axiomt axiom)
144 {
145  PRECONDITION(!numbering.empty());
146  irep_idt identifier;
147 
148  if(event->is_shared_write())
149  identifier=rw_clock_id(event, axiom);
150  else if(event->is_shared_read())
151  identifier=rw_clock_id(event, axiom);
152  else if(event->is_spawn())
153  {
154  identifier=
155  "t"+std::to_string(event->source.thread_nr+1)+"$"+
156  std::to_string(numbering[event])+"$spwnclk$"+std::to_string(axiom);
157  }
158  else
159  UNREACHABLE;
160 
161  return symbol_exprt(identifier, clock_type);
162 }
163 
165 {
166  PRECONDITION(!numbering.empty());
167 
168  std::size_t width = address_bits(numbering.size());
169  clock_type = unsignedbv_typet(width);
170 }
171 
173  event_it e1, event_it e2, unsigned axioms)
174 {
175  const axiomt axiom_bits[]=
176  {
181  };
182 
183  exprt::operandst ops;
184  ops.reserve(sizeof(axiom_bits)/sizeof(axiomt));
185 
186  for(int i=0; i<int(sizeof(axiom_bits)/sizeof(axiomt)); ++i)
187  {
188  const axiomt ax=axiom_bits[i];
189 
190  if((axioms &ax)==0)
191  continue;
192 
193  if(e1->atomic_section_id!=0 &&
194  e1->atomic_section_id==e2->atomic_section_id)
195  ops.push_back(equal_exprt(clock(e1, ax), clock(e2, ax)));
196  else
197  ops.push_back(
198  binary_relation_exprt(clock(e1, ax), ID_lt, clock(e2, ax)));
199  }
200 
201  POSTCONDITION(!ops.empty());
202 
203  return conjunction(ops);
204 }
205 
207  symex_target_equationt &equation,
208  const exprt &cond,
209  const std::string &msg,
210  const symex_targett::sourcet &source) const
211 {
212  exprt tmp=cond;
213  simplify(tmp, ns);
214 
215  equation.constraint(tmp, msg, source);
216 }
partial_order_concurrencyt::event_it
eventst::const_iterator event_it
Definition: partial_order_concurrency.h:27
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:438
symex_target_equationt::SSA_stept::guard
exprt guard
Definition: symex_target_equation.h:285
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:50
arith_tools.h
ssa_exprt::remove_level_2
void remove_level_2()
Definition: ssa_expr.h:101
symex_target_equationt::SSA_stepst
std::list< SSA_stept > SSA_stepst
Definition: symex_target_equation.h:368
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
partial_order_concurrencyt::axiomt
axiomt
Definition: partial_order_concurrency.h:30
template_numberingt
Definition: numbering.h:21
symex_target_equationt::SSA_stept::type
goto_trace_stept::typet type
Definition: symex_target_equation.h:247
symex_target_equationt::SSA_stept
Single SSA step in the equation.
Definition: symex_target_equation.h:243
partial_order_concurrencyt::add_init_writes
void add_init_writes(symex_target_equationt &)
Definition: partial_order_concurrency.cpp:28
exprt
Base class for all expressions.
Definition: expr.h:54
template_numberingt::size
size_type size() const
Definition: numbering.h:66
to_string
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
Definition: string_constraint.cpp:53
messaget::eom
static eomt eom
Definition: message.h:284
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:143
partial_order_concurrencyt::build_clock_type
void build_clock_type()
Definition: partial_order_concurrency.cpp:164
equal_exprt
Equality.
Definition: std_expr.h:1484
partial_order_concurrencyt::rw_clock_id
static irep_idt rw_clock_id(event_it e, axiomt axiom=AX_PROPAGATION)
Definition: partial_order_concurrency.cpp:127
partial_order_concurrencyt::~partial_order_concurrencyt
virtual ~partial_order_concurrencyt()
Definition: partial_order_concurrency.cpp:24
UNREACHABLE
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:478
unsignedbv_typet
Fixed-width bit-vector with unsigned binary interpretation.
Definition: std_types.h:1223
partial_order_concurrencyt::ns
const namespacet & ns
Definition: partial_order_concurrency.h:43
partial_order_concurrencyt::AX_NO_THINAIR
@ AX_NO_THINAIR
Definition: partial_order_concurrency.h:33
symex_target_equationt::SSA_stept::source
sourcet source
Definition: symex_target_equation.h:246
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
address_bits
std::size_t address_bits(const mp_integer &size)
ceil(log2(size))
Definition: arith_tools.cpp:200
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
partial_order_concurrencyt::AX_OBSERVATION
@ AX_OBSERVATION
Definition: partial_order_concurrency.h:34
partial_order_concurrencyt::build_event_lists
void build_event_lists(symex_target_equationt &)
Definition: partial_order_concurrency.cpp:77
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
partial_order_concurrencyt::address_map
address_mapt address_map
Definition: partial_order_concurrency.h:54
partial_order_concurrencyt::clock
symbol_exprt clock(event_it e, axiomt axiom)
Definition: partial_order_concurrency.cpp:141
simplify
bool simplify(exprt &expr, const namespacet &ns)
Definition: simplify_expr.cpp:2320
POSTCONDITION
#define POSTCONDITION(CONDITION)
Definition: invariant.h:454
exprt::operandst
std::vector< exprt > operandst
Definition: expr.h:57
partial_order_concurrencyt::AX_PROPAGATION
@ AX_PROPAGATION
Definition: partial_order_concurrency.h:35
partial_order_concurrencyt::AX_SC_PER_LOCATION
@ AX_SC_PER_LOCATION
Definition: partial_order_concurrency.h:32
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
simplify_expr.h
goto_trace_stept::typet::SHARED_WRITE
@ SHARED_WRITE
partial_order_concurrencyt::partial_order_concurrencyt
partial_order_concurrencyt(const namespacet &_ns)
Definition: partial_order_concurrency.cpp:19
symex_target_equationt::SSA_steps
SSA_stepst SSA_steps
Definition: symex_target_equation.h:369
binary_relation_exprt
A base class for relations, i.e., binary predicates.
Definition: std_expr.h:878
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:348
partial_order_concurrencyt::a_rect::writes
event_listt writes
Definition: partial_order_concurrency.h:50
symex_target_equationt::SSA_stept::atomic_section_id
unsigned atomic_section_id
Definition: symex_target_equation.h:313
symex_targett::sourcet
Identifies source in the context of symbolic execution.
Definition: symex_target.h:35
partial_order_concurrency.h
symex_target_equationt::SSA_stept::ssa_lhs
ssa_exprt ssa_lhs
Definition: symex_target_equation.h:289
true_exprt
The Boolean constant true.
Definition: std_expr.h:4443
partial_order_concurrencyt::clock_type
typet clock_type
Definition: partial_order_concurrency.h:78
messaget::statistics
mstreamt & statistics() const
Definition: message.h:406
partial_order_concurrencyt::address
irep_idt address(event_it event) const
Definition: partial_order_concurrency.h:70