mirror of
https://github.com/GaloisInc/macaw.git
synced 2024-11-29 21:44:11 +03:00
62 lines
2.8 KiB
Haskell
62 lines
2.8 KiB
Haskell
|
{-# LANGUAGE DataKinds #-}
|
||
|
|
{-# LANGUAGE FlexibleContexts #-}
|
||
|
|
{-# LANGUAGE GADTs #-}
|
||
|
|
{-# LANGUAGE ScopedTypeVariables #-}
|
||
|
|
{-# LANGUAGE TypeApplications #-}
|
||
|
|
{-# LANGUAGE TypeOperators #-}
|
||
|
|
|
||
|
|
import GHC.TypeLits
|
||
|
|
import Control.Monad.ST ( stToIO, RealWorld )
|
||
|
|
import qualified Data.Macaw.CFG as MC
|
||
|
|
import qualified Data.Macaw.Symbolic as MS
|
||
|
|
import qualified Data.Macaw.Symbolic.Memory as MSM
|
||
|
|
import Data.Proxy ( Proxy(..) )
|
||
|
|
import qualified Lang.Crucible.Backend as CB
|
||
|
|
import qualified Lang.Crucible.CFG.Core as CC
|
||
|
|
import qualified Lang.Crucible.FunctionHandle as CFH
|
||
|
|
import qualified Lang.Crucible.LLVM.MemModel as CLM
|
||
|
|
import qualified Lang.Crucible.LLVM.Intrinsics as CLI
|
||
|
|
import qualified Lang.Crucible.LLVM.DataLayout as LDL
|
||
|
|
import qualified Lang.Crucible.Simulator as CS
|
||
|
|
import qualified Lang.Crucible.Simulator.GlobalState as CSG
|
||
|
|
import qualified System.IO as IO
|
||
|
|
import qualified What4.Interface as WI
|
||
|
|
|
||
|
|
useCFG :: forall sym arch blocks
|
||
|
|
. ( CB.IsSymInterface sym
|
||
|
|
, MS.SymArchConstraints arch
|
||
|
|
, 16 <= MC.ArchAddrWidth arch
|
||
|
|
, Ord (WI.SymExpr sym WI.BaseNatType)
|
||
|
|
, KnownNat (MC.ArchAddrWidth arch)
|
||
|
|
)
|
||
|
|
=> CFH.HandleAllocator RealWorld
|
||
|
|
-- ^ The handle allocator used to construct the CFG
|
||
|
|
-> sym
|
||
|
|
-- ^ The symbolic backend
|
||
|
|
-> MS.ArchVals arch
|
||
|
|
-- ^ 'ArchVals' from a prior call to 'archVals'
|
||
|
|
-> CS.RegMap sym (MS.MacawFunctionArgs arch)
|
||
|
|
-- ^ Initial register state for the simulation
|
||
|
|
-> MC.Memory (MC.ArchAddrWidth arch)
|
||
|
|
-- ^ The memory recovered by macaw
|
||
|
|
-> MS.LookupFunctionHandle sym arch
|
||
|
|
-- ^ A translator for machine code addresses to function handles
|
||
|
|
-> CC.CFG (MS.MacawExt arch) blocks (MS.MacawFunctionArgs arch) (MS.MacawFunctionResult arch)
|
||
|
|
-- ^ The CFG to simulate
|
||
|
|
-> IO ()
|
||
|
|
useCFG hdlAlloc sym MS.ArchVals { MS.withArchEval = withArchEval }
|
||
|
|
initialRegs mem lfh cfg = withArchEval sym $ \archEvalFns -> do
|
||
|
|
let rep = CFH.handleReturnType (CC.cfgHandle cfg)
|
||
|
|
memModelVar <- stToIO (CLM.mkMemVar hdlAlloc)
|
||
|
|
(initialMem, memPtrTbl) <- MSM.newGlobalMemory (Proxy @arch) sym LDL.LittleEndian MSM.SymbolicMutable mem
|
||
|
|
let extImpl = MS.macawExtensions archEvalFns memModelVar (MSM.mapRegionPointers memPtrTbl) lfh
|
||
|
|
let simCtx = CS.initSimContext sym CLI.llvmIntrinsicTypes hdlAlloc IO.stderr CFH.emptyHandleMap extImpl MS.MacawSimulatorState
|
||
|
|
let simGlobalState = CSG.insertGlobal memModelVar initialMem CS.emptyGlobals
|
||
|
|
let simulation = CS.regValue <$> CS.callCFG cfg initialRegs
|
||
|
|
let initialState = CS.InitialState simCtx simGlobalState CS.defaultAbortHandler (CS.runOverrideSim rep simulation)
|
||
|
|
let executionFeatures = []
|
||
|
|
execRes <- CS.executeCrucible executionFeatures initialState
|
||
|
|
case execRes of
|
||
|
|
CS.FinishedResult {} -> return ()
|
||
|
|
_ -> putStrLn "Simulation failed"
|