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

Implement variant of crucible_alloc with user-specified alignment #633

Closed
brianhuffman opened this issue Jan 23, 2020 · 1 comment
Closed
Labels
subsystem: crucible-llvm Issues related to LLVM bitcode verification with crucible-llvm type: enhancement Issues describing an improvement to an existing feature or capability

Comments

@brianhuffman
Copy link
Contributor

In a CrucibleSetup block, crucible_alloc always chooses an alignment based on the maximum required for any primitive type (usually 8 bytes).

doAlloc ::
(?lc :: Crucible.TypeContext, Crucible.HasPtrWidth (Crucible.ArchWidth arch)) =>
LLVMCrucibleContext arch ->
LLVMAllocSpec ->
StateT MemImpl IO (LLVMPtr (Crucible.ArchWidth arch))
doAlloc cc (LLVMAllocSpec mut _memTy sz loc) = StateT $ \mem ->
do let sym = cc^.ccBackend
let dl = Crucible.llvmDataLayout ?lc
sz' <- W4.bvLit sym Crucible.PtrWidth $ Crucible.bytesToInteger sz
let alignment = Crucible.maxAlignment dl -- Use the maximum alignment required for any primitive type (FIXME?)
let l = show (W4.plSourceLoc loc)
liftIO $
Crucible.doMalloc sym Crucible.HeapAlloc mut l mem sz' alignment

However, sometimes C/LLVM functions might require more-aligned pointers. E.g. if a type is declared with __attribute__((aligned(64))), then dereferencing a pointer to it would require 64-byte alignment. (Thanks to @andreistefanescu for bringing this to my attention.)

To support specifying and verifying such code, we should implement a variant of crucible_alloc called something like crucible_alloc_aligned that takes an extra numeric argument for the desired alignment. This should be pretty easy to implement, as the Crucible/LLVM memory model allows arbitrary alignments to be specified for each allocation.

@brianhuffman brianhuffman added type: enhancement Issues describing an improvement to an existing feature or capability subsystem: crucible-llvm Issues related to LLVM bitcode verification with crucible-llvm labels Jan 23, 2020
@brianhuffman
Copy link
Contributor Author

Implemented by PR #637.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
subsystem: crucible-llvm Issues related to LLVM bitcode verification with crucible-llvm type: enhancement Issues describing an improvement to an existing feature or capability
Projects
None yet
Development

No branches or pull requests

1 participant