Skip to content

Conversation

@langston-barrett
Copy link
Contributor

@langston-barrett langston-barrett commented Jan 14, 2026

Fixes #1138.

While this PR adds lines overall, a large chunk of that is identity cases in pattern matches that are included for the sake of future-proofing those cases. Fundamentally, this is a significant simplification.

Some improvements to the Cast module that were enabled by this change:

  • A type family that specifies the sorts of casts that are performed
  • Make all functions total
  • Separate casts to and from the Crucible-LLVM ABI

One breaking change: Crucible-LLVM S-expression files now have to use the exact signature of the underlying override. See the changes to tests for examples of this breakage. Not a huge deal, as the S-expression syntax is mostly developer-facing.

After this change, it would be feasible to completely remove the quasiquoters. I haven't done that in this PR, but would be happy to do so if requested. It might be nice to instead move them to the type level as quasiquoters for LLVMOverride p sym ext args ret where args and ret are determined by their LLVM types.

@langston-barrett

This comment was marked as resolved.

@langston-barrett langston-barrett force-pushed the rm-llvm-decl branch 3 times, most recently from 89653bd to 19c0c38 Compare January 15, 2026 18:08
@langston-barrett
Copy link
Contributor Author

langston-barrett commented Jan 16, 2026

Status: I'm adapting GREASE to these changes to make sure they work in practice.

[EDIT]: See GaloisInc/grease#525

@langston-barrett langston-barrett marked this pull request as ready for review January 16, 2026 21:09
Copy link
Contributor

@RyanGlScott RyanGlScott left a comment

Choose a reason for hiding this comment

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

Do you envision these changes being breaking to most downstream consumers? (I mainly ask this in a SAW context, since we are in the middle of planning new releases soon.)

After this change, it would be feasible to completely remove the quasiquoters. I haven't done that in this PR, but would be happy to do so if requested.

That is an interesting idea, although I do like the fact that the quasiquoter syntax is much more terse than what the equivalent Haskell code would be. As such, I'm a bit on the fence about this idea. Perhaps we could discuss this in a separate issue?

@langston-barrett
Copy link
Contributor Author

Do you envision these changes being breaking to most downstream consumers?

Only the ones (like crucible-llvm-syntax or GREASE) that use the S-expression syntax. I would expect that SAW, like Crux-LLVM, will require no changes. That being said, I'd prefer to delay merging until the SAW release is complete just in case.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

Projects

None yet

Development

Successfully merging this pull request may close these issues.

llvm: Remove the LLVM declaration from LLVMOverride

3 participants