content: {-# LANGUAGE OverloadedLists #-}
  {-# OPTIONS_GHC -fno-warn-incomplete-uni-patterns #-}
  module ConstantPropagationUnitMemorySpec where
  
  import qualified Concrete as Concrete
  --import qualified Data as D
  import           ConstantPropagationUnitMemory as A
  import           ConstantPropagationValue as A
  -- import           UnitAnalysisValue as U
  import           ConstantPropagationSoundness
  --import           GraphToDot
  
  import qualified Data.ByteString.Lazy as LBS
  import qualified Data.Abstract.Except as Exc
  import           Data.Abstract.MonotoneErrors(toSet)
  import           Data.Abstract.Terminating
  import qualified Data.HashSet as HashSet
  import           Data.Text.Lazy (pack)
  
  import           Language.Wasm
  import qualified Language.Wasm.Interpreter as Wasm
  import           Language.Wasm.Structure (Function(..), Expression)
  
  --import           Numeric.Natural
  
  import           Test.Hspec
  
  main :: IO ()
  main = hspec spec
  
  term :: Terminating a -> a
  term (Terminating a) = a
  term _ = error "not defined"
  
  getFunctionBody :: Function -> Expression
  getFunctionBody (Function _ _ b) = b
  
  readModule :: String -> IO ValidModule
  readModule path = do
      content <- LBS.readFile path
      let Right m = parse content
      let Right validMod = validate m
      return validMod
  
  runFunc :: String -> String -> [A.Value] -> IO Result
  runFunc modName funcName args = do
      m <- readModule ("test/samples/" ++ modName ++ ".wast")
      Right (modInst, staticS, tabs) <- instantiateAbstract m
      return $ invokeExported staticS tabs modInst (pack funcName) args
  
  checkSoundness :: String -> String -> [[Concrete.Value]] -> IO Bool
  checkSoundness m f args = do
      validMod <- readModule ("test/samples/" ++ m ++ ".wast")
      isSoundlyAbstracted validMod f args
  
  succResult :: Result -> [A.Value]
  succResult (_,(_,(Terminating (_,(_,(Exc.Success (_,result))))))) = result
  succResult res = error $ "unsuccessful result " ++ show res
  
  terminatedSucc :: Result -> Bool
  terminatedSucc (_, (errs, Terminating (_,(_,(Exc.Success _))))) = HashSet.null (toSet errs)
  terminatedSucc (_, (errs, NonTerminating)) = HashSet.null (toSet errs)
  terminatedSucc _ = False
  
  terminatedErr :: Result -> Bool
  terminatedErr (_,(errs, NonTerminating)) = not $ HashSet.null (toSet errs)
  terminatedErr _ = False
  
  terminatedMaybeErr :: Result -> Bool
  terminatedMaybeErr (_,(errs, Terminating (_,(_,(Exc.Success _))))) = not $ HashSet.null (toSet errs)
  terminatedMaybeErr _ = False
  
  isNonTerminating :: Result -> Bool
  isNonTerminating (_,(_, NonTerminating)) = True
  isNonTerminating _ = False
  
  minialpha :: A.Value -> A.Value
  minialpha = A.NotConstant . A.asNotConstant
  
  spec :: Spec
  spec = do
  
      -- CONSTANT VALUES
  
      it "run noop" $ do
          result <- runFunc "simple" "noop" []
          succResult result `shouldBe` [A.constantValue $ Wasm.VI32 0]
  
      it "run const" $ do
          result <- runFunc "simple" "const" [A.constantValue $ Wasm.VI32 5]
          succResult result `shouldBe` [A.constantValue $ Wasm.VI32 5]
  
      it "run fac-rec" $ do
          let params = map (singleton . A.constantValue . Wasm.VI64) [0 .. 8]
          results <- mapM (runFunc "fact" "fac-rec") params
          let rs = map succResult results
          rs `shouldBe` map (singleton . A.constantValue . Wasm.VI64) [1,1,2,6,24,120,720,5040,40320]
  
      it "run fac-rec2" $ do
          result <- runFunc "fact" "fac-rec" [A.constantValue $ Wasm.VI64 25]
          succResult result `shouldBe` [A.constantValue $ Wasm.VI64 7034535277573963776]
  
      it "run fac-iter" $ do
          result <- runFunc "fact" "fac-iter" [A.constantValue $ Wasm.VI64 25]
          succResult result `shouldBe` [A.constantValue $ Wasm.VI64 7034535277573963776]
  
      it "run fac-rec-named" $ do
          result <- runFunc "fact" "fac-rec-named" [A.constantValue $ Wasm.VI64 25]
          succResult result `shouldBe` [A.constantValue $ Wasm.VI64 7034535277573963776]
  
      it "run fac-iter-named" $ do
          result <- runFunc "fact" "fac-iter-named" [A.constantValue $ Wasm.VI64 25]
          succResult result `shouldBe` [A.constantValue $ Wasm.VI64 7034535277573963776]
  
      it "run fac-opt" $ do
          result <- runFunc "fact" "fac-opt" [A.constantValue $ Wasm.VI64 25]
          succResult result `shouldBe` [A.constantValue $ Wasm.VI64 7034535277573963776]
  
      it "run test-mem" $ do
          -- result <- runFunc "simple" "test-mem" [A.constantValue $ Wasm.VI32 42]
          -- succResult result `shouldBe` [minialpha $ A.constantValue $ Wasm.VI32 43]
          result <- runFunc "simple" "test-mem" [A.constantValue $ Wasm.VI32 (2^(32::Int)-2)]
          succResult result `shouldBe` [minialpha $ A.constantValue $ Wasm.VI32 (2^(32::Int)-1)]
  
      it "run test-size" $ do
          result <- runFunc "simple" "test-size" []
          succResult result `shouldBe` [minialpha $ A.constantValue $ Wasm.VI32 1]
  
      it "run test-memgrow" $ do
          result <- runFunc "simple" "test-memgrow" []
          succResult result `shouldBe` [minialpha $ A.constantValue $ Wasm.VI32 1, minialpha $ A.constantValue $ Wasm.VI32 2]
  
      it "run test-call-indirect" $ do
          result <- runFunc "simple" "test-call-indirect" []
          succResult result `shouldBe` [A.constantValue $ Wasm.VI32 0]
  
      it "run first" $ do
          result <- runFunc "simple" "first" [A.constantValue $ Wasm.VI32 0, A.constantValue $ Wasm.VI32 1]
          succResult result `shouldBe` [A.constantValue $ Wasm.VI32 0]
  
      it "run call-first" $ do
          result <- runFunc "simple" "call-first" []
          succResult result `shouldBe` [A.constantValue $ Wasm.VI32 0]
  
      it "run nesting" $ do
          result <- runFunc "simple" "nesting" [A.constantValue $ Wasm.VF32 1, A.constantValue $ Wasm.VF32 2]
          succResult result `shouldBe` [A.constantValue $ Wasm.VF32 2]
  
  
      -- UNIT VALUES
  
      -- it "const: run fact" $ do
      --     result <- runFunc "fact" "fac-rec" [minialpha $ A.constantValue $ Wasm.VI64 1]
      --     result `shouldSatisfy` terminatedSucc
      --     (succResult result) `shouldBe` [minialpha $ A.constantValue $ Wasm.VI64 1]
      --     let args = [[Concrete.Value $ Wasm.VI64 1],[Concrete.Value $ Wasm.VI64 10]]
      --     checkSoundness "fact" "fac-rec" args `shouldReturn` True
  
      it "const: run test2" $ do
          checkSoundness "simple" "test2" [[]] `shouldReturn` True
  
      it "const: run test-br3" $ do
          let args = [[Concrete.Value $ Wasm.VI32 10]]
          checkSoundness "simple" "test-br3" args `shouldReturn` True
  
      it "const: run test-call-indirect" $ do
          checkSoundness "simple" "test-call-indirect" [[]] `shouldReturn` True
  
      it "const: run maybe-non-terminating" $ do
          let args = [[Concrete.Value $ Wasm.VI32 42]]
          checkSoundness "simple" "maybe-non-terminating" args `shouldReturn` True
  
      it "const: run test-unreachable" $ do
          checkSoundness "simple" "test-unreachable" [[]] `shouldReturn` True
  
      it "const: run test-unreachable2" $ do
          checkSoundness "simple" "test-unreachable2" [[]] `shouldReturn` True
  
      it "const: run test-unreachable3" $ do
          checkSoundness "simple" "test-unreachable3" [[]] `shouldReturn` True
  
      it "const: run test-unreachable4" $ do
          checkSoundness "simple" "test-unreachable4" [[]] `shouldReturn` True
  
      it "const: run test-unreachable5" $ do
          checkSoundness "simple" "test-unreachable4" [[]] `shouldReturn` True
  
      it "const: run test-br-and-return" $ do
          let args = [[Concrete.Value $ Wasm.VI32 10]]
          checkSoundness "simple" "test-br-and-return" args `shouldReturn` True
  
      it "const: run test-br-and-return2" $ do
          let args = [[Concrete.Value $ Wasm.VI32 10]]
          checkSoundness "simple" "test-br-and-return2" args `shouldReturn` True
  
      it "const: run test-br-and-return3" $ do
          let args = [[Concrete.Value $ Wasm.VI32 10]]
          checkSoundness "simple" "test-br-and-return3" args `shouldReturn` True
  
  
    where
      singleton :: a -> [a]
      singleton x = [x]
  
  
  
  --    it "print cfg" $ do
  --        result <- runFunc "fact" "fac-rec" [A.constantValue $ VI64 ()]
  --        let cfg = fst result
  --        putStrLn (show cfg)
  --        putStrLn $ graphToDot showForGraph cfg
  --        pending
  --
  --
  --showForGraph :: D.Instruction Natural -> String
  --showForGraph (D.I32Const i _) = "I32Const " ++ (show i)
  --showForGraph (D.I64Const i _) = "I64Const " ++ (show i)
  --showForGraph (D.GetLocal n _) = "GetLocal " ++ (show n)
  --showForGraph (D.IRelOp bs op _) = "IRelOp " ++ (show bs) ++ " " ++ (show op)
  --showForGraph (D.IBinOp bs op _) = "IBinOp " ++ (show bs) ++ " " ++ (show op)
  --showForGraph (D.Call i _) = "Call " ++ (show i)
  --showForGraph (D.If t _ _ _) = "If " ++ (show t)
  --showForGraph _ = error "todo"
  