Unsound: a call to a trait method with a default body is typed by the default body even when the impl overrides it with its own spec (#[thrust::callable]), so panicking programs verify as safe #337

Summary

When a trait method has a default body and an impl overrides it with a method that carries its own spec (today only #[thrust::callable] is possible, see #258), a call that resolves to the override is typed by the trait method's type. That type is inferred from the default body. The override is checked only against its own spec, so the default body's postcondition reaches the caller without ever being proved for the code that actually runs.

Reproduction

trait Tr {
    fn m(&self) -> i64 {
        2
    }
}

struct A;

impl Tr for A {
    #[thrust::callable]
    fn m(&self) -> i64 {
        1
    }
}

fn main() {
    assert!(A.m() == 2);
}

$ thrust-rustc -Adead_code -C debug-assertions=false repro.rs && echo safe
safe

At runtime A.m() runs the override, returns 1, and the assertion panics. callable gives m the spec true/true, so the call's result should be unconstrained and the program should be rejected with Unsat.

These variants also verify as safe:

• the call goes through a generic, fn g<T: Tr>(t: &T) -> i64 { t.m() } with assert!(g(&A) == 2);
• the override is #[thrust::trusted] #[thrust::callable].

Root cause

• The call uses the trait method's type. fn_def_ty (src/analyze/basic_block.rs) first asks def_ty_with_args(def_id, args) for the unresolved trait method. A defaulted trait method is registered as a deferred def, so this lookup succeeds and returns the default body's type, with Self instantiated to A. The resolved impl method is looked up only so that its body gets analyzed, and its type is thrown away.
• The override is checked against something else. expected_ty (src/analyze/local_def.rs) checks a fully annotated method (is_fully_annotated(), which includes callable) against its own annotations, not against trait_item_ty.
• Result: callers assume the default body's postcondition, but the override is never required to satisfy it.

An unannotated override is checked against trait_item_ty, so using the trait method's type at the call site is sound there. That case is the incompleteness reported in #187. This issue is the case where the override has its own spec.

Fix direction

When the call resolves to a different impl method that has a type, type the call by that impl method's type. For an unannotated override this is the same trait_item_ty as before. For an annotated override it is the spec the body was actually checked against.

Environment

• thrust @ 187a1e9
• Z3 5.0.0