cprover
variable_sensitivity_dependence_graph.cpp
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 
11 
13 #include <langapi/language_util.h>
14 #include <util/json.h>
15 #include <util/json_irep.h>
16 
26  const exprt &expr,
27  const namespacet &ns,
28  data_depst &deps) const
29 {
30  const auto res =
31  std::dynamic_pointer_cast<const data_dependency_contextt>(eval(expr, ns));
32 
33  if(res->get_data_dependencies().size() > 0)
34  {
35  // If the expression was able to be eval'ed to something with data
36  // dependencies, then that's all we need to gather.
37  for(const auto &dep : res->get_data_dependencies())
38  deps[dep].insert(expr);
39  }
40  else
41  {
42  // If the expression could not be eval'ed to something with data
43  // dependencies, then it may have been some sort of compound expression,
44  // so attempt to eval the data dependencies for all the operands, taking
45  // the union of them all.
46  for(const exprt &op : expr.operands())
47  {
48  eval_data_deps(op, ns, deps);
49  }
50  }
51 }
52 
67  const irep_idt &function_from,
68  trace_ptrt trace_from,
69  const irep_idt &function_to,
70  trace_ptrt trace_to,
71  ai_baset &ai,
72  const namespacet &ns)
73 {
74  locationt from{trace_from->current_location()};
75  locationt to{trace_to->current_location()};
76 
78  function_from, trace_from, function_to, trace_to, ai, ns);
79 
81  dynamic_cast<variable_sensitivity_dependence_grapht *>(&ai);
83  dep_graph != nullptr, "Domains should all be of the same type");
84 
85  // propagate control dependencies across function calls
86  if(from->is_function_call())
87  {
88  if(function_from == function_to)
89  {
90  control_dependencies(function_from, from, function_to, to, *dep_graph);
91  }
92  else
93  {
94  // edge to function entry point
95  const goto_programt::const_targett next = std::next(from);
96 
99  &(dep_graph->get_state(next)));
100  DATA_INVARIANT(s != nullptr, "Domains should all be of the same type");
101 
102  if(s->has_values.is_false())
103  {
104  s->has_values = tvt::unknown();
105  s->has_changed = true;
106  }
107 
108  // modify abstract state of return location
110  control_deps,
114  s->has_changed = true;
115 
116  control_deps.clear();
117  control_dep_candidates.clear();
118 
119  control_dep_calls.clear();
120  control_dep_calls.insert(from);
121 
123  control_dep_call_candidates.insert(from);
124  }
125  }
126  else
127  control_dependencies(function_from, from, function_to, to, *dep_graph);
128 
129  // Find all the data dependencies in the the 'to' expression
130  data_dependencies(from, to, *dep_graph, ns);
131 }
132 
137  const namespacet &ns)
138 {
139  // Find all the data dependencies in the the 'to' expression
140  domain_data_deps.clear();
141  if(to->is_assign())
142  {
143  const code_assignt &inst = to_code_assign(to->code);
144  const exprt &rhs = inst.rhs();
145 
146  // Handle return value of a 'no body' function
147  if(rhs.id() == ID_side_effect)
148  {
149  const side_effect_exprt &see = to_side_effect_expr(rhs);
150  if(see.get_statement() == ID_nondet)
151  {
152  if(from->is_function_call())
153  {
154  const code_function_callt &cfc = to_code_function_call(from->code);
155  const exprt &call = cfc.function();
156 
157  if(call.id() == ID_symbol)
158  {
159  const irep_idt id = to_symbol_expr(call).id();
160  const goto_functionst &goto_functions = dep_graph.goto_functions;
161 
162  goto_functionst::function_mapt::const_iterator it =
163  goto_functions.function_map.find(id);
164 
165  if(it != goto_functions.function_map.end())
166  {
167  if(!it->second.body_available()) // body not available
168  {
169  domain_data_deps[from].insert(call);
170  }
171  }
172  else // function not in map
173  {
174  domain_data_deps[from].insert(call);
175  }
176  }
177  else // complex call expression
178  {
179  domain_data_deps[from].insert(call);
180  }
181  }
182  }
183  }
184  else
185  {
186  // Just an ordinary assignement
188  }
189  }
190  else if(to->is_function_call())
191  {
192  const code_function_callt &call = to_code_function_call(to->code);
193  const code_function_callt::argumentst &args = call.arguments();
194  for(const auto &arg : args)
195  {
197  }
198  }
199  else if(to->is_goto())
200  {
201  eval_data_deps(to->guard, ns, domain_data_deps);
202  }
203 }
204 
206  const irep_idt &from_function,
208  const irep_idt &to_function,
211 {
212  // Better Slicing of Programs with Jumps and Switches
213  // Kumar and Horwitz, FASE'02:
214  // "Node N is control dependent on node M iff N postdominates, in
215  // the CFG, one but not all of M's CFG successors."
216  //
217  // The "successor" above refers to an immediate successor of M.
218 
219  // Candidates for M for "to" are "from" and all existing control
220  // dependencies on nodes. "from" is added if it is a goto or assume
221  // instruction
222 
223  // Add new candidates
224 
225  if(from->is_goto() || from->is_assume())
226  control_dep_candidates.insert(from);
227  else if(from->is_end_function())
228  {
229  control_deps.clear();
230  control_dep_candidates.clear();
231  control_dep_calls.clear();
233  return;
234  }
235 
236  // Compute postdominators if needed
237 
238  const goto_functionst &goto_functions = dep_graph.goto_functions;
239 
240  const irep_idt id = from_function;
241  cfg_post_dominatorst &pd_tmp = dep_graph.cfg_post_dominators()[id];
242 
243  goto_functionst::function_mapt::const_iterator f_it =
244  goto_functions.function_map.find(id);
245 
246  if(f_it == goto_functions.function_map.end())
247  return;
248 
249  const goto_programt &goto_program = f_it->second.body;
250 
251  if(pd_tmp.cfg.size() == 0) // have we computed the dominators already?
252  {
253  pd_tmp(goto_program);
254  }
255 
256  const cfg_post_dominatorst &pd = pd_tmp;
257 
258  // Check all candidates
259 
260  for(const auto &cd : control_dep_candidates)
261  {
262  // check all CFG successors of M
263  // special case: assumptions also introduce a control dependency
264  bool post_dom_all = !cd->is_assume();
265  bool post_dom_one = false;
266 
267  // we could hard-code assume and goto handling here to improve
268  // performance
270 
271  // successors of M
272  for(const auto &edge : m.out)
273  {
274  const cfg_post_dominatorst::cfgt::nodet &m_s = pd.cfg[edge.first];
275 
276  if(m_s.dominators.find(to) != m_s.dominators.end())
277  post_dom_one = true;
278  else
279  post_dom_all = false;
280  }
281 
282  if(post_dom_all || !post_dom_one)
283  {
284  control_deps.erase(cd);
285  }
286  else
287  {
288  tvt branch = tvt::unknown();
289 
290  if(cd->is_goto() && !cd->is_backwards_goto())
291  {
292  goto_programt::const_targett t = cd->get_target();
293  branch =
294  to->location_number >= t->location_number ? tvt(false) : tvt(true);
295  }
296 
297  control_deps.insert(std::make_pair(cd, branch));
298  }
299  }
300 
301  if(control_deps.empty())
302  {
304  }
305  else
306  {
307  control_dep_calls.clear();
308  }
309 
310  // add edges to the graph
311  for(const auto &c_dep : control_deps)
312  dep_graph.add_dep(vs_dep_edget::kindt::CTRL, c_dep.first, to);
313 }
314 
316  const control_depst &other_control_deps,
317  const control_dep_candidatest &other_control_dep_candidates,
318  const control_dep_callst &other_control_dep_calls,
319  const control_dep_callst &other_control_dep_call_candidates)
320 {
321  bool changed = false;
322 
323  // Merge control dependencies
324 
325  control_depst::iterator it = control_deps.begin();
326 
327  for(const auto &c_dep : other_control_deps)
328  {
329  // find position to insert
330  while(it != control_deps.end() && it->first < c_dep.first)
331  ++it;
332 
333  if(it == control_deps.end() || c_dep.first < it->first)
334  {
335  // hint points at position that will follow the new element
336  control_deps.insert(it, c_dep);
337  changed = true;
338  }
339  else
340  {
341  INVARIANT(
342  it != control_deps.end(), "Property of branch needed for safety");
343  INVARIANT(
344  !(it->first < c_dep.first), "Property of loop needed for safety");
345  INVARIANT(
346  !(c_dep.first < it->first), "Property of loop needed for safety");
347 
348  tvt &branch1 = it->second;
349  const tvt &branch2 = c_dep.second;
350 
351  if(branch1 != branch2 && !branch1.is_unknown())
352  {
353  branch1 = tvt::unknown();
354  changed = true;
355  }
356 
357  ++it;
358  }
359  }
360 
361  // Merge control dependency candidates
362 
363  size_t n = control_dep_candidates.size();
364 
365  control_dep_candidates.insert(
366  other_control_dep_candidates.begin(), other_control_dep_candidates.end());
367 
368  changed |= n != control_dep_candidates.size();
369 
370  // Merge call control dependencies
371 
372  n = control_dep_calls.size();
373 
374  control_dep_calls.insert(
375  other_control_dep_calls.begin(), other_control_dep_calls.end());
376 
377  changed |= n != control_dep_calls.size();
378 
379  // Merge call control dependency candidates
380 
381  n = control_dep_call_candidates.size();
382 
384  other_control_dep_call_candidates.begin(),
385  other_control_dep_call_candidates.end());
386 
387  changed |= n != control_dep_call_candidates.size();
388 
389  return changed;
390 }
391 
402  locationt from,
403  locationt to)
404 {
405  bool changed = false;
406 
407  changed = variable_sensitivity_domaint::merge(b, from, to);
408  changed |= has_values.is_false() || has_changed;
409 
410  // Handle data dependencies
411  const auto &cast_b =
412  dynamic_cast<const variable_sensitivity_dependence_domaint &>(b);
413 
414  // Merge data dependencies
415  for(auto bdep : cast_b.domain_data_deps)
416  {
417  for(exprt bexpr : bdep.second)
418  {
419  auto result = domain_data_deps[bdep.first].insert(bexpr);
420  changed |= result.second;
421  }
422  }
423 
424  changed |= merge_control_dependencies(
425  cast_b.control_deps,
426  cast_b.control_dep_candidates,
427  cast_b.control_dep_calls,
428  cast_b.control_dep_call_candidates);
429 
430  has_changed = false;
432 
433  return changed;
434 }
435 
447 
450  const ai_domain_baset &function_call,
451  const ai_domain_baset &function_start,
452  const ai_domain_baset &function_end,
453  const namespacet &ns)
454 {
455  // The gathering of the data dependencies for the domain is handled by the
456  // 'transform' and simply relies on the underlying domains with their
457  // data_dependency_context to be correct. Therefore all we need to ensure at
458  // the three way merge is that the underlying variable sensitivity domain
459  // does its three way merge.
461  function_call, function_start, function_end, ns);
462 }
463 
472  std::ostream &out,
473  const ai_baset &ai,
474  const namespacet &ns) const
475 {
476  if(!control_deps.empty() || !control_dep_calls.empty())
477  {
478  out << "Control dependencies: ";
479  for(control_depst::const_iterator it = control_deps.begin();
480  it != control_deps.end();
481  ++it)
482  {
483  if(it != control_deps.begin())
484  out << ",";
485 
486  const goto_programt::const_targett cd = it->first;
487  const tvt branch = it->second;
488 
489  out << cd->location_number << " [" << branch << "]";
490  }
491 
492  for(control_dep_callst::const_iterator it = control_dep_calls.begin();
493  it != control_dep_calls.end();
494  ++it)
495  {
496  if(!control_deps.empty() || it != control_dep_calls.begin())
497  out << ",";
498 
499  out << (*it)->location_number << " [UNCONDITIONAL]";
500  }
501 
502  out << "\n";
503  }
504 
505  if(!domain_data_deps.empty())
506  {
507  out << "Data dependencies: ";
508  bool first = true;
509  for(auto &dep : domain_data_deps)
510  {
511  if(!first)
512  out << ", ";
513 
514  out << dep.first->location_number;
515  out << " [";
516  bool first_expr = true;
517  for(auto &expr : dep.second)
518  {
519  if(!first_expr)
520  out << ", ";
521 
522  out << from_expr(ns, "", expr);
523  first_expr = false;
524  }
525  out << "]";
526 
527  first = false;
528  }
529  out << std::endl;
530  }
531 }
532 
542  const ai_baset &ai,
543  const namespacet &ns) const
544 {
545  json_arrayt graph;
546 
547  for(const auto &cd : control_deps)
548  {
549  const goto_programt::const_targett target = cd.first;
550  const tvt branch = cd.second;
551 
552  json_objectt &link = graph.push_back().make_object();
553 
554  link["locationNumber"] =
555  json_numbert(std::to_string(target->location_number));
556  link["sourceLocation"] = json(target->source_location);
557  link["type"] = json_stringt("control");
558  link["branch"] = json_stringt(branch.to_string());
559  }
560 
561  for(const auto &target : control_dep_calls)
562  {
563  json_objectt &link = graph.push_back().make_object();
564  link["locationNumber"] =
565  json_numbert(std::to_string(target->location_number));
566  link["sourceLocation"] = json(target->source_location);
567  link["type"] = json_stringt("control");
568  link["branch"] = json_stringt("UNCONDITIONAL");
569  }
570 
571  for(const auto &dep : domain_data_deps)
572  {
573  json_objectt &link = graph.push_back().make_object();
574  link["locationNumber"] =
575  json_numbert(std::to_string(dep.first->location_number));
576  link["sourceLocation"] = json(dep.first->source_location);
577  json_stringt(dep.first->source_location.as_string());
578  link["type"] = json_stringt("data");
579 
580  const std::set<exprt> &expr_set = dep.second;
581  json_arrayt &expressions = link["expressions"].make_array();
582 
583  for(const exprt &e : expr_set)
584  {
585  json_objectt &object = expressions.push_back().make_object();
586  object["expression"] = json_stringt(from_expr(ns, "", e));
587  object["certainty"] = json_stringt("maybe");
588  }
589  }
590 
591  return std::move(graph);
592 }
593 
596  goto_programt::const_targett this_loc) const
597 {
598  for(const auto &c_dep : control_deps)
599  dep_graph.add_dep(vs_dep_edget::kindt::CTRL, c_dep.first, this_loc);
600 
601  for(const auto &c_dep : control_dep_calls)
602  dep_graph.add_dep(vs_dep_edget::kindt::CTRL, c_dep, this_loc);
603 
604  for(const auto &d_dep : domain_data_deps)
605  dep_graph.add_dep(vs_dep_edget::kindt::DATA, d_dep.first, this_loc);
606 }
607 
612  : public ai_domain_factoryt<variable_sensitivity_dependence_domaint>
613 {
614 public:
618  const vsd_configt &_configuration)
619  : dg(_dg), object_factory(_object_factory), configuration(_configuration)
620  {
621  }
622 
623  std::unique_ptr<statet> make(locationt l) const override
624  {
625  auto node_id = dg.add_node();
626  dg.nodes[node_id].PC = l;
627  auto p = util_make_unique<variable_sensitivity_dependence_domaint>(
628  node_id, object_factory, configuration);
629  CHECK_RETURN(p->is_bottom());
630 
631  return std::unique_ptr<statet>(p.release());
632  }
633 
634 private:
638 };
639 
641  const goto_functionst &goto_functions,
642  const namespacet &_ns,
644  const vsd_configt &configuration)
648  *this,
650  configuration),
652  goto_functions(goto_functions),
653  ns(_ns)
654 {
655 }
656 
658  vs_dep_edget::kindt kind,
661 {
662  const node_indext n_from = (*this)[from].get_node_id();
663  DATA_INVARIANT(n_from < size(), "Node ids must be within the graph");
664  const node_indext n_to = (*this)[to].get_node_id();
665  DATA_INVARIANT(n_to < size(), "Node ids must be within the graph");
666 
667  // add_edge is redundant as the subsequent operations also insert
668  // entries into the edge maps (implicitly)
669 
670  // add_edge(n_from, n_to);
671 
672  nodes[n_from].out[n_to].add(kind);
673  nodes[n_to].in[n_from].add(kind);
674 }
variable_sensitivity_dependence_domain_factoryt::object_factory
variable_sensitivity_object_factory_ptrt object_factory
Definition: variable_sensitivity_dependence_graph.cpp:636
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
json_numbert
Definition: json.h:291
variable_sensitivity_dependence_domaint::control_deps
control_depst control_deps
Definition: variable_sensitivity_dependence_graph.h:184
grapht::size
std::size_t size() const
Definition: graph.h:212
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
CHECK_RETURN
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:496
ahistoricalt
The common case of history is to only care about where you are now, not how you got there!...
Definition: ai_history.h:155
code_assignt::rhs
exprt & rhs()
Definition: std_code.h:317
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_domaint::merge
virtual bool merge(const variable_sensitivity_domaint &b, locationt from, locationt to)
Computes the join between "this" and "b".
Definition: variable_sensitivity_domain.cpp:198
variable_sensitivity_dependence_domaint::control_dep_callst
std::set< goto_programt::const_targett > control_dep_callst
Definition: variable_sensitivity_dependence_graph.h:189
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_domaint::eval
virtual abstract_object_pointert eval(const exprt &expr, const namespacet &ns) const
Definition: variable_sensitivity_domain.h:168
grapht::add_node
node_indext add_node(arguments &&... values)
Definition: graph.h:180
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
variable_sensitivity_dependence_domain_factoryt::configuration
const vsd_configt configuration
Definition: variable_sensitivity_dependence_graph.cpp:637
variable_sensitivity_dependence_domain_factoryt::make
std::unique_ptr< statet > make(locationt l) const override
Definition: variable_sensitivity_dependence_graph.cpp:623
variable_sensitivity_dependence_domain_factoryt::dg
variable_sensitivity_dependence_grapht & dg
Definition: variable_sensitivity_dependence_graph.cpp:635
variable_sensitivity_dependence_domain_factoryt::variable_sensitivity_dependence_domain_factoryt
variable_sensitivity_dependence_domain_factoryt(variable_sensitivity_dependence_grapht &_dg, variable_sensitivity_object_factory_ptrt _object_factory, const vsd_configt &_configuration)
Definition: variable_sensitivity_dependence_graph.cpp:615
tvt::is_unknown
bool is_unknown() const
Definition: threeval.h:27
to_string
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
Definition: string_constraint.cpp:55
to_side_effect_expr
side_effect_exprt & to_side_effect_expr(exprt &expr)
Definition: std_code.h:1954
vs_dep_edget::kindt::DATA
@ DATA
goto_functionst::function_map
function_mapt function_map
Definition: goto_functions.h:27
jsont::make_object
json_objectt & make_object()
Definition: json.h:438
jsont
Definition: json.h:27
variable_sensitivity_dependence_graph.h
A forked and modified version of analyses/dependence_graph.
vsd_configt
Definition: variable_sensitivity_configuration.h:41
json_irep.h
Util.
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
json_arrayt
Definition: json.h:165
grapht< vs_dep_nodet >::node_indext
nodet::node_indext node_indext
Definition: graph.h:173
json_objectt
Definition: json.h:300
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
vs_dep_edget::kindt
kindt
Definition: variable_sensitivity_dependence_graph.h:30
util_make_unique
std::unique_ptr< T > util_make_unique(Ts &&... ts)
Definition: make_unique.h:19
code_function_callt
codet representation of a function call statement.
Definition: std_code.h:1215
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
ai_history_factory_default_constructort
An easy factory implementation for histories that don't need parameters.
Definition: ai_history.h:255
branch
void branch(goto_modelt &goto_model, const irep_idt &id)
Definition: branch.cpp:20
language_util.h
util_inplace_set_union
bool util_inplace_set_union(std::set< T, Compare, Alloc > &target, const std::set< T, Compare, Alloc > &source)
Compute union of two sets.
Definition: container_utils.h:28
variable_sensitivity_object_factory_ptrt
std::shared_ptr< variable_sensitivity_object_factoryt > variable_sensitivity_object_factory_ptrt
Definition: abstract_environment.h:33
json
static void json(json_objectT &result, const irep_idt &property_id, const property_infot &property_info)
Definition: properties.cpp:114
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_domaint::merge_three_way_function_return
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...
Definition: variable_sensitivity_domain.cpp:397
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
cfg_dominators_templatet::nodet::dominators
target_sett dominators
Definition: cfg_dominators.h:43
json_expr.h
Expressions in JSON.
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
cfg_dominators_templatet::get_node
const cfgt::nodet & get_node(const T &program_point) const
Get the graph node (which gives dominators, predecessors and successors) for program_point.
Definition: cfg_dominators.h:53
variable_sensitivity_dependence_domaint::has_changed
bool has_changed
Definition: variable_sensitivity_dependence_graph.h:166
variable_sensitivity_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_domain.cpp:24
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:190
irept::id
const irep_idt & id() const
Definition: irep.h:407
grapht::nodes
nodest nodes
Definition: graph.h:176
tvt::unknown
static tvt unknown()
Definition: threeval.h:33
to_code_function_call
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:1326
code_function_callt::argumentst
exprt::operandst argumentst
Definition: std_code.h:1224
jsont::make_array
json_arrayt & make_array()
Definition: json.h:420
variable_sensitivity_dependence_grapht
Definition: variable_sensitivity_dependence_graph.h:220
data_dependency_context.h
Maintain data dependencies as a context in the variable sensitivity domain.
tvt::is_false
bool is_false() const
Definition: threeval.h:26
code_function_callt::arguments
argumentst & arguments()
Definition: std_code.h:1260
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
side_effect_exprt::get_statement
const irep_idt & get_statement() const
Definition: std_code.h:1920
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
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
ai_domain_factoryt
Definition: ai_domain.h:201
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
to_code_assign
const code_assignt & to_code_assign(const codet &code)
Definition: std_code.h:383
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
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
json.h
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
ai_domain_factory_baset::locationt
ai_domain_baset::locationt locationt
Definition: ai_domain.h:175
goto_programt::const_targett
instructionst::const_iterator const_targett
Definition: goto_program.h:551
exprt::operands
operandst & operands()
Definition: expr.h:96
cfg_dominators_templatet::nodet
Definition: cfg_dominators.h:42
INVARIANT
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:424
code_assignt
A codet representing an assignment in the program.
Definition: std_code.h:295
ai_domain_baset
The interface offered by a domain, allows code to manipulate domains without knowing their exact type...
Definition: ai_domain.h:59
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
cfg_dominators_templatet::cfg
cfgt cfg
Definition: cfg_dominators.h:47
from_expr
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
Definition: language_util.cpp:20
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
json_arrayt::push_back
jsont & push_back(const jsont &json)
Definition: json.h:212
variable_sensitivity_dependence_domaint::control_dep_calls
control_dep_callst control_dep_calls
Definition: variable_sensitivity_dependence_graph.h:190
code_function_callt::function
exprt & function()
Definition: std_code.h:1250
side_effect_exprt
An expression containing a side effect.
Definition: std_code.h:1898
variable_sensitivity_dependence_grapht::get_state
virtual statet & get_state(locationt l)
Definition: variable_sensitivity_dependence_graph.h:225
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
cfg_dominators_templatet
Dominator graph.
Definition: cfg_dominators.h:37
json_stringt
Definition: json.h:270