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 "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                                         \
  " {y--" RESTRICT_FUNCTION_POINTER_OPT                                        \
  "} "                                                                         \
  "{upointer_name}/{utarget[,targets]*} \t "                                   \
  "restrict a function pointer to a set of possible targets; targets must "    \
  "all exist in the symbol table with a matching type; works for globals "     \
  "and function parameters right now\n"                                        \
  " {y--" RESTRICT_FUNCTION_POINTER_FROM_FILE_OPT                              \
  "} {ufile_name} \t "                                                         \
  "add function pointer restrictions from file {ufile_name}\n"                 \
  " {y--" RESTRICT_FUNCTION_POINTER_BY_NAME_OPT                                \
  "} "                                                                         \
  "{usymbol_name}/{utarget[targets]*} \t "                                     \
  "restrict a function pointer where {usymbol_name} 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 std::optional<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