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.

Sign up for GitHub

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

Jump to bottom

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
Open

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

wants to merge 1 commit into from

Commits on Sep 28, 2022

  1. crucible-llvm: Type-level pointer width, rather than architecture 

    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.
    @langston-barrett
    langston-barrett committed Sep 28, 2022
    Configuration menu
    Copy the full SHA
    2bc5e25 View commit details
    Browse the repository at this point in the history