libriscv (empty) → 0.1.0.0

raw patch · 33 files changed

+2608/−0 lines, 33 filesdep +arraydep +basedep +bv

Dependencies added: array, base, bv, bytestring, containers, exceptions, extra, file-embed, filepath, freer-simple, libriscv, melf, optparse-applicative, parameterized-utils, tasty, tasty-hunit, template-haskell, transformers, yaml

Files

LICENSE.txt +19/−0
app/Main.hs +65/−0
data/instr_dict.yaml +478/−0
internal/LibRISCV/Internal/Decoder/Generator.hs +200/−0
internal/LibRISCV/Internal/Decoder/Instruction.hs +61/−0
internal/LibRISCV/Internal/Decoder/Opcodes.hs +9/−0
internal/LibRISCV/Internal/Decoder/YamlParser.hs +18/−0
lib/LibRISCV.hs +28/−0
lib/LibRISCV/CmdLine.hs +51/−0
lib/LibRISCV/Effects/Decoding/Default/Interpreter.hs +54/−0
lib/LibRISCV/Effects/Decoding/Language.hs +34/−0
lib/LibRISCV/Effects/Expressions/Default/Interpreter.hs +53/−0
lib/LibRISCV/Effects/Expressions/Expr.hs +32/−0
lib/LibRISCV/Effects/Expressions/Generator.hs +66/−0
lib/LibRISCV/Effects/Expressions/Language.hs +70/−0
lib/LibRISCV/Effects/Expressions/Type.hs +38/−0
lib/LibRISCV/Effects/Logging/Default/Interpreter.hs +27/−0
lib/LibRISCV/Effects/Logging/Language.hs +21/−0
lib/LibRISCV/Effects/Operations/Default/Interpreter.hs +69/−0
lib/LibRISCV/Effects/Operations/Default/Machine/Memory.hs +161/−0
lib/LibRISCV/Effects/Operations/Default/Machine/Register.hs +65/−0
lib/LibRISCV/Effects/Operations/Language.hs +34/−0
lib/LibRISCV/Loader.hs +87/−0
lib/LibRISCV/Semantics.hs +13/−0
lib/LibRISCV/Semantics/Default.hs +97/−0
lib/LibRISCV/Semantics/RV32_I/Default.hs +38/−0
lib/LibRISCV/Semantics/RV_I/Default.hs +212/−0
lib/LibRISCV/Semantics/RV_M/Default.hs +112/−0
lib/LibRISCV/Semantics/Utils.hs +75/−0
libriscv.cabal +141/−0
test/ArchStateTest.hs +90/−0
test/DecoderTest.hs +75/−0
test/Main.hs +15/−0

+ LICENSE.txt view

@@ -0,0 +1,19 @@+Copyright (c) 2022-2023 Group of Computer Architecture, University of Bremen <riscv@systemc-verification.org>++Permission is hereby granted, free of charge, to any person obtaining a copy+of this software and associated documentation files (the "Software"), to deal+in the Software without restriction, including without limitation the rights+to use, copy, modify, merge, publish, distribute, sublicense, and/or sell+copies of the Software, and to permit persons to whom the Software is+furnished to do so, subject to the following conditions:++The above copyright notice and this permission notice shall be included in all+copies or substantial portions of the Software.++THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR+IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,+FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE+AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER+LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,+OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE+SOFTWARE.

+ app/Main.hs view

@@ -0,0 +1,65 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE TypeApplications #-}++module Main where++import Control.Monad (when)+import Control.Monad.Freer+import Data.BitVector+import Data.IORef (newIORef)+import Data.Word (Word32)+import LibRISCV (RegIdx (SP), align)+import LibRISCV.CmdLine+import LibRISCV.Effects.Decoding.Default.Interpreter (+    defaultDecoding,+ )+import LibRISCV.Effects.Expressions.Default.Interpreter (defaultEval, evalE)+import qualified LibRISCV.Effects.Expressions.Expr as E+import LibRISCV.Effects.Logging.Default.Interpreter (+    defaultLogging,+    noLogging,+ )+import LibRISCV.Effects.Operations.Default.Interpreter (+    defaultInstructions,+    dumpState,+    getMem,+    mkArchState,+ )+import LibRISCV.Effects.Operations.Default.Machine.Memory (storeByteString)+import LibRISCV.Loader+import LibRISCV.Semantics (buildAST, writeRegister)+import Options.Applicative++main' :: BasicArgs -> IO ()+main' (BasicArgs memAddr memSize trace putReg fp) = do+    state <- mkArchState memAddr memSize++    elf <- readElf fp+    loadElf elf $ storeByteString fromIntegral (getMem state)+    entry <- startAddr elf++    instRef <- newIORef (0 :: Word32)+    let+        initalSP = align (memAddr + memSize - 1)+        evalEnv = ((== 1), evalE)+        interpreter =+            interpretM (defaultInstructions state)+                . interpretM (defaultEval evalEnv)+                . interpretM (defaultDecoding @BV instRef)+                . interpretM (if trace then defaultLogging else noLogging)+    runM $ interpreter $ do+        writeRegister (bitVec 32 $ fromEnum SP) (E.FromInt 32 $ fromIntegral initalSP)+        buildAST @32 (bitVec 32 entry)++    when putReg $+        dumpState state++main :: IO ()+main = main' =<< execParser opts+  where+    opts =+        info+            (basicArgs <**> helper)+            ( fullDesc+                <> progDesc "Concrete execution of RV32I machine code"+            )

+ data/instr_dict.yaml view

@@ -0,0 +1,478 @@+add:+  encoding: 0000000----------000-----0110011+  extension:+  - rv_i+  mask: '0xfe00707f'+  match: '0x33'+  variable_fields:+  - rd+  - rs1+  - rs2+addi:+  encoding: '-----------------000-----0010011'+  extension:+  - rv_i+  mask: '0x707f'+  match: '0x13'+  variable_fields:+  - rd+  - rs1+  - imm12+and:+  encoding: 0000000----------111-----0110011+  extension:+  - rv_i+  mask: '0xfe00707f'+  match: '0x7033'+  variable_fields:+  - rd+  - rs1+  - rs2+andi:+  encoding: '-----------------111-----0010011'+  extension:+  - rv_i+  mask: '0x707f'+  match: '0x7013'+  variable_fields:+  - rd+  - rs1+  - imm12+auipc:+  encoding: '-------------------------0010111'+  extension:+  - rv_i+  mask: '0x7f'+  match: '0x17'+  variable_fields:+  - rd+  - imm20+beq:+  encoding: '-----------------000-----1100011'+  extension:+  - rv_i+  mask: '0x707f'+  match: '0x63'+  variable_fields:+  - bimm12hi+  - rs1+  - rs2+  - bimm12lo+bge:+  encoding: '-----------------101-----1100011'+  extension:+  - rv_i+  mask: '0x707f'+  match: '0x5063'+  variable_fields:+  - bimm12hi+  - rs1+  - rs2+  - bimm12lo+bgeu:+  encoding: '-----------------111-----1100011'+  extension:+  - rv_i+  mask: '0x707f'+  match: '0x7063'+  variable_fields:+  - bimm12hi+  - rs1+  - rs2+  - bimm12lo+blt:+  encoding: '-----------------100-----1100011'+  extension:+  - rv_i+  mask: '0x707f'+  match: '0x4063'+  variable_fields:+  - bimm12hi+  - rs1+  - rs2+  - bimm12lo+bltu:+  encoding: '-----------------110-----1100011'+  extension:+  - rv_i+  mask: '0x707f'+  match: '0x6063'+  variable_fields:+  - bimm12hi+  - rs1+  - rs2+  - bimm12lo+bne:+  encoding: '-----------------001-----1100011'+  extension:+  - rv_i+  mask: '0x707f'+  match: '0x1063'+  variable_fields:+  - bimm12hi+  - rs1+  - rs2+  - bimm12lo+ebreak:+  encoding: '00000000000100000000000001110011'+  extension:+  - rv_i+  mask: '0xffffffff'+  match: '0x100073'+  variable_fields: []+ecall:+  encoding: '00000000000000000000000001110011'+  extension:+  - rv_i+  mask: '0xffffffff'+  match: '0x73'+  variable_fields: []+fence:+  encoding: '-----------------000-----0001111'+  extension:+  - rv_i+  mask: '0x707f'+  match: '0xf'+  variable_fields: []+jal:+  encoding: '-------------------------1101111'+  extension:+  - rv_i+  mask: '0x7f'+  match: '0x6f'+  variable_fields:+  - rd+  - jimm20+jalr:+  encoding: '-----------------000-----1100111'+  extension:+  - rv_i+  mask: '0x707f'+  match: '0x67'+  variable_fields:+  - rd+  - rs1+  - imm12+lb:+  encoding: '-----------------000-----0000011'+  extension:+  - rv_i+  mask: '0x707f'+  match: '0x3'+  variable_fields:+  - rd+  - rs1+  - imm12+lbu:+  encoding: '-----------------100-----0000011'+  extension:+  - rv_i+  mask: '0x707f'+  match: '0x4003'+  variable_fields:+  - rd+  - rs1+  - imm12+lh:+  encoding: '-----------------001-----0000011'+  extension:+  - rv_i+  mask: '0x707f'+  match: '0x1003'+  variable_fields:+  - rd+  - rs1+  - imm12+lhu:+  encoding: '-----------------101-----0000011'+  extension:+  - rv_i+  mask: '0x707f'+  match: '0x5003'+  variable_fields:+  - rd+  - rs1+  - imm12+lui:+  encoding: '-------------------------0110111'+  extension:+  - rv_i+  mask: '0x7f'+  match: '0x37'+  variable_fields:+  - rd+  - imm20+lw:+  encoding: '-----------------010-----0000011'+  extension:+  - rv_i+  mask: '0x707f'+  match: '0x2003'+  variable_fields:+  - rd+  - rs1+  - imm12+or:+  encoding: 0000000----------110-----0110011+  extension:+  - rv_i+  mask: '0xfe00707f'+  match: '0x6033'+  variable_fields:+  - rd+  - rs1+  - rs2+ori:+  encoding: '-----------------110-----0010011'+  extension:+  - rv_i+  mask: '0x707f'+  match: '0x6013'+  variable_fields:+  - rd+  - rs1+  - imm12+sb:+  encoding: '-----------------000-----0100011'+  extension:+  - rv_i+  mask: '0x707f'+  match: '0x23'+  variable_fields:+  - imm12hi+  - rs1+  - rs2+  - imm12lo+sh:+  encoding: '-----------------001-----0100011'+  extension:+  - rv_i+  mask: '0x707f'+  match: '0x1023'+  variable_fields:+  - imm12hi+  - rs1+  - rs2+  - imm12lo+sll:+  encoding: 0000000----------001-----0110011+  extension:+  - rv_i+  mask: '0xfe00707f'+  match: '0x1033'+  variable_fields:+  - rd+  - rs1+  - rs2+slli:+  encoding: 0000000----------001-----0010011+  extension:+  - rv32_i+  mask: '0xfe00707f'+  match: '0x1013'+  variable_fields:+  - rd+  - rs1+  - shamtw+slt:+  encoding: 0000000----------010-----0110011+  extension:+  - rv_i+  mask: '0xfe00707f'+  match: '0x2033'+  variable_fields:+  - rd+  - rs1+  - rs2+slti:+  encoding: '-----------------010-----0010011'+  extension:+  - rv_i+  mask: '0x707f'+  match: '0x2013'+  variable_fields:+  - rd+  - rs1+  - imm12+sltiu:+  encoding: '-----------------011-----0010011'+  extension:+  - rv_i+  mask: '0x707f'+  match: '0x3013'+  variable_fields:+  - rd+  - rs1+  - imm12+sltu:+  encoding: 0000000----------011-----0110011+  extension:+  - rv_i+  mask: '0xfe00707f'+  match: '0x3033'+  variable_fields:+  - rd+  - rs1+  - rs2+sra:+  encoding: 0100000----------101-----0110011+  extension:+  - rv_i+  mask: '0xfe00707f'+  match: '0x40005033'+  variable_fields:+  - rd+  - rs1+  - rs2+srai:+  encoding: 0100000----------101-----0010011+  extension:+  - rv32_i+  mask: '0xfe00707f'+  match: '0x40005013'+  variable_fields:+  - rd+  - rs1+  - shamtw+srl:+  encoding: 0000000----------101-----0110011+  extension:+  - rv_i+  mask: '0xfe00707f'+  match: '0x5033'+  variable_fields:+  - rd+  - rs1+  - rs2+srli:+  encoding: 0000000----------101-----0010011+  extension:+  - rv32_i+  mask: '0xfe00707f'+  match: '0x5013'+  variable_fields:+  - rd+  - rs1+  - shamtw+sub:+  encoding: 0100000----------000-----0110011+  extension:+  - rv_i+  mask: '0xfe00707f'+  match: '0x40000033'+  variable_fields:+  - rd+  - rs1+  - rs2+sw:+  encoding: '-----------------010-----0100011'+  extension:+  - rv_i+  mask: '0x707f'+  match: '0x2023'+  variable_fields:+  - imm12hi+  - rs1+  - rs2+  - imm12lo+xor:+  encoding: 0000000----------100-----0110011+  extension:+  - rv_i+  mask: '0xfe00707f'+  match: '0x4033'+  variable_fields:+  - rd+  - rs1+  - rs2+xori:+  encoding: '-----------------100-----0010011'+  extension:+  - rv_i+  mask: '0x707f'+  match: '0x4013'+  variable_fields:+  - rd+  - rs1+  - imm12++div:+  encoding: 0000001----------100-----0110011+  extension:+  - rv_m+  mask: '0xfe00707f'+  match: '0x2004033'+  variable_fields:+  - rd+  - rs1+  - rs2+divu:+  encoding: 0000001----------101-----0110011+  extension:+  - rv_m+  mask: '0xfe00707f'+  match: '0x2005033'+  variable_fields:+  - rd+  - rs1+  - rs2+mul:+  encoding: 0000001----------000-----0110011+  extension:+  - rv_m+  mask: '0xfe00707f'+  match: '0x2000033'+  variable_fields:+  - rd+  - rs1+  - rs2+mulh:+  encoding: 0000001----------001-----0110011+  extension:+  - rv_m+  mask: '0xfe00707f'+  match: '0x2001033'+  variable_fields:+  - rd+  - rs1+  - rs2+mulhsu:+  encoding: 0000001----------010-----0110011+  extension:+  - rv_m+  mask: '0xfe00707f'+  match: '0x2002033'+  variable_fields:+  - rd+  - rs1+  - rs2+mulhu:+  encoding: 0000001----------011-----0110011+  extension:+  - rv_m+  mask: '0xfe00707f'+  match: '0x2003033'+  variable_fields:+  - rd+  - rs1+  - rs2+rem:+  encoding: 0000001----------110-----0110011+  extension:+  - rv_m+  mask: '0xfe00707f'+  match: '0x2006033'+  variable_fields:+  - rd+  - rs1+  - rs2+remu:+  encoding: 0000001----------111-----0110011+  extension:+  - rv_m+  mask: '0xfe00707f'+  match: '0x2007033'+  variable_fields:+  - rd+  - rs1+  - rs2

+ internal/LibRISCV/Internal/Decoder/Generator.hs view

@@ -0,0 +1,200 @@+{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE TupleSections #-}++module LibRISCV.Internal.Decoder.Generator where++import Control.Monad (forM)+import Control.Monad.IO.Class (MonadIO, liftIO)+import Data.Bits ((.&.))+import Data.Char (toUpper)+import Data.FileEmbed (makeRelativeToProject)+import Data.List (nub)+import qualified Data.Map.Strict as M+import Data.Maybe (fromJust, isJust)+import Data.Word (Word32)+import Data.Yaml+import Language.Haskell.TH hiding (match)+import LibRISCV.Internal.Decoder.YamlParser++readAndParse :: (MonadIO m) => FilePath -> m [(String, InstructionFields)]+readAndParse filePath = M.toList <$> liftIO (decodeFileThrow filePath)++generateConsts :: [(String, InstructionFields)] -> String -> (InstructionFields -> String) -> Q [Dec]+generateConsts entries suffix f = do+    forM entries $ \(instructionName, fields) -> do+        let+            nameD = mkName $ instructionName <> "_" <> suffix+            valE = read $ f fields+        pure $+            ValD+                (VarP nameD)+                (NormalB $ LitE $ IntegerL valE)+                []++generateExtType :: [(String, InstructionFields)] -> Q [Dec]+generateExtType entries = do+    let+        byExts =+            M.fromListWith (<>)+                . map (\(x, y) -> (x, [y]))+                . concatMap+                    ( \(inst, fs) ->+                        map (,inst) (extension fs)+                    )+                $ entries+        superType =+            DataD+                []+                (mkName "InstructionType")+                []+                Nothing+                ( NormalC (mkName "InvalidInstruction") []+                    : map+                        ( \ex ->+                            NormalC+                                (mkName $ map toUpper ex)+                                [(Bang NoSourceUnpackedness NoSourceStrictness, ConT (mkName $ map toUpper ex))]+                        )+                        (M.keys byExts)+                )+                [DerivClause Nothing [ConT ''Eq, ConT ''Show]]+    extTypes <- forM (M.toList byExts) $ \(ext, instructions) -> do+        pure $+            DataD+                []+                (mkName $ map toUpper ext)+                []+                Nothing+                (map (\instr -> NormalC (mkName $ map toUpper instr) []) instructions)+                [DerivClause Nothing [ConT ''Eq, ConT ''Show]]++    pure $ extTypes <> [superType]++generateExtDecodeFns :: [(String, InstructionFields)] -> Q [Dec]+generateExtDecodeFns entries = do+    let+        byExts =+            M.fromListWith (<>)+                . map (\(x, y) -> (x, [y]))+                . concatMap+                    ( \(inst, fs) ->+                        map (,inst) (extension fs)+                    )+                $ entries++    sigs <- forM (M.toList byExts) $ \(ex, _) ->+        pure $+            SigD+                (mkName $ "decode_" <> map toUpper ex)+                ( AppT+                    ( AppT+                        ArrowT+                        (ConT ''Word32)+                    )+                    ( AppT+                        (ConT ''Maybe)+                        (ConT $ mkName $ map toUpper ex)+                    )+                )+    defs <- forM (M.toList byExts) $ \(ex, instrs) ->+        pure $+            FunD+                (mkName $ "decode_" <> map toUpper ex)+                [ Clause+                    [VarP (mkName "w")]+                    ( GuardedB $+                        map+                            ( \instr ->+                                ( NormalG $+                                    InfixE+                                        ( Just+                                            ( InfixE+                                                (Just (VarE $ mkName "w"))+                                                (VarE '(.&.))+                                                (Just (VarE $ mkName $ instr <> "_mask"))+                                            )+                                        )+                                        (VarE '(==))+                                        (Just (VarE $ mkName $ instr <> "_match"))+                                , AppE (ConE 'Just) $ ConE $ mkName $ map toUpper instr+                                )+                            )+                            instrs+                            <> [(NormalG (ConE 'True), ConE 'Nothing)]+                    )+                    []+                ]+    pure $ sigs <> defs++generateDecodeFn :: [(String, InstructionFields)] -> Q [Dec]+generateDecodeFn entries = do+    let+        exts =+            map (map toUpper)+                . nub+                . concatMap (extension . snd)+                $ entries+        sig =+            SigD+                (mkName "decode")+                ( AppT+                    ( AppT+                        ArrowT+                        (ConT ''Word32)+                    )+                    (ConT $ mkName "InstructionType")+                )+        def =+            FunD+                (mkName "decode")+                [ Clause+                    [VarP $ mkName "w"]+                    ( GuardedB $+                        map+                            ( \ex ->+                                ( NormalG $+                                    AppE+                                        (VarE 'isJust)+                                        ( AppE+                                            (VarE $ mkName $ "decode_" <> ex)+                                            (VarE $ mkName "w")+                                        )+                                , AppE+                                    (ConE $ mkName ex)+                                    ( AppE+                                        (VarE 'fromJust)+                                        ( AppE+                                            (VarE $ mkName $ "decode_" <> ex)+                                            (VarE $ mkName "w")+                                        )+                                    )+                                )+                            )+                            exts+                            <> [(NormalG (ConE 'True), ConE $ mkName "InvalidInstruction")]+                    )+                    []+                ]+    pure [def, sig]++generateMasks :: [(String, InstructionFields)] -> Q [Dec]+generateMasks entries = generateConsts entries "mask" mask++generateMatches :: [(String, InstructionFields)] -> Q [Dec]+generateMatches entries = generateConsts entries "match" match++generateAll :: [[(String, InstructionFields)] -> Q [Dec]] -> FilePath -> Q [Dec]+generateAll seqs path = do+    entries <- liftIO $ readAndParse path+    concat <$> mapM (\f -> f entries) seqs++generateDefaultDecoder :: Q [Dec]+generateDefaultDecoder =+    makeRelativeToProject "data/instr_dict.yaml"+        >>= generateAll+            [ generateMasks+            , generateMatches+            , generateExtType+            , generateExtDecodeFns+            , generateDecodeFn+            ]

+ internal/LibRISCV/Internal/Decoder/Instruction.hs view

@@ -0,0 +1,61 @@+module LibRISCV.Internal.Decoder.Instruction where++import Data.Bits+import Data.Word++-- Convert to an unsigned word (in two's complement) to a signed number.+fromTwoscomp :: Word32 -> Word32 -> Word32+fromTwoscomp numBits n = fromIntegral $ -(n .&. mask) + (n .&. complement mask)+  where+    mask :: Word32+    mask = 2 ^ (numBits - 1)++-- Extract a bit field from a RISC-V instruction word.+instrField :: Int -> Int -> Word32 -> Word32+instrField start end w = mask start (end + 1) .&. shiftR w start+  where+    -- Create a 32-bit bit mask in the range [start,end-1].+    mask :: Int -> Int -> Word32+    mask start end = complement $ shift (maxBound :: Word32) (end - start)++------------------------------------------------------------------------++immI :: Word32 -> Word32+immI = fromTwoscomp 12 . instrField 20 31++immS :: Word32 -> Word32+immS i =+    fromTwoscomp 12 $+        fromIntegral $+            (instrField 25 31 i `shift` 5) .|. instrField 07 11 i++immU :: Word32 -> Word32+immU i = instrField 12 31 i `shiftL` 12++{- FOURMOLU_DISABLE -}+immB :: Word32 -> Word32+immB i = fromTwoscomp 13 $+         (instrField 31 31 i `shift` 12)+     .|. (instrField 07 07 i `shift` 11)+     .|. (instrField 25 30 i `shift` 05)+     .|. (instrField 08 11 i `shift` 01)++immJ :: Word32 -> Word32+immJ i = fromTwoscomp 21 $+         (instrField 31 31 i `shift` 20)+     .|. (instrField 12 19 i `shift` 12)+     .|. (instrField 20 20 i `shift` 11)+     .|. (instrField 21 30 i `shift` 1)+{- FOURMOLU_ENABLE -}++mkShamt :: Word32 -> Word32+mkShamt = instrField 20 25++mkRs1 :: Word32 -> Word32+mkRs1 = instrField 15 19++mkRs2 :: Word32 -> Word32+mkRs2 = instrField 20 24++mkRd :: Word32 -> Word32+mkRd = instrField 7 11

+ internal/LibRISCV/Internal/Decoder/Opcodes.hs view

@@ -0,0 +1,9 @@+{-# LANGUAGE TemplateHaskell #-}+-- generateDefaultDecoder doesn't generate signatures.+{-# OPTIONS_GHC -Wno-missing-signatures #-}++module LibRISCV.Internal.Decoder.Opcodes where++import LibRISCV.Internal.Decoder.Generator++generateDefaultDecoder

+ internal/LibRISCV/Internal/Decoder/YamlParser.hs view

@@ -0,0 +1,18 @@+{-# LANGUAGE DeriveGeneric #-}++module LibRISCV.Internal.Decoder.YamlParser where++import qualified Data.Map.Strict as M+import Data.Yaml (FromJSON)+import GHC.Generics (Generic)++data InstructionFields = InstructionFields+    { extension :: [String]+    , mask :: String+    , match :: String+    }+    deriving (Eq, Show, Generic)++instance FromJSON InstructionFields++type InstructionEntries = M.Map String InstructionFields

+ lib/LibRISCV.hs view

@@ -0,0 +1,28 @@+{-# LANGUAGE MultiParamTypeClasses #-}++module LibRISCV where++import Data.Ix+import Data.Word++-- | Representation of a 32-bit addresses for RV32.+type Address = Word32++-- | Align an 'Address' on the next word boundary.+align :: Address -> Address+align addr = addr - addr `mod` 4++-- | Type to represent an index for the register file.+--+-- >>> toEnum 12 :: RegIdx+-- A2+-- >>> toEnum 31 :: RegIdx+-- T6+-- >>> fromEnum (minBound :: RegIdx)+-- 0+{- FOURMOLU_DISABLE -}+data RegIdx = Zero | RA | SP | GP | TP | T0 | T1 | T2 | FP+    | S1 | A0 | A1 | A2 | A3 | A4 | A5 | A6 | A7 | S2 | S3+    | S4 | S5 | S6 | S7 | S8 | S9 | S10 | S11 | T3 | T4+    | T5 | T6 deriving (Ord, Eq, Ix, Bounded, Show, Enum, Read)+{- FOURMOLU_ENABLE -}

+ lib/LibRISCV/CmdLine.hs view

@@ -0,0 +1,51 @@+-- | Implementation of common command-line arguments using <https://hackage.haskell.org/package/optparse-applicative  optparse-applicative>.+module LibRISCV.CmdLine where++import Data.Word+import Options.Applicative++-- | t'BasicArgs' can be combined/extended with additional parsers using+-- the '<*>' applicative operator provided by "Options.Applicative".+data BasicArgs = BasicArgs+    { memAddr :: Word32+    -- ^ Start address of the general-purpose memory.+    , memSize :: Word32+    -- ^ Size of the memory in bytes.+    , trace :: Bool+    -- ^ Whether to enable instruction tracing.+    , putRegs :: Bool+    -- ^ Whether to print all register values at the end.+    , file :: String+    -- ^ Path to ELf file which should be executed.+    }++-- TODO: Rename memStart to memSize.++-- | "Options.Applicative" parser for t'BasicArgs'.+basicArgs :: Parser BasicArgs+basicArgs =+    BasicArgs+        <$> option+            auto+            ( long "memory-start"+                <> short 'm'+                <> value 0x10000+            )+        <*> option+            auto+            ( long "memory-size"+                <> short 's'+                <> value (1024 * 1024 * 1) -- 1 MB RAM+                <> help "Size of the memory region"+            )+        <*> switch+            ( long "trace"+                <> short 't'+                <> help "Whether to trace all executed instructions"+            )+        <*> switch+            ( long "registers"+                <> short 'r'+                <> help "Whether to print all register values"+            )+        <*> argument str (metavar "FILE")

+ lib/LibRISCV/Effects/Decoding/Default/Interpreter.hs view

@@ -0,0 +1,54 @@+{-# LANGUAGE GADTs #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE TypeOperators #-}++-- | Provides the default (concrete) interpretation for the decoding effect. This+-- implementation assumes that the 'Decodable' type class can be implemented for+-- the underlying type parameter, that is, it must be possible to convert the+-- type to a fixed-width concrete integer.+module LibRISCV.Effects.Decoding.Default.Interpreter where++import Control.Monad.Freer (type (~>))+import Control.Monad.IO.Class (MonadIO (liftIO))+import Data.BitVector (BV, bitVec)+import Data.Data (Proxy (..))+import Data.IORef (IORef, readIORef, writeIORef)+import Data.Word (Word32)+import LibRISCV.Effects.Decoding.Language (Decoding (..))+import LibRISCV.Internal.Decoder.Instruction (immB, immI, immJ, immS, immU, mkRd, mkRs1, mkRs2, mkShamt)+import LibRISCV.Internal.Decoder.Opcodes (decode)++-- | Decoder state used to implement the stateful 'SetInstr' constructor of the 'Decoding' effect.+type DecoderState = IORef Word32++-- | Type class used to perform conversion from/to a fixed-with concrete integer.+class Decodable a where+    fromWord :: Word32 -> a+    -- ^ Convert from a fixed-with integer to the underlying value type of the interpreter.++    toWord :: a -> Word32+    -- ^ Convert from the underlying value type to a fixed-with integer.++instance Decodable BV where+    fromWord = bitVec 32+    toWord = fromIntegral++-- | Concrete implementation of the decoding effect.+defaultDecoding :: forall v m. (Decodable v, MonadIO m) => DecoderState -> Decoding v ~> m+defaultDecoding instRef =+    let+        decodeAndConvert f = fmap (fromWord . f) . readIORef+     in+        liftIO . \case+            SetInstr v -> writeIORef instRef $ toWord v+            WithInstrType Proxy f -> f . decode <$> readIORef instRef+            DecodeRD -> decodeAndConvert mkRd instRef+            DecodeRS1 -> decodeAndConvert mkRs1 instRef+            DecodeRS2 -> decodeAndConvert mkRs2 instRef+            DecodeImmI -> decodeAndConvert immI instRef+            DecodeImmS -> decodeAndConvert immS instRef+            DecodeImmB -> decodeAndConvert immB instRef+            DecodeImmU -> decodeAndConvert immU instRef+            DecodeImmJ -> decodeAndConvert immJ instRef+            DecodeShamt -> decodeAndConvert mkShamt instRef

+ lib/LibRISCV/Effects/Decoding/Language.hs view

@@ -0,0 +1,34 @@+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE TemplateHaskell #-}++-- | Implements an effect for instruction decoding. Specifically, the effect+-- is only used to describe obtaining of instruction operands. The instruction+-- opcode is determined seperatly using code generated from the existing+-- <https://github.com/riscv/riscv-opcodes riscv-opcodes> tool. The decoding+-- effect is stateful and operates on a current instruction word specified via+-- 'setInstr', thereby avoiding the need to pass the current instruction word+-- to every decoding function.+module LibRISCV.Effects.Decoding.Language where++import Control.Monad.Freer.TH (makeEffect)+import Data.Data (Proxy)+import LibRISCV.Internal.Decoder.Opcodes (InstructionType)++data Decoding v r where+    DecodeRS1 :: Decoding v v+    DecodeRS2 :: Decoding v v+    DecodeRD :: Decoding v v+    DecodeImmI :: Decoding v v+    DecodeImmS :: Decoding v v+    DecodeImmB :: Decoding v v+    DecodeImmU :: Decoding v v+    DecodeImmJ :: Decoding v v+    DecodeShamt :: Decoding v v+    SetInstr :: v -> Decoding v ()+    -- TODO: WithInstrType is only used to determine which Haskell module+    -- provides the semantics for a given instruction. Can we eliminate+    -- the need to do this somehow?+    WithInstrType :: Proxy v -> (InstructionType -> b) -> Decoding v b++makeEffect ''Decoding

+ lib/LibRISCV/Effects/Expressions/Default/Interpreter.hs view

@@ -0,0 +1,53 @@+{-# LANGUAGE GADTs #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TypeOperators #-}++-- | Provides the default (concrete) evaluation of the expression abstraction.+module LibRISCV.Effects.Expressions.Default.Interpreter where++import Control.Monad.Freer (type (~>))+import Control.Monad.IO.Class (MonadIO)+import Data.BitVector (BV, Bits (unsafeShiftL, unsafeShiftR, xor, (.&.), (.|.)), bitVec, extract, signExtend, zeroExtend)+import Data.Bool (bool)+import Data.Int (Int32)+import Data.Word (Word8)+import LibRISCV.Effects.Expressions.Expr (Expr (..))+import LibRISCV.Effects.Expressions.Language (ExprEval (..))++-- | Evaluate an 'Expr' abstraction which encapsulates a concrete 'BV'.+evalE :: Expr BV -> BV+evalE (FromImm a) = a+evalE (FromInt n i) = bitVec n i+evalE (ZExt n e) = zeroExtend n (evalE e)+evalE (SExt n e) = signExtend n (evalE e)+evalE (Extract start len e) = extract (start + (len - 1)) start (evalE e)+evalE (Add e1 e2) = evalE e1 + evalE e2+evalE (Sub e1 e2) =+    fromIntegral $+        (fromIntegral (evalE e1) :: Int32) - fromIntegral (evalE e2)+evalE (Eq e1 e2) = bool 0 1 $ (fromIntegral (evalE e1) :: Int32) == fromIntegral (evalE e2)+evalE (Slt e1 e2) = bool 0 1 $ (fromIntegral (evalE e1) :: Int32) < fromIntegral (evalE e2)+evalE (Sge e1 e2) = bool 0 1 $ (fromIntegral (evalE e1) :: Int32) >= fromIntegral (evalE e2)+evalE (Ult e1 e2) = bool 0 1 $ evalE e1 < evalE e2+evalE (Uge e1 e2) = bool 0 1 $ evalE e1 >= evalE e2+evalE (And e1 e2) = evalE e1 .&. evalE e2+evalE (Or e1 e2) = evalE e1 .|. evalE e2+evalE (Xor e1 e2) = evalE e1 `xor` evalE e2+evalE (LShl e1 e2) = evalE e1 `unsafeShiftL` fromIntegral (fromIntegral (evalE e2) :: Word8)+evalE (LShr e1 e2) = evalE e1 `unsafeShiftR` fromIntegral (fromIntegral (evalE e2) :: Word8)+evalE (AShr e1 e2) = fromIntegral $ (fromIntegral (evalE e1) :: Int32) `unsafeShiftR` fromIntegral (fromIntegral (evalE e2) :: Word8)+evalE (Mul e1 e2) = evalE e1 * evalE e2+evalE (SDiv e1 e2) = fromIntegral $ fromIntegral @_ @Int32 (evalE e1) `quot` fromIntegral (evalE e2)+evalE (SRem e1 e2) = fromIntegral $ fromIntegral @_ @Int32 (evalE e1) `rem` fromIntegral (evalE e2)+evalE (UDiv e1 e2) = evalE e1 `quot` evalE e2+evalE (URem e1 e2) = evalE e1 `rem` evalE e2++-- | Concrete implementation of the 'ExprEval' effect.+defaultEval :: (MonadIO m) => (v -> Bool, Expr v -> v) -> ExprEval v ~> m+defaultEval (pred, evalE) =+    pure . \case+        Eval e -> evalE e+        IsTrue e -> pred $ evalE e+        IsFalse e -> not . pred $ evalE e

+ lib/LibRISCV/Effects/Expressions/Expr.hs view

@@ -0,0 +1,32 @@+{-# LANGUAGE TemplateHaskell #-}+-- generateImmediates doesn't generate signatures.+{-# OPTIONS_GHC -Wno-missing-signatures #-}++-- | Defines the expression abstraction to express arithmetic and logic+-- operations within the formal description of RISC-V instructions. The+-- abstraction is just a non-monadic algebraic data type called 'Expr'.+-- In addition to the the data type definition, this module also provides+-- several smart constructors for utilzing the expression lanuage, these+-- are generated using template-haskell.+module LibRISCV.Effects.Expressions.Expr (+    module LibRISCV.Effects.Expressions.Type,+    module LibRISCV.Effects.Expressions.Expr,+) where++import Data.Function (on)+import LibRISCV.Effects.Expressions.Generator+import LibRISCV.Effects.Expressions.Type++-- | Extract shamt value from an expression (lower 5 bits).+regShamt :: Int -> Expr a -> Expr a+regShamt w a = a `And` FromInt w 0x1f++------------------------------------------------------------------------++zextImm :: Int -> a -> Expr a+zextImm w = ZExt w . FromImm++sextImm :: Int -> a -> Expr a+sextImm w = SExt w . FromImm++generateImmediates

+ lib/LibRISCV/Effects/Expressions/Generator.hs view

@@ -0,0 +1,66 @@+-- This module generates smart constructors for the LibRISCV expressions+-- language through template-haskell. These constructors are syntactic sugar+-- intended to ease usage of the expression language.+module LibRISCV.Effects.Expressions.Generator (generateImmediates) where++import Data.Char (toLower)+import Language.Haskell.TH++binOps :: [String]+binOps =+    [ "Add"+    , "Sub"+    , "Eq"+    , "Slt"+    , "Sge"+    , "Ult"+    , "Uge"+    , "And"+    , "Or"+    , "Xor"+    , "LShl"+    , "LShr"+    , "AShr"+    , "Mul"+    , "UDiv"+    , "SDiv"+    , "URem"+    , "SRem"+    ]++------------------------------------------------------------------------++foldcase :: String -> String+foldcase = map toLower++genImm :: String -> Q Dec+genImm operator = do+    let name = mkName $ foldcase operator++    let consName = mkName operator+    let immName = mkName "FromImm"+    rval <- newName "rval"+    lval <- newName "lval"++    let body =+            AppE+                (AppE (ConE consName) (AppE (ConE immName) (VarE lval)))+                (AppE (ConE immName) (VarE rval))+    return $ FunD name [Clause [VarP lval, VarP rval] (NormalB body) []]++genImmRval :: String -> Q Dec+genImmRval operator = do+    let name = mkName $ foldcase operator ++ "Imm"++    let onName = mkName "on"+    let consName = mkName operator+    let immName = mkName "FromImm"++    let body = AppE (AppE (VarE onName) (ConE consName)) (ConE immName)+    return $ FunD name [Clause [] (NormalB body) []]++generateImmediates :: Q [Dec]+generateImmediates = do+    l1 <- mapM genImmRval binOps+    l2 <- mapM genImm binOps+    pure (l1 ++ l2)

+ lib/LibRISCV/Effects/Expressions/Language.hs view

@@ -0,0 +1,70 @@+{-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE ImpredicativeTypes #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TypeOperators #-}++-- | Implements an effect for /evaluation/ of the 'Expr' abstraction.+module LibRISCV.Effects.Expressions.Language (+    ExprEval (..),+    eval,+    defaultEval,+    ifExprM,+    whenExprM,+    unlessExprM,+) where++import Control.Monad.Freer (Eff, Member, type (~>))+import Control.Monad.Freer.TH (makeEffect)+import Control.Monad.IO.Class (MonadIO)+import LibRISCV.Effects.Expressions.Expr (Expr)++-- TODO: Reevaluate if we really need the distinction between IsTrue / IsFalse+-- for symbolic execution or if this is just nice to have for debugging.+data ExprEval v r where+    IsTrue :: Expr v -> ExprEval v Bool+    IsFalse :: Expr v -> ExprEval v Bool+    Eval :: Expr v -> ExprEval v v++makeEffect ''ExprEval++defaultEval :: (MonadIO m) => (v -> Bool, Expr v -> v) -> ExprEval v ~> m+defaultEval (pred, evalE) = \case+    Eval e -> pure $ evalE e+    IsTrue e -> pure $ pred $ evalE e+    IsFalse e -> pure $ not . pred $ evalE e++------------------------------------------------------------------------++-- Higher-level abstraction for making use of IsTrue / IsFalse without+-- having to export the isTrue / isFalse smart constructor. The standard+-- constructor is still exported as it will need to be interpreted.++condExprM ::+    forall v r v'.+    (Member (ExprEval v) r) =>+    (Expr v -> Eff r Bool) ->+    Expr v ->+    Eff r v' ->+    Eff r v' ->+    Eff r v'+condExprM p b t f = do+    b <- p b+    if b then t else f++-- | Like 'Control.Monad.Extra.ifM' but with internal expression evaluation.+ifExprM :: forall v r v'. (Member (ExprEval v) r) => Expr v -> Eff r v' -> Eff r v' -> Eff r v'+ifExprM = (condExprM isTrue)++-- | Like 'Control.Monad.Extra.whenM' but with internal expression evaluation.+whenExprM :: forall v r. (Member (ExprEval v) r) => Expr v -> Eff r () -> Eff r ()+whenExprM b t = (condExprM isTrue) b t (pure ())++-- | Like 'Control.Monad.Extra.unlessM' but with internal expression evaluation.+unlessExprM :: forall v r. (Member (ExprEval v) r) => Expr v -> Eff r () -> Eff r ()+unlessExprM b t = (condExprM isFalse) b t (pure ())

+ lib/LibRISCV/Effects/Expressions/Type.hs view

@@ -0,0 +1,38 @@+module LibRISCV.Effects.Expressions.Type where++data Expr a+    = -- | Create a new 'Expr' from a given immediate value.+      FromImm a+    | -- | Create an expression from a concrete 'Integer', treating it as a fixed-width two's+      -- complement value of the size (in bits) specified by the first argument to the constructor.+      FromInt Int Integer+    | -- | Zero extend an expression by adding the given amount of bits to it, for example,+      -- an 8-bit value can be zero-extended to 32-bit by passing 24 as the first argument.+      ZExt Int (Expr a)+    | -- | Same as 'ZExt' but performs sign-extension instead of zero-extension.+      SExt Int (Expr a)+    | -- | Extract a specified amount of bits from an expression. The first argument specifies+      -- the first bit which should be extracted, the second specifies the amount of bits to extract.+      Extract Int Int (Expr a)+    | Add (Expr a) (Expr a)+    | Sub (Expr a) (Expr a)+    | Eq (Expr a) (Expr a)+    | Slt (Expr a) (Expr a)+    | Sge (Expr a) (Expr a)+    | Ult (Expr a) (Expr a)+    | Uge (Expr a) (Expr a)+    | And (Expr a) (Expr a)+    | Or (Expr a) (Expr a)+    | Xor (Expr a) (Expr a)+    | LShl (Expr a) (Expr a)+    | LShr (Expr a) (Expr a)+    | AShr (Expr a) (Expr a)+    | Mul (Expr a) (Expr a)+    | UDiv (Expr a) (Expr a)+    | SDiv (Expr a) (Expr a)+    | URem (Expr a) (Expr a)+    | SRem (Expr a) (Expr a)++-- XXX: For binary operations, consider creation of a smart constructor which+-- allows passing an immediate value of type `a` as a second parameter. See+-- LibRISCV.Effects.Expressions.Generator for more information.

+ lib/LibRISCV/Effects/Logging/Default/Interpreter.hs view

@@ -0,0 +1,27 @@+{-# LANGUAGE GADTs #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE TypeOperators #-}++-- | Provides the default interpretation for the logging effect.+module LibRISCV.Effects.Logging.Default.Interpreter where++import Control.Monad.Freer (type (~>))+import Control.Monad.IO.Class (MonadIO (..))+import LibRISCV.Effects.Logging.Language (+    LogInstructionFetch (..),+ )++-- | The default effectful logging interpreter which writes the+-- 'LibRISCV.Internal.Decoder.Opcodes.InstructionType' of a fetched instruction+-- to standard output, before executing it. This is particularly useful for+-- debugging but is quite verbose in the common case.+defaultLogging :: (MonadIO m) => LogInstructionFetch ~> m+defaultLogging =+    liftIO . \case+        LogFetched inst -> print inst++-- | A stub implementation of an effectful interpreter which ignores any logging+-- effects entirely. Should be used when no debugging output is desired.+noLogging :: (Monad m) => LogInstructionFetch ~> m+noLogging = \case+    LogFetched _ -> pure ()

+ lib/LibRISCV/Effects/Logging/Language.hs view

@@ -0,0 +1,21 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE DeriveFunctor #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE TypeOperators #-}++-- | Implements the logging effect for instruction tracing. This effect+-- is primarly intended to be used for debugging.+module LibRISCV.Effects.Logging.Language where++import Control.Monad.Freer.TH (makeEffect)+import LibRISCV.Internal.Decoder.Opcodes (InstructionType)++data LogInstructionFetch r where+    -- TODO: Log program counter (i.e. instruction address) too.+    LogFetched :: InstructionType -> LogInstructionFetch ()++makeEffect ''LogInstructionFetch

+ lib/LibRISCV/Effects/Operations/Default/Interpreter.hs view

@@ -0,0 +1,69 @@+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TypeOperators #-}++-- | Implements the default (concrete) interpreter for the 'Operations' effect.+module LibRISCV.Effects.Operations.Default.Interpreter (+    ArchState (..),+    mkArchState,+    dumpState,+    defaultInstructions,+) where++import Control.Monad.Freer (type (~>))+import Control.Monad.IO.Class (MonadIO (..))+import Data.Array.IO (IOUArray)+import Data.BitVector (BV, bitVec)+import Data.Int (Int32)+import Data.Word (Word16, Word32, Word8)+import LibRISCV (Address)+import qualified LibRISCV.Effects.Operations.Default.Machine.Memory as MEM+import qualified LibRISCV.Effects.Operations.Default.Machine.Register as REG+import LibRISCV.Effects.Operations.Language (+    Operations (..),+    Size (Byte, Half, Word),+ )+import Numeric (showHex)++-- | Representation of the concrete architectural state of the interpreter.+data ArchState = ArchState+    { getReg :: REG.RegisterFile IOUArray Int32+    -- ^ Register file implementation of the architectural state.+    , getMem :: MEM.Memory IOUArray Word8+    -- ^ Memory implementation of the architectural state.+    }++-- | Create a new t'ArchState' based on a memory start address and a memory size.+mkArchState :: Address -> Word32 -> IO ArchState+mkArchState memStart memSize = do+    reg <- REG.mkRegFile 0+    mem <- MEM.mkMemory memStart memSize+    pure $ ArchState reg mem++-- | Write a textual representation of the t'ArchState' to standard output.+dumpState :: ArchState -> IO ()+dumpState ArchState{getReg = r} =+    REG.dumpRegs (showHex . fromIntegral @Int32 @Word32) r >>= putStr++-- | Implements concrete interpretation of the 'Operations' effect based on a 'BV' value representation.+defaultInstructions :: (MonadIO m) => ArchState -> Operations BV ~> m+defaultInstructions (ArchState regFile mem) =+    liftIO . \case+        ReadRegister idx -> bitVec 32 <$> REG.readRegister regFile (toEnum $ fromIntegral idx)+        WriteRegister idx reg -> REG.writeRegister regFile (toEnum $ fromIntegral idx) (fromIntegral reg)+        Load size addr -> case size of+            Byte -> bitVec 8 <$> MEM.loadByte mem (fromIntegral addr)+            Half -> bitVec 16 <$> (MEM.loadHalf mem (fromIntegral addr) :: IO Word16)+            Word -> bitVec 32 <$> MEM.loadWord @_ @_ @BV mem (fromIntegral addr)+        Store size addr w -> case size of+            Byte -> MEM.storeByte mem (fromIntegral addr) (fromIntegral w)+            Half -> MEM.storeHalf mem (fromIntegral addr) w+            Word -> MEM.storeWord mem (fromIntegral addr) w+        WritePC w -> REG.writePC regFile (fromIntegral w)+        ReadPC -> bitVec 32 <$> REG.readPC regFile+        Exception pc msg -> error $ "[0x" ++ showHex pc "" ++ "] " ++ msg+        Ecall pc -> putStrLn $ "ecall at 0x" ++ showHex pc ""+        Ebreak pc -> putStrLn $ "ebreak at 0x" ++ showHex pc ""

+ lib/LibRISCV/Effects/Operations/Default/Machine/Memory.hs view

@@ -0,0 +1,161 @@+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE TupleSections #-}++-- | Provides an implementatio of a byte-addressable memory, intended for internal+-- usage in interpreters for the 'LibRISCV.Effects.Operations.Operations' effect.+module LibRISCV.Effects.Operations.Default.Machine.Memory (+    Memory,+    HalfStorage (..),+    WordStorage (..),+    mkMemory,+    memSize,+    loadByte,+    loadHalf,+    loadWord,+    storeByte,+    storeHalf,+    storeWord,+    storeByteString,+    mkWord,+    mkBytes,+) where++import Data.Array.IO (+    MArray (getBounds, newArray_),+    readArray,+    writeArray,+ )+import Data.BitVector (BV, bitVec)+import Data.Bits (Bits (shift, shiftR, (.&.), (.|.)))+import qualified Data.ByteString.Lazy as BSL+import Data.Int ()+import Data.Word (Word16, Word32, Word8)+import LibRISCV++-- | Since the memory is byte-addressable it requires converting values of a+-- larger size to bytes. This type class is responsible for a conversion of+-- 16-bit values (halfs). That is, it converts halfs to bytes (and vice versa)+-- in little endian.+class HalfStorage halfType byteType where+    -- | Convert a list of two bytes to a single half.+    toHalf :: [byteType] -> halfType++    -- | Convert a single half to a list of two bytes.+    halfToBytes :: halfType -> [byteType]++-- | Similar to 'HalfStorage' but handles conversion of 32-bit values (words).+class WordStorage wordType byteType where+    -- | Convert a list of four bytes to a single word.+    toWord :: [byteType] -> wordType++    -- | Convert a single word to a list of four bytes.+    wordToBytes :: wordType -> [byteType]++instance WordStorage Word32 Word8 where+    toWord = mkWord+    wordToBytes = mkBytes++instance HalfStorage Word16 Word8 where+    toHalf = fromIntegral . mkWord+    halfToBytes = mkBytes . fromIntegral++instance WordStorage BV Word8 where+    toWord = (bitVec 32 :: Word32 -> BV) . fromIntegral . mkWord+    wordToBytes = mkBytes . fromIntegral++instance HalfStorage BV Word8 where+    toHalf = bitVec 16 . mkWord+    halfToBytes = mkBytes . fromIntegral++-- | Converts a list of bytes to a 'Word32' in little endian.+mkWord :: [Word8] -> Word32+mkWord bytes =+    foldl+        (\x (byte, idx) -> (fromIntegral byte `shift` (idx * 8)) .|. x)+        0+        $ zip bytes [0 .. length bytes - 1]++-- | Split a 32-bit word into four octets in little endian.+mkBytes :: Word32 -> [Word8]+mkBytes w = map (\off -> fromIntegral $ shiftR w off .&. 0xff) offs+  where+    offs = take 4 $ iterate (+ 8) 0++------------------------------------------------------------------------++-- | Representation of a byte-addressable memory. The type is parameterized+-- over an array implementation (such as 'Data.Array.IO.IOUArray') and a+-- generic value type (used to represent instruction operands).+data Memory t a = Memory+    { memStart :: Address+    , memBytes :: t Address a+    }++-- | Create a new memory of the given size starting at the given address.+mkMemory :: (MArray t a IO) => Address -> Word32 -> IO (Memory t a)+mkMemory addr size = fmap (Memory addr) (newArray_ (0, size - 1))++-- Translate global address to a memory-local address.+toMemAddr :: Memory t a -> Address -> Address+toMemAddr mem addr = addr - (memStart mem)++-- | Returns the size of the memory in bytes.+memSize :: (MArray t a IO) => Memory t a -> IO Word32+memSize = fmap ((+ 1) . snd) . getBounds . memBytes++------------------------------------------------------------------------++-- TODO: Only provide load/store, remove all wrapper functions. Could+-- use the 'Size' type from the operations language for this purpose too.++-- | Load a single byte from memory at the given address.+loadByte :: (MArray t a IO) => Memory t a -> Address -> IO a+loadByte mem = readArray (memBytes mem) . toMemAddr mem++load :: (MArray t a IO) => ([a] -> b) -> Word32 -> Memory t a -> Address -> IO b+load proc bytesize mem addr =+    proc+        <$> mapM (\off -> loadByte mem $ addr + off) [0 .. (bytesize - 1)]++-- | Load a half (16-bit) from memory at the given address.+loadHalf :: (MArray t a IO, HalfStorage b a) => Memory t a -> Address -> IO b+loadHalf = load toHalf 2++-- | Load a word (32-bit) from memory at the given address.+loadWord :: (MArray t a IO, WordStorage b a) => Memory t a -> Address -> IO b+loadWord = load toWord 4++-- | Store a single byte in memory.+storeByte :: (MArray t a IO) => Memory t a -> Address -> a -> IO ()+storeByte mem addr = writeArray (memBytes mem) $ toMemAddr mem addr++store :: (MArray t a IO) => (b -> [a]) -> Word32 -> Memory t a -> Address -> b -> IO ()+store proc bytesize mem addr =+    mapM_ (\(off, val) -> storeByte mem (addr + off) val)+        . zip [0 .. (bytesize - 1)]+        . proc++-- | Store a half (16-bit) in memory.+storeHalf :: (MArray t a IO, HalfStorage b a) => Memory t a -> Address -> b -> IO ()+storeHalf = store halfToBytes 2++-- | Store a word (32-bit) in memory.+storeWord :: (MArray t a IO, WordStorage b a) => Memory t a -> Address -> b -> IO ()+storeWord = store wordToBytes 4++-- | Write a 'BSL.ByteString' to memory in little endian byteorder. Expects a+-- function to convert single bytes ('Word8') to the chosen value+-- representation, a t'Memory', as well the 'Address' where the string should be+-- stored and the 'BSL.ByteString' itself.+storeByteString ::+    (MArray t a IO) =>+    (Word8 -> a) ->+    Memory t a ->+    Address ->+    BSL.ByteString ->+    IO ()+storeByteString convert mem addr bs =+    mapM_ (\(off, val) -> storeByte mem (addr + off) (convert val)) $+        zip [0 ..] $+            BSL.unpack bs

+ lib/LibRISCV/Effects/Operations/Default/Machine/Register.hs view

@@ -0,0 +1,65 @@+{-# LANGUAGE FlexibleContexts #-}++-- | Provides a polymorphic implementation of a register file. This module is+-- intended to be used internally by interpreters for the+-- 'LibRISCV.Effects.Operations.Operations' effect. This register file+-- implementation also provides facilities for storing a concrete program+-- counter.+module LibRISCV.Effects.Operations.Default.Machine.Register where++import Control.Monad (unless)+import Data.Array.IO (+    MArray (newArray),+    getElems,+    readArray,+    writeArray,+ )+import Data.IORef (IORef, newIORef, readIORef, writeIORef)+import Data.Word (Word32)+import LibRISCV++-- | Register file addressed by 'RegIdx'. The type is parameterized over an array+-- implementation (such as 'Data.Array.IO.IOUArray') and a generic value type+-- (used to represent instruction operands).+data RegisterFile t a = RegisterFile+    { pc :: IORef Word32+    -- ^ The current program counter (always concrete in this implementation).+    , regs :: t RegIdx a+    -- ^ The underlying array to store the register values.+    }++-- | Create a new register file, initializing all registers with the given default+-- value. This value /must/ represent the zero value in the chosen value type.+mkRegFile :: (MArray t a IO) => a -> IO (RegisterFile t a)+mkRegFile defValue = RegisterFile <$> newIORef 0 <*> newArray (minBound, maxBound) defValue++-- | Dump the current register file state as a 'String'.+dumpRegs :: (MArray t a IO) => (a -> ShowS) -> RegisterFile t a -> IO String+dumpRegs sh =+    fmap+        ( foldr (\(a, v) s -> show a ++ "\t= 0x" ++ sh v "\n" ++ s) ""+            . zip [(minBound :: RegIdx) .. maxBound]+        )+        . getElems+        . regs++------------------------------------------------------------------------++-- | Read register value at given register index. For the 'Zero' register index, the+-- zero/default value (as passed to 'mkRegFile' is always returned.+readRegister :: (MArray t a IO) => RegisterFile t a -> RegIdx -> IO a+readRegister = readArray . regs++-- | Write register at given register index. Writes to the 'Zero' register are ignored.+writeRegister :: (MArray t a IO) => RegisterFile t a -> RegIdx -> a -> IO ()+writeRegister RegisterFile{regs = r} idx val = unless (idx == Zero) $ writeArray r idx val++------------------------------------------------------------------------++-- | Returs the current program counter value.+readPC :: RegisterFile t a -> IO Word32+readPC = readIORef . pc++-- | Write a new program counter value.+writePC :: RegisterFile t a -> Word32 -> IO ()+writePC = writeIORef . pc

+ lib/LibRISCV/Effects/Operations/Language.hs view

@@ -0,0 +1,34 @@+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE InstanceSigs #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE TemplateHaskell #-}++-- | Implements an effect for interactions with the architectural state, upon+-- which instructions are executed (register file, memory, program counter, etc.).+module LibRISCV.Effects.Operations.Language where++import Control.Monad.Freer.TH (makeEffect)++-- | Abstraction for expressing a 8-, 16-, or 32-bit size.+data Size = Byte | Half | Word+    deriving (Eq, Show)++-- | Returns the size in bits (either 8, 16, or 32).+bitSize :: Size -> Int+bitSize Byte = 8+bitSize Half = 16+bitSize Word = 32++data Operations v r where+    ReadRegister :: v -> Operations v v+    WriteRegister :: v -> v -> Operations v ()+    Load :: Size -> v -> Operations v v+    Store :: Size -> v -> v -> Operations v ()+    WritePC :: v -> Operations v ()+    ReadPC :: Operations v v+    Exception :: v -> String -> Operations v ()+    Ecall :: v -> Operations v ()+    Ebreak :: v -> Operations v ()++makeEffect ''Operations

+ lib/LibRISCV/Loader.hs view

@@ -0,0 +1,87 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE RecordWildCards #-}+{-# LANGUAGE TypeFamilies #-}++-- | An implementation of an /Executable Loadable Format/ (ELF) loader. The module+-- is responsible for loading instructions into a provided memory implementation+-- and obtaining the entry point for the executable.+module LibRISCV.Loader (readElf, LoadFunc, loadElf, startAddr) where++import Control.Monad.Catch (MonadCatch)+import Data.Bits ()+import qualified Data.ByteString.Lazy as BSL+import Data.Elf (+    Elf (..),+    ElfListXX (..),+    ElfNodeType (..),+    ElfSectionData (ElfSectionData),+    ElfXX (+        ElfSection,+        ElfSegment,+        ehEntry,+        epAddMemSize,+        epData,+        epType,+        esAddr,+        esData+    ),+    elfFindHeader,+    parseElf,+ )+import Data.Elf.Constants+import Data.Elf.Headers (+    SingElfClass (SELFCLASS32, SELFCLASS64),+    SingElfClassI,+    withSingElfClassI,+ )+import Data.Elf.PrettyPrint (readFileLazy)+import Data.Int (Int64)+import Data.Word (Word32)+import LibRISCV+import System.FilePath ()++-- Filter all ELF segments with type PT_LOAD.+loadableSegments :: ElfListXX a -> [ElfXX 'Segment a]+loadableSegments (ElfListCons v@(ElfSegment{..}) l) =+    if epType == PT_LOAD+        then v : loadableSegments l+        else loadableSegments l+loadableSegments (ElfListCons _ l) = loadableSegments l+loadableSegments ElfListNull = []++-- Copy data from ElfSection to memory at the given absolute address.+copyData :: (Monad m, SingElfClassI a) => ElfListXX a -> Int64 -> LoadFunc m -> m ()+copyData ElfListNull _ _ = pure ()+copyData (ElfListCons (ElfSection{esData = ElfSectionData textData, ..}) xs) zeros f = do+    f (fromIntegral esAddr) $ BSL.append textData (BSL.replicate zeros 0)+    copyData xs zeros f+copyData (ElfListCons _ xs) zeros f = copyData xs zeros f++-- Load an ElfSegment into memory at the given address.+loadSegment :: (Monad m, SingElfClassI a) => LoadFunc m -> ElfXX 'Segment a -> m ()+loadSegment loadFunc ElfSegment{..} =+    copyData epData (fromIntegral epAddMemSize) loadFunc++------------------------------------------------------------------------++-- | Load a 'BSL.ByteString' into memory at a given address.+type LoadFunc m = Address -> BSL.ByteString -> m ()++-- | Load all loadable segments of an ELF file into memory. An addition to the+-- 'Data.Elf.Elf' file, it requires an implementation of a 'LoadFunc' which is+-- responsible for converting a 'BSL.ByteString' to the internal value+-- representation.+loadElf :: (Monad m) => Elf -> LoadFunc m -> m ()+loadElf (Elf classS elfs) loadFunc = withSingElfClassI classS $ do+    let loadable = loadableSegments elfs+    mapM_ (loadSegment loadFunc) loadable++-- | Read an ELF from a given 'FilePath'.+readElf :: FilePath -> IO Elf+readElf path = readFileLazy path >>= parseElf++-- | Return the entry point from the ELF header.+startAddr :: (MonadCatch m) => Elf -> m Word32+startAddr (Elf SELFCLASS32 elfs) = ehEntry <$> elfFindHeader elfs+startAddr (Elf SELFCLASS64 _) = error "64-bit executables not supported"

+ lib/LibRISCV/Semantics.hs view

@@ -0,0 +1,13 @@+-- | Functions for interacting with the free monad abstraction used to formally+-- describe the semantics of RISC-V instructions.+module LibRISCV.Semantics (+    LibRISCV.Semantics.Default.buildAST,+    LibRISCV.Semantics.Utils.writeRegister,+    LibRISCV.Semantics.Utils.readRegister,+    LibRISCV.Semantics.Utils.load,+    LibRISCV.Semantics.Utils.store,+    LibRISCV.Semantics.Utils.writePC,+) where++import LibRISCV.Semantics.Default+import LibRISCV.Semantics.Utils

+ lib/LibRISCV/Semantics/Default.hs view

@@ -0,0 +1,97 @@+{-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE BangPatterns #-}+{-# LANGUAGE BlockArguments #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE QualifiedDo #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TypeFamilies #-}++module LibRISCV.Semantics.Default where++import Control.Monad.Freer+import Data.Data (Proxy (..))+import Data.Parameterized.NatRepr+import GHC.TypeLits+import LibRISCV.Effects.Decoding.Language+import LibRISCV.Effects.Expressions.Expr+import LibRISCV.Effects.Expressions.Language+import LibRISCV.Effects.Logging.Language (LogInstructionFetch, logFetched)+import LibRISCV.Effects.Operations.Language hiding (load, readRegister, store, writePC, writeRegister)+import LibRISCV.Internal.Decoder.Opcodes+import qualified LibRISCV.Semantics.RV32_I.Default as RV32_I+import qualified LibRISCV.Semantics.RV_I.Default as RV_I+import qualified LibRISCV.Semantics.RV_M.Default as RV_M+import LibRISCV.Semantics.Utils++------------------------------------------------------------------------++-- We require type annotations here to workaround a limitation of+-- GHC type inference in conjunction with freer-simple. Alternatively,+-- we could use a proxy type.+--+-- See: https://github.com/lexi-lambda/freer-simple/issues/7++instrSemantics ::+    forall v r.+    ( Member (Operations v) r+    , Member LogInstructionFetch r+    , Member (Decoding v) r+    , Member (ExprEval v) r+    ) =>+    Int ->+    v ->+    Eff r ()+instrSemantics width pc = do+    ty <- withInstrType @v Proxy id+    logFetched ty+    case ty of+        RV_I inst -> RV_I.instrSemantics width pc inst >> buildInstruction @v width+        RV32_I inst -> RV32_I.instrSemantics @v inst >> buildInstruction @v width+        RV_M inst -> RV_M.instrSemantics @v width inst >> buildInstruction @v width+        InvalidInstruction -> pure ()++buildInstruction ::+    forall v r.+    ( Member (Operations v) r+    , Member LogInstructionFetch r+    , Member (Decoding v) r+    , Member (ExprEval v) r+    ) =>+    Int ->+    Eff r ()+buildInstruction width = do+    -- fetch instruction at current PC+    pc <- readPC @v+    instrWord <- load @v Word $ FromImm pc+    setInstr instrWord++    -- Increment PC before execute', allows setting PC to to+    -- different values in execute' for jumps and branches.+    writePC $ FromImm pc `Add` FromInt width 4+    instrSemantics width pc++-- | Obtain the free monad AST for a program loaded into memory, e.g. through+-- the provided ELF 'LibRISCV.Loader' implementation. The function takes one+-- argument  which corresponds to an address in memory at which program+-- execution will start. An instruction word will be loaded from this address,+-- decoded, and executed.+buildAST ::+    forall w v r.+    ( KnownNat w+    , Member (Operations v) r+    , Member LogInstructionFetch r+    , Member (Decoding v) r+    , Member (ExprEval v) r+    ) =>+    v ->+    Eff r ()+buildAST entry =+    let+        !width = fromIntegral (intValue (knownNat :: NatRepr w))+     in+        writePC (FromImm entry) >> buildInstruction @v width

+ lib/LibRISCV/Semantics/RV32_I/Default.hs view

@@ -0,0 +1,38 @@+{-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE BlockArguments #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE QualifiedDo #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TypeFamilies #-}++module LibRISCV.Semantics.RV32_I.Default where++import Control.Monad.Freer+import LibRISCV.Effects.Decoding.Language (Decoding, decodeShamt)+import LibRISCV.Effects.Expressions.Expr+import LibRISCV.Effects.Expressions.Language (ExprEval)+import LibRISCV.Effects.Logging.Language (LogInstructionFetch)+import LibRISCV.Effects.Operations.Language (Operations (..))+import LibRISCV.Internal.Decoder.Opcodes (RV32_I (..))+import LibRISCV.Semantics.Utils++instrSemantics :: forall v r. (Member (Operations v) r, Member LogInstructionFetch r, Member (Decoding v) r, Member (ExprEval v) r) => RV32_I -> Eff r ()+instrSemantics = \case+    SLLI -> do+        (r1, rd, _) <- decodeAndReadIType @v+        shamt <- decodeShamt+        writeRegister rd $ r1 `lshlImm` shamt+    SRLI -> do+        (r1, rd, _) <- decodeAndReadIType @v+        shamt <- decodeShamt+        writeRegister rd $ r1 `lshrImm` shamt+    SRAI -> do+        (r1, rd, _) <- decodeAndReadIType @v+        shamt <- decodeShamt+        writeRegister rd $ r1 `ashrImm` shamt

+ lib/LibRISCV/Semantics/RV_I/Default.hs view

@@ -0,0 +1,212 @@+{-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE BlockArguments #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE QualifiedDo #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TypeFamilies #-}++module LibRISCV.Semantics.RV_I.Default where++import Control.Monad.Freer+import LibRISCV.Effects.Decoding.Language (Decoding)+import LibRISCV.Effects.Expressions.Expr+import LibRISCV.Effects.Expressions.Language (ExprEval, unlessExprM, whenExprM)+import LibRISCV.Effects.Logging.Language (LogInstructionFetch)+import LibRISCV.Effects.Operations.Language (Operations (..), Size (..), ebreak, ecall, exception, readPC)+import LibRISCV.Internal.Decoder.Opcodes (RV_I (..))+import LibRISCV.Semantics.Utils++instrSemantics ::+    forall v r.+    ( Member (Operations v) r+    , Member LogInstructionFetch r+    , Member (Decoding v) r+    , Member (ExprEval v) r+    ) =>+    Int ->+    v ->+    RV_I ->+    Eff r ()+instrSemantics width pc =+    let+        fromUInt :: Integer -> Expr v+        fromUInt = FromInt width++        -- False if a given address is not aligned at the four-byte boundary.+        isMisaligned :: Expr v -> Expr v+        isMisaligned addr = (addr `And` fromUInt 0x3) `Uge` fromUInt 1+     in+        \case+            ADDI -> do+                (r1, rd, imm) <- decodeAndReadIType @v+                writeRegister rd $ r1 `addImm` imm+            SLTI -> do+                (r1, rd, imm) <- decodeAndReadIType @v+                let cond = r1 `slt` imm+                writeRegister rd cond+            SLTIU -> do+                (r1, rd, imm) <- decodeAndReadIType @v+                let cond = r1 `ult` imm+                writeRegister rd cond+            ANDI -> do+                (r1, rd, imm) <- decodeAndReadIType @v+                writeRegister rd $ r1 `andImm` imm+            ORI -> do+                (r1, rd, imm) <- decodeAndReadIType @v+                writeRegister rd $ r1 `orImm` imm+            XORI -> do+                (r1, rd, imm) <- decodeAndReadIType @v+                writeRegister rd $ r1 `xorImm` imm+            LUI -> do+                (rd, imm) <- decodeUType @v+                writeRegister rd $ FromImm imm+            AUIPC -> do+                (rd, imm) <- decodeUType+                writeRegister rd $ pc `addImm` imm+            ADD -> do+                (r1, r2, rd) <- decodeAndReadRType @v+                writeRegister rd $ r1 `addImm` r2+            SLT -> do+                (r1, r2, rd) <- decodeAndReadRType+                let cond = r1 `slt` r2 :: Expr v+                writeRegister rd cond+            SLTU -> do+                (r1, r2, rd) <- decodeAndReadRType+                let cond = r1 `ult` r2 :: Expr v+                writeRegister rd cond+            AND -> do+                (r1, r2, rd) <- decodeAndReadRType @v+                writeRegister rd $ r1 `andImm` r2+            OR -> do+                (r1, r2, rd) <- decodeAndReadRType @v+                writeRegister rd $ r1 `orImm` r2+            XOR -> do+                (r1, r2, rd) <- decodeAndReadRType @v+                writeRegister rd $ r1 `xorImm` r2+            SLL -> do+                (r1, r2, rd) <- decodeAndReadRType @v+                writeRegister rd $ FromImm r1 `LShl` regShamt width (FromImm r2)+            SRL -> do+                (r1, r2, rd) <- decodeAndReadRType @v+                writeRegister rd $ FromImm r1 `LShr` regShamt width (FromImm r2)+            SUB -> do+                (r1, r2, rd) <- decodeAndReadRType @v+                writeRegister rd $ r1 `sub` r2+            SRA -> do+                (r1, r2, rd) <- decodeAndReadRType @v+                writeRegister rd $ FromImm r1 `AShr` regShamt width (FromImm r2)+            JAL -> do+                nextInstr <- readPC+                (rd, imm) <- decodeJType++                let newPC = pc `addImm` imm+                writePC newPC+                whenExprM (isMisaligned newPC) $+                    exception pc "misaligned PC"+                writeRegister rd (FromImm nextInstr)+            JALR -> do+                nextInstr <- readPC+                (r1, rd, imm) <- decodeAndReadIType++                let newPC = (r1 `addImm` imm) `And` fromUInt 0xfffffffe+                writePC newPC+                whenExprM (isMisaligned newPC) $+                    exception pc "misaligned PC"+                writeRegister rd $ FromImm nextInstr+            LB -> do+                (r1, rd, imm) <- decodeAndReadIType @v+                byte <- load Byte $ r1 `addImm` imm+                -- TODO: Alignment handling+                writeRegister rd $ sextImm 24 byte+            LBU -> do+                (r1, rd, imm) <- decodeAndReadIType @v+                -- TODO: Alignment handling+                byte <- load Byte $ r1 `addImm` imm+                writeRegister rd $ zextImm 24 byte+            LH -> do+                (r1, rd, imm) <- decodeAndReadIType @v+                -- TODO: Alignment handling+                half <- load Half $ r1 `addImm` imm+                writeRegister rd $ sextImm 16 half+            LHU -> do+                (r1, rd, imm) <- decodeAndReadIType @v+                -- TODO: Alignment handling+                half <- load Half $ r1 `addImm` imm+                writeRegister rd $ zextImm 16 half+            LW -> do+                (r1, rd, imm) <- decodeAndReadIType @v++                -- TODO: Alignment handling+                word <- load Word $ r1 `addImm` imm+                writeRegister rd $ FromImm word+            SB -> do+                (r1, r2, imm) <- decodeAndReadSType @v++                -- TODO: Alignment handling+                store Byte (r1 `addImm` imm) $ FromImm r2+            SH -> do+                (r1, r2, imm) <- decodeAndReadSType @v++                -- TODO: Alignment handling+                store Half (r1 `addImm` imm) $ FromImm r2+            SW -> do+                (r1, r2, imm) <- decodeAndReadSType @v+                -- TODO: Alignment handling+                store Word (r1 `addImm` imm) $ FromImm r2+            BEQ -> do+                (r1, r2, imm) <- decodeAndReadBType++                let addr = pc `add` imm+                whenExprM (r1 `eq` r2) $ do+                    writePC addr+                    whenExprM (isMisaligned addr) $+                        exception pc "misaligned PC"+            BNE -> do+                (r1, r2, imm) <- decodeAndReadBType++                let addr = pc `add` imm+                unlessExprM (r1 `eq` r2) $ do+                    writePC addr+                    whenExprM (isMisaligned addr) $+                        exception pc "misaligned PC"+            BLT -> do+                (r1, r2, imm) <- decodeAndReadBType++                let addr = pc `add` imm+                whenExprM (r1 `slt` r2) $ do+                    writePC addr+                    whenExprM (isMisaligned addr) $+                        exception pc "misaligned PC"+            BLTU -> do+                (r1, r2, imm) <- decodeAndReadBType++                let addr = pc `add` imm+                whenExprM (r1 `ult` r2) $ do+                    writePC @v $ addr+                    whenExprM (isMisaligned addr) $+                        exception pc "misaligned PC"+            BGE -> do+                (r1, r2, imm) <- decodeAndReadBType++                let addr = pc `add` imm+                whenExprM (r1 `sge` r2) $ do+                    writePC addr+                    whenExprM (isMisaligned addr) $+                        exception pc "misaligned PC"+            BGEU -> do+                (r1, r2, imm) <- decodeAndReadBType++                let addr = pc `add` imm+                whenExprM (r1 `uge` r2) $ do+                    writePC addr+                    whenExprM (isMisaligned addr) $+                        exception pc "misaligned PC"+            FENCE -> pure () -- XXX: ignore for now+            ECALL -> ecall pc+            EBREAK -> ebreak pc

+ lib/LibRISCV/Semantics/RV_M/Default.hs view

@@ -0,0 +1,112 @@+{-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE BlockArguments #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE QualifiedDo #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeFamilies #-}++module LibRISCV.Semantics.RV_M.Default where++import Control.Monad.Freer+import Data.Function (on)+import LibRISCV.Effects.Decoding.Language (Decoding)+import LibRISCV.Effects.Expressions.Expr+import LibRISCV.Effects.Expressions.Language (ExprEval, ifExprM)+import LibRISCV.Effects.Logging.Language (LogInstructionFetch)+import LibRISCV.Effects.Operations.Language (Operations (..))+import LibRISCV.Internal.Decoder.Opcodes (RV_M (..))+import LibRISCV.Semantics.Utils++instrSemantics ::+    forall v r.+    ( Member (Operations v) r+    , Member LogInstructionFetch r+    , Member (Decoding v) r+    , Member (ExprEval v) r+    ) =>+    Int ->+    RV_M ->+    Eff r ()+instrSemantics width =+    let+        fromUInt :: Integer -> Expr v+        fromUInt = FromInt width++        immEqInt :: v -> Integer -> Expr v+        immEqInt imm int = FromImm imm `Eq` fromUInt int++        mask1 :: Expr v+        mask1 = FromInt width (2 ^ width - 1)++        extract32 :: Int -> Expr v -> Expr v+        extract32 = flip Extract 32++        mostNegative :: Integer+        mostNegative = 2 ^ (width - 1)++        -- Signed division overflow occurs when the most-negative integer is divided by -1.+        sdivOverflow :: v -> v -> Expr v+        sdivOverflow n divisor = (n `immEqInt` mostNegative) `And` (divisor `immEqInt` (-1))+     in+        \case+            MUL -> do+                (r1, r2, rd) <- decodeAndReadRType+                let+                    multRes = (Mul `on` sextImm 32) r1 r2+                    res = extract32 0 multRes+                writeRegister rd res+            MULH -> do+                (r1, r2, rd) <- decodeAndReadRType+                let+                    multRes = (Mul `on` sextImm 32) r1 r2+                    res = extract32 32 multRes+                writeRegister rd res+            MULHU -> do+                (r1, r2, rd) <- decodeAndReadRType+                let+                    multRes = (Mul `on` zextImm 32) r1 r2+                    res = extract32 32 multRes+                writeRegister rd res+            MULHSU -> do+                (r1, r2, rd) <- decodeAndReadRType+                let+                    multRes = sextImm 32 r1 `Mul` zextImm 32 r2+                    res = extract32 32 multRes+                writeRegister rd res+            DIV -> do+                (r1, r2, rd) <- decodeAndReadRType+                ifExprM+                    (r2 `immEqInt` 0)+                    do writeRegister rd mask1+                    do+                        ifExprM+                            (sdivOverflow r1 r2)+                            do writeRegister rd $ FromImm r1+                            do writeRegister rd $ r1 `sdiv` r2+            DIVU -> do+                (r1, r2, rd) <- decodeAndReadRType+                ifExprM+                    (r2 `immEqInt` 0)+                    do writeRegister rd mask1+                    do writeRegister rd $ r1 `udiv` r2+            REM -> do+                (r1, r2, rd) <- decodeAndReadRType+                ifExprM+                    (r2 `immEqInt` 0)+                    do writeRegister rd $ FromImm r1+                    do+                        ifExprM+                            (sdivOverflow r1 r2)+                            do writeRegister rd $ fromUInt 0+                            do writeRegister rd $ r1 `srem` r2+            REMU -> do+                (r1, r2, rd) <- decodeAndReadRType+                ifExprM+                    (r2 `immEqInt` 0)+                    do writeRegister rd $ FromImm r1+                    do writeRegister rd $ r1 `urem` r2

+ lib/LibRISCV/Semantics/Utils.hs view

@@ -0,0 +1,75 @@+{-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE BlockArguments #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE QualifiedDo #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeFamilies #-}++module LibRISCV.Semantics.Utils where++import Control.Applicative+import Control.Monad.Freer+import LibRISCV.Effects.Decoding.Language+import LibRISCV.Effects.Expressions.Expr+import LibRISCV.Effects.Expressions.Language+import LibRISCV.Effects.Operations.Language+import qualified LibRISCV.Effects.Operations.Language as Op++-- TODO add newTypes for type safety+-- decode and read register+decodeAndReadIType :: forall v r. (Member (Decoding v) r, Member (Operations v) r) => Eff r (v, v, v)+decodeAndReadIType = liftA3 (,,) (decodeRS1 >>= Op.readRegister) decodeRD decodeImmI++-- decode and read register+decodeAndReadBType :: forall v r. (Member (Decoding v) r, Member (Operations v) r) => Eff r (v, v, v)+decodeAndReadBType = liftA3 (,,) (decodeRS1 >>= Op.readRegister) (decodeRS2 >>= Op.readRegister) decodeImmB++-- decode and read register+decodeAndReadSType :: forall v r. (Member (Decoding v) r, Member (Operations v) r) => Eff r (v, v, v)+decodeAndReadSType = liftA3 (,,) (decodeRS1 >>= Op.readRegister) (decodeRS2 >>= Op.readRegister) decodeImmS++-- decode and read register+decodeAndReadRType :: forall v r. (Member (Decoding v) r, Member (Operations v) r) => Eff r (v, v, v)+decodeAndReadRType = liftA3 (,,) (decodeRS1 >>= Op.readRegister) (decodeRS2 >>= Op.readRegister) decodeRD++-- decode and read register+decodeJType :: forall v r. (Member (Decoding v) r, Member (Operations v) r) => Eff r (v, v)+decodeJType = liftA2 (,) decodeRD decodeImmJ++decodeUType :: forall v r. (Member (Decoding v) r, Member (Operations v) r) => Eff r (v, v)+decodeUType = liftA2 (,) decodeRD decodeImmU++-- | Write to a register in the register file. The function takes a register index and+-- a value which should be written to the register (represented as an 'Expr'). This function+-- is primarly useful to initialize special registers, e.g. setting the stack pointer to a+-- meaningful value at the very beginning of the free monad AST.+writeRegister :: forall v r. (Member (ExprEval v) r, Member (Operations v) r) => v -> Expr v -> Eff r ()+writeRegister reg e = eval e >>= Op.writeRegister reg++-- | Obtain the current value for a register in the register file. The functions takes a register+-- index (encapsulated in an 'Expr') and returns the value of this register.+readRegister :: forall v r. (Member (ExprEval v) r, Member (Operations v) r) => Expr v -> Eff r v+readRegister e = eval e >>= Op.readRegister++-- | Change the current value of the /Program Counter/ (PC). The new value is the only function+-- argument and is represented as an 'Expr'.+writePC :: forall v r. (Member (ExprEval v) r, Member (Operations v) r) => Expr v -> Eff r ()+writePC e = eval e >>= Op.writePC++-- | Load a fixed-size value from memory. The function takes two arguments: The 'Size' of the+-- value to load and the start address of the value in memory (represented as an 'Expr').+load :: forall v r. (Member (ExprEval v) r, Member (Operations v) r) => Size -> Expr v -> Eff r v+load s e = eval e >>= Op.load s++-- | Store a fixed-size value in memory. The arguments are: The 'Size' of the value, the start+-- address where the value should be stored, and the value itself. The latter two are encapuslated+-- in the 'Expr' abstraction.+store :: forall v r. (Member (ExprEval v) r, Member (Operations v) r) => Size -> Expr v -> Expr v -> Eff r ()+store s r e = do+    reg <- eval r+    v <- eval e+    Op.store s reg v

+ libriscv.cabal view

@@ -0,0 +1,141 @@+cabal-version:      2.4+name:               libriscv+version:            0.1.0.0++synopsis:           A versatile, flexible and executable formal model for the RISC-V architecture.+description:+  A formal model for the <https://riscv.org/ RISC-V> /Instruction Set Architecture/ (ISA).+  Contrary to other Haskell RISC-V ISA models, like <https://github.com/GaloisInc/grift GRIFT>+  or <https://github.com/mit-plv/riscv-semantics riscv-semantics>, LibRISCV is specifically+  tailored to the creation of custom ISA interpreters. To this end, it is designed for+  flexibility, allowing a versatile representation of instruction operands. For example,+  instruction operands can be <https://en.wikipedia.org/wiki/Satisfiability_modulo_theories SMT>+  expressions for <https://doi.org/10.48550/arXiv.2404.04132 symbolic execution> of binary code.+  .+  LibRISCV abstractly describes instruction semantics using an /Embedded Domain Specific Language/+  (EDSL) with <https://doi.org/10.1145/2887747.2804319 free(r) monads>. This Haskell library+  is intended to build custom interpreters for this free monad. The entry point for this purpose is+  the 'LibRISCV.Semantics.buildAST' function which obtains the free monad AST based on an entry address.+  The entry address can be obtained from a provided ELF loader implementation, this "Loader" module+  is also responsible for loading binary instructions into a provided memory implementation. Refer to+  provided example interpreters in the <https://github.com/agra-uni-bremen/libriscv GitHub repository>+  for practical usage instruction. More detailed information on LibRISCV and its concepts is also+  available in a <https://doi.org/10.1007/978-3-031-38938-2_2 TFP'23 publication>.++homepage:           https://github.com/agra-uni-bremen/libriscv+bug-reports:        https://github.com/agra-uni-bremen/libriscv/issues+license:            MIT+license-file:       LICENSE.txt+author:             Sören Tempel, Tobias Brandt, and Christoph Lüth+maintainer:         Group of Computer Architecture <riscv@informatik.uni-bremen.de>+copyright:          (c) 2022-2024 University of Bremen+data-files:         data/instr_dict.yaml+category:           Formal Languages++source-repository head+    type: git+    location: https://github.com/agra-uni-bremen/libriscv.git++common opts+    ghc-options:    -Wall -Wno-name-shadowing++library libriscv-internal+    import:          opts++    exposed-modules: LibRISCV.Internal.Decoder.Generator+                   , LibRISCV.Internal.Decoder.Opcodes+                   , LibRISCV.Internal.Decoder.Instruction+                   , LibRISCV.Internal.Decoder.YamlParser++    build-depends:+        base+        , yaml                  >= 0.11.8.0 && <0.12+        , containers            >= 0.6.5.1 && <0.7+        , file-embed            >= 0.0.10 && <0.1+        , template-haskell+        , bv++    hs-source-dirs:   internal+    default-language: Haskell2010++library+    import:          opts++    exposed-modules: LibRISCV+                   , LibRISCV.Loader+                   , LibRISCV.CmdLine+                   , LibRISCV.Effects.Decoding.Language+                   , LibRISCV.Effects.Decoding.Default.Interpreter+                   , LibRISCV.Effects.Operations.Language+                   , LibRISCV.Effects.Operations.Default.Interpreter+                   , LibRISCV.Effects.Operations.Default.Machine.Register+                   , LibRISCV.Effects.Operations.Default.Machine.Memory+                   , LibRISCV.Effects.Logging.Language+                   , LibRISCV.Effects.Logging.Default.Interpreter+                   , LibRISCV.Effects.Expressions.Language+                   , LibRISCV.Effects.Expressions.Default.Interpreter+                   , LibRISCV.Effects.Expressions.Expr+                   , LibRISCV.Semantics+    other-modules: LibRISCV.Effects.Expressions.Type+                   , LibRISCV.Effects.Expressions.Generator+                   , LibRISCV.Semantics.Default+                   , LibRISCV.Semantics.Utils+                   , LibRISCV.Semantics.RV_I.Default+                   , LibRISCV.Semantics.RV32_I.Default+                   , LibRISCV.Semantics.RV_M.Default++    -- LANGUAGE extensions used by modules in this package.+    -- other-extensions:+    build-depends:+        libriscv-internal+        , base                  >= 4.15.0.0 && <4.20.0.0+        , array                ^>= 0.5.4.0+        , filepath             ^>= 1.4.2.1+        , bytestring            >= 0.10.10 && <0.12+        , exceptions           ^>= 0.10.4+        , melf                 ^>= 1.3.0+        , freer-simple         ^>= 1.2.1.2+        , transformers          >= 0.5.6.0 && <0.7+        , optparse-applicative  >= 0.16.1 && <0.19+        , bv                   ^>= 0.5+        , parameterized-utils  ^>= 2.1.6.0+        , extra                 >= 1.7.0 && <1.8+        , template-haskell      >= 2.18.0 && <2.22++    hs-source-dirs:   lib+    default-language: Haskell2010++executable riscv-tiny+    import:               opts+    main-is:              Main.hs+    hs-source-dirs:       app+    default-language:     Haskell2010+    build-depends:+        base+        , libriscv+        , freer-simple+        , optparse-applicative+        , bv++test-suite test+    import: opts+    default-language:+      Haskell2010+    type:+      exitcode-stdio-1.0+    hs-source-dirs: test+    main-is: Main.hs++    other-modules:+      DecoderTest+      ArchStateTest++    build-depends:+      libriscv-internal+      , base+      , libriscv+      , array+      , bytestring+      , bv+      , tasty        >= 1.4.2.3+      , tasty-hunit  >= 0.10.0.3

+ test/ArchStateTest.hs view

@@ -0,0 +1,90 @@+module ArchStateTest where++import Data.Array.IO (IOUArray)+import qualified Data.ByteString.Lazy as BSL+import Data.Word+import LibRISCV (RegIdx (..))+import LibRISCV.Effects.Operations.Default.Machine.Memory+import LibRISCV.Effects.Operations.Default.Machine.Register+import Test.Tasty+import Test.Tasty.HUnit++mkReg :: IO (RegisterFile IOUArray Word32)+mkReg = mkRegFile 0++registerTests :: TestTree+registerTests =+    testGroup+        "RegisterFile Tests"+        [ testCase "Read and write general-puropose register" $ do+            r <- mkReg+            writeRegister r A1 23+            regVal <- readRegister r A1+            assertEqual "" 23 regVal+        , testCase "Write zero register" $ do+            r <- mkReg+            writeRegister r Zero 42+            regVal <- readRegister r Zero+            assertEqual "" 0 regVal+        , testCase "Read and write program counter" $ do+            r <- mkReg+            initVal <- readPC r+            assertEqual "PC is zero initially" 0 initVal++            writePC r 1337+            regVal <- readPC r+            assertEqual "PC can be written" 1337 regVal++            writePC r 0+            regVal <- readPC r+            assertEqual "Zero can be written to PC" 0 regVal+        ]++memoryTests :: TestTree+memoryTests =+    testGroup+        "Memory Tests"+        [ testCase "Create memory and extract its size" $ do+            m <- mkMemory 0x0 512 :: IO (Memory IOUArray Word8)+            memSize m >>= assertEqual "" 512+        , testCase "Store and load byte" $ do+            m <- mkMemory 0x0 512 :: IO (Memory IOUArray Word8)+            storeByte m 0x4 0xab+            loadByte m 0x04 >>= assertEqual "" 0xab+        , testCase "Read uninitialized memory" $ do+            m <- mkMemory 0x0 256 :: IO (Memory IOUArray Word8)++            -- We don't really care what this evaluates to. This returns+            -- undefined values which is fine as long as the memory doesn't+            -- error on an uninitialized memory accesses.+            (loadWord m 128 :: IO Word32) >> pure ()+        , testCase "StoreWord in between" $ do+            m <- mkMemory 0x0 12 :: IO (Memory IOUArray Word8)+            storeWord m 0 (0xffffffff :: Word32)+            storeWord m 4 (0xffffffff :: Word32)+            storeWord m 8 (0xffffffff :: Word32)+            storeWord m 0x2 (0x12345678 :: Word32)+            (loadWord m 0 :: IO Word32) >>= assertEqual "1st word" 0x5678ffff+            (loadWord m 4 :: IO Word32) >>= assertEqual "2nd word" 0xffff1234+            (loadWord m 8 :: IO Word32) >>= assertEqual "3rd word" 0xffffffff+        , testCase "Store and load word" $ do+            m <- mkMemory 0x0 256 :: IO (Memory IOUArray Word8)+            storeWord m 8 (0xdeadbeef :: Word32)+            (loadWord m 8 :: IO Word32) >>= assertEqual "Load entire word" 0xdeadbeef+            loadByte m 8 >>= assertEqual "Load 1st byte" 0xef+            loadByte m 9 >>= assertEqual "Load 2nd byte" 0xbe+            loadByte m 11 >>= assertEqual "Load 4th byte" 0xde+        , testCase "Write ByteString in little endian byteorder" $ do+            m <- mkMemory 0x0 32 :: IO (Memory IOUArray Word8)+            let bs = BSL.pack [0xde, 0xad, 0xbe, 0xef]++            storeByteString fromIntegral m 0x0 bs+            (loadWord m 0x0 :: IO Word32) >>= assertEqual "" 0xefbeadde+        , testCase "Write ByteString with multiple bytes" $ do+            m <- mkMemory 0x0 8 :: IO (Memory IOUArray Word8)+            let bs = BSL.pack [0xde, 0xad, 0xbe, 0xef, 0x12, 0x23, 0x34, 0xff]++            storeByteString fromIntegral m 0x0 bs+            (loadWord m 0x0 :: IO Word32) >>= assertEqual "" 0xefbeadde+            (loadWord m 0x4 :: IO Word32) >>= assertEqual "" 0xff342312+        ]

+ test/DecoderTest.hs view

@@ -0,0 +1,75 @@+module DecoderTest where++import Data.Int+import LibRISCV+import LibRISCV.Internal.Decoder.Instruction+import LibRISCV.Internal.Decoder.Opcodes+import Test.Tasty+import Test.Tasty.HUnit++decoderTests :: TestTree+decoderTests =+    testGroup+        "Decoder Tests"+        [ testCase "Decode ADD instruction" $ do+            let inst = 0x00a605b3++            assertEqual "opcode" (RV_I ADD) $ decode inst+            assertEqual "rd" A1 $ toEnum $ fromIntegral $ mkRd inst+            assertEqual "rs1" A2 $ toEnum $ fromIntegral $ mkRs1 inst+            assertEqual "rs2" A0 $ toEnum $ fromIntegral $ mkRs2 inst+        , testCase "Decode ADDI instruction" $ do+            let inst = 0x02a30293++            assertEqual "opcode" (RV_I ADDI) $ decode inst+            assertEqual "rd" T0 $ toEnum $ fromIntegral $ mkRd inst+            assertEqual "rs1" T1 $ toEnum $ fromIntegral $ mkRs1 inst+            assertEqual "immI" 42 $ immI inst+        , testCase "Decode LW instruction" $ do+            let inst = 0xffc52503++            assertEqual "opcode" (RV_I LW) $ decode inst+            assertEqual "rd" A0 $ toEnum $ fromIntegral $ mkRd inst+            assertEqual "rs1" A0 $ toEnum $ fromIntegral $ mkRs1 inst+            assertEqual "immI" (-4) (fromIntegral (immI inst) :: Int32)+        , testCase "Decode AUIPC instruction" $ do+            let inst = 0x00000297++            assertEqual "opcode" (RV_I AUIPC) $ decode inst+            assertEqual "rd" T0 (toEnum $ fromIntegral (mkRd inst))+            assertEqual "immU" 0 (immU inst)+        , testCase "Decode SW instruction" $ do+            let inst = 0x00102423++            assertEqual "opcode" (RV_I SW) $ decode inst+            assertEqual "rs1" Zero (toEnum $ fromIntegral (mkRs1 inst))+            assertEqual "rs2" RA (toEnum $ fromIntegral (mkRs2 inst))+            assertEqual "immS" 8 $ immS inst+        , testCase "Decode JAL instruction" $ do+            let inst = 0xffdff06f++            assertEqual "opcode" (RV_I JAL) $ decode inst+            assertEqual "rd" Zero (toEnum $ fromIntegral (mkRd inst))+            assertEqual "immJ" (-4) (fromIntegral (immJ inst) :: Int32)+        , testCase "Decode BLT instruction" $ do+            let inst = 0x00b54263++            assertEqual "opcode" (RV_I BLT) $ decode inst+            assertEqual "rs1" A0 (toEnum $ fromIntegral (mkRs1 inst))+            assertEqual "rs2" A1 (toEnum $ fromIntegral (mkRs2 inst))+            assertEqual "immB" 4 $ immB inst+        , testCase "Decode SLLI instruction" $ do+            let inst = 0x00129593++            assertEqual "opcode" (RV32_I SLLI) $ decode inst+            assertEqual "rd" A1 (toEnum $ fromIntegral (mkRd inst))+            assertEqual "rs1" T0 (toEnum $ fromIntegral (mkRs1 inst))+            assertEqual "shamt" 01 $ mkShamt inst+        , testCase "Decode SLLI instruction" $ do+            let inst = 0x01f2d693++            assertEqual "opcode" (RV32_I SRLI) $ decode inst+            assertEqual "rd" A3 (toEnum $ fromIntegral (mkRd inst))+            assertEqual "rs1" T0 (toEnum $ fromIntegral (mkRs1 inst))+            assertEqual "shamt" 31 $ mkShamt inst+        ]

+ test/Main.hs view

@@ -0,0 +1,15 @@+import ArchStateTest+import DecoderTest+import Test.Tasty++main :: IO ()+main = defaultMain tests++tests :: TestTree+tests =+    testGroup+        "Tests"+        [ decoderTests+        , registerTests+        , memoryTests+        ]