]> git.proxmox.com Git - rustc.git/blobdiff - vendor/polonius-engine/src/output/datafrog_opt.rs
New upstream version 1.44.1+dfsg1
[rustc.git] / vendor / polonius-engine / src / output / datafrog_opt.rs
index 8140535015a258539ed4262a6a129c8f99ef8524..0ffd390b8aa299aa8a1b7f2114a6733329cd63e3 100644 (file)
-// Copyright 2017 The Rust Project Developers. See the COPYRIGHT
-// file at the top-level directory of this distribution and at
-// http://rust-lang.org/COPYRIGHT.
-//
-// Licensed under the Apache License, Version 2.0 <LICENSE-APACHE or
-// http://www.apache.org/licenses/LICENSE-2.0> or the MIT license
-// <LICENSE-MIT or http://opensource.org/licenses/MIT>, at your
-// option. This file may not be copied, modified, or distributed
-// except according to those terms.
-
-use datafrog::{Iteration, Relation, RelationLeaper};
-use std::time::Instant;
-
-use crate::facts::FactTypes;
-use crate::output::{Context, Output};
-
-pub(super) fn compute<T: FactTypes>(
-    ctx: &Context<'_, T>,
-    result: &mut Output<T>,
-) -> Relation<(T::Loan, T::Point)> {
-    let timer = Instant::now();
-
-    let errors = {
-        // Static inputs
-        let origin_live_on_entry_rel = &ctx.origin_live_on_entry;
-        let cfg_edge_rel = &ctx.cfg_edge;
-        let killed_rel = &ctx.killed;
-
-        // Create a new iteration context, ...
-        let mut iteration = Iteration::new();
-
-        // `invalidates` facts, stored ready for joins
-        let invalidates = iteration.variable::<((T::Loan, T::Point), ())>("invalidates");
-
-        // we need `origin_live_on_entry` in both variable and relation forms,
-        // (respectively, for join and antijoin).
-        let origin_live_on_entry_var =
-            iteration.variable::<((T::Origin, T::Point), ())>("origin_live_on_entry");
-
-        // `borrow_region` input but organized for join
-        let borrow_region_op =
-            iteration.variable::<((T::Origin, T::Point), T::Loan)>("borrow_region_op");
-
-        // .decl subset(origin1, origin2, point)
-        //
-        // Indicates that `origin1: origin2` at `point`.
-        let subset_o1p = iteration.variable::<((T::Origin, T::Point), T::Origin)>("subset_o1p");
-
-        // .decl requires(origin, loan, point)
-        //
-        // At `point`, things with `origin` may depend on data from `loan`.
-        let requires_op = iteration.variable::<((T::Origin, T::Point), T::Loan)>("requires_op");
-
-        // .decl borrow_live_at(loan, point)
-        //
-        // True if the restrictions of the `loan` need to be enforced at `point`.
-        let borrow_live_at = iteration.variable::<((T::Loan, T::Point), ())>("borrow_live_at");
-
-        // .decl live_to_dying_regions(origin1, origin2, point1, point2)
-        //
-        // The origins `origin1` and `origin2` are "live to dead"
-        // on the edge `point1 -> point2` if:
-        //
-        // - In `point1`, `origin1` <= `origin2`
-        // - In `point2`, `origin1` is live but `origin2` is dead.
-        //
-        // In that case, `point2` would like to add all the
-        // live things reachable from `origin2` to `origin1`.
-        //
-        let live_to_dying_regions_o2pq = iteration
-            .variable::<((T::Origin, T::Point, T::Point), T::Origin)>("live_to_dying_regions_o2pq");
-
-        // .decl dying_region_requires((origin, point1, point2), loan)
-        //
-        // The `origin` requires `loan`, but the `origin` goes dead
-        // along the edge `point1 -> point2`.
-        let dying_region_requires = iteration
-            .variable::<((T::Origin, T::Point, T::Point), T::Loan)>("dying_region_requires");
-
-        // .decl dying_can_reach_origins(origin, point1, point2)
-        //
-        // Contains dead origins where we are interested
-        // in computing the transitive closure of things they
-        // can reach.
-        //
-        // FIXME: this relation was named before renaming the `regions` atoms to `origins`, and
-        // will need to be renamed to change "_origins" to "_ascendants", "_roots", etc.
-        let dying_can_reach_origins =
-            iteration.variable::<((T::Origin, T::Point), T::Point)>("dying_can_reach_origins");
-
-        // .decl dying_can_reach(origin1, origin2, point1, point2)
-        //
-        // Indicates that `origin1`, which is dead
-        // in `point2`, can reach `origin2` in `point1`.
-        //
-        // This is effectively the transitive subset
-        // relation, but we try to limit it to origins
-        // that are dying on the edge `point1 -> point2`.
-        let dying_can_reach_o2q =
-            iteration.variable::<((T::Origin, T::Point), (T::Origin, T::Point))>("dying_can_reach");
-        let dying_can_reach_1 = iteration.variable_indistinct("dying_can_reach_1");
-
-        // .decl dying_can_reach_live(origin1, origin2, point1, point2)
-        //
-        // Indicates that, along the edge `point1 -> point2`, the dead (in `point2`)
-        // `origin1` can reach the live (in `point2`) `origin2` via a subset
-        // relation. This is a subset of the full `dying_can_reach`
-        // relation where we filter down to those cases where `origin2` is
-        // live in `point2`.
-        let dying_can_reach_live = iteration
-            .variable::<((T::Origin, T::Point, T::Point), T::Origin)>("dying_can_reach_live");
-
-        // .decl dead_borrow_region_can_reach_root((origin, point), loan)
-        //
-        // Indicates a "borrow region" `origin` at `point` which is not live on
-        // entry to `point`.
-        let dead_borrow_region_can_reach_root = iteration
-            .variable::<((T::Origin, T::Point), T::Loan)>("dead_borrow_region_can_reach_root");
-
-        // .decl dead_borrow_region_can_reach_dead((origin2, point), loan)
-        let dead_borrow_region_can_reach_dead = iteration
-            .variable::<((T::Origin, T::Point), T::Loan)>("dead_borrow_region_can_reach_dead");
-        let dead_borrow_region_can_reach_dead_1 =
-            iteration.variable_indistinct("dead_borrow_region_can_reach_dead_1");
-
-        // .decl errors(loan, point)
-        let errors = iteration.variable("errors");
-
-        // Make "variable" versions of the relations, needed for joins.
-        borrow_region_op.extend(
-            ctx.borrow_region
-                .iter()
-                .map(|&(origin, loan, point)| ((origin, point), loan)),
-        );
-        invalidates.extend(
-            ctx.invalidates
-                .iter()
-                .map(|&(loan, point)| ((loan, point), ())),
-        );
-        origin_live_on_entry_var.extend(
-            origin_live_on_entry_rel
-                .iter()
-                .map(|&(origin, point)| ((origin, point), ())),
-        );
-
-        // subset(origin1, origin2, point) :- outlives(origin1, origin2, point).
-        subset_o1p.extend(
-            ctx.outlives
-                .iter()
-                .map(|&(origin1, origin2, point)| ((origin1, point), origin2)),
-        );
-
-        // requires(origin, loan, point) :- borrow_region(origin, loan, point).
-        requires_op.extend(
-            ctx.borrow_region
-                .iter()
-                .map(|&(origin, loan, point)| ((origin, point), loan)),
-        );
-
-        // .. and then start iterating rules!
-        while iteration.changed() {
-            // Cleanup step: remove symmetries
-            // - remove origins which are `subset`s of themselves
-            //
-            // FIXME: investigate whether is there a better way to do that without complicating
-            // the rules too much, because it would also require temporary variables and
-            // impact performance. Until then, the big reduction in tuples improves performance
-            // a lot, even if we're potentially adding a small number of tuples
-            // per round just to remove them in the next round.
-            subset_o1p
-                .recent
-                .borrow_mut()
-                .elements
-                .retain(|&((origin1, _), origin2)| origin1 != origin2);
-
-            // live_to_dying_regions(origin1, origin2, point1, point2) :-
-            //   subset(origin1, origin2, point1),
-            //   cfg_edge(point1, point2),
-            //   origin_live_on_entry(origin1, point2),
-            //   !origin_live_on_entry(origin2, point2).
-            live_to_dying_regions_o2pq.from_leapjoin(
-                &subset_o1p,
-                (
-                    cfg_edge_rel.extend_with(|&((_, point1), _)| point1),
-                    origin_live_on_entry_rel.extend_with(|&((origin1, _), _)| origin1),
-                    origin_live_on_entry_rel.extend_anti(|&((_, _), origin2)| origin2),
-                ),
-                |&((origin1, point1), origin2), &point2| ((origin2, point1, point2), origin1),
-            );
-
-            // dying_region_requires((origin, point1, point2), loan) :-
-            //   requires(origin, loan, point1),
-            //   !killed(loan, point1),
-            //   cfg_edge(point1, point2),
-            //   !origin_live_on_entry(origin, point2).
-            dying_region_requires.from_leapjoin(
-                &requires_op,
-                (
-                    killed_rel.filter_anti(|&((_, point1), loan)| (loan, point1)),
-                    cfg_edge_rel.extend_with(|&((_, point1), _)| point1),
-                    origin_live_on_entry_rel.extend_anti(|&((origin, _), _)| origin),
-                ),
-                |&((origin, point1), loan), &point2| ((origin, point1, point2), loan),
-            );
-
-            // dying_can_reach_origins(origin2, point1, point2) :-
-            //   live_to_dying_regions(_, origin2, point1, point2).
-            dying_can_reach_origins.from_map(
-                &live_to_dying_regions_o2pq,
-                |&((origin2, point1, point2), _origin1)| ((origin2, point1), point2),
-            );
-
-            // dying_can_reach_origins(origin, point1, point2) :-
-            //   dying_region_requires(origin, point1, point2, _loan).
-            dying_can_reach_origins.from_map(
-                &dying_region_requires,
-                |&((origin, point1, point2), _loan)| ((origin, point1), point2),
-            );
-
-            // dying_can_reach(origin1, origin2, point1, point2) :-
-            //   dying_can_reach_origins(origin1, point1, point2),
-            //   subset(origin1, origin2, point1).
-            dying_can_reach_o2q.from_join(
-                &dying_can_reach_origins,
-                &subset_o1p,
-                |&(origin1, point1), &point2, &origin2| ((origin2, point2), (origin1, point1)),
-            );
-
-            // dying_can_reach(origin1, origin3, point1, point2) :-
-            //   dying_can_reach(origin1, origin2, point1, point2),
-            //   !origin_live_on_entry(origin2, point2),
-            //   subset(origin2, origin3, point1).
-            //
-            // This is the "transitive closure" rule, but
-            // note that we only apply it with the
-            // "intermediate" `origin2` is dead at `point2`.
-            dying_can_reach_1.from_antijoin(
-                &dying_can_reach_o2q,
-                &origin_live_on_entry_rel,
-                |&(origin2, point2), &(origin1, point1)| ((origin2, point1), (origin1, point2)),
-            );
-            dying_can_reach_o2q.from_join(
-                &dying_can_reach_1,
-                &subset_o1p,
-                |&(_origin2, point1), &(origin1, point2), &origin3| {
-                    ((origin3, point2), (origin1, point1))
-                },
-            );
-
-            // dying_can_reach_live(origin1, origin2, point1, point2) :-
-            //   dying_can_reach(origin1, origin2, point1, point2),
-            //   origin_live_on_entry(origin2, point2).
-            dying_can_reach_live.from_join(
-                &dying_can_reach_o2q,
-                &origin_live_on_entry_var,
-                |&(origin2, point2), &(origin1, point1), _| ((origin1, point1, point2), origin2),
-            );
-
-            // subset(origin1, origin2, point2) :-
-            //   subset(origin1, origin2, point1),
-            //   cfg_edge(point1, point2),
-            //   origin_live_on_entry(origin1, point2),
-            //   origin_live_on_entry(origin2, point2).
-            //
-            // Carry `origin1 <= origin2` from `point1` into `point2` if both `origin1` and
-            // `origin2` are live in `point2`.
-            subset_o1p.from_leapjoin(
-                &subset_o1p,
-                (
-                    cfg_edge_rel.extend_with(|&((_, point1), _)| point1),
-                    origin_live_on_entry_rel.extend_with(|&((origin1, _), _)| origin1),
-                    origin_live_on_entry_rel.extend_with(|&((_, _), origin2)| origin2),
-                ),
-                |&((origin1, _point1), origin2), &point2| ((origin1, point2), origin2),
-            );
-
-            // subset(origin1, origin3, point2) :-
-            //   live_to_dying_regions(origin1, origin2, point1, point2),
-            //   dying_can_reach_live(origin2, origin3, point1, point2).
-            subset_o1p.from_join(
-                &live_to_dying_regions_o2pq,
-                &dying_can_reach_live,
-                |&(_origin2, _point1, point2), &origin1, &origin3| ((origin1, point2), origin3),
-            );
-
-            // requires(origin2, loan, point2) :-
-            //   dying_region_requires(origin1, loan, point1, point2),
-            //   dying_can_reach_live(origin1, origin2, point1, point2).
-            //
-            // Communicate a `origin1 requires loan` relation across
-            // an edge `point1 -> point2` where `origin1` is dead in `point2`; in
-            // that case, for each origin `origin2` live in `point2`
-            // where `origin1 <= origin2` in `point1`, we add `origin2 requires loan`
-            // to `point2`.
-            requires_op.from_join(
-                &dying_region_requires,
-                &dying_can_reach_live,
-                |&(_origin1, _point1, point2), &loan, &origin2| ((origin2, point2), loan),
-            );
-
-            // requires(origin, loan, point2) :-
-            //   requires(origin, loan, point1),
-            //   !killed(loan, point1),
-            //   cfg_edge(point1, point2),
-            //   origin_live_on_entry(origin, point2).
-            requires_op.from_leapjoin(
-                &requires_op,
-                (
-                    killed_rel.filter_anti(|&((_, point1), loan)| (loan, point1)),
-                    cfg_edge_rel.extend_with(|&((_, point1), _)| point1),
-                    origin_live_on_entry_rel.extend_with(|&((origin, _), _)| origin),
-                ),
-                |&((origin, _), loan), &point2| ((origin, point2), loan),
-            );
-
-            // dead_borrow_region_can_reach_root((origin, point), loan) :-
-            //   borrow_region(origin, loan, point),
-            //   !origin_live_on_entry(origin, point).
-            dead_borrow_region_can_reach_root.from_antijoin(
-                &borrow_region_op,
-                &origin_live_on_entry_rel,
-                |&(origin, point), &loan| ((origin, point), loan),
-            );
-
-            // dead_borrow_region_can_reach_dead((origin, point), loan) :-
-            //   dead_borrow_region_can_reach_root((origin, point), loan).
-            dead_borrow_region_can_reach_dead
-                .from_map(&dead_borrow_region_can_reach_root, |&tuple| tuple);
-
-            // dead_borrow_region_can_reach_dead((origin2, point), loan) :-
-            //   dead_borrow_region_can_reach_dead(origin1, loan, point),
-            //   subset(origin1, origin2, point),
-            //   !origin_live_on_entry(origin2, point).
-            dead_borrow_region_can_reach_dead_1.from_join(
-                &dead_borrow_region_can_reach_dead,
-                &subset_o1p,
-                |&(_origin1, point), &loan, &origin2| ((origin2, point), loan),
-            );
-            dead_borrow_region_can_reach_dead.from_antijoin(
-                &dead_borrow_region_can_reach_dead_1,
-                &origin_live_on_entry_rel,
-                |&(origin2, point), &loan| ((origin2, point), loan),
-            );
-
-            // borrow_live_at(loan, point) :-
-            //   requires(origin, loan, point),
-            //   origin_live_on_entry(origin, point).
-            borrow_live_at.from_join(
-                &requires_op,
-                &origin_live_on_entry_var,
-                |&(_origin, point), &loan, _| ((loan, point), ()),
-            );
-
-            // borrow_live_at(loan, point) :-
-            //   dead_borrow_region_can_reach_dead(origin1, loan, point),
-            //   subset(origin1, origin2, point),
-            //   origin_live_on_entry(origin2, point).
-            //
-            // NB: the datafrog code below uses
-            // `dead_borrow_region_can_reach_dead_1`, which is equal
-            // to `dead_borrow_region_can_reach_dead` and `subset`
-            // joined together.
-            borrow_live_at.from_join(
-                &dead_borrow_region_can_reach_dead_1,
-                &origin_live_on_entry_var,
-                |&(_origin2, point), &loan, _| ((loan, point), ()),
-            );
-
-            // errors(loan, point) :-
-            //   invalidates(loan, point),
-            //   borrow_live_at(loan, point).
-            errors.from_join(&invalidates, &borrow_live_at, |&(loan, point), _, _| {
-                (loan, point)
-            });
-        }
-
-        if result.dump_enabled {
-            let subset_o1p = subset_o1p.complete();
-            assert!(
-                subset_o1p
-                    .iter()
-                    .filter(|&((origin1, _), origin2)| origin1 == origin2)
-                    .count()
-                    == 0,
-                "unwanted subset symmetries"
-            );
-            for &((origin1, location), origin2) in subset_o1p.iter() {
-                result
-                    .subset
-                    .entry(location)
-                    .or_default()
-                    .entry(origin1)
-                    .or_default()
-                    .insert(origin2);
-            }
-
-            let requires_op = requires_op.complete();
-            for &((origin, location), loan) in requires_op.iter() {
-                result
-                    .restricts
-                    .entry(location)
-                    .or_default()
-                    .entry(origin)
-                    .or_default()
-                    .insert(loan);
-            }
-
-            let borrow_live_at = borrow_live_at.complete();
-            for &((loan, location), _) in borrow_live_at.iter() {
-                result
-                    .borrow_live_at
-                    .entry(location)
-                    .or_default()
-                    .push(loan);
-            }
-        }
-
-        errors.complete()
-    };
-
-    info!(
-        "errors is complete: {} tuples, {:?}",
-        errors.len(),
-        timer.elapsed()
-    );
-
-    errors
-}
+// 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