Core.formatProgram to produce round-trip-parseable output for all constructs#1165
Merged
MikaelMayer merged 23 commits intoMay 18, 2026
Merged
Conversation
- Fix inline function formatting: add trailing space to 'inline' op in Grammar.lean to prevent 'inlinefunction' concatenation - Emit inline attribute when formatting functions that have it - Use prettyName for quantifier variables instead of generated __qN names - Add overflow predicate support: grammar entries, formatter handling, parser entries, and Factory operations for Bv32 overflow predicates - Add roundtrip test infrastructure for Core programs - Update test expected outputs to reflect prettyName fix
Resolve conflicts between the formatProgram roundtrip fix and main's refactoring (FormatCore extraction, recFnDeclToCST, procedure syntax). - Apply prettyName and inline? fixes to FormatCore.lean - Use proper overflow CST constructors instead of approximations - Remove duplicate overflow declarations in Factory.lean - Update test expected outputs for combined changes - Fix RoundtripTest to handle new 'program Core;' header
This comment was marked as resolved.
This comment was marked as resolved.
Sorry, something went wrong.
… grammar entry - Overflow ops in translateFn now match on type parameter (.some .bv1, .some .bv8, etc.) instead of using wildcard _, consistent with all other type-parameterized BV ops. - Added bv_sdiv_overflow grammar entry so SDivOverflow formats as Bv.SDivOverflow(x, y) instead of the incorrect x <= y. - Added overflow ops to the polymorphic binary dispatch in translateExpr. - Updated editor syntax files with Bv.SDivOverflow.
This comment was marked as resolved.
This comment was marked as resolved.
MikaelMayer
changed the title
… roundtrip - Implement lhsArray (m[k] := v) in Translate.lean by decomposing nested LHS into base identifier + indices and building map_update expressions - Add decomposeMapUpdate in FormatCore.lean to detect map_update patterns and format them back as lhsArray syntax for proper roundtrip - Add seq_empty grammar entry with explicit type annotation syntax (Sequence.empty<T>()) and corresponding translate/format handling - Add full roundtrip test for datatypes (parentheses issue is resolved) - Add roundtrip tests for lhsArray and Sequence.empty - Regenerate editor syntax files with Sequence.empty - Update AdvancedMaps expected output to match new lhsArray formatting
This comment was marked as resolved.
This comment was marked as resolved.
…tprogram-does-not-produce-roun
This comment was marked as resolved.
This comment was marked as resolved.
Sorry, something went wrong.
…de, fix docstring - Add separate bv_uneg_overflow grammar entry so UNegOverflow roundtrips correctly (previously both mapped to bv_neg_overflow losing semantics) - Remove dead bv32NegOverflowFunc/bv32NegOverflowOp definitions - Fix decomposeMapUpdate docstring to say single-level instead of nested - Regenerate editor syntax files
MikaelMayer
commented
May 15, 2026
…tprogram-does-not-produce-roun
MikaelMayer
enabled auto-merge
May 15, 2026 20:40
…tprogram-does-not-produce-roun
shigoel
reviewed
May 15, 2026
shigoel
reviewed
May 15, 2026
shigoel
reviewed
May 15, 2026
shigoel
reviewed
May 15, 2026
shigoel
reviewed
May 15, 2026
shigoel
previously approved these changes
May 15, 2026
joscoh
previously approved these changes
May 15, 2026
joscoh
left a comment
joscoh
left a comment
Contributor
There was a problem hiding this comment.
Nothing blocking but a few minor comments/questions
The getLFuncCall refactoring processes arguments left-to-right, so variable 'n' is registered as a free variable before the 'top' error is logged, adding freeVars: [n] to the error context.
Cherry-pick the verification tests (seqEmptyPgm, seqEmptyTypesPgm) that exercise Sequence.empty with the SMT solver, covering basic usage and various element types (bool, nested Sequence, Map).
The cherry-pick in 3f3a940 attributed the tests to the wrong author. Removing them so they can be re-added with correct authorship.
Cherry-pick the verification tests (seqEmptyPgm, seqEmptyTypesPgm) that exercise Sequence.empty with the SMT solver, covering basic usage and various element types (bool, nested Sequence, Map). Co-authored-by: Aaron Tomb <aarotomb@amazon.com>
joscoh
reviewed
May 18, 2026
joscoh
approved these changes
May 18, 2026
shigoel
approved these changes
May 18, 2026
MikaelMayer
deleted the
issue-1158-core-formatprogram-does-not-produce-roun
branch
May 18, 2026 16:19
PROgram52bc
added a commit
that referenced
this pull request
May 21, 2026
Reproduction run on htd/smack tip: regenerated all 12 .bpl via SMACK Docker, ran run_pipeline.py with all three backends, verified each known blocker against current source. - Drop FormatCore.lean blocker (resolved by PR #1165 / 75e806e). - Refine CBMC structured-body and inout double-collection blockers with current source line numbers and observed error messages; the visible split is 5 (structured-body) vs 7 (inout) on this run. - Document the ProcBodyVerifyCorrect.lean type mismatch surfaced and fixed during this reproduction (3 call sites swapping proc.body for the destructured ss). - bugFinding partials remain a characterization, not a bug. Pipeline numbers (deductive 4/7/1, bugFinding 0/11/1, cbmc 0/12) are unchanged from the previous snapshot, so the results table itself is left as-is. Add .gitignore for pipeline-run.log and the local blocker scratch file.
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
4 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.
Fixes #1158
Supersedes #1036
Summary
Fixes several issues with
Core.formatProgramthat prevented round-trip parsing:inline functionformatted without space — Theinlinegrammar op now includes a trailing space, preventinginlinefunctionconcatenation. The formatter also now emits theinlineattribute when present on functions.Quantifier variable names — The formatter now uses the
prettyNamefield fromLExpr.quantinstead of generating__qNnames, preserving the original variable names through formatting.Overflow predicates — Added grammar entries, formatter handling, parser entries, and Factory operations for all bitvector overflow predicates (
SNegOverflow,UNegOverflow,SAddOverflow,SSubOverflow,SMulOverflow,SDivOverflow,UAddOverflow,USubOverflow,UMulOverflow).SNegOverflowandUNegOverflowuse distinct grammar entries (Bv.SNegOverflow/Bv.UNegOverflow) to preserve their different semantics through roundtrip. The translate direction correctly dispatches overflow ops by type parameter (bv1/bv8/bv16/bv32/bv64), logging an error for unsupported widths.Array assignment (
lhsArray) — Implementedm[k] := vtranslation in both directions: the parser decomposes nested LHS into base identifier + indices and buildsmap_updateexpressions; the formatter detects themap_update(var, idx, val)pattern and produceslhsArraysyntax.Sequence.empty— Added grammar entry with explicit type annotation syntax (Sequence.empty<int>()), plus translate and format handling, resolving the 0-ary polymorphic function limitation for this operation. Includes solver verification tests (cherry-picked from feat(core): Add Sequence.empty<T>() syntax for creating empty sequences #1036) covering basic usage and various element types.Datatype roundtrip — Verified that datatype formatting roundtrips correctly (the extra-parentheses issue noted earlier is resolved).
Roundtrip test infrastructure — Added
RoundtripTest.leanthat verifies parse → format → re-parse → re-format produces stable output for types, functions, procedures, inline functions, parameterized type arguments, datatypes, array assignments, andSequence.empty.getLFuncCallreuse — RefactoredlappToExpranddecomposeMapUpdateto usegetLFuncCallfor decomposing nested applications, reducing code duplication with the existing utility.Testing
Remaining limitations