diff --git a/macaw-ppc/src/Data/Macaw/PPC/Semantics/TH.hs b/macaw-ppc/src/Data/Macaw/PPC/Semantics/TH.hs index 13793dd6..a88c9f37 100644 --- a/macaw-ppc/src/Data/Macaw/PPC/Semantics/TH.hs +++ b/macaw-ppc/src/Data/Macaw/PPC/Semantics/TH.hs @@ -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 .