Some cleanup for the function pointer restriction feature

Author: danpoe

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

@@ -135,7 +135,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.
@@ -168,6 +168,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>(

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

src/goto-programs/restrict_function_pointers.cpp

@@ -103,15 +103,15 @@ source_locationt make_function_pointer_restriction_assertion_source_location(
     }
     comment << ']';
   }
-  source_location.set_comment(string2id(comment.str()));
+  source_location.set_comment(comment.str());
   source_location.set_property_class(ID_assertion);
   return source_location;
 }
 
 template <typename Handler>
 void for_each_function_call(goto_functiont &goto_function, Handler handler)
 {
-  for_each_goto_location_if(
+  for_each_instruction_if(
     goto_function,
     [](goto_programt::targett target) { return target->is_function_call(); },
     handler);
@@ -148,9 +148,10 @@ void restrict_function_pointers(
           if(restriction_iterator != restrictions.restrictions.end())
           {
             auto const &restriction = *restriction_iterator;
-            // if we can, we will replace uses of it by the
-            // this is intentionally a copy because we're just about to change
-            // the instruction this iterator points to
+            // this is intentionally a copy because we're about to change the
+            // instruction this iterator points to
+            // if we can, we will replace uses of it by a case distinction over
+            // given functions the function pointer can point to
             auto const original_function_call_instruction = *location;
             *location = goto_programt::make_assertion(
               false_exprt{},
@@ -279,15 +280,10 @@ parse_function_pointer_restrictions_from_command_line(
         "--" RESTRICT_FUNCTION_POINTER_OPT,
         restriction_format_message};
     }
-    auto const target_names = ([&target_name_strings] {
-      auto target_names = std::unordered_set<irep_idt>{};
-      std::transform(
-        target_name_strings.begin(),
-        target_name_strings.end(),
-        std::inserter(target_names, target_names.end()),
-        string2id);
-      return target_names;
-    })();
+
+    std::unordered_set<irep_idt> target_names;
+    target_names.insert(target_name_strings.begin(), target_name_strings.end());
+
     for(auto const &target_name : target_names)
     {
       if(target_name == ID_empty_string)

src/goto-programs/restrict_function_pointers.h

@@ -31,11 +31,10 @@ Author: Diffblue Ltd.
   "function-pointer-restrictions-file"
 
 #define OPT_RESTRICT_FUNCTION_POINTER                                          \
-  "(" RESTRICT_FUNCTION_POINTER_OPT                                            \
-  "):"                                                                         \
+  "(" RESTRICT_FUNCTION_POINTER_OPT "):"                                       \
   "(" RESTRICT_FUNCTION_POINTER_FROM_FILE_OPT "):"
 
-#define RESTRICT_FUNCTION_POINTER_HELP                                         \
+#define HELP_RESTRICT_FUNCTION_POINTER                                         \
   "--" RESTRICT_FUNCTION_POINTER_OPT                                           \
   " <pointer_name>/<target[,targets]*>\n"                                      \
   "           restrict a function pointer to a set of possible targets\n"      \
@@ -44,7 +43,7 @@ Author: Diffblue Ltd.
   "           works for globals and function parameters right now\n"           \
   "--" RESTRICT_FUNCTION_POINTER_FROM_FILE_OPT                                 \
   " <file_name>\n"                                                             \
-  "           add from function pointer restrictions from file"
+  "           add function pointer restrictions from file"
 
 void parse_function_pointer_restriction_options_from_cmdline(
   const cmdlinet &cmdline,
@@ -72,7 +71,7 @@ struct function_pointer_restrictionst
   void write_to_file(const std::string &filename) const;
 };
 
-/// Apply a function pointer restrictions to a goto_model. Each restriction is a
+/// Apply function pointer restrictions to a goto_model. Each restriction is a
 /// mapping from a pointer name to a set of possible targets. Replace calls of
 /// these "restricted" pointers with a branch on the value of the function
 /// pointer, comparing it to the set of possible targets. This also adds an

src/util/irep.h

@@ -50,11 +50,6 @@ inline const std::string &id2string(const irep_idt &d)
   #endif
 }
 
-inline irep_idt string2id(const std::string &id_string)
-{
-  return irep_idt{id_string};
-}
-
 inline const std::string &name2string(const irep_namet &n)
 {
   #ifdef USE_DSTRING