Go to the documentation of this file.
64 #ifndef CPROVER_ANALYSES_VARIABLE_SENSITIVITY_VARIABLE_SENSITIVITY_DOMAIN_H
65 #define CPROVER_ANALYSES_VARIABLE_SENSITIVITY_VARIABLE_SENSITIVITY_DOMAIN_H
81 "(vsd-flow-insensitive)" \
82 "(vsd-data-dependencies)"
86 " --vsd-values value tracking - constants|intervals|set-of-constants\n" \
87 " --vsd-structs struct field sensitive analysis - top-bottom|every-field\n" \
88 " --vsd-arrays array entry sensitive analysis - top-bottom|every-element\n" \
89 " --vsd-pointers pointer sensitive analysis - top-bottom|constants|value-set\n" \
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" \
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")); \
103 options.set_option("data-dependencies", cmdline.isset("vsd-data-dependencies")); \
196 bool is_top()
const override;
234 std::vector<irep_idt>
243 std::vector<symbol_exprt> modified_symbols,
269 auto d = util_make_unique<variable_sensitivity_domaint>(
272 return std::unique_ptr<statet>(d.release());
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;
301 void print(std::ostream &out)
const
303 out <<
"<< Begin Variable Sensitivity Domain Statistics >>\n"
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
310 <<
" Number of constants: " << total_statistics.number_of_constants
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";
322 #endif // CPROVER_ANALYSES_VARIABLE_SENSITIVITY_VARIABLE_SENSITIVITY_DOMAIN_H
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
sharing_ptrt< class abstract_objectt > abstract_object_pointert
#define CHECK_RETURN(CONDITION)
variable_sensitivity_domaint(variable_sensitivity_object_factory_ptrt _object_factory, const vsd_configt &_configuration)
bool is_bottom() const override
Find out if the domain is currently unreachable.
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...
virtual abstract_object_pointert eval(const exprt &expr, const namespacet &ns) const
Base class for all expressions.
variable_sensitivity_domain_factoryt(variable_sensitivity_object_factory_ptrt _object_factory, const vsd_configt &_configuration)
ai_history_baset::trace_ptrt trace_ptrt
std::vector< irep_idt > get_modified_symbols(const variable_sensitivity_domaint &other) const
Get symbols that have been modified since this domain and other.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
void make_bottom() override
Sets the domain to bottom (no states / unreachable).
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.
std::shared_ptr< variable_sensitivity_object_factoryt > variable_sensitivity_object_factory_ptrt
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...
abstract_environmentt abstract_state
An abstract version of a program environment.
std::unique_ptr< statet > make(locationt l) const override
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
These three are really the heart of the method.
bool is_top() const override
Is the domain completely top at this state.
void output(std::ostream &out, const ai_baset &ai, const namespacet &ns) const override
Basic text output of the abstract domain.
goto_programt::const_targett locationt
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.
This is the basic interface of the abstract interpreter with default implementations of the core func...
void make_entry() override
Set up a reasonable entry-point state.
ai_domain_baset::locationt locationt
virtual bool merge(const variable_sensitivity_domaint &b, trace_ptrt from, trace_ptrt to)
Computes the join between "this" and "b".
The interface offered by a domain, allows code to manipulate domains without knowing their exact type...
Captures the user-supplied configuration for VSD, determining which domain abstractions are used,...
void make_top() override
Sets the domain to top (all states).
flow_sensitivityt flow_sensitivity
void output(std::ostream &out) const
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.