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;
27  tmp.add_instruction(SKIP)->source_location=code.source_location();
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
35  targets.destructor_stack.push_back(to_code(code.op1()));
36 
37  // do 'try' code
38  convert(to_code(code.op0()), dest, mode);
39 
40  // pop 'finally' from destructor stack
41  targets.destructor_stack.pop_back();
42 
43  // 'leave' target gets restored here
44  }
45 
46  // now add 'finally' code
47  convert(to_code(code.op1()), dest, mode);
48 
49  // this is the target for 'leave'
50  dest.destructive_append(tmp);
51 }
52 
54  const codet &code,
55  goto_programt &dest,
56  const irep_idt &mode)
57 {
59  code.operands().size() == 3,
60  "msc_try_except expects three arguments",
61  code.find_source_location());
62 
63  convert(to_code(code.op0()), dest, mode);
64 
65  // todo: generate exception tracking
66 }
67 
69  const codet &code,
70  goto_programt &dest,
71  const irep_idt &mode)
72 {
74  targets.leave_set, "leave without target", code.find_source_location());
75 
76  // need to process destructor stack
77  for(std::size_t d=targets.destructor_stack.size();
79  d--)
80  {
81  codet d_code=targets.destructor_stack[d-1];
82  d_code.add_source_location()=code.source_location();
83  convert(d_code, dest, mode);
84  }
85 
87  t->make_goto(targets.leave_target);
88  t->source_location=code.source_location();
89 }
90 
92  const codet &code,
93  goto_programt &dest,
94  const irep_idt &mode)
95 {
97  code.operands().size() >= 2,
98  "try_catch expects at least two arguments",
99  code.find_source_location());
100 
101  // add the CATCH-push instruction to 'dest'
102  goto_programt::targett catch_push_instruction=dest.add_instruction();
103  catch_push_instruction->make_catch();
104  catch_push_instruction->source_location=code.source_location();
105 
106  code_push_catcht push_catch_code;
107 
108  // the CATCH-push instruction is annotated with a list of IDs,
109  // one per target
110  code_push_catcht::exception_listt &exception_list=
111  push_catch_code.exception_list();
112 
113  // add a SKIP target for the end of everything
114  goto_programt end;
115  goto_programt::targett end_target=end.add_instruction();
116  end_target->make_skip();
117 
118  // the first operand is the 'try' block
119  convert(to_code(code.op0()), dest, mode);
120 
121  // add the CATCH-pop to the end of the 'try' block
122  goto_programt::targett catch_pop_instruction=dest.add_instruction();
123  catch_pop_instruction->make_catch();
124  catch_pop_instruction->code=code_pop_catcht();
125 
126  // add a goto to the end of the 'try' block
127  dest.add_instruction()->make_goto(end_target);
128 
129  for(std::size_t i=1; i<code.operands().size(); i++)
130  {
131  const codet &block=to_code(code.operands()[i]);
132 
133  // grab the ID and add to CATCH instruction
134  exception_list.push_back(
135  code_push_catcht::exception_list_entryt(block.get(ID_exception_id)));
136 
137  goto_programt tmp;
138  convert(block, tmp, mode);
139  catch_push_instruction->targets.push_back(tmp.instructions.begin());
140  dest.destructive_append(tmp);
141 
142  // add a goto to the end of the 'catch' block
143  dest.add_instruction()->make_goto(end_target);
144  }
145 
146  catch_push_instruction->code=push_catch_code;
147 
148  // add the end-target
149  dest.destructive_append(end);
150 }
151 
153  const codet &code,
154  goto_programt &dest,
155  const irep_idt &mode)
156 {
158  code.operands().size() == 2,
159  "CPROVER_try_catch expects two arguments",
160  code.find_source_location());
161 
162  // this is where we go after 'throw'
163  goto_programt tmp;
164  tmp.add_instruction(SKIP)->source_location=code.source_location();
165 
166  // set 'throw' target
167  throw_targett throw_target(targets);
168  targets.set_throw(tmp.instructions.begin());
169 
170  // now put 'catch' code onto destructor stack
171  code_ifthenelset catch_code(exception_flag(), to_code(code.op1()));
172  catch_code.add_source_location()=code.source_location();
173 
174  targets.destructor_stack.push_back(std::move(catch_code));
175 
176  // now convert 'try' code
177  convert(to_code(code.op0()), dest, mode);
178 
179  // pop 'catch' code off stack
180  targets.destructor_stack.pop_back();
181 
182  // add 'throw' target
183  dest.destructive_append(tmp);
184 }
185 
187  const codet &code,
188  goto_programt &dest,
189  const irep_idt &mode)
190 {
191  // set the 'exception' flag
192  {
193  goto_programt::targett t_set_exception=
194  dest.add_instruction(ASSIGN);
195 
196  t_set_exception->source_location=code.source_location();
197  t_set_exception->code=code_assignt(exception_flag(), true_exprt());
198  }
199 
200  // do we catch locally?
201  if(targets.throw_set)
202  {
203  // need to process destructor stack
205  code.source_location(), targets.throw_stack_size, dest, mode);
206 
207  // add goto
209  t->make_goto(targets.throw_target);
210  t->source_location=code.source_location();
211  }
212  else // otherwise, we do a return
213  {
214  // need to process destructor stack
215  unwind_destructor_stack(code.source_location(), 0, dest, mode);
216 
217  // add goto
219  t->make_goto(targets.return_target);
220  t->source_location=code.source_location();
221  }
222 }
223 
225  const codet &code,
226  goto_programt &dest,
227  const irep_idt &mode)
228 {
230  code.operands().size() == 2,
231  "CPROVER_try_finally expects two arguments",
232  code.find_source_location());
233 
234  // first put 'finally' code onto destructor stack
235  targets.destructor_stack.push_back(to_code(code.op1()));
236 
237  // do 'try' code
238  convert(to_code(code.op0()), dest, mode);
239 
240  // pop 'finally' from destructor stack
241  targets.destructor_stack.pop_back();
242 
243  // now add 'finally' code
244  convert(to_code(code.op1()), dest, mode);
245 }
246 
248 {
249  irep_idt id="$exception_flag";
250 
251  symbol_tablet::symbolst::const_iterator s_it=
252  symbol_table.symbols.find(id);
253 
254  if(s_it==symbol_table.symbols.end())
255  {
256  symbolt new_symbol;
257  new_symbol.base_name="$exception_flag";
258  new_symbol.name=id;
259  new_symbol.is_lvalue=true;
260  new_symbol.is_thread_local=true;
261  new_symbol.is_file_local=false;
262  new_symbol.type=bool_typet();
263  symbol_table.insert(std::move(new_symbol));
264  }
265 
266  return symbol_exprt(id, bool_typet());
267 }
268 
270  const source_locationt &source_location,
271  std::size_t final_stack_size,
272  goto_programt &dest,
273  const irep_idt &mode)
274 {
276  source_location, final_stack_size, dest, targets.destructor_stack, mode);
277 }
278 
280  const source_locationt &source_location,
281  std::size_t final_stack_size,
282  goto_programt &dest,
283  destructor_stackt &destructor_stack,
284  const irep_idt &mode)
285 {
286  // There might be exceptions happening in the exception
287  // handler. We thus pop off the stack, and then later
288  // one restore the original stack.
289  destructor_stackt old_stack=destructor_stack;
290 
291  while(destructor_stack.size()>final_stack_size)
292  {
293  codet d_code=destructor_stack.back();
294  d_code.add_source_location()=source_location;
295 
296  // pop now to avoid doing this again
297  destructor_stack.pop_back();
298 
299  convert(d_code, dest, mode);
300  }
301 
302  // Now restore old stack.
303  old_stack.swap(destructor_stack);
304 }
goto_convertt::exception_flag
symbol_exprt exception_flag()
Definition: goto_convert_exceptions.cpp:247
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
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
goto_convertt::targetst::leave_target
goto_programt::targett leave_target
Definition: goto_convert_class.h:382
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:425
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:224
goto_convertt::convert_try_catch
void convert_try_catch(const codet &code, goto_programt &dest, const irep_idt &mode)
Definition: goto_convert_exceptions.cpp:91
goto_convertt::targetst::throw_target
goto_programt::targett throw_target
Definition: goto_convert_class.h:382
goto_convert_class.h
goto_convertt::leave_targett
Definition: goto_convert_class.h:525
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:1845
goto_convertt::targetst::destructor_stack
destructor_stackt destructor_stack
Definition: goto_convert_class.h:377
exprt::op0
exprt & op0()
Definition: expr.h:84
goto_convertt::destructor_stackt
std::vector< codet > destructor_stackt
Definition: goto_convert_class.h:336
bool_typet
The Boolean type.
Definition: std_types.h:28
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:143
code_pop_catcht
Pops an exception handler from the stack of active handlers (i.e.
Definition: std_code.h:1933
goto_convertt::targetst::throw_set
bool throw_set
Definition: goto_convert_class.h:371
code_ifthenelset
codet representation of an if-then-else statement.
Definition: std_code.h:614
to_code
const codet & to_code(const exprt &expr)
Definition: std_code.h:136
goto_convertt::throw_targett
Definition: goto_convert_class.h:503
goto_convertt::targetst::set_leave
void set_leave(goto_programt::targett _leave_target)
Definition: goto_convert_class.h:436
goto_convertt::targetst::leave_set
bool leave_set
Definition: goto_convert_class.h:371
goto_programt::add_instruction
targett add_instruction()
Adds an instruction at the end.
Definition: goto_program.h:541
symbolt::is_thread_local
bool is_thread_local
Definition: symbol.h:65
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:152
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:414
goto_convertt::convert_CPROVER_throw
void convert_CPROVER_throw(const codet &code, goto_programt &dest, const irep_idt &mode)
Definition: goto_convert_exceptions.cpp:186
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:229
code_push_catcht::exception_list_entryt
Definition: std_code.h:1853
exprt::op1
exprt & op1()
Definition: expr.h:87
code_push_catcht::exception_list
exception_listt & exception_list()
Definition: std_code.h:1901
goto_convertt::targetst::set_throw
void set_throw(goto_programt::targett _throw_target)
Definition: goto_convert_class.h:429
SKIP
Definition: goto_program.h:38
goto_convertt::targetst::throw_stack_size
std::size_t throw_stack_size
Definition: goto_convert_class.h:385
goto_programt::destructive_append
void destructive_append(goto_programt &p)
Appends the given program p to *this. p is destroyed.
Definition: goto_program.h:524
source_locationt
Definition: source_location.h:20
goto_convertt::targets
struct goto_convertt::targetst targets
goto_programt::instructions
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:420
ASSIGN
Definition: goto_program.h:46
goto_convertt::convert_msc_leave
void convert_msc_leave(const codet &code, goto_programt &dest, const irep_idt &mode)
Definition: goto_convert_exceptions.cpp:68
irept::get
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:212
code_push_catcht::exception_listt
std::vector< exception_list_entryt > exception_listt
Definition: std_code.h:1890
symbolt
Symbol table entry.
Definition: symbol.h:27
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:53
symbol_table_baset::symbols
const symbolst & symbols
Definition: symbol_table_base.h:27
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:72
goto_convertt::unwind_destructor_stack
void unwind_destructor_stack(const source_locationt &, std::size_t stack_size, goto_programt &dest, const irep_idt &mode)
Definition: goto_convert_exceptions.cpp:269
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:47
symbolt::is_file_local
bool is_file_local
Definition: symbol.h:66
exprt::operands
operandst & operands()
Definition: expr.h:78
symbolt::is_lvalue
bool is_lvalue
Definition: symbol.h:66
goto_convertt::targetst::leave_stack_size
std::size_t leave_stack_size
Definition: goto_convert_class.h:385
exprt::add_source_location
source_locationt & add_source_location()
Definition: expr.h:233
code_assignt
A codet representing an assignment in the program.
Definition: std_code.h:256
true_exprt
The Boolean constant true.
Definition: std_expr.h:4443
std_expr.h
exprt::source_location
const source_locationt & source_location() const
Definition: expr.h:228
symbolt::name
irep_idt name
The unique identifier.
Definition: symbol.h:40
goto_programt::targett
instructionst::iterator targett
Definition: goto_program.h:414
codet
Data structure for representing an arbitrary statement in a program.
Definition: std_code.h:34
goto_convertt::targetst::return_target
goto_programt::targett return_target
Definition: goto_convert_class.h:382