cprover
variable_sensitivity_dependence_graph.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3  Module: analyses variable-sensitivity variable-sensitivity-dependence-graph
4 
5  Author: Diffblue Ltd.
6 
7 \*******************************************************************/
8 
12 #ifndef CPROVER_ANALYSES_VARIABLE_SENSITIVITY_VARIABLE_SENSITIVITY_DEPENDENCE_GRAPH_H
13 #define CPROVER_ANALYSES_VARIABLE_SENSITIVITY_VARIABLE_SENSITIVITY_DEPENDENCE_GRAPH_H
14 
17 
19 #include <util/container_utils.h>
20 #include <util/graph.h>
21 
22 #include <ostream>
23 
25 
27 {
28 public:
29  enum class kindt
30  {
31  NONE,
32  CTRL,
33  DATA,
34  BOTH
35  };
36 
37  void add(kindt _kind)
38  {
39  switch(kind)
40  {
41  case kindt::NONE:
42  kind = _kind;
43  break;
44  case kindt::DATA:
45  case kindt::CTRL:
46  if(kind != _kind)
47  kind = kindt::BOTH;
48  break;
49  case kindt::BOTH:
50  break;
51  }
52  }
53 
54  kindt get() const
55  {
56  return kind;
57  }
58 
59 protected:
61 };
62 
63 struct vs_dep_nodet : public graph_nodet<vs_dep_edget>
64 {
67 
69 };
70 
73 {
74 public:
76 
78  node_indext id,
80  const vsd_configt &configuration)
82  node_id(id),
83  has_values(false),
84  has_changed(false)
85  {
86  }
87 
88  void transform(
89  const irep_idt &function_from,
90  trace_ptrt trace_from,
91  const irep_idt &function_to,
92  trace_ptrt trace_to,
93  ai_baset &ai,
94  const namespacet &ns) override;
95 
96  void make_bottom() override
97  {
99  has_values = tvt(false);
100  has_changed = false;
101  domain_data_deps.clear();
102  control_deps.clear();
103  control_dep_candidates.clear();
104  control_dep_calls.clear();
106  }
107 
108  void make_top() override
109  {
111  has_values = tvt(true);
112  has_changed = false;
113  domain_data_deps.clear();
114  control_deps.clear();
115  control_dep_candidates.clear();
116  control_dep_calls.clear();
118  }
119 
120  void make_entry() override
121  {
122  make_top();
123  }
124 
125  bool is_bottom() const override
126  {
128  }
129 
130  bool is_top() const override
131  {
133  }
134 
135  bool merge(
137  locationt from,
138  locationt to) override;
139 
141  const ai_domain_baset &function_call,
142  const ai_domain_baset &function_start,
143  const ai_domain_baset &function_end,
144  const namespacet &ns) override;
145 
146  void output(std::ostream &out, const ai_baset &ai, const namespacet &ns)
147  const override;
148 
149  jsont output_json(const ai_baset &ai, const namespacet &ns) const override;
150 
151  void populate_dep_graph(
154 
156  {
158  node_id != std::numeric_limits<node_indext>::max(),
159  "Check for the old uninitialised value");
160  return node_id;
161  }
162 
163 private:
167 
169  {
170  public:
173  const goto_programt::const_targett &b) const
174  {
175  return a->location_number < b->location_number;
176  }
177  };
178  typedef std::
179  map<goto_programt::const_targett, std::set<exprt>, dependency_ordert>
182 
183  typedef std::map<goto_programt::const_targett, tvt> control_depst;
185 
186  typedef std::set<goto_programt::const_targett> control_dep_candidatest;
188 
189  typedef std::set<goto_programt::const_targett> control_dep_callst;
192 
193  void eval_data_deps(const exprt &expr, const namespacet &ns, data_depst &deps)
194  const;
195 
197  const irep_idt &from_function,
199  const irep_idt &to_function,
202 
203  void data_dependencies(
207  const namespacet &ns);
208 
210  const control_depst &other_control_deps,
211  const control_dep_candidatest &other_control_dep_candidates,
212  const control_dep_callst &other_control_dep_calls,
213  const control_dep_callst &other_control_dep_call_candidates);
214 };
215 
217 
219  public grapht<vs_dep_nodet>
220 {
221 protected:
222  using ai_baset::get_state;
223 
224  // Legacy-style mutable access to the storage
226  {
227  auto &s = dynamic_cast<location_sensitive_storaget &>(*storage);
228  return s.get_state(l, *domain_factory);
229  }
230 
232  {
233  return dynamic_cast<variable_sensitivity_dependence_domaint &>(
234  get_state(l));
235  }
236 
237 public:
239 
241 
242  typedef std::map<irep_idt, cfg_post_dominatorst> post_dominators_mapt;
243 
246  const namespacet &_ns,
248  const vsd_configt &_configuration);
249 
250  void
251  initialize(const irep_idt &function_id, const goto_programt &goto_program)
252  {
253  ai_recursive_interproceduralt::initialize(function_id, goto_program);
254  }
255 
256  void finalize()
257  {
258  for(const auto &location_state :
259  static_cast<location_sensitive_storaget &>(*storage).internal())
260  {
261  std::static_pointer_cast<variable_sensitivity_dependence_domaint>(
262  location_state.second)
263  ->populate_dep_graph(*this, location_state.first);
264  }
265  }
266 
267  void add_dep(
268  vs_dep_edget::kindt kind,
271 
273  {
274  return post_dominators;
275  }
276 
277 protected:
281  const namespacet &ns;
282 
284 };
285 
286 // NOLINTNEXTLINE(whitespace/line_length)
287 #endif // CPROVER_ANALYSES_VARIABLE_SENSITIVITY_VARIABLE_SENSITIVITY_DEPENDENCE_GRAPH_H
std::shared_ptr< variable_sensitivity_object_factoryt > variable_sensitivity_object_factory_ptrt
Compute dominators for CFG of goto_function.
This is the basic interface of the abstract interpreter with default implementations of the core func...
Definition: ai.h:120
goto_programt::const_targett locationt
Definition: ai.h:127
std::unique_ptr< ai_domain_factory_baset > domain_factory
For creating domain objects.
Definition: ai.h:495
virtual void initialize(const irep_idt &function_id, const goto_programt &goto_program)
Initialize all the abstract states for a single function.
Definition: ai.cpp:190
virtual statet & get_state(trace_ptrt p)
Get the state for the given history, creating it with the factory if it doesn't exist.
Definition: ai.h:516
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
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 collection of goto functions.
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:74
instructionst::const_iterator const_targett
Definition: goto_program.h:551
This class represents a node in a directed graph.
Definition: graph.h:35
A generic directed graph with a parametric node type.
Definition: graph.h:167
Definition: json.h:27
The most conventional storage; one domain per location.
Definition: ai_storage.h:153
statet & get_state(trace_ptrt p, const ai_domain_factory_baset &fac) override
Look up the analysis state for a given history, instantiating a new domain if required.
Definition: ai_storage.h:192
state_mapt & internal(void)
Definition: ai_storage.h:168
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
Definition: threeval.h:20
bool is_false() const
Definition: threeval.h:26
bool is_true() const
Definition: threeval.h:25
This ensures that all domains are constructed with the node ID that links them to the graph part of t...
bool operator()(const goto_programt::const_targett &a, const goto_programt::const_targett &b) const
std::set< goto_programt::const_targett > control_dep_callst
void control_dependencies(const irep_idt &from_function, goto_programt::const_targett from, const irep_idt &to_function, goto_programt::const_targett to, variable_sensitivity_dependence_grapht &dep_graph)
std::map< goto_programt::const_targett, tvt > control_depst
void populate_dep_graph(variable_sensitivity_dependence_grapht &, goto_programt::const_targett) const
void make_entry() override
Make this domain a reasonable entry-point state.
std::map< goto_programt::const_targett, std::set< exprt >, dependency_ordert > data_depst
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.
bool merge(const variable_sensitivity_domaint &b, locationt from, locationt to) override
Computes the join between "this" and "b".
void make_top() override
all states – the analysis doesn't use this, and domains may refuse to implement it.
void eval_data_deps(const exprt &expr, const namespacet &ns, data_depst &deps) const
Evaluate an expression and accumulate all the data dependencies involved in the evaluation.
std::set< goto_programt::const_targett > control_dep_candidatest
bool merge_control_dependencies(const control_depst &other_control_deps, const control_dep_candidatest &other_control_dep_candidates, const control_dep_callst &other_control_dep_calls, const control_dep_callst &other_control_dep_call_candidates)
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) override
Perform a context aware merge of the changes that have been applied between function_start and the cu...
variable_sensitivity_dependence_domaint(node_indext id, variable_sensitivity_object_factory_ptrt object_factory, const vsd_configt &configuration)
void output(std::ostream &out, const ai_baset &ai, const namespacet &ns) const override
Basic text output of the abstract domain.
void data_dependencies(goto_programt::const_targett from, goto_programt::const_targett to, variable_sensitivity_dependence_grapht &dep_graph, const namespacet &ns)
jsont output_json(const ai_baset &ai, const namespacet &ns) const override
Outputs the current value of the domain.
std::map< irep_idt, cfg_post_dominatorst > post_dominators_mapt
void initialize(const irep_idt &function_id, const goto_programt &goto_program)
Initialize all the abstract states for a single function.
variable_sensitivity_dependence_domaint & operator[](locationt l)
void finalize()
Override this to add a cleanup or post-processing step after fixedpoint has run.
void add_dep(vs_dep_edget::kindt kind, goto_programt::const_targett from, goto_programt::const_targett to)
variable_sensitivity_dependence_grapht(const goto_functionst &goto_functions, const namespacet &_ns, variable_sensitivity_object_factory_ptrt object_factory, const vsd_configt &_configuration)
virtual statet & get_state(trace_ptrt p)
Get the state for the given history, creating it with the factory if it doesn't exist.
Definition: ai.h:516
void make_bottom() override
Sets the domain to bottom (no states / unreachable).
void make_top() override
Sets the domain to top (all states).
bool is_bottom() const override
Find out if the domain is currently unreachable.
bool is_top() const override
Is the domain completely top at this state.
A Template Class for Graphs.
exprt object_factory(const typet &type, const irep_idt base_name, code_blockt &init_code, symbol_table_baset &symbol_table, java_object_factory_parameterst parameters, lifetimet lifetime, const source_locationt &loc, const select_pointer_typet &pointer_type_selector, message_handlert &log)
Similar to gen_nondet_init below, but instead of allocating and non-deterministically initializing th...
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:511
graph_nodet< vs_dep_edget >::edgest edgest
graph_nodet< vs_dep_edget >::edget edget
goto_programt::const_targett PC
An abstract interpreter, based on the default recursive-interprocedural that uses variable sensitivit...
There are different ways of handling arrays, structures, unions and pointers.