{-# LANGUAGE ScopedTypeVariables #-}
module Spec.ExecuteF where
import Spec.Decode
import Spec.Machine
import Utility.Utility
import Spec.VirtualMemory
import qualified Spec.CSRField as Field
import Data.Bits
import Data.Word
import Data.Int
import SoftFloat
import Prelude hiding (isNaN)

canonicalNaN = 0x7fc00000 :: Int32
negativeZero = 0x80000000 :: Int32
positiveZero = 0x00000000 :: Int32
negativeInfinity = 0xff800000 :: Int32
positiveInfinity = 0x7f800000 :: Int32

intToRoundingMode :: MachineInt -> Maybe RoundingMode
intToRoundingMode 0 = Just RoundNearEven
intToRoundingMode 1 = Just RoundMinMag
intToRoundingMode 2 = Just RoundMin
intToRoundingMode 3 = Just RoundMax
intToRoundingMode 4 = Just RoundNearMaxMag
intToRoundingMode _ = Nothing

isNaN :: (Integral t) => t -> Bool
isNaN x = not notNaN
  where Result notNaN _ = f32Eq (fromIntegral x :: Word32) (fromIntegral x :: Word32)

getRoundMode :: (RiscvMachine p t) => MachineInt -> p RoundingMode
getRoundMode rm = do
  frm <- (if rm == 7 then
            getCSRField Field.FRM
          else
            return rm)
  case intToRoundingMode frm of
    Just roundMode -> return roundMode
    Nothing -> raiseException 0 2

boolBit :: (Bits t) => Int -> Bool -> t
boolBit i b = if b then bit i else zeroBits

updateFFlags :: (RiscvMachine p t) => ExceptionFlags -> p ()
updateFFlags (ExceptionFlags inexact underflow overflow infinite invalid) = do
  flags <- getCSRField Field.FFlags
  let flags' = flags .|. boolBit 0 inexact .|. boolBit 1 underflow .|.
               boolBit 2 overflow .|. boolBit 3 infinite .|. boolBit 4 invalid
  setCSRField Field.FFlags flags'

runFPUnary :: (RiscvMachine p t) => (RoundingMode -> Word32 -> F32Result) -> RoundingMode -> Int32 -> p Int32
runFPUnary f roundMode x = do
  let Result y flags = f roundMode (fromIntegral x)
  updateFFlags flags
  if (invalid flags) then
    return canonicalNaN
  else
    return (fromIntegral y)

runFPBinary :: (RiscvMachine p t) => (RoundingMode -> Word32 -> Word32 -> F32Result) -> RoundingMode -> Int32 -> Int32 -> p Int32
runFPBinary f roundMode x y = do
  let Result z flags = f roundMode (fromIntegral x) (fromIntegral y)
  updateFFlags flags
  if (invalid flags) then
    return canonicalNaN
  else
    return (fromIntegral z)

execute :: forall p t. (RiscvMachine p t) => InstructionF -> p ()
execute (Flw rd rs1 oimm12) = do
  a <- getRegister rs1
  addr <- translate Load 4 (a + fromImm oimm12)
  x <- loadWord Execute addr
  setFPRegister rd x
execute (Fsw rs1 rs2 simm12) = do
  a <- getRegister rs1
  addr <- translate Store 4 (a + fromImm simm12)
  x <- getFPRegister rs2
  storeWord Execute addr x
execute (Fmadd_s rd rs1 rs2 rs3 rm) = do
  roundMode <- getRoundMode rm
  v <- getFPRegister rs1
  w <- getFPRegister rs2
  x <- getFPRegister rs3
  y <- runFPBinary f32Mul roundMode v w
  z <- runFPBinary f32Add roundMode y x
  setFPRegister rd z
execute (Fmsub_s rd rs1 rs2 rs3 rm) = do
  roundMode <- getRoundMode rm
  v <- getFPRegister rs1
  w <- getFPRegister rs2
  x <- getFPRegister rs3
  y <- runFPBinary f32Mul roundMode v w
  z <- runFPBinary f32Sub roundMode y x
  setFPRegister rd z
execute (Fnmsub_s rd rs1 rs2 rs3 rm) = do
  roundMode <- getRoundMode rm
  v <- getFPRegister rs1
  w <- getFPRegister rs2
  x <- getFPRegister rs3
  y <- runFPBinary f32Mul roundMode v w
  z <- runFPBinary f32Sub roundMode x y
  setFPRegister rd z
execute (Fnmadd_s rd rs1 rs2 rs3 rm) = do
  roundMode <- getRoundMode rm
  v <- getFPRegister rs1
  w <- getFPRegister rs2
  x <- getFPRegister rs3
  y <- runFPBinary f32Mul roundMode v w
  z <- runFPBinary f32Sub roundMode (xor y (bit 31)) x
  setFPRegister rd z
execute (Fadd_s rd rs1 rs2 rm) = do
  roundMode <- getRoundMode rm
  x <- getFPRegister rs1
  y <- getFPRegister rs2
  z <- runFPBinary f32Add roundMode x y
  setFPRegister rd z
execute (Fsub_s rd rs1 rs2 rm) = do
  roundMode <- getRoundMode rm
  x <- getFPRegister rs1
  y <- getFPRegister rs2
  z <- runFPBinary f32Sub roundMode x y
  setFPRegister rd z
execute (Fmul_s rd rs1 rs2 rm) = do
  roundMode <- getRoundMode rm
  x <- getFPRegister rs1
  y <- getFPRegister rs2
  z <- runFPBinary f32Mul roundMode x y
  setFPRegister rd z
execute (Fdiv_s rd rs1 rs2 rm) = do
  roundMode <- getRoundMode rm
  x <- getFPRegister rs1
  y <- getFPRegister rs2
  z <- runFPBinary f32Div roundMode x y
  setFPRegister rd z
execute (Fsqrt_s rd rs1 rm) = do
  roundMode <- getRoundMode rm
  x <- getFPRegister rs1
  y <- runFPUnary f32Sqrt roundMode x
  setFPRegister rd y
execute (Fsgnj_s rd rs1 rs2) = do
  x <- getFPRegister rs1
  y <- getFPRegister rs2
  setFPRegister rd (bitSlice x 0 31 .|. (y .&. bit 31))
execute (Fsgnjn_s rd rs1 rs2) = do
  x <- getFPRegister rs1
  y <- getFPRegister rs2
  setFPRegister rd (bitSlice x 0 31 .|. (complement y .&. bit 31))
execute (Fsgnjx_s rd rs1 rs2) = do
  x <- getFPRegister rs1
  y <- getFPRegister rs2
  setFPRegister rd (x `xor` (y .&. bit 31))
execute (Fmin_s rd rs1 rs2) = do
  x <- getFPRegister rs1
  y <- getFPRegister rs2
  let Result z flags = f32LtQuiet (fromIntegral x :: Word32) (fromIntegral y :: Word32)
  updateFFlags flags
  -- Special cases and other sheNaNigans. Current behavior (v2.3-draft) differs
  -- from v2.2 of spec.
  let result | x == negativeZero && y == positiveZero = x
             | isNaN x && isNaN y = canonicalNaN
             | isNaN y = x
             | isNaN x = y
             | z = x
             | otherwise = y
  setFPRegister rd result
execute (Fmax_s rd rs1 rs2) = do
  x <- getFPRegister rs1
  y <- getFPRegister rs2
  let Result z flags = f32LtQuiet (fromIntegral x :: Word32) (fromIntegral y :: Word32)
  updateFFlags flags
  -- Special cases and other sheNaNigans. Current behavior (v2.3-draft) differs
  -- from v2.2 of spec.
  let result | x == negativeZero && y == positiveZero = y
             | isNaN x && isNaN y = canonicalNaN
             | isNaN y = x
             | isNaN x = y
             | z = y
             | otherwise = x
  setFPRegister rd result
execute (Fcvt_w_s rd rs1 rm) = do
  roundMode <- getRoundMode rm
  x <- getFPRegister rs1
  let Result y flags = f32ToI32 roundMode (fromIntegral x :: Word32)
  updateFFlags flags
  -- Special case for the softfloat library.
  let result | isNaN x || (y == 2^31 && not (testBit x 31)) = 2^31 - 1
             | otherwise = y
  setRegister rd (fromIntegral result)
execute (Fcvt_wu_s rd rs1 rm) = do
  roundMode <- getRoundMode rm
  x <- getFPRegister rs1
  let Result y flags = f32ToUi32 roundMode (fromIntegral x :: Word32)
  updateFFlags flags
  -- Another special case for the softfloat library.
  let result | not (isNaN x) && testBit x 31 = 0
             | otherwise = y
  setRegister rd (fromIntegral (fromIntegral result :: Int32))
execute (Fmv_x_w rd rs1) = do
  x <- getFPRegister rs1
  setRegister rd (fromIntegral x)
execute (Feq_s rd rs1 rs2) = do
  x <- getFPRegister rs1
  y <- getFPRegister rs2
  let Result z flags = f32Eq (fromIntegral x :: Word32) (fromIntegral y :: Word32)
  updateFFlags flags
  let result = fromIntegral (fromEnum z)
  setRegister rd result
execute (Flt_s rd rs1 rs2) = do
  x <- getFPRegister rs1
  y <- getFPRegister rs2
  let Result z flags = f32Lt (fromIntegral x :: Word32) (fromIntegral y :: Word32)
  updateFFlags flags
  let result = fromIntegral (fromEnum z)
  setRegister rd result
execute (Fle_s rd rs1 rs2) = do
  x <- getFPRegister rs1
  y <- getFPRegister rs2
  let Result z flags = f32Le (fromIntegral x :: Word32) (fromIntegral y :: Word32)
  updateFFlags flags
  let result = fromIntegral (fromEnum z)
  setRegister rd result
execute (Fclass_s rd rs1) = do
  x <- getFPRegister rs1
  let special = bitSlice x 23 31 == 2^8 - 1
  let result | x == negativeInfinity = bit 0
             | x == negativeZero = bit 3
             | x == positiveZero = bit 4
             | x == positiveInfinity = bit 7
             | testBit x 22 && special = bit 9 -- quiet NaN
             | special = bit 8 -- signaling NaN
             | testBit x 22 && testBit x 31 = bit 2 -- negative subnormal
             | testBit x 22 = bit 5 -- positive subnormal
             | testBit x 31 = bit 1 -- negative normal
             | otherwise = bit 6 -- positive normal
  setRegister rd result
execute (Fcvt_s_w rd rs1 rm) = do
  roundMode <- getRoundMode rm
  x <- getRegister rs1
  let Result y flags = i32ToF32 roundMode (fromIntegral x :: Int32)
  updateFFlags flags
  setFPRegister rd (fromIntegral y)
execute (Fcvt_s_wu rd rs1 rm) = do
  roundMode <- getRoundMode rm
  x <- getRegister rs1
  let Result y flags = ui32ToF32 roundMode (fromIntegral x :: Word32)
  updateFFlags flags
  setFPRegister rd (fromIntegral y)
execute (Fmv_w_x rd rs1) = do
  x <- getRegister rs1
  setFPRegister rd (fromIntegral x)
execute inst = error $ "dispatch bug: " ++ show inst
