Function pointer restrictions: support labels in JSON input

This is a follow-up fix to 771a153, 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

Author: tautschnig

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.

regression/goto-instrument/restrict-function-pointer-by-label/restriction.json

@@ -0,0 +1,5 @@
+{
+  "use_f.labelled_call":[
+    "f"
+  ]
+}

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

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(

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 ==