cprover
variable_sensitivity_domain.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3  Module: analyses variable-sensitivity
4 
5  Author: Thomas Kiley, thomas.kiley@diffblue.com
6 
7 \*******************************************************************/
8 
63 
64 #ifndef CPROVER_ANALYSES_VARIABLE_SENSITIVITY_VARIABLE_SENSITIVITY_DOMAIN_H
65 #define CPROVER_ANALYSES_VARIABLE_SENSITIVITY_VARIABLE_SENSITIVITY_DOMAIN_H
66 
67 #include <iosfwd>
68 #include <map>
69 #include <memory>
70 
71 #include <analyses/ai.h>
74 
75 #define OPT_VSD \
76  "(vsd-values):" \
77  "(vsd-structs):" \
78  "(vsd-arrays):" \
79  "(vsd-pointers):" \
80  "(vsd-unions):" \
81  "(vsd-flow-insensitive)" \
82  "(vsd-data-dependencies)"
83 
84 // clang-format off
85 #define HELP_VSD \
86  " --vsd-values value tracking - constants|intervals|set-of-constants\n" /* NOLINT(whitespace/line_length) */ \
87  " --vsd-structs struct field sensitive analysis - top-bottom|every-field\n" /* NOLINT(whitespace/line_length) */ \
88  " --vsd-arrays array entry sensitive analysis - top-bottom|every-element\n" /* NOLINT(whitespace/line_length) */ \
89  " --vsd-pointers pointer sensitive analysis - top-bottom|constants|value-set\n" /* NOLINT(whitespace/line_length) */ \
90  " --vsd-unions union sensitive analysis - top-bottom\n" \
91  " --vsd-flow-insensitive disables flow sensitivity\n" \
92  " --vsd-data-dependencies track data dependencies\n" \
93 
94 // cland-format on
95 
96 #define PARSE_OPTIONS_VSD(cmdline, options) \
97  options.set_option("values", cmdline.get_value("vsd-values")); \
98  options.set_option("pointers", cmdline.get_value("vsd-pointers")); \
99  options.set_option("arrays", cmdline.get_value("vsd-arrays")); \
100  options.set_option("structs", cmdline.get_value("vsd-structs")); \
101  options.set_option("unions", cmdline.get_value("vsd-unions")); \
102  options.set_option("flow-insensitive", cmdline.isset("vsd-flow-insensitive")); /* NOLINT(whitespace/line_length) */ \
103  options.set_option("data-dependencies", cmdline.isset("vsd-data-dependencies")); /* NOLINT(whitespace/line_length) */ \
104  (void)0
105 
107 {
108 public:
111  const vsd_configt &_configuration)
112  : abstract_state(_object_factory),
113  flow_sensitivity(_configuration.flow_sensitivity)
114  {
115  }
116 
125  void transform(
126  const irep_idt &function_from,
127  trace_ptrt trace_from,
128  const irep_idt &function_to,
129  trace_ptrt trace_to,
130  ai_baset &ai,
131  const namespacet &ns) override;
132 
134  void make_bottom() override;
135 
137  void make_top() override;
138 
140  void make_entry() override;
141 
147  void output(std::ostream &out, const ai_baset &ai, const namespacet &ns)
148  const override;
149 
150  void output(std::ostream &out) const;
151 
159  virtual bool
161 
172  virtual void merge_three_way_function_return(
173  const ai_domain_baset &function_call,
174  const ai_domain_baset &function_start,
175  const ai_domain_baset &function_end,
176  const namespacet &ns);
177 
186  bool ai_simplify(exprt &condition, const namespacet &ns) const override;
187 
191  bool is_bottom() const override;
192 
196  bool is_top() const override;
197 
199  eval(const exprt &expr, const namespacet &ns) const
200  {
201  return abstract_state.eval(expr, ns);
202  }
203 
204 private:
218  locationt from,
219  locationt to,
220  ai_baset &ai,
221  const namespacet &ns);
222 
229  bool ignore_function_call_transform(const irep_idt &function_id) const;
230 
234  std::vector<irep_idt>
236 
242  void apply_domain(
243  std::vector<symbol_exprt> modified_symbols,
244  const variable_sensitivity_domaint &target,
245  const namespacet &ns);
246 
249 
250 #ifdef ENABLE_STATS
251 public:
252  abstract_object_statisticst gather_statistics(const namespacet &ns) const;
253 #endif
254 };
255 
257  : public ai_domain_factoryt<variable_sensitivity_domaint>
258 {
259 public:
262  const vsd_configt &_configuration)
263  : object_factory(_object_factory), configuration(_configuration)
264  {
265  }
266 
267  std::unique_ptr<statet> make(locationt l) const override
268  {
269  auto d = util_make_unique<variable_sensitivity_domaint>(
271  CHECK_RETURN(d->is_bottom());
272  return std::unique_ptr<statet>(d.release());
273  }
274 
275 private:
278 };
279 
280 #ifdef ENABLE_STATS
281 template <>
282 struct get_domain_statisticst<variable_sensitivity_domaint>
283 {
284  abstract_object_statisticst total_statistics = {};
285  void
286  add_entry(const variable_sensitivity_domaint &domain, const namespacet &ns)
287  {
288  auto statistics = domain.gather_statistics(ns);
289  total_statistics.number_of_interval_abstract_objects +=
290  statistics.number_of_interval_abstract_objects;
291  total_statistics.number_of_globals += statistics.number_of_globals;
292  total_statistics.number_of_single_value_intervals +=
293  statistics.number_of_single_value_intervals;
294  total_statistics.number_of_constants += statistics.number_of_constants;
295  total_statistics.number_of_pointers += statistics.number_of_constants;
296  total_statistics.number_of_arrays += statistics.number_of_arrays;
297  total_statistics.number_of_structs += statistics.number_of_arrays;
298  total_statistics.objects_memory_usage += statistics.objects_memory_usage;
299  }
300 
301  void print(std::ostream &out) const
302  {
303  out << "<< Begin Variable Sensitivity Domain Statistics >>\n"
304  << " Memory Usage: "
305  << total_statistics.objects_memory_usage.to_string() << '\n'
306  << " Number of structs: " << total_statistics.number_of_structs << '\n'
307  << " Number of arrays: " << total_statistics.number_of_arrays << '\n'
308  << " Number of pointers: " << total_statistics.number_of_pointers
309  << '\n'
310  << " Number of constants: " << total_statistics.number_of_constants
311  << '\n'
312  << " Number of intervals: "
313  << total_statistics.number_of_interval_abstract_objects << '\n'
314  << " Number of single value intervals: "
315  << total_statistics.number_of_single_value_intervals << '\n'
316  << " Number of globals: " << total_statistics.number_of_globals << '\n'
317  << "<< End Variable Sensitivity Domain Statistics >>\n";
318  }
319 };
320 #endif
321 
322 #endif // CPROVER_ANALYSES_VARIABLE_SENSITIVITY_VARIABLE_SENSITIVITY_DOMAIN_H
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
abstract_object_pointert
sharing_ptrt< class abstract_objectt > abstract_object_pointert
Definition: abstract_object.h:75
flow_sensitivityt
flow_sensitivityt
Definition: variable_sensitivity_configuration.h:35
CHECK_RETURN
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:496
variable_sensitivity_domaint::variable_sensitivity_domaint
variable_sensitivity_domaint(variable_sensitivity_object_factory_ptrt _object_factory, const vsd_configt &_configuration)
Definition: variable_sensitivity_domain.h:109
variable_sensitivity_domaint::is_bottom
bool is_bottom() const override
Find out if the domain is currently unreachable.
Definition: variable_sensitivity_domain.cpp:242
variable_sensitivity_domaint::ignore_function_call_transform
bool ignore_function_call_transform(const irep_idt &function_id) const
Used to specify which CPROVER internal functions should be skipped over when doing function call tran...
Definition: variable_sensitivity_domain.cpp:381
variable_sensitivity_domaint::eval
virtual abstract_object_pointert eval(const exprt &expr, const namespacet &ns) const
Definition: variable_sensitivity_domain.h:199
abstract_environmentt
Definition: abstract_environment.h:36
exprt
Base class for all expressions.
Definition: expr.h:54
vsd_configt
Definition: variable_sensitivity_configuration.h:41
variable_sensitivity_domain_factoryt::variable_sensitivity_domain_factoryt
variable_sensitivity_domain_factoryt(variable_sensitivity_object_factory_ptrt _object_factory, const vsd_configt &_configuration)
Definition: variable_sensitivity_domain.h:260
ai_domain_baset::trace_ptrt
ai_history_baset::trace_ptrt trace_ptrt
Definition: ai_domain.h:78
variable_sensitivity_domaint::get_modified_symbols
std::vector< irep_idt > get_modified_symbols(const variable_sensitivity_domaint &other) const
Get symbols that have been modified since this domain and other.
Definition: variable_sensitivity_domain.cpp:252
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
variable_sensitivity_domaint::make_bottom
void make_bottom() override
Sets the domain to bottom (no states / unreachable).
Definition: variable_sensitivity_domain.cpp:182
variable_sensitivity_domain_factoryt::object_factory
variable_sensitivity_object_factory_ptrt object_factory
Definition: variable_sensitivity_domain.h:276
variable_sensitivity_domain_factoryt::configuration
const vsd_configt configuration
Definition: variable_sensitivity_domain.h:277
abstract_object_statisticst
Definition: abstract_object_statistics.h:19
variable_sensitivity_domaint::apply_domain
void apply_domain(std::vector< symbol_exprt > modified_symbols, const variable_sensitivity_domaint &target, const namespacet &ns)
Given a domain and some symbols, apply those symbols values to the current domain.
Definition: variable_sensitivity_domain.cpp:429
variable_sensitivity_object_factory_ptrt
std::shared_ptr< variable_sensitivity_object_factoryt > variable_sensitivity_object_factory_ptrt
Definition: abstract_environment.h:33
variable_sensitivity_domaint::merge_three_way_function_return
virtual void merge_three_way_function_return(const ai_domain_baset &function_call, const ai_domain_baset &function_start, const ai_domain_baset &function_end, const namespacet &ns)
Perform a context aware merge of the changes that have been applied between function_start and the cu...
Definition: variable_sensitivity_domain.cpp:397
variable_sensitivity_domaint::abstract_state
abstract_environmentt abstract_state
Definition: variable_sensitivity_domain.h:247
abstract_environment.h
An abstract version of a program environment.
variable_sensitivity_domain_factoryt::make
std::unique_ptr< statet > make(locationt l) const override
Definition: variable_sensitivity_domain.h:267
variable_sensitivity_domaint::transform
void transform(const irep_idt &function_from, trace_ptrt trace_from, const irep_idt &function_to, trace_ptrt trace_to, ai_baset &ai, const namespacet &ns) override
Compute the abstract transformer for a single instruction.
Definition: variable_sensitivity_domain.cpp:24
abstract_environmentt::eval
virtual abstract_object_pointert eval(const exprt &expr, const namespacet &ns) const
These three are really the heart of the method.
Definition: abstract_environment.cpp:37
variable_sensitivity_domaint::is_top
bool is_top() const override
Is the domain completely top at this state.
Definition: variable_sensitivity_domain.cpp:247
ai.h
Abstract Interpretation.
variable_sensitivity_domain_factoryt
Definition: variable_sensitivity_domain.h:258
variable_sensitivity_domaint::output
void output(std::ostream &out, const ai_baset &ai, const namespacet &ns) const override
Basic text output of the abstract domain.
Definition: variable_sensitivity_domain.cpp:174
ai_domain_baset::locationt
goto_programt::const_targett locationt
Definition: ai_domain.h:77
ai_domain_factoryt
Definition: ai_domain.h:201
variable_sensitivity_domaint::ai_simplify
bool ai_simplify(exprt &condition, const namespacet &ns) const override
Use the information in the domain to simplify the expression with respect to the current location.
Definition: variable_sensitivity_domain.cpp:215
ai_baset
This is the basic interface of the abstract interpreter with default implementations of the core func...
Definition: ai.h:120
variable_sensitivity_domaint
Definition: variable_sensitivity_domain.h:107
variable_sensitivity_domaint::make_entry
void make_entry() override
Set up a reasonable entry-point state.
Definition: variable_sensitivity_domain.cpp:193
ai_domain_factory_baset::locationt
ai_domain_baset::locationt locationt
Definition: ai_domain.h:175
variable_sensitivity_domaint::merge
virtual bool merge(const variable_sensitivity_domaint &b, trace_ptrt from, trace_ptrt to)
Computes the join between "this" and "b".
Definition: variable_sensitivity_domain.cpp:198
ai_domain_baset
The interface offered by a domain, allows code to manipulate domains without knowing their exact type...
Definition: ai_domain.h:59
variable_sensitivity_configuration.h
Captures the user-supplied configuration for VSD, determining which domain abstractions are used,...
variable_sensitivity_domaint::make_top
void make_top() override
Sets the domain to top (all states).
Definition: variable_sensitivity_domain.cpp:188
variable_sensitivity_domaint::flow_sensitivity
flow_sensitivityt flow_sensitivity
Definition: variable_sensitivity_domain.h:248
variable_sensitivity_domaint::output
void output(std::ostream &out) const
variable_sensitivity_domaint::transform_function_call
void transform_function_call(locationt from, locationt to, ai_baset &ai, const namespacet &ns)
Used by variable_sensitivity_domaint::transform to handle FUNCTION_CALL transforms.
Definition: variable_sensitivity_domain.cpp:259