Fix declaration order and enum mangling issues#681
Open
tahina-pro wants to merge 7 commits intoFStarLang:masterfrom
Open
Fix declaration order and enum mangling issues#681tahina-pro wants to merge 7 commits intoFStarLang:masterfrom
tahina-pro wants to merge 7 commits intoFStarLang:masterfrom
Conversation
…order The hoist pass in Simplify.ml builds a field_types table from DType declarations, then uses it when processing DFunction bodies. When monomorphization emits types after the functions that reference them, Hashtbl.find crashes with Not_found. Use Hashtbl.find_opt with a safe default (false = not an array type) instead. This is correct because the lookup only determines whether a struct field is an array type for hoisting purposes. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
The changes in FStarLang#676 (commit c1e092f) introduced three problems for non-polymorphic types: 1. The fast-path in visit_node skipped non-polymorphic types that hadn't been seen yet, deferring them to their source position. This broke DFS dependency ordering: types could appear after the types that use them by value. 2. The 'if args <> [] || cgs <> []' guards prevented visit_node from recording non-polymorphic types, forcing them to be emitted at their source position via visit_decl instead of in DFS order. 3. The visit_decl handler for non-polymorphic DTypes used Gray/Black state management and appended the visited declaration, instead of delegating to visit_node for proper DFS ordering. 4. Type arguments were visited with the caller's under_ref flag, which could trigger full processing of types that are actually used behind pointers inside the parameterized type (e.g., slice<T> stores T*). Fix: restore the old DFS-based ordering by (1) only fast-pathing Black types, (2) always recording in visit_node, (3) using visit_node from visit_decl, and (4) visiting type arguments with under_ref=true. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
The mangle_enum function creates composite names from (type_lid, enum_lid) to disambiguate enum values across types. When the type at the use site is a typedef alias rather than the canonical tag type, mangle_enum produces a different name than at the definition site. Fix by resolving type abbreviations before calling mangle_enum at both the EEnum expression and SEnum switch case sites. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
- DeclOrder.fst: Tests that non-polymorphic types used by value inside monomorphised polymorphic types are emitted in correct DFS order. Fails without commits d72e7fa and c105d05 (types emitted after their users, causing C compilation errors). - EnumAliasResolve.fst + EnumAliasHelper.fst: Tests that enum values are correctly resolved when the type at the use site is a typedef alias. Two types share constructor names, causing the DataTypes pass to make one an abbreviation of the other. Fails without commit 8acc4b3 (mangle_enum produces mismatched names for aliases). Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Member
Author
|
Also shown to work well with Pulse: https://github.com/tahina-pro/FStar/actions/runs/22158831433/job/64073712693 |
Collaborator
|
Thanks. The testcases are helpful but the code change seems like it doesn't address the root of the issue (stray abbreviations). My suspicion is that this is a combination of optimizing data types representation (which generates type abbreviations that are not inlined away) and the enum mangling scheme taking the lid on the node at face value. I'd rather insert another call to inline_type_abbrevs in the main driver to re-establish the invariant that there are no uses of type abbreviations and that subsequent passes do not need to worry about maintaining their own tables to keep track of equivalence classes. |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
This PR fixes C and Rust extraction issues that have been hitting EverParse since moving ahead of Karamel's "last known good" commit for EverParse, fb36fec, and which #679 has not entirely fixed.
Changes introduced by this PR, including unit test cases, have been entirely AI-generated by GitHub Copilot CLI using Claude Opus 4.6 (apart from a few purely cosmetic changes of mine.) Commit descriptions contain more details about the issues, their fixes and the corresponding unit test cases.
Full EverParse CI works with 660f525 : https://github.com/tahina-pro/quackyducky/actions/runs/22151241820