cprover
Loading...
Searching...
No Matches
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
13#include <limits>
14#include <util/options.h>
15
16static void check_one_of_options(
17 const optionst &options,
18 const std::vector<std::string> &names);
19
21{
23
24 config.value_abstract_type =
26
27 config.pointer_abstract_type = option_to_abstract_type(
28 options, "pointers", pointer_option_mappings, POINTER_INSENSITIVE);
29
30 config.struct_abstract_type = option_to_abstract_type(
31 options, "structs", struct_option_mappings, STRUCT_INSENSITIVE);
32
33 config.array_abstract_type = option_to_abstract_type(
34 options, "arrays", array_option_mappings, ARRAY_INSENSITIVE);
35
36 config.union_abstract_type = option_to_abstract_type(
37 options, "unions", union_option_mappings, UNION_INSENSITIVE);
38
39 // This should always be on (for efficiency with 3-way merge)
40 config.context_tracking.last_write_context = true;
41 config.context_tracking.data_dependency_context =
42 options.get_bool_option("data-dependencies");
43 config.context_tracking.liveness = options.get_bool_option("liveness");
44 check_one_of_options(options, {"data-dependencies", "liveness"});
45
46 config.flow_sensitivity = (options.get_bool_option("flow-insensitive"))
47 ? flow_sensitivityt::insensitive
48 : flow_sensitivityt::sensitive;
49
50 config.maximum_array_index = configure_max_array_size(options);
51
52 return config;
53}
54
56{
58 config.context_tracking.last_write_context = true;
59 config.value_abstract_type = CONSTANT;
60 config.pointer_abstract_type = POINTER_SENSITIVE;
61 config.struct_abstract_type = STRUCT_SENSITIVE;
62 config.array_abstract_type = ARRAY_SENSITIVE;
63 config.maximum_array_index = std::numeric_limits<size_t>::max();
64 return config;
65}
66
68{
70 config.value_abstract_type = VALUE_SET;
71 config.pointer_abstract_type = VALUE_SET_OF_POINTERS;
72 config.struct_abstract_type = STRUCT_SENSITIVE;
73 config.array_abstract_type = ARRAY_SENSITIVE;
74 config.maximum_array_index = std::numeric_limits<size_t>::max();
75 return config;
76}
77
79{
81 config.context_tracking.last_write_context = true;
82 config.value_abstract_type = INTERVAL;
83 config.pointer_abstract_type = POINTER_SENSITIVE;
84 config.struct_abstract_type = STRUCT_SENSITIVE;
85 config.array_abstract_type = ARRAY_SENSITIVE;
86 config.maximum_array_index = std::numeric_limits<size_t>::max();
87 return config;
88}
89
91 {"intervals", INTERVAL},
92 {"constants", CONSTANT},
93 {"set-of-constants", VALUE_SET}};
94
96 {"top-bottom", POINTER_INSENSITIVE},
97 {"constants", POINTER_SENSITIVE},
98 {"value-set", VALUE_SET_OF_POINTERS}};
99
101 {"top-bottom", STRUCT_INSENSITIVE},
102 {"every-field", STRUCT_SENSITIVE}};
103
105 {"top-bottom", ARRAY_INSENSITIVE},
106 {"smash", ARRAY_SENSITIVE},
107 {"up-to-n-elements", ARRAY_SENSITIVE},
108 {"every-element", ARRAY_SENSITIVE}};
109
112 {"top-bottom", 0},
113 {"smash", 0},
114 {"up-to-n-elements", 10},
115 {"every-element", std::numeric_limits<size_t>::max()}};
116
118 {"top-bottom", UNION_INSENSITIVE}};
119
120template <class mappingt>
122 const std::string &option_name,
123 const std::string &bad_argument,
124 const mappingt &mapping)
125{
126 auto option = "--vsd-" + option_name;
127 auto choices = std::string("");
128 for(auto &kv : mapping)
129 {
130 choices += (!choices.empty() ? "|" : "");
131 choices += kv.first;
132 }
133
135 "Unknown argument '" + bad_argument + "'", option, option + " " + choices};
136}
137
139 const optionst &options,
140 const std::string &option_name,
141 const option_mappingt &mapping,
142 ABSTRACT_OBJECT_TYPET default_type)
143{
144 const auto argument = options.get_option(option_name);
145
146 if(argument.empty())
147 return default_type;
148
149 auto selected = mapping.find(argument);
150 if(selected == mapping.end())
151 {
152 throw invalid_argument(option_name, argument, mapping);
153 }
154 return selected->second;
155}
156
158{
159 if(options.get_option("arrays") == "up-to-n-elements")
160 {
161 size_t max_elements = options.get_unsigned_int_option("array-max-elements");
162 if(max_elements != 0)
163 return max_elements - 1;
164 }
165 return option_to_size(options, "arrays", array_option_size_mappings);
166}
167
169 const optionst &options,
170 const std::string &option_name,
171 const option_size_mappingt &mapping)
172{
173 const size_t def = std::numeric_limits<size_t>::max();
174 const auto argument = options.get_option(option_name);
175
176 if(argument.empty())
177 return def;
178
179 auto selected = mapping.find(argument);
180 if(selected == mapping.end())
181 {
182 throw invalid_argument(option_name, argument, mapping);
183 }
184 return selected->second;
185}
186
188 const optionst &options,
189 const std::vector<std::string> &names)
190{
191 int how_many = 0;
192 for(auto &name : names)
193 how_many += options.get_bool_option(name);
194
195 if(how_many <= 1)
196 return;
197
198 auto choices = std::string("");
199 for(auto &name : names)
200 {
201 choices += (!choices.empty() ? "|" : "");
202 auto option = "--vsd-" + name;
203 choices += option;
204 }
205
206 throw invalid_command_line_argument_exceptiont{"Conflicting arguments",
207 "Can only use of " + choices};
208}
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
configt config
Definition: config.cpp:25
Options.
std::map< std::string, ABSTRACT_OBJECT_TYPET > option_mappingt
static vsd_configt value_set()
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 intervals()
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,...