GaloisInc/macaw
1
1
Fork 0
mirror of https://github.com/GaloisInc/macaw.git synced 2024-12-02 23:43:52 +03:00
Code Issues Projects Releases Wiki Activity

Definition for Unpack

Browse Source
This commit is contained in:
Iavor Diatchki 2018-03-27 10:46:47 -07:00
parent f54f0a13ba
commit 0f3b97b8bf
1 changed files with 7 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

7
x86_symbolic/src/Data/Macaw/X86/Crucible.hs
View File

@ -207,6 +207,12 @@ pureSem sym fn =
_ -> fail "Unepected size for VPCLMULQDQ"
M.VPUnpackLQDQ -> vecOp2 sym LittleEndian w (knownNat @64) x y $
\xs ys -> let n = V.length xs
in case mul2Plus n of
Refl -> V.take n (V.interlieve xs ys)
M.VAESEnc
| Just Refl <- testEquality w n128 ->
do let f = fnAesEnc (symFuns sym)
@ -247,6 +253,7 @@ pureSem sym fn =
case mulCancelR elNum (V.length xs) elSz of
Refl -> V.insertAt i e xs
semPointwise :: (1 <= w) =>
M.AVXPointWiseOp2 -> NatRepr w ->
E sym (BVType w) -> E sym (BVType w) -> E sym (BVType w)