GaloisInc/macaw
1
1
Fork 0
mirror of https://github.com/GaloisInc/macaw.git synced 2024-12-18 03:21:49 +03:00
Code Issues Projects Releases Wiki Activity

Add BVUrem App support.

Browse Source
This commit is contained in:
Kevin Quick 2018-02-21 20:39:57 -08:00
parent 9200b2bcdd
commit 6a0a59e298
No known key found for this signature in database
GPG Key ID: E6D7733599CC0A21
1 changed files with 10 additions and 5 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

15
base/src/Data/Macaw/CFG/App.hs
View File

@ -82,6 +82,9 @@ data App (f :: Type -> *) (tp :: Type) where
-- Multiply two numbers -- Multiply two numbers
BVMul :: (1 <= n) => !(NatRepr n) -> !(f (BVType n)) -> !(f (BVType n)) -> App f (BVType n) BVMul :: (1 <= n) => !(NatRepr n) -> !(f (BVType n)) -> !(f (BVType n)) -> App f (BVType n)
-- Divide two numbers and get the remainder (i.e. mod)
BVUrem :: (1 <= n) => !(NatRepr n) -> !(f (BVType n)) -> !(f (BVType n)) -> App f (BVType n)
-- Unsigned less than or equal. -- Unsigned less than or equal.
BVUnsignedLe :: (1 <= n) => !(f (BVType n)) -> !(f (BVType n)) -> App f BoolType BVUnsignedLe :: (1 <= n) => !(f (BVType n)) -> !(f (BVType n)) -> App f BoolType
@ -261,6 +264,7 @@ ppAppA pp a0 =
BVSub _ x y -> sexprA "bv_sub" [ pp x, pp y ] BVSub _ x y -> sexprA "bv_sub" [ pp x, pp y ]
BVSbb _ x y b -> sexprA "bv_sbb" [ pp x, pp y, pp b ] BVSbb _ x y b -> sexprA "bv_sbb" [ pp x, pp y, pp b ]
BVMul _ x y -> sexprA "bv_mul" [ pp x, pp y ] BVMul _ x y -> sexprA "bv_mul" [ pp x, pp y ]
BVUrem _ x y -> sexprA "bv_urem" [ pp x, pp y ]
BVUnsignedLt x y -> sexprA "bv_ult" [ pp x, pp y ] BVUnsignedLt x y -> sexprA "bv_ult" [ pp x, pp y ]
BVUnsignedLe x y -> sexprA "bv_ule" [ pp x, pp y ] BVUnsignedLe x y -> sexprA "bv_ule" [ pp x, pp y ]
BVSignedLt x y -> sexprA "bv_slt" [ pp x, pp y ] BVSignedLt x y -> sexprA "bv_slt" [ pp x, pp y ]
@ -307,11 +311,12 @@ instance HasRepr (App f) TypeRepr where
NotApp{} -> knownRepr NotApp{} -> knownRepr
XorApp{} -> knownRepr XorApp{} -> knownRepr
BVAdd w _ _ -> BVTypeRepr w BVAdd w _ _ -> BVTypeRepr w
BVAdc w _ _ _ -> BVTypeRepr w BVAdc w _ _ _ -> BVTypeRepr w
BVSub w _ _ -> BVTypeRepr w BVSub w _ _ -> BVTypeRepr w
BVSbb w _ _ _ -> BVTypeRepr w BVSbb w _ _ _ -> BVTypeRepr w
BVMul w _ _ -> BVTypeRepr w BVMul w _ _ -> BVTypeRepr w
BVUrem w _ _ -> BVTypeRepr w
BVUnsignedLt{} -> knownRepr BVUnsignedLt{} -> knownRepr
BVUnsignedLe{} -> knownRepr BVUnsignedLe{} -> knownRepr