mirror of
https://github.com/GaloisInc/macaw.git
synced 2024-12-23 22:23:40 +03:00
Generalize the generator monad, the TH helper monad, and the simplifier
This code was mostly architecture independent already, so this commit moves it to the macaw-semmc module so that it can be shared with the ARM backend. I still plan to move the main TH module with the SimpleBuilder to macaw translation, but that requires a few other changes first.
This commit is contained in:
Tristan Ravitch
parent
1d49256c23
commit
7256fd597f
@ -1,4 +1,5 @@
|
||||
packages: macaw-ppc/
|
||||
macaw-semmc/
|
||||
submodules/macaw/base/
|
||||
submodules/semmc/semmc/
|
||||
submodules/semmc/semmc-ppc/
|
||||
|
||||
@ -21,7 +21,6 @@ library
|
||||
Data.Macaw.PPC.BinaryFormat.ELF
|
||||
Data.Macaw.PPC.Disassemble
|
||||
Data.Macaw.PPC.Eval
|
||||
Data.Macaw.PPC.Generator
|
||||
Data.Macaw.PPC.Identify
|
||||
Data.Macaw.PPC.Operand
|
||||
Data.Macaw.PPC.PPCReg
|
||||
@ -30,8 +29,6 @@ library
|
||||
Data.Macaw.PPC.Semantics.PPC64
|
||||
Data.Macaw.PPC.Semantics.PPC32
|
||||
Data.Macaw.PPC.Semantics.TH
|
||||
Data.Macaw.PPC.Semantics.TH.Monad
|
||||
Data.Macaw.PPC.Simplify
|
||||
build-depends: base >=4.9 && <5,
|
||||
bytestring,
|
||||
containers,
|
||||
@ -42,6 +39,7 @@ library
|
||||
dismantle-ppc,
|
||||
semmc,
|
||||
semmc-ppc,
|
||||
macaw-semmc,
|
||||
lens,
|
||||
macaw-base,
|
||||
ansi-wl-pprint,
|
||||
|
||||
@ -7,6 +7,7 @@
|
||||
{-# LANGUAGE KindSignatures #-}
|
||||
{-# LANGUAGE MultiParamTypeClasses #-}
|
||||
{-# LANGUAGE RankNTypes #-}
|
||||
{-# LANGUAGE TemplateHaskell #-}
|
||||
{-# LANGUAGE TypeFamilies #-}
|
||||
{-# LANGUAGE TypeOperators #-}
|
||||
module Data.Macaw.PPC.Arch (
|
||||
@ -17,20 +18,24 @@ module Data.Macaw.PPC.Arch (
|
||||
PPCPrimFn(..),
|
||||
rewritePrimFn,
|
||||
ppcPrimFnHasSideEffects,
|
||||
PPCArchConstraints
|
||||
PPCArchConstraints,
|
||||
specialSemanticsCases
|
||||
) where
|
||||
|
||||
import GHC.TypeLits
|
||||
|
||||
import Language.Haskell.TH
|
||||
import qualified Text.PrettyPrint.ANSI.Leijen as PP
|
||||
import qualified Data.Parameterized.NatRepr as NR
|
||||
import qualified Data.Parameterized.TraversableFC as FC
|
||||
import qualified Data.Parameterized.TraversableF as TF
|
||||
import qualified Data.Macaw.CFG as MC
|
||||
import qualified Data.Macaw.CFG.Block as MC
|
||||
import Data.Macaw.CFG.Rewriter ( Rewriter, rewriteValue, evalRewrittenArchFn, appendRewrittenArchStmt )
|
||||
import qualified Data.Macaw.Memory as MM
|
||||
import qualified Data.Macaw.Types as MT
|
||||
|
||||
import qualified Dismantle.PPC as D
|
||||
import qualified SemMC.Architecture.PPC32 as PPC32
|
||||
import qualified SemMC.Architecture.PPC64 as PPC64
|
||||
|
||||
@ -172,3 +177,18 @@ type PPCArchConstraints ppc = ( MC.ArchReg ppc ~ PPCReg ppc
|
||||
, KnownNat (MC.RegAddrWidth (PPCReg ppc))
|
||||
, MC.ArchConstraints ppc
|
||||
)
|
||||
|
||||
-- | Manually-provided semantics for instructions whose full semantics cannot be
|
||||
-- expressed in our semantics format.
|
||||
--
|
||||
-- This includes instructions with special side effects that we don't have a way
|
||||
-- to talk about in the semantics; especially useful for architecture-specific
|
||||
-- terminator statements.
|
||||
specialSemanticsCases :: [MatchQ]
|
||||
specialSemanticsCases =
|
||||
[ match (conP 'D.SC []) (normalB [| Just (finishWithTerminator (MC.ArchTermStmt PPCSyscall)) |]) []
|
||||
, match (conP 'D.TRAP []) (normalB [| Just (finishWithTerminator (MC.ArchTermStmt PPCTrap)) |]) []
|
||||
, match (conP 'D.ATTN []) (normalB [| Just (addStmt (MC.ExecArchStmt Attn)) |]) []
|
||||
, match (conP 'D.SYNC []) (normalB [| Just (addStmt (MC.ExecArchStmt Sync)) |]) []
|
||||
, match (conP 'D.ISYNC []) (normalB [| Just (addStmt (MC.ExecArchStmt Isync)) |]) []
|
||||
]
|
||||
|
||||
@ -37,9 +37,10 @@ import qualified Data.Macaw.Memory.Permissions as MMP
|
||||
import Data.Macaw.Types ( BVType, BoolType )
|
||||
import qualified Data.Parameterized.Nonce as NC
|
||||
|
||||
import Data.Macaw.PPC.Generator
|
||||
import Data.Macaw.SemMC.Generator
|
||||
import Data.Macaw.SemMC.Simplify ( simplifyValue )
|
||||
import Data.Macaw.PPC.Arch ( PPCArchConstraints )
|
||||
import Data.Macaw.PPC.PPCReg
|
||||
import Data.Macaw.PPC.Simplify ( simplifyValue )
|
||||
|
||||
-- | Read one instruction from the 'MM.Memory' at the given segmented offset.
|
||||
--
|
||||
@ -87,7 +88,7 @@ readInstruction mem addr = MM.addrWidthClass (MM.memAddrWidth mem) $ do
|
||||
-- becomes a mux, we split execution using 'conditionalBranch'.
|
||||
disassembleBlock :: forall ppc ids s
|
||||
. PPCArchConstraints ppc
|
||||
=> (Value ppc ids (BVType (ArchAddrWidth ppc)) -> D.Instruction -> Maybe (PPCGenerator ppc ids s ()))
|
||||
=> (Value ppc ids (BVType (ArchAddrWidth ppc)) -> D.Instruction -> Maybe (Generator ppc ids s ()))
|
||||
-- ^ A function to look up the semantics for an instruction that we disassemble
|
||||
-> MM.Memory (ArchAddrWidth ppc)
|
||||
-> GenState ppc ids s
|
||||
@ -119,7 +120,7 @@ disassembleBlock lookupSemantics mem gs curIPAddr maxOffset = do
|
||||
Just transformer -> do
|
||||
-- Once we have the semantics for the instruction (represented by a
|
||||
-- state transformer), we apply the state transformer and then extract
|
||||
-- a result from the state of the 'PPCGenerator'.
|
||||
-- a result from the state of the 'Generator'.
|
||||
egs1 <- liftST $ ET.runExceptT (runGenerator genResult gs $ do
|
||||
let lineStr = printf "%s: %s" (show curIPAddr) (show (D.ppInstruction i))
|
||||
addStmt (Comment (T.pack lineStr))
|
||||
@ -127,7 +128,7 @@ disassembleBlock lookupSemantics mem gs curIPAddr maxOffset = do
|
||||
|
||||
-- Check to see if the IP has become conditionally-defined (by e.g.,
|
||||
-- a mux). If it has, we need to split execution using a primitive
|
||||
-- provided by the PPCGenerator monad.
|
||||
-- provided by the Generator monad.
|
||||
nextIPExpr <- getRegValue PPC_IP
|
||||
case matchConditionalBranch nextIPExpr of
|
||||
Just (cond, t_ip, f_ip) ->
|
||||
@ -168,10 +169,8 @@ matchConditionalBranch v =
|
||||
_ -> Nothing
|
||||
_ -> Nothing
|
||||
|
||||
tryDisassembleBlock :: ( PPCArchConstraints ppc
|
||||
, Show (Block ppc ids)
|
||||
, Show (BlockSeq ppc ids))
|
||||
=> (Value ppc ids (BVType (ArchAddrWidth ppc)) -> D.Instruction -> Maybe (PPCGenerator ppc ids s ()))
|
||||
tryDisassembleBlock :: (PPCArchConstraints ppc)
|
||||
=> (Value ppc ids (BVType (ArchAddrWidth ppc)) -> D.Instruction -> Maybe (Generator ppc ids s ()))
|
||||
-> MM.Memory (ArchAddrWidth ppc)
|
||||
-> NC.NonceGenerator (ST s) ids
|
||||
-> ArchSegmentOff ppc
|
||||
@ -191,11 +190,9 @@ tryDisassembleBlock lookupSemantics mem nonceGen startAddr maxSize = do
|
||||
--
|
||||
-- Return a list of disassembled blocks as well as the total number of bytes
|
||||
-- occupied by those blocks.
|
||||
disassembleFn :: ( PPCArchConstraints ppc
|
||||
, Show (Block ppc ids)
|
||||
, Show (BlockSeq ppc ids))
|
||||
disassembleFn :: (PPCArchConstraints ppc)
|
||||
=> proxy ppc
|
||||
-> (Value ppc ids (BVType (ArchAddrWidth ppc)) -> D.Instruction -> Maybe (PPCGenerator ppc ids s ()))
|
||||
-> (Value ppc ids (BVType (ArchAddrWidth ppc)) -> D.Instruction -> Maybe (Generator ppc ids s ()))
|
||||
-- ^ A function to look up the semantics for an instruction. The
|
||||
-- lookup is provided with the value of the IP in case IP-relative
|
||||
-- addressing is necessary.
|
||||
|
||||
@ -25,9 +25,9 @@ import Data.Parameterized.Some ( Some(..) )
|
||||
|
||||
import qualified Dismantle.PPC as D
|
||||
|
||||
import Data.Macaw.SemMC.Simplify ( simplifyValue )
|
||||
import Data.Macaw.PPC.Arch
|
||||
import Data.Macaw.PPC.PPCReg
|
||||
import Data.Macaw.PPC.Simplify ( simplifyValue )
|
||||
|
||||
preserveRegAcrossSyscall :: (ArchReg ppc ~ PPCReg ppc, 1 <= RegAddrWidth (PPCReg ppc))
|
||||
=> proxy ppc
|
||||
|
||||
@ -1,502 +0,0 @@
|
||||
{-# LANGUAGE ConstraintKinds #-}
|
||||
{-# LANGUAGE DataKinds #-}
|
||||
{-# LANGUAGE FlexibleContexts #-}
|
||||
{-# LANGUAGE GADTs #-}
|
||||
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
|
||||
{-# LANGUAGE MultiParamTypeClasses #-}
|
||||
{-# LANGUAGE RankNTypes #-}
|
||||
{-# LANGUAGE ScopedTypeVariables #-}
|
||||
{-# LANGUAGE StandaloneDeriving #-}
|
||||
{-# LANGUAGE TypeApplications #-}
|
||||
{-# LANGUAGE TypeOperators #-}
|
||||
{-# LANGUAGE UndecidableInstances #-}
|
||||
module Data.Macaw.PPC.Generator (
|
||||
GenResult(..),
|
||||
GenState(..),
|
||||
initGenState,
|
||||
initRegState,
|
||||
PPCGenerator,
|
||||
GenCont,
|
||||
runGenerator,
|
||||
genResult,
|
||||
Expr(..),
|
||||
BlockSeq(..),
|
||||
PreBlock(..),
|
||||
-- * Generator actions
|
||||
addStmt,
|
||||
addAssignment,
|
||||
getRegs,
|
||||
getRegValue,
|
||||
shiftGen,
|
||||
finishBlock,
|
||||
finishBlock',
|
||||
finishWithTerminator,
|
||||
conditionalBranch,
|
||||
addExpr,
|
||||
bvconcat,
|
||||
bvselect,
|
||||
setRegVal,
|
||||
-- * Lenses
|
||||
blockState,
|
||||
pBlockStmts,
|
||||
pBlockState,
|
||||
frontierBlocks,
|
||||
blockSeq,
|
||||
-- * Constraints
|
||||
PPCArchConstraints,
|
||||
-- * Errors
|
||||
GeneratorError(..)
|
||||
) where
|
||||
|
||||
import GHC.TypeLits
|
||||
|
||||
import Control.Lens
|
||||
import qualified Control.Monad.Cont as Ct
|
||||
import qualified Control.Monad.Except as ET
|
||||
import qualified Control.Monad.Reader as Rd
|
||||
import Control.Monad.ST ( ST )
|
||||
import qualified Control.Monad.State.Strict as St
|
||||
import Control.Monad.Trans ( lift )
|
||||
import qualified Data.Foldable as F
|
||||
import Data.Maybe ( fromMaybe )
|
||||
import qualified Data.Sequence as Seq
|
||||
import Data.Word (Word64)
|
||||
|
||||
import Data.Macaw.CFG
|
||||
import Data.Macaw.CFG.Block
|
||||
import Data.Macaw.Types ( BVType, BoolType )
|
||||
import qualified Data.Macaw.Memory as MM
|
||||
import Data.Parameterized.Classes
|
||||
import qualified Data.Parameterized.NatRepr as NR
|
||||
import qualified Data.Parameterized.Nonce as NC
|
||||
import qualified Lang.Crucible.BaseTypes as S
|
||||
|
||||
import qualified SemMC.Architecture.PPC.Location as APPC
|
||||
|
||||
import Data.Macaw.PPC.PPCReg
|
||||
import Data.Macaw.PPC.Arch ( PPCArchConstraints )
|
||||
import Data.Macaw.PPC.Simplify ( simplifyValue, simplifyApp )
|
||||
|
||||
-- GenResult
|
||||
|
||||
data GenResult ppc ids =
|
||||
GenResult { resBlockSeq :: BlockSeq ppc ids
|
||||
, resState :: Maybe (PreBlock ppc ids)
|
||||
}
|
||||
|
||||
------------------------------------------------------------------------
|
||||
-- Expr
|
||||
|
||||
data Expr ppc ids tp where
|
||||
ValueExpr :: !(Value ppc ids tp) -> Expr ppc ids tp
|
||||
AppExpr :: !(App (Value ppc ids) tp) -> Expr ppc ids tp
|
||||
------------------------------------------------------------------------
|
||||
-- BlockSeq
|
||||
data BlockSeq ppc ids = BlockSeq
|
||||
{ _nextBlockID :: !Word64
|
||||
-- ^ index of next block
|
||||
, _frontierBlocks :: !(Seq.Seq (Block ppc ids))
|
||||
-- ^ Blocks added to CFG
|
||||
}
|
||||
|
||||
deriving instance Show (Block ppc ids) => Show (BlockSeq ppc ids)
|
||||
deriving instance (PPCArchConstraints ppc) => Show (Block ppc ids)
|
||||
deriving instance (PPCArchConstraints ppc) => Show (TermStmt ppc ids)
|
||||
|
||||
-- | Control flow blocs generated so far.
|
||||
nextBlockID :: Simple Lens (BlockSeq ppc s) Word64
|
||||
nextBlockID = lens _nextBlockID (\s v -> s { _nextBlockID = v })
|
||||
|
||||
-- | Blocks that are not in CFG that end with a FetchAndExecute,
|
||||
-- which we need to analyze to compute new potential branch targets.
|
||||
frontierBlocks :: Simple Lens (BlockSeq ppc s) (Seq.Seq (Block ppc s))
|
||||
frontierBlocks = lens _frontierBlocks (\s v -> s { _frontierBlocks = v })
|
||||
|
||||
------------------------------------------------------------------------
|
||||
-- PreBlock
|
||||
|
||||
-- | A basic block that is under construction; when we get to the end of a block
|
||||
-- (by reaching a terminator statement), we turn this into a full 'Block' (added
|
||||
-- to the 'BlockSeq').
|
||||
data PreBlock ppc ids =
|
||||
PreBlock { pBlockIndex :: !Word64
|
||||
-- ^ The index of the block we are currently constructing
|
||||
, pBlockAddr :: !(MM.MemSegmentOff (ArchAddrWidth ppc))
|
||||
-- ^ Starting address of function in preblock.
|
||||
, _pBlockStmts :: !(Seq.Seq (Stmt ppc ids))
|
||||
-- ^ The list of statements that we have constructed so far. We
|
||||
-- append to the right.
|
||||
, _pBlockState :: !(RegState (PPCReg ppc) (Value ppc ids))
|
||||
-- ^ The current register state, which is updated as we simulate
|
||||
-- instructions
|
||||
}
|
||||
|
||||
-- | An accessor for the current statements in the 'PreBlock'
|
||||
pBlockStmts :: Simple Lens (PreBlock ppc ids) (Seq.Seq (Stmt ppc ids))
|
||||
pBlockStmts = lens _pBlockStmts (\s v -> s { _pBlockStmts = v })
|
||||
|
||||
-- | An accessor for the current register state held in the 'PreBlock'
|
||||
pBlockState :: Simple Lens (PreBlock ppc ids) (RegState (PPCReg ppc) (Value ppc ids))
|
||||
pBlockState = lens _pBlockState (\s v -> s { _pBlockState = v })
|
||||
|
||||
------------------------------------------------------------------------
|
||||
-- GenState
|
||||
|
||||
-- | The state held in our state monad. It tracks the current model of the
|
||||
-- machine state as well as a collection of discovered blocks and the current
|
||||
-- block we are constructing.
|
||||
data GenState ppc ids s =
|
||||
GenState { assignIdGen :: !(NC.NonceGenerator (ST s) ids)
|
||||
, _blockSeq :: !(BlockSeq ppc ids)
|
||||
, _blockState :: !(PreBlock ppc ids)
|
||||
, genAddr :: !(MM.MemSegmentOff (ArchAddrWidth ppc))
|
||||
, genMemory :: !(MM.Memory (ArchAddrWidth ppc))
|
||||
}
|
||||
|
||||
-- | Initialize a fresh 'GenState'
|
||||
--
|
||||
-- This does most of what you would expect. Note that the next block ID is set
|
||||
-- to 1, since we use ID 0 for the first block (assigned to the initial
|
||||
-- 'PreBlock'.
|
||||
initGenState :: NC.NonceGenerator (ST s) ids
|
||||
-> MM.Memory (ArchAddrWidth ppc)
|
||||
-> MM.MemSegmentOff (ArchAddrWidth ppc)
|
||||
-> RegState (PPCReg ppc) (Value ppc ids)
|
||||
-> GenState ppc ids s
|
||||
initGenState nonceGen mem addr st =
|
||||
GenState { assignIdGen = nonceGen
|
||||
, _blockSeq = BlockSeq { _nextBlockID = 1, _frontierBlocks = Seq.empty }
|
||||
, _blockState = emptyPreBlock st 0 addr
|
||||
, genAddr = addr
|
||||
, genMemory = mem
|
||||
}
|
||||
|
||||
-- | Create an initial register state.
|
||||
--
|
||||
-- All of the register values are set to the special 'Initial' value, which
|
||||
-- indicates that the values are not known precisely, but are some abstract
|
||||
-- initial values.
|
||||
--
|
||||
-- Aside from that, we set the initial IP to the given value (@startIP@).
|
||||
initRegState :: ( PPCArchConstraints ppc)
|
||||
=> ArchSegmentOff ppc
|
||||
-> RegState (PPCReg ppc) (Value ppc ids)
|
||||
initRegState startIP = mkRegState Initial
|
||||
& curIP .~ RelocatableValue NR.knownNat (MM.relativeSegmentAddr startIP)
|
||||
|
||||
-- | Set up an empty initial block with a provided state, address, and block ID.
|
||||
emptyPreBlock :: RegState (PPCReg ppc) (Value ppc ids)
|
||||
-> Word64
|
||||
-> MM.MemSegmentOff (RegAddrWidth (ArchReg ppc))
|
||||
-> PreBlock ppc ids
|
||||
emptyPreBlock s0 idx addr =
|
||||
PreBlock { pBlockIndex = idx
|
||||
, pBlockAddr = addr
|
||||
, _pBlockStmts = Seq.empty
|
||||
, _pBlockState = s0
|
||||
}
|
||||
|
||||
blockSeq :: Simple Lens (GenState ppc ids s) (BlockSeq ppc ids)
|
||||
blockSeq = lens _blockSeq (\s v -> s { _blockSeq = v })
|
||||
|
||||
blockState :: Simple Lens (GenState ppc ids s) (PreBlock ppc ids)
|
||||
blockState = lens _blockState (\s v -> s { _blockState = v })
|
||||
|
||||
curPPCState :: Simple Lens (GenState ppc ids s) (RegState (PPCReg ppc) (Value ppc ids))
|
||||
curPPCState = blockState . pBlockState
|
||||
|
||||
------------------------------------------------------------------------
|
||||
-- Factored-out Operations for PPCGenerator
|
||||
|
||||
-- | Set a register to a value after attempting to simplify the value as much as
|
||||
-- possible (using 'simplifyValue').
|
||||
setRegVal :: (PPCArchConstraints ppc, RegAddrWidth (PPCReg ppc) ~ w)
|
||||
=> PPCReg ppc tp
|
||||
-> Value ppc ids tp
|
||||
-> PPCGenerator ppc ids s ()
|
||||
setRegVal reg val =
|
||||
curPPCState . boundValue reg .= fromMaybe val (simplifyValue val)
|
||||
|
||||
-- | The implementation of bitvector concatenation
|
||||
--
|
||||
-- We pull this out to reduce the amount of code generated by TH
|
||||
bvconcat :: (ArchConstraints ppc, 1 <= v, (u+1) <= w, 1 <= u, 1 <= w, (u+v) ~ w)
|
||||
=> Value ppc ids (BVType u)
|
||||
-> Value ppc ids (BVType v)
|
||||
-> NR.NatRepr v
|
||||
-> NR.NatRepr u
|
||||
-> NR.NatRepr w
|
||||
-> PPCGenerator ppc ids s (Expr ppc ids (BVType w))
|
||||
bvconcat bv1Val bv2Val repV repU repW = do
|
||||
S.LeqProof <- return (S.leqAdd2 (S.leqRefl repU) (S.leqProof (S.knownNat @1) repV))
|
||||
pf1@S.LeqProof <- return (S.leqAdd2 (S.leqRefl repV) (S.leqProof (S.knownNat @1) repU))
|
||||
Refl <- return (S.plusComm repU repV)
|
||||
S.LeqProof <- return (S.leqTrans pf1 (S.leqRefl repW))
|
||||
bv1Ext <- addExpr (AppExpr (UExt bv1Val repW))
|
||||
bv2Ext <- addExpr (AppExpr (UExt bv2Val repW))
|
||||
bv1Shifter <- addExpr (ValueExpr (BVValue repW (NR.natValue repV)))
|
||||
bv1Shf <- addExpr (AppExpr (BVShl repW bv1Ext bv1Shifter))
|
||||
return $ AppExpr (BVOr repW bv1Shf bv2Ext)
|
||||
|
||||
-- | Select @n@ bits from a @w@ bit bitvector starting at index @i@
|
||||
--
|
||||
-- This code is factored out of the TH module to improve compilation times.
|
||||
bvselect :: (ArchConstraints ppc, 1 <= w, 1 <= n, 1 <= i, (i+n) <= w)
|
||||
=> Value ppc ids (BVType w)
|
||||
-> NR.NatRepr n
|
||||
-> NR.NatRepr i
|
||||
-> NR.NatRepr w
|
||||
-> PPCGenerator ppc ids s (Expr ppc ids (BVType n))
|
||||
bvselect bvVal repN repI repW = do
|
||||
Just S.LeqProof <- return (S.testLeq (repN `S.addNat` (NR.knownNat @1)) repW)
|
||||
pf1@S.LeqProof <- return $ S.leqAdd2 (S.leqRefl repI) (S.leqProof (NR.knownNat @1) repN)
|
||||
pf2@S.LeqProof <- return $ S.leqAdd (S.leqRefl (NR.knownNat @1)) repI
|
||||
Refl <- return (S.plusComm (NR.knownNat @1) repI)
|
||||
pf3@S.LeqProof <- return $ S.leqTrans pf2 pf1
|
||||
S.LeqProof <- return $ S.leqTrans pf3 (S.leqProof (repI `S.addNat` repN) repW)
|
||||
bvShf <- addExpr (AppExpr (BVShr repW bvVal (mkLit repW (NR.natValue repI))))
|
||||
return (AppExpr (Trunc bvShf repN))
|
||||
|
||||
-- | Add an expression in the PPCGenerator monad. This returns a Macaw value
|
||||
-- corresponding to the added expression.
|
||||
addExpr :: (ArchConstraints ppc) => Expr ppc ids tp -> PPCGenerator ppc ids s (Value ppc ids tp)
|
||||
addExpr expr = do
|
||||
case expr of
|
||||
ValueExpr val -> return val
|
||||
AppExpr app
|
||||
| Just val <- simplifyApp app -> return val
|
||||
| otherwise -> do
|
||||
assignment <- addAssignment (EvalApp app)
|
||||
return $ AssignedValue assignment
|
||||
|
||||
|
||||
------------------------------------------------------------------------
|
||||
-- PPCGenerator
|
||||
|
||||
data GeneratorError = InvalidEncoding
|
||||
| GeneratorMessage String
|
||||
deriving (Show)
|
||||
|
||||
-- | This is a state monad (with error termination via 'ET.ExceptT') built on
|
||||
-- top of 'Ct.ContT' and 'Rd.ReaderT'.
|
||||
--
|
||||
-- We use the 'Ct.ContT' for early termination when dealing with control flow
|
||||
-- terminators (e.g., syscall) and to split for dealing with conditional
|
||||
-- branches.
|
||||
--
|
||||
-- The state is managed by explicitly passing it through the continuation.
|
||||
--
|
||||
-- The most important operation provided is the primitive 'shiftGen', which is
|
||||
-- used to build 'conditionalBranch'.
|
||||
--
|
||||
-- The base monad is 'ST', which is used for nonce generation.
|
||||
newtype PPCGenerator ppc ids s a =
|
||||
PPCGenerator { runG :: Ct.ContT (GenResult ppc ids)
|
||||
(Rd.ReaderT (GenState ppc ids s)
|
||||
(ET.ExceptT GeneratorError (ST s))) a }
|
||||
deriving (Applicative,
|
||||
Functor,
|
||||
Rd.MonadReader (GenState ppc ids s),
|
||||
Ct.MonadCont)
|
||||
|
||||
-- | The 'Monad' instance is manually-specified so that calls to 'fail' actually
|
||||
-- use our 'ET.ExceptT' 'ET.throwError' for nicer error behavior.
|
||||
instance Monad (PPCGenerator ppc ids s) where
|
||||
return v = PPCGenerator (return v)
|
||||
PPCGenerator m >>= h = PPCGenerator (m >>= \v -> runG (h v))
|
||||
PPCGenerator m >> PPCGenerator n = PPCGenerator (m >> n)
|
||||
fail msg = PPCGenerator (Ct.ContT (\_ -> ET.throwError (GeneratorMessage msg)))
|
||||
|
||||
instance St.MonadState (GenState ppc ids s) (PPCGenerator ppc ids s) where
|
||||
get = PPCGenerator Rd.ask
|
||||
put nextState = PPCGenerator $ Ct.ContT $ \c -> Rd.ReaderT $ \_s ->
|
||||
Rd.runReaderT (c ()) nextState
|
||||
|
||||
instance ET.MonadError GeneratorError (PPCGenerator ppc ids s) where
|
||||
throwError e = PPCGenerator (Ct.ContT (\_ -> ET.throwError e))
|
||||
-- catchError a hdlr = do
|
||||
-- r <- liftST $ ET.runExceptT (unDisM a)
|
||||
-- case r of
|
||||
-- Left l -> do
|
||||
-- r' <- liftST $ ET.runExceptT (unDisM (hdlr l))
|
||||
-- case r' of
|
||||
-- Left e -> DisM (ET.throwError e)
|
||||
-- Right res -> return res
|
||||
-- Right res -> return res
|
||||
|
||||
-- | The type of continuations provided by 'shiftGen'
|
||||
type GenCont ppc ids s a = a -> GenState ppc ids s -> ET.ExceptT GeneratorError (ST s) (GenResult ppc ids)
|
||||
|
||||
-- | Given a final continuation to call, run the generator (and produce a final
|
||||
-- result with the given continuation @k@). Also takes an initial state.
|
||||
runGenerator :: GenCont ppc ids s a
|
||||
-> GenState ppc ids s
|
||||
-> PPCGenerator ppc ids s a
|
||||
-> ET.ExceptT GeneratorError (ST s) (GenResult ppc ids)
|
||||
runGenerator k st (PPCGenerator m) = Rd.runReaderT (Ct.runContT m (Rd.ReaderT . k)) st
|
||||
|
||||
-- | Capture the current continuation and execute an action that gets that
|
||||
-- continuation as an argument (it can be invoked as many times as desired).
|
||||
shiftGen :: (GenCont ppc ids s a -> GenState ppc ids s -> ET.ExceptT GeneratorError (ST s) (GenResult ppc ids))
|
||||
-> PPCGenerator ppc ids s a
|
||||
shiftGen f =
|
||||
PPCGenerator $ Ct.ContT $ \k -> Rd.ReaderT $ \s -> f (Rd.runReaderT . k) s
|
||||
|
||||
genResult :: (Monad m) => a -> GenState ppc ids s -> m (GenResult ppc ids)
|
||||
genResult _ s = do
|
||||
return GenResult { resBlockSeq = s ^. blockSeq
|
||||
, resState = Just (s ^. blockState)
|
||||
}
|
||||
|
||||
-- | Append a statement (on the right) to the list of statements in the current
|
||||
-- 'PreBlock'.
|
||||
addStmt :: (ArchConstraints ppc) => Stmt ppc ids -> PPCGenerator ppc ids s ()
|
||||
addStmt stmt = (blockState . pBlockStmts) %= (Seq.|> stmt)
|
||||
|
||||
-- | Generate the next unique ID for an assignment using the nonce generator
|
||||
newAssignId :: PPCGenerator ppc ids s (AssignId ids tp)
|
||||
newAssignId = do
|
||||
nonceGen <- St.gets assignIdGen
|
||||
n <- liftST $ NC.freshNonce nonceGen
|
||||
return (AssignId n)
|
||||
|
||||
-- | Lift an 'ST' action into 'PPCGenerator'
|
||||
liftST :: ST s a -> PPCGenerator ppc ids s a
|
||||
liftST = PPCGenerator . lift . lift . lift
|
||||
|
||||
-- | Append an assignment statement to the list of statements in the current
|
||||
-- 'PreBlock'
|
||||
addAssignment :: (ArchConstraints ppc)
|
||||
=> AssignRhs ppc ids tp
|
||||
-> PPCGenerator ppc ids s (Assignment ppc ids tp)
|
||||
addAssignment rhs = do
|
||||
l <- newAssignId
|
||||
let a = Assignment l rhs
|
||||
addStmt $ AssignStmt a
|
||||
return a
|
||||
|
||||
-- | Get all of the current register values
|
||||
--
|
||||
-- This is meant to be used to snapshot the register state at the beginning of
|
||||
-- an instruction transformer so that we can perform atomic updates to the
|
||||
-- machine state (by reading values from the captured initial state).
|
||||
getRegs :: PPCGenerator ppc ids s (RegState (PPCReg ppc) (Value ppc ids))
|
||||
getRegs = do
|
||||
genState <- St.get
|
||||
return (genState ^. blockState ^. pBlockState)
|
||||
|
||||
-- | Get the value of a single register.
|
||||
--
|
||||
-- NOTE: This should not be called from the generated semantics transformers.
|
||||
-- Those must get their register values through 'getRegs', which is used to take
|
||||
-- a snapshot of the register state at the beginning of each instruction. This
|
||||
-- is required for instruction updates to register values to have the necessary
|
||||
-- atomic update behavior.
|
||||
getRegValue :: PPCReg ppc tp -> PPCGenerator ppc ids s (Value ppc ids tp)
|
||||
getRegValue r = do
|
||||
genState <- St.get
|
||||
return (genState ^. blockState ^. pBlockState ^. boundValue r)
|
||||
|
||||
-- | A primitive for splitting execution in the presence of conditional
|
||||
-- branches.
|
||||
--
|
||||
-- This function uses the underlying continuation monad to split execution. It
|
||||
-- captures the current continuation and builds a block for the true branch and
|
||||
-- another block for the false branch. It manually threads the state between
|
||||
-- the two branches and makes updates to keep them consistent. It also joins
|
||||
-- the two exploration frontiers after processing the true and false branches so
|
||||
-- that the underlying return value contains all discovered blocks.
|
||||
conditionalBranch :: (PPCArchConstraints ppc)
|
||||
=> Value ppc ids BoolType
|
||||
-- ^ The conditional guarding the branch
|
||||
-> PPCGenerator ppc ids s ()
|
||||
-- ^ The action to take on the true branch
|
||||
-> PPCGenerator ppc ids s ()
|
||||
-- ^ The action to take on the false branch
|
||||
-> PPCGenerator ppc ids s ()
|
||||
conditionalBranch condExpr t f =
|
||||
go (fromMaybe condExpr (simplifyValue condExpr))
|
||||
where
|
||||
go condv =
|
||||
case condv of
|
||||
BoolValue True -> t
|
||||
BoolValue False -> f
|
||||
_ -> shiftGen $ \c s0 -> do
|
||||
let pre_block = s0 ^. blockState
|
||||
let st = pre_block ^. pBlockState
|
||||
let t_block_label = s0 ^. blockSeq ^. nextBlockID
|
||||
let s1 = s0 & blockSeq . nextBlockID +~ 1
|
||||
& blockSeq . frontierBlocks .~ Seq.empty
|
||||
& blockState .~ emptyPreBlock st t_block_label (genAddr s0)
|
||||
|
||||
-- Explore the true block
|
||||
t_seq <- finishBlock FetchAndExecute <$> runGenerator c s1 t
|
||||
|
||||
-- Explore the false block
|
||||
let f_block_label = t_seq ^. nextBlockID
|
||||
let s2 = GenState { assignIdGen = assignIdGen s0
|
||||
, _blockSeq = BlockSeq { _nextBlockID = t_seq ^. nextBlockID + 1
|
||||
, _frontierBlocks = Seq.empty
|
||||
}
|
||||
, _blockState = emptyPreBlock st f_block_label (genAddr s0)
|
||||
, genAddr = genAddr s0
|
||||
, genMemory = genMemory s0
|
||||
}
|
||||
f_seq <- finishBlock FetchAndExecute <$> runGenerator c s2 f
|
||||
|
||||
-- Join the results with a branch terminator
|
||||
let fin_block = finishBlock' pre_block (\_ -> Branch condv t_block_label f_block_label)
|
||||
let frontier = mconcat [ s0 ^. blockSeq ^. frontierBlocks Seq.|> fin_block
|
||||
, t_seq ^. frontierBlocks
|
||||
, f_seq ^. frontierBlocks
|
||||
]
|
||||
return GenResult { resBlockSeq =
|
||||
BlockSeq { _nextBlockID = _nextBlockID f_seq
|
||||
, _frontierBlocks = frontier
|
||||
}
|
||||
, resState = Nothing
|
||||
}
|
||||
|
||||
-- | Finish a block immediately with the given terminator statement
|
||||
--
|
||||
-- This uses the underlying continuation monad to skip the normal
|
||||
-- post-instruction behavior.
|
||||
--
|
||||
-- NOTE: We do not do an explicit instruction pointer update; the handler for
|
||||
-- architecture-specific terminator statements handles that.
|
||||
finishWithTerminator :: forall ppc ids s a
|
||||
. (PPCArchConstraints ppc, KnownNat (APPC.ArchRegWidth ppc))
|
||||
=> (RegState (PPCReg ppc) (Value ppc ids) -> TermStmt ppc ids)
|
||||
-> PPCGenerator ppc ids s a
|
||||
finishWithTerminator term =
|
||||
shiftGen $ \_ s0 -> do
|
||||
let pre_block = s0 ^. blockState
|
||||
let fin_block = finishBlock' pre_block term
|
||||
return GenResult { resBlockSeq = s0 ^. blockSeq & frontierBlocks %~ (Seq.|> fin_block)
|
||||
, resState = Nothing
|
||||
}
|
||||
|
||||
-- | Convert the contents of a 'PreBlock' (a block being constructed) into a
|
||||
-- full-fledged 'Block'
|
||||
--
|
||||
-- The @term@ function is used to create the terminator statement of the block.
|
||||
finishBlock' :: PreBlock ppc ids
|
||||
-> (RegState (PPCReg ppc) (Value ppc ids) -> TermStmt ppc ids)
|
||||
-> Block ppc ids
|
||||
finishBlock' preBlock term =
|
||||
Block { blockLabel = pBlockIndex preBlock
|
||||
, blockStmts = F.toList (preBlock ^. pBlockStmts)
|
||||
, blockTerm = term (preBlock ^. pBlockState)
|
||||
}
|
||||
|
||||
-- | Consume a 'GenResult', finish off the contained 'PreBlock', and append the
|
||||
-- new block to the block frontier.
|
||||
finishBlock :: (RegState (PPCReg ppc) (Value ppc ids) -> TermStmt ppc ids)
|
||||
-> GenResult ppc ids
|
||||
-> BlockSeq ppc ids
|
||||
finishBlock term st =
|
||||
case resState st of
|
||||
Nothing -> resBlockSeq st
|
||||
Just preBlock ->
|
||||
let b = finishBlock' preBlock term
|
||||
in resBlockSeq st & frontierBlocks %~ (Seq.|> b)
|
||||
@ -11,9 +11,9 @@ import qualified Data.Sequence as Seq
|
||||
import qualified Data.Macaw.CFG as MC
|
||||
import qualified Data.Macaw.Memory as MM
|
||||
|
||||
import Data.Macaw.SemMC.Simplify ( simplifyValue )
|
||||
import Data.Macaw.PPC.Arch
|
||||
import Data.Macaw.PPC.PPCReg
|
||||
import Data.Macaw.PPC.Simplify ( simplifyValue )
|
||||
|
||||
import Debug.Trace (trace)
|
||||
|
||||
|
||||
@ -27,11 +27,11 @@ import qualified Dismantle.PPC as D
|
||||
|
||||
import qualified SemMC.Architecture.PPC32 as PPC32
|
||||
import qualified SemMC.Architecture.PPC64 as PPC64
|
||||
import qualified Data.Macaw.SemMC.Generator as G
|
||||
import qualified Data.Macaw.PPC.PPCReg as R
|
||||
import qualified Data.Macaw.PPC.Generator as G
|
||||
|
||||
class ExtractValue arch a tp | arch a -> tp where
|
||||
extractValue :: a -> G.PPCGenerator arch ids s (MC.Value arch ids tp)
|
||||
extractValue :: a -> G.Generator arch ids s (MC.Value arch ids tp)
|
||||
|
||||
instance ExtractValue arch Bool BoolType where
|
||||
extractValue = return . MC.BoolValue
|
||||
@ -54,7 +54,7 @@ instance ExtractValue PPC64.PPC (Maybe D.GPR) (BVType 64) where
|
||||
Just gpr -> extractValue gpr
|
||||
Nothing -> return $ MC.BVValue NR.knownNat 0
|
||||
|
||||
instance ExtractValue ppc D.FR (BVType 128) where
|
||||
instance (MC.ArchReg ppc ~ R.PPCReg ppc) => ExtractValue ppc D.FR (BVType 128) where
|
||||
extractValue fr = G.getRegValue (R.PPC_FR fr)
|
||||
|
||||
instance ExtractValue arch D.AbsBranchTarget (BVType 24) where
|
||||
|
||||
@ -14,13 +14,16 @@ module Data.Macaw.PPC.PPCReg (
|
||||
PPCReg(..),
|
||||
linuxSystemCallPreservedRegisters,
|
||||
linuxCalleeSaveRegisters,
|
||||
ArchWidth(..)
|
||||
ArchWidth(..),
|
||||
locToRegTH
|
||||
) where
|
||||
|
||||
import GHC.TypeLits
|
||||
|
||||
import Data.Proxy ( Proxy(..) )
|
||||
import qualified Data.Set as S
|
||||
import Language.Haskell.TH
|
||||
import Language.Haskell.TH.Syntax ( lift )
|
||||
import qualified Data.Macaw.CFG as MC
|
||||
import qualified Data.Macaw.Memory as MM
|
||||
import Data.Macaw.Types
|
||||
@ -29,6 +32,7 @@ import Data.Parameterized.Some ( Some(..) )
|
||||
import qualified Data.Parameterized.TH.GADT as TH
|
||||
|
||||
import qualified Dismantle.PPC as D
|
||||
import qualified SemMC.Architecture.PPC.Location as APPC
|
||||
import qualified SemMC.Architecture.PPC32 as PPC32
|
||||
import qualified SemMC.Architecture.PPC64 as PPC64
|
||||
|
||||
@ -141,3 +145,17 @@ ppcRegs = concat [ gprs
|
||||
fprs = [ Some (PPC_FR (D.FR rnum))
|
||||
| rnum <- [0..31]
|
||||
]
|
||||
|
||||
locToRegTH :: (1 <= APPC.ArchRegWidth ppc,
|
||||
MC.RegAddrWidth (PPCReg ppc) ~ APPC.ArchRegWidth ppc)
|
||||
=> proxy ppc
|
||||
-> APPC.Location ppc ctp
|
||||
-> Q Exp
|
||||
locToRegTH _ (APPC.LocGPR (D.GPR gpr)) = [| PPC_GP (D.GPR $(lift gpr)) |]
|
||||
locToRegTH _ (APPC.LocVSR (D.VSReg vsr)) = [| PPC_FR (D.VSReg $(lift vsr)) |]
|
||||
locToRegTH _ APPC.LocIP = [| PPC_IP |]
|
||||
locToRegTH _ APPC.LocLNK = [| PPC_LNK |]
|
||||
locToRegTH _ APPC.LocCTR = [| PPC_CTR |]
|
||||
locToRegTH _ APPC.LocCR = [| PPC_CR |]
|
||||
locToRegTH _ APPC.LocXER = [| PPC_XER |]
|
||||
locToRegTH _ _ = [| undefined |]
|
||||
|
||||
@ -35,14 +35,15 @@ import Data.Parameterized.NatRepr ( knownNat
|
||||
, natValue
|
||||
)
|
||||
|
||||
import Data.Macaw.PPC.Generator
|
||||
import Data.Macaw.SemMC.Generator
|
||||
import Data.Macaw.PPC.Arch ( PPCArchConstraints )
|
||||
import Data.Macaw.PPC.PPCReg
|
||||
|
||||
type family FromCrucibleBaseType (btp :: S.BaseType) :: M.Type where
|
||||
FromCrucibleBaseType (S.BaseBVType w) = M.BVType w
|
||||
FromCrucibleBaseType (S.BaseBoolType) = M.BoolType
|
||||
|
||||
crucAppToExpr :: (M.ArchConstraints ppc) => S.App (S.Elt t) ctp -> PPCGenerator ppc ids s (Expr ppc ids (FromCrucibleBaseType ctp))
|
||||
crucAppToExpr :: (M.ArchConstraints ppc) => S.App (S.Elt t) ctp -> Generator ppc ids s (Expr ppc ids (FromCrucibleBaseType ctp))
|
||||
crucAppToExpr S.TrueBool = return $ ValueExpr (M.BoolValue True)
|
||||
crucAppToExpr S.FalseBool = return $ ValueExpr (M.BoolValue False)
|
||||
crucAppToExpr (S.NotBool bool) = (AppExpr . M.NotApp) <$> addElt bool
|
||||
@ -140,13 +141,13 @@ locToReg _ APPC.LocCR = PPC_CR
|
||||
locToReg _ _ = undefined
|
||||
-- fill the rest out later
|
||||
|
||||
-- | Given a location to modify and a crucible formula, construct a PPCGenerator that
|
||||
-- | Given a location to modify and a crucible formula, construct a Generator that
|
||||
-- will modify the location by the function encoded in the formula.
|
||||
interpretFormula :: forall ppc t ctp s ids
|
||||
. (PPCArchConstraints ppc, 1 <= APPC.ArchRegWidth ppc, M.RegAddrWidth (PPCReg ppc) ~ APPC.ArchRegWidth ppc)
|
||||
=> APPC.Location ppc ctp
|
||||
-> S.Elt t ctp
|
||||
-> PPCGenerator ppc ids s ()
|
||||
-> Generator ppc ids s ()
|
||||
interpretFormula loc elt = do
|
||||
expr <- eltToExpr elt
|
||||
let reg = (locToReg (Proxy @ppc) loc)
|
||||
@ -157,11 +158,11 @@ interpretFormula loc elt = do
|
||||
setRegVal reg (M.AssignedValue assignment)
|
||||
|
||||
-- Convert a Crucible element into an expression.
|
||||
eltToExpr :: M.ArchConstraints ppc => S.Elt t ctp -> PPCGenerator ppc ids s (Expr ppc ids (FromCrucibleBaseType ctp))
|
||||
eltToExpr :: M.ArchConstraints ppc => S.Elt t ctp -> Generator ppc ids s (Expr ppc ids (FromCrucibleBaseType ctp))
|
||||
eltToExpr (S.BVElt w val _) = return $ ValueExpr (M.BVValue w val)
|
||||
eltToExpr (S.AppElt appElt) = crucAppToExpr (S.appEltApp appElt)
|
||||
eltToExpr _ = undefined
|
||||
|
||||
-- Add a Crucible element in the PPCGenerator monad.
|
||||
addElt :: M.ArchConstraints ppc => S.Elt t ctp -> PPCGenerator ppc ids s (M.Value ppc ids (FromCrucibleBaseType ctp))
|
||||
-- Add a Crucible element in the Generator monad.
|
||||
addElt :: M.ArchConstraints ppc => S.Elt t ctp -> Generator ppc ids s (M.Value ppc ids (FromCrucibleBaseType ctp))
|
||||
addElt elt = eltToExpr elt >>= addExpr
|
||||
|
||||
@ -14,8 +14,10 @@ import qualified Data.Macaw.Types as MT
|
||||
import SemMC.Architecture.PPC32 ( PPC )
|
||||
import SemMC.Architecture.PPC32.Opcodes ( allSemantics, allOpcodeInfo )
|
||||
|
||||
import Data.Macaw.PPC.Generator
|
||||
import Data.Macaw.SemMC.Generator
|
||||
import Data.Macaw.PPC.Arch ( specialSemanticsCases )
|
||||
import Data.Macaw.PPC.PPCReg ( locToRegTH )
|
||||
import Data.Macaw.PPC.Semantics.TH ( genExecInstruction )
|
||||
|
||||
execInstruction :: MC.Value PPC ids (MT.BVType 32) -> Instruction -> Maybe (PPCGenerator PPC ids s ())
|
||||
execInstruction = $(genExecInstruction (Proxy @PPC) (C.Sub C.Dict) allSemantics allOpcodeInfo)
|
||||
execInstruction :: MC.Value PPC ids (MT.BVType 32) -> Instruction -> Maybe (Generator PPC ids s ())
|
||||
execInstruction = $(genExecInstruction (Proxy @PPC) (locToRegTH (Proxy @PPC)) specialSemanticsCases (C.Sub C.Dict) allSemantics allOpcodeInfo)
|
||||
|
||||
@ -14,8 +14,10 @@ import qualified Data.Macaw.Types as MT
|
||||
import SemMC.Architecture.PPC64 ( PPC )
|
||||
import SemMC.Architecture.PPC64.Opcodes ( allSemantics, allOpcodeInfo )
|
||||
|
||||
import Data.Macaw.PPC.Generator
|
||||
import Data.Macaw.SemMC.Generator
|
||||
import Data.Macaw.PPC.Arch ( specialSemanticsCases )
|
||||
import Data.Macaw.PPC.PPCReg ( locToRegTH )
|
||||
import Data.Macaw.PPC.Semantics.TH
|
||||
|
||||
execInstruction :: MC.Value PPC ids (MT.BVType 64) -> Instruction -> Maybe (PPCGenerator PPC ids s ())
|
||||
execInstruction = $(genExecInstruction (Proxy @PPC) (C.Sub C.Dict) allSemantics allOpcodeInfo)
|
||||
execInstruction :: MC.Value PPC ids (MT.BVType 64) -> Instruction -> Maybe (Generator PPC ids s ())
|
||||
execInstruction = $(genExecInstruction (Proxy @PPC) (locToRegTH (Proxy @PPC)) specialSemanticsCases (C.Sub C.Dict) allSemantics allOpcodeInfo)
|
||||
|
||||
@ -52,7 +52,6 @@ import qualified SemMC.Architecture.Location as L
|
||||
import qualified SemMC.Architecture.PPC.Eval as PE
|
||||
import qualified SemMC.Architecture.PPC.Location as APPC
|
||||
import qualified Data.Macaw.CFG as M
|
||||
import qualified Data.Macaw.CFG.Block as M
|
||||
import qualified Data.Macaw.Memory as M
|
||||
import qualified Data.Macaw.Types as M
|
||||
|
||||
@ -60,11 +59,13 @@ import Data.Parameterized.NatRepr ( knownNat
|
||||
, natValue
|
||||
)
|
||||
|
||||
import Data.Macaw.SemMC.Generator
|
||||
import Data.Macaw.SemMC.Translations
|
||||
import Data.Macaw.SemMC.TH.Monad
|
||||
|
||||
import Data.Macaw.PPC.Arch
|
||||
import Data.Macaw.PPC.Generator
|
||||
import Data.Macaw.PPC.Operand
|
||||
import Data.Macaw.PPC.PPCReg
|
||||
import Data.Macaw.PPC.Semantics.TH.Monad
|
||||
|
||||
type Sym t = S.SimpleBackend t
|
||||
|
||||
@ -87,32 +88,16 @@ instructionMatcher :: (OrdF a, LF.LiftF a,
|
||||
L.Location arch ~ APPC.Location arch,
|
||||
1 <= APPC.ArchRegWidth arch,
|
||||
M.RegAddrWidth (PPCReg arch) ~ APPC.ArchRegWidth arch)
|
||||
=> Map.MapF (Witness c a) (PairF (ParameterizedFormula (Sym t) arch) (DT.CaptureInfo c a))
|
||||
=> (forall tp . L.Location arch tp -> Q Exp)
|
||||
-> [MatchQ]
|
||||
-> Map.MapF (Witness c a) (PairF (ParameterizedFormula (Sym t) arch) (DT.CaptureInfo c a))
|
||||
-> Q Exp
|
||||
instructionMatcher formulas = do
|
||||
instructionMatcher ltr specialCases formulas = do
|
||||
ipVarName <- newName "ipVal"
|
||||
opcodeVar <- newName "opcode"
|
||||
operandListVar <- newName "operands"
|
||||
let normalCases = map (mkSemanticsCase ipVarName operandListVar) (Map.toList formulas)
|
||||
lamE [varP ipVarName, conP 'D.Instruction [varP opcodeVar, varP operandListVar]] (caseE (varE opcodeVar) (normalCases ++ specialSemanticsCases))
|
||||
|
||||
-- | Manually-provided semantics for instructions whose full semantics cannot be
|
||||
-- expressed in our semantics format.
|
||||
--
|
||||
-- This includes instructions with special side effects that we don't have a way
|
||||
-- to talk about in the semantics; especially useful for architecture-specific
|
||||
-- terminator statements.
|
||||
specialSemanticsCases :: [MatchQ]
|
||||
specialSemanticsCases =
|
||||
[ match (conP 'D.SC []) (normalB syscallBody) []
|
||||
, match (conP 'D.TRAP []) (normalB trapBody) []
|
||||
, match (conP 'D.ATTN []) (normalB [| Just (addStmt (M.ExecArchStmt Attn)) |]) []
|
||||
, match (conP 'D.SYNC []) (normalB [| Just (addStmt (M.ExecArchStmt Sync)) |]) []
|
||||
, match (conP 'D.ISYNC []) (normalB [| Just (addStmt (M.ExecArchStmt Isync)) |]) []
|
||||
]
|
||||
where
|
||||
syscallBody = [| Just (finishWithTerminator (M.ArchTermStmt PPCSyscall)) |]
|
||||
trapBody = [| Just (finishWithTerminator (M.ArchTermStmt PPCTrap)) |]
|
||||
let normalCases = map (mkSemanticsCase ltr ipVarName operandListVar) (Map.toList formulas)
|
||||
lamE [varP ipVarName, conP 'D.Instruction [varP opcodeVar, varP operandListVar]] (caseE (varE opcodeVar) (normalCases ++ specialCases))
|
||||
|
||||
-- | Generate a single case for one opcode of the case expression.
|
||||
--
|
||||
@ -124,12 +109,13 @@ mkSemanticsCase :: (LF.LiftF a,
|
||||
L.Location arch ~ APPC.Location arch,
|
||||
1 <= APPC.ArchRegWidth arch,
|
||||
M.RegAddrWidth (PPCReg arch) ~ APPC.ArchRegWidth arch)
|
||||
=> Name
|
||||
=> (forall tp . L.Location arch tp -> Q Exp)
|
||||
-> Name
|
||||
-> Name
|
||||
-> Map.Pair (Witness c a) (PairF (ParameterizedFormula (Sym t) arch) (DT.CaptureInfo c a))
|
||||
-> MatchQ
|
||||
mkSemanticsCase ipVarName operandListVar (Map.Pair (Witness opc) (PairF semantics capInfo)) =
|
||||
match (conP (DT.capturedOpcodeName capInfo) []) (normalB (mkOperandListCase ipVarName operandListVar opc semantics capInfo)) []
|
||||
mkSemanticsCase ltr ipVarName operandListVar (Map.Pair (Witness opc) (PairF semantics capInfo)) =
|
||||
match (conP (DT.capturedOpcodeName capInfo) []) (normalB (mkOperandListCase ltr ipVarName operandListVar opc semantics capInfo)) []
|
||||
|
||||
-- | For each opcode case, we have a sub-case expression to destructure the
|
||||
-- operand list into names that we can reference. This generates an expression
|
||||
@ -158,14 +144,15 @@ mkOperandListCase :: (L.Location arch ~ APPC.Location arch,
|
||||
A.Architecture arch,
|
||||
1 <= APPC.ArchRegWidth arch,
|
||||
M.RegAddrWidth (PPCReg arch) ~ APPC.ArchRegWidth arch)
|
||||
=> Name
|
||||
=> (forall tp0 . L.Location arch tp0 -> Q Exp)
|
||||
-> Name
|
||||
-> Name
|
||||
-> a tp
|
||||
-> ParameterizedFormula (Sym t) arch tp
|
||||
-> DT.CaptureInfo c a tp
|
||||
-> Q Exp
|
||||
mkOperandListCase ipVarName operandListVar opc semantics capInfo = do
|
||||
body <- genCaseBody ipVarName opc semantics (DT.capturedOperandNames capInfo)
|
||||
mkOperandListCase ltr ipVarName operandListVar opc semantics capInfo = do
|
||||
body <- genCaseBody ltr ipVarName opc semantics (DT.capturedOperandNames capInfo)
|
||||
DT.genCase capInfo operandListVar body
|
||||
|
||||
data BoundVarInterpretations arch t =
|
||||
@ -190,14 +177,15 @@ genCaseBody :: forall a sh t arch
|
||||
A.Architecture arch,
|
||||
1 <= APPC.ArchRegWidth arch,
|
||||
M.RegAddrWidth (PPCReg arch) ~ APPC.ArchRegWidth arch)
|
||||
=> Name
|
||||
=> (forall tp . L.Location arch tp -> Q Exp)
|
||||
-> Name
|
||||
-> a sh
|
||||
-> ParameterizedFormula (Sym t) arch sh
|
||||
-> SL.ShapedList (FreeParamF Name) sh
|
||||
-> Q Exp
|
||||
genCaseBody ipVarName _opc semantics varNames = do
|
||||
genCaseBody ltr ipVarName _opc semantics varNames = do
|
||||
regsName <- newName "_regs"
|
||||
translateFormula ipVarName semantics (BoundVarInterpretations locVarsMap opVarsMap regsName) varNames
|
||||
translateFormula ltr ipVarName semantics (BoundVarInterpretations locVarsMap opVarsMap regsName) varNames
|
||||
where
|
||||
locVarsMap :: Map.MapF (SI.BoundVar (Sym t)) (L.Location arch)
|
||||
locVarsMap = Map.foldrWithKey (collectVarForLocation (Proxy @arch)) Map.empty (pfLiteralVars semantics)
|
||||
@ -249,6 +237,9 @@ genExecInstruction :: (A.Architecture arch,
|
||||
1 <= APPC.ArchRegWidth arch,
|
||||
M.RegAddrWidth (PPCReg arch) ~ APPC.ArchRegWidth arch)
|
||||
=> proxy arch
|
||||
-> (forall tp . L.Location arch tp -> Q Exp)
|
||||
-> [MatchQ]
|
||||
-- ^ Special cases to splice into the expression
|
||||
-> (forall sh . c sh C.:- BuildOperandList arch sh)
|
||||
-- ^ A constraint implication to let us extract/weaken the
|
||||
-- constraint in our 'Witness' to the required 'BuildOperandList'
|
||||
@ -261,12 +252,12 @@ genExecInstruction :: (A.Architecture arch,
|
||||
-- some TH to match them. This comes from the semantics
|
||||
-- definitions in semmc.
|
||||
-> Q Exp
|
||||
genExecInstruction _ impl semantics captureInfo = do
|
||||
genExecInstruction _ ltr specialCases impl semantics captureInfo = do
|
||||
Some ng <- runIO PN.newIONonceGenerator
|
||||
sym <- runIO (S.newSimpleBackend ng)
|
||||
formulas <- runIO (loadFormulas sym impl semantics)
|
||||
let formulasWithInfo = foldr (attachInfo formulas) Map.empty captureInfo
|
||||
instructionMatcher formulasWithInfo
|
||||
instructionMatcher ltr specialCases formulasWithInfo
|
||||
where
|
||||
attachInfo m0 (Some ci) m =
|
||||
let co = DT.capturedOpcode ci
|
||||
@ -290,17 +281,18 @@ translateFormula :: forall arch t sh .
|
||||
A.Architecture arch,
|
||||
1 <= APPC.ArchRegWidth arch,
|
||||
M.RegAddrWidth (PPCReg arch) ~ APPC.ArchRegWidth arch)
|
||||
=> Name
|
||||
=> (forall tp . L.Location arch tp -> Q Exp)
|
||||
-> Name
|
||||
-> ParameterizedFormula (Sym t) arch sh
|
||||
-> BoundVarInterpretations arch t
|
||||
-> SL.ShapedList (FreeParamF Name) sh
|
||||
-> Q Exp
|
||||
translateFormula ipVarName semantics interps varNames = do
|
||||
translateFormula ltr ipVarName semantics interps varNames = do
|
||||
let preamble = [ bindS (varP (regsValName interps)) [| getRegs |] ]
|
||||
exps <- runMacawQ (mapM_ translateDefinition (Map.toList (pfDefs semantics)))
|
||||
exps <- runMacawQ ltr (mapM_ translateDefinition (Map.toList (pfDefs semantics)))
|
||||
[| Just $(doSequenceQ preamble exps) |]
|
||||
where translateDefinition :: Map.Pair (Parameter arch sh) (S.SymExpr (Sym t))
|
||||
-> MacawQ t ()
|
||||
-> MacawQ arch t ()
|
||||
translateDefinition (Map.Pair param expr) = do
|
||||
case param of
|
||||
OperandParameter _w idx -> do
|
||||
@ -310,7 +302,7 @@ translateFormula ipVarName semantics interps varNames = do
|
||||
LiteralParameter APPC.LocMem -> writeMemTH interps expr
|
||||
LiteralParameter loc -> do
|
||||
valExp <- addEltTH interps expr
|
||||
appendStmt [| setRegVal $(locToRegTH (Proxy @arch) loc) $(return valExp) |]
|
||||
appendStmt [| setRegVal $(ltr loc) $(return valExp) |]
|
||||
FunctionParameter str (WrappedOperand _ opIx) _w -> do
|
||||
let FreeParamF boundOperandName = SL.indexShapedList varNames opIx
|
||||
case lookup str (A.locationFuncInterpretation (Proxy @arch)) of
|
||||
@ -329,7 +321,7 @@ addEltTH :: forall arch t ctp .
|
||||
M.RegAddrWidth (PPCReg arch) ~ APPC.ArchRegWidth arch)
|
||||
=> BoundVarInterpretations arch t
|
||||
-> S.Elt t ctp
|
||||
-> MacawQ t Exp
|
||||
-> MacawQ arch t Exp
|
||||
addEltTH interps elt = do
|
||||
mexp <- lookupElt elt
|
||||
case mexp of
|
||||
@ -343,8 +335,8 @@ addEltTH interps elt = do
|
||||
bindExpr elt [| addExpr =<< $(return translatedExpr) |]
|
||||
S.BoundVarElt bVar ->
|
||||
case Map.lookup bVar (locVars interps) of
|
||||
Just loc ->
|
||||
bindExpr elt [| return ($(varE (regsValName interps)) ^. M.boundValue $(locToRegTH (Proxy @arch) loc)) |]
|
||||
Just loc -> withLocToReg $ \ltr -> do
|
||||
bindExpr elt [| return ($(varE (regsValName interps)) ^. M.boundValue $(ltr loc)) |]
|
||||
Nothing ->
|
||||
case Map.lookup bVar (opVars interps) of
|
||||
Just (FreeParamF name) -> bindExpr elt [| extractValue $(varE name) |]
|
||||
@ -364,7 +356,7 @@ writeMemTH :: forall arch t tp
|
||||
M.RegAddrWidth (PPCReg arch) ~ APPC.ArchRegWidth arch)
|
||||
=> BoundVarInterpretations arch t
|
||||
-> S.Elt t tp
|
||||
-> MacawQ t ()
|
||||
-> MacawQ arch t ()
|
||||
writeMemTH bvi expr =
|
||||
case expr of
|
||||
S.NonceAppElt n ->
|
||||
@ -393,7 +385,7 @@ evalNonceAppTH :: forall arch t tp
|
||||
M.RegAddrWidth (PPCReg arch) ~ APPC.ArchRegWidth arch)
|
||||
=> BoundVarInterpretations arch t
|
||||
-> S.NonceApp t (S.Elt t) tp
|
||||
-> MacawQ t Exp
|
||||
-> MacawQ arch t Exp
|
||||
evalNonceAppTH bvi nonceApp =
|
||||
case nonceApp of
|
||||
S.FnApp symFn args -> do
|
||||
@ -516,7 +508,7 @@ floatingPointTH :: forall arch t f c
|
||||
=> BoundVarInterpretations arch t
|
||||
-> String
|
||||
-> f (S.Elt t) c
|
||||
-> MacawQ t Exp
|
||||
-> MacawQ arch t Exp
|
||||
floatingPointTH bvi fnName args =
|
||||
case FC.toListFC Some args of
|
||||
[Some a] ->
|
||||
@ -642,7 +634,7 @@ crucAppToExprTH :: (L.Location arch ~ APPC.Location arch,
|
||||
M.RegAddrWidth (PPCReg arch) ~ APPC.ArchRegWidth arch)
|
||||
=> S.App (S.Elt t) ctp
|
||||
-> BoundVarInterpretations arch t
|
||||
-> MacawQ t Exp
|
||||
-> MacawQ arch t Exp
|
||||
crucAppToExprTH elt interps = case elt of
|
||||
S.TrueBool -> liftQ [| return $ ValueExpr (M.BoolValue True) |]
|
||||
S.FalseBool -> liftQ [| return $ ValueExpr (M.BoolValue False) |]
|
||||
@ -763,17 +755,3 @@ crucAppToExprTH elt interps = case elt of
|
||||
liftQ [| return (AppExpr (M.BVXor $(natReprTH w) $(return e1) $(return e2))) |]
|
||||
_ -> liftQ [| error "unsupported Crucible elt" |]
|
||||
|
||||
locToRegTH :: (1 <= APPC.ArchRegWidth ppc,
|
||||
M.RegAddrWidth (PPCReg ppc) ~ APPC.ArchRegWidth ppc)
|
||||
=> proxy ppc
|
||||
-> APPC.Location ppc ctp
|
||||
-> Q Exp
|
||||
locToRegTH _ (APPC.LocGPR (D.GPR gpr)) = [| PPC_GP (D.GPR $(lift gpr)) |]
|
||||
locToRegTH _ (APPC.LocVSR (D.VSReg vsr)) = [| PPC_FR (D.VSReg $(lift vsr)) |]
|
||||
locToRegTH _ APPC.LocIP = [| PPC_IP |]
|
||||
locToRegTH _ APPC.LocLNK = [| PPC_LNK |]
|
||||
locToRegTH _ APPC.LocCTR = [| PPC_CTR |]
|
||||
locToRegTH _ APPC.LocCR = [| PPC_CR |]
|
||||
locToRegTH _ APPC.LocXER = [| PPC_XER |]
|
||||
locToRegTH _ _ = [| undefined |]
|
||||
-- fill the rest out later
|
||||
|
||||
@ -1,80 +0,0 @@
|
||||
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
|
||||
module Data.Macaw.PPC.Semantics.TH.Monad (
|
||||
MacawQ,
|
||||
runMacawQ,
|
||||
liftQ,
|
||||
lookupElt,
|
||||
appendStmt,
|
||||
bindExpr
|
||||
) where
|
||||
|
||||
import qualified Control.Monad.State.Strict as St
|
||||
import Control.Monad.Trans ( lift )
|
||||
import qualified Data.Foldable as F
|
||||
import qualified Data.Map.Strict as M
|
||||
import qualified Data.Sequence as Seq
|
||||
import Language.Haskell.TH
|
||||
|
||||
import Data.Parameterized.Some ( Some(..) )
|
||||
import qualified Lang.Crucible.Solver.SimpleBuilder as S
|
||||
|
||||
data QState t = QState { accumulatedStatements :: !(Seq.Seq Stmt)
|
||||
-- ^ The list of template haskell statements accumulated
|
||||
-- for this monadic context. At the end of the context, we
|
||||
-- can extract these and wrap them in a @do@ expression.
|
||||
, expressionCache :: !(M.Map (Some (S.Elt t)) Exp)
|
||||
-- ^ A cache of translations of SimpleBuilder terms into
|
||||
-- TH. The cached values are not the translated exprs;
|
||||
-- instead, they are names that are bound for those
|
||||
-- terms (via 'VarE')
|
||||
}
|
||||
|
||||
emptyQState :: QState t
|
||||
emptyQState = QState { accumulatedStatements = Seq.empty
|
||||
, expressionCache = M.empty
|
||||
}
|
||||
|
||||
newtype MacawQ t a = MacawQ { unQ :: St.StateT (QState t) Q a }
|
||||
deriving (Functor,
|
||||
Applicative,
|
||||
Monad,
|
||||
St.MonadState (QState t))
|
||||
|
||||
runMacawQ :: MacawQ t () -> Q [Stmt]
|
||||
runMacawQ act = (F.toList . accumulatedStatements) <$> St.execStateT (unQ act) emptyQState
|
||||
|
||||
-- | Lift a TH computation (in the 'Q' monad) into the monad.
|
||||
liftQ :: Q a -> MacawQ t a
|
||||
liftQ q = MacawQ (lift q)
|
||||
|
||||
-- | Look up an 'S.Elt' in the cache
|
||||
lookupElt :: S.Elt t tp -> MacawQ t (Maybe Exp)
|
||||
lookupElt elt = do
|
||||
c <- St.gets expressionCache
|
||||
return (M.lookup (Some elt) c)
|
||||
|
||||
-- | Append a statement that doesn't need to bind a new name
|
||||
appendStmt :: ExpQ -> MacawQ t ()
|
||||
appendStmt eq = do
|
||||
e <- liftQ eq
|
||||
St.modify' $ \s -> s { accumulatedStatements = accumulatedStatements s Seq.|> NoBindS e }
|
||||
|
||||
-- | Bind a TH expression to a name (as a 'Stmt') and return the expression that
|
||||
-- refers to the bound value. For example, if you call
|
||||
--
|
||||
-- > bindExpr [| return (1 + 2) |]
|
||||
--
|
||||
-- The statement added to the state is
|
||||
--
|
||||
-- > newName <- expr
|
||||
--
|
||||
-- and the new name is returned.
|
||||
bindExpr :: S.Elt t tp -> ExpQ -> MacawQ t Exp
|
||||
bindExpr elt eq = do
|
||||
e <- liftQ eq
|
||||
n <- liftQ (newName "val")
|
||||
let res = VarE n
|
||||
St.modify' $ \s -> s { accumulatedStatements = accumulatedStatements s Seq.|> BindS (VarP n) e
|
||||
, expressionCache = M.insert (Some elt) res (expressionCache s)
|
||||
}
|
||||
return res
|
||||
@ -16,9 +16,20 @@ extra-source-files: ChangeLog.md
|
||||
cabal-version: >=1.10
|
||||
|
||||
library
|
||||
-- exposed-modules:
|
||||
-- other-modules:
|
||||
exposed-modules: Data.Macaw.SemMC.Generator
|
||||
Data.Macaw.SemMC.Simplify
|
||||
Data.Macaw.SemMC.Translations
|
||||
Data.Macaw.SemMC.TH.Monad
|
||||
-- other-extensions:
|
||||
build-depends: base >=4.9 && <5
|
||||
build-depends: base >=4.9 && <5,
|
||||
template-haskell,
|
||||
containers,
|
||||
mtl,
|
||||
lens,
|
||||
parameterized-utils,
|
||||
crucible,
|
||||
macaw-base,
|
||||
semmc
|
||||
hs-source-dirs: src
|
||||
default-language: Haskell2010
|
||||
ghc-options: -Wall
|
||||
395
macaw-semmc/src/Data/Macaw/SemMC/Generator.hs
Normal file
395
macaw-semmc/src/Data/Macaw/SemMC/Generator.hs
Normal file
@ -0,0 +1,395 @@
|
||||
{-# LANGUAGE DataKinds #-}
|
||||
{-# LANGUAGE FlexibleContexts #-}
|
||||
{-# LANGUAGE GADTs #-}
|
||||
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
|
||||
{-# LANGUAGE MultiParamTypeClasses #-}
|
||||
{-# LANGUAGE StandaloneDeriving #-}
|
||||
{-# LANGUAGE TypeOperators #-}
|
||||
{-# LANGUAGE UndecidableInstances #-}
|
||||
module Data.Macaw.SemMC.Generator (
|
||||
-- * Expressions
|
||||
Expr(..),
|
||||
-- * Blocks
|
||||
BlockSeq(..),
|
||||
nextBlockID,
|
||||
frontierBlocks,
|
||||
PreBlock(..),
|
||||
pBlockStmts,
|
||||
pBlockState,
|
||||
GenState(..),
|
||||
initGenState,
|
||||
initRegState,
|
||||
blockSeq,
|
||||
blockState,
|
||||
finishBlock,
|
||||
finishBlock',
|
||||
-- * State updates
|
||||
curRegState,
|
||||
setRegVal,
|
||||
addStmt,
|
||||
addAssignment,
|
||||
addExpr,
|
||||
finishWithTerminator,
|
||||
conditionalBranch,
|
||||
-- * State access
|
||||
getRegs,
|
||||
getRegValue,
|
||||
-- * Results
|
||||
GenResult(..),
|
||||
-- * Monad
|
||||
GenCont,
|
||||
Generator,
|
||||
runGenerator,
|
||||
shiftGen,
|
||||
genResult,
|
||||
-- * Errors
|
||||
GeneratorError(..)
|
||||
) where
|
||||
|
||||
import GHC.TypeLits
|
||||
|
||||
import Control.Lens
|
||||
import qualified Control.Monad.Cont as Ct
|
||||
import qualified Control.Monad.Except as ET
|
||||
import qualified Control.Monad.Reader as Rd
|
||||
import Control.Monad.ST ( ST )
|
||||
import qualified Control.Monad.State.Strict as St
|
||||
import Control.Monad.Trans ( lift )
|
||||
import qualified Data.Foldable as F
|
||||
import Data.Maybe ( fromMaybe )
|
||||
import qualified Data.Sequence as Seq
|
||||
import Data.Word (Word64)
|
||||
|
||||
import Data.Macaw.CFG
|
||||
import Data.Macaw.CFG.Block
|
||||
import qualified Data.Macaw.Memory as MM
|
||||
import Data.Macaw.Types ( BoolType )
|
||||
import Data.Parameterized.Classes
|
||||
import qualified Data.Parameterized.NatRepr as NR
|
||||
import qualified Data.Parameterized.Nonce as NC
|
||||
|
||||
import Data.Macaw.SemMC.Simplify ( simplifyValue, simplifyApp )
|
||||
|
||||
data Expr arch ids tp where
|
||||
ValueExpr :: !(Value arch ids tp) -> Expr arch ids tp
|
||||
AppExpr :: !(App (Value arch ids) tp) -> Expr arch ids tp
|
||||
|
||||
data GenResult arch ids =
|
||||
GenResult { resBlockSeq :: BlockSeq arch ids
|
||||
, resState :: Maybe (PreBlock arch ids)
|
||||
}
|
||||
|
||||
data BlockSeq arch ids =
|
||||
BlockSeq { _nextBlockID :: !Word64
|
||||
, _frontierBlocks :: !(Seq.Seq (Block arch ids))
|
||||
}
|
||||
|
||||
deriving instance Show (Block arch ids) => Show (BlockSeq arch ids)
|
||||
-- deriving instance (PPCArchConstraints ppc) => Show (Block ppc ids)
|
||||
-- deriving instance (PPCArchConstraints ppc) => Show (TermStmt ppc ids)
|
||||
|
||||
-- | Control flow blocs generated so far.
|
||||
nextBlockID :: Simple Lens (BlockSeq arch ids) Word64
|
||||
nextBlockID = lens _nextBlockID (\s v -> s { _nextBlockID = v })
|
||||
|
||||
-- | Blocks that are not in CFG that end with a FetchAndExecute,
|
||||
-- which we need to analyze to compute new potential branch targets.
|
||||
frontierBlocks :: Simple Lens (BlockSeq arch ids) (Seq.Seq (Block arch ids))
|
||||
frontierBlocks = lens _frontierBlocks (\s v -> s { _frontierBlocks = v })
|
||||
|
||||
data PreBlock arch ids =
|
||||
PreBlock { pBlockIndex :: !Word64
|
||||
, pBlockAddr :: MM.MemSegmentOff (ArchAddrWidth arch)
|
||||
, _pBlockStmts :: !(Seq.Seq (Stmt arch ids))
|
||||
, _pBlockState :: !(RegState (ArchReg arch) (Value arch ids))
|
||||
}
|
||||
|
||||
-- | An accessor for the current statements in the 'PreBlock'
|
||||
pBlockStmts :: Simple Lens (PreBlock arch ids) (Seq.Seq (Stmt arch ids))
|
||||
pBlockStmts = lens _pBlockStmts (\s v -> s { _pBlockStmts = v })
|
||||
|
||||
-- | An accessor for the current register state held in the 'PreBlock'
|
||||
pBlockState :: Simple Lens (PreBlock arch ids) (RegState (ArchReg arch) (Value arch ids))
|
||||
pBlockState = lens _pBlockState (\s v -> s { _pBlockState = v })
|
||||
|
||||
data GenState arch ids s =
|
||||
GenState { assignIdGen :: NC.NonceGenerator (ST s) ids
|
||||
, _blockSeq :: !(BlockSeq arch ids)
|
||||
, _blockState :: !(PreBlock arch ids)
|
||||
, genAddr :: MM.MemSegmentOff (ArchAddrWidth arch)
|
||||
, genMemory :: MM.Memory (ArchAddrWidth arch)
|
||||
}
|
||||
|
||||
emptyPreBlock :: RegState (ArchReg arch) (Value arch ids)
|
||||
-> Word64
|
||||
-> MM.MemSegmentOff (RegAddrWidth (ArchReg arch))
|
||||
-> PreBlock arch ids
|
||||
emptyPreBlock s0 idx addr =
|
||||
PreBlock { pBlockIndex = idx
|
||||
, pBlockAddr = addr
|
||||
, _pBlockStmts = Seq.empty
|
||||
, _pBlockState = s0
|
||||
}
|
||||
|
||||
initGenState :: NC.NonceGenerator (ST s) ids
|
||||
-> MM.Memory (ArchAddrWidth arch)
|
||||
-> MM.MemSegmentOff (ArchAddrWidth arch)
|
||||
-> RegState (ArchReg arch) (Value arch ids)
|
||||
-> GenState arch ids s
|
||||
initGenState nonceGen mem addr st =
|
||||
GenState { assignIdGen = nonceGen
|
||||
, _blockSeq = BlockSeq { _nextBlockID = 1, _frontierBlocks = Seq.empty }
|
||||
, _blockState = emptyPreBlock st 0 addr
|
||||
, genAddr = addr
|
||||
, genMemory = mem
|
||||
}
|
||||
|
||||
initRegState :: (KnownNat (RegAddrWidth (ArchReg arch)),
|
||||
1 <= RegAddrWidth (ArchReg arch),
|
||||
RegisterInfo (ArchReg arch),
|
||||
MM.MemWidth (RegAddrWidth (ArchReg arch)))
|
||||
=> MM.MemSegmentOff (RegAddrWidth (ArchReg arch))
|
||||
-> RegState (ArchReg arch) (Value arch ids)
|
||||
initRegState startIP =
|
||||
mkRegState Initial & curIP .~ RelocatableValue NR.knownNat (MM.relativeSegmentAddr startIP)
|
||||
|
||||
blockSeq :: Simple Lens (GenState arch ids s) (BlockSeq arch ids)
|
||||
blockSeq = lens _blockSeq (\s v -> s { _blockSeq = v })
|
||||
|
||||
blockState :: Simple Lens (GenState arch ids s) (PreBlock arch ids)
|
||||
blockState = lens _blockState (\s v -> s { _blockState = v })
|
||||
|
||||
curRegState :: Simple Lens (GenState arch ids s) (RegState (ArchReg arch) (Value arch ids))
|
||||
curRegState = blockState . pBlockState
|
||||
|
||||
setRegVal :: (OrdF (ArchReg arch), MM.MemWidth (RegAddrWidth (ArchReg arch)))
|
||||
=> ArchReg arch tp
|
||||
-> Value arch ids tp
|
||||
-> Generator arch ids s ()
|
||||
setRegVal reg val =
|
||||
curRegState . boundValue reg .= fromMaybe val (simplifyValue val)
|
||||
|
||||
addExpr :: (OrdF (ArchReg arch), MM.MemWidth (RegAddrWidth (ArchReg arch)))
|
||||
=> Expr arch ids tp
|
||||
-> Generator arch ids s (Value arch ids tp)
|
||||
addExpr expr =
|
||||
case expr of
|
||||
ValueExpr val -> return val
|
||||
AppExpr app
|
||||
| Just val <- simplifyApp app -> return val
|
||||
| otherwise -> AssignedValue <$> addAssignment (EvalApp app)
|
||||
|
||||
data GeneratorError = InvalidEncoding
|
||||
| GeneratorMessage String
|
||||
deriving (Show)
|
||||
|
||||
-- | This is a state monad (with error termination via 'ET.ExceptT') built on
|
||||
-- top of 'Ct.ContT' and 'Rd.ReaderT'.
|
||||
--
|
||||
-- We use the 'Ct.ContT' for early termination when dealing with control flow
|
||||
-- terminators (e.g., syscall) and to split for dealing with conditional
|
||||
-- branches.
|
||||
--
|
||||
-- The state is managed by explicitly passing it through the continuation.
|
||||
--
|
||||
-- The most important operation provided is the primitive 'shiftGen', which is
|
||||
-- used to build 'conditionalBranch'.
|
||||
--
|
||||
-- The base monad is 'ST', which is used for nonce generation.
|
||||
newtype Generator arch ids s a =
|
||||
Generator { runG :: Ct.ContT (GenResult arch ids)
|
||||
(Rd.ReaderT (GenState arch ids s)
|
||||
(ET.ExceptT GeneratorError (ST s))) a }
|
||||
deriving (Applicative,
|
||||
Functor,
|
||||
Rd.MonadReader (GenState arch ids s),
|
||||
Ct.MonadCont)
|
||||
-- | The 'Monad' instance is manually-specified so that calls to 'fail' actually
|
||||
-- use our 'ET.ExceptT' 'ET.throwError' for nicer error behavior.
|
||||
instance Monad (Generator arch ids s) where
|
||||
return v = Generator (return v)
|
||||
Generator m >>= h = Generator (m >>= \v -> runG (h v))
|
||||
Generator m >> Generator n = Generator (m >> n)
|
||||
fail msg = Generator (Ct.ContT (\_ -> ET.throwError (GeneratorMessage msg)))
|
||||
|
||||
instance St.MonadState (GenState arch ids s) (Generator arch ids s) where
|
||||
get = Generator Rd.ask
|
||||
put nextState = Generator $ Ct.ContT $ \c -> Rd.ReaderT $ \_s ->
|
||||
Rd.runReaderT (c ()) nextState
|
||||
|
||||
instance ET.MonadError GeneratorError (Generator arch ids s) where
|
||||
throwError e = Generator (Ct.ContT (\_ -> ET.throwError e))
|
||||
|
||||
-- | The type of continuations provided by 'shiftGen'
|
||||
type GenCont arch ids s a = a -> GenState arch ids s -> ET.ExceptT GeneratorError (ST s) (GenResult arch ids)
|
||||
|
||||
-- | Given a final continuation to call, run the generator (and produce a final
|
||||
-- result with the given continuation @k@). Also takes an initial state.
|
||||
runGenerator :: GenCont arch ids s a
|
||||
-> GenState arch ids s
|
||||
-> Generator arch ids s a
|
||||
-> ET.ExceptT GeneratorError (ST s) (GenResult arch ids)
|
||||
runGenerator k st (Generator m) = Rd.runReaderT (Ct.runContT m (Rd.ReaderT . k)) st
|
||||
|
||||
-- | Capture the current continuation and execute an action that gets that
|
||||
-- continuation as an argument (it can be invoked as many times as desired).
|
||||
shiftGen :: (GenCont arch ids s a -> GenState arch ids s -> ET.ExceptT GeneratorError (ST s) (GenResult arch ids))
|
||||
-> Generator arch ids s a
|
||||
shiftGen f =
|
||||
Generator $ Ct.ContT $ \k -> Rd.ReaderT $ \s -> f (Rd.runReaderT . k) s
|
||||
|
||||
genResult :: (Monad m) => a -> GenState arch ids s -> m (GenResult arch ids)
|
||||
genResult _ s = do
|
||||
return GenResult { resBlockSeq = s ^. blockSeq
|
||||
, resState = Just (s ^. blockState)
|
||||
}
|
||||
|
||||
-- | Append a statement (on the right) to the list of statements in the current
|
||||
-- 'PreBlock'.
|
||||
addStmt :: Stmt arch ids -> Generator arch ids s ()
|
||||
addStmt stmt = (blockState . pBlockStmts) %= (Seq.|> stmt)
|
||||
|
||||
-- | Generate the next unique ID for an assignment using the nonce generator
|
||||
newAssignId :: Generator arch ids s (AssignId ids tp)
|
||||
newAssignId = do
|
||||
nonceGen <- St.gets assignIdGen
|
||||
AssignId <$> liftST (NC.freshNonce nonceGen)
|
||||
|
||||
-- | Lift an 'ST' action into 'PPCGenerator'
|
||||
liftST :: ST s a -> Generator arch ids s a
|
||||
liftST = Generator . lift . lift . lift
|
||||
|
||||
-- | Append an assignment statement to the list of statements in the current
|
||||
-- 'PreBlock'
|
||||
addAssignment :: AssignRhs arch ids tp
|
||||
-> Generator arch ids s (Assignment arch ids tp)
|
||||
addAssignment rhs = do
|
||||
l <- newAssignId
|
||||
let a = Assignment l rhs
|
||||
addStmt (AssignStmt a)
|
||||
return a
|
||||
|
||||
-- | Get all of the current register values
|
||||
--
|
||||
-- This is meant to be used to snapshot the register state at the beginning of
|
||||
-- an instruction transformer so that we can perform atomic updates to the
|
||||
-- machine state (by reading values from the captured initial state).
|
||||
getRegs :: Generator arch ids s (RegState (ArchReg arch) (Value arch ids))
|
||||
getRegs = do
|
||||
genState <- St.get
|
||||
return (genState ^. (blockState . pBlockState))
|
||||
|
||||
-- | Get the value of a single register.
|
||||
--
|
||||
-- NOTE: This should not be called from the generated semantics transformers.
|
||||
-- Those must get their register values through 'getRegs', which is used to take
|
||||
-- a snapshot of the register state at the beginning of each instruction. This
|
||||
-- is required for instruction updates to register values to have the necessary
|
||||
-- atomic update behavior.
|
||||
getRegValue :: (OrdF (ArchReg arch)) => ArchReg arch tp -> Generator arch ids s (Value arch ids tp)
|
||||
getRegValue r = do
|
||||
genState <- St.get
|
||||
return (genState ^. (blockState . pBlockState . boundValue r))
|
||||
|
||||
-- | Finish a block immediately with the given terminator statement
|
||||
--
|
||||
-- This uses the underlying continuation monad to skip the normal
|
||||
-- post-instruction behavior.
|
||||
--
|
||||
-- NOTE: We do not do an explicit instruction pointer update; the handler for
|
||||
-- architecture-specific terminator statements handles that.
|
||||
finishWithTerminator :: (RegState (ArchReg arch) (Value arch ids) -> TermStmt arch ids)
|
||||
-> Generator arch ids s a
|
||||
finishWithTerminator term =
|
||||
shiftGen $ \_ s0 -> do
|
||||
let pre_block = s0 ^. blockState
|
||||
let fin_block = finishBlock' pre_block term
|
||||
return GenResult { resBlockSeq = s0 ^. blockSeq & frontierBlocks %~ (Seq.|> fin_block)
|
||||
, resState = Nothing
|
||||
}
|
||||
|
||||
-- | Convert the contents of a 'PreBlock' (a block being constructed) into a
|
||||
-- full-fledged 'Block'
|
||||
--
|
||||
-- The @term@ function is used to create the terminator statement of the block.
|
||||
finishBlock' :: PreBlock arch ids
|
||||
-> (RegState (ArchReg arch) (Value arch ids) -> TermStmt arch ids)
|
||||
-> Block arch ids
|
||||
finishBlock' preBlock term =
|
||||
Block { blockLabel = pBlockIndex preBlock
|
||||
, blockStmts = F.toList (preBlock ^. pBlockStmts)
|
||||
, blockTerm = term (preBlock ^. pBlockState)
|
||||
}
|
||||
|
||||
-- | Consume a 'GenResult', finish off the contained 'PreBlock', and append the
|
||||
-- new block to the block frontier.
|
||||
finishBlock :: (RegState (ArchReg arch) (Value arch ids) -> TermStmt arch ids)
|
||||
-> GenResult arch ids
|
||||
-> BlockSeq arch ids
|
||||
finishBlock term st =
|
||||
case resState st of
|
||||
Nothing -> resBlockSeq st
|
||||
Just preBlock ->
|
||||
let b = finishBlock' preBlock term
|
||||
in resBlockSeq st & frontierBlocks %~ (Seq.|> b)
|
||||
|
||||
-- | A primitive for splitting execution in the presence of conditional
|
||||
-- branches.
|
||||
--
|
||||
-- This function uses the underlying continuation monad to split execution. It
|
||||
-- captures the current continuation and builds a block for the true branch and
|
||||
-- another block for the false branch. It manually threads the state between
|
||||
-- the two branches and makes updates to keep them consistent. It also joins
|
||||
-- the two exploration frontiers after processing the true and false branches so
|
||||
-- that the underlying return value contains all discovered blocks.
|
||||
conditionalBranch :: (OrdF (ArchReg arch),
|
||||
MM.MemWidth (RegAddrWidth (ArchReg arch)))
|
||||
=> Value arch ids BoolType
|
||||
-- ^ The conditional guarding the branch
|
||||
-> Generator arch ids s ()
|
||||
-- ^ The action to take on the true branch
|
||||
-> Generator arch ids s ()
|
||||
-- ^ The action to take on the false branch
|
||||
-> Generator arch ids s ()
|
||||
conditionalBranch condExpr t f =
|
||||
go (fromMaybe condExpr (simplifyValue condExpr))
|
||||
where
|
||||
go condv =
|
||||
case condv of
|
||||
BoolValue True -> t
|
||||
BoolValue False -> f
|
||||
_ -> shiftGen $ \c s0 -> do
|
||||
let pre_block = s0 ^. blockState
|
||||
let st = pre_block ^. pBlockState
|
||||
let t_block_label = s0 ^. blockSeq ^. nextBlockID
|
||||
let s1 = s0 & blockSeq . nextBlockID +~ 1
|
||||
& blockSeq . frontierBlocks .~ Seq.empty
|
||||
& blockState .~ emptyPreBlock st t_block_label (genAddr s0)
|
||||
|
||||
-- Explore the true block
|
||||
t_seq <- finishBlock FetchAndExecute <$> runGenerator c s1 t
|
||||
|
||||
-- Explore the false block
|
||||
let f_block_label = t_seq ^. nextBlockID
|
||||
let s2 = GenState { assignIdGen = assignIdGen s0
|
||||
, _blockSeq = BlockSeq { _nextBlockID = t_seq ^. nextBlockID + 1
|
||||
, _frontierBlocks = Seq.empty
|
||||
}
|
||||
, _blockState = emptyPreBlock st f_block_label (genAddr s0)
|
||||
, genAddr = genAddr s0
|
||||
, genMemory = genMemory s0
|
||||
}
|
||||
f_seq <- finishBlock FetchAndExecute <$> runGenerator c s2 f
|
||||
|
||||
-- Join the results with a branch terminator
|
||||
let fin_block = finishBlock' pre_block (\_ -> Branch condv t_block_label f_block_label)
|
||||
let frontier = mconcat [ s0 ^. blockSeq ^. frontierBlocks Seq.|> fin_block
|
||||
, t_seq ^. frontierBlocks
|
||||
, f_seq ^. frontierBlocks
|
||||
]
|
||||
return GenResult { resBlockSeq =
|
||||
BlockSeq { _nextBlockID = _nextBlockID f_seq
|
||||
, _frontierBlocks = frontier
|
||||
}
|
||||
, resState = Nothing
|
||||
}
|
||||
@ -2,7 +2,7 @@
|
||||
{-# LANGUAGE GADTs #-}
|
||||
{-# LANGUAGE RankNTypes #-}
|
||||
{-# LANGUAGE ScopedTypeVariables #-}
|
||||
module Data.Macaw.PPC.Simplify (
|
||||
module Data.Macaw.SemMC.Simplify (
|
||||
simplifyValue,
|
||||
simplifyApp
|
||||
) where
|
||||
90
macaw-semmc/src/Data/Macaw/SemMC/TH/Monad.hs
Normal file
90
macaw-semmc/src/Data/Macaw/SemMC/TH/Monad.hs
Normal file
@ -0,0 +1,90 @@
|
||||
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
|
||||
{-# LANGUAGE RankNTypes #-}
|
||||
module Data.Macaw.SemMC.TH.Monad (
|
||||
MacawQ,
|
||||
runMacawQ,
|
||||
liftQ,
|
||||
lookupElt,
|
||||
appendStmt,
|
||||
withLocToReg,
|
||||
bindExpr
|
||||
) where
|
||||
|
||||
import qualified Control.Monad.State.Strict as St
|
||||
import Control.Monad.Trans ( lift )
|
||||
import qualified Data.Foldable as F
|
||||
import qualified Data.Map.Strict as M
|
||||
import qualified Data.Sequence as Seq
|
||||
import Language.Haskell.TH
|
||||
|
||||
import Data.Parameterized.Some ( Some(..) )
|
||||
import qualified Lang.Crucible.Solver.SimpleBuilder as S
|
||||
import qualified SemMC.Architecture.Location as L
|
||||
|
||||
data QState arch t = QState { accumulatedStatements :: !(Seq.Seq Stmt)
|
||||
-- ^ The list of template haskell statements accumulated
|
||||
-- for this monadic context. At the end of the context, we
|
||||
-- can extract these and wrap them in a @do@ expression.
|
||||
, expressionCache :: !(M.Map (Some (S.Elt t)) Exp)
|
||||
-- ^ A cache of translations of SimpleBuilder terms into
|
||||
-- TH. The cached values are not the translated exprs;
|
||||
-- instead, they are names that are bound for those
|
||||
-- terms (via 'VarE')
|
||||
, locToReg :: forall tp . L.Location arch tp -> Q Exp
|
||||
}
|
||||
|
||||
emptyQState :: (forall tp . L.Location arch tp -> Q Exp) -> QState arch t
|
||||
emptyQState ltr = QState { accumulatedStatements = Seq.empty
|
||||
, expressionCache = M.empty
|
||||
, locToReg = ltr
|
||||
}
|
||||
|
||||
newtype MacawQ arch t a = MacawQ { unQ :: St.StateT (QState arch t) Q a }
|
||||
deriving (Functor,
|
||||
Applicative,
|
||||
Monad,
|
||||
St.MonadState (QState arch t))
|
||||
|
||||
runMacawQ :: (forall tp . L.Location arch tp -> Q Exp) -> MacawQ arch t () -> Q [Stmt]
|
||||
runMacawQ ltr act = (F.toList . accumulatedStatements) <$> St.execStateT (unQ act) (emptyQState ltr)
|
||||
|
||||
-- | Lift a TH computation (in the 'Q' monad) into the monad.
|
||||
liftQ :: Q a -> MacawQ arch t a
|
||||
liftQ q = MacawQ (lift q)
|
||||
|
||||
withLocToReg :: ((L.Location arch tp -> Q Exp) -> MacawQ arch t a) -> MacawQ arch t a
|
||||
withLocToReg k = do
|
||||
f <- St.gets locToReg
|
||||
k f
|
||||
|
||||
-- | Look up an 'S.Elt' in the cache
|
||||
lookupElt :: S.Elt t tp -> MacawQ arch t (Maybe Exp)
|
||||
lookupElt elt = do
|
||||
c <- St.gets expressionCache
|
||||
return (M.lookup (Some elt) c)
|
||||
|
||||
-- | Append a statement that doesn't need to bind a new name
|
||||
appendStmt :: ExpQ -> MacawQ arch t ()
|
||||
appendStmt eq = do
|
||||
e <- liftQ eq
|
||||
St.modify' $ \s -> s { accumulatedStatements = accumulatedStatements s Seq.|> NoBindS e }
|
||||
|
||||
-- | Bind a TH expression to a name (as a 'Stmt') and return the expression that
|
||||
-- refers to the bound value. For example, if you call
|
||||
--
|
||||
-- > bindExpr [| return (1 + 2) |]
|
||||
--
|
||||
-- The statement added to the state is
|
||||
--
|
||||
-- > newName <- expr
|
||||
--
|
||||
-- and the new name is returned.
|
||||
bindExpr :: S.Elt t tp -> ExpQ -> MacawQ arch t Exp
|
||||
bindExpr elt eq = do
|
||||
e <- liftQ eq
|
||||
n <- liftQ (newName "val")
|
||||
let res = VarE n
|
||||
St.modify' $ \s -> s { accumulatedStatements = accumulatedStatements s Seq.|> BindS (VarP n) e
|
||||
, expressionCache = M.insert (Some elt) res (expressionCache s)
|
||||
}
|
||||
return res
|
||||
62
macaw-semmc/src/Data/Macaw/SemMC/Translations.hs
Normal file
62
macaw-semmc/src/Data/Macaw/SemMC/Translations.hs
Normal file
@ -0,0 +1,62 @@
|
||||
{-# LANGUAGE DataKinds #-}
|
||||
{-# LANGUAGE FlexibleContexts #-}
|
||||
{-# LANGUAGE GADTs #-}
|
||||
{-# LANGUAGE TypeApplications #-}
|
||||
{-# LANGUAGE TypeOperators #-}
|
||||
module Data.Macaw.SemMC.Translations (
|
||||
bvconcat,
|
||||
bvselect
|
||||
) where
|
||||
|
||||
import GHC.TypeLits
|
||||
|
||||
import Data.Macaw.CFG
|
||||
import qualified Data.Macaw.Memory as MM
|
||||
import Data.Macaw.Types ( BVType )
|
||||
import Data.Parameterized.Classes
|
||||
import qualified Data.Parameterized.NatRepr as NR
|
||||
import qualified Lang.Crucible.BaseTypes as S
|
||||
|
||||
import Data.Macaw.SemMC.Generator
|
||||
|
||||
-- | The implementation of bitvector concatenation
|
||||
--
|
||||
-- We pull this out to reduce the amount of code generated by TH
|
||||
bvconcat :: (OrdF (ArchReg arch), MM.MemWidth (RegAddrWidth (ArchReg arch)))
|
||||
=> (1 <= v, (u+1) <= w, 1 <= u, 1 <= w, (u+v) ~ w)
|
||||
=> Value arch ids (BVType u)
|
||||
-> Value arch ids (BVType v)
|
||||
-> NR.NatRepr v
|
||||
-> NR.NatRepr u
|
||||
-> NR.NatRepr w
|
||||
-> Generator arch ids s (Expr arch ids (BVType w))
|
||||
bvconcat bv1Val bv2Val repV repU repW = do
|
||||
S.LeqProof <- return (S.leqAdd2 (S.leqRefl repU) (S.leqProof (S.knownNat @1) repV))
|
||||
pf1@S.LeqProof <- return (S.leqAdd2 (S.leqRefl repV) (S.leqProof (S.knownNat @1) repU))
|
||||
Refl <- return (S.plusComm repU repV)
|
||||
S.LeqProof <- return (S.leqTrans pf1 (S.leqRefl repW))
|
||||
bv1Ext <- addExpr (AppExpr (UExt bv1Val repW))
|
||||
bv2Ext <- addExpr (AppExpr (UExt bv2Val repW))
|
||||
bv1Shifter <- addExpr (ValueExpr (BVValue repW (NR.natValue repV)))
|
||||
bv1Shf <- addExpr (AppExpr (BVShl repW bv1Ext bv1Shifter))
|
||||
return $ AppExpr (BVOr repW bv1Shf bv2Ext)
|
||||
|
||||
-- | Select @n@ bits from a @w@ bit bitvector starting at index @i@
|
||||
--
|
||||
-- This code is factored out of the TH module to improve compilation times.
|
||||
bvselect :: (OrdF (ArchReg arch), MM.MemWidth (RegAddrWidth (ArchReg arch)))
|
||||
=> (1 <= w, 1 <= n, 1 <= i, (i+n) <= w)
|
||||
=> Value arch ids (BVType w)
|
||||
-> NR.NatRepr n
|
||||
-> NR.NatRepr i
|
||||
-> NR.NatRepr w
|
||||
-> Generator arch ids s (Expr arch ids (BVType n))
|
||||
bvselect bvVal repN repI repW = do
|
||||
Just S.LeqProof <- return (S.testLeq (repN `S.addNat` (NR.knownNat @1)) repW)
|
||||
pf1@S.LeqProof <- return $ S.leqAdd2 (S.leqRefl repI) (S.leqProof (NR.knownNat @1) repN)
|
||||
pf2@S.LeqProof <- return $ S.leqAdd (S.leqRefl (NR.knownNat @1)) repI
|
||||
Refl <- return (S.plusComm (NR.knownNat @1) repI)
|
||||
pf3@S.LeqProof <- return $ S.leqTrans pf2 pf1
|
||||
S.LeqProof <- return $ S.leqTrans pf3 (S.leqProof (repI `S.addNat` repN) repW)
|
||||
bvShf <- addExpr (AppExpr (BVShr repW bvVal (mkLit repW (NR.natValue repI))))
|
||||
return (AppExpr (Trunc bvShf repN))
|
||||
Loading…
Reference in New Issue
Block a user