cprover
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 <map>
69 #include <memory>
70 
71 #include <analyses/ai.h>
74 
76 {
77 public:
80  const vsd_configt &_configuration)
81  : abstract_state(_object_factory),
82  flow_sensitivity(_configuration.flow_sensitivity)
83  {
84  }
85 
94  void transform(
95  const irep_idt &function_from,
96  trace_ptrt trace_from,
97  const irep_idt &function_to,
98  trace_ptrt trace_to,
99  ai_baset &ai,
100  const namespacet &ns) override;
101 
103  void make_bottom() override;
104 
106  void make_top() override;
107 
109  void make_entry() override;
110 
116  void output(std::ostream &out, const ai_baset &ai, const namespacet &ns)
117  const override;
118 
119  void output(std::ostream &out) const;
120 
128  virtual bool
130 
141  virtual void merge_three_way_function_return(
142  const ai_domain_baset &function_call,
143  const ai_domain_baset &function_start,
144  const ai_domain_baset &function_end,
145  const namespacet &ns);
146 
155  bool ai_simplify(exprt &condition, const namespacet &ns) const override;
156 
160  bool is_bottom() const override;
161 
165  bool is_top() const override;
166 
168  eval(const exprt &expr, const namespacet &ns) const
169  {
170  return abstract_state.eval(expr, ns);
171  }
172 
173 private:
187  locationt from,
188  locationt to,
189  ai_baset &ai,
190  const namespacet &ns);
191 
198  bool ignore_function_call_transform(const irep_idt &function_id) const;
199 
203  std::vector<irep_idt>
205 
211  void apply_domain(
212  std::vector<symbol_exprt> modified_symbols,
213  const variable_sensitivity_domaint &target,
214  const namespacet &ns);
215 
218 
219 #ifdef ENABLE_STATS
220 public:
221  abstract_object_statisticst gather_statistics(const namespacet &ns) const;
222 #endif
223 };
224 
226  : public ai_domain_factoryt<variable_sensitivity_domaint>
227 {
228 public:
231  const vsd_configt &_configuration)
232  : object_factory(_object_factory), configuration(_configuration)
233  {
234  }
235 
236  std::unique_ptr<statet> make(locationt l) const override
237  {
238  auto d = util_make_unique<variable_sensitivity_domaint>(
240  CHECK_RETURN(d->is_bottom());
241  return std::unique_ptr<statet>(d.release());
242  }
243 
244 private:
247 };
248 
249 #ifdef ENABLE_STATS
250 template <>
251 struct get_domain_statisticst<variable_sensitivity_domaint>
252 {
253  abstract_object_statisticst total_statistics = {};
254  void
255  add_entry(const variable_sensitivity_domaint &domain, const namespacet &ns)
256  {
257  auto statistics = domain.gather_statistics(ns);
258  total_statistics.number_of_interval_abstract_objects +=
259  statistics.number_of_interval_abstract_objects;
260  total_statistics.number_of_globals += statistics.number_of_globals;
261  total_statistics.number_of_single_value_intervals +=
262  statistics.number_of_single_value_intervals;
263  total_statistics.number_of_constants += statistics.number_of_constants;
264  total_statistics.number_of_pointers += statistics.number_of_constants;
265  total_statistics.number_of_arrays += statistics.number_of_arrays;
266  total_statistics.number_of_structs += statistics.number_of_arrays;
267  total_statistics.objects_memory_usage += statistics.objects_memory_usage;
268  }
269 
270  void print(std::ostream &out) const
271  {
272  out << "<< Begin Variable Sensitivity Domain Statistics >>\n"
273  << " Memory Usage: "
274  << total_statistics.objects_memory_usage.to_string() << '\n'
275  << " Number of structs: " << total_statistics.number_of_structs << '\n'
276  << " Number of arrays: " << total_statistics.number_of_arrays << '\n'
277  << " Number of pointers: " << total_statistics.number_of_pointers
278  << '\n'
279  << " Number of constants: " << total_statistics.number_of_constants
280  << '\n'
281  << " Number of intervals: "
282  << total_statistics.number_of_interval_abstract_objects << '\n'
283  << " Number of single value intervals: "
284  << total_statistics.number_of_single_value_intervals << '\n'
285  << " Number of globals: " << total_statistics.number_of_globals << '\n'
286  << "<< End Variable Sensitivity Domain Statistics >>\n";
287  }
288 };
289 #endif
290 
291 #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.
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:120
The interface offered by a domain, allows code to manipulate domains without knowing their exact type...
Definition: ai_domain.h:59
ai_history_baset::trace_ptrt trace_ptrt
Definition: ai_domain.h:78
goto_programt::const_targett locationt
Definition: ai_domain.h:77
ai_domain_baset::locationt locationt
Definition: ai_domain.h:175
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
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
std::unique_ptr< statet > make(locationt l) const override
variable_sensitivity_object_factory_ptrt object_factory
variable_sensitivity_domain_factoryt(variable_sensitivity_object_factory_ptrt _object_factory, const vsd_configt &_configuration)
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.
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.
void output(std::ostream &out) const
virtual abstract_object_pointert eval(const exprt &expr, const namespacet &ns) const
virtual bool merge(const variable_sensitivity_domaint &b, locationt from, locationt to)
Computes the join between "this" and "b".
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.
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:496
Captures the user-supplied configuration for VSD, determining which domain abstractions are used,...