Skip to content

Commit d58e578

Browse files
committed
Export additional interface for remove-function-pointers
that takes the target map as argument. To avoid duplication we also refactor the existing functions a bit.
1 parent 759b7f3 commit d58e578

File tree

2 files changed

+108
-37
lines changed

2 files changed

+108
-37
lines changed

src/goto-programs/remove_function_pointers.cpp

Lines changed: 89 additions & 37 deletions
Original file line numberDiff line numberDiff line change
@@ -38,35 +38,45 @@ class remove_function_pointerst
3838
bool only_resolve_const_fps,
3939
const goto_functionst &goto_functions);
4040

41-
void operator()(goto_functionst &goto_functions);
42-
41+
/// Call the function pointer removal via an operator
42+
/// \param goto_functions: functions to modify
43+
/// \param target_map: candidate functions
44+
void operator()(
45+
goto_functionst &goto_functions,
46+
const possible_fp_targets_mapt &target_map);
47+
48+
/// Call the function pointer removal within the \p goto_program
49+
/// \param goto_program: program to modify
50+
/// \param function_id: identifier of the function pointer to be removed
51+
/// \param target_map: candidate functions
4352
bool remove_function_pointers(
4453
goto_programt &goto_program,
45-
const irep_idt &function_id);
54+
const irep_idt &function_id,
55+
const possible_fp_targets_mapt &target_map);
4656

4757
// a set of function symbols
4858
using functionst = remove_const_function_pointerst::functionst;
4959

5060
/// Replace a call to a dynamic function at location
51-
/// target in the given goto-program by a case-split
61+
/// \p target in the given goto-program by a case-split
5262
/// over a given set of functions
5363
/// \param goto_program: The goto program that contains target
5464
/// \param function_id: Name of function containing the target
5565
/// \param target: location with function call with function pointer
56-
/// \param functions: The set of functions to consider
57-
void remove_function_pointer(
66+
/// \param functions: the set of functions to consider
67+
void remove_function_pointer_non_const(
5868
goto_programt &goto_program,
5969
const irep_idt &function_id,
6070
goto_programt::targett target,
6171
const functionst &functions);
6272

6373
/// Go through the whole model and find all potential function the pointer at
6474
/// \p call site may point to
65-
/// \param goto_model: model to search for potential functions
75+
/// \param goto_functions: goto functions to search for potential candidates
6676
/// \param call_site: the call site of the function pointer under analysis
6777
/// \return the set of the potential functions
6878
functionst get_function_pointer_targets(
69-
const goto_modelt &goto_model,
79+
const goto_functionst &goto_functions,
7080
goto_programt::const_targett &call_site);
7181

7282
/// Go through a single function body and find all potential function the
@@ -78,6 +88,13 @@ class remove_function_pointerst
7888
const goto_programt &goto_program,
7989
goto_programt::const_targett &call_site);
8090

91+
/// Go through the whole model and find all potential function the pointer at
92+
/// all call sites
93+
/// \param goto_functions: goto functions to search for potential candidates
94+
/// \return a map from ids to sets of function candidates
95+
possible_fp_targets_mapt
96+
get_function_pointer_targets(const goto_functionst &goto_functions);
97+
8198
protected:
8299
messaget log;
83100
const namespacet ns;
@@ -137,10 +154,12 @@ class remove_function_pointerst
137154
/// \param goto_program: The goto program that contains target
138155
/// \param function_id: Name of function containing the target
139156
/// \param target: location with function call with function pointer
140-
void remove_function_pointer(
157+
/// \param functions: the set of functions to consider
158+
void remove_function_pointer_const(
141159
goto_programt &goto_program,
142160
const irep_idt &function_id,
143-
goto_programt::targett target);
161+
goto_programt::targett target,
162+
const functionst &functions);
144163

145164
std::unordered_set<irep_idt> address_taken;
146165

@@ -173,10 +192,12 @@ class remove_function_pointerst
173192
/// \param goto_program: the function body to run the const_removal_check on
174193
/// \param functions: the list of functions the const removal found
175194
/// \param pointer: the pointer to be resolved
195+
/// \param callee_id: function id
176196
void try_remove_const_fp(
177197
const goto_programt &goto_program,
178198
functionst &functions,
179-
const exprt &pointer);
199+
const exprt &pointer,
200+
const irep_idt &callee_id);
180201

181202
/// From *fp() build the following sequence of instructions:
182203
///
@@ -424,11 +445,11 @@ void remove_function_pointerst::try_remove_const_fp(
424445

425446
remove_function_pointerst::functionst
426447
remove_function_pointerst::get_function_pointer_targets(
427-
const goto_modelt &goto_model,
448+
const goto_functionst &goto_functions,
428449
goto_programt::const_targett &call_site)
429450
{
430451
functionst functions;
431-
for(const auto &function_pair : goto_model.goto_functions.function_map)
452+
for(const auto &function_pair : goto_functions.function_map)
432453
{
433454
const auto &function_body = function_pair.second.body;
434455
const auto &candidates =
@@ -486,15 +507,12 @@ remove_function_pointerst::get_function_pointer_targets(
486507
return functions;
487508
}
488509

489-
void remove_function_pointerst::remove_function_pointer(
510+
void remove_function_pointerst::remove_function_pointer_const(
490511
goto_programt &goto_program,
491512
const irep_idt &function_id,
492-
goto_programt::targett target)
513+
goto_programt::targett target,
514+
const functionst &functions)
493515
{
494-
goto_programt::const_targett const_target = target;
495-
const auto functions =
496-
get_function_pointer_targets(goto_program, const_target);
497-
498516
auto callee_id = get_callee_id(target->get_function_call().function());
499517
if(was_only_remove_const_function_pointers_called(callee_id))
500518
{
@@ -511,11 +529,12 @@ void remove_function_pointerst::remove_function_pointer(
511529
// Since we haven't found functions, we would now resort to
512530
// replacing the function pointer with any function with a valid signature
513531
// Since we don't want to do that, we abort.
514-
remove_function_pointer(goto_program, function_id, target, functions);
532+
remove_function_pointer_non_const(
533+
goto_program, function_id, target, functions);
515534
}
516535
}
517536

518-
void remove_function_pointerst::remove_function_pointer(
537+
void remove_function_pointerst::remove_function_pointer_non_const(
519538
goto_programt &goto_program,
520539
const irep_idt &function_id,
521540
goto_programt::targett target,
@@ -542,18 +561,23 @@ void remove_function_pointerst::remove_function_pointer(
542561

543562
bool remove_function_pointerst::remove_function_pointers(
544563
goto_programt &goto_program,
545-
const irep_idt &function_id)
564+
const irep_idt &function_id,
565+
const possible_fp_targets_mapt &target_map)
546566
{
547567
bool did_something=false;
548568

549569
Forall_goto_program_instructions(target, goto_program)
550570
if(target->is_function_call())
551571
{
552572
const code_function_callt &code = target->get_function_call();
573+
const auto &callee = code.function();
553574

554575
if(code.function().id()==ID_dereference)
555576
{
556-
remove_function_pointer(goto_program, function_id, target);
577+
auto callee_id = get_callee_id(callee);
578+
CHECK_RETURN(target_map.count(callee_id) > 0);
579+
remove_function_pointer_const(
580+
goto_program, function_id, target, target_map.at(callee_id));
557581
did_something=true;
558582
}
559583
}
@@ -564,18 +588,20 @@ bool remove_function_pointerst::remove_function_pointers(
564588
return did_something;
565589
}
566590

567-
void remove_function_pointerst::operator()(goto_functionst &functions)
591+
void remove_function_pointerst::operator()(
592+
goto_functionst &functions,
593+
const possible_fp_targets_mapt &target_map)
568594
{
569595
bool did_something=false;
570596

571-
for(goto_functionst::function_mapt::iterator f_it=
572-
functions.function_map.begin();
573-
f_it!=functions.function_map.end();
597+
for(goto_functionst::function_mapt::iterator f_it =
598+
functions.function_map.begin();
599+
f_it != functions.function_map.end();
574600
f_it++)
575601
{
576602
goto_programt &goto_program=f_it->second.body;
577603

578-
if(remove_function_pointers(goto_program, f_it->first))
604+
if(remove_function_pointers(goto_program, f_it->first, target_map))
579605
did_something=true;
580606
}
581607

@@ -600,7 +626,10 @@ bool remove_function_pointers(
600626
only_remove_const_fps,
601627
goto_functions);
602628

603-
return rfp.remove_function_pointers(goto_program, function_id);
629+
return rfp.remove_function_pointers(
630+
goto_program,
631+
function_id,
632+
rfp.get_function_pointer_targets(goto_functions));
604633
}
605634

606635
void remove_function_pointers(
@@ -618,7 +647,7 @@ void remove_function_pointers(
618647
only_remove_const_fps,
619648
goto_functions);
620649

621-
rfp(goto_functions);
650+
rfp(goto_functions, rfp.get_function_pointer_targets(goto_functions));
622651
}
623652

624653
void remove_function_pointers(message_handlert &_message_handler,
@@ -634,19 +663,28 @@ void remove_function_pointers(message_handlert &_message_handler,
634663
only_remove_const_fps);
635664
}
636665

637-
possible_fp_targets_mapt get_function_pointer_targets(
638-
message_handlert &message_handler,
639-
goto_modelt &goto_model)
666+
void remove_function_pointers(
667+
message_handlert &_message_handler,
668+
goto_modelt &goto_model,
669+
const possible_fp_targets_mapt &target_map,
670+
bool add_safety_assertion,
671+
bool only_remove_const_fps)
640672
{
641673
remove_function_pointerst rfp(
642-
message_handler,
674+
_message_handler,
643675
goto_model.symbol_table,
644-
false,
645-
false,
676+
add_safety_assertion,
677+
only_remove_const_fps,
646678
goto_model.goto_functions);
647679

680+
rfp(goto_model.goto_functions, target_map);
681+
}
682+
683+
possible_fp_targets_mapt
684+
remove_function_pointerst::get_function_pointer_targets(
685+
const goto_functionst &goto_functions)
686+
{
648687
possible_fp_targets_mapt target_map;
649-
const auto &goto_functions = goto_model.goto_functions;
650688
for(const auto &function_pair : goto_functions.function_map)
651689
{
652690
const auto &instructions = function_pair.second.body.instructions;
@@ -671,6 +709,20 @@ possible_fp_targets_mapt get_function_pointer_targets(
671709
return target_map;
672710
}
673711

712+
possible_fp_targets_mapt get_function_pointer_targets(
713+
message_handlert &message_handler,
714+
goto_modelt &goto_model)
715+
{
716+
remove_function_pointerst rfp(
717+
message_handler,
718+
goto_model.symbol_table,
719+
false,
720+
false,
721+
goto_model.goto_functions);
722+
723+
return rfp.get_function_pointer_targets(goto_model.goto_functions);
724+
}
725+
674726
goto_programt remove_function_pointerst::build_new_code(
675727
const functionst &functions,
676728
const code_function_callt &code,

src/goto-programs/remove_function_pointers.h

Lines changed: 19 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -29,6 +29,11 @@ class symbol_tablet;
2929
using possible_fp_targetst = remove_const_function_pointerst::functionst;
3030
using possible_fp_targets_mapt = std::map<irep_idt, possible_fp_targetst>;
3131

32+
/// Go through the whole model and find all potential function the pointer at
33+
/// all call sites
34+
/// \param message_handler: a message handler for reporting
35+
/// \param goto_model: model to search for potential functions
36+
/// \return a map from ids to sets of function candidates
3237
possible_fp_targets_mapt get_function_pointer_targets(
3338
message_handlert &message_handler,
3439
goto_modelt &goto_model);
@@ -41,6 +46,20 @@ void remove_function_pointers(
4146
bool add_safety_assertion,
4247
bool only_remove_const_fps=false);
4348

49+
/// Replace all calls to a dynamic function by a case-split over a given set of
50+
/// candidate functions
51+
/// \param _message_handler: a message handler for reporting
52+
/// \param goto_model: model to search for potential functions
53+
/// \param target_map: candidate functions
54+
/// \param add_safety_assertion: check that at least one function matches
55+
/// \param only_remove_const_fps: restrict the pointer remove to const
56+
void remove_function_pointers(
57+
message_handlert &_message_handler,
58+
goto_modelt &goto_model,
59+
const possible_fp_targets_mapt &target_map,
60+
bool add_safety_assertion,
61+
bool only_remove_const_fps = false);
62+
4463
void remove_function_pointers(
4564
message_handlert &_message_handler,
4665
symbol_tablet &symbol_table,

0 commit comments

Comments
 (0)