CBMC: /home/runner/work/cbmc/cbmc/src/analyses/dependence_graph.cpp Source File

CBMC
Loading...
Searching...
No Matches
dependence_graph.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Field-Sensitive Program Dependence Analysis, Litvak et al.,
4 FSE 2010
5
6Author: Michael Tautschnig
7
8Date: August 2013
9
10\*******************************************************************/
11
14
15#include "dependence_graph.h"
16
17#include <util/container_utils.h>
18#include <util/json_irep.h>
19
20#include "goto_rw.h"
21
23 const dep_graph_domaint &src,
26{
27 // An abstract state at location `to` may be non-bottom even if
28 // `merge(..., `to`) has not been called so far. This is due to the special
29 // handling of function entry edges (see transform()).
30 bool changed = is_bottom() || has_changed;
31
32 // For computing the data dependencies, we would not need a fixpoint
33 // computation. The data dependencies at a location are computed from the
34 // result of the reaching definitions analysis at that location
35 // (in data_dependencies()). Thus, we only need to set the data dependencies
36 // part of an abstract state at a certain location once.
37 if(changed && data_deps.empty())
38 {
39 data_deps = src.data_deps;
41 }
42
44 changed |=
46
47 has_changed = false;
48
49 return changed;
50}
51
53 const irep_idt &function_id,
57{
58 // Better Slicing of Programs with Jumps and Switches
59 // Kumar and Horwitz, FASE'02:
60 // "Node N is control dependent on node M iff N postdominates, in
61 // the CFG, one but not all of M's CFG successors."
62 //
63 // The "successor" above refers to an immediate successor of M.
64 //
65 // When computing the control dependencies of a node N (i.e., "to"
66 // being N), candidates for M are all control statements (gotos or
67 // assumes) from which there is a path in the CFG to N.
68
69 // Add new candidates
70
71 if(from->is_goto() || from->is_assume())
72 control_dep_candidates.insert(from);
73 else if(from->is_end_function())
74 {
76 return;
77 }
78
79 if(control_dep_candidates.empty())
80 return;
81
82 // Get postdominators
83
84 const irep_idt id = function_id;
85 const cfg_post_dominatorst &pd=dep_graph.cfg_post_dominators().at(id);
86
87 // Check all candidates
88
90 {
91 // check all CFG successors of M
92 // special case: assumptions also introduce a control dependency
93 bool post_dom_all = !control_dep_candidate->is_assume();
94 bool post_dom_one=false;
95
96 // we could hard-code assume and goto handling here to improve
97 // performance
98 const cfg_post_dominatorst::cfgt::nodet &m =
99 pd.get_node(control_dep_candidate);
100
101 // successors of M
102 for(const auto &edge : m.out)
103 {
104 // Could use pd.dominates(to, control_dep_candidate) but this would impose
105 // another dominator node lookup per call to this function, which is too
106 // expensive.
107 const cfg_post_dominatorst::cfgt::nodet &m_s=
108 pd.cfg[edge.first];
109
110 if(m_s.dominators.find(to)!=m_s.dominators.end())
111 post_dom_one=true;
112 else
113 post_dom_all=false;
114 }
115
117 {
119 }
120 else
121 {
123 }
124 }
125}
126
128 const range_spect &w_start,
129 const range_spect &w_end,
130 const range_spect &r_start,
131 const range_spect &r_end)
132{
135
136 if(
137 (!w_end.is_unknown() && w_end <= r_start) || // we < rs
138 (!r_end.is_unknown() && w_start >= r_end)) // re < we
139 {
140 return false;
141 }
142 else if(w_start >= r_start) // rs <= ws < we,re
143 return true;
144 else if(
145 w_end.is_unknown() ||
146 (!r_end.is_unknown() && w_end > r_start)) // ws <= rs < we,re
147 {
148 return true;
149 }
150 else
151 return false;
152}
153
156 const irep_idt &function_to,
159 const namespacet &ns)
160{
161 // data dependencies using def-use pairs
163
164 // TODO use (future) reaching-definitions-dereferencing rw_set
165 value_setst &value_sets=
166 dep_graph.reaching_definitions().get_value_sets();
169
170 for(const auto &read_object_entry : rw_set.get_r_set())
171 {
172 const range_domaint &r_ranges = rw_set.get_ranges(read_object_entry.second);
174 dep_graph.reaching_definitions()[to].get(read_object_entry.first);
175
176 for(const auto &w_range : w_ranges)
177 {
178 bool found=false;
179 for(const auto &wr : w_range.second)
180 {
181 for(const auto &r_range : r_ranges)
182 {
183 if(!found &&
184 may_be_def_use_pair(wr.first, wr.second,
185 r_range.first, r_range.second))
186 {
187 // found a def-use pair
188 data_deps.insert(w_range.first);
189 found=true;
190 }
191 }
192 }
193 }
194
195 dep_graph.reaching_definitions()[to].clear_cache(read_object_entry.first);
196 }
197
198 if(to->is_set_return_value())
199 {
200 auto entry = dep_graph.end_function_map.find(function_to);
201 CHECK_RETURN(entry != dep_graph.end_function_map.end());
202
204
207 CHECK_RETURN(s != nullptr);
208
209 if(s->is_bottom())
211
212 if(s->data_deps.insert(to).second)
213 s->has_changed = true;
214 }
215}
216
218 const irep_idt &function_from,
220 const irep_idt &function_to,
222 ai_baset &ai,
223 const namespacet &ns)
224{
225 locationt from{trace_from->current_location()};
226 locationt to{trace_to->current_location()};
227
229 CHECK_RETURN(dep_graph != nullptr);
230
231 // We do not propagate control dependencies on function calls, i.e., only the
232 // entry point of a function should have a control dependency on the call
234 std::copy_if(
235 control_deps.begin(),
236 control_deps.end(),
237 std::inserter(filtered_control_deps, filtered_control_deps.end()),
238 [](goto_programt::const_targett dep) { return !dep->is_function_call(); });
240
241 // propagate control dependencies across function calls
242 if(from->is_function_call() && function_from != function_to)
243 {
244 // edge to function entry point
245 const goto_programt::const_targett next = std::next(from);
246
248 dynamic_cast<dep_graph_domaint *>(&(dep_graph->get_state(next)));
249 CHECK_RETURN(s != nullptr);
250
251 if(s->is_bottom())
252 {
254 s->has_changed = true;
255 }
256
258 s->has_changed |=
260
261 control_deps.clear();
262 control_deps.insert(from);
263
265 }
266 else
268
269 data_dependencies(from, function_to, to, *dep_graph, ns);
270}
271
273 std::ostream &out,
274 const ai_baset &,
275 const namespacet &) const
276{
277 if(!control_deps.empty())
278 {
279 out << "Control dependencies: ";
280 for(depst::const_iterator
281 it=control_deps.begin();
282 it!=control_deps.end();
283 ++it)
284 {
285 if(it!=control_deps.begin())
286 out << ",";
287 out << (*it)->location_number;
288 }
289 out << '\n';
290 }
291
292 if(!data_deps.empty())
293 {
294 out << "Data dependencies: ";
295 for(depst::const_iterator
296 it=data_deps.begin();
297 it!=data_deps.end();
298 ++it)
299 {
300 if(it!=data_deps.begin())
301 out << ",";
302 out << (*it)->location_number;
303 }
304 out << '\n';
305 }
306}
307
312 const ai_baset &,
313 const namespacet &) const
314{
315 json_arrayt graph;
316
317 for(const auto &cd : control_deps)
318 {
319 json_objectt link{
320 {"locationNumber", json_numbert(std::to_string(cd->location_number))},
321 {"sourceLocation", json(cd->source_location())},
322 {"type", json_stringt("control")}};
323 graph.push_back(std::move(link));
324 }
325
326 for(const auto &dd : data_deps)
327 {
328 json_objectt link{
329 {"locationNumber", json_numbert(std::to_string(dd->location_number))},
330 {"sourceLocation", json(dd->source_location())},
331 {"type", json_stringt("data")}};
332 graph.push_back(std::move(link));
333 }
334
335 return std::move(graph);
336}
337
341 class dep_graph_domain_factoryt : public ai_domain_factoryt<dep_graph_domaint>
342{
343public:
350
351 std::unique_ptr<statet> make(locationt l) const override
352{
353 auto node_id = dg.add_node();
354 dg.nodes[node_id].PC = l;
355 auto p = std::make_unique<dep_graph_domaint>(node_id, message_handler);
356 CHECK_RETURN(p->is_bottom());
357
358 return std::unique_ptr<statet>(p.release());
359 }
360
361private:
364};
365
367 const namespacet &_ns,
368 message_handlert &message_handler)
370 std::make_unique<dep_graph_domain_factoryt>(*this, message_handler)),
371 ns(_ns),
372 rd(ns, message_handler)
373{
374}
375
377 dep_edget::kindt kind,
380{
381 const node_indext n_from = (*this)[from].get_node_id();
383 const node_indext n_to = (*this)[to].get_node_id();
385
386 // add_edge is redundant as the subsequent operations also insert
387 // entries into the edge maps (implicitly)
388 // add_edge(n_from, n_to);
389 nodes[n_from].out[n_to].add(kind);
390 nodes[n_to].in[n_from].add(kind);
391}
392
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
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
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
kindt
@ CTRL
@ DATA
This ensures that all domains are constructed with the node ID that links them to the graph part of t...
dependence_grapht & dg
std::unique_ptr< statet > make(locationt l) const override
dep_graph_domain_factoryt(dependence_grapht &_dg, message_handlert &message_handler)
message_handlert & message_handler
tvt has_values
void control_dependencies(const irep_idt &function_id, goto_programt::const_targett from, goto_programt::const_targett to, dependence_grapht &dep_graph)
std::set< goto_programt::const_targett, goto_programt::target_less_than > depst
depst data_deps
bool merge(const dep_graph_domaint &src, trace_ptrt from, trace_ptrt to)
bool is_bottom() const final override
bool has_changed
depst control_deps
void populate_dep_graph(dependence_grapht &, goto_programt::const_targett) const
jsont output_json(const ai_baset &ai, const namespacet &ns) const override
Outputs the current value of the 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) final override
how function calls are treated: a) there is an edge from each call site to the function head b) there...
depst control_dep_candidates
void data_dependencies(goto_programt::const_targett from, const irep_idt &function_to, goto_programt::const_targett to, dependence_grapht &dep_graph, const namespacet &ns)
void output(std::ostream &out, const ai_baset &ai, const namespacet &ns) const final override
message_handlert & message_handler
void add_dep(dep_edget::kindt kind, goto_programt::const_targett from, goto_programt::const_targett to)
dependence_grapht(const namespacet &_ns, message_handlert &)
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:38
instructionst::const_iterator const_targett
Definition goto_program.h:614
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
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
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
Definition goto_rw.h:177
Data type to describe upper and lower bounds of the range of bits that a read or write access may aff...
Definition goto_rw.h:63
std::map< locationt, rangest, goto_programt::target_less_than > ranges_at_loct
Definition goto_rw.h:367
static tvt unknown()
Definition threeval.h:33
Definition value_sets.h:22
bool util_inplace_set_union(std::set< T, Compare, Alloc > &target, const std::set< T, Compare, Alloc > &source)
Compute union of two sets.
static bool may_be_def_use_pair(const range_spect &w_start, const range_spect &w_end, const range_spect &r_start, const range_spect &r_end)
Field-Sensitive Program Dependence Analysis, Litvak et al., FSE 2010.
static void goto_rw(const irep_idt &function, goto_programt::const_targett target, const exprt &lhs, const exprt &function_expr, const exprt::operandst &arguments, rw_range_sett &rw_set)
Definition goto_rw.cpp:845
Util.
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 PRECONDITION(CONDITION)
Definition invariant.h:463

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