Add restrict-function-pointer-by-name option

This works similar to restrict-function-pointer, but for names of individual
function pointer variables (globals, locals, parameters) rather than call sites.
This isn't applicable to all situations (for example, calling function pointers
in structs or function pointers returned from functions), but is more readily
applicable to some common use scenarios (e.g. global function pointers loaded at
start time like in OpenGL).

Author: hannes-steffenhagen-diffblue

regression/goto-instrument/restrict-function-pointer-by-name/test.c

@@ -0,0 +1,43 @@
+#include <assert.h>
+
+int f(void)
+{
+  return 1;
+}
+int g(void)
+{
+  return 2;
+}
+int h(void)
+{
+  return 3;
+}
+
+typedef int (*fptr_t)(void);
+
+void use_f(fptr_t fptr)
+{
+  assert(fptr() == 2);
+}
+
+int nondet_int(void);
+
+fptr_t g_fptr;
+int main(void)
+{
+  int cond = nondet_int();
+  if(cond)
+  {
+    g_fptr = f;
+  }
+  else
+  {
+    g_fptr = h;
+  }
+  int res = g_fptr();
+  assert(res == 1 || res == 3);
+  use_f(g);
+  fptr_t fptr = f;
+  assert(fptr() == 1);
+  return 0;
+}

regression/goto-instrument/restrict-function-pointer-by-name/test.desc

@@ -0,0 +1,11 @@
+CORE
+test.c
+--restrict-function-pointer-by-name main::1::fptr/f --restrict-function-pointer-by-name use_f::fptr/g --restrict-function-pointer-by-name g_fptr/f,h
+\[use_f.assertion.2\] line \d+ assertion fptr\(\) == 2: SUCCESS
+\[use_f.assertion.1\] line \d+ dereferenced function pointer at use_f.function_pointer_call.1 must be g: SUCCESS
+\[main.assertion.1\] line \d+ dereferenced function pointer at main.function_pointer_call.1 must be one of \[(h|f), (h|f)\]: SUCCESS
+\[main.assertion.2\] line \d+ assertion res == 1 \|\| res == 3: SUCCESS
+\[main.assertion.3\] line \d+ dereferenced function pointer at main.function_pointer_call.2 must be f: SUCCESS
+\[main.assertion.4\] line \d+ assertion fptr\(\) == 1: SUCCESS
+^EXIT=0$
+^SIGNAL=0$

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -1037,13 +1037,20 @@ void goto_instrument_parse_optionst::instrument_goto_program()
   {
     parse_function_pointer_restriction_options_from_cmdline(cmdline, options);
 
-    const auto function_pointer_restrictions =
-      function_pointer_restrictionst::from_options(
-        options, log.get_message_handler());
-
-    if(!function_pointer_restrictions.restrictions.empty())
+    if(
+      !options.get_list_option(RESTRICT_FUNCTION_POINTER_OPT).empty() ||
+      !options.get_list_option(RESTRICT_FUNCTION_POINTER_BY_NAME_OPT).empty() ||
+      !options.get_list_option(RESTRICT_FUNCTION_POINTER_FROM_FILE_OPT).empty())
     {
       label_function_pointer_call_sites(goto_model);
+
+      auto const by_name_restrictions =
+        get_function_pointer_by_name_restrictions(goto_model, options);
+
+      const auto function_pointer_restrictions =
+        by_name_restrictions.merge(function_pointer_restrictionst::from_options(
+          options, log.get_message_handler()));
+
       restrict_function_pointers(goto_model, function_pointer_restrictions);
     }
   }

src/goto-programs/restrict_function_pointers.cpp

@@ -104,12 +104,13 @@ source_locationt make_function_pointer_restriction_assertion_source_location(
   return source_location;
 }
 
-template <typename Handler>
-void for_each_function_call(goto_functiont &goto_function, Handler handler)
+template <typename Handler, typename GotoFunctionT>
+void for_each_function_call(GotoFunctionT &&goto_function, Handler handler)
 {
+  using targett = decltype(goto_function.body.instructions.begin());
   for_each_instruction_if(
     goto_function,
-    [](goto_programt::targett target) { return target->is_function_call(); },
+    [](targett target) { return target->is_function_call(); },
     handler);
 }
 
@@ -220,6 +221,9 @@ void parse_function_pointer_restriction_options_from_cmdline(
   options.set_option(
     RESTRICT_FUNCTION_POINTER_FROM_FILE_OPT,
     cmdline.get_values(RESTRICT_FUNCTION_POINTER_FROM_FILE_OPT));
+  options.set_option(
+    RESTRICT_FUNCTION_POINTER_BY_NAME_OPT,
+    cmdline.get_values(RESTRICT_FUNCTION_POINTER_BY_NAME_OPT));
 }
 
 function_pointer_restrictionst::restrictionst
@@ -244,9 +248,11 @@ function_pointer_restrictionst::merge_function_pointer_restrictions(
   return result;
 }
 
-function_pointer_restrictionst::restrictionst function_pointer_restrictionst::
-  parse_function_pointer_restrictions_from_command_line(
-    const std::list<std::string> &restriction_opts)
+function_pointer_restrictionst::restrictionst
+function_pointer_restrictionst::
+parse_function_pointer_restrictions_from_command_line(
+  const std::list<std::string> &restriction_opts,
+  const std::string &option_name)
 {
   auto function_pointer_restrictions =
     function_pointer_restrictionst::restrictionst{};
@@ -361,7 +367,8 @@ function_pointer_restrictionst function_pointer_restrictionst::from_options(
   auto const restriction_opts =
     options.get_list_option(RESTRICT_FUNCTION_POINTER_OPT);
   auto const commandline_restrictions =
-    parse_function_pointer_restrictions_from_command_line(restriction_opts);
+    parse_function_pointer_restrictions_from_command_line(
+      restriction_opts, RESTRICT_FUNCTION_POINTER_OPT);
   auto const file_restrictions = parse_function_pointer_restrictions_from_file(
     options.get_list_option(RESTRICT_FUNCTION_POINTER_FROM_FILE_OPT),
     message_handler);
@@ -459,3 +466,61 @@ void function_pointer_restrictionst::write_to_file(
 
   function_pointer_restrictions_json.output(outFile);
 }
+function_pointer_restrictionst function_pointer_restrictionst::merge(
+  const function_pointer_restrictionst &other) const
+{
+  return function_pointer_restrictionst{
+    merge_function_pointer_restrictions(restrictions, other.restrictions)};
+}
+
+function_pointer_restrictionst get_function_pointer_by_name_restrictions(
+  const goto_modelt &goto_model,
+  const optionst &options)
+{
+  function_pointer_restrictionst::restrictionst by_name_restrictions =
+      function_pointer_restrictionst::
+      parse_function_pointer_restrictions_from_command_line(
+        options.get_list_option(RESTRICT_FUNCTION_POINTER_BY_NAME_OPT),
+        RESTRICT_FUNCTION_POINTER_BY_NAME_OPT);
+  function_pointer_restrictionst::restrictionst restrictions;
+  for(auto const &goto_function : goto_model.goto_functions.function_map)
+  {
+    for_each_function_call(
+      goto_function.second, [&](goto_programt::const_targett location) {
+        PRECONDITION(location->is_function_call());
+        if(can_cast_expr<dereference_exprt>(
+             location->get_function_call().function()))
+        {
+          PRECONDITION(can_cast_expr<symbol_exprt>(
+            to_dereference_expr(location->get_function_call().function())
+              .pointer()));
+          auto const &function_pointer_call_site = to_symbol_expr(
+            to_dereference_expr(location->get_function_call().function())
+              .pointer());
+          auto const &body = goto_function.second.body;
+          for(auto it = std::prev(location); it != body.instructions.end();
+              ++it)
+          {
+            if(
+              it->is_assign() &&
+              it->get_assign().lhs() == function_pointer_call_site &&
+              can_cast_expr<symbol_exprt>(it->get_assign().rhs()))
+            {
+              auto const &assign_rhs = to_symbol_expr(it->get_assign().rhs());
+              auto const restriction =
+                by_name_restrictions.find(assign_rhs.get_identifier());
+              if(
+                restriction != by_name_restrictions.end() &&
+                restriction->first == assign_rhs.get_identifier())
+              {
+                restrictions.emplace(
+                  function_pointer_call_site.get_identifier(),
+                  restriction->second);
+              }
+            }
+          }
+        }
+      });
+  }
+  return function_pointer_restrictionst{restrictions};
+}

src/goto-programs/restrict_function_pointers.h

@@ -29,11 +29,15 @@ Author: Diffblue Ltd.
 #define RESTRICT_FUNCTION_POINTER_OPT "restrict-function-pointer"
 #define RESTRICT_FUNCTION_POINTER_FROM_FILE_OPT                                \
   "function-pointer-restrictions-file"
+#define RESTRICT_FUNCTION_POINTER_BY_NAME_OPT                                  \
+  "restrict-function-pointer-by-name"
 
 #define OPT_RESTRICT_FUNCTION_POINTER                                          \
   "(" RESTRICT_FUNCTION_POINTER_OPT                                            \
   "):"                                                                         \
-  "(" RESTRICT_FUNCTION_POINTER_FROM_FILE_OPT "):"
+  "(" RESTRICT_FUNCTION_POINTER_FROM_FILE_OPT                                  \
+  "):"                                                                         \
+  "(" RESTRICT_FUNCTION_POINTER_BY_NAME_OPT "):"
 
 #define HELP_RESTRICT_FUNCTION_POINTER                                         \
   "--" RESTRICT_FUNCTION_POINTER_OPT                                           \
@@ -78,14 +82,18 @@ class function_pointer_restrictionst
 
   void write_to_file(const std::string &filename) const;
 
+  function_pointer_restrictionst
+  merge(const function_pointer_restrictionst &other) const;
+
+  static restrictionst parse_function_pointer_restrictions_from_command_line(
+    const std::list<std::string> &restriction_opts,
+    const std::string &option_name);
+
 protected:
   static restrictionst merge_function_pointer_restrictions(
     restrictionst lhs,
     const restrictionst &rhs);
 
-  static restrictionst parse_function_pointer_restrictions_from_command_line(
-    const std::list<std::string> &restriction_opts);
-
   static restrictionst parse_function_pointer_restrictions_from_file(
     const std::list<std::string> &filenames,
     message_handlert &message_handler);
@@ -94,6 +102,10 @@ class function_pointer_restrictionst
   parse_function_pointer_restriction(const std::string &restriction_opt);
 };
 
+function_pointer_restrictionst get_function_pointer_by_name_restrictions(
+  const goto_modelt &goto_model,
+  const optionst &options);
+
 /// 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