From 3da4bc8916438654ba3bdf92c5492b0efe6455eb Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Wed, 4 Dec 2024 05:53:10 -0500 Subject: [PATCH] `macaw-riscv-symbolic`: Indexes for registers Like #445, but for RISC-V. --- .../macaw-riscv-symbolic.cabal | 1 + .../src/Data/Macaw/RISCV/Symbolic.hs | 103 +- .../src/Data/Macaw/RISCV/Symbolic/Regs.hs | 1044 +++++++++++++++++ macaw-riscv-symbolic/tests/Main.hs | 182 ++- 4 files changed, 1229 insertions(+), 101 deletions(-) create mode 100644 macaw-riscv-symbolic/src/Data/Macaw/RISCV/Symbolic/Regs.hs diff --git a/macaw-riscv-symbolic/macaw-riscv-symbolic.cabal b/macaw-riscv-symbolic/macaw-riscv-symbolic.cabal index 8c2a149a..82097630 100644 --- a/macaw-riscv-symbolic/macaw-riscv-symbolic.cabal +++ b/macaw-riscv-symbolic/macaw-riscv-symbolic.cabal @@ -106,6 +106,7 @@ library exposed-modules: Data.Macaw.RISCV.Symbolic + Data.Macaw.RISCV.Symbolic.Regs other-modules: Data.Macaw.RISCV.Symbolic.AtomWrapper Data.Macaw.RISCV.Symbolic.Functions diff --git a/macaw-riscv-symbolic/src/Data/Macaw/RISCV/Symbolic.hs b/macaw-riscv-symbolic/src/Data/Macaw/RISCV/Symbolic.hs index 6c1a9b97..a1e9c651 100644 --- a/macaw-riscv-symbolic/src/Data/Macaw/RISCV/Symbolic.hs +++ b/macaw-riscv-symbolic/src/Data/Macaw/RISCV/Symbolic.hs @@ -13,20 +13,16 @@ module Data.Macaw.RISCV.Symbolic ( riscvMacawSymbolicFns , riscvMacawEvalFn - , lookupReg - , updateReg + , Regs.lookupReg + , Regs.updateReg ) where -import Control.Lens ((%~), (&)) -import qualified Control.Monad.Catch as X import Control.Monad.IO.Class (liftIO) import Data.Functor (void) import qualified Data.Kind as DK import qualified Data.Functor.Identity as I -import qualified Data.Parameterized.Map as MapF import qualified Data.Parameterized.Classes as PC import qualified Data.Parameterized.Context as Ctx -import Data.Parameterized.Some (Some(..)) import qualified Data.Parameterized.TraversableF as TF import qualified Data.Parameterized.TraversableFC as FC import Data.Typeable (Typeable) @@ -43,9 +39,6 @@ import qualified Lang.Crucible.LLVM.MemModel as LCLM -- grift import qualified GRIFT.Types as G --- what4 -import qualified What4.Symbol as WS - -- macaw-base import qualified Data.Macaw.CFG as MC import qualified Data.Macaw.Types as MT @@ -61,7 +54,7 @@ import qualified Data.Macaw.Symbolic.Backend as MSB import qualified Data.Macaw.RISCV.Symbolic.AtomWrapper as RA import qualified Data.Macaw.RISCV.Symbolic.Functions as RF import qualified Data.Macaw.RISCV.Symbolic.Panic as RP -import qualified Data.Macaw.RISCV.Symbolic.Repeat as RR +import qualified Data.Macaw.RISCV.Symbolic.Regs as Regs riscvMacawSymbolicFns :: forall rv @@ -70,27 +63,14 @@ riscvMacawSymbolicFns :: riscvMacawSymbolicFns = MSB.MacawSymbolicArchFunctions { MSB.crucGenArchConstraints = \x -> x - , MSB.crucGenArchRegName = riscvRegName - , MSB.crucGenRegAssignment = riscvRegAssignment - , MSB.crucGenRegStructType = riscvRegStructType (PC.knownRepr :: G.RVRepr rv) + , MSB.crucGenArchRegName = Regs.riscvRegName + , MSB.crucGenRegAssignment = Regs.riscvRegAssignment + , MSB.crucGenRegStructType = Regs.riscvRegStructType (PC.knownRepr :: G.RVRepr rv) , MSB.crucGenArchFn = riscvGenFn , MSB.crucGenArchStmt = riscvGenStmt , MSB.crucGenArchTermStmt = riscvGenTermStmt } -type instance MS.ArchRegContext (MR.RISCV rv) = - (Ctx.EmptyCtx Ctx.::> MT.BVType (G.RVWidth rv) -- PC - Ctx.<+> RR.CtxRepeat 31 (MT.BVType (G.RVWidth rv)) -- GPR regs. We use 31 instead of 32 - -- because we exclude x0, which is - -- hardwired to the constant 0. - Ctx.<+> RR.CtxRepeat 32 (MT.BVType (G.RVFloatWidth rv)) -- FPR regs - Ctx.<+> RR.CtxRepeat 23 (MT.BVType (G.RVWidth rv)) -- CSR regs. Although there is a - -- theoretical maximum of 4096 of - -- these registers, `grift` only - -- supports 23 of them in practice. - Ctx.<+> (Ctx.EmptyCtx Ctx.::> MT.BVType 2 -- PrivLevel - Ctx.::> MT.BoolType)) -- EXC - riscvMacawEvalFn :: RF.SymFuns sym -> MS.MacawArchStmtExtensionOverride (MR.RISCV rv) -> MS.MacawArchEvalFn p sym mem (MR.RISCV rv) @@ -120,98 +100,31 @@ instance (MS.IsMemoryModel mem, G.KnownRV rv, MR.RISCVConstraints rv, Typeable r , MS.updateReg = archUpdateReg } -riscvRegName :: MR.RISCVReg rv tp -> WS.SolverSymbol -riscvRegName r = WS.systemSymbol ("r!" ++ show (MC.prettyF r)) - --- Note that `repeatAssign` starts indexing from 0, but we want to exclude --- `GPR 0` (i.e., x0), as this is always hardwired to the constant 0. As such, --- we offset all of the indexes by one using (+ 1). -gprRegs :: Ctx.Assignment (MR.RISCVReg rv) (RR.CtxRepeat 31 (MT.BVType (G.RVWidth rv))) -gprRegs = RR.repeatAssign (MR.GPR . fromIntegral . (+ 1)) - -fprRegs :: Ctx.Assignment (MR.RISCVReg rv) (RR.CtxRepeat 32 (MT.BVType (G.RVFloatWidth rv))) -fprRegs = RR.repeatAssign (MR.FPR . fromIntegral) - --- | The RISC-V control/status registers that are directly supported by Macaw. -csrRegs :: Ctx.Assignment (MR.RISCVReg rv) (RR.CtxRepeat 23 (MT.BVType (G.RVWidth rv))) -csrRegs = RR.repeatAssign (MR.CSR . toEnum) - --- | This contains an assignment that stores the register associated with each index in the --- RISC-V register structure. -riscvRegAssignment :: Ctx.Assignment (MR.RISCVReg rv) (MS.ArchRegContext (MR.RISCV rv)) -riscvRegAssignment = - Ctx.Empty Ctx.:> MR.PC - Ctx.<++> gprRegs - Ctx.<++> fprRegs - Ctx.<++> csrRegs - Ctx.<++> (Ctx.Empty Ctx.:> MR.PrivLevel Ctx.:> MR.EXC) - -riscvRegStructType :: - forall rv - . G.KnownRV rv - => G.RVRepr rv - -> C.TypeRepr (MSB.ArchRegStruct (MR.RISCV rv)) -riscvRegStructType _rv = - C.StructRepr $ MS.typeCtxToCrucible $ FC.fmapFC MT.typeRepr $ riscvRegAssignment @rv - -regIndexMap :: forall rv - . G.KnownRV rv - => MSB.RegIndexMap (MR.RISCV rv) -regIndexMap = MSB.mkRegIndexMap assgn sz - where - assgn = riscvRegAssignment @rv - sz = Ctx.size $ MS.typeCtxToCrucible $ FC.fmapFC MT.typeRepr assgn - -lookupReg :: forall rv m f tp - . (G.KnownRV rv, Typeable rv, X.MonadThrow m) - => MR.RISCVReg rv tp - -> Ctx.Assignment f (MS.MacawCrucibleRegTypes (MR.RISCV rv)) - -> m (f (MS.ToCrucibleType tp)) -lookupReg r asgn = - case MapF.lookup r regIndexMap of - Nothing -> X.throwM (MissingRegisterInState (Some r)) - Just pair -> return (asgn Ctx.! MSB.crucibleIndex pair) - archLookupReg :: (G.KnownRV rv, Typeable rv) => C.RegEntry sym (MS.ArchRegStruct (MR.RISCV rv)) -> MR.RISCVReg rv tp -> C.RegEntry sym (MS.ToCrucibleType tp) archLookupReg regEntry reg = - case lookupReg reg (C.regValue regEntry) of + case Regs.lookupReg reg (C.regValue regEntry) of Just (C.RV val) -> C.RegEntry (MS.typeToCrucible $ MT.typeRepr reg) val Nothing -> RP.panic RP.RISCV "archLookupReg" ["unexpected register: " ++ show (MC.prettyF reg)] -updateReg :: forall rv m f tp - . (G.KnownRV rv, Typeable rv, X.MonadThrow m) - => MR.RISCVReg rv tp - -> (f (MS.ToCrucibleType tp) -> f (MS.ToCrucibleType tp)) - -> Ctx.Assignment f (MS.MacawCrucibleRegTypes (MR.RISCV rv)) - -> m (Ctx.Assignment f (MS.MacawCrucibleRegTypes (MR.RISCV rv))) -updateReg r upd asgn = do - case MapF.lookup r regIndexMap of - Nothing -> X.throwM (MissingRegisterInState (Some r)) - Just pair -> return (asgn & MapF.ixF (MSB.crucibleIndex pair) %~ upd) - archUpdateReg :: (G.KnownRV rv, Typeable rv) => C.RegEntry sym (MS.ArchRegStruct (MR.RISCV rv)) -> MR.RISCVReg rv tp -> C.RegValue sym (MS.ToCrucibleType tp) -> C.RegEntry sym (MS.ArchRegStruct (MR.RISCV rv)) archUpdateReg regEntry reg val = - case updateReg reg (const $ C.RV val) (C.regValue regEntry) of + case Regs.updateReg reg (const $ C.RV val) (C.regValue regEntry) of Just r -> regEntry { C.regValue = r } Nothing -> RP.panic RP.RISCV "archUpdateReg" ["unexpected register: " ++ show (MC.prettyF reg)] -newtype RISCVSymbolicException rv = MissingRegisterInState (Some (MR.RISCVReg rv)) - deriving Show -instance Typeable rv => X.Exception (RISCVSymbolicException rv) - data RISCVStmtExtension rv (f :: C.CrucibleType -> DK.Type) (ctp :: C.CrucibleType) where -- | Wrappers around the arch-specific functions in RISC-V; these are -- interpreted in 'funcSemantics'. diff --git a/macaw-riscv-symbolic/src/Data/Macaw/RISCV/Symbolic/Regs.hs b/macaw-riscv-symbolic/src/Data/Macaw/RISCV/Symbolic/Regs.hs new file mode 100644 index 00000000..c2086f96 --- /dev/null +++ b/macaw-riscv-symbolic/src/Data/Macaw/RISCV/Symbolic/Regs.hs @@ -0,0 +1,1044 @@ +{-| +Copyright : (c) Galois, Inc 2024 +Maintainer : Ryan Scott + +RISC-V registers. + +This module is meant to be imported qualified, as it exports many terse names. +-} + +{-# LANGUAGE AllowAmbiguousTypes #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE UndecidableInstances #-} +{-# OPTIONS_GHC -Wno-orphans #-} + +module Data.Macaw.RISCV.Symbolic.Regs + ( RISCVSymbolicException(..) + , riscvRegName + , riscvRegAssignment + , riscvRegStructType + , regIndexMap + , lookupReg + , updateReg + , PC + , GPR + , RA, SP, GP, TP, T0, T1, T2, S0, S1, A0, A1, A2, A3, A4, A5, A6, A7, S2, S3 + , S4, S5, S6, S7, S8, S9, S10, S11, T3, T4, T5, T6 + , X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, X17 + , X18, X19, X20, X21, X22, X23, X24, X25, X26, X27, X28, X29, X30, X31 + , FPR + , FT0, FT1, FT2, FT3, FT4, FT5, FT6, FT7, FS0, FS1, FA0, FA1, FA2, FA3 + , FA4, FA5, FA6, FA7, FS2, FS3, FS4, FS5, FS6, FS7, FS8, FS9, FS10, FS11, FT8 + , FT9, FT10, FT11 + , F0, F1, F2, F3, F4, F5, F6, F7, F8, F9, F10, F11, F12, F13, F14, F15, F16 + , F17, F18, F19, F20, F21, F22, F23, F24, F25, F26, F27, F28, F29, F30, F31 + , CSR + , MVendorID, MArchID, MImpID, MHartID, MStatus, MISA, MEDeleg, MIDeleg, MIE + , MTVec, MCounterEn, MScratch, MEPC, MCause, MTVal, MIP, MCycle, MInstRet + , MCycleh, MInstReth, FRm, FFlags, FCSR + , Priv, EXC + , pc + , ra, sp, gp, tp, t0, t1, t2, s0, s1, a0, a1, a2, a3, a4, a5, a6, a7, s2, s3 + , s4, s5, s6, s7, s8, s9, s10, s11, t3, t4, t5, t6 + , x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17 + , x18, x19, x20, x21, x22, x23, x24, x25, x26, x27, x28, x29, x30, x31 + , ft0, ft1, ft2, ft3, ft4, ft5, ft6, ft7, fs0, fs1, fa0, fa1, fa2, fa3 + , fa4, fa5, fa6, fa7, fs2, fs3, fs4, fs5, fs6, fs7, fs8, fs9, fs10, fs11, ft8 + , ft9, ft10, ft11 + , f0, f1, f2, f3, f4, f5, f6, f7, f8, f9, f10, f11, f12, f13, f14, f15, f16 + , f17, f18, f19, f20, f21, f22, f23, f24, f25, f26, f27, f28, f29, f30, f31 + , mvendorid, marchid, mimpid, mhartid, mstatus, misa, medeleg, mideleg, mie + , mtvec, mcounteren, mscratch, mepc, mcause, mtval, mip, mcycle, minstret + , mcycleh, minstreth, frm, fflags, fcsr + , priv, exc + ) where + +import Control.Lens ( (%~), (&) ) +import qualified Control.Monad.Catch as X +import qualified Data.Parameterized.Context as Ctx +import qualified Data.Parameterized.Map as MapF +import Data.Parameterized.Some ( Some(..) ) +import qualified Data.Parameterized.TraversableFC as FC +import Data.Typeable ( Typeable ) +import GHC.TypeLits +import qualified GRIFT.Types as G +import qualified Lang.Crucible.Types as C +import qualified Lang.Crucible.LLVM.MemModel as MM +import qualified What4.Interface as W4 +import qualified What4.Symbol as W4 + +import qualified Data.Macaw.CFG as MC +import qualified Data.Macaw.RISCV as MR +import qualified Data.Macaw.Types as MT +import qualified Data.Macaw.Symbolic as MS +import qualified Data.Macaw.Symbolic.Backend as MSB + +import qualified Data.Macaw.RISCV.Symbolic.Repeat as RR + +type instance MS.ArchRegContext (MR.RISCV rv) = + (Ctx.EmptyCtx Ctx.::> MT.BVType (G.RVWidth rv) -- PC + Ctx.<+> RR.CtxRepeat 31 (MT.BVType (G.RVWidth rv)) -- GPR regs. We use 31 instead of 32 + -- because we exclude x0, which is + -- hardwired to the constant 0. + Ctx.<+> RR.CtxRepeat 32 (MT.BVType (G.RVFloatWidth rv)) -- FPR regs + Ctx.<+> RR.CtxRepeat 23 (MT.BVType (G.RVWidth rv)) -- CSR regs. Although there is a + -- theoretical maximum of 4096 of + -- these registers, `grift` only + -- supports 23 of them in practice. + Ctx.<+> (Ctx.EmptyCtx Ctx.::> MT.BVType 2 -- PrivLevel + Ctx.::> MT.BoolType)) -- EXC + +riscvRegName :: MR.RISCVReg rv tp -> W4.SolverSymbol +riscvRegName r = W4.systemSymbol ("r!" ++ show (MC.prettyF r)) + +-- Note that `repeatAssign` starts indexing from 0, but we want to exclude +-- `GPR 0` (i.e., x0), as this is always hardwired to the constant 0. As such, +-- we offset all of the indexes by one using (+ 1). +gprRegs :: Ctx.Assignment (MR.RISCVReg rv) (RR.CtxRepeat 31 (MT.BVType (G.RVWidth rv))) +gprRegs = RR.repeatAssign (MR.GPR . fromIntegral . (+ 1)) + +fprRegs :: Ctx.Assignment (MR.RISCVReg rv) (RR.CtxRepeat 32 (MT.BVType (G.RVFloatWidth rv))) +fprRegs = RR.repeatAssign (MR.FPR . fromIntegral) + +-- | The RISC-V control/status registers that are directly supported by Macaw. +csrRegs :: Ctx.Assignment (MR.RISCVReg rv) (RR.CtxRepeat 23 (MT.BVType (G.RVWidth rv))) +csrRegs = RR.repeatAssign (MR.CSR . toEnum) + +-- | This contains an assignment that stores the register associated with each index in the +-- RISC-V register structure. +riscvRegAssignment :: Ctx.Assignment (MR.RISCVReg rv) (MS.ArchRegContext (MR.RISCV rv)) +riscvRegAssignment = + Ctx.Empty Ctx.:> MR.PC + Ctx.<++> gprRegs + Ctx.<++> fprRegs + Ctx.<++> csrRegs + Ctx.<++> (Ctx.Empty Ctx.:> MR.PrivLevel Ctx.:> MR.EXC) + +riscvRegStructType :: + forall rv + . G.KnownRV rv + => G.RVRepr rv + -> C.TypeRepr (MSB.ArchRegStruct (MR.RISCV rv)) +riscvRegStructType _rv = + C.StructRepr $ MS.typeCtxToCrucible $ FC.fmapFC MT.typeRepr $ riscvRegAssignment @rv + +regIndexMap :: forall rv + . G.KnownRV rv + => MSB.RegIndexMap (MR.RISCV rv) +regIndexMap = MSB.mkRegIndexMap assgn sz + where + assgn = riscvRegAssignment @rv + sz = Ctx.size $ MS.typeCtxToCrucible $ FC.fmapFC MT.typeRepr assgn + +lookupReg :: forall rv m f tp + . (G.KnownRV rv, Typeable rv, X.MonadThrow m) + => MR.RISCVReg rv tp + -> Ctx.Assignment f (MS.MacawCrucibleRegTypes (MR.RISCV rv)) + -> m (f (MS.ToCrucibleType tp)) +lookupReg r asgn = + case MapF.lookup r regIndexMap of + Nothing -> X.throwM (MissingRegisterInState (Some r)) + Just pair -> return (asgn Ctx.! MSB.crucibleIndex pair) + +updateReg :: forall rv m f tp + . (G.KnownRV rv, Typeable rv, X.MonadThrow m) + => MR.RISCVReg rv tp + -> (f (MS.ToCrucibleType tp) -> f (MS.ToCrucibleType tp)) + -> Ctx.Assignment f (MS.MacawCrucibleRegTypes (MR.RISCV rv)) + -> m (Ctx.Assignment f (MS.MacawCrucibleRegTypes (MR.RISCV rv))) +updateReg r upd asgn = do + case MapF.lookup r regIndexMap of + Nothing -> X.throwM (MissingRegisterInState (Some r)) + Just pair -> return (asgn & MapF.ixF (MSB.crucibleIndex pair) %~ upd) + +newtype RISCVSymbolicException rv = MissingRegisterInState (Some (MR.RISCVReg rv)) + deriving Show +instance Typeable rv => X.Exception (RISCVSymbolicException rv) + +-- The following definitions are tightly coupled to that of ArchRegContext for +-- RISCV. Unit tests in the test suite ensure that they are consistent with +-- riscvRegAssignment (below). + +-- | Program counter. +type PC = 0 + +-- | A general-purpose register. Note that this excludes @x0@, which is +-- hard-wired to the constant @0@. +type GPR n = 1 + n +-- | Return address (AKA 'X1'). +type RA = GPR 0 +-- | Stack pointer (AKA 'X2'). +type SP = GPR 1 +-- | Global pointer (AKA 'X3'). +type GP = GPR 2 +-- | Thread pointer (AKA 'X4'). +type TP = GPR 3 +-- | Temporary register (AKA 'X5'). +type T0 = GPR 4 +-- | Temporary register (AKA 'X6'). +type T1 = GPR 5 +-- | Temporary register (AKA 'X7'). +type T2 = GPR 6 +-- | Callee-saved register (AKA 'X8'). +type S0 = GPR 7 +-- | Callee-saved register (AKA 'X9'). +type S1 = GPR 8 +-- | Argument register (AKA 'X10'). +type A0 = GPR 9 +-- | Argument register (AKA 'X11'). +type A1 = GPR 10 +-- | Argument register (AKA 'X12'). +type A2 = GPR 11 +-- | Argument register (AKA 'X13'). +type A3 = GPR 12 +-- | Argument register (AKA 'X14'). +type A4 = GPR 13 +-- | Argument register (AKA 'X15'). +type A5 = GPR 14 +-- | Argument register (AKA 'X16'). +type A6 = GPR 15 +-- | Argument register (AKA 'X17'). +type A7 = GPR 16 +-- | Callee-saved register (AKA 'X18'). +type S2 = GPR 17 +-- | Callee-saved register (AKA 'X19'). +type S3 = GPR 18 +-- | Callee-saved register (AKA 'X20'). +type S4 = GPR 19 +-- | Callee-saved register (AKA 'X21'). +type S5 = GPR 20 +-- | Callee-saved register (AKA 'X22'). +type S6 = GPR 21 +-- | Callee-saved register (AKA 'X23'). +type S7 = GPR 22 +-- | Callee-saved register (AKA 'X24'). +type S8 = GPR 23 +-- | Callee-saved register (AKA 'X25'). +type S9 = GPR 24 +-- | Callee-saved register (AKA 'X26'). +type S10 = GPR 25 +-- | Callee-saved register (AKA 'X27'). +type S11 = GPR 26 +-- | Temporary register (AKA 'X28'). +type T3 = GPR 27 +-- | Temporary register (AKA 'X29'). +type T4 = GPR 28 +-- | Temporary register (AKA 'X30'). +type T5 = GPR 29 +-- | Temporary register (AKA 'X31'). +type T6 = GPR 30 +-- | Return address (AKA 'RA'). +type X1 = GPR 0 +-- | Stack pointer (AKA 'SP'). +type X2 = GPR 1 +-- | Global pointer (AKA 'GP'). +type X3 = GPR 2 +-- | Thread pointer (AKA 'TP'). +type X4 = GPR 3 +-- | Temporary register (AKA 'T0'). +type X5 = GPR 4 +-- | Temporary register (AKA 'T1'). +type X6 = GPR 5 +-- | Temporary register (AKA 'T2'). +type X7 = GPR 6 +-- | Callee-saved register (AKA 'S0'). +type X8 = GPR 7 +-- | Callee-saved register (AKA 'S1'). +type X9 = GPR 8 +-- | Argument register (AKA 'A0'). +type X10 = GPR 9 +-- | Argument register (AKA 'A1'). +type X11 = GPR 10 +-- | Argument register (AKA 'A2'). +type X12 = GPR 11 +-- | Argument register (AKA 'A3'). +type X13 = GPR 12 +-- | Argument register (AKA 'A4'). +type X14 = GPR 13 +-- | Argument register (AKA 'A5'). +type X15 = GPR 14 +-- | Argument register (AKA 'A6'). +type X16 = GPR 15 +-- | Argument register (AKA 'A7'). +type X17 = GPR 16 +-- | Callee-saved register (AKA 'S2'). +type X18 = GPR 17 +-- | Callee-saved register (AKA 'S3'). +type X19 = GPR 18 +-- | Callee-saved register (AKA 'S4'). +type X20 = GPR 19 +-- | Callee-saved register (AKA 'S5'). +type X21 = GPR 20 +-- | Callee-saved register (AKA 'S6'). +type X22 = GPR 21 +-- | Callee-saved register (AKA 'S7'). +type X23 = GPR 22 +-- | Callee-saved register (AKA 'S8'). +type X24 = GPR 23 +-- | Callee-saved register (AKA 'S9'). +type X25 = GPR 24 +-- | Callee-saved register (AKA 'S10'). +type X26 = GPR 25 +-- | Callee-saved register (AKA 'S11'). +type X27 = GPR 26 +-- | Temporary register (AKA 'T3'). +type X28 = GPR 27 +-- | Temporary register (AKA 'T4'). +type X29 = GPR 28 +-- | Temporary register (AKA 'T5'). +type X30 = GPR 29 +-- | Temporary register (AKA 'T6'). +type X31 = GPR 30 + +-- | A floating-point register. +type FPR n = 32 + n +-- | Temporary register (AKA 'F0'). +type FT0 = FPR 0 +-- | Temporary register (AKA 'F1'). +type FT1 = FPR 1 +-- | Temporary register (AKA 'F2'). +type FT2 = FPR 2 +-- | Temporary register (AKA 'F3'). +type FT3 = FPR 3 +-- | Temporary register (AKA 'F4'). +type FT4 = FPR 4 +-- | Temporary register (AKA 'F5'). +type FT5 = FPR 5 +-- | Temporary register (AKA 'F6'). +type FT6 = FPR 6 +-- | Temporary register (AKA 'F7'). +type FT7 = FPR 7 +-- | Callee-saved register (AKA 'F8'). +type FS0 = FPR 8 +-- | Callee-saved register (AKA 'F9'). +type FS1 = FPR 9 +-- | Argument register (AKA 'F10'). +type FA0 = FPR 10 +-- | Argument register (AKA 'F11'). +type FA1 = FPR 11 +-- | Argument register (AKA 'F12'). +type FA2 = FPR 12 +-- | Argument register (AKA 'F13'). +type FA3 = FPR 13 +-- | Argument register (AKA 'F14'). +type FA4 = FPR 14 +-- | Argument register (AKA 'F15'). +type FA5 = FPR 15 +-- | Argument register (AKA 'F16'). +type FA6 = FPR 16 +-- | Argument register (AKA 'F17'). +type FA7 = FPR 17 +-- | Callee-saved register (AKA 'F18'). +type FS2 = FPR 18 +-- | Callee-saved register (AKA 'F19'). +type FS3 = FPR 19 +-- | Callee-saved register (AKA 'F20'). +type FS4 = FPR 20 +-- | Callee-saved register (AKA 'F21'). +type FS5 = FPR 21 +-- | Callee-saved register (AKA 'F22'). +type FS6 = FPR 22 +-- | Callee-saved register (AKA 'F23'). +type FS7 = FPR 23 +-- | Callee-saved register (AKA 'F24'). +type FS8 = FPR 24 +-- | Callee-saved register (AKA 'F25'). +type FS9 = FPR 25 +-- | Callee-saved register (AKA 'F26'). +type FS10 = FPR 26 +-- | Callee-saved register (AKA 'F27'). +type FS11 = FPR 27 +-- | Temporary register (AKA 'F28'). +type FT8 = FPR 28 +-- | Temporary register (AKA 'F29'). +type FT9 = FPR 29 +-- | Temporary register (AKA 'F30'). +type FT10 = FPR 30 +-- | Temporary register (AKA 'F31'). +type FT11 = FPR 31 +-- | Temporary register (AKA 'FT0'). +type F0 = FPR 0 +-- | Temporary register (AKA 'FT1'). +type F1 = FPR 1 +-- | Temporary register (AKA 'FT2'). +type F2 = FPR 2 +-- | Temporary register (AKA 'FT3'). +type F3 = FPR 3 +-- | Temporary register (AKA 'FT4'). +type F4 = FPR 4 +-- | Temporary register (AKA 'FT5'). +type F5 = FPR 5 +-- | Temporary register (AKA 'FT6'). +type F6 = FPR 6 +-- | Temporary register (AKA 'FT7'). +type F7 = FPR 7 +-- | Callee-saved register (AKA 'FS0'). +type F8 = FPR 8 +-- | Callee-saved register (AKA 'FS1'). +type F9 = FPR 9 +-- | Argument register (AKA 'FA0'). +type F10 = FPR 10 +-- | Argument register (AKA 'FA1'). +type F11 = FPR 11 +-- | Argument register (AKA 'FA2'). +type F12 = FPR 12 +-- | Argument register (AKA 'FA3'). +type F13 = FPR 13 +-- | Argument register (AKA 'FA4'). +type F14 = FPR 14 +-- | Argument register (AKA 'FA5'). +type F15 = FPR 15 +-- | Argument register (AKA 'FA6'). +type F16 = FPR 16 +-- | Argument register (AKA 'FA7'). +type F17 = FPR 17 +-- | Callee-saved register (AKA 'FS2'). +type F18 = FPR 18 +-- | Callee-saved register (AKA 'FS3'). +type F19 = FPR 19 +-- | Callee-saved register (AKA 'FS4'). +type F20 = FPR 20 +-- | Callee-saved register (AKA 'FS5'). +type F21 = FPR 21 +-- | Callee-saved register (AKA 'FS6'). +type F22 = FPR 22 +-- | Callee-saved register (AKA 'FS7'). +type F23 = FPR 23 +-- | Callee-saved register (AKA 'FS8'). +type F24 = FPR 24 +-- | Callee-saved register (AKA 'FS9'). +type F25 = FPR 25 +-- | Callee-saved register (AKA 'FS10'). +type F26 = FPR 26 +-- | Callee-saved register (AKA 'FS11'). +type F27 = FPR 27 +-- | Temporary register (AKA 'FT8'). +type F28 = FPR 28 +-- | Temporary register (AKA 'FT9'). +type F29 = FPR 29 +-- | Temporary register (AKA 'FT10'). +type F30 = FPR 30 +-- | Temporary register (AKA 'FT11'). +type F31 = FPR 31 + +-- | A control/status register. +type CSR n = 64 + n +type MVendorID = CSR 0 +type MArchID = CSR 1 +type MImpID = CSR 2 +type MHartID = CSR 3 +type MStatus = CSR 4 +type MISA = CSR 5 +type MEDeleg = CSR 6 +type MIDeleg = CSR 7 +type MIE = CSR 8 +type MTVec = CSR 9 +type MCounterEn = CSR 10 +type MScratch = CSR 11 +type MEPC = CSR 12 +type MCause = CSR 13 +type MTVal = CSR 14 +type MIP = CSR 15 +type MCycle = CSR 16 +type MInstRet = CSR 17 +type MCycleh = CSR 18 +type MInstReth = CSR 19 +type FRm = CSR 20 +type FFlags = CSR 21 +type FCSR = CSR 22 + +-- | Current privilege level. +type Priv = 87 + +-- | Trip this if something bad happens. +type EXC = 88 + +-- | Program counter. +pc :: Ctx.Index (MS.MacawCrucibleRegTypes (MR.RISCV rv)) (MM.LLVMPointerType (G.RVWidth rv)) +pc = Ctx.natIndex @PC + +-- | Return address (AKA 'x1'). +ra :: Ctx.Index (MS.MacawCrucibleRegTypes (MR.RISCV rv)) (MM.LLVMPointerType (G.RVWidth rv)) +ra = Ctx.natIndex @RA + +-- | Stack pointer (AKA 'x2'). +sp :: Ctx.Index (MS.MacawCrucibleRegTypes (MR.RISCV rv)) (MM.LLVMPointerType (G.RVWidth rv)) +sp = Ctx.natIndex @SP + +-- | Global pointer (AKA 'x3'). +gp :: Ctx.Index (MS.MacawCrucibleRegTypes (MR.RISCV rv)) (MM.LLVMPointerType (G.RVWidth rv)) +gp = Ctx.natIndex @GP + +-- | Thread pointer (AKA 'x4'). +tp :: Ctx.Index (MS.MacawCrucibleRegTypes (MR.RISCV rv)) (MM.LLVMPointerType (G.RVWidth rv)) +tp = Ctx.natIndex @TP + +-- | Temporary register (AKA 'x5'). +t0 :: Ctx.Index (MS.MacawCrucibleRegTypes (MR.RISCV rv)) (MM.LLVMPointerType (G.RVWidth rv)) +t0 = Ctx.natIndex @T0 + +-- | Temporary register (AKA 'x6'). +t1 :: Ctx.Index (MS.MacawCrucibleRegTypes (MR.RISCV rv)) (MM.LLVMPointerType (G.RVWidth rv)) +t1 = Ctx.natIndex @T1 + +-- | Temporary register (AKA 'x7'). +t2 :: Ctx.Index (MS.MacawCrucibleRegTypes (MR.RISCV rv)) (MM.LLVMPointerType (G.RVWidth rv)) +t2 = Ctx.natIndex @T2 + +-- | Callee-saved register (AKA 'x8'). +s0 :: Ctx.Index (MS.MacawCrucibleRegTypes (MR.RISCV rv)) (MM.LLVMPointerType (G.RVWidth rv)) +s0 = Ctx.natIndex @S0 + +-- | Callee-saved register (AKA 'x9'). +s1 :: Ctx.Index (MS.MacawCrucibleRegTypes (MR.RISCV rv)) (MM.LLVMPointerType (G.RVWidth rv)) +s1 = Ctx.natIndex @S1 + +-- | Argument register (AKA 'x10'). +a0 :: Ctx.Index (MS.MacawCrucibleRegTypes (MR.RISCV rv)) (MM.LLVMPointerType (G.RVWidth rv)) +a0 = Ctx.natIndex @A0 + +-- | Argument register (AKA 'x11'). +a1 :: Ctx.Index (MS.MacawCrucibleRegTypes (MR.RISCV rv)) (MM.LLVMPointerType (G.RVWidth rv)) +a1 = Ctx.natIndex @A1 + +-- | Argument register (AKA 'x12'). +a2 :: Ctx.Index (MS.MacawCrucibleRegTypes (MR.RISCV rv)) (MM.LLVMPointerType (G.RVWidth rv)) +a2 = Ctx.natIndex @A2 + +-- | Argument register (AKA 'x13'). +a3 :: Ctx.Index (MS.MacawCrucibleRegTypes (MR.RISCV rv)) (MM.LLVMPointerType (G.RVWidth rv)) +a3 = Ctx.natIndex @A3 + +-- | Argument register (AKA 'x14'). +a4 :: Ctx.Index (MS.MacawCrucibleRegTypes (MR.RISCV rv)) (MM.LLVMPointerType (G.RVWidth rv)) +a4 = Ctx.natIndex @A4 + +-- | Argument register (AKA 'x15'). +a5 :: Ctx.Index (MS.MacawCrucibleRegTypes (MR.RISCV rv)) (MM.LLVMPointerType (G.RVWidth rv)) +a5 = Ctx.natIndex @A5 + +-- | Argument register (AKA 'x16'). +a6 :: Ctx.Index (MS.MacawCrucibleRegTypes (MR.RISCV rv)) (MM.LLVMPointerType (G.RVWidth rv)) +a6 = Ctx.natIndex @A6 + +-- | Argument register (AKA 'x17'). +a7 :: Ctx.Index (MS.MacawCrucibleRegTypes (MR.RISCV rv)) (MM.LLVMPointerType (G.RVWidth rv)) +a7 = Ctx.natIndex @A7 + +-- | Callee-saved register (AKA 'x18'). +s2 :: Ctx.Index (MS.MacawCrucibleRegTypes (MR.RISCV rv)) (MM.LLVMPointerType (G.RVWidth rv)) +s2 = Ctx.natIndex @S2 + +-- | Callee-saved register (AKA 'x19'). +s3 :: Ctx.Index (MS.MacawCrucibleRegTypes (MR.RISCV rv)) (MM.LLVMPointerType (G.RVWidth rv)) +s3 = Ctx.natIndex @S3 + +-- | Callee-saved register (AKA 'x20'). +s4 :: Ctx.Index (MS.MacawCrucibleRegTypes (MR.RISCV rv)) (MM.LLVMPointerType (G.RVWidth rv)) +s4 = Ctx.natIndex @S4 + +-- | Callee-saved register (AKA 'x21'). +s5 :: Ctx.Index (MS.MacawCrucibleRegTypes (MR.RISCV rv)) (MM.LLVMPointerType (G.RVWidth rv)) +s5 = Ctx.natIndex @S5 + +-- | Callee-saved register (AKA 'x22'). +s6 :: Ctx.Index (MS.MacawCrucibleRegTypes (MR.RISCV rv)) (MM.LLVMPointerType (G.RVWidth rv)) +s6 = Ctx.natIndex @S6 + +-- | Callee-saved register (AKA 'x23'). +s7 :: Ctx.Index (MS.MacawCrucibleRegTypes (MR.RISCV rv)) (MM.LLVMPointerType (G.RVWidth rv)) +s7 = Ctx.natIndex @S7 + +-- | Callee-saved register (AKA 'x24'). +s8 :: Ctx.Index (MS.MacawCrucibleRegTypes (MR.RISCV rv)) (MM.LLVMPointerType (G.RVWidth rv)) +s8 = Ctx.natIndex @S8 + +-- | Callee-saved register (AKA 'x25'). +s9 :: Ctx.Index (MS.MacawCrucibleRegTypes (MR.RISCV rv)) (MM.LLVMPointerType (G.RVWidth rv)) +s9 = Ctx.natIndex @S9 + +-- | Callee-saved register (AKA 'x26'). +s10 :: Ctx.Index (MS.MacawCrucibleRegTypes (MR.RISCV rv)) (MM.LLVMPointerType (G.RVWidth rv)) +s10 = Ctx.natIndex @S10 + +-- | Callee-saved register (AKA 'x27'). +s11 :: Ctx.Index (MS.MacawCrucibleRegTypes (MR.RISCV rv)) (MM.LLVMPointerType (G.RVWidth rv)) +s11 = Ctx.natIndex @S11 + +-- | Temporary register (AKA 'x28'). +t3 :: Ctx.Index (MS.MacawCrucibleRegTypes (MR.RISCV rv)) (MM.LLVMPointerType (G.RVWidth rv)) +t3 = Ctx.natIndex @T3 + +-- | Temporary register (AKA 'x29'). +t4 :: Ctx.Index (MS.MacawCrucibleRegTypes (MR.RISCV rv)) (MM.LLVMPointerType (G.RVWidth rv)) +t4 = Ctx.natIndex @T4 + +-- | Temporary register (AKA 'x30'). +t5 :: Ctx.Index (MS.MacawCrucibleRegTypes (MR.RISCV rv)) (MM.LLVMPointerType (G.RVWidth rv)) +t5 = Ctx.natIndex @T5 + +-- | Temporary register (AKA 'x31'). +t6 :: Ctx.Index (MS.MacawCrucibleRegTypes (MR.RISCV rv)) (MM.LLVMPointerType (G.RVWidth rv)) +t6 = Ctx.natIndex @T6 + +-- | Return address (AKA 'ra'). +x1 :: Ctx.Index (MS.MacawCrucibleRegTypes (MR.RISCV rv)) (MM.LLVMPointerType (G.RVWidth rv)) +x1 = Ctx.natIndex @X1 + +-- | Stack pointer (AKA 'sp'). +x2 :: Ctx.Index (MS.MacawCrucibleRegTypes (MR.RISCV rv)) (MM.LLVMPointerType (G.RVWidth rv)) +x2 = Ctx.natIndex @X2 + +-- | Global pointer (AKA 'gp'). +x3 :: Ctx.Index (MS.MacawCrucibleRegTypes (MR.RISCV rv)) (MM.LLVMPointerType (G.RVWidth rv)) +x3 = Ctx.natIndex @X3 + +-- | Thread pointer (AKA 'tp'). +x4 :: Ctx.Index (MS.MacawCrucibleRegTypes (MR.RISCV rv)) (MM.LLVMPointerType (G.RVWidth rv)) +x4 = Ctx.natIndex @X4 + +-- | Temporary register (AKA 't0'). +x5 :: Ctx.Index (MS.MacawCrucibleRegTypes (MR.RISCV rv)) (MM.LLVMPointerType (G.RVWidth rv)) +x5 = Ctx.natIndex @X5 + +-- | Temporary register (AKA 't1'). +x6 :: Ctx.Index (MS.MacawCrucibleRegTypes (MR.RISCV rv)) (MM.LLVMPointerType (G.RVWidth rv)) +x6 = Ctx.natIndex @X6 + +-- | Temporary register (AKA 't2'). +x7 :: Ctx.Index (MS.MacawCrucibleRegTypes (MR.RISCV rv)) (MM.LLVMPointerType (G.RVWidth rv)) +x7 = Ctx.natIndex @X7 + +-- | Callee-saved register (AKA 's0'). +x8 :: Ctx.Index (MS.MacawCrucibleRegTypes (MR.RISCV rv)) (MM.LLVMPointerType (G.RVWidth rv)) +x8 = Ctx.natIndex @X8 + +-- | Callee-saved register (AKA 's1'). +x9 :: Ctx.Index (MS.MacawCrucibleRegTypes (MR.RISCV rv)) (MM.LLVMPointerType (G.RVWidth rv)) +x9 = Ctx.natIndex @X9 + +-- | Argument register (AKA 'a0'). +x10 :: Ctx.Index (MS.MacawCrucibleRegTypes (MR.RISCV rv)) (MM.LLVMPointerType (G.RVWidth rv)) +x10 = Ctx.natIndex @X10 + +-- | Argument register (AKA 'a1'). +x11 :: Ctx.Index (MS.MacawCrucibleRegTypes (MR.RISCV rv)) (MM.LLVMPointerType (G.RVWidth rv)) +x11 = Ctx.natIndex @X11 + +-- | Argument register (AKA 'a2'). +x12 :: Ctx.Index (MS.MacawCrucibleRegTypes (MR.RISCV rv)) (MM.LLVMPointerType (G.RVWidth rv)) +x12 = Ctx.natIndex @X12 + +-- | Argument register (AKA 'a3'). +x13 :: Ctx.Index (MS.MacawCrucibleRegTypes (MR.RISCV rv)) (MM.LLVMPointerType (G.RVWidth rv)) +x13 = Ctx.natIndex @X13 + +-- | Argument register (AKA 'a4'). +x14 :: Ctx.Index (MS.MacawCrucibleRegTypes (MR.RISCV rv)) (MM.LLVMPointerType (G.RVWidth rv)) +x14 = Ctx.natIndex @X14 + +-- | Argument register (AKA 'a5'). +x15 :: Ctx.Index (MS.MacawCrucibleRegTypes (MR.RISCV rv)) (MM.LLVMPointerType (G.RVWidth rv)) +x15 = Ctx.natIndex @X15 + +-- | Argument register (AKA 'a6'). +x16 :: Ctx.Index (MS.MacawCrucibleRegTypes (MR.RISCV rv)) (MM.LLVMPointerType (G.RVWidth rv)) +x16 = Ctx.natIndex @X16 + +-- | Argument register (AKA 'a7'). +x17 :: Ctx.Index (MS.MacawCrucibleRegTypes (MR.RISCV rv)) (MM.LLVMPointerType (G.RVWidth rv)) +x17 = Ctx.natIndex @X17 + +-- | Callee-saved register (AKA 's2'). +x18 :: Ctx.Index (MS.MacawCrucibleRegTypes (MR.RISCV rv)) (MM.LLVMPointerType (G.RVWidth rv)) +x18 = Ctx.natIndex @X18 + +-- | Callee-saved register (AKA 's3'). +x19 :: Ctx.Index (MS.MacawCrucibleRegTypes (MR.RISCV rv)) (MM.LLVMPointerType (G.RVWidth rv)) +x19 = Ctx.natIndex @X19 + +-- | Callee-saved register (AKA 's4'). +x20 :: Ctx.Index (MS.MacawCrucibleRegTypes (MR.RISCV rv)) (MM.LLVMPointerType (G.RVWidth rv)) +x20 = Ctx.natIndex @X20 + +-- | Callee-saved register (AKA 's5'). +x21 :: Ctx.Index (MS.MacawCrucibleRegTypes (MR.RISCV rv)) (MM.LLVMPointerType (G.RVWidth rv)) +x21 = Ctx.natIndex @X21 + +-- | Callee-saved register (AKA 's6'). +x22 :: Ctx.Index (MS.MacawCrucibleRegTypes (MR.RISCV rv)) (MM.LLVMPointerType (G.RVWidth rv)) +x22 = Ctx.natIndex @X22 + +-- | Callee-saved register (AKA 's7'). +x23 :: Ctx.Index (MS.MacawCrucibleRegTypes (MR.RISCV rv)) (MM.LLVMPointerType (G.RVWidth rv)) +x23 = Ctx.natIndex @X23 + +-- | Callee-saved register (AKA 's8'). +x24 :: Ctx.Index (MS.MacawCrucibleRegTypes (MR.RISCV rv)) (MM.LLVMPointerType (G.RVWidth rv)) +x24 = Ctx.natIndex @X24 + +-- | Callee-saved register (AKA 's9'). +x25 :: Ctx.Index (MS.MacawCrucibleRegTypes (MR.RISCV rv)) (MM.LLVMPointerType (G.RVWidth rv)) +x25 = Ctx.natIndex @X25 + +-- | Callee-saved register (AKA 's10'). +x26 :: Ctx.Index (MS.MacawCrucibleRegTypes (MR.RISCV rv)) (MM.LLVMPointerType (G.RVWidth rv)) +x26 = Ctx.natIndex @X26 + +-- | Callee-saved register (AKA 's11'). +x27 :: Ctx.Index (MS.MacawCrucibleRegTypes (MR.RISCV rv)) (MM.LLVMPointerType (G.RVWidth rv)) +x27 = Ctx.natIndex @X27 + +-- | Temporary register (AKA 't3'). +x28 :: Ctx.Index (MS.MacawCrucibleRegTypes (MR.RISCV rv)) (MM.LLVMPointerType (G.RVWidth rv)) +x28 = Ctx.natIndex @X28 + +-- | Temporary register (AKA 't4'). +x29 :: Ctx.Index (MS.MacawCrucibleRegTypes (MR.RISCV rv)) (MM.LLVMPointerType (G.RVWidth rv)) +x29 = Ctx.natIndex @X29 + +-- | Temporary register (AKA 't5'). +x30 :: Ctx.Index (MS.MacawCrucibleRegTypes (MR.RISCV rv)) (MM.LLVMPointerType (G.RVWidth rv)) +x30 = Ctx.natIndex @X30 + +-- | Temporary register (AKA 't6'). +x31 :: Ctx.Index (MS.MacawCrucibleRegTypes (MR.RISCV rv)) (MM.LLVMPointerType (G.RVWidth rv)) +x31 = Ctx.natIndex @X31 + +-- | Temporary register (AKA 'f0'). +ft0 :: Ctx.Index (MS.MacawCrucibleRegTypes (MR.RISCV rv)) (MM.LLVMPointerType (G.RVFloatWidth rv)) +ft0 = Ctx.natIndex @FT0 + +-- | Temporary register (AKA 'f1'). +ft1 :: Ctx.Index (MS.MacawCrucibleRegTypes (MR.RISCV rv)) (MM.LLVMPointerType (G.RVFloatWidth rv)) +ft1 = Ctx.natIndex @FT1 + +-- | Temporary register (AKA 'f2'). +ft2 :: Ctx.Index (MS.MacawCrucibleRegTypes (MR.RISCV rv)) (MM.LLVMPointerType (G.RVFloatWidth rv)) +ft2 = Ctx.natIndex @FT2 + +-- | Temporary register (AKA 'f3'). +ft3 :: Ctx.Index (MS.MacawCrucibleRegTypes (MR.RISCV rv)) (MM.LLVMPointerType (G.RVFloatWidth rv)) +ft3 = Ctx.natIndex @FT3 + +-- | Temporary register (AKA 'f4'). +ft4 :: Ctx.Index (MS.MacawCrucibleRegTypes (MR.RISCV rv)) (MM.LLVMPointerType (G.RVFloatWidth rv)) +ft4 = Ctx.natIndex @FT4 + +-- | Temporary register (AKA 'f5'). +ft5 :: Ctx.Index (MS.MacawCrucibleRegTypes (MR.RISCV rv)) (MM.LLVMPointerType (G.RVFloatWidth rv)) +ft5 = Ctx.natIndex @FT5 + +-- | Temporary register (AKA 'f6'). +ft6 :: Ctx.Index (MS.MacawCrucibleRegTypes (MR.RISCV rv)) (MM.LLVMPointerType (G.RVFloatWidth rv)) +ft6 = Ctx.natIndex @FT6 + +-- | Temporary register (AKA 'f7'). +ft7 :: Ctx.Index (MS.MacawCrucibleRegTypes (MR.RISCV rv)) (MM.LLVMPointerType (G.RVFloatWidth rv)) +ft7 = Ctx.natIndex @FT7 + +-- | Callee-saved register (AKA 'f8'). +fs0 :: Ctx.Index (MS.MacawCrucibleRegTypes (MR.RISCV rv)) (MM.LLVMPointerType (G.RVFloatWidth rv)) +fs0 = Ctx.natIndex @FS0 + +-- | Callee-saved register (AKA 'f9'). +fs1 :: Ctx.Index (MS.MacawCrucibleRegTypes (MR.RISCV rv)) (MM.LLVMPointerType (G.RVFloatWidth rv)) +fs1 = Ctx.natIndex @FS1 + +-- | Argument register (AKA 'f10'). +fa0 :: Ctx.Index (MS.MacawCrucibleRegTypes (MR.RISCV rv)) (MM.LLVMPointerType (G.RVFloatWidth rv)) +fa0 = Ctx.natIndex @FA0 + +-- | Argument register (AKA 'f11'). +fa1 :: Ctx.Index (MS.MacawCrucibleRegTypes (MR.RISCV rv)) (MM.LLVMPointerType (G.RVFloatWidth rv)) +fa1 = Ctx.natIndex @FA1 + +-- | Argument register (AKA 'f12'). +fa2 :: Ctx.Index (MS.MacawCrucibleRegTypes (MR.RISCV rv)) (MM.LLVMPointerType (G.RVFloatWidth rv)) +fa2 = Ctx.natIndex @FA2 + +-- | Argument register (AKA 'f13'). +fa3 :: Ctx.Index (MS.MacawCrucibleRegTypes (MR.RISCV rv)) (MM.LLVMPointerType (G.RVFloatWidth rv)) +fa3 = Ctx.natIndex @FA3 + +-- | Argument register (AKA 'f14'). +fa4 :: Ctx.Index (MS.MacawCrucibleRegTypes (MR.RISCV rv)) (MM.LLVMPointerType (G.RVFloatWidth rv)) +fa4 = Ctx.natIndex @FA4 + +-- | Argument register (AKA 'f15'). +fa5 :: Ctx.Index (MS.MacawCrucibleRegTypes (MR.RISCV rv)) (MM.LLVMPointerType (G.RVFloatWidth rv)) +fa5 = Ctx.natIndex @FA5 + +-- | Argument register (AKA 'f16'). +fa6 :: Ctx.Index (MS.MacawCrucibleRegTypes (MR.RISCV rv)) (MM.LLVMPointerType (G.RVFloatWidth rv)) +fa6 = Ctx.natIndex @FA6 + +-- | Argument register (AKA 'f17'). +fa7 :: Ctx.Index (MS.MacawCrucibleRegTypes (MR.RISCV rv)) (MM.LLVMPointerType (G.RVFloatWidth rv)) +fa7 = Ctx.natIndex @FA7 + +-- | Callee-saved register (AKA 'f18'). +fs2 :: Ctx.Index (MS.MacawCrucibleRegTypes (MR.RISCV rv)) (MM.LLVMPointerType (G.RVFloatWidth rv)) +fs2 = Ctx.natIndex @FS2 + +-- | Callee-saved register (AKA 'f19'). +fs3 :: Ctx.Index (MS.MacawCrucibleRegTypes (MR.RISCV rv)) (MM.LLVMPointerType (G.RVFloatWidth rv)) +fs3 = Ctx.natIndex @FS3 + +-- | Callee-saved register (AKA 'f20'). +fs4 :: Ctx.Index (MS.MacawCrucibleRegTypes (MR.RISCV rv)) (MM.LLVMPointerType (G.RVFloatWidth rv)) +fs4 = Ctx.natIndex @FS4 + +-- | Callee-saved register (AKA 'f21'). +fs5 :: Ctx.Index (MS.MacawCrucibleRegTypes (MR.RISCV rv)) (MM.LLVMPointerType (G.RVFloatWidth rv)) +fs5 = Ctx.natIndex @FS5 + +-- | Callee-saved register (AKA 'f22'). +fs6 :: Ctx.Index (MS.MacawCrucibleRegTypes (MR.RISCV rv)) (MM.LLVMPointerType (G.RVFloatWidth rv)) +fs6 = Ctx.natIndex @FS6 + +-- | Callee-saved register (AKA 'f23'). +fs7 :: Ctx.Index (MS.MacawCrucibleRegTypes (MR.RISCV rv)) (MM.LLVMPointerType (G.RVFloatWidth rv)) +fs7 = Ctx.natIndex @FS7 + +-- | Callee-saved register (AKA 'f24'). +fs8 :: Ctx.Index (MS.MacawCrucibleRegTypes (MR.RISCV rv)) (MM.LLVMPointerType (G.RVFloatWidth rv)) +fs8 = Ctx.natIndex @FS8 + +-- | Callee-saved register (AKA 'f25'). +fs9 :: Ctx.Index (MS.MacawCrucibleRegTypes (MR.RISCV rv)) (MM.LLVMPointerType (G.RVFloatWidth rv)) +fs9 = Ctx.natIndex @FS9 + +-- | Callee-saved register (AKA 'f26'). +fs10 :: Ctx.Index (MS.MacawCrucibleRegTypes (MR.RISCV rv)) (MM.LLVMPointerType (G.RVFloatWidth rv)) +fs10 = Ctx.natIndex @FS10 + +-- | Callee-saved register (AKA 'f27'). +fs11 :: Ctx.Index (MS.MacawCrucibleRegTypes (MR.RISCV rv)) (MM.LLVMPointerType (G.RVFloatWidth rv)) +fs11 = Ctx.natIndex @FS11 + +-- | Temporary register (AKA 'f28'). +ft8 :: Ctx.Index (MS.MacawCrucibleRegTypes (MR.RISCV rv)) (MM.LLVMPointerType (G.RVFloatWidth rv)) +ft8 = Ctx.natIndex @FT8 + +-- | Temporary register (AKA 'f29'). +ft9 :: Ctx.Index (MS.MacawCrucibleRegTypes (MR.RISCV rv)) (MM.LLVMPointerType (G.RVFloatWidth rv)) +ft9 = Ctx.natIndex @FT9 + +-- | Temporary register (AKA 'f30'). +ft10 :: Ctx.Index (MS.MacawCrucibleRegTypes (MR.RISCV rv)) (MM.LLVMPointerType (G.RVFloatWidth rv)) +ft10 = Ctx.natIndex @FT10 + +-- | Temporary register (AKA 'f31'). +ft11 :: Ctx.Index (MS.MacawCrucibleRegTypes (MR.RISCV rv)) (MM.LLVMPointerType (G.RVFloatWidth rv)) +ft11 = Ctx.natIndex @FT11 + +-- | Temporary register (AKA 'ft0'). +f0 :: Ctx.Index (MS.MacawCrucibleRegTypes (MR.RISCV rv)) (MM.LLVMPointerType (G.RVFloatWidth rv)) +f0 = Ctx.natIndex @F0 + +-- | Temporary register (AKA 'ft1'). +f1 :: Ctx.Index (MS.MacawCrucibleRegTypes (MR.RISCV rv)) (MM.LLVMPointerType (G.RVFloatWidth rv)) +f1 = Ctx.natIndex @F1 + +-- | Temporary register (AKA 'ft2'). +f2 :: Ctx.Index (MS.MacawCrucibleRegTypes (MR.RISCV rv)) (MM.LLVMPointerType (G.RVFloatWidth rv)) +f2 = Ctx.natIndex @F2 + +-- | Temporary register (AKA 'ft3'). +f3 :: Ctx.Index (MS.MacawCrucibleRegTypes (MR.RISCV rv)) (MM.LLVMPointerType (G.RVFloatWidth rv)) +f3 = Ctx.natIndex @F3 + +-- | Temporary register (AKA 'ft4'). +f4 :: Ctx.Index (MS.MacawCrucibleRegTypes (MR.RISCV rv)) (MM.LLVMPointerType (G.RVFloatWidth rv)) +f4 = Ctx.natIndex @F4 + +-- | Temporary register (AKA 'ft5'). +f5 :: Ctx.Index (MS.MacawCrucibleRegTypes (MR.RISCV rv)) (MM.LLVMPointerType (G.RVFloatWidth rv)) +f5 = Ctx.natIndex @F5 + +-- | Temporary register (AKA 'ft6'). +f6 :: Ctx.Index (MS.MacawCrucibleRegTypes (MR.RISCV rv)) (MM.LLVMPointerType (G.RVFloatWidth rv)) +f6 = Ctx.natIndex @F6 + +-- | Temporary register (AKA 'ft7'). +f7 :: Ctx.Index (MS.MacawCrucibleRegTypes (MR.RISCV rv)) (MM.LLVMPointerType (G.RVFloatWidth rv)) +f7 = Ctx.natIndex @F7 + +-- | Callee-saved register (AKA 'fs0'). +f8 :: Ctx.Index (MS.MacawCrucibleRegTypes (MR.RISCV rv)) (MM.LLVMPointerType (G.RVFloatWidth rv)) +f8 = Ctx.natIndex @F8 + +-- | Callee-saved register (AKA 'fs1'). +f9 :: Ctx.Index (MS.MacawCrucibleRegTypes (MR.RISCV rv)) (MM.LLVMPointerType (G.RVFloatWidth rv)) +f9 = Ctx.natIndex @F9 + +-- | Argument register (AKA 'fa0'). +f10 :: Ctx.Index (MS.MacawCrucibleRegTypes (MR.RISCV rv)) (MM.LLVMPointerType (G.RVFloatWidth rv)) +f10 = Ctx.natIndex @F10 + +-- | Argument register (AKA 'fa1'). +f11 :: Ctx.Index (MS.MacawCrucibleRegTypes (MR.RISCV rv)) (MM.LLVMPointerType (G.RVFloatWidth rv)) +f11 = Ctx.natIndex @F11 + +-- | Argument register (AKA 'fa2'). +f12 :: Ctx.Index (MS.MacawCrucibleRegTypes (MR.RISCV rv)) (MM.LLVMPointerType (G.RVFloatWidth rv)) +f12 = Ctx.natIndex @F12 + +-- | Argument register (AKA 'fa3'). +f13 :: Ctx.Index (MS.MacawCrucibleRegTypes (MR.RISCV rv)) (MM.LLVMPointerType (G.RVFloatWidth rv)) +f13 = Ctx.natIndex @F13 + +-- | Argument register (AKA 'fa4'). +f14 :: Ctx.Index (MS.MacawCrucibleRegTypes (MR.RISCV rv)) (MM.LLVMPointerType (G.RVFloatWidth rv)) +f14 = Ctx.natIndex @F14 + +-- | Argument register (AKA 'fa5'). +f15 :: Ctx.Index (MS.MacawCrucibleRegTypes (MR.RISCV rv)) (MM.LLVMPointerType (G.RVFloatWidth rv)) +f15 = Ctx.natIndex @F15 + +-- | Argument register (AKA 'fa6'). +f16 :: Ctx.Index (MS.MacawCrucibleRegTypes (MR.RISCV rv)) (MM.LLVMPointerType (G.RVFloatWidth rv)) +f16 = Ctx.natIndex @F16 + +-- | Argument register (AKA 'fa7'). +f17 :: Ctx.Index (MS.MacawCrucibleRegTypes (MR.RISCV rv)) (MM.LLVMPointerType (G.RVFloatWidth rv)) +f17 = Ctx.natIndex @F17 + +-- | Callee-saved register (AKA 'fs2'). +f18 :: Ctx.Index (MS.MacawCrucibleRegTypes (MR.RISCV rv)) (MM.LLVMPointerType (G.RVFloatWidth rv)) +f18 = Ctx.natIndex @F18 + +-- | Callee-saved register (AKA 'fs3'). +f19 :: Ctx.Index (MS.MacawCrucibleRegTypes (MR.RISCV rv)) (MM.LLVMPointerType (G.RVFloatWidth rv)) +f19 = Ctx.natIndex @F19 + +-- | Callee-saved register (AKA 'fs4'). +f20 :: Ctx.Index (MS.MacawCrucibleRegTypes (MR.RISCV rv)) (MM.LLVMPointerType (G.RVFloatWidth rv)) +f20 = Ctx.natIndex @F20 + +-- | Callee-saved register (AKA 'fs5'). +f21 :: Ctx.Index (MS.MacawCrucibleRegTypes (MR.RISCV rv)) (MM.LLVMPointerType (G.RVFloatWidth rv)) +f21 = Ctx.natIndex @F21 + +-- | Callee-saved register (AKA 'fs6'). +f22 :: Ctx.Index (MS.MacawCrucibleRegTypes (MR.RISCV rv)) (MM.LLVMPointerType (G.RVFloatWidth rv)) +f22 = Ctx.natIndex @F22 + +-- | Callee-saved register (AKA 'fs7'). +f23 :: Ctx.Index (MS.MacawCrucibleRegTypes (MR.RISCV rv)) (MM.LLVMPointerType (G.RVFloatWidth rv)) +f23 = Ctx.natIndex @F23 + +-- | Callee-saved register (AKA 'fs8'). +f24 :: Ctx.Index (MS.MacawCrucibleRegTypes (MR.RISCV rv)) (MM.LLVMPointerType (G.RVFloatWidth rv)) +f24 = Ctx.natIndex @F24 + +-- | Callee-saved register (AKA 'fs9'). +f25 :: Ctx.Index (MS.MacawCrucibleRegTypes (MR.RISCV rv)) (MM.LLVMPointerType (G.RVFloatWidth rv)) +f25 = Ctx.natIndex @F25 + +-- | Callee-saved register (AKA 'fs10'). +f26 :: Ctx.Index (MS.MacawCrucibleRegTypes (MR.RISCV rv)) (MM.LLVMPointerType (G.RVFloatWidth rv)) +f26 = Ctx.natIndex @F26 + +-- | Callee-saved register (AKA 'fs11'). +f27 :: Ctx.Index (MS.MacawCrucibleRegTypes (MR.RISCV rv)) (MM.LLVMPointerType (G.RVFloatWidth rv)) +f27 = Ctx.natIndex @F27 + +-- | Temporary register (AKA 'ft8'). +f28 :: Ctx.Index (MS.MacawCrucibleRegTypes (MR.RISCV rv)) (MM.LLVMPointerType (G.RVFloatWidth rv)) +f28 = Ctx.natIndex @F28 + +-- | Temporary register (AKA 'ft9'). +f29 :: Ctx.Index (MS.MacawCrucibleRegTypes (MR.RISCV rv)) (MM.LLVMPointerType (G.RVFloatWidth rv)) +f29 = Ctx.natIndex @F29 + +-- | Temporary register (AKA 'ft10'). +f30 :: Ctx.Index (MS.MacawCrucibleRegTypes (MR.RISCV rv)) (MM.LLVMPointerType (G.RVFloatWidth rv)) +f30 = Ctx.natIndex @F30 + +-- | Temporary register (AKA 'ft11'). +f31 :: Ctx.Index (MS.MacawCrucibleRegTypes (MR.RISCV rv)) (MM.LLVMPointerType (G.RVFloatWidth rv)) +f31 = Ctx.natIndex @F31 + +mvendorid :: Ctx.Index (MS.MacawCrucibleRegTypes (MR.RISCV rv)) (MM.LLVMPointerType (G.RVWidth rv)) +mvendorid = Ctx.natIndex @MVendorID + +marchid :: Ctx.Index (MS.MacawCrucibleRegTypes (MR.RISCV rv)) (MM.LLVMPointerType (G.RVWidth rv)) +marchid = Ctx.natIndex @MArchID + +mimpid :: Ctx.Index (MS.MacawCrucibleRegTypes (MR.RISCV rv)) (MM.LLVMPointerType (G.RVWidth rv)) +mimpid = Ctx.natIndex @MImpID + +mhartid :: Ctx.Index (MS.MacawCrucibleRegTypes (MR.RISCV rv)) (MM.LLVMPointerType (G.RVWidth rv)) +mhartid = Ctx.natIndex @MHartID + +mstatus :: Ctx.Index (MS.MacawCrucibleRegTypes (MR.RISCV rv)) (MM.LLVMPointerType (G.RVWidth rv)) +mstatus = Ctx.natIndex @MStatus + +misa :: Ctx.Index (MS.MacawCrucibleRegTypes (MR.RISCV rv)) (MM.LLVMPointerType (G.RVWidth rv)) +misa = Ctx.natIndex @MISA + +medeleg :: Ctx.Index (MS.MacawCrucibleRegTypes (MR.RISCV rv)) (MM.LLVMPointerType (G.RVWidth rv)) +medeleg = Ctx.natIndex @MEDeleg + +mideleg :: Ctx.Index (MS.MacawCrucibleRegTypes (MR.RISCV rv)) (MM.LLVMPointerType (G.RVWidth rv)) +mideleg = Ctx.natIndex @MIDeleg + +mie :: Ctx.Index (MS.MacawCrucibleRegTypes (MR.RISCV rv)) (MM.LLVMPointerType (G.RVWidth rv)) +mie = Ctx.natIndex @MIE + +mtvec :: Ctx.Index (MS.MacawCrucibleRegTypes (MR.RISCV rv)) (MM.LLVMPointerType (G.RVWidth rv)) +mtvec = Ctx.natIndex @MTVec + +mcounteren :: Ctx.Index (MS.MacawCrucibleRegTypes (MR.RISCV rv)) (MM.LLVMPointerType (G.RVWidth rv)) +mcounteren = Ctx.natIndex @MCounterEn + +mscratch :: Ctx.Index (MS.MacawCrucibleRegTypes (MR.RISCV rv)) (MM.LLVMPointerType (G.RVWidth rv)) +mscratch = Ctx.natIndex @MScratch + +mepc :: Ctx.Index (MS.MacawCrucibleRegTypes (MR.RISCV rv)) (MM.LLVMPointerType (G.RVWidth rv)) +mepc = Ctx.natIndex @MEPC + +mcause :: Ctx.Index (MS.MacawCrucibleRegTypes (MR.RISCV rv)) (MM.LLVMPointerType (G.RVWidth rv)) +mcause = Ctx.natIndex @MCause + +mtval :: Ctx.Index (MS.MacawCrucibleRegTypes (MR.RISCV rv)) (MM.LLVMPointerType (G.RVWidth rv)) +mtval = Ctx.natIndex @MTVal + +mip :: Ctx.Index (MS.MacawCrucibleRegTypes (MR.RISCV rv)) (MM.LLVMPointerType (G.RVWidth rv)) +mip = Ctx.natIndex @MIP + +mcycle :: Ctx.Index (MS.MacawCrucibleRegTypes (MR.RISCV rv)) (MM.LLVMPointerType (G.RVWidth rv)) +mcycle = Ctx.natIndex @MCycle + +minstret :: Ctx.Index (MS.MacawCrucibleRegTypes (MR.RISCV rv)) (MM.LLVMPointerType (G.RVWidth rv)) +minstret = Ctx.natIndex @MInstRet + +mcycleh :: Ctx.Index (MS.MacawCrucibleRegTypes (MR.RISCV rv)) (MM.LLVMPointerType (G.RVWidth rv)) +mcycleh = Ctx.natIndex @MCycleh + +minstreth :: Ctx.Index (MS.MacawCrucibleRegTypes (MR.RISCV rv)) (MM.LLVMPointerType (G.RVWidth rv)) +minstreth = Ctx.natIndex @MInstReth + +frm :: Ctx.Index (MS.MacawCrucibleRegTypes (MR.RISCV rv)) (MM.LLVMPointerType (G.RVWidth rv)) +frm = Ctx.natIndex @FRm + +fflags :: Ctx.Index (MS.MacawCrucibleRegTypes (MR.RISCV rv)) (MM.LLVMPointerType (G.RVWidth rv)) +fflags = Ctx.natIndex @FFlags + +fcsr :: Ctx.Index (MS.MacawCrucibleRegTypes (MR.RISCV rv)) (MM.LLVMPointerType (G.RVWidth rv)) +fcsr = Ctx.natIndex @FCSR + +-- | Current privilege level. +priv :: Ctx.Index (MS.MacawCrucibleRegTypes (MR.RISCV rv)) (MM.LLVMPointerType 2) +priv = Ctx.natIndex @Priv + +-- | Trip this if something bad happens. +exc :: Ctx.Index (MS.MacawCrucibleRegTypes (MR.RISCV rv)) C.BoolType +exc = Ctx.natIndex @EXC diff --git a/macaw-riscv-symbolic/tests/Main.hs b/macaw-riscv-symbolic/tests/Main.hs index 0034d97a..d5dbdbf6 100644 --- a/macaw-riscv-symbolic/tests/Main.hs +++ b/macaw-riscv-symbolic/tests/Main.hs @@ -15,6 +15,7 @@ import qualified Data.ElfEdit as Elf import qualified Data.Foldable as F import qualified Data.Map as Map import Data.Maybe ( mapMaybe ) +import qualified Data.Parameterized.Context as Ctx import qualified Data.Parameterized.Classes as PC import qualified Data.Parameterized.Nonce as PN import Data.Parameterized.Some ( Some(..) ) @@ -35,7 +36,8 @@ import qualified Data.Macaw.Discovery as M import qualified Data.Macaw.Symbolic as MS import qualified Data.Macaw.Symbolic.Testing as MST import qualified Data.Macaw.RISCV as MR -import Data.Macaw.RISCV.Symbolic () +import qualified Data.Macaw.RISCV.Symbolic as MRS +import qualified Data.Macaw.RISCV.Symbolic.Regs as MRSR import qualified GRIFT.Types as G import qualified What4.Config as WC import qualified What4.Expr.Builder as WEB @@ -72,6 +74,18 @@ ingredients = TT.includingOptions [ TTO.Option (Proxy @SaveSMT) , TTO.Option (Proxy @SaveMacaw) ] : TT.defaultIngredients +getRegName :: + Ctx.Index (MS.MacawCrucibleRegTypes (MR.RISCV G.RV32GC)) t -> + String +getRegName reg = + case Ctx.intIndex (Ctx.indexVal reg) (Ctx.size regs) of + Just (Some i) -> + let r = regs Ctx.! i + rName = MS.crucGenArchRegName MRS.riscvMacawSymbolicFns r + in show rName + Nothing -> error "impossible" + where regs = MS.crucGenRegAssignment (MRS.riscvMacawSymbolicFns @G.RV32GC) + main :: IO () main = do -- These are pass/fail in that the assertions in the "pass" set are true (and @@ -84,11 +98,167 @@ main = do let passTests mmPreset = TT.testGroup "True assertions" (map (mkSymExTest passRes mmPreset) passTestFilePaths) let failTests mmPreset = TT.testGroup "False assertions" (map (mkSymExTest failRes mmPreset) failTestFilePaths) TT.defaultMainWithIngredients ingredients $ - TT.testGroup "Binary Tests" $ - map (\mmPreset -> - TT.testGroup (MST.describeMemModelPreset mmPreset) - [passTests mmPreset, failTests mmPreset]) - [MST.DefaultMemModel, MST.LazyMemModel] + TT.testGroup "macaw-riscv-symbolic tests" + [ TT.testGroup "Unit tests" + [ TTH.testCase "pc" $ getRegName (MRSR.pc @G.RV32GC) TTH.@?= "r!pc" + , TTH.testCase "ra" $ getRegName (MRSR.ra @G.RV32GC) TTH.@?= "r!ra" + , TTH.testCase "sp" $ getRegName (MRSR.sp @G.RV32GC) TTH.@?= "r!sp" + , TTH.testCase "gp" $ getRegName (MRSR.gp @G.RV32GC) TTH.@?= "r!gp" + , TTH.testCase "tp" $ getRegName (MRSR.tp @G.RV32GC) TTH.@?= "r!tp" + , TTH.testCase "t0" $ getRegName (MRSR.t0 @G.RV32GC) TTH.@?= "r!t0" + , TTH.testCase "t1" $ getRegName (MRSR.t1 @G.RV32GC) TTH.@?= "r!t1" + , TTH.testCase "t2" $ getRegName (MRSR.t2 @G.RV32GC) TTH.@?= "r!t2" + , TTH.testCase "s0" $ getRegName (MRSR.s0 @G.RV32GC) TTH.@?= "r!s0" + , TTH.testCase "s1" $ getRegName (MRSR.s1 @G.RV32GC) TTH.@?= "r!s1" + , TTH.testCase "a0" $ getRegName (MRSR.a0 @G.RV32GC) TTH.@?= "r!a0" + , TTH.testCase "a1" $ getRegName (MRSR.a1 @G.RV32GC) TTH.@?= "r!a1" + , TTH.testCase "a2" $ getRegName (MRSR.a2 @G.RV32GC) TTH.@?= "r!a2" + , TTH.testCase "a3" $ getRegName (MRSR.a3 @G.RV32GC) TTH.@?= "r!a3" + , TTH.testCase "a4" $ getRegName (MRSR.a4 @G.RV32GC) TTH.@?= "r!a4" + , TTH.testCase "a5" $ getRegName (MRSR.a5 @G.RV32GC) TTH.@?= "r!a5" + , TTH.testCase "a6" $ getRegName (MRSR.a6 @G.RV32GC) TTH.@?= "r!a6" + , TTH.testCase "a7" $ getRegName (MRSR.a7 @G.RV32GC) TTH.@?= "r!a7" + , TTH.testCase "s2" $ getRegName (MRSR.s2 @G.RV32GC) TTH.@?= "r!s2" + , TTH.testCase "s3" $ getRegName (MRSR.s3 @G.RV32GC) TTH.@?= "r!s3" + , TTH.testCase "s4" $ getRegName (MRSR.s4 @G.RV32GC) TTH.@?= "r!s4" + , TTH.testCase "s5" $ getRegName (MRSR.s5 @G.RV32GC) TTH.@?= "r!s5" + , TTH.testCase "s6" $ getRegName (MRSR.s6 @G.RV32GC) TTH.@?= "r!s6" + , TTH.testCase "s7" $ getRegName (MRSR.s7 @G.RV32GC) TTH.@?= "r!s7" + , TTH.testCase "s8" $ getRegName (MRSR.s8 @G.RV32GC) TTH.@?= "r!s8" + , TTH.testCase "s9" $ getRegName (MRSR.s9 @G.RV32GC) TTH.@?= "r!s9" + , TTH.testCase "s10" $ getRegName (MRSR.s10 @G.RV32GC) TTH.@?= "r!s10" + , TTH.testCase "s11" $ getRegName (MRSR.s11 @G.RV32GC) TTH.@?= "r!s11" + , TTH.testCase "t3" $ getRegName (MRSR.t3 @G.RV32GC) TTH.@?= "r!t3" + , TTH.testCase "t4" $ getRegName (MRSR.t4 @G.RV32GC) TTH.@?= "r!t4" + , TTH.testCase "t5" $ getRegName (MRSR.t5 @G.RV32GC) TTH.@?= "r!t5" + , TTH.testCase "t6" $ getRegName (MRSR.t6 @G.RV32GC) TTH.@?= "r!t6" + , TTH.testCase "x1" $ getRegName (MRSR.x1 @G.RV32GC) TTH.@?= "r!ra" + , TTH.testCase "x2" $ getRegName (MRSR.x2 @G.RV32GC) TTH.@?= "r!sp" + , TTH.testCase "x3" $ getRegName (MRSR.x3 @G.RV32GC) TTH.@?= "r!gp" + , TTH.testCase "x4" $ getRegName (MRSR.x4 @G.RV32GC) TTH.@?= "r!tp" + , TTH.testCase "x5" $ getRegName (MRSR.x5 @G.RV32GC) TTH.@?= "r!t0" + , TTH.testCase "x6" $ getRegName (MRSR.x6 @G.RV32GC) TTH.@?= "r!t1" + , TTH.testCase "x7" $ getRegName (MRSR.x7 @G.RV32GC) TTH.@?= "r!t2" + , TTH.testCase "x8" $ getRegName (MRSR.x8 @G.RV32GC) TTH.@?= "r!s0" + , TTH.testCase "x9" $ getRegName (MRSR.x9 @G.RV32GC) TTH.@?= "r!s1" + , TTH.testCase "x10" $ getRegName (MRSR.x10 @G.RV32GC) TTH.@?= "r!a0" + , TTH.testCase "x11" $ getRegName (MRSR.x11 @G.RV32GC) TTH.@?= "r!a1" + , TTH.testCase "x12" $ getRegName (MRSR.x12 @G.RV32GC) TTH.@?= "r!a2" + , TTH.testCase "x13" $ getRegName (MRSR.x13 @G.RV32GC) TTH.@?= "r!a3" + , TTH.testCase "x14" $ getRegName (MRSR.x14 @G.RV32GC) TTH.@?= "r!a4" + , TTH.testCase "x15" $ getRegName (MRSR.x15 @G.RV32GC) TTH.@?= "r!a5" + , TTH.testCase "x16" $ getRegName (MRSR.x16 @G.RV32GC) TTH.@?= "r!a6" + , TTH.testCase "x17" $ getRegName (MRSR.x17 @G.RV32GC) TTH.@?= "r!a7" + , TTH.testCase "x18" $ getRegName (MRSR.x18 @G.RV32GC) TTH.@?= "r!s2" + , TTH.testCase "x19" $ getRegName (MRSR.x19 @G.RV32GC) TTH.@?= "r!s3" + , TTH.testCase "x20" $ getRegName (MRSR.x20 @G.RV32GC) TTH.@?= "r!s4" + , TTH.testCase "x21" $ getRegName (MRSR.x21 @G.RV32GC) TTH.@?= "r!s5" + , TTH.testCase "x22" $ getRegName (MRSR.x22 @G.RV32GC) TTH.@?= "r!s6" + , TTH.testCase "x23" $ getRegName (MRSR.x23 @G.RV32GC) TTH.@?= "r!s7" + , TTH.testCase "x24" $ getRegName (MRSR.x24 @G.RV32GC) TTH.@?= "r!s8" + , TTH.testCase "x25" $ getRegName (MRSR.x25 @G.RV32GC) TTH.@?= "r!s9" + , TTH.testCase "x26" $ getRegName (MRSR.x26 @G.RV32GC) TTH.@?= "r!s10" + , TTH.testCase "x27" $ getRegName (MRSR.x27 @G.RV32GC) TTH.@?= "r!s11" + , TTH.testCase "x28" $ getRegName (MRSR.x28 @G.RV32GC) TTH.@?= "r!t3" + , TTH.testCase "x29" $ getRegName (MRSR.x29 @G.RV32GC) TTH.@?= "r!t4" + , TTH.testCase "x30" $ getRegName (MRSR.x30 @G.RV32GC) TTH.@?= "r!t5" + , TTH.testCase "x31" $ getRegName (MRSR.x31 @G.RV32GC) TTH.@?= "r!t6" + , TTH.testCase "ft0" $ getRegName (MRSR.ft0 @G.RV32GC) TTH.@?= "r!ft0" + , TTH.testCase "ft1" $ getRegName (MRSR.ft1 @G.RV32GC) TTH.@?= "r!ft1" + , TTH.testCase "ft2" $ getRegName (MRSR.ft2 @G.RV32GC) TTH.@?= "r!ft2" + , TTH.testCase "ft3" $ getRegName (MRSR.ft3 @G.RV32GC) TTH.@?= "r!ft3" + , TTH.testCase "ft4" $ getRegName (MRSR.ft4 @G.RV32GC) TTH.@?= "r!ft4" + , TTH.testCase "ft5" $ getRegName (MRSR.ft5 @G.RV32GC) TTH.@?= "r!ft5" + , TTH.testCase "ft6" $ getRegName (MRSR.ft6 @G.RV32GC) TTH.@?= "r!ft6" + , TTH.testCase "ft7" $ getRegName (MRSR.ft7 @G.RV32GC) TTH.@?= "r!ft7" + , TTH.testCase "fs0" $ getRegName (MRSR.fs0 @G.RV32GC) TTH.@?= "r!fs0" + , TTH.testCase "fs1" $ getRegName (MRSR.fs1 @G.RV32GC) TTH.@?= "r!fs1" + , TTH.testCase "fa0" $ getRegName (MRSR.fa0 @G.RV32GC) TTH.@?= "r!fa0" + , TTH.testCase "fa1" $ getRegName (MRSR.fa1 @G.RV32GC) TTH.@?= "r!fa1" + , TTH.testCase "fa2" $ getRegName (MRSR.fa2 @G.RV32GC) TTH.@?= "r!fa2" + , TTH.testCase "fa3" $ getRegName (MRSR.fa3 @G.RV32GC) TTH.@?= "r!fa3" + , TTH.testCase "fa4" $ getRegName (MRSR.fa4 @G.RV32GC) TTH.@?= "r!fa4" + , TTH.testCase "fa5" $ getRegName (MRSR.fa5 @G.RV32GC) TTH.@?= "r!fa5" + , TTH.testCase "fa6" $ getRegName (MRSR.fa6 @G.RV32GC) TTH.@?= "r!fa6" + , TTH.testCase "fa7" $ getRegName (MRSR.fa7 @G.RV32GC) TTH.@?= "r!fa7" + , TTH.testCase "fs2" $ getRegName (MRSR.fs2 @G.RV32GC) TTH.@?= "r!fs2" + , TTH.testCase "fs3" $ getRegName (MRSR.fs3 @G.RV32GC) TTH.@?= "r!fs3" + , TTH.testCase "fs4" $ getRegName (MRSR.fs4 @G.RV32GC) TTH.@?= "r!fs4" + , TTH.testCase "fs5" $ getRegName (MRSR.fs5 @G.RV32GC) TTH.@?= "r!fs5" + , TTH.testCase "fs6" $ getRegName (MRSR.fs6 @G.RV32GC) TTH.@?= "r!fs6" + , TTH.testCase "fs7" $ getRegName (MRSR.fs7 @G.RV32GC) TTH.@?= "r!fs7" + , TTH.testCase "fs8" $ getRegName (MRSR.fs8 @G.RV32GC) TTH.@?= "r!fs8" + , TTH.testCase "fs9" $ getRegName (MRSR.fs9 @G.RV32GC) TTH.@?= "r!fs9" + , TTH.testCase "fs10" $ getRegName (MRSR.fs10 @G.RV32GC) TTH.@?= "r!fs10" + , TTH.testCase "fs11" $ getRegName (MRSR.fs11 @G.RV32GC) TTH.@?= "r!fs11" + , TTH.testCase "ft8" $ getRegName (MRSR.ft8 @G.RV32GC) TTH.@?= "r!ft8" + , TTH.testCase "ft9" $ getRegName (MRSR.ft9 @G.RV32GC) TTH.@?= "r!ft9" + , TTH.testCase "ft10" $ getRegName (MRSR.ft10 @G.RV32GC) TTH.@?= "r!ft10" + , TTH.testCase "ft11" $ getRegName (MRSR.ft11 @G.RV32GC) TTH.@?= "r!ft11" + , TTH.testCase "f0" $ getRegName (MRSR.f0 @G.RV32GC) TTH.@?= "r!ft0" + , TTH.testCase "f1" $ getRegName (MRSR.f1 @G.RV32GC) TTH.@?= "r!ft1" + , TTH.testCase "f2" $ getRegName (MRSR.f2 @G.RV32GC) TTH.@?= "r!ft2" + , TTH.testCase "f3" $ getRegName (MRSR.f3 @G.RV32GC) TTH.@?= "r!ft3" + , TTH.testCase "f4" $ getRegName (MRSR.f4 @G.RV32GC) TTH.@?= "r!ft4" + , TTH.testCase "f5" $ getRegName (MRSR.f5 @G.RV32GC) TTH.@?= "r!ft5" + , TTH.testCase "f6" $ getRegName (MRSR.f6 @G.RV32GC) TTH.@?= "r!ft6" + , TTH.testCase "f7" $ getRegName (MRSR.f7 @G.RV32GC) TTH.@?= "r!ft7" + , TTH.testCase "f8" $ getRegName (MRSR.f8 @G.RV32GC) TTH.@?= "r!fs0" + , TTH.testCase "f9" $ getRegName (MRSR.f9 @G.RV32GC) TTH.@?= "r!fs1" + , TTH.testCase "f10" $ getRegName (MRSR.f10 @G.RV32GC) TTH.@?= "r!fa0" + , TTH.testCase "f11" $ getRegName (MRSR.f11 @G.RV32GC) TTH.@?= "r!fa1" + , TTH.testCase "f12" $ getRegName (MRSR.f12 @G.RV32GC) TTH.@?= "r!fa2" + , TTH.testCase "f13" $ getRegName (MRSR.f13 @G.RV32GC) TTH.@?= "r!fa3" + , TTH.testCase "f14" $ getRegName (MRSR.f14 @G.RV32GC) TTH.@?= "r!fa4" + , TTH.testCase "f15" $ getRegName (MRSR.f15 @G.RV32GC) TTH.@?= "r!fa5" + , TTH.testCase "f16" $ getRegName (MRSR.f16 @G.RV32GC) TTH.@?= "r!fa6" + , TTH.testCase "f17" $ getRegName (MRSR.f17 @G.RV32GC) TTH.@?= "r!fa7" + , TTH.testCase "f18" $ getRegName (MRSR.f18 @G.RV32GC) TTH.@?= "r!fs2" + , TTH.testCase "f19" $ getRegName (MRSR.f19 @G.RV32GC) TTH.@?= "r!fs3" + , TTH.testCase "f20" $ getRegName (MRSR.f20 @G.RV32GC) TTH.@?= "r!fs4" + , TTH.testCase "f21" $ getRegName (MRSR.f21 @G.RV32GC) TTH.@?= "r!fs5" + , TTH.testCase "f22" $ getRegName (MRSR.f22 @G.RV32GC) TTH.@?= "r!fs6" + , TTH.testCase "f23" $ getRegName (MRSR.f23 @G.RV32GC) TTH.@?= "r!fs7" + , TTH.testCase "f24" $ getRegName (MRSR.f24 @G.RV32GC) TTH.@?= "r!fs8" + , TTH.testCase "f25" $ getRegName (MRSR.f25 @G.RV32GC) TTH.@?= "r!fs9" + , TTH.testCase "f26" $ getRegName (MRSR.f26 @G.RV32GC) TTH.@?= "r!fs10" + , TTH.testCase "f27" $ getRegName (MRSR.f27 @G.RV32GC) TTH.@?= "r!fs11" + , TTH.testCase "f28" $ getRegName (MRSR.f28 @G.RV32GC) TTH.@?= "r!ft8" + , TTH.testCase "f29" $ getRegName (MRSR.f29 @G.RV32GC) TTH.@?= "r!ft9" + , TTH.testCase "f30" $ getRegName (MRSR.f30 @G.RV32GC) TTH.@?= "r!ft10" + , TTH.testCase "f31" $ getRegName (MRSR.f31 @G.RV32GC) TTH.@?= "r!ft11" + , TTH.testCase "mvendorid" $ getRegName (MRSR.mvendorid @G.RV32GC) TTH.@?= "r!MVendorID" + , TTH.testCase "marchid" $ getRegName (MRSR.marchid @G.RV32GC) TTH.@?= "r!MArchID" + , TTH.testCase "mimpid" $ getRegName (MRSR.mimpid @G.RV32GC) TTH.@?= "r!MImpID" + , TTH.testCase "mhartid" $ getRegName (MRSR.mhartid @G.RV32GC) TTH.@?= "r!MHartID" + , TTH.testCase "mstatus" $ getRegName (MRSR.mstatus @G.RV32GC) TTH.@?= "r!MStatus" + , TTH.testCase "misa" $ getRegName (MRSR.misa @G.RV32GC) TTH.@?= "r!MISA" + , TTH.testCase "medeleg" $ getRegName (MRSR.medeleg @G.RV32GC) TTH.@?= "r!MEDeleg" + , TTH.testCase "mideleg" $ getRegName (MRSR.mideleg @G.RV32GC) TTH.@?= "r!MIDeleg" + , TTH.testCase "mie" $ getRegName (MRSR.mie @G.RV32GC) TTH.@?= "r!MIE" + , TTH.testCase "mtvec" $ getRegName (MRSR.mtvec @G.RV32GC) TTH.@?= "r!MTVec" + , TTH.testCase "mcounteren" $ getRegName (MRSR.mcounteren @G.RV32GC) TTH.@?= "r!MCounterEn" + , TTH.testCase "mscratch" $ getRegName (MRSR.mscratch @G.RV32GC) TTH.@?= "r!MScratch" + , TTH.testCase "mepc" $ getRegName (MRSR.mepc @G.RV32GC) TTH.@?= "r!MEPC" + , TTH.testCase "mcause" $ getRegName (MRSR.mcause @G.RV32GC) TTH.@?= "r!MCause" + , TTH.testCase "mtval" $ getRegName (MRSR.mtval @G.RV32GC) TTH.@?= "r!MTVal" + , TTH.testCase "mip" $ getRegName (MRSR.mip @G.RV32GC) TTH.@?= "r!MIP" + , TTH.testCase "mcycle" $ getRegName (MRSR.mcycle @G.RV32GC) TTH.@?= "r!MCycle" + , TTH.testCase "minstret" $ getRegName (MRSR.minstret @G.RV32GC) TTH.@?= "r!MInstRet" + , TTH.testCase "mcycleh" $ getRegName (MRSR.mcycleh @G.RV32GC) TTH.@?= "r!MCycleh" + , TTH.testCase "minstreth" $ getRegName (MRSR.minstreth @G.RV32GC) TTH.@?= "r!MInstReth" + , TTH.testCase "frm" $ getRegName (MRSR.frm @G.RV32GC) TTH.@?= "r!FRm" + , TTH.testCase "fflags" $ getRegName (MRSR.fflags @G.RV32GC) TTH.@?= "r!FFlags" + , TTH.testCase "fcsr" $ getRegName (MRSR.fcsr @G.RV32GC) TTH.@?= "r!FCSR" + , TTH.testCase "priv" $ getRegName (MRSR.priv @G.RV32GC) TTH.@?= "r!priv" + , TTH.testCase "exc" $ getRegName (MRSR.exc @G.RV32GC) TTH.@?= "r!exc" + ] + , TT.testGroup "Binary Tests" $ + map (\mmPreset -> + TT.testGroup (MST.describeMemModelPreset mmPreset) + [passTests mmPreset, failTests mmPreset]) + [MST.DefaultMemModel, MST.LazyMemModel] + ] hasTestPrefix :: Some (M.DiscoveryFunInfo arch) -> Maybe (BS8.ByteString, Some (M.DiscoveryFunInfo arch)) hasTestPrefix (Some dfi) = do