mirror of
https://github.com/GaloisInc/macaw.git
synced 2024-12-24 22:53:43 +03:00
work in progress TH translation
This commit is contained in:
Ben Selfridge
parent
d48f30f173
commit
ebe47b74fc
@ -57,6 +57,8 @@ import Data.Parameterized.NatRepr ( knownNat
|
||||
import Data.Macaw.PPC.Generator
|
||||
import Data.Macaw.PPC.PPCReg
|
||||
|
||||
-- run stack with --ghc-options=-ddump-splices
|
||||
|
||||
-- | A different parameterized pair wrapper; the one in Data.Parameterized.Map
|
||||
-- hides the @tp@ parameter under an existential, while we need the variant that
|
||||
-- exposes it.
|
||||
@ -71,7 +73,10 @@ data PairF a b tp = PairF (a tp) (b tp)
|
||||
--
|
||||
-- where each case in ${CASES} is defined by 'mkSemanticsCase'; each case
|
||||
-- matches one opcode.
|
||||
instructionMatcher :: (OrdF a, LF.LiftF a)
|
||||
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))
|
||||
-> Q Exp
|
||||
instructionMatcher formulas = do
|
||||
@ -86,7 +91,10 @@ instructionMatcher formulas = do
|
||||
-- > ADD4 -> ${BODY}
|
||||
--
|
||||
-- where the ${BODY} is generated by 'mkOperandListCase'
|
||||
mkSemanticsCase :: (LF.LiftF a)
|
||||
mkSemanticsCase :: (LF.LiftF a,
|
||||
L.Location arch ~ APPC.Location arch,
|
||||
1 <= APPC.ArchRegWidth arch,
|
||||
M.RegAddrWidth (PPCReg arch) ~ APPC.ArchRegWidth arch)
|
||||
=> Name
|
||||
-> Name
|
||||
-> Map.Pair (Witness c a) (PairF (ParameterizedFormula (Sym t) arch) (DT.CaptureInfo c a))
|
||||
@ -117,7 +125,15 @@ mkSemanticsCase ipVarName operandListVar (Map.Pair (Witness opc) (PairF semantic
|
||||
-- > -> ${BODY}
|
||||
--
|
||||
-- in an example with three general purpose register operands.
|
||||
mkOperandListCase :: Name -> Name -> a tp -> ParameterizedFormula (Sym t) arch tp -> DT.CaptureInfo c a tp -> Q Exp
|
||||
mkOperandListCase :: (L.Location arch ~ APPC.Location arch,
|
||||
1 <= APPC.ArchRegWidth arch,
|
||||
M.RegAddrWidth (PPCReg arch) ~ APPC.ArchRegWidth arch)
|
||||
=> 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)
|
||||
DT.genCase capInfo operandListVar body
|
||||
@ -134,13 +150,16 @@ mkOperandListCase ipVarName operandListVar opc semantics capInfo = do
|
||||
-- The two maps (locVars and opVars) are crucial for translating parameterized
|
||||
-- formulas into expressions.
|
||||
genCaseBody :: forall a sh t arch
|
||||
. Name
|
||||
. (L.Location arch ~ APPC.Location arch,
|
||||
1 <= APPC.ArchRegWidth arch,
|
||||
M.RegAddrWidth (PPCReg arch) ~ APPC.ArchRegWidth arch)
|
||||
=> Name
|
||||
-> a sh
|
||||
-> ParameterizedFormula (Sym t) arch sh
|
||||
-> SL.ShapedList (FreeParamF Name) sh
|
||||
-> Q Exp
|
||||
genCaseBody ipVarName opc semantics varNames =
|
||||
[| undefined $(tupE (map varE binders)) |]
|
||||
translateFormula semantics locVars opVars
|
||||
where
|
||||
binders = ipVarName : FC.toListFC unFreeParamF varNames
|
||||
|
||||
@ -186,7 +205,13 @@ collectOperandVars varNames ix (BV.BoundVar bv) m =
|
||||
-- all of the things we would need to for that).
|
||||
--
|
||||
-- The structure of the term produced is documented in 'instructionMatcher'
|
||||
genExecInstruction :: (A.Architecture arch, OrdF a, ShowF a, LF.LiftF a)
|
||||
genExecInstruction :: (A.Architecture arch,
|
||||
OrdF a,
|
||||
ShowF a,
|
||||
LF.LiftF a,
|
||||
L.Location arch ~ APPC.Location arch,
|
||||
1 <= APPC.ArchRegWidth arch,
|
||||
M.RegAddrWidth (PPCReg arch) ~ APPC.ArchRegWidth arch)
|
||||
=> proxy arch
|
||||
-> (forall sh . c sh C.:- BuildOperandList arch sh)
|
||||
-- ^ A constraint implication to let us extract/weaken the
|
||||
@ -244,9 +269,11 @@ addExpr expr = do
|
||||
assignment <- addAssignment (M.EvalApp app)
|
||||
return $ M.AssignedValue assignment
|
||||
|
||||
-- This function needs to be written.
|
||||
addExprTH :: Expr ppc ids tp -> Q Exp
|
||||
addExprTH expr = do
|
||||
undefined
|
||||
addExprTH expr = case expr of
|
||||
ValueExpr val -> [| undefined |]
|
||||
AppExpr app -> [| undefined |]
|
||||
|
||||
addElt :: S.Elt t ctp -> PPCGenerator ppc ids (M.Value ppc ids (FromCrucibleBaseType ctp))
|
||||
addElt elt = eltToExpr elt >>= addExpr
|
||||
@ -267,17 +294,138 @@ addElt' elt = case elt of
|
||||
natReprTH :: M.NatRepr w -> Q Exp
|
||||
natReprTH w = [| knownNat :: M.NatRepr $(litT (return $ NumTyLit (natValue w))) |]
|
||||
|
||||
translateFormula :: forall arch t sh .
|
||||
(L.Location arch ~ APPC.Location arch,
|
||||
1 <= APPC.ArchRegWidth arch,
|
||||
M.RegAddrWidth (PPCReg arch) ~ APPC.ArchRegWidth arch)
|
||||
=> ParameterizedFormula (Sym t) arch sh
|
||||
-> Map.MapF (SI.BoundVar (Sym t)) (L.Location arch)
|
||||
-> Map.MapF (SI.BoundVar (Sym t)) (FreeParamF Name)
|
||||
-> Q Exp
|
||||
translateFormula semantics locVars opVars = do
|
||||
let exps = map translateDefinition (Map.toList (pfDefs semantics))
|
||||
[| Just (sequence_ $(listE exps)) |]
|
||||
where translateDefinition :: Map.Pair (Parameter arch sh) (S.SymExpr (Sym t))
|
||||
-> Q Exp
|
||||
translateDefinition (Map.Pair param expr) = do
|
||||
case param of
|
||||
OperandParameter w idx -> [| undefined |]
|
||||
LiteralParameter loc -> do
|
||||
e <- addEltTH expr
|
||||
reg <- locToRegTH (Proxy @arch) loc
|
||||
[| do val <- $(return e)
|
||||
curPPCState . M.boundValue $(return reg) .= val
|
||||
-- case c of
|
||||
-- ValueExpr val -> curPPCState . M.boundValue $(return reg) .= val
|
||||
-- AppExpr app -> do
|
||||
-- assignment <- addAssignment (M.EvalApp app)
|
||||
-- curPPCState . M.boundValue $(return reg) .= M.AssignedValue assignment
|
||||
|]
|
||||
FunctionParameter str operand w -> [| undefined |]
|
||||
|
||||
addEltTH :: S.Elt t ctp -> Q Exp
|
||||
addEltTH elt = case elt of
|
||||
S.BVElt w val loc ->
|
||||
[| return (M.BVValue $(natReprTH w) $(lift val)) |]
|
||||
S.AppElt appElt -> do
|
||||
x <- newName "x"
|
||||
let app = S.appEltApp appElt
|
||||
appExpr <- crucAppToExprTH app
|
||||
[| do $(varP x) <- $(crucAppToExprTH (S.appEltApp appElt))
|
||||
addExpr $(varE x)
|
||||
|]
|
||||
[| $(crucAppToExprTH (S.appEltApp appElt)) >>= addExpr |]
|
||||
_ -> [| error "addEltTH" |]
|
||||
|
||||
crucAppToExprTH :: S.App (S.Elt t) ctp -> Q Exp
|
||||
crucAppToExprTH S.TrueBool = [| return $ ValueExpr (M.BoolValue True) |]
|
||||
crucAppToExprTH S.FalseBool = [| return $ ValueExpr (M.BoolValue False) |]
|
||||
crucAppToExprTH (S.NotBool bool) =
|
||||
[| AppExpr (M.NotApp <$> $(addEltTH bool)) |]
|
||||
crucAppToExprTH (S.AndBool bool1 bool2) =
|
||||
[| AppExpr (M.AndApp <$> $(addEltTH bool1) <*> $(addEltTH bool2)) |]
|
||||
crucAppToExprTH (S.XorBool bool1 bool2) =
|
||||
[| AppExpr (M.XorApp <$> $(addEltTH bool1) <*> $(addEltTH bool2)) |]
|
||||
crucAppToExprTH (S.IteBool test t f) =
|
||||
[| AppExpr (M.Mux M.BoolTypeRepr <$> $(addEltTH test) <*> $(addEltTH t) <*> $(addEltTH f)) |]
|
||||
crucAppToExprTH (S.BVIte w numBranches test t f) =
|
||||
[| AppExpr (M.Mux (M.BVTypeRepr $(natReprTH w)) <$> $(addEltTH test) <*> $(addEltTH t) <*> $(addEltTH f)) |]
|
||||
crucAppToExprTH (S.BVEq bv1 bv2) =
|
||||
[| AppExpr (M.Eq <$> $(addEltTH bv1) <*> $(addEltTH bv2)) |]
|
||||
crucAppToExprTH (S.BVSlt bv1 bv2) =
|
||||
[| AppExpr (M.BVSignedLt <$> $(addEltTH bv1) <*> $(addEltTH bv2)) |]
|
||||
crucAppToExprTH (S.BVUlt bv1 bv2) =
|
||||
[| AppExpr (M.BVUnsignedLt <$> $(addEltTH bv1) <*> $(addEltTH bv2)) |]
|
||||
crucAppToExprTH (S.BVConcat w bv1 bv2) = do
|
||||
[| error "BVConcat" |]
|
||||
-- [| AppExpr (M.BVUnsignedLt <$> $(addEltTH bv1) <*> $(addEltTH bv2)) |]
|
||||
-- let u = S.bvWidth bv1
|
||||
-- v = S.bvWidth bv2
|
||||
-- bv1Val <- addElt bv1
|
||||
-- bv2Val <- addElt bv2
|
||||
-- S.LeqProof <- return $ S.leqAdd2 (S.leqRefl u) (S.leqProof (knownNat @1) v)
|
||||
-- S.LeqProof <- return $ S.leqAdd2 (S.leqRefl v) (S.leqProof (knownNat @1) u)
|
||||
-- Refl <- return $ S.plusComm u v
|
||||
-- bv1Ext <- addExpr (AppExpr (M.UExt bv1Val w)) ---(u `addNat` v)))
|
||||
-- bv2Ext <- addExpr (AppExpr (M.UExt bv2Val w))
|
||||
-- bv1Shifter <- addExpr (ValueExpr (M.BVValue w (natValue v)))
|
||||
-- bv1Shf <- addExpr (AppExpr (M.BVShl w bv1Ext bv1Shifter))
|
||||
-- return $ M.BVOr w bv1Shf bv2Ext
|
||||
crucAppToExprTH (S.BVSelect idx n bv) = do
|
||||
[| error "BVSelect" |]
|
||||
-- let w = S.bvWidth bv
|
||||
-- bvVal <- addElt bv
|
||||
-- case natValue n + 1 <= natValue w of
|
||||
-- True -> do
|
||||
-- -- Is there a way to just "know" that n + 1 <= w?
|
||||
-- Just S.LeqProof <- return $ S.testLeq (n `addNat` (knownNat @1)) w
|
||||
-- pf1@S.LeqProof <- return $ S.leqAdd2 (S.leqRefl idx) (S.leqProof (knownNat @1) n)
|
||||
-- pf2@S.LeqProof <- return $ S.leqAdd (S.leqRefl (knownNat @1)) idx
|
||||
-- Refl <- return $ S.plusComm (knownNat @1) idx
|
||||
-- pf3@S.LeqProof <- return $ S.leqTrans pf2 pf1
|
||||
-- S.LeqProof <- return $ S.leqTrans pf3 (S.leqProof (idx `addNat` n) w)
|
||||
-- bvShf <- addExpr (AppExpr (M.BVShr w bvVal (M.mkLit w (natValue idx))))
|
||||
-- return $ AppExpr (M.Trunc bvShf n)
|
||||
-- False -> do
|
||||
-- -- Is there a way to just "know" that n = w?
|
||||
-- Just Refl <- return $ testEquality n w
|
||||
-- return $ ValueExpr bvVal
|
||||
crucAppToExprTH (S.BVNeg w bv) = do
|
||||
[| error "BVNeg" |]
|
||||
-- bvVal <- addElt bv
|
||||
-- bvComp <- addExpr (AppExpr (M.BVComplement w bvVal))
|
||||
-- return $ AppExpr (M.BVAdd w bvComp (M.mkLit w 1))
|
||||
crucAppToExprTH (S.BVTestBit idx bv) = do
|
||||
-- Note: below is untested, could be wrong.
|
||||
[| do let bitExp = ValueExpr (M.BVValue $(natReprTH (S.bvWidth bv)) $(lift idx))
|
||||
bitExpVal <- addExpr bitExp
|
||||
AppExpr <$> (M.BVTestBit <$> bitExpVal <*> $(addEltTH bv)) |]
|
||||
crucAppToExprTH (S.BVAdd w bv1 bv2) =
|
||||
[| AppExpr <$> (M.BVAdd $(natReprTH w) <$> $(addEltTH bv1) <*> $(addEltTH bv2)) |]
|
||||
crucAppToExprTH (S.BVMul w bv1 bv2) =
|
||||
[| AppExpr <$> (M.BVMul $(natReprTH w) <$> $(addEltTH bv1) <*> $(addEltTH bv2)) |]
|
||||
crucAppToExprTH (S.BVShl w bv1 bv2) =
|
||||
[| AppExpr <$> (M.BVShl $(natReprTH w) <$> $(addEltTH bv1) <*> $(addEltTH bv2)) |]
|
||||
crucAppToExprTH (S.BVLshr w bv1 bv2) =
|
||||
[| AppExpr <$> (M.BVShr $(natReprTH w) <$> $(addEltTH bv1) <*> $(addEltTH bv2)) |]
|
||||
crucAppToExprTH (S.BVAshr w bv1 bv2) =
|
||||
[| AppExpr <$> (M.BVSar $(natReprTH w) <$> $(addEltTH bv1) <*> $(addEltTH bv2)) |]
|
||||
crucAppToExprTH (S.BVZext w bv) =
|
||||
-- [| AppExpr <$> (M.UExt <$> $(addEltTH bv) <*> (pure $(natReprTH w))) |]
|
||||
[| undefined |]
|
||||
-- [| do val <- $(addEltTH bv)
|
||||
-- return $ AppExpr (M.UExt val $(natReprTH w)) |]
|
||||
crucAppToExprTH (S.BVSext w bv) =
|
||||
-- [| AppExpr <$> (M.SExt <$> $(addEltTH bv) <*> (pure $(natReprTH w))) |]
|
||||
[| undefined |]
|
||||
crucAppToExprTH (S.BVTrunc w bv) =
|
||||
[| AppExpr <$> (M.Trunc <$> $(addEltTH bv) <*> (pure $(natReprTH w))) |]
|
||||
crucAppToExprTH (S.BVBitNot w bv) =
|
||||
[| AppExpr <$> (M.BVComplement <$> $(addEltTH bv) <*> (pure $(natReprTH w))) |]
|
||||
crucAppToExprTH (S.BVBitAnd w bv1 bv2) =
|
||||
[| AppExpr <$> (M.BVAnd $(natReprTH w) <$> $(addEltTH bv1) <*> $(addEltTH bv2)) |]
|
||||
crucAppToExprTH (S.BVBitOr w bv1 bv2) =
|
||||
[| AppExpr <$> (M.BVOr $(natReprTH w) <$> $(addEltTH bv1) <*> $(addEltTH bv2)) |]
|
||||
crucAppToExprTH (S.BVBitXor w bv1 bv2) =
|
||||
[| AppExpr <$> (M.BVXor $(natReprTH w) <$> $(addEltTH bv1) <*> $(addEltTH bv2)) |]
|
||||
|
||||
|
||||
|
||||
crucAppToExpr :: S.App (S.Elt t) ctp -> PPCGenerator ppc ids (Expr ppc ids (FromCrucibleBaseType ctp))
|
||||
crucAppToExpr S.TrueBool = return $ ValueExpr (M.BoolValue True)
|
||||
@ -362,129 +510,6 @@ crucAppToExpr (S.BVBitXor repr bv1 bv2) = AppExpr <$> do
|
||||
M.BVXor <$> pure repr <*> addElt bv1 <*> addElt bv2
|
||||
crucAppToExpr _ = error "crucAppToExpr: unimplemented crucible operation"
|
||||
|
||||
crucAppToExprTH :: S.App (S.Elt t) ctp -> Q Exp
|
||||
crucAppToExprTH S.TrueBool = [| return $ ValueExpr (M.BoolValue True) |]
|
||||
crucAppToExprTH S.FalseBool = [| return $ ValueExpr (M.BoolValue False) |]
|
||||
crucAppToExprTH (S.NotBool bool) = do
|
||||
boolExp <- addEltTH bool
|
||||
[| AppExpr (M.NotApp $(return boolExp)) |]
|
||||
crucAppToExprTH (S.AndBool bool1 bool2) = do
|
||||
bool1Exp <- addEltTH bool1
|
||||
bool2Exp <- addEltTH bool2
|
||||
[| AppExpr (M.AndApp $(return bool1Exp) $(return bool2Exp)) |]
|
||||
crucAppToExprTH (S.XorBool bool1 bool2) = do
|
||||
bool1Exp <- addEltTH bool1
|
||||
bool2Exp <- addEltTH bool2
|
||||
[| AppExpr (M.AndApp $(return bool1Exp) $(return bool2Exp)) |]
|
||||
crucAppToExprTH (S.IteBool test t f) = do
|
||||
testExp <- addEltTH test
|
||||
tExp <- addEltTH t
|
||||
fExp <- addEltTH f
|
||||
[| AppExpr (M.Mux M.BoolTypeRepr $(return testExp) $(return tExp) $(return fExp)) |]
|
||||
crucAppToExprTH (S.BVIte w numBranches test t f) = do
|
||||
testExp <- addEltTH test
|
||||
tExp <- addEltTH t
|
||||
fExp <- addEltTH f
|
||||
[| AppExpr (M.Mux (M.BVTypeRepr $(natReprTH w)) $(return testExp) $(return tExp) $(return fExp)) |]
|
||||
crucAppToExprTH (S.BVEq bv1 bv2) = do
|
||||
bv1Exp <- addEltTH bv1
|
||||
bv2Exp <- addEltTH bv2
|
||||
[| AppExpr (M.Eq $(return bv1Exp) $(return bv2Exp)) |]
|
||||
crucAppToExprTH (S.BVSlt bv1 bv2) = do
|
||||
bv1Exp <- addEltTH bv1
|
||||
bv2Exp <- addEltTH bv2
|
||||
[| AppExpr (M.BVSignedLt $(return bv1Exp) $(return bv2Exp)) |]
|
||||
crucAppToExprTH (S.BVUlt bv1 bv2) = do
|
||||
bv1Exp <- addEltTH bv1
|
||||
bv2Exp <- addEltTH bv2
|
||||
[| AppExpr (M.BVUnsignedLt $(return bv1Exp) $(return bv2Exp)) |]
|
||||
crucAppToExprTH (S.BVConcat w bv1 bv2) = do
|
||||
undefined
|
||||
-- let u = S.bvWidth bv1
|
||||
-- v = S.bvWidth bv2
|
||||
-- bv1Val <- addElt bv1
|
||||
-- bv2Val <- addElt bv2
|
||||
-- S.LeqProof <- return $ S.leqAdd2 (S.leqRefl u) (S.leqProof (knownNat @1) v)
|
||||
-- S.LeqProof <- return $ S.leqAdd2 (S.leqRefl v) (S.leqProof (knownNat @1) u)
|
||||
-- Refl <- return $ S.plusComm u v
|
||||
-- bv1Ext <- addExpr (AppExpr (M.UExt bv1Val w)) ---(u `addNat` v)))
|
||||
-- bv2Ext <- addExpr (AppExpr (M.UExt bv2Val w))
|
||||
-- bv1Shifter <- addExpr (ValueExpr (M.BVValue w (natValue v)))
|
||||
-- bv1Shf <- addExpr (AppExpr (M.BVShl w bv1Ext bv1Shifter))
|
||||
-- return $ M.BVOr w bv1Shf bv2Ext
|
||||
crucAppToExprTH (S.BVSelect idx n bv) = do
|
||||
undefined
|
||||
-- let w = S.bvWidth bv
|
||||
-- bvVal <- addElt bv
|
||||
-- case natValue n + 1 <= natValue w of
|
||||
-- True -> do
|
||||
-- -- Is there a way to just "know" that n + 1 <= w?
|
||||
-- Just S.LeqProof <- return $ S.testLeq (n `addNat` (knownNat @1)) w
|
||||
-- pf1@S.LeqProof <- return $ S.leqAdd2 (S.leqRefl idx) (S.leqProof (knownNat @1) n)
|
||||
-- pf2@S.LeqProof <- return $ S.leqAdd (S.leqRefl (knownNat @1)) idx
|
||||
-- Refl <- return $ S.plusComm (knownNat @1) idx
|
||||
-- pf3@S.LeqProof <- return $ S.leqTrans pf2 pf1
|
||||
-- S.LeqProof <- return $ S.leqTrans pf3 (S.leqProof (idx `addNat` n) w)
|
||||
-- bvShf <- addExpr (AppExpr (M.BVShr w bvVal (M.mkLit w (natValue idx))))
|
||||
-- return $ AppExpr (M.Trunc bvShf n)
|
||||
-- False -> do
|
||||
-- -- Is there a way to just "know" that n = w?
|
||||
-- Just Refl <- return $ testEquality n w
|
||||
-- return $ ValueExpr bvVal
|
||||
crucAppToExprTH (S.BVNeg w bv) = do
|
||||
undefined
|
||||
-- bvVal <- addElt bv
|
||||
-- bvComp <- addExpr (AppExpr (M.BVComplement w bvVal))
|
||||
-- return $ AppExpr (M.BVAdd w bvComp (M.mkLit w 1))
|
||||
crucAppToExprTH (S.BVTestBit idx bv) = do
|
||||
bitExp <- addExprTH (ValueExpr (M.BVValue (S.bvWidth bv) (fromIntegral idx)))
|
||||
bvExp <- addEltTH bv
|
||||
[| AppExpr (M.BVTestBit $(return bitExp) $(return bvExp)) |]
|
||||
crucAppToExprTH (S.BVAdd w bv1 bv2) = do
|
||||
bv1Exp <- addEltTH bv1
|
||||
bv2Exp <- addEltTH bv2
|
||||
[| AppExpr (M.BVAdd $(natReprTH w) $(return bv1Exp) $(return bv2Exp)) |]
|
||||
crucAppToExprTH (S.BVMul w bv1 bv2) = do
|
||||
bv1Exp <- addEltTH bv1
|
||||
bv2Exp <- addEltTH bv2
|
||||
[| AppExpr (M.BVMul $(natReprTH w) $(return bv1Exp) $(return bv2Exp)) |]
|
||||
crucAppToExprTH (S.BVShl w bv1 bv2) = do
|
||||
bv1Exp <- addEltTH bv1
|
||||
bv2Exp <- addEltTH bv2
|
||||
[| AppExpr (M.BVShl $(natReprTH w) $(return bv1Exp) $(return bv2Exp)) |]
|
||||
crucAppToExprTH (S.BVLshr w bv1 bv2) = do
|
||||
bv1Exp <- addEltTH bv1
|
||||
bv2Exp <- addEltTH bv2
|
||||
[| AppExpr (M.BVShr $(natReprTH w) $(return bv1Exp) $(return bv2Exp)) |]
|
||||
crucAppToExprTH (S.BVAshr w bv1 bv2) = do
|
||||
bv1Exp <- addEltTH bv1
|
||||
bv2Exp <- addEltTH bv2
|
||||
[| AppExpr (M.BVSar $(natReprTH w) $(return bv1Exp) $(return bv2Exp)) |]
|
||||
crucAppToExprTH (S.BVZext w bv) = do
|
||||
bvExp <- addEltTH bv
|
||||
[| AppExpr (M.UExt $(return bvExp) $(natReprTH w)) |]
|
||||
crucAppToExprTH (S.BVSext w bv) = do
|
||||
bvExp <- addEltTH bv
|
||||
[| AppExpr (M.SExt $(return bvExp) $(natReprTH w)) |]
|
||||
crucAppToExprTH (S.BVTrunc w bv) = do
|
||||
bvExp <- addEltTH bv
|
||||
[| AppExpr (M.Trunc $(return bvExp) $(natReprTH w)) |]
|
||||
crucAppToExprTH (S.BVBitNot w bv) = do
|
||||
bvExp <- addEltTH bv
|
||||
[| AppExpr (M.BVComplement $(return bvExp) $(natReprTH w)) |]
|
||||
crucAppToExprTH (S.BVBitAnd w bv1 bv2) = do
|
||||
bv1Exp <- addEltTH bv1
|
||||
bv2Exp <- addEltTH bv2
|
||||
[| AppExpr (M.BVAnd $(natReprTH w) $(return bv1Exp) $(return bv2Exp)) |]
|
||||
crucAppToExprTH (S.BVBitOr w bv1 bv2) = do
|
||||
bv1Exp <- addEltTH bv1
|
||||
bv2Exp <- addEltTH bv2
|
||||
[| AppExpr (M.BVOr $(natReprTH w) $(return bv1Exp) $(return bv2Exp)) |]
|
||||
crucAppToExprTH (S.BVBitXor w bv1 bv2) = do
|
||||
bv1Exp <- addEltTH bv1
|
||||
bv2Exp <- addEltTH bv2
|
||||
[| AppExpr (M.BVXor $(natReprTH w) $(return bv1Exp) $(return bv2Exp)) |]
|
||||
|
||||
|
||||
locToReg :: (1 <= APPC.ArchRegWidth ppc,
|
||||
M.RegAddrWidth (PPCReg ppc) ~ APPC.ArchRegWidth ppc)
|
||||
@ -498,6 +523,19 @@ locToReg _ APPC.LocCTR = PPC_CTR
|
||||
locToReg _ APPC.LocCR = PPC_CR
|
||||
-- fill the rest out later
|
||||
|
||||
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.LocIP = [| PPC_IP |]
|
||||
locToRegTH _ APPC.LocLNK = [| PPC_LNK |]
|
||||
locToRegTH _ APPC.LocCTR = [| PPC_CTR |]
|
||||
locToRegTH _ APPC.LocCR = [| PPC_CR |]
|
||||
locToRegTH _ _ = [| undefined |]
|
||||
-- fill the rest out later
|
||||
|
||||
-- | Given a location to modify and a crucible formula, construct a PPCGenerator that
|
||||
-- will modify the location by the function encoded in the formula.
|
||||
interpretFormula :: forall tp ppc t ctp s .
|
||||
|
||||
Loading…
Reference in New Issue
Block a user