CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
symex_atomic_section.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Symbolic Execution
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
11
12#include "goto_symex.h"
13
15
17{
18 if(!state.reachable)
19 return;
20
21 if(state.atomic_section_id != 0)
23 "we don't support nesting of atomic sections",
24 state.source.pc->source_location());
25
27 state.read_in_atomic_section.clear();
28 state.written_in_atomic_section.clear();
29
31 state.guard.as_expr(),
33 state.source);
34}
35
37{
38 if(!state.reachable)
39 return;
40
41 if(state.atomic_section_id == 0)
43 "ATOMIC_END unmatched", state.source.pc->source_location());
44
45 const unsigned atomic_section_id=state.atomic_section_id;
46 state.atomic_section_id=0;
47
48 for(const auto &pair : state.read_in_atomic_section)
49 {
50 ssa_exprt r = pair.first;
51 r.set_level_2(pair.second.first);
52
53 // guard is the disjunction over reads
54 PRECONDITION(!pair.second.second.empty());
55 guardt read_guard(pair.second.second.front());
56 for(std::list<guardt>::const_iterator it = ++(pair.second.second.begin());
57 it != pair.second.second.end();
58 ++it)
59 read_guard|=*it;
62
65 r,
66 atomic_section_id,
67 state.source);
68 }
69
70 for(const auto &pair : state.written_in_atomic_section)
71 {
72 ssa_exprt w = pair.first;
73 w.set_level_2(state.get_level2().latest_index(w.get_identifier()));
74
75 // guard is the disjunction over writes
76 PRECONDITION(!pair.second.empty());
77 guardt write_guard(pair.second.front());
78 for(std::list<guardt>::const_iterator it = ++(pair.second.begin());
79 it != pair.second.end();
80 ++it)
81 write_guard|=*it;
84
87 w,
88 atomic_section_id,
89 state.source);
90 }
91
93 state.guard.as_expr(),
94 atomic_section_id,
95 state.source);
96}
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
Base class for all expressions.
Definition expr.h:56
guardt guard
Definition goto_state.h:58
bool reachable
Is this code reachable? If not we can take shortcuts such as not entering function calls,...
Definition goto_state.h:62
unsigned atomic_section_id
Threads.
Definition goto_state.h:76
const symex_level2t & get_level2() const
Definition goto_state.h:45
Central data structure: state.
std::unordered_map< ssa_exprt, a_s_r_entryt, irep_hash > read_in_atomic_section
std::unordered_map< ssa_exprt, a_s_w_entryt, irep_hash > written_in_atomic_section
symex_targett::sourcet source
virtual void symex_atomic_begin(statet &state)
Symbolically execute an ATOMIC_BEGIN instruction.
symex_target_equationt & target
The equation that this execution is building up.
Definition goto_symex.h:266
unsigned atomic_section_counter
A monotonically increasing index for each encountered ATOMIC_BEGIN instruction.
Definition goto_symex.h:270
virtual void do_simplify(exprt &expr)
virtual void symex_atomic_end(statet &state)
Symbolically execute an ATOMIC_END instruction.
exprt as_expr() const
Definition guard_expr.h:46
Thrown when a goto program that's being processed is in an invalid format, for example passing the wr...
Expression providing an SSA-renamed symbol of expressions.
Definition ssa_expr.h:17
virtual void shared_read(const exprt &guard, const ssa_exprt &ssa_object, unsigned atomic_section_id, const sourcet &source)
Read from a shared variable ssa_object (which is both the left- and the right–hand side of assignment...
virtual void atomic_begin(const exprt &guard, unsigned atomic_section_id, const sourcet &source)
Record a beginning of an atomic section.
virtual void shared_write(const exprt &guard, const ssa_exprt &ssa_object, unsigned atomic_section_id, const sourcet &source)
Write to a shared variable ssa_object: we effectively assign a value from this thread to be visible b...
virtual void atomic_end(const exprt &guard, unsigned atomic_section_id, const sourcet &source)
Record ending an atomic section.
Symbolic Execution.
static int8_t r
Definition irep_hash.h:60
#define PRECONDITION(CONDITION)
Definition invariant.h:463
goto_programt::const_targett pc