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

symbolic: Rename and move a helper function in Testing

Browse Source
This commit is contained in:
Langston Barrett 2024-09-04 15:21:07 -04:00
parent f3fd0e0fcf
commit 0c5ed97e84
1 changed files with 10 additions and 10 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -439,14 +439,6 @@ simulateAndVerify goalSolver logger bak execFeatures archInfo archVals binfo mmP
WSR.Unsat {} -> return (SimulationResult Unsat) WSR.Unsat {} -> return (SimulationResult Unsat)
WSR.Unknown -> return (SimulationResult Unknown) WSR.Unknown -> return (SimulationResult Unknown)
discMems ::
BinariesInfo arch ->
V.Vector (MEL.Memory (MC.ArchAddrWidth arch))
discMems binfo =
let mainInfo = mainBinaryInfo binfo in
let soInfos = sharedLibraryInfos binfo in
V.map (MD.memory . binaryDiscState) (V.cons mainInfo soInfos)
initialMem :: initialMem ::
( ext ~ MS.MacawExt arch ( ext ~ MS.MacawExt arch
, CCE.IsSyntaxExtension ext , CCE.IsSyntaxExtension ext
@ -469,7 +461,7 @@ initialMem binfo bak archInfo archVals = do
let endianness = MSMLazy.toCrucibleEndian (MAI.archEndianness archInfo) let endianness = MSMLazy.toCrucibleEndian (MAI.archEndianness archInfo)
(mem, memPtrTbl) <- (mem, memPtrTbl) <-
MSM.newMergedGlobalMemoryWith populateRelocation archInfo bak MSM.newMergedGlobalMemoryWith populateRelocation archInfo bak
endianness MSM.ConcreteMutable (discMems binfo) endianness MSM.ConcreteMutable (binariesMems binfo)
let mmConf = (MSM.memModelConfig bak memPtrTbl) let mmConf = (MSM.memModelConfig bak memPtrTbl)
{ MS.lookupFunctionHandle = lookupFunction archVals binfo { MS.lookupFunctionHandle = lookupFunction archVals binfo
, MS.lookupSyscallHandle = lookupSyscall , MS.lookupSyscallHandle = lookupSyscall
@ -500,7 +492,7 @@ lazyInitialMem binfo bak archInfo archVals = do
let endianness = MSMLazy.toCrucibleEndian (MAI.archEndianness archInfo) let endianness = MSMLazy.toCrucibleEndian (MAI.archEndianness archInfo)
(mem, memPtrTbl) <- (mem, memPtrTbl) <-
MSMLazy.newMergedGlobalMemoryWith populateRelocation archInfo bak MSMLazy.newMergedGlobalMemoryWith populateRelocation archInfo bak
endianness MSMLazy.ConcreteMutable (discMems binfo) endianness MSMLazy.ConcreteMutable (binariesMems binfo)
let mmConf = (MSMLazy.memModelConfig bak memPtrTbl) let mmConf = (MSMLazy.memModelConfig bak memPtrTbl)
{ MS.lookupFunctionHandle = lookupFunction archVals binfo { MS.lookupFunctionHandle = lookupFunction archVals binfo
, MS.lookupSyscallHandle = lookupSyscall , MS.lookupSyscallHandle = lookupSyscall
@ -866,6 +858,14 @@ data BinariesInfo arch = BinariesInfo
-- revisited. -- revisited.
} }
binariesMems ::
BinariesInfo arch ->
V.Vector (MEL.Memory (MC.ArchAddrWidth arch))
binariesMems binfo =
let mainInfo = mainBinaryInfo binfo in
let soInfos = sharedLibraryInfos binfo in
V.map (MD.memory . binaryDiscState) (V.cons mainInfo soInfos)
-- | Information about an individual binary. -- | Information about an individual binary.
data BinaryInfo arch = BinaryInfo data BinaryInfo arch = BinaryInfo
{ binaryDiscState :: MD.DiscoveryState arch { binaryDiscState :: MD.DiscoveryState arch