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

symbolic: Add special cases for null pointers in doPtrEq (#165)

Browse Source
This commit is contained in:
Sam Breese 2020-10-08 14:38:46 -04:00 committed by GitHub
parent cbc7a3ca31
commit 00d8530255
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
1 changed files with 18 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

18
symbolic/src/Data/Macaw/Symbolic/MemOps.hs
View File

@ -441,6 +441,18 @@ isValidPtr sym mem w p =
let ?ptrWidth = M.addrWidthNatRepr w let ?ptrWidth = M.addrWidthNatRepr w
isValidPointer sym p mem isValidPointer sym p mem
isNullPtr ::
(IsSymInterface sym) =>
sym ->
M.AddrWidthRepr w ->
LLVMPtr sym w ->
IO (Pred sym)
isNullPtr sym w p =
do LeqProof <- pure $ addrWidthIsPos w
LeqProof <- pure $ addrWidthAtLeast16 w
let ?ptrWidth = M.addrWidthNatRepr w
Mem.ptrIsNull sym Mem.PtrWidth p
doPtrMux :: Pred sym -> PtrOp sym w (LLVMPtr sym w) doPtrMux :: Pred sym -> PtrOp sym w (LLVMPtr sym w)
doPtrMux c = ptrOp $ \sym _ w xPtr xBits yPtr yBits x y -> doPtrMux c = ptrOp $ \sym _ w xPtr xBits yPtr yBits x y ->
do both_bits <- andPred sym xBits yBits do both_bits <- andPred sym xBits yBits
@ -652,6 +664,9 @@ doPtrEq :: PtrOp sym w (RegValue sym BoolType)
doPtrEq = ptrOp $ \sym mem w xPtr xBits yPtr yBits x y -> doPtrEq = ptrOp $ \sym mem w xPtr xBits yPtr yBits x y ->
do both_bits <- andPred sym xBits yBits do both_bits <- andPred sym xBits yBits
both_ptrs <- andPred sym xPtr yPtr both_ptrs <- andPred sym xPtr yPtr
xNull <- isNullPtr sym w x
yNull <- isNullPtr sym w y
both_null <- andPred sym xNull yNull
undef <- mkUndefinedBool sym "ptr_eq" undef <- mkUndefinedBool sym "ptr_eq"
let nw = M.addrWidthNatRepr w let nw = M.addrWidthNatRepr w
cases sym (binOpLabel "ptr_eq" x y) itePred (Just undef) cases sym (binOpLabel "ptr_eq" x y) itePred (Just undef)
@ -662,6 +677,9 @@ doPtrEq = ptrOp $ \sym mem w xPtr xBits yPtr yBits x y ->
ok <- andPred sym okP1 okP2 ok <- andPred sym okP1 okP2
ps <- ptrEq sym nw x y ps <- ptrEq sym nw x y
endCaseCheck ok "Comparing invalid pointers" ps endCaseCheck ok "Comparing invalid pointers" ps
, both_null ~> endCase (truePred sym)
, xNull ~> endCase (falsePred sym)
, yNull ~> endCase (falsePred sym)
] ]
getEnd :: MemImpl sym -> M.Endianness getEnd :: MemImpl sym -> M.Endianness