@@ -143,6 +143,31 @@ class remove_function_pointerst
143
143
const goto_programt &goto_program,
144
144
functionst &functions,
145
145
const exprt &pointer);
146
+
147
+ // / From *fp() build
148
+ // / if (fp=&f1) then goto 1
149
+ // / if (fp=&f2) then goto 2
150
+ // / ..
151
+ // / 1: f1(); goto N+1;
152
+ // / 2: f2(); goto N+1;
153
+ // / ..
154
+ // / \param functions: set of function candidates
155
+ // / \param code: the original function call
156
+ // / \param function_id: name of the function
157
+ // / \param target: iterator to the target call-site
158
+ // / \return the GOTO program for the new code
159
+ goto_programt build_new_code (
160
+ const functionst &functions,
161
+ const code_function_callt &code,
162
+ const irep_idt &function_id,
163
+ goto_programt::targett target);
164
+
165
+ // / Log the statistics collected during this analysis
166
+ // / \param target: iterator to the target call-site
167
+ // / \param functions: the set of function candidates
168
+ void remove_function_pointer_log (
169
+ goto_programt::targett target,
170
+ const functionst &functions) const ;
146
171
};
147
172
148
173
remove_function_pointerst::remove_function_pointerst (
@@ -454,75 +479,9 @@ void remove_function_pointerst::remove_function_pointer(
454
479
const functionst &functions)
455
480
{
456
481
const code_function_callt &code = target->get_function_call ();
457
-
458
482
const exprt &function = code.function ();
459
- const exprt &pointer = to_dereference_expr (function).pointer ();
460
-
461
- // the final target is a skip
462
- goto_programt final_skip;
463
-
464
- goto_programt::targett t_final = final_skip.add (goto_programt::make_skip ());
465
-
466
- // build the calls and gotos
467
-
468
- goto_programt new_code_calls;
469
- goto_programt new_code_gotos;
470
-
471
- for (const auto &fun : functions)
472
- {
473
- // call function
474
- auto new_call = code;
475
- new_call.function () = fun;
476
483
477
- // the signature of the function might not match precisely
478
- fix_argument_types (new_call);
479
-
480
- goto_programt tmp;
481
- fix_return_type (function_id, new_call, tmp);
482
-
483
- auto call = new_code_calls.add (goto_programt::make_function_call (new_call));
484
- new_code_calls.destructive_append (tmp);
485
-
486
- // goto final
487
- new_code_calls.add (goto_programt::make_goto (t_final, true_exprt ()));
488
-
489
- // goto to call
490
- const address_of_exprt address_of (fun, pointer_type (fun.type ()));
491
-
492
- const auto casted_address =
493
- typecast_exprt::conditional_cast (address_of, pointer.type ());
494
-
495
- new_code_gotos.add (
496
- goto_programt::make_goto (call, equal_exprt (pointer, casted_address)));
497
- }
498
-
499
- // fall-through
500
- if (add_safety_assertion)
501
- {
502
- goto_programt::targett t =
503
- new_code_gotos.add (goto_programt::make_assertion (false_exprt ()));
504
- t->source_location .set_property_class (" pointer dereference" );
505
- t->source_location .set_comment (" invalid function pointer" );
506
- }
507
-
508
- goto_programt new_code;
509
-
510
- // patch them all together
511
- new_code.destructive_append (new_code_gotos);
512
- new_code.destructive_append (new_code_calls);
513
- new_code.destructive_append (final_skip);
514
-
515
- // set locations
516
- Forall_goto_program_instructions (it, new_code)
517
- {
518
- irep_idt property_class=it->source_location .get_property_class ();
519
- irep_idt comment=it->source_location .get_comment ();
520
- it->source_location =target->source_location ;
521
- if (!property_class.empty ())
522
- it->source_location .set_property_class (property_class);
523
- if (!comment.empty ())
524
- it->source_location .set_comment (comment);
525
- }
484
+ goto_programt new_code = build_new_code (functions, code, function_id, target);
526
485
527
486
goto_programt::targett next_target=target;
528
487
next_target++;
@@ -537,27 +496,7 @@ void remove_function_pointerst::remove_function_pointer(
537
496
target->type =OTHER;
538
497
539
498
// report statistics
540
- log.statistics ().source_location = target->source_location ;
541
- log.statistics () << " replacing function pointer by " << functions.size ()
542
- << " possible targets" << messaget::eom;
543
-
544
- // list the names of functions when verbosity is at debug level
545
- log.conditional_output (
546
- log.debug (), [&functions](messaget::mstreamt &mstream) {
547
- mstream << " targets: " ;
548
-
549
- bool first = true ;
550
- for (const auto &function : functions)
551
- {
552
- if (!first)
553
- mstream << " , " ;
554
-
555
- mstream << function.get_identifier ();
556
- first = false ;
557
- }
558
-
559
- mstream << messaget::eom;
560
- });
499
+ remove_function_pointer_log (target, functions);
561
500
}
562
501
563
502
bool remove_function_pointerst::remove_function_pointers (
@@ -685,3 +624,100 @@ possible_fp_targets_mapt get_function_pointer_targets(
685
624
}
686
625
return target_map;
687
626
}
627
+
628
+ goto_programt remove_function_pointerst::build_new_code (
629
+ const functionst &functions,
630
+ const code_function_callt &code,
631
+ const irep_idt &function_id,
632
+ goto_programt::targett target)
633
+ {
634
+ // the final target is a skip
635
+ goto_programt final_skip;
636
+ const exprt &pointer = to_dereference_expr (code.function ()).pointer ();
637
+ goto_programt::targett t_final = final_skip.add (goto_programt::make_skip ());
638
+
639
+ goto_programt new_code_calls;
640
+ goto_programt new_code_gotos;
641
+ for (const auto &function : functions)
642
+ {
643
+ // call function
644
+ auto new_call = code;
645
+
646
+ new_call.function () = function;
647
+
648
+ // the signature of the function might not match precisely
649
+ fix_argument_types (new_call);
650
+
651
+ goto_programt tmp;
652
+ fix_return_type (function_id, new_call, tmp);
653
+
654
+ auto call = new_code_calls.add (goto_programt::make_function_call (new_call));
655
+ new_code_calls.destructive_append (tmp);
656
+
657
+ // goto final
658
+ new_code_calls.add (goto_programt::make_goto (t_final, true_exprt{}));
659
+
660
+ // goto to call
661
+ const auto casted_address = typecast_exprt::conditional_cast (
662
+ address_of_exprt{function, pointer_type (function.type ())},
663
+ pointer.type ());
664
+
665
+ const auto goto_it = new_code_gotos.add (
666
+ goto_programt::make_goto (call, equal_exprt{pointer, casted_address}));
667
+
668
+ // set locations for the above goto
669
+ irep_idt property_class = goto_it->source_location .get_property_class ();
670
+ irep_idt comment = goto_it->source_location .get_comment ();
671
+ goto_it->source_location = target->source_location ;
672
+ if (!property_class.empty ())
673
+ goto_it->source_location .set_property_class (property_class);
674
+ if (!comment.empty ())
675
+ goto_it->source_location .set_comment (comment);
676
+ }
677
+ // return {std::move(new_code_calls), std::move(new_code_gotos)};
678
+
679
+ // fall-through
680
+ if (add_safety_assertion)
681
+ {
682
+ goto_programt::targett t =
683
+ new_code_gotos.add (goto_programt::make_assertion (false_exprt{}));
684
+ t->source_location .set_property_class (" pointer dereference" );
685
+ t->source_location .set_comment (" invalid function pointer" );
686
+ }
687
+
688
+ goto_programt new_code;
689
+
690
+ // patch them all together
691
+ new_code.destructive_append (new_code_gotos);
692
+ new_code.destructive_append (new_code_calls);
693
+ new_code.destructive_append (final_skip);
694
+
695
+ return new_code;
696
+ }
697
+
698
+ void remove_function_pointerst::remove_function_pointer_log (
699
+ goto_programt::targett target,
700
+ const functionst &functions) const
701
+ {
702
+ log.statistics ().source_location = target->source_location ;
703
+ log.statistics () << " replacing function pointer by " << functions.size ()
704
+ << " possible targets" << messaget::eom;
705
+
706
+ // list the names of functions when verbosity is at debug level
707
+ log.conditional_output (
708
+ log.debug (), [&functions](messaget::mstreamt &mstream) {
709
+ mstream << " targets: " ;
710
+
711
+ bool first = true ;
712
+ for (const auto &function : functions)
713
+ {
714
+ if (!first)
715
+ mstream << " , " ;
716
+
717
+ mstream << function.get_identifier ();
718
+ first = false ;
719
+ }
720
+
721
+ mstream << messaget::eom;
722
+ });
723
+ }
0 commit comments