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 {
20  if(code.operands().size()!=2)
21  {
23  error() << "msc_try_finally expects two arguments" << eom;
24  throw 0;
25  }
26 
27  goto_programt tmp;
28  tmp.add_instruction(SKIP)->source_location=code.source_location();
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
36  targets.destructor_stack.push_back(to_code(code.op1()));
37 
38  // do 'try' code
39  convert(to_code(code.op0()), dest);
40 
41  // pop 'finally' from destructor stack
42  targets.destructor_stack.pop_back();
43 
44  // 'leave' target gets restored here
45  }
46 
47  // now add 'finally' code
48  convert(to_code(code.op1()), dest);
49 
50  // this is the target for 'leave'
51  dest.destructive_append(tmp);
52 }
53 
55  const codet &code,
56  goto_programt &dest)
57 {
58  if(code.operands().size()!=3)
59  {
61  error() << "msc_try_except expects three arguments" << eom;
62  throw 0;
63  }
64 
65  convert(to_code(code.op0()), dest);
66 
67  // todo: generate exception tracking
68 }
69 
71  const codet &code,
72  goto_programt &dest)
73 {
74  if(!targets.leave_set)
75  {
77  error() << "leave without target" << eom;
78  throw 0;
79  }
80 
81  // need to process destructor stack
82  for(std::size_t d=targets.destructor_stack.size();
84  d--)
85  {
86  codet d_code=targets.destructor_stack[d-1];
87  d_code.add_source_location()=code.source_location();
88  convert(d_code, dest);
89  }
90 
92  t->make_goto(targets.leave_target);
93  t->source_location=code.source_location();
94 }
95 
97  const codet &code,
98  goto_programt &dest)
99 {
100  assert(!code.operands().empty());
101 
102  // add the CATCH instruction to 'dest'
103  goto_programt::targett catch_instruction=dest.add_instruction();
104  catch_instruction->make_catch();
105  catch_instruction->code.set_statement(ID_catch);
106  catch_instruction->source_location=code.source_location();
107  catch_instruction->function=code.source_location().get_function();
108 
109  // the CATCH instruction is annotated with a list of exception IDs
110  const irept exceptions=code.op0().find(ID_exception_list);
111  if(exceptions.is_not_nil())
112  {
113  irept::subt exceptions_sub=exceptions.get_sub();
114  irept::subt &exception_list=
115  catch_instruction->code.add(ID_exception_list).get_sub();
116  exception_list.resize(exceptions_sub.size());
117  for(size_t i=0; i<exceptions_sub.size(); ++i)
118  exception_list[i].id(exceptions_sub[i].id());
119  }
120 
121  // the CATCH instruction is also annotated with a list of handle labels
122  const irept handlers=code.op0().find(ID_label);
123  if(handlers.is_not_nil())
124  {
125  irept::subt handlers_sub=handlers.get_sub();
126  irept::subt &handlers_list=
127  catch_instruction->code.add(ID_label).get_sub();
128  handlers_list.resize(handlers_sub.size());
129  for(size_t i=0; i<handlers_sub.size(); ++i)
130  handlers_list[i].id(handlers_sub[i].id());
131  }
132 
133  // the CATCH instruction may also signal a handler
134  if(code.op0().has_operands())
135  {
136  catch_instruction->code.get_sub().resize(1);
137  catch_instruction->code.get_sub()[0]=code.op0().op0();
138  }
139 
140  // add a SKIP target for the end of everything
141  goto_programt end;
142  goto_programt::targett end_target=end.add_instruction();
143  end_target->make_skip();
144  end_target->source_location=code.source_location();
145  end_target->function=code.source_location().get_function();
146 
147  // add the end-target
148  dest.destructive_append(end);
149 }
150 
152  const codet &code,
153  goto_programt &dest)
154 {
155  assert(code.operands().size()>=2);
156 
157  // add the CATCH-push instruction to 'dest'
158  goto_programt::targett catch_push_instruction=dest.add_instruction();
159  catch_push_instruction->make_catch();
160  catch_push_instruction->code.set_statement(ID_catch);
161  catch_push_instruction->source_location=code.source_location();
162 
163  // the CATCH-push instruction is annotated with a list of IDs,
164  // one per target
165  irept::subt &exception_list=
166  catch_push_instruction->code.add(ID_exception_list).get_sub();
167 
168  // add a SKIP target for the end of everything
169  goto_programt end;
170  goto_programt::targett end_target=end.add_instruction();
171  end_target->make_skip();
172 
173  // the first operand is the 'try' block
174  convert(to_code(code.op0()), dest);
175 
176  // add the CATCH-pop to the end of the 'try' block
177  goto_programt::targett catch_pop_instruction=dest.add_instruction();
178  catch_pop_instruction->make_catch();
179  catch_pop_instruction->code.set_statement(ID_catch);
180 
181  // add a goto to the end of the 'try' block
182  dest.add_instruction()->make_goto(end_target);
183 
184  for(unsigned i=1; i<code.operands().size(); i++)
185  {
186  const codet &block=to_code(code.operands()[i]);
187 
188  // grab the ID and add to CATCH instruction
189  exception_list.push_back(irept(block.get(ID_exception_id)));
190 
191  goto_programt tmp;
192  convert(block, tmp);
193  catch_push_instruction->targets.push_back(tmp.instructions.begin());
194  dest.destructive_append(tmp);
195 
196  // add a goto to the end of the 'catch' block
197  dest.add_instruction()->make_goto(end_target);
198  }
199 
200  // add the end-target
201  dest.destructive_append(end);
202 }
203 
205  const codet &code,
206  goto_programt &dest)
207 {
208  if(code.operands().size()!=2)
209  {
211  error() << "CPROVER_try_catch expects two arguments" << eom;
212  throw 0;
213  }
214 
215  // this is where we go after 'throw'
216  goto_programt tmp;
217  tmp.add_instruction(SKIP)->source_location=code.source_location();
218 
219  // set 'throw' target
220  throw_targett throw_target(targets);
221  targets.set_throw(tmp.instructions.begin());
222 
223  // now put 'catch' code onto destructor stack
224  code_ifthenelset catch_code;
225  catch_code.cond()=exception_flag();
226  catch_code.add_source_location()=code.source_location();
227  catch_code.then_case()=to_code(code.op1());
228 
229  targets.destructor_stack.push_back(catch_code);
230 
231  // now convert 'try' code
232  convert(to_code(code.op0()), dest);
233 
234  // pop 'catch' code off stack
235  targets.destructor_stack.pop_back();
236 
237  // add 'throw' target
238  dest.destructive_append(tmp);
239 }
240 
242  const codet &code,
243  goto_programt &dest)
244 {
245  // set the 'exception' flag
246  {
247  goto_programt::targett t_set_exception=
248  dest.add_instruction(ASSIGN);
249 
250  t_set_exception->source_location=code.source_location();
251  t_set_exception->code=code_assignt(exception_flag(), true_exprt());
252  }
253 
254  // do we catch locally?
255  if(targets.throw_set)
256  {
257  // need to process destructor stack
260 
261  // add goto
263  t->make_goto(targets.throw_target);
264  t->source_location=code.source_location();
265  }
266  else // otherwise, we do a return
267  {
268  // need to process destructor stack
269  unwind_destructor_stack(code.source_location(), 0, dest);
270 
271  // add goto
273  t->make_goto(targets.return_target);
274  t->source_location=code.source_location();
275  }
276 }
277 
279  const codet &code,
280  goto_programt &dest)
281 {
282  if(code.operands().size()!=2)
283  {
285  error() << "CPROVER_try_finally expects two arguments" << eom;
286  throw 0;
287  }
288 
289  // first put 'finally' code onto destructor stack
290  targets.destructor_stack.push_back(to_code(code.op1()));
291 
292  // do 'try' code
293  convert(to_code(code.op0()), dest);
294 
295  // pop 'finally' from destructor stack
296  targets.destructor_stack.pop_back();
297 
298  // now add 'finally' code
299  convert(to_code(code.op1()), dest);
300 }
301 
303 {
304  irep_idt id="$exception_flag";
305 
306  symbol_tablet::symbolst::const_iterator s_it=
307  symbol_table.symbols.find(id);
308 
309  if(s_it==symbol_table.symbols.end())
310  {
311  symbolt new_symbol;
312  new_symbol.base_name="$exception_flag";
313  new_symbol.name=id;
314  new_symbol.is_lvalue=true;
315  new_symbol.is_thread_local=true;
316  new_symbol.is_file_local=false;
317  new_symbol.type=bool_typet();
318  symbol_table.move(new_symbol);
319  }
320 
321  return symbol_exprt(id, bool_typet());
322 }
323 
325  const source_locationt &source_location,
326  std::size_t final_stack_size,
327  goto_programt &dest)
328 {
330  source_location,
331  final_stack_size,
332  dest,
334 }
335 
337  const source_locationt &source_location,
338  std::size_t final_stack_size,
339  goto_programt &dest,
340  destructor_stackt &destructor_stack)
341 {
342  // There might be exceptions happening in the exception
343  // handler. We thus pop off the stack, and then later
344  // one restore the original stack.
345  destructor_stackt old_stack=destructor_stack;
346 
347  while(destructor_stack.size()>final_stack_size)
348  {
349  codet d_code=destructor_stack.back();
350  d_code.add_source_location()=source_location;
351 
352  // pop now to avoid doing this again
353  destructor_stack.pop_back();
354 
355  convert(d_code, dest);
356  }
357 
358  // Now restore old stack.
359  old_stack.swap(destructor_stack);
360 }
irep_idt name
The unique identifier.
Definition: symbol.h:46
const codet & then_case() const
Definition: std_code.h:370
targett add_instruction()
Adds an instruction at the end.
bool is_not_nil() const
Definition: irep.h:104
void convert(const codet &code, goto_programt &dest)
converts &#39;code&#39; and appends the result to &#39;dest&#39;
bool is_thread_local
Definition: symbol.h:70
symbol_tablet & symbol_table
goto_programt::targett return_target
exprt & op0()
Definition: expr.h:84
void unwind_destructor_stack(const source_locationt &, std::size_t stack_size, goto_programt &dest)
std::vector< irept > subt
Definition: irep.h:91
struct goto_convertt::targetst targets
const exprt & cond() const
Definition: std_code.h:360
instructionst instructions
The list of instructions in the goto program.
const irep_idt & get_function() const
The proper Booleans.
Definition: std_types.h:33
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:33
static mstreamt & eom(mstreamt &m)
Definition: message.h:193
subt & get_sub()
Definition: irep.h:245
goto_programt::targett throw_target
destructor_stackt destructor_stack
The boolean constant true.
Definition: std_expr.h:3742
symbolst symbols
Definition: symbol_table.h:57
void convert_msc_try_finally(const codet &code, goto_programt &dest)
symbol_exprt exception_flag()
goto_programt::targett leave_target
const source_locationt & find_source_location() const
Definition: expr.cpp:466
source_locationt source_location
Definition: message.h:175
Program Transformation.
API to expression classes.
exprt & op1()
Definition: expr.h:87
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:213
void convert_CPROVER_try_finally(const codet &code, goto_programt &dest)
Base class for tree-like data structures with sharing.
Definition: irep.h:87
void convert_msc_leave(const codet &code, goto_programt &dest)
bool move(symbolt &symbol, symbolt *&new_symbol)
Move a symbol into the symbol table.
bool has_operands() const
Definition: expr.h:67
A specialization of goto_program_templatet over goto programs in which instructions have codet type...
Definition: goto_program.h:24
void convert_CPROVER_try_catch(const codet &code, goto_programt &dest)
void convert_java_try_catch(const codet &code, goto_programt &dest)
typet type
Type of symbol.
Definition: symbol.h:37
std::vector< codet > destructor_stackt
void convert_try_catch(const codet &code, goto_programt &dest)
void set_leave(goto_programt::targett _leave_target)
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:52
void set_throw(goto_programt::targett _throw_target)
const source_locationt & source_location() const
Definition: expr.h:142
bool is_file_local
Definition: symbol.h:71
irept & add(const irep_namet &name)
Definition: irep.cpp:306
mstreamt & error()
Definition: message.h:223
source_locationt & add_source_location()
Definition: expr.h:147
const codet & to_code(const exprt &expr)
Definition: std_code.h:49
An if-then-else.
Definition: std_code.h:350
Expression to hold a symbol (variable)
Definition: std_expr.h:82
void destructive_append(goto_program_templatet< codeT, guardT > &p)
Appends the given program, which is destroyed.
A statement in a programming language.
Definition: std_code.h:19
void convert_msc_try_except(const codet &code, goto_programt &dest)
operandst & operands()
Definition: expr.h:70
const irept & find(const irep_namet &name) const
Definition: irep.cpp:285
Assignment.
Definition: std_code.h:144
void convert_CPROVER_throw(const codet &code, goto_programt &dest)
bool is_lvalue
Definition: symbol.h:71