[rustc.git] / vendor / polonius-engine / src / output / datafrog_opt.rs

// Copyright 2017 The Rust Project Developers. See the COPYRIGHT\r
// file at the top-level directory of this distribution and at\r
// http://rust-lang.org/COPYRIGHT.\r
//\r
// Licensed under the Apache License, Version 2.0 <LICENSE-APACHE or\r
// http://www.apache.org/licenses/LICENSE-2.0> or the MIT license\r
// <LICENSE-MIT or http://opensource.org/licenses/MIT>, at your\r
// option. This file may not be copied, modified, or distributed\r
// except according to those terms.\r
\r
use datafrog::{Iteration, Relation, RelationLeaper};\r
use std::time::Instant;\r
\r
use crate::facts::FactTypes;\r
use crate::output::{Context, Output};\r
\r
pub(super) fn compute<T: FactTypes>(\r
    ctx: &Context<'_, T>,\r
    result: &mut Output<T>,\r
) -> Relation<(T::Loan, T::Point)> {\r
    let timer = Instant::now();\r
\r
    let errors = {\r
        // Static inputs\r
        let origin_live_on_entry_rel = &ctx.origin_live_on_entry;\r
        let cfg_edge_rel = &ctx.cfg_edge;\r
        let killed_rel = &ctx.killed;\r
\r
        // Create a new iteration context, ...\r
        let mut iteration = Iteration::new();\r
\r
        // `invalidates` facts, stored ready for joins\r
        let invalidates = iteration.variable::<((T::Loan, T::Point), ())>("invalidates");\r
\r
        // we need `origin_live_on_entry` in both variable and relation forms,\r
        // (respectively, for join and antijoin).\r
        let origin_live_on_entry_var =\r
            iteration.variable::<((T::Origin, T::Point), ())>("origin_live_on_entry");\r
\r
        // `borrow_region` input but organized for join\r
        let borrow_region_op =\r
            iteration.variable::<((T::Origin, T::Point), T::Loan)>("borrow_region_op");\r
\r
        // .decl subset(origin1, origin2, point)\r
        //\r
        // Indicates that `origin1: origin2` at `point`.\r
        let subset_o1p = iteration.variable::<((T::Origin, T::Point), T::Origin)>("subset_o1p");\r
\r
        // .decl requires(origin, loan, point)\r
        //\r
        // At `point`, things with `origin` may depend on data from `loan`.\r
        let requires_op = iteration.variable::<((T::Origin, T::Point), T::Loan)>("requires_op");\r
\r
        // .decl borrow_live_at(loan, point)\r
        //\r
        // True if the restrictions of the `loan` need to be enforced at `point`.\r
        let borrow_live_at = iteration.variable::<((T::Loan, T::Point), ())>("borrow_live_at");\r
\r
        // .decl live_to_dying_regions(origin1, origin2, point1, point2)\r
        //\r
        // The origins `origin1` and `origin2` are "live to dead"\r
        // on the edge `point1 -> point2` if:\r
        //\r
        // - In `point1`, `origin1` <= `origin2`\r
        // - In `point2`, `origin1` is live but `origin2` is dead.\r
        //\r
        // In that case, `point2` would like to add all the\r
        // live things reachable from `origin2` to `origin1`.\r
        //\r
        let live_to_dying_regions_o2pq = iteration\r
            .variable::<((T::Origin, T::Point, T::Point), T::Origin)>("live_to_dying_regions_o2pq");\r
\r
        // .decl dying_region_requires((origin, point1, point2), loan)\r
        //\r
        // The `origin` requires `loan`, but the `origin` goes dead\r
        // along the edge `point1 -> point2`.\r
        let dying_region_requires = iteration\r
            .variable::<((T::Origin, T::Point, T::Point), T::Loan)>("dying_region_requires");\r
\r
        // .decl dying_can_reach_origins(origin, point1, point2)\r
        //\r
        // Contains dead origins where we are interested\r
        // in computing the transitive closure of things they\r
        // can reach.\r
        //\r
        // FIXME: this relation was named before renaming the `regions` atoms to `origins`, and\r
        // will need to be renamed to change "_origins" to "_ascendants", "_roots", etc.\r
        let dying_can_reach_origins =\r
            iteration.variable::<((T::Origin, T::Point), T::Point)>("dying_can_reach_origins");\r
\r
        // .decl dying_can_reach(origin1, origin2, point1, point2)\r
        //\r
        // Indicates that `origin1`, which is dead\r
        // in `point2`, can reach `origin2` in `point1`.\r
        //\r
        // This is effectively the transitive subset\r
        // relation, but we try to limit it to origins\r
        // that are dying on the edge `point1 -> point2`.\r
        let dying_can_reach_o2q =\r
            iteration.variable::<((T::Origin, T::Point), (T::Origin, T::Point))>("dying_can_reach");\r
        let dying_can_reach_1 = iteration.variable_indistinct("dying_can_reach_1");\r
\r
        // .decl dying_can_reach_live(origin1, origin2, point1, point2)\r
        //\r
        // Indicates that, along the edge `point1 -> point2`, the dead (in `point2`)\r
        // `origin1` can reach the live (in `point2`) `origin2` via a subset\r
        // relation. This is a subset of the full `dying_can_reach`\r
        // relation where we filter down to those cases where `origin2` is\r
        // live in `point2`.\r
        let dying_can_reach_live = iteration\r
            .variable::<((T::Origin, T::Point, T::Point), T::Origin)>("dying_can_reach_live");\r
\r
        // .decl dead_borrow_region_can_reach_root((origin, point), loan)\r
        //\r
        // Indicates a "borrow region" `origin` at `point` which is not live on\r
        // entry to `point`.\r
        let dead_borrow_region_can_reach_root = iteration\r
            .variable::<((T::Origin, T::Point), T::Loan)>("dead_borrow_region_can_reach_root");\r
\r
        // .decl dead_borrow_region_can_reach_dead((origin2, point), loan)\r
        let dead_borrow_region_can_reach_dead = iteration\r
            .variable::<((T::Origin, T::Point), T::Loan)>("dead_borrow_region_can_reach_dead");\r
        let dead_borrow_region_can_reach_dead_1 =\r
            iteration.variable_indistinct("dead_borrow_region_can_reach_dead_1");\r
\r
        // .decl errors(loan, point)\r
        let errors = iteration.variable("errors");\r
\r
        // Make "variable" versions of the relations, needed for joins.\r
        borrow_region_op.extend(\r
            ctx.borrow_region\r
                .iter()\r
                .map(|&(origin, loan, point)| ((origin, point), loan)),\r
        );\r
        invalidates.extend(\r
            ctx.invalidates\r
                .iter()\r
                .map(|&(loan, point)| ((loan, point), ())),\r
        );\r
        origin_live_on_entry_var.extend(\r
            origin_live_on_entry_rel\r
                .iter()\r
                .map(|&(origin, point)| ((origin, point), ())),\r
        );\r
\r
        // subset(origin1, origin2, point) :- outlives(origin1, origin2, point).\r
        subset_o1p.extend(\r
            ctx.outlives\r
                .iter()\r
                .map(|&(origin1, origin2, point)| ((origin1, point), origin2)),\r
        );\r
\r
        // requires(origin, loan, point) :- borrow_region(origin, loan, point).\r
        requires_op.extend(\r
            ctx.borrow_region\r
                .iter()\r
                .map(|&(origin, loan, point)| ((origin, point), loan)),\r
        );\r
\r
        // .. and then start iterating rules!\r
        while iteration.changed() {\r
            // Cleanup step: remove symmetries\r
            // - remove origins which are `subset`s of themselves\r
            //\r
            // FIXME: investigate whether is there a better way to do that without complicating\r
            // the rules too much, because it would also require temporary variables and\r
            // impact performance. Until then, the big reduction in tuples improves performance\r
            // a lot, even if we're potentially adding a small number of tuples\r
            // per round just to remove them in the next round.\r
            subset_o1p\r
                .recent\r
                .borrow_mut()\r
                .elements\r
                .retain(|&((origin1, _), origin2)| origin1 != origin2);\r
\r
            // live_to_dying_regions(origin1, origin2, point1, point2) :-\r
            //   subset(origin1, origin2, point1),\r
            //   cfg_edge(point1, point2),\r
            //   origin_live_on_entry(origin1, point2),\r
            //   !origin_live_on_entry(origin2, point2).\r
            live_to_dying_regions_o2pq.from_leapjoin(\r
                &subset_o1p,\r
                (\r
                    cfg_edge_rel.extend_with(|&((_, point1), _)| point1),\r
                    origin_live_on_entry_rel.extend_with(|&((origin1, _), _)| origin1),\r
                    origin_live_on_entry_rel.extend_anti(|&((_, _), origin2)| origin2),\r
                ),\r
                |&((origin1, point1), origin2), &point2| ((origin2, point1, point2), origin1),\r
            );\r
\r
            // dying_region_requires((origin, point1, point2), loan) :-\r
            //   requires(origin, loan, point1),\r
            //   !killed(loan, point1),\r
            //   cfg_edge(point1, point2),\r
            //   !origin_live_on_entry(origin, point2).\r
            dying_region_requires.from_leapjoin(\r
                &requires_op,\r
                (\r
                    killed_rel.filter_anti(|&((_, point1), loan)| (loan, point1)),\r
                    cfg_edge_rel.extend_with(|&((_, point1), _)| point1),\r
                    origin_live_on_entry_rel.extend_anti(|&((origin, _), _)| origin),\r
                ),\r
                |&((origin, point1), loan), &point2| ((origin, point1, point2), loan),\r
            );\r
\r
            // dying_can_reach_origins(origin2, point1, point2) :-\r
            //   live_to_dying_regions(_, origin2, point1, point2).\r
            dying_can_reach_origins.from_map(\r
                &live_to_dying_regions_o2pq,\r
                |&((origin2, point1, point2), _origin1)| ((origin2, point1), point2),\r
            );\r
\r
            // dying_can_reach_origins(origin, point1, point2) :-\r
            //   dying_region_requires(origin, point1, point2, _loan).\r
            dying_can_reach_origins.from_map(\r
                &dying_region_requires,\r
                |&((origin, point1, point2), _loan)| ((origin, point1), point2),\r
            );\r
\r
            // dying_can_reach(origin1, origin2, point1, point2) :-\r
            //   dying_can_reach_origins(origin1, point1, point2),\r
            //   subset(origin1, origin2, point1).\r
            dying_can_reach_o2q.from_join(\r
                &dying_can_reach_origins,\r
                &subset_o1p,\r
                |&(origin1, point1), &point2, &origin2| ((origin2, point2), (origin1, point1)),\r
            );\r
\r
            // dying_can_reach(origin1, origin3, point1, point2) :-\r
            //   dying_can_reach(origin1, origin2, point1, point2),\r
            //   !origin_live_on_entry(origin2, point2),\r
            //   subset(origin2, origin3, point1).\r
            //\r
            // This is the "transitive closure" rule, but\r
            // note that we only apply it with the\r
            // "intermediate" `origin2` is dead at `point2`.\r
            dying_can_reach_1.from_antijoin(\r
                &dying_can_reach_o2q,\r
                &origin_live_on_entry_rel,\r
                |&(origin2, point2), &(origin1, point1)| ((origin2, point1), (origin1, point2)),\r
            );\r
            dying_can_reach_o2q.from_join(\r
                &dying_can_reach_1,\r
                &subset_o1p,\r
                |&(_origin2, point1), &(origin1, point2), &origin3| {\r
                    ((origin3, point2), (origin1, point1))\r
                },\r
            );\r
\r
            // dying_can_reach_live(origin1, origin2, point1, point2) :-\r
            //   dying_can_reach(origin1, origin2, point1, point2),\r
            //   origin_live_on_entry(origin2, point2).\r
            dying_can_reach_live.from_join(\r
                &dying_can_reach_o2q,\r
                &origin_live_on_entry_var,\r
                |&(origin2, point2), &(origin1, point1), _| ((origin1, point1, point2), origin2),\r
            );\r
\r
            // subset(origin1, origin2, point2) :-\r
            //   subset(origin1, origin2, point1),\r
            //   cfg_edge(point1, point2),\r
            //   origin_live_on_entry(origin1, point2),\r
            //   origin_live_on_entry(origin2, point2).\r
            //\r
            // Carry `origin1 <= origin2` from `point1` into `point2` if both `origin1` and\r
            // `origin2` are live in `point2`.\r
            subset_o1p.from_leapjoin(\r
                &subset_o1p,\r
                (\r
                    cfg_edge_rel.extend_with(|&((_, point1), _)| point1),\r
                    origin_live_on_entry_rel.extend_with(|&((origin1, _), _)| origin1),\r
                    origin_live_on_entry_rel.extend_with(|&((_, _), origin2)| origin2),\r
                ),\r
                |&((origin1, _point1), origin2), &point2| ((origin1, point2), origin2),\r
            );\r
\r
            // subset(origin1, origin3, point2) :-\r
            //   live_to_dying_regions(origin1, origin2, point1, point2),\r
            //   dying_can_reach_live(origin2, origin3, point1, point2).\r
            subset_o1p.from_join(\r
                &live_to_dying_regions_o2pq,\r
                &dying_can_reach_live,\r
                |&(_origin2, _point1, point2), &origin1, &origin3| ((origin1, point2), origin3),\r
            );\r
\r
            // requires(origin2, loan, point2) :-\r
            //   dying_region_requires(origin1, loan, point1, point2),\r
            //   dying_can_reach_live(origin1, origin2, point1, point2).\r
            //\r
            // Communicate a `origin1 requires loan` relation across\r
            // an edge `point1 -> point2` where `origin1` is dead in `point2`; in\r
            // that case, for each origin `origin2` live in `point2`\r
            // where `origin1 <= origin2` in `point1`, we add `origin2 requires loan`\r
            // to `point2`.\r
            requires_op.from_join(\r
                &dying_region_requires,\r
                &dying_can_reach_live,\r
                |&(_origin1, _point1, point2), &loan, &origin2| ((origin2, point2), loan),\r
            );\r
\r
            // requires(origin, loan, point2) :-\r
            //   requires(origin, loan, point1),\r
            //   !killed(loan, point1),\r
            //   cfg_edge(point1, point2),\r
            //   origin_live_on_entry(origin, point2).\r
            requires_op.from_leapjoin(\r
                &requires_op,\r
                (\r
                    killed_rel.filter_anti(|&((_, point1), loan)| (loan, point1)),\r
                    cfg_edge_rel.extend_with(|&((_, point1), _)| point1),\r
                    origin_live_on_entry_rel.extend_with(|&((origin, _), _)| origin),\r
                ),\r
                |&((origin, _), loan), &point2| ((origin, point2), loan),\r
            );\r
\r
            // dead_borrow_region_can_reach_root((origin, point), loan) :-\r
            //   borrow_region(origin, loan, point),\r
            //   !origin_live_on_entry(origin, point).\r
            dead_borrow_region_can_reach_root.from_antijoin(\r
                &borrow_region_op,\r
                &origin_live_on_entry_rel,\r
                |&(origin, point), &loan| ((origin, point), loan),\r
            );\r
\r
            // dead_borrow_region_can_reach_dead((origin, point), loan) :-\r
            //   dead_borrow_region_can_reach_root((origin, point), loan).\r
            dead_borrow_region_can_reach_dead\r
                .from_map(&dead_borrow_region_can_reach_root, |&tuple| tuple);\r
\r
            // dead_borrow_region_can_reach_dead((origin2, point), loan) :-\r
            //   dead_borrow_region_can_reach_dead(origin1, loan, point),\r
            //   subset(origin1, origin2, point),\r
            //   !origin_live_on_entry(origin2, point).\r
            dead_borrow_region_can_reach_dead_1.from_join(\r
                &dead_borrow_region_can_reach_dead,\r
                &subset_o1p,\r
                |&(_origin1, point), &loan, &origin2| ((origin2, point), loan),\r
            );\r
            dead_borrow_region_can_reach_dead.from_antijoin(\r
                &dead_borrow_region_can_reach_dead_1,\r
                &origin_live_on_entry_rel,\r
                |&(origin2, point), &loan| ((origin2, point), loan),\r
            );\r
\r
            // borrow_live_at(loan, point) :-\r
            //   requires(origin, loan, point),\r
            //   origin_live_on_entry(origin, point).\r
            borrow_live_at.from_join(\r
                &requires_op,\r
                &origin_live_on_entry_var,\r
                |&(_origin, point), &loan, _| ((loan, point), ()),\r
            );\r
\r
            // borrow_live_at(loan, point) :-\r
            //   dead_borrow_region_can_reach_dead(origin1, loan, point),\r
            //   subset(origin1, origin2, point),\r
            //   origin_live_on_entry(origin2, point).\r
            //\r
            // NB: the datafrog code below uses\r
            // `dead_borrow_region_can_reach_dead_1`, which is equal\r
            // to `dead_borrow_region_can_reach_dead` and `subset`\r
            // joined together.\r
            borrow_live_at.from_join(\r
                &dead_borrow_region_can_reach_dead_1,\r
                &origin_live_on_entry_var,\r
                |&(_origin2, point), &loan, _| ((loan, point), ()),\r
            );\r
\r
            // errors(loan, point) :-\r
            //   invalidates(loan, point),\r
            //   borrow_live_at(loan, point).\r
            errors.from_join(&invalidates, &borrow_live_at, |&(loan, point), _, _| {\r
                (loan, point)\r
            });\r
        }\r
\r
        if result.dump_enabled {\r
            let subset_o1p = subset_o1p.complete();\r
            assert!(\r
                subset_o1p\r
                    .iter()\r
                    .filter(|&((origin1, _), origin2)| origin1 == origin2)\r
                    .count()\r
                    == 0,\r
                "unwanted subset symmetries"\r
            );\r
            for &((origin1, location), origin2) in subset_o1p.iter() {\r
                result\r
                    .subset\r
                    .entry(location)\r
                    .or_default()\r
                    .entry(origin1)\r
                    .or_default()\r
                    .insert(origin2);\r
            }\r
\r
            let requires_op = requires_op.complete();\r
            for &((origin, location), loan) in requires_op.iter() {\r
                result\r
                    .restricts\r
                    .entry(location)\r
                    .or_default()\r
                    .entry(origin)\r
                    .or_default()\r
                    .insert(loan);\r
            }\r
\r
            let borrow_live_at = borrow_live_at.complete();\r
            for &((loan, location), _) in borrow_live_at.iter() {\r
                result\r
                    .borrow_live_at\r
                    .entry(location)\r
                    .or_default()\r
                    .push(loan);\r
            }\r
        }\r
\r
        errors.complete()\r
    };\r
\r
    info!(\r
        "errors is complete: {} tuples, {:?}",\r
        errors.len(),\r
        timer.elapsed()\r
    );\r
\r
    errors\r
}\r
Commit	Line	Data
ba9703b0 XL	1	// Copyright 2017 The Rust Project Developers. See the COPYRIGHT\r
	2	// file at the top-level directory of this distribution and at\r
	3	// http://rust-lang.org/COPYRIGHT.\r
	4	//\r
	5	// Licensed under the Apache License, Version 2.0 <LICENSE-APACHE or\r
	6	// http://www.apache.org/licenses/LICENSE-2.0> or the MIT license\r
	7	// <LICENSE-MIT or http://opensource.org/licenses/MIT>, at your\r
	8	// option. This file may not be copied, modified, or distributed\r
	9	// except according to those terms.\r
	10	\r
	11	use datafrog::{Iteration, Relation, RelationLeaper};\r
	12	use std::time::Instant;\r
	13	\r
	14	use crate::facts::FactTypes;\r
	15	use crate::output::{Context, Output};\r
	16	\r
	17	pub(super) fn compute<T: FactTypes>(\r
	18	ctx: &Context<'_, T>,\r
	19	result: &mut Output<T>,\r
	20	) -> Relation<(T::Loan, T::Point)> {\r
	21	let timer = Instant::now();\r
	22	\r
	23	let errors = {\r
	24	// Static inputs\r
	25	let origin_live_on_entry_rel = &ctx.origin_live_on_entry;\r
	26	let cfg_edge_rel = &ctx.cfg_edge;\r
	27	let killed_rel = &ctx.killed;\r
	28	\r
	29	// Create a new iteration context, ...\r
	30	let mut iteration = Iteration::new();\r
	31	\r
	32	// `invalidates` facts, stored ready for joins\r
	33	let invalidates = iteration.variable::<((T::Loan, T::Point), ())>("invalidates");\r
	34	\r
	35	// we need `origin_live_on_entry` in both variable and relation forms,\r
	36	// (respectively, for join and antijoin).\r
	37	let origin_live_on_entry_var =\r
	38	iteration.variable::<((T::Origin, T::Point), ())>("origin_live_on_entry");\r
	39	\r
	40	// `borrow_region` input but organized for join\r
	41	let borrow_region_op =\r
	42	iteration.variable::<((T::Origin, T::Point), T::Loan)>("borrow_region_op");\r
	43	\r
	44	// .decl subset(origin1, origin2, point)\r
	45	//\r
	46	// Indicates that `origin1: origin2` at `point`.\r
	47	let subset_o1p = iteration.variable::<((T::Origin, T::Point), T::Origin)>("subset_o1p");\r
	48	\r
	49	// .decl requires(origin, loan, point)\r
	50	//\r
	51	// At `point`, things with `origin` may depend on data from `loan`.\r
	52	let requires_op = iteration.variable::<((T::Origin, T::Point), T::Loan)>("requires_op");\r
	53	\r
	54	// .decl borrow_live_at(loan, point)\r
	55	//\r
	56	// True if the restrictions of the `loan` need to be enforced at `point`.\r
	57	let borrow_live_at = iteration.variable::<((T::Loan, T::Point), ())>("borrow_live_at");\r
	58	\r
	59	// .decl live_to_dying_regions(origin1, origin2, point1, point2)\r
	60	//\r
	61	// The origins `origin1` and `origin2` are "live to dead"\r
	62	// on the edge `point1 -> point2` if:\r
	63	//\r
	64	// - In `point1`, `origin1` <= `origin2`\r
65	// - In `point2`, `origin1` is live but `origin2` is dead.\r
66	//\r
67	// In that case, `point2` would like to add all the\r
68	// live things reachable from `origin2` to `origin1`.\r
69	//\r
70	let live_to_dying_regions_o2pq = iteration\r
71	.variable::<((T::Origin, T::Point, T::Point), T::Origin)>("live_to_dying_regions_o2pq");\r
72	\r
73	// .decl dying_region_requires((origin, point1, point2), loan)\r
74	//\r
75	// The `origin` requires `loan`, but the `origin` goes dead\r
76	// along the edge `point1 -> point2`.\r
77	let dying_region_requires = iteration\r
78	.variable::<((T::Origin, T::Point, T::Point), T::Loan)>("dying_region_requires");\r
79	\r
80	// .decl dying_can_reach_origins(origin, point1, point2)\r
81	//\r
82	// Contains dead origins where we are interested\r
83	// in computing the transitive closure of things they\r
84	// can reach.\r
85	//\r
86	// FIXME: this relation was named before renaming the `regions` atoms to `origins`, and\r
87	// will need to be renamed to change "_origins" to "_ascendants", "_roots", etc.\r
88	let dying_can_reach_origins =\r
89	iteration.variable::<((T::Origin, T::Point), T::Point)>("dying_can_reach_origins");\r
90	\r
91	// .decl dying_can_reach(origin1, origin2, point1, point2)\r
92	//\r
93	// Indicates that `origin1`, which is dead\r
94	// in `point2`, can reach `origin2` in `point1`.\r
95	//\r
96	// This is effectively the transitive subset\r
97	// relation, but we try to limit it to origins\r
98	// that are dying on the edge `point1 -> point2`.\r
99	let dying_can_reach_o2q =\r
100	iteration.variable::<((T::Origin, T::Point), (T::Origin, T::Point))>("dying_can_reach");\r
101	let dying_can_reach_1 = iteration.variable_indistinct("dying_can_reach_1");\r
102	\r
103	// .decl dying_can_reach_live(origin1, origin2, point1, point2)\r
104	//\r
105	// Indicates that, along the edge `point1 -> point2`, the dead (in `point2`)\r
106	// `origin1` can reach the live (in `point2`) `origin2` via a subset\r
107	// relation. This is a subset of the full `dying_can_reach`\r
108	// relation where we filter down to those cases where `origin2` is\r
109	// live in `point2`.\r
110	let dying_can_reach_live = iteration\r
111	.variable::<((T::Origin, T::Point, T::Point), T::Origin)>("dying_can_reach_live");\r
112	\r
113	// .decl dead_borrow_region_can_reach_root((origin, point), loan)\r
114	//\r
115	// Indicates a "borrow region" `origin` at `point` which is not live on\r
116	// entry to `point`.\r
117	let dead_borrow_region_can_reach_root = iteration\r
118	.variable::<((T::Origin, T::Point), T::Loan)>("dead_borrow_region_can_reach_root");\r
119	\r
120	// .decl dead_borrow_region_can_reach_dead((origin2, point), loan)\r
121	let dead_borrow_region_can_reach_dead = iteration\r
122	.variable::<((T::Origin, T::Point), T::Loan)>("dead_borrow_region_can_reach_dead");\r
123	let dead_borrow_region_can_reach_dead_1 =\r
124	iteration.variable_indistinct("dead_borrow_region_can_reach_dead_1");\r
125	\r
126	// .decl errors(loan, point)\r
127	let errors = iteration.variable("errors");\r
128	\r
129	// Make "variable" versions of the relations, needed for joins.\r
130	borrow_region_op.extend(\r
131	ctx.borrow_region\r
132	.iter()\r
133	.map(\|&(origin, loan, point)\| ((origin, point), loan)),\r
134	);\r
135	invalidates.extend(\r
136	ctx.invalidates\r
137	.iter()\r
138	.map(\|&(loan, point)\| ((loan, point), ())),\r
139	);\r
140	origin_live_on_entry_var.extend(\r
141	origin_live_on_entry_rel\r
142	.iter()\r
143	.map(\|&(origin, point)\| ((origin, point), ())),\r
144	);\r
145	\r
146	// subset(origin1, origin2, point) :- outlives(origin1, origin2, point).\r
147	subset_o1p.extend(\r
148	ctx.outlives\r
149	.iter()\r
150	.map(\|&(origin1, origin2, point)\| ((origin1, point), origin2)),\r
151	);\r
152	\r
153	// requires(origin, loan, point) :- borrow_region(origin, loan, point).\r
154	requires_op.extend(\r
155	ctx.borrow_region\r
156	.iter()\r
157	.map(\|&(origin, loan, point)\| ((origin, point), loan)),\r
158	);\r
159	\r
160	// .. and then start iterating rules!\r
161	while iteration.changed() {\r
162	// Cleanup step: remove symmetries\r
163	// - remove origins which are `subset`s of themselves\r
164	//\r
165	// FIXME: investigate whether is there a better way to do that without complicating\r
166	// the rules too much, because it would also require temporary variables and\r
167	// impact performance. Until then, the big reduction in tuples improves performance\r
168	// a lot, even if we're potentially adding a small number of tuples\r
169	// per round just to remove them in the next round.\r
170	subset_o1p\r
171	.recent\r
172	.borrow_mut()\r
173	.elements\r
174	.retain(\|&((origin1, _), origin2)\| origin1 != origin2);\r
175	\r
176	// live_to_dying_regions(origin1, origin2, point1, point2) :-\r
177	// subset(origin1, origin2, point1),\r
178	// cfg_edge(point1, point2),\r
179	// origin_live_on_entry(origin1, point2),\r
180	// !origin_live_on_entry(origin2, point2).\r
181	live_to_dying_regions_o2pq.from_leapjoin(\r
182	&subset_o1p,\r
183	(\r
184	cfg_edge_rel.extend_with(\|&((_, point1), _)\| point1),\r
185	origin_live_on_entry_rel.extend_with(\|&((origin1, _), _)\| origin1),\r
186	origin_live_on_entry_rel.extend_anti(\|&((_, _), origin2)\| origin2),\r
187	),\r
188	\|&((origin1, point1), origin2), &point2\| ((origin2, point1, point2), origin1),\r
189	);\r
190	\r
191	// dying_region_requires((origin, point1, point2), loan) :-\r
192	// requires(origin, loan, point1),\r
193	// !killed(loan, point1),\r
194	// cfg_edge(point1, point2),\r
195	// !origin_live_on_entry(origin, point2).\r
196	dying_region_requires.from_leapjoin(\r
197	&requires_op,\r
198	(\r
199	killed_rel.filter_anti(\|&((_, point1), loan)\| (loan, point1)),\r
200	cfg_edge_rel.extend_with(\|&((_, point1), _)\| point1),\r
201	origin_live_on_entry_rel.extend_anti(\|&((origin, _), _)\| origin),\r
202	),\r
203	\|&((origin, point1), loan), &point2\| ((origin, point1, point2), loan),\r
204	);\r
205	\r
206	// dying_can_reach_origins(origin2, point1, point2) :-\r
207	// live_to_dying_regions(_, origin2, point1, point2).\r
208	dying_can_reach_origins.from_map(\r
209	&live_to_dying_regions_o2pq,\r
210	\|&((origin2, point1, point2), _origin1)\| ((origin2, point1), point2),\r
211	);\r
212	\r
213	// dying_can_reach_origins(origin, point1, point2) :-\r
214	// dying_region_requires(origin, point1, point2, _loan).\r
215	dying_can_reach_origins.from_map(\r
216	&dying_region_requires,\r
217	\|&((origin, point1, point2), _loan)\| ((origin, point1), point2),\r
218	);\r
219	\r
220	// dying_can_reach(origin1, origin2, point1, point2) :-\r
221	// dying_can_reach_origins(origin1, point1, point2),\r
222	// subset(origin1, origin2, point1).\r
223	dying_can_reach_o2q.from_join(\r
224	&dying_can_reach_origins,\r
225	&subset_o1p,\r
226	\|&(origin1, point1), &point2, &origin2\| ((origin2, point2), (origin1, point1)),\r
227	);\r
228	\r
229	// dying_can_reach(origin1, origin3, point1, point2) :-\r
230	// dying_can_reach(origin1, origin2, point1, point2),\r
231	// !origin_live_on_entry(origin2, point2),\r
232	// subset(origin2, origin3, point1).\r
233	//\r
234	// This is the "transitive closure" rule, but\r
235	// note that we only apply it with the\r
236	// "intermediate" `origin2` is dead at `point2`.\r
237	dying_can_reach_1.from_antijoin(\r
238	&dying_can_reach_o2q,\r
239	&origin_live_on_entry_rel,\r
240	\|&(origin2, point2), &(origin1, point1)\| ((origin2, point1), (origin1, point2)),\r
241	);\r
242	dying_can_reach_o2q.from_join(\r
243	&dying_can_reach_1,\r
244	&subset_o1p,\r
245	\|&(_origin2, point1), &(origin1, point2), &origin3\| {\r
246	((origin3, point2), (origin1, point1))\r
247	},\r
248	);\r
249	\r
250	// dying_can_reach_live(origin1, origin2, point1, point2) :-\r
251	// dying_can_reach(origin1, origin2, point1, point2),\r
252	// origin_live_on_entry(origin2, point2).\r
253	dying_can_reach_live.from_join(\r
254	&dying_can_reach_o2q,\r
255	&origin_live_on_entry_var,\r
256	\|&(origin2, point2), &(origin1, point1), _\| ((origin1, point1, point2), origin2),\r
257	);\r
258	\r
259	// subset(origin1, origin2, point2) :-\r
260	// subset(origin1, origin2, point1),\r
261	// cfg_edge(point1, point2),\r
262	// origin_live_on_entry(origin1, point2),\r
263	// origin_live_on_entry(origin2, point2).\r
264	//\r
265	// Carry `origin1 <= origin2` from `point1` into `point2` if both `origin1` and\r
266	// `origin2` are live in `point2`.\r
267	subset_o1p.from_leapjoin(\r
268	&subset_o1p,\r
269	(\r
270	cfg_edge_rel.extend_with(\|&((_, point1), _)\| point1),\r
271	origin_live_on_entry_rel.extend_with(\|&((origin1, _), _)\| origin1),\r
272	origin_live_on_entry_rel.extend_with(\|&((_, _), origin2)\| origin2),\r
273	),\r
274	\|&((origin1, _point1), origin2), &point2\| ((origin1, point2), origin2),\r
275	);\r
276	\r
277	// subset(origin1, origin3, point2) :-\r
278	// live_to_dying_regions(origin1, origin2, point1, point2),\r
279	// dying_can_reach_live(origin2, origin3, point1, point2).\r
280	subset_o1p.from_join(\r
281	&live_to_dying_regions_o2pq,\r
282	&dying_can_reach_live,\r
283	\|&(_origin2, _point1, point2), &origin1, &origin3\| ((origin1, point2), origin3),\r
284	);\r
285	\r
286	// requires(origin2, loan, point2) :-\r
287	// dying_region_requires(origin1, loan, point1, point2),\r
288	// dying_can_reach_live(origin1, origin2, point1, point2).\r
289	//\r
290	// Communicate a `origin1 requires loan` relation across\r
291	// an edge `point1 -> point2` where `origin1` is dead in `point2`; in\r
292	// that case, for each origin `origin2` live in `point2`\r
293	// where `origin1 <= origin2` in `point1`, we add `origin2 requires loan`\r
294	// to `point2`.\r
295	requires_op.from_join(\r
296	&dying_region_requires,\r
297	&dying_can_reach_live,\r
298	\|&(_origin1, _point1, point2), &loan, &origin2\| ((origin2, point2), loan),\r
299	);\r
300	\r
301	// requires(origin, loan, point2) :-\r
302	// requires(origin, loan, point1),\r
303	// !killed(loan, point1),\r
304	// cfg_edge(point1, point2),\r
305	// origin_live_on_entry(origin, point2).\r
306	requires_op.from_leapjoin(\r
307	&requires_op,\r
308	(\r
309	killed_rel.filter_anti(\|&((_, point1), loan)\| (loan, point1)),\r
310	cfg_edge_rel.extend_with(\|&((_, point1), _)\| point1),\r
311	origin_live_on_entry_rel.extend_with(\|&((origin, _), _)\| origin),\r
312	),\r
313	\|&((origin, _), loan), &point2\| ((origin, point2), loan),\r
314	);\r
315	\r
316	// dead_borrow_region_can_reach_root((origin, point), loan) :-\r
317	// borrow_region(origin, loan, point),\r
318	// !origin_live_on_entry(origin, point).\r
319	dead_borrow_region_can_reach_root.from_antijoin(\r
320	&borrow_region_op,\r
321	&origin_live_on_entry_rel,\r
322	\|&(origin, point), &loan\| ((origin, point), loan),\r
323	);\r
324	\r
325	// dead_borrow_region_can_reach_dead((origin, point), loan) :-\r
326	// dead_borrow_region_can_reach_root((origin, point), loan).\r
327	dead_borrow_region_can_reach_dead\r
328	.from_map(&dead_borrow_region_can_reach_root, \|&tuple\| tuple);\r
329	\r
330	// dead_borrow_region_can_reach_dead((origin2, point), loan) :-\r
331	// dead_borrow_region_can_reach_dead(origin1, loan, point),\r
332	// subset(origin1, origin2, point),\r
333	// !origin_live_on_entry(origin2, point).\r
334	dead_borrow_region_can_reach_dead_1.from_join(\r
335	&dead_borrow_region_can_reach_dead,\r
336	&subset_o1p,\r
337	\|&(_origin1, point), &loan, &origin2\| ((origin2, point), loan),\r
338	);\r
339	dead_borrow_region_can_reach_dead.from_antijoin(\r
340	&dead_borrow_region_can_reach_dead_1,\r
341	&origin_live_on_entry_rel,\r
342	\|&(origin2, point), &loan\| ((origin2, point), loan),\r
343	);\r
344	\r
345	// borrow_live_at(loan, point) :-\r
346	// requires(origin, loan, point),\r
347	// origin_live_on_entry(origin, point).\r
348	borrow_live_at.from_join(\r
349	&requires_op,\r
350	&origin_live_on_entry_var,\r
351	\|&(_origin, point), &loan, _\| ((loan, point), ()),\r
352	);\r
353	\r
354	// borrow_live_at(loan, point) :-\r
355	// dead_borrow_region_can_reach_dead(origin1, loan, point),\r
356	// subset(origin1, origin2, point),\r
357	// origin_live_on_entry(origin2, point).\r
358	//\r
359	// NB: the datafrog code below uses\r
360	// `dead_borrow_region_can_reach_dead_1`, which is equal\r
361	// to `dead_borrow_region_can_reach_dead` and `subset`\r
362	// joined together.\r
363	borrow_live_at.from_join(\r
364	&dead_borrow_region_can_reach_dead_1,\r
365	&origin_live_on_entry_var,\r
366	\|&(_origin2, point), &loan, _\| ((loan, point), ()),\r
367	);\r
368	\r
369	// errors(loan, point) :-\r
370	// invalidates(loan, point),\r
371	// borrow_live_at(loan, point).\r
372	errors.from_join(&invalidates, &borrow_live_at, \|&(loan, point), _, _\| {\r
373	(loan, point)\r
374	});\r
375	}\r
376	\r
377	if result.dump_enabled {\r
378	let subset_o1p = subset_o1p.complete();\r
379	assert!(\r
380	subset_o1p\r
381	.iter()\r
382	.filter(\|&((origin1, _), origin2)\| origin1 == origin2)\r
383	.count()\r
384	== 0,\r
385	"unwanted subset symmetries"\r
386	);\r
387	for &((origin1, location), origin2) in subset_o1p.iter() {\r
388	result\r
389	.subset\r
390	.entry(location)\r
391	.or_default()\r
392	.entry(origin1)\r
393	.or_default()\r
394	.insert(origin2);\r
395	}\r
396	\r
397	let requires_op = requires_op.complete();\r
398	for &((origin, location), loan) in requires_op.iter() {\r
399	result\r
400	.restricts\r
401	.entry(location)\r
402	.or_default()\r
403	.entry(origin)\r
404	.or_default()\r
405	.insert(loan);\r
406	}\r
407	\r
408	let borrow_live_at = borrow_live_at.complete();\r
409	for &((loan, location), _) in borrow_live_at.iter() {\r
410	result\r
411	.borrow_live_at\r
412	.entry(location)\r
413	.or_default()\r
414	.push(loan);\r
415	}\r
416	}\r
417	\r
418	errors.complete()\r
419	};\r
420	\r
421	info!(\r
422	"errors is complete: {} tuples, {:?}",\r
423	errors.len(),\r
424	timer.elapsed()\r
425	);\r
426	\r
427	errors\r
428	}\r