summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorNick Fitzgerald <fitzgen@gmail.com>2017-07-20 12:55:28 -0700
committerNick Fitzgerald <fitzgen@gmail.com>2017-07-20 15:34:34 -0700
commitdc73bc6cd8c74109bd04b8cc846b5262c7854f0a (patch)
treef02d14dcc798ec9a5ad7eb1a0b9d83598634e82d
parent9dbc2cad27837d6e5c088eb8d3b85148502c67b4 (diff)
Rearrange monotone framework and used templates analysis comments
They used to live in the same module, and there was less distinction between them, so they used to make more sense entangled with each other. Now that they are in separate files, they need a little bit of disentangling.
-rw-r--r--src/ir/analysis.rs40
-rw-r--r--src/ir/named.rs60
2 files changed, 50 insertions, 50 deletions
diff --git a/src/ir/analysis.rs b/src/ir/analysis.rs
index 28425a2c..e12f890f 100644
--- a/src/ir/analysis.rs
+++ b/src/ir/analysis.rs
@@ -1,4 +1,42 @@
-//! Fix-point analyses on the IR using the monotone framework.
+//! Fix-point analyses on the IR using the "monotone framework".
+//!
+//! A lattice is a set with a partial ordering between elements, where there is
+//! a single least upper bound and a single greatest least bound for every
+//! subset. We are dealing with finite lattices, which means that it has a
+//! finite number of elements, and it follows that there exists a single top and
+//! a single bottom member of the lattice. For example, the power set of a
+//! finite set forms a finite lattice where partial ordering is defined by set
+//! inclusion, that is `a <= b` if `a` is a subset of `b`. Here is the finite
+//! lattice constructed from the set {0,1,2}:
+//!
+//! ```text
+//! .----- Top = {0,1,2} -----.
+//! / | \
+//! / | \
+//! / | \
+//! {0,1} -------. {0,2} .--------- {1,2}
+//! | \ / \ / |
+//! | / \ |
+//! | / \ / \ |
+//! {0} --------' {1} `---------- {2}
+//! \ | /
+//! \ | /
+//! \ | /
+//! `------ Bottom = {} ------'
+//! ```
+//!
+//! A monotone function `f` is a function where if `x <= y`, then it holds that
+//! `f(x) <= f(y)`. It should be clear that running a monotone function to a
+//! fix-point on a finite lattice will always terminate: `f` can only "move"
+//! along the lattice in a single direction, and therefore can only either find
+//! a fix-point in the middle of the lattice or continue to the top or bottom
+//! depending if it is ascending or descending the lattice respectively.
+//!
+//! For a deeper introduction to the general form of this kind of analysis, see
+//! [Static Program Analysis by Anders Møller and Michael I. Schwartzbach][spa].
+//!
+//! [spa]: https://cs.au.dk/~amoeller/spa/spa.pdf
+
use std::fmt;
/// An analysis in the monotone framework.
diff --git a/src/ir/named.rs b/src/ir/named.rs
index 5351f309..6176faf1 100644
--- a/src/ir/named.rs
+++ b/src/ir/named.rs
@@ -75,56 +75,18 @@
//! union of its sub-item's used template parameters) and iterate to a
//! fixed-point.
//!
-//! We use the "monotone framework" for this fix-point analysis where our
-//! lattice is the mapping from each IR item to the powerset of the template
-//! parameters that appear in the input C++ header, our join function is set
-//! union, and we use the `ir::traversal::Trace` trait to implement the
-//! work-list optimization so we don't have to revisit every node in the graph
-//! when for every iteration towards the fix-point.
+//! We use the `ir::analysis::MonotoneFramework` infrastructure for this
+//! fix-point analysis, where our lattice is the mapping from each IR item to
+//! the powerset of the template parameters that appear in the input C++ header,
+//! our join function is set union. The set of template parameters appearing in
+//! the program is finite, as is the number of IR items. We start at our
+//! lattice's bottom element: every item mapping to an empty set of template
+//! parameters. Our analysis only adds members to each item's set of used
+//! template parameters, never removes them, so it is monotone. Because our
+//! lattice is finite and our constraint function is monotone, iteration to a
+//! fix-point will terminate.
//!
-//! A lattice is a set with a partial ordering between elements, where there is
-//! a single least upper bound and a single greatest least bound for every
-//! subset. We are dealing with finite lattices, which means that it has a
-//! finite number of elements, and it follows that there exists a single top and
-//! a single bottom member of the lattice. For example, the power set of a
-//! finite set forms a finite lattice where partial ordering is defined by set
-//! inclusion, that is `a <= b` if `a` is a subset of `b`. Here is the finite
-//! lattice constructed from the set {0,1,2}:
-//!
-//! ```text
-//! .----- Top = {0,1,2} -----.
-//! / | \
-//! / | \
-//! / | \
-//! {0,1} -------. {0,2} .--------- {1,2}
-//! | \ / \ / |
-//! | / \ |
-//! | / \ / \ |
-//! {0} --------' {1} `---------- {2}
-//! \ | /
-//! \ | /
-//! \ | /
-//! `------ Bottom = {} ------'
-//! ```
-//!
-//! A monotone function `f` is a function where if `x <= y`, then it holds that
-//! `f(x) <= f(y)`. It should be clear that running a monotone function to a
-//! fix-point on a finite lattice will always terminate: `f` can only "move"
-//! along the lattice in a single direction, and therefore can only either find
-//! a fix-point in the middle of the lattice or continue to the top or bottom
-//! depending if it is ascending or descending the lattice respectively.
-//!
-//! For our analysis, we are collecting the set of template parameters used by
-//! any given IR node. The set of template parameters appearing in the program
-//! is finite. Our lattice is their powerset. We start at the bottom element,
-//! the empty set. Our analysis only adds members to the set of used template
-//! parameters, never removes them, so it is monotone, and therefore iteration
-//! to a fix-point will terminate.
-//!
-//! For a deeper introduction to the general form of this kind of analysis, see
-//! [Static Program Analysis by Anders Møller and Michael I. Schwartzbach][spa].
-//!
-//! [spa]: https://cs.au.dk/~amoeller/spa/spa.pdf
+//! See `src/ir/analysis.rs` for more.
use super::analysis::MonotoneFramework;
use super::context::{BindgenContext, ItemId};