Typecheck.hs

-- SPDX-FileCopyrightText: 2020 Tocqueville Group
--
-- SPDX-License-Identifier: LicenseRef-MIT-TQ

{-# LANGUAGE ViewPatterns #-}

module Test.Typecheck
  ( unit_Good_contracts
  , unit_Bad_contracts
  , test_srcPosition
  , unit_Unreachable_code
  , test_Roundtrip
  , test_StackRef
  , test_TCTypeError_display
  , hprop_ValueSeq_as_list
  , test_SELF
  , test_Value_contract
  ) where

import Data.Default (def)
import qualified Data.Kind as Kind
import qualified Data.Map as M
import Data.Singletons (SingI(..))
import Data.Typeable (typeRep)
import Fmt (build, pretty)
import Hedgehog (Gen, Property, forAll, property, (===))
import qualified Hedgehog.Gen as Gen
import qualified Hedgehog.Range as Range
import Test.Hspec (expectationFailure)
import Test.Hspec.Expectations (Expectation)
import Test.HUnit (Assertion, assertFailure, (@?=))
import Test.Tasty (TestTree, testGroup)
import Test.Tasty.Hedgehog (testProperty)
import Test.Tasty.HUnit (testCase)

import Michelson.ErrorPos (InstrCallStack(..), LetName(..), Pos(..), SrcPos(..), srcPos)
import Michelson.Parser (utypeQ)
import Michelson.Runtime (prepareContract)
import Michelson.Test (failedTest, meanTimeUpperBoundPropNF, sec, total)
import Michelson.Test.Gen (genValueInt, genValueTimestamp)
import Michelson.Test.Import (ImportContractError(..), readContract)
import Michelson.TypeCheck
import qualified Michelson.Typed as T
import Michelson.Untyped (ParameterType(..), noAnn, unsafeBuildEpName)
import qualified Michelson.Untyped as Un
import Tezos.Address (Address(..), ContractHash, mkContractHashHack)
import Tezos.Core (Timestamp)
import Util.IO (readFileUtf8)

import Test.Util.Contracts (getIllTypedContracts, getWellTypedContracts, inContractsDir)

unit_Good_contracts :: Assertion
unit_Good_contracts = mapM_ (\f -> checkFile [] True f (const pass)) =<< getWellTypedContracts

unit_Bad_contracts :: Assertion
unit_Bad_contracts = mapM_ (\f -> checkFile [] False f (const pass)) =<< getIllTypedContracts

pattern IsSrcPos :: Word -> Word -> InstrCallStack
pattern IsSrcPos l c <- InstrCallStack [] (SrcPos (Pos l) (Pos c))

test_srcPosition :: [TestTree]
test_srcPosition =
  [ testCase "Verify instruction position in a typecheck error" $ do
      checkIllFile (inContractsDir "ill-typed/basic3.tz") $ \case
          TCFailedOnInstr (Un.CONS _) _ (IsSrcPos 8 6) _ (Just (AnnError _)) -> True
          _ -> False

      checkIllFile (inContractsDir "ill-typed/testassert_invalid_stack3.mtz") $ \case
          TCFailedOnInstr Un.DROP _ (IsSrcPos 10 17) _ (Just NotEnoughItemsOnStack) -> True
          _ -> False

      checkIllFile (inContractsDir "ill-typed/testassert_invalid_stack2.mtz") $ \case
          TCExtError _ (IsSrcPos 9 2) (TestAssertError _) -> True
          _ -> False

      checkIllFile (inContractsDir "ill-typed/macro_in_let_fail.mtz") $ \case
          TCFailedOnInstr (Un.COMPARE _) _ (InstrCallStack [LetName "cmpLet"] (SrcPos (Pos 7) (Pos 6))) _
                                              (Just (TypeEqError _ _)) -> True
          _ -> False
      checkIllFile (inContractsDir "ill-typed/compare_annotation_mismatch.tz") $ \case
          TCFailedOnInstr (Un.COMPARE _) _ _ _ (Just (AnnError _)) -> True
          _ -> False

      checkIllFile (inContractsDir "ill-typed/annotation_mismatch_map_update.tz") $ \case
          TCFailedOnInstr (Un.UPDATE _) (SomeHST (_ ::& _ ::& (T.NTMap{}, _, _) ::& SNil)) _ _ (Just (AnnError _)) -> True
          _ -> False

      checkIllFile (inContractsDir "ill-typed/annotation_mismatch_map_get.tz") $ \case
          TCFailedOnInstr (Un.GET _) (SomeHST (_ ::& (T.NTMap{}, _, _) ::& SNil)) _ _ (Just (AnnError _)) -> True
          _ -> False

      checkIllFile (inContractsDir "ill-typed/annotation_mismatch_map_mem.tz") $ \case
          TCFailedOnInstr (Un.MEM _) (SomeHST (_ ::& (T.NTMap{}, _, _) ::& SNil)) _ _ (Just (AnnError _)) -> True
          _ -> False

      checkIllFile (inContractsDir "ill-typed/annotation_mismatch_big_map_update.tz") $ \case
          TCFailedOnInstr (Un.UPDATE _) (SomeHST (_ ::& _ ::& (T.NTBigMap{}, _, _) ::& SNil)) _ _ (Just (AnnError _)) -> True
          _ -> False

      checkIllFile (inContractsDir "ill-typed/annotation_mismatch_big_map_get.tz") $ \case
          TCFailedOnInstr (Un.GET _) (SomeHST (_ ::& (T.NTBigMap{}, _, _) ::& SNil)) _ _ (Just (AnnError _)) -> True
          _ -> False

      checkIllFile (inContractsDir "ill-typed/annotation_mismatch_big_map_mem.tz") $ \case
          TCFailedOnInstr (Un.MEM _) (SomeHST (_ ::& (T.NTBigMap{}, _, _) ::& SNil)) _ _ (Just (AnnError _)) -> True
          _ -> False

      checkIllFile (inContractsDir "ill-typed/annotation_mismatch_set_update.tz") $ \case
          TCFailedOnInstr (Un.UPDATE _) (SomeHST (_ ::& _ ::& (T.NTSet{}, _, _) ::& SNil)) _ _ (Just (AnnError _)) -> True
          _ -> False

      checkIllFile (inContractsDir "ill-typed/annotation_mismatch_set_mem.tz") $ \case
          TCFailedOnInstr (Un.MEM _) (SomeHST (_ ::& (T.NTSet{}, _, _) ::& SNil)) _ _ (Just (AnnError _)) -> True
          _ -> False
  ]
  where
    unexpected f e =
      expectationFailure $ "Unexpected typecheck error: " <> displayException e <> " in file: " <> f
    checkIllFile file check = checkFile [] False file $
      \e -> if check e then pass else unexpected file e

checkFile
  :: HasCallStack
  => [(ContractHash, ParameterType)]
  -> Bool
  -> FilePath
  -> (TCError -> Expectation)
  -> Expectation
checkFile originatedContracts wellTyped file onError = do
  c <- prepareContract (Just file)
  case doTC c of
    Left err
      | wellTyped ->
        expectationFailure $
        "Typechecker unexpectedly failed on " <> show file <> ": " <> displayException err
      | otherwise -> onError err
    Right _
      | not wellTyped ->
        assertFailure $
        "Typechecker unexpectedly considered " <> show file <> " well-typed."
      | otherwise -> pass
  where
    doTC = typeCheckContract (M.fromList originatedContracts)

unit_Unreachable_code :: Assertion
unit_Unreachable_code = do
  let file = inContractsDir "ill-typed/fail_before_nop.tz"
  let ics = InstrCallStack [] (srcPos 7 13)
  econtract <- readContract @'T.TUnit @'T.TUnit file <$> readFileUtf8 file
  econtract @?= Left (ICETypeCheck $ TCUnreachableCode ics (one $ Un.WithSrcEx ics $ Un.SeqEx []))

test_Roundtrip :: [TestTree]
test_Roundtrip =
  [ testGroup "Value"
    [ roundtripValue @Integer genValueInt
    , roundtripValue @Timestamp genValueTimestamp
    ]
  ]
  where
  roundtripValue
    :: forall (a :: Kind.Type).
        ( Each [T.KnownT, T.HasNoOp] '[T.ToT a]
        , Typeable a
        )
    => Gen (T.Value $ T.ToT a)
    -> TestTree
  roundtripValue genValue =
    testProperty (show $ typeRep (Proxy @a)) $ property $ do
      val :: T.Value (T.ToT a) <- forAll $ genValue
      let uval = T.untypeValue val
          runTC = runTypeCheckIsolated . usingReaderT (def @InstrCallStack)
      case runTC $ typeCheckValue uval of
        Right got -> got === val
        Left err -> failedTest $
                    "Type check unexpectedly failed: " <> pretty err

test_StackRef :: [TestTree]
test_StackRef =
  [ testProperty "Typecheck fails when ref is out of bounds" $ property $ do
      let instr = printStRef 2
          hst = stackEl ::& stackEl ::& SNil
      case
        runTypeCheck (error "no contract param") mempty $
        typeCheckList [Un.WithSrcEx def $ Un.PrimEx instr] hst
        of
          Left err -> void $ total err
          Right _ -> failedTest "Typecheck unexpectedly succeded"
  , testProperty "Typecheck time is reasonably bounded" $
      let hst = stackEl ::& SNil
          run i =
            case
              runTypeCheck (error "no contract param") mempty $
              typeCheckList [Un.WithSrcEx def $ Un.PrimEx (printStRef i)] hst
            of
              Left err -> err
              Right _ -> error "Typecheck unexpectedly succeded"
      -- Making code processing performance scale with code size looks like a
      -- good property, so we'd like to avoid scenario when user tries to
      -- access 100500-th element of stack and typecheck hangs as a result
      in  meanTimeUpperBoundPropNF (sec 1) run 100000000000
  ]
  where
    printStRef i = Un.EXT . Un.UPRINT $ Un.PrintComment [Right (Un.StackRef i)]
    stackEl = (T.starNotes @'T.TUnit, T.Dict, noAnn)

test_TCTypeError_display :: [TestTree]
test_TCTypeError_display =
  -- One may say that it's madness to write tests on 'Buildable' instances,
  -- but IMO (martoon) it's worth resulting duplication because tests allow
  -- avoiding silly errors like lost spaces and ensuring general sanity
  -- of used way to display content.
  [ testCase "TypeEqError" $
      build (TypeEqError T.TUnit T.TKey)
      @?= "Types not equal: unit /= key"

  , testCase "StackEqError" $
      build (StackEqError [T.TUnit, T.TBytes] [])
      @?= "Stacks not equal: [unit, bytes] /= []"

  , testCase "UnsupportedTypes" $
      build (UnsupportedTypeForScope (T.TBigMap T.TInt T.TInt) T.BtHasBigMap)
      @?= "Type 'big_map int int' is unsupported here because it has 'big_map'"

  , testCase "InvalidValueType" $
      build (InvalidValueType T.TUnit)
      @?= "Value type is never a valid `unit`"
  ]

hprop_ValueSeq_as_list :: Property
hprop_ValueSeq_as_list = property $ do
  l <- forAll $ Gen.nonEmpty (Range.linear 0 100) (Gen.integral (Range.linearFrom 0 -1000 1000))
  let
    untypedValue = Un.ValueSeq $ Un.ValueInt <$> l
    typedValue = T.VList $ T.VInt <$> toList l
    runTypeCheckInstr = runTypeCheckIsolated . usingReaderT def
  runTypeCheckInstr (typeCheckValue untypedValue) === Right typedValue

test_SELF :: [TestTree]
test_SELF =
  [ testCase "Entrypoint not present" $
      checkFile [] False (inContractsDir "ill-typed/self-bad-entrypoint.mtz") $ \case
        TCFailedOnInstr Un.SELF{} _ _ _ (Just EntryPointNotFound{}) -> pass
        other -> assertFailure $ "Unexpected error: " <> pretty other

  , testCase "Entrypoint type mismatch" $
      checkFile [] False (inContractsDir "ill-typed/self-entrypoint-type-mismatch.mtz")
        (const pass)

  , testCase "Entrypoint can be found" $
      checkFile [] True (inContractsDir "entrypoints/self1.mtz")
        (const pass)
  ]

test_Value_contract :: [TestTree]
test_Value_contract =
  [ testCase "No contract exists" $
      case doTypeCheckVal @('T.TContract 'T.TUnit) mempty addrUVal1 of
        Left (TCFailedOnValue _ _ _ _ (Just (UnknownContract _))) -> pass
        res -> assertFailure $ "Unexpected result: " <> show res

  , testCase "Entrypoint does not exist" $
      case doTypeCheckVal @('T.TContract 'T.TKey) env1 addrUVal1 of
        Left (TCFailedOnValue _ _ _ _ (Just (EntryPointNotFound _))) -> pass
        res -> assertFailure $ "Unexpected result: " <> show res

  , testCase "Correct contract value" $
      case doTypeCheckVal @('T.TContract 'T.TInt) env1 addrUVal2 of
        Right _ -> pass
        res -> assertFailure $ "Unexpected result: " <> show res
  ]
  where
    addr1' = mkContractHashHack "123"
    addr1 = T.EpAddress (ContractAddress addr1') (unsafeBuildEpName "a")
    addr2 = T.EpAddress (ContractAddress addr1') (unsafeBuildEpName "q")
    addrUVal1 = Un.ValueString $ T.mformatEpAddress addr1
    addrUVal2 = Un.ValueString $ T.mformatEpAddress addr2

    env1 = M.fromList
      [ ( addr1', ParameterType [utypeQ| ( nat %s | int %q ) |] noAnn)
      ]

    doTypeCheckVal
      :: SingI t
      => TcOriginatedContracts -> Un.Value -> Either TCError (T.Value t)
    doTypeCheckVal env uval =
      runTypeCheck (error "hello there") env $ usingReaderT def $
        typeCheckValue uval