Incompleteness: a `fn(..)` pointer value called outside the basic block that created it loses the callee's refinement spec (result is havoc'd), so valid programs verify as `Unsat`

[coord-e]

Summary

When a function-pointer value (a local of type fn(..) -> .., produced by a ReifyFnPointer coercion such as let f: fn(i64) -> i64 = add1;) is called from a basic block other than the one that created it, the call is related against the unrefined function type (..) -> .. instead of the callee's inferred refinement. The callee's precondition and postcondition are both dropped, so the call's result becomes completely unconstrained (havoc'd).

Because a call is a MIR terminator that ends its block, the first fn-pointer call in a body happens in the reify cast's own block and is typed precisely, but every subsequent fn-pointer call lives in a later block and is havoc'd. The effect is that trivially-correct programs are rejected with verification error: Unsat.

This is a completeness failure (over-rejection), not an unsoundness: the havoc'd result is genuinely free, so false assertions after such a call are still (correctly) rejected — Thrust only ever over-rejects here, never over-accepts.

Minimal reproducer

fn incr(m: &mut i64) { *m += 1; }
fn main() {
    let f: fn(&mut i64) = incr;
    let mut x = 0;
    f(&mut x);
    f(&mut x);
    assert!(x == 2);
}

$ cargo run -- -Adead_code -C debug-assertions=false min.rs && echo safe
error: verification error: Unsat

error: aborting due to 1 previous error

x is 0, incremented twice, so x == 2 always holds (concrete values 0, 1, 2 — no overflow), yet Thrust reports Unsat. Calling incr directly twice (not through a pointer value) verifies correctly as safe.

A cleaner return-value witness with no mutable references:

fn add1(x: i64) -> i64 { x + 1 }
fn main() {
    let f: fn(i64) -> i64 = add1;
    let a = f(0);   // first call  — typed precisely, a == 1 is provable
    let b = f(a);   // second call — result havoc'd
    assert!(b == 2);
}

This also reports Unsat.

The trigger is the block, not the count of calls

The "second call" is only incidental: what matters is that the call is in a block other than the reify cast's block. A single fn-pointer call placed behind a branch already reproduces it:

fn add1(x: i64) -> i64 { x + 1 }
#[thrust::callable]
fn check(c: bool) {
    let f: fn(i64) -> i64 = add1;   // reify cast in the entry block
    if c {
        let a = f(0);               // call in a *later* block
        assert!(a == 1);            // true, but rejected as Unsat
    }
}
fn main() {}

Moving the same call into the entry block (no branch) verifies as safe.

Behavior matrix (all with -Adead_code -C debug-assertions=off)

Program	Expected	Thrust
let f=add1; let a=f(0); assert!(a==1); (single call, entry block)	SAFE	safe ✔
let f=add1; if c { let a=f(0); assert!(a==1); } (single call, later block)	SAFE	Unsat ❌
let f=add1; let a=f(0); let b=f(a); assert!(b==2);	SAFE	Unsat ❌
let f=add1; let a=f(0); let _b=f(0); assert!(a==1); (assert on first call)	SAFE	safe ✔
let f=add1; let _a=f(0); let b=f(0); assert!(b==1); (assert on second call)	SAFE	Unsat ❌
let f=add1; let g=add2; let a=f(0); let b=g(a); assert!(b==3); (two targets)	SAFE	Unsat ❌
let f=add1; let g=add2; let b=g(0); let a=f(0); assert!(b==2); (assert on first-called g)	SAFE	safe ✔
incr(&mut x); incr(&mut x); assert!(x==2); (direct calls, no pointer)	SAFE	safe ✔

The last-but-one row (b==2 on the first-called pointer) verifying while the two-targets b==3 does not, confirms it is call order (= block order), not the pointer's identity or the target function, that decides which call keeps its spec. It is not vacuity either: after a havoc'd call, asserting x==i, x==i+1, and x==i+2 are all rejected, i.e. the value is genuinely unconstrained.

Root cause

At each basic-block entry, live locals are re-typed from their declared MIR type via TypeBuilder::build (src/refine/template.rs), driven by build_basic_block. The FnPtr case builds a fully unrefined function type:

// src/refine/template.rs  (fn build)
mir_ty::TyKind::FnPtr(sig_tys, hdr) => {
    let sig = sig_tys.with(*hdr).skip_binder();
    let params = sig
        .inputs()
        .iter()
        .map(|ty| rty::RefinedType::unrefined(self.build(*ty)).vacuous())
        .collect();
    let ret = rty::RefinedType::unrefined(self.build(sig.output()));
    rty::FunctionType::new(params, ret.vacuous()).into()
}

So a fn-pointer local that carried the callee's refinement (attached by the ReifyFnPointer cast in analyze::basic_block, which uses fn_def_ty) has that refinement discarded on entry to any later block. When type_call (src/analyze/basic_block.rs, the non-const_fn_def branch) reads the pointer via operand_type(func).ty, it gets this unrefined (..) -> .. type and relate_fn_sub_type relates the call against true, leaving the result unconstrained.

CHC / trace evidence

For the return-value repro, the fn_sub_type debug log shows the two calls seeing different got types — the second is unrefined:

fn_sub_type got=({ int | p0 ν }) → { int | p1 ν $0 }   expected=({ int | ν = 0 }) → { int | p6 ν }     ; _2 = copy _1(const 0)   [bb0]
fn_sub_type got=(int) → int                            expected=({ int | ν = _2 }) → { int | p7 ν _2 }  ; _3 = copy _1(copy _2)   [bb1]

and the emitted Horn clauses confirm the postcondition predicate is applied for the first call but the second call's result is free (p1 present in the first, absent in the second):

; c3 — first call: postcondition p1 applied, result constrained
(assert (forall (...) (=> (and p5 (= v0 0) (p1 v1 v0) true) (p6 v1))))
; c4 — second call: result v3 is FREE, callee spec never referenced
(assert (forall (...) (=> (and (p6 v1) p5 (= v0 v1) (= v2 v0) true) (p7 v3 v0))))

With the second target's spec predicates (p2/p3 in the two-targets variant) declared and defined but never referenced at the call site.

Notes

• Distinct from Panic unimplemented!(unrefined_ty: FnDef(..)) when passing a named function (function item) to a higher-order function #140 (passing a function item / FnDef to a higher-order function panics with unimplemented!(unrefined_ty: FnDef(..))) — here the pointer is a fn(..) value, it does not panic, and the symptom is a wrong Unsat verdict.
• Distinct from Incompleteness: function-type subtyping in relate_sub_type proves the return obligation without assuming the parameters' preconditions #128 (function-type subtyping in relate_sub_type omits the parameters' preconditions): that drops only the param preconditions during a subtyping relation; here the fn-pointer local loses its entire spec (pre- and post-condition) at the block boundary, before any relation runs.
• The existing passing test tests/ui/pass/fn_ptr.rs is unaffected only because its single f(&mut x) call happens to sit in the same block as the parameter binding; adding a second call, or moving the call behind a branch, reproduces the rejection.
• Numerical-range / overflow concerns are not involved (all values are small non-negative constants).

Environment

• branch main @ 6953863
• solver: Z3 (HORN / Spacer)