Panic: a null-sorted value (`fn(..)` pointer, `&str`) stored in an aggregate that also has a non-singleton field is filtered out of `Env::dependencies`, aborting with `unbound var` or `no entry found for key`

[coord-e]

Summary

A value whose sort is Null — a fn(..) pointer or a &str — aborts the analysis when it is stored into an aggregate (tuple or struct) that also carries at least one non-singleton-sorted field.

Env::dependencies drops every local whose sort is_singleton(), so such a local is never registered as a clause variable. The enclosing aggregate, however, is not singleton-sorted (Tuple([Box(Null), Int]) contains an Int), so it survives as a dependency — and its term still references the dropped local. Whichever consumer reaches that reference first panics.

Two panic sites are reachable, depending on whether the field is called:

trigger	panic
calling through the aggregate's fn field	src/chc/clause_builder.rs:113 — unbound var _2
merely holding the aggregate live across a basic-block boundary	src/analyze/basic_block.rs:123 — no entry found for key

Neither is an unimplemented! on an unsupported construct: both are unwrap-style aborts deep in constraint construction, on programs Thrust otherwise handles.

Minimal reproducers

Calling through a tuple field — unbound var:

fn add1(x: i64) -> i64 { x + 1 }
fn main() {
 let p: (fn(i64) -> i64, i64) = (add1, 3);
 let a = (p.0)(0);
 assert!(a == 1);
}

$ cargo run -- -Adead_code -C debug-assertions=false v1.rs
thread 'rustc' panicked at src/chc/clause_builder.rs:113:32:
unbound var _2

No call at all, and no function pointer either — a &str beside an i64 is enough:

fn main() {
 let p: (&str, i64) = ("hi", 3);
 assert!(p.1 == 3);
}

$ cargo run -- -Adead_code -C debug-assertions=false v7.rs
thread 'rustc' panicked at src/analyze/basic_block.rs:123:84:
no entry found for key

Behavior matrix

All with -Adead_code -C debug-assertions=off. Every program is trivially correct.

Program	Thrust
let f: fn(i64)->i64 = add1; let a = f(0); (bare local)	safe ✔
let p: (fn(i64)->i64,) = (add1,); let a = (p.0)(0); (fn-only tuple)	safe ✔
struct S { f: fn(i64)->i64 } … (s.f)(0) (fn-only struct)	safe ✔
let p: (&str, &str) = ("a","b"); let _q = p.1; (all-null tuple)	safe ✔
let u = (); let p = (u, 3); assert!(p.1 == 3); (unit beside int)	safe ✔
let p: (fn(i64)->i64, i64) = (add1, 3); let a = (p.0)(0);	panic unbound var _2 ❌
struct S { f: fn(i64)->i64, n: i64 } … (s.f)(0)	panic unbound var _2 ❌
let p: (fn(i64)->i64, i64) = (add1, 3); assert!(p.1 == 3); (no call)	panic no entry found for key ❌
let p: (&str, i64) = ("hi", 3); assert!(p.1 == 3);	panic no entry found for key ❌
let s = "hi"; let p = (s, 3); assert!(p.1 == 3);	panic no entry found for key ❌
let p: (&str, i64, i64) = ("a", 3, 4); assert!(p.1 + p.2 == 7);	panic no entry found for key ❌

The fn-only and all-null rows isolate the trigger: it is the mixture of a null-sorted field with a non-singleton one, not the function pointer, the call, or the aggregate kind. A unit field is unaffected.

Root cause

Env::dependencies (src/refine/env.rs) excludes every local of a singleton sort:

pub fn dependencies(&self) -> impl Iterator<Item = (Var, chc::Sort)> + '_ {
 self.locals
 .iter()
 .map(|(local, rty)| (Var::Local(*local), rty.ty.to_sort()))
 .filter(|(_, s)| !s.is_singleton())
 .chain(...)
}

Type::Function and Type::String both lower to chc::Sort::Null, and Sort::is_singleton is true for Null and for Box/Tuple built only from singletons — so a fn(..) local, or a &str local, is never a dependency. That is fine on its own: such a value carries no logical content, and a bare fn(..) local verifies (row 1).

It stops being fine once the value is moved into a mixed aggregate. From the MIR of the first reproducer:

_2 = add1 as fn(i64) -> i64 (PointerCoercion(ReifyFnPointer(Safe), Implicit));
_1 = (move _2, const 3_i64);
_4 = copy (_1.0: fn(i64) -> i64);
_3 = move _4(const 0_i64) -> [return: bb1, unwind continue];

_1 has sort Tuple([Box(Null), Int]), which is not singleton, so _1 is a dependency and its term — which references _2 — reaches clause construction. _2 itself was filtered out. The two consumers then fail in their own way:

• type_call → relate_fn_sub_type maps the env's free vars onto clause variables through ClauseBuilder::mapped_var, which panics on the unregistered _2:

  thrust::chc::clause_builder::ClauseBuilder::mapped_var
  thrust::rty::Formula<RefinedTypeVar<FV>>::map_free_var::{{closure}}
  thrust::analyze::basic_block::Analyzer::relate_fn_sub_type
  thrust::analyze::basic_block::Analyzer::type_call
  

• type_goto → install_inherited_bb_ty → PrecondCapture::finish builds substs from env.dependencies() and then indexes it for every free var of the captured body, so the missing entry is a bare HashMap index panic:

  thrust::analyze::basic_block::PrecondCapture::finish::{{closure}} // substs[&v]
  thrust::analyze::basic_block::Analyzer::install_inherited_bb_ty
  thrust::analyze::basic_block::Analyzer::type_goto
  thrust::analyze::basic_block::Analyzer::type_switch_int
  

The second path needs only a block boundary, which is why the plain assert!(p.1 == 3) variants abort without any call.

Notes

• Distinct from Panic unimplemented!(unrefined_ty: FnDef(..)) when passing a named function (function item) to a higher-order function #140 (unimplemented!(unrefined_ty: FnDef(..)) when passing a function item to a higher-order function): here the aggregate holds a fn(..) value, and the abort is an unwrap/index panic in constraint construction rather than an unimplemented!.
• Distinct from 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 #201 (a fn(..) pointer local losing its spec across a block boundary): that is a wrong Unsat, and it does not involve aggregates. A bare fn-pointer local is row 1 above and is fine.
• Distinct from Undefined sort name in SMT2 when predicate argument is a struct containing a closure #47 (undefined SMT sort name when a predicate argument is a struct containing a closure): that surfaces in the emitted SMT2, not as a panic, and the null-sorted field here need not be callable at all.
• Distinct from Calling a closure in a struct field causes a panic #38 (inconsistent types when calling a closure in a struct field), which was fixed by Allow non-return ZST places to appear without proceding defs in BB #42.
• Not specific to function pointers: &str reproduces both panics. Type::Never also lowers to Sort::Null and is presumably affected the same way, though I did not construct a case for it.

Environment

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