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

symbolic: Data type for (mem, mmConf) tuple

Browse Source
This commit is contained in:
Langston Barrett 2024-09-04 15:29:27 -04:00
parent 820401d12e
commit c65ad34343
1 changed files with 11 additions and 5 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

16
symbolic/src/Data/Macaw/Symbolic/Testing.hs
View File

@ -468,7 +468,7 @@ initialMem ::
bak ->
MAI.ArchitectureInfo arch ->
MS.ArchVals arch ->
IO (CLM.MemImpl sym, MS.MemModelConfig p sym arch CLM.Mem)
IO (InitialMem p sym arch)
initialMem binfo bak archInfo archVals = do
let endianness = MSMLazy.toCrucibleEndian (MAI.archEndianness archInfo)
(mem, memPtrTbl) <-
@ -479,7 +479,7 @@ initialMem binfo bak archInfo archVals = do
, MS.lookupSyscallHandle = lookupSyscall
, MS.mkGlobalPointerValidityAssertion = validityCheck
}
pure (mem, mmConf)
pure (InitialMem mem mmConf)
lazyInitialMem ::
( ext ~ MS.MacawExt arch
@ -499,7 +499,7 @@ lazyInitialMem ::
bak ->
MAI.ArchitectureInfo arch ->
MS.ArchVals arch ->
IO (CLM.MemImpl sym, MS.MemModelConfig p sym arch CLM.Mem)
IO (InitialMem p sym arch)
lazyInitialMem binfo bak archInfo archVals = do
let endianness = MSMLazy.toCrucibleEndian (MAI.archEndianness archInfo)
(mem, memPtrTbl) <-
@ -510,7 +510,13 @@ lazyInitialMem binfo bak archInfo archVals = do
, MS.lookupSyscallHandle = lookupSyscall
, MS.mkGlobalPointerValidityAssertion = validityCheck
}
pure (mem, mmConf)
pure (InitialMem mem mmConf)
data InitialMem p sym arch
= InitialMem
{ _initMemMem :: CLM.MemImpl sym
, _initMemMmConf :: MS.MemModelConfig p sym arch CLM.Mem
}
-- | Set up the symbolic execution engine with initial states and execute
--
@ -564,7 +570,7 @@ simulateFunction binfo bak execFeatures archInfo archVals halloc mmPreset g = do
-- initial contents) and a totally symbolic stack
let ?ptrWidth = WI.knownRepr
(initMem, mmConf) <-
(InitialMem initMem mmConf) <-
case mmPreset of
DefaultMemModel -> initialMem binfo bak archInfo archVals
LazyMemModel -> lazyInitialMem binfo bak archInfo archVals