mirror of
https://github.com/GaloisInc/macaw.git
synced 2024-12-29 00:59:09 +03:00
Update for parameterized-utils compat.
This commit is contained in:
Joe Hendrix
parent
3f32b82943
commit
deab99869d
@ -21,7 +21,7 @@ library
|
||||
hs-source-dirs: src
|
||||
|
||||
exposed-modules:
|
||||
Data.Macaw.Symbolic.App
|
||||
Data.Macaw.Symbolic.CrucGen
|
||||
Data.Macaw.Symbolic.PersistentState
|
||||
Data.Macaw.Symbolic
|
||||
|
||||
|
||||
@ -1,14 +1,19 @@
|
||||
{-# LANGUAGE CPP #-}
|
||||
{-# LANGUAGE DataKinds #-}
|
||||
{-# LANGUAGE FlexibleContexts #-}
|
||||
{-# LANGUAGE KindSignatures #-}
|
||||
{-# LANGUAGE PatternSynonyms #-}
|
||||
{-# LANGUAGE RankNTypes #-}
|
||||
{-# LANGUAGE ScopedTypeVariables #-}
|
||||
{-# LANGUAGE TypeFamilies #-}
|
||||
{-# LANGUAGE TypeOperators #-}
|
||||
module Data.Macaw.Symbolic
|
||||
( ArchTranslateFunctions(..)
|
||||
( Data.Macaw.Symbolic.CrucGen.CrucGenArchFunctions(..)
|
||||
, Data.Macaw.Symbolic.CrucGen.CrucGen
|
||||
, MacawSimulatorState
|
||||
, stepBlocks
|
||||
, Data.Macaw.Symbolic.PersistentState.ArchRegContext
|
||||
, Data.Macaw.Symbolic.PersistentState.ToCrucibleType
|
||||
) where
|
||||
|
||||
import Control.Monad.Except
|
||||
@ -16,8 +21,7 @@ import Control.Monad.ST
|
||||
import Control.Monad.State.Strict
|
||||
import Data.Map.Strict (Map)
|
||||
import qualified Data.Map.Strict as Map
|
||||
import Data.Parameterized.Ctx
|
||||
import qualified Data.Parameterized.Context as Ctx
|
||||
import Data.Parameterized.Context as Ctx
|
||||
import qualified Data.Parameterized.Map as MapF
|
||||
import Data.Parameterized.TraversableFC
|
||||
import qualified Data.Set as Set
|
||||
@ -42,7 +46,7 @@ import qualified Data.Macaw.CFG.Core as M
|
||||
import qualified Data.Macaw.Memory as M
|
||||
import qualified Data.Macaw.Types as M
|
||||
|
||||
import Data.Macaw.Symbolic.App
|
||||
import Data.Macaw.Symbolic.CrucGen
|
||||
import Data.Macaw.Symbolic.PersistentState
|
||||
|
||||
data MacawSimulatorState sym = MacawSimulatorState
|
||||
@ -54,16 +58,19 @@ regVars :: (IsSymInterface sym, M.HasRepr reg M.TypeRepr)
|
||||
-> Ctx.Assignment reg ctx
|
||||
-> IO (Ctx.Assignment (C.RegValue' sym) (CtxToCrucibleType ctx))
|
||||
regVars sym nameFn a =
|
||||
case Ctx.view a of
|
||||
Ctx.AssignEmpty -> pure Ctx.empty
|
||||
Ctx.AssignExtend b reg -> do
|
||||
case a of
|
||||
Empty -> pure Ctx.empty
|
||||
b :> reg -> do
|
||||
varAssign <- regVars sym nameFn b
|
||||
c <- freshConstant sym (nameFn reg) (typeToCrucibleBase (M.typeRepr reg))
|
||||
pure (varAssign Ctx.%> C.RV c)
|
||||
pure (varAssign :> C.RV c)
|
||||
#if !MIN_VERSION_base(4,10,0)
|
||||
_ -> error "internal: regVars encountered case non-exhaustive pattern"
|
||||
#endif
|
||||
|
||||
runFreshSymOverride :: M.TypeRepr tp
|
||||
-> C.OverrideSim MacawSimulatorState sym ret
|
||||
Ctx.EmptyCtx
|
||||
EmptyCtx
|
||||
(ToCrucibleType tp)
|
||||
(C.RegValue sym (ToCrucibleType tp))
|
||||
runFreshSymOverride = undefined
|
||||
@ -135,7 +142,7 @@ mkMemBaseVarMap halloc mem = do
|
||||
stepBlocks :: forall sym arch ids
|
||||
. (IsSymInterface sym, M.ArchConstraints arch)
|
||||
=> sym
|
||||
-> ArchTranslateFunctions arch
|
||||
-> CrucGenArchFunctions arch
|
||||
-> M.Memory (M.ArchAddrWidth arch)
|
||||
-- ^ Memory image for executable
|
||||
-> Text
|
||||
@ -151,11 +158,11 @@ stepBlocks :: forall sym arch ids
|
||||
sym
|
||||
(C.RegEntry sym (C.StructType (CtxToCrucibleType (ArchRegContext arch)))))
|
||||
stepBlocks sym sinfo mem binPath nm addr macawBlocks = do
|
||||
let regAssign = archRegAssignment sinfo
|
||||
let regAssign = crucGenRegAssignment sinfo
|
||||
let crucRegTypes = typeCtxToCrucible (fmapFC M.typeRepr regAssign)
|
||||
let macawStructRepr = C.StructRepr crucRegTypes
|
||||
halloc <- C.newHandleAllocator
|
||||
let argTypes = Ctx.empty Ctx.%> macawStructRepr
|
||||
let argTypes = Empty :> macawStructRepr
|
||||
h <- stToIO $ C.mkHandle' halloc nm argTypes macawStructRepr
|
||||
-- Map block map to Crucible CFG
|
||||
let blockLabelMap :: Map Word64 (CR.Label RealWorld)
|
||||
@ -197,7 +204,7 @@ stepBlocks sym sinfo mem binPath nm addr macawBlocks = do
|
||||
let s = C.initSimState ctx C.emptyGlobals C.defaultErrorHandler
|
||||
-- Define the arguments to call the Reopt CFG with.
|
||||
-- This should be a symbolic variable for each register in the architecture.
|
||||
regStruct <- regVars sym (archRegNameFn sinfo) regAssign
|
||||
regStruct <- regVars sym (crucGenArchRegName sinfo) regAssign
|
||||
let args :: C.RegMap sym (MacawFunctionArgs arch)
|
||||
args = C.RegMap (Ctx.singleton (C.RegEntry macawStructRepr regStruct))
|
||||
-- Run the symbolic simulator.
|
||||
|
||||
@ -16,13 +16,14 @@ This defines the core operations for mapping from Reopt to Crucible.
|
||||
{-# LANGUAGE TypeFamilies #-}
|
||||
{-# LANGUAGE TypeOperators #-}
|
||||
{-# OPTIONS_GHC -Wwarn #-}
|
||||
module Data.Macaw.Symbolic.App
|
||||
( ArchTranslateFunctions(..)
|
||||
, MacawMonad
|
||||
module Data.Macaw.Symbolic.CrucGen
|
||||
( CrucGenArchFunctions(..)
|
||||
-- ** Operations for implementing new backends.
|
||||
, CrucGen
|
||||
, addMacawBlock
|
||||
) where
|
||||
|
||||
import Control.Lens
|
||||
import Control.Lens hiding (Empty, (:>))
|
||||
import Control.Monad.Except
|
||||
import Control.Monad.ST
|
||||
import Control.Monad.State.Strict
|
||||
@ -32,7 +33,7 @@ import qualified Data.Macaw.CFG.Block as M
|
||||
import qualified Data.Macaw.Memory as M
|
||||
import qualified Data.Macaw.Types as M
|
||||
import qualified Data.Map.Strict as Map
|
||||
import qualified Data.Parameterized.Context as Ctx
|
||||
import Data.Parameterized.Context as Ctx
|
||||
import Data.Parameterized.Map (MapF)
|
||||
import qualified Data.Parameterized.Map as MapF
|
||||
import Data.Parameterized.NatRepr
|
||||
@ -54,34 +55,38 @@ import Data.Macaw.Symbolic.PersistentState
|
||||
-- CrucPersistentState
|
||||
|
||||
-- | Architecture-specific information needed to translate from Macaw to Crucible
|
||||
data ArchTranslateFunctions arch
|
||||
= ArchTranslateFunctions
|
||||
{ archRegNameFn :: !(forall tp . M.ArchReg arch tp -> C.SolverSymbol)
|
||||
, archRegAssignment :: !(Ctx.Assignment (M.ArchReg arch) (ArchRegContext arch))
|
||||
data CrucGenArchFunctions arch
|
||||
= CrucGenArchFunctions
|
||||
{ crucGenArchConstraints :: !(forall a . (M.MemWidth (M.ArchAddrWidth arch) => a) -> a)
|
||||
, crucGenRegAssignment :: !(Ctx.Assignment (M.ArchReg arch) (ArchRegContext arch))
|
||||
-- ^ Map from indices in the ArchRegContext to the associated register.
|
||||
, archTranslateFn :: !(forall ids s tp
|
||||
, crucGenArchRegName :: !(forall tp . M.ArchReg arch tp -> C.SolverSymbol)
|
||||
-- ^ Provides a solver name to use for referring to register.
|
||||
, crucGenArchFn :: !(forall ids s tp
|
||||
. M.ArchFn arch (M.Value arch ids) tp
|
||||
-> CrucGen arch ids s (CR.Atom s (ToCrucibleType tp)))
|
||||
-- ^ Function for translating an architecture specific function
|
||||
, archTranslateStmt :: !(forall ids s . M.ArchStmt arch (M.Value arch ids) -> CrucGen arch ids s ())
|
||||
, archTranslateTermStmt :: !(forall ids s
|
||||
-- ^ Generate crucible for architecture-specific function.
|
||||
, crucGenArchStmt
|
||||
:: !(forall ids s . M.ArchStmt arch (M.Value arch ids) -> CrucGen arch ids s ())
|
||||
-- ^ Generate crucible for architecture-specific statement.
|
||||
, crucGenArchTermStmt :: !(forall ids s
|
||||
. M.ArchTermStmt arch ids
|
||||
-> M.RegState (M.ArchReg arch) (M.Value arch ids)
|
||||
-> CrucGen arch ids s ())
|
||||
-- ^ Generate crucible for architecture-specific terminal statement.
|
||||
}
|
||||
|
||||
-- | State used for generating blocks
|
||||
data CrucGenState arch ids s
|
||||
= CrucGenState
|
||||
{ translateFns :: !(ArchTranslateFunctions arch)
|
||||
{ translateFns :: !(CrucGenArchFunctions arch)
|
||||
, crucCtx :: !(CrucGenContext arch ids s)
|
||||
, crucPState :: !(CrucPersistentState arch ids s)
|
||||
-- ^ State that persists across blocks.
|
||||
, blockLabel :: (CR.Label s)
|
||||
-- ^ Label for this block we are translating
|
||||
, macawBlockIndex :: !Word64
|
||||
, codeAddr :: !Word64
|
||||
-- ^ Address of this code
|
||||
, crucPos :: !C.Position
|
||||
-- ^ Position in the crucible file.
|
||||
, prevStmts :: ![C.Posd (CR.Stmt s)]
|
||||
-- ^ List of states in reverse order
|
||||
}
|
||||
@ -89,28 +94,30 @@ data CrucGenState arch ids s
|
||||
crucPStateLens :: Simple Lens (CrucGenState arch ids s) (CrucPersistentState arch ids s)
|
||||
crucPStateLens = lens crucPState (\s v -> s { crucPState = v })
|
||||
|
||||
assignValueMapLens :: Simple Lens (CrucGenState arch ids s)
|
||||
assignValueMapLens :: Simple Lens (CrucPersistentState arch ids s)
|
||||
(MapF (M.AssignId ids) (MacawCrucibleValue (CR.Atom s)))
|
||||
assignValueMapLens = crucPStateLens . lens assignValueMap (\s v -> s { assignValueMap = v })
|
||||
assignValueMapLens = lens assignValueMap (\s v -> s { assignValueMap = v })
|
||||
|
||||
newtype CrucGen arch ids s r
|
||||
= CrucGen { unContGen
|
||||
= CrucGen { unCrucGen
|
||||
:: CrucGenState arch ids s
|
||||
-> (CrucGenState arch ids s -> r -> ST s (CrucPersistentState arch ids s))
|
||||
-> ST s (CrucPersistentState arch ids s)
|
||||
-> (CrucGenState arch ids s
|
||||
-> r
|
||||
-> ST s (CrucPersistentState arch ids s, CR.Block s (MacawFunctionResult arch)))
|
||||
-> ST s (CrucPersistentState arch ids s, CR.Block s (MacawFunctionResult arch))
|
||||
}
|
||||
|
||||
instance Functor (CrucGen arch ids s) where
|
||||
fmap f m = CrucGen $ \s0 cont -> unContGen m s0 $ \s1 v -> cont s1 (f v)
|
||||
fmap f m = CrucGen $ \s0 cont -> unCrucGen m s0 $ \s1 v -> cont s1 (f v)
|
||||
|
||||
instance Applicative (CrucGen arch ids s) where
|
||||
pure r = CrucGen $ \s cont -> cont s r
|
||||
mf <*> ma = CrucGen $ \s0 cont -> unContGen mf s0
|
||||
$ \s1 f -> unContGen ma s1
|
||||
mf <*> ma = CrucGen $ \s0 cont -> unCrucGen mf s0
|
||||
$ \s1 f -> unCrucGen ma s1
|
||||
$ \s2 a -> cont s2 (f a)
|
||||
|
||||
instance Monad (CrucGen arch ids s) where
|
||||
m >>= h = CrucGen $ \s0 cont -> unContGen m s0 $ \s1 r -> unContGen (h r) s1 cont
|
||||
m >>= h = CrucGen $ \s0 cont -> unCrucGen m s0 $ \s1 r -> unCrucGen (h r) s1 cont
|
||||
|
||||
instance MonadState (CrucGenState arch ids s) (CrucGen arch ids s) where
|
||||
get = CrucGen $ \s cont -> cont s s
|
||||
@ -122,12 +129,9 @@ getCtx = gets crucCtx
|
||||
liftST :: ST s r -> CrucGen arch ids s r
|
||||
liftST m = CrucGen $ \s cont -> m >>= cont s
|
||||
|
||||
|
||||
-- | Get current position
|
||||
getPos :: CrucGen arch ids s C.Position
|
||||
getPos = do
|
||||
ctx <- getCtx
|
||||
C.BinaryPos (binaryPath ctx) <$> gets codeAddr
|
||||
getPos = gets crucPos
|
||||
|
||||
addStmt :: CR.Stmt s -> CrucGen arch ids s ()
|
||||
addStmt stmt = seq stmt $ do
|
||||
@ -142,11 +146,11 @@ addTermStmt :: CR.TermStmt s (MacawFunctionResult arch)
|
||||
addTermStmt tstmt = do
|
||||
termPos <- getPos
|
||||
CrucGen $ \s _ -> do
|
||||
let lbl = CR.LabelID (blockLabel s)
|
||||
let lbl = blockLabel s
|
||||
let stmts = Seq.fromList (reverse (prevStmts s))
|
||||
let term = C.Posd termPos tstmt
|
||||
let blk = CR.mkBlock lbl Set.empty stmts term
|
||||
pure $! crucPState s & seenBlockMapLens %~ Map.insert (macawBlockIndex s) blk
|
||||
let blk = CR.mkBlock (CR.LabelID lbl) Set.empty stmts term
|
||||
pure $ (crucPState s, blk)
|
||||
|
||||
freshValueIndex :: CrucGen arch ids s Int
|
||||
freshValueIndex = do
|
||||
@ -337,11 +341,12 @@ valueToCrucible v = do
|
||||
Nothing -> fail $ "internal: Register is not bound."
|
||||
M.AssignedValue asgn -> do
|
||||
let idx = M.assignId asgn
|
||||
amap <- use assignValueMapLens
|
||||
amap <- use $ crucPStateLens . assignValueMapLens
|
||||
case MapF.lookup idx amap of
|
||||
Just (MacawCrucibleValue r) -> pure r
|
||||
Nothing -> fail "internal: Assignment id is not bound."
|
||||
|
||||
-- |
|
||||
mkHandleVal :: HandleId arch '(args,ret)
|
||||
-> CrucGen arch ids s (C.FnHandle args ret)
|
||||
mkHandleVal hid = do
|
||||
@ -380,7 +385,7 @@ readMem :: M.ArchAddrValue arch ids
|
||||
readMem addr repr = do
|
||||
hndl <- mkHandleVal (ReadMemId repr)
|
||||
caddr <- valueToCrucible addr
|
||||
callFnHandle hndl (Ctx.empty Ctx.%> caddr)
|
||||
callFnHandle hndl (Empty :> caddr)
|
||||
|
||||
writeMem :: M.ArchAddrValue arch ids
|
||||
-> M.MemRepr tp
|
||||
@ -390,8 +395,7 @@ writeMem addr repr val = do
|
||||
hndl <- mkHandleVal (WriteMemId repr)
|
||||
caddr <- valueToCrucible addr
|
||||
cval <- valueToCrucible val
|
||||
let args = Ctx.empty Ctx.%> caddr Ctx.%> cval
|
||||
void $ callFnHandle hndl args
|
||||
void $ callFnHandle hndl (Empty :> caddr :> cval)
|
||||
|
||||
assignRhsToCrucible :: M.AssignRhs arch (M.Value arch ids) tp
|
||||
-> CrucGen arch ids s (CR.Atom s (ToCrucibleType tp))
|
||||
@ -402,7 +406,7 @@ assignRhsToCrucible rhs =
|
||||
M.ReadMem addr repr -> readMem addr repr
|
||||
M.EvalArchFn f _ -> do
|
||||
fns <- translateFns <$> get
|
||||
archTranslateFn fns f
|
||||
crucGenArchFn fns f
|
||||
|
||||
addMacawStmt :: M.Stmt arch ids -> CrucGen arch ids s ()
|
||||
addMacawStmt stmt =
|
||||
@ -410,20 +414,22 @@ addMacawStmt stmt =
|
||||
M.AssignStmt asgn -> do
|
||||
let idx = M.assignId asgn
|
||||
a <- assignRhsToCrucible (M.assignRhs asgn)
|
||||
assignValueMapLens %= MapF.insert idx (MacawCrucibleValue a)
|
||||
crucPStateLens . assignValueMapLens %= MapF.insert idx (MacawCrucibleValue a)
|
||||
M.WriteMem addr repr val -> do
|
||||
writeMem addr repr val
|
||||
M.PlaceHolderStmt _vals msg -> do
|
||||
cmsg <- crucibleValue (C.TextLit (Text.pack msg))
|
||||
addTermStmt (CR.ErrorStmt cmsg)
|
||||
M.InstructionStart _addr _ -> do
|
||||
-- TODO: Fix this
|
||||
pure ()
|
||||
M.InstructionStart addr _ -> do
|
||||
-- Update the position
|
||||
modify $ \s ->
|
||||
crucGenArchConstraints (translateFns s) $
|
||||
s { crucPos = C.BinaryPos (binaryPath (crucCtx s)) (fromIntegral addr) }
|
||||
M.Comment _txt -> do
|
||||
pure ()
|
||||
M.ExecArchStmt astmt -> do
|
||||
fns <- translateFns <$> get
|
||||
archTranslateStmt fns astmt
|
||||
crucGenArchStmt fns astmt
|
||||
|
||||
lookupCrucibleLabel :: Word64 -> CrucGen arch ids s (CR.Label s)
|
||||
lookupCrucibleLabel idx = do
|
||||
@ -458,15 +464,17 @@ addMacawTermStmt tstmt =
|
||||
addTermStmt (CR.Br p t f)
|
||||
M.ArchTermStmt ts regs -> do
|
||||
fns <- translateFns <$> get
|
||||
archTranslateTermStmt fns ts regs
|
||||
crucGenArchTermStmt fns ts regs
|
||||
M.TranslateError _regs msg -> do
|
||||
cmsg <- crucibleValue (C.TextLit msg)
|
||||
addTermStmt (CR.ErrorStmt cmsg)
|
||||
|
||||
-- | Type level monad for building blocks.
|
||||
-----------------
|
||||
|
||||
-- | Monad for adding new blocks to a state.
|
||||
type MacawMonad arch ids s = ExceptT String (StateT (CrucPersistentState arch ids s) (ST s))
|
||||
|
||||
addMacawBlock :: ArchTranslateFunctions arch
|
||||
addMacawBlock :: CrucGenArchFunctions arch
|
||||
-> CrucGenContext arch ids s
|
||||
-> Word64
|
||||
-- ^ Code address
|
||||
@ -479,17 +487,17 @@ addMacawBlock tfns ctx addr b = do
|
||||
case Map.lookup idx (macawIndexToLabelMap ctx) of
|
||||
Just lbl -> pure lbl
|
||||
Nothing -> throwError $ "Internal: Could not find block with index " ++ show idx
|
||||
|
||||
let s0 = CrucGenState { translateFns = tfns
|
||||
, crucCtx = ctx
|
||||
, crucPState = pstate
|
||||
, blockLabel = lbl
|
||||
, macawBlockIndex = idx
|
||||
, codeAddr = addr
|
||||
, prevStmts = []
|
||||
, crucPos = C.BinaryPos (binaryPath ctx) addr
|
||||
, prevStmts = []
|
||||
}
|
||||
let cont _s () = fail "Unterminated crucible block"
|
||||
let action = do
|
||||
mapM_ addMacawStmt (M.blockStmts b)
|
||||
addMacawTermStmt (M.blockTerm b)
|
||||
r <- lift $ lift $ unContGen action s0 cont
|
||||
put r
|
||||
(ps, blk) <- lift $ lift $ unCrucGen action s0 cont
|
||||
put $ ps & seenBlockMapLens %~ Map.insert idx blk
|
||||
@ -58,15 +58,14 @@ module Data.Macaw.Symbolic.PersistentState
|
||||
, CrucSeenBlockMap
|
||||
) where
|
||||
|
||||
import Control.Lens
|
||||
import Control.Lens hiding (Index, (:>), Empty)
|
||||
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 qualified Data.Map.Strict as Map
|
||||
import Data.Parameterized.Classes
|
||||
import qualified Data.Parameterized.Context as Ctx
|
||||
import Data.Parameterized.Ctx
|
||||
import Data.Parameterized.Context
|
||||
import Data.Parameterized.Map (MapF)
|
||||
import qualified Data.Parameterized.Map as MapF
|
||||
import Data.Parameterized.NatRepr
|
||||
@ -94,6 +93,25 @@ type family CtxToCrucibleType (mtp :: Ctx M.Type) :: Ctx C.CrucibleType where
|
||||
CtxToCrucibleType EmptyCtx = EmptyCtx
|
||||
CtxToCrucibleType (c ::> tp) = CtxToCrucibleType c ::> ToCrucibleType tp
|
||||
|
||||
-- | Create the variables from a collection of registers.
|
||||
macawAssignToCruc :: (forall tp . f tp -> g (ToCrucibleType tp))
|
||||
-> Assignment f ctx
|
||||
-> Assignment g (CtxToCrucibleType ctx)
|
||||
macawAssignToCruc f a =
|
||||
case a of
|
||||
Empty -> empty
|
||||
b :> x -> macawAssignToCruc f b :> f x
|
||||
|
||||
-- | Create the variables from a collection of registers.
|
||||
macawAssignToCrucM :: Applicative m
|
||||
=> (forall tp . f tp -> m (g (ToCrucibleType tp)))
|
||||
-> Assignment f ctx
|
||||
-> m (Assignment g (CtxToCrucibleType ctx))
|
||||
macawAssignToCrucM f a =
|
||||
case a of
|
||||
Empty -> pure empty
|
||||
b :> x -> (:>) <$> macawAssignToCrucM f b <*> f x
|
||||
|
||||
-- | Type family for arm registers
|
||||
type family ArchRegContext (arch :: *) :: Ctx M.Type
|
||||
|
||||
@ -109,36 +127,16 @@ type ArchAddrCrucibleType arch = C.BVType (M.ArchAddrWidth arch)
|
||||
typeToCrucibleBase :: M.TypeRepr tp -> C.BaseTypeRepr (ToCrucibleBaseType tp)
|
||||
typeToCrucibleBase tp =
|
||||
case tp of
|
||||
M.BoolTypeRepr -> C.BaseBoolRepr
|
||||
M.BVTypeRepr w -> C.BaseBVRepr w
|
||||
M.BoolTypeRepr -> C.BaseBoolRepr
|
||||
M.BVTypeRepr w -> C.BaseBVRepr w
|
||||
-- M.TupleTypeRepr a -> C.BaseStructRepr (macawAssignToCruc tpyeToCrucibleBase a)
|
||||
|
||||
typeToCrucible :: M.TypeRepr tp -> C.TypeRepr (ToCrucibleType tp)
|
||||
typeToCrucible = C.baseToType . typeToCrucibleBase
|
||||
|
||||
|
||||
-- | Create the variables from a collection of registers.
|
||||
macawAssignToCruc :: (forall tp . f tp -> g (ToCrucibleType tp))
|
||||
-> Ctx.Assignment f ctx
|
||||
-> Ctx.Assignment g (CtxToCrucibleType ctx)
|
||||
macawAssignToCruc f a =
|
||||
case Ctx.view a of
|
||||
Ctx.AssignEmpty -> Ctx.empty
|
||||
Ctx.AssignExtend b x -> macawAssignToCruc f b Ctx.%> f x
|
||||
|
||||
-- | Create the variables from a collection of registers.
|
||||
macawAssignToCrucM :: Applicative m
|
||||
=> (forall tp . f tp -> m (g (ToCrucibleType tp)))
|
||||
-> Ctx.Assignment f ctx
|
||||
-> m (Ctx.Assignment g (CtxToCrucibleType ctx))
|
||||
macawAssignToCrucM f a =
|
||||
case Ctx.view a of
|
||||
Ctx.AssignEmpty -> pure Ctx.empty
|
||||
Ctx.AssignExtend b x -> (Ctx.%>) <$> macawAssignToCrucM f b <*> f x
|
||||
|
||||
|
||||
-- Return the types associated with a register assignment.
|
||||
typeCtxToCrucible :: Ctx.Assignment M.TypeRepr ctx
|
||||
-> Ctx.Assignment C.TypeRepr (CtxToCrucibleType ctx)
|
||||
typeCtxToCrucible :: Assignment M.TypeRepr ctx
|
||||
-> Assignment C.TypeRepr (CtxToCrucibleType ctx)
|
||||
typeCtxToCrucible = macawAssignToCruc typeToCrucible
|
||||
|
||||
memReprToCrucible :: M.MemRepr tp -> C.TypeRepr (ToCrucibleType tp)
|
||||
@ -148,27 +146,27 @@ memReprToCrucible = typeToCrucible . M.typeRepr
|
||||
-- RegIndexMap
|
||||
|
||||
-- | This relates an index from macaw to Crucible.
|
||||
data IndexPair ctx tp = IndexPair { macawIndex :: !(Ctx.Index ctx tp)
|
||||
, crucibleIndex :: !(Ctx.Index (CtxToCrucibleType ctx) (ToCrucibleType tp))
|
||||
data IndexPair ctx tp = IndexPair { macawIndex :: !(Index ctx tp)
|
||||
, crucibleIndex :: !(Index (CtxToCrucibleType ctx) (ToCrucibleType tp))
|
||||
}
|
||||
|
||||
-- | This extends the indices in the pair.
|
||||
extendIndexPair :: IndexPair ctx tp -> IndexPair (ctx::>utp) tp
|
||||
extendIndexPair (IndexPair i j) = IndexPair (Ctx.extendIndex i) (Ctx.extendIndex j)
|
||||
extendIndexPair (IndexPair i j) = IndexPair (extendIndex i) (extendIndex j)
|
||||
|
||||
|
||||
type RegIndexMap arch = MapF (M.ArchReg arch) (IndexPair (ArchRegContext arch))
|
||||
|
||||
mkRegIndexMap :: OrdF r
|
||||
=> Ctx.Assignment r ctx
|
||||
-> Ctx.Size (CtxToCrucibleType ctx)
|
||||
=> Assignment r ctx
|
||||
-> Size (CtxToCrucibleType ctx)
|
||||
-> MapF r (IndexPair ctx)
|
||||
mkRegIndexMap r0 csz =
|
||||
case (Ctx.view r0, Ctx.viewSize csz) of
|
||||
(Ctx.AssignEmpty, _) -> MapF.empty
|
||||
(Ctx.AssignExtend a r, Ctx.IncSize csz0) ->
|
||||
case (r0, viewSize csz) of
|
||||
(Empty, _) -> MapF.empty
|
||||
(a :> r, IncSize csz0) ->
|
||||
let m = fmapF extendIndexPair (mkRegIndexMap a csz0)
|
||||
idx = IndexPair (Ctx.nextIndex (Ctx.size a)) (Ctx.nextIndex csz0)
|
||||
idx = IndexPair (nextIndex (size a)) (nextIndex csz0)
|
||||
in MapF.insert r idx m
|
||||
|
||||
------------------------------------------------------------------------
|
||||
@ -189,7 +187,7 @@ data CrucGenContext arch ids s
|
||||
= CrucGenContext
|
||||
{ archConstraints :: !(forall a . (ArchConstraints arch => a) -> a)
|
||||
-- ^ Typeclass constraints for architecture
|
||||
, macawRegAssign :: !(Ctx.Assignment (M.ArchReg arch) (ArchRegContext arch))
|
||||
, macawRegAssign :: !(Assignment (M.ArchReg arch) (ArchRegContext arch))
|
||||
-- ^ Assignment from register to the context
|
||||
, regIndexMap :: !(RegIndexMap arch)
|
||||
, handleAlloc :: !(C.HandleAllocator s)
|
||||
@ -266,17 +264,17 @@ handleIdName h =
|
||||
|
||||
handleIdArgTypes :: CrucGenContext arch ids s
|
||||
-> HandleId arch '(args, ret)
|
||||
-> Ctx.Assignment C.TypeRepr args
|
||||
-> Assignment C.TypeRepr args
|
||||
handleIdArgTypes ctx h =
|
||||
case h of
|
||||
MkFreshSymId _repr -> Ctx.empty
|
||||
MkFreshSymId _repr -> empty
|
||||
ReadMemId _repr -> archConstraints ctx $
|
||||
Ctx.empty Ctx.%> C.BVRepr (archWidthRepr ctx)
|
||||
empty :> C.BVRepr (archWidthRepr ctx)
|
||||
WriteMemId repr -> archConstraints ctx $
|
||||
Ctx.empty Ctx.%> C.BVRepr (archWidthRepr ctx)
|
||||
Ctx.%> memReprToCrucible repr
|
||||
empty :> C.BVRepr (archWidthRepr ctx)
|
||||
:> memReprToCrucible repr
|
||||
SyscallId ->
|
||||
Ctx.empty Ctx.%> regStructRepr ctx
|
||||
empty :> regStructRepr ctx
|
||||
|
||||
handleIdRetType :: CrucGenContext arch ids s
|
||||
-> HandleId arch '(args, ret)
|
||||
@ -326,11 +324,11 @@ data CrucPersistentState arch ids s
|
||||
initCrucPersistentState :: forall arch ids s . CrucPersistentState arch ids s
|
||||
initCrucPersistentState =
|
||||
-- Infer number of arguments to function so that we have values skip inputs.
|
||||
let argCount :: Ctx.Size (MacawFunctionArgs arch)
|
||||
argCount = Ctx.knownSize
|
||||
let argCount :: Size (MacawFunctionArgs arch)
|
||||
argCount = knownSize
|
||||
in CrucPersistentState
|
||||
{ handleMap = MapF.empty
|
||||
, valueCount = Ctx.sizeInt argCount
|
||||
, valueCount = sizeInt argCount
|
||||
, assignValueMap = MapF.empty
|
||||
, seenBlockMap = Map.empty
|
||||
}
|
||||
|
||||
@ -30,6 +30,10 @@ module Data.Macaw.X86
|
||||
, rootLoc
|
||||
, disassembleBlock
|
||||
, X86TranslateError(..)
|
||||
, Data.Macaw.X86.ArchTypes.X86_64
|
||||
, Data.Macaw.X86.ArchTypes.X86PrimFn(..)
|
||||
, Data.Macaw.X86.ArchTypes.X86Stmt(..)
|
||||
, Data.Macaw.X86.ArchTypes.X86TermStmt(..)
|
||||
, Data.Macaw.X86.X86Reg.X86Reg(..)
|
||||
, Data.Macaw.X86.X86Reg.x86ArgumentRegs
|
||||
, Data.Macaw.X86.X86Reg.x86ResultRegs
|
||||
|
||||
@ -1 +1 @@
|
||||
Subproject commit f0d85b41cbcd68871b9f7557e49fdeb89c95419e
|
||||
Subproject commit 0d7a19fdbcefc4d7e97edb623bec549504d4f4d0
|
||||
Loading…
Reference in New Issue
Block a user