GaloisInc/cryptol
1
1
Fork 0
mirror of https://github.com/GaloisInc/cryptol.git synced 2024-12-28 02:15:31 +03:00
Code Issues Projects Releases Wiki Activity

refactor :check and :exhaust

Browse Source 
This is to set up improvements to the cryptol-server, and therefore
pycryptol interface.

This patch also fixes a regression in pretty-printing output caused by a
previous error in fixity of the `<>` operator
This commit is contained in:
Adam C. Foltzer 2015-12-22 18:17:20 -08:00
parent f87ea62646
commit aeefab69a1
14 changed files with 168 additions and 139 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
cryptol.cabal
View File

@ -149,8 +149,7 @@ library
Cryptol.Eval.Type,
Cryptol.Eval.Value,
Cryptol.Testing.Eval,
Cryptol.Testing.Exhaust,
Cryptol.Testing.Concrete,
Cryptol.Testing.Random,
Cryptol.Symbolic,

2
src/Cryptol/ModuleSystem/Renamer.hs
View File

@ -139,7 +139,7 @@ instance PP RenamerWarning where
ppPrec _ (SymbolShadowed new originals disp) = fixNameDisp disp $
hang (text "[warning] at" <+> loc)
4 $ fsep [ text "This binding for" <+> sym
, text "shadows the existing binding" <> plural <+> text "from" ]
, (text "shadows the existing binding" <> plural) <+> text "from" ]
$$ vcat (map ppLocName originals)
where

2
src/Cryptol/Parser/AST.hs
View File

@ -717,7 +717,7 @@ instance (Show name, PPName name) => PP (Expr name) where
ESel e l -> ppPrec 4 e <> text "." <> pp l
-- low prec
EFun xs e -> wrap n 0 (text "\\" <> hsep (map (ppPrec 3) xs) <+>
EFun xs e -> wrap n 0 ((text "\\" <> hsep (map (ppPrec 3) xs)) <+>
text "->" <+> pp e)
EIf e1 e2 e3 -> wrap n 0 $ sep [ text "if" <+> pp e1

79
src/Cryptol/REPL/Command.hs
View File

@ -54,9 +54,8 @@ import qualified Cryptol.ModuleSystem.Renamer as M (RenamerWarning(SymbolShadowe
import qualified Cryptol.Utils.Ident as M
import qualified Cryptol.Eval.Value as E
import qualified Cryptol.Testing.Eval as Test
import Cryptol.Testing.Concrete
import qualified Cryptol.Testing.Random as TestR
import qualified Cryptol.Testing.Exhaust as TestX
import Cryptol.Parser
(parseExprWith,parseReplWith,ParseError(),Config(..),defaultConfig
,parseModName,parseHelpName)
@ -267,25 +266,47 @@ qcCmd qcMode str =
do expr <- replParseExpr str
(val,ty) <- replEvalExpr expr
EnvNum testNum <- getUser "tests"
case TestX.testableType ty of
Just (sz,vss) | qcMode == QCExhaust || sz <= toInteger testNum ->
do rPutStrLn "Using exhaustive testing."
let doTest _ [] = panic "We've unexpectedly run out of test cases"
[]
doTest _ (vs : vss1) = do
result <- TestX.runOneTest val vs
case testableType ty of
Just (sz,vss) | qcMode == QCExhaust || sz <= toInteger testNum -> do
rPutStrLn "Using exhaustive testing."
let f _ [] = panic "Cryptol.REPL.Command"
["Exhaustive testing ran out of test cases"]
f _ (vs : vss1) = do
result <- io $ runOneTest val vs
return (result, vss1)
ok <- go doTest sz 0 vss
when ok $ rPutStrLn "Q.E.D."
testSpec = TestSpec {
testFn = f
, testTotal = sz
, testRptProgress = ppProgress
, testClrProgress = delProgress
, testRptFailure = ppFailure
, testRptSuccess = do
delTesting
prtLn $ "passed " ++ show sz ++ " tests."
rPutStrLn "Q.E.D."
}
prt testingMsg
_report <- runTests testSpec vss
return ()
n -> case TestR.testableType ty of
Nothing -> raise (TypeNotTestable ty)
Just gens ->
do rPutStrLn "Using random testing."
Just gens -> do
rPutStrLn "Using random testing."
let testSpec = TestSpec {
testFn = \sz g -> io $ TestR.runOneTest val gens sz g
, testTotal = toInteger testNum
, testRptProgress = ppProgress
, testClrProgress = delProgress
, testRptFailure = ppFailure
, testRptSuccess = do
delTesting
prtLn $ "passed " ++ show testNum ++ " tests."
}
prt testingMsg
g <- io newTFGen
ok <- go (TestR.runOneTest val gens) testNum 0 g
when ok $
report <- runTests testSpec g
when (isPass (reportResult report)) $
case n of
Just (valNum,_) ->
do let valNumD = fromIntegral valNum :: Double
@ -325,37 +346,23 @@ qcCmd qcMode str =
delTesting = del (length testingMsg)
delProgress = del totProgressWidth
go _ totNum testNum _
| testNum >= totNum =
do delTesting
prtLn $ "passed " ++ show totNum ++ " tests."
return True
go doTest totNum testNum st =
do ppProgress testNum totNum
res <- io $ doTest (div (100 * (1 + testNum)) totNum) st
opts <- getPPValOpts
delProgress
case res of
(Test.Pass, st1) -> do delProgress
go doTest totNum (testNum + 1) st1
(failure, _g1) -> do
ppFailure failure = do
delTesting
opts <- getPPValOpts
case failure of
Test.FailFalse [] -> do
FailFalse [] -> do
prtLn "FAILED"
Test.FailFalse vs -> do
FailFalse vs -> do
prtLn "FAILED for the following inputs:"
mapM_ (rPrint . pp . E.WithBase opts) vs
Test.FailError err [] -> do
FailError err [] -> do
prtLn "ERROR"
rPrint (pp err)
Test.FailError err vs -> do
FailError err vs -> do
prtLn "ERROR for the following inputs:"
mapM_ (rPrint . pp . E.WithBase opts) vs
rPrint (pp err)
Test.Pass -> panic "Cryptol.REPL.Command" ["unexpected Test.Pass"]
return False
Pass -> panic "Cryptol.REPL.Command" ["unexpected Test.Pass"]
satCmd, proveCmd :: String -> REPL ()
satCmd = cmdProveSat True

82
src/Cryptol/Testing/Exhaust.hs → src/Cryptol/Testing/Concrete.hs
View File

@ -6,17 +6,56 @@
-- Stability : provisional
-- Portability : portable
module Cryptol.Testing.Exhaust where
{-# LANGUAGE RecordWildCards #-}
module Cryptol.Testing.Concrete where
import qualified Cryptol.Testing.Eval as Eval
import Cryptol.TypeCheck.AST
import Cryptol.Eval.Error
import Cryptol.Eval.Value
import Cryptol.Utils.Panic (panic)
import qualified Control.Exception as X
import Data.List(genericReplicate)
import Prelude ()
import Prelude.Compat
-- | A test result is either a pass, a failure due to evaluating to
-- @False@, or a failure due to an exception raised during evaluation
data TestResult
= Pass
| FailFalse [Value]
| FailError EvalError [Value]
isPass :: TestResult -> Bool
isPass Pass = True
isPass _ = False
-- | Apply a testable value to some arguments.
-- Note that this function assumes that the values come from a call to
-- `testableType` (i.e., things are type-correct). We run in the IO
-- monad in order to catch any @EvalError@s.
runOneTest :: Value -> [Value] -> IO TestResult
runOneTest v0 vs0 = run `X.catch` handle
where
run = do
result <- X.evaluate (go v0 vs0)
if result
then return Pass
else return (FailFalse vs0)
handle e = return (FailError e vs0)
go :: Value -> [Value] -> Bool
go (VFun f) (v : vs) = go (f v) vs
go (VFun _) [] = panic "Not enough arguments while applying function"
[]
go (VBit b) [] = b
go v vs = panic "Type error while running test" $
[ "Function:"
, show $ ppValue defaultPPOpts v
, "Arguments:"
] ++ map (show . ppValue defaultPPOpts) vs
{- | Given a (function) type, compute all possible inputs for it.
We also return the total number of test (i.e., the length of the outer list. -}
testableType :: Type -> Maybe (Integer, [[Value]])
@ -29,13 +68,6 @@ testableType ty =
TCon (TC TCBit) [] -> return (1, [[]])
_ -> Nothing
{- | Apply a testable value to some arguments.
Please note that this function assumes that the values come from
a call to `testableType` (i.e., things are type-correct)
-}
runOneTest :: Value -> [Value] -> IO Eval.TestResult
runOneTest = Eval.runOneTest
{- | Given a fully-evaluated type, try to compute the number of values in it.
Returns `Nothing` for infinite types, user-defined types, polymorhic types,
and, currently, function spaces. Of course, we can easily compute the
@ -95,4 +127,36 @@ typeValues ty =
TCon _ _ -> []
--------------------------------------------------------------------------------
-- Driver function
data TestSpec m s = TestSpec {
testFn :: Integer -> s -> m (TestResult, s)
, testTotal :: Integer
, testRptProgress :: Integer -> Integer -> m ()
, testClrProgress :: m ()
, testRptFailure :: TestResult -> m ()
, testRptSuccess :: m ()
}
data TestReport = TestReport {
reportResult :: TestResult
, reportTestTotal :: Integer
}
runTests :: Monad m => TestSpec m s -> s -> m TestReport
runTests TestSpec {..} st0 = go 0 st0
where
go testNum _ | testNum >= testTotal = do
testRptSuccess
return $ TestReport Pass testTotal
go testNum st =
do testRptProgress testNum testTotal
res <- testFn (div (100 * (1 + testNum)) testTotal) st
testClrProgress
case res of
(Pass, st') -> do -- delProgress -- unnecessary?
go (testNum + 1) st'
(failure, _st') -> do
testRptFailure failure
return $ TestReport failure testTotal

50
src/Cryptol/Testing/Eval.hs
View File

@ -1,50 +0,0 @@
{-# LANGUAGE TupleSections #-}
-- |
-- Module : $Header$
-- Copyright : (c) 2013-2015 Galois, Inc.
-- License : BSD3
-- Maintainer : cryptol@galois.com
-- Stability : provisional
-- Portability : portable
--
-- Evaluate test cases and handle exceptions appropriately
module Cryptol.Testing.Eval where
import Cryptol.Eval.Error
import Cryptol.Eval.Value
import Cryptol.Utils.Panic (panic)
import qualified Control.Exception as X
-- | A test result is either a pass, a failure due to evaluating to
-- @False@, or a failure due to an exception raised during evaluation
data TestResult
= Pass
| FailFalse [Value]
| FailError EvalError [Value]
-- | Apply a testable value to some arguments.
-- Note that this function assumes that the values come from a call to
-- `testableType` (i.e., things are type-correct). We run in the IO
-- monad in order to catch any @EvalError@s.
runOneTest :: Value -> [Value] -> IO TestResult
runOneTest v0 vs0 = run `X.catch` handle
where
run = do
result <- X.evaluate (go v0 vs0)
if result
then return Pass
else return (FailFalse vs0)
handle e = return (FailError e vs0)
go :: Value -> [Value] -> Bool
go (VFun f) (v : vs) = go (f v) vs
go (VFun _) [] = panic "Not enough arguments while applying function"
[]
go (VBit b) [] = b
go v vs = panic "Type error while running test" $
[ "Function:"
, show $ ppValue defaultPPOpts v
, "Arguments:"
] ++ map (show . ppValue defaultPPOpts) vs

10
src/Cryptol/Testing/Random.hs
View File

@ -12,7 +12,7 @@
module Cryptol.Testing.Random where
import Cryptol.Eval.Value (BV(..),Value,GenValue(..))
import qualified Cryptol.Testing.Eval as Eval
import qualified Cryptol.Testing.Concrete as Conc
import Cryptol.TypeCheck.AST (Type(..),TCon(..),TC(..),tNoUser)
import Cryptol.Utils.Ident (Ident)
@ -20,7 +20,7 @@ import Control.Monad (forM)
import Data.List (unfoldr, genericTake)
import System.Random (RandomGen, split, random, randomR)
type Gen g = Int -> g -> (Value, g)
type Gen g = Integer -> g -> (Value, g)
{- | Apply a testable value to some randomly-generated arguments.
@ -33,13 +33,13 @@ type Gen g = Int -> g -> (Value, g)
runOneTest :: RandomGen g
=> Value -- ^ Function under test
-> [Gen g] -- ^ Argument generators
-> Int -- ^ Size
-> Integer -- ^ Size
-> g
-> IO (Eval.TestResult, g)
-> IO (Conc.TestResult, g)
runOneTest fun argGens sz g0 = do
let (args, g1) = foldr mkArg ([], g0) argGens
mkArg argGen (as, g) = let (a, g') = argGen sz g in (a:as, g')
result <- Eval.runOneTest fun args
result <- Conc.runOneTest fun args
return (result, g1)
{- | Given a (function) type, compute generators for

13
src/Cryptol/Utils/PP.hs
View File

@ -9,19 +9,21 @@
{-# LANGUAGE Safe #-}
{-# LANGUAGE PatternGuards #-}
{-# LANGUAGE DeriveGeneric #-}
module Cryptol.Utils.PP (module Cryptol.Utils.PP, (<>)) where
module Cryptol.Utils.PP where
import Cryptol.Utils.Ident
import Control.DeepSeq.Generics
import Control.Monad (mplus)
import Data.Maybe (fromMaybe)
import Data.Monoid
import Data.String (IsString(..))
import qualified Data.Text as T
import GHC.Generics (Generic)
import qualified Text.PrettyPrint as PJ
import Prelude ()
import Prelude.Compat
-- Name Displaying -------------------------------------------------------------
-- | How to display names, inspired by the GHC `Outputable` module. Getting a
@ -201,9 +203,16 @@ liftPJ2 f (Doc a) (Doc b) = Doc (\e -> f (a e) (b e))
liftSep :: ([PJ.Doc] -> PJ.Doc) -> ([Doc] -> Doc)
liftSep f ds = Doc (\e -> f [ d e | Doc d <- ds ])
infixl 6 <>, <+>
(<>) :: Doc -> Doc -> Doc
(<>) = liftPJ2 (PJ.<>)
(<+>) :: Doc -> Doc -> Doc
(<+>) = liftPJ2 (PJ.<+>)
infixl 5 $$
($$) :: Doc -> Doc -> Doc
($$) = liftPJ2 (PJ.$$)

4
tests/issues/issue093.icry.stdout
View File

@ -2,9 +2,9 @@ Loading module Cryptol
Loading module Cryptol
Loading module Main
property f0 Using exhaustive testing.
FAILED
testing...FAILED
property t0 Using exhaustive testing.
passed 1 tests.
testing...passed 1 tests.
Q.E.D.
property t1 Using random testing.
testing...passed 100 tests.

2
tests/issues/issue094.icry.stdout
View File

@ -3,5 +3,5 @@ Using random testing.
testing...passed 100 tests.
Coverage: 39.06% (100 of 256 values)
Using exhaustive testing.
passed 256 tests.
testing...passed 256 tests.
Q.E.D.

2
tests/issues/issue103.icry.stdout
View File

@ -2,6 +2,6 @@ Loading module Cryptol
Run-time error: undefined
Using exhaustive testing.
ERROR for the following inputs:
testing...ERROR for the following inputs:
()
invalid sequence index: 1

2
tests/issues/issue128.icry.stdout
View File

@ -2,6 +2,6 @@ Loading module Cryptol
Loading module Cryptol
Loading module Main
Using exhaustive testing.
passed 1 tests.
testing...passed 1 tests.
Q.E.D.
Q.E.D.

2
tests/issues/issue130.icry.stdout
View File

@ -2,6 +2,6 @@ Loading module Cryptol
Loading module Cryptol
Loading module Main
Using exhaustive testing.
passed 8 tests.
testing...passed 8 tests.
Q.E.D.
Q.E.D.

2
tests/issues/issue133.icry.stdout
View File

@ -2,6 +2,6 @@ Loading module Cryptol
Loading module Cryptol
Loading module Main
Using exhaustive testing.
passed 256 tests.
testing...passed 256 tests.
Q.E.D.
Q.E.D.