Some cleanup for restrict function pointer by name feature

Author: danpoe

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -1038,18 +1038,15 @@ void goto_instrument_parse_optionst::instrument_goto_program()
     parse_function_pointer_restriction_options_from_cmdline(cmdline, options);
 
     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())
+      options.is_set(RESTRICT_FUNCTION_POINTER_OPT) ||
+      options.is_set(RESTRICT_FUNCTION_POINTER_BY_NAME_OPT) ||
+      options.is_set(RESTRICT_FUNCTION_POINTER_FROM_FILE_OPT))
     {
       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()));
+        function_pointer_restrictionst::from_options(
+          options, goto_model, log.get_message_handler());
 
       restrict_function_pointers(goto_model, function_pointer_restrictions);
     }

src/goto-programs/restrict_function_pointers.cpp

@@ -206,15 +206,26 @@ void parse_function_pointer_restriction_options_from_cmdline(
   const cmdlinet &cmdline,
   optionst &options)
 {
-  options.set_option(
-    RESTRICT_FUNCTION_POINTER_OPT,
-    cmdline.get_values(RESTRICT_FUNCTION_POINTER_OPT));
-  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));
+  if(cmdline.isset(RESTRICT_FUNCTION_POINTER_OPT))
+  {
+    options.set_option(
+      RESTRICT_FUNCTION_POINTER_OPT,
+      cmdline.get_values(RESTRICT_FUNCTION_POINTER_OPT));
+  }
+
+  if(cmdline.isset(RESTRICT_FUNCTION_POINTER_FROM_FILE_OPT))
+  {
+    options.set_option(
+      RESTRICT_FUNCTION_POINTER_FROM_FILE_OPT,
+      cmdline.get_values(RESTRICT_FUNCTION_POINTER_FROM_FILE_OPT));
+  }
+
+  if(cmdline.isset(RESTRICT_FUNCTION_POINTER_BY_NAME_OPT))
+  {
+    options.set_option(
+      RESTRICT_FUNCTION_POINTER_BY_NAME_OPT,
+      cmdline.get_values(RESTRICT_FUNCTION_POINTER_BY_NAME_OPT));
+  }
 }
 
 namespace
@@ -240,10 +251,12 @@ merge_function_pointer_restrictions(
 }
 
 function_pointer_restrictionst::restrictionst
-parse_function_pointer_restrictions_from_command_line(
+parse_function_pointer_restrictions(
   const std::list<std::string> &restriction_opts,
   const std::string &option_name)
 {
+  const std::string option = "--" + option_name;
+
   auto function_pointer_restrictions =
     function_pointer_restrictionst::restrictionst{};
   for(auto const &restriction_opt : restriction_opts)
@@ -258,21 +271,21 @@ parse_function_pointer_restrictions_from_command_line(
     {
       throw invalid_command_line_argument_exceptiont{
         "couldn't find '/' in `" + restriction_opt + "'",
-        "--" RESTRICT_FUNCTION_POINTER_OPT,
+        option,
         restriction_format_message};
     }
     if(pointer_name_end == restriction_opt.size())
     {
       throw invalid_command_line_argument_exceptiont{
         "couldn't find names of targets after '/' in `" + restriction_opt + "'",
-        "--" RESTRICT_FUNCTION_POINTER_OPT,
+        option,
         restriction_format_message};
     }
     if(pointer_name_end == 0)
     {
       throw invalid_command_line_argument_exceptiont{
         "couldn't find target name before '/' in `" + restriction_opt + "'",
-        "--" RESTRICT_FUNCTION_POINTER_OPT};
+        option_name};
     }
     auto const pointer_name = restriction_opt.substr(0, pointer_name_end);
     auto const target_names_substring =
@@ -282,7 +295,7 @@ parse_function_pointer_restrictions_from_command_line(
     {
       throw invalid_command_line_argument_exceptiont{
         "missing target list for function pointer restriction " + pointer_name,
-        "--" RESTRICT_FUNCTION_POINTER_OPT,
+        option,
         restriction_format_message};
     }
 
@@ -296,7 +309,7 @@ parse_function_pointer_restrictions_from_command_line(
         throw invalid_command_line_argument_exceptiont(
           "leading or trailing comma in restrictions for `" + pointer_name +
             "'",
-          "--" RESTRICT_FUNCTION_POINTER_OPT,
+          option,
           restriction_format_message);
       }
     }
@@ -307,12 +320,20 @@ parse_function_pointer_restrictions_from_command_line(
       throw invalid_command_line_argument_exceptiont{
         "function pointer restriction for `" + pointer_name +
           "' was specified twice",
-        "--" RESTRICT_FUNCTION_POINTER_OPT};
+        option};
     };
   }
   return function_pointer_restrictions;
 }
 
+function_pointer_restrictionst::restrictionst
+parse_function_pointer_restrictions_from_command_line(
+  const std::list<std::string> &restriction_opts)
+{
+  return parse_function_pointer_restrictions(
+    restriction_opts, RESTRICT_FUNCTION_POINTER_OPT);
+}
+
 function_pointer_restrictionst::restrictionst
 parse_function_pointer_restrictions_from_file(
   const std::list<std::string> &filenames,
@@ -328,22 +349,84 @@ parse_function_pointer_restrictions_from_file(
   }
   return merged_restrictions;
 }
+
+function_pointer_restrictionst::restrictionst
+get_function_pointer_by_name_restrictions(
+  const std::list<std::string> &restriction_name_opts,
+  const goto_modelt &goto_model)
+{
+  function_pointer_restrictionst::restrictionst by_name_restrictions =
+    parse_function_pointer_restrictions(
+      restriction_name_opts, 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 restrictions;
+}
 } // namespace
 
 function_pointer_restrictionst function_pointer_restrictionst::from_options(
   const optionst &options,
+  const goto_modelt &goto_model,
   message_handlert &message_handler)
 {
   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, RESTRICT_FUNCTION_POINTER_OPT);
+    parse_function_pointer_restrictions_from_command_line(restriction_opts);
+
+  auto const restriction_file_opts =
+    options.get_list_option(RESTRICT_FUNCTION_POINTER_FROM_FILE_OPT);
   auto const file_restrictions = parse_function_pointer_restrictions_from_file(
-    options.get_list_option(RESTRICT_FUNCTION_POINTER_FROM_FILE_OPT),
+    restriction_file_opts,
     message_handler);
-  return {merge_function_pointer_restrictions(
-    file_restrictions, commandline_restrictions)};
+
+  auto const restriction_name_opts =
+    options.get_list_option(RESTRICT_FUNCTION_POINTER_BY_NAME_OPT);
+  auto const name_restrictions =
+    get_function_pointer_by_name_restrictions(
+      restriction_name_opts, goto_model);
+
+  return {merge_function_pointer_restrictions(commandline_restrictions,
+    merge_function_pointer_restrictions(file_restrictions, name_restrictions))};
 }
 
 function_pointer_restrictionst function_pointer_restrictionst::read_from_file(
@@ -415,60 +498,3 @@ 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 =
-    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

@@ -55,33 +55,28 @@ void parse_function_pointer_restriction_options_from_cmdline(
   optionst &options);
 
 class message_handlert;
+
 struct function_pointer_restrictionst
 {
   using restrictionst =
     std::unordered_map<irep_idt, std::unordered_set<irep_idt>>;
   using value_type = restrictionst::value_type;
+
   const restrictionst restrictions;
 
-  /// parse function pointer restrictions from command line
-  ///
-  /// Note: These are are only syntactically checked at this stage,
-  ///       because type checking them requires a goto_modelt
-  static function_pointer_restrictionst
-  from_options(const optionst &options, message_handlert &message_handler);
+  /// Parse function pointer restrictions from command line
+  static function_pointer_restrictionst from_options(
+    const optionst &options,
+    const goto_modelt &goto_model,
+    message_handlert &message_handler);
 
   static function_pointer_restrictionst read_from_file(
     const std::string &filename,
     message_handlert &message_handler);
 
   void write_to_file(const std::string &filename) const;
-  function_pointer_restrictionst
-  merge(const function_pointer_restrictionst &other) const;
 };
 
-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