1 // Copyright 2017 The Rust Project Developers. See the COPYRIGHT
2 // file at the top-level directory of this distribution and at
3 // http://rust-lang.org/COPYRIGHT.
5 // Licensed under the Apache License, Version 2.0 <LICENSE-APACHE or
6 // http://www.apache.org/licenses/LICENSE-2.0> or the MIT license
7 // <LICENSE-MIT or http://opensource.org/licenses/MIT>, at your
8 // option. This file may not be copied, modified, or distributed
9 // except according to those terms.
11 //! A version of the Naive datalog analysis using Datafrog.
13 use datafrog
::{Iteration, Relation, RelationLeaper}
;
14 use std
::time
::Instant
;
16 use crate::facts
::FactTypes
;
17 use crate::output
::{Context, Output}
;
19 pub(super) fn compute
<T
: FactTypes
>(
21 result
: &mut Output
<T
>,
23 Relation
<(T
::Loan
, T
::Point
)>,
24 Relation
<(T
::Origin
, T
::Origin
, T
::Point
)>,
26 let timer
= Instant
::now();
28 let (errors
, subset_errors
) = {
30 let origin_live_on_entry_rel
= &ctx
.origin_live_on_entry
;
31 let cfg_edge
= &ctx
.cfg_edge
;
32 let loan_killed_at
= &ctx
.loan_killed_at
;
33 let known_placeholder_subset
= &ctx
.known_placeholder_subset
;
34 let placeholder_origin
= &ctx
.placeholder_origin
;
36 // Create a new iteration context, ...
37 let mut iteration
= Iteration
::new();
39 // .. some variables, ..
40 let subset
= iteration
.variable
::<(T
::Origin
, T
::Origin
, T
::Point
)>("subset");
41 let origin_contains_loan_on_entry
=
42 iteration
.variable
::<(T
::Origin
, T
::Loan
, T
::Point
)>("origin_contains_loan_on_entry");
43 let loan_live_at
= iteration
.variable
::<((T
::Loan
, T
::Point
), ())>("loan_live_at");
45 // `loan_invalidated_at` facts, stored ready for joins
46 let loan_invalidated_at
= Relation
::from_iter(
47 ctx
.loan_invalidated_at
49 .map(|&(loan
, point
)| ((loan
, point
), ())),
52 // different indices for `subset`.
53 let subset_o1p
= iteration
.variable_indistinct("subset_o1p");
54 let subset_o2p
= iteration
.variable_indistinct("subset_o2p");
56 // different index for `origin_contains_loan_on_entry`.
57 let origin_contains_loan_on_entry_op
=
58 iteration
.variable_indistinct("origin_contains_loan_on_entry_op");
60 // Unfortunately, we need `origin_live_on_entry` in both variable and relation forms:
62 // - `origin_live_on_entry` as a Relation for the leapjoins in rules 3 & 6
63 // - `origin_live_on_entry` as a Variable for the join in rule 7
65 // The leapjoins use `origin_live_on_entry` as `(Origin, Point)` tuples, while the join uses
66 // it as a `((O, P), ())` tuple to filter the `((Origin, Point), Loan)` tuples from
67 // `origin_contains_loan_on_entry_op`.
69 // The regular join in rule 7 could be turned into a `filter_with` leaper but that would
70 // result in a leapjoin with no `extend_*` leapers: a leapjoin that is not well-formed.
71 // Doing the filtering via an `extend_with` leaper would be extremely inefficient.
73 // Until there's an API in datafrog to handle this use-case better, we do a slightly less
74 // inefficient thing of copying the whole static input into a Variable to use a regular
75 // join, even though the liveness information can be quite heavy (around 1M tuples
77 // This is the Naive variant so this is not a big problem, but needs an
79 let origin_live_on_entry_var
=
80 iteration
.variable
::<((T
::Origin
, T
::Point
), ())>("origin_live_on_entry");
81 origin_live_on_entry_var
.extend(
82 origin_live_on_entry_rel
84 .map(|&(origin
, point
)| ((origin
, point
), ())),
87 // output relations: illegal accesses errors, and illegal subset relations errors
88 let errors
= iteration
.variable("errors");
89 let subset_errors
= iteration
.variable
::<(T
::Origin
, T
::Origin
, T
::Point
)>("subset_errors");
91 // load initial facts:
93 // Rule 1: the initial subsets are the non-transitive `subset_base` static input.
95 // subset(Origin1, Origin2, Point) :-
96 // subset_base(Origin1, Origin2, Point).
97 subset
.extend(ctx
.subset_base
.iter());
99 // Rule 4: the issuing origins are the ones initially containing loans.
101 // origin_contains_loan_on_entry(Origin, Loan, Point) :-
102 // loan_issued_at(Origin, Loan, Point).
103 origin_contains_loan_on_entry
.extend(ctx
.loan_issued_at
.iter());
105 // .. and then start iterating rules!
106 while iteration
.changed() {
107 // Cleanup step: remove symmetries
108 // - remove origins which are `subset`s of themselves
110 // FIXME: investigate whether is there a better way to do that without complicating
111 // the rules too much, because it would also require temporary variables and
112 // impact performance. Until then, the big reduction in tuples improves performance
113 // a lot, even if we're potentially adding a small number of tuples
114 // per round just to remove them in the next round.
119 .retain(|&(origin1
, origin2
, _
)| origin1
!= origin2
);
121 // Remap fields to re-index by keys, to prepare the data needed by the rules below.
122 subset_o1p
.from_map(&subset
, |&(origin1
, origin2
, point
)| {
123 ((origin1
, point
), origin2
)
125 subset_o2p
.from_map(&subset
, |&(origin1
, origin2
, point
)| {
126 ((origin2
, point
), origin1
)
129 origin_contains_loan_on_entry_op
130 .from_map(&origin_contains_loan_on_entry
, |&(origin
, loan
, point
)| {
131 ((origin
, point
), loan
)
134 // Rule 1: done above, as part of the static input facts setup.
136 // Rule 2: compute the subset transitive closure, at a given point.
138 // subset(Origin1, Origin3, Point) :-
139 // subset(Origin1, Origin2, Point),
140 // subset(Origin2, Origin3, Point).
144 |&(_origin2
, point
), &origin1
, &origin3
| (origin1
, origin3
, point
),
147 // Rule 3: propagate subsets along the CFG, according to liveness.
149 // subset(Origin1, Origin2, Point2) :-
150 // subset(Origin1, Origin2, Point1),
151 // cfg_edge(Point1, Point2),
152 // origin_live_on_entry(Origin1, Point2),
153 // origin_live_on_entry(Origin2, Point2).
154 subset
.from_leapjoin(
157 cfg_edge
.extend_with(|&(_origin1
, _origin2
, point1
)| point1
),
158 origin_live_on_entry_rel
.extend_with(|&(origin1
, _origin2
, _point1
)| origin1
),
159 origin_live_on_entry_rel
.extend_with(|&(_origin1
, origin2
, _point1
)| origin2
),
161 |&(origin1
, origin2
, _point1
), &point2
| (origin1
, origin2
, point2
),
164 // Rule 4: done above as part of the static input facts setup.
166 // Rule 5: propagate loans within origins, at a given point, according to subsets.
168 // origin_contains_loan_on_entry(Origin2, Loan, Point) :-
169 // origin_contains_loan_on_entry(Origin1, Loan, Point),
170 // subset(Origin1, Origin2, Point).
171 origin_contains_loan_on_entry
.from_join(
172 &origin_contains_loan_on_entry_op
,
174 |&(_origin1
, point
), &loan
, &origin2
| (origin2
, loan
, point
),
177 // Rule 6: propagate loans along the CFG, according to liveness.
179 // origin_contains_loan_on_entry(Origin, Loan, Point2) :-
180 // origin_contains_loan_on_entry(Origin, Loan, Point1),
181 // !loan_killed_at(Loan, Point1),
182 // cfg_edge(Point1, Point2),
183 // origin_live_on_entry(Origin, Point2).
184 origin_contains_loan_on_entry
.from_leapjoin(
185 &origin_contains_loan_on_entry
,
187 loan_killed_at
.filter_anti(|&(_origin
, loan
, point1
)| (loan
, point1
)),
188 cfg_edge
.extend_with(|&(_origin
, _loan
, point1
)| point1
),
189 origin_live_on_entry_rel
.extend_with(|&(origin
, _loan
, _point1
)| origin
),
191 |&(origin
, loan
, _point1
), &point2
| (origin
, loan
, point2
),
194 // Rule 7: compute whether a loan is live at a given point, i.e. whether it is
195 // contained in a live origin at this point.
197 // loan_live_at(Loan, Point) :-
198 // origin_contains_loan_on_entry(Origin, Loan, Point),
199 // origin_live_on_entry(Origin, Point).
200 loan_live_at
.from_join(
201 &origin_contains_loan_on_entry_op
,
202 &origin_live_on_entry_var
,
203 |&(_origin
, point
), &loan
, _
| ((loan
, point
), ()),
206 // Rule 8: compute illegal access errors, i.e. an invalidation of a live loan.
208 // Here again, this join acts as a pure filter and could be a more efficient leapjoin.
209 // However, similarly to the `origin_live_on_entry` example described above, the
210 // leapjoin with a single `filter_with` leaper would currently not be well-formed.
211 // We don't explictly need to materialize `loan_live_at` either, and that doesn't
212 // change the well-formedness situation, so we still materialize it (since that also
213 // helps in testing).
215 // errors(Loan, Point) :-
216 // loan_invalidated_at(Loan, Point),
217 // loan_live_at(Loan, Point).
220 &loan_invalidated_at
,
221 |&(loan
, point
), _
, _
| (loan
, point
),
224 // Rule 9: compute illegal subset relations errors, i.e. the undeclared subsets
225 // between two placeholder origins.
226 // Here as well, WF-ness prevents this join from being a filter-only leapjoin. It
227 // doesn't matter much, as `placeholder_origin` is single-value relation.
229 // subset_error(Origin1, Origin2, Point) :-
230 // subset(Origin1, Origin2, Point),
231 // placeholder_origin(Origin1),
232 // placeholder_origin(Origin2),
233 // !known_placeholder_subset(Origin1, Origin2).
234 subset_errors
.from_leapjoin(
237 placeholder_origin
.extend_with(|&(origin1
, _origin2
, _point
)| origin1
),
238 placeholder_origin
.extend_with(|&(_origin1
, origin2
, _point
)| origin2
),
239 known_placeholder_subset
240 .filter_anti(|&(origin1
, origin2
, _point
)| (origin1
, origin2
)),
241 // remove symmetries:
242 datafrog
::ValueFilter
::from(|&(origin1
, origin2
, _point
), _
| {
246 |&(origin1
, origin2
, point
), _
| (origin1
, origin2
, point
),
250 // Handle verbose output data
251 if result
.dump_enabled
{
252 let subset
= subset
.complete();
256 .filter(|&(origin1
, origin2
, _
)| origin1
== origin2
)
259 "unwanted subset symmetries"
261 for &(origin1
, origin2
, location
) in subset
.iter() {
271 let origin_contains_loan_on_entry
= origin_contains_loan_on_entry
.complete();
272 for &(origin
, loan
, location
) in origin_contains_loan_on_entry
.iter() {
274 .origin_contains_loan_at
282 let loan_live_at
= loan_live_at
.complete();
283 for &((loan
, location
), _
) in loan_live_at
.iter() {
284 result
.loan_live_at
.entry(location
).or_default().push(loan
);
288 (errors
.complete(), subset_errors
.complete())
292 "analysis done: {} `errors` tuples, {} `subset_errors` tuples, {:?}",
298 (errors
, subset_errors
)