cprover
Loading...
Searching...
No Matches
symex_start_thread.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
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 const std::size_t new_thread_nr = 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.function_id = state.source.function_id;
49 new_thread.guard=state.guard;
50 new_thread.call_stack.push_back(state.call_stack().top());
51 new_thread.call_stack.back().local_objects.clear();
52 new_thread.call_stack.back().goto_state_map.clear();
53 #if 0
54 new_thread.abstract_events=&(target.new_thread(cur_thread.abstract_events));
55 #endif
56
57 const std::size_t current_thread_nr = state.source.thread_nr;
58
59 // create a copy of the local variables for the new thread
60 framet &frame = state.call_stack().top();
61
63 state.get_level2().current_names.get_view(view);
64
65 for(const auto &pair : view)
66 {
67 const irep_idt l1_o_id = pair.second.first.get_l1_object_identifier();
68
69 // could use iteration over local_objects as l1_o_id is prefix
70 if(frame.local_objects.find(l1_o_id)==frame.local_objects.end())
71 continue;
72
73 // get original name
74 ssa_exprt lhs(pair.second.first.get_original_expr());
75
76 // get L0 name for current thread
77 const renamedt<ssa_exprt, L0> l0_lhs =
78 symex_level0(std::move(lhs), ns, new_thread_nr);
79 const irep_idt &l0_name = l0_lhs.get().get_identifier();
80 std::size_t l1_index = path_storage.get_unique_l1_index(l0_name, 0);
81 CHECK_RETURN(l1_index == 0);
82
83 // set up L1 name
84 state.level1.insert(l0_lhs, 0);
85
86 const ssa_exprt lhs_l1 = state.rename_ssa<L1>(l0_lhs.get(), ns).get();
87 const irep_idt l1_name = lhs_l1.get_l1_object_identifier();
88 // store it
89 new_thread.call_stack.back().local_objects.insert(l1_name);
90
91 // make copy
92 ssa_exprt rhs = pair.second.first;
93
94 exprt::operandst lhs_conditions;
95 state.record_events.push(false);
98 state,
100 ns,
102 target}
103 .assign_symbol(lhs_l1, expr_skeletont{}, rhs, lhs_conditions);
104 const exprt l2_lhs = state.rename(lhs_l1, ns).get();
105 state.record_events.pop();
106
107 // record a shared write in the new thread
108 if(
109 state.write_is_shared(lhs_l1, ns) ==
111 is_ssa_expr(l2_lhs))
112 {
113 state.source.thread_nr = new_thread_nr;
114 target.shared_write(
115 state.guard.as_expr(), to_ssa_expr(l2_lhs), 0, state.source);
116 state.source.thread_nr = current_thread_nr;
117 }
118 }
119
120 // initialize all variables marked thread-local
121 const symbol_tablet &symbol_table=ns.get_symbol_table();
122
123 for(const auto &symbol_pair : symbol_table.symbols)
124 {
125 const symbolt &symbol = symbol_pair.second;
126
127 if(!symbol.is_thread_local ||
128 !symbol.is_static_lifetime ||
129 (symbol.is_extern && symbol.value.is_nil()))
130 continue;
131
132 // get original name
133 ssa_exprt lhs(symbol.symbol_expr());
134
135 // get L0 name for current thread
136 lhs.set_level_0(new_thread_nr);
137
138 exprt rhs=symbol.value;
139 if(rhs.is_nil())
140 {
141 const auto zero = zero_initializer(symbol.type, symbol.location, ns);
142 CHECK_RETURN(zero.has_value());
143 rhs = *zero;
144 }
145
146 exprt::operandst lhs_conditions;
149 state,
151 ns,
153 target}
154 .assign_symbol(lhs, expr_skeletont{}, rhs, lhs_conditions);
155 }
156}
framet & top()
Definition call_stack.h:17
Expression in which some part is missing and can be substituted for another expression.
Base class for all expressions.
Definition expr.h:56
std::vector< exprt > operandst
Definition expr.h:58
Stack frames – these are used for function calls and for exceptions.
std::set< irep_idt > local_objects
Definition frame.h:44
This class represents an instruction in the GOTO intermediate representation.
targetst targets
The list of successor instructions.
const_targett get_target() const
Returns the first (and only) successor for the usual case of a single target.
instructionst::const_iterator const_targett
guardt guard
Definition goto_state.h:58
bool reachable
Is this code reachable?
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
call_stackt & call_stack()
std::stack< bool > record_events
symex_level1t level1
renamedt< exprt, level > rename(exprt expr, const namespacet &ns)
Rewrites symbol expressions in exprt, applying a suffix to each symbol reflecting its most recent ver...
write_is_shared_resultt write_is_shared(const ssa_exprt &expr, const namespacet &ns) const
symex_targett::sourcet source
renamedt< ssa_exprt, level > rename_ssa(ssa_exprt ssa, const namespacet &ns)
Version of rename which is specialized for SSA exprt.
std::vector< threadt > threads
goto_symex_statet statet
A type abbreviation for goto_symex_statet.
Definition goto_symex.h:40
symex_target_equationt & target
The equation that this execution is building up.
Definition goto_symex.h:266
guard_managert & guard_manager
Used to create guards.
Definition goto_symex.h:263
shadow_memoryt shadow_memory
Shadow memory instrumentation API.
Definition goto_symex.h:839
virtual void symex_start_thread(statet &state)
Symbolically execute a START_THREAD instruction.
namespacet ns
Initialized just before symbolic execution begins, to point to both outer_symbol_table and the symbol...
Definition goto_symex.h:258
const symex_configt symex_config
The configuration to use for this symbolic execution.
Definition goto_symex.h:185
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...
bool is_nil() const
Definition irep.h:368
Wrapper for expressions or types which have been renamed up to a given level.
Definition renamed.h:33
const underlyingt & get() const
Definition renamed.h:40
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...
Expression providing an SSA-renamed symbol of expressions.
Definition ssa_expr.h:17
const irep_idt get_l1_object_identifier() const
Definition ssa_expr.cpp:170
void set_level_0(std::size_t i)
Definition ssa_expr.cpp:181
const symbolst & symbols
Read-only field, used to look up symbols given their names.
The symbol table.
Symbol table entry.
Definition symbol.h:28
bool is_extern
Definition symbol.h:74
bool is_static_lifetime
Definition symbol.h:70
bool is_thread_local
Definition symbol.h:71
source_locationt location
Source code location of definition of symbol.
Definition symbol.h:37
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition symbol.cpp:121
typet type
Type of symbol.
Definition symbol.h:31
exprt value
Initial value of symbol.
Definition symbol.h:34
Functor for symex assignment.
void assign_symbol(const ssa_exprt &lhs, const expr_skeletont &full_lhs, const exprt &rhs, const exprt::operandst &guard)
Record the assignment of value rhs to variable lhs in state and add the equation to target: lhs#{n+1}...
std::optional< exprt > zero_initializer(const typet &type, const source_locationt &source_location, const namespacet &ns)
Create the equivalent of zero for type type.
Expression Initialization.
Expression skeleton.
Symbolic Execution.
Storage of symbolic execution paths to resume.
@ L1
Definition renamed.h:24
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.
#define CHECK_RETURN(CONDITION)
Definition invariant.h:495
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition invariant.h:423
bool is_ssa_expr(const exprt &expr)
Definition ssa_expr.h:125
const ssa_exprt & to_ssa_expr(const exprt &expr)
Cast a generic exprt to an ssa_exprt.
Definition ssa_expr.h:145
goto_programt::const_targett pc
void insert(const renamedt< ssa_exprt, L0 > &ssa, std::size_t index)
Assume ssa is not already known.
symex_renaming_levelt current_names
goto_programt::const_targett pc
Symbolic Execution of assignments.
dstringt irep_idt