CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
variable_sensitivity_configuration.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3 Module: variable sensitivity domain configuration
4
5 Author: Jez Higgins
6
7\*******************************************************************/
12
14#include <util/options.h>
15
16#include <limits>
17
18static void check_one_of_options(
19 const optionst &options,
20 const std::vector<std::string> &names);
21
23{
25
26 config.value_abstract_type =
28
29 config.pointer_abstract_type = option_to_abstract_type(
30 options, "pointers", pointer_option_mappings, POINTER_INSENSITIVE);
31
32 config.struct_abstract_type = option_to_abstract_type(
33 options, "structs", struct_option_mappings, STRUCT_INSENSITIVE);
34
35 config.array_abstract_type = option_to_abstract_type(
36 options, "arrays", array_option_mappings, ARRAY_INSENSITIVE);
37
38 config.union_abstract_type = option_to_abstract_type(
39 options, "unions", union_option_mappings, UNION_INSENSITIVE);
40
41 // This should always be on (for efficiency with 3-way merge)
42 config.context_tracking.last_write_context = true;
43 config.context_tracking.data_dependency_context =
44 options.get_bool_option("data-dependencies");
45 config.context_tracking.liveness = options.get_bool_option("liveness");
46 check_one_of_options(options, {"data-dependencies", "liveness"});
47
48 config.flow_sensitivity = (options.get_bool_option("flow-insensitive"))
51
52 config.maximum_array_index = configure_max_array_size(options);
53
54 return config;
55}
56
58{
60 config.context_tracking.last_write_context = true;
61 config.value_abstract_type = CONSTANT;
62 config.pointer_abstract_type = POINTER_SENSITIVE;
63 config.struct_abstract_type = STRUCT_SENSITIVE;
64 config.array_abstract_type = ARRAY_SENSITIVE;
65 config.maximum_array_index = std::numeric_limits<size_t>::max();
66 return config;
67}
68
70{
72 config.value_abstract_type = VALUE_SET;
73 config.pointer_abstract_type = VALUE_SET_OF_POINTERS;
74 config.struct_abstract_type = STRUCT_SENSITIVE;
75 config.array_abstract_type = ARRAY_SENSITIVE;
76 config.maximum_array_index = std::numeric_limits<size_t>::max();
77 return config;
78}
79
81{
83 config.context_tracking.last_write_context = true;
84 config.value_abstract_type = INTERVAL;
85 config.pointer_abstract_type = POINTER_SENSITIVE;
86 config.struct_abstract_type = STRUCT_SENSITIVE;
87 config.array_abstract_type = ARRAY_SENSITIVE;
88 config.maximum_array_index = std::numeric_limits<size_t>::max();
89 return config;
90}
91
93 {"intervals", INTERVAL},
94 {"constants", CONSTANT},
95 {"set-of-constants", VALUE_SET}};
96
98 {"top-bottom", POINTER_INSENSITIVE},
99 {"constants", POINTER_SENSITIVE},
100 {"value-set", VALUE_SET_OF_POINTERS}};
101
103 {"top-bottom", STRUCT_INSENSITIVE},
104 {"every-field", STRUCT_SENSITIVE}};
105
107 {"top-bottom", ARRAY_INSENSITIVE},
108 {"smash", ARRAY_SENSITIVE},
109 {"up-to-n-elements", ARRAY_SENSITIVE},
110 {"every-element", ARRAY_SENSITIVE}};
111
114 {"top-bottom", 0},
115 {"smash", 0},
116 {"up-to-n-elements", 10},
117 {"every-element", std::numeric_limits<size_t>::max()}};
118
120 {"top-bottom", UNION_INSENSITIVE}};
121
122template <class mappingt>
124 const std::string &option_name,
125 const std::string &bad_argument,
126 const mappingt &mapping)
127{
128 auto option = "--vsd-" + option_name;
129 auto choices = std::string("");
130 for(auto &kv : mapping)
131 {
132 choices += (!choices.empty() ? "|" : "");
133 choices += kv.first;
134 }
135
137 "Unknown argument '" + bad_argument + "'", option, option + " " + choices};
138}
139
141 const optionst &options,
142 const std::string &option_name,
143 const option_mappingt &mapping,
145{
146 const auto argument = options.get_option(option_name);
147
148 if(argument.empty())
149 return default_type;
150
151 auto selected = mapping.find(argument);
152 if(selected == mapping.end())
153 {
154 throw invalid_argument(option_name, argument, mapping);
155 }
156 return selected->second;
157}
158
160{
161 if(options.get_option("arrays") == "up-to-n-elements")
162 {
163 size_t max_elements = options.get_unsigned_int_option("array-max-elements");
164 if(max_elements != 0)
165 return max_elements - 1;
166 }
167 return option_to_size(options, "arrays", array_option_size_mappings);
168}
169
171 const optionst &options,
172 const std::string &option_name,
173 const option_size_mappingt &mapping)
174{
175 const size_t def = std::numeric_limits<size_t>::max();
176 const auto argument = options.get_option(option_name);
177
178 if(argument.empty())
179 return def;
180
181 auto selected = mapping.find(argument);
182 if(selected == mapping.end())
183 {
184 throw invalid_argument(option_name, argument, mapping);
185 }
186 return selected->second;
187}
188
190 const optionst &options,
191 const std::vector<std::string> &names)
192{
193 int how_many = 0;
194 for(auto &name : names)
195 how_many += options.get_bool_option(name);
196
197 if(how_many <= 1)
198 return;
199
200 auto choices = std::string("");
201 for(auto &name : names)
202 {
203 choices += (!choices.empty() ? "|" : "");
204 auto option = "--vsd-" + name;
205 choices += option;
206 }
207
208 throw invalid_command_line_argument_exceptiont{"Conflicting arguments",
209 "Can only use of " + choices};
210}
configt config
Definition config.cpp:25
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
Thrown when users pass incorrect command line arguments, for example passing no files to analysis or ...
unsigned int get_unsigned_int_option(const std::string &option) const
Definition options.cpp:56
bool get_bool_option(const std::string &option) const
Definition options.cpp:44
const std::string get_option(const std::string &option) const
Definition options.cpp:67
Options.
std::map< std::string, ABSTRACT_OBJECT_TYPET > option_mappingt
static const option_mappingt array_option_mappings
static ABSTRACT_OBJECT_TYPET option_to_abstract_type(const optionst &options, const std::string &option_name, const option_mappingt &mapping, ABSTRACT_OBJECT_TYPET default_type)
static const option_mappingt struct_option_mappings
static const option_mappingt value_option_mappings
static const option_mappingt pointer_option_mappings
static const option_size_mappingt array_option_size_mappings
static size_t configure_max_array_size(const optionst &options)
static const option_mappingt union_option_mappings
static vsd_configt from_options(const optionst &options)
static vsd_configt constant_domain()
std::map< std::string, size_t > option_size_mappingt
static size_t option_to_size(const optionst &options, const std::string &option_name, const option_size_mappingt &mapping)
static void check_one_of_options(const optionst &options, const std::vector< std::string > &names)
invalid_command_line_argument_exceptiont invalid_argument(const std::string &option_name, const std::string &bad_argument, const mappingt &mapping)
Captures the user-supplied configuration for VSD, determining which domain abstractions are used,...