CBMC
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 #include <util/symbol_table_base.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",
25  code.find_source_location());
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
37  targets.scope_stack.add(to_code(code.op1()), {});
38 
39  // do 'try' code
40  convert(to_code(code.op0()), dest, mode);
41 
42  // pop 'finally' from destructor stack
43  targets.scope_stack.set_current_node(old_stack_top);
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",
63  code.find_source_location());
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",
94  code.find_source_location());
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.scope_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
175  targets.scope_stack.set_current_node(old_stack_top);
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?
191  if(targets.throw_set)
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
224  targets.scope_stack.add(to_code(code.op1()), {});
225 
226  // do 'try' code
227  convert(to_code(code.op0()), dest, mode);
228 
229  // pop 'finally' from destructor stack
230  targets.scope_stack.set_current_node(old_stack_top);
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_table_baset::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{id, bool_typet{}, mode};
246  new_symbol.base_name = "$exception_flag";
247  new_symbol.is_lvalue = true;
248  new_symbol.is_thread_local = true;
249  symbol_table.insert(std::move(new_symbol));
250  }
251 
252  return symbol_exprt(id, bool_typet());
253 }
254 
281  const source_locationt &source_location,
282  goto_programt &dest,
283  const irep_idt &mode,
284  std::optional<node_indext> end_index,
285  std::optional<node_indext> starting_index)
286 {
287  // As we go we'll keep targets.scope_stack.current_node pointing at the
288  // next node we intend to destroy, so that if our convert(...) call for each
289  // destructor returns, throws or otherwise unwinds then it will carry on from
290  // the correct point in the stack of variables we intend to destroy, and if it
291  // contains any DECL statements they will be added as a new child branch,
292  // again at the right point.
293 
294  // We back up the current node as of entering this function so this
295  // side-effect is only noticed by that convert(...) call.
296 
297  node_indext start_id =
298  starting_index.value_or(targets.scope_stack.get_current_node());
299 
301 
302  node_indext end_id = end_index.value_or(0);
303 
304  while(targets.scope_stack.get_current_node() > end_id)
305  {
307 
308  std::optional<codet> &destructor =
309  targets.scope_stack.get_destructor(current_node);
310 
311  // Descend the tree before unwinding so we don't re-do the current node
312  // in event that convert(...) recurses into this function:
314  if(destructor)
315  {
316  // Copy, assign source location then convert.
317  codet copied_instruction = *destructor;
318  copied_instruction.add_source_location() = source_location;
319  convert(copied_instruction, dest, mode);
320  }
321  }
322 
323  // Restore the working destructor stack to how it was before we began:
325 }
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
std::vector< exception_list_entryt > exception_listt
Definition: std_code.h:1849
exception_listt & exception_list()
Definition: std_code.h:1860
Data structure for representing an arbitrary statement in a program.
Definition: std_code_base.h:29
exprt & op1()
Definition: expr.h:136
exprt & op0()
Definition: expr.h:133
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:38
const source_locationt & find_source_location() const
Get a source_locationt from the expression or from its operands (non-recursively).
Definition: expr.cpp:147
source_locationt & add_source_location()
Definition: expr.h:236
const source_locationt & source_location() const
Definition: expr.h:231
operandst & operands()
Definition: expr.h:94
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)
void unwind_destructor_stack(const source_locationt &source_location, goto_programt &dest, const irep_idt &mode, std::optional< node_indext > destructor_end_point={}, std::optional< node_indext > destructor_start_point={})
Unwinds the destructor stack and creates destructors for each node between destructor_start_point and...
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 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:622
instructionst::iterator targett
Definition: goto_program.h:614
void destructive_append(goto_programt &p)
Appends the given program p to *this. p is destroyed.
Definition: goto_program.h:722
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:891
static instructiont make_catch(const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:923
targett add(instructiont &&instruction)
Adds a given instruction at the end.
Definition: goto_program.h:739
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:44
void add(const codet &destructor, std::optional< goto_programt::targett > declaration)
Adds a destructor/declaration pair to the current stack, attaching it to the current node.
Definition: scope_tree.cpp:11
void descend_tree()
Walks the current node down to its child.
Definition: scope_tree.cpp:100
void set_current_node(std::optional< node_indext > val)
Sets the current node.
Definition: scope_tree.cpp:89
std::optional< codet > & get_destructor(node_indext index)
Fetches the destructor value for the passed-in node index.
Definition: scope_tree.cpp:24
node_indext get_current_node() const
Gets the node that the next addition will be added to as a child.
Definition: scope_tree.cpp:109
Expression to hold a symbol (variable)
Definition: std_expr.h:131
const symbolst & symbols
Read-only field, used to look up symbols given their names.
virtual std::pair< symbolt &, bool > insert(symbolt symbol)=0
Move or copy a new symbol to the symbol table.
Symbol table entry.
Definition: symbol.h:28
The Boolean constant true.
Definition: std_expr.h:3063
Program Transformation.
std::size_t node_indext
Definition: scope_tree.h:19
#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)
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.