30
30
#include " compute_called_functions.h"
31
31
#include " remove_const_function_pointers.h"
32
32
33
+ #define UNKNOWN_ASSIGN " ##unknown##"
34
+
33
35
class remove_function_pointerst
34
36
{
35
37
public:
@@ -67,6 +69,11 @@ class remove_function_pointerst
67
69
const namespacet ns;
68
70
symbol_tablet &symbol_table;
69
71
bool add_safety_assertion;
72
+ std::map<irep_idt, std::unordered_set<irep_idt>> function_pointer_map;
73
+ // counters to provide detailed statistics
74
+ std::size_t number_of_function_pointers_replaced = 0 ;
75
+ std::size_t max_size_of_case_split = 0 ;
76
+ std::size_t total_number_of_replacement_candidates = 0 ;
70
77
71
78
// We can optionally halt the FP removal if we aren't able to use
72
79
// remove_const_function_pointerst to successfully narrow to a small
@@ -106,8 +113,22 @@ class remove_function_pointerst
106
113
const irep_idt &in_function_id,
107
114
code_function_callt &function_call,
108
115
goto_programt &dest);
116
+
117
+ // / Scans through goto functions and builds a map of function
118
+ // / pointers to a set of functions that have been written to each pointer,
119
+ // / stored as irep_idts.
120
+ // / The map is stored as variable in remove_function_pointerst
121
+ // / \param goto_functions: goto functions to scan through
122
+ void gather_all_writes_to_function_pointers (goto_functionst &goto_functions);
109
123
};
110
124
125
+ static irep_idt get_member_identifier (const member_exprt &member)
126
+ {
127
+ // we only expect member expressions that have a symbol as compound operand
128
+ return id2string (to_symbol_expr (member.compound ()).get_identifier ()) + " ." +
129
+ id2string (member.get_component_name ());
130
+ }
131
+
111
132
remove_function_pointerst::remove_function_pointerst (
112
133
message_handlert &_message_handler,
113
134
symbol_tablet &_symbol_table,
@@ -361,19 +382,43 @@ void remove_function_pointerst::remove_function_pointer(
361
382
}
362
383
}
363
384
364
- remove_function_pointer (goto_program, function_id, target, functions);
365
- }
385
+ // we only handle cases where the LHS is a symbol or a member of a struct
386
+ if (pointer.id () == ID_symbol || pointer.id () == ID_member)
387
+ {
388
+ irep_idt identifier;
389
+ if (pointer.id () == ID_symbol)
390
+ {
391
+ identifier =
392
+ to_symbol_expr (to_dereference_expr (code.function ()).pointer ())
393
+ .get_identifier ();
394
+ }
395
+ else
396
+ {
397
+ identifier = get_member_identifier (to_member_expr (pointer));
398
+ }
366
399
367
- void remove_function_pointerst::remove_function_pointer (
368
- goto_programt &goto_program,
369
- const irep_idt &function_id,
370
- goto_programt::targett target,
371
- const functionst &functions)
372
- {
373
- const code_function_callt &code = target->get_function_call ();
400
+ auto entry = function_pointer_map.find (identifier);
401
+ if (entry != function_pointer_map.end ())
402
+ {
403
+ log.status () << " Replacing function pointer from map of possible assigns"
404
+ << messaget::eom;
374
405
375
- const exprt &function = code.function ();
376
- const exprt &pointer = to_dereference_expr (function).pointer ();
406
+ if (entry->second .find (UNKNOWN_ASSIGN) == entry->second .end ())
407
+ {
408
+ for (auto func_itr = functions.begin (); func_itr != functions.end ();)
409
+ {
410
+ if (
411
+ entry->second .find (func_itr->get_identifier ()) ==
412
+ entry->second .end ())
413
+ {
414
+ func_itr = functions.erase (func_itr);
415
+ }
416
+ else
417
+ func_itr++;
418
+ }
419
+ }
420
+ }
421
+ }
377
422
378
423
// the final target is a skip
379
424
goto_programt final_skip;
@@ -457,6 +502,10 @@ void remove_function_pointerst::remove_function_pointer(
457
502
log.statistics ().source_location = target->source_location ;
458
503
log.statistics () << " replacing function pointer by " << functions.size ()
459
504
<< " possible targets" << messaget::eom;
505
+ number_of_function_pointers_replaced++;
506
+ total_number_of_replacement_candidates += functions.size ();
507
+ if (functions.size () > max_size_of_case_split)
508
+ max_size_of_case_split = functions.size ();
460
509
461
510
// list the names of functions when verbosity is at debug level
462
511
log.conditional_output (
@@ -503,6 +552,7 @@ bool remove_function_pointerst::remove_function_pointers(
503
552
504
553
void remove_function_pointerst::operator ()(goto_functionst &functions)
505
554
{
555
+ gather_all_writes_to_function_pointers (functions);
506
556
bool did_something=false ;
507
557
508
558
for (goto_functionst::function_mapt::iterator f_it=
@@ -517,7 +567,21 @@ void remove_function_pointerst::operator()(goto_functionst &functions)
517
567
}
518
568
519
569
if (did_something)
570
+ {
520
571
functions.compute_location_numbers ();
572
+
573
+ log.statistics () << " Statistics:\n "
574
+ << " Replaced " << number_of_function_pointers_replaced
575
+ << " function pointers "
576
+ << " with " << total_number_of_replacement_candidates
577
+ << " possible candidate functions. \n "
578
+ << " Max number of candidates in a single replacement: "
579
+ << max_size_of_case_split << " \n "
580
+ << " Mean number of candidates in a single replacement: "
581
+ << total_number_of_replacement_candidates /
582
+ number_of_function_pointers_replaced
583
+ << messaget::eom;
584
+ }
521
585
}
522
586
523
587
bool remove_function_pointers (
@@ -570,3 +634,44 @@ void remove_function_pointers(message_handlert &_message_handler,
570
634
add_safety_assertion,
571
635
only_remove_const_fps);
572
636
}
637
+
638
+ void remove_function_pointerst::gather_all_writes_to_function_pointers (
639
+ goto_functionst &goto_functions)
640
+ {
641
+ for (auto &gf_entry : goto_functions.function_map )
642
+ {
643
+ goto_programt &goto_program = gf_entry.second .body ;
644
+ Forall_goto_program_instructions (target, goto_program)
645
+ {
646
+ if (!target->is_assign ())
647
+ continue ;
648
+
649
+ const code_assignt &code_assign = to_code_assign (target->code );
650
+ const auto &lhs = code_assign.lhs ();
651
+ const auto &rhs = code_assign.rhs ();
652
+
653
+ if (lhs.type ().id () == ID_pointer && lhs.type ().subtype ().id () == ID_code)
654
+ {
655
+ irep_idt lhs_identifier;
656
+ if (lhs.id () == ID_symbol)
657
+ lhs_identifier = to_symbol_expr (lhs).get_identifier ();
658
+ else if (lhs.id () == ID_member)
659
+ {
660
+ lhs_identifier = get_member_identifier (to_member_expr (lhs));
661
+ }
662
+ else
663
+ continue ;
664
+
665
+ if (rhs.id () == ID_address_of && rhs.type ().subtype ().id () == ID_code)
666
+ {
667
+ irep_idt rhs_identifier =
668
+ to_symbol_expr (to_address_of_expr (rhs).object ()).get_identifier ();
669
+
670
+ function_pointer_map[lhs_identifier].insert (rhs_identifier);
671
+ }
672
+ else
673
+ function_pointer_map[lhs_identifier] = {{UNKNOWN_ASSIGN}};
674
+ }
675
+ }
676
+ }
677
+ }
0 commit comments