Add documentation to rty and some other modules

src/analyze.rs

@@ -1,3 +1,11 @@
+//! Analysis of Rust MIR to generate a CHC system.
+//!
+//! The [`Analyzer`] generates subtyping constraints in the form of CHCs ([`chc::System`]).
+//! The entry point is [`crate_::Analyzer::run`], followed by [`local_def::Analyzer::run`]
+//! and [`basic_block::Analyzer::run`], while accumulating the necessary information in
+//! [`Analyzer`]. Once [`chc::System`] is collected for the entire input, it invokes an external
+//! CHC solver with the [`Analyzer::solve`] and subsequently reports the result.
+
 use std::cell::RefCell;
 use std::collections::HashMap;
 use std::rc::Rc;

src/analyze/annot.rs

@@ -1,3 +1,5 @@
+//! Supporting implementation for parsing Thrust annotations.
+
 use rustc_ast::ast::Attribute;
 use rustc_ast::tokenstream::TokenStream;
 use rustc_index::IndexVec;
@@ -31,6 +33,10 @@ pub fn callable_path() -> [Symbol; 2] {
     [Symbol::intern("thrust"), Symbol::intern("callable")]
 }
 
+/// A [`annot::Resolver`] implementation for resolving function parameters.
+///
+/// The parameter names and their sorts needs to be configured via
+/// [`ParamResolver::push_param`] before use.
 #[derive(Debug, Clone, Default)]
 pub struct ParamResolver {
     params: IndexVec<rty::FunctionParamIdx, (Symbol, chc::Sort)>,
@@ -52,6 +58,10 @@ impl ParamResolver {
     }
 }
 
+/// A [`annot::Resolver`] implementation for resolving the special identifier `result`.
+///
+/// The `result` identifier is used to refer to [`rty::RefinedTypeVar::Value`] in postconditions, denoting
+/// the return value of a function.
 #[derive(Debug, Clone)]
 pub struct ResultResolver {
     result_symbol: Symbol,

src/analyze/crate_.rs

@@ -1,3 +1,5 @@
+//! Analyze a local crate.
+
 use std::collections::HashSet;
 
 use rustc_hir::def::DefKind;
@@ -12,6 +14,16 @@ use crate::chc;
 use crate::refine::{self, TemplateTypeGenerator, UnrefinedTypeGenerator};
 use crate::rty::{self, ClauseBuilderExt as _};
 
+/// An implementation of local crate analysis.
+///
+/// The entry point is [`Analyzer::run`], which performs the following steps in order:
+///
+/// 1. Register enum definitions found in the crate.
+/// 2. Give initial refinement types to local function definitions based on their signatures and
+///    annotations. This generates template refinement types with predicate variables for parameters and
+///    return types that are not known via annotations.
+/// 3. Type local function definition bodies via [`super::local_def::Analyzer`] using the refinement types
+///    generated in the previous step.
 pub struct Analyzer<'tcx, 'ctx> {
     tcx: TyCtxt<'tcx>,
     ctx: &'ctx mut analyze::Analyzer<'tcx>,

src/analyze/did_cache.rs

@@ -1,3 +1,5 @@
+//! Retrieves and caches well-known [`DefId`]s.
+
 use std::cell::OnceCell;
 
 use rustc_middle::ty::TyCtxt;
@@ -10,6 +12,10 @@ struct DefIds {
     nonnull: OnceCell<Option<DefId>>,
 }
 
+/// Retrieves and caches well-known [`DefId`]s.
+///
+/// [`DefId`]s of some well-known types can be retrieved as lang items or via the definition of
+/// lang items. This struct implements that logic and caches the results.
 #[derive(Clone)]
 pub struct DefIdCache<'tcx> {
     tcx: TyCtxt<'tcx>,

src/analyze/local_def.rs

@@ -1,3 +1,5 @@
+//! Analyze a local definition.
+
 use std::collections::{HashMap, HashSet};
 
 use rustc_index::bit_set::BitSet;
@@ -12,6 +14,10 @@ use crate::pretty::PrettyDisplayExt as _;
 use crate::refine::{BasicBlockType, TemplateTypeGenerator};
 use crate::rty;
 
+/// An implementation of the typing of local definitions.
+///
+/// The current implementation only applies to function definitions. The entry point is
+/// [`Analyzer::run`], which generates constraints during typing, given the expected type of the function.
 pub struct Analyzer<'tcx, 'ctx> {
     ctx: &'ctx mut analyze::Analyzer<'tcx>,
     tcx: TyCtxt<'tcx>,

src/refine.rs

@@ -1,3 +1,12 @@
+//! Core logic of refinement typing.
+//!
+//! This module includes the definition of the refinement typing environment and the template
+//! type generation from MIR types.
+//!
+//! This module is used by the [`crate::analyze`] module. There is currently no clear boundary between
+//! the `analyze` and `refine` modules, so it is a TODO to integrate this into the `analyze`
+//! module and remove this one.
+
 mod template;
 pub use template::{TemplateScope, TemplateTypeGenerator, UnrefinedTypeGenerator};
 

src/refine/basic_block.rs

@@ -1,12 +1,17 @@
+//! The refinement type for a basic block.
+
 use pretty::{termcolor, Pretty};
 use rustc_index::IndexVec;
 use rustc_middle::mir::Local;
 use rustc_middle::ty as mir_ty;
 
 use crate::rty;
 
-/// `BasicBlockType` is a special case of `FunctionType` whose parameters are
-/// associated with `Local`s.
+/// A special case of [`rty::FunctionType`] whose parameters are associated with [`Local`]s.
+///
+/// Thrust handles basic blocks as functions, but it needs to associate function
+/// parameters with MIR [`Local`]s during its analysis. [`BasicBlockType`] includes this mapping
+/// from function parameters to [`Local`]s, along with the underlying function type.
 #[derive(Debug, Clone)]
 pub struct BasicBlockType {
     // TODO: make this completely private by exposing appropriate ctor

src/rty.rs

@@ -1,3 +1,42 @@
+//! Data structures for refinement types.
+//!
+//! Thrust is a refinement type system, and so its analysis is about giving refinement types to
+//! variables and terms. This module defines the data structures for representing refinement
+//! types. The central data structure is [`RefinedType`], which is just [`Type`] plus [`Refinement`].
+//!
+//! Note that there are two notions of "variables" in this module. First is a type variable which is
+//! a polymorphic type parameter which is represented by [`TypeParamIdx`], and forms one of valid type as [`ParamType`].
+//! `T` in `struct S<T> { f: T }` is a type variable. See [`params`] module for the handling of type parameters.
+//! Second is a logical variable which is a variable that can appear in logical predicates.
+//! `x` and `y` in `{ x: int | x > y }` are logical variables.
+//! The actual representation of logical variables varies by context and so it is often parameterized
+//! as a type parameter in this module (`T` in `Type<T>`). In [`FunctionType`], logical variables are
+//! function parameters (`Type<FunctionParamIdx`), and during the actual analysis, logical variables are
+//! program variables bound in the environment (`Type<Var>`, see [`crate::refine::Var`]).
+//! We have [`RefinedTypeVar<T>`] to denote logical variables in refinement predicates, which
+//! accepts existential variables and a variable bound in the refinement type (`x` in `{ x: T | phi
+//! }`) in addition to variables `T` from the outer scope. This module also contains [`Closed`] which is
+//! used to denote a closed type, so `Type<Closed>` ensures no logical variables from the outer scope
+//! appear in that type.
+//!
+//! We have distinct types for each variant of [`Type`], such as [`FunctionType`] and
+//! [`PointerType`]. [`Type`], [`RefinedType`] and these variant types share some common operations:
+//!
+//! - `subst_var`: Substitutes logical variables with logical terms.
+//! - `map_var`: Maps logical variables to other logical variables.
+//! - `free_ty_params`: Collects free type parameters [`TypeParamIdx`] in the type.
+//! - `subst_ty_params`: Substitutes type parameters with other types. Since this replaces
+//!   type parameters with refinement types, [`Type`] does not implement this, and
+//!   [`RefinedType::subst_ty_params`] handles the substitution logic instead.
+//! - `strip_refinement`: Strips the refinements recursively and returns a [`Closed`] type.
+//!
+//! This module also implements several logics for manipulating refinement types and is extensively used in
+//! upstream logic in the [`crate::refine`] and [`crate::analyze`] modules.
+//!
+//! - [`template`]: Generates "template" refinement types with unknown predicates to be inferred.
+//! - [`subtyping`]: Generates CHC constraints [`crate::chc`] from subtyping relations between types.
+//! - [`clause_builder`]: Helper to build [`crate::chc::Clause`] from the refinement types.
+
 use std::collections::{HashMap, HashSet};
 
 use pretty::{termcolor, Pretty};
@@ -19,6 +58,11 @@ mod params;
 pub use params::{TypeParamIdx, TypeParamSubst, TypeParams};
 
 rustc_index::newtype_index! {
+    /// An index representing function parameter.
+    ///
+    /// We manage function parameters using indices that are unique in a function.
+    /// [`FunctionType`] contains `IndexVec<FunctionParamIdx, RefinedType<FunctionParamIdx>>`
+    /// that manages the indices and types of the function parameters.
     #[orderable]
     #[debug_format = "${}"]
     pub struct FunctionParamIdx { }
@@ -39,6 +83,11 @@ where
     }
 }
 
+/// A function type.
+///
+/// In Thrust, function types are closed. Because of that, function types, thus its parameters and
+/// return type only refer to the parameters of the function itself using [`FunctionParamIdx`] and
+/// do not accept other type of variables from the environment.
 #[derive(Debug, Clone)]
 pub struct FunctionType {
     pub params: IndexVec<FunctionParamIdx, RefinedType<FunctionParamIdx>>,
@@ -74,6 +123,8 @@ impl FunctionType {
         }
     }
 
+    /// Because function types are always closed in Thrust, we can convert this into
+    /// [`Type<Closed>`].
     pub fn into_closed_ty(self) -> Type<Closed> {
         Type::Function(self)
     }
@@ -104,6 +155,7 @@ impl FunctionType {
     }
 }
 
+/// The kind of a reference, which is either mutable or immutable.
 #[derive(Debug, Clone, Copy, PartialEq, Eq)]
 pub enum RefKind {
     Mut,
@@ -128,6 +180,7 @@ where
     }
 }
 
+/// The kind of a pointer, which is either a reference or an owned pointer.
 #[derive(Debug, Clone, Copy, PartialEq, Eq)]
 pub enum PointerKind {
     Ref(RefKind),
@@ -167,6 +220,7 @@ impl PointerKind {
     }
 }
 
+/// A pointer type.
 #[derive(Debug, Clone)]
 pub struct PointerType<T> {
     pub kind: PointerKind,
@@ -275,6 +329,11 @@ impl<T> PointerType<T> {
     }
 }
 
+/// A tuple type.
+///
+/// Note that the current implementation uses tuples to represent structs. See
+/// implementation in `crate::refine::template` module for details.
+/// It is our TODO to improve the struct representation.
 #[derive(Debug, Clone)]
 pub struct TupleType<T> {
     pub elems: Vec<RefinedType<T>>,
@@ -374,13 +433,15 @@ impl<T> TupleType<T> {
     }
 }
 
+/// A definition of an enum variant, found in [`EnumDatatypeDef`].
 #[derive(Debug, Clone)]
 pub struct EnumVariantDef {
     pub name: chc::DatatypeSymbol,
     pub discr: u32,
     pub field_tys: Vec<Type<Closed>>,
 }
 
+/// A definition of an enum datatype.
 #[derive(Debug, Clone)]
 pub struct EnumDatatypeDef {
     pub name: chc::DatatypeSymbol,
@@ -394,6 +455,9 @@ impl EnumDatatypeDef {
     }
 }
 
+/// An enum type.
+///
+/// An enum type includes its type arguments and the argument types can refer to outer variables `T`.
 #[derive(Debug, Clone)]
 pub struct EnumType<T> {
     pub symbol: chc::DatatypeSymbol,
@@ -495,6 +559,7 @@ impl<T> EnumType<T> {
     }
 }
 
+/// A type parameter.
 #[derive(Debug, Clone)]
 pub struct ParamType {
     pub idx: TypeParamIdx,
@@ -523,6 +588,7 @@ impl ParamType {
     }
 }
 
+/// An underlying type of a refinement type.
 #[derive(Debug, Clone)]
 pub enum Type<T> {
     Int,
@@ -803,6 +869,10 @@ impl Type<Closed> {
     }
 }
 
+/// A marker type for closed types.
+///
+/// Because the value of `Closed` can never exist, `Type<Closed>` ensures that no
+/// logical variables from outer scope appear in the type.
 #[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Hash)]
 pub enum Closed {}
 
@@ -822,6 +892,11 @@ where
 }
 
 rustc_index::newtype_index! {
+    /// An index representing existential variables.
+    ///
+    /// We manage existential variables using indices that are unique in a [`Formula`].
+    /// [`Formula`] contains `IndexVec<ExistentialVarIdx, chc::Sort>` that manages the indices
+    /// and sorts of the existential variables.
     #[orderable]
     #[debug_format = "e{}"]
     pub struct ExistentialVarIdx { }
@@ -846,6 +921,15 @@ pub trait ShiftExistential {
     fn shift_existential(self, offset: usize) -> Self;
 }
 
+/// A logical variable in a refinement predicate.
+///
+/// Given a refinement type `{ v: T | ∃e. φ }`, there are three cases of logical variables
+/// occurring in the predicate `φ`:
+///
+/// - `RefinedTypeVar::Value`: a variable `v` representing the value of the type
+/// - `RefinedTypeVar::Existential`: an existential variable `e`
+/// - `RefinedTypeVar::Free`: a variable from the outer scope, such as function parameters or
+///    variables bound in the environment
 #[derive(Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Hash)]
 pub enum RefinedTypeVar<FV> {
     Value,
@@ -908,6 +992,9 @@ impl<T> ShiftExistential for RefinedTypeVar<T> {
     }
 }
 
+/// A formula, potentially equipped with an existential quantifier.
+///
+/// Note: This is not to be confused with [`crate::chc::Formula`] in the [`crate::chc`] module, which is a different notion.
 #[derive(Debug, Clone)]
 pub struct Formula<V> {
     pub existentials: IndexVec<ExistentialVarIdx, chc::Sort>,
@@ -1051,6 +1138,10 @@ where
     }
 }
 
+/// A refinement predicate in a refinement type.
+///
+/// This is a [`Formula`], but gives an explicit representation of the kinds of variables that can appear in
+/// the refinement predicates. See [`RefinedTypeVar`] for details.
 pub type Refinement<FV = Closed> = Formula<RefinedTypeVar<FV>>;
 
 impl<FV> Refinement<FV> {
@@ -1105,6 +1196,10 @@ impl<FV> Refinement<FV> {
     }
 }
 
+/// A helper type to map logical variables in a refinement at once.
+///
+/// This is essentially just calling `Refinement::map_var`, but provides a convenient interface to
+/// construct the mapping of the variables.
 #[derive(Debug, Clone)]
 pub struct Instantiator<T> {
     value_var: Option<T>,
@@ -1140,6 +1235,7 @@ impl<T> Instantiator<T> {
     }
 }
 
+/// A refinement type.
 #[derive(Debug, Clone)]
 pub struct RefinedType<FV = Closed> {
     pub ty: Type<FV>,

src/rty/clause_builder.rs

@@ -1,7 +1,19 @@
+//! Helpers to build [`crate::chc::Clause`] from the refinement types.
+//!
+//! This module provides an extension trait named [`ClauseBuilderExt`] for [`chc::ClauseBuilder`]
+//! that allows it to work with refinement types. It provides a convenient way to generate CHC clauses from
+//! [`Refinement`]s by handling the mapping of [`super::RefinedTypeVar`] to [`chc::TermVarIdx`].
+//! This is primarily used to generate clauses from [`super::subtyping`] constraints between refinement types.
+
 use crate::chc;
 
 use super::{Refinement, Type};
 
+/// An extension trait for [`chc::ClauseBuilder`] to work with refinement types.
+///
+/// We implement a custom logic to deal with [`Refinement`]s in [`RefinementClauseBuilder`],
+/// and this extension trait provides methods to create [`RefinementClauseBuilder`]s while
+/// specifying how to handle [`super::RefinedTypeVar::Value`] during the instantiation.
 pub trait ClauseBuilderExt {
     fn with_value_var<'a, T>(&'a mut self, ty: &Type<T>) -> RefinementClauseBuilder<'a>;
     fn with_mapped_value_var<T>(&mut self, v: T) -> RefinementClauseBuilder<'_>
@@ -31,6 +43,10 @@ impl ClauseBuilderExt for chc::ClauseBuilder {
     }
 }
 
+/// A builder for a CHC clause with a refinement.
+///
+/// You can supply [`Refinement`]s as the body and head of the clause directly, and this builder
+/// will take care of mapping the variables appropriately.
 pub struct RefinementClauseBuilder<'a> {
     builder: &'a mut chc::ClauseBuilder,
     value_var: Option<chc::TermVarIdx>,