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.
4 //
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.
10
11 //! A version of the Naive datalog analysis using Datafrog.
12
13 use datafrog::{Iteration, Relation, RelationLeaper};
14 use std::time::Instant;
15
16 use crate::facts::FactTypes;
17 use crate::output::{Context, Output};
18
compute<T: FactTypes>( ctx: &Context<'_, T>, result: &mut Output<T>, ) -> ( Relation<(T::Loan, T::Point)>, Relation<(T::Origin, T::Origin, T::Point)>, )19 pub(super) fn compute<T: FactTypes>(
20 ctx: &Context<'_, T>,
21 result: &mut Output<T>,
22 ) -> (
23 Relation<(T::Loan, T::Point)>,
24 Relation<(T::Origin, T::Origin, T::Point)>,
25 ) {
26 let timer = Instant::now();
27
28 let (errors, subset_errors) = {
29 // Static inputs
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;
35
36 // Create a new iteration context, ...
37 let mut iteration = Iteration::new();
38
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");
44
45 // `loan_invalidated_at` facts, stored ready for joins
46 let loan_invalidated_at = Relation::from_iter(
47 ctx.loan_invalidated_at
48 .iter()
49 .map(|&(loan, point)| ((loan, point), ())),
50 );
51
52 // different indices for `subset`.
53 let subset_o1p = iteration.variable_indistinct("subset_o1p");
54 let subset_o2p = iteration.variable_indistinct("subset_o2p");
55
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");
59
60 // Unfortunately, we need `origin_live_on_entry` in both variable and relation forms:
61 // We need:
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
64 //
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`.
68 //
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.
72 //
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
76 // on `clap`).
77 // This is the Naive variant so this is not a big problem, but needs an
78 // explanation.
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
83 .iter()
84 .map(|&(origin, point)| ((origin, point), ())),
85 );
86
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");
90
91 // load initial facts:
92
93 // Rule 1: the initial subsets are the non-transitive `subset_base` static input.
94 //
95 // subset(Origin1, Origin2, Point) :-
96 // subset_base(Origin1, Origin2, Point).
97 subset.extend(ctx.subset_base.iter());
98
99 // Rule 4: the issuing origins are the ones initially containing loans.
100 //
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());
104
105 // .. and then start iterating rules!
106 while iteration.changed() {
107 // Cleanup step: remove symmetries
108 // - remove origins which are `subset`s of themselves
109 //
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.
115 subset
116 .recent
117 .borrow_mut()
118 .elements
119 .retain(|&(origin1, origin2, _)| origin1 != origin2);
120
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)
124 });
125 subset_o2p.from_map(&subset, |&(origin1, origin2, point)| {
126 ((origin2, point), origin1)
127 });
128
129 origin_contains_loan_on_entry_op
130 .from_map(&origin_contains_loan_on_entry, |&(origin, loan, point)| {
131 ((origin, point), loan)
132 });
133
134 // Rule 1: done above, as part of the static input facts setup.
135
136 // Rule 2: compute the subset transitive closure, at a given point.
137 //
138 // subset(Origin1, Origin3, Point) :-
139 // subset(Origin1, Origin2, Point),
140 // subset(Origin2, Origin3, Point).
141 subset.from_join(
142 &subset_o2p,
143 &subset_o1p,
144 |&(_origin2, point), &origin1, &origin3| (origin1, origin3, point),
145 );
146
147 // Rule 3: propagate subsets along the CFG, according to liveness.
148 //
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(
155 &subset,
156 (
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),
160 ),
161 |&(origin1, origin2, _point1), &point2| (origin1, origin2, point2),
162 );
163
164 // Rule 4: done above as part of the static input facts setup.
165
166 // Rule 5: propagate loans within origins, at a given point, according to subsets.
167 //
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,
173 &subset_o1p,
174 |&(_origin1, point), &loan, &origin2| (origin2, loan, point),
175 );
176
177 // Rule 6: propagate loans along the CFG, according to liveness.
178 //
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,
186 (
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),
190 ),
191 |&(origin, loan, _point1), &point2| (origin, loan, point2),
192 );
193
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.
196 //
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), ()),
204 );
205
206 // Rule 8: compute illegal access errors, i.e. an invalidation of a live loan.
207 //
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).
214 //
215 // errors(Loan, Point) :-
216 // loan_invalidated_at(Loan, Point),
217 // loan_live_at(Loan, Point).
218 errors.from_join(
219 &loan_live_at,
220 &loan_invalidated_at,
221 |&(loan, point), _, _| (loan, point),
222 );
223
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.
228 //
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(
235 &subset,
236 (
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), _| {
243 origin1 != origin2
244 }),
245 ),
246 |&(origin1, origin2, point), _| (origin1, origin2, point),
247 );
248 }
249
250 // Handle verbose output data
251 if result.dump_enabled {
252 let subset = subset.complete();
253 assert!(
254 subset
255 .iter()
256 .filter(|&(origin1, origin2, _)| origin1 == origin2)
257 .count()
258 == 0,
259 "unwanted subset symmetries"
260 );
261 for &(origin1, origin2, location) in subset.iter() {
262 result
263 .subset
264 .entry(location)
265 .or_default()
266 .entry(origin1)
267 .or_default()
268 .insert(origin2);
269 }
270
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() {
273 result
274 .origin_contains_loan_at
275 .entry(location)
276 .or_default()
277 .entry(origin)
278 .or_default()
279 .insert(loan);
280 }
281
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);
285 }
286 }
287
288 (errors.complete(), subset_errors.complete())
289 };
290
291 info!(
292 "analysis done: {} `errors` tuples, {} `subset_errors` tuples, {:?}",
293 errors.len(),
294 subset_errors.len(),
295 timer.elapsed()
296 );
297
298 (errors, subset_errors)
299 }
300