Refactorings and cleanups for the function pointer restriction feature

Author: danpoe

doc/cprover-manual/restrict-function-pointer.md

@@ -142,7 +142,7 @@ nothing other than `nullfs`; But perhaps due to the logic being too complicated
 symex ends up being unable to figure this out, so in the call to `fs_open()` we
 end up branching on all functions matching the signature of
 `filesystem_t::open`, which could be quite a few functions within the program.
-Worst of all, if it's address is ever taken in the program, as far as the "dumb"
+Worst of all, if its address is ever taken in the program, as far as the "dumb"
 function pointer removal is concerned it could be `fs_open()` itself due to it
 having a matching signature, leading to symex being forced to follow a
 potentially infinite recursion until its unwind limit.
@@ -175,6 +175,6 @@ restrictions.
 
 **Note:** as of now, if something goes wrong during type checking (i.e. making
 sure that all function pointer replacements refer to functions in the symbol
-table that have the correct type), the error message will refer the command line
-option `--restrict-function-pointer` regardless of whether the restriction in
-question came from the command line or a file.
+table that have the correct type), the error message will refer to the command
+line option `--restrict-function-pointer` regardless of whether the restriction
+in question came from the command line or a file.

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -1867,7 +1867,7 @@ void goto_instrument_parse_optionst::help()
     " --no-caching                 disable caching of intermediate results during transitive function inlining\n" // NOLINT(*)
     " --log <file>                 log in json format which code segments were inlined, use with --function-inline\n" // NOLINT(*)
     " --remove-function-pointers   replace function pointers by case statement over function calls\n" // NOLINT(*)
-    RESTRICT_FUNCTION_POINTER_HELP
+    HELP_RESTRICT_FUNCTION_POINTER
     HELP_REMOVE_CALLS_NO_BODY
     HELP_REMOVE_CONST_FUNCTION_POINTERS
     " --add-library                add models of C library functions\n"

src/goto-programs/goto_program.h

@@ -1170,27 +1170,27 @@ struct pointee_address_equalt
 };
 
 template <typename GotoFunctionT, typename PredicateT, typename HandlerT>
-void for_each_goto_location_if(
+void for_each_instruction_if(
   GotoFunctionT &&goto_function,
   PredicateT predicate,
-  HandlerT handle)
+  HandlerT handler)
 {
   auto &&instructions = goto_function.body.instructions;
   for(auto it = instructions.begin(); it != instructions.end(); ++it)
   {
     if(predicate(it))
     {
-      handle(it);
+      handler(it);
     }
   }
 }
 
 template <typename GotoFunctionT, typename HandlerT>
-void for_each_goto_location(GotoFunctionT &&goto_function, HandlerT handle)
+void for_each_instruction(GotoFunctionT &&goto_function, HandlerT handler)
 {
   using iterator_t = decltype(goto_function.body.instructions.begin());
-  for_each_goto_location_if(
-    goto_function, [](const iterator_t &) { return true; }, handle);
+  for_each_instruction_if(
+    goto_function, [](const iterator_t &) { return true; }, handler);
 }
 
 #define forall_goto_program_instructions(it, program) \

src/goto-programs/label_function_pointer_call_sites.cpp

@@ -15,7 +15,7 @@ void label_function_pointer_call_sites(goto_modelt &goto_model)
   for(auto &goto_function : goto_model.goto_functions.function_map)
   {
     std::size_t function_pointer_call_counter = 0;
-    for_each_goto_location_if(
+    for_each_instruction_if(
       goto_function.second,
       [](const goto_programt::targett it) {
         return it->is_function_call() && can_cast_expr<dereference_exprt>(
@@ -28,22 +28,30 @@ void label_function_pointer_call_sites(goto_modelt &goto_model)
         auto const &source_location = function_call.source_location();
         auto const &goto_function_symbol_mode =
           goto_model.symbol_table.lookup_ref(goto_function.first).mode;
-        auto const new_symbol_name =
+
+        auto const call_site_symbol_name =
           irep_idt{id2string(goto_function.first) + ".function_pointer_call." +
                    std::to_string(++function_pointer_call_counter)};
+
+        // insert new function pointer variable into the symbol table
         goto_model.symbol_table.insert([&] {
           symbolt function_call_site_symbol{};
           function_call_site_symbol.name = function_call_site_symbol.base_name =
-            function_call_site_symbol.pretty_name = new_symbol_name;
+            function_call_site_symbol.pretty_name = call_site_symbol_name;
           function_call_site_symbol.type =
             function_pointer_dereference.pointer().type();
           function_call_site_symbol.location = function_call.source_location();
           function_call_site_symbol.is_lvalue = true;
           function_call_site_symbol.mode = goto_function_symbol_mode;
           return function_call_site_symbol;
         }());
+
         auto const new_function_pointer =
-          goto_model.symbol_table.lookup_ref(new_symbol_name).symbol_expr();
+          goto_model.symbol_table.lookup_ref(call_site_symbol_name)
+            .symbol_expr();
+
+        // add assignment to the new function pointer variable, followed by a
+        // call of the new variable
         auto const assign_instruction = goto_programt::make_assignment(
           code_assignt{new_function_pointer,
                        function_pointer_dereference.pointer()},

src/goto-programs/label_function_pointer_call_sites.h

@@ -21,9 +21,10 @@ Author: Diffblue Ltd.
 /// only need to be able to handle these two cases.
 ///
 /// It does this by replacing all CALL instructions to function pointers with an
-/// assignment to a function pointer variable with a name following the pattern
-/// [function_name].function_pointer_call.[N], where "N" is the nth call to a
-/// function pointer in the function "function_name".
+/// assignment to a new function pointer variable followed by a call to that new
+/// function pointer. The name of the introduced variable follows the pattern
+/// [function_name].function_pointer_call.[N], where N is the nth call to a
+/// function pointer in the function function_name.
 void label_function_pointer_call_sites(goto_modelt &goto_model);
 
 #endif // CPROVER_GOTO_PROGRAMS_LABEL_FUNCTION_POINTER_CALL_SITES_H