mirror of
https://github.com/GaloisInc/macaw.git
synced 2024-12-28 08:34:23 +03:00
Progress on macaw-symbolic and macaw-x86-symbolic.
This commit is contained in:
Joe Hendrix
parent
eebc94cbe8
commit
b7e06e64ee
@ -885,20 +885,17 @@ mkFunState :: NonceGenerator (ST s) ids
|
||||
-> ArchSegmentOff arch
|
||||
-> FunState arch s ids
|
||||
mkFunState gen s rsn addr = do
|
||||
let info = archInfo s
|
||||
let mem = memory s
|
||||
let faddr = FoundAddr { foundReason = rsn
|
||||
, foundAbstractState = mkInitialAbsState info mem addr
|
||||
, foundAbstractState = mkInitialAbsState (archInfo s) (memory s) addr
|
||||
}
|
||||
let fs0 = FunState { funNonceGen = gen
|
||||
, curFunAddr = addr
|
||||
, _curFunCtx = s
|
||||
, _curFunBlocks = Map.empty
|
||||
, _foundAddrs = Map.singleton addr faddr
|
||||
, _reverseEdges = Map.empty
|
||||
, _frontier = Set.singleton addr
|
||||
}
|
||||
fs0
|
||||
in FunState { funNonceGen = gen
|
||||
, curFunAddr = addr
|
||||
, _curFunCtx = s
|
||||
, _curFunBlocks = Map.empty
|
||||
, _foundAddrs = Map.singleton addr faddr
|
||||
, _reverseEdges = Map.empty
|
||||
, _frontier = Set.singleton addr
|
||||
}
|
||||
|
||||
mkFunInfo :: FunState arch s ids -> DiscoveryFunInfo arch ids
|
||||
mkFunInfo fs =
|
||||
@ -929,7 +926,7 @@ analyzeFunction :: (ArchSegmentOff arch -> ST s ())
|
||||
-> DiscoveryState arch
|
||||
-- ^ The current binary information.
|
||||
-> ST s (DiscoveryState arch, Some (DiscoveryFunInfo arch))
|
||||
analyzeFunction logFn addr rsn s = do
|
||||
analyzeFunction logFn addr rsn s =
|
||||
case Map.lookup addr (s^.funInfo) of
|
||||
Just finfo -> pure (s, finfo)
|
||||
Nothing -> do
|
||||
|
||||
@ -21,9 +21,6 @@ module Data.Macaw.Memory.ElfLoader
|
||||
, LoadStyle(..)
|
||||
, LoadOptions(..)
|
||||
, memoryForElf
|
||||
-- * High-level exports
|
||||
, readElf
|
||||
, loadExecutable
|
||||
-- * Symbol resolution utilities
|
||||
, resolveElfFuncSymbols
|
||||
, ppElfUnresolvedSymbols
|
||||
@ -39,10 +36,8 @@ import qualified Data.ByteString.Char8 as BSC
|
||||
import qualified Data.ByteString.Lazy as L
|
||||
import Data.Either
|
||||
import Data.ElfEdit
|
||||
( SomeElf(..)
|
||||
, ElfIntType
|
||||
( ElfIntType
|
||||
, ElfWordType
|
||||
, ElfGetResult(..)
|
||||
|
||||
, Elf
|
||||
, elfSections
|
||||
@ -54,7 +49,6 @@ import Data.ElfEdit
|
||||
, elfMachine
|
||||
, ElfData(..)
|
||||
|
||||
, ElfParseError
|
||||
, ElfSection
|
||||
, ElfSectionIndex(..)
|
||||
, elfSectionIndex
|
||||
@ -81,10 +75,8 @@ import qualified Data.IntervalMap.Strict as IMap
|
||||
import Data.Map.Strict (Map)
|
||||
import qualified Data.Map.Strict as Map
|
||||
import Data.Maybe
|
||||
import Data.Parameterized.Some
|
||||
import qualified Data.Vector as V
|
||||
import Numeric (showHex)
|
||||
import System.IO
|
||||
import Text.PrettyPrint.ANSI.Leijen hiding ((<$>))
|
||||
|
||||
import Data.Macaw.Memory
|
||||
@ -476,67 +468,35 @@ memoryForElf opt e =
|
||||
LoadBySection -> memoryForElfSections e
|
||||
LoadBySegment -> memoryForElfSegments e
|
||||
|
||||
-- | Pretty print parser errors to stderr.
|
||||
ppErrors :: (Integral (ElfWordType w), Show (ElfWordType w))
|
||||
=> FilePath
|
||||
-> [ElfParseError w]
|
||||
-> IO ()
|
||||
ppErrors path errl = do
|
||||
when (not (null errl)) $ do
|
||||
hPutStrLn stderr $ "Non-fatal errors during parsing " ++ path
|
||||
forM_ errl $ \e -> do
|
||||
hPutStrLn stderr $ " " ++ show e
|
||||
|
||||
-- | This reads the elf file from the given path.
|
||||
--
|
||||
-- As a side effect it may print warnings for errors encountered during parsing
|
||||
-- to stderr.
|
||||
readElf :: FilePath -> IO (SomeElf Elf)
|
||||
readElf path = do
|
||||
bs <- BS.readFile path
|
||||
case Elf.parseElf bs of
|
||||
ElfHeaderError _ msg -> do
|
||||
fail $ "Could not parse Elf header: " ++ msg
|
||||
Elf32Res errl e -> do
|
||||
ppErrors path errl
|
||||
return (Elf32 e)
|
||||
Elf64Res errl e -> do
|
||||
ppErrors path errl
|
||||
return (Elf64 e)
|
||||
|
||||
loadExecutable :: LoadOptions -> FilePath -> IO (Some Memory)
|
||||
loadExecutable opt path = do
|
||||
se <- readElf path
|
||||
case se of
|
||||
Elf64 e -> either fail (return . Some . snd) $ memoryForElf opt e
|
||||
Elf32 e -> either fail (return . Some . snd) $ memoryForElf opt e
|
||||
|
||||
------------------------------------------------------------------------
|
||||
-- Elf symbol utilities
|
||||
|
||||
-- | Error when resolving symbols.
|
||||
data SymbolResolutionError
|
||||
= EmptySymbolName
|
||||
= EmptySymbolName !Int !Elf.ElfSymbolType
|
||||
-- ^ Symbol names must be non-empty
|
||||
| CouldNotResolveAddr !BSC.ByteString
|
||||
-- ^ Symbol address could not be resolved.
|
||||
| MultipleSymbolTables
|
||||
-- ^ The elf file contained multiple symbol tables
|
||||
|
||||
instance Show SymbolResolutionError where
|
||||
show EmptySymbolName = "Found empty symbol name"
|
||||
show (EmptySymbolName idx tp ) = "Symbol Num " ++ show idx ++ " " ++ show tp ++ " has an empty name."
|
||||
show (CouldNotResolveAddr sym) = "Could not resolve address of " ++ BSC.unpack sym ++ "."
|
||||
show MultipleSymbolTables = "Elf contains multiple symbol tables."
|
||||
|
||||
resolveEntry :: Memory w
|
||||
-> SectionIndexMap w
|
||||
-> ElfSymbolTableEntry (ElfWordType w)
|
||||
-> (Int,ElfSymbolTableEntry (ElfWordType w))
|
||||
-> Maybe (Either SymbolResolutionError
|
||||
(BS.ByteString, MemSegmentOff w))
|
||||
resolveEntry mem secMap ste
|
||||
resolveEntry mem secMap (idx,ste)
|
||||
-- Check this is a defined function symbol
|
||||
| (Elf.steType ste `elem` [ Elf.STT_FUNC, Elf.STT_NOTYPE ]) == False = Nothing
|
||||
-- Check symbol is defined
|
||||
| Elf.steIndex ste == Elf.SHN_UNDEF = Nothing
|
||||
-- Check symbol name is non-empty
|
||||
| Elf.steName ste /= "" = Just (Left EmptySymbolName)
|
||||
| Elf.steName ste == "" = Just $ Left $ EmptySymbolName idx (Elf.steType ste)
|
||||
-- Lookup absolute symbol
|
||||
| Elf.steIndex ste == Elf.SHN_ABS = reprConstraints (memAddrWidth mem) $ do
|
||||
let val = Elf.steValue ste
|
||||
@ -563,12 +523,17 @@ resolveElfFuncSymbols
|
||||
:: forall w
|
||||
. Memory w
|
||||
-> SectionIndexMap w
|
||||
-> [ElfSymbolTableEntry (ElfWordType w)]
|
||||
-> Elf w
|
||||
-> ( [SymbolResolutionError]
|
||||
, [(BS.ByteString, MemSegmentOff w)]
|
||||
)
|
||||
resolveElfFuncSymbols mem secMap entries = reprConstraints (memAddrWidth mem) $
|
||||
partitionEithers (mapMaybe (resolveEntry mem secMap) entries)
|
||||
resolveElfFuncSymbols mem secMap e =
|
||||
case Elf.elfSymtab e of
|
||||
[] -> ([], [])
|
||||
[tbl] ->
|
||||
let entries = V.toList (Elf.elfSymbolTableEntries tbl)
|
||||
in partitionEithers (mapMaybe (resolveEntry mem secMap) (zip [0..] entries))
|
||||
_ -> ([MultipleSymbolTables], [])
|
||||
|
||||
ppElfUnresolvedSymbols :: forall w
|
||||
. MemWidth w
|
||||
|
||||
@ -10,8 +10,9 @@
|
||||
{-# LANGUAGE TypeFamilies #-}
|
||||
{-# LANGUAGE TypeOperators #-}
|
||||
module Data.Macaw.Symbolic
|
||||
( Data.Macaw.Symbolic.CrucGen.CrucGenArchFunctions(..)
|
||||
( Data.Macaw.Symbolic.CrucGen.MacawSymbolicArchFunctions(..)
|
||||
, Data.Macaw.Symbolic.CrucGen.CrucGen
|
||||
, Data.Macaw.Symbolic.CrucGen.MemSegmentMap
|
||||
, MacawSimulatorState
|
||||
, freshVarsForRegs
|
||||
, runCodeBlock
|
||||
@ -20,6 +21,9 @@ module Data.Macaw.Symbolic
|
||||
, mkFunCFG
|
||||
, Data.Macaw.Symbolic.PersistentState.ArchRegContext
|
||||
, Data.Macaw.Symbolic.PersistentState.ToCrucibleType
|
||||
, Data.Macaw.Symbolic.PersistentState.macawAssignToCrucM
|
||||
, Data.Macaw.Symbolic.CrucGen.ArchRegStruct
|
||||
, Data.Macaw.Symbolic.CrucGen.MacawCrucibleRegTypes
|
||||
) where
|
||||
|
||||
import Control.Lens ((^.))
|
||||
@ -30,7 +34,6 @@ import Data.Map.Strict (Map)
|
||||
import qualified Data.Map.Strict as Map
|
||||
import Data.Parameterized.Context as Ctx
|
||||
import qualified Data.Parameterized.Map as MapF
|
||||
import Data.Parameterized.TraversableFC
|
||||
import qualified Data.Set as Set
|
||||
import qualified Data.Text as Text
|
||||
import Data.Word
|
||||
@ -103,32 +106,22 @@ mkMemBaseVarMap halloc mem = do
|
||||
-- | Create a Crucible CFG from a list of blocks
|
||||
mkCrucCFG :: forall s arch ids
|
||||
. M.ArchConstraints arch
|
||||
=> C.HandleAllocator s
|
||||
-- ^ Handle allocator to make function handles
|
||||
-> CrucGenArchFunctions arch
|
||||
=> MacawSymbolicArchFunctions arch
|
||||
-- ^ Crucible architecture-specific functions.
|
||||
-> MemSegmentMap (M.ArchAddrWidth arch)
|
||||
-- ^ Map from region indices to their address
|
||||
-> C.HandleAllocator s
|
||||
-- ^ Handle allocator to make function handles
|
||||
-> C.FunctionName
|
||||
-- ^ Name of function for pretty print purposes.
|
||||
-> (CrucGenContext arch s
|
||||
-> MacawMonad arch ids s [CR.Block (MacawExt arch) s (MacawFunctionResult arch)])
|
||||
-> MacawMonad arch ids s [CR.Block (MacawExt arch) s (MacawFunctionResult arch)]
|
||||
-- ^ Action to run
|
||||
-> ST s (C.SomeCFG (MacawExt arch) (EmptyCtx ::> ArchRegStruct arch) (ArchRegStruct arch))
|
||||
mkCrucCFG halloc archFns memBaseVarMap nm action = do
|
||||
let regAssign = crucGenRegAssignment archFns
|
||||
let crucRegTypes = typeCtxToCrucible (fmapFC M.typeRepr regAssign)
|
||||
mkCrucCFG archFns halloc nm action = do
|
||||
let crucRegTypes = crucArchRegTypes archFns
|
||||
let macawStructRepr = C.StructRepr crucRegTypes
|
||||
let argTypes = Empty :> macawStructRepr
|
||||
h <- C.mkHandle' halloc nm argTypes macawStructRepr
|
||||
let genCtx = CrucGenContext { archConstraints = \x -> x
|
||||
, macawRegAssign = regAssign
|
||||
, regIndexMap = mkRegIndexMap regAssign (Ctx.size crucRegTypes)
|
||||
, handleAlloc = halloc
|
||||
, memBaseAddrMap = memBaseVarMap
|
||||
}
|
||||
let ps0 = initCrucPersistentState 1
|
||||
blockRes <- runMacawMonad ps0 (action genCtx)
|
||||
blockRes <- runMacawMonad ps0 action
|
||||
blks <-
|
||||
case blockRes of
|
||||
(Left err, _) -> fail err
|
||||
@ -143,29 +136,30 @@ mkCrucCFG halloc archFns memBaseVarMap nm action = do
|
||||
-- | Create a Crucible CFG from a list of blocks
|
||||
addBlocksCFG :: forall s arch ids
|
||||
. M.ArchConstraints arch
|
||||
=> CrucGenArchFunctions arch
|
||||
=> MacawSymbolicArchFunctions arch
|
||||
-- ^ Crucible specific functions.
|
||||
-> CrucGenContext arch s
|
||||
-> (M.ArchAddrWord arch -> C.Position)
|
||||
-- ^ Function that maps offsets from start of block to Crucible position.
|
||||
-> MemSegmentMap (M.ArchAddrWidth arch)
|
||||
-- ^ Base address map
|
||||
-> (M.ArchAddrWord arch -> C.Position)
|
||||
-- ^ Function that maps offsets from start of block to Crucible position.
|
||||
-> [M.Block arch ids]
|
||||
-- ^ List of blocks for this region.
|
||||
-> MacawMonad arch ids s [CR.Block (MacawExt arch) s (MacawFunctionResult arch)]
|
||||
addBlocksCFG archFns ctx posFn macawBlocks = do
|
||||
addBlocksCFG archFns baseAddrMap posFn macawBlocks = do
|
||||
-- Map block map to Crucible CFG
|
||||
let blockLabelMap :: Map Word64 (CR.Label s)
|
||||
blockLabelMap = Map.fromList [ (w, CR.Label (fromIntegral w))
|
||||
| w <- M.blockLabel <$> macawBlocks ]
|
||||
forM macawBlocks $ \b -> do
|
||||
addMacawBlock archFns ctx blockLabelMap posFn b
|
||||
addMacawBlock archFns baseAddrMap blockLabelMap posFn b
|
||||
|
||||
-- | Create a Crucible CFG from a list of blocks
|
||||
mkBlocksCFG :: forall s arch ids
|
||||
. M.ArchConstraints arch
|
||||
=> C.HandleAllocator s
|
||||
-- ^ Handle allocator to make the blocks
|
||||
-> CrucGenArchFunctions arch
|
||||
=> MacawSymbolicArchFunctions arch
|
||||
-- ^ Crucible specific functions.
|
||||
-> C.HandleAllocator s
|
||||
-- ^ Handle allocator to make the blocks
|
||||
-> MemSegmentMap (M.ArchAddrWidth arch)
|
||||
-- ^ Map from region indices to their address
|
||||
-> C.FunctionName
|
||||
@ -175,18 +169,18 @@ mkBlocksCFG :: forall s arch ids
|
||||
-> [M.Block arch ids]
|
||||
-- ^ List of blocks for this region.
|
||||
-> ST s (C.SomeCFG (MacawExt arch) (EmptyCtx ::> ArchRegStruct arch) (ArchRegStruct arch))
|
||||
mkBlocksCFG halloc archFns memBaseVarMap nm posFn macawBlocks = do
|
||||
mkCrucCFG halloc archFns memBaseVarMap nm $ \ctx -> do
|
||||
addBlocksCFG archFns ctx posFn macawBlocks
|
||||
mkBlocksCFG archFns halloc memBaseVarMap nm posFn macawBlocks = do
|
||||
mkCrucCFG archFns halloc nm $ do
|
||||
addBlocksCFG archFns memBaseVarMap posFn macawBlocks
|
||||
|
||||
type FunBlockMap arch s = Map (M.ArchSegmentOff arch, Word64) (CR.Label s)
|
||||
|
||||
mkFunCFG :: forall s arch ids
|
||||
. M.ArchConstraints arch
|
||||
=> C.HandleAllocator s
|
||||
=> MacawSymbolicArchFunctions arch
|
||||
-- ^ Architecture specific functions.
|
||||
-> C.HandleAllocator s
|
||||
-- ^ Handle allocator to make the blocks
|
||||
-> CrucGenArchFunctions arch
|
||||
-- ^ Crucible specific functions.
|
||||
-> MemSegmentMap (M.ArchAddrWidth arch)
|
||||
-- ^ Map from region indices to their address
|
||||
-> C.FunctionName
|
||||
@ -196,8 +190,8 @@ mkFunCFG :: forall s arch ids
|
||||
-> M.DiscoveryFunInfo arch ids
|
||||
-- ^ List of blocks for this region.
|
||||
-> ST s (C.SomeCFG (MacawExt arch) (EmptyCtx ::> ArchRegStruct arch) (ArchRegStruct arch))
|
||||
mkFunCFG halloc archFns memBaseVarMap nm posFn fn = do
|
||||
mkCrucCFG halloc archFns memBaseVarMap nm $ \ctx -> do
|
||||
mkFunCFG archFns halloc memBaseVarMap nm posFn fn = do
|
||||
mkCrucCFG archFns halloc nm $ do
|
||||
let insSentences :: M.ArchSegmentOff arch
|
||||
-> (FunBlockMap arch s,Int)
|
||||
-> [M.StatementList arch ids]
|
||||
@ -211,9 +205,14 @@ mkFunCFG halloc archFns memBaseVarMap nm posFn fn = do
|
||||
insBlock m b = insSentences (M.pblockAddr b) m [M.blockStatementList b]
|
||||
let blockLabelMap :: FunBlockMap arch s
|
||||
blockLabelMap = fst $ foldl' insBlock (Map.empty,0) (Map.elems (fn^.M.parsedBlocks))
|
||||
let regReg = CR.Reg { CR.regPosition = posFn (M.discoveredFunAddr fn)
|
||||
, CR.regId = 0
|
||||
, CR.typeOfReg = C.StructRepr (crucArchRegTypes archFns)
|
||||
}
|
||||
fmap concat $
|
||||
forM (Map.elems (fn^.M.parsedBlocks)) $ \b -> do
|
||||
addParsedBlock archFns ctx blockLabelMap posFn b
|
||||
-- TODO: Initialize regReg
|
||||
addParsedBlock archFns memBaseVarMap blockLabelMap posFn regReg b
|
||||
|
||||
macawExecApp :: sym
|
||||
-> (forall utp . f utp -> IO (C.RegValue sym utp))
|
||||
@ -227,8 +226,10 @@ macawExecStmt :: C.CrucibleState MacawSimulatorState sym (MacawExt arch) rtp blo
|
||||
macawExecStmt _st s0 =
|
||||
case s0 of
|
||||
MacawReadMem{} -> undefined
|
||||
MacawCondReadMem{} -> undefined
|
||||
MacawWriteMem{} -> undefined
|
||||
MacawFreshSymbolic{} -> undefined
|
||||
MacawCall{} -> undefined
|
||||
|
||||
-- | Return macaw extension evaluation functions.
|
||||
macawExtensions :: sym -> C.ExtensionImpl MacawSimulatorState sym (MacawExt arch)
|
||||
@ -241,10 +242,10 @@ macawExtensions sym =
|
||||
runCodeBlock :: forall sym arch blocks
|
||||
. (IsSymInterface sym, M.ArchConstraints arch)
|
||||
=> sym
|
||||
-> CrucGenArchFunctions arch
|
||||
-> MacawSymbolicArchFunctions arch
|
||||
-> C.HandleAllocator RealWorld
|
||||
-> C.CFG (MacawExt arch) blocks (EmptyCtx ::> ArchRegStruct arch) (ArchRegStruct arch)
|
||||
-> Ctx.Assignment (C.RegValue' sym) (ArchCrucibleRegTypes arch)
|
||||
-> Ctx.Assignment (C.RegValue' sym) (MacawCrucibleRegTypes arch)
|
||||
-- ^ Register assignment
|
||||
-> IO (C.ExecResult
|
||||
MacawSimulatorState
|
||||
@ -252,8 +253,7 @@ runCodeBlock :: forall sym arch blocks
|
||||
(MacawExt arch)
|
||||
(C.RegEntry sym (ArchRegStruct arch)))
|
||||
runCodeBlock sym archFns halloc g regStruct = do
|
||||
let regAssign = crucGenRegAssignment archFns
|
||||
let crucRegTypes = typeCtxToCrucible (fmapFC M.typeRepr regAssign)
|
||||
let crucRegTypes = crucArchRegTypes archFns
|
||||
let macawStructRepr = C.StructRepr crucRegTypes
|
||||
-- Run the symbolic simulator.
|
||||
cfg <- C.initialConfig 0 []
|
||||
@ -281,7 +281,7 @@ runCodeBlock sym archFns halloc g regStruct = do
|
||||
runBlocks :: forall sym arch ids
|
||||
. (IsSymInterface sym, M.ArchConstraints arch)
|
||||
=> sym
|
||||
-> CrucGenArchFunctions arch
|
||||
-> MacawSymbolicArchFunctions arch
|
||||
-- ^ Crucible specific functions.
|
||||
-> M.Memory (M.ArchAddrWidth arch)
|
||||
-- ^ Memory image for executable
|
||||
@ -301,6 +301,6 @@ runBlocks :: forall sym arch ids
|
||||
runBlocks sym archFns mem nm posFn macawBlocks regStruct = do
|
||||
halloc <- C.newHandleAllocator
|
||||
memBaseVarMap <- stToIO $ mkMemBaseVarMap halloc mem
|
||||
C.SomeCFG g <- stToIO $ mkBlocksCFG halloc archFns memBaseVarMap nm posFn macawBlocks
|
||||
C.SomeCFG g <- stToIO $ mkBlocksCFG archFns halloc memBaseVarMap nm posFn macawBlocks
|
||||
-- Run the symbolic simulator.
|
||||
runCodeBlock sym archFns halloc g regStruct
|
||||
|
||||
@ -19,9 +19,15 @@ This defines the core operations for mapping from Reopt to Crucible.
|
||||
{-# LANGUAGE TypeFamilies #-}
|
||||
{-# LANGUAGE TypeOperators #-}
|
||||
module Data.Macaw.Symbolic.CrucGen
|
||||
( CrucGenArchFunctions(..)
|
||||
( MacawSymbolicArchFunctions(..)
|
||||
, crucArchRegTypes
|
||||
, MacawExt
|
||||
, MacawStmtExtension(..)
|
||||
, MacawFunctionArgs
|
||||
, MacawFunctionResult
|
||||
, ArchAddrCrucibleType
|
||||
, MacawCrucibleRegTypes
|
||||
, ArchRegStruct
|
||||
-- ** Operations for implementing new backends.
|
||||
, CrucGen
|
||||
, MacawMonad
|
||||
@ -29,6 +35,7 @@ module Data.Macaw.Symbolic.CrucGen
|
||||
, addMacawBlock
|
||||
, addParsedBlock
|
||||
, nextStatements
|
||||
, MemSegmentMap
|
||||
) where
|
||||
|
||||
import Control.Lens hiding (Empty, (:>))
|
||||
@ -43,6 +50,7 @@ import qualified Data.Macaw.Memory as M
|
||||
import qualified Data.Macaw.Types as M
|
||||
import Data.Map.Strict (Map)
|
||||
import qualified Data.Map.Strict as Map
|
||||
import Data.Maybe
|
||||
import Data.Parameterized.Context as Ctx
|
||||
import Data.Parameterized.Map (MapF)
|
||||
import qualified Data.Parameterized.Map as MapF
|
||||
@ -61,13 +69,24 @@ import Text.PrettyPrint.ANSI.Leijen hiding ((<$>))
|
||||
|
||||
import Data.Macaw.Symbolic.PersistentState
|
||||
|
||||
|
||||
-- | List of crucible types for architecture.
|
||||
type MacawCrucibleRegTypes (arch :: *) = CtxToCrucibleType (ArchRegContext arch)
|
||||
|
||||
type ArchRegStruct (arch :: *) = C.StructType (MacawCrucibleRegTypes arch)
|
||||
|
||||
type ArchAddrCrucibleType arch = C.BVType (M.ArchAddrWidth arch)
|
||||
|
||||
type MacawFunctionArgs arch = EmptyCtx ::> ArchRegStruct arch
|
||||
type MacawFunctionResult arch = ArchRegStruct arch
|
||||
|
||||
------------------------------------------------------------------------
|
||||
-- CrucPersistentState
|
||||
|
||||
-- | Architecture-specific information needed to translate from Macaw to Crucible
|
||||
data CrucGenArchFunctions arch
|
||||
= CrucGenArchFunctions
|
||||
{ crucGenArchConstraints :: !(forall a . (M.MemWidth (M.ArchAddrWidth arch) => a) -> a)
|
||||
data MacawSymbolicArchFunctions arch
|
||||
= MacawSymbolicArchFunctions
|
||||
{ crucGenArchConstraints :: !(forall a . (M.RegisterInfo (M.ArchReg arch) => a) -> a)
|
||||
, crucGenRegAssignment :: !(Ctx.Assignment (M.ArchReg arch) (ArchRegContext arch))
|
||||
-- ^ Map from indices in the ArchRegContext to the associated register.
|
||||
, crucGenArchRegName :: !(forall tp . M.ArchReg arch tp -> C.SolverSymbol)
|
||||
@ -86,6 +105,13 @@ data CrucGenArchFunctions arch
|
||||
-- ^ Generate crucible for architecture-specific terminal statement.
|
||||
}
|
||||
|
||||
-- | Return types of registers in Crucible
|
||||
crucArchRegTypes :: MacawSymbolicArchFunctions arch
|
||||
-> Assignment C.TypeRepr (CtxToCrucibleType (ArchRegContext arch))
|
||||
crucArchRegTypes archFns = crucGenArchConstraints archFns $
|
||||
typeCtxToCrucible (fmapFC M.typeRepr regAssign)
|
||||
where regAssign = crucGenRegAssignment archFns
|
||||
|
||||
------------------------------------------------------------------------
|
||||
-- MacawStmtExtension
|
||||
|
||||
@ -93,12 +119,22 @@ data MacawStmtExtension (arch :: *) (f :: C.CrucibleType -> *) (tp :: C.Crucible
|
||||
MacawReadMem :: !(M.MemRepr tp)
|
||||
-> !(f (ArchAddrCrucibleType arch))
|
||||
-> MacawStmtExtension arch f (ToCrucibleType tp)
|
||||
MacawCondReadMem :: !(M.MemRepr tp)
|
||||
-> !(f C.BoolType)
|
||||
-> !(f (ArchAddrCrucibleType arch))
|
||||
-> !(f (ToCrucibleType tp))
|
||||
-> MacawStmtExtension arch f (ToCrucibleType tp)
|
||||
MacawWriteMem :: !(M.MemRepr tp)
|
||||
-> !(f (ArchAddrCrucibleType arch))
|
||||
-> !(f (ToCrucibleType tp))
|
||||
-> MacawStmtExtension arch f C.UnitType
|
||||
MacawFreshSymbolic :: !(M.TypeRepr tp)
|
||||
-> MacawStmtExtension arch f (ToCrucibleType tp)
|
||||
MacawCall :: !(Assignment C.TypeRepr (CtxToCrucibleType (ArchRegContext arch)))
|
||||
-- ^ Types of fields in register struct
|
||||
-> !(f (ArchRegStruct arch))
|
||||
-- ^ Arguments to call.
|
||||
-> MacawStmtExtension arch f (ArchRegStruct arch)
|
||||
|
||||
instance FunctorFC (MacawStmtExtension arch) where
|
||||
fmapFC = fmapFCDefault
|
||||
@ -110,8 +146,10 @@ instance TraversableFC (MacawStmtExtension arch) where
|
||||
traverseFC f a0 =
|
||||
case a0 of
|
||||
MacawReadMem r a -> MacawReadMem r <$> f a
|
||||
MacawCondReadMem r c a d -> MacawCondReadMem r <$> f c <*> f a <*> f d
|
||||
MacawWriteMem r a v -> MacawWriteMem r <$> f a <*> f v
|
||||
MacawFreshSymbolic r -> pure (MacawFreshSymbolic r)
|
||||
MacawCall regTypes regs -> MacawCall regTypes <$> f regs
|
||||
|
||||
sexpr :: String -> [Doc] -> Doc
|
||||
sexpr s [] = text s
|
||||
@ -120,14 +158,18 @@ sexpr s l = parens (text s <+> hsep l)
|
||||
instance C.PrettyApp (MacawStmtExtension arch) where
|
||||
ppApp f a0 =
|
||||
case a0 of
|
||||
MacawReadMem r a -> sexpr "macawReadMem" [pretty r, f a]
|
||||
MacawWriteMem r a v -> sexpr "macawWriteMem" [pretty r, f a, f v]
|
||||
MacawReadMem r a -> sexpr "macawReadMem" [pretty r, f a]
|
||||
MacawCondReadMem r c a d -> sexpr "macawCondReadMem" [pretty r, f c, f a, f d ]
|
||||
MacawWriteMem r a v -> sexpr "macawWriteMem" [pretty r, f a, f v]
|
||||
MacawFreshSymbolic r -> sexpr "macawFreshSymbolic" [ text (show r) ]
|
||||
MacawCall _ regs -> sexpr "macawCall" [ f regs ]
|
||||
|
||||
instance C.TypeApp (MacawStmtExtension arch) where
|
||||
appType (MacawReadMem r _) = memReprToCrucible r
|
||||
appType (MacawCondReadMem r _ _ _) = memReprToCrucible r
|
||||
appType (MacawWriteMem _ _ _) = C.knownRepr
|
||||
appType (MacawFreshSymbolic r) = typeToCrucible r
|
||||
appType (MacawCall regTypes _) = C.StructRepr regTypes
|
||||
|
||||
------------------------------------------------------------------------
|
||||
-- MacawExt
|
||||
@ -139,20 +181,32 @@ type instance C.StmtExtension (MacawExt arch) = MacawStmtExtension arch
|
||||
|
||||
instance C.IsSyntaxExtension (MacawExt arch)
|
||||
|
||||
-- | Map from indices of segments without a fixed base address to a
|
||||
-- global variable storing the base address.
|
||||
--
|
||||
-- This uses a global variable so that we can do the translation, and then
|
||||
-- decide where to locate it without requiring us to also pass the values
|
||||
-- around arguments.
|
||||
type MemSegmentMap w = Map M.RegionIndex (CR.GlobalVar (C.BVType w))
|
||||
|
||||
-- | State used for generating blocks
|
||||
data CrucGenState arch ids s
|
||||
= CrucGenState
|
||||
{ translateFns :: !(CrucGenArchFunctions arch)
|
||||
, crucCtx :: !(CrucGenContext arch s)
|
||||
, crucPState :: !(CrucPersistentState ids s)
|
||||
{ translateFns :: !(MacawSymbolicArchFunctions arch)
|
||||
, crucMemBaseAddrMap :: !(MemSegmentMap (M.ArchAddrWidth arch))
|
||||
-- ^ Map from memory region to base address
|
||||
, crucRegIndexMap :: !(RegIndexMap arch)
|
||||
-- ^ Map from architecture register to Crucible/Macaw index pair.
|
||||
, crucPState :: !(CrucPersistentState ids s)
|
||||
-- ^ State that persists across blocks.
|
||||
, crucRegisterReg :: !(CR.Reg s (ArchRegStruct arch))
|
||||
, macawPositionFn :: !(M.ArchAddrWord arch -> C.Position)
|
||||
-- ^ Map from offset to Crucible position.
|
||||
, blockLabel :: (CR.Label s)
|
||||
-- ^ Label for this block we are translating
|
||||
, codeOff :: !(M.ArchAddrWord arch)
|
||||
, codeOff :: !(M.ArchAddrWord arch)
|
||||
-- ^ Offset
|
||||
, prevStmts :: ![C.Posd (CR.Stmt (MacawExt arch) s)]
|
||||
, prevStmts :: ![C.Posd (CR.Stmt (MacawExt arch) s)]
|
||||
-- ^ List of states in reverse order
|
||||
}
|
||||
|
||||
@ -190,9 +244,6 @@ instance MonadState (CrucGenState arch ids s) (CrucGen arch ids s) where
|
||||
get = CrucGen $ \s cont -> cont s s
|
||||
put s = CrucGen $ \_ cont -> cont s ()
|
||||
|
||||
getCtx :: CrucGen arch ids s (CrucGenContext arch s)
|
||||
getCtx = gets crucCtx
|
||||
|
||||
-- | Get current position
|
||||
getPos :: CrucGen arch ids s C.Position
|
||||
getPos = gets $ \s -> macawPositionFn s (codeOff s)
|
||||
@ -244,21 +295,20 @@ evalAtom av = do
|
||||
crucibleValue :: C.App (MacawExt arch) (CR.Atom s) ctp -> CrucGen arch ids s (CR.Atom s ctp)
|
||||
crucibleValue app = evalAtom (CR.EvalApp app)
|
||||
|
||||
-- | Evaluate the crucible app and return a reference to the result.
|
||||
getRegInput :: Ctx.Assignment (M.ArchReg arch) (ArchRegContext arch)
|
||||
-> IndexPair (ArchRegContext arch) tp
|
||||
-- | Return the value associated with the given register
|
||||
getRegValue :: M.ArchReg arch tp
|
||||
-> CrucGen arch ids s (CR.Atom s (ToCrucibleType tp))
|
||||
getRegInput regAssign idx = do
|
||||
ctx <- getCtx
|
||||
archConstraints ctx $ do
|
||||
-- Make atom
|
||||
let regStruct = CR.Atom { CR.atomPosition = C.InternalPos
|
||||
, CR.atomId = 0
|
||||
, CR.atomSource = CR.FnInput
|
||||
, CR.typeOfAtom = regStructRepr ctx
|
||||
}
|
||||
let tp = M.typeRepr (regAssign Ctx.! macawIndex idx)
|
||||
crucibleValue (C.GetStruct regStruct (crucibleIndex idx) (typeToCrucible tp))
|
||||
getRegValue r = do
|
||||
archFns <- gets translateFns
|
||||
idxMap <- gets crucRegIndexMap
|
||||
crucGenArchConstraints archFns $ do
|
||||
case MapF.lookup r idxMap of
|
||||
Nothing -> fail $ "internal: Register is not bound."
|
||||
Just idx -> do
|
||||
reg <- gets crucRegisterReg
|
||||
regStruct <- evalAtom (CR.ReadReg reg)
|
||||
let tp = M.typeRepr (crucGenRegAssignment archFns Ctx.! macawIndex idx)
|
||||
crucibleValue (C.GetStruct regStruct (crucibleIndex idx) (typeToCrucible tp))
|
||||
|
||||
v2c :: M.Value arch ids tp
|
||||
-> CrucGen arch ids s (CR.Atom s (ToCrucibleType tp))
|
||||
@ -304,8 +354,8 @@ bvAdc w x y c = do
|
||||
appToCrucible :: M.App (M.Value arch ids) tp
|
||||
-> CrucGen arch ids s (CR.Atom s (ToCrucibleType tp))
|
||||
appToCrucible app = do
|
||||
ctx <- getCtx
|
||||
archConstraints ctx $ do
|
||||
archFns <- gets translateFns
|
||||
crucGenArchConstraints archFns $ do
|
||||
case app of
|
||||
M.Eq x y -> do
|
||||
let btp = typeToCrucibleBase (M.typeRepr x)
|
||||
@ -383,18 +433,18 @@ appToCrucible app = do
|
||||
valueToCrucible :: M.Value arch ids tp
|
||||
-> CrucGen arch ids s (CR.Atom s (ToCrucibleType tp))
|
||||
valueToCrucible v = do
|
||||
ctx <- getCtx
|
||||
archConstraints ctx $ do
|
||||
case v of
|
||||
archFns <- gets translateFns
|
||||
crucGenArchConstraints archFns $ do
|
||||
case v of
|
||||
M.BVValue w c -> bvLit w c
|
||||
M.BoolValue b -> crucibleValue (C.BoolLit b)
|
||||
-- In this case,
|
||||
M.RelocatableValue w addr
|
||||
| M.addrBase addr == 0 ->
|
||||
crucibleValue (C.BVLit w (toInteger (M.addrOffset addr)))
|
||||
| M.addrBase addr == 0 -> do
|
||||
crucibleValue (C.BVLit w (toInteger (M.addrOffset addr)))
|
||||
| otherwise -> do
|
||||
let idx = M.addrBase addr
|
||||
segMap <- memBaseAddrMap <$> getCtx
|
||||
segMap <- gets crucMemBaseAddrMap
|
||||
case Map.lookup idx segMap of
|
||||
Just g -> do
|
||||
a <- evalAtom (CR.ReadGlobal g)
|
||||
@ -403,10 +453,7 @@ valueToCrucible v = do
|
||||
Nothing ->
|
||||
fail $ "internal: No Crucible address associated with segment."
|
||||
M.Initial r -> do
|
||||
case MapF.lookup r (regIndexMap ctx) of
|
||||
Just idx -> do
|
||||
getRegInput (macawRegAssign ctx) idx
|
||||
Nothing -> fail $ "internal: Register is not bound."
|
||||
getRegValue r
|
||||
M.AssignedValue asgn -> do
|
||||
let idx = M.assignId asgn
|
||||
amap <- use $ crucPStateLens . assignValueMapLens
|
||||
@ -422,33 +469,20 @@ freshSymbolic repr = evalMacawStmt (MacawFreshSymbolic repr)
|
||||
evalMacawStmt :: MacawStmtExtension arch (CR.Atom s) tp -> CrucGen arch ids s (CR.Atom s tp)
|
||||
evalMacawStmt s = evalAtom (CR.EvalExt s)
|
||||
|
||||
-- | Read the given memory address
|
||||
callReadMem :: M.ArchAddrValue arch ids
|
||||
-> M.MemRepr tp
|
||||
-> CrucGen arch ids s (CR.Atom s (ToCrucibleType tp))
|
||||
callReadMem addr repr = do
|
||||
caddr <- valueToCrucible addr
|
||||
evalMacawStmt (MacawReadMem repr caddr)
|
||||
|
||||
callWriteMem :: M.ArchAddrValue arch ids
|
||||
-> M.MemRepr tp
|
||||
-> M.Value arch ids tp
|
||||
-> CrucGen arch ids s ()
|
||||
callWriteMem addr repr val = do
|
||||
caddr <- valueToCrucible addr
|
||||
cval <- valueToCrucible val
|
||||
_ <- evalMacawStmt (MacawWriteMem repr caddr cval)
|
||||
pure ()
|
||||
|
||||
assignRhsToCrucible :: M.AssignRhs arch (M.Value arch ids) tp
|
||||
-> CrucGen arch ids s (CR.Atom s (ToCrucibleType tp))
|
||||
assignRhsToCrucible rhs =
|
||||
case rhs of
|
||||
M.EvalApp app -> appToCrucible app
|
||||
M.SetUndefined mrepr -> freshSymbolic mrepr
|
||||
M.ReadMem addr repr -> callReadMem addr repr
|
||||
M.CondReadMem repr c addr def -> do
|
||||
undefined repr c addr def
|
||||
M.ReadMem addr repr -> do
|
||||
caddr <- valueToCrucible addr
|
||||
evalMacawStmt (MacawReadMem repr caddr)
|
||||
M.CondReadMem repr cond addr def -> do
|
||||
ccond <- valueToCrucible cond
|
||||
caddr <- valueToCrucible addr
|
||||
cdef <- valueToCrucible def
|
||||
evalMacawStmt (MacawCondReadMem repr ccond caddr cdef)
|
||||
M.EvalArchFn f _ -> do
|
||||
fns <- translateFns <$> get
|
||||
crucGenArchFn fns f
|
||||
@ -462,7 +496,9 @@ addMacawStmt stmt =
|
||||
a <- assignRhsToCrucible (M.assignRhs asgn)
|
||||
crucPStateLens . assignValueMapLens %= MapF.insert idx (MacawCrucibleValue a)
|
||||
M.WriteMem addr repr val -> do
|
||||
callWriteMem addr repr val
|
||||
caddr <- valueToCrucible addr
|
||||
cval <- valueToCrucible val
|
||||
void $ evalMacawStmt (MacawWriteMem repr caddr cval)
|
||||
M.PlaceHolderStmt _vals msg -> do
|
||||
cmsg <- crucibleValue (C.TextLit (Text.pack msg))
|
||||
addTermStmt (CR.ErrorStmt cmsg)
|
||||
@ -490,9 +526,9 @@ createRegStruct :: forall arch ids s
|
||||
. M.RegState (M.ArchReg arch) (M.Value arch ids)
|
||||
-> CrucGen arch ids s (CR.Atom s (ArchRegStruct arch))
|
||||
createRegStruct regs = do
|
||||
ctx <- getCtx
|
||||
archConstraints ctx $ do
|
||||
let regAssign = macawRegAssign ctx
|
||||
archFns <- gets translateFns
|
||||
crucGenArchConstraints archFns $ do
|
||||
let regAssign = crucGenRegAssignment archFns
|
||||
let tps = fmapFC M.typeRepr regAssign
|
||||
let a = fmapFC (\r -> regs ^. M.boundValue r) regAssign
|
||||
fields <- macawAssignToCrucM valueToCrucible a
|
||||
@ -539,20 +575,29 @@ runMacawMonad s (MacawMonad m) = runStateT (runExceptT m) s
|
||||
mmExecST :: ST s a -> MacawMonad arch ids s a
|
||||
mmExecST = MacawMonad . lift . lift
|
||||
|
||||
runCrucGen :: CrucGenArchFunctions arch
|
||||
-> CrucGenContext arch s
|
||||
runCrucGen :: forall arch ids s
|
||||
. MacawSymbolicArchFunctions arch
|
||||
-> MemSegmentMap (M.ArchAddrWidth arch)
|
||||
-- ^ Base address map
|
||||
-> (M.ArchAddrWord arch -> C.Position)
|
||||
-- ^ Function for generating position from offset from start of this block.
|
||||
-> M.ArchAddrWord arch
|
||||
-- ^ Offset
|
||||
-- ^ Offset of this block
|
||||
-> CR.Label s
|
||||
-- ^ Label for this block
|
||||
-> CR.Reg s (ArchRegStruct arch)
|
||||
-- ^ Crucible register for struct containing all Macaw registers.
|
||||
-> CrucGen arch ids s ()
|
||||
-> MacawMonad arch ids s (CR.Block (MacawExt arch) s (MacawFunctionResult arch), M.ArchAddrWord arch)
|
||||
runCrucGen tfns ctx posFn off lbl action = do
|
||||
runCrucGen archFns baseAddrMap posFn off lbl regReg action = crucGenArchConstraints archFns $ do
|
||||
ps <- get
|
||||
let s0 = CrucGenState { translateFns = tfns
|
||||
, crucCtx = ctx
|
||||
let regAssign = crucGenRegAssignment archFns
|
||||
let crucRegTypes = crucArchRegTypes archFns
|
||||
let s0 = CrucGenState { translateFns = archFns
|
||||
, crucMemBaseAddrMap = baseAddrMap
|
||||
, crucRegIndexMap = mkRegIndexMap regAssign (Ctx.size crucRegTypes)
|
||||
, crucPState = ps
|
||||
, crucRegisterReg = regReg
|
||||
, macawPositionFn = posFn
|
||||
, blockLabel = lbl
|
||||
, codeOff = off
|
||||
@ -561,22 +606,23 @@ runCrucGen tfns ctx posFn off lbl action = do
|
||||
let cont _s () = fail "Unterminated crucible block"
|
||||
(s, tstmt) <- mmExecST $ unCrucGen action s0 cont
|
||||
put (crucPState s)
|
||||
let termPos = macawPositionFn s (codeOff s)
|
||||
let termPos = posFn (codeOff s)
|
||||
let stmts = Seq.fromList (reverse (prevStmts s))
|
||||
let term = C.Posd termPos tstmt
|
||||
let blk = CR.mkBlock (CR.LabelID lbl) Set.empty stmts term
|
||||
pure (blk, codeOff s)
|
||||
|
||||
addMacawBlock :: M.MemWidth (M.ArchAddrWidth arch)
|
||||
=> CrucGenArchFunctions arch
|
||||
-> CrucGenContext arch s
|
||||
=> MacawSymbolicArchFunctions arch
|
||||
-> MemSegmentMap (M.ArchAddrWidth arch)
|
||||
-- ^ Base address map
|
||||
-> Map Word64 (CR.Label s)
|
||||
-- ^ Map from block index to Crucible label
|
||||
-> (M.ArchAddrWord arch -> C.Position)
|
||||
-- ^ Function for generating position from offset from start of this block.
|
||||
-> M.Block arch ids
|
||||
-> MacawMonad arch ids s (CR.Block (MacawExt arch) s (MacawFunctionResult arch))
|
||||
addMacawBlock tfns ctx blockLabelMap posFn b = do
|
||||
addMacawBlock archFns baseAddrMap blockLabelMap posFn b = do
|
||||
let idx = M.blockLabel b
|
||||
lbl <-
|
||||
case Map.lookup idx blockLabelMap of
|
||||
@ -584,19 +630,59 @@ addMacawBlock tfns ctx blockLabelMap posFn b = do
|
||||
pure lbl
|
||||
Nothing ->
|
||||
throwError $ "Internal: Could not find block with index " ++ show idx
|
||||
fmap fst $ runCrucGen tfns ctx posFn 0 lbl $ do
|
||||
let archRegStructRepr = C.StructRepr (crucArchRegTypes archFns)
|
||||
let regReg = CR.Reg { CR.regPosition = posFn 0
|
||||
, CR.regId = 0
|
||||
, CR.typeOfReg = archRegStructRepr
|
||||
}
|
||||
let regStruct = CR.Atom { CR.atomPosition = C.InternalPos
|
||||
, CR.atomId = 0
|
||||
, CR.atomSource = CR.FnInput
|
||||
, CR.typeOfAtom = archRegStructRepr
|
||||
}
|
||||
fmap fst $ runCrucGen archFns baseAddrMap posFn 0 lbl regReg $ do
|
||||
addStmt $ CR.SetReg regReg regStruct
|
||||
mapM_ addMacawStmt (M.blockStmts b)
|
||||
addMacawTermStmt blockLabelMap (M.blockTerm b)
|
||||
|
||||
addMacawParsedTermStmt :: M.ParsedTermStmt arch ids
|
||||
parsedBlockLabel :: (Ord addr, Show addr)
|
||||
=> Map (addr, Word64) (CR.Label s)
|
||||
-- ^ Map from block addresses to starting label
|
||||
-> addr
|
||||
-> Word64
|
||||
-> CR.Label s
|
||||
parsedBlockLabel blockLabelMap addr idx =
|
||||
fromMaybe (error $ "Could not find entry point: " ++ show addr) $
|
||||
Map.lookup (addr, idx) blockLabelMap
|
||||
|
||||
addMacawParsedTermStmt :: Map (M.ArchSegmentOff arch, Word64) (CR.Label s)
|
||||
-- ^ Map from block addresses to starting label
|
||||
-> M.ArchSegmentOff arch
|
||||
-- ^ Address of this block
|
||||
-> M.ParsedTermStmt arch ids
|
||||
-> CrucGen arch ids s ()
|
||||
addMacawParsedTermStmt tstmt =
|
||||
addMacawParsedTermStmt blockLabelMap thisAddr tstmt = do
|
||||
archFns <- translateFns <$> get
|
||||
crucGenArchConstraints archFns $ do
|
||||
case tstmt of
|
||||
M.ParsedCall{} -> undefined
|
||||
M.ParsedCall regs mret -> do
|
||||
curRegs <- createRegStruct regs
|
||||
newRegs <- evalMacawStmt (MacawCall (crucArchRegTypes archFns) curRegs)
|
||||
case mret of
|
||||
Just nextAddr -> do
|
||||
regReg <- gets crucRegisterReg
|
||||
addStmt $ CR.SetReg regReg newRegs
|
||||
addTermStmt $ CR.Jump (parsedBlockLabel blockLabelMap nextAddr 0)
|
||||
Nothing ->
|
||||
addTermStmt $ CR.Return newRegs
|
||||
M.ParsedJump{} -> undefined
|
||||
M.ParsedLookupTable{} -> undefined
|
||||
M.ParsedReturn{} -> undefined
|
||||
M.ParsedIte{} -> undefined
|
||||
M.ParsedIte c t f -> do
|
||||
crucCond <- valueToCrucible c
|
||||
let tlbl = parsedBlockLabel blockLabelMap thisAddr (M.stmtsIdent t)
|
||||
let flbl = parsedBlockLabel blockLabelMap thisAddr (M.stmtsIdent f)
|
||||
addTermStmt $! CR.Br crucCond tlbl flbl
|
||||
M.ParsedArchTermStmt{} -> undefined
|
||||
M.ParsedTranslateError{} -> undefined
|
||||
M.ClassifyFailure{} -> undefined
|
||||
@ -608,47 +694,53 @@ nextStatements tstmt =
|
||||
_ -> []
|
||||
|
||||
addStatementList :: M.MemWidth (M.ArchAddrWidth arch)
|
||||
=> CrucGenArchFunctions arch
|
||||
-> CrucGenContext arch s
|
||||
=> MacawSymbolicArchFunctions arch
|
||||
-> MemSegmentMap (M.ArchAddrWidth arch)
|
||||
-- ^ Base address map
|
||||
-> Map (M.ArchSegmentOff arch, Word64) (CR.Label s)
|
||||
-- ^ Map from block index to Crucible label
|
||||
-> M.ArchSegmentOff arch
|
||||
-- ^ Address of statements
|
||||
-- ^ Address of block that starts statements
|
||||
-> (M.ArchAddrWord arch -> C.Position)
|
||||
-- ^ Function for generating position from offset from start of this block.
|
||||
-> CR.Reg s (ArchRegStruct arch)
|
||||
-- ^ Register that stores Macaw registers
|
||||
-> [(M.ArchAddrWord arch, M.StatementList arch ids)]
|
||||
-> [CR.Block (MacawExt arch) s (MacawFunctionResult arch)]
|
||||
-> MacawMonad arch ids s [CR.Block (MacawExt arch) s (MacawFunctionResult arch)]
|
||||
addStatementList _ _ _ _ _ [] rlist =
|
||||
addStatementList _ _ _ _ _ _ [] rlist =
|
||||
pure (reverse rlist)
|
||||
addStatementList tfns ctx blockLabelMap addr posFn ((off,stmts):rest) r = do
|
||||
addStatementList archFns baseAddrMap blockLabelMap startAddr posFn regReg ((off,stmts):rest) r = do
|
||||
let idx = M.stmtsIdent stmts
|
||||
lbl <-
|
||||
case Map.lookup (addr, idx) blockLabelMap of
|
||||
case Map.lookup (startAddr, idx) blockLabelMap of
|
||||
Just lbl ->
|
||||
pure lbl
|
||||
Nothing ->
|
||||
throwError $ "Internal: Could not find block with address " ++ show addr ++ " index " ++ show idx
|
||||
throwError $ "Internal: Could not find block with address " ++ show startAddr ++ " index " ++ show idx
|
||||
(b,off') <-
|
||||
runCrucGen tfns ctx posFn off lbl $ do
|
||||
runCrucGen archFns baseAddrMap posFn off lbl regReg $ do
|
||||
mapM_ addMacawStmt (M.stmtsNonterm stmts)
|
||||
addMacawParsedTermStmt (M.stmtsTerm stmts)
|
||||
addMacawParsedTermStmt blockLabelMap startAddr (M.stmtsTerm stmts)
|
||||
let new = (off',) <$> nextStatements (M.stmtsTerm stmts)
|
||||
addStatementList tfns ctx blockLabelMap addr posFn (new ++ rest) (b:r)
|
||||
addStatementList archFns baseAddrMap blockLabelMap startAddr posFn regReg (new ++ rest) (b:r)
|
||||
|
||||
addParsedBlock :: forall arch ids s
|
||||
. M.MemWidth (M.ArchAddrWidth arch)
|
||||
=> CrucGenArchFunctions arch
|
||||
-> CrucGenContext arch s
|
||||
=> MacawSymbolicArchFunctions arch
|
||||
-> MemSegmentMap (M.ArchAddrWidth arch)
|
||||
-- ^ Base address map
|
||||
-> Map (M.ArchSegmentOff arch, Word64) (CR.Label s)
|
||||
-- ^ Map from block index to Crucible label
|
||||
-> (M.ArchSegmentOff arch -> C.Position)
|
||||
-- ^ Function for generating position from offset from start of this block.
|
||||
-> CR.Reg s (ArchRegStruct arch)
|
||||
-- ^ Register that stores Macaw registers
|
||||
-> M.ParsedBlock arch ids
|
||||
-> MacawMonad arch ids s [CR.Block (MacawExt arch) s (MacawFunctionResult arch)]
|
||||
addParsedBlock tfns ctx blockLabelMap posFn b = do
|
||||
addParsedBlock tfns baseAddrMap blockLabelMap posFn regReg b = do
|
||||
let base = M.pblockAddr b
|
||||
let thisPosFn :: M.ArchAddrWord arch -> C.Position
|
||||
thisPosFn off = posFn r
|
||||
where Just r = M.incSegmentOff base (toInteger off)
|
||||
addStatementList tfns ctx blockLabelMap (M.pblockAddr b) thisPosFn [(0, M.blockStatementList b)] []
|
||||
addStatementList tfns baseAddrMap blockLabelMap (M.pblockAddr b) thisPosFn regReg [(0, M.blockStatementList b)] []
|
||||
|
||||
@ -23,23 +23,13 @@ module Data.Macaw.Symbolic.PersistentState
|
||||
-- * Types
|
||||
, ToCrucibleBaseType
|
||||
, ToCrucibleType
|
||||
, ArchAddrCrucibleType
|
||||
, CtxToCrucibleType
|
||||
, ArchRegContext
|
||||
, ArchCrucibleRegTypes
|
||||
, ArchRegStruct
|
||||
, MacawFunctionArgs
|
||||
, MacawFunctionResult
|
||||
, typeToCrucibleBase
|
||||
, typeToCrucible
|
||||
, typeCtxToCrucible
|
||||
, regStructRepr
|
||||
, macawAssignToCrucM
|
||||
, memReprToCrucible
|
||||
-- * CrucGenContext
|
||||
, CrucGenContext(..)
|
||||
, archWidthRepr
|
||||
, MemSegmentMap
|
||||
-- * Register index map
|
||||
, RegIndexMap
|
||||
, mkRegIndexMap
|
||||
@ -49,19 +39,14 @@ module Data.Macaw.Symbolic.PersistentState
|
||||
) where
|
||||
|
||||
import qualified Data.Macaw.CFG as M
|
||||
import qualified Data.Macaw.Memory as M
|
||||
import qualified Data.Macaw.Types as M
|
||||
import Data.Map.Strict (Map)
|
||||
import Data.Parameterized.Classes
|
||||
import Data.Parameterized.Context
|
||||
import qualified Data.Parameterized.List as P
|
||||
import Data.Parameterized.Map (MapF)
|
||||
import qualified Data.Parameterized.Map as MapF
|
||||
import Data.Parameterized.TraversableF
|
||||
import Data.Parameterized.TraversableFC
|
||||
import qualified Lang.Crucible.CFG.Common as C
|
||||
import qualified Lang.Crucible.CFG.Reg as CR
|
||||
import qualified Lang.Crucible.FunctionHandle as C
|
||||
import qualified Lang.Crucible.Types as C
|
||||
|
||||
------------------------------------------------------------------------
|
||||
@ -105,18 +90,6 @@ macawAssignToCrucM f a =
|
||||
Empty -> pure empty
|
||||
b :> x -> (:>) <$> macawAssignToCrucM f b <*> f x
|
||||
|
||||
-- | Type family for arm registers
|
||||
type family ArchRegContext (arch :: *) :: Ctx M.Type
|
||||
|
||||
-- | List of crucible types for architecture.
|
||||
type ArchCrucibleRegTypes (arch :: *) = CtxToCrucibleType (ArchRegContext arch)
|
||||
|
||||
type ArchRegStruct (arch :: *) = C.StructType (ArchCrucibleRegTypes arch)
|
||||
type MacawFunctionArgs arch = EmptyCtx ::> ArchRegStruct arch
|
||||
type MacawFunctionResult arch = ArchRegStruct arch
|
||||
|
||||
type ArchAddrCrucibleType arch = C.BVType (M.ArchAddrWidth arch)
|
||||
|
||||
typeToCrucibleBase :: M.TypeRepr tp -> C.BaseTypeRepr (ToCrucibleBaseType tp)
|
||||
typeToCrucibleBase tp =
|
||||
case tp of
|
||||
@ -142,6 +115,9 @@ memReprToCrucible = typeToCrucible . M.typeRepr
|
||||
------------------------------------------------------------------------
|
||||
-- RegIndexMap
|
||||
|
||||
-- | Type family for architecture registers
|
||||
type family ArchRegContext (arch :: *) :: Ctx M.Type
|
||||
|
||||
-- | This relates an index from macaw to Crucible.
|
||||
data IndexPair ctx tp = IndexPair { macawIndex :: !(Index ctx tp)
|
||||
, crucibleIndex :: !(Index (CtxToCrucibleType ctx) (ToCrucibleType tp))
|
||||
@ -166,61 +142,6 @@ mkRegIndexMap (a :> r) csz =
|
||||
idx = IndexPair (nextIndex (size a)) (nextIndex csz0)
|
||||
in MapF.insert r idx m
|
||||
|
||||
------------------------------------------------------------------------
|
||||
-- CrucGenContext
|
||||
|
||||
type ArchConstraints arch
|
||||
= ( M.MemWidth (M.ArchAddrWidth arch)
|
||||
, OrdF (M.ArchReg arch)
|
||||
, M.HasRepr (M.ArchReg arch) M.TypeRepr
|
||||
)
|
||||
|
||||
-- | Map from indices of segments without a fixed base address to a
|
||||
-- global variable storing the base address.
|
||||
--
|
||||
-- This uses a global variable so that we can do the translation, and then
|
||||
-- decide where to locate it without requiring us to also pass the values
|
||||
-- around arguments.
|
||||
type MemSegmentMap w = Map M.RegionIndex (C.GlobalVar (C.BVType w))
|
||||
|
||||
--- | Information that does not change during generating Crucible from MAcaw
|
||||
data CrucGenContext arch s
|
||||
= CrucGenContext
|
||||
{ archConstraints :: !(forall a . (ArchConstraints arch => a) -> a)
|
||||
-- ^ Typeclass constraints for architecture
|
||||
, macawRegAssign :: !(Assignment (M.ArchReg arch) (ArchRegContext arch))
|
||||
-- ^ Assignment from register index to the register identifier.
|
||||
, regIndexMap :: !(RegIndexMap arch)
|
||||
-- ^ Map from register identifier to the index in Macaw/Crucible.
|
||||
, handleAlloc :: !(C.HandleAllocator s)
|
||||
-- ^ Handle allocator
|
||||
, memBaseAddrMap :: !(MemSegmentMap (M.ArchAddrWidth arch))
|
||||
-- ^ Map from indices of segments without a fixed base address to a global
|
||||
-- variable storing the base address.
|
||||
}
|
||||
|
||||
archWidthRepr :: forall arch s . CrucGenContext arch s -> M.AddrWidthRepr (M.ArchAddrWidth arch)
|
||||
archWidthRepr ctx = archConstraints ctx $ M.addrWidthRepr (archWidthRepr ctx)
|
||||
|
||||
regStructRepr :: CrucGenContext arch s -> C.TypeRepr (ArchRegStruct arch)
|
||||
regStructRepr ctx = archConstraints ctx $
|
||||
C.StructRepr (typeCtxToCrucible (fmapFC M.typeRepr (macawRegAssign ctx)))
|
||||
|
||||
{-
|
||||
typeName :: M.TypeRepr tp -> String
|
||||
typeName M.BoolTypeRepr = "Bool"
|
||||
typeName (M.BVTypeRepr w) = "BV" ++ show w
|
||||
typeName (M.TupleTypeRepr ctx) = "(" ++ intercalate "," (toListFC typeName ctx) ++ ")"
|
||||
|
||||
endName :: M.Endianness -> String
|
||||
endName M.LittleEndian = "le"
|
||||
endName M.BigEndian = "be"
|
||||
|
||||
widthTypeRepr :: M.AddrWidthRepr w -> C.TypeRepr (C.BVType w)
|
||||
widthTypeRepr M.Addr32 = C.knownRepr
|
||||
widthTypeRepr M.Addr64 = C.knownRepr
|
||||
-}
|
||||
|
||||
------------------------------------------------------------------------
|
||||
-- Misc types
|
||||
|
||||
|
||||
@ -277,14 +277,15 @@ disassembleBlock mem nonce_gen loc max_size = do
|
||||
|
||||
-- | The abstract state for a function begining at a given address.
|
||||
initialX86AbsState :: MemSegmentOff 64 -> AbsBlockState X86Reg
|
||||
initialX86AbsState addr =
|
||||
top & setAbsIP addr
|
||||
& absRegState . boundValue sp_reg .~ concreteStackOffset (relativeSegmentAddr addr) 0
|
||||
-- x87 top register points to top of stack.
|
||||
& absRegState . boundValue X87_TopReg .~ FinSet (Set.singleton 7)
|
||||
-- Direction flag is initially zero.
|
||||
& absRegState . boundValue DF .~ BoolConst False
|
||||
& startAbsStack .~ Map.singleton 0 (StackEntry (BVMemRepr n8 LittleEndian) ReturnAddr)
|
||||
initialX86AbsState addr
|
||||
= top
|
||||
& setAbsIP addr
|
||||
& absRegState . boundValue sp_reg .~ concreteStackOffset (relativeSegmentAddr addr) 0
|
||||
-- x87 top register points to top of stack.
|
||||
& absRegState . boundValue X87_TopReg .~ FinSet (Set.singleton 7)
|
||||
-- Direction flag is initially zero.
|
||||
& absRegState . boundValue DF .~ BoolConst False
|
||||
& startAbsStack .~ Map.singleton 0 (StackEntry (BVMemRepr n8 LittleEndian) ReturnAddr)
|
||||
|
||||
preserveFreeBSDSyscallReg :: X86Reg tp -> Bool
|
||||
preserveFreeBSDSyscallReg r
|
||||
@ -504,7 +505,7 @@ x86_64_info preservePred =
|
||||
, archEndianness = LittleEndian
|
||||
, jumpTableEntrySize = 8
|
||||
, disassembleFn = disassembleBlockFromAbsState
|
||||
, mkInitialAbsState = \_ -> initialX86AbsState
|
||||
, mkInitialAbsState = \_ addr -> initialX86AbsState addr
|
||||
, absEvalArchFn = transferAbsValue
|
||||
, absEvalArchStmt = \s _ -> s
|
||||
, postCallAbsState = x86PostCallAbsState
|
||||
|
||||
@ -199,10 +199,9 @@ getSomeBVLocation v =
|
||||
F.FPMem32 ar -> getBVAddress ar >>= mk . (`MemoryAddr` (floatMemRepr SingleFloatRepr))
|
||||
F.FPMem64 ar -> getBVAddress ar >>= mk . (`MemoryAddr` (floatMemRepr DoubleFloatRepr))
|
||||
F.FPMem80 ar -> getBVAddress ar >>= mk . (`MemoryAddr` (floatMemRepr X86_80FloatRepr))
|
||||
F.ByteReg r
|
||||
| Just r64 <- F.is_low_reg r -> mk (reg_low8 $ X86_GP r64)
|
||||
| Just r64 <- F.is_high_reg r -> mk (reg_high8 $ X86_GP r64)
|
||||
| otherwise -> fail "unknown r8"
|
||||
F.ByteReg (F.LowReg8 r) -> mk $ reg_low8 $ X86_GP $ F.Reg64 r
|
||||
F.ByteReg (F.HighReg8 r) -> mk $ reg_high8 $ X86_GP $ F.Reg64 r
|
||||
F.ByteReg _ -> error "internal: getSomeBVLocation illegal ByteReg"
|
||||
F.WordReg r -> mk (reg16Loc r)
|
||||
F.DWordReg r -> mk (reg32Loc r)
|
||||
F.QWordReg r -> mk (reg64Loc r)
|
||||
@ -267,10 +266,8 @@ getSignExtendedValue v out_w =
|
||||
F.Mem64 ar -> mk =<< getBV64Addr ar
|
||||
F.Mem128 ar -> mk =<< getBV128Addr ar
|
||||
|
||||
F.ByteReg r
|
||||
| Just r64 <- F.is_low_reg r -> mk (reg_low8 $ X86_GP r64)
|
||||
| Just r64 <- F.is_high_reg r -> mk (reg_high8 $ X86_GP r64)
|
||||
| otherwise -> fail "unknown r8"
|
||||
F.ByteReg (F.LowReg8 r) -> mk $ reg_low8 $ X86_GP $ F.Reg64 r
|
||||
F.ByteReg (F.HighReg8 r) -> mk $ reg_high8 $ X86_GP $ F.Reg64 r
|
||||
F.WordReg r -> mk (reg16Loc r)
|
||||
F.DWordReg r -> mk (reg32Loc r)
|
||||
F.QWordReg r -> mk (reg64Loc r)
|
||||
@ -332,10 +329,8 @@ getAddrRegOrSegment v =
|
||||
F.Mem32 ar -> Some . HasRepSize DWordRepVal <$> getBV32Addr ar
|
||||
F.Mem64 ar -> Some . HasRepSize QWordRepVal <$> getBV64Addr ar
|
||||
|
||||
F.ByteReg r
|
||||
| Just r64 <- F.is_low_reg r -> pure $ Some $ HasRepSize ByteRepVal (reg_low8 $ X86_GP r64)
|
||||
| Just r64 <- F.is_high_reg r -> pure $ Some $ HasRepSize ByteRepVal (reg_high8 $ X86_GP r64)
|
||||
| otherwise -> fail "unknown r8"
|
||||
F.ByteReg (F.LowReg8 r) -> pure $ Some $ HasRepSize ByteRepVal $ reg_low8 $ X86_GP $ F.Reg64 r
|
||||
F.ByteReg (F.HighReg8 r) -> pure $ Some $ HasRepSize ByteRepVal $ reg_high8 $ X86_GP $ F.Reg64 r
|
||||
F.WordReg r -> pure $ Some $ HasRepSize WordRepVal (reg16Loc r)
|
||||
F.DWordReg r -> pure $ Some $ HasRepSize DWordRepVal (reg32Loc r)
|
||||
F.QWordReg r -> pure $ Some $ HasRepSize QWordRepVal (reg64Loc r)
|
||||
|
||||
@ -713,8 +713,8 @@ exec_sh lw l val val_setter cf_setter of_setter = do
|
||||
case val of
|
||||
F.ByteImm i ->
|
||||
pure (bvLit n8 (toInteger i))
|
||||
F.ByteReg r | Just r64 <- F.is_low_reg r -> do
|
||||
get (reg_low8 $ R.X86_GP r64)
|
||||
F.ByteReg (F.LowReg8 r) -> do
|
||||
get $ reg_low8 $ R.X86_GP $ F.Reg64 r
|
||||
_ -> fail "Count could not be interpreted."
|
||||
v <- get l
|
||||
-- The intel manual says that the count is masked to give an upper
|
||||
|
||||
@ -23,22 +23,25 @@ module Data.Macaw.X86.X86Flag
|
||||
import qualified Data.Vector as V
|
||||
import Data.Word
|
||||
|
||||
-- | X86 flag
|
||||
-- | A bit in an x86_64 flag register.
|
||||
--
|
||||
-- We only model a subset of the full 64 bits in RFLAGS. The supported
|
||||
-- registers have pattern synonyms, and the full list is in `flagList`.
|
||||
newtype X86Flag = X86Flag { flagIndex :: Word8 }
|
||||
deriving (Eq, Ord)
|
||||
|
||||
flagNames :: V.Vector String
|
||||
flagNames = V.fromList
|
||||
[ "cf", "RESERVED", "pf", "RESERVED", "af", "RESERVED"
|
||||
, "zf", "sf", "tf", "if", "df", "of"
|
||||
, "iopl", "nt", "SBZ", "rf", "vm", "ac", "vif", "vip", "id"
|
||||
[ "cf", "RESERVED_1", "pf", "RESERVED_3", "af", "RESERVED_5", "zf", "sf"
|
||||
, "tf", "if", "df", "of", "iopl1", "iopl2", "nt", "RESERVED_15"
|
||||
, "rf", "vm", "ac", "vif", "vip", "id"
|
||||
]
|
||||
|
||||
instance Show X86Flag where
|
||||
show (X86Flag i) =
|
||||
case flagNames V.!? fromIntegral i of
|
||||
Just nm -> nm
|
||||
Nothing -> "Unknown" ++ show i
|
||||
Nothing -> "RESERVED_" ++ show i
|
||||
|
||||
pattern CF :: X86Flag
|
||||
pattern CF = X86Flag 0
|
||||
@ -69,4 +72,4 @@ pattern OF = X86Flag 11
|
||||
|
||||
-- | Return list of x86 flags
|
||||
flagList :: [X86Flag]
|
||||
flagList = X86Flag <$> [0,2,4,6,7,8,9,10,11]
|
||||
flagList = [ CF, PF, AF, ZF, SF, TF, IF, DF, OF ]
|
||||
|
||||
@ -364,7 +364,7 @@ x86SyscallArgumentRegs :: [ X86Reg (BVType 64) ]
|
||||
x86SyscallArgumentRegs = X86_GP <$> [ F.RDI, F.RSI, F.RDX, F.R10, F.R8, F.R9 ]
|
||||
|
||||
gpRegList :: [X86Reg (BVType 64)]
|
||||
gpRegList = [X86_GP (F.reg64 i) | i <- [0..15]]
|
||||
gpRegList = [X86_GP (F.Reg64 i) | i <- [0..15]]
|
||||
|
||||
flagRegList :: [X86Reg BoolType]
|
||||
flagRegList = X86_FlagReg <$> R.flagList
|
||||
|
||||
@ -8,13 +8,13 @@ license: BSD3
|
||||
license-file: LICENSE
|
||||
|
||||
library
|
||||
build-depends:
|
||||
base >= 4,
|
||||
crucible,
|
||||
macaw-base,
|
||||
macaw-symbolic,
|
||||
macaw-x86,
|
||||
parameterized-utils
|
||||
build-depends: base >= 4,
|
||||
crucible,
|
||||
flexdis86,
|
||||
macaw-base,
|
||||
macaw-symbolic,
|
||||
macaw-x86,
|
||||
parameterized-utils
|
||||
hs-source-dirs: src
|
||||
|
||||
exposed-modules:
|
||||
@ -22,3 +22,23 @@ library
|
||||
|
||||
ghc-options: -Wall -Werror
|
||||
ghc-prof-options: -O2 -fprof-auto-top
|
||||
|
||||
test-suite macaw-x86-symbolic-tests
|
||||
type: exitcode-stdio-1.0
|
||||
default-language: Haskell2010
|
||||
ghc-options: -Wall
|
||||
main-is: Main.hs
|
||||
hs-source-dirs: tests
|
||||
build-depends:
|
||||
base >= 4,
|
||||
bytestring,
|
||||
containers,
|
||||
crucible,
|
||||
elf-edit,
|
||||
macaw-base,
|
||||
macaw-symbolic,
|
||||
macaw-x86,
|
||||
macaw-x86-symbolic,
|
||||
parameterized-utils,
|
||||
text,
|
||||
vector
|
||||
|
||||
@ -1,43 +1,131 @@
|
||||
{-# LANGUAGE DataKinds #-}
|
||||
{-# LANGUAGE PolyKinds #-}
|
||||
{-# LANGUAGE TypeFamilies #-}
|
||||
{-# LANGUAGE TypeOperators #-}
|
||||
{-# LANGUAGE FlexibleInstances #-}
|
||||
{-# LANGUAGE MultiParamTypeClasses #-}
|
||||
{-# LANGUAGE TypeSynonymInstances #-}
|
||||
{-# LANGUAGE UndecidableInstances #-}
|
||||
module Data.Macaw.X86.Symbolic
|
||||
( x86TranslateFunctions
|
||||
( x86_64MacawSymbolicFns
|
||||
) where
|
||||
|
||||
import Data.Parameterized.Context as Ctx
|
||||
import GHC.TypeLits
|
||||
|
||||
import qualified Data.Macaw.CFG as M
|
||||
import Data.Macaw.Symbolic
|
||||
import qualified Data.Macaw.Types as M
|
||||
import qualified Data.Macaw.X86 as M
|
||||
import Data.Parameterized.Context as Ctx
|
||||
import qualified Data.Macaw.X86.X86Reg as M
|
||||
import qualified Flexdis86.Register as F
|
||||
|
||||
import qualified Lang.Crucible.CFG.Reg as C
|
||||
import qualified Lang.Crucible.Solver.Symbol as C
|
||||
|
||||
------------------------------------------------------------------------
|
||||
-- Utilities for generating a type-level context with repeated elements.
|
||||
|
||||
type family CtxRepeat (n :: Nat) (c :: k) :: Ctx k where
|
||||
CtxRepeat 0 c = EmptyCtx
|
||||
CtxRepeat 1 c = CtxRepeat 0 c ::> c
|
||||
CtxRepeat 2 c = CtxRepeat 1 c ::> c
|
||||
CtxRepeat 3 c = CtxRepeat 2 c ::> c
|
||||
CtxRepeat 4 c = CtxRepeat 3 c ::> c
|
||||
CtxRepeat 5 c = CtxRepeat 4 c ::> c
|
||||
CtxRepeat 6 c = CtxRepeat 5 c ::> c
|
||||
CtxRepeat 7 c = CtxRepeat 6 c ::> c
|
||||
CtxRepeat 8 c = CtxRepeat 7 c ::> c
|
||||
CtxRepeat 9 c = CtxRepeat 8 c ::> c
|
||||
CtxRepeat 10 c = CtxRepeat 9 c ::> c
|
||||
CtxRepeat 11 c = CtxRepeat 10 c ::> c
|
||||
CtxRepeat 12 c = CtxRepeat 11 c ::> c
|
||||
CtxRepeat 13 c = CtxRepeat 12 c ::> c
|
||||
CtxRepeat 14 c = CtxRepeat 13 c ::> c
|
||||
CtxRepeat 15 c = CtxRepeat 14 c ::> c
|
||||
CtxRepeat 16 c = CtxRepeat 15 c ::> c
|
||||
|
||||
class RepeatAssign (tp :: k) (ctx :: Ctx k) where
|
||||
repeatAssign :: (Int -> f tp) -> Assignment f ctx
|
||||
|
||||
instance RepeatAssign tp EmptyCtx where
|
||||
repeatAssign _ = Empty
|
||||
|
||||
instance RepeatAssign tp ctx => RepeatAssign tp (ctx ::> tp) where
|
||||
repeatAssign f =
|
||||
let r = repeatAssign f
|
||||
in r :> f (sizeInt (Ctx.size r))
|
||||
|
||||
------------------------------------------------------------------------
|
||||
-- X86 Registers
|
||||
|
||||
type instance ArchRegContext M.X86_64
|
||||
= EmptyCtx -- TODO: Fix this
|
||||
= (EmptyCtx ::> M.BVType 64)
|
||||
<+> CtxRepeat 16 (M.BVType 64)
|
||||
<+> CtxRepeat 9 M.BoolType
|
||||
<+> CtxRepeat 16 M.BoolType
|
||||
<+> (EmptyCtx ::> M.BVType 3)
|
||||
<+> CtxRepeat 8 (M.BVType 2)
|
||||
<+> CtxRepeat 8 (M.BVType 80)
|
||||
<+> CtxRepeat 16 (M.BVType 128)
|
||||
|
||||
x86RegName :: M.X86Reg tp -> C.SolverSymbol
|
||||
x86RegName = undefined
|
||||
x86RegName M.X86_IP = C.systemSymbol "!ip"
|
||||
x86RegName (M.X86_GP r) = C.systemSymbol $ "!" ++ show r
|
||||
x86RegName (M.X86_FlagReg r) = C.systemSymbol $ "!" ++ show r
|
||||
x86RegName (M.X87_StatusReg r) = C.systemSymbol $ "!x87Status" ++ show r
|
||||
x86RegName M.X87_TopReg = C.systemSymbol $ "!x87Top"
|
||||
x86RegName (M.X87_TagReg r) = C.systemSymbol $ "!x87Tag" ++ show r
|
||||
x86RegName (M.X87_FPUReg r) = C.systemSymbol $ "!" ++ show r
|
||||
x86RegName (M.X86_XMMReg r) = C.systemSymbol $ "!" ++ show r
|
||||
|
||||
gpReg :: Int -> M.X86Reg (M.BVType 64)
|
||||
gpReg = M.X86_GP . F.Reg64 . fromIntegral
|
||||
|
||||
-- | The x86 flag registers that are directly supported by Macw.
|
||||
flagRegs :: Assignment M.X86Reg (CtxRepeat 9 M.BoolType)
|
||||
flagRegs =
|
||||
Empty :> M.CF :> M.PF :> M.AF :> M.ZF :> M.SF :> M.TF :> M.IF :> M.DF :> M.OF
|
||||
|
||||
-- | This contains an assignment that stores the register associated with each index in the
|
||||
-- X86 register structure.
|
||||
x86RegAssignment :: Assignment M.X86Reg (ArchRegContext M.X86_64)
|
||||
x86RegAssignment = undefined
|
||||
x86RegAssignment =
|
||||
Empty :> M.X86_IP
|
||||
<++> (repeatAssign gpReg :: Assignment M.X86Reg (CtxRepeat 16 (M.BVType 64)))
|
||||
<++> flagRegs
|
||||
<++> (repeatAssign (M.X87_StatusReg . fromIntegral) :: Assignment M.X86Reg (CtxRepeat 16 M.BoolType))
|
||||
<++> (Empty :> M.X87_TopReg)
|
||||
<++> (repeatAssign (M.X87_TagReg . fromIntegral) :: Assignment M.X86Reg (CtxRepeat 8 (M.BVType 2)))
|
||||
<++> (repeatAssign (M.X87_FPUReg . F.mmxReg . fromIntegral) :: Assignment M.X86Reg (CtxRepeat 8 (M.BVType 80)))
|
||||
<++> (repeatAssign (M.X86_XMMReg . F.xmmReg . fromIntegral) :: Assignment M.X86Reg (CtxRepeat 16 (M.BVType 128)))
|
||||
|
||||
------------------------------------------------------------------------
|
||||
-- Other X86 specific
|
||||
|
||||
crucGenX86Fn :: M.X86PrimFn (M.Value M.X86_64 ids) tp
|
||||
-> CrucGen M.X86_64 ids s (C.Atom s (ToCrucibleType tp))
|
||||
crucGenX86Fn = undefined
|
||||
crucGenX86Fn fn =
|
||||
case fn of
|
||||
_ -> undefined fn
|
||||
|
||||
crucGenX86Stmt :: M.X86Stmt (M.Value M.X86_64 ids)
|
||||
-> CrucGen M.X86_64 ids s ()
|
||||
crucGenX86Stmt = undefined
|
||||
crucGenX86Stmt stmt =
|
||||
case stmt of
|
||||
_ -> undefined stmt
|
||||
|
||||
crucGenX86TermStmt :: M.X86TermStmt ids
|
||||
-> M.RegState M.X86Reg (M.Value M.X86_64 ids)
|
||||
-> CrucGen M.X86_64 ids s ()
|
||||
crucGenX86TermStmt = undefined
|
||||
crucGenX86TermStmt tstmt regs =
|
||||
case tstmt of
|
||||
_ -> undefined regs
|
||||
|
||||
-- | The symbolic tra
|
||||
x86TranslateFunctions :: CrucGenArchFunctions M.X86_64
|
||||
x86TranslateFunctions =
|
||||
CrucGenArchFunctions
|
||||
x86_64MacawSymbolicFns :: MacawSymbolicArchFunctions M.X86_64
|
||||
x86_64MacawSymbolicFns =
|
||||
MacawSymbolicArchFunctions
|
||||
{ crucGenArchConstraints = \x -> x
|
||||
, crucGenRegAssignment = x86RegAssignment
|
||||
, crucGenArchRegName = x86RegName
|
||||
|
||||
128
x86_symbolic/tests/Main.hs
Normal file
128
x86_symbolic/tests/Main.hs
Normal file
@ -0,0 +1,128 @@
|
||||
{-# LANGUAGE FlexibleContexts #-}
|
||||
{-# LANGUAGE GADTs #-}
|
||||
{-# LANGUAGE DataKinds #-}
|
||||
{-# LANGUAGE OverloadedStrings #-}
|
||||
module Main (main) where
|
||||
|
||||
import Control.Monad
|
||||
import Control.Monad.ST
|
||||
import qualified Data.ByteString as BS
|
||||
import qualified Data.ElfEdit as Elf
|
||||
import Data.Parameterized.Nonce
|
||||
import Data.Parameterized.Some
|
||||
import qualified Data.Text as Text
|
||||
import qualified Data.Map.Strict as Map
|
||||
import System.IO
|
||||
import GHC.IO (ioToST)
|
||||
|
||||
import qualified Data.Macaw.Architecture.Info as M
|
||||
import qualified Data.Macaw.CFG.Core as M
|
||||
import qualified Data.Macaw.Discovery as M
|
||||
import qualified Data.Macaw.Memory as M
|
||||
import qualified Data.Macaw.Memory.ElfLoader as Elf
|
||||
import qualified Data.Macaw.Symbolic as MS
|
||||
import qualified Data.Macaw.Types as M
|
||||
import qualified Data.Macaw.X86 as MX
|
||||
import qualified Data.Macaw.X86.Symbolic as MX
|
||||
|
||||
import qualified Lang.Crucible.CFG.Core as C
|
||||
import qualified Lang.Crucible.FunctionHandle as C
|
||||
import qualified Lang.Crucible.ProgramLoc as C
|
||||
import qualified Lang.Crucible.Simulator.ExecutionTree as C
|
||||
import qualified Lang.Crucible.Simulator.RegValue as C
|
||||
import qualified Lang.Crucible.Solver.Interface as C
|
||||
import qualified Lang.Crucible.Solver.SimpleBackend as C
|
||||
|
||||
mkReg :: (C.IsSymInterface sym, M.HasRepr (M.ArchReg arch) M.TypeRepr)
|
||||
=> MS.MacawSymbolicArchFunctions arch
|
||||
-> sym
|
||||
-> M.ArchReg arch tp
|
||||
-> IO (C.RegValue' sym (MS.ToCrucibleType tp))
|
||||
mkReg archFns sym r =
|
||||
case M.typeRepr r of
|
||||
M.BoolTypeRepr ->
|
||||
C.RV <$> C.freshConstant sym (MS.crucGenArchRegName archFns r) C.BaseBoolRepr
|
||||
M.BVTypeRepr w ->
|
||||
C.RV <$> C.freshConstant sym (MS.crucGenArchRegName archFns r) (C.BaseBVRepr w)
|
||||
M.TupleTypeRepr{} ->
|
||||
error "macaw-symbolic do not support tuple types."
|
||||
|
||||
main :: IO ()
|
||||
main = do
|
||||
putStrLn "Start test case"
|
||||
Some gen <- newIONonceGenerator
|
||||
halloc <- C.newHandleAllocator
|
||||
sym <- C.newSimpleBackend gen
|
||||
let x86ArchFns :: MS.MacawSymbolicArchFunctions MX.X86_64
|
||||
x86ArchFns = MX.x86_64MacawSymbolicFns
|
||||
|
||||
let posFn :: M.MemSegmentOff 64 -> C.Position
|
||||
posFn = C.OtherPos . Text.pack . show
|
||||
|
||||
let loadOpt :: Elf.LoadOptions
|
||||
loadOpt = Elf.LoadOptions { Elf.loadRegionIndex = 1
|
||||
, Elf.loadStyle = Elf.LoadBySection
|
||||
, Elf.includeBSS = False
|
||||
}
|
||||
putStrLn "Read elf"
|
||||
elfContents <- BS.readFile "tests/add_ubuntu64.o"
|
||||
elf <-
|
||||
case Elf.parseElf elfContents of
|
||||
Elf.Elf64Res errs e -> do
|
||||
unless (null errs) $
|
||||
fail "Error parsing Elf file"
|
||||
pure e
|
||||
_ -> fail "Expected 64-bit elf file"
|
||||
(secIdxMap, mem) <-
|
||||
case Elf.memoryForElf loadOpt elf of
|
||||
Left err -> fail err
|
||||
Right r -> pure r
|
||||
|
||||
let (symErrs, nameAddrList) = Elf.resolveElfFuncSymbols mem secIdxMap elf
|
||||
forM_ symErrs $ \err -> do
|
||||
hPutStrLn stderr $ show err
|
||||
|
||||
putStrLn "Lookup addr"
|
||||
addAddr <-
|
||||
case [ addr | ("add", addr) <- nameAddrList ] of
|
||||
[addr] -> pure $! addr
|
||||
[] -> fail "Could not find add function"
|
||||
_ -> fail "Found multiple add functions"
|
||||
putStrLn $ "Addr " ++ show addAddr
|
||||
|
||||
memBaseVar <- stToIO $ C.freshGlobalVar halloc "add_mem_base" C.knownRepr
|
||||
|
||||
let memBaseVarMap :: MS.MemSegmentMap 64
|
||||
memBaseVarMap = Map.singleton 1 memBaseVar
|
||||
|
||||
let addrSymMap :: M.AddrSymMap 64
|
||||
addrSymMap = Map.fromList [ (addr,nm) | (nm,addr) <- nameAddrList ]
|
||||
let archInfo :: M.ArchitectureInfo MX.X86_64
|
||||
archInfo = MX.x86_64_linux_info
|
||||
|
||||
let ds0 :: M.DiscoveryState MX.X86_64
|
||||
ds0 = M.emptyDiscoveryState mem addrSymMap archInfo
|
||||
|
||||
putStrLn "Analyze a function"
|
||||
let logFn addr = ioToST $ do
|
||||
putStrLn $ "Analyzing " ++ show addr
|
||||
|
||||
(_, Some funInfo) <- stToIO $ M.analyzeFunction logFn addAddr M.UserRequest ds0
|
||||
putStrLn "Make CFG"
|
||||
C.SomeCFG g <- stToIO $ MS.mkFunCFG x86ArchFns halloc memBaseVarMap "add" posFn funInfo
|
||||
|
||||
regs <- MS.macawAssignToCrucM (mkReg x86ArchFns sym) (MS.crucGenRegAssignment x86ArchFns)
|
||||
putStrLn "Run code block"
|
||||
execResult <- MS.runCodeBlock sym x86ArchFns halloc g regs
|
||||
case execResult of
|
||||
C.FinishedExecution _ (C.TotalRes _pair) -> do
|
||||
putStrLn "Done"
|
||||
_ -> do
|
||||
fail "Partial execution returned."
|
||||
|
||||
{-
|
||||
-- Steps:
|
||||
-- Load up Elf file.
|
||||
-- Call symbolic simulator
|
||||
-- Check Result
|
||||
-}
|
||||
14
x86_symbolic/tests/add.c
Normal file
14
x86_symbolic/tests/add.c
Normal file
@ -0,0 +1,14 @@
|
||||
/*
|
||||
|
||||
This is a small file designed to create a minimal test of the symbolic simulator.
|
||||
|
||||
It can be compiled with:
|
||||
|
||||
clang -o test_add.o -O2 -c -momit-leaf-frame-pointer test_add.c
|
||||
*/
|
||||
|
||||
#include <stdint.h>
|
||||
|
||||
uint64_t add(uint64_t x, uint64_t y) {
|
||||
return x + y;
|
||||
}
|
||||
BIN
x86_symbolic/tests/add_ubuntu64.o
Normal file
BIN
x86_symbolic/tests/add_ubuntu64.o
Normal file
Binary file not shown.
Loading…
Reference in New Issue
Block a user