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 
17 #include "expr_skeleton.h"
18 #include "path_storage.h"
19 #include "symex_assign.h"
20 
22 {
23  if(!state.reachable)
24  return;
25 
26  if(state.atomic_section_id != 0)
28  "spawning threads out of atomic sections is not allowed; "
29  "this would require amendments to ordering constraints",
30  state.source.pc->source_location);
31 
32  // record this
33  target.spawn(state.guard.as_expr(), state.source);
34 
35  const goto_programt::instructiont &instruction=*state.source.pc;
36 
37  INVARIANT(instruction.targets.size() == 1, "start_thread expects one target");
38 
39  goto_programt::const_targett thread_target=
40  instruction.get_target();
41 
42  // put into thread vector
43  std::size_t t=state.threads.size();
44  state.threads.push_back(statet::threadt(guard_manager));
45  // statet::threadt &cur_thread=state.threads[state.source.thread_nr];
46  statet::threadt &new_thread=state.threads.back();
47  new_thread.pc=thread_target;
48  new_thread.guard=state.guard;
49  new_thread.call_stack.push_back(state.call_stack().top());
50  new_thread.call_stack.back().local_objects.clear();
51  new_thread.call_stack.back().goto_state_map.clear();
52  #if 0
53  new_thread.abstract_events=&(target.new_thread(cur_thread.abstract_events));
54  #endif
55 
56  // create a copy of the local variables for the new thread
57  framet &frame = state.call_stack().top();
58 
60  state.get_level2().current_names.get_view(view);
61 
62  for(const auto &pair : view)
63  {
64  const irep_idt l1_o_id = pair.second.first.get_l1_object_identifier();
65 
66  // could use iteration over local_objects as l1_o_id is prefix
67  if(frame.local_objects.find(l1_o_id)==frame.local_objects.end())
68  continue;
69 
70  // get original name
71  ssa_exprt lhs(pair.second.first.get_original_expr());
72 
73  // get L0 name for current thread
74  const renamedt<ssa_exprt, L0> l0_lhs = symex_level0(std::move(lhs), ns, t);
75  const irep_idt &l0_name = l0_lhs.get().get_identifier();
76  std::size_t l1_index = path_storage.get_unique_l1_index(l0_name, 0);
77  CHECK_RETURN(l1_index == 0);
78 
79  // set up L1 name
80  state.level1.insert(l0_lhs, 0);
81 
82  const ssa_exprt lhs_l1 = state.rename_ssa<L1>(l0_lhs.get(), ns).get();
83  const irep_idt l1_name = lhs_l1.get_l1_object_identifier();
84  // store it
85  new_thread.call_stack.back().local_objects.insert(l1_name);
86 
87  // make copy
88  ssa_exprt rhs = pair.second.first;
89 
90  exprt::operandst lhs_conditions;
91  state.record_events.push(false);
94  .assign_symbol(lhs_l1, expr_skeletont{}, rhs, lhs_conditions);
95  state.record_events.pop();
96  }
97 
98  // initialize all variables marked thread-local
99  const symbol_tablet &symbol_table=ns.get_symbol_table();
100 
101  for(const auto &symbol_pair : symbol_table.symbols)
102  {
103  const symbolt &symbol = symbol_pair.second;
104 
105  if(!symbol.is_thread_local ||
106  !symbol.is_static_lifetime ||
107  (symbol.is_extern && symbol.value.is_nil()))
108  continue;
109 
110  // get original name
111  ssa_exprt lhs(symbol.symbol_expr());
112 
113  // get L0 name for current thread
114  lhs.set_level_0(t);
115 
116  exprt rhs=symbol.value;
117  if(rhs.is_nil())
118  {
119  const auto zero = zero_initializer(symbol.type, symbol.location, ns);
120  CHECK_RETURN(zero.has_value());
121  rhs = *zero;
122  }
123 
124  exprt::operandst lhs_conditions;
127  .assign_symbol(lhs, expr_skeletont{}, rhs, lhs_conditions);
128  }
129 }
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:37
ssa_exprt::set_level_0
void set_level_0(std::size_t i)
symbol_tablet
The symbol table.
Definition: symbol_table.h:14
symex_assign.h
Symbolic Execution of assignments.
goto_symex_statet::threadt::pc
goto_programt::const_targett pc
Definition: goto_symex_state.h:183
goto_symex_statet::level1
symex_level1t level1
Definition: goto_symex_state.h:71
L1
@ L1
Definition: renamed.h:24
CHECK_RETURN
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:495
goto_statet::reachable
bool reachable
Is this code reachable? If not we can take shortcuts such as not entering function calls,...
Definition: goto_state.h:62
symex_targett::sourcet::pc
goto_programt::const_targett pc
Definition: symex_target.h:42
expr_skeleton.h
Expression skeleton.
sharing_mapt::get_view
void get_view(V &view) const
Get a view of the elements in the map A view is a list of pairs with the components being const refer...
goto_symext::target
symex_target_equationt & target
The equation that this execution is building up.
Definition: goto_symex.h:251
symbolt::type
typet type
Type of symbol.
Definition: symbol.h:31
goto_symext::path_storage
path_storaget & path_storage
Symbolic execution paths to be resumed later.
Definition: goto_symex.h:789
goto_symex_statet
Central data structure: state.
Definition: goto_symex_state.h:42
goto_symext::guard_manager
guard_managert & guard_manager
Used to create guards.
Definition: goto_symex.h:248
exprt
Base class for all expressions.
Definition: expr.h:54
goto_symex_statet::source
symex_targett::sourcet source
Definition: goto_symex_state.h:60
goto_symex_statet::rename_ssa
NODISCARD renamedt< ssa_exprt, level > rename_ssa(ssa_exprt ssa, const namespacet &ns)
Version of rename which is specialized for SSA exprt.
goto_programt::instructiont::targets
targetst targets
The list of successor instructions.
Definition: goto_program.h:468
symex_assignt
Functor for symex assignment.
Definition: symex_assign.h:26
symex_level0
renamedt< ssa_exprt, L0 > symex_level0(ssa_exprt ssa_expr, const namespacet &ns, std::size_t thread_nr)
Set the level 0 renaming of SSA expressions.
Definition: renaming_level.cpp:22
renamedt::get
const underlyingt & get() const
Definition: renamed.h:40
path_storage.h
Storage of symbolic execution paths to resume.
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:317
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:90
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
goto_symex_statet::threadt::guard
guardt guard
Definition: goto_symex_state.h:184
sharing_mapt< irep_idt, std::pair< ssa_exprt, std::size_t > >::viewt
std::vector< view_itemt > viewt
View of the key-value pairs in the map.
Definition: sharing_map.h:388
goto_symex_statet::threads
std::vector< threadt > threads
Definition: goto_symex_state.h:194
expr_initializer.h
Expression Initialization.
goto_symex_statet::call_stack
call_stackt & call_stack()
Definition: goto_symex_state.h:143
call_stackt::top
framet & top()
Definition: call_stack.h:17
guard_exprt::as_expr
exprt as_expr() const
Definition: guard_expr.h:46
symbol_exprt::get_identifier
const irep_idt & get_identifier() const
Definition: std_expr.h:109
goto_symex.h
Symbolic Execution.
goto_statet::guard
guardt guard
Definition: goto_state.h:58
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:387
symex_level1t::insert
void insert(const renamedt< ssa_exprt, L0 > &ssa, std::size_t index)
Assume ssa is not already known.
Definition: renaming_level.cpp:47
exprt::operandst
std::vector< exprt > operandst
Definition: expr.h:56
framet
Stack frames – these are used for function calls and for exceptions.
Definition: frame.h:21
symex_target_equationt::spawn
virtual void spawn(const exprt &guard, const sourcet &source)
Record spawning a new thread.
Definition: symex_target_equation.cpp:65
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:243
symbolt::value
exprt value
Initial value of symbol.
Definition: symbol.h:34
namespacet::get_symbol_table
const symbol_table_baset & get_symbol_table() const
Return first symbol table registered with the namespace.
Definition: namespace.h:123
ssa_exprt::get_l1_object_identifier
const irep_idt get_l1_object_identifier() const
symbolt::is_extern
bool is_extern
Definition: symbol.h:66
symex_level2t::current_names
symex_renaming_levelt current_names
Definition: renaming_level.h:70
goto_symex_statet::threadt
Definition: goto_symex_state.h:182
symbolt::location
source_locationt location
Source code location of definition of symbol.
Definition: symbol.h:37
symbolt
Symbol table entry.
Definition: symbol.h:28
goto_statet::atomic_section_id
unsigned atomic_section_id
Threads.
Definition: goto_state.h:76
goto_statet::get_level2
const symex_level2t & get_level2() const
Definition: goto_state.h:45
symbol_table_baset::symbols
const symbolst & symbols
Read-only field, used to look up symbols given their names.
Definition: symbol_table_base.h:30
goto_symext::symex_config
const symex_configt symex_config
The configuration to use for this symbolic execution.
Definition: goto_symex.h:170
framet::local_objects
std::set< irep_idt > local_objects
Definition: frame.h:38
path_storaget::get_unique_l1_index
std::size_t get_unique_l1_index(const irep_idt &id, std::size_t minimum_index)
Provide a unique L1 index for a given id, starting from minimum_index.
Definition: path_storage.h:104
symbolt::is_static_lifetime
bool is_static_lifetime
Definition: symbol.h:65
goto_symex_statet::record_events
std::stack< bool > record_events
Definition: goto_symex_state.h:208
goto_programt::const_targett
instructionst::const_iterator const_targett
Definition: goto_program.h:647
symex_targett::assignment_typet::HIDDEN
@ HIDDEN
INVARIANT
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:423
goto_symex_statet::threadt::call_stack
call_stackt call_stack
Definition: goto_symex_state.h:185
goto_programt::instructiont
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:178
goto_symext::symex_start_thread
virtual void symex_start_thread(statet &state)
Symbolically execute a START_THREAD instruction.
Definition: symex_start_thread.cpp:21
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:472
renamedt
Wrapper for expressions or types which have been renamed up to a given level.
Definition: renamed.h:33
expr_skeletont
Expression in which some part is missing and can be substituted for another expression.
Definition: expr_skeleton.h:26