@@ -140,6 +140,16 @@ class remove_function_pointerst
140
140
const goto_programt &goto_program,
141
141
functionst &functions,
142
142
const exprt &pointer);
143
+
144
+ goto_programt build_new_code (
145
+ const functionst &functions,
146
+ const code_function_callt &code,
147
+ const irep_idt &function_id,
148
+ goto_programt::targett target);
149
+
150
+ void remove_function_pointer_log (
151
+ goto_programt::targett target,
152
+ const functionst &functions) const ;
143
153
};
144
154
145
155
remove_function_pointerst::remove_function_pointerst (
@@ -444,75 +454,9 @@ void remove_function_pointerst::remove_function_pointer(
444
454
const functionst &functions)
445
455
{
446
456
const code_function_callt &code = target->get_function_call ();
447
-
448
457
const exprt &function = code.function ();
449
- const exprt &pointer = to_dereference_expr (function).pointer ();
450
-
451
- // the final target is a skip
452
- goto_programt final_skip;
453
-
454
- goto_programt::targett t_final = final_skip.add (goto_programt::make_skip ());
455
-
456
- // build the calls and gotos
457
-
458
- goto_programt new_code_calls;
459
- goto_programt new_code_gotos;
460
-
461
- for (const auto &fun : functions)
462
- {
463
- // call function
464
- auto new_call = code;
465
- new_call.function () = fun;
466
458
467
- // the signature of the function might not match precisely
468
- fix_argument_types (new_call);
469
-
470
- goto_programt tmp;
471
- fix_return_type (function_id, new_call, tmp);
472
-
473
- auto call = new_code_calls.add (goto_programt::make_function_call (new_call));
474
- new_code_calls.destructive_append (tmp);
475
-
476
- // goto final
477
- new_code_calls.add (goto_programt::make_goto (t_final, true_exprt ()));
478
-
479
- // goto to call
480
- const address_of_exprt address_of (fun, pointer_type (fun.type ()));
481
-
482
- const auto casted_address =
483
- typecast_exprt::conditional_cast (address_of, pointer.type ());
484
-
485
- new_code_gotos.add (
486
- goto_programt::make_goto (call, equal_exprt (pointer, casted_address)));
487
- }
488
-
489
- // fall-through
490
- if (add_safety_assertion)
491
- {
492
- goto_programt::targett t =
493
- new_code_gotos.add (goto_programt::make_assertion (false_exprt ()));
494
- t->source_location .set_property_class (" pointer dereference" );
495
- t->source_location .set_comment (" invalid function pointer" );
496
- }
497
-
498
- goto_programt new_code;
499
-
500
- // patch them all together
501
- new_code.destructive_append (new_code_gotos);
502
- new_code.destructive_append (new_code_calls);
503
- new_code.destructive_append (final_skip);
504
-
505
- // set locations
506
- Forall_goto_program_instructions (it, new_code)
507
- {
508
- irep_idt property_class=it->source_location .get_property_class ();
509
- irep_idt comment=it->source_location .get_comment ();
510
- it->source_location =target->source_location ;
511
- if (!property_class.empty ())
512
- it->source_location .set_property_class (property_class);
513
- if (!comment.empty ())
514
- it->source_location .set_comment (comment);
515
- }
459
+ goto_programt new_code = build_new_code (functions, code, function_id, target);
516
460
517
461
goto_programt::targett next_target=target;
518
462
next_target++;
@@ -527,27 +471,7 @@ void remove_function_pointerst::remove_function_pointer(
527
471
target->type =OTHER;
528
472
529
473
// report statistics
530
- log.statistics ().source_location = target->source_location ;
531
- log.statistics () << " replacing function pointer by " << functions.size ()
532
- << " possible targets" << messaget::eom;
533
-
534
- // list the names of functions when verbosity is at debug level
535
- log.conditional_output (
536
- log.debug (), [&functions](messaget::mstreamt &mstream) {
537
- mstream << " targets: " ;
538
-
539
- bool first = true ;
540
- for (const auto &function : functions)
541
- {
542
- if (!first)
543
- mstream << " , " ;
544
-
545
- mstream << function.get_identifier ();
546
- first = false ;
547
- }
548
-
549
- mstream << messaget::eom;
550
- });
474
+ remove_function_pointer_log (target, functions);
551
475
}
552
476
553
477
bool remove_function_pointerst::remove_function_pointers (
@@ -675,3 +599,100 @@ possible_fp_targets_mapt get_function_pointer_targets(
675
599
}
676
600
return target_map;
677
601
}
602
+
603
+ goto_programt remove_function_pointerst::build_new_code (
604
+ const functionst &functions,
605
+ const code_function_callt &code,
606
+ const irep_idt &function_id,
607
+ goto_programt::targett target)
608
+ {
609
+ // the final target is a skip
610
+ goto_programt final_skip;
611
+ const exprt &pointer = to_dereference_expr (code.function ()).pointer ();
612
+ goto_programt::targett t_final = final_skip.add (goto_programt::make_skip ());
613
+
614
+ goto_programt new_code_calls;
615
+ goto_programt new_code_gotos;
616
+ for (const auto &function : functions)
617
+ {
618
+ // call function
619
+ auto new_call = code;
620
+
621
+ new_call.function () = function;
622
+
623
+ // the signature of the function might not match precisely
624
+ fix_argument_types (new_call);
625
+
626
+ goto_programt tmp;
627
+ fix_return_type (function_id, new_call, tmp);
628
+
629
+ auto call = new_code_calls.add (goto_programt::make_function_call (new_call));
630
+ new_code_calls.destructive_append (tmp);
631
+
632
+ // goto final
633
+ new_code_calls.add (goto_programt::make_goto (t_final, true_exprt{}));
634
+
635
+ // goto to call
636
+ const auto casted_address = typecast_exprt::conditional_cast (
637
+ address_of_exprt{function, pointer_type (function.type ())},
638
+ pointer.type ());
639
+
640
+ const auto goto_it = new_code_gotos.add (
641
+ goto_programt::make_goto (call, equal_exprt{pointer, casted_address}));
642
+
643
+ // set locations for the above goto
644
+ irep_idt property_class = goto_it->source_location .get_property_class ();
645
+ irep_idt comment = goto_it->source_location .get_comment ();
646
+ goto_it->source_location = target->source_location ;
647
+ if (!property_class.empty ())
648
+ goto_it->source_location .set_property_class (property_class);
649
+ if (!comment.empty ())
650
+ goto_it->source_location .set_comment (comment);
651
+ }
652
+ // return {std::move(new_code_calls), std::move(new_code_gotos)};
653
+
654
+ // fall-through
655
+ if (add_safety_assertion)
656
+ {
657
+ goto_programt::targett t =
658
+ new_code_gotos.add (goto_programt::make_assertion (false_exprt{}));
659
+ t->source_location .set_property_class (" pointer dereference" );
660
+ t->source_location .set_comment (" invalid function pointer" );
661
+ }
662
+
663
+ goto_programt new_code;
664
+
665
+ // patch them all together
666
+ new_code.destructive_append (new_code_gotos);
667
+ new_code.destructive_append (new_code_calls);
668
+ new_code.destructive_append (final_skip);
669
+
670
+ return new_code;
671
+ }
672
+
673
+ void remove_function_pointerst::remove_function_pointer_log (
674
+ goto_programt::targett target,
675
+ const functionst &functions) const
676
+ {
677
+ log.statistics ().source_location = target->source_location ;
678
+ log.statistics () << " replacing function pointer by " << functions.size ()
679
+ << " possible targets" << messaget::eom;
680
+
681
+ // list the names of functions when verbosity is at debug level
682
+ log.conditional_output (
683
+ log.debug (), [&functions](messaget::mstreamt &mstream) {
684
+ mstream << " targets: " ;
685
+
686
+ bool first = true ;
687
+ for (const auto &function : functions)
688
+ {
689
+ if (!first)
690
+ mstream << " , " ;
691
+
692
+ mstream << function.get_identifier ();
693
+ first = false ;
694
+ }
695
+
696
+ mstream << messaget::eom;
697
+ });
698
+ }
0 commit comments