mirror of
https://github.com/GaloisInc/macaw.git
synced 2024-11-26 09:22:20 +03:00
cc85cfe657
This cleanup consolidates the interface to macaw symbolic into two (and a half) modules: - Data.Macaw.Symbolic for clients who just need to symbolically simulate machine code - Data.Macaw.Symbolic.Backend for clients that need to implement new architectures - Data.Macaw.Symbolic.Memory provides a reusable example implementation of machine pointer to LLVM memory model pointer mapping Most functions are now documented and are grouped by use case. There are two worked (compiling) examples in the haddocks that show how to translate Macaw into Crucible and then symbolically simulate the results (including setting up all aspects of Crucible). The examples are included in the symbolic/examples directory and can be loaded with GHCi to type check them. The Data.Macaw.Symbolic.Memory module still needs a worked example. There were very few changes to actual code as part of this overhaul, but there are a few places where complicated functions were hidden behind newtypes, as users never need to construct the values themselves (e.g., MacawArchEvalFn and MacawSymbolicArchFunctions). There was also a slight consolidation of constraint synonyms to reduce duplication. All callers will have to be updated. There is also now a README for macaw-symbolic that explains its purpose and includes pointers to the new haddocks. This commit also fixes up the (minor) breakage in the macaw-x86-symbolic implementation from the API changes.
46 lines
2.3 KiB
Haskell
46 lines
2.3 KiB
Haskell
{-# LANGUAGE FlexibleContexts #-}
|
|
import Control.Monad.ST ( stToIO, RealWorld )
|
|
import qualified Data.Macaw.CFG as MC
|
|
import qualified Data.Macaw.Symbolic as MS
|
|
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.Simulator as CS
|
|
import qualified Lang.Crucible.Simulator.GlobalState as CSG
|
|
import qualified System.IO as IO
|
|
|
|
useCFG :: (CB.IsSymInterface sym, MS.SymArchConstraints 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
|
|
-> CLM.MemImpl sym
|
|
-- ^ The initial memory state of the simulator
|
|
-> MS.GlobalMap sym (MC.ArchAddrWidth arch)
|
|
-- ^ A translator of machine code addresses to LLVM pointers
|
|
-> 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 initialMem globalMap lfh cfg = withArchEval sym $ \archEvalFns -> do
|
|
let rep = CFH.handleReturnType (CC.cfgHandle cfg)
|
|
memModelVar <- stToIO (CLM.mkMemVar hdlAlloc)
|
|
let extImpl = MS.macawExtensions archEvalFns memModelVar globalMap 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"
|