CBMC: /home/runner/work/cbmc/cbmc/src/analyses/variable-sensitivity/variable_sensitivity_dependence_graph.cpp Source File

CBMC
Loading...
Searching...
No Matches
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
9#include "variable_sensitivity_dependence_graph.h"
10#include "data_dependency_context.h"
11
12#include <langapi/language_util.h>
13
14#include <util/container_utils.h>
15#include <util/json.h>
16#include <util/json_irep.h>
17#include <util/std_code.h>
18
28 const exprt &expr,
29 const namespacet &ns,
30 data_depst &deps) const
31{
32 const auto res =
33 std::dynamic_pointer_cast<const data_dependency_contextt>(eval(expr, ns));
34
35 if(res->get_data_dependencies().size() > 0)
36 {
37 // If the expression was able to be eval'ed to something with data
38 // dependencies, then that's all we need to gather.
39 for(const auto &dep : res->get_data_dependencies())
40 deps[dep].insert(expr);
41 }
42 else
43 {
44 // If the expression could not be eval'ed to something with data
45 // dependencies, then it may have been some sort of compound expression,
46 // so attempt to eval the data dependencies for all the operands, taking
47 // the union of them all.
48 for(const exprt &op : expr.operands())
49 {
50 eval_data_deps(op, ns, deps);
51 }
52 }
53}
54
71 const irep_idt &function_to,
73 ai_baset &ai,
74 const namespacet &ns)
75{
76 locationt from{trace_from->current_location()};
77 locationt to{trace_to->current_location()};
78
81
85 dep_graph != nullptr, "Domains should all be of the same type");
86
87 // propagate control dependencies across function calls
88 if(from->is_function_call())
89 {
91 {
93 }
94 else
95 {
96 // edge to function entry point
97 const goto_programt::const_targett next = std::next(from);
98
101 &(dep_graph->get_state(next)));
102 DATA_INVARIANT(s != nullptr, "Domains should all be of the same type");
103
104 if(s->has_values.is_false())
105 {
107 s->has_changed = true;
108 }
109
110 // modify abstract state of return location
116 s->has_changed = true;
117
120
122 control_dep_calls.insert(from);
123
125 control_dep_call_candidates.insert(from);
126 }
127 }
128 else
130
131 // Find all the data dependencies in the the 'to' expression
132 data_dependencies(from, to, *dep_graph, ns);
133}
134
139 const namespacet &ns)
140{
141 // Find all the data dependencies in the the 'to' expression
143 if(to->is_assign())
144 {
145 const exprt &rhs = to->assign_rhs();
146
147 // Handle return value of a 'no body' function
148 if(rhs.id() == ID_side_effect)
149 {
151 if(see.get_statement() == ID_nondet)
152 {
153 if(from->is_function_call())
154 {
155 const exprt &call = from->call_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::argumentst &args = to->call_arguments();
193 for(const auto &arg : args)
194 {
196 }
197 }
198 else if(to->is_goto())
199 {
200 eval_data_deps(to->condition(), ns, domain_data_deps);
201 }
202}
203
205 const irep_idt &from_function,
207 const irep_idt &to_function,
210{
211 // Better Slicing of Programs with Jumps and Switches
212 // Kumar and Horwitz, FASE'02:
213 // "Node N is control dependent on node M iff N postdominates, in
214 // the CFG, one but not all of M's CFG successors."
215 //
216 // The "successor" above refers to an immediate successor of M.
217
218 // Candidates for M for "to" are "from" and all existing control
219 // dependencies on nodes. "from" is added if it is a goto or assume
220 // instruction
221
222 // Add new candidates
223
224 if(from->is_goto() || from->is_assume())
225 control_dep_candidates.insert(from);
226 else if(from->is_end_function())
227 {
232 return;
233 }
234
235 // Compute postdominators if needed
236
237 const goto_functionst &goto_functions = dep_graph.goto_functions;
238
239 const irep_idt id = from_function;
240 cfg_post_dominatorst &pd_tmp = dep_graph.cfg_post_dominators()[id];
241
242 goto_functionst::function_mapt::const_iterator f_it =
243 goto_functions.function_map.find(id);
244
245 if(f_it == goto_functions.function_map.end())
246 return;
247
248 const goto_programt &goto_program = f_it->second.body;
249
250 if(pd_tmp.cfg.size() == 0) // have we computed the dominators already?
251 {
252 pd_tmp(goto_program);
253 }
254
256
257 // Check all candidates
258
259 for(const auto &cd : control_dep_candidates)
260 {
261 // check all CFG successors of M
262 // special case: assumptions also introduce a control dependency
263 bool post_dom_all = !cd->is_assume();
264 bool post_dom_one = false;
265
266 // we could hard-code assume and goto handling here to improve
267 // performance
268 const cfg_post_dominatorst::cfgt::nodet &m = pd.get_node(cd);
269
270 // successors of M
271 for(const auto &edge : m.out)
272 {
273 const cfg_post_dominatorst::cfgt::nodet &m_s = pd.cfg[edge.first];
274
275 if(m_s.dominators.find(to) != m_s.dominators.end())
276 post_dom_one = true;
277 else
278 post_dom_all = false;
279 }
280
282 {
283 control_deps.erase(cd);
284 }
285 else
286 {
288
289 if(cd->is_goto() && !cd->is_backwards_goto())
290 {
291 goto_programt::const_targett t = cd->get_target();
292 branch =
293 to->location_number >= t->location_number ? tvt(false) : tvt(true);
294 }
295
296 control_deps.insert(std::make_pair(cd, branch));
297 }
298 }
299
300 if(control_deps.empty())
301 {
303 }
304 else
305 {
306 control_dep_calls.clear();
307 }
308
309 // add edges to the graph
310 for(const auto &c_dep : control_deps)
311 dep_graph.add_dep(vs_dep_edget::kindt::CTRL, c_dep.first, to);
312}
313
319{
320 bool changed = false;
321
322 // Merge control dependencies
323
324 control_depst::iterator it = control_deps.begin();
325
326 for(const auto &c_dep : other_control_deps)
327 {
328 // find position to insert
329 while(it != control_deps.end() &&
330 goto_programt::target_less_than()(it->first, c_dep.first))
331 ++it;
332
333 if(
334 it == control_deps.end() ||
335 goto_programt::target_less_than()(c_dep.first, it->first))
336 {
337 // hint points at position that will follow the new element
338 control_deps.insert(it, c_dep);
339 changed = true;
340 }
341 else
342 {
343 INVARIANT(
344 it != control_deps.end(), "Property of branch needed for safety");
345 INVARIANT(
346 !(goto_programt::target_less_than()(it->first, c_dep.first)),
347 "Property of loop needed for safety");
348 INVARIANT(
349 !(goto_programt::target_less_than()(c_dep.first, it->first)),
350 "Property of loop needed for safety");
351
352 tvt &branch1 = it->second;
353 const tvt &branch2 = c_dep.second;
354
355 if(branch1 != branch2 && !branch1.is_unknown())
356 {
358 changed = true;
359 }
360
361 ++it;
362 }
363 }
364
365 // Merge control dependency candidates
366
367 size_t n = control_dep_candidates.size();
368
371
372 changed |= n != control_dep_candidates.size();
373
374 // Merge call control dependencies
375
376 n = control_dep_calls.size();
377
378 control_dep_calls.insert(
380
381 changed |= n != control_dep_calls.size();
382
383 // Merge call control dependency candidates
384
386
390
391 changed |= n != control_dep_call_candidates.size();
392
393 return changed;
394}
395
406 trace_ptrt from,
407 trace_ptrt to)
408{
409 bool changed = false;
410
411 changed = variable_sensitivity_domaint::merge(b, from, to);
412 changed |= has_values.is_false() || has_changed;
413
414 // Handle data dependencies
415 const auto &cast_b =
416 dynamic_cast<const variable_sensitivity_dependence_domaint &>(b);
417
418 // Merge data dependencies
419 for(auto bdep : cast_b.domain_data_deps)
420 {
421 for(exprt bexpr : bdep.second)
422 {
423 auto result = domain_data_deps[bdep.first].insert(bexpr);
424 changed |= result.second;
425 }
426 }
427
429 cast_b.control_deps,
430 cast_b.control_dep_candidates,
431 cast_b.control_dep_calls,
432 cast_b.control_dep_call_candidates);
433
434 has_changed = false;
436
437 return changed;
438}
439
446 const namespacet &ns)
447{
448 // The gathering of the data dependencies for the domain is handled by the
449 // 'transform' and simply relies on the underlying domains with their
450 // data_dependency_context to be correct. Therefore all we need to ensure at
451 // the three way merge is that the underlying variable sensitivity domain
452 // does its three way merge.
455}
456
465 std::ostream &out,
466 const ai_baset &ai,
467 const namespacet &ns) const
468{
469 if(!control_deps.empty() || !control_dep_calls.empty())
470 {
471 out << "Control dependencies: ";
472 for(control_depst::const_iterator it = control_deps.begin();
473 it != control_deps.end();
474 ++it)
475 {
476 if(it != control_deps.begin())
477 out << ",";
478
479 const goto_programt::const_targett cd = it->first;
480 const tvt branch = it->second;
481
482 out << cd->location_number << " [" << branch << "]";
483 }
484
485 for(control_dep_callst::const_iterator it = control_dep_calls.begin();
486 it != control_dep_calls.end();
487 ++it)
488 {
489 if(!control_deps.empty() || it != control_dep_calls.begin())
490 out << ",";
491
492 out << (*it)->location_number << " [UNCONDITIONAL]";
493 }
494
495 out << "\n";
496 }
497
498 if(!domain_data_deps.empty())
499 {
500 out << "Data dependencies: ";
501 bool first = true;
502 for(auto &dep : domain_data_deps)
503 {
504 if(!first)
505 out << ", ";
506
507 out << dep.first->location_number;
508 out << " [";
509 bool first_expr = true;
510 for(auto &expr : dep.second)
511 {
512 if(!first_expr)
513 out << ", ";
514
515 out << from_expr(ns, "", expr);
516 first_expr = false;
517 }
518 out << "]";
519
520 first = false;
521 }
522 out << std::endl;
523 }
524}
525
535 const ai_baset &ai,
536 const namespacet &ns) const
537{
538 json_arrayt graph;
539
540 for(const auto &cd : control_deps)
541 {
542 const goto_programt::const_targett target = cd.first;
543 const tvt branch = cd.second;
544
545 json_objectt &link = graph.push_back().make_object();
546
547 link["locationNumber"] =
548 json_numbert(std::to_string(target->location_number));
549 link["sourceLocation"] = json(target->source_location());
550 link["type"] = json_stringt("control");
551 link["branch"] = json_stringt(branch.to_string());
552 }
553
554 for(const auto &target : control_dep_calls)
555 {
556 json_objectt &link = graph.push_back().make_object();
557 link["locationNumber"] =
558 json_numbert(std::to_string(target->location_number));
559 link["sourceLocation"] = json(target->source_location());
560 link["type"] = json_stringt("control");
561 link["branch"] = json_stringt("UNCONDITIONAL");
562 }
563
564 for(const auto &dep : domain_data_deps)
565 {
566 json_objectt &link = graph.push_back().make_object();
567 link["locationNumber"] =
568 json_numbert(std::to_string(dep.first->location_number));
569 link["sourceLocation"] = json(dep.first->source_location());
570 json_stringt(dep.first->source_location().as_string());
571 link["type"] = json_stringt("data");
572
573 const std::set<exprt> &expr_set = dep.second;
574 json_arrayt &expressions = link["expressions"].make_array();
575
576 for(const exprt &e : expr_set)
577 {
578 json_objectt &object = expressions.push_back().make_object();
579 object["expression"] = json_stringt(from_expr(ns, "", e));
580 object["certainty"] = json_stringt("maybe");
581 }
582 }
583
584 return std::move(graph);
585}
586
600
605 : public ai_domain_factoryt<variable_sensitivity_dependence_domaint>
606{
607public:
615
616 std::unique_ptr<statet> make(locationt l) const override
617{
618 auto node_id = dg.add_node();
619 dg.nodes[node_id].PC = l;
620 auto p = std::make_unique<variable_sensitivity_dependence_domaint>(
621 node_id, object_factory, configuration);
622 CHECK_RETURN(p->is_bottom());
623
624 return std::unique_ptr<statet>(p.release());
625 }
626
627private:
631};
632
651
656{
657 const node_indext n_from = (*this)[from].get_node_id();
658 DATA_INVARIANT(n_from < size(), "Node ids must be within the graph");
659 const node_indext n_to = (*this)[to].get_node_id();
660 DATA_INVARIANT(n_to < size(), "Node ids must be within the graph");
661
662 // add_edge is redundant as the subsequent operations also insert
663 // entries into the edge maps (implicitly)
664
665 // add_edge(n_from, n_to);
666
667 nodes[n_from].out[n_to].add(kind);
668 nodes[n_to].in[n_from].add(kind);
669}
std::shared_ptr< variable_sensitivity_object_factoryt > variable_sensitivity_object_factory_ptrt
void branch(goto_modelt &goto_model, const irep_idt &id)
Definition branch.cpp:21
The common case of history is to only care about where you are now, not how you got there!...
Definition ai_history.h:155
This is the basic interface of the abstract interpreter with default implementations of the core func...
Definition ai.h:117
virtual void clear()
Reset the abstract state.
Definition ai.h:269
The interface offered by a domain, allows code to manipulate domains without knowing their exact type...
Definition ai_domain.h:54
ai_history_baset::trace_ptrt trace_ptrt
Definition ai_domain.h:73
goto_programt::const_targett locationt
Definition ai_domain.h:72
Definition ai_domain.h:200
ai_domain_factory_baset::locationt locationt
Definition ai_domain.h:203
An easy factory implementation for histories that don't need parameters.
Definition ai_history.h:255
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:566
virtual statet & get_state(locationt l)
Definition ai.h:615
exprt::operandst argumentst
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:38
Base class for all expressions.
Definition expr.h:57
operandst & operands()
Definition expr.h:95
A collection of goto functions.
function_mapt function_map
A generic container class for the GOTO intermediate representation of one function.
Definition goto_program.h:72
instructionst::const_iterator const_targett
Definition goto_program.h:614
instructiont::target_less_than target_less_than
Definition goto_program.h:618
nodest nodes
Definition graph.h:176
nodet::node_indext node_indext
Definition graph.h:173
node_indext add_node(arguments &&... values)
Definition graph.h:180
std::size_t size() const
Definition graph.h:212
const irep_idt & id() const
Definition irep.h:388
Definition json.h:165
jsont & push_back(const jsont &json)
Definition json.h:212
Definition json.h:289
Definition json.h:298
Definition json.h:270
Definition json.h:27
json_arrayt & make_array()
Definition json.h:418
json_objectt & make_object()
Definition json.h:436
The most conventional storage; one domain per location.
Definition ai_storage.h:154
Definition message.h:27
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
An expression containing a side effect.
Definition std_code.h:1450
Definition threeval.h:20
bool is_false() const
Definition threeval.h:26
static tvt unknown()
Definition threeval.h:33
This ensures that all domains are constructed with the node ID that links them to the graph part of t...
variable_sensitivity_object_factory_ptrt object_factory
const vsd_configt configuration
variable_sensitivity_dependence_grapht & dg
std::unique_ptr< statet > make(locationt l) const override
variable_sensitivity_dependence_domain_factoryt(variable_sensitivity_dependence_grapht &_dg, variable_sensitivity_object_factory_ptrt _object_factory, const vsd_configt &_configuration)
control_dep_candidatest control_dep_candidates
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)
control_depst control_deps
void populate_dep_graph(variable_sensitivity_dependence_grapht &, goto_programt::const_targett) const
control_dep_callst control_dep_calls
std::map< goto_programt::const_targett, tvt, goto_programt::target_less_than > control_depst
std::map< goto_programt::const_targett, std::set< exprt >, dependency_ordert > data_depst
std::set< goto_programt::const_targett, goto_programt::target_less_than > control_dep_candidatest
std::set< goto_programt::const_targett, goto_programt::target_less_than > control_dep_callst
control_dep_callst control_dep_call_candidates
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.
tvt has_values
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.
void merge_three_way_function_return(const ai_domain_baset &function_start, const ai_domain_baset &function_end, const namespacet &ns) override
Merges just the things that have changes between "function_start" and "function_end" into "this".
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)
bool merge(const variable_sensitivity_domaint &b, trace_ptrt from, trace_ptrt to) override
Computes the join between "this" and "b".
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)
data_depst domain_data_deps
bool has_changed
jsont output_json(const ai_baset &ai, const namespacet &ns) const override
Outputs the current value of the domain.
variable_sensitivity_dependence_grapht(const goto_functionst &goto_functions, const namespacet &_ns, variable_sensitivity_object_factory_ptrt object_factory, const vsd_configt &_configuration, message_handlert &message_handler)
void add_dep(vs_dep_edget::kindt kind, goto_programt::const_targett from, goto_programt::const_targett to)
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 void merge_three_way_function_return(const ai_domain_baset &function_start, const ai_domain_baset &function_end, const namespacet &ns)
Merges just the things that have changes between "function_start" and "function_end" into "this".
virtual abstract_object_pointert eval(const exprt &expr, const namespacet &ns) const
virtual bool merge(const variable_sensitivity_domaint &b, trace_ptrt from, trace_ptrt to)
Computes the join between "this" and "b".
kindt
@ CTRL
@ DATA
bool util_inplace_set_union(std::set< T, Compare, Alloc > &target, const std::set< T, Compare, Alloc > &source)
Compute union of two sets.
Maintain data dependencies as a context in the variable sensitivity domain.
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...
Util.
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
STL namespace.
static void json(json_objectT &result, const irep_idt &property_id, const property_infot &property_info)
Definition properties.cpp:120
#define CHECK_RETURN(CONDITION)
Definition invariant.h:495
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition invariant.h:534
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition invariant.h:423
side_effect_exprt & to_side_effect_expr(exprt &expr)
Definition std_code.h:1506
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition std_expr.h:221
A total order over targett and const_targett.
Definition goto_program.h:391
A forked and modified version of analyses/dependence_graph.

AltStyle によって変換されたページ (->オリジナル) /