diff --git a/macaw-ppc/src/Data/Macaw/PPC/Generator.hs b/macaw-ppc/src/Data/Macaw/PPC/Generator.hs index e38bd117..b3063fe7 100644 --- a/macaw-ppc/src/Data/Macaw/PPC/Generator.hs +++ b/macaw-ppc/src/Data/Macaw/PPC/Generator.hs @@ -7,6 +7,7 @@ {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE StandaloneDeriving #-} +{-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-} module Data.Macaw.PPC.Generator ( @@ -21,6 +22,7 @@ module Data.Macaw.PPC.Generator ( Expr(..), BlockSeq(..), PreBlock(..), + -- * Generator actions addStmt, addAssignment, getReg, @@ -29,6 +31,9 @@ module Data.Macaw.PPC.Generator ( finishBlock, finishBlock', finishWithTerminator, + addExpr, + bvconcat, + bvselect, -- * Lenses blockState, curPPCState, @@ -57,10 +62,13 @@ import Data.Word (Word64) import Data.Macaw.CFG import Data.Macaw.CFG.Block +import Data.Macaw.Types ( BVType ) import qualified Data.Macaw.Memory as MM +import Data.Parameterized.Classes import qualified Data.Parameterized.Map as MapF 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 @@ -171,6 +179,57 @@ 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 + +-- | 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) + +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 -> do + assignment <- addAssignment (EvalApp app) + return $ AssignedValue assignment + + ------------------------------------------------------------------------ -- PPCGenerator diff --git a/macaw-ppc/src/Data/Macaw/PPC/Semantics/TH.hs b/macaw-ppc/src/Data/Macaw/PPC/Semantics/TH.hs index 1590a97e..df0c2e6a 100644 --- a/macaw-ppc/src/Data/Macaw/PPC/Semantics/TH.hs +++ b/macaw-ppc/src/Data/Macaw/PPC/Semantics/TH.hs @@ -59,7 +59,6 @@ import qualified Data.Macaw.Memory as M import qualified Data.Macaw.Types as M import Data.Parameterized.NatRepr ( knownNat - , addNat , natValue ) @@ -279,16 +278,6 @@ genExecInstruction _ impl semantics captureInfo = do -- SemMC.Formula: instantiateFormula --- Add an expression in the PPCGenerator monad. This returns a Macaw value --- corresponding to the added expression. -addExpr :: M.ArchConstraints ppc => Expr ppc ids tp -> PPCGenerator ppc ids s (M.Value ppc ids tp) -addExpr expr = do - case expr of - ValueExpr val -> return val - AppExpr app -> do - assignment <- addAssignment (M.EvalApp app) - return $ M.AssignedValue assignment - natReprTH :: M.NatRepr w -> Q Exp natReprTH w = [| knownNat :: M.NatRepr $(litT (numTyLit (natValue w))) |] @@ -678,30 +667,20 @@ crucAppToExprTH elt interps = case elt of v = S.bvWidth bv2 [| do bv1Val <- $(addEltTH interps bv1) bv2Val <- $(addEltTH interps bv2) - S.LeqProof <- return $ S.leqAdd2 (S.leqRefl $(natReprTH u)) (S.leqProof (knownNat @1) $(natReprTH v)) - pf1@S.LeqProof <- return $ S.leqAdd2 (S.leqRefl $(natReprTH v)) (S.leqProof (knownNat @1) $(natReprTH u)) - Refl <- return $ S.plusComm $(natReprTH u) $(natReprTH v) - S.LeqProof <- return (S.leqTrans pf1 (S.leqRefl $(natReprTH w))) - bv1Ext <- addExpr (AppExpr (M.UExt bv1Val $(natReprTH w))) - bv2Ext <- addExpr (AppExpr (M.UExt bv2Val $(natReprTH w))) - bv1Shifter <- addExpr (ValueExpr (M.BVValue $(natReprTH w) (natValue $(natReprTH v)))) - bv1Shf <- addExpr (AppExpr (M.BVShl $(natReprTH w) bv1Ext bv1Shifter)) - return $ AppExpr (M.BVOr $(natReprTH w) bv1Shf bv2Ext) + let repV = $(natReprTH v) + let repU = $(natReprTH u) + let repW = $(natReprTH w) + bvconcat bv1Val bv2Val repV repU repW |] S.BVSelect idx n bv -> do let w = S.bvWidth bv case natValue n + 1 <= natValue w of True -> [| do bvVal <- $(addEltTH interps bv) - Just S.LeqProof <- return $ S.testLeq ($(natReprTH n) `addNat` (knownNat @1)) $(natReprTH w) - pf1@S.LeqProof <- return $ S.leqAdd2 (S.leqRefl $(natReprTH idx)) (S.leqProof (knownNat @1) $(natReprTH n)) - pf2@S.LeqProof <- return $ S.leqAdd (S.leqRefl (knownNat @1)) $(natReprTH idx) - Refl <- return $ S.plusComm (knownNat @1) $(natReprTH idx) - pf3@S.LeqProof <- return $ S.leqTrans pf2 pf1 - S.LeqProof <- return $ S.leqTrans pf3 (S.leqProof ($(natReprTH idx) `addNat` $(natReprTH n)) $(natReprTH w)) - bvShf <- addExpr (AppExpr (M.BVShr $(natReprTH w) bvVal (M.mkLit $(natReprTH w) (natValue $(natReprTH idx))))) - -- return $ ValueExpr (M.mkLit $(natReprTH n) 1) - return $ AppExpr (M.Trunc bvShf $(natReprTH n)) + let repW = $(natReprTH w) + let repN = $(natReprTH n) + let repI = $(natReprTH idx) + bvselect bvVal repN repI repW |] False -> [| do Just Refl <- return $ testEquality $(natReprTH n) $(natReprTH w) return $ ValueExpr bvVal @@ -709,8 +688,9 @@ crucAppToExprTH elt interps = case elt of S.BVNeg w bv -> do -- Note: This is still untested [| do bvVal <- $(addEltTH interps bv) - bvComp <- addExpr (AppExpr (M.BVComplement $(natReprTH w) bvVal)) - return $ AppExpr (M.BVAdd $(natReprTH w) bvComp (M.mkLit $(natReprTH w) 1)) + let repW = $(natReprTH w) + bvComp <- addExpr (AppExpr (M.BVComplement repW bvVal)) + return $ AppExpr (M.BVAdd repW bvComp (M.mkLit repW 1)) |] S.BVTestBit idx bv -> -- Note: below is untested, could be wrong.