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
variable_sensitivity_dependence_domaint::node_id
node_indext node_id
Definition: variable_sensitivity_dependence_graph.h:164
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
variable_sensitivity_dependence_domaint::make_bottom
void make_bottom() override
no states
Definition: variable_sensitivity_dependence_graph.h:96
variable_sensitivity_dependence_domaint::control_deps
control_depst control_deps
Definition: variable_sensitivity_dependence_graph.h:184
variable_sensitivity_dependence_domaint::merge
bool merge(const variable_sensitivity_domaint &b, locationt from, locationt to) override
Computes the join between "this" and "b".
Definition: variable_sensitivity_dependence_graph.cpp:400
variable_sensitivity_dependence_grapht::add_dep
void add_dep(vs_dep_edget::kindt kind, goto_programt::const_targett from, goto_programt::const_targett to)
Definition: variable_sensitivity_dependence_graph.cpp:657
variable_sensitivity_dependence_domaint::data_dependencies
void data_dependencies(goto_programt::const_targett from, goto_programt::const_targett to, variable_sensitivity_dependence_grapht &dep_graph, const namespacet &ns)
Definition: variable_sensitivity_dependence_graph.cpp:133
ai_baset::locationt
goto_programt::const_targett locationt
Definition: ai.h:127
vs_dep_nodet
Definition: variable_sensitivity_dependence_graph.h:64
ai_three_way_merget
Definition: three_way_merge_abstract_interpreter.h:28
variable_sensitivity_dependence_domaint::output
void output(std::ostream &out, const ai_baset &ai, const namespacet &ns) const override
Basic text output of the abstract domain.
Definition: variable_sensitivity_dependence_graph.cpp:471
variable_sensitivity_dependence_domaint::dependency_ordert::operator()
bool operator()(const goto_programt::const_targett &a, const goto_programt::const_targett &b) const
Definition: variable_sensitivity_dependence_graph.h:171
variable_sensitivity_domaint::is_bottom
bool is_bottom() const override
Find out if the domain is currently unreachable.
Definition: variable_sensitivity_domain.cpp:242
grapht
A generic directed graph with a parametric node type.
Definition: graph.h:167
location_sensitive_storaget::internal
state_mapt & internal(void)
Definition: ai_storage.h:168
variable_sensitivity_dependence_domaint::control_dep_callst
std::set< goto_programt::const_targett > control_dep_callst
Definition: variable_sensitivity_dependence_graph.h:189
vs_dep_edget::kindt::BOTH
@ BOTH
variable_sensitivity_dependence_domaint::data_depst
std::map< goto_programt::const_targett, std::set< exprt >, dependency_ordert > data_depst
Definition: variable_sensitivity_dependence_graph.h:180
variable_sensitivity_dependence_grapht::variable_sensitivity_dependence_domain_factoryt
friend variable_sensitivity_dependence_domain_factoryt
Definition: variable_sensitivity_dependence_graph.h:278
variable_sensitivity_dependence_domaint::domain_data_deps
data_depst domain_data_deps
Definition: variable_sensitivity_dependence_graph.h:181
exprt
Base class for all expressions.
Definition: expr.h:54
three_way_merge_abstract_interpreter.h
An abstract interpreter, based on the default recursive-interprocedural that uses variable sensitivit...
vs_dep_edget::kindt::DATA
@ DATA
jsont
Definition: json.h:27
vsd_configt
Definition: variable_sensitivity_configuration.h:41
variable_sensitivity_dependence_domaint::is_top
bool is_top() const override
Definition: variable_sensitivity_dependence_graph.h:130
location_sensitive_storaget::get_state
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
ai_domain_baset::trace_ptrt
ai_history_baset::trace_ptrt trace_ptrt
Definition: ai_domain.h:78
variable_sensitivity_dependence_grapht::goto_functions
const goto_functionst & goto_functions
Definition: variable_sensitivity_dependence_graph.h:280
vs_dep_nodet::edget
graph_nodet< vs_dep_edget >::edget edget
Definition: variable_sensitivity_dependence_graph.h:65
cfg_dominators.h
Compute dominators for CFG of goto_function.
variable_sensitivity_dependence_grapht::finalize
void finalize()
Override this to add a cleanup or post-processing step after fixedpoint has run.
Definition: variable_sensitivity_dependence_graph.h:256
variable_sensitivity_dependence_domaint::make_entry
void make_entry() override
Make this domain a reasonable entry-point state.
Definition: variable_sensitivity_dependence_graph.h:120
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
variable_sensitivity_domaint::make_bottom
void make_bottom() override
Sets the domain to bottom (no states / unreachable).
Definition: variable_sensitivity_domain.cpp:182
vs_dep_edget::kindt
kindt
Definition: variable_sensitivity_dependence_graph.h:30
vs_dep_edget::get
kindt get() const
Definition: variable_sensitivity_dependence_graph.h:54
ai_baset::get_state
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
variable_sensitivity_dependence_domaint::is_bottom
bool is_bottom() const override
Definition: variable_sensitivity_dependence_graph.h:125
vs_dep_edget::add
void add(kindt _kind)
Definition: variable_sensitivity_dependence_graph.h:37
DATA_INVARIANT
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:511
variable_sensitivity_dependence_grapht::variable_sensitivity_dependence_domaint
friend variable_sensitivity_dependence_domaint
Definition: variable_sensitivity_dependence_graph.h:279
vs_dep_nodet::PC
goto_programt::const_targett PC
Definition: variable_sensitivity_dependence_graph.h:68
variable_sensitivity_dependence_domaint::make_top
void make_top() override
all states – the analysis doesn't use this, and domains may refuse to implement it.
Definition: variable_sensitivity_dependence_graph.h:108
variable_sensitivity_object_factory_ptrt
std::shared_ptr< variable_sensitivity_object_factoryt > variable_sensitivity_object_factory_ptrt
Definition: abstract_environment.h:33
ai_baset::domain_factory
std::unique_ptr< ai_domain_factory_baset > domain_factory
For creating domain objects.
Definition: ai.h:495
vs_dep_edget::kindt::CTRL
@ CTRL
variable_sensitivity_dependence_domaint::control_dep_candidatest
std::set< goto_programt::const_targett > control_dep_candidatest
Definition: variable_sensitivity_dependence_graph.h:186
variable_sensitivity_dependence_grapht::variable_sensitivity_dependence_grapht
variable_sensitivity_dependence_grapht(const goto_functionst &goto_functions, const namespacet &_ns, variable_sensitivity_object_factory_ptrt object_factory, const vsd_configt &_configuration)
Definition: variable_sensitivity_dependence_graph.cpp:640
object_factory
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...
Definition: java_object_factory.cpp:1537
variable_sensitivity_dependence_domaint::control_dependencies
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)
Definition: variable_sensitivity_dependence_graph.cpp:205
variable_sensitivity_dependence_domaint::eval_data_deps
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.
Definition: variable_sensitivity_dependence_graph.cpp:25
variable_sensitivity_dependence_domaint::has_changed
bool has_changed
Definition: variable_sensitivity_dependence_graph.h:166
variable_sensitivity_dependence_grapht::initialize
void initialize(const irep_idt &function_id, const goto_programt &goto_program)
Initialize all the abstract states for a single function.
Definition: variable_sensitivity_dependence_graph.h:251
variable_sensitivity_dependence_grapht::post_dominators
post_dominators_mapt post_dominators
Definition: variable_sensitivity_dependence_graph.h:283
variable_sensitivity_domaint::is_top
bool is_top() const override
Is the domain completely top at this state.
Definition: variable_sensitivity_domain.cpp:247
variable_sensitivity_dependence_grapht
Definition: variable_sensitivity_dependence_graph.h:220
tvt::is_false
bool is_false() const
Definition: threeval.h:26
location_sensitive_storaget
The most conventional storage; one domain per location.
Definition: ai_storage.h:153
variable_sensitivity_dependence_grapht::cfg_post_dominators
post_dominators_mapt & cfg_post_dominators()
Definition: variable_sensitivity_dependence_graph.h:272
tvt
Definition: threeval.h:20
variable_sensitivity_dependence_domaint::control_depst
std::map< goto_programt::const_targett, tvt > control_depst
Definition: variable_sensitivity_dependence_graph.h:183
variable_sensitivity_dependence_domaint::node_indext
grapht< vs_dep_nodet >::node_indext node_indext
Definition: variable_sensitivity_dependence_graph.h:75
variable_sensitivity_dependence_domaint::merge_control_dependencies
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)
Definition: variable_sensitivity_dependence_graph.cpp:315
variable_sensitivity_dependence_domaint::populate_dep_graph
void populate_dep_graph(variable_sensitivity_dependence_grapht &, goto_programt::const_targett) const
Definition: variable_sensitivity_dependence_graph.cpp:594
ai_baset::initialize
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
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:23
ai_domain_baset::locationt
goto_programt::const_targett locationt
Definition: ai_domain.h:77
variable_sensitivity_dependence_domaint::output_json
jsont output_json(const ai_baset &ai, const namespacet &ns) const override
Outputs the current value of the domain.
Definition: variable_sensitivity_dependence_graph.cpp:541
graph.h
A Template Class for Graphs.
variable_sensitivity_dependence_domaint::variable_sensitivity_dependence_domaint
variable_sensitivity_dependence_domaint(node_indext id, variable_sensitivity_object_factory_ptrt object_factory, const vsd_configt &configuration)
Definition: variable_sensitivity_dependence_graph.h:77
vs_dep_edget
Definition: variable_sensitivity_dependence_graph.h:27
variable_sensitivity_dependence_grapht::get_state
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
graph_nodet
This class represents a node in a directed graph.
Definition: graph.h:35
container_utils.h
variable_sensitivity_domain.h
There are different ways of handling arrays, structures, unions and pointers.
variable_sensitivity_dependence_domaint::has_values
tvt has_values
Definition: variable_sensitivity_dependence_graph.h:165
variable_sensitivity_dependence_domain_factoryt
This ensures that all domains are constructed with the node ID that links them to the graph part of t...
Definition: variable_sensitivity_dependence_graph.cpp:613
variable_sensitivity_dependence_domaint::get_node_id
node_indext get_node_id() const
Definition: variable_sensitivity_dependence_graph.h:155
ai_baset
This is the basic interface of the abstract interpreter with default implementations of the core func...
Definition: ai.h:120
variable_sensitivity_domaint
Definition: variable_sensitivity_domain.h:76
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:74
variable_sensitivity_dependence_domaint
Definition: variable_sensitivity_dependence_graph.h:73
goto_programt::const_targett
instructionst::const_iterator const_targett
Definition: goto_program.h:551
variable_sensitivity_dependence_domaint::dependency_ordert
Definition: variable_sensitivity_dependence_graph.h:169
ai_domain_baset
The interface offered by a domain, allows code to manipulate domains without knowing their exact type...
Definition: ai_domain.h:59
vs_dep_nodet::edgest
graph_nodet< vs_dep_edget >::edgest edgest
Definition: variable_sensitivity_dependence_graph.h:66
vs_dep_edget::kind
kindt kind
Definition: variable_sensitivity_dependence_graph.h:60
variable_sensitivity_domaint::make_top
void make_top() override
Sets the domain to top (all states).
Definition: variable_sensitivity_domain.cpp:188
variable_sensitivity_dependence_domaint::merge_three_way_function_return
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...
Definition: variable_sensitivity_dependence_graph.cpp:449
vs_dep_edget::kindt::NONE
@ NONE
variable_sensitivity_dependence_domaint::transform
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.
Definition: variable_sensitivity_dependence_graph.cpp:66
variable_sensitivity_dependence_domaint::control_dep_calls
control_dep_callst control_dep_calls
Definition: variable_sensitivity_dependence_graph.h:190
variable_sensitivity_dependence_grapht::post_dominators_mapt
std::map< irep_idt, cfg_post_dominatorst > post_dominators_mapt
Definition: variable_sensitivity_dependence_graph.h:242
variable_sensitivity_dependence_grapht::get_state
virtual statet & get_state(locationt l)
Definition: variable_sensitivity_dependence_graph.h:225
tvt::is_true
bool is_true() const
Definition: threeval.h:25
variable_sensitivity_dependence_grapht::ns
const namespacet & ns
Definition: variable_sensitivity_dependence_graph.h:281
variable_sensitivity_dependence_domaint::control_dep_candidates
control_dep_candidatest control_dep_candidates
Definition: variable_sensitivity_dependence_graph.h:187
variable_sensitivity_dependence_domaint::control_dep_call_candidates
control_dep_callst control_dep_call_candidates
Definition: variable_sensitivity_dependence_graph.h:191
variable_sensitivity_dependence_grapht::operator[]
variable_sensitivity_dependence_domaint & operator[](locationt l)
Definition: variable_sensitivity_dependence_graph.h:231