Support labels to identify function pointer to restrict

Function pointer indexes may change as code is modified. Labelling
function calls provides for a more stable way of referencing.

Fixes: #6464

Author: tautschnig

doc/architectural/restrict-function-pointer.md

@@ -73,9 +73,12 @@ function where function pointers are being called, to this pattern:
 ```
 <function-name>.function_pointer_call.<N>
 ```
-
 where `N` is referring to which function call it is - so the first call to a
-function pointer in a function will have `N=1`, the 5th `N=5` etc.
+function pointer in a function will have `N=1`, the 5th `N=5` etc, or
+```
+<function-name>.<label>
+```
+when the function call is labelled.
 
 We can call `goto-instrument --restrict-function-pointer
 call.function_pointer_call.1/f,g in.gb out.gb`. This can be read as

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

@@ -0,0 +1,29 @@
+#include <assert.h>
+
+typedef int (*fptr_t)(int);
+
+void use_f(fptr_t fptr)
+{
+labelled_call:
+  assert(fptr(10) == 11);
+}
+
+int f(int x)
+{
+  return x + 1;
+}
+
+int g(int x)
+{
+  return x;
+}
+
+int main(void)
+{
+  int one = 1;
+
+  // We take the address of f and g. In this case remove_function_pointers()
+  // would create a case distinction involving both f and g in the function
+  // use_f() above.
+  use_f(one ? f : g);
+}

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

@@ -0,0 +1,10 @@
+CORE
+test.c
+--restrict-function-pointer use_f.labelled_call/f
+\[use_f\.assertion\.1\] line \d+ assertion fptr\(10\) == 11: SUCCESS
+^EXIT=0$
+^SIGNAL=0$
+--
+--
+This test checks that the function f is called for the first function pointer
+call in function use_f when using the label to refer to the call site.

src/goto-programs/restrict_function_pointers.cpp

@@ -238,15 +238,16 @@ function_pointer_restrictionst::merge_function_pointer_restrictions(
 function_pointer_restrictionst::restrictionst
 function_pointer_restrictionst::parse_function_pointer_restrictions(
   const std::list<std::string> &restriction_opts,
-  const std::string &option)
+  const std::string &option,
+  const goto_modelt &goto_model)
 {
   auto function_pointer_restrictions =
     function_pointer_restrictionst::restrictionst{};
 
   for(const std::string &restriction_opt : restriction_opts)
   {
     const auto restriction =
-      parse_function_pointer_restriction(restriction_opt, option);
+      parse_function_pointer_restriction(restriction_opt, option, goto_model);
 
     const bool inserted = function_pointer_restrictions
                             .emplace(restriction.first, restriction.second)
@@ -265,10 +266,11 @@ function_pointer_restrictionst::parse_function_pointer_restrictions(
 
 function_pointer_restrictionst::restrictionst function_pointer_restrictionst::
   parse_function_pointer_restrictions_from_command_line(
-    const std::list<std::string> &restriction_opts)
+    const std::list<std::string> &restriction_opts,
+    const goto_modelt &goto_model)
 {
   return parse_function_pointer_restrictions(
-    restriction_opts, "--" RESTRICT_FUNCTION_POINTER_OPT);
+    restriction_opts, "--" RESTRICT_FUNCTION_POINTER_OPT, goto_model);
 }
 
 function_pointer_restrictionst::restrictionst
@@ -292,7 +294,8 @@ function_pointer_restrictionst::parse_function_pointer_restrictions_from_file(
 function_pointer_restrictionst::restrictiont
 function_pointer_restrictionst::parse_function_pointer_restriction(
   const std::string &restriction_opt,
-  const std::string &option)
+  const std::string &option,
+  const goto_modelt &goto_model)
 {
   // the format for restrictions is <pointer_name>/<target[,more_targets]*>
   // exactly one pointer and at least one target
@@ -321,7 +324,50 @@ function_pointer_restrictionst::parse_function_pointer_restriction(
       "couldn't find target name before '/' in `" + restriction_opt + "'"};
   }
 
-  auto const pointer_name = restriction_opt.substr(0, pointer_name_end);
+  auto pointer_name = restriction_opt.substr(0, pointer_name_end);
+  const auto last_dot = pointer_name.rfind('.');
+  if(
+    last_dot != std::string::npos && last_dot + 1 != pointer_name.size() &&
+    !isdigit(pointer_name[last_dot + 1]))
+  {
+    const auto function_id = pointer_name.substr(0, last_dot);
+    const auto label = pointer_name.substr(last_dot + 1);
+
+    bool found = false;
+    const auto it = goto_model.goto_functions.function_map.find(function_id);
+    if(it != goto_model.goto_functions.function_map.end())
+    {
+      for(const auto &instruction : it->second.body.instructions)
+      {
+        if(!instruction.is_function_call())
+          continue;
+
+        const auto &called_function = instruction.call_function();
+        if(called_function.id() != ID_dereference)
+          continue;
+
+        if(
+          std::find(
+            instruction.labels.begin(), instruction.labels.end(), label) !=
+          instruction.labels.end())
+        {
+          auto const &called_function_pointer =
+            to_dereference_expr(called_function).pointer();
+          pointer_name =
+            id2string(to_symbol_expr(called_function_pointer).get_identifier());
+          found = true;
+          break;
+        }
+      }
+    }
+    if(!found)
+    {
+      throw invalid_restriction_exceptiont{"non-existent pointer name " +
+                                             pointer_name,
+                                           restriction_format_message};
+    }
+  }
+
   auto const target_names_substring =
     restriction_opt.substr(pointer_name_end + 1);
   auto const target_name_strings = split_string(target_names_substring, ',');
@@ -405,7 +451,8 @@ function_pointer_restrictionst function_pointer_restrictionst::from_options(
   try
   {
     commandline_restrictions =
-      parse_function_pointer_restrictions_from_command_line(restriction_opts);
+      parse_function_pointer_restrictions_from_command_line(
+        restriction_opts, goto_model);
     typecheck_function_pointer_restrictions(
       goto_model, commandline_restrictions);
   }
@@ -549,7 +596,9 @@ function_pointer_restrictionst::get_function_pointer_by_name_restrictions(
 {
   function_pointer_restrictionst::restrictionst by_name_restrictions =
     parse_function_pointer_restrictions(
-      restriction_name_opts, "--" RESTRICT_FUNCTION_POINTER_BY_NAME_OPT);
+      restriction_name_opts,
+      "--" RESTRICT_FUNCTION_POINTER_BY_NAME_OPT,
+      goto_model);
 
   function_pointer_restrictionst::restrictionst restrictions;
   for(auto const &goto_function : goto_model.goto_functions.function_map)

src/goto-programs/restrict_function_pointers.h

@@ -115,15 +115,18 @@ class function_pointer_restrictionst
     message_handlert &message_handler);
 
   static restrictionst parse_function_pointer_restrictions_from_command_line(
-    const std::list<std::string> &restriction_opts);
+    const std::list<std::string> &restriction_opts,
+    const goto_modelt &goto_model);
 
   static restrictionst parse_function_pointer_restrictions(
     const std::list<std::string> &restriction_opts,
-    const std::string &option);
+    const std::string &option,
+    const goto_modelt &goto_model);
 
   static restrictiont parse_function_pointer_restriction(
     const std::string &restriction_opt,
-    const std::string &option);
+    const std::string &option,
+    const goto_modelt &goto_model);
 
   static optionalt<restrictiont> get_by_name_restriction(
     const goto_functiont &goto_function,

unit/goto-programs/restrict_function_pointers.cpp

@@ -24,47 +24,53 @@ class fp_restrictionst : public function_pointer_restrictionst
 
 void restriction_parsing_test()
 {
+  goto_modelt goto_model;
+
   {
     const auto res = fp_restrictionst::parse_function_pointer_restriction(
-      "func1/func2", "test");
+      "func1/func2", "test", goto_model);
     REQUIRE(res.first == "func1");
     REQUIRE(res.second.size() == 1);
     REQUIRE(res.second.find("func2") != res.second.end());
   }
 
   {
     const auto res = fp_restrictionst::parse_function_pointer_restriction(
-      "func1/func2,func3", "test");
+      "func1/func2,func3", "test", goto_model);
     REQUIRE(res.first == "func1");
     REQUIRE(res.second.size() == 2);
     REQUIRE(res.second.find("func2") != res.second.end());
     REQUIRE(res.second.find("func3") != res.second.end());
   }
 
   REQUIRE_THROWS_AS(
-    fp_restrictionst::parse_function_pointer_restriction("func", "test"),
+    fp_restrictionst::parse_function_pointer_restriction(
+      "func", "test", goto_model),
     fp_restrictionst::invalid_restriction_exceptiont);
 
   REQUIRE_THROWS_AS(
-    fp_restrictionst::parse_function_pointer_restriction("/func", "test"),
+    fp_restrictionst::parse_function_pointer_restriction(
+      "/func", "test", goto_model),
     fp_restrictionst::invalid_restriction_exceptiont);
 
   REQUIRE_THROWS_AS(
-    fp_restrictionst::parse_function_pointer_restriction("func/", "test"),
+    fp_restrictionst::parse_function_pointer_restriction(
+      "func/", "test", goto_model),
     fp_restrictionst::invalid_restriction_exceptiont);
 
   REQUIRE_THROWS_AS(
-    fp_restrictionst::parse_function_pointer_restriction("func/,", "test"),
+    fp_restrictionst::parse_function_pointer_restriction(
+      "func/,", "test", goto_model),
     fp_restrictionst::invalid_restriction_exceptiont);
 
   REQUIRE_THROWS_AS(
     fp_restrictionst::parse_function_pointer_restriction(
-      "func1/func2,", "test"),
+      "func1/func2,", "test", goto_model),
     fp_restrictionst::invalid_restriction_exceptiont);
 
   REQUIRE_THROWS_AS(
     fp_restrictionst::parse_function_pointer_restriction(
-      "func1/,func2", "test"),
+      "func1/,func2", "test", goto_model),
     fp_restrictionst::invalid_restriction_exceptiont);
 }