restrict_function_pointers.h

Go to the documentation of this file.

/*******************************************************************\
 
Module: Restrict function pointers
 
Author: Diffblue Ltd.
 
\*******************************************************************/
 
 
#ifndef CPROVER_GOTO_PROGRAMS_RESTRICT_FUNCTION_POINTERS_H
#define CPROVER_GOTO_PROGRAMS_RESTRICT_FUNCTION_POINTERS_H
 
#include <unordered_map>
#include <unordered_set>
 
#include <util/exception_utils.h>
#include <util/irep.h>
#include <util/optional.h>
 
#include "goto_program.h"
 
class cmdlinet;
class goto_functiont;
class goto_modelt;
class jsont;
class message_handlert;
class optionst;
 
#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_BY_NAME_OPT "):"
 
#define HELP_RESTRICT_FUNCTION_POINTER                                         \
  " --" 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"                                                               \
  " --" RESTRICT_FUNCTION_POINTER_FROM_FILE_OPT                                \
  " <file_name>\n"                                                             \
  "                              add function pointer restrictions from "      \
  "file\n"                                                                     \
  " --" RESTRICT_FUNCTION_POINTER_BY_NAME_OPT                                  \
  " <symbol_name>/target[targets]*>\n"                                         \
  "                              restrict a function pointer where "           \
  " <symbol_name>\n"                                                           \
  "                              is the unmangled name, before labelling "     \
  "function pointers\n"
 
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 correct_format;
};
 
class function_pointer_restrictionst
{
public:
  using restrictionst =
    std::unordered_map<irep_idt, std::unordered_set<irep_idt>>;
  using restrictiont = restrictionst::value_type;
 
  const restrictionst restrictions;
 
  static function_pointer_restrictionst from_options(
    const optionst &options,
    const goto_modelt &goto_model,
    message_handlert &message_handler);
 
  jsont to_json() const;
  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;
 
protected:
  static void typecheck_function_pointer_restrictions(
    const goto_modelt &goto_model,
    const restrictionst &restrictions);
 
  static restrictionst merge_function_pointer_restrictions(
    restrictionst lhs,
    const restrictionst &rhs);
 
  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(
    const std::list<std::string> &restriction_opts,
    const goto_modelt &goto_model);
 
  static restrictionst parse_function_pointer_restrictions(
    const std::list<std::string> &restriction_opts,
    const std::string &option,
    const goto_modelt &goto_model);
 
  static restrictiont parse_function_pointer_restriction(
    const std::string &restriction_opt,
    const std::string &option,
    const goto_modelt &goto_model);
 
  static optionalt<restrictiont> get_by_name_restriction(
    const goto_functiont &goto_function,
    const function_pointer_restrictionst::restrictionst &by_name_restrictions,
    const goto_programt::const_targett &location);
 
  static restrictionst get_function_pointer_by_name_restrictions(
    const std::list<std::string> &restriction_name_opts,
    const goto_modelt &goto_model);
};
 
void restrict_function_pointers(
  message_handlert &message_handler,
  goto_modelt &goto_model,
  const optionst &options);
 
#endif // CPROVER_GOTO_PROGRAMS_RESTRICT_FUNCTION_POINTERS_H