64#ifndef CPROVER_ANALYSES_VARIABLE_SENSITIVITY_VARIABLE_SENSITIVITY_DOMAIN_H
65#define CPROVER_ANALYSES_VARIABLE_SENSITIVITY_VARIABLE_SENSITIVITY_DOMAIN_H
78 "(vsd-array-max-elements):" \
81 "(vsd-flow-insensitive)" \
82 "(vsd-data-dependencies)" \
87 " --vsd-values value tracking - " \
88 "constants|intervals|set-of-constants\n"
\
89 " --vsd-structs struct field sensitive analysis - " \
90 "top-bottom|every-field\n"
\
91 " --vsd-arrays array entry sensitive analysis - " \
92 "top-bottom|smash|up-to-n-elements|every-element\n"
\
93 " --vsd-array-max-elements the n in --vsd-arrays up-to-n-elements - " \
94 "defaults 10 if not given\n"
\
95 " --vsd-pointers pointer sensitive analysis - " \
96 "top-bottom|constants|value-set\n"
\
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" \
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"));
\
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"));
\
112 options.set_option("data-dependencies", cmdline.isset("vsd-data-dependencies"));
\
113 options.set_option("liveness", cmdline.isset("vsd-liveness"));
\
213 bool is_top()
const override;
251 std::vector<irep_idt>
260 std::vector<symbol_exprt> modified_symbols,
288 auto d = util_make_unique<variable_sensitivity_domaint>(
291 return std::unique_ptr<statet>(d.release());
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;
320 void print(std::ostream &out)
const
322 out <<
"<< Begin Variable Sensitivity Domain Statistics >>\n"
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
329 <<
" Number of constants: " << total_statistics.number_of_constants
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";
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...
The interface offered by a domain, allows code to manipulate domains without knowing their exact type...
ai_history_baset::trace_ptrt trace_ptrt
goto_programt::const_targett locationt
ai_domain_baset::locationt locationt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Base class for all expressions.
std::vector< exprt > operandst
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
const vsd_configt configuration
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.
abstract_environmentt abstract_state
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".
flow_sensitivityt flow_sensitivity
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)
Captures the user-supplied configuration for VSD, determining which domain abstractions are used,...