From 788fa993f1dd95d60bd1c428bce4e8b34e78d2b8 Mon Sep 17 00:00:00 2001 From: Claude Date: Thu, 20 Aug 2026 12:18:55 +0000 Subject: [PATCH 1/2] Carry a fn pointer's specification across a basic block boundary A function type states the callee's specification in the type itself, and `Type::Function` lowers to a null sort, so a fn-pointer local carries no logical content at all. A block that inherits its predecessor's env state as its precondition therefore cannot receive that specification: the precondition is a formula about the parameters' values, and there is no value to speak about. The capture loop skips the parameter as singleton-sorted, `TypeBuilder::build` has meanwhile rebuilt it from its MIR type alone, and `type_call` relates the call against `true`, leaving the result unconstrained. Because a call ends its block, the first call in a body sits in the reify cast's own block and is typed precisely, while every later one is not; a single call behind a branch is enough on its own. A fn-pointer parameter reaches the same path once it is called from a later block. `install_inherited_bb_ty` already materializes the target's type from the env, so hand the function types over there too. The copy walks into the type rather than matching only its root, so a function type nested inside a tuple or a struct is carried across as well. A position where the two shapes disagree is left alone: missing a specification costs precision, while taking one from an unrelated position would be wrong. Relating the two types at the goto instead, as the other path in `type_goto` does, would achieve nothing here: the target's type is built without predicate variables, so there would be nothing for the subtyping to constrain. --- src/analyze.rs | 22 +++++++++++ src/analyze/basic_block.rs | 31 +++++++++++++++ src/refine/basic_block.rs | 9 +++++ src/rty.rs | 44 +++++++++++++++++++++ tests/ui/fail/fn_ptr_call_in_branch.rs | 18 +++++++++ tests/ui/fail/fn_ptr_call_twice.rs | 15 +++++++ tests/ui/fail/fn_ptr_in_tuple_call_twice.rs | 14 +++++++ tests/ui/fail/fn_ptr_param_call_twice.rs | 24 +++++++++++ tests/ui/pass/fn_ptr_call_in_branch.rs | 20 ++++++++++ tests/ui/pass/fn_ptr_call_twice.rs | 17 ++++++++ tests/ui/pass/fn_ptr_in_tuple_call_twice.rs | 15 +++++++ tests/ui/pass/fn_ptr_param_call_twice.rs | 26 ++++++++++++ 12 files changed, 255 insertions(+) create mode 100644 tests/ui/fail/fn_ptr_call_in_branch.rs create mode 100644 tests/ui/fail/fn_ptr_call_twice.rs create mode 100644 tests/ui/fail/fn_ptr_in_tuple_call_twice.rs create mode 100644 tests/ui/fail/fn_ptr_param_call_twice.rs create mode 100644 tests/ui/pass/fn_ptr_call_in_branch.rs create mode 100644 tests/ui/pass/fn_ptr_call_twice.rs create mode 100644 tests/ui/pass/fn_ptr_in_tuple_call_twice.rs create mode 100644 tests/ui/pass/fn_ptr_param_call_twice.rs diff --git a/src/analyze.rs b/src/analyze.rs index fce97595..58c846c3 100644 --- a/src/analyze.rs +++ b/src/analyze.rs @@ -585,6 +585,28 @@ impl<'tcx> Analyzer<'tcx> { self.basic_blocks.entry(def_id).or_default().insert(bb, def); } + /// Installs the types of a basic block's parameters. + /// + /// A block whose parameters are typed from MIR types alone carries an unrefined + /// specification for every function type they contain. This overwrites those + /// parameters with types whose specifications were recovered from elsewhere. + pub fn register_basic_block_param_tys( + &mut self, + def_id: LocalDefId, + bb: BasicBlock, + tys: impl IntoIterator)>, + ) { + let bb_def = self + .basic_blocks + .get_mut(&def_id) + .unwrap() + .get_mut(&bb) + .unwrap(); + for (idx, ty) in tys { + bb_def.ty.set_param_ty(idx, ty); + } + } + pub fn register_basic_block_precondition( &mut self, def_id: LocalDefId, diff --git a/src/analyze/basic_block.rs b/src/analyze/basic_block.rs index 4ed04196..e5e5501e 100644 --- a/src/analyze/basic_block.rs +++ b/src/analyze/basic_block.rs @@ -816,11 +816,42 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { } capture.push_env_state(&self.env); let precondition = capture.finish(&self.env); + let param_tys = self.inherited_param_tys(bty); + self.ctx + .register_basic_block_param_tys(self.local_def_id, bb, param_tys); self.ctx .register_basic_block_precondition(self.local_def_id, bb, precondition); } + /// Rebuilds a goto target's params that contain a function type, taking the + /// specifications the env holds. + /// + /// A function type carries the callee's specification in the type itself rather than + /// in a refinement, so a precondition captured from the env cannot bring it along. + /// The target's params are typed from their MIR types alone, which leaves every + /// function type in them unrefined. + fn inherited_param_tys( + &self, + bty: &BasicBlockType, + ) -> Vec<(rty::FunctionParamIdx, rty::Type)> { + let mut tys = Vec::new(); + for (param_idx, param_rty) in bty.as_ref().params.iter_enumerated() { + // Only a param standing for a local is ever called; an `OuterFnParam` copy of + // a function-typed argument exists to name the argument's entry value. + let BasicBlockTypeParamKind::Local(local, _) = bty.param_kind(param_idx) else { + continue; + }; + if !param_rty.ty.contains_function() { + continue; + } + let mut ty = param_rty.ty.clone(); + ty.copy_function_types(&self.env.local_type(local).ty); + tys.push((param_idx, ty)); + } + tys + } + fn with_assumptions(&mut self, assumptions: Vec>, callback: F) -> T where F: FnOnce(&mut Self) -> T, diff --git a/src/refine/basic_block.rs b/src/refine/basic_block.rs index e02e1d68..9a4d22c5 100644 --- a/src/refine/basic_block.rs +++ b/src/refine/basic_block.rs @@ -137,6 +137,15 @@ impl BasicBlockType { self.ty.clone() } + /// Replaces the type of the parameter at `idx`, keeping its refinement. + pub fn set_param_ty( + &mut self, + idx: rty::FunctionParamIdx, + ty: rty::Type, + ) { + self.ty.params[idx].ty = ty; + } + pub fn set_precondition(&mut self, refinement: rty::Refinement) { let last_param_idx = self.ty.params.last_index().unwrap(); self.ty.params.raw.last_mut().unwrap().refinement = refinement.map_var(|v| { diff --git a/src/rty.rs b/src/rty.rs index cea3583d..9bfc2af5 100644 --- a/src/rty.rs +++ b/src/rty.rs @@ -1056,6 +1056,50 @@ impl Type { } } + /// Whether a function type occurs anywhere in this type. + pub fn contains_function(&self) -> bool { + match self { + Type::Function(_) => true, + Type::Pointer(ty) => ty.elem.ty.contains_function(), + Type::Tuple(ty) => ty.elems.iter().any(|elem| elem.ty.contains_function()), + Type::Enum(ty) => ty.args.iter().any(|arg| arg.ty.contains_function()), + Type::Array(ty) => ty.index.ty.contains_function() || ty.elem.ty.contains_function(), + Type::Int | Type::Bool | Type::String | Type::Never | Type::Param(_) => false, + } + } + + /// Replaces every function type in this type with the one at the same position in `src`. + /// + /// A function type states the callee's specification in the type itself, so a type built + /// from a MIR type alone (see [`crate::refine::TypeBuilder`]) leaves that specification + /// unrefined. This takes the specifications from a type of the same shape and leaves the + /// rest of this type alone. A position where the two shapes disagree is left as it is: + /// missing a specification only costs precision, whereas installing one from an unrelated + /// position would be wrong. + pub fn copy_function_types(&mut self, src: &Type) { + match (self, src) { + (Type::Function(dst), Type::Function(src)) => *dst = src.clone(), + (Type::Pointer(dst), Type::Pointer(src)) => { + dst.elem.ty.copy_function_types(&src.elem.ty) + } + (Type::Tuple(dst), Type::Tuple(src)) if dst.elems.len() == src.elems.len() => { + for (dst, src) in dst.elems.iter_mut().zip(src.elems.iter()) { + dst.ty.copy_function_types(&src.ty); + } + } + (Type::Enum(dst), Type::Enum(src)) if dst.args.len() == src.args.len() => { + for (dst, src) in dst.args.iter_mut().zip(src.args.iter()) { + dst.ty.copy_function_types(&src.ty); + } + } + (Type::Array(dst), Type::Array(src)) => { + dst.index.ty.copy_function_types(&src.index.ty); + dst.elem.ty.copy_function_types(&src.elem.ty); + } + _ => {} + } + } + pub fn as_pointer(&self) -> Option<&PointerType> { match self { Type::Pointer(ty) => Some(ty), diff --git a/tests/ui/fail/fn_ptr_call_in_branch.rs b/tests/ui/fail/fn_ptr_call_in_branch.rs new file mode 100644 index 00000000..a6ffde40 --- /dev/null +++ b/tests/ui/fail/fn_ptr_call_in_branch.rs @@ -0,0 +1,18 @@ +//@error-in-other-file: Unsat +//@compile-flags: -C debug-assertions=off + +fn add1(x: i64) -> i64 { + x + 1 +} + +// `add1(0)` is 1 rather than 0. +#[thrust::callable] +fn check(c: bool) { + let f: fn(i64) -> i64 = add1; + if c { + let a = f(0); + assert!(a == 0); + } +} + +fn main() {} diff --git a/tests/ui/fail/fn_ptr_call_twice.rs b/tests/ui/fail/fn_ptr_call_twice.rs new file mode 100644 index 00000000..5b1a1067 --- /dev/null +++ b/tests/ui/fail/fn_ptr_call_twice.rs @@ -0,0 +1,15 @@ +//@error-in-other-file: Unsat +//@compile-flags: -C debug-assertions=off + +fn incr(m: &mut i64) { + *m += 1; +} + +// `x` is incremented twice, so it is 2 rather than 1 here. +fn main() { + let f: fn(&mut i64) = incr; + let mut x = 0; + f(&mut x); + f(&mut x); + assert!(x == 1); +} diff --git a/tests/ui/fail/fn_ptr_in_tuple_call_twice.rs b/tests/ui/fail/fn_ptr_in_tuple_call_twice.rs new file mode 100644 index 00000000..a612dd0d --- /dev/null +++ b/tests/ui/fail/fn_ptr_in_tuple_call_twice.rs @@ -0,0 +1,14 @@ +//@error-in-other-file: Unsat +//@compile-flags: -C debug-assertions=off + +fn add1(x: i64) -> i64 { + x + 1 +} + +// `add1` is applied twice, so the result is 2 rather than 1. +fn main() { + let p: (fn(i64) -> i64,) = (add1,); + let a = (p.0)(0); + let b = (p.0)(a); + assert!(b == 1); +} diff --git a/tests/ui/fail/fn_ptr_param_call_twice.rs b/tests/ui/fail/fn_ptr_param_call_twice.rs new file mode 100644 index 00000000..961ffe5e --- /dev/null +++ b/tests/ui/fail/fn_ptr_param_call_twice.rs @@ -0,0 +1,24 @@ +//@error-in-other-file: Unsat +//@compile-flags: -C debug-assertions=off + +#[thrust_macros::requires(true)] +#[thrust_macros::ensures(true)] +#[thrust::trusted] +fn rand() -> i64 { unimplemented!() } + +fn incr(m: &mut i64) { + *m += 1; +} + +fn app(f: fn(&mut i64), mut x: i64) -> i64 { + f(&mut x); + f(&mut x); + x +} + +// `x` is incremented twice, so it is `i + 2` rather than `i + 1` here. +fn main() { + let i = rand(); + let x = app(incr, i); + assert!(x == i + 1); +} diff --git a/tests/ui/pass/fn_ptr_call_in_branch.rs b/tests/ui/pass/fn_ptr_call_in_branch.rs new file mode 100644 index 00000000..3dfcc6c2 --- /dev/null +++ b/tests/ui/pass/fn_ptr_call_in_branch.rs @@ -0,0 +1,20 @@ +//@check-pass +//@compile-flags: -C debug-assertions=off + +fn add1(x: i64) -> i64 { + x + 1 +} + +// The cast that produces `f` and the call of `f` sit in different basic blocks. +// The callee's specification must survive that boundary; without it the call's +// result is unconstrained. +#[thrust::callable] +fn check(c: bool) { + let f: fn(i64) -> i64 = add1; + if c { + let a = f(0); + assert!(a == 1); + } +} + +fn main() {} diff --git a/tests/ui/pass/fn_ptr_call_twice.rs b/tests/ui/pass/fn_ptr_call_twice.rs new file mode 100644 index 00000000..2ddce151 --- /dev/null +++ b/tests/ui/pass/fn_ptr_call_twice.rs @@ -0,0 +1,17 @@ +//@check-pass +//@compile-flags: -C debug-assertions=off + +fn incr(m: &mut i64) { + *m += 1; +} + +// A call ends its basic block, so the second call sees `f` re-entering the block +// it lives in. The callee's specification must survive that boundary; without it +// the second call's effect on `x` is unconstrained. +fn main() { + let f: fn(&mut i64) = incr; + let mut x = 0; + f(&mut x); + f(&mut x); + assert!(x == 2); +} diff --git a/tests/ui/pass/fn_ptr_in_tuple_call_twice.rs b/tests/ui/pass/fn_ptr_in_tuple_call_twice.rs new file mode 100644 index 00000000..85d8a41c --- /dev/null +++ b/tests/ui/pass/fn_ptr_in_tuple_call_twice.rs @@ -0,0 +1,15 @@ +//@check-pass +//@compile-flags: -C debug-assertions=off + +fn add1(x: i64) -> i64 { + x + 1 +} + +// The specification has to reach a function type nested inside another type, not +// just one a local holds directly. +fn main() { + let p: (fn(i64) -> i64,) = (add1,); + let a = (p.0)(0); + let b = (p.0)(a); + assert!(b == 2); +} diff --git a/tests/ui/pass/fn_ptr_param_call_twice.rs b/tests/ui/pass/fn_ptr_param_call_twice.rs new file mode 100644 index 00000000..4cbde632 --- /dev/null +++ b/tests/ui/pass/fn_ptr_param_call_twice.rs @@ -0,0 +1,26 @@ +//@check-pass +//@compile-flags: -C debug-assertions=off + +#[thrust_macros::requires(true)] +#[thrust_macros::ensures(true)] +#[thrust::trusted] +fn rand() -> i64 { unimplemented!() } + +fn incr(m: &mut i64) { + *m += 1; +} + +// A call ends its basic block, so the second call sees `f` re-entering the block +// it lives in. The specification the caller supplied for `f` must survive that +// boundary; without it the second call's effect on `x` is unconstrained. +fn app(f: fn(&mut i64), mut x: i64) -> i64 { + f(&mut x); + f(&mut x); + x +} + +fn main() { + let i = rand(); + let x = app(incr, i); + assert!(x == i + 2); +} From 22a95e4296594d269b95d05a4771c65561a76aca Mon Sep 17 00:00:00 2001 From: Claude Date: Thu, 20 Aug 2026 13:59:42 +0000 Subject: [PATCH 2/2] Carry what a type states across a basic block boundary A block that inherits its precondition takes over what its predecessor's env says about each parameter's *value*, and is otherwise typed from MIR types alone. Everything a type states by itself is dropped at that boundary: the refinements nested in it, and the specification a function type spells out. A fn-pointer value is where this shows: called from a block other than the one that created it, it is related against an unrefined `(..) -> ..`, so the callee's pre- and postcondition are both gone and the result is left unconstrained. A call ends its block, so the first call in a body is typed precisely and every later one is not. Hand the env's types over alongside the precondition. A type in the env is closed -- a refinement nested in one constrains the value at its own position and names nothing from the env -- so it transfers as it stands, and `assert_closed` pins that down. Blocks that need their own precondition keep relating the two types at the goto, which already transferred all of this. Fixes #201. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_014bFB7y5QM3ebxvtusQYZBo --- src/analyze/basic_block.rs | 29 ++++++++++++++----------- src/rty.rs | 44 -------------------------------------- 2 files changed, 16 insertions(+), 57 deletions(-) diff --git a/src/analyze/basic_block.rs b/src/analyze/basic_block.rs index e5e5501e..0461a3ba 100644 --- a/src/analyze/basic_block.rs +++ b/src/analyze/basic_block.rs @@ -824,29 +824,32 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { .register_basic_block_precondition(self.local_def_id, bb, precondition); } - /// Rebuilds a goto target's params that contain a function type, taking the - /// specifications the env holds. + /// Takes the types the env holds for a goto target's params. /// - /// A function type carries the callee's specification in the type itself rather than - /// in a refinement, so a precondition captured from the env cannot bring it along. - /// The target's params are typed from their MIR types alone, which leaves every - /// function type in them unrefined. + /// The captured precondition carries what a parameter's *value* satisfies, and the + /// target's params are otherwise built from their MIR types alone. Everything a type + /// states by itself is therefore missing from the target: the refinements nested in + /// it, and the specification a function type spells out. Those are handed over here. + /// + /// A type in the env is closed — a refinement nested in one constrains the value at + /// its own position and names nothing from the env — so it transfers as it stands. fn inherited_param_tys( &self, bty: &BasicBlockType, ) -> Vec<(rty::FunctionParamIdx, rty::Type)> { let mut tys = Vec::new(); for (param_idx, param_rty) in bty.as_ref().params.iter_enumerated() { - // Only a param standing for a local is ever called; an `OuterFnParam` copy of - // a function-typed argument exists to name the argument's entry value. + // An `OuterFnParam` copy of an argument names that argument's entry value, and + // takes its type from the outer function's signature rather than from the env. let BasicBlockTypeParamKind::Local(local, _) = bty.param_kind(param_idx) else { continue; }; - if !param_rty.ty.contains_function() { - continue; - } - let mut ty = param_rty.ty.clone(); - ty.copy_function_types(&self.env.local_type(local).ty); + let ty = self.env.local_type(local).ty.assert_closed().vacuous(); + assert_eq!( + ty.to_sort(), + param_rty.ty.to_sort(), + "env holds {local:?} at a different sort than the goto target's parameter" + ); tys.push((param_idx, ty)); } tys diff --git a/src/rty.rs b/src/rty.rs index 9bfc2af5..cea3583d 100644 --- a/src/rty.rs +++ b/src/rty.rs @@ -1056,50 +1056,6 @@ impl Type { } } - /// Whether a function type occurs anywhere in this type. - pub fn contains_function(&self) -> bool { - match self { - Type::Function(_) => true, - Type::Pointer(ty) => ty.elem.ty.contains_function(), - Type::Tuple(ty) => ty.elems.iter().any(|elem| elem.ty.contains_function()), - Type::Enum(ty) => ty.args.iter().any(|arg| arg.ty.contains_function()), - Type::Array(ty) => ty.index.ty.contains_function() || ty.elem.ty.contains_function(), - Type::Int | Type::Bool | Type::String | Type::Never | Type::Param(_) => false, - } - } - - /// Replaces every function type in this type with the one at the same position in `src`. - /// - /// A function type states the callee's specification in the type itself, so a type built - /// from a MIR type alone (see [`crate::refine::TypeBuilder`]) leaves that specification - /// unrefined. This takes the specifications from a type of the same shape and leaves the - /// rest of this type alone. A position where the two shapes disagree is left as it is: - /// missing a specification only costs precision, whereas installing one from an unrelated - /// position would be wrong. - pub fn copy_function_types(&mut self, src: &Type) { - match (self, src) { - (Type::Function(dst), Type::Function(src)) => *dst = src.clone(), - (Type::Pointer(dst), Type::Pointer(src)) => { - dst.elem.ty.copy_function_types(&src.elem.ty) - } - (Type::Tuple(dst), Type::Tuple(src)) if dst.elems.len() == src.elems.len() => { - for (dst, src) in dst.elems.iter_mut().zip(src.elems.iter()) { - dst.ty.copy_function_types(&src.ty); - } - } - (Type::Enum(dst), Type::Enum(src)) if dst.args.len() == src.args.len() => { - for (dst, src) in dst.args.iter_mut().zip(src.args.iter()) { - dst.ty.copy_function_types(&src.ty); - } - } - (Type::Array(dst), Type::Array(src)) => { - dst.index.ty.copy_function_types(&src.index.ty); - dst.elem.ty.copy_function_types(&src.elem.ty); - } - _ => {} - } - } - pub fn as_pointer(&self) -> Option<&PointerType> { match self { Type::Pointer(ty) => Some(ty),