{-# LANGUAGE NoImplicitPrelude #-}

-- | This will fail to verify since the verification does not assume the
-- @withinRange@ property, which is needed to prevent signed integer underflow or overflow.
module Copilot.Verifier.Examples.ShouldFail.Partial.MulSignedWrap where

import qualified Prelude as P

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

spec :: Spec
spec :: Spec
spec = do
  let stream :: Stream Int32
      stream :: Stream Int32
stream = String -> Maybe [Int32] -> Stream Int32
forall a. Typed a => String -> Maybe [a] -> Stream a
extern String
"stream" Maybe [Int32]
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
"withinRange" (Stream Bool -> Prop Universal
forAll
           (Int32 -> Stream Int32
constI32 ((Int32
forall a. Bounded a => a
minBound Int32 -> Int32 -> Int32
forall a. Num a => a -> a -> a
P.+ Int32
1) Int32 -> Int32 -> Int32
forall a. Num a => a -> a -> a
P.* Int32
2) Stream Int32 -> Stream Int32 -> Stream Bool
forall a. (Ord a, Typed a) => Stream a -> Stream a -> Stream Bool
< Stream Int32
stream
         Stream Bool -> Stream Bool -> Stream Bool
&& Stream Int32
stream Stream Int32 -> Stream Int32 -> Stream Bool
forall a. (Ord a, Typed a) => Stream a -> Stream a -> Stream Bool
< Int32 -> Stream Int32
constI32 ((Int32
forall a. Bounded a => a
maxBound Int32 -> Int32 -> Int32
forall a. Num a => a -> a -> a
P.- Int32
1) Int32 -> Int32 -> Int32
forall a. Integral a => a -> a -> a
`P.div` Int32
2)))
  String -> Stream Bool -> [Arg] -> Spec
trigger String
"streamMulSigned" ((Stream Int32
stream Stream Int32 -> Stream Int32 -> Stream Int32
forall a. Num a => a -> a -> a
* Stream Int32
2) Stream Int32 -> Stream Int32 -> Stream Bool
forall a. (Eq a, Typed a) => Stream a -> Stream a -> Stream Bool
== Stream Int32
2) [Stream Int32 -> Arg
forall a. Typed a => Stream a -> Arg
arg Stream Int32
stream]

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
    -- ["withinRange"]
    []
    String
"mulSignedWrapFail" Spec
spec'