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

Update to the latest crucible version

Browse Source 
The llvm memory model was extended with better diagnostics and configurable
handling of undefined behavior.  macaw-symbolic uses no undefined behavior
checking, as those operations are only undefined in C.
This commit is contained in:
Tristan Ravitch 2019-01-11 23:01:07 -08:00
parent 7b57ac0c34
commit 379f89ee78
6 changed files with 10 additions and 7 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
deps/crucible vendored

@ -1 +1 @@
Subproject commit ca9173d2ca5ffdf55750d676e9e67c297b38d377 Subproject commit 284cda6bf9f85ae2df30cdf41099948504c34463

2
deps/flexdis86 vendored

@ -1 +1 @@
Subproject commit 5c4453b0b2c89af2267174bf06b486a9dd6c57a2 Subproject commit 2ac3d616996885f93b66c870520381cb09e783ca

2
deps/llvm-pretty vendored

@ -1 +1 @@
Subproject commit e05cf3195b0938961cb0d8ecf4b7a4821f0d2673 Subproject commit 4690fa103c6ce4d13fb659f0ac76b6c059157280

2
deps/parameterized-utils vendored

@ -1 +1 @@
Subproject commit 045e90c564c7839667ff92274d442a343b76d168 Subproject commit fac47a2a783cd885bdabfce026a5e7880be11537

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

@ -396,7 +396,9 @@ doPtrEq = ptrOp $ \sym mem w xPtr xBits yPtr yBits x y ->
do okP1 <- isValidPtr sym mem w x do okP1 <- isValidPtr sym mem w x
okP2 <- isValidPtr sym mem w y okP2 <- isValidPtr sym mem w y
ok <- andPred sym okP1 okP2 ok <- andPred sym okP1 okP2
endCaseCheck ok "Comparing invalid pointers" =<< ptrEq sym nw x y (p1, p2) <- ptrEq sym nw x y
ps <- andPred sym p1 p2
endCaseCheck ok "Comparing invalid pointers" ps
] ]
doReadMem :: doReadMem ::

5
symbolic/src/Data/Macaw/Symbolic/Memory.hs
View File

@ -110,6 +110,7 @@ import qualified Data.Macaw.Memory.Permissions as MMP
import qualified Lang.Crucible.Backend as CB import qualified Lang.Crucible.Backend as CB
import qualified Lang.Crucible.LLVM.DataLayout as CLD import qualified Lang.Crucible.LLVM.DataLayout as CLD
import qualified Lang.Crucible.LLVM.MemModel as CL import qualified Lang.Crucible.LLVM.MemModel as CL
import qualified Lang.Crucible.LLVM.UndefinedBehavior as UB
import qualified Lang.Crucible.Simulator as CS import qualified Lang.Crucible.Simulator as CS
import qualified Lang.Crucible.Types as CT import qualified Lang.Crucible.Types as CT
import qualified What4.Interface as WI import qualified What4.Interface as WI
@ -365,7 +366,7 @@ mapBitvectorToLLVMPointer mpt@(MemPtrTable im _) sym mem offsetVal =
allocBase <- WI.bvLit sym wrep (MC.memWordToUnsigned (allocationBase alloc)) allocBase <- WI.bvLit sym wrep (MC.memWordToUnsigned (allocationBase alloc))
allocationOffset <- WI.bvSub sym offsetVal allocBase allocationOffset <- WI.bvSub sym offsetVal allocBase
let ?ptrWidth = wrep let ?ptrWidth = wrep
Just <$> CL.doPtrAddOffset sym mem (allocationPtr alloc) allocationOffset Just <$> CL.doPtrAddOffset sym (Just UB.laxConfig) mem (allocationPtr alloc) allocationOffset
[] -> return Nothing [] -> return Nothing
_ -> error ("Overlapping allocations for pointer: " ++ show (WI.printSymExpr offsetVal)) _ -> error ("Overlapping allocations for pointer: " ++ show (WI.printSymExpr offsetVal))
Nothing -> do Nothing -> do
@ -416,7 +417,7 @@ staticRegionMuxTree (MemPtrTable im _) sym mem offsetVal = do
allocBase <- WI.bvLit sym rep (MC.memWordToUnsigned (allocationBase alloc)) allocBase <- WI.bvLit sym rep (MC.memWordToUnsigned (allocationBase alloc))
allocationOffset <- WI.bvSub sym offsetVal allocBase allocationOffset <- WI.bvSub sym offsetVal allocBase
let ?ptrWidth = rep let ?ptrWidth = rep
thisPtr <- CL.doPtrAddOffset sym mem (allocationPtr alloc) allocationOffset thisPtr <- CL.doPtrAddOffset sym (Just UB.laxConfig) mem (allocationPtr alloc) allocationOffset
CL.muxLLVMPtr sym p thisPtr f CL.muxLLVMPtr sym p thisPtr f
addMuxForRegion f (interval, alloc) = do addMuxForRegion f (interval, alloc) = do
case interval of case interval of