FPNegation.hs

{-# LANGUAGE NoImplicitPrelude #-}

-- | This will not succeed when 'smtFloatMode' is 'FloatUninterpreted', as Clang
-- will turn @input /= 30.0@ below into a more complicated expression that also
-- checks if @30.0@ is NaN or not. This is logically equivalent to the original
-- specification, but an SMT solver cannot conclude this when all of the
-- floating-point operations involved are treated as uninterpreted functions.
--
-- To make this work, we set 'smtFloatMode' to 'FloatIEEE' instead. This works
-- because all of the floating-point operations in the specification below are
-- native to SMT-LIB.
module Copilot.Verifier.Examples.ShouldPass.FPNegation where

import Copilot.Compile.C99 (mkDefaultCSettings)
import Copilot.Verifier ( Verbosity, VerifierOptions(..)
                        , defaultVerifierOptions, verifyWithOptions )
import Copilot.Verifier.FloatMode (FloatMode(..))
import qualified Copilot.Library.PTLTL as PTLTL
import Language.Copilot

input :: Stream Float
input = extern "input" Nothing

-- | MyProperty
--   @
--   Input is never 30.0
--   @
propMyProperty :: Stream Bool
propMyProperty = PTLTL.alwaysBeen (input /= 30.0)

-- | Clock that increases in one-unit steps.
clock :: Stream Int64
clock = [0] ++ (clock + 1)

-- | First Time Point
ftp :: Stream Bool
ftp = [True] ++ false

pre :: Stream Bool -> Stream Bool
pre = ([False] ++)

tpre :: Stream Bool -> Stream Bool
tpre = ([True] ++)

notPreviousNot :: Stream Bool -> Stream Bool
notPreviousNot = not . PTLTL.previous . not

-- | Complete specification. Calls C handler functions when properties are
-- violated.
spec :: Spec
spec = do
  trigger "handlerMyProperty" (not propMyProperty) []

verifySpec :: Verbosity -> IO ()
verifySpec verb = do
  spec' <- reify spec
  verifyWithOptions
    (defaultVerifierOptions
      { verbosity = verb
      , smtFloatMode = FloatIEEE
      })
    mkDefaultCSettings [] "fpNegation" spec'