CBMC
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/exception_utils.h>
24 #include <util/irep.h>
25 
26 #include "goto_program.h"
27 
28 class cmdlinet;
29 class goto_functiont;
30 class goto_modelt;
31 class jsont;
32 class message_handlert;
33 class optionst;
34 
35 #define RESTRICT_FUNCTION_POINTER_OPT "restrict-function-pointer"
36 #define RESTRICT_FUNCTION_POINTER_FROM_FILE_OPT \
37  "function-pointer-restrictions-file"
38 #define RESTRICT_FUNCTION_POINTER_BY_NAME_OPT \
39  "restrict-function-pointer-by-name"
40 
41 #define OPT_RESTRICT_FUNCTION_POINTER \
42  "(" RESTRICT_FUNCTION_POINTER_OPT \
43  "):" \
44  "(" RESTRICT_FUNCTION_POINTER_FROM_FILE_OPT \
45  "):" \
46  "(" RESTRICT_FUNCTION_POINTER_BY_NAME_OPT "):"
47 
48 #define HELP_RESTRICT_FUNCTION_POINTER \
49  " {y--" RESTRICT_FUNCTION_POINTER_OPT \
50  "} " \
51  "{upointer_name}/{utarget[,targets]*} \t " \
52  "restrict a function pointer to a set of possible targets; targets must " \
53  "all exist in the symbol table with a matching type; works for globals " \
54  "and function parameters right now\n" \
55  " {y--" RESTRICT_FUNCTION_POINTER_FROM_FILE_OPT \
56  "} {ufile_name} \t " \
57  "add function pointer restrictions from file {ufile_name}\n" \
58  " {y--" RESTRICT_FUNCTION_POINTER_BY_NAME_OPT \
59  "} " \
60  "{usymbol_name}/{utarget[targets]*} \t " \
61  "restrict a function pointer where {usymbol_name} is the unmangled " \
62  "name, before labelling function pointers\n"
63 
65  const cmdlinet &cmdline,
66  optionst &options);
67 
69 {
70 public:
72  std::string reason,
73  std::string correct_format = "");
74 
75  std::string what() const override;
76 
77  std::string correct_format;
78 };
79 
81 {
82 public:
83  using restrictionst =
84  std::unordered_map<irep_idt, std::unordered_set<irep_idt>>;
85  using restrictiont = restrictionst::value_type;
86 
88 
91  const optionst &options,
92  const goto_modelt &goto_model,
93  message_handlert &message_handler);
94 
95  jsont to_json() const;
97  from_json(const jsont &json, const goto_modelt &goto_model);
98 
100  const std::string &filename,
101  const goto_modelt &goto_model,
102  message_handlert &message_handler);
103 
104  void write_to_file(const std::string &filename) const;
105 
106 protected:
108  const goto_modelt &goto_model,
109  const restrictionst &restrictions);
110 
112  restrictionst lhs,
113  const restrictionst &rhs);
114 
116  const std::list<std::string> &filenames,
117  const goto_modelt &goto_model,
118  message_handlert &message_handler);
119 
121  const std::list<std::string> &restriction_opts,
122  const goto_modelt &goto_model);
123 
125  const std::list<std::string> &restriction_opts,
126  const std::string &option,
127  const goto_modelt &goto_model);
128 
130  const std::string &restriction_opt,
131  const std::string &option,
132  const goto_modelt &goto_model);
133 
134  static std::optional<restrictiont> get_by_name_restriction(
135  const goto_functiont &goto_function,
136  const function_pointer_restrictionst::restrictionst &by_name_restrictions,
137  const goto_programt::const_targett &location);
138 
152  const std::list<std::string> &restriction_name_opts,
153  const goto_modelt &goto_model);
154 };
155 
165  message_handlert &message_handler,
166  goto_modelt &goto_model,
167  const optionst &options);
168 
169 #endif // CPROVER_GOTO_PROGRAMS_RESTRICT_FUNCTION_POINTERS_H
Base class for exceptions thrown in the cprover project.
Definition: c_errors.h:64
std::string reason
The reason this exception was generated.
Definition: c_errors.h:83
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 parse_function_pointer_restrictions_from_command_line(const std::list< std::string > &restriction_opts, const goto_modelt &goto_model)
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 parse_function_pointer_restrictions(const std::list< std::string > &restriction_opts, const std::string &option, const goto_modelt &goto_model)
static restrictionst merge_function_pointer_restrictions(restrictionst lhs, const restrictionst &rhs)
static restrictiont parse_function_pointer_restriction(const std::string &restriction_opt, const std::string &option, 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)
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, const goto_modelt &goto_model, 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 from_json(const jsont &json, 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)
A goto function, consisting of function body (see body) and parameter identifiers (see parameter_iden...
Definition: goto_function.h:24
instructionst::const_iterator const_targett
Definition: goto_program.h:615
invalid_restriction_exceptiont(std::string reason, std::string correct_format="")
std::string what() const override
A human readable description of what went wrong.
Definition: json.h:27
Concrete Goto Program.
static void json(json_objectT &result, const irep_idt &property_id, const property_infot &property_info)
Definition: properties.cpp:120
void parse_function_pointer_restriction_options_from_cmdline(const cmdlinet &cmdline, optionst &options)
void restrict_function_pointers(message_handlert &message_handler, goto_modelt &goto_model, const optionst &options)
Apply function pointer restrictions to a goto_model.