@@ -90,49 +90,53 @@ class remove_exceptionst
90
90
{
91
91
}
92
92
93
- void operator ()(
94
- goto_functionst &goto_functions);
93
+ void operator ()(goto_functionst &goto_functions);
95
94
96
95
protected:
97
96
symbol_tablet &symbol_table;
98
97
std::map<irep_idt, std::set<irep_idt>> &exceptions_map;
99
98
100
99
void add_exceptional_returns (
101
- const goto_functionst::function_mapt::iterator &);
100
+ const irep_idt &function_id,
101
+ goto_programt &goto_program);
102
102
103
103
void instrument_exception_handler (
104
- const goto_functionst::function_mapt::iterator &,
104
+ const irep_idt &function_id,
105
+ goto_programt &goto_program,
105
106
const goto_programt::targett &);
106
107
107
108
void add_exception_dispatch_sequence (
108
- const goto_functionst::function_mapt::iterator &,
109
+ const irep_idt &function_id,
110
+ goto_programt &goto_program,
109
111
const goto_programt::targett &instr_it,
110
112
const stack_catcht &stack_catch,
111
113
const std::vector<exprt> &locals);
112
114
113
115
void instrument_throw (
114
- const goto_functionst::function_mapt::iterator &,
116
+ const irep_idt &function_id,
117
+ goto_programt &goto_program,
115
118
const goto_programt::targett &,
116
119
const stack_catcht &,
117
120
const std::vector<exprt> &);
118
121
119
122
void instrument_function_call (
120
- const goto_functionst::function_mapt::iterator &,
123
+ const irep_idt &function_id,
124
+ goto_programt &goto_program,
121
125
const goto_programt::targett &,
122
126
const stack_catcht &,
123
127
const std::vector<exprt> &);
124
128
125
129
void instrument_exceptions (
126
- const goto_functionst::function_mapt::iterator &);
130
+ const irep_idt &function_id,
131
+ goto_programt &goto_program);
127
132
};
128
133
129
134
// / adds exceptional return variables for every function that may escape
130
135
// / exceptions
131
136
void remove_exceptionst::add_exceptional_returns (
132
- const goto_functionst::function_mapt::iterator &func_it)
137
+ const irep_idt &function_id,
138
+ goto_programt &goto_program)
133
139
{
134
- const irep_idt &function_id=func_it->first ;
135
- goto_programt &goto_program=func_it->second .body ;
136
140
137
141
auto maybe_symbol=symbol_table.lookup (function_id);
138
142
INVARIANT (maybe_symbol, " functions should be recorded in the symbol table" );
@@ -236,17 +240,17 @@ void remove_exceptionst::add_exceptional_returns(
236
240
// / Translates an exception landing-pad into instructions that copy the
237
241
// / in-flight exception pointer to a nominated expression, then clear the
238
242
// / in-flight exception (i.e. null the pointer), hence marking it caught.
239
- // / \param func_it: iterator pointing to the function containing this
240
- // / landingpad instruction
241
- // / \param instr_it [in, out]: iterator pointing to the landingpad instruction.
243
+ // / \param function_id: name of the function containing this landingpad
244
+ // / instruction
245
+ // / \param goto_program: body of the function containing this landingpad
246
+ // / instruction
247
+ // / \param instr_it: iterator pointing to the landingpad instruction.
242
248
// / Will be overwritten.
243
249
void remove_exceptionst::instrument_exception_handler (
244
- const goto_functionst::function_mapt::iterator &func_it,
250
+ const irep_idt &function_id,
251
+ goto_programt &goto_program,
245
252
const goto_programt::targett &instr_it)
246
253
{
247
- const irep_idt &function_id=func_it->first ;
248
- goto_programt &goto_program=func_it->second .body ;
249
-
250
254
PRECONDITION (instr_it->type ==CATCH);
251
255
252
256
// retrieve the exception variable
@@ -285,20 +289,19 @@ void remove_exceptionst::instrument_exception_handler(
285
289
// / if (exception instanceof ExnA) then goto handlerA
286
290
// / else if (exception instanceof ExnB) then goto handlerB
287
291
// / else goto universal_handler or (dead locals; function exit)
288
- // / \param func_it: iterator pointing to function instr_it belongs to
292
+ // / \param function_id: name of the function to which instr_it belongs
293
+ // / \param goto_program: body of the function to which instr_it belongs
289
294
// / \param instr_it: throw or call instruction that may be an
290
295
// / exception source
291
296
// / \param stack_catch: exception handlers currently registered
292
297
// / \param locals: local variables to kill on a function-exit edge
293
298
void remove_exceptionst::add_exception_dispatch_sequence (
294
- const goto_functionst::function_mapt::iterator &func_it,
299
+ const irep_idt &function_id,
300
+ goto_programt &goto_program,
295
301
const goto_programt::targett &instr_it,
296
302
const remove_exceptionst::stack_catcht &stack_catch,
297
303
const std::vector<exprt> &locals)
298
304
{
299
- const irep_idt &function_id=func_it->first ;
300
- goto_programt &goto_program=func_it->second .body ;
301
-
302
305
// Unless we have a universal exception handler, jump to end of function
303
306
// if not caught:
304
307
goto_programt::targett default_target=goto_program.get_end_function ();
@@ -360,10 +363,11 @@ void remove_exceptionst::add_exception_dispatch_sequence(
360
363
}
361
364
}
362
365
363
- // / instruments each throw with conditional GOTOS to the corresponding
366
+ // / instruments each throw with conditional GOTOS to the corresponding
364
367
// / exception handlers
365
368
void remove_exceptionst::instrument_throw (
366
- const goto_functionst::function_mapt::iterator &func_it,
369
+ const irep_idt &function_id,
370
+ goto_programt &goto_program,
367
371
const goto_programt::targett &instr_it,
368
372
const remove_exceptionst::stack_catcht &stack_catch,
369
373
const std::vector<exprt> &locals)
@@ -383,11 +387,11 @@ void remove_exceptionst::instrument_throw(
383
387
return ;
384
388
385
389
add_exception_dispatch_sequence (
386
- func_it , instr_it, stack_catch, locals);
390
+ function_id, goto_program , instr_it, stack_catch, locals);
387
391
388
392
// find the symbol where the thrown exception should be stored:
389
- const symbolt &exc_symbol=
390
- symbol_table.lookup_ref (id2string (func_it-> first )+ EXC_SUFFIX);
393
+ const symbolt &exc_symbol =
394
+ symbol_table.lookup_ref (id2string (function_id) + EXC_SUFFIX);
391
395
symbol_exprt exc_thrown=exc_symbol.symbol_expr ();
392
396
393
397
// add the assignment with the appropriate cast
@@ -401,16 +405,14 @@ void remove_exceptionst::instrument_throw(
401
405
// / instruments each function call that may escape exceptions with conditional
402
406
// / GOTOS to the corresponding exception handlers
403
407
void remove_exceptionst::instrument_function_call (
404
- const goto_functionst::function_mapt::iterator &func_it,
408
+ const irep_idt &function_id,
409
+ goto_programt &goto_program,
405
410
const goto_programt::targett &instr_it,
406
411
const stack_catcht &stack_catch,
407
412
const std::vector<exprt> &locals)
408
413
{
409
414
PRECONDITION (instr_it->type ==FUNCTION_CALL);
410
415
411
- goto_programt &goto_program=func_it->second .body ;
412
- const irep_idt &function_id=func_it->first ;
413
-
414
416
// save the address of the next instruction
415
417
goto_programt::targett next_it=instr_it;
416
418
next_it++;
@@ -430,7 +432,7 @@ void remove_exceptionst::instrument_function_call(
430
432
if (callee_inflight_exception && local_inflight_exception)
431
433
{
432
434
add_exception_dispatch_sequence (
433
- func_it , instr_it, stack_catch, locals);
435
+ function_id, goto_program , instr_it, stack_catch, locals);
434
436
435
437
const symbol_exprt callee_inflight_exception_expr=
436
438
callee_inflight_exception->symbol_expr ();
@@ -463,12 +465,12 @@ void remove_exceptionst::instrument_function_call(
463
465
// / handlers. Additionally, it re-computes the live-range of local variables in
464
466
// / order to add DEAD instructions.
465
467
void remove_exceptionst::instrument_exceptions (
466
- const goto_functionst::function_mapt::iterator &func_it)
468
+ const irep_idt &function_id,
469
+ goto_programt &goto_program)
467
470
{
468
471
stack_catcht stack_catch; // stack of try-catch blocks
469
472
std::vector<std::vector<exprt>> stack_locals; // stack of local vars
470
473
std::vector<exprt> locals;
471
- goto_programt &goto_program=func_it->second .body ;
472
474
473
475
if (goto_program.empty ())
474
476
return ;
@@ -486,7 +488,7 @@ void remove_exceptionst::instrument_exceptions(
486
488
// Is it an exception landing pad (start of a catch block)?
487
489
if (statement==ID_exception_landingpad)
488
490
{
489
- instrument_exception_handler (func_it , instr_it);
491
+ instrument_exception_handler (function_id, goto_program , instr_it);
490
492
}
491
493
// Is it a catch handler pop?
492
494
else if (statement==ID_pop_catch)
@@ -551,21 +553,23 @@ void remove_exceptionst::instrument_exceptions(
551
553
}
552
554
else if (instr_it->type ==THROW)
553
555
{
554
- instrument_throw (func_it, instr_it, stack_catch, locals);
556
+ instrument_throw (
557
+ function_id, goto_program, instr_it, stack_catch, locals);
555
558
}
556
559
else if (instr_it->type ==FUNCTION_CALL)
557
560
{
558
- instrument_function_call (func_it, instr_it, stack_catch, locals);
561
+ instrument_function_call (
562
+ function_id, goto_program, instr_it, stack_catch, locals);
559
563
}
560
564
}
561
565
}
562
566
563
567
void remove_exceptionst::operator ()(goto_functionst &goto_functions)
564
568
{
565
569
Forall_goto_functions (it, goto_functions)
566
- add_exceptional_returns (it);
570
+ add_exceptional_returns (it-> first , it-> second . body );
567
571
Forall_goto_functions (it, goto_functions)
568
- instrument_exceptions (it);
572
+ instrument_exceptions (it-> first , it-> second . body );
569
573
}
570
574
571
575
// / removes throws/CATCH-POP/CATCH-PUSH
@@ -583,7 +587,5 @@ void remove_exceptions(
583
587
// / removes throws/CATCH-POP/CATCH-PUSH
584
588
void remove_exceptions (goto_modelt &goto_model)
585
589
{
586
- remove_exceptions (
587
- goto_model.symbol_table ,
588
- goto_model.goto_functions );
590
+ remove_exceptions (goto_model.symbol_table , goto_model.goto_functions );
589
591
}
0 commit comments