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 
14 #include <util/exception_utils.h>
15 
17 {
18  if(state.guard.is_false())
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.guard.is_false())
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;
60  exprt read_guard_expr=read_guard.as_expr();
61  do_simplify(read_guard_expr);
62 
64  read_guard_expr,
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;
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;
82  exprt write_guard_expr=write_guard.as_expr();
83  do_simplify(write_guard_expr);
84 
86  write_guard_expr,
87  w,
88  atomic_section_id,
89  state.source);
90  }
91 
93  state.guard.as_expr(),
94  atomic_section_id,
95  state.source);
96 }
exception_utils.h
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:438
goto_symex_statet::guard
guardt guard
Definition: goto_symex_state.h:57
goto_symext::symex_atomic_begin
virtual void symex_atomic_begin(statet &)
Definition: symex_atomic_section.cpp:16
symex_targett::sourcet::pc
goto_programt::const_targett pc
Definition: symex_target.h:41
goto_symext::target
symex_target_equationt & target
Definition: goto_symex.h:216
goto_symex_statet::read_in_atomic_section
std::unordered_map< ssa_exprt, a_s_r_entryt, irep_hash > read_in_atomic_section
Definition: goto_symex_state.h:237
goto_symex_statet
Definition: goto_symex_state.h:34
goto_symex_statet::written_in_atomic_section
std::unordered_map< ssa_exprt, a_s_w_entryt, irep_hash > written_in_atomic_section
Definition: goto_symex_state.h:239
exprt
Base class for all expressions.
Definition: expr.h:54
goto_symex_statet::source
symex_targett::sourcet source
Definition: goto_symex_state.h:58
goto_symext::do_simplify
virtual void do_simplify(exprt &)
Definition: goto_symex.cpp:18
exprt::is_false
bool is_false() const
Return whether the expression is a constant representing false.
Definition: expr.cpp:99
incorrect_goto_program_exceptiont
Thrown when a goto program that's being processed is in an invalid format, for example passing the wr...
Definition: exception_utils.h:89
symex_renaming_levelt::current_count
unsigned current_count(const irep_idt &identifier) const
Counter corresponding to an identifier.
Definition: renaming_level.h:34
ssa_exprt
Expression providing an SSA-renamed symbol of expressions.
Definition: ssa_expr.h:17
symex_target_equationt::atomic_end
virtual void atomic_end(const exprt &guard, unsigned atomic_section_id, const sourcet &source)
Record ending an atomic section.
Definition: symex_target_equation.cpp:111
guardt
Definition: guard.h:19
goto_symex_statet::atomic_section_id
unsigned atomic_section_id
Definition: goto_symex_state.h:234
symbol_exprt::get_identifier
const irep_idt & get_identifier() const
Definition: std_expr.h:176
goto_symex.h
symex_target_equationt::shared_write
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...
Definition: symex_target_equation.cpp:49
symex_target_equationt::atomic_begin
virtual void atomic_begin(const exprt &guard, unsigned atomic_section_id, const sourcet &source)
Record a beginning of an atomic section.
Definition: symex_target_equation.cpp:95
goto_symext::atomic_section_counter
unsigned atomic_section_counter
Definition: goto_symex.h:217
goto_symext::symex_atomic_end
virtual void symex_atomic_end(statet &)
Definition: symex_atomic_section.cpp:36
symex_target_equationt::shared_read
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 assignme...
Definition: symex_target_equation.cpp:31
ssa_exprt::set_level_2
void set_level_2(unsigned i)
Definition: ssa_expr.h:95
guardt::as_expr
exprt as_expr() const
Definition: guard.h:41
r
static int8_t r
Definition: irep_hash.h:59
goto_symex_statet::level2
symex_level2t level2
Definition: goto_symex_state.h:66