Factor out verifier-specific options into their own data type

Currently, there is only one verifier-specific option, the `Verbosity`. However, implementing a fix for #5 will require yet another option, so this patch will make it simpler to add another option when the time comes.
Copilot-Language · Jan 24, 2022 · b277a2b · b277a2b
1 parent 6c6d652
commit b277a2b
Show file tree

Hide file tree

Showing 13 changed files with 71 additions and 30 deletions.
diff --git a/copilot-verifier/examples/Copilot/Verifier/Examples/ShouldFail/UnderConstrained.hs b/copilot-verifier/examples/Copilot/Verifier/Examples/ShouldFail/UnderConstrained.hs
@@ -6,7 +6,8 @@ module Copilot.Verifier.Examples.ShouldFail.UnderConstrained where
 
 import Language.Copilot
 import Copilot.Compile.C99
-import Copilot.Verifier (Verbosity, verifyWithVerbosity)
+import Copilot.Verifier ( Verbosity, VerifierOptions(..)
+                        , defaultVerifierOptions, verifyWithOptions )
 
 spec :: Spec
 spec = do
@@ -19,7 +20,8 @@ spec = do
 verifySpec :: Verbosity -> IO ()
 verifySpec verb = do
   spec' <- reify spec
-  verifyWithVerbosity verb mkDefaultCSettings
+  verifyWithOptions defaultVerifierOptions{verbosity = verb}
+    mkDefaultCSettings
     -- ["nonzero"]
     []
     "underConstrained" spec'
diff --git a/copilot-verifier/examples/Copilot/Verifier/Examples/ShouldPass/Arith.hs b/copilot-verifier/examples/Copilot/Verifier/Examples/ShouldPass/Arith.hs
@@ -8,7 +8,8 @@ import qualified Prelude as P
 
 import Language.Copilot
 import Copilot.Compile.C99
-import Copilot.Verifier (Verbosity(..), verifyWithVerbosity)
+import Copilot.Verifier ( Verbosity(..), VerifierOptions(..)
+                        , defaultVerifierOptions, verifyWithOptions )
 import Copilot.Theorem.What4 (prove, Solver(..))
 
 -- The largest unsigned 32-bit prime
@@ -45,6 +46,7 @@ verifySpec verb =
      r <- prove Z3 s
      when (verb P.== Noisy) $
        print r
-     verifyWithVerbosity verb mkDefaultCSettings ["reduced"] "multRingSpec" s
+     verifyWithOptions defaultVerifierOptions{verbosity = verb}
+                       mkDefaultCSettings ["reduced"] "multRingSpec" s
 
 --verifySpec _ = interpret 10 engineMonitor
diff --git a/copilot-verifier/examples/Copilot/Verifier/Examples/ShouldPass/Array.hs b/copilot-verifier/examples/Copilot/Verifier/Examples/ShouldPass/Array.hs
@@ -15,7 +15,8 @@ module Copilot.Verifier.Examples.ShouldPass.Array where
 
 import Language.Copilot
 import Copilot.Compile.C99
-import Copilot.Verifier (Verbosity, verifyWithVerbosity)
+import Copilot.Verifier ( Verbosity, VerifierOptions(..)
+                        , defaultVerifierOptions, verifyWithOptions )
 
 -- Lets define an array of length 2.
 -- Make the buffer of the streams 3 elements long.
@@ -34,5 +35,6 @@ spec = do
 
 -- Compile the spec
 verifySpec :: Verbosity -> IO ()
-verifySpec verb = reify spec >>= verifyWithVerbosity verb mkDefaultCSettings [] "array"
+verifySpec verb = reify spec >>= verifyWithOptions defaultVerifierOptions{verbosity = verb}
+                                                   mkDefaultCSettings [] "array"
 -- verifySpec _ = interpret 30 spec
diff --git a/copilot-verifier/examples/Copilot/Verifier/Examples/ShouldPass/Clock.hs b/copilot-verifier/examples/Copilot/Verifier/Examples/ShouldPass/Clock.hs
@@ -12,7 +12,8 @@ import qualified Prelude as P
 
 import Language.Copilot
 import Copilot.Compile.C99
-import Copilot.Verifier (Verbosity(..), verifyWithVerbosity)
+import Copilot.Verifier ( Verbosity(..), VerifierOptions(..)
+                        , defaultVerifierOptions, verifyWithOptions )
 import Copilot.Theorem.What4 (prove, Solver(..))
 
 -- | We need to force a type for the argument of `period`.
@@ -41,4 +42,5 @@ verifySpec verb =
      r <- prove Z3 s
      when (verb P.== Noisy) $
        print r
-     verifyWithVerbosity verb mkDefaultCSettings [] "clock" s
+     verifyWithOptions defaultVerifierOptions{verbosity = verb}
+                       mkDefaultCSettings [] "clock" s
diff --git a/copilot-verifier/examples/Copilot/Verifier/Examples/ShouldPass/Counter.hs b/copilot-verifier/examples/Copilot/Verifier/Examples/ShouldPass/Counter.hs
@@ -13,7 +13,8 @@ import qualified Prelude as P
 
 import Language.Copilot
 import Copilot.Compile.C99
-import Copilot.Verifier (Verbosity(..), verifyWithVerbosity)
+import Copilot.Verifier ( Verbosity(..), VerifierOptions(..)
+                        , defaultVerifierOptions, verifyWithOptions )
 import Copilot.Theorem.What4 (prove, Solver(..))
 
 -- A resettable counter
@@ -51,4 +52,5 @@ verifySpec verb =
      r <- prove Z3 s
      when (verb P.== Noisy) $
        print r
-     verifyWithVerbosity verb mkDefaultCSettings ["range", "range2"] "counter" s
+     verifyWithOptions defaultVerifierOptions{verbosity = verb}
+                       mkDefaultCSettings ["range", "range2"] "counter" s
diff --git a/copilot-verifier/examples/Copilot/Verifier/Examples/ShouldPass/Engine.hs b/copilot-verifier/examples/Copilot/Verifier/Examples/ShouldPass/Engine.hs
@@ -10,7 +10,8 @@ module Copilot.Verifier.Examples.ShouldPass.Engine where
 
 import Language.Copilot
 import Copilot.Compile.C99
-import Copilot.Verifier (Verbosity, verifyWithVerbosity)
+import Copilot.Verifier ( Verbosity, VerifierOptions(..)
+                        , defaultVerifierOptions, verifyWithOptions )
 
 import qualified Prelude as P
 
@@ -38,5 +39,6 @@ engineMonitor = do
   cooler = Just $ [True, True] P.++ repeat False
 
 verifySpec :: Verbosity -> IO ()
-verifySpec verb = reify engineMonitor >>= verifyWithVerbosity verb mkDefaultCSettings [] "engine"
+verifySpec verb = reify engineMonitor >>= verifyWithOptions defaultVerifierOptions{verbosity = verb}
+                                                            mkDefaultCSettings [] "engine"
 --verifySpec _ = interpret 10 engineMonitor
diff --git a/copilot-verifier/examples/Copilot/Verifier/Examples/ShouldPass/FPOps.hs b/copilot-verifier/examples/Copilot/Verifier/Examples/ShouldPass/FPOps.hs
@@ -5,7 +5,8 @@ module Copilot.Verifier.Examples.ShouldPass.FPOps where
 
 import Copilot.Compile.C99 (mkDefaultCSettings)
 import qualified Copilot.Language.Stream as Copilot
-import Copilot.Verifier (Verbosity, verifyWithVerbosity)
+import Copilot.Verifier ( Verbosity, VerifierOptions(..)
+                        , defaultVerifierOptions, verifyWithOptions )
 import Data.Proxy (Proxy(..))
 import Language.Copilot
 import qualified Prelude as P
@@ -83,4 +84,5 @@ testOp2 op stream =
 verifySpec :: Verbosity -> IO ()
 verifySpec verb = do
   spec' <- reify spec
-  verifyWithVerbosity verb mkDefaultCSettings [] "fpOps" spec'
+  verifyWithOptions defaultVerifierOptions{verbosity = verb}
+                    mkDefaultCSettings [] "fpOps" spec'
diff --git a/copilot-verifier/examples/Copilot/Verifier/Examples/ShouldPass/Heater.hs b/copilot-verifier/examples/Copilot/Verifier/Examples/ShouldPass/Heater.hs
@@ -14,7 +14,8 @@ import Copilot.Compile.C99
 --import Copilot.Core.PrettyDot (prettyPrintDot)
 --import Copilot.Language.Prelude
 
-import Copilot.Verifier (Verbosity, verifyWithVerbosity)
+import Copilot.Verifier ( Verbosity, VerifierOptions(..)
+                        , defaultVerifierOptions, verifyWithOptions )
 
 import Prelude ()
 
@@ -37,7 +38,8 @@ spec = do
 
 -- Compile the spec
 verifySpec :: Verbosity -> IO ()
-verifySpec verb = reify spec >>= verifyWithVerbosity verb mkDefaultCSettings [] "heater"
+verifySpec verb = reify spec >>= verifyWithOptions defaultVerifierOptions{verbosity = verb}
+                                                   mkDefaultCSettings [] "heater"
 {-
   do spec' <- reify spec
      putStrLn $ prettyPrintDot spec'

diff --git a/copilot-verifier/examples/Copilot/Verifier/Examples/ShouldPass/IntOps.hs b/copilot-verifier/examples/Copilot/Verifier/Examples/ShouldPass/IntOps.hs
@@ -2,7 +2,8 @@
 module Copilot.Verifier.Examples.ShouldPass.IntOps where
 
 import Copilot.Compile.C99 (mkDefaultCSettings)
-import Copilot.Verifier (Verbosity, verifyWithVerbosity)
+import Copilot.Verifier ( Verbosity, VerifierOptions(..)
+                        , defaultVerifierOptions, verifyWithOptions )
 import Language.Copilot
 import qualified Prelude as P
 
@@ -59,4 +60,5 @@ testOp2 op stream1 stream2 =
 verifySpec :: Verbosity -> IO ()
 verifySpec verb = do
   spec' <- reify spec
-  verifyWithVerbosity verb mkDefaultCSettings ["nonzero", "shiftByBits"] "intOps" spec'
+  verifyWithOptions defaultVerifierOptions{verbosity = verb}
+                    mkDefaultCSettings ["nonzero", "shiftByBits"] "intOps" spec'
diff --git a/copilot-verifier/examples/Copilot/Verifier/Examples/ShouldPass/Structs.hs b/copilot-verifier/examples/Copilot/Verifier/Examples/ShouldPass/Structs.hs
@@ -12,7 +12,8 @@ import qualified Prelude as P
 import Language.Copilot
 import Copilot.Compile.C99
 import Copilot.Theorem.What4
-import Copilot.Verifier (Verbosity(..), verifyWithVerbosity)
+import Copilot.Verifier ( Verbosity(..), VerifierOptions(..)
+                        , defaultVerifierOptions, verifyWithOptions )
 
 
 -- | Definition for `Volts`.
@@ -87,4 +88,5 @@ verifySpec verb = do
         Invalid -> putStrLn "invalid"
         Unknown -> putStrLn "unknown"
 
-  verifyWithVerbosity verb mkDefaultCSettings [] "structs" spec'
+  verifyWithOptions defaultVerifierOptions{verbosity = verb}
+                    mkDefaultCSettings [] "structs" spec'
diff --git a/copilot-verifier/examples/Copilot/Verifier/Examples/ShouldPass/Voting.hs b/copilot-verifier/examples/Copilot/Verifier/Examples/ShouldPass/Voting.hs
@@ -10,7 +10,8 @@ module Copilot.Verifier.Examples.ShouldPass.Voting where
 
 import Language.Copilot
 import Copilot.Compile.C99
-import Copilot.Verifier (Verbosity, verifyWithVerbosity)
+import Copilot.Verifier ( Verbosity, VerifierOptions(..)
+                        , defaultVerifierOptions, verifyWithOptions )
 
 vote :: Spec
 vote = do
@@ -59,4 +60,5 @@ vote = do
 
 verifySpec :: Verbosity -> IO ()
 --verifySpec _ = interpret 30 vote
-verifySpec verb = reify vote >>= verifyWithVerbosity verb mkDefaultCSettings [] "voting"
+verifySpec verb = reify vote >>= verifyWithOptions defaultVerifierOptions{verbosity = verb}
+                                                   mkDefaultCSettings [] "voting"
diff --git a/copilot-verifier/examples/Copilot/Verifier/Examples/ShouldPass/WCV.hs b/copilot-verifier/examples/Copilot/Verifier/Examples/ShouldPass/WCV.hs
@@ -11,7 +11,8 @@ module Copilot.Verifier.Examples.ShouldPass.WCV where
 import Language.Copilot
 import qualified Copilot.Theorem.What4 as CT
 import Copilot.Compile.C99
-import Copilot.Verifier (Verbosity, verifyWithVerbosity)
+import Copilot.Verifier ( Verbosity, VerifierOptions(..)
+                        , defaultVerifierOptions, verifyWithOptions )
 
 import qualified Prelude as P
 import Data.Foldable (forM_)
@@ -176,7 +177,8 @@ spec = do
 verifySpec :: Verbosity -> IO ()
 verifySpec verb = do
   spec' <- reify spec
-  verifyWithVerbosity verb mkDefaultCSettings [] "wcv" spec'
+  verifyWithOptions defaultVerifierOptions{verbosity = verb}
+                    mkDefaultCSettings [] "wcv" spec'
 
 {-
   -- Use Z3 to prove the properties.

diff --git a/copilot-verifier/src/Copilot/Verifier.hs b/copilot-verifier/src/Copilot/Verifier.hs
@@ -15,8 +15,10 @@
 
 module Copilot.Verifier
   ( verify
+  , verifyWithOptions
+  , VerifierOptions(..)
+  , defaultVerifierOptions
   , Verbosity(..)
-  , verifyWithVerbosity
   ) where
 
 import Control.Lens (view, (^.), to)
@@ -148,17 +150,32 @@ import What4.Symbol (safeSymbol)
 -- @spec@ under the assumptions @props@ matches the behavior of the C program
 -- compiled with @csettings@ within a directory prefixed by @prefix@.
 verify :: CSettings -> [String] -> String -> Spec -> IO ()
-verify = verifyWithVerbosity Noisy
+verify = verifyWithOptions defaultVerifierOptions
+
+-- | Options for configuring the behavior of the verifier.
+newtype VerifierOptions = VerifierOptions
+  { verbosity :: Verbosity
+    -- ^ How much output the verifier should produce.
+  } deriving stock Show
+
+-- | The default 'VerifierOptions':
+--
+-- * Produce diagnostics as verification proceeds ('Noisy').
+defaultVerifierOptions :: VerifierOptions
+defaultVerifierOptions = VerifierOptions
+  { verbosity = Noisy
+  }
 
 -- | How much output should verification produce?
 data Verbosity
   = Noisy -- ^ Produce diagnostics as verification proceeds.
   | Quiet -- ^ Don't produce any diagnostics.
   deriving stock (Eq, Show)
 
--- | Like 'verify', but with an option to control its 'Verbosity'.
-verifyWithVerbosity :: Verbosity -> CSettings -> [String] -> String -> Spec -> IO ()
-verifyWithVerbosity verb csettings0 properties prefix spec =
+-- | Like 'verify', but with 'VerifierOptions' to more finely control the
+-- verifier's behavior.
+verifyWithOptions :: VerifierOptions -> CSettings -> [String] -> String -> Spec -> IO ()
+verifyWithOptions opts csettings0 properties prefix spec =
   withCopilotLogging $
   do ocfg1 <- defaultOutputConfig copilotLoggingToSayWhat
      let ocfg2 mbOutputOpts = (ocfg1 mbOutputOpts) { Log._quiet = quiet }
@@ -195,7 +212,7 @@ verifyWithVerbosity verb csettings0 properties prefix spec =
 
      verifyBitcode csettings properties spec cruxOpts llvmOpts bcFile
   where
-    quiet = verb == Quiet
+    quiet = verbosity opts == Quiet
 
 verifyBitcode ::
   Log.Logs msgs =>