diff --git a/src/analyze.rs b/src/analyze.rs index 9913f26a..898df5b7 100644 --- a/src/analyze.rs +++ b/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; diff --git a/src/analyze/annot.rs b/src/analyze/annot.rs index 7d23cfe4..91dd2099 100644 --- a/src/analyze/annot.rs +++ b/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, @@ -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, diff --git a/src/analyze/crate_.rs b/src/analyze/crate_.rs index 016c7095..9a1fa675 100644 --- a/src/analyze/crate_.rs +++ b/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>, diff --git a/src/analyze/did_cache.rs b/src/analyze/did_cache.rs index d671f8a9..efeea6be 100644 --- a/src/analyze/did_cache.rs +++ b/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>, } +/// 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>, diff --git a/src/analyze/local_def.rs b/src/analyze/local_def.rs index b1df237e..ef5870e2 100644 --- a/src/analyze/local_def.rs +++ b/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>, diff --git a/src/refine.rs b/src/refine.rs index 60f29f4e..0371da19 100644 --- a/src/refine.rs +++ b/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}; diff --git a/src/refine/basic_block.rs b/src/refine/basic_block.rs index 57e99306..ac39a1ce 100644 --- a/src/refine/basic_block.rs +++ b/src/refine/basic_block.rs @@ -1,3 +1,5 @@ +//! The refinement type for a basic block. + use pretty::{termcolor, Pretty}; use rustc_index::IndexVec; use rustc_middle::mir::Local; @@ -5,8 +7,11 @@ 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 diff --git a/src/rty.rs b/src/rty.rs index c8e6e9e1..72fede82 100644 --- a/src/rty.rs +++ b/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 { 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`). In [`FunctionType`], logical variables are +//! function parameters (`Type`, see [`crate::refine::Var`]). +//! We have [`RefinedTypeVar`] 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` 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>` + /// 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>, @@ -74,6 +123,8 @@ impl FunctionType { } } + /// Because function types are always closed in Thrust, we can convert this into + /// [`Type`]. pub fn into_closed_ty(self) -> Type { 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 { pub kind: PointerKind, @@ -275,6 +329,11 @@ impl PointerType { } } +/// 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 { pub elems: Vec>, @@ -374,6 +433,7 @@ impl TupleType { } } +/// A definition of an enum variant, found in [`EnumDatatypeDef`]. #[derive(Debug, Clone)] pub struct EnumVariantDef { pub name: chc::DatatypeSymbol, @@ -381,6 +441,7 @@ pub struct EnumVariantDef { pub field_tys: Vec>, } +/// 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 { pub symbol: chc::DatatypeSymbol, @@ -495,6 +559,7 @@ impl EnumType { } } +/// 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 { Int, @@ -803,6 +869,10 @@ impl Type { } } +/// A marker type for closed types. +/// +/// Because the value of `Closed` can never exist, `Type` 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` 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 { Value, @@ -908,6 +992,9 @@ impl ShiftExistential for RefinedTypeVar { } } +/// 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 { pub existentials: IndexVec, @@ -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 = Formula>; impl Refinement { @@ -1105,6 +1196,10 @@ impl Refinement { } } +/// 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 { value_var: Option, @@ -1140,6 +1235,7 @@ impl Instantiator { } } +/// A refinement type. #[derive(Debug, Clone)] pub struct RefinedType { pub ty: Type, diff --git a/src/rty/clause_builder.rs b/src/rty/clause_builder.rs index f45e948a..ce3c54f4 100644 --- a/src/rty/clause_builder.rs +++ b/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) -> RefinementClauseBuilder<'a>; fn with_mapped_value_var(&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, diff --git a/src/rty/params.rs b/src/rty/params.rs index 26bd2893..17ebc2b3 100644 --- a/src/rty/params.rs +++ b/src/rty/params.rs @@ -1,3 +1,5 @@ +//! Data structures for type parameters and substitutions. + use std::collections::BTreeMap; use pretty::{termcolor, Pretty}; @@ -8,6 +10,7 @@ use crate::chc; use super::{Closed, RefinedType}; rustc_index::newtype_index! { + /// An index representing a type parameter. #[orderable] #[debug_format = "T{}"] pub struct TypeParamIdx { } @@ -38,6 +41,7 @@ impl TypeParamIdx { pub type TypeParams = IndexVec>; +/// A substitution for type parameters that maps type parameters to refinement types. #[derive(Debug, Clone)] pub struct TypeParamSubst { subst: BTreeMap>, diff --git a/src/rty/subtyping.rs b/src/rty/subtyping.rs index df3d4463..82465a88 100644 --- a/src/rty/subtyping.rs +++ b/src/rty/subtyping.rs @@ -1,8 +1,17 @@ +//! Translation of subtyping relations into CHC constraints. + use crate::chc; use crate::pretty::PrettyDisplayExt; use super::{ClauseBuilderExt as _, Closed, PointerKind, RefKind, RefinedType, Type}; +/// A scope for building clauses. +/// +/// The construction of CHC clauses requires knowledge of the current +/// environment to determine variable sorts and include necessary premises. +/// This trait abstracts the preparation of a [`chc::ClauseBuilder`] to allow an +/// environment defined outside of this module (in Thrust, [`crate::refine::Env`]) +/// to build a [`chc::ClauseBuilder`] equipped with in-scope variables and assumptions. pub trait ClauseScope { fn build_clause(&self) -> chc::ClauseBuilder; } @@ -22,6 +31,7 @@ impl ClauseScope for chc::ClauseBuilder { } } +/// Produces CHC constraints for subtyping relations. pub trait Subtyping { #[must_use] fn relate_sub_type( diff --git a/src/rty/template.rs b/src/rty/template.rs index f2f1112e..3d758201 100644 --- a/src/rty/template.rs +++ b/src/rty/template.rs @@ -1,9 +1,22 @@ +//! "Template" refinement types with unknown predicates to be inferred. +//! +//! A [`Template`] is used to generate a [`RefinedType`] with a refinement consisting of a +//! single atom with a fresh predicate variable. The unknown predicate can carry dependencies, +//! which are the arguments to the predicate. When Thrust infers refinement types, it +//! first generates template refinement types with unknown refinements, and then +//! generates constraints on the predicate variables in these templates. + use std::collections::BTreeMap; use crate::chc; use super::{RefinedType, RefinedTypeVar, Type}; +/// A template of a refinement type. +/// +/// This is a refinement type in the form of `{ T | P(x1, ..., xn) }` where `P` is a +/// predicate variable, `T` is a type, and `x1, ..., xn` are the dependencies. The predicate +/// variable is actually allocated when [`Template::into_refined_type`] is called. #[derive(Debug, Clone)] pub struct Template { pred_sig: chc::PredSig, @@ -24,6 +37,11 @@ impl Template { } } +/// A builder for a [`Template`]. +/// +/// Note that we have a convenient mechanism in the [`crate::refine`] module +/// to prepare a [`TemplateBuilder`] with variables in scope, and we usually don't +/// construct a [`TemplateBuilder`] directly. #[derive(Debug, Clone)] pub struct TemplateBuilder { dependencies: BTreeMap, chc::Sort>,