Unsound: a user `Drop` impl is never checked at the drop site — `TerminatorKind::Drop` only resolves prophecies, so a destructor that panics verifies as `safe`

[coord-e]

When a type has a user-written Drop impl, the destructor body is never verified. TerminatorKind::Drop is handled purely as Thrust's own prophecy-resolution step: it runs drop_local for the drop points and then gotos, without ever typing a call to <T as Drop>::drop. The destructor's obligations are therefore discharged nowhere, and a program whose destructor always panics verifies as safe.

Reproduction

tests/ui/fail/drop_impl.rs — the destructor's assertion fails for the value that is actually dropped, so this should be Unsat:

//@error-in-other-file: Unsat
//@compile-flags: -C debug-assertions=off

#[derive(PartialEq)]
struct G {
    n: i64,
}

impl thrust_models::Model for G {
    type Ty = Self;
}

impl Drop for G {
    fn drop(&mut self) {
        assert!(self.n == 0);
    }
}

fn main() {
    let _g = G { n: 5 };
}

$ cargo run -- -Adead_code -C debug-assertions=false drop_impl_fail.rs && echo 'safe'
safe

Expected error: verification error: Unsat. The program does panic:

$ rustc -C debug-assertions=off -o native native.rs && ./native
thread 'main' (7596) panicked at native.rs:3:26:
assertion failed: self.n == 0
...
   3: <native::G as core::ops::drop::Drop>::drop
   4: core::ptr::drop_in_place<native::G>
   5: native::main

The pass half of the pair (self.n == 5, which is what is actually dropped) also verifies, so the pair currently does not distinguish the two directions at all:

//@check-pass
//@compile-flags: -C debug-assertions=off
// ... same, with `assert!(self.n == 5);`

Writes the destructor makes to self are not modeled either — this also verifies as safe, where the assertion is false at runtime:

impl Drop for G {
    fn drop(&mut self) {
        self.n = 0;
        assert!(self.n == 5);
    }
}

fn main() {
    let _g = G { n: 5 };
}

Cause

main's MIR for the reproducer is a plain drop terminator, not a call:

bb0: {
    _1 = G { n: const 5_i64 };
    drop(_1) -> [return: bb1, unwind continue];
}

analyze_terminator_goto treats that terminator as Thrust's internal drop only (src/analyze/basic_block.rs:1276):

TerminatorKind::Drop { target, .. } => {
    for local in self.drop_points.after_terminator(target) {
        tracing::info!(?local, "dropped");
        self.drop_local(local);
    }
    self.type_goto(*target, outer_fn_param_vars);
}

drop_local resolves the prophecies reachable from the local; nothing types <G as Drop>::drop(&mut _1). The neighbouring terminator_is_drop_call hack (src/analyze/basic_block.rs:1129, used at 1162 and 1189) rewrites a direct std::ops::Drop::drop call terminator into a Goto and skips the borrow statement in front of it, so the explicit-call shape is skipped by construction as well.

The body itself is perfectly analyzable — it is only the missing call that leaves it ungrounded. Forcing it to be checked on its own reports the error:

impl Drop for G {
    #[thrust::callable]
    fn drop(&mut self) { assert!(self.n == 0); }
}

error: verification error: Unsat

So the drop site needs to type a call to the destructor (checking its precondition against the value being dropped, and taking its effect on self into the environment) before running the existing prophecy resolution, rather than skipping it.

Not a duplicate

The existing drop issues (#121, #122, #173, #175, #202, #207) are all about Thrust's internal drop — which prophecies drop_local resolves and when. This one is about the user's Drop impl never being invoked by the analysis at all, and it is independent of them: it reproduces on a type with no &mut anywhere.

It is also distinct from #179/#200. Those are about a body that is never called being discharged vacuously; here the destructor is called on every execution, and Thrust drops that call on the floor.