From cea41149ce5929d098ee50ef12936819ffb18f4d Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Tue, 21 Dec 2021 18:00:46 -0500 Subject: [PATCH] Reference #338 in the FIXMEs adjacent to uses of noAlignment --- src/SAWScript/Crucible/LLVM/Override.hs | 8 ++++---- src/SAWScript/X86Spec.hs | 12 ++++++------ 2 files changed, 10 insertions(+), 10 deletions(-) diff --git a/src/SAWScript/Crucible/LLVM/Override.hs b/src/SAWScript/Crucible/LLVM/Override.hs index 88a04eee87..337ad7b284 100644 --- a/src/SAWScript/Crucible/LLVM/Override.hs +++ b/src/SAWScript/Crucible/LLVM/Override.hs @@ -1467,7 +1467,7 @@ matchPointsToValue opts sc cc spec prepost loc maybe_cond ptr val = mem <- readGlobal $ Crucible.llvmMemVar $ ccLLVMContext cc - let alignment = Crucible.noAlignment -- default to byte alignment (FIXME) + let alignment = Crucible.noAlignment -- default to byte alignment (FIXME, see #338) case val of ConcreteSizeValue val' -> @@ -1566,7 +1566,7 @@ matchPointsToBitfieldValue opts sc cc spec prepost loc ptr bfIndex val = mem <- readGlobal $ Crucible.llvmMemVar $ ccLLVMContext cc - let alignment = Crucible.noAlignment -- default to byte alignment (FIXME) + let alignment = Crucible.noAlignment -- default to byte alignment (FIXME, see #338) -- Unlike in matchPointsToValue, we compute the MemTy/StorageType not from -- the RHS value, but from the BitfieldIndex. This is because we need to @@ -2037,7 +2037,7 @@ storePointsToValue :: storePointsToValue opts cc env tyenv nameEnv base_mem maybe_cond ptr val maybe_invalidate_msg = do let sym = cc ^. ccBackend - let alignment = Crucible.noAlignment -- default to byte alignment (FIXME) + let alignment = Crucible.noAlignment -- default to byte alignment (FIXME, see #338) smt_array_memory_model_enabled <- W4.getOpt =<< W4.getOptionSetting enableSMTArrayMemoryModel (W4.getConfiguration sym) @@ -2124,7 +2124,7 @@ storePointsToBitfieldValue :: storePointsToBitfieldValue opts cc env tyenv nameEnv base_mem ptr bfIndex val = do let sym = cc ^. ccBackend - let alignment = Crucible.noAlignment -- default to byte alignment (FIXME) + let alignment = Crucible.noAlignment -- default to byte alignment (FIXME, see #338) smt_array_memory_model_enabled <- W4.getOpt =<< W4.getOptionSetting enableSMTArrayMemoryModel (W4.getConfiguration sym) diff --git a/src/SAWScript/X86Spec.hs b/src/SAWScript/X86Spec.hs index b6c29adc78..badae2c0d0 100644 --- a/src/SAWScript/X86Spec.hs +++ b/src/SAWScript/X86Spec.hs @@ -510,7 +510,7 @@ setLoc l = let lty = llvmBytes w ty = locRepr l val <- packMemValue sym lty ty v - let alignment = noAlignment -- default to byte-aligned (FIXME) + let alignment = noAlignment -- default to byte-aligned (FIXME, see #338) mem1 <- storeConstRaw sym mem loc lty alignment val return s { stateMem = mem1 } @@ -885,7 +885,7 @@ setCryPost opts s (_nm,p) = do let ?ptrWidth = knownNat loc <- adjustPtr sym mem ptrV (bytesToInteger (i *. u)) val <- packMemValue sym llT cruT v - let alignment = noAlignment -- default to byte-aligned (FIXME) + let alignment = noAlignment -- default to byte-aligned (FIXME, see #338) storeConstRaw sym mem loc llT alignment val let cur = Proxy @p @@ -933,7 +933,7 @@ allocate sym ar s = do let ?ptrWidth = knownNat @64 let szInt = bytesToInteger (uncurry (*.) (areaSize ar)) sz <- bvLit sym knownNat (BV.mkBV knownNat szInt) - let alignment = noAlignment -- default to byte-aligned (FIXME) + let alignment = noAlignment -- default to byte-aligned (FIXME, see #338) (base,mem) <- doMalloc sym HeapAlloc mut (areaName ar) (stateMem s) sz alignment ptr <- adjustPtr sym mem base (bytesToInteger (areaPtr ar)) return (base,ptr,mem) @@ -960,7 +960,7 @@ fillFresh sym ptrOk p u todo mem = val <- packMemValue sym lty ty =<< freshVal sym ty ptrOk nm -- Here we use the write that ignore mutability. -- This is because we are writinging initialization code. - let alignment = noAlignment -- default to byte-aligned (FIXME) + let alignment = noAlignment -- default to byte-aligned (FIXME, see #338) mem1 <- storeConstRaw sym mem p lty alignment val p1 <- adjustPtr sym mem1 p elS fillFresh sym ptrOk p1 u more mem1 @@ -1070,7 +1070,7 @@ setupGlobals opts gs fs s let ?ptrWidth = knownNat @64 sz <- bvLit sym knownNat (BV.mkBV knownNat size) - let alignment = noAlignment -- default to byte-aligned (FIXME) + let alignment = noAlignment -- default to byte-aligned (FIXME, see #338) (p,mem) <- doMalloc sym GlobalAlloc Immutable "Globals" (stateMem s) sz alignment let Just base = asNat (fst (llvmPointerView p)) @@ -1146,7 +1146,7 @@ setupGlobals opts gs fs s z <- natLit sym 0 val <- LLVMValInt z <$> bvLit sym w (BV.mkBV w v) let ?ptrWidth = knownNat - let alignment = noAlignment -- default to byte-aligned (FIXME) + let alignment = noAlignment -- default to byte-aligned (FIXME, see #338) mem1 <- storeConstRaw sym mem p lty alignment val p1 <- adjustPtr sym mem1 p szI return (p1,mem1)