content: {-# LANGUAGE DataKinds #-}
  {-# LANGUAGE FlexibleContexts #-}
  {-# LANGUAGE GADTs #-}
  {-# LANGUAGE KindSignatures #-}
  {-# LANGUAGE LambdaCase #-}
  {-# LANGUAGE PolyKinds #-}
  {-# LANGUAGE RankNTypes #-}
  {-# LANGUAGE ScopedTypeVariables #-}
  {-# LANGUAGE TemplateHaskell #-}
  {-# LANGUAGE TypeFamilies #-}
  {-# LANGUAGE TypeOperators #-}
  {-# LANGUAGE TypeApplications #-}
  
  module Data.Macaw.PPC.Semantics.TH (
    ppcAppEvaluator,
    ppcNonceAppEval
    ) where
  
  import qualified Data.Functor.Const as C
  import           Data.Proxy ( Proxy(..) )
  import qualified Data.List as L
  import           Language.Haskell.TH
  import           Language.Haskell.TH.Syntax (lift)
  
  import           Data.Parameterized.Classes
  import qualified Data.Parameterized.Map as Map
  import           Data.Parameterized.Some ( Some(..) )
  import qualified Data.Parameterized.TraversableFC as FC
  import qualified What4.Expr.Builder as S
  import qualified What4.Interface as S
  
  import qualified SemMC.Architecture as A
  import qualified SemMC.Architecture.PPC as SP
  import qualified SemMC.Architecture.PPC.Eval as PE
  import qualified SemMC.Util as U
  import qualified Data.Macaw.CFG as M
  import qualified Data.Macaw.Memory as MM
  import qualified Data.Macaw.Types as M
  
  import qualified Data.Macaw.SemMC.Generator as G
  import qualified Data.Macaw.SemMC.Operands as O
  import qualified Data.Macaw.SemMC.Simplify as MSS
  import           Data.Macaw.SemMC.TH.Monad
  import           Data.Macaw.SemMC.TH ( natReprTH, floatInfoFromPrecisionTH, addEltTH, symFnName, asName )
  
  import           Data.Macaw.PPC.Arch
  
  getOpName :: S.Expr t x -> Maybe String
  getOpName e
    | S.NonceAppExpr nae <- e
    , S.FnApp fn _ <- S.nonceExprApp nae =
      Just $ show $ S.symFnName fn
    | otherwise = Nothing
  
  ppcNonceAppEval :: forall v t fs tp
                   . (A.Architecture (SP.AnyPPC v))
                  => BoundVarInterpretations (SP.AnyPPC v) t fs
                  -> S.NonceApp t (S.Expr t) tp
                  -> Maybe (MacawQ (SP.AnyPPC v) t fs Exp)
  ppcNonceAppEval bvi nonceApp =
    case nonceApp of
      S.FnApp symFn args -> do
        let fnName = symFnName symFn
        case fnName of
          "uf_fp_un_op_fpscr" -> return $
            case FC.toListFC Some args of
              [Some op, Some frA, Some fpscr] -> case getOpName op of
                Just name -> do
                  valA <- addEltTH M.BigEndian bvi frA
                  valFpscr <- addEltTH M.BigEndian bvi fpscr
                  liftQ [|
                      addArchExpr =<<
                          (FPSCR1 $(lift name) <$> $(refBinding valA) <*> $(refBinding valFpscr))
                    |]
                Nothing ->
                  fail $ "Invalid argument list for un_op_fpscr: " ++ showF args
              _ -> fail $ "Invalid argument list for un_op_fpscr: " ++ showF args
          "uf_fp_bin_op_fpscr" -> return $
            case FC.toListFC Some args of
              [Some op, Some frA, Some frB, Some fpscr] -> case getOpName op of
                Just name -> do
                  valA <- addEltTH M.BigEndian bvi frA
                  valB <- addEltTH M.BigEndian bvi frB
                  valFpscr <- addEltTH M.BigEndian bvi fpscr
                  liftQ [|
                      addArchExpr =<< (FPSCR2
                        $(lift name) <$>
                        $(refBinding valA) <*>
                        $(refBinding valB) <*>
                        $(refBinding valFpscr))
                    |]
                Nothing ->
                  fail $ "Invalid argument list for un_op_fpscr: " ++ showF args
              _ -> fail $ "Invalid argument list for bin_op_fpscr: " ++ showF args
          "uf_fp_tern_op_fpscr" -> return $
            case FC.toListFC Some args of
              [Some op, Some frA, Some frB, Some frC, Some fpscr] ->
                case getOpName op of
                  Just name -> do
                    valA <- addEltTH M.BigEndian bvi frA
                    valB <- addEltTH M.BigEndian bvi frB
                    valC <- addEltTH M.BigEndian bvi frC
                    valFpscr <- addEltTH M.BigEndian bvi fpscr
                    liftQ [|
                        addArchExpr =<< (FPSCR3
                          $(lift name) <$>
                          $(refBinding valA) <*>
                          $(refBinding valB) <*>
                          $(refBinding valC) <*>
                          $(refBinding valFpscr))
                      |]
                  Nothing -> fail $
                    "Invalid argument list for un_op_fpscr: " ++ showF args
              _ -> fail $ "Invalid argument list for tern_op_fpscr: " ++ showF args
          "uf_ppc_fp1" -> return $ do
            case FC.toListFC Some args of
              [Some op, Some frA, Some fpscr] -> do
                case getOpName op of
                  Just name -> do
                    valA <- addEltTH M.BigEndian bvi frA
                    valFpscr <- addEltTH M.BigEndian bvi fpscr
                    liftQ [| addArchExpr =<< (FP1 $(lift name) <$> $(refBinding valA) <*> $(refBinding valFpscr)) |]
                  Nothing -> fail $ "Invalid argument list for ppc.fp1: " ++ showF args
              _ -> fail $ "Invalid argument list for ppc.fp1: " ++ showF args
          "uf_ppc_fp2" -> return $ do
            case FC.toListFC Some args of
              [Some op, Some frA, Some frB, Some fpscr] -> do
                case getOpName op of
                  Just name -> do
                    valA <- addEltTH M.BigEndian bvi frA
                    valB <- addEltTH M.BigEndian bvi frB
                    valFpscr <- addEltTH M.BigEndian bvi fpscr
                    liftQ [| addArchExpr =<< (FP2 $(lift name) <$> $(refBinding valA) <*> $(refBinding valB) <*> $(refBinding valFpscr)) |]
                  Nothing -> fail $ "Invalid argument list for ppc.fp2: " ++ showF args
              _ -> fail $ "Invalid argument list for ppc.fp2: " ++ showF args
          "uf_ppc_fp3" -> return $ do
            case FC.toListFC Some args of
              [Some op, Some frA, Some frB, Some frC, Some fpscr] -> do
                case getOpName op of
                  Just name -> do
                    valA <- addEltTH M.BigEndian bvi frA
                    valB <- addEltTH M.BigEndian bvi frB
                    valC <- addEltTH M.BigEndian bvi frC
                    valFpscr <- addEltTH M.BigEndian bvi fpscr
                    liftQ [| addArchExpr =<< (FP3 $(lift name) <$> $(refBinding valA) <*> $(refBinding valB) <*> $(refBinding valC) <*> $(refBinding valFpscr)) |]
                  Nothing -> fail $ "Invalid argument list for ppc.fp2: " ++ showF args
              _ -> fail $ "Invalid argument list for ppc.fp2: " ++ showF args
          "uf_ppc_vec1" -> return $ do
            case FC.toListFC Some args of
              [Some op, Some rA, Some vscr] -> do
                case getOpName op of
                  Just name -> do
                    valA <- addEltTH M.BigEndian bvi rA
                    valVscr <- addEltTH M.BigEndian bvi vscr
                    liftQ [| addArchExpr =<< (Vec1 $(lift name) <$> $(refBinding valA) <*> $(refBinding valVscr)) |]
                  Nothing -> fail $ "Invalid argument list for ppc.vec1: " ++ showF args
              _ -> fail $ "Invalid argument list for ppc.vec1: " ++ showF args
          "uf_ppc_vec2" -> return $ do
            case FC.toListFC Some args of
              [Some op, Some rA, Some rB, Some vscr] -> do
                case getOpName op of
                  Just name -> do
                    valA <- addEltTH M.BigEndian bvi rA
                    valB <- addEltTH M.BigEndian bvi rB
                    valVscr <- addEltTH M.BigEndian bvi vscr
                    liftQ [| addArchExpr =<< (Vec2 $(lift name) <$> $(refBinding valA) <*> $(refBinding valB) <*> $(refBinding valVscr)) |]
                  Nothing -> fail $ "Invalid argument list for ppc.vec2: " ++ showF args
              _ -> fail $ "Invalid argument list for ppc.vec2: " ++ showF args
          "uf_ppc_vec3" -> return $ do
            case FC.toListFC Some args of
              [Some op, Some rA, Some rB, Some rC, Some vscr] -> do
                case getOpName op of
                  Just name -> do
                    valA <- addEltTH M.BigEndian bvi rA
                    valB <- addEltTH M.BigEndian bvi rB
                    valC <- addEltTH M.BigEndian bvi rC
                    valVscr <- addEltTH M.BigEndian bvi vscr
                    liftQ [| addArchExpr =<< (Vec3 $(lift name) <$> $(refBinding valA) <*> $(refBinding valB) <*> $(refBinding valC) <*> $(refBinding valVscr)) |]
                  Nothing -> fail $ "Invalid argument list for ppc.vec3: " ++ showF args
              _ -> fail $ "Invalid argument list for ppc.vec3: " ++ showF args
          "uf_ppc_is_r0" -> return $ do
            case FC.toListFC Some args of
              [Some operand] -> do
                -- The operand can be either a variable (TH name bound from
                -- matching on the instruction operand list) or a call on such.
                case operand of
                  S.BoundVarExpr bv -> do
                    case Map.lookup bv (opVars bvi) of
                      Just (C.Const name) -> liftQ [| return $ O.extractValue $(varE (regsValName bvi)) (PE.interpIsR0 $(varE name)) |]
                      Nothing -> fail ("bound var not found: " ++ show bv)
                  S.NonceAppExpr nonceApp' -> do
                    case S.nonceExprApp nonceApp' of
                      S.FnApp symFn' args' -> do
                        let recName = symFnName symFn'
                        case lookup recName (A.locationFuncInterpretation (Proxy @(SP.AnyPPC v))) of
                          Nothing -> fail ("Unsupported UF: " ++ recName)
                          Just fi -> do
                            case FC.toListFC (asName fnName bvi) args' of
                              [] -> fail ("zero-argument uninterpreted functions are not supported: " ++ fnName)
                              argNames -> do
                                let call = appE (varE (A.exprInterpName fi)) $ foldr1 appE (map varE argNames)
                                liftQ [| return $ O.extractValue $(varE (regsValName bvi)) (PE.interpIsR0 ($(call))) |]
                      _ -> fail ("Unsupported nonce app type")
                  _ -> fail "Unsupported operand to ppc.is_r0"
              _ -> fail ("Invalid argument list for ppc.is_r0: " ++ showF args)
          _ | Just fpFunc <- elementaryFPName fnName -> return (floatingPointTH bvi fpFunc args)
            | otherwise -> Nothing
      _ -> Nothing
  
  elementaryFPName :: String -> Maybe String
  elementaryFPName = L.stripPrefix "uf_fp_"
  
  addArchAssignment
    :: ( M.HasRepr (M.ArchFn arch (M.Value arch ids)) M.TypeRepr
       , MSS.SimplifierExtension arch
       , OrdF (M.ArchReg arch)
       , MM.MemWidth (M.ArchAddrWidth arch)
       , ShowF (M.ArchReg arch)
       )
    => M.ArchFn arch (M.Value arch ids) tp
    -> G.Generator arch ids s (G.Expr arch ids tp)
  addArchAssignment expr = G.ValueExpr . M.AssignedValue <$>
    G.addAssignment (M.EvalArchFn expr (M.typeRepr expr))
  
  addArchExpr
    :: ( MM.MemWidth (M.RegAddrWidth (M.ArchReg arch))
       , OrdF (M.ArchReg arch)
       , M.HasRepr (M.ArchFn arch (M.Value arch ids)) M.TypeRepr
       , MSS.SimplifierExtension arch
       , ShowF (M.ArchReg arch)
       )
    => M.ArchFn arch (M.Value arch ids) tp
    -> G.Generator arch ids s (M.Value arch ids tp)
  addArchExpr expr = G.addExpr =<< addArchAssignment expr
  
  floatingPointTH :: forall v t fs f c
                   . ( A.Architecture (SP.AnyPPC v),
                       MSS.SimplifierExtension (SP.AnyPPC v),
                       FC.FoldableFC f)
                   => BoundVarInterpretations (SP.AnyPPC v) t fs
                   -> String
                   -> f (S.Expr t) c
                   -> MacawQ (SP.AnyPPC v) t fs Exp
  floatingPointTH bvi fnName args =
    case FC.toListFC Some args of
      [Some a] -> case fnName of
        "double_to_single" -> do
          fpval <- addEltTH M.BigEndian bvi a
          liftQ [|
              addArchExpr =<<
                  (FPCoerce M.SingleFloatRepr M.DoubleFloatRepr <$> $(refBinding fpval))
            |]
        _ -> fail ("Unsupported unary floating point intrinsic: " ++ fnName)
      [Some _a, Some _b] ->
        case fnName of
          _ -> fail ("Unsupported binary floating point intrinsic: " ++ fnName)
      [Some _a, Some _b, Some _c] ->
        case fnName of
          _ -> fail ("Unsupported ternary floating point intrinsic: " ++ fnName)
      _ -> fail ("Unsupported floating point intrinsic: " ++ fnName)
  
  
  
  ppcAppEvaluator :: (A.Architecture (SP.AnyPPC v),
                      MSS.SimplifierExtension (SP.AnyPPC v)
                     )
                  => BoundVarInterpretations (SP.AnyPPC v) t fs
                  -> S.App (S.Expr t) ctp
                  -> Maybe (MacawQ (SP.AnyPPC v) t fs Exp)
  ppcAppEvaluator interps = \case
    S.BVSdiv w bv1 bv2 -> return $ do
      e1 <- addEltTH M.BigEndian interps bv1
      e2 <- addEltTH M.BigEndian interps bv2
      liftQ [| addArchExpr =<< (SDiv $(natReprTH w) <$> $(refBinding e1) <*> $(refBinding e2))
             |]
    S.BVUdiv w bv1 bv2 -> return $ do
      e1 <- addEltTH M.BigEndian interps bv1
      e2 <- addEltTH M.BigEndian interps bv2
      liftQ [| addArchExpr =<< (UDiv $(natReprTH w) <$> $(refBinding e1) <*> $(refBinding e2))
             |]
  
    S.FloatNeg fpp fp -> return $ do
      e <- addEltTH M.BigEndian interps fp
      liftQ [|
          addArchExpr =<< (FPNeg $(floatInfoFromPrecisionTH fpp) <$> $(refBinding e))
        |]
    S.FloatAbs fpp fp -> return $ do
      e <- addEltTH M.BigEndian interps fp
      liftQ [|
          addArchExpr =<< (FPAbs $(floatInfoFromPrecisionTH fpp) <$> $(refBinding e))
        |]
    S.FloatSqrt fpp r fp -> return $ do
      e <- addEltTH M.BigEndian interps fp
      liftQ [|
          addArchExpr =<< (FPSqrt
            $(floatInfoFromPrecisionTH fpp)
            $(roundingModeToBitsTH r) <$>
            $(refBinding e))
        |]
  
    S.FloatAdd fpp r fp1 fp2 -> return $ do
      e1 <- addEltTH M.BigEndian interps fp1
      e2 <- addEltTH M.BigEndian interps fp2
      liftQ [|
          addArchExpr =<< (FPAdd
            $(floatInfoFromPrecisionTH fpp)
            $(roundingModeToBitsTH r) <$>
            $(refBinding e1) <*>
            $(refBinding e2))
        |]
    S.FloatSub fpp r fp1 fp2 -> return $ do
      e1 <- addEltTH M.BigEndian interps fp1
      e2 <- addEltTH M.BigEndian interps fp2
      liftQ [|
          addArchExpr =<< (FPSub
            $(floatInfoFromPrecisionTH fpp)
            $(roundingModeToBitsTH r) <$>
            $(refBinding e1) <*>
            $(refBinding e2))
        |]
    S.FloatMul fpp r fp1 fp2 -> return $ do
      e1 <- addEltTH M.BigEndian interps fp1
      e2 <- addEltTH M.BigEndian interps fp2
      liftQ [|
          addArchExpr =<< (FPMul
            $(floatInfoFromPrecisionTH fpp)
            $(roundingModeToBitsTH r) <$>
            $(refBinding e1) <*>
            $(refBinding e2))
        |]
    S.FloatDiv fpp r fp1 fp2 -> return $ do
      e1 <- addEltTH M.BigEndian interps fp1
      e2 <- addEltTH M.BigEndian interps fp2
      liftQ [|
          addArchExpr =<< (FPDiv
            $(floatInfoFromPrecisionTH fpp)
            $(roundingModeToBitsTH r) <$>
            $(refBinding e1) <*>
            $(refBinding e2))
        |]
  
    S.FloatFMA fpp r fp1 fp2 fp3 -> return $ do
      e1 <- addEltTH M.BigEndian interps fp1
      e2 <- addEltTH M.BigEndian interps fp2
      e3 <- addEltTH M.BigEndian interps fp3
      liftQ [|
          addArchExpr =<< (FPFMA
            $(floatInfoFromPrecisionTH fpp)
            $(roundingModeToBitsTH r) <$>
            $(refBinding e1) <*>
            $(refBinding e2) <*>
            $(refBinding e3))
        |]
  
    S.FloatLt fp1 fp2 -> return $ do
      e1 <- addEltTH M.BigEndian interps fp1
      e2 <- addEltTH M.BigEndian interps fp2
      liftQ [| addArchExpr =<< (FPLt <$> $(refBinding e1) <*> $(refBinding e2)) |]
    S.FloatFpEq fp1 fp2 -> return $ do
      e1 <- addEltTH M.BigEndian interps fp1
      e2 <- addEltTH M.BigEndian interps fp2
      liftQ [| addArchExpr =<< (FPEq <$> $(refBinding e1) <*> $(refBinding e2)) |]
    S.FloatLe fp1 fp2 -> return $ do
      e1 <- addEltTH M.BigEndian interps fp1
      e2 <- addEltTH M.BigEndian interps fp2
      liftQ [| addArchExpr =<< (FPLe <$> $(refBinding e1) <*> $(refBinding e2)) |]
  
    S.FloatIsNaN fp -> return $ do
      e <- addEltTH M.BigEndian interps fp
      liftQ [| addArchExpr =<< (FPIsNaN <$> $(refBinding e)) |]
  
    S.FloatCast fpp r fp -> return $ do
      e <- addEltTH M.BigEndian interps fp
      liftQ [|
          addArchExpr =<< (FPCast
            $(floatInfoFromPrecisionTH fpp)
            $(roundingModeToBitsTH r) <$>
            $(refBinding e))
        |]
    S.FloatRound fpp r fp -> return $ do
      e <- addEltTH M.BigEndian interps fp
      liftQ [|
          addArchExpr =<< (FPRound
            $(floatInfoFromPrecisionTH fpp)
            $(roundingModeToBitsTH r) <$>
            $(refBinding e))
        |]
    S.FloatToBinary fpp fp -> return $ do
      e <- addEltTH M.BigEndian interps fp
      liftQ [|
          addArchExpr =<<
              (FPToBinary $(floatInfoFromPrecisionTH fpp) <$> $(refBinding e))
        |]
    S.FloatFromBinary fpp fp -> return $ do
      e <- addEltTH M.BigEndian interps fp
      liftQ [|
          addArchExpr =<<
              (FPFromBinary $(floatInfoFromPrecisionTH fpp) <$> $(refBinding e))
        |]
    S.FloatToSBV w r fp -> return $ do
      e <- addEltTH M.BigEndian interps fp
      liftQ [|
          addArchExpr =<<
              (FPToSBV $(natReprTH w) $(roundingModeToBitsTH r) <$> $(refBinding e))
        |]
    S.FloatToBV w r fp -> return $ do
      e <- addEltTH M.BigEndian interps fp
      liftQ [|
          addArchExpr =<<
              (FPToUBV $(natReprTH w) $(roundingModeToBitsTH r) <$> $(refBinding e))
        |]
    S.SBVToFloat fpp r fp -> return $ do
      e <- addEltTH M.BigEndian interps fp
      liftQ [|
          addArchExpr =<< (FPFromSBV
            $(floatInfoFromPrecisionTH fpp)
            $(roundingModeToBitsTH r) <$>
            $(refBinding e))
        |]
    S.BVToFloat fpp r fp -> return $ do
      e <- addEltTH M.BigEndian interps fp
      liftQ [|
          addArchExpr =<< (FPFromUBV
            $(floatInfoFromPrecisionTH fpp)
            $(roundingModeToBitsTH r) <$>
            $(refBinding e))
        |]
  
    _ -> Nothing
  
  roundingModeToBitsTH :: S.RoundingMode -> Q Exp
  roundingModeToBitsTH r =
    [| M.BVValue $(natReprTH (M.knownNat @2)) $(lift $ U.roundingModeToBits r) |]
  