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