Add a basic ShouldFail test

This adds a basic test that is expected to fail due to not asserting a
necessary precondition. We check that such tests fail in the test suite by way
of the `tasty-expected-failure` package.

Fixes #13.

Author: RyanGlScott

copilot-verifier/copilot-verifier.cabal

@@ -67,6 +67,9 @@ library copilot-verifier-examples
     copilot-verifier
   exposed-modules:
     Copilot.Verifier.Examples
+
+    Copilot.Verifier.Examples.ShouldFail.UnderConstrained
+
     Copilot.Verifier.Examples.ShouldPass.Array
     Copilot.Verifier.Examples.ShouldPass.Arith
     Copilot.Verifier.Examples.ShouldPass.Clock
@@ -99,6 +102,8 @@ test-suite copilot-verifier-test
     case-insensitive,
     copilot-verifier,
     copilot-verifier-examples,
+    silently >= 1.2,
     tasty >= 0.10,
+    tasty-expected-failure >= 0.12,
     tasty-hunit >= 0.10
   main-is: Test.hs

copilot-verifier/examples/Copilot/Verifier/Examples.hs

@@ -1,5 +1,8 @@
 {-# LANGUAGE OverloadedStrings #-}
-module Copilot.Verifier.Examples (shouldPassExamples) where
+module Copilot.Verifier.Examples
+  ( shouldFailExamples
+  , shouldPassExamples
+  ) where
 
 import qualified Data.CaseInsensitive as CI
 import Data.CaseInsensitive (CI)
@@ -8,6 +11,7 @@ import Data.Map (Map)
 import Data.Text (Text)
 
 import Copilot.Verifier (Verbosity)
+import qualified Copilot.Verifier.Examples.ShouldFail.UnderConstrained as UnderConstrained
 import qualified Copilot.Verifier.Examples.ShouldPass.Array   as Array
 import qualified Copilot.Verifier.Examples.ShouldPass.Arith   as Arith
 import qualified Copilot.Verifier.Examples.ShouldPass.Clock   as Clock
@@ -20,6 +24,11 @@ import qualified Copilot.Verifier.Examples.ShouldPass.Structs as Structs
 import qualified Copilot.Verifier.Examples.ShouldPass.Voting  as Voting
 import qualified Copilot.Verifier.Examples.ShouldPass.WCV     as WCV
 
+shouldFailExamples :: Verbosity -> Map (CI Text) (IO ())
+shouldFailExamples verb = Map.fromList
+    [ example "UnderConstrained" (UnderConstrained.verifySpec verb)
+    ]
+
 shouldPassExamples :: Verbosity -> Map (CI Text) (IO ())
 shouldPassExamples verb = Map.fromList
     [ example "Array" (Array.verifySpec verb)
@@ -34,6 +43,6 @@ shouldPassExamples verb = Map.fromList
     , example "Voting" (Voting.verifySpec verb)
     , example "WCV" (WCV.verifySpec verb)
     ]
-  where
-    example :: Text -> IO () -> (CI Text, IO ())
-    example name action = (CI.mk name, action)
+
+example :: Text -> IO () -> (CI Text, IO ())
+example name action = (CI.mk name, action)

copilot-verifier/examples/Copilot/Verifier/Examples/ShouldFail/UnderConstrained.hs

@@ -0,0 +1,25 @@
+{-# LANGUAGE NoImplicitPrelude #-}
+
+-- | This will fail to verify since the verification does not assume the
+-- @nonzero@ property, which is needed to prevent a division-by-zero error.
+module Copilot.Verifier.Examples.ShouldFail.UnderConstrained where
+
+import Language.Copilot
+import Copilot.Compile.C99
+import Copilot.Verifier (Verbosity, verifyWithVerbosity)
+
+spec :: Spec
+spec = do
+  let stream :: Stream Int16
+      stream = extern "stream" Nothing
+
+  _ <- prop "nonzero" (forall (stream /= 0))
+  trigger "streamDiv" ((stream `div` stream) == 1) [arg stream]
+
+verifySpec :: Verbosity -> IO ()
+verifySpec verb = do
+  spec' <- reify spec
+  verifyWithVerbosity verb mkDefaultCSettings
+    -- ["nonzero"]
+    []
+    "underConstrained" spec'

copilot-verifier/exe/VerifyExamples.hs

@@ -13,7 +13,7 @@ import Data.Traversable (for)
 import Options.Applicative
 
 import Copilot.Verifier (Verbosity(..))
-import Copilot.Verifier.Examples (shouldPassExamples)
+import Copilot.Verifier.Examples (shouldFailExamples, shouldPassExamples)
 
 newtype Options = Options
   { examples :: [CI Text]
@@ -39,7 +39,7 @@ verifyExamples :: Options -> IO ()
 verifyExamples Options{examples} = do
   -- Check that all requested examples exist
   examplesWithMain <- for examples $ \example ->
-    case Map.lookup example (shouldPassExamples Noisy) of
+    case Map.lookup example (shouldFailExamples Noisy `Map.union` shouldPassExamples Noisy) of
       Just m  -> pure (example, m)
       Nothing -> fail $ "No example named " ++ Text.unpack (CI.original example)
 

copilot-verifier/test/Test.hs

@@ -3,14 +3,30 @@ module Main (main) where
 import qualified Data.CaseInsensitive as CI
 import qualified Data.Map as Map
 import qualified Data.Text as Text
+import System.IO (stderr, stdout)
+import System.IO.Silently (hSilence)
 import Test.Tasty
+import Test.Tasty.ExpectedFailure
 import Test.Tasty.HUnit
 
 import Copilot.Verifier (Verbosity(..))
-import Copilot.Verifier.Examples (shouldPassExamples)
+import Copilot.Verifier.Examples (shouldFailExamples, shouldPassExamples)
 
 main :: IO ()
 main = defaultMain $
-  testGroup "copilot-verifier-examples tests" $
-    map (\(name, action) -> testCase (Text.unpack (CI.original name)) action)
-        (Map.toAscList (shouldPassExamples Quiet))
+  testGroup "copilot-verifier-examples tests"
+    [ testGroup "should-fail tests" $
+        -- Why use hSilence for the should-fail tests when we are passing
+        -- Quiet? It's because crux-llvm errors are logged at the highest
+        -- severity possible, and even Crux's quietMode isn't enough to
+        -- suppress those messages. We could try messing with things on the
+        -- Crux side to avoid this, but it's simpler just to use hSilence here.
+        -- After all, we don't really care about the output of failing tests
+        -- anyway, just their exit codes.
+        map (\(name, action) -> expectFail (testCase (Text.unpack (CI.original name))
+                                                     (hSilence [stderr, stdout] action)))
+            (Map.toAscList (shouldFailExamples Quiet))
+    , testGroup "should-pass tests" $
+        map (\(name, action) -> testCase (Text.unpack (CI.original name)) action)
+            (Map.toAscList (shouldPassExamples Quiet))
+    ]