Skip to content

Add metadata to more places in Laurel#396

Merged
keyboardDrummer merged 21 commits intostrata-org:mainfrom
keyboardDrummer:laurelMetadata
Feb 11, 2026
Merged

Add metadata to more places in Laurel#396
keyboardDrummer merged 21 commits intostrata-org:mainfrom
keyboardDrummer:laurelMetadata

Conversation

@keyboardDrummer
Copy link
Contributor

@keyboardDrummer keyboardDrummer commented Feb 9, 2026 •
edited
Loading

Changes

  • Add metadata to many more places in Laurel. For example, preconditions and postconditions are now given a metadata and that is propagated to Core
  • Made it an internal error if diagnostics are reported for which no source location is known
  • Remove the default empty value for the metadata of Procedure.Check

Testing

  • Turned on tests for preconditions and postconditions, although the precondition test does not report errors correctly due to Core reporting them on the precondition instead of on the call, and with an incorrect message.

By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.

@keyboardDrummer keyboardDrummer requested review from andrewmwells-amazon, atomb and joscoh and removed request for atomb February 9, 2026 15:00
@keyboardDrummer keyboardDrummer marked this pull request as ready for review February 9, 2026 15:01
@keyboardDrummer keyboardDrummer requested a review from a team as a code owner February 9, 2026 15:01
@keyboardDrummer
Copy link
Contributor Author

keyboardDrummer commented Feb 9, 2026 •
edited
Loading

@atomb the codebase contains many pieces like md : MetaData Expression := .empty. I think we should remove the defaults because anytime an AST node is created on which an error could be reported, it is a bug if there is no source location information available. The default empty metadata prevents the programmer from having to think about whether metadata is available.

@keyboardDrummer keyboardDrummer mentioned this pull request Feb 9, 2026
Merged
@keyboardDrummer keyboardDrummer requested review from MikaelMayer and removed request for andrewmwells-amazon February 9, 2026 21:36
MikaelMayer
MikaelMayer reviewed Feb 10, 2026
View reviewed changes
Copy link
Contributor

@MikaelMayer MikaelMayer left a comment •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

One small change to consider.

fabiomadge added a commit that referenced this pull request Feb 10, 2026
@fabiomadge
LaurelToCoreTranslator: prove termination for translateType
0025b01 
Add HighTypeMd.sizeOf_val_lt lemma and use it to prove translateType
terminates. The remaining partial defs recurse through List StmtExprMd
which requires the same sizeOf bridging pattern that is a known issue
across the codebase (see PR #396).
joscoh
joscoh reviewed Feb 10, 2026
View reviewed changes
@keyboardDrummer keyboardDrummer mentioned this pull request Feb 11, 2026
Merged
@keyboardDrummer keyboardDrummer added this pull request to the merge queue Feb 11, 2026
Merged via the queue into strata-org:main with commit bab0508 Feb 11, 2026
9 checks passed
@keyboardDrummer keyboardDrummer deleted the laurelMetadata branch February 11, 2026 16:17
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@MikaelMayer MikaelMayer MikaelMayer approved these changes

@joscoh joscoh joscoh approved these changes

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@keyboardDrummer @MikaelMayer @joscoh

Comments