Improve documentation for the expression abstraction

app/Main.hs

@@ -16,8 +16,7 @@ import LibRISCV.Effects.Logging.Default.Interpreter
 import LibRISCV.Effects.Operations.Default.Interpreter
     ( mkArchState, dumpState, defaultInstructions )
 import qualified LibRISCV.Effects.Expressions.Expr as E
-import LibRISCV.Effects.Expressions.Default.Interpreter (defaultEval)
-import LibRISCV.Effects.Expressions.Default.EvalE ( evalE )
+import LibRISCV.Effects.Expressions.Default.Interpreter (defaultEval, evalE)
 import LibRISCV.Effects.Decoding.Default.Interpreter
     ( defaultDecoding )
 import Data.BitVector 

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

@@ -1,13 +1,49 @@
 {-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE TypeApplications #-}
 {-# LANGUAGE TypeOperators #-}
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE GADTs #-}
+
+-- | Provides the default (concrete) evaluation of the expression abstraction.
 module LibRISCV.Effects.Expressions.Default.Interpreter where
+
+import Data.Int ( Int32 )
+import Data.Word ( Word8 )
+import Data.Bool ( bool )
+import Data.BitVector (BV, extract, Bits (unsafeShiftR, unsafeShiftL, xor, (.|.), (.&.)), signExtend, zeroExtend, bitVec, ones)
 import Control.Monad.IO.Class ( MonadIO )
 import LibRISCV.Effects.Expressions.Language ( ExprEval(..) )
-import LibRISCV.Effects.Expressions.Expr ( Expr )
+import LibRISCV.Effects.Expressions.Expr ( Expr(..) )
 import Control.Monad.Freer ( type (~>) )
 
+-- | 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

lib/LibRISCV/Effects/Expressions/Expr.hs

@@ -1,8 +1,11 @@
 {-# LANGUAGE TemplateHaskell #-}
 
--- This module provides an additional abstraction for the LibRISCV
--- expression language. Some of the provided abstractions are generated
--- using template-haskell and LibRISCV.Effects.Expressions.Generator.
+-- | 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,
@@ -13,7 +16,7 @@ import Data.BitVector (BV)
 import LibRISCV.Effects.Expressions.Type
 import LibRISCV.Effects.Expressions.Generator
 
--- Extract shamt value from an expression (lower 5 bits).
+-- | Extract shamt value from an expression (lower 5 bits).
 regShamt :: Int -> Expr a -> Expr a
 regShamt w a = a `And` FromInt w 0x1f
 

lib/LibRISCV/Effects/Expressions/Language.hs

@@ -6,14 +6,21 @@
 {-# LANGUAGE ImpredicativeTypes #-}
 {-# LANGUAGE AllowAmbiguousTypes #-}
 {-# LANGUAGE LambdaCase #-}
+
+-- | Implements an effect for /evaluation/ of the 'Expr' abstraction. The effect
+-- differentiates evaluating to a 'Bool' (via 'IsTrue' / 'IsFalse') and evaluatation
+-- to the enclosing value type (via 'Eval').
 module LibRISCV.Effects.Expressions.Language where
 
 import LibRISCV.Effects.Expressions.Expr (Expr)
 import Control.Monad.Freer.TH (makeEffect)
 import Control.Monad.IO.Class (MonadIO)
-import Control.Monad.Freer ( type (~>) ) 
-
+import Control.Monad.Freer ( type (~>) )
 
+-- TODO: The distinction between IsTrue (i.e. take the path it evaluates to true)
+-- and IsFalse is primarily interesting for symbolic execution as we need to know
+-- if a branch is (not) taken depending on the expression. Would be cool to come
+-- up with a better abstraction for this.
 data ExprEval v r where
     IsTrue :: Expr v -> ExprEval v Bool
     IsFalse :: Expr v -> ExprEval v Bool

lib/LibRISCV/Effects/Expressions/Type.hs

@@ -2,10 +2,18 @@ module LibRISCV.Effects.Expressions.Type where
 
 data Expr a =
     FromImm a |
+    -- ^ Create a new 'Expr' from a given immediate value.
     FromInt Int Integer |
+    -- ^ 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.
     ZExt Int (Expr a) |
+    -- ^ 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.
     SExt Int (Expr a) |
+    -- ^ Same as 'ZExt' but performs sign-extension instead of zero-extension.
     Extract Int 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.
     Add  (Expr a) (Expr a) |
     Sub  (Expr a) (Expr a) |
     Eq   (Expr a) (Expr a) |

libriscv.cabal

@@ -70,7 +70,6 @@ library
                    , LibRISCV.Effects.Logging.Default.Interpreter
                    , LibRISCV.Effects.Expressions.Language
                    , LibRISCV.Effects.Expressions.Default.Interpreter
-                   , LibRISCV.Effects.Expressions.Default.EvalE
                    , LibRISCV.Effects.Expressions.Expr
                    , LibRISCV.Semantics
     other-modules: LibRISCV.Utils

riscv-tests/Main.hs

@@ -29,7 +29,6 @@ import LibRISCV.Effects.Operations.Default.Interpreter
 import LibRISCV.Effects.Operations.Language
 import qualified LibRISCV.Effects.Expressions.Expr as E
 import LibRISCV.Effects.Expressions.Default.Interpreter
-import LibRISCV.Effects.Expressions.Default.EvalE 
 import LibRISCV.Effects.Decoding.Default.Interpreter
 import LibRISCV.Effects.Operations.Default.Machine.Memory (storeByteString)