From 32710829f6c44bf0c97eb28f807feb590f404cf3 Mon Sep 17 00:00:00 2001 From: Iavor Diatchki Date: Mon, 5 Mar 2018 13:47:55 -0800 Subject: [PATCH] Use pointer addition, only when the value is not a bit-vector. The other version was getting confusing by the NULL pointer. --- symbolic/src/Data/Macaw/Symbolic/MemOps.hs | 11 +++++++---- 1 file changed, 7 insertions(+), 4 deletions(-) diff --git a/symbolic/src/Data/Macaw/Symbolic/MemOps.hs b/symbolic/src/Data/Macaw/Symbolic/MemOps.hs index 80f112db..93a49abe 100644 --- a/symbolic/src/Data/Macaw/Symbolic/MemOps.hs +++ b/symbolic/src/Data/Macaw/Symbolic/MemOps.hs @@ -135,12 +135,12 @@ doPtrAdd = ptrOp $ \sym mem w xPtr xBits yPtr yBits x y -> , ptr_bits ~> do r <- ptrAdd sym w x (asBits y) ok <- let ?ptrWidth = w in isValidPointer sym r mem - endCaseCheck ok "Invalid result" r + endCaseCheck ok "Invalid result (ptr_bits)" r , bits_ptr ~> do r <- ptrAdd sym w y (asBits x) ok <- let ?ptrWidth = w in isValidPointer sym r mem - endCaseCheck ok "Invalid result" r + endCaseCheck ok "Invalid result (bits_ptr)" r ] @@ -345,10 +345,13 @@ ptrOp k st mvar w x0 y0 = let sym = stateSymInterface st x = regValue x0 y = regValue y0 - xPtr <- let ?ptrWidth = w in isValidPointer sym x mem - yPtr <- let ?ptrWidth = w in isValidPointer sym y mem + -- xPtr <- let ?ptrWidth = w in isValidPointer sym x mem + -- yPtr <- let ?ptrWidth = w in isValidPointer sym y mem xBits <- isBitVec sym x yBits <- isBitVec sym y + + xPtr <- notPred sym xBits + yPtr <- notPred sym yBits a <- k sym mem w xPtr xBits yPtr yBits x y return (a,st)