Conversation
…ype name
The datatype symbol of an enum was its `def_path_str`. For an enum declared
inside a trait impl method or a closure, that path contains spaces, braces,
and `#` (`<S as T>::f::E`, `main::{closure#0}::E`), so the emitted SMT-LIB was
rejected by the solver. Two same-named enums in different blocks of one
function also shared a symbol and crashed the analyzer.
Items whose def path is entirely in the type namespace (modules and types)
keep their readable path name, which is unique and SMT-safe; any other item
uses the existing `stable_def_id_symbol`. Keeping the old names for module
items also keeps the generated SMT for existing programs unchanged, which
matters because PCSat's running time is sensitive to symbol names.
Fixes #316
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01NuD8BuMA1PzziM9f59oQHb
Codex Review SummaryThis comment shows the latest Codex review activity on this pull request.
ℹ️ About Codex in GitHubYour team has set up Codex to review pull requests in this repo. Reviews are triggered when you
Codex reacts with 👀 while any review is running, comments if it has suggestions, and reacts with 👍 once all reviews finish with no findings. |
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01NuD8BuMA1PzziM9f59oQHb
![chatgpt-codex-connector[bot]](https://avatars.githubusercontent.com/in/1144995?s=60&v=4){kind=small}
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: ff61c0b53c
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
|
|
||
| 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)) |
There was a problem hiding this comment.
When verification uses an existing module-level enum—most notably std.option.Option in tests/ui/pass/slice_split_first_mut_loop.rs—this unconditionally replaces its prior readable symbol with a hash-suffixed name even though only locally nested enums need disambiguation. PCSat is sensitive to these names: this renaming increases that representative case from roughly 5 seconds to beyond the solver's 30-second default, turning a valid program into a timeout. Keep the old def_path_str symbol for paths consisting only of module/type-namespace segments and use the stable def-id symbol only for nested items.
Useful? React with 👍 / 👎.
There was a problem hiding this comment.
Leaving this as is. The maintainer asked to drop the module-path branch, so this PR now uses the stable symbol for every enum. The slowdown is PCSat reacting to one particular name string: the SMT is semantically identical, and other renamings of the same file solve in 6–9s. So it isn't a good reason to keep two naming schemes. I'm waiting for CI on ff61c0b to see whether that test times out on the runner.
Generated by Claude Code
|
CI This is caused by this PR's renaming. The SMT is identical to main except that Ways forward, waiting on a decision:
Generated by Claude Code |
This branch has not been deployed
2 participants
Fixes #316.
Problem
refine::datatype_symbolnamed an enum's datatype aftertcx.def_path_str(did). If the enum is declared inside a function body, that path:<S as T>::f::E) or a closure (main::{closure#0}::E), so the solver rejects the file (unknown sort 'A1_<S');E(both becomef.E), so the analyzer panics atsrc/refine/env.rs:444.Change
If every segment of an item's def path is
DefPathData::TypeNs(modules and types), the item keeps its readabledef_path_strname. That name is unique and SMT-safe. Any other item gets the existingstable_def_id_symbol({name}_{DefPathHash}), which user-defined predicates already use.At first I used
stable_def_id_symbolfor every enum. That produced semantically identical SMT, butstd.option.OptionbecameOption_<hash>, and with that one name PCSat took more than 30s ontests/ui/pass/slice_split_first_mut_loop.rsinstead of about 5s. PCSat's running time depends on symbol names. Keeping module-level names unchanged means every existing test produces byte-identical SMT. I confirmed this withTHRUST_OUTPUT_DIRfor that test.Tests
tests/ui/{pass,fail}/enum_local_in_trait_impl.rs: two impls of one trait, each declaring its own localenum Ewith different variants. Before this change, thepassfile fails with a solver parse error.cargo testlocally, with z3 5.0.0 and the pinned PCSat: 387/388 pass. The one failure istests/ui/fail/slice_split_first_mut_loop.rs, and it is flaky without this change too. Rerunning it alone on the same input gaveTimeout(30s)once and thenUnsatin 18s and 11s. This PR doesn't change the SMT for that test.cargo clippy -- -D warningsis clean. I didn't runrustfmtbecause it isn't installed in this container; the diff is small and formatted by hand.🤖 Generated with Claude Code
https://claude.ai/code/session_01NuD8BuMA1PzziM9f59oQHb
Generated by Claude Code