| 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 | use datafrog::{Iteration, Relation, RelationLeaper}; |
| 12 | use std::time::Instant; |
| 13 | |
| 14 | use crate::facts::FactTypes; |
| 15 | use crate::output::{Context, Output}; |
| 16 | |
| 17 | pub(super) fn compute<T: FactTypes>( |
| 18 | ctx: &Context<'_, T>, |
| 19 | result: &mut Output<T>, |
| 20 | ) -> ( |
| 21 | Relation<(T::Loan, T::Point)>, |
| 22 | Relation<(T::Origin, T::Origin)>, |
| 23 | ) { |
| 24 | let timer = Instant::now(); |
| 25 | |
| 26 | let (potential_errors, potential_subset_errors) = { |
| 27 | // Static inputs |
| 28 | let origin_live_on_entry = &ctx.origin_live_on_entry; |
| 29 | let loan_invalidated_at = &ctx.loan_invalidated_at; |
| 30 | let placeholder_origin = &ctx.placeholder_origin; |
| 31 | let placeholder_loan = &ctx.placeholder_loan; |
| 32 | let known_contains = &ctx.known_contains; |
| 33 | |
| 34 | // subset(Origin1, Origin2) :- |
| 35 | // subset_base(Origin1, Origin2, _). |
| 36 | let subset = Relation::from_iter( |
| 37 | ctx.subset_base |
| 38 | .iter() |
| 39 | .map(|&(origin1, origin2, _point)| (origin1, origin2)), |
| 40 | ); |
| 41 | |
| 42 | // Create a new iteration context, ... |
| 43 | let mut iteration = Iteration::new(); |
| 44 | |
| 45 | // .. some variables, .. |
| 46 | let origin_contains_loan_on_entry = |
| 47 | iteration.variable::<(T::Origin, T::Loan)>("origin_contains_loan_on_entry" ); |
| 48 | |
| 49 | let potential_errors = iteration.variable::<(T::Loan, T::Point)>("potential_errors" ); |
| 50 | let potential_subset_errors = |
| 51 | iteration.variable::<(T::Origin, T::Origin)>("potential_subset_errors" ); |
| 52 | |
| 53 | // load initial facts. |
| 54 | |
| 55 | // origin_contains_loan_on_entry(Origin, Loan) :- |
| 56 | // loan_issued_at(Origin, Loan, _). |
| 57 | origin_contains_loan_on_entry.extend( |
| 58 | ctx.loan_issued_at |
| 59 | .iter() |
| 60 | .map(|&(origin, loan, _point)| (origin, loan)), |
| 61 | ); |
| 62 | |
| 63 | // origin_contains_loan_on_entry(Origin, Loan) :- |
| 64 | // placeholder_loan(Origin, Loan). |
| 65 | origin_contains_loan_on_entry.extend( |
| 66 | placeholder_loan |
| 67 | .iter() |
| 68 | .map(|&(loan, origin)| (origin, loan)), |
| 69 | ); |
| 70 | |
| 71 | // .. and then start iterating rules! |
| 72 | while iteration.changed() { |
| 73 | // origin_contains_loan_on_entry(Origin2, Loan) :- |
| 74 | // origin_contains_loan_on_entry(Origin1, Loan), |
| 75 | // subset(Origin1, Origin2). |
| 76 | // |
| 77 | // Note: Since `subset` is effectively a static input, this join can be ported to |
| 78 | // a leapjoin. Doing so, however, was 7% slower on `clap`. |
| 79 | origin_contains_loan_on_entry.from_join( |
| 80 | &origin_contains_loan_on_entry, |
| 81 | &subset, |
| 82 | |&_origin1, &loan, &origin2| (origin2, loan), |
| 83 | ); |
| 84 | |
| 85 | // loan_live_at(Loan, Point) :- |
| 86 | // origin_contains_loan_on_entry(Origin, Loan), |
| 87 | // origin_live_on_entry(Origin, Point) |
| 88 | // |
| 89 | // potential_errors(Loan, Point) :- |
| 90 | // loan_invalidated_at(Loan, Point), |
| 91 | // loan_live_at(Loan, Point). |
| 92 | // |
| 93 | // Note: we don't need to materialize `loan_live_at` here |
| 94 | // so we can inline it in the `potential_errors` relation. |
| 95 | // |
| 96 | potential_errors.from_leapjoin( |
| 97 | &origin_contains_loan_on_entry, |
| 98 | ( |
| 99 | origin_live_on_entry.extend_with(|&(origin, _loan)| origin), |
| 100 | loan_invalidated_at.extend_with(|&(_origin, loan)| loan), |
| 101 | ), |
| 102 | |&(_origin, loan), &point| (loan, point), |
| 103 | ); |
| 104 | |
| 105 | // potential_subset_errors(Origin1, Origin2) :- |
| 106 | // placeholder(Origin1, Loan1), |
| 107 | // placeholder(Origin2, _), |
| 108 | // origin_contains_loan_on_entry(Origin2, Loan1), |
| 109 | // !known_contains(Origin2, Loan1). |
| 110 | potential_subset_errors.from_leapjoin( |
| 111 | &origin_contains_loan_on_entry, |
| 112 | ( |
| 113 | known_contains.filter_anti(|&(origin2, loan1)| (origin2, loan1)), |
| 114 | placeholder_origin.filter_with(|&(origin2, _loan1)| (origin2, ())), |
| 115 | placeholder_loan.extend_with(|&(_origin2, loan1)| loan1), |
| 116 | // remove symmetries: |
| 117 | datafrog::ValueFilter::from(|&(origin2, _loan1), &origin1| origin2 != origin1), |
| 118 | ), |
| 119 | |&(origin2, _loan1), &origin1| (origin1, origin2), |
| 120 | ); |
| 121 | } |
| 122 | |
| 123 | if result.dump_enabled { |
| 124 | for &(origin1, origin2) in subset.iter() { |
| 125 | result |
| 126 | .subset_anywhere |
| 127 | .entry(origin1) |
| 128 | .or_default() |
| 129 | .insert(origin2); |
| 130 | } |
| 131 | |
| 132 | let origin_contains_loan_on_entry = origin_contains_loan_on_entry.complete(); |
| 133 | for &(origin, loan) in origin_contains_loan_on_entry.iter() { |
| 134 | result |
| 135 | .origin_contains_loan_anywhere |
| 136 | .entry(origin) |
| 137 | .or_default() |
| 138 | .insert(loan); |
| 139 | } |
| 140 | } |
| 141 | |
| 142 | ( |
| 143 | potential_errors.complete(), |
| 144 | potential_subset_errors.complete(), |
| 145 | ) |
| 146 | }; |
| 147 | |
| 148 | info!( |
| 149 | "analysis done: {} `potential_errors` tuples, {} `potential_subset_errors` tuples, {:?}" , |
| 150 | potential_errors.len(), |
| 151 | potential_subset_errors.len(), |
| 152 | timer.elapsed() |
| 153 | ); |
| 154 | |
| 155 | (potential_errors, potential_subset_errors) |
| 156 | } |
| 157 | |