12 #ifndef CPROVER_GOTO_SYMEX_PARTIAL_ORDER_CONCURRENCY_H 13 #define CPROVER_GOTO_SYMEX_PARTIAL_ORDER_CONCURRENCY_H 66 return event->ssa_lhs.get_identifier();
86 const std::string &msg,
100 #include "abstract_event_structure.h" 109 typedef std::vector<evtt const*> ordered_evtst;
111 typedef ordered_evtst::const_iterator const_iterator;
112 typedef std::map<evtt const*, ordered_evtst::size_type> ordered_evts_mapt;
114 void add_event(
const evtt &evt)
117 ordered_evts.push_back(&evt);
118 if(!ordered_evts_map.insert(std::make_pair(&evt, offset)).second)
120 assert(ordered_evts.size()==ordered_evts_map.size());
122 if(evt.direction==evtt::D_SYNC ||
123 evt.direction==evtt::D_LWSYNC)
124 barriers.insert(barriers.end(), offset);
127 void add_events(const_iterator first, const_iterator last)
129 ordered_evts.reserve(ordered_evts.size()+last-first);
130 for( ; first!=last; ++first)
134 const_iterator begin()
const 136 return ordered_evts.begin();
139 const_iterator end()
const 141 return ordered_evts.end();
144 const_iterator find(
const evtt &evt)
const 146 ordered_evts_mapt::const_iterator entry=ordered_evts_map.find(&evt);
147 if(entry==ordered_evts_map.end())
150 return ordered_evts.begin()+entry->second;
153 std::list<const_iterator> barriers_after(
const evtt &evt)
const 155 const_iterator entry=find(evt);
157 return std::list<const_iterator>();
159 std::list<const_iterator> ret;
161 for(std::set<ordered_evtst::size_type>::const_iterator
162 lb=barriers.lower_bound(offset);
165 ret.push_back(ordered_evts.begin()+*lb);
170 std::list<const_iterator> barriers_before(
const evtt &evt)
const 172 const_iterator entry=find(evt);
174 return std::list<const_iterator>();
176 std::list<const_iterator> ret;
178 for(std::set<ordered_evtst::size_type>::const_iterator
180 ub!=barriers.end() && *ub<=offset;
182 ret.push_back(ordered_evts.begin()+*ub);
188 ordered_evtst ordered_evts;
189 ordered_evts_mapt ordered_evts_map;
190 std::set<ordered_evtst::size_type> barriers;
207 typedef std::map<evtt const*, std::map<evtt const*, exprt> > adj_matrixt;
208 typedef adj_matrixt adj_matricest[AC_N_AXIOMS];
209 typedef std::list<evtt const*> per_valuet;
210 typedef std::map<irep_idt, per_valuet> per_address_mapt;
211 typedef std::vector<numbered_evtst> numbered_per_thread_evtst;
219 void init(
const abstract_events_in_program_ordert &abstract_events_in_po);
220 void add_atomic_sections();
223 void add_program_order(adj_matricest &po);
224 void add_read_from(adj_matricest &rf);
225 void add_write_serialisation(adj_matricest &ws);
227 const adj_matricest &rf,
228 const adj_matricest &ws,
231 const adj_matricest &po,
232 const adj_matricest &rf,
233 const adj_matricest &fr);
241 # define S_PROP(t) ((t+1)<<1) 243 const acyclict check,
245 const unsigned step)
const;
247 const acyclict check,
250 const evtt::event_dirt other_dir)
const;
257 const std::string &po_name);
258 void add_atomic_sections(
const acyclict check);
259 void add_partial_order_constraint(
260 const acyclict check,
261 const std::string &po_name,
265 void add_partial_order_constraint(
266 const acyclict check,
267 const std::string &po_name,
269 const unsigned n1_step,
270 const evtt::event_dirt n1_o_d,
272 const unsigned n2_step,
273 const evtt::event_dirt n2_o_d,
276 const evtt* first_of(
const evtt &e1,
const evtt &e2)
const;
277 const numbered_evtst &get_thread(
const evtt &e)
const;
278 const numbered_per_thread_evtst &get_all_threads()
const 280 return per_thread_evt_no;
284 messaget &get_message() {
return message; }
285 std::map<std::string, unsigned> num_concurrency_constraints;
294 per_address_mapt reads_per_address, writes_per_address;
297 std::map<irep_idt, evtt> init_val;
300 const std::string prop_var;
304 numbered_per_thread_evtst per_thread_evt_no;
308 std::map<evtt const*, unsigned> barrier_id;
311 const std::string &prefix)
const;
312 std::vector<std::pair<symbol_exprt, symbol_exprt>>
313 atomic_section_bounds[AC_N_AXIOMS];
315 std::list<exprt> acyclic_constraints[AC_N_AXIOMS];
316 static std::string check_to_string(
const acyclict check);
319 typedef std::pair<evtt const*, std::pair<unsigned, evtt::event_dirt>>
321 typedef std::map<std::pair<evt_dir_pairt, evt_dir_pairt>,
323 pointwise_mapt edge_cache[AC_N_AXIOMS];
324 typedef std::map<evtt
const*,
325 std::list<std::pair<evtt const*, std::pair<exprt, std::string> > > >
327 edge_to_guardt edge_to_guard[AC_N_AXIOMS];
329 void add_sub_clock_rules();
331 typedef std::map<std::pair<irep_idt, irep_idt>,
symbol_exprt> clock_mapt;
332 clock_mapt clock_constraint_cache;
337 const std::string &po_name);
339 const acyclict check,
340 const std::string &po_name,
342 const unsigned n1_step,
343 const evtt::event_dirt n1_o_d,
345 const unsigned n2_step,
346 const evtt::event_dirt n2_o_d);
347 void build_partial_order_constraint(
348 const acyclict check,
349 const std::string &po_name,
351 const unsigned n1_step,
352 const evtt::event_dirt n1_o_d,
354 const unsigned n2_step,
355 const evtt::event_dirt n2_o_d,
359 std::string event_to_string(
const evtt &evt)
const;
361 const adj_matrixt &graph,
362 const std::string &edge_label,
367 #endif // CPROVER_GOTO_SYMEX_PARTIAL_ORDER_CONCURRENCY_H The type of an expression.
irep_idt address(event_it event) const
Generate Equation using Symbolic Execution.
const irep_idt & get_identifier() const
symbol_exprt clock(event_it e, axiomt axiom)
unsignedbv_typet size_type()
exprt before(event_it e1, event_it e2, unsigned axioms)
void build_clock_type(const symex_target_equationt &)
static irep_idt id(event_it event)
void build_event_lists(symex_target_equationt &)
static irep_idt rw_clock_id(event_it e, axiomt axiom=AX_PROPAGATION)
std::map< irep_idt, a_rect > address_mapt
void add_init_writes(symex_target_equationt &)
partial_order_concurrencyt(const namespacet &_ns)
std::list< SSA_stept > SSA_stepst
eventst::const_iterator event_it
Base class for all expressions.
virtual ~partial_order_concurrencyt()
std::map< event_it, unsigned > numberingt
void add_constraint(symex_target_equationt &equation, const exprt &cond, const std::string &msg, const symex_targett::sourcet &source) const
Expression to hold a symbol (variable)
std::vector< event_it > event_listt
symex_target_equationt::SSA_stepst eventst
Expression providing an SSA-renamed symbol of expressions.
symex_target_equationt::SSA_stept eventt