diff --git a/src/analyze.rs b/src/analyze.rs index fce97595..ed544293 100644 --- a/src/analyze.rs +++ b/src/analyze.rs @@ -188,7 +188,18 @@ enum DefTy<'tcx> { #[derive(Debug, Clone)] struct BasicBlockDef { ty: BasicBlockType, - has_precondition: bool, + precondition: BasicBlockPrecondition, +} + +/// How a basic block comes by its precondition. +#[derive(Debug, Clone)] +enum BasicBlockPrecondition { + /// Already installed, be it from an annotation, the signature of the function, or a predicate + /// variable left to be inferred. + Installed, + /// The disjunction of the states its predecessors leave, collected as they are analyzed and + /// installed once they all have been. + Inherited(Vec>), } #[derive(Debug, Clone, Default)] @@ -553,7 +564,7 @@ impl<'tcx> Analyzer<'tcx> { bb, BasicBlockDef { ty: rty, - has_precondition: true, + precondition: BasicBlockPrecondition::Installed, }, ); } @@ -569,7 +580,7 @@ impl<'tcx> Analyzer<'tcx> { bb, BasicBlockDef { ty: rty, - has_precondition: false, + precondition: BasicBlockPrecondition::Inherited(Vec::new()), }, ); } @@ -579,30 +590,89 @@ impl<'tcx> Analyzer<'tcx> { def_id = ?def_id, ?bb, rty = %def.ty.display(), - has_precondition = def.has_precondition, "register_basic_block_def", ); self.basic_blocks.entry(def_id).or_default().insert(bb, def); } - pub fn register_basic_block_precondition( + /// Records the state a predecessor leaves as one of the states the block is entered in. + pub fn push_basic_block_precondition( &mut self, def_id: LocalDefId, bb: BasicBlock, precondition: rty::Refinement, ) { - let bb_def = &mut self - .basic_blocks + let bb_def = self.basic_block_def_mut(def_id, bb); + match &mut bb_def.precondition { + BasicBlockPrecondition::Inherited(states) => states.push(precondition), + BasicBlockPrecondition::Installed => { + panic!("precondition of {bb:?} is already installed") + } + } + } + + /// Installs the precondition of a block that inherits it, once every predecessor has been + /// analyzed. + /// + /// The states its predecessors leave are the states it is entered in, so their disjunction is + /// its precondition. A disjunction is no conjunct of a Horn clause body, so when a predicate + /// variable appears in one of the states, the disjunction has to be named by a predicate + /// variable of its own, bounded from below by every state. + pub fn install_inherited_basic_block_precondition( + &mut self, + def_id: LocalDefId, + bb: BasicBlock, + ) { + let bb_def = self.basic_block_def_mut(def_id, bb); + let states = + match std::mem::replace(&mut bb_def.precondition, BasicBlockPrecondition::Installed) { + BasicBlockPrecondition::Inherited(states) => states, + BasicBlockPrecondition::Installed => return, + }; + let ty = bb_def.ty.clone(); + + let precondition = match rty::Refinement::disjunction(states.iter().cloned()) { + Some(disjunction) => disjunction, + None => { + let template = self.precondition_template(&ty); + for state in states { + let clauses = + rty::relate_sub_precondition(&ty.as_ref().params, state, template.clone()); + self.extend_clauses(clauses); + } + template + } + }; + self.basic_block_def_mut(def_id, bb) + .ty + .set_precondition(precondition); + } + + /// A predicate variable standing for the precondition of a basic block, over its parameters. + fn precondition_template( + &mut self, + ty: &BasicBlockType, + ) -> rty::Refinement { + use crate::refine::TemplateRegistry as _; + + let params = &ty.as_ref().params; + let last_param_idx = params.last_index().expect("basic block has a parameter"); + let mut builder = rty::TemplateBuilder::default(); + for (param_idx, param) in params.iter_enumerated() { + if param_idx != last_param_idx { + builder.add_dependency(param_idx, param.ty.to_sort()); + } + } + let template = builder.build(params[last_param_idx].ty.clone()); + self.register_template(template).refinement + } + + fn basic_block_def_mut(&mut self, def_id: LocalDefId, bb: BasicBlock) -> &mut BasicBlockDef { + self.basic_blocks .get_mut(&def_id) .unwrap() .get_mut(&bb) - .unwrap(); - assert!( - !bb_def.has_precondition, - "precondition is already registered for basic block" - ); - bb_def.has_precondition = true; - bb_def.ty.set_precondition(precondition); + .unwrap() } pub fn basic_block_ty(&self, def_id: LocalDefId, bb: BasicBlock) -> &BasicBlockType { @@ -616,7 +686,7 @@ impl<'tcx> Analyzer<'tcx> { ) -> &BasicBlockType { let def = &self.basic_blocks[&def_id][&bb]; assert!( - def.has_precondition, + matches!(def.precondition, BasicBlockPrecondition::Installed), "basic block does not have precondition" ); &def.ty diff --git a/src/analyze/basic_block.rs b/src/analyze/basic_block.rs index 4ed04196..50329bdc 100644 --- a/src/analyze/basic_block.rs +++ b/src/analyze/basic_block.rs @@ -11,7 +11,7 @@ use rustc_span::def_id::{DefId, LocalDefId}; use crate::analyze; use crate::chc; -use crate::pretty::PrettyDisplayExt as _; +use crate::pretty::{PrettyDisplayExt as _, PrettySliceExt as _}; use crate::refine::{ Assumption, BasicBlockType, BasicBlockTypeParamKind, PlaceType, PlaceTypeBuilder, PlaceTypeVar, TempVarIdx, TypeBuilder, Var, @@ -24,29 +24,116 @@ mod drop_point; mod visitor; pub use drop_point::DropPoints; -/// Whether a basic block needs a precondition of its own, rather than -/// inheriting its predecessor's outgoing env state. +/// Whether `bb` is a loop header, i.e. it is reached by an edge that closes a cycle. /// -/// This holds for `START_BLOCK` (whose precondition comes from the function -/// signature, not a predecessor) and for every block reached by more than one -/// CFG edge — i.e. join points with multiple predecessors, or multiple edges -/// from a single predecessor (e.g. `SwitchInt` arms that share a target). +/// Basic blocks are analyzed in reverse postorder, under which every predecessor of a block comes +/// before it unless the edge back to it closes a cycle. A block reached only from blocks analyzed +/// before it inherits the states they leave as its precondition; a loop header cannot, as the +/// state carried around the loop is not yet known when it is analyzed, and has to be inferred. /// -/// A block with a unique incoming edge can inherit that edge's env state, so it -/// needs no precondition of its own. A block that does need one currently models -/// it with a fresh predicate variable; this is also the set of CFG cutpoints, so -/// it cuts every cycle (a loop header always has in-degree >= 2). -pub fn needs_own_precondition(body: &Body<'_>, bb: BasicBlock) -> bool { - if bb == mir::START_BLOCK { - return true; +/// These blocks are the cutpoints of the CFG, so a precondition inferred here cuts every cycle. +pub fn is_loop_header(body: &Body<'_>, bb: BasicBlock) -> bool { + let doms = body.basic_blocks.dominators(); + body.basic_blocks.predecessors()[bb] + .iter() + .any(|&pred| doms.dominates(bb, pred)) +} + +/// Adapts the actual arguments of a call to the parameter list of the callee's function type. +/// +/// A function type carries its precondition on its last parameter, so it has one even when the +/// function takes no argument (see `refine::FunctionTemplateTypeBuilder::build`); a call with no +/// argument passes a unit value for it. Under the `rust-call` ABI the caller passes the arguments +/// after the receiver as a single tuple, while the parameter list spells them out one by one: +/// +/// ```text +/// &Closure, ((own i32)[<0>], (own bool)[])[t] +/// => +/// &Closure, i32[0], bool[false] +/// ``` +fn adapt_args_to_abi( + mut args: Vec, + abi: rty::FunctionAbi, +) -> IndexVec { + match abi { + rty::FunctionAbi::Rust => { + if args.is_empty() { + args.push(PlaceType::with_ty_and_term( + rty::Type::unit(), + chc::Term::tuple(Vec::new()), + )); + } + } + rty::FunctionAbi::RustCall => { + let tupled = args.pop().expect("rust-call last arg"); + let elems = tupled + .ty + .as_tuple() + .expect("rust-call last arg is tuple") + .elems + .len(); + for idx in 0..elems { + // elaboration: all tuple elements are boxed + args.push(tupled.clone().tuple_proj(idx).deref()); + } + + tracing::info!(args = %args.pretty_slice().display(), "rust-call expanded"); + } } - let preds = &body.basic_blocks.predecessors()[bb]; - if preds.len() != 1 { - return true; + args.into_iter().collect() +} + +/// The refined type of a value described by a [`PlaceType`]. +/// +/// A value of a singleton sort is the only value of its sort, and its refinement is dropped so +/// that it is not stated in terms of the variable holding it (see `refine::Env::var_type`). +fn refined_type(pty: PlaceType) -> rty::RefinedType { + // TODO: should we cover "is_singleton" ness in relate_* methods or here? + if pty.ty.to_sort().is_singleton() { + return rty::RefinedType::unrefined(pty.ty); } - let pred = preds[0]; - let pred_term = body.basic_blocks[pred].terminator(); - pred_term.successors().filter(|s| *s == bb).count() > 1 + pty.into() +} + +/// The type of the value a call gives, which is the callee's return type with each parameter +/// replaced by the argument passed for it. +/// +/// The arguments are values of the environment, described by [`PlaceType`]s, and the existential +/// variables they are stated in terms of are taken over by the refinement of the result. An +/// argument stated that way cannot reach a refinement nested in the return type, which has an +/// existential scope of its own. +fn instantiate_return_type( + ret: rty::RefinedType, + args: IndexVec, +) -> rty::RefinedType { + let mut arg_builder = PlaceTypeBuilder::default(); + let arg_terms: IndexVec = args + .into_iter() + .map(|arg| arg_builder.subsume(arg).1) + .collect(); + let rty::RefinedType { ty, refinement } = + ret.subst_var(|param_idx| arg_terms[param_idx].clone()); + + let ty = ty.map_var(|v| { + v.into_var() + .unwrap_or_else(|| unimplemented!("argument of a dependent return type: {:?}", v)) + }); + let rty::Formula { + mut existentials, + body: arg_body, + } = arg_builder.build_assumption(); + let arg_existentials = existentials.len(); + existentials.extend(refinement.existentials); + + let mut body = arg_body.map_var(Into::into); + body.push_conj(refinement.body.map_var(|v| match v { + rty::RefinedTypeVar::Value => rty::RefinedTypeVar::Value, + rty::RefinedTypeVar::Free(v) => v.into(), + rty::RefinedTypeVar::Existential(ev) => { + rty::RefinedTypeVar::Existential(ev + arg_existentials) + } + })); + rty::RefinedType::new(ty, rty::Refinement::new(existentials, body)) } /// Converts the current env state into a `Refinement` to be @@ -191,106 +278,23 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { } } - // this can't be implmeneted in relate_sub_type because rty::FunctionType is free from Var - fn relate_fn_sub_type( - &mut self, - got: rty::FunctionType, - expected_args: IndexVec>, - expected_ret: rty::RefinedType, - ) -> Vec { - let mut clauses = Vec::new(); - - tracing::debug!( - got = %got.display(), - expected = %crate::pretty::FunctionType::new(&expected_args, &expected_ret).display(), - "fn_sub_type" - ); - - let mut builder = self.env.build_clause(); - let cs = self.relate_fn_param_sub_types_with_builder( - got.params, - expected_args, - &mut builder, - got.abi, - ); - clauses.extend(cs); - - let cs = builder - .with_value_var(&got.ret.ty) - .add_body(got.ret.refinement) - .head(expected_ret.refinement); - clauses.extend(cs); - - clauses.extend(builder.relate_sub_type(&got.ret.ty, &expected_ret.ty)); - clauses - } - fn relate_fn_param_sub_types( &mut self, got_args: IndexVec>, expected_args: IndexVec>, ) -> Vec { let mut builder = self.env.build_clause(); - self.relate_fn_param_sub_types_with_builder( - got_args, - expected_args, - &mut builder, - rty::FunctionAbi::Rust, - ) + self.relate_fn_param_sub_types_with_builder(got_args, expected_args, &mut builder) } fn relate_fn_param_sub_types_with_builder( &mut self, got_args: IndexVec>, - mut expected_args: IndexVec>, + expected_args: IndexVec>, builder: &mut chc::ClauseBuilder, - abi: rty::FunctionAbi, ) -> Vec { let mut clauses = Vec::new(); - match abi { - rty::FunctionAbi::Rust => { - if expected_args.is_empty() { - // elaboration: we need at least one predicate variable in parameter (see mir_function_ty_impl) - expected_args.push(rty::RefinedType::unrefined(rty::Type::unit()).vacuous()); - } - } - rty::FunctionAbi::RustCall => { - // &Closure, { v: (own i32, own bool) | v = (<0>, ) } - // => - // &Closure, { v: i32 | (, _) = (<0>, ) }, { v: bool | (_, ) = (<0>, ) } - - let rty::RefinedType { ty, mut refinement } = - expected_args.pop().expect("rust-call last arg"); - let ty = ty.into_tuple().expect("rust-call last arg is tuple"); - let mut replacement_tuple = Vec::new(); // will be (, _) or (_, ) - for elem in &ty.elems { - let existential = refinement.existentials.push(elem.ty.to_sort()); - replacement_tuple.push(chc::Term::var(rty::RefinedTypeVar::Existential( - existential, - ))); - } - - for (i, elem) in ty.elems.into_iter().enumerate() { - // all tuple elements are boxed during the translation to rty::Type - let mut param_ty = elem.deref(); - param_ty - .refinement - .push_conj(refinement.clone().subst_value_var(|| { - let mut value_elems = replacement_tuple.clone(); - value_elems[i] = chc::Term::var(rty::RefinedTypeVar::Value).boxed(); - chc::Term::tuple(value_elems) - })); - expected_args.push(param_ty); - } - - tracing::info!( - expected = %crate::pretty::FunctionParams::new(&expected_args).display(), - "rust-call expanded", - ); - } - } - assert!(got_args.len() == expected_args.len()); // TODO: check stys are equal for (param_idx, param_rty) in got_args.iter_enumerated() { @@ -688,14 +692,7 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { } fn rvalue_refined_type(&mut self, rvalue: Rvalue<'tcx>) -> rty::RefinedType { - let ty = self.rvalue_type(rvalue); - - // TODO: should we cover "is_singleton" ness in relate_* methods or here? - if !ty.ty.to_sort().is_singleton() { - return ty.into(); - } - - rty::RefinedType::unrefined(ty.ty) + refined_type(self.rvalue_type(rvalue)) } fn type_rvalue(&mut self, rvalue: Rvalue<'tcx>, expected: &rty::RefinedType) { @@ -748,8 +745,8 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { bb: BasicBlock, outer_fn_param_vars: &HashMap, ) { - if !needs_own_precondition(&self.body, bb) { - self.install_inherited_bb_ty(bb, outer_fn_param_vars); + if !is_loop_header(&self.body, bb) { + self.push_inherited_precondition(bb, outer_fn_param_vars); return; } let bty = self.basic_block_ty_with_precondition(bb); @@ -786,10 +783,9 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { self.ctx.extend_clauses(clauses); } - /// Materializes the `BasicBlockType` for a target that inherits its - /// precondition by building its (pvar-free) layout and overwriting the last - /// param's refinement with the current env state. - fn install_inherited_bb_ty( + /// Records the env state this block leaves as one of the states `bb` is entered in, which its + /// precondition is the disjunction of. + fn push_inherited_precondition( &mut self, bb: BasicBlock, outer_fn_param_vars: &HashMap, @@ -818,7 +814,7 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { let precondition = capture.finish(&self.env); self.ctx - .register_basic_block_precondition(self.local_def_id, bb, precondition); + .push_basic_block_precondition(self.local_def_id, bb, precondition); } fn with_assumptions(&mut self, assumptions: Vec>, callback: F) -> T @@ -946,7 +942,13 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { def_ty.ty } - fn type_call(&mut self, func: Operand<'tcx>, args: I, expected_ret: &rty::RefinedType) + /// Checks a call against the callee's type and gives the type of its result. + /// + /// The arguments are checked against the parameters of the callee, and the result is the + /// return type of the callee instantiated at those arguments. Naming the result with a + /// predicate variable instead would leave its refinement to be inferred, while the callee + /// already states everything that is known about it. + fn type_call(&mut self, func: Operand<'tcx>, args: I) -> rty::RefinedType where I: IntoIterator>, { @@ -956,16 +958,26 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { } else { self.operand_type(func.clone()).ty }; - let expected_args: IndexVec<_, _> = args - .into_iter() - .map(|op| self.operand_refined_type(op)) - .collect(); - if let rty::Type::Function(func_ty) = func_ty { - let clauses = self.relate_fn_sub_type(func_ty, expected_args, expected_ret.clone()); - self.ctx.extend_clauses(clauses); - } else { + let rty::Type::Function(func_ty) = func_ty else { panic!("unexpected def type: {:?}", func_ty); - } + }; + let args = adapt_args_to_abi( + args.into_iter().map(|op| self.operand_type(op)).collect(), + func_ty.abi, + ); + tracing::debug!( + callee = %func_ty.display(), + args = %args.pretty_slice().display(), + "call" + ); + + let arg_rtys = args.iter().cloned().map(refined_type).collect(); + let mut builder = self.env.build_clause(); + let clauses = + self.relate_fn_param_sub_types_with_builder(func_ty.params, arg_rtys, &mut builder); + self.ctx.extend_clauses(clauses); + + instantiate_return_type(*func_ty.ret, args) } fn elaborate_place(&self, place: &mir::Place<'tcx>) -> mir::Place<'tcx> { @@ -1103,13 +1115,7 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { } else { operand.clone() }; - let decl = self.local_decls[lhs.local].clone(); - let rty = self - .type_builder - .for_template(&mut self.ctx) - .with_scope(&self.env) - .build_refined(decl.ty); - self.type_call(func, [operand], &rty); + let rty = self.type_call(func, [operand]); self.bind_local(lhs.local, rty); return; } @@ -1222,17 +1228,7 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { unimplemented!() } - let decl = self.local_decls[destination].clone(); - let rty = self - .type_builder - .for_template(&mut self.ctx) - .with_scope(&self.env) - .build_refined(decl.ty); - self.type_call( - func.clone(), - args.clone().iter().map(|a| a.node.clone()), - &rty, - ); + let rty = self.type_call(func.clone(), args.iter().map(|a| a.node.clone())); self.bind_local(destination, rty); } } diff --git a/src/analyze/local_def.rs b/src/analyze/local_def.rs index 68b0d646..7f5d476f 100644 --- a/src/analyze/local_def.rs +++ b/src/analyze/local_def.rs @@ -9,7 +9,6 @@ use rustc_span::def_id::{DefId, LocalDefId}; use crate::analyze; use crate::chc; -use crate::pretty::PrettyDisplayExt as _; use crate::refine::{self, BasicBlockType, TypeBuilder}; use crate::rty; @@ -745,16 +744,12 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { } /// Walks up the dominator tree from the marker block to the innermost - /// enclosing loop header: the first dominator that needs its own - /// precondition (in-degree >= 2) and has a back edge. + /// enclosing loop header. fn loop_header_of(body: &Body<'_>, marker_bb: BasicBlock) -> Option { let doms = body.basic_blocks.dominators(); - let preds = body.basic_blocks.predecessors(); let mut cur = Some(marker_bb); while let Some(bb) = cur { - if analyze::basic_block::needs_own_precondition(body, bb) - && preds[bb].iter().any(|&p| doms.dominates(bb, p)) - { + if analyze::basic_block::is_loop_header(body, bb) { return Some(bb); } cur = doms.immediate_dominator(bb); @@ -889,7 +884,73 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { .into() } - fn refine_basic_blocks(&mut self) { + /// The precondition of the entry block, which is the precondition of the function itself. + /// + /// The entry block takes each parameter of the function twice: as the local that holds it and + /// as the value it has on entry ([`refine::BasicBlockTypeParamKind::OuterFnParam`]), which the + /// postcondition of the function is stated in terms of. Both denote the argument, so the + /// precondition equates them along with carrying the refinement of every parameter. + fn entry_precondition( + &self, + expected: &rty::FunctionType, + bty: &BasicBlockType, + ) -> rty::Refinement { + // The value of a parameter of the function among the parameters of the entry block. One of + // a singleton sort is denoted by its only value, as it is no variable of the constraints + // (see `refine::Env::var_type`), and so is the synthetic parameter that a function without + // one carries its precondition on, which has no local in the entry block. + let param_term = |idx: rty::FunctionParamIdx| { + let sort = expected.params[idx].ty.to_sort(); + match bty.param_of_local(analyze::local_of_function_param(idx)) { + Some(param_idx) if !sort.is_singleton() => { + chc::Term::var(rty::RefinedTypeVar::Free(param_idx)) + } + _ => chc::Term::default_for(&sort), + } + }; + + let mut precondition = rty::Refinement::top(); + for (idx, param) in expected.params.iter_enumerated() { + precondition.push_conj(param.refinement.clone().subst_var(|v| match v { + rty::RefinedTypeVar::Value => param_term(idx), + rty::RefinedTypeVar::Free(free_idx) => param_term(free_idx), + rty::RefinedTypeVar::Existential(ev) => { + chc::Term::var(rty::RefinedTypeVar::Existential(ev)) + } + })); + + if let Some(outer_param_idx) = bty.param_of_outer_fn_param(idx) { + precondition.push_conj( + chc::Term::var(rty::RefinedTypeVar::Free(outer_param_idx)) + .equal_to(param_term(idx)) + .into(), + ); + } + } + precondition + } + + /// The type of the entry block, which takes the arguments of the call under the precondition + /// of the function, leaving nothing about its state to be inferred. + fn entry_block_ty( + &self, + expected: &rty::RefinedType, + live_locals: Vec<(Local, TypeAndMut<'tcx>)>, + ret_ty: mir_ty::Ty<'tcx>, + ) -> BasicBlockType { + let mut expected_fn = expected.ty.as_function().cloned().unwrap(); + self.elaborate_mut_params(&mut expected_fn); + + let mut bty = self + .type_builder + .build_basic_block(&self.body, live_locals, ret_ty); + bty.install_signature_types(&expected_fn.params); + let precondition = self.entry_precondition(&expected_fn, &bty); + bty.set_precondition(precondition); + bty + } + + fn refine_basic_blocks(&mut self, expected: &rty::RefinedType) { use rustc_mir_dataflow::Analysis as _; let loop_invariants = self.collect_loop_invariant_annotations(); let mut results = rustc_mir_dataflow::impls::MaybeLiveLocals @@ -952,7 +1013,11 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { bty.set_precondition(inv); self.ctx .register_basic_block_ty_with_precondition(self.local_def_id, bb, bty); - } else if analyze::basic_block::needs_own_precondition(&self.body, bb) { + } else if bb == mir::START_BLOCK { + let bty = self.entry_block_ty(expected, live_locals, ret_ty); + self.ctx + .register_basic_block_ty_with_precondition(self.local_def_id, bb, bty); + } else if analyze::basic_block::is_loop_header(&self.body, bb) { let bty = self .type_builder .for_template(&mut self.ctx) @@ -960,9 +1025,8 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { self.ctx .register_basic_block_ty_with_precondition(self.local_def_id, bb, bty); } else { - // The block inherits its predecessor's outgoing env state as its - // precondition, materialized lazily during the predecessor's - // analysis. Record only unrefined type here. + // The block inherits the states its predecessors leave as its precondition, + // which is only known once they have all been analyzed. Record the type alone. let bty = self .type_builder .build_basic_block(&self.body, live_locals, ret_ty); @@ -974,12 +1038,14 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { fn analyze_basic_blocks(&mut self, expected_fn_ty: &rty::RefinedType) { let expected_fn_ty = expected_fn_ty.ty.as_function().unwrap(); - // Reverse postorder guarantees each block that inherits its precondition - // is visited after the predecessor that lazily materialized its type. + // Reverse postorder guarantees each block that inherits its precondition is visited + // after every predecessor that leaves a state for it. for (bb, data) in mir::traversal::reverse_postorder(&self.body) { if data.is_cleanup { continue; } + self.ctx + .install_inherited_basic_block_precondition(self.local_def_id, bb); let rty = self .ctx .basic_block_ty_with_precondition(self.local_def_id, bb) @@ -1034,79 +1100,6 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { } }); } - - /// Drop excessive parameters from the BB-side entry function type that do not - /// correspond to any function argument. These are introduced by ZST locals whose - /// liveness analysis treats them as live without an explicit def. - fn drop_bb_zst_params(&self, bb_ty: &BasicBlockType) -> rty::FunctionType { - let mut fn_ty = bb_ty.to_function_ty(); - let arg_locals: HashSet<_> = self.body.args_iter().collect(); - - for idx in bb_ty.local_params().rev() { - let local = bb_ty.local_of_param(idx).unwrap(); - if !arg_locals.contains(&local) { - fn_ty.remove_param(idx); - } - } - - // A function type must keep at least one parameter to host the precondition - // predicate. When the function has no real argument, both the expected type and - // the BB type carry a synthetic unit parameter (see - // `crate::refine::TypeBuilder::build_basic_block`). That synthetic has no - // backing local, so it survives the drop loop untouched. If instead the entry - // block exposed only ZST-local parameters (e.g. `RETURN_PLACE`), dropping them - // empties the type, and we re-introduce the synthetic unit parameter carrying - // the precondition refinement of the last dropped parameter. - if self.body.arg_count == 0 && fn_ty.params.is_empty() { - let refinement = bb_ty.as_ref().last_param().unwrap().refinement.clone(); - fn_ty - .params - .push(rty::RefinedType::new(rty::Type::unit(), refinement)); - } - - fn_ty - } - - /// Drop function parameters from `expected_ty` whose corresponding local is unused - /// (and thus not represented) in the BB-side entry function type. - fn drop_unused_expected_params( - &self, - expected_ty: &mut rty::FunctionType, - bb_ty: &BasicBlockType, - ) { - if self.body.arg_count == 0 { - return; - } - let arg_locals: HashSet<_> = self.body.args_iter().collect(); - let present_arg_locals: HashSet<_> = bb_ty - .locals() - .filter(|local| arg_locals.contains(local)) - .collect(); - for idx in expected_ty.params.indices().rev() { - let arg_local = analyze::local_of_function_param(idx); - if !present_arg_locals.contains(&arg_local) { - expected_ty.remove_param(idx); - } - } - } - - fn assert_entry(&mut self, expected: &rty::RefinedType) { - let mut entry_ty = self - .ctx - .basic_block_ty_with_precondition(self.local_def_id, mir::START_BLOCK) - .clone(); - tracing::debug!(expected = %expected.display(), entry = %entry_ty.display(), "assert_entry before"); - let mut expected = expected.ty.as_function().cloned().unwrap(); - self.elaborate_mut_params(&mut expected); - - entry_ty.truncate_outer_fn_params(); - self.drop_unused_expected_params(&mut expected, &entry_ty); - let entry_ty = self.drop_bb_zst_params(&entry_ty); - - tracing::debug!(expected = %expected.display(), entry = %entry_ty.display(), "assert_entry after"); - let clauses = rty::relate_sub_param_types(&entry_ty.params, &expected.params); - self.ctx.extend_clauses(clauses); - } } impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { @@ -1145,8 +1138,8 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { self.unelaborate_derefs(); analyze::reconstruct_slice_indexing::reconstruct(self.tcx, &mut self.body); self.reassign_local_mutabilities(); - self.refine_basic_blocks(); + + self.refine_basic_blocks(expected); self.analyze_basic_blocks(expected); - self.assert_entry(expected); } } diff --git a/src/chc.rs b/src/chc.rs index b70112c0..e145f7fd 100644 --- a/src/chc.rs +++ b/src/chc.rs @@ -1225,6 +1225,10 @@ impl Pred { } } + pub fn is_var(&self) -> bool { + matches!(self, Pred::Var(_)) + } + pub fn is_top(&self) -> bool { match self { Pred::Known(p) => p.is_top(), @@ -1787,6 +1791,21 @@ impl Body { self.formula.push_conj(formula); } + /// The body stated as a single formula, unless a predicate variable appears in it. + /// + /// A formula holds no predicate variable, because the only place a Horn clause has for one is + /// a conjunct of its body or its head (see [`Formula`]). + pub fn into_formula(self) -> Option> { + if self.atoms.iter().any(|atom| atom.pred.is_var()) { + return None; + } + let mut formula = self.formula; + for atom in self.atoms { + formula.push_conj(Formula::Atom(atom)); + } + Some(formula) + } + pub fn map_var(self, mut f: F) -> Body where F: FnMut(V) -> W, diff --git a/src/refine/basic_block.rs b/src/refine/basic_block.rs index e02e1d68..c2314244 100644 --- a/src/refine/basic_block.rs +++ b/src/refine/basic_block.rs @@ -1,12 +1,11 @@ //! The refinement type for a basic block. -use std::collections::HashMap; - use pretty::{termcolor, Pretty}; use rustc_index::IndexVec; -use rustc_middle::mir::Local; +use rustc_middle::mir::{self, Local}; use rustc_middle::ty as mir_ty; +use crate::chc; use crate::rty; #[derive(Debug, Clone)] @@ -105,17 +104,6 @@ impl BasicBlockType { } } - pub fn local_params(&self) -> impl DoubleEndedIterator + '_ { - self.locals.indices() - } - - pub fn locals(&self) -> impl Iterator + '_ { - self.ty - .params - .iter_enumerated() - .filter_map(|(idx, _)| self.local_of_param(idx)) - } - pub fn param_of_local(&self, local: Local) -> Option { self.locals .iter_enumerated() @@ -133,8 +121,48 @@ impl BasicBlockType { } } - pub fn to_function_ty(&self) -> rty::FunctionType { - self.ty.clone() + /// Replaces the type of every parameter that holds a parameter of the function with the type + /// the signature of the function gives it. + /// + /// A signature can refine a type where the MIR type it is built from has nothing to say, as in + /// `Vec<{ v: i32 | v > 0 }>` or in the pre- and postcondition of a function-typed parameter. + /// The entry block is entered with the arguments of the call, so those are the types it takes. + pub fn install_signature_types( + &mut self, + params: &IndexVec>, + ) { + let param_of_fn_param = |idx| { + self.param_of_local(crate::analyze::local_of_function_param(idx)) + .expect("the entry block takes every parameter of the function") + }; + let signature_types: Vec<_> = self + .ty + .params + .indices() + .filter_map(|idx| { + let fn_param_idx = self.fn_param_of_param(idx)?; + let ty = params[fn_param_idx] + .ty + .clone() + .subst_var(|idx| chc::Term::var(param_of_fn_param(idx))); + Some((idx, ty)) + }) + .collect(); + for (idx, ty) in signature_types { + self.ty.params[idx].ty = ty; + } + } + + /// The parameter of the function held by the parameter `idx`, if it holds one. + fn fn_param_of_param(&self, idx: rty::FunctionParamIdx) -> Option { + match self.param_kind(idx) { + BasicBlockTypeParamKind::Local(local, _) if local != mir::RETURN_PLACE => { + let fn_param_idx = crate::analyze::function_param_of_local(local); + (fn_param_idx.index() < self.outer_fn_param_count).then_some(fn_param_idx) + } + BasicBlockTypeParamKind::OuterFnParam(fn_param_idx) => Some(fn_param_idx), + _ => None, + } } pub fn set_precondition(&mut self, refinement: rty::Refinement) { @@ -147,59 +175,4 @@ impl BasicBlockType { } }); } - - /// Inner function type of BasicBlockType contains extra parameters that carry original - /// function parameter values. `truncate_outer_fn_params` removes these extra parameters - /// to subtype output of [`BasicBlockType::to_function_ty`] against the function type. - /// - /// before: (_1: int, _2: int, int, { int | p4 ν $0 $1 $2 }) → { int | p5 ν $0 $1 $2 $3 } - /// after: (_1: int, _2: { int | p4 v $0 $1 $0 }) → { int | p5 ν $0 $1 _1 _2 } - /// - /// FIXME: this should be (&self) -> FunctionType - pub fn truncate_outer_fn_params(&mut self) { - let last_param_idx = self.ty.params.last_index().unwrap(); - let last_param_ty = self.ty.params.raw.last().unwrap(); - - let mut mapping = HashMap::new(); - for (idx, param_ty) in self.ty.params.iter_enumerated() { - let mapped_idx = if let Some(outer_idx) = self.param_kind(idx).outer_fn_param_idx() { - let corresponding_local = crate::analyze::local_of_function_param(outer_idx); - self.param_of_local(corresponding_local).unwrap() - } else { - idx - }; - mapping.insert(idx, mapped_idx); - - // to be sure - if idx != last_param_idx { - assert!(param_ty.refinement.is_top()); - } - } - - let last_param_refinement = last_param_ty.refinement.clone().map_var(|v| { - let idx = match v { - rty::RefinedTypeVar::Free(idx) => idx, - rty::RefinedTypeVar::Value => last_param_idx, - v => return v, - }; - let mapped_idx = mapping[&idx]; - if Some(mapped_idx) == self.locals.last_index() { - rty::RefinedTypeVar::Value - } else { - rty::RefinedTypeVar::Free(mapped_idx) - } - }); - - if !self.locals.is_empty() { - self.ty.params.truncate(self.locals.len()); - } - - self.ty.params.raw.last_mut().unwrap().refinement = last_param_refinement; - self.ty.ret.refinement = self - .ty - .ret - .refinement - .clone() - .map_free_var(|idx| mapping[&idx]); - } } diff --git a/src/refine/template.rs b/src/refine/template.rs index bf123213..cd385c45 100644 --- a/src/refine/template.rs +++ b/src/refine/template.rs @@ -263,7 +263,7 @@ impl<'tcx> TypeBuilder<'tcx> { } pub fn build_basic_block( - &mut self, + &self, body: &rustc_middle::mir::Body<'tcx>, live_locals: I, ret_ty: mir_ty::Ty<'tcx>, diff --git a/src/rty.rs b/src/rty.rs index cea3583d..c2b43771 100644 --- a/src/rty.rs +++ b/src/rty.rs @@ -52,7 +52,7 @@ mod clause_builder; pub use clause_builder::ClauseBuilderExt; mod subtyping; -pub use subtyping::{relate_sub_param_types, ClauseScope, Subtyping}; +pub use subtyping::{relate_sub_precondition, ClauseScope, Subtyping}; mod params; pub use params::{RefinedTypeArgs, TypeParamIdx, TypeParamSubst}; @@ -1522,6 +1522,37 @@ where self.existentials.extend(existentials); self.body.simplify(); } + + /// The disjunction of the formulas, unless a predicate variable appears in one of them. + /// + /// The existential variables of every disjunct are hoisted in front of the disjunction, which + /// they may be as long as every sort is inhabited. A disjunct that holds a predicate variable + /// has no such form, as a disjunction is no conjunct of a Horn clause body. A single formula + /// stands for itself, and is under no such restriction. + pub fn disjunction(formulas: impl IntoIterator) -> Option { + let mut formulas: Vec<_> = formulas.into_iter().collect(); + if formulas.len() == 1 { + return formulas.pop(); + } + + let mut existentials = IndexVec::new(); + let mut disjuncts = Vec::new(); + for Formula { + existentials: disjunct_existentials, + body, + } in formulas + { + let base = existentials.len(); + existentials.extend(disjunct_existentials); + disjuncts.push(body.map_var(|v| v.shift_existential(base)).into_formula()?); + } + let body = match disjuncts.len() { + 0 => chc::Body::bottom(), + 1 => disjuncts.pop().unwrap().into(), + _ => chc::Formula::Or(disjuncts).into(), + }; + Some(Formula::new(existentials, body)) + } } /// A refinement predicate in a refinement type. diff --git a/src/rty/subtyping.rs b/src/rty/subtyping.rs index 03477f02..d2dd00d8 100644 --- a/src/rty/subtyping.rs +++ b/src/rty/subtyping.rs @@ -5,7 +5,9 @@ use rustc_index::IndexVec; use crate::chc; use crate::pretty::PrettyDisplayExt; -use super::{ClauseBuilderExt as _, FunctionParamIdx, PointerKind, RefKind, RefinedType, Type}; +use super::{ + ClauseBuilderExt as _, FunctionParamIdx, PointerKind, RefKind, RefinedType, Refinement, Type, +}; /// A scope for building clauses. /// @@ -171,27 +173,27 @@ where } } +/// Produces the constraint that a state a basic block is entered in satisfies its precondition. +/// +/// A precondition is a refinement of the last parameter of the block, over the other parameters +/// (see [`crate::refine::BasicBlockType::set_precondition`]), and both refinements are stated in +/// terms of the given parameters. #[must_use] -pub fn relate_sub_param_types( - got: &IndexVec>, - expected: &IndexVec>, +pub fn relate_sub_precondition( + params: &IndexVec>, + got: Refinement, + expected: Refinement, ) -> Vec { - assert_eq!(got.len(), expected.len()); - - let mut clauses = Vec::new(); let mut builder = chc::ClauseBuilder::default(); - - for (param_idx, param_rty) in got.iter_enumerated() { - let param_sort = param_rty.ty.to_sort(); + for (param_idx, param) in params.iter_enumerated() { + let param_sort = param.ty.to_sort(); if !param_sort.is_singleton() { builder.add_mapped_var(param_idx, param_sort); } } - - for (got_ty, expected_ty) in got.iter().zip(expected.iter()) { - let cs = builder.relate_sub_refined_type(expected_ty, got_ty); - clauses.extend(cs); - } - - clauses + let last_param_idx = params.last_index().expect("basic block has a parameter"); + builder + .with_mapped_value_var(last_param_idx) + .add_body(got) + .head(expected) }