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,
291 return std::unique_ptr<statet>(d.release());
307 auto statistics = domain.gather_statistics(ns);
309 statistics.number_of_interval_abstract_objects;
312 statistics.number_of_single_value_intervals;
320 void print(std::ostream &out)
const
322 out <<
"<< Begin Variable Sensitivity Domain Statistics >>\n"
331 <<
" Number of intervals: "
333 <<
" Number of single value intervals: "
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_factory_baset::locationt locationt
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
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,...