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/cbmc/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/cbmc/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\]: 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/cbmc/cbmc_parse_options.cpp

@@ -11,8 +11,8 @@ Author: Daniel Kroening, [email protected]
 
 #include "cbmc_parse_options.h"
 
-#include <fstream>
 #include <cstdlib> // exit()
+#include <fstream>
 #include <iostream>
 #include <memory>
 
@@ -178,8 +178,9 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
     exit(CPROVER_EXIT_USAGE_ERROR);
   }
 
-  if(cmdline.isset("reachability-slice") &&
-     cmdline.isset("reachability-slice-fb"))
+  if(
+    cmdline.isset("reachability-slice") &&
+    cmdline.isset("reachability-slice-fb"))
   {
     log.error()
       << "--reachability-slice and --reachability-slice-fb must not be "
@@ -258,9 +259,9 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
   if(cmdline.isset("no-simplify"))
     options.set_option("simplify", false);
 
-  if(cmdline.isset("stop-on-fail") ||
-     cmdline.isset("dimacs") ||
-     cmdline.isset("outfile"))
+  if(
+    cmdline.isset("stop-on-fail") || cmdline.isset("dimacs") ||
+    cmdline.isset("outfile"))
     options.set_option("stop-on-fail", true);
 
   if(
@@ -370,8 +371,7 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
 
   if(cmdline.isset("max-node-refinement"))
     options.set_option(
-      "max-node-refinement",
-      cmdline.get_value("max-node-refinement"));
+      "max-node-refinement", cmdline.get_value("max-node-refinement"));
 
   // SMT Options
 
@@ -387,11 +387,11 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
   if(cmdline.isset("fpa"))
     options.set_option("fpa", true);
 
-  bool solver_set=false;
+  bool solver_set = false;
 
   if(cmdline.isset("boolector"))
   {
-    options.set_option("boolector", true), solver_set=true;
+    options.set_option("boolector", true), solver_set = true;
     options.set_option("smt2", true);
   }
 
@@ -403,25 +403,25 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
 
   if(cmdline.isset("mathsat"))
   {
-    options.set_option("mathsat", true), solver_set=true;
+    options.set_option("mathsat", true), solver_set = true;
     options.set_option("smt2", true);
   }
 
   if(cmdline.isset("cvc4"))
   {
-    options.set_option("cvc4", true), solver_set=true;
+    options.set_option("cvc4", true), solver_set = true;
     options.set_option("smt2", true);
   }
 
   if(cmdline.isset("yices"))
   {
-    options.set_option("yices", true), solver_set=true;
+    options.set_option("yices", true), solver_set = true;
     options.set_option("smt2", true);
   }
 
   if(cmdline.isset("z3"))
   {
-    options.set_option("z3", true), solver_set=true;
+    options.set_option("z3", true), solver_set = true;
     options.set_option("smt2", true);
   }
 
@@ -461,8 +461,7 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
   if(cmdline.isset("symex-coverage-report"))
   {
     options.set_option(
-      "symex-coverage-report",
-      cmdline.get_value("symex-coverage-report"));
+      "symex-coverage-report", cmdline.get_value("symex-coverage-report"));
     options.set_option("paths-symex-explore-all", true);
   }
 
@@ -512,8 +511,7 @@ int cbmc_parse_optionst::doit()
   // Unwinding of transition systems is done by hw-cbmc.
   //
 
-  if(cmdline.isset("module") ||
-     cmdline.isset("gen-interface"))
+  if(cmdline.isset("module") || cmdline.isset("gen-interface"))
   {
     log.error() << "This version of CBMC has no support for "
                    " hardware modules. Please use hw-cbmc."
@@ -552,13 +550,13 @@ int cbmc_parse_optionst::doit()
       return CPROVER_EXIT_INCORRECT_TASK;
     }
 
-    std::string filename=cmdline.args[0];
+    std::string filename = cmdline.args[0];
 
-    #ifdef _MSC_VER
+#ifdef _MSC_VER
     std::ifstream infile(widen(filename));
-    #else
+#else
     std::ifstream infile(filename);
-    #endif
+#endif
 
     if(!infile)
     {
@@ -567,10 +565,9 @@ int cbmc_parse_optionst::doit()
       return CPROVER_EXIT_INCORRECT_TASK;
     }
 
-    std::unique_ptr<languaget> language=
-      get_language_from_filename(filename);
+    std::unique_ptr<languaget> language = get_language_from_filename(filename);
 
-    if(language==nullptr)
+    if(language == nullptr)
     {
       log.error() << "failed to figure out type of file '" << filename << "'"
                   << messaget::eom;
@@ -595,11 +592,12 @@ int cbmc_parse_optionst::doit()
   int get_goto_program_ret =
     get_goto_program(goto_model, options, cmdline, ui_message_handler);
 
-  if(get_goto_program_ret!=-1)
+  if(get_goto_program_ret != -1)
     return get_goto_program_ret;
 
-  if(cmdline.isset("show-claims") || // will go away
-     cmdline.isset("show-properties")) // use this one
+  if(
+    cmdline.isset("show-claims") ||   // will go away
+    cmdline.isset("show-properties")) // use this one
   {
     show_properties(goto_model, ui_message_handler);
     return CPROVER_EXIT_SUCCESS;
@@ -840,14 +838,20 @@ bool cbmc_parse_optionst::process_goto_program(
   log.status() << "Removal of function pointers and virtual functions"
                << messaget::eom;
 
-  const auto function_pointer_restrictions =
-    function_pointer_restrictionst::from_options(
-      options, log.get_message_handler());
-  if(!function_pointer_restrictions.restrictions.empty())
+  if(
+    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()));
     restrict_function_pointers(goto_model, function_pointer_restrictions);
   }
+
   remove_function_pointers(
     log.get_message_handler(),
     goto_model,

src/goto-programs/restrict_function_pointers.cpp

@@ -108,12 +108,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_goto_location_if(
     goto_function,
-    [](goto_programt::targett target) { return target->is_function_call(); },
+    [](targett target) { return target->is_function_call(); },
     handler);
 }
 } // namespace
@@ -210,6 +211,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));
 }
 
 namespace
@@ -236,7 +240,8 @@ merge_function_pointer_restrictions(
 
 function_pointer_restrictionst::restrictionst
 parse_function_pointer_restrictions_from_command_line(
-  const std::list<std::string> &restriction_opts)
+  const std::list<std::string> &restriction_opts,
+  const std::string &option_name)
 {
   auto function_pointer_restrictions =
     function_pointer_restrictionst::restrictionst{};
@@ -336,7 +341,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);
@@ -413,3 +419,60 @@ 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

@@ -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 RESTRICT_FUNCTION_POINTER_HELP                                         \
   "--" RESTRICT_FUNCTION_POINTER_OPT                                           \
@@ -70,8 +74,13 @@ struct function_pointer_restrictionst
     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 a 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