cprover
symex_atomic_section.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Symbolic Execution
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #include "goto_symex.h"
13 
15 {
16  if(state.guard.is_false())
17  return;
18 
19  // we don't allow any nesting of atomic sections
20  if(state.atomic_section_id!=0)
21  throw "nested atomic section detected at "+
22  state.source.pc->source_location.as_string();
23 
25  state.read_in_atomic_section.clear();
26  state.written_in_atomic_section.clear();
27 
29  state.guard.as_expr(),
31  state.source);
32 }
33 
35 {
36  if(state.guard.is_false())
37  return;
38 
39  if(state.atomic_section_id==0)
40  throw "ATOMIC_END unmatched"; // NOLINT(readability/throw)
41 
42  const unsigned atomic_section_id=state.atomic_section_id;
43  state.atomic_section_id=0;
44 
45  for(goto_symex_statet::read_in_atomic_sectiont::const_iterator
46  r_it=state.read_in_atomic_section.begin();
47  r_it!=state.read_in_atomic_section.end();
48  ++r_it)
49  {
50  ssa_exprt r=r_it->first;
51  r.set_level_2(r_it->second.first);
52 
53  // guard is the disjunction over reads
54  assert(!r_it->second.second.empty());
55  guardt read_guard(r_it->second.second.front());
56  for(std::list<guardt>::const_iterator
57  it=++(r_it->second.second.begin());
58  it!=r_it->second.second.end();
59  ++it)
60  read_guard|=*it;
61  exprt read_guard_expr=read_guard.as_expr();
62  do_simplify(read_guard_expr);
63 
65  read_guard_expr,
66  r,
67  atomic_section_id,
68  state.source);
69  }
70 
71  for(goto_symex_statet::written_in_atomic_sectiont::const_iterator
72  w_it=state.written_in_atomic_section.begin();
73  w_it!=state.written_in_atomic_section.end();
74  ++w_it)
75  {
76  ssa_exprt w=w_it->first;
78 
79  // guard is the disjunction over writes
80  assert(!w_it->second.empty());
81  guardt write_guard(w_it->second.front());
82  for(std::list<guardt>::const_iterator
83  it=++(w_it->second.begin());
84  it!=w_it->second.end();
85  ++it)
86  write_guard|=*it;
87  exprt write_guard_expr=write_guard.as_expr();
88  do_simplify(write_guard_expr);
89 
91  write_guard_expr,
92  w,
93  atomic_section_id,
94  state.source);
95  }
96 
98  state.guard.as_expr(),
99  atomic_section_id,
100  state.source);
101 }
exprt as_expr() const
Definition: guard.h:43
static int8_t r
Definition: irep_hash.h:59
goto_programt::const_targett pc
Definition: symex_target.h:32
read_in_atomic_sectiont read_in_atomic_section
const irep_idt & get_identifier() const
Definition: std_expr.h:128
bool is_false() const
Definition: expr.cpp:131
written_in_atomic_sectiont written_in_atomic_section
Definition: guard.h:19
void set_level_2(unsigned i)
Definition: ssa_expr.h:95
virtual void atomic_begin(const exprt &guard, unsigned atomic_section_id, const sourcet &source)
start an atomic section
virtual void do_simplify(exprt &)
Definition: goto_symex.cpp:19
virtual void atomic_end(const exprt &guard, unsigned atomic_section_id, const sourcet &source)
end 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 sharedvariable
virtual void symex_atomic_end(statet &)
goto_symex_statet::level2t level2
virtual void symex_atomic_begin(statet &)
Symbolic Execution.
symex_target_equationt & target
Definition: goto_symex.h:240
unsigned atomic_section_counter
Definition: goto_symex.h:241
virtual void shared_read(const exprt &guard, const ssa_exprt &ssa_object, unsigned atomic_section_id, const sourcet &source)
read from a shared variable
unsigned current_count(const irep_idt &identifier) const
Base class for all expressions.
Definition: expr.h:42
Expression providing an SSA-renamed symbol of expressions.
Definition: ssa_expr.h:17
symex_targett::sourcet source