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 {
21  if(code.operands().size()!=2)
22  {
24  error() << "msc_try_finally expects two arguments" << eom;
25  throw 0;
26  }
27 
28  goto_programt tmp;
29  tmp.add_instruction(SKIP)->source_location=code.source_location();
30 
31  {
32  // save 'leave' target
33  leave_targett leave_target(targets);
34  targets.set_leave(tmp.instructions.begin());
35 
36  // first put 'finally' code onto destructor stack
37  targets.destructor_stack.push_back(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.destructor_stack.pop_back();
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 {
60  if(code.operands().size()!=3)
61  {
63  error() << "msc_try_except expects three arguments" << eom;
64  throw 0;
65  }
66 
67  convert(to_code(code.op0()), dest, mode);
68 
69  // todo: generate exception tracking
70 }
71 
73  const codet &code,
74  goto_programt &dest,
75  const irep_idt &mode)
76 {
77  if(!targets.leave_set)
78  {
80  error() << "leave without target" << eom;
81  throw 0;
82  }
83 
84  // need to process destructor stack
85  for(std::size_t d=targets.destructor_stack.size();
87  d--)
88  {
89  codet d_code=targets.destructor_stack[d-1];
90  d_code.add_source_location()=code.source_location();
91  convert(d_code, dest, mode);
92  }
93 
95  t->make_goto(targets.leave_target);
96  t->source_location=code.source_location();
97 }
98 
100  const codet &code,
101  goto_programt &dest,
102  const irep_idt &mode)
103 {
104  assert(code.operands().size()>=2);
105 
106  // add the CATCH-push instruction to 'dest'
107  goto_programt::targett catch_push_instruction=dest.add_instruction();
108  catch_push_instruction->make_catch();
109  catch_push_instruction->source_location=code.source_location();
110 
111  code_push_catcht push_catch_code;
112 
113  // the CATCH-push instruction is annotated with a list of IDs,
114  // one per target
115  code_push_catcht::exception_listt &exception_list=
116  push_catch_code.exception_list();
117 
118  // add a SKIP target for the end of everything
119  goto_programt end;
120  goto_programt::targett end_target=end.add_instruction();
121  end_target->make_skip();
122 
123  // the first operand is the 'try' block
124  convert(to_code(code.op0()), dest, mode);
125 
126  // add the CATCH-pop to the end of the 'try' block
127  goto_programt::targett catch_pop_instruction=dest.add_instruction();
128  catch_pop_instruction->make_catch();
129  catch_pop_instruction->code=code_pop_catcht();
130 
131  // add a goto to the end of the 'try' block
132  dest.add_instruction()->make_goto(end_target);
133 
134  for(std::size_t i=1; i<code.operands().size(); i++)
135  {
136  const codet &block=to_code(code.operands()[i]);
137 
138  // grab the ID and add to CATCH instruction
139  exception_list.push_back(
140  code_push_catcht::exception_list_entryt(block.get(ID_exception_id)));
141 
142  goto_programt tmp;
143  convert(block, tmp, mode);
144  catch_push_instruction->targets.push_back(tmp.instructions.begin());
145  dest.destructive_append(tmp);
146 
147  // add a goto to the end of the 'catch' block
148  dest.add_instruction()->make_goto(end_target);
149  }
150 
151  catch_push_instruction->code=push_catch_code;
152 
153  // add the end-target
154  dest.destructive_append(end);
155 }
156 
158  const codet &code,
159  goto_programt &dest,
160  const irep_idt &mode)
161 {
162  if(code.operands().size()!=2)
163  {
165  error() << "CPROVER_try_catch expects two arguments" << eom;
166  throw 0;
167  }
168 
169  // this is where we go after 'throw'
170  goto_programt tmp;
171  tmp.add_instruction(SKIP)->source_location=code.source_location();
172 
173  // set 'throw' target
174  throw_targett throw_target(targets);
175  targets.set_throw(tmp.instructions.begin());
176 
177  // now put 'catch' code onto destructor stack
178  code_ifthenelset catch_code;
179  catch_code.cond()=exception_flag();
180  catch_code.add_source_location()=code.source_location();
181  catch_code.then_case()=to_code(code.op1());
182 
183  targets.destructor_stack.push_back(catch_code);
184 
185  // now convert 'try' code
186  convert(to_code(code.op0()), dest, mode);
187 
188  // pop 'catch' code off stack
189  targets.destructor_stack.pop_back();
190 
191  // add 'throw' target
192  dest.destructive_append(tmp);
193 }
194 
196  const codet &code,
197  goto_programt &dest,
198  const irep_idt &mode)
199 {
200  // set the 'exception' flag
201  {
202  goto_programt::targett t_set_exception=
203  dest.add_instruction(ASSIGN);
204 
205  t_set_exception->source_location=code.source_location();
206  t_set_exception->code=code_assignt(exception_flag(), true_exprt());
207  }
208 
209  // do we catch locally?
210  if(targets.throw_set)
211  {
212  // need to process destructor stack
214  code.source_location(), targets.throw_stack_size, dest, mode);
215 
216  // add goto
218  t->make_goto(targets.throw_target);
219  t->source_location=code.source_location();
220  }
221  else // otherwise, we do a return
222  {
223  // need to process destructor stack
224  unwind_destructor_stack(code.source_location(), 0, dest, mode);
225 
226  // add goto
228  t->make_goto(targets.return_target);
229  t->source_location=code.source_location();
230  }
231 }
232 
234  const codet &code,
235  goto_programt &dest,
236  const irep_idt &mode)
237 {
238  if(code.operands().size()!=2)
239  {
241  error() << "CPROVER_try_finally expects two arguments" << eom;
242  throw 0;
243  }
244 
245  // first put 'finally' code onto destructor stack
246  targets.destructor_stack.push_back(to_code(code.op1()));
247 
248  // do 'try' code
249  convert(to_code(code.op0()), dest, mode);
250 
251  // pop 'finally' from destructor stack
252  targets.destructor_stack.pop_back();
253 
254  // now add 'finally' code
255  convert(to_code(code.op1()), dest, mode);
256 }
257 
259 {
260  irep_idt id="$exception_flag";
261 
262  symbol_tablet::symbolst::const_iterator s_it=
263  symbol_table.symbols.find(id);
264 
265  if(s_it==symbol_table.symbols.end())
266  {
267  symbolt new_symbol;
268  new_symbol.base_name="$exception_flag";
269  new_symbol.name=id;
270  new_symbol.is_lvalue=true;
271  new_symbol.is_thread_local=true;
272  new_symbol.is_file_local=false;
273  new_symbol.type=bool_typet();
274  symbol_table.insert(std::move(new_symbol));
275  }
276 
277  return symbol_exprt(id, bool_typet());
278 }
279 
281  const source_locationt &source_location,
282  std::size_t final_stack_size,
283  goto_programt &dest,
284  const irep_idt &mode)
285 {
287  source_location, final_stack_size, dest, targets.destructor_stack, mode);
288 }
289 
291  const source_locationt &source_location,
292  std::size_t final_stack_size,
293  goto_programt &dest,
294  destructor_stackt &destructor_stack,
295  const irep_idt &mode)
296 {
297  // There might be exceptions happening in the exception
298  // handler. We thus pop off the stack, and then later
299  // one restore the original stack.
300  destructor_stackt old_stack=destructor_stack;
301 
302  while(destructor_stack.size()>final_stack_size)
303  {
304  codet d_code=destructor_stack.back();
305  d_code.add_source_location()=source_location;
306 
307  // pop now to avoid doing this again
308  destructor_stack.pop_back();
309 
310  convert(d_code, dest, mode);
311  }
312 
313  // Now restore old stack.
314  old_stack.swap(destructor_stack);
315 }
irep_idt name
The unique identifier.
Definition: symbol.h:43
const codet & then_case() const
Definition: std_code.h:486
std::vector< exception_list_entryt > exception_listt
Definition: std_code.h:1589
bool is_thread_local
Definition: symbol.h:67
goto_programt::targett return_target
exprt & op0()
Definition: expr.h:72
struct goto_convertt::targetst targets
void convert(const codet &code, goto_programt &dest, const irep_idt &mode)
converts &#39;code&#39; and appends the result to &#39;dest&#39;
const exprt & cond() const
Definition: std_code.h:476
Pushes an exception handler, of the form: exception_tag1 -> label1 exception_tag2 -> label2 ...
Definition: std_code.h:1544
void destructive_append(goto_programt &p)
Appends the given program, which is destroyed.
Definition: goto_program.h:486
void convert_try_catch(const codet &code, goto_programt &dest, const irep_idt &mode)
Pops an exception handler from the stack of active handlers (i.e.
Definition: std_code.h:1632
The proper Booleans.
Definition: std_types.h:34
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:30
static mstreamt & eom(mstreamt &m)
Definition: message.h:272
goto_programt::targett throw_target
destructor_stackt destructor_stack
The boolean constant true.
Definition: std_expr.h:4486
instructionst::iterator targett
Definition: goto_program.h:397
symbol_exprt exception_flag()
goto_programt::targett leave_target
const source_locationt & find_source_location() const
Definition: expr.cpp:246
source_locationt source_location
Definition: message.h:214
Program Transformation.
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:403
API to expression classes.
exprt & op1()
Definition: expr.h:75
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:213
mstreamt & error() const
Definition: message.h:302
void convert_CPROVER_throw(const codet &code, goto_programt &dest, const irep_idt &mode)
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:33
void convert_msc_leave(const codet &code, goto_programt &dest, const irep_idt &mode)
const symbolst & symbols
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:70
typet type
Type of symbol.
Definition: symbol.h:34
std::vector< codet > destructor_stackt
targett add_instruction()
Adds an instruction at the end.
Definition: goto_program.h:505
void set_leave(goto_programt::targett _leave_target)
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:49
void set_throw(goto_programt::targett _throw_target)
const source_locationt & source_location() const
Definition: expr.h:125
void convert_msc_try_except(const codet &code, goto_programt &dest, const irep_idt &mode)
void unwind_destructor_stack(const source_locationt &, std::size_t stack_size, goto_programt &dest, const irep_idt &mode)
bool is_file_local
Definition: symbol.h:68
void convert_CPROVER_try_catch(const codet &code, goto_programt &dest, const irep_idt &mode)
virtual std::pair< symbolt &, bool > insert(symbolt symbol)=0
Move or copy a new symbol to the symbol table.
symbol_table_baset & symbol_table
void convert_CPROVER_try_finally(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)
source_locationt & add_source_location()
Definition: expr.h:130
const codet & to_code(const exprt &expr)
Definition: std_code.h:75
An if-then-else.
Definition: std_code.h:466
Expression to hold a symbol (variable)
Definition: std_expr.h:90
A statement in a programming language.
Definition: std_code.h:21
operandst & operands()
Definition: expr.h:66
exception_listt & exception_list()
Definition: std_code.h:1600
Assignment.
Definition: std_code.h:196
bool is_lvalue
Definition: symbol.h:68