{-# 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 :: 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 Int
width v
pc =
    let
        fromUInt :: Integer -> Expr v
        fromUInt :: Integer -> Expr v
fromUInt = Int -> Integer -> Expr v
forall a. Int -> Integer -> Expr a
FromInt Int
width

        -- False if a given address is not aligned at the four-byte boundary.
        isMisaligned :: Expr v -> Expr v
        isMisaligned :: Expr v -> Expr v
isMisaligned Expr v
addr = (Expr v
addr Expr v -> Expr v -> Expr v
forall a. Expr a -> Expr a -> Expr a
`And` Integer -> Expr v
fromUInt Integer
0x3) Expr v -> Expr v -> Expr v
forall a. Expr a -> Expr a -> Expr a
`Uge` Integer -> Expr v
fromUInt Integer
1
     in
        \case
            RV_I
ADDI -> do
                (v
r1, v
rd, v
imm) <- forall v (r :: [* -> *]).
(Member (Decoding v) r, Member (Operations v) r) =>
Eff r (v, v, v)
decodeAndReadIType @v
                v -> Expr v -> Eff r ()
forall v (r :: [* -> *]).
(Member (ExprEval v) r, Member (Operations v) r) =>
v -> Expr v -> Eff r ()
writeRegister v
rd (Expr v -> Eff r ()) -> Expr v -> Eff r ()
forall a b. (a -> b) -> a -> b
$ v
r1 v -> v -> Expr v
forall {a}. a -> a -> Expr a
`addImm` v
imm
            RV_I
SLTI -> do
                (v
r1, v
rd, v
imm) <- forall v (r :: [* -> *]).
(Member (Decoding v) r, Member (Operations v) r) =>
Eff r (v, v, v)
decodeAndReadIType @v
                let cond :: Expr v
cond = v
r1 v -> v -> Expr v
forall {a}. a -> a -> Expr a
`slt` v
imm
                v -> Expr v -> Eff r ()
forall v (r :: [* -> *]).
(Member (ExprEval v) r, Member (Operations v) r) =>
v -> Expr v -> Eff r ()
writeRegister v
rd Expr v
cond
            RV_I
SLTIU -> do
                (v
r1, v
rd, v
imm) <- forall v (r :: [* -> *]).
(Member (Decoding v) r, Member (Operations v) r) =>
Eff r (v, v, v)
decodeAndReadIType @v
                let cond :: Expr v
cond = v
r1 v -> v -> Expr v
forall {a}. a -> a -> Expr a
`ult` v
imm
                v -> Expr v -> Eff r ()
forall v (r :: [* -> *]).
(Member (ExprEval v) r, Member (Operations v) r) =>
v -> Expr v -> Eff r ()
writeRegister v
rd Expr v
cond
            RV_I
ANDI -> do
                (v
r1, v
rd, v
imm) <- forall v (r :: [* -> *]).
(Member (Decoding v) r, Member (Operations v) r) =>
Eff r (v, v, v)
decodeAndReadIType @v
                v -> Expr v -> Eff r ()
forall v (r :: [* -> *]).
(Member (ExprEval v) r, Member (Operations v) r) =>
v -> Expr v -> Eff r ()
writeRegister v
rd (Expr v -> Eff r ()) -> Expr v -> Eff r ()
forall a b. (a -> b) -> a -> b
$ v
r1 v -> v -> Expr v
forall {a}. a -> a -> Expr a
`andImm` v
imm
            RV_I
ORI -> do
                (v
r1, v
rd, v
imm) <- forall v (r :: [* -> *]).
(Member (Decoding v) r, Member (Operations v) r) =>
Eff r (v, v, v)
decodeAndReadIType @v
                v -> Expr v -> Eff r ()
forall v (r :: [* -> *]).
(Member (ExprEval v) r, Member (Operations v) r) =>
v -> Expr v -> Eff r ()
writeRegister v
rd (Expr v -> Eff r ()) -> Expr v -> Eff r ()
forall a b. (a -> b) -> a -> b
$ v
r1 v -> v -> Expr v
forall {a}. a -> a -> Expr a
`orImm` v
imm
            RV_I
XORI -> do
                (v
r1, v
rd, v
imm) <- forall v (r :: [* -> *]).
(Member (Decoding v) r, Member (Operations v) r) =>
Eff r (v, v, v)
decodeAndReadIType @v
                v -> Expr v -> Eff r ()
forall v (r :: [* -> *]).
(Member (ExprEval v) r, Member (Operations v) r) =>
v -> Expr v -> Eff r ()
writeRegister v
rd (Expr v -> Eff r ()) -> Expr v -> Eff r ()
forall a b. (a -> b) -> a -> b
$ v
r1 v -> v -> Expr v
forall {a}. a -> a -> Expr a
`xorImm` v
imm
            RV_I
LUI -> do
                (v
rd, v
imm) <- forall v (r :: [* -> *]).
(Member (Decoding v) r, Member (Operations v) r) =>
Eff r (v, v)
decodeUType @v
                v -> Expr v -> Eff r ()
forall v (r :: [* -> *]).
(Member (ExprEval v) r, Member (Operations v) r) =>
v -> Expr v -> Eff r ()
writeRegister v
rd (Expr v -> Eff r ()) -> Expr v -> Eff r ()
forall a b. (a -> b) -> a -> b
$ v -> Expr v
forall a. a -> Expr a
FromImm v
imm
            RV_I
AUIPC -> do
                (v
rd, v
imm) <- Eff r (v, v)
forall v (r :: [* -> *]).
(Member (Decoding v) r, Member (Operations v) r) =>
Eff r (v, v)
decodeUType
                v -> Expr v -> Eff r ()
forall v (r :: [* -> *]).
(Member (ExprEval v) r, Member (Operations v) r) =>
v -> Expr v -> Eff r ()
writeRegister v
rd (Expr v -> Eff r ()) -> Expr v -> Eff r ()
forall a b. (a -> b) -> a -> b
$ v
pc v -> v -> Expr v
forall {a}. a -> a -> Expr a
`addImm` v
imm
            RV_I
ADD -> do
                (v
r1, v
r2, v
rd) <- forall v (r :: [* -> *]).
(Member (Decoding v) r, Member (Operations v) r) =>
Eff r (v, v, v)
decodeAndReadRType @v
                v -> Expr v -> Eff r ()
forall v (r :: [* -> *]).
(Member (ExprEval v) r, Member (Operations v) r) =>
v -> Expr v -> Eff r ()
writeRegister v
rd (Expr v -> Eff r ()) -> Expr v -> Eff r ()
forall a b. (a -> b) -> a -> b
$ v
r1 v -> v -> Expr v
forall {a}. a -> a -> Expr a
`addImm` v
r2
            RV_I
SLT -> do
                (v
r1, v
r2, v
rd) <- Eff r (v, v, v)
forall v (r :: [* -> *]).
(Member (Decoding v) r, Member (Operations v) r) =>
Eff r (v, v, v)
decodeAndReadRType
                let cond :: Expr v
cond = v
r1 v -> v -> Expr v
forall {a}. a -> a -> Expr a
`slt` v
r2 :: Expr v
                v -> Expr v -> Eff r ()
forall v (r :: [* -> *]).
(Member (ExprEval v) r, Member (Operations v) r) =>
v -> Expr v -> Eff r ()
writeRegister v
rd Expr v
cond
            RV_I
SLTU -> do
                (v
r1, v
r2, v
rd) <- Eff r (v, v, v)
forall v (r :: [* -> *]).
(Member (Decoding v) r, Member (Operations v) r) =>
Eff r (v, v, v)
decodeAndReadRType
                let cond :: Expr v
cond = v
r1 v -> v -> Expr v
forall {a}. a -> a -> Expr a
`ult` v
r2 :: Expr v
                v -> Expr v -> Eff r ()
forall v (r :: [* -> *]).
(Member (ExprEval v) r, Member (Operations v) r) =>
v -> Expr v -> Eff r ()
writeRegister v
rd Expr v
cond
            RV_I
AND -> do
                (v
r1, v
r2, v
rd) <- forall v (r :: [* -> *]).
(Member (Decoding v) r, Member (Operations v) r) =>
Eff r (v, v, v)
decodeAndReadRType @v
                v -> Expr v -> Eff r ()
forall v (r :: [* -> *]).
(Member (ExprEval v) r, Member (Operations v) r) =>
v -> Expr v -> Eff r ()
writeRegister v
rd (Expr v -> Eff r ()) -> Expr v -> Eff r ()
forall a b. (a -> b) -> a -> b
$ v
r1 v -> v -> Expr v
forall {a}. a -> a -> Expr a
`andImm` v
r2
            RV_I
OR -> do
                (v
r1, v
r2, v
rd) <- forall v (r :: [* -> *]).
(Member (Decoding v) r, Member (Operations v) r) =>
Eff r (v, v, v)
decodeAndReadRType @v
                v -> Expr v -> Eff r ()
forall v (r :: [* -> *]).
(Member (ExprEval v) r, Member (Operations v) r) =>
v -> Expr v -> Eff r ()
writeRegister v
rd (Expr v -> Eff r ()) -> Expr v -> Eff r ()
forall a b. (a -> b) -> a -> b
$ v
r1 v -> v -> Expr v
forall {a}. a -> a -> Expr a
`orImm` v
r2
            RV_I
XOR -> do
                (v
r1, v
r2, v
rd) <- forall v (r :: [* -> *]).
(Member (Decoding v) r, Member (Operations v) r) =>
Eff r (v, v, v)
decodeAndReadRType @v
                v -> Expr v -> Eff r ()
forall v (r :: [* -> *]).
(Member (ExprEval v) r, Member (Operations v) r) =>
v -> Expr v -> Eff r ()
writeRegister v
rd (Expr v -> Eff r ()) -> Expr v -> Eff r ()
forall a b. (a -> b) -> a -> b
$ v
r1 v -> v -> Expr v
forall {a}. a -> a -> Expr a
`xorImm` v
r2
            RV_I
SLL -> do
                (v
r1, v
r2, v
rd) <- forall v (r :: [* -> *]).
(Member (Decoding v) r, Member (Operations v) r) =>
Eff r (v, v, v)
decodeAndReadRType @v
                v -> Expr v -> Eff r ()
forall v (r :: [* -> *]).
(Member (ExprEval v) r, Member (Operations v) r) =>
v -> Expr v -> Eff r ()
writeRegister v
rd (Expr v -> Eff r ()) -> Expr v -> Eff r ()
forall a b. (a -> b) -> a -> b
$ v -> Expr v
forall a. a -> Expr a
FromImm v
r1 Expr v -> Expr v -> Expr v
forall a. Expr a -> Expr a -> Expr a
`LShl` Int -> Expr v -> Expr v
forall a. Int -> Expr a -> Expr a
regShamt Int
width (v -> Expr v
forall a. a -> Expr a
FromImm v
r2)
            RV_I
SRL -> do
                (v
r1, v
r2, v
rd) <- forall v (r :: [* -> *]).
(Member (Decoding v) r, Member (Operations v) r) =>
Eff r (v, v, v)
decodeAndReadRType @v
                v -> Expr v -> Eff r ()
forall v (r :: [* -> *]).
(Member (ExprEval v) r, Member (Operations v) r) =>
v -> Expr v -> Eff r ()
writeRegister v
rd (Expr v -> Eff r ()) -> Expr v -> Eff r ()
forall a b. (a -> b) -> a -> b
$ v -> Expr v
forall a. a -> Expr a
FromImm v
r1 Expr v -> Expr v -> Expr v
forall a. Expr a -> Expr a -> Expr a
`LShr` Int -> Expr v -> Expr v
forall a. Int -> Expr a -> Expr a
regShamt Int
width (v -> Expr v
forall a. a -> Expr a
FromImm v
r2)
            RV_I
SUB -> do
                (v
r1, v
r2, v
rd) <- forall v (r :: [* -> *]).
(Member (Decoding v) r, Member (Operations v) r) =>
Eff r (v, v, v)
decodeAndReadRType @v
                v -> Expr v -> Eff r ()
forall v (r :: [* -> *]).
(Member (ExprEval v) r, Member (Operations v) r) =>
v -> Expr v -> Eff r ()
writeRegister v
rd (Expr v -> Eff r ()) -> Expr v -> Eff r ()
forall a b. (a -> b) -> a -> b
$ v
r1 v -> v -> Expr v
forall {a}. a -> a -> Expr a
`sub` v
r2
            RV_I
SRA -> do
                (v
r1, v
r2, v
rd) <- forall v (r :: [* -> *]).
(Member (Decoding v) r, Member (Operations v) r) =>
Eff r (v, v, v)
decodeAndReadRType @v
                v -> Expr v -> Eff r ()
forall v (r :: [* -> *]).
(Member (ExprEval v) r, Member (Operations v) r) =>
v -> Expr v -> Eff r ()
writeRegister v
rd (Expr v -> Eff r ()) -> Expr v -> Eff r ()
forall a b. (a -> b) -> a -> b
$ v -> Expr v
forall a. a -> Expr a
FromImm v
r1 Expr v -> Expr v -> Expr v
forall a. Expr a -> Expr a -> Expr a
`AShr` Int -> Expr v -> Expr v
forall a. Int -> Expr a -> Expr a
regShamt Int
width (v -> Expr v
forall a. a -> Expr a
FromImm v
r2)
            RV_I
JAL -> do
                v
nextInstr <- Eff r v
forall v (effs :: [* -> *]).
Member (Operations v) effs =>
Eff effs v
readPC
                (v
rd, v
imm) <- Eff r (v, v)
forall v (r :: [* -> *]).
(Member (Decoding v) r, Member (Operations v) r) =>
Eff r (v, v)
decodeJType

                let newPC :: Expr v
newPC = v
pc v -> v -> Expr v
forall {a}. a -> a -> Expr a
`addImm` v
imm
                Expr v -> Eff r ()
forall v (r :: [* -> *]).
(Member (ExprEval v) r, Member (Operations v) r) =>
Expr v -> Eff r ()
writePC Expr v
newPC
                Expr v -> Eff r () -> Eff r ()
forall v (r :: [* -> *]).
Member (ExprEval v) r =>
Expr v -> Eff r () -> Eff r ()
whenExprM (Expr v -> Expr v
isMisaligned Expr v
newPC) (Eff r () -> Eff r ()) -> Eff r () -> Eff r ()
forall a b. (a -> b) -> a -> b
$
                    v -> String -> Eff r ()
forall v (effs :: [* -> *]).
Member (Operations v) effs =>
v -> String -> Eff effs ()
exception v
pc String
"misaligned PC"
                v -> Expr v -> Eff r ()
forall v (r :: [* -> *]).
(Member (ExprEval v) r, Member (Operations v) r) =>
v -> Expr v -> Eff r ()
writeRegister v
rd (v -> Expr v
forall a. a -> Expr a
FromImm v
nextInstr)
            RV_I
JALR -> do
                v
nextInstr <- Eff r v
forall v (effs :: [* -> *]).
Member (Operations v) effs =>
Eff effs v
readPC
                (v
r1, v
rd, v
imm) <- Eff r (v, v, v)
forall v (r :: [* -> *]).
(Member (Decoding v) r, Member (Operations v) r) =>
Eff r (v, v, v)
decodeAndReadIType

                let newPC :: Expr v
newPC = (v
r1 v -> v -> Expr v
forall {a}. a -> a -> Expr a
`addImm` v
imm) Expr v -> Expr v -> Expr v
forall a. Expr a -> Expr a -> Expr a
`And` Integer -> Expr v
fromUInt Integer
0xfffffffe
                Expr v -> Eff r ()
forall v (r :: [* -> *]).
(Member (ExprEval v) r, Member (Operations v) r) =>
Expr v -> Eff r ()
writePC Expr v
newPC
                Expr v -> Eff r () -> Eff r ()
forall v (r :: [* -> *]).
Member (ExprEval v) r =>
Expr v -> Eff r () -> Eff r ()
whenExprM (Expr v -> Expr v
isMisaligned Expr v
newPC) (Eff r () -> Eff r ()) -> Eff r () -> Eff r ()
forall a b. (a -> b) -> a -> b
$
                    v -> String -> Eff r ()
forall v (effs :: [* -> *]).
Member (Operations v) effs =>
v -> String -> Eff effs ()
exception v
pc String
"misaligned PC"
                v -> Expr v -> Eff r ()
forall v (r :: [* -> *]).
(Member (ExprEval v) r, Member (Operations v) r) =>
v -> Expr v -> Eff r ()
writeRegister v
rd (Expr v -> Eff r ()) -> Expr v -> Eff r ()
forall a b. (a -> b) -> a -> b
$ v -> Expr v
forall a. a -> Expr a
FromImm v
nextInstr
            RV_I
LB -> do
                (v
r1, v
rd, v
imm) <- forall v (r :: [* -> *]).
(Member (Decoding v) r, Member (Operations v) r) =>
Eff r (v, v, v)
decodeAndReadIType @v
                v
byte <- Size -> Expr v -> Eff r v
forall v (r :: [* -> *]).
(Member (ExprEval v) r, Member (Operations v) r) =>
Size -> Expr v -> Eff r v
load Size
Byte (Expr v -> Eff r v) -> Expr v -> Eff r v
forall a b. (a -> b) -> a -> b
$ v
r1 v -> v -> Expr v
forall {a}. a -> a -> Expr a
`addImm` v
imm
                -- TODO: Alignment handling
                v -> Expr v -> Eff r ()
forall v (r :: [* -> *]).
(Member (ExprEval v) r, Member (Operations v) r) =>
v -> Expr v -> Eff r ()
writeRegister v
rd (Expr v -> Eff r ()) -> Expr v -> Eff r ()
forall a b. (a -> b) -> a -> b
$ Int -> v -> Expr v
forall a. Int -> a -> Expr a
sextImm Int
24 v
byte
            RV_I
LBU -> do
                (v
r1, v
rd, v
imm) <- forall v (r :: [* -> *]).
(Member (Decoding v) r, Member (Operations v) r) =>
Eff r (v, v, v)
decodeAndReadIType @v
                -- TODO: Alignment handling
                v
byte <- Size -> Expr v -> Eff r v
forall v (r :: [* -> *]).
(Member (ExprEval v) r, Member (Operations v) r) =>
Size -> Expr v -> Eff r v
load Size
Byte (Expr v -> Eff r v) -> Expr v -> Eff r v
forall a b. (a -> b) -> a -> b
$ v
r1 v -> v -> Expr v
forall {a}. a -> a -> Expr a
`addImm` v
imm
                v -> Expr v -> Eff r ()
forall v (r :: [* -> *]).
(Member (ExprEval v) r, Member (Operations v) r) =>
v -> Expr v -> Eff r ()
writeRegister v
rd (Expr v -> Eff r ()) -> Expr v -> Eff r ()
forall a b. (a -> b) -> a -> b
$ Int -> v -> Expr v
forall a. Int -> a -> Expr a
zextImm Int
24 v
byte
            RV_I
LH -> do
                (v
r1, v
rd, v
imm) <- forall v (r :: [* -> *]).
(Member (Decoding v) r, Member (Operations v) r) =>
Eff r (v, v, v)
decodeAndReadIType @v
                -- TODO: Alignment handling
                v
half <- Size -> Expr v -> Eff r v
forall v (r :: [* -> *]).
(Member (ExprEval v) r, Member (Operations v) r) =>
Size -> Expr v -> Eff r v
load Size
Half (Expr v -> Eff r v) -> Expr v -> Eff r v
forall a b. (a -> b) -> a -> b
$ v
r1 v -> v -> Expr v
forall {a}. a -> a -> Expr a
`addImm` v
imm
                v -> Expr v -> Eff r ()
forall v (r :: [* -> *]).
(Member (ExprEval v) r, Member (Operations v) r) =>
v -> Expr v -> Eff r ()
writeRegister v
rd (Expr v -> Eff r ()) -> Expr v -> Eff r ()
forall a b. (a -> b) -> a -> b
$ Int -> v -> Expr v
forall a. Int -> a -> Expr a
sextImm Int
16 v
half
            RV_I
LHU -> do
                (v
r1, v
rd, v
imm) <- forall v (r :: [* -> *]).
(Member (Decoding v) r, Member (Operations v) r) =>
Eff r (v, v, v)
decodeAndReadIType @v
                -- TODO: Alignment handling
                v
half <- Size -> Expr v -> Eff r v
forall v (r :: [* -> *]).
(Member (ExprEval v) r, Member (Operations v) r) =>
Size -> Expr v -> Eff r v
load Size
Half (Expr v -> Eff r v) -> Expr v -> Eff r v
forall a b. (a -> b) -> a -> b
$ v
r1 v -> v -> Expr v
forall {a}. a -> a -> Expr a
`addImm` v
imm
                v -> Expr v -> Eff r ()
forall v (r :: [* -> *]).
(Member (ExprEval v) r, Member (Operations v) r) =>
v -> Expr v -> Eff r ()
writeRegister v
rd (Expr v -> Eff r ()) -> Expr v -> Eff r ()
forall a b. (a -> b) -> a -> b
$ Int -> v -> Expr v
forall a. Int -> a -> Expr a
zextImm Int
16 v
half
            RV_I
LW -> do
                (v
r1, v
rd, v
imm) <- forall v (r :: [* -> *]).
(Member (Decoding v) r, Member (Operations v) r) =>
Eff r (v, v, v)
decodeAndReadIType @v

                -- TODO: Alignment handling
                v
word <- Size -> Expr v -> Eff r v
forall v (r :: [* -> *]).
(Member (ExprEval v) r, Member (Operations v) r) =>
Size -> Expr v -> Eff r v
load Size
Word (Expr v -> Eff r v) -> Expr v -> Eff r v
forall a b. (a -> b) -> a -> b
$ v
r1 v -> v -> Expr v
forall {a}. a -> a -> Expr a
`addImm` v
imm
                v -> Expr v -> Eff r ()
forall v (r :: [* -> *]).
(Member (ExprEval v) r, Member (Operations v) r) =>
v -> Expr v -> Eff r ()
writeRegister v
rd (Expr v -> Eff r ()) -> Expr v -> Eff r ()
forall a b. (a -> b) -> a -> b
$ v -> Expr v
forall a. a -> Expr a
FromImm v
word
            RV_I
SB -> do
                (v
r1, v
r2, v
imm) <- forall v (r :: [* -> *]).
(Member (Decoding v) r, Member (Operations v) r) =>
Eff r (v, v, v)
decodeAndReadSType @v

                -- TODO: Alignment handling
                Size -> Expr v -> Expr v -> Eff r ()
forall v (r :: [* -> *]).
(Member (ExprEval v) r, Member (Operations v) r) =>
Size -> Expr v -> Expr v -> Eff r ()
store Size
Byte (v
r1 v -> v -> Expr v
forall {a}. a -> a -> Expr a
`addImm` v
imm) (Expr v -> Eff r ()) -> Expr v -> Eff r ()
forall a b. (a -> b) -> a -> b
$ v -> Expr v
forall a. a -> Expr a
FromImm v
r2
            RV_I
SH -> do
                (v
r1, v
r2, v
imm) <- forall v (r :: [* -> *]).
(Member (Decoding v) r, Member (Operations v) r) =>
Eff r (v, v, v)
decodeAndReadSType @v

                -- TODO: Alignment handling
                Size -> Expr v -> Expr v -> Eff r ()
forall v (r :: [* -> *]).
(Member (ExprEval v) r, Member (Operations v) r) =>
Size -> Expr v -> Expr v -> Eff r ()
store Size
Half (v
r1 v -> v -> Expr v
forall {a}. a -> a -> Expr a
`addImm` v
imm) (Expr v -> Eff r ()) -> Expr v -> Eff r ()
forall a b. (a -> b) -> a -> b
$ v -> Expr v
forall a. a -> Expr a
FromImm v
r2
            RV_I
SW -> do
                (v
r1, v
r2, v
imm) <- forall v (r :: [* -> *]).
(Member (Decoding v) r, Member (Operations v) r) =>
Eff r (v, v, v)
decodeAndReadSType @v
                -- TODO: Alignment handling
                Size -> Expr v -> Expr v -> Eff r ()
forall v (r :: [* -> *]).
(Member (ExprEval v) r, Member (Operations v) r) =>
Size -> Expr v -> Expr v -> Eff r ()
store Size
Word (v
r1 v -> v -> Expr v
forall {a}. a -> a -> Expr a
`addImm` v
imm) (Expr v -> Eff r ()) -> Expr v -> Eff r ()
forall a b. (a -> b) -> a -> b
$ v -> Expr v
forall a. a -> Expr a
FromImm v
r2
            RV_I
BEQ -> do
                (v
r1, v
r2, v
imm) <- Eff r (v, v, v)
forall v (r :: [* -> *]).
(Member (Decoding v) r, Member (Operations v) r) =>
Eff r (v, v, v)
decodeAndReadBType

                let addr :: Expr v
addr = v
pc v -> v -> Expr v
forall {a}. a -> a -> Expr a
`add` v
imm
                Expr v -> Eff r () -> Eff r ()
forall v (r :: [* -> *]).
Member (ExprEval v) r =>
Expr v -> Eff r () -> Eff r ()
whenExprM (v
r1 v -> v -> Expr v
forall {a}. a -> a -> Expr a
`eq` v
r2) (Eff r () -> Eff r ()) -> Eff r () -> Eff r ()
forall a b. (a -> b) -> a -> b
$ do
                    Expr v -> Eff r ()
forall v (r :: [* -> *]).
(Member (ExprEval v) r, Member (Operations v) r) =>
Expr v -> Eff r ()
writePC Expr v
addr
                    Expr v -> Eff r () -> Eff r ()
forall v (r :: [* -> *]).
Member (ExprEval v) r =>
Expr v -> Eff r () -> Eff r ()
whenExprM (Expr v -> Expr v
isMisaligned Expr v
addr) (Eff r () -> Eff r ()) -> Eff r () -> Eff r ()
forall a b. (a -> b) -> a -> b
$
                        v -> String -> Eff r ()
forall v (effs :: [* -> *]).
Member (Operations v) effs =>
v -> String -> Eff effs ()
exception v
pc String
"misaligned PC"
            RV_I
BNE -> do
                (v
r1, v
r2, v
imm) <- Eff r (v, v, v)
forall v (r :: [* -> *]).
(Member (Decoding v) r, Member (Operations v) r) =>
Eff r (v, v, v)
decodeAndReadBType

                let addr :: Expr v
addr = v
pc v -> v -> Expr v
forall {a}. a -> a -> Expr a
`add` v
imm
                Expr v -> Eff r () -> Eff r ()
forall v (r :: [* -> *]).
Member (ExprEval v) r =>
Expr v -> Eff r () -> Eff r ()
unlessExprM (v
r1 v -> v -> Expr v
forall {a}. a -> a -> Expr a
`eq` v
r2) (Eff r () -> Eff r ()) -> Eff r () -> Eff r ()
forall a b. (a -> b) -> a -> b
$ do
                    Expr v -> Eff r ()
forall v (r :: [* -> *]).
(Member (ExprEval v) r, Member (Operations v) r) =>
Expr v -> Eff r ()
writePC Expr v
addr
                    Expr v -> Eff r () -> Eff r ()
forall v (r :: [* -> *]).
Member (ExprEval v) r =>
Expr v -> Eff r () -> Eff r ()
whenExprM (Expr v -> Expr v
isMisaligned Expr v
addr) (Eff r () -> Eff r ()) -> Eff r () -> Eff r ()
forall a b. (a -> b) -> a -> b
$
                        v -> String -> Eff r ()
forall v (effs :: [* -> *]).
Member (Operations v) effs =>
v -> String -> Eff effs ()
exception v
pc String
"misaligned PC"
            RV_I
BLT -> do
                (v
r1, v
r2, v
imm) <- Eff r (v, v, v)
forall v (r :: [* -> *]).
(Member (Decoding v) r, Member (Operations v) r) =>
Eff r (v, v, v)
decodeAndReadBType

                let addr :: Expr v
addr = v
pc v -> v -> Expr v
forall {a}. a -> a -> Expr a
`add` v
imm
                Expr v -> Eff r () -> Eff r ()
forall v (r :: [* -> *]).
Member (ExprEval v) r =>
Expr v -> Eff r () -> Eff r ()
whenExprM (v
r1 v -> v -> Expr v
forall {a}. a -> a -> Expr a
`slt` v
r2) (Eff r () -> Eff r ()) -> Eff r () -> Eff r ()
forall a b. (a -> b) -> a -> b
$ do
                    Expr v -> Eff r ()
forall v (r :: [* -> *]).
(Member (ExprEval v) r, Member (Operations v) r) =>
Expr v -> Eff r ()
writePC Expr v
addr
                    Expr v -> Eff r () -> Eff r ()
forall v (r :: [* -> *]).
Member (ExprEval v) r =>
Expr v -> Eff r () -> Eff r ()
whenExprM (Expr v -> Expr v
isMisaligned Expr v
addr) (Eff r () -> Eff r ()) -> Eff r () -> Eff r ()
forall a b. (a -> b) -> a -> b
$
                        v -> String -> Eff r ()
forall v (effs :: [* -> *]).
Member (Operations v) effs =>
v -> String -> Eff effs ()
exception v
pc String
"misaligned PC"
            RV_I
BLTU -> do
                (v
r1, v
r2, v
imm) <- Eff r (v, v, v)
forall v (r :: [* -> *]).
(Member (Decoding v) r, Member (Operations v) r) =>
Eff r (v, v, v)
decodeAndReadBType

                let addr :: Expr v
addr = v
pc v -> v -> Expr v
forall {a}. a -> a -> Expr a
`add` v
imm
                Expr v -> Eff r () -> Eff r ()
forall v (r :: [* -> *]).
Member (ExprEval v) r =>
Expr v -> Eff r () -> Eff r ()
whenExprM (v
r1 v -> v -> Expr v
forall {a}. a -> a -> Expr a
`ult` v
r2) (Eff r () -> Eff r ()) -> Eff r () -> Eff r ()
forall a b. (a -> b) -> a -> b
$ do
                    forall v (r :: [* -> *]).
(Member (ExprEval v) r, Member (Operations v) r) =>
Expr v -> Eff r ()
writePC @v (Expr v -> Eff r ()) -> Expr v -> Eff r ()
forall a b. (a -> b) -> a -> b
$ Expr v
addr
                    Expr v -> Eff r () -> Eff r ()
forall v (r :: [* -> *]).
Member (ExprEval v) r =>
Expr v -> Eff r () -> Eff r ()
whenExprM (Expr v -> Expr v
isMisaligned Expr v
addr) (Eff r () -> Eff r ()) -> Eff r () -> Eff r ()
forall a b. (a -> b) -> a -> b
$
                        v -> String -> Eff r ()
forall v (effs :: [* -> *]).
Member (Operations v) effs =>
v -> String -> Eff effs ()
exception v
pc String
"misaligned PC"
            RV_I
BGE -> do
                (v
r1, v
r2, v
imm) <- Eff r (v, v, v)
forall v (r :: [* -> *]).
(Member (Decoding v) r, Member (Operations v) r) =>
Eff r (v, v, v)
decodeAndReadBType

                let addr :: Expr v
addr = v
pc v -> v -> Expr v
forall {a}. a -> a -> Expr a
`add` v
imm
                Expr v -> Eff r () -> Eff r ()
forall v (r :: [* -> *]).
Member (ExprEval v) r =>
Expr v -> Eff r () -> Eff r ()
whenExprM (v
r1 v -> v -> Expr v
forall {a}. a -> a -> Expr a
`sge` v
r2) (Eff r () -> Eff r ()) -> Eff r () -> Eff r ()
forall a b. (a -> b) -> a -> b
$ do
                    Expr v -> Eff r ()
forall v (r :: [* -> *]).
(Member (ExprEval v) r, Member (Operations v) r) =>
Expr v -> Eff r ()
writePC Expr v
addr
                    Expr v -> Eff r () -> Eff r ()
forall v (r :: [* -> *]).
Member (ExprEval v) r =>
Expr v -> Eff r () -> Eff r ()
whenExprM (Expr v -> Expr v
isMisaligned Expr v
addr) (Eff r () -> Eff r ()) -> Eff r () -> Eff r ()
forall a b. (a -> b) -> a -> b
$
                        v -> String -> Eff r ()
forall v (effs :: [* -> *]).
Member (Operations v) effs =>
v -> String -> Eff effs ()
exception v
pc String
"misaligned PC"
            RV_I
BGEU -> do
                (v
r1, v
r2, v
imm) <- Eff r (v, v, v)
forall v (r :: [* -> *]).
(Member (Decoding v) r, Member (Operations v) r) =>
Eff r (v, v, v)
decodeAndReadBType

                let addr :: Expr v
addr = v
pc v -> v -> Expr v
forall {a}. a -> a -> Expr a
`add` v
imm
                Expr v -> Eff r () -> Eff r ()
forall v (r :: [* -> *]).
Member (ExprEval v) r =>
Expr v -> Eff r () -> Eff r ()
whenExprM (v
r1 v -> v -> Expr v
forall {a}. a -> a -> Expr a
`uge` v
r2) (Eff r () -> Eff r ()) -> Eff r () -> Eff r ()
forall a b. (a -> b) -> a -> b
$ do
                    Expr v -> Eff r ()
forall v (r :: [* -> *]).
(Member (ExprEval v) r, Member (Operations v) r) =>
Expr v -> Eff r ()
writePC Expr v
addr
                    Expr v -> Eff r () -> Eff r ()
forall v (r :: [* -> *]).
Member (ExprEval v) r =>
Expr v -> Eff r () -> Eff r ()
whenExprM (Expr v -> Expr v
isMisaligned Expr v
addr) (Eff r () -> Eff r ()) -> Eff r () -> Eff r ()
forall a b. (a -> b) -> a -> b
$
                        v -> String -> Eff r ()
forall v (effs :: [* -> *]).
Member (Operations v) effs =>
v -> String -> Eff effs ()
exception v
pc String
"misaligned PC"
            RV_I
FENCE -> () -> Eff r ()
forall a. a -> Eff r a
forall (f :: * -> *) a. Applicative f => a -> f a
pure () -- XXX: ignore for now
            RV_I
ECALL -> v -> Eff r ()
forall v (effs :: [* -> *]).
Member (Operations v) effs =>
v -> Eff effs ()
ecall v
pc
            RV_I
EBREAK -> v -> Eff r ()
forall v (effs :: [* -> *]).
Member (Operations v) effs =>
v -> Eff effs ()
ebreak v
pc