cprover
Loading...
Searching...
No Matches
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 <memory>
69
70#include <analyses/ai_domain.h>
73
74#define OPT_VSD \
75 "(vsd-values):" \
76 "(vsd-structs):" \
77 "(vsd-arrays):" \
78 "(vsd-array-max-elements):" \
79 "(vsd-pointers):" \
80 "(vsd-unions):" \
81 "(vsd-flow-insensitive)" \
82 "(vsd-data-dependencies)" \
83 "(vsd-liveness)" \
84 \
85 // clang-format off
86#define HELP_VSD \
87 " --vsd-values value tracking - " \
88 "constants|intervals|set-of-constants\n" /* NOLINT(whitespace/line_length) */\
89 " --vsd-structs struct field sensitive analysis - " \
90 "top-bottom|every-field\n" /* NOLINT(whitespace/line_length) */ \
91 " --vsd-arrays array entry sensitive analysis - " \
92 "top-bottom|smash|up-to-n-elements|every-element\n" /* NOLINT(whitespace/line_length) */ \
93 " --vsd-array-max-elements the n in --vsd-arrays up-to-n-elements - " \
94 "defaults 10 if not given\n" /* NOLINT(whitespace/line_length) */ \
95 " --vsd-pointers pointer sensitive analysis - " \
96 "top-bottom|constants|value-set\n" /* NOLINT(whitespace/line_length) */ \
97 " --vsd-unions union sensitive analysis - top-bottom\n" \
98 " --vsd-flow-insensitive disables flow sensitivity\n" \
99 " --vsd-data-dependencies track data dependencies\n" \
100 " --vsd-liveness track variable liveness\n" \
101
102// cland-format on
103
104#define PARSE_OPTIONS_VSD(cmdline, options) \
105 options.set_option("values", cmdline.get_value("vsd-values")); \
106 options.set_option("pointers", cmdline.get_value("vsd-pointers")); \
107 options.set_option("arrays", cmdline.get_value("vsd-arrays")); \
108 options.set_option("array-max-elements", cmdline.get_value("vsd-array-max-elements")); /* NOLINT(whitespace/line_length) */ \
109 options.set_option("structs", cmdline.get_value("vsd-structs")); \
110 options.set_option("unions", cmdline.get_value("vsd-unions")); \
111 options.set_option("flow-insensitive", cmdline.isset("vsd-flow-insensitive")); /* NOLINT(whitespace/line_length) */ \
112 options.set_option("data-dependencies", cmdline.isset("vsd-data-dependencies")); /* NOLINT(whitespace/line_length) */ \
113 options.set_option("liveness", cmdline.isset("vsd-liveness")); /* NOLINT(whitespace/line_length) */ \
114 (void)0
115
117{
118public:
121 const vsd_configt &_configuration)
122 : abstract_state(_object_factory),
123 flow_sensitivity(_configuration.flow_sensitivity)
124 {
125 }
126
135 void transform(
136 const irep_idt &function_from,
137 trace_ptrt trace_from,
138 const irep_idt &function_to,
139 trace_ptrt trace_to,
140 ai_baset &ai,
141 const namespacet &ns) override;
142
144 void make_bottom() override;
145
147 void make_top() override;
148
150 void make_entry() override;
151
157 void output(std::ostream &out, const ai_baset &ai, const namespacet &ns)
158 const override;
159
164 exprt to_predicate() const override;
165
166 exprt to_predicate(const exprt &expr, const namespacet &ns) const;
167 exprt to_predicate(const exprt::operandst &exprs, const namespacet &ns) const;
168
176 virtual bool
178
190 const ai_domain_baset &function_call,
191 const ai_domain_baset &function_start,
192 const ai_domain_baset &function_end,
193 const namespacet &ns);
194
203 bool ai_simplify(exprt &condition, const namespacet &ns) const override;
204
208 bool is_bottom() const override;
209
213 bool is_top() const override;
214
216 eval(const exprt &expr, const namespacet &ns) const
217 {
218 return abstract_state.eval(expr, ns);
219 }
220
221private:
235 locationt from,
236 locationt to,
237 ai_baset &ai,
238 const namespacet &ns);
239
246 bool ignore_function_call_transform(const irep_idt &function_id) const;
247
251 std::vector<irep_idt>
253
259 void apply_domain(
260 std::vector<symbol_exprt> modified_symbols,
261 const variable_sensitivity_domaint &target,
262 const namespacet &ns);
263
264 void assume(exprt expr, namespacet ns);
265
268
269#ifdef ENABLE_STATS
270public:
271 abstract_object_statisticst gather_statistics(const namespacet &ns) const;
272#endif
273};
274
276 : public ai_domain_factoryt<variable_sensitivity_domaint>
277{
278public:
281 const vsd_configt &_configuration)
282 : object_factory(_object_factory), configuration(_configuration)
283 {
284 }
285
286 std::unique_ptr<statet> make(locationt l) const override
287 {
288 auto d = util_make_unique<variable_sensitivity_domaint>(
290 CHECK_RETURN(d->is_bottom());
291 return std::unique_ptr<statet>(d.release());
292 }
293
294private:
297};
298
299#ifdef ENABLE_STATS
300template <>
301struct get_domain_statisticst<variable_sensitivity_domaint>
302{
303 abstract_object_statisticst total_statistics = {};
304 void
305 add_entry(const variable_sensitivity_domaint &domain, const namespacet &ns)
306 {
307 auto statistics = domain.gather_statistics(ns);
308 total_statistics.number_of_interval_abstract_objects +=
309 statistics.number_of_interval_abstract_objects;
310 total_statistics.number_of_globals += statistics.number_of_globals;
311 total_statistics.number_of_single_value_intervals +=
312 statistics.number_of_single_value_intervals;
313 total_statistics.number_of_constants += statistics.number_of_constants;
314 total_statistics.number_of_pointers += statistics.number_of_constants;
315 total_statistics.number_of_arrays += statistics.number_of_arrays;
316 total_statistics.number_of_structs += statistics.number_of_arrays;
317 total_statistics.objects_memory_usage += statistics.objects_memory_usage;
318 }
319
320 void print(std::ostream &out) const
321 {
322 out << "<< Begin Variable Sensitivity Domain Statistics >>\n"
323 << " Memory Usage: "
324 << total_statistics.objects_memory_usage.to_string() << '\n'
325 << " Number of structs: " << total_statistics.number_of_structs << '\n'
326 << " Number of arrays: " << total_statistics.number_of_arrays << '\n'
327 << " Number of pointers: " << total_statistics.number_of_pointers
328 << '\n'
329 << " Number of constants: " << total_statistics.number_of_constants
330 << '\n'
331 << " Number of intervals: "
332 << total_statistics.number_of_interval_abstract_objects << '\n'
333 << " Number of single value intervals: "
334 << total_statistics.number_of_single_value_intervals << '\n'
335 << " Number of globals: " << total_statistics.number_of_globals << '\n'
336 << "<< End Variable Sensitivity Domain Statistics >>\n";
337 }
338};
339#endif
340
341#endif // CPROVER_ANALYSES_VARIABLE_SENSITIVITY_VARIABLE_SENSITIVITY_DOMAIN_H
An abstract version of a program environment.
std::shared_ptr< variable_sensitivity_object_factoryt > variable_sensitivity_object_factory_ptrt
sharing_ptrt< class abstract_objectt > abstract_object_pointert
Abstract Interpretation Domain.
virtual abstract_object_pointert eval(const exprt &expr, const namespacet &ns) const
These three are really the heart of the method.
This is the basic interface of the abstract interpreter with default implementations of the core func...
Definition ai.h:119
The interface offered by a domain, allows code to manipulate domains without knowing their exact type...
Definition ai_domain.h:55
ai_history_baset::trace_ptrt trace_ptrt
Definition ai_domain.h:74
goto_programt::const_targett locationt
Definition ai_domain.h:73
ai_domain_factory_baset::locationt locationt
Definition ai_domain.h:200
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:37
Base class for all expressions.
Definition expr.h:54
std::vector< exprt > operandst
Definition expr.h:56
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
variable_sensitivity_object_factory_ptrt object_factory
variable_sensitivity_domain_factoryt(variable_sensitivity_object_factory_ptrt _object_factory, const vsd_configt &_configuration)
std::unique_ptr< statet > make(locationt l) const override
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.
exprt to_predicate() const override
Gives a Boolean condition that is true for all values represented by the domain.
void make_bottom() override
Sets the domain to bottom (no states / unreachable).
void output(std::ostream &out, const ai_baset &ai, const namespacet &ns) const override
Basic text output of the abstract domain.
void make_top() override
Sets the domain to top (all states).
variable_sensitivity_domaint(variable_sensitivity_object_factory_ptrt _object_factory, const vsd_configt &_configuration)
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.
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.
virtual abstract_object_pointert eval(const exprt &expr, const namespacet &ns) const
std::vector< irep_idt > get_modified_symbols(const variable_sensitivity_domaint &other) const
Get symbols that have been modified since this domain and other.
bool is_bottom() const override
Find out if the domain is currently unreachable.
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...
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.
virtual bool merge(const variable_sensitivity_domaint &b, trace_ptrt from, trace_ptrt to)
Computes the join between "this" and "b".
void assume(exprt expr, namespacet ns)
bool is_top() const override
Is the domain completely top at this state.
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...
void make_entry() override
Set up a reasonable entry-point state.
#define CHECK_RETURN(CONDITION)
Definition invariant.h:495
Captures the user-supplied configuration for VSD, determining which domain abstractions are used,...