{-# 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 :: Expr BV -> BV
evalE (FromImm BV
a) = BV
a
evalE (FromInt Int
n Integer
i) = Int -> Integer -> BV
forall a. Integral a => Int -> a -> BV
bitVec Int
n Integer
i
evalE (ZExt Int
n Expr BV
e) = Int -> BV -> BV
forall size. Integral size => size -> BV -> BV
zeroExtend Int
n (Expr BV -> BV
evalE Expr BV
e)
evalE (SExt Int
n Expr BV
e) = Int -> BV -> BV
forall size. Integral size => size -> BV -> BV
signExtend Int
n (Expr BV -> BV
evalE Expr BV
e)
evalE (Extract Int
start Int
len Expr BV
e) = Int -> Int -> BV -> BV
forall ix. Integral ix => ix -> ix -> BV -> BV
extract (Int
start Int -> Int -> Int
forall a. Num a => a -> a -> a
+ (Int
len Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)) Int
start (Expr BV -> BV
evalE Expr BV
e)
evalE (Add Expr BV
e1 Expr BV
e2) = Expr BV -> BV
evalE Expr BV
e1 BV -> BV -> BV
forall a. Num a => a -> a -> a
+ Expr BV -> BV
evalE Expr BV
e2
evalE (Sub Expr BV
e1 Expr BV
e2) =
    Int32 -> BV
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int32 -> BV) -> Int32 -> BV
forall a b. (a -> b) -> a -> b
$
        (BV -> Int32
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Expr BV -> BV
evalE Expr BV
e1) :: Int32) Int32 -> Int32 -> Int32
forall a. Num a => a -> a -> a
- BV -> Int32
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Expr BV -> BV
evalE Expr BV
e2)
evalE (Eq Expr BV
e1 Expr BV
e2) = BV -> BV -> Bool -> BV
forall a. a -> a -> Bool -> a
bool BV
0 BV
1 (Bool -> BV) -> Bool -> BV
forall a b. (a -> b) -> a -> b
$ (BV -> Int32
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Expr BV -> BV
evalE Expr BV
e1) :: Int32) Int32 -> Int32 -> Bool
forall a. Eq a => a -> a -> Bool
== BV -> Int32
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Expr BV -> BV
evalE Expr BV
e2)
evalE (Slt Expr BV
e1 Expr BV
e2) = BV -> BV -> Bool -> BV
forall a. a -> a -> Bool -> a
bool BV
0 BV
1 (Bool -> BV) -> Bool -> BV
forall a b. (a -> b) -> a -> b
$ (BV -> Int32
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Expr BV -> BV
evalE Expr BV
e1) :: Int32) Int32 -> Int32 -> Bool
forall a. Ord a => a -> a -> Bool
< BV -> Int32
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Expr BV -> BV
evalE Expr BV
e2)
evalE (Sge Expr BV
e1 Expr BV
e2) = BV -> BV -> Bool -> BV
forall a. a -> a -> Bool -> a
bool BV
0 BV
1 (Bool -> BV) -> Bool -> BV
forall a b. (a -> b) -> a -> b
$ (BV -> Int32
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Expr BV -> BV
evalE Expr BV
e1) :: Int32) Int32 -> Int32 -> Bool
forall a. Ord a => a -> a -> Bool
>= BV -> Int32
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Expr BV -> BV
evalE Expr BV
e2)
evalE (Ult Expr BV
e1 Expr BV
e2) = BV -> BV -> Bool -> BV
forall a. a -> a -> Bool -> a
bool BV
0 BV
1 (Bool -> BV) -> Bool -> BV
forall a b. (a -> b) -> a -> b
$ Expr BV -> BV
evalE Expr BV
e1 BV -> BV -> Bool
forall a. Ord a => a -> a -> Bool
< Expr BV -> BV
evalE Expr BV
e2
evalE (Uge Expr BV
e1 Expr BV
e2) = BV -> BV -> Bool -> BV
forall a. a -> a -> Bool -> a
bool BV
0 BV
1 (Bool -> BV) -> Bool -> BV
forall a b. (a -> b) -> a -> b
$ Expr BV -> BV
evalE Expr BV
e1 BV -> BV -> Bool
forall a. Ord a => a -> a -> Bool
>= Expr BV -> BV
evalE Expr BV
e2
evalE (And Expr BV
e1 Expr BV
e2) = Expr BV -> BV
evalE Expr BV
e1 BV -> BV -> BV
forall a. Bits a => a -> a -> a
.&. Expr BV -> BV
evalE Expr BV
e2
evalE (Or Expr BV
e1 Expr BV
e2) = Expr BV -> BV
evalE Expr BV
e1 BV -> BV -> BV
forall a. Bits a => a -> a -> a
.|. Expr BV -> BV
evalE Expr BV
e2
evalE (Xor Expr BV
e1 Expr BV
e2) = Expr BV -> BV
evalE Expr BV
e1 BV -> BV -> BV
forall a. Bits a => a -> a -> a
`xor` Expr BV -> BV
evalE Expr BV
e2
evalE (LShl Expr BV
e1 Expr BV
e2) = Expr BV -> BV
evalE Expr BV
e1 BV -> Int -> BV
forall a. Bits a => a -> Int -> a
`unsafeShiftL` Word8 -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (BV -> Word8
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Expr BV -> BV
evalE Expr BV
e2) :: Word8)
evalE (LShr Expr BV
e1 Expr BV
e2) = Expr BV -> BV
evalE Expr BV
e1 BV -> Int -> BV
forall a. Bits a => a -> Int -> a
`unsafeShiftR` Word8 -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (BV -> Word8
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Expr BV -> BV
evalE Expr BV
e2) :: Word8)
evalE (AShr Expr BV
e1 Expr BV
e2) = Int32 -> BV
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int32 -> BV) -> Int32 -> BV
forall a b. (a -> b) -> a -> b
$ (BV -> Int32
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Expr BV -> BV
evalE Expr BV
e1) :: Int32) Int32 -> Int -> Int32
forall a. Bits a => a -> Int -> a
`unsafeShiftR` Word8 -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (BV -> Word8
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Expr BV -> BV
evalE Expr BV
e2) :: Word8)
evalE (Mul Expr BV
e1 Expr BV
e2) = Expr BV -> BV
evalE Expr BV
e1 BV -> BV -> BV
forall a. Num a => a -> a -> a
* Expr BV -> BV
evalE Expr BV
e2
evalE (SDiv Expr BV
e1 Expr BV
e2) = Int32 -> BV
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int32 -> BV) -> Int32 -> BV
forall a b. (a -> b) -> a -> b
$ forall a b. (Integral a, Num b) => a -> b
fromIntegral @_ @Int32 (Expr BV -> BV
evalE Expr BV
e1) Int32 -> Int32 -> Int32
forall a. Integral a => a -> a -> a
`quot` BV -> Int32
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Expr BV -> BV
evalE Expr BV
e2)
evalE (SRem Expr BV
e1 Expr BV
e2) = Int32 -> BV
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int32 -> BV) -> Int32 -> BV
forall a b. (a -> b) -> a -> b
$ forall a b. (Integral a, Num b) => a -> b
fromIntegral @_ @Int32 (Expr BV -> BV
evalE Expr BV
e1) Int32 -> Int32 -> Int32
forall a. Integral a => a -> a -> a
`rem` BV -> Int32
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Expr BV -> BV
evalE Expr BV
e2)
evalE (UDiv Expr BV
e1 Expr BV
e2) = Expr BV -> BV
evalE Expr BV
e1 BV -> BV -> BV
forall a. Integral a => a -> a -> a
`quot` Expr BV -> BV
evalE Expr BV
e2
evalE (URem Expr BV
e1 Expr BV
e2) = Expr BV -> BV
evalE Expr BV
e1 BV -> BV -> BV
forall a. Integral a => a -> a -> a
`rem` Expr BV -> BV
evalE Expr BV
e2

-- | Concrete implementation of the 'ExprEval' effect.
defaultEval :: (MonadIO m) => (v -> Bool, Expr v -> v) -> ExprEval v ~> m
defaultEval :: forall (m :: * -> *) v.
MonadIO m =>
(v -> Bool, Expr v -> v) -> ExprEval v ~> m
defaultEval (v -> Bool
pred, Expr v -> v
evalE) =
    x -> m x
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (x -> m x) -> (ExprEval v x -> x) -> ExprEval v x -> m x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. \case
        Eval Expr v
e -> Expr v -> v
evalE Expr v
e
        IsTrue Expr v
e -> v -> Bool
pred (v -> Bool) -> v -> Bool
forall a b. (a -> b) -> a -> b
$ Expr v -> v
evalE Expr v
e
        IsFalse Expr v
e -> Bool -> x
Bool -> Bool
not (Bool -> x) -> (v -> Bool) -> v -> x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. v -> Bool
pred (v -> x) -> v -> x
forall a b. (a -> b) -> a -> b
$ Expr v -> v
evalE Expr v
e