diff --git a/LICENSE.txt b/LICENSE.txt new file mode 100644 --- /dev/null +++ b/LICENSE.txt @@ -0,0 +1,19 @@ +Copyright (c) 2022-2023 Group of Computer Architecture, University of Bremen + +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. diff --git a/app/Main.hs b/app/Main.hs new file mode 100644 --- /dev/null +++ b/app/Main.hs @@ -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" + ) diff --git a/data/instr_dict.yaml b/data/instr_dict.yaml new file mode 100644 --- /dev/null +++ b/data/instr_dict.yaml @@ -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 diff --git a/internal/LibRISCV/Internal/Decoder/Generator.hs b/internal/LibRISCV/Internal/Decoder/Generator.hs new file mode 100644 --- /dev/null +++ b/internal/LibRISCV/Internal/Decoder/Generator.hs @@ -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 + ] diff --git a/internal/LibRISCV/Internal/Decoder/Instruction.hs b/internal/LibRISCV/Internal/Decoder/Instruction.hs new file mode 100644 --- /dev/null +++ b/internal/LibRISCV/Internal/Decoder/Instruction.hs @@ -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 diff --git a/internal/LibRISCV/Internal/Decoder/Opcodes.hs b/internal/LibRISCV/Internal/Decoder/Opcodes.hs new file mode 100644 --- /dev/null +++ b/internal/LibRISCV/Internal/Decoder/Opcodes.hs @@ -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 diff --git a/internal/LibRISCV/Internal/Decoder/YamlParser.hs b/internal/LibRISCV/Internal/Decoder/YamlParser.hs new file mode 100644 --- /dev/null +++ b/internal/LibRISCV/Internal/Decoder/YamlParser.hs @@ -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 diff --git a/lib/LibRISCV.hs b/lib/LibRISCV.hs new file mode 100644 --- /dev/null +++ b/lib/LibRISCV.hs @@ -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 -} diff --git a/lib/LibRISCV/CmdLine.hs b/lib/LibRISCV/CmdLine.hs new file mode 100644 --- /dev/null +++ b/lib/LibRISCV/CmdLine.hs @@ -0,0 +1,51 @@ +-- | Implementation of common command-line arguments using . +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") diff --git a/lib/LibRISCV/Effects/Decoding/Default/Interpreter.hs b/lib/LibRISCV/Effects/Decoding/Default/Interpreter.hs new file mode 100644 --- /dev/null +++ b/lib/LibRISCV/Effects/Decoding/Default/Interpreter.hs @@ -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 diff --git a/lib/LibRISCV/Effects/Decoding/Language.hs b/lib/LibRISCV/Effects/Decoding/Language.hs new file mode 100644 --- /dev/null +++ b/lib/LibRISCV/Effects/Decoding/Language.hs @@ -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 +-- 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 diff --git a/lib/LibRISCV/Effects/Expressions/Default/Interpreter.hs b/lib/LibRISCV/Effects/Expressions/Default/Interpreter.hs new file mode 100644 --- /dev/null +++ b/lib/LibRISCV/Effects/Expressions/Default/Interpreter.hs @@ -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 diff --git a/lib/LibRISCV/Effects/Expressions/Expr.hs b/lib/LibRISCV/Effects/Expressions/Expr.hs new file mode 100644 --- /dev/null +++ b/lib/LibRISCV/Effects/Expressions/Expr.hs @@ -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 diff --git a/lib/LibRISCV/Effects/Expressions/Generator.hs b/lib/LibRISCV/Effects/Expressions/Generator.hs new file mode 100644 --- /dev/null +++ b/lib/LibRISCV/Effects/Expressions/Generator.hs @@ -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) diff --git a/lib/LibRISCV/Effects/Expressions/Language.hs b/lib/LibRISCV/Effects/Expressions/Language.hs new file mode 100644 --- /dev/null +++ b/lib/LibRISCV/Effects/Expressions/Language.hs @@ -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 ()) diff --git a/lib/LibRISCV/Effects/Expressions/Type.hs b/lib/LibRISCV/Effects/Expressions/Type.hs new file mode 100644 --- /dev/null +++ b/lib/LibRISCV/Effects/Expressions/Type.hs @@ -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. diff --git a/lib/LibRISCV/Effects/Logging/Default/Interpreter.hs b/lib/LibRISCV/Effects/Logging/Default/Interpreter.hs new file mode 100644 --- /dev/null +++ b/lib/LibRISCV/Effects/Logging/Default/Interpreter.hs @@ -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 () diff --git a/lib/LibRISCV/Effects/Logging/Language.hs b/lib/LibRISCV/Effects/Logging/Language.hs new file mode 100644 --- /dev/null +++ b/lib/LibRISCV/Effects/Logging/Language.hs @@ -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 diff --git a/lib/LibRISCV/Effects/Operations/Default/Interpreter.hs b/lib/LibRISCV/Effects/Operations/Default/Interpreter.hs new file mode 100644 --- /dev/null +++ b/lib/LibRISCV/Effects/Operations/Default/Interpreter.hs @@ -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 "" diff --git a/lib/LibRISCV/Effects/Operations/Default/Machine/Memory.hs b/lib/LibRISCV/Effects/Operations/Default/Machine/Memory.hs new file mode 100644 --- /dev/null +++ b/lib/LibRISCV/Effects/Operations/Default/Machine/Memory.hs @@ -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 diff --git a/lib/LibRISCV/Effects/Operations/Default/Machine/Register.hs b/lib/LibRISCV/Effects/Operations/Default/Machine/Register.hs new file mode 100644 --- /dev/null +++ b/lib/LibRISCV/Effects/Operations/Default/Machine/Register.hs @@ -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 diff --git a/lib/LibRISCV/Effects/Operations/Language.hs b/lib/LibRISCV/Effects/Operations/Language.hs new file mode 100644 --- /dev/null +++ b/lib/LibRISCV/Effects/Operations/Language.hs @@ -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 diff --git a/lib/LibRISCV/Loader.hs b/lib/LibRISCV/Loader.hs new file mode 100644 --- /dev/null +++ b/lib/LibRISCV/Loader.hs @@ -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" diff --git a/lib/LibRISCV/Semantics.hs b/lib/LibRISCV/Semantics.hs new file mode 100644 --- /dev/null +++ b/lib/LibRISCV/Semantics.hs @@ -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 diff --git a/lib/LibRISCV/Semantics/Default.hs b/lib/LibRISCV/Semantics/Default.hs new file mode 100644 --- /dev/null +++ b/lib/LibRISCV/Semantics/Default.hs @@ -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 diff --git a/lib/LibRISCV/Semantics/RV32_I/Default.hs b/lib/LibRISCV/Semantics/RV32_I/Default.hs new file mode 100644 --- /dev/null +++ b/lib/LibRISCV/Semantics/RV32_I/Default.hs @@ -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 diff --git a/lib/LibRISCV/Semantics/RV_I/Default.hs b/lib/LibRISCV/Semantics/RV_I/Default.hs new file mode 100644 --- /dev/null +++ b/lib/LibRISCV/Semantics/RV_I/Default.hs @@ -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 diff --git a/lib/LibRISCV/Semantics/RV_M/Default.hs b/lib/LibRISCV/Semantics/RV_M/Default.hs new file mode 100644 --- /dev/null +++ b/lib/LibRISCV/Semantics/RV_M/Default.hs @@ -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 diff --git a/lib/LibRISCV/Semantics/Utils.hs b/lib/LibRISCV/Semantics/Utils.hs new file mode 100644 --- /dev/null +++ b/lib/LibRISCV/Semantics/Utils.hs @@ -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 diff --git a/libriscv.cabal b/libriscv.cabal new file mode 100644 --- /dev/null +++ b/libriscv.cabal @@ -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 /Instruction Set Architecture/ (ISA). + Contrary to other Haskell RISC-V ISA models, like + or , 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 + expressions for of binary code. + . + LibRISCV abstractly describes instruction semantics using an /Embedded Domain Specific Language/ + (EDSL) with . 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 + for practical usage instruction. More detailed information on LibRISCV and its concepts is also + available in a . + +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 +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 diff --git a/test/ArchStateTest.hs b/test/ArchStateTest.hs new file mode 100644 --- /dev/null +++ b/test/ArchStateTest.hs @@ -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 + ] diff --git a/test/DecoderTest.hs b/test/DecoderTest.hs new file mode 100644 --- /dev/null +++ b/test/DecoderTest.hs @@ -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 + ] diff --git a/test/Main.hs b/test/Main.hs new file mode 100644 --- /dev/null +++ b/test/Main.hs @@ -0,0 +1,15 @@ +import ArchStateTest +import DecoderTest +import Test.Tasty + +main :: IO () +main = defaultMain tests + +tests :: TestTree +tests = + testGroup + "Tests" + [ decoderTests + , registerTests + , memoryTests + ]