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

Add write operation

Browse Source
This commit is contained in:
Iavor Diatchki 2018-02-12 10:28:39 -08:00
parent b57483b1f8
commit ad5f7ceddb
2 changed files with 42 additions and 15 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

24
symbolic/src/Data/Macaw/Symbolic.hs
View File

@ -290,19 +290,21 @@ execMacawStmtExtension ::
EvalStmtFunc (MacawStmtExtension arch) MacawSimulatorState sym (MacawExt arch)
execMacawStmtExtension archStmtFn s0 st =
case s0 of
MacawReadMem mvar w mr x -> doReadMem st mvar w mr x
MacawReadMem mvar w mr x -> doReadMem st mvar w mr x
MacawCondReadMem mvar w mr p x d -> doCondReadMem st mvar w mr p x d
MacawWriteMem mvar w mr x v -> doWriteMem st mvar w mr x v
MacawFreshSymbolic{} -> undefined
MacawCall{} -> undefined
MacawArchStmtExtension s -> archStmtFn s st
MacawWriteMem mvar w mr x v -> doWriteMem st mvar w mr x v
PtrEq mvar w x y -> doPtrEq st mvar w x y
PtrLt mvar w x y -> doPtrLt st mvar w x y
PtrLeq mvar w x y -> doPtrLeq st mvar w x y
PtrMux mvar w c x y -> doPtrMux (C.regValue c) st mvar w x y
PtrAdd mvar w x y -> doPtrAdd st mvar w x y
PtrSub mvar w x y -> doPtrSub st mvar w x y
MacawFreshSymbolic{} -> error "XXX: FreshSymbolic"
MacawCall{} -> error "XXX: MacawCall"
MacawArchStmtExtension s -> archStmtFn s st
PtrEq mvar w x y -> doPtrEq st mvar w x y
PtrLt mvar w x y -> doPtrLt st mvar w x y
PtrLeq mvar w x y -> doPtrLeq st mvar w x y
PtrMux mvar w c x y -> doPtrMux (C.regValue c) st mvar w x y
PtrAdd mvar w x y -> doPtrAdd st mvar w x y
PtrSub mvar w x y -> doPtrSub st mvar w x y
-- | Return macaw extension evaluation functions.

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

@ -21,7 +21,7 @@ module Data.Macaw.Symbolic.MemOps
, doWriteMem
) where
import Control.Lens((^.))
import Control.Lens((^.),(&),(%~))
import Lang.Crucible.Simulator.ExecutionTree
( CrucibleState
@ -32,7 +32,7 @@ import Lang.Crucible.Simulator.ExecutionTree
)
import Lang.Crucible.Simulator.RegMap(RegEntry,regValue)
import Lang.Crucible.Simulator.RegValue(RegValue)
import Lang.Crucible.Simulator.GlobalState(lookupGlobal)
import Lang.Crucible.Simulator.GlobalState(lookupGlobal,insertGlobal)
import Lang.Crucible.Simulator.SimError(SimErrorReason(AssertFailureSimError))
import Lang.Crucible.CFG.Common(GlobalVar)
import Lang.Crucible.Types
@ -43,6 +43,7 @@ import Lang.Crucible.LLVM.MemModel
, LLVMVal(LLVMValInt)
, loadRaw
, loadRawWithCondition
, storeRaw
)
import Lang.Crucible.LLVM.MemModel.Pointer
( llvmPointerView, muxLLVMPtr, llvmPointer_bv, ptrAdd, ptrSub, ptrEq
@ -227,18 +228,34 @@ doCondReadMem st mvar w (BVMemRepr bytes endian) cond0 ptr def0 =
return (a,st)
doWriteMem ::
(IsSymInterface sym, 16 <= ptrW) =>
CrucibleState s sym ext rtp blocks r ctx {- ^ Simulator state -} ->
GlobalVar Mem -> {- ^ Memory model -}
NatRepr ptrW {- ^ Width of ptr -} ->
MemRepr ty {- ^ What/how we are reading -} ->
MemRepr ty {- ^ What/how we are writing -} ->
RegEntry sym (LLVMPointerType ptrW) {- ^ Pointer -} ->
RegEntry sym (ToCrucibleType ty) {- ^ Write this value -} ->
IO ( RegValue sym UnitType
, CrucibleState s sym ext rtp blocks r ctx
)
doWriteMem = undefined
doWriteMem st mvar w (BVMemRepr bytes endian) ptr val =
do mem <- getMem st mvar
checkEndian mem endian
let sym = stateSymInterface st
ty = bitvectorType (toBytes (widthVal bytes))
LeqProof <- return (lemma1_16 w)
LeqProof <- return (leqMulPos (knownNat @8) bytes)
let ?ptrWidth = w
let v0 = regValue val
v = LLVMValInt (ptrBase v0) (asBits v0)
mem1 <- storeRaw sym mem (regValue ptr) ty v
return ((), setMem st mvar mem1)
@ -302,6 +319,14 @@ getMem st mvar =
Just mem -> return mem
Nothing -> fail ("Global heap value not initialized: " ++ show mvar)
setMem :: CrucibleState s sym ext rtp blocks r ctx ->
GlobalVar Mem ->
MemImpl sym ->
CrucibleState s sym ext rtp blocks r ctx
setMem st mvar mem =
st & stateTree . actFrame . gpGlobals %~ insertGlobal mvar mem
-- | Define an operation by cases.
cases ::
(IsSymInterface sym) =>