An enum declared inside a trait-impl method or a closure produces ill-formed SMT-LIB (unknown sort 'A1_<S'), and two same-named local enums in one function share a datatype and panic: datatype symbols come from def_path_str #316

Summary

refine::datatype_symbol names an enum's CHC datatype after tcx.def_path_str(did) with :: replaced by .:

https://github.com/coord-e/thrust/blob/429c643/src/refine.rs#L35-L37

def_path_str is a human-readable path. It is not a valid SMT-LIB symbol in general, and it is not unique. So an enum declared locally in a function body breaks verification in two ways, depending on where the function is:

1. Ill-formed SMT. In a trait impl method the path is <S as T>::f::E, and in a closure it is main::{closure#0}::E. The spaces, braces and # in those paths go straight into declare-datatypes, the constructor/selector names and every sort reference. The solver rejects the file and verification aborts with verification error: Error { stdout: "(error \"line 3 column 40: invalid sort declaration, arity expected\") ... unknown sort 'A1_<S' ..." }.
2. Name collision. Two different enums named E, each declared in its own block of the same function, both get the symbol f.E. They then share one datatype, and the analyzer panics with index out of bounds: the len is 0 but the index is 0 at src/refine/env.rs:444 (it looks up a variant's fields in the other enum's definition).

The analysis itself is fine here. Only the naming is wrong: give each enum a unique, SMT-safe symbol and all three programs below behave correctly. Declaring a helper enum next to the only code that uses it, inside a method, is ordinary Rust. A trait impl method (impl Iterator for .., impl Display for ..) is a common place for that.

Reproduction

All programs run with thrust-rustc --edition 2021 -Adead_code -C debug-assertions=false on 429c643, default solver (z3).

1. Local enum in a trait impl method → solver error

trait T { fn f(b: bool) -> i64; }
struct S;
impl thrust_models::Model for S { type Ty = Self; }
impl T for S {
    fn f(b: bool) -> i64 {
        enum E { A(i64), B }
        impl thrust_models::Model for E { type Ty = Self; }
        let e = if b { E::A(1) } else { E::B };
        match e { E::A(x) => x, E::B => 0 }
    }
}
fn main() { assert!(S::f(true) == 1); }

error: verification error: Error { stdout: "(error \"line 3 column 40: invalid sort declaration, arity expected\")\n ... (error \"line 28 column 22: Parsing function declaration. Expecting sort list '(': unknown sort 'A1_<S'\")\n ..." }

2. Local enum in a closure → solver error

fn main() {
    let g = |b: bool| -> i64 {
        enum E { A(i64), B }
        impl thrust_models::Model for E { type Ty = Self; }
        let e = if b { E::A(1) } else { E::B };
        match e { E::A(x) => x, E::B => 0 }
    };
    assert!(g(true) == 1);
}

error: verification error: Error { stdout: "(error \"line 3 column 61: unexpected character\")\n(error \"line 3 column 70: invalid bit-vector literal, expecting 'x' or 'b'\")\n ... unknown sort 'A2_main.' ..." }

({closure#0}: { is an "unexpected character" and #0 is read as a bit-vector literal.)

3. Two local enums with the same name in one function → panic

fn f(b: bool) -> i64 {
    let x = {
        enum E { A(i64), B }
        impl thrust_models::Model for E { type Ty = Self; }
        let e = if b { E::A(1) } else { E::B };
        match e { E::A(x) => x, E::B => 0 }
    };
    let y = {
        enum E { C(bool), D(i64), F }
        impl thrust_models::Model for E { type Ty = Self; }
        let e = if b { E::C(true) } else { E::D(5) };
        match e { E::C(_) => 10, E::D(v) => v, E::F => 100 }
    };
    x + y
}
fn main() { assert!(f(true) == 11); assert!(f(false) == 5); }

thread 'rustc' panicked at src/refine/env.rs:444:27:
index out of bounds: the len is 0 but the index is 0

All three are safe programs. With the fix below, each one verifies. If you then break its assertion (== 0 in 1 and 2, f(false) == 6 in 3), each one is rejected with Unsat.

Root cause and fix

datatype_symbol is the only place that turns a DefId into a datatype name. variant constructor names ({name}.{variant}), selectors (_get{ctor}.{idx}), datatype_discr<..> and matcher_pred<..> are all derived from it. The same file already has stable_def_id_symbol, used for user-defined predicate names. It builds {last path segment}_{DefPathHash hex}, which is unique per definition and contains only identifier characters. Using it for datatypes too fixes all three cases:

 pub fn datatype_symbol(tcx: mir_ty::TyCtxt<'_>, did: DefId) -> DatatypeSymbol {
-    DatatypeSymbol::new(tcx.def_path_str(did).replace("::", "."))
+    DatatypeSymbol::new(stable_def_id_symbol(tcx, did))
 }

No code matches on datatype symbol strings, so nothing else depends on the old naming.