WIP file interface and refactor

Author: hannes-steffenhagen-diffblue

src/cbmc/cbmc_parse_options.cpp

@@ -138,9 +138,7 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
   cbmc_parse_optionst::set_default_options(options);
   parse_c_object_factory_options(cmdline, options);
 
-  options.set_option(
-    RESTRICT_FUNCTION_POINTER_OPT,
-    cmdline.get_values(RESTRICT_FUNCTION_POINTER_OPT));
+  parse_function_pointer_restriction_options_from_cmdline(cmdline, options);
 
   if(cmdline.isset("function"))
     options.set_option("function", cmdline.get_value("function"));
@@ -843,7 +841,7 @@ bool cbmc_parse_optionst::process_goto_program(
                << messaget::eom;
 
   const auto function_pointer_restrictions =
-    function_pointer_restrictionst::from_options(options);
+    function_pointer_restrictionst::from_options(options, log.get_message_handler());
   if(!function_pointer_restrictions.restrictions.empty()) {
     label_function_pointer_call_sites(goto_model);
     restrict_function_pointers(

src/goto-programs/restrict_function_pointers.cpp

@@ -9,9 +9,14 @@ Author: Diffblue Ltd.
 #include "restrict_function_pointers.h"
 
 #include <ansi-c/expr2c.h>
+#include <json/json_parser.h>
 #include <util/expr_iterator.h>
 #include <util/string_utils.h>
 
+#include <algorithm>
+#include <fstream>
+#include <iostream>
+
 namespace
 {
 void typecheck_function_pointer_restrictions(
@@ -77,7 +82,7 @@ source_locationt make_function_pointer_restriction_assertion_source_location(
           << " must be ";
   if(restriction.second.size() == 1)
   {
-    comment << restriction.second.front();
+    comment << *restriction.second.begin();
   }
   else
   {
@@ -197,13 +202,46 @@ void restrict_function_pointers(
   }
 }
 
-function_pointer_restrictionst
-function_pointer_restrictionst::from_options(const optionst &options)
+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));
+}
+
+namespace
+{
+function_pointer_restrictionst::restrictionst
+merge_function_pointer_restrictions(
+  const function_pointer_restrictionst::restrictionst &lhs,
+  const function_pointer_restrictionst::restrictionst &rhs)
+{
+  auto result = lhs;
+  for(auto const &restriction : rhs)
+  {
+    auto emplace_result = result.emplace(restriction.first, restriction.second);
+    if(!emplace_result.second)
+    {
+      for(auto const &target : restriction.second)
+      {
+        emplace_result.first->second.insert(target);
+      }
+    }
+  }
+  return result;
+}
+
+function_pointer_restrictionst::restrictionst
+parse_function_pointer_restrictions_from_command_line(
+  const std::list<std::string> &restriction_opts)
 {
   auto function_pointer_restrictions =
-    std::unordered_map<irep_idt, std::vector<irep_idt>>{};
-  auto const restriction_opts =
-    options.get_list_option(RESTRICT_FUNCTION_POINTER_OPT);
+    function_pointer_restrictionst::restrictionst{};
   for(auto const &restriction_opt : restriction_opts)
   {
     // the format for restrictions is <pointer_name>/<target[,more_targets]*>
@@ -244,11 +282,11 @@ function_pointer_restrictionst::from_options(const optionst &options)
         restriction_format_message};
     }
     auto const target_names = ([&target_name_strings] {
-      auto target_names = std::vector<irep_idt>(target_name_strings.size());
+      auto target_names = std::unordered_set<irep_idt>{};
       std::transform(
         target_name_strings.begin(),
         target_name_strings.end(),
-        target_names.begin(),
+        std::inserter(target_names, target_names.end()),
         string2id);
       return target_names;
     })();
@@ -273,5 +311,106 @@ function_pointer_restrictionst::from_options(const optionst &options)
         "--" RESTRICT_FUNCTION_POINTER_OPT};
     };
   }
-  return {function_pointer_restrictions};
+  return function_pointer_restrictions;
+}
+
+function_pointer_restrictionst::restrictionst
+parse_function_pointer_restrictions_from_file(
+  const std::list<std::string> &filenames,
+  message_handlert &message_handler)
+{
+  auto merged_restrictions = function_pointer_restrictionst::restrictionst{};
+  for(auto const &filename : filenames)
+  {
+    auto const restrictions =
+      function_pointer_restrictionst::read_from_file(filename, message_handler);
+    merged_restrictions = merge_function_pointer_restrictions(
+      merged_restrictions, restrictions.restrictions);
+  }
+  return merged_restrictions;
+}
+} // namespace
+
+function_pointer_restrictionst function_pointer_restrictionst::from_options(
+  const optionst &options,
+  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);
+  auto const file_restrictions = parse_function_pointer_restrictions_from_file(
+    options.get_list_option(RESTRICT_FUNCTION_POINTER_FROM_FILE_OPT),
+    message_handler);
+  return {merge_function_pointer_restrictions(
+    file_restrictions, commandline_restrictions)};
+}
+
+function_pointer_restrictionst function_pointer_restrictionst::read_from_file(
+  const std::string &filename,
+  message_handlert &message_handler)
+{
+  auto failed = [](bool failFlag) { return failFlag; };
+  function_pointer_restrictionst::restrictionst restrictions;
+  auto inFile = std::ifstream{filename};
+  jsont json;
+  if(failed(parse_json(inFile, filename, message_handler, json)))
+  {
+    throw system_exceptiont{
+      "failed to read function pointer restrictions from " + filename};
+  }
+  if(!json.is_object())
+  {
+    throw system_exceptiont{"top level item is not an object"};
+  }
+  for(auto const &kv_pair : to_json_object(json))
+  {
+    restrictions.emplace(irep_idt{kv_pair.first}, [&] {
+      if(!kv_pair.second.is_array())
+      {
+        throw system_exceptiont{"In " + filename + ", value of " +
+                                kv_pair.first + " is not an array"};
+      }
+      auto possible_targets = std::unordered_set<irep_idt>{};
+      auto const &array = to_json_array(kv_pair.second);
+      std::transform(
+        array.begin(),
+        array.end(),
+        std::inserter(possible_targets, possible_targets.end()),
+        [&](const jsont &array_element) {
+          if(!array_element.is_string())
+          {
+            throw system_exceptiont{"In " + filename + ", value of " +
+                                    kv_pair.first +
+                                    "contains a non-string array element"};
+          }
+          return irep_idt{to_json_string(array_element).value};
+        });
+      return possible_targets;
+    }());
+  }
+  return function_pointer_restrictionst{restrictions};
+}
+void function_pointer_restrictionst::write_to_file(
+  const std::string &filename) const
+{
+  auto function_pointer_restrictions_json = jsont{};
+  auto &restrictions_json_object =
+    function_pointer_restrictions_json.make_object();
+  for(auto const &restriction : restrictions)
+  {
+    auto &targets_array =
+      restrictions_json_object[id2string(restriction.first)].make_array();
+    for(auto const &target : restriction.second)
+    {
+      targets_array.push_back(json_stringt{target});
+    }
+  }
+  auto outFile = std::ofstream{filename};
+  if(!outFile)
+  {
+    throw system_exceptiont{"cannot open " + filename +
+                            " for writing function pointer restrictions"};
+  }
+  function_pointer_restrictions_json.output(outFile);
 }

src/goto-programs/restrict_function_pointers.h

@@ -17,7 +17,8 @@ Author: Diffblue Ltd.
 #ifndef CPROVER_GOTO_PROGRAMS_RESTRICT_FUNCTION_POINTERS_H
 #define CPROVER_GOTO_PROGRAMS_RESTRICT_FUNCTION_POINTERS_H
 
-#include <vector>
+#include <unordered_map>
+#include <unordered_set>
 
 #include <util/cmdline.h>
 #include <util/irep.h>
@@ -26,27 +27,49 @@ Author: Diffblue Ltd.
 #include <util/options.h>
 
 #define RESTRICT_FUNCTION_POINTER_OPT "restrict-function-pointer"
-#define OPT_RESTRICT_FUNCTION_POINTER "(" RESTRICT_FUNCTION_POINTER_OPT "):"
+#define RESTRICT_FUNCTION_POINTER_FROM_FILE_OPT                                \
+  "function-pointer-restrictions-file"
+
+#define OPT_RESTRICT_FUNCTION_POINTER                                          \
+  "(" RESTRICT_FUNCTION_POINTER_OPT                                            \
+  "):"                                                                         \
+  "(" RESTRICT_FUNCTION_POINTER_FROM_FILE_OPT "):"
 
 #define RESTRICT_FUNCTION_POINTER_HELP                                         \
   "--" RESTRICT_FUNCTION_POINTER_OPT                                           \
   " <pointer_name>/<target[,targets]*>\n"                                      \
   "           restrict a function pointer to a set of possible targets\n"      \
   "           targets must all exist in the symbol table with a matching "     \
   "type\n"                                                                     \
-  "           works for globals and function parameters right now\n"
+  "           works for globals and function parameters right now\n"           \
+  "--" RESTRICT_FUNCTION_POINTER_FROM_FILE_OPT                                 \
+  " <file_name>\n"                                                             \
+  "           add from function pointer restrictions from file"
+
+void parse_function_pointer_restriction_options_from_cmdline(
+  const cmdlinet &cmdline,
+  optionst &options);
 
+class message_handlert;
 struct function_pointer_restrictionst
 {
-  using restrictionst = std::unordered_map<irep_idt, std::vector<irep_idt>>;
+  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);
+  static function_pointer_restrictionst
+  from_options(const optionst &options, 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;
 };
 
 /// Apply a function pointer restrictions to a goto_model. Each restriction is a