cprover
Loading...
Searching...
No Matches
goto_convert_exceptions.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Program Transformation
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
11
12#include "goto_convert_class.h"
13
14#include <util/std_expr.h>
15#include <util/symbol_table.h>
16
18 const codet &code,
19 goto_programt &dest,
20 const irep_idt &mode)
21{
23 code.operands().size() == 2,
24 "msc_try_finally expects two arguments",
26
27 goto_programt tmp;
29
30 {
31 // save 'leave' target
32 leave_targett leave_target(targets);
33 targets.set_leave(tmp.instructions.begin());
34
35 // first put 'finally' code onto destructor stack
38
39 // do 'try' code
40 convert(to_code(code.op0()), dest, mode);
41
42 // pop 'finally' from destructor stack
44
45 // 'leave' target gets restored here
46 }
47
48 // now add 'finally' code
49 convert(to_code(code.op1()), dest, mode);
50
51 // this is the target for 'leave'
52 dest.destructive_append(tmp);
53}
54
56 const codet &code,
57 goto_programt &dest,
58 const irep_idt &mode)
59{
61 code.operands().size() == 3,
62 "msc_try_except expects three arguments",
64
65 convert(to_code(code.op0()), dest, mode);
66
67 // todo: generate exception tracking
68}
69
71 const codet &code,
72 goto_programt &dest,
73 const irep_idt &mode)
74{
76 targets.leave_set, "leave without target", code.find_source_location());
77
78 // need to process destructor stack
80 code.source_location(), dest, mode, targets.leave_stack_node);
81
82 dest.add(
84}
85
87 const codet &code,
88 goto_programt &dest,
89 const irep_idt &mode)
90{
92 code.operands().size() >= 2,
93 "try_catch expects at least two arguments",
95
96 // add the CATCH-push instruction to 'dest'
97 goto_programt::targett catch_push_instruction =
99
100 code_push_catcht push_catch_code;
101
102 // the CATCH-push instruction is annotated with a list of IDs,
103 // one per target
104 code_push_catcht::exception_listt &exception_list=
105 push_catch_code.exception_list();
106
107 // add a SKIP target for the end of everything
108 goto_programt end;
110
111 // the first operand is the 'try' block
112 convert(to_code(code.op0()), dest, mode);
113
114 // add the CATCH-pop to the end of the 'try' block
115 goto_programt::targett catch_pop_instruction =
117 catch_pop_instruction->code_nonconst() = code_pop_catcht();
118
119 // add a goto to the end of the 'try' block
120 dest.add(goto_programt::make_goto(end_target));
121
122 for(std::size_t i=1; i<code.operands().size(); i++)
123 {
124 const codet &block=to_code(code.operands()[i]);
125
126 // grab the ID and add to CATCH instruction
127 exception_list.push_back(
128 code_push_catcht::exception_list_entryt(block.get(ID_exception_id)));
129
130 goto_programt tmp;
131 convert(block, tmp, mode);
132 catch_push_instruction->targets.push_back(tmp.instructions.begin());
133 dest.destructive_append(tmp);
134
135 // add a goto to the end of the 'catch' block
136 dest.add(goto_programt::make_goto(end_target));
137 }
138
139 catch_push_instruction->code_nonconst() = push_catch_code;
140
141 // add the end-target
142 dest.destructive_append(end);
143}
144
146 const codet &code,
147 goto_programt &dest,
148 const irep_idt &mode)
149{
151 code.operands().size() == 2,
152 "CPROVER_try_catch expects two arguments",
153 code.find_source_location());
154
155 // this is where we go after 'throw'
156 goto_programt tmp;
158
159 // set 'throw' target
160 throw_targett throw_target(targets);
161 targets.set_throw(tmp.instructions.begin());
162
163 // now put 'catch' code onto destructor stack
164 code_ifthenelset catch_code(exception_flag(mode), to_code(code.op1()));
165 catch_code.add_source_location()=code.source_location();
166
167 // Store the point before the temp catch code.
169 targets.destructor_stack.add(catch_code);
170
171 // now convert 'try' code
172 convert(to_code(code.op0()), dest, mode);
173
174 // pop 'catch' code off stack
176
177 // add 'throw' target
178 dest.destructive_append(tmp);
179}
180
182 const codet &code,
183 goto_programt &dest,
184 const irep_idt &mode)
185{
186 // set the 'exception' flag
188 exception_flag(mode), true_exprt(), code.source_location()));
189
190 // do we catch locally?
192 {
193 // need to process destructor stack
195 code.source_location(), dest, mode, targets.throw_stack_node);
196
197 // add goto
198 dest.add(
200 }
201 else // otherwise, we do a return
202 {
203 // need to process destructor stack
204 unwind_destructor_stack(code.source_location(), dest, mode);
205
206 // add goto
207 dest.add(
209 }
210}
211
213 const codet &code,
214 goto_programt &dest,
215 const irep_idt &mode)
216{
218 code.operands().size() == 2,
219 "CPROVER_try_finally expects two arguments",
220 code.find_source_location());
221
222 // first put 'finally' code onto destructor stack
225
226 // do 'try' code
227 convert(to_code(code.op0()), dest, mode);
228
229 // pop 'finally' from destructor stack
231
232 // now add 'finally' code
233 convert(to_code(code.op1()), dest, mode);
234}
235
237{
238 irep_idt id="$exception_flag";
239
240 symbol_tablet::symbolst::const_iterator s_it=
241 symbol_table.symbols.find(id);
242
243 if(s_it==symbol_table.symbols.end())
244 {
245 symbolt new_symbol;
246 new_symbol.base_name="$exception_flag";
247 new_symbol.name=id;
248 new_symbol.is_lvalue=true;
249 new_symbol.is_thread_local=true;
250 new_symbol.is_file_local=false;
251 new_symbol.type=bool_typet();
252 new_symbol.mode = mode;
253 symbol_table.insert(std::move(new_symbol));
254 }
255
256 return symbol_exprt(id, bool_typet());
257}
258
285 const source_locationt &source_location,
286 goto_programt &dest,
287 const irep_idt &mode,
288 optionalt<node_indext> end_index,
289 optionalt<node_indext> starting_index)
290{
291 // As we go we'll keep targets.destructor_stack.current_node pointing at the
292 // next node we intend to destroy, so that if our convert(...) call for each
293 // destructor returns, throws or otherwise unwinds then it will carry on from
294 // the correct point in the stack of variables we intend to destroy, and if it
295 // contains any DECL statements they will be added as a new child branch,
296 // again at the right point.
297
298 // We back up the current node as of entering this function so this
299 // side-effect is only noticed by that convert(...) call.
300
301 node_indext start_id =
302 starting_index.value_or(targets.destructor_stack.get_current_node());
303
305
306 node_indext end_id = end_index.value_or(0);
307
309 {
311
312 optionalt<codet> &destructor =
314
315 // Descend the tree before unwinding so we don't re-do the current node
316 // in event that convert(...) recurses into this function:
318 if(destructor)
319 {
320 // Copy, assign source location then convert.
321 codet copied_instruction = *destructor;
322 copied_instruction.add_source_location() = source_location;
323 convert(copied_instruction, dest, mode);
324 }
325 }
326
327 // Restore the working destructor stack to how it was before we began:
329}
The Boolean type.
Definition: std_types.h:36
codet representation of an if-then-else statement.
Definition: std_code.h:460
Pops an exception handler from the stack of active handlers (i.e.
Definition: std_code.h:1899
Pushes an exception handler, of the form: exception_tag1 -> label1 exception_tag2 -> label2 ....
Definition: std_code.h:1805
exception_listt & exception_list()
Definition: std_code.h:1860
std::vector< exception_list_entryt > exception_listt
Definition: std_code.h:1849
Data structure for representing an arbitrary statement in a program.
Definition: std_code_base.h:29
exprt & op0()
Definition: expr.h:99
exprt & op1()
Definition: expr.h:102
void set_current_node(optionalt< node_indext > val)
Sets the current node.
void add(const codet &destructor)
Adds a destructor to the current stack, attaching itself to the current node.
void descend_tree()
Walks the current node down to its child.
optionalt< codet > & get_destructor(node_indext index)
Fetches the destructor value for the passed-in node index.
node_indext get_current_node() const
Gets the node that the next addition will be added to as a child.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
const source_locationt & find_source_location() const
Get a source_locationt from the expression or from its operands (non-recursively).
Definition: expr.cpp:165
operandst & operands()
Definition: expr.h:92
const source_locationt & source_location() const
Definition: expr.h:230
source_locationt & add_source_location()
Definition: expr.h:235
symbol_table_baset & symbol_table
void convert_CPROVER_throw(const codet &code, goto_programt &dest, const irep_idt &mode)
void convert_msc_try_finally(const codet &code, goto_programt &dest, const irep_idt &mode)
struct goto_convertt::targetst targets
symbol_exprt exception_flag(const irep_idt &mode)
void convert_CPROVER_try_catch(const codet &code, goto_programt &dest, const irep_idt &mode)
void unwind_destructor_stack(const source_locationt &source_location, goto_programt &dest, const irep_idt &mode, optionalt< node_indext > destructor_start_point={}, optionalt< node_indext > destructor_end_point={})
Unwinds the destructor stack and creates destructors for each node between destructor_start_point and...
void convert_msc_try_except(const codet &code, goto_programt &dest, const irep_idt &mode)
void convert_try_catch(const codet &code, goto_programt &dest, const irep_idt &mode)
void convert(const codet &code, goto_programt &dest, const irep_idt &mode)
converts 'code' and appends the result to 'dest'
void convert_CPROVER_try_finally(const codet &code, goto_programt &dest, const irep_idt &mode)
void convert_msc_leave(const codet &code, goto_programt &dest, const irep_idt &mode)
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:598
instructionst::iterator targett
Definition: goto_program.h:592
void destructive_append(goto_programt &p)
Appends the given program p to *this. p is destroyed.
Definition: goto_program.h:698
static instructiont make_assignment(const code_assignt &_code, const source_locationt &l=source_locationt::nil())
Create an assignment instruction.
static instructiont make_skip(const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:880
static instructiont make_catch(const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:912
targett add(instructiont &&instruction)
Adds a given instruction at the end.
Definition: goto_program.h:715
static instructiont make_goto(targett _target, const source_locationt &l=source_locationt::nil())
const irep_idt & get(const irep_idt &name) const
Definition: irep.cpp:45
Expression to hold a symbol (variable)
Definition: std_expr.h:80
virtual std::pair< symbolt &, bool > insert(symbolt symbol)=0
Move or copy a new symbol to the symbol table.
const symbolst & symbols
Read-only field, used to look up symbols given their names.
Symbol table entry.
Definition: symbol.h:28
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:46
bool is_file_local
Definition: symbol.h:66
bool is_thread_local
Definition: symbol.h:65
typet type
Type of symbol.
Definition: symbol.h:31
irep_idt name
The unique identifier.
Definition: symbol.h:40
bool is_lvalue
Definition: symbol.h:66
irep_idt mode
Language mode.
Definition: symbol.h:49
The Boolean constant true.
Definition: std_expr.h:2856
std::size_t node_indext
Program Transformation.
nonstd::optional< T > optionalt
Definition: optional.h:35
#define INVARIANT_WITH_DIAGNOSTICS(CONDITION, REASON,...)
Same as invariant, with one or more diagnostics attached Diagnostics can be of any type that has a sp...
Definition: invariant.h:437
const codet & to_code(const exprt &expr)
API to expression classes.
void set_leave(goto_programt::targett _leave_target)
destructor_treet destructor_stack
goto_programt::targett return_target
goto_programt::targett leave_target
void set_throw(goto_programt::targett _throw_target)
goto_programt::targett throw_target
Author: Diffblue Ltd.