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/exception_utils.h>
24 #include <util/irep.h>
25 #include <util/optional.h>
26 
27 #include "goto_program.h"
28 
29 class cmdlinet;
30 class goto_functiont;
31 class goto_modelt;
32 class jsont;
33 class message_handlert;
34 class optionst;
35 
36 #define RESTRICT_FUNCTION_POINTER_OPT "restrict-function-pointer"
37 #define RESTRICT_FUNCTION_POINTER_FROM_FILE_OPT \
38  "function-pointer-restrictions-file"
39 #define RESTRICT_FUNCTION_POINTER_BY_NAME_OPT \
40  "restrict-function-pointer-by-name"
41 
42 #define OPT_RESTRICT_FUNCTION_POINTER \
43  "(" RESTRICT_FUNCTION_POINTER_OPT \
44  "):" \
45  "(" RESTRICT_FUNCTION_POINTER_FROM_FILE_OPT \
46  "):" \
47  "(" RESTRICT_FUNCTION_POINTER_BY_NAME_OPT "):"
48 
49 #define HELP_RESTRICT_FUNCTION_POINTER \
50  " --" RESTRICT_FUNCTION_POINTER_OPT \
51  " <pointer_name>/<target[,targets]*>\n" \
52  " restrict a function pointer to a set of " \
53  "possible targets\n" \
54  " targets must all exist in the symbol table" \
55  " with a matching type\n" \
56  " works for globals and function parameters" \
57  " right now\n" \
58  " --" RESTRICT_FUNCTION_POINTER_FROM_FILE_OPT \
59  " <file_name>\n" \
60  " add function pointer restrictions from " \
61  "file\n"
62 
64  const cmdlinet &cmdline,
65  optionst &options);
66 
68 {
69 public:
70  using restrictionst =
71  std::unordered_map<irep_idt, std::unordered_set<irep_idt>>;
72  using restrictiont = restrictionst::value_type;
73 
75 
78  const optionst &options,
79  const goto_modelt &goto_model,
80  message_handlert &message_handler);
81 
82  jsont to_json() const;
84 
86  const std::string &filename,
87  message_handlert &message_handler);
88 
89  void write_to_file(const std::string &filename) const;
90 
91 protected:
93  {
94  public:
96  std::string reason,
97  std::string correct_format = "");
98 
99  std::string what() const override;
100 
101  std::string reason;
102  std::string correct_format;
103  };
104 
106  const goto_modelt &goto_model,
107  const restrictionst &restrictions);
108 
110  restrictionst lhs,
111  const restrictionst &rhs);
112 
114  const std::list<std::string> &filenames,
115  message_handlert &message_handler);
116 
118  const std::list<std::string> &restriction_opts);
119 
121  const std::list<std::string> &restriction_opts,
122  const std::string &option);
123 
125  const std::string &restriction_opt,
126  const std::string &option);
127 
129  const goto_functiont &goto_function,
130  const function_pointer_restrictionst::restrictionst &by_name_restrictions,
131  const goto_programt::const_targett &location);
132 
146  const std::list<std::string> &restriction_name_opts,
147  const goto_modelt &goto_model);
148 };
149 
159  goto_modelt &goto_model,
160  const function_pointer_restrictionst &restrictions);
161 
162 #endif // CPROVER_GOTO_PROGRAMS_RESTRICT_FUNCTION_POINTERS_H
function_pointer_restrictionst::invalid_restriction_exceptiont::reason
std::string reason
Definition: restrict_function_pointers.h:101
exception_utils.h
function_pointer_restrictionst::read_from_file
static function_pointer_restrictionst read_from_file(const std::string &filename, message_handlert &message_handler)
Definition: restrict_function_pointers.cpp:535
optionst
Definition: options.h:23
optional.h
function_pointer_restrictionst::to_json
jsont to_json() const
Definition: restrict_function_pointers.cpp:551
goto_modelt
Definition: goto_model.h:26
jsont
Definition: json.h:27
function_pointer_restrictionst::invalid_restriction_exceptiont::what
std::string what() const override
A human readable description of what went wrong.
Definition: restrict_function_pointers.cpp:154
function_pointer_restrictionst::from_options
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.
Definition: restrict_function_pointers.cpp:439
function_pointer_restrictionst::restrictions
const restrictionst restrictions
Definition: restrict_function_pointers.h:74
function_pointer_restrictionst::get_function_pointer_by_name_restrictions
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.
Definition: restrict_function_pointers.cpp:589
cmdlinet
Definition: cmdline.h:21
function_pointer_restrictionst::parse_function_pointer_restrictions_from_file
static restrictionst parse_function_pointer_restrictions_from_file(const std::list< std::string > &filenames, message_handlert &message_handler)
Definition: restrict_function_pointers.cpp:318
function_pointer_restrictionst::merge_function_pointer_restrictions
static restrictionst merge_function_pointer_restrictions(restrictionst lhs, const restrictionst &rhs)
Definition: restrict_function_pointers.cpp:260
json
static void json(json_objectT &result, const irep_idt &property_id, const property_infot &property_info)
Definition: properties.cpp:116
restrict_function_pointers
void restrict_function_pointers(goto_modelt &goto_model, const function_pointer_restrictionst &restrictions)
Apply function pointer restrictions to a goto_model.
Definition: restrict_function_pointers.cpp:219
function_pointer_restrictionst::restrictionst
std::unordered_map< irep_idt, std::unordered_set< irep_idt > > restrictionst
Definition: restrict_function_pointers.h:71
function_pointer_restrictionst::get_by_name_restriction
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)
Definition: restrict_function_pointers.cpp:396
message_handlert
Definition: message.h:28
goto_functiont
A goto function, consisting of function body (see body) and parameter identifiers (see parameter_iden...
Definition: goto_function.h:24
function_pointer_restrictionst::restrictiont
restrictionst::value_type restrictiont
Definition: restrict_function_pointers.h:72
function_pointer_restrictionst
Definition: restrict_function_pointers.h:68
optionalt
nonstd::optional< T > optionalt
Definition: optional.h:35
function_pointer_restrictionst::parse_function_pointer_restrictions_from_command_line
static restrictionst parse_function_pointer_restrictions_from_command_line(const std::list< std::string > &restriction_opts)
Definition: restrict_function_pointers.cpp:310
goto_program.h
Concrete Goto Program.
function_pointer_restrictionst::invalid_restriction_exceptiont::invalid_restriction_exceptiont
invalid_restriction_exceptiont(std::string reason, std::string correct_format="")
Definition: restrict_function_pointers.cpp:148
function_pointer_restrictionst::invalid_restriction_exceptiont::correct_format
std::string correct_format
Definition: restrict_function_pointers.h:102
parse_function_pointer_restriction_options_from_cmdline
void parse_function_pointer_restriction_options_from_cmdline(const cmdlinet &cmdline, optionst &options)
Definition: restrict_function_pointers.cpp:233
function_pointer_restrictionst::typecheck_function_pointer_restrictions
static void typecheck_function_pointer_restrictions(const goto_modelt &goto_model, const restrictionst &restrictions)
Definition: restrict_function_pointers.cpp:169
function_pointer_restrictionst::write_to_file
void write_to_file(const std::string &filename) const
Definition: restrict_function_pointers.cpp:570
function_pointer_restrictionst::parse_function_pointer_restrictions
static restrictionst parse_function_pointer_restrictions(const std::list< std::string > &restriction_opts, const std::string &option)
Definition: restrict_function_pointers.cpp:282
function_pointer_restrictionst::parse_function_pointer_restriction
static restrictiont parse_function_pointer_restriction(const std::string &restriction_opt, const std::string &option)
Definition: restrict_function_pointers.cpp:336
function_pointer_restrictionst::from_json
static function_pointer_restrictionst from_json(const jsont &json)
Definition: restrict_function_pointers.cpp:496
goto_programt::const_targett
instructionst::const_iterator const_targett
Definition: goto_program.h:647
function_pointer_restrictionst::invalid_restriction_exceptiont
Definition: restrict_function_pointers.h:93
cprover_exception_baset
Base class for exceptions thrown in the cprover project.
Definition: exception_utils.h:25
irep.h