cprover
symex_start_thread.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 #include <util/expr_initializer.h>
16 
18 {
19  if(state.guard.is_false())
20  return;
21 
22  if(state.atomic_section_id != 0)
24  "spawning threads out of atomic sections is not allowed; "
25  "this would require amendments to ordering constraints",
26  state.source.pc->source_location);
27 
28  // record this
29  target.spawn(state.guard.as_expr(), state.source);
30 
31  const goto_programt::instructiont &instruction=*state.source.pc;
32 
33  INVARIANT(instruction.targets.size() == 1, "start_thread expects one target");
34 
35  goto_programt::const_targett thread_target=
36  instruction.get_target();
37 
38  // put into thread vector
39  std::size_t t=state.threads.size();
40  state.threads.push_back(statet::threadt());
41  // statet::threadt &cur_thread=state.threads[state.source.thread_nr];
42  statet::threadt &new_thread=state.threads.back();
43  new_thread.pc=thread_target;
44  new_thread.guard=state.guard;
45  new_thread.call_stack.push_back(state.top());
46  new_thread.call_stack.back().local_objects.clear();
47  new_thread.call_stack.back().goto_state_map.clear();
48  #if 0
49  new_thread.abstract_events=&(target.new_thread(cur_thread.abstract_events));
50  #endif
51 
52  // create a copy of the local variables for the new thread
53  statet::framet &frame=state.top();
54 
55  for(auto c_it = state.level2.current_names.begin();
56  c_it != state.level2.current_names.end();
57  ++c_it)
58  {
59  const irep_idt l1_o_id=c_it->second.first.get_l1_object_identifier();
60  // could use iteration over local_objects as l1_o_id is prefix
61  if(frame.local_objects.find(l1_o_id)==frame.local_objects.end())
62  continue;
63 
64  // get original name
65  ssa_exprt lhs(c_it->second.first.get_original_expr());
66 
67  // get L0 name for current thread
68  lhs.set_level_0(t);
69 
70  // set up L1 name
71  if(!state.level1.current_names.insert(
72  std::make_pair(lhs.get_l1_object_identifier(),
73  std::make_pair(lhs, 0))).second)
75  state.rename(lhs, ns, goto_symex_statet::L1);
76  const irep_idt l1_name=lhs.get_l1_object_identifier();
77  // store it
78  state.l1_history.insert(l1_name);
79  new_thread.call_stack.back().local_objects.insert(l1_name);
80 
81  // make copy
82  ssa_exprt rhs=c_it->second.first;
83 
84  guardt guard;
85  const bool record_events=state.record_events;
86  state.record_events=false;
88  state,
89  lhs,
90  nil_exprt(),
91  rhs,
92  guard,
94  state.record_events=record_events;
95  }
96 
97  // initialize all variables marked thread-local
98  const symbol_tablet &symbol_table=ns.get_symbol_table();
99 
100  for(const auto &symbol_pair : symbol_table.symbols)
101  {
102  const symbolt &symbol = symbol_pair.second;
103 
104  if(!symbol.is_thread_local ||
105  !symbol.is_static_lifetime ||
106  (symbol.is_extern && symbol.value.is_nil()))
107  continue;
108 
109  // get original name
110  ssa_exprt lhs(symbol.symbol_expr());
111 
112  // get L0 name for current thread
113  lhs.set_level_0(t);
114 
115  exprt rhs=symbol.value;
116  if(rhs.is_nil())
117  {
118  const auto zero = zero_initializer(symbol.type, symbol.location, ns);
119  CHECK_RETURN(zero.has_value());
120  rhs = *zero;
121  }
122 
123  guardt guard;
125  state,
126  lhs,
127  nil_exprt(),
128  rhs,
129  guard,
131  }
132 }
exception_utils.h
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
symbol_tablet
The symbol table.
Definition: symbol_table.h:19
goto_symex_statet::guard
guardt guard
Definition: goto_symex_state.h:57
goto_symex_statet::threadt::pc
goto_programt::const_targett pc
Definition: goto_symex_state.h:245
goto_symex_statet::level1
symex_level1t level1
Definition: goto_symex_state.h:65
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
symbolt::type
typet type
Type of symbol.
Definition: symbol.h:31
goto_symex_statet
Definition: goto_symex_state.h:34
goto_symex_statet::L1
@ L1
Definition: goto_symex_state.h:72
goto_symex_statet::rename
void rename(exprt &expr, const namespacet &ns, levelt level=L2)
Definition: goto_symex_state.cpp:273
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_symex_statet::l1_history
std::set< irep_idt > l1_history
Definition: goto_symex_state.h:62
goto_programt::instructiont::targets
targetst targets
The list of successor instructions.
Definition: goto_program.h:203
goto_symext::symex_start_thread
virtual void symex_start_thread(statet &)
Definition: symex_start_thread.cpp:17
goto_symex_statet::framet::local_objects
std::set< irep_idt > local_objects
Definition: goto_symex_state.h:187
UNREACHABLE
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:478
zero_initializer
optionalt< exprt > zero_initializer(const typet &type, const source_locationt &source_location, const namespacet &ns)
Create the equivalent of zero for type type.
Definition: expr_initializer.cpp:322
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
ssa_exprt
Expression providing an SSA-renamed symbol of expressions.
Definition: ssa_expr.h:17
symbolt::is_thread_local
bool is_thread_local
Definition: symbol.h:65
guardt
Definition: guard.h:19
goto_symex_statet::threadt::guard
guardt guard
Definition: goto_symex_state.h:246
goto_symex_statet::threads
std::vector< threadt > threads
Definition: goto_symex_state.h:252
goto_symex_statet::record_events
bool record_events
Definition: goto_symex_state.h:257
goto_symext::symex_assign_symbol
void symex_assign_symbol(statet &, const ssa_exprt &lhs, const exprt &full_lhs, const exprt &rhs, guardt &, assignment_typet)
Definition: symex_assign.cpp:213
expr_initializer.h
goto_symex_statet::atomic_section_id
unsigned atomic_section_id
Definition: goto_symex_state.h:234
goto_symex_statet::top
framet & top()
Definition: goto_symex_state.h:215
nil_exprt
The NIL expression.
Definition: std_expr.h:4461
goto_symex.h
symbolt::symbol_expr
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition: symbol.cpp:121
irept::is_nil
bool is_nil() const
Definition: irep.h:172
symex_target_equationt::spawn
virtual void spawn(const exprt &guard, const sourcet &source)
Record spawning a new thread.
Definition: symex_target_equation.cpp:68
goto_symext::ns
namespacet ns
Initialized just before symbolic execution begins, to point to both outer_symbol_table and the symbol...
Definition: goto_symex.h:215
symbolt::value
exprt value
Initial value of symbol.
Definition: symbol.h:34
goto_symex_statet::framet
Definition: goto_symex_state.h:174
namespacet::get_symbol_table
const symbol_table_baset & get_symbol_table() const
Return first symbol table registered with the namespace.
Definition: namespace.h:126
ssa_exprt::get_l1_object_identifier
const irep_idt get_l1_object_identifier() const
Definition: ssa_expr.h:66
symbolt::is_extern
bool is_extern
Definition: symbol.h:66
goto_symex_statet::threadt
Definition: goto_symex_state.h:243
ssa_exprt::set_level_0
void set_level_0(unsigned i)
Definition: ssa_expr.h:83
symbolt::location
source_locationt location
Source code location of definition of symbol.
Definition: symbol.h:37
symbolt
Symbol table entry.
Definition: symbol.h:27
symbol_table_baset::symbols
const symbolst & symbols
Definition: symbol_table_base.h:27
guardt::as_expr
exprt as_expr() const
Definition: guard.h:41
symbolt::is_static_lifetime
bool is_static_lifetime
Definition: symbol.h:65
goto_programt::const_targett
instructionst::const_iterator const_targett
Definition: goto_program.h:415
symex_targett::assignment_typet::HIDDEN
@ HIDDEN
goto_symex_statet::threadt::call_stack
call_stackt call_stack
Definition: goto_symex_state.h:247
goto_symex_statet::level2
symex_level2t level2
Definition: goto_symex_state.h:66
goto_programt::instructiont
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:178
symex_renaming_levelt::current_names
current_namest current_names
Definition: renaming_level.h:31
goto_programt::instructiont::get_target
targett get_target() const
Returns the first (and only) successor for the usual case of a single target.
Definition: goto_program.h:207
validation_modet::INVARIANT
@ INVARIANT
CHECK_RETURN
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:470