GaloisInc/macaw
1
1
Fork 0
mirror of https://github.com/GaloisInc/macaw.git synced 2024-11-26 09:22:20 +03:00
Code Issues Projects Releases Wiki Activity

symbolic: Fix PackBits and UnpackBits (#166)

Browse Source
This commit is contained in:
Sam Breese 2020-10-12 14:20:05 -04:00 committed by GitHub
parent 34e7394c14
commit 3a071e317b
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
1 changed files with 3 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
symbolic/src/Data/Macaw/Symbolic/Bitcast.hs
View File

@ -67,8 +67,8 @@ doBitcast sym x eqPr =
extY <- bvZext sym outW =<< MM.projectLLVM_bv sym y extY <- bvZext sym outW =<< MM.projectLLVM_bv sym y
shiftAmt <- bvLit sym outW (BV.mkBV outW i) shiftAmt <- bvLit sym outW (BV.mkBV outW i)
r' <- bvOrBits sym r =<< bvShl sym extY shiftAmt r' <- bvOrBits sym r =<< bvShl sym extY shiftAmt
pure (i+1,r') pure (i+intValue w,r')
(_,r) <- F.foldlM doPack (1,extH) rest (_,r) <- F.foldlM doPack (intValue w,extH) rest
MM.llvmPointer_bv sym r MM.llvmPointer_bv sym r
M.UnpackBits n w -> do M.UnpackBits n w -> do
let inW = natMultiply n w let inW = natMultiply n w
@ -76,7 +76,7 @@ doBitcast sym x eqPr =
LeqProof <- pure $ plus1LeqDbl n w LeqProof <- pure $ plus1LeqDbl n w
xbv <- MM.projectLLVM_bv sym x xbv <- MM.projectLLVM_bv sym x
V.generateM (fromIntegral (natValue n)) $ \i -> do V.generateM (fromIntegral (natValue n)) $ \i -> do
shiftAmt <- bvLit sym inW (BV.mkBV inW (toInteger i)) shiftAmt <- bvLit sym inW (BV.mkBV inW (toInteger i * intValue w))
MM.llvmPointer_bv sym =<< bvTrunc sym w =<< bvLshr sym xbv shiftAmt MM.llvmPointer_bv sym =<< bvTrunc sym w =<< bvLshr sym xbv shiftAmt
M.FromFloat f -> do M.FromFloat f -> do
Refl <- pure $ checkMacawFloatEq f Refl <- pure $ checkMacawFloatEq f