cprover
restrict_function_pointers.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Restrict function pointers
4 
5 Author: Diffblue Ltd.
6 
7 \*******************************************************************/
8 
16 
17 #ifndef CPROVER_GOTO_PROGRAMS_RESTRICT_FUNCTION_POINTERS_H
18 #define CPROVER_GOTO_PROGRAMS_RESTRICT_FUNCTION_POINTERS_H
19 
20 #include <unordered_map>
21 #include <unordered_set>
22 
23 #include <util/cmdline.h>
24 #include <util/irep.h>
25 
27 #include <util/options.h>
28 
29 #define RESTRICT_FUNCTION_POINTER_OPT "restrict-function-pointer"
30 #define RESTRICT_FUNCTION_POINTER_FROM_FILE_OPT \
31  "function-pointer-restrictions-file"
32 #define RESTRICT_FUNCTION_POINTER_BY_NAME_OPT \
33  "restrict-function-pointer-by-name"
34 
35 #define OPT_RESTRICT_FUNCTION_POINTER \
36  "(" RESTRICT_FUNCTION_POINTER_OPT \
37  "):" \
38  "(" RESTRICT_FUNCTION_POINTER_FROM_FILE_OPT \
39  "):" \
40  "(" RESTRICT_FUNCTION_POINTER_BY_NAME_OPT "):"
41 
42 #define HELP_RESTRICT_FUNCTION_POINTER \
43  " --" RESTRICT_FUNCTION_POINTER_OPT \
44  " <pointer_name>/<target[,targets]*>\n" \
45  " restrict a function pointer to a set of " \
46  "possible targets\n" \
47  " targets must all exist in the symbol table" \
48  " with a matching type\n" \
49  " works for globals and function parameters" \
50  " right now\n" \
51  " --" RESTRICT_FUNCTION_POINTER_FROM_FILE_OPT \
52  " <file_name>\n" \
53  " add function pointer restrictions from " \
54  "file\n"
55 
57  const cmdlinet &cmdline,
58  optionst &options);
59 
60 class jsont;
61 class message_handlert;
62 
64 {
65 public:
66  using restrictionst =
67  std::unordered_map<irep_idt, std::unordered_set<irep_idt>>;
68  using restrictiont = restrictionst::value_type;
69 
71 
74  const optionst &options,
75  const goto_modelt &goto_model,
76  message_handlert &message_handler);
77 
78  jsont to_json() const;
80 
82  const std::string &filename,
83  message_handlert &message_handler);
84 
85  void write_to_file(const std::string &filename) const;
86 
87 protected:
89  {
90  public:
92  std::string reason,
93  std::string correct_format = "");
94 
95  std::string what() const override;
96 
97  std::string reason;
98  std::string correct_format;
99  };
100 
102  const goto_modelt &goto_model,
103  const restrictionst &restrictions);
104 
106  restrictionst lhs,
107  const restrictionst &rhs);
108 
110  const std::list<std::string> &filenames,
111  message_handlert &message_handler);
112 
114  const std::list<std::string> &restriction_opts);
115 
117  const std::list<std::string> &restriction_opts,
118  const std::string &option);
119 
121  const std::string &restriction_opt,
122  const std::string &option);
123 
125  const goto_functiont &goto_function,
126  const function_pointer_restrictionst::restrictionst &by_name_restrictions,
127  const goto_programt::const_targett &location);
128 
142  const std::list<std::string> &restriction_name_opts,
143  const goto_modelt &goto_model);
144 };
145 
155  goto_modelt &goto_model,
156  const function_pointer_restrictionst &restrictions);
157 
158 #endif // CPROVER_GOTO_PROGRAMS_RESTRICT_FUNCTION_POINTERS_H
Base class for exceptions thrown in the cprover project.
std::string what() const override
A human readable description of what went wrong.
invalid_restriction_exceptiont(std::string reason, std::string correct_format="")
static function_pointer_restrictionst from_options(const optionst &options, const goto_modelt &goto_model, message_handlert &message_handler)
Parse function pointer restrictions from command line.
static restrictionst get_function_pointer_by_name_restrictions(const std::list< std::string > &restriction_name_opts, const goto_modelt &goto_model)
Get function pointer restrictions from restrictions with named pointers.
static restrictionst merge_function_pointer_restrictions(restrictionst lhs, const restrictionst &rhs)
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 parse_function_pointer_restrictions_from_command_line(const std::list< std::string > &restriction_opts)
static restrictiont parse_function_pointer_restriction(const std::string &restriction_opt, const std::string &option)
static restrictionst parse_function_pointer_restrictions(const std::list< std::string > &restriction_opts, const std::string &option)
restrictionst::value_type restrictiont
std::unordered_map< irep_idt, std::unordered_set< irep_idt > > restrictionst
static restrictionst parse_function_pointer_restrictions_from_file(const std::list< std::string > &filenames, message_handlert &message_handler)
void write_to_file(const std::string &filename) const
static void typecheck_function_pointer_restrictions(const goto_modelt &goto_model, const restrictionst &restrictions)
static function_pointer_restrictionst read_from_file(const std::string &filename, message_handlert &message_handler)
static function_pointer_restrictionst from_json(const jsont &json)
A goto function, consisting of function body (see body) and parameter identifiers (see parameter_iden...
Definition: goto_function.h:27
instructionst::const_iterator const_targett
Definition: goto_program.h:551
Definition: json.h:27
Symbol Table + CFG.
nonstd::optional< T > optionalt
Definition: optional.h:35
Options.
static void json(json_objectT &result, const irep_idt &property_id, const property_infot &property_info)
Definition: properties.cpp:114
void restrict_function_pointers(goto_modelt &goto_model, const function_pointer_restrictionst &restrictions)
Apply function pointer restrictions to a goto_model.
void parse_function_pointer_restriction_options_from_cmdline(const cmdlinet &cmdline, optionst &options)