Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

RFC: crucible-llvm: Don't represent architecture at the type level #1046

Open
wants to merge 1 commit into
base: master
Choose a base branch
from

Conversation

langston-barrett
Copy link
Contributor

It's necessary to represent the pointer width at the type level in order to statically prevent the formation of ill-typed Crucible/What4 expressions. However, there is no similar motivation for representing architectures at the type level.

The previous state of affairs was incoherent in the sense that we always provided an ArchRepr signaling the use of x86, without actually checking that this architecture was in use:

do let archRepr = X86Repr wptr -- FIXME! we should select the architecture based on

We could have fixed this by checking the target triple (functionality recently added to llvm-pretty{,-bc-parser}) and adding constructors for more architectures to ArchRepr, but as discussed above there's no motivation to actually do this.

If we want to move forward with this, we should make a follow-up issue for removing all of the LLVMArch stuff.

It's necessary to represent the pointer width at the type level in order to
statically prevent the formation of ill-typed Crucible/What4 expressions.
However, there is no similar motivation for representing architectures at the
type level.

The previous state of affairs was incoherent in the sense that we always
provided an `ArchRepr` signaling the use of x86, without actually checking
that this architecture was in use:

  https://github.com/GaloisInc/crucible/blob/041975a5ad4200633613ed30df144c3a9d0e9403/crucible-llvm/src/Lang/Crucible/LLVM/Translation/Monad.hs#L113

We could have fixed this by checking the target triple (functionality recently
added to llvm-pretty{,-bc-parser}) and adding constructors for more
architectures to `ArchRepr`, but as discussed above there's no motivation to
actually do this.
@kquick
Copy link
Member

kquick commented Sep 28, 2022

I would like to defer a decision on this until I've had a chance to refresh on the unmerged polyglot work (which needs to be merged, but had type-level impact) to see if this is used at the type level for polyglot.

@langston-barrett
Copy link
Contributor Author

langston-barrett commented Sep 28, 2022

I would like to defer a decision on this until I've had a chance to refresh on the unmerged polyglot work (which needs to be merged, but had type-level impact) to see if this is used at the type level for polyglot.

That sounds fine to me. Could you open an issue with a description of this upcoming feature and a pointer to the implementation as it stands today, and assign it to yourself? That context would help me understand the impact of potential changes like this while that work is pending, and serve as a place to track progress towards merging it.

@langston-barrett
Copy link
Contributor Author

@kquick Any updates on the polyglot work?

@langston-barrett
Copy link
Contributor Author

@kquick Any updates on this?

@langston-barrett
Copy link
Contributor Author

@kquick Are there still plans to merge the polyglot work?

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants