Factor out the implementations of some of the TH translations

These operations generate a lot of code, so it is helpful to factor them out and
reduce the burden on the type checker.  Factoring these two definitions out cuts
the generated code nearly in half.

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
 

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))
+          let repV = $(natReprTH v)
-          pf1@S.LeqProof <- return $ S.leqAdd2 (S.leqRefl $(natReprTH v)) (S.leqProof (knownNat @1) $(natReprTH u))
+          let repU = $(natReprTH u)
-          Refl <- return $ S.plusComm $(natReprTH u) $(natReprTH v)
+          let repW = $(natReprTH w)
-          S.LeqProof <- return (S.leqTrans pf1 (S.leqRefl $(natReprTH w)))
+          bvconcat bv1Val bv2Val repV repU repW
-          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)
      |]
   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)
+              let repW = $(natReprTH w)
-              pf1@S.LeqProof <- return $ S.leqAdd2 (S.leqRefl $(natReprTH idx)) (S.leqProof (knownNat @1) $(natReprTH n))
+              let repN = $(natReprTH n)
-              pf2@S.LeqProof <- return $ S.leqAdd (S.leqRefl (knownNat @1)) $(natReprTH idx)
+              let repI = $(natReprTH idx)
-              Refl <- return $ S.plusComm (knownNat @1) $(natReprTH idx)
+              bvselect bvVal repN repI repW
-              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))
          |]
       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))
+          let repW = $(natReprTH w)
-          return $ AppExpr (M.BVAdd $(natReprTH w) bvComp (M.mkLit $(natReprTH w) 1))
+          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.