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

Added TestBit, done (for now) with crucible expressions

Browse Source
This commit is contained in:
Ben Selfridge 2017-10-10 14:51:25 -07:00
parent d0fac23418
commit 064d0c4e8d
1 changed files with 4 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
macaw-ppc/src/Data/Macaw/PPC/Semantics/TH.hs
View File

@ -154,6 +154,10 @@ crucAppToExpr (S.BVNeg w bv) = do
bvVal <- addElt bv bvVal <- addElt bv
bvComp <- addExpr (AppExpr (M.BVComplement w bvVal)) bvComp <- addExpr (AppExpr (M.BVComplement w bvVal))
return $ AppExpr (M.BVAdd w bvComp (M.mkLit w 1)) return $ AppExpr (M.BVAdd w bvComp (M.mkLit w 1))
crucAppToExpr (S.BVTestBit idx bv) = AppExpr <$> do
M.BVTestBit
<$> addExpr (ValueExpr (M.BVValue (S.bvWidth bv) (fromIntegral idx)))
<*> addElt bv
crucAppToExpr (S.BVAdd repr bv1 bv2) = AppExpr <$> do crucAppToExpr (S.BVAdd repr bv1 bv2) = AppExpr <$> do
M.BVAdd <$> pure repr <*> addElt bv1 <*> addElt bv2 M.BVAdd <$> pure repr <*> addElt bv1 <*> addElt bv2
crucAppToExpr (S.BVMul repr bv1 bv2) = AppExpr <$> do crucAppToExpr (S.BVMul repr bv1 bv2) = AppExpr <$> do