GaloisInc/macaw
1
1
Fork 0
mirror of https://github.com/GaloisInc/macaw.git synced 2024-12-24 06:35:41 +03:00
Code Issues Projects Releases Wiki Activity

Start on writeMem

Browse Source
This commit is contained in:
Iavor Diatchki 2018-02-09 16:59:42 -08:00
parent 1c07b88ae7
commit b57483b1f8
3 changed files with 14 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -292,7 +292,7 @@ execMacawStmtExtension archStmtFn s0 st =
case s0 of
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{} -> undefined
MacawWriteMem mvar w mr x v -> doWriteMem st mvar w mr x v
MacawFreshSymbolic{} -> undefined
MacawCall{} -> undefined
MacawArchStmtExtension s -> archStmtFn s st

BIN
symbolic/src/Data/Macaw/Symbolic/.CrucGen.hs.swp
View File

Binary file not shown.

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

@ -18,6 +18,7 @@ module Data.Macaw.Symbolic.MemOps
, doPtrLeq
, doReadMem
, doCondReadMem
, doWriteMem
) where
import Control.Lens((^.))
@ -226,6 +227,18 @@ 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 -} ->
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