Skip to content

Commit 78a4032

Browse files
RyanGlScottRyanGlScott
committed
Control verbosity more in logging
This adds a new `Verbosity` data type and a corresponding `verifyWithVerbosity` function that controls whether `copilot-verifier` should produce logs or not. We want to make the `Verbosity` be `Quiet` primarily in the test suite so that the diagnostic output does not drown out the output from `tasty`. This is a first step towards the first bullet point in #13.
1 parent f1af89b commit 78a4032

17 files changed

Lines changed: 137 additions & 92 deletions

File tree

‎copilot-verifier/copilot-verifier.cabal‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -86,6 +86,7 @@ executable verify-examples
8686
main-is: VerifyExamples.hs
8787
build-depends:
8888
case-insensitive,
89+
copilot-verifier,
8990
copilot-verifier-examples,
9091
optparse-applicative
9192

@@ -96,6 +97,7 @@ test-suite copilot-verifier-test
9697
hs-source-dirs: test
9798
build-depends:
9899
case-insensitive,
100+
copilot-verifier,
99101
copilot-verifier-examples,
100102
tasty >= 0.10,
101103
tasty-hunit >= 0.10

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

Lines changed: 14 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -7,6 +7,7 @@ import qualified Data.Map as Map
77
import Data.Map (Map)
88
import Data.Text (Text)
99

10+
import Copilot.Verifier (Verbosity)
1011
import qualified Copilot.Verifier.Examples.Array as Array
1112
import qualified Copilot.Verifier.Examples.Arith as Arith
1213
import qualified Copilot.Verifier.Examples.Clock as Clock
@@ -19,19 +20,19 @@ import qualified Copilot.Verifier.Examples.Structs as Structs
1920
import qualified Copilot.Verifier.Examples.Voting as Voting
2021
import qualified Copilot.Verifier.Examples.WCV as WCV
2122

22-
allExamples :: Map (CI Text) (IO ())
23-
allExamples = Map.fromList
24-
[ example "Array" Array.main
25-
, example "Arith" Arith.main
26-
, example "Clock" Clock.main
27-
, example "Counter" Counter.main
28-
, example "Engine" Engine.main
29-
, example "FPOps" FPOps.main
30-
, example "Heater" Heater.main
31-
, example "IntOps" IntOps.main
32-
, example "Structs" Structs.main
33-
, example "Voting" Voting.main
34-
, example "WCV" WCV.main
23+
allExamples :: Verbosity -> Map (CI Text) (IO ())
24+
allExamples verb = Map.fromList
25+
[ example "Array" (Array.verifySpec verb)
26+
, example "Arith" (Arith.verifySpec verb)
27+
, example "Clock" (Clock.verifySpec verb)
28+
, example "Counter" (Counter.verifySpec verb)
29+
, example "Engine" (Engine.verifySpec verb)
30+
, example "FPOps" (FPOps.verifySpec verb)
31+
, example "Heater" (Heater.verifySpec verb)
32+
, example "IntOps" (IntOps.verifySpec verb)
33+
, example "Structs" (Structs.verifySpec verb)
34+
, example "Voting" (Voting.verifySpec verb)
35+
, example "WCV" (WCV.verifySpec verb)
3536
]
3637
where
3738
example :: Text -> IO () -> (CI Text, IO ())

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

Lines changed: 10 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -3,9 +3,12 @@
33

44
module Copilot.Verifier.Examples.Arith where
55

6+
import Control.Monad (when)
7+
import qualified Prelude as P
8+
69
import Language.Copilot
710
import Copilot.Compile.C99
8-
import Copilot.Verifier (verify)
11+
import Copilot.Verifier (Verbosity(..), verifyWithVerbosity)
912
import Copilot.Theorem.What4 (prove, Solver(..))
1013

1114
-- The largest unsigned 32-bit prime
@@ -36,11 +39,12 @@ multRingSpec = do
3639
acc :: Stream Word32
3740
acc = [1] ++ unsafeCast ((cast acc * cast clamp) `mod` (cast lastPrime :: Stream Word64))
3841

39-
main :: IO ()
40-
main =
42+
verifySpec :: Verbosity -> IO ()
43+
verifySpec verb =
4144
do s <- reify multRingSpec
4245
r <- prove Z3 s
43-
print r
44-
verify mkDefaultCSettings ["reduced"] "multRingSpec" s
46+
when (verb P.== Noisy) $
47+
print r
48+
verifyWithVerbosity verb mkDefaultCSettings ["reduced"] "multRingSpec" s
4549

46-
--main = interpret 10 engineMonitor
50+
--verifySpec _ = interpret 10 engineMonitor

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

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -15,7 +15,7 @@ module Copilot.Verifier.Examples.Array where
1515

1616
import Language.Copilot
1717
import Copilot.Compile.C99
18-
import Copilot.Verifier (verify)
18+
import Copilot.Verifier (Verbosity, verifyWithVerbosity)
1919

2020
-- Lets define an array of length 2.
2121
-- Make the buffer of the streams 3 elements long.
@@ -33,6 +33,6 @@ spec = do
3333
trigger "func" (arr .!! 0) [arg arr]
3434

3535
-- Compile the spec
36-
main :: IO ()
37-
main = reify spec >>= verify mkDefaultCSettings [] "array"
38-
-- main = interpret 30 spec
36+
verifySpec :: Verbosity -> IO ()
37+
verifySpec verb = reify spec >>= verifyWithVerbosity verb mkDefaultCSettings [] "array"
38+
-- verifySpec _ = interpret 30 spec

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

Lines changed: 9 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -7,11 +7,12 @@
77

88
module Copilot.Verifier.Examples.Clock where
99

10-
import qualified Prelude as P ()
10+
import Control.Monad (when)
11+
import qualified Prelude as P
1112

1213
import Language.Copilot
1314
import Copilot.Compile.C99
14-
import Copilot.Verifier (verify)
15+
import Copilot.Verifier (Verbosity(..), verifyWithVerbosity)
1516
import Copilot.Theorem.What4 (prove, Solver(..))
1617

1718
-- | We need to force a type for the argument of `period`.
@@ -34,8 +35,10 @@ spec = do
3435
trigger "clksHigh" (clkStream && clkStream') []
3536

3637

37-
main :: IO ()
38-
main =
38+
verifySpec :: Verbosity -> IO ()
39+
verifySpec verb =
3940
do s <- reify spec
40-
print =<< prove Z3 s
41-
verify mkDefaultCSettings [] "clock" s
41+
r <- prove Z3 s
42+
when (verb P.== Noisy) $
43+
print r
44+
verifyWithVerbosity verb mkDefaultCSettings [] "clock" s

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

Lines changed: 11 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -8,9 +8,12 @@
88

99
module Copilot.Verifier.Examples.Counter where
1010

11+
import Control.Monad (when)
12+
import qualified Prelude as P
13+
1114
import Language.Copilot
1215
import Copilot.Compile.C99
13-
import Copilot.Verifier (verify)
16+
import Copilot.Verifier (Verbosity(..), verifyWithVerbosity)
1417
import Copilot.Theorem.What4 (prove, Solver(..))
1518

1619
-- A resettable counter
@@ -41,9 +44,11 @@ spec =
4144
(bytecounter == bytecounter2)))
4245
trigger "counter" true [arg $ bytecounter, arg $ bytecounter2]
4346

44-
main :: IO ()
45-
-- main = interpret 1280 spec
46-
main =
47+
verifySpec :: Verbosity -> IO ()
48+
-- verifSpec _ = interpret 1280 spec
49+
verifySpec verb =
4750
do s <- reify spec
48-
print =<< prove Z3 s
49-
verify mkDefaultCSettings ["range", "range2"] "counter" s
51+
r <- prove Z3 s
52+
when (verb P.== Noisy) $
53+
print r
54+
verifyWithVerbosity verb mkDefaultCSettings ["range", "range2"] "counter" s

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

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -10,7 +10,7 @@ module Copilot.Verifier.Examples.Engine where
1010

1111
import Language.Copilot
1212
import Copilot.Compile.C99
13-
import Copilot.Verifier (verify)
13+
import Copilot.Verifier (Verbosity, verifyWithVerbosity)
1414

1515
import qualified Prelude as P
1616

@@ -37,6 +37,6 @@ engineMonitor = do
3737
zero = Just $ repeat (0 :: Word8)
3838
cooler = Just $ [True, True] P.++ repeat False
3939

40-
main :: IO ()
41-
main = reify engineMonitor >>= verify mkDefaultCSettings [] "engine"
42-
--main = interpret 10 engineMonitor
40+
verifySpec :: Verbosity -> IO ()
41+
verifySpec verb = reify engineMonitor >>= verifyWithVerbosity verb mkDefaultCSettings [] "engine"
42+
--verifySpec _ = interpret 10 engineMonitor

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

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,7 @@ module Copilot.Verifier.Examples.FPOps where
55

66
import Copilot.Compile.C99 (mkDefaultCSettings)
77
import qualified Copilot.Language.Stream as Copilot
8-
import Copilot.Verifier (verify)
8+
import Copilot.Verifier (Verbosity, verifyWithVerbosity)
99
import Data.Proxy (Proxy(..))
1010
import Language.Copilot
1111
import qualified Prelude as P
@@ -80,7 +80,7 @@ testOp2 :: (RealFloat a, Typed a) =>
8080
testOp2 op stream =
8181
op stream stream >= op stream stream
8282

83-
main :: IO ()
84-
main = do
83+
verifySpec :: Verbosity -> IO ()
84+
verifySpec verb = do
8585
spec' <- reify spec
86-
verify mkDefaultCSettings [] "fpOps" spec'
86+
verifyWithVerbosity verb mkDefaultCSettings [] "fpOps" spec'

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

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -14,7 +14,7 @@ import Copilot.Compile.C99
1414
--import Copilot.Core.PrettyDot (prettyPrintDot)
1515
--import Copilot.Language.Prelude
1616

17-
import Copilot.Verifier (verify)
17+
import Copilot.Verifier (Verbosity, verifyWithVerbosity)
1818

1919
import Prelude ()
2020

@@ -36,8 +36,8 @@ spec = do
3636
trigger "heatoff" (sumTemp > (21*fromIntegral window)) [arg sumTemp]
3737

3838
-- Compile the spec
39-
main :: IO ()
40-
main = reify spec >>= verify mkDefaultCSettings [] "heater"
39+
verifySpec :: Verbosity -> IO ()
40+
verifySpec verb = reify spec >>= verifyWithVerbosity verb mkDefaultCSettings [] "heater"
4141
{-
4242
do spec' <- reify spec
4343
putStrLn $ prettyPrintDot spec'

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

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -2,7 +2,7 @@
22
module Copilot.Verifier.Examples.IntOps where
33

44
import Copilot.Compile.C99 (mkDefaultCSettings)
5-
import Copilot.Verifier (verify)
5+
import Copilot.Verifier (Verbosity, verifyWithVerbosity)
66
import Language.Copilot
77
import qualified Prelude as P
88

@@ -56,7 +56,7 @@ testOp2 :: (Stream Int16 -> Stream Int16 -> Stream Int16) ->
5656
testOp2 op stream1 stream2 =
5757
op stream1 stream2 == op stream1 stream2
5858

59-
main :: IO ()
60-
main = do
59+
verifySpec :: Verbosity -> IO ()
60+
verifySpec verb = do
6161
spec' <- reify spec
62-
verify mkDefaultCSettings ["nonzero", "shiftByBits"] "intOps" spec'
62+
verifyWithVerbosity verb mkDefaultCSettings ["nonzero", "shiftByBits"] "intOps" spec'

0 commit comments

Comments
 (0)