CBMC
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#define HELP_VSD \
86 " {y--vsd-values} [{yconstants}|{yintervals}|{yset-of-constants}] \t " \
87 "value tracking\n" \
88 " {y--vsd-structs} [{ytop-bottom}|{yevery-field}] \t " \
89 "struct field sensitive analysis\n" \
90 " {y--vsd-arrays} [{ytop-bottom}|{ysmash}|{yup-to-n-elements}|" \
91 "{yevery-element}] \t " \
92 "array entry sensitive analysis\n" \
93 " {y--vsd-array-max-elements} {uN} \t " \
94 "set the {un} in {y--vsd-arrays} {yup-to-n-elements} (defaults to 10 if " \
95 "not given)\n" \
96 " {y--vsd-pointers} [{ytop-bottom}|{yconstants}|{yvalue-set}] \t " \
97 "pointer sensitive analysis\n" \
98 " {y--vsd-unions} [{ytop-bottom}] \t union sensitive analysis\n" \
99 " {y--vsd-data-dependencies} \t track data dependencies\n" \
100 " {y--vsd-liveness} \t track variable liveness\n" \
101 " {y--vsd-flow-insensitive} \t disables flow sensitivity\n"
102
103#define PARSE_OPTIONS_VSD(cmdline, options) \
104 options.set_option("values", cmdline.get_value("vsd-values")); \
105 options.set_option("pointers", cmdline.get_value("vsd-pointers")); \
106 options.set_option("arrays", cmdline.get_value("vsd-arrays")); \
107 options.set_option("array-max-elements", cmdline.get_value("vsd-array-max-elements")); /* NOLINT(whitespace/line_length) */ \
108 options.set_option("structs", cmdline.get_value("vsd-structs")); \
109 options.set_option("unions", cmdline.get_value("vsd-unions")); \
110 options.set_option("flow-insensitive", cmdline.isset("vsd-flow-insensitive")); /* NOLINT(whitespace/line_length) */ \
111 options.set_option("data-dependencies", cmdline.isset("vsd-data-dependencies")); /* NOLINT(whitespace/line_length) */ \
112 options.set_option("liveness", cmdline.isset("vsd-liveness")); /* NOLINT(whitespace/line_length) */ \
113 (void)0
114
116{
117public:
125
134 void transform(
135 const irep_idt &function_from,
137 const irep_idt &function_to,
139 ai_baset &ai,
140 const namespacet &ns) override;
141
143 void make_bottom() override;
144
146 void make_top() override;
147
153 void output(std::ostream &out, const ai_baset &ai, const namespacet &ns)
154 const override;
155
160 exprt to_predicate() const override;
161
162 exprt to_predicate(const exprt &expr, const namespacet &ns) const;
163 exprt to_predicate(const exprt::operandst &exprs, const namespacet &ns) const;
164
172 virtual bool
174
188 const namespacet &ns);
189
198 bool ai_simplify(exprt &condition, const namespacet &ns) const override;
199
203 bool is_bottom() const override;
204
208 bool is_top() const override;
209
211 eval(const exprt &expr, const namespacet &ns) const
212 {
213 return abstract_state.eval(expr, ns);
214 }
215
216private:
232 ai_baset &ai,
233 const namespacet &ns);
234
241 bool ignore_function_call_transform(const irep_idt &function_id) const;
242
243 void assume(exprt expr, namespacet ns);
244
247
248#ifdef ENABLE_STATS
249public:
250 abstract_object_statisticst gather_statistics(const namespacet &ns) const;
251#endif
252};
253
255 : public ai_domain_factoryt<variable_sensitivity_domaint>
256{
257public:
264
265 std::unique_ptr<statet> make(locationt l) const override
266 {
267 auto d = std::make_unique<variable_sensitivity_domaint>(
269 CHECK_RETURN(d->is_bottom());
270 return std::unique_ptr<statet>(d.release());
271 }
272
273private:
276};
277
278#ifdef ENABLE_STATS
279template <>
281{
283 void
284 add_entry(const variable_sensitivity_domaint &domain, const namespacet &ns)
285 {
286 auto statistics = domain.gather_statistics(ns);
287 total_statistics.number_of_interval_abstract_objects +=
288 statistics.number_of_interval_abstract_objects;
289 total_statistics.number_of_globals += statistics.number_of_globals;
290 total_statistics.number_of_single_value_intervals +=
291 statistics.number_of_single_value_intervals;
292 total_statistics.number_of_constants += statistics.number_of_constants;
293 total_statistics.number_of_pointers += statistics.number_of_constants;
294 total_statistics.number_of_arrays += statistics.number_of_arrays;
295 total_statistics.number_of_structs += statistics.number_of_arrays;
296 total_statistics.objects_memory_usage += statistics.objects_memory_usage;
297 }
298
299 void print(std::ostream &out) const
300 {
301 out << "<< Begin Variable Sensitivity Domain Statistics >>\n"
302 << " Memory Usage: "
303 << total_statistics.objects_memory_usage.to_string() << '\n'
304 << " Number of structs: " << total_statistics.number_of_structs << '\n'
305 << " Number of arrays: " << total_statistics.number_of_arrays << '\n'
306 << " Number of pointers: " << total_statistics.number_of_pointers
307 << '\n'
308 << " Number of constants: " << total_statistics.number_of_constants
309 << '\n'
310 << " Number of intervals: "
311 << total_statistics.number_of_interval_abstract_objects << '\n'
312 << " Number of single value intervals: "
313 << total_statistics.number_of_single_value_intervals << '\n'
314 << " Number of globals: " << total_statistics.number_of_globals << '\n'
315 << "<< End Variable Sensitivity Domain Statistics >>\n";
316 }
317};
318#endif
319
320#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:117
The interface offered by a domain, allows code to manipulate domains without knowing their exact type...
Definition ai_domain.h:54
ai_history_baset::trace_ptrt trace_ptrt
Definition ai_domain.h:73
goto_programt::const_targett locationt
Definition ai_domain.h:72
ai_domain_factory_baset::locationt locationt
Definition ai_domain.h:203
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
ait()
Definition ai.h:565
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:38
Base class for all expressions.
Definition expr.h:56
std::vector< exprt > operandst
Definition expr.h:58
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 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 void merge_three_way_function_return(const ai_domain_baset &function_start, const ai_domain_baset &function_end, const namespacet &ns)
Merges just the things that have changes between "function_start" and "function_end" into "this".
virtual abstract_object_pointert eval(const exprt &expr, const namespacet &ns) const
bool is_bottom() const override
Find out if the domain is currently unreachable.
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...
#define CHECK_RETURN(CONDITION)
Definition invariant.h:495
Captures the user-supplied configuration for VSD, determining which domain abstractions are used,...