{-# LANGUAGE DataKinds #-}
{-# LANGUAGE NoImplicitPrelude #-}

-- | This will fail to verify since the verification does not assume the
-- @withinBounds@ property, which is needed to prevent an out-of-bounds array index.
module Copilot.Verifier.Examples.ShouldFail.Partial.IndexOutOfBounds where

import Language.Copilot
import Copilot.Compile.C99
import Copilot.Verifier ( Verbosity, VerifierOptions(..)
                        , defaultVerifierOptions, verifyWithOptions )

spec :: Spec
spec :: Spec
spec = do
  let stream1 :: Stream (Array 2 Int16)
      stream1 :: Stream (Array 2 Int16)
stream1 = Array 2 Int16 -> Stream (Array 2 Int16)
forall a. Typed a => a -> Stream a
constant ([Int16] -> Array 2 Int16
forall (n :: Nat) t. KnownNat n => [t] -> Array n t
array [Int16
27, Int16
42])

      stream2 :: Stream Word32
      stream2 :: Stream Word32
stream2 = String -> Maybe [Word32] -> Stream Word32
forall a. Typed a => String -> Maybe [a] -> Stream a
extern String
"stream2" Maybe [Word32]
forall a. Maybe a
Nothing

  PropRef Universal
_ <- String -> Prop Universal -> Writer [SpecItem] (PropRef Universal)
forall a. String -> Prop a -> Writer [SpecItem] (PropRef a)
prop String
"withinBounds" (Stream Bool -> Prop Universal
forAll (Stream Word32
stream2 Stream Word32 -> Stream Word32 -> Stream Bool
forall a. (Ord a, Typed a) => Stream a -> Stream a -> Stream Bool
< Word32 -> Stream Word32
constW32 Word32
2))
  String -> Stream Bool -> [Arg] -> Spec
trigger String
"streamIndex" ((Stream (Array 2 Int16)
stream1 Stream (Array 2 Int16) -> Stream Word32 -> Stream Int16
forall (n :: Nat) t.
(KnownNat n, Typed t) =>
Stream (Array n t) -> Stream Word32 -> Stream t
! Stream Word32
stream2) Stream Int16 -> Stream Int16 -> Stream Bool
forall a. (Eq a, Typed a) => Stream a -> Stream a -> Stream Bool
== Stream Int16
1) [Stream (Array 2 Int16) -> Arg
forall a. Typed a => Stream a -> Arg
arg Stream (Array 2 Int16)
stream1, Stream Word32 -> Arg
forall a. Typed a => Stream a -> Arg
arg Stream Word32
stream2]

verifySpec :: Verbosity -> IO ()
verifySpec :: Verbosity -> IO ()
verifySpec Verbosity
verb = do
  Spec
spec' <- Spec -> IO Spec
forall a. Spec' a -> IO Spec
reify Spec
spec
  VerifierOptions -> CSettings -> [String] -> String -> Spec -> IO ()
verifyWithOptions VerifierOptions
defaultVerifierOptions{verbosity = verb}
    CSettings
mkDefaultCSettings
    -- ["withinBounds"]
    []
    String
"indexFail" Spec
spec'