content: module NullnessSpec where
  
  import Test.Hspec
  
  import Utils
  
  import Syntax
  import qualified ConcreteSemantics as Con
  import NullnessSemantics
  import JimpleSoundness
  
  import Data.String
  
  import qualified Data.Abstract.Boolean as Abs
  import           Data.Abstract.HandleError
  import           Data.Abstract.Exception
  
  -- import Java.Lang.Throwable
  import Classes.ArrayFieldExample
  -- import Classes.FactorialExample
  import Classes.PersonExample
  import Classes.SingleMethodExample
  import Classes.TryCatchExample
  
  main :: IO ()
  main = hspec spec
  
  spec :: Spec
  spec = do
    describe "Literals" $ do
      it "LocalName lookup" $ do
        let i = Local "x"
        let mem = [("x",NonNull)]
        evalImmediate'' mem i `shouldSatisfy` ifSuccess NonNull
      it "Integer literals" $ do
        let i = IntConstant 7
        evalImmediate'' [] i `shouldBe` Success NonNull
      it "Float literals" $ do
        let i = FloatConstant 2.5
        evalImmediate'' [] i `shouldBe` Success NonNull
      it "String literals" $ do
        let i = StringConstant "Hello World"
        evalImmediate'' [] i `shouldBe` Success NonNull
      it "Class literals" $ do
        let i = ClassConstant "java.lang.Object"
        evalImmediate'' [] i `shouldBe` Success NonNull
      it "Null literals" $ do
        let i = NullConstant
        evalImmediate'' [] i `shouldBe` Success Null
  
    describe "Boolean expressions" $ do
      it "3 < 4" $ do
        let expr = BoolExpr (IntConstant 3) Cmplt (IntConstant 4)
        evalBool'' [] expr `shouldSatisfy` ifSuccess Abs.Top
      it "3 != 'three'" $ do
        let expr = BoolExpr (IntConstant 3) Cmpne (StringConstant "three")
        evalBool'' [] expr `shouldBe` Success Abs.Top
  
    describe "Simple Expressions" $ do
      it "-3" $ do
        let expr = UnopExpr Neg (IntConstant 3)
        eval'' [] expr `shouldSatisfy` ifSuccess NonNull
      it "lengthof [1, 2, 3]" $ do
        let expr = UnopExpr Lengthof (Local "x")
        let mem = [("x",NonNull)]
        eval'' mem expr `shouldSatisfy` ifSuccess NonNull
      it "8 + 2" $ do
        let expr = BinopExpr (IntConstant 8) Plus (IntConstant 2)
        eval'' [] expr `shouldSatisfy` ifSuccess NonNull
      it "8 / 0" $ do
        let expr = BinopExpr (IntConstant 8) Div (IntConstant 0)
        eval'' [] expr `shouldBe` SuccessOrFail (fromString "Expected numeric variables for 'div'") NonNull
      it "3.0 % 2.5" $ do
        let expr = BinopExpr (FloatConstant 3.0) Rem (FloatConstant 2.5)
        eval'' [] expr `shouldSatisfy` ifSuccess NonNull
      it "new boolean" $ do
        let expr = NewExpr BooleanType
        eval'' [] expr `shouldBe` Success NonNull
      it "[1, 2, 3][2]" $ do
        let expr = RefExpr (ArrayRef "xs" (IntConstant 2))
        let mem = [("xs",NonNull)]
        eval'' mem expr `shouldSatisfy` ifSuccess Top
      it "newmultiarray (float) [3][2]" $ do
        let expr = NewMultiArrayExpr FloatType [IntConstant 3, IntConstant 2]
        eval'' [] expr `shouldSatisfy` ifSuccess NonNull
  
    describe "Simple Statements" $ do
      it "i0 = 2 + 3; return i0;" $ do
        let mem = [("i0",NonNull)]
        let stmts = [Assign (LocalVar "i0") (BinopExpr (IntConstant 2) Plus (IntConstant 3)),
                     Return (Just (Local "i0"))]
        runStatements'' mem stmts `shouldSatisfy` ifSuccess (Just NonNull)
      it "assign non-declared variable" $ do
        let stmts = [Assign (LocalVar "s") (ImmediateExpr (IntConstant 2))]
        runStatements'' [] stmts `shouldBe` Fail (fromString "Variable \"s\" not bound")
      it "s = 2; xs = newarray (int)[s]; y = lengthof xs; return xs;" $ do
        let mem = [("s",  NonNull),
                  ("xs", Null),
                  ("y",  NonNull)]
        let stmts = [Assign (LocalVar "s") (ImmediateExpr (IntConstant 2)),
                     Assign (LocalVar "xs") (NewArrayExpr IntType (Local "s")),
                     Assign (LocalVar "y") (UnopExpr Lengthof (Local "xs")),
                     Return (Just (Local "y"))]
        runStatements'' mem stmts `shouldSatisfy` ifSuccess (Just NonNull)
      it "if 2 <= 3 goto l2; l1: return 1; l2: return 0;" $ do
        let stmts = [If (BoolExpr (IntConstant 2) Cmple (IntConstant 3)) "l2",
                     Label "l1",
                     Return (Just (IntConstant 1)),
                     Label "l2",
                     Return (Just (IntConstant 0))]
        runStatements'' [] stmts `shouldSatisfy` ifSuccess (Just NonNull)
      it "lookupswitch(4) { case 0: goto l1; case 4: goto l2; default: goto l3;}; l1: return 1; l2: return 2; l3: return 3;" $ do
        let stmts = [Lookupswitch (IntConstant 4) [(ConstantCase 0, "l1"),
                                                   (ConstantCase 4, "l2"),
                                                   (DefaultCase, "l3")],
                     Label "l1",
                     Return (Just (IntConstant 1)),
                     Label "l2",
                     Return (Just (IntConstant 2)),
                     Label "l3",
                     Return (Just (IntConstant 3))]
        runStatements'' [] stmts `shouldSatisfy` ifSuccess (Just NonNull)
      it "lookupswitch(2) { case 0: goto l1; case 4: goto l2; default: goto l3;}; l1: return 1; l2: return 2; l3: return 3;" $ do
        let stmts = [Lookupswitch (IntConstant 2) [(ConstantCase 0, "l1"),
                                            (ConstantCase 4, "l2"),
                                            (DefaultCase, "l3")],
                     Label "l1",
                     Return (Just (IntConstant 1)),
                     Label "l2",
                     Return (Just (IntConstant 2)),
                     Label "l3",
                     Return (Just (IntConstant 3))]
        runStatements'' [] stmts `shouldSatisfy` ifSuccess (Just NonNull)
      it "f0 := @parameter0: float; f1 = f0 * 2.5; return f1; (@parameter0 = 2.0)" $ do
        let mem = [("@parameter0", NonNull),
                   ("f0",          NonNull),
                   ("f1",          NonNull)]
        let stmts = [Identity "f0" (ParameterRef 0) FloatType,
                     Assign (LocalVar "f1") (BinopExpr (Local "f0") Mult (FloatConstant 2.5)),
                     Return (Just (Local "f1"))]
        runStatements'' mem stmts `shouldSatisfy` ifSuccess (Just NonNull)
  
    describe "Complete program" $ do
      -- it "10! = 3628800" $ do
      --   runProgram'' factorialExampleFile [IntConstant 10] `shouldSatisfy` ifSuccess (Just NonNull)
      it "s = new SingleMethodExample; s.x = 2; return s.x" $
        runProgram'' singleMethodExampleFile [] `shouldSatisfy` ifSuccess (Just NonNull)
      -- it "(-10)! throws IllegalArgumentException" $ do
      --   runProgram'' factorialExampleFile [IntConstant (-10)] `shouldBe` Fail (DynamicException NonNull)
      it "5 -> [5,10,5,10]" $
        runProgram'' arrayFieldExampleFile [IntConstant 5] `shouldSatisfy` ifSuccess (Just Top)
      it "(new Person(10)).yearsToLive() = 90" $
        runProgram'' personExampleFile [] `shouldSatisfy` ifSuccess (Just NonNull)
      it "try { throw e } catch (e) { throw e' }" $
        runProgram'' tryCatchExampleFile [] `shouldSatisfy` ifFail (DynamicException NonNull)
  
    describe "Sound interpretation" $ jimpleSoundness
      (Con.evalImmediate' baseCompilationUnits) evalImmediate''
      (Con.evalBool' baseCompilationUnits)      evalBool''
      (Con.eval' baseCompilationUnits)          eval''
      (Con.runStatements' baseCompilationUnits) runStatements''
      runProgramCon                             runProgram''
  
    where
      evalImmediate'' = evalImmediate' baseCompilationUnits
      evalBool'' = evalBool' baseCompilationUnits
      eval'' = eval' baseCompilationUnits
      runStatements'' = runStatements' baseCompilationUnits
      runProgram'' unit params = runProgram' (unit:baseCompilationUnits) (methodSignature unit (mainMethod unit),params)
      runProgramCon unit params = Con.runProgram' (unit:baseCompilationUnits) (methodSignature unit (mainMethod unit),params)
  
      ifSuccess x e = case e of
        Success y -> y == x
        SuccessOrFail _ y -> y == x
        _ -> False
  
      ifFail x e = case e of
        Fail y -> y == x
        SuccessOrFail y _ -> y == x
        _ -> False
  