From 0d8e0057ef5bbf9f2fb85cb80b76054a96feefd3 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Tue, 25 Jan 2022 15:20:44 +0000
Subject: [PATCH 1/3] Function pointer restrictions: refactor pointer-name
 parsing

No changes in behaviour: this commit just moves the pointer-name parsing
introduced in 771a153b2187b08 to a function of its own. This is to
prepare for a fix of #6609: the same name parsing also needs to be added
to function-pointer-restriction parsing from JSON files.

To enable this code move, the exception class is moved to the global
scope.
---
 .../restrict_function_pointers.cpp            | 115 ++++++++++--------
 .../restrict_function_pointers.h              |  26 ++--
 .../restrict_function_pointers.cpp            |  12 +-
 3 files changed, 85 insertions(+), 68 deletions(-)

diff --git a/src/goto-programs/restrict_function_pointers.cpp b/src/goto-programs/restrict_function_pointers.cpp
index dceecb4fbff..1f48834b911 100644
--- a/src/goto-programs/restrict_function_pointers.cpp
+++ b/src/goto-programs/restrict_function_pointers.cpp
@@ -84,14 +84,14 @@ static void restrict_function_pointer(
 }
 } // namespace
 
-function_pointer_restrictionst::invalid_restriction_exceptiont::
-  invalid_restriction_exceptiont(std::string reason, std::string correct_format)
+invalid_restriction_exceptiont::invalid_restriction_exceptiont(
+  std::string reason,
+  std::string correct_format)
   : reason(std::move(reason)), correct_format(std::move(correct_format))
 {
 }
 
-std::string
-function_pointer_restrictionst::invalid_restriction_exceptiont::what() const
+std::string invalid_restriction_exceptiont::what() const
 {
   std::string res;
 
@@ -291,6 +291,66 @@ function_pointer_restrictionst::parse_function_pointer_restrictions_from_file(
   return merged_restrictions;
 }
 
+/// Parse \p candidate to distinguish whether it refers to a function pointer
+/// symbol directly (as produced by \ref label_function_pointer_call_sites), or
+/// a source location via its statement label. In the latter case, resolve the
+/// name to the underlying function pointer symbol.
+static std::string resolve_pointer_name(
+  const std::string &candidate,
+  const goto_modelt &goto_model)
+{
+  const auto last_dot = candidate.rfind('.');
+  if(
+    last_dot == std::string::npos || last_dot + 1 == candidate.size() ||
+    isdigit(candidate[last_dot + 1]))
+  {
+    return candidate;
+  }
+
+  std::string pointer_name = candidate;
+
+  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())
+  {
+    optionalt<source_locationt> location;
+    for(const auto &instruction : it->second.body.instructions)
+    {
+      if(
+        std::find(
+          instruction.labels.begin(), instruction.labels.end(), label) !=
+        instruction.labels.end())
+      {
+        location = instruction.source_location();
+      }
+
+      if(
+        instruction.is_function_call() &&
+        instruction.call_function().id() == ID_dereference &&
+        location.has_value() && instruction.source_location() == *location)
+      {
+        auto const &called_function_pointer =
+          to_dereference_expr(instruction.call_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,
+      "pointers should be identifiers or <function_name>.<label>"};
+  }
+
+  return pointer_name;
+}
+
 function_pointer_restrictionst::restrictiont
 function_pointer_restrictionst::parse_function_pointer_restriction(
   const std::string &restriction_opt,
@@ -324,51 +384,8 @@ function_pointer_restrictionst::parse_function_pointer_restriction(
       "couldn't find target name before '/' in `" + restriction_opt + "'"};
   }
 
-  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())
-    {
-      optionalt<source_locationt> location;
-      for(const auto &instruction : it->second.body.instructions)
-      {
-        if(
-          std::find(
-            instruction.labels.begin(), instruction.labels.end(), label) !=
-          instruction.labels.end())
-        {
-          location = instruction.source_location();
-        }
-
-        if(
-          instruction.is_function_call() &&
-          instruction.call_function().id() == ID_dereference &&
-          location.has_value() && instruction.source_location() == *location)
-        {
-          auto const &called_function_pointer =
-            to_dereference_expr(instruction.call_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};
-    }
-  }
+  std::string pointer_name = resolve_pointer_name(
+    restriction_opt.substr(0, pointer_name_end), goto_model);
 
   auto const target_names_substring =
     restriction_opt.substr(pointer_name_end + 1);
diff --git a/src/goto-programs/restrict_function_pointers.h b/src/goto-programs/restrict_function_pointers.h
index 33845ac3503..a1d177c37bc 100644
--- a/src/goto-programs/restrict_function_pointers.h
+++ b/src/goto-programs/restrict_function_pointers.h
@@ -64,6 +64,19 @@ void parse_function_pointer_restriction_options_from_cmdline(
   const cmdlinet &cmdline,
   optionst &options);
 
+class invalid_restriction_exceptiont : public cprover_exception_baset
+{
+public:
+  explicit invalid_restriction_exceptiont(
+    std::string reason,
+    std::string correct_format = "");
+
+  std::string what() const override;
+
+  std::string reason;
+  std::string correct_format;
+};
+
 class function_pointer_restrictionst
 {
 public:
@@ -89,19 +102,6 @@ class function_pointer_restrictionst
   void write_to_file(const std::string &filename) const;
 
 protected:
-  class invalid_restriction_exceptiont : public cprover_exception_baset
-  {
-  public:
-    explicit invalid_restriction_exceptiont(
-      std::string reason,
-      std::string correct_format = "");
-
-    std::string what() const override;
-
-    std::string reason;
-    std::string correct_format;
-  };
-
   static void typecheck_function_pointer_restrictions(
     const goto_modelt &goto_model,
     const restrictionst &restrictions);
diff --git a/unit/goto-programs/restrict_function_pointers.cpp b/unit/goto-programs/restrict_function_pointers.cpp
index 807a047f70c..7ba6d6b2e04 100644
--- a/unit/goto-programs/restrict_function_pointers.cpp
+++ b/unit/goto-programs/restrict_function_pointers.cpp
@@ -46,32 +46,32 @@ void restriction_parsing_test()
   REQUIRE_THROWS_AS(
     fp_restrictionst::parse_function_pointer_restriction(
       "func", "test", goto_model),
-    fp_restrictionst::invalid_restriction_exceptiont);
+    invalid_restriction_exceptiont);
 
   REQUIRE_THROWS_AS(
     fp_restrictionst::parse_function_pointer_restriction(
       "/func", "test", goto_model),
-    fp_restrictionst::invalid_restriction_exceptiont);
+    invalid_restriction_exceptiont);
 
   REQUIRE_THROWS_AS(
     fp_restrictionst::parse_function_pointer_restriction(
       "func/", "test", goto_model),
-    fp_restrictionst::invalid_restriction_exceptiont);
+    invalid_restriction_exceptiont);
 
   REQUIRE_THROWS_AS(
     fp_restrictionst::parse_function_pointer_restriction(
       "func/,", "test", goto_model),
-    fp_restrictionst::invalid_restriction_exceptiont);
+    invalid_restriction_exceptiont);
 
   REQUIRE_THROWS_AS(
     fp_restrictionst::parse_function_pointer_restriction(
       "func1/func2,", "test", goto_model),
-    fp_restrictionst::invalid_restriction_exceptiont);
+    invalid_restriction_exceptiont);
 
   REQUIRE_THROWS_AS(
     fp_restrictionst::parse_function_pointer_restriction(
       "func1/,func2", "test", goto_model),
-    fp_restrictionst::invalid_restriction_exceptiont);
+    invalid_restriction_exceptiont);
 }
 
 void merge_restrictions_test()

From c0270a4cdb68ce5a337df10fd9c6a480f3566066 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Tue, 25 Jan 2022 16:07:27 +0000
Subject: [PATCH 2/3] Function pointer restrictions: support labels in JSON
 input

This is a follow-up fix to 771a153b2187b08, which added support for
labels as function-pointer identifiers. That commit, however, failed to
consider JSON input, and instead only resulted in support for
command-line specified restrictions.

Fixes: #6609
---
 .../json.desc                                  | 11 +++++++++++
 .../restriction.json                           |  5 +++++
 .../restrict_function_pointers.cpp             | 18 ++++++++++++------
 src/goto-programs/restrict_function_pointers.h |  5 ++++-
 .../restrict_function_pointers.cpp             |  5 +++--
 5 files changed, 35 insertions(+), 9 deletions(-)
 create mode 100644 regression/goto-instrument/restrict-function-pointer-by-label/json.desc
 create mode 100644 regression/goto-instrument/restrict-function-pointer-by-label/restriction.json

diff --git a/regression/goto-instrument/restrict-function-pointer-by-label/json.desc b/regression/goto-instrument/restrict-function-pointer-by-label/json.desc
new file mode 100644
index 00000000000..26d3346ead8
--- /dev/null
+++ b/regression/goto-instrument/restrict-function-pointer-by-label/json.desc
@@ -0,0 +1,11 @@
+CORE
+test.c
+--function-pointer-restrictions-file restriction.json
+\[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, with the
+restriction described in the JSON file instead of the command-line directly.
diff --git a/regression/goto-instrument/restrict-function-pointer-by-label/restriction.json b/regression/goto-instrument/restrict-function-pointer-by-label/restriction.json
new file mode 100644
index 00000000000..db94bbc0d5f
--- /dev/null
+++ b/regression/goto-instrument/restrict-function-pointer-by-label/restriction.json
@@ -0,0 +1,5 @@
+{
+  "use_f.labelled_call":[
+    "f"
+  ]
+}
diff --git a/src/goto-programs/restrict_function_pointers.cpp b/src/goto-programs/restrict_function_pointers.cpp
index 1f48834b911..dc6f53c7590 100644
--- a/src/goto-programs/restrict_function_pointers.cpp
+++ b/src/goto-programs/restrict_function_pointers.cpp
@@ -276,13 +276,15 @@ function_pointer_restrictionst::restrictionst function_pointer_restrictionst::
 function_pointer_restrictionst::restrictionst
 function_pointer_restrictionst::parse_function_pointer_restrictions_from_file(
   const std::list<std::string> &filenames,
+  const goto_modelt &goto_model,
   message_handlert &message_handler)
 {
   auto merged_restrictions = function_pointer_restrictionst::restrictionst{};
 
   for(auto const &filename : filenames)
   {
-    auto const restrictions = read_from_file(filename, message_handler);
+    auto const restrictions =
+      read_from_file(filename, goto_model, message_handler);
 
     merged_restrictions = merge_function_pointer_restrictions(
       std::move(merged_restrictions), restrictions.restrictions);
@@ -487,7 +489,7 @@ function_pointer_restrictionst function_pointer_restrictionst::from_options(
     auto const restriction_file_opts =
       options.get_list_option(RESTRICT_FUNCTION_POINTER_FROM_FILE_OPT);
     file_restrictions = parse_function_pointer_restrictions_from_file(
-      restriction_file_opts, message_handler);
+      restriction_file_opts, goto_model, message_handler);
     typecheck_function_pointer_restrictions(goto_model, file_restrictions);
   }
   catch(const invalid_restriction_exceptiont &e)
@@ -515,8 +517,9 @@ function_pointer_restrictionst function_pointer_restrictionst::from_options(
     merge_function_pointer_restrictions(file_restrictions, name_restrictions))};
 }
 
-function_pointer_restrictionst
-function_pointer_restrictionst::from_json(const jsont &json)
+function_pointer_restrictionst function_pointer_restrictionst::from_json(
+  const jsont &json,
+  const goto_modelt &goto_model)
 {
   function_pointer_restrictionst::restrictionst restrictions;
 
@@ -527,7 +530,9 @@ function_pointer_restrictionst::from_json(const jsont &json)
 
   for(auto const &restriction : to_json_object(json))
   {
-    restrictions.emplace(irep_idt{restriction.first}, [&] {
+    std::string pointer_name =
+      resolve_pointer_name(restriction.first, goto_model);
+    restrictions.emplace(irep_idt{pointer_name}, [&] {
       if(!restriction.second.is_array())
       {
         throw deserialization_exceptiont{"Value of " + restriction.first +
@@ -557,6 +562,7 @@ function_pointer_restrictionst::from_json(const jsont &json)
 
 function_pointer_restrictionst function_pointer_restrictionst::read_from_file(
   const std::string &filename,
+  const goto_modelt &goto_model,
   message_handlert &message_handler)
 {
   auto inFile = std::ifstream{filename};
@@ -568,7 +574,7 @@ function_pointer_restrictionst function_pointer_restrictionst::read_from_file(
       "failed to read function pointer restrictions from " + filename};
   }
 
-  return from_json(json);
+  return from_json(json, goto_model);
 }
 
 jsont function_pointer_restrictionst::to_json() const
diff --git a/src/goto-programs/restrict_function_pointers.h b/src/goto-programs/restrict_function_pointers.h
index a1d177c37bc..1b69adc9386 100644
--- a/src/goto-programs/restrict_function_pointers.h
+++ b/src/goto-programs/restrict_function_pointers.h
@@ -93,10 +93,12 @@ class function_pointer_restrictionst
     message_handlert &message_handler);
 
   jsont to_json() const;
-  static function_pointer_restrictionst from_json(const jsont &json);
+  static function_pointer_restrictionst
+  from_json(const jsont &json, const goto_modelt &goto_model);
 
   static function_pointer_restrictionst read_from_file(
     const std::string &filename,
+    const goto_modelt &goto_model,
     message_handlert &message_handler);
 
   void write_to_file(const std::string &filename) const;
@@ -112,6 +114,7 @@ class function_pointer_restrictionst
 
   static restrictionst parse_function_pointer_restrictions_from_file(
     const std::list<std::string> &filenames,
+    const goto_modelt &goto_model,
     message_handlert &message_handler);
 
   static restrictionst parse_function_pointer_restrictions_from_command_line(
diff --git a/unit/goto-programs/restrict_function_pointers.cpp b/unit/goto-programs/restrict_function_pointers.cpp
index 7ba6d6b2e04..2c25aaaf199 100644
--- a/unit/goto-programs/restrict_function_pointers.cpp
+++ b/unit/goto-programs/restrict_function_pointers.cpp
@@ -250,6 +250,7 @@ TEST_CASE("Json conversion", "[core]")
   // representation for the same restrictions can differ, due to the array
   // elements appearing in different orders)
 
+  goto_modelt goto_model;
   std::istringstream ss(
     "{"
     "  \"use_f.function_pointer_call.1\": [\"f\", \"g\"],"
@@ -262,7 +263,7 @@ TEST_CASE("Json conversion", "[core]")
 
   // json1 -> restrictions1
   const auto function_pointer_restrictions1 =
-    function_pointer_restrictionst::from_json(json1);
+    function_pointer_restrictionst::from_json(json1, goto_model);
 
   const auto &restrictions = function_pointer_restrictions1.restrictions;
 
@@ -284,7 +285,7 @@ TEST_CASE("Json conversion", "[core]")
 
   // json2 -> restrictions2
   const auto function_pointer_restrictions2 =
-    function_pointer_restrictionst::from_json(json2);
+    function_pointer_restrictionst::from_json(json2, goto_model);
 
   REQUIRE(
     function_pointer_restrictions1.restrictions ==

From 73980e4e8beb73148260d3e412a4173fa6b85785 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Tue, 25 Jan 2022 16:22:53 +0000
Subject: [PATCH 3/3] Function pointer restrictions: simplify interface

Rather than requiring users to (necessarily!) make at least two calls,
just process what users actually have available (a goto model and some
command line options).
---
 src/goto-instrument/goto_instrument_parse_options.cpp | 7 +------
 src/goto-programs/restrict_function_pointers.cpp      | 7 ++++++-
 src/goto-programs/restrict_function_pointers.h        | 2 +-
 3 files changed, 8 insertions(+), 8 deletions(-)

diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp
index 0d337897c47..3a7a11a4d20 100644
--- a/src/goto-instrument/goto_instrument_parse_options.cpp
+++ b/src/goto-instrument/goto_instrument_parse_options.cpp
@@ -1029,12 +1029,7 @@ void goto_instrument_parse_optionst::instrument_goto_program()
     {
       label_function_pointer_call_sites(goto_model);
 
-      const auto function_pointer_restrictions =
-        function_pointer_restrictionst::from_options(
-          options, goto_model, log.get_message_handler());
-
-      restrict_function_pointers(
-        ui_message_handler, goto_model, function_pointer_restrictions);
+      restrict_function_pointers(ui_message_handler, goto_model, options);
     }
   }
 
diff --git a/src/goto-programs/restrict_function_pointers.cpp b/src/goto-programs/restrict_function_pointers.cpp
index dc6f53c7590..db57e4c3826 100644
--- a/src/goto-programs/restrict_function_pointers.cpp
+++ b/src/goto-programs/restrict_function_pointers.cpp
@@ -169,8 +169,13 @@ void function_pointer_restrictionst::typecheck_function_pointer_restrictions(
 void restrict_function_pointers(
   message_handlert &message_handler,
   goto_modelt &goto_model,
-  const function_pointer_restrictionst &restrictions)
+  const optionst &options)
 {
+  const auto restrictions = function_pointer_restrictionst::from_options(
+    options, goto_model, message_handler);
+  if(restrictions.restrictions.empty())
+    return;
+
   for(auto &function_item : goto_model.goto_functions.function_map)
   {
     goto_functiont &goto_function = function_item.second;
diff --git a/src/goto-programs/restrict_function_pointers.h b/src/goto-programs/restrict_function_pointers.h
index 1b69adc9386..13c44d74c7e 100644
--- a/src/goto-programs/restrict_function_pointers.h
+++ b/src/goto-programs/restrict_function_pointers.h
@@ -164,6 +164,6 @@ class function_pointer_restrictionst
 void restrict_function_pointers(
   message_handlert &message_handler,
   goto_modelt &goto_model,
-  const function_pointer_restrictionst &restrictions);
+  const optionst &options);
 
 #endif // CPROVER_GOTO_PROGRAMS_RESTRICT_FUNCTION_POINTERS_H