cprover
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 
16 static 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"))
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 
120 template <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,...