diff --git a/src/Cryptol/Prims/Eval.hs b/src/Cryptol/Prims/Eval.hs index 4f957e99..bf40c76d 100644 --- a/src/Cryptol/Prims/Eval.hs +++ b/src/Cryptol/Prims/Eval.hs @@ -1271,7 +1271,7 @@ infFromThenV = -- | Produce a random value with the given seed. If we do not support -- making values of the given type, return zero of that type. -- TODO: do better than returning zero -randomV :: TValue -> Integer -> Value +randomV :: BitWord b w => TValue -> Integer -> GenValue b w randomV ty seed = case randomValue (tValTy ty) of Nothing -> zeroV ty diff --git a/src/Cryptol/Symbolic/Prims.hs b/src/Cryptol/Symbolic/Prims.hs index 3c090c4f..88fa7533 100644 --- a/src/Cryptol/Symbolic/Prims.hs +++ b/src/Cryptol/Symbolic/Prims.hs @@ -25,7 +25,7 @@ import Data.Ord (comparing) import qualified Data.Sequence as Seq import qualified Data.Foldable as Fold -import Cryptol.Eval.Monad (Eval(..), ready, invalidIndex) +import Cryptol.Eval.Monad (Eval(..), ready, invalidIndex, cryUserError) import Cryptol.Eval.Type (finNat', TValue(..)) import Cryptol.Eval.Value (BitWord(..), EvalPrims(..), enumerateSeqMap, SeqMap(..), reverseSeqMap, wlam, nlam, WordValue(..), @@ -38,7 +38,7 @@ import Cryptol.Prims.Eval (binary, unary, arithUnary, reverseV, infFromV, infFromThenV, fromThenV, fromToV, fromThenToV, transposeV, indexPrimOne, indexPrimMany, - ecDemoteV, updatePrim) + ecDemoteV, updatePrim, randomV) import Cryptol.Symbolic.Value import Cryptol.TypeCheck.AST (Decl(..)) import Cryptol.TypeCheck.Solver.InfNat(Nat'(..)) @@ -209,11 +209,11 @@ primTable = Map.fromList $ map (\(n, v) -> (mkIdent (T.pack n), v)) return $ zeroV at) -- error/undefined, is arbitrarily translated to 0 , ("random" , - tlam $ \_a -> - wlam $ \_x -> - Thunk $ return $ panic - "Cryptol.Symbolic.Prims.evalECon" - [ "can't symbolically evaluate ECRandom" ]) + tlam $ \a -> + wlam $ \x -> + case SBV.svAsInteger x of + Just i -> return $ randomV a i + Nothing -> cryUserError "cannot evaluatate 'random' with symbolic inputs") -- The trace function simply forces its first two -- values before returing the third in the symbolic diff --git a/src/Cryptol/Testing/Random.hs b/src/Cryptol/Testing/Random.hs index 8b338801..e4d018c3 100644 --- a/src/Cryptol/Testing/Random.hs +++ b/src/Cryptol/Testing/Random.hs @@ -12,7 +12,7 @@ module Cryptol.Testing.Random where import Cryptol.Eval.Monad (ready) -import Cryptol.Eval.Value (BV(..),Value,GenValue(..),SeqMap(..), WordValue(..)) +import Cryptol.Eval.Value (BV(..),Value,GenValue(..),SeqMap(..), WordValue(..), BitWord(..)) import qualified Cryptol.Testing.Concrete as Conc import Cryptol.TypeCheck.AST (Type(..),TCon(..),TC(..),tNoUser) import Cryptol.TypeCheck.SimpType(tRebuild') @@ -24,7 +24,7 @@ import Data.List (unfoldr, genericTake, genericIndex) import System.Random (RandomGen, split, random, randomR) import qualified Data.Sequence as Seq -type Gen g = Integer -> g -> (Value, g) +type Gen g b w = Integer -> g -> (GenValue b w, g) {- | Apply a testable value to some randomly-generated arguments. @@ -36,7 +36,7 @@ type Gen g = Integer -> g -> (Value, g) -} runOneTest :: RandomGen g => Value -- ^ Function under test - -> [Gen g] -- ^ Argument generators + -> [Gen g Bool BV] -- ^ Argument generators -> Integer -- ^ Size -> g -> IO (Conc.TestResult, g) @@ -49,7 +49,7 @@ runOneTest fun argGens sz g0 = do {- | Given a (function) type, compute generators for the function's arguments. Currently we do not support polymorphic functions. In principle, we could apply these to random types, and test the results. -} -testableType :: RandomGen g => Type -> Maybe [Gen g] +testableType :: RandomGen g => Type -> Maybe [Gen g Bool BV] testableType ty = case tNoUser ty of TCon (TC TCFun) [t1,t2] -> @@ -62,7 +62,7 @@ testableType ty = {- | A generator for values of the given type. This fails if we are given a type that lacks a suitable random value generator. -} -randomValue :: RandomGen g => Type -> Maybe (Gen g) +randomValue :: (BitWord b w, RandomGen g) => Type -> Maybe (Gen g b w) randomValue ty = case ty of TCon tc ts -> @@ -93,28 +93,28 @@ randomValue ty = return (randomRecord gs) -- | Generate a random bit value. -randomBit :: RandomGen g => Gen g +randomBit :: (BitWord b w, RandomGen g) => Gen g b w randomBit _ g = let (b,g1) = random g - in (VBit b, g1) + in (VBit (bitLit b), g1) -- | Generate a random word of the given length (i.e., a value of type @[w]@) -- The size parameter is assumed to vary between 1 and 100, and we use -- it to generate smaller numbers first. -randomWord :: RandomGen g => Integer -> Gen g +randomWord :: (BitWord b w, RandomGen g) => Integer -> Gen g b w randomWord w _sz g = let (val, g1) = randomR (0,2^w-1) g - in (VWord w (ready (WordVal (BV w val))), g1) + in (VWord w (ready (WordVal (wordLit w val))), g1) -- | Generate a random infinite stream value. -randomStream :: RandomGen g => Gen g -> Gen g +randomStream :: RandomGen g => Gen g b w -> Gen g b w randomStream mkElem sz g = let (g1,g2) = split g in (VStream $ IndexSeqMap $ genericIndex (map ready (unfoldr (Just . mkElem sz) g1)), g2) {- | Generate a random sequence. This should be used for sequences other than bits. For sequences of bits use "randomWord". -} -randomSequence :: RandomGen g => Integer -> Gen g -> Gen g +randomSequence :: RandomGen g => Integer -> Gen g b w -> Gen g b w randomSequence w mkElem sz g0 = do let (g1,g2) = split g0 let f g = let (x,g') = mkElem sz g @@ -123,7 +123,7 @@ randomSequence w mkElem sz g0 = do seq xs (VSeq w $ IndexSeqMap $ (Seq.index xs . fromInteger), g2) -- | Generate a random tuple value. -randomTuple :: RandomGen g => [Gen g] -> Gen g +randomTuple :: RandomGen g => [Gen g b w] -> Gen g b w randomTuple gens sz = go [] gens where go els [] g = (VTuple (reverse els), g) @@ -132,7 +132,7 @@ randomTuple gens sz = go [] gens in seq v (go (ready v : els) more g1) -- | Generate a random record value. -randomRecord :: RandomGen g => [(Ident, Gen g)] -> Gen g +randomRecord :: RandomGen g => [(Ident, Gen g b w)] -> Gen g b w randomRecord gens sz = go [] gens where go els [] g = (VRecord (reverse els), g) diff --git a/tests/issues/issue364.cry b/tests/issues/issue364.cry new file mode 100644 index 00000000..041e6711 --- /dev/null +++ b/tests/issues/issue364.cry @@ -0,0 +1,11 @@ +x : [64] +x = random 123 + +x_val : [64] +x_val = 0x80b483887be1a6e5 + +property x_eval = x == x_val +property x_distinct = ~ (x == zero) + +property moderately_bogus_property (seed:[8]) = + ~(random (zero#seed) == (0:[64])) diff --git a/tests/issues/issue364.icry b/tests/issues/issue364.icry new file mode 100644 index 00000000..7900bc12 --- /dev/null +++ b/tests/issues/issue364.icry @@ -0,0 +1,5 @@ +:set prover-stats=off +:l issue364.cry +:check +:exhaust +:prove diff --git a/tests/issues/issue364.icry.stdout b/tests/issues/issue364.icry.stdout new file mode 100644 index 00000000..96a610dd --- /dev/null +++ b/tests/issues/issue364.icry.stdout @@ -0,0 +1,28 @@ +Loading module Cryptol +Loading module Cryptol +Loading module Main +property x_eval Using exhaustive testing. +testing...passed 1 tests. +Q.E.D. +property x_distinct Using exhaustive testing. +testing...passed 1 tests. +Q.E.D. +property moderately_bogus_property Using random testing. +testing...passed 100 tests. +Coverage: 39.06% (100 of 256 values) +property x_eval Using exhaustive testing. +testing...passed 1 tests. +Q.E.D. +property x_distinct Using exhaustive testing. +testing...passed 1 tests. +Q.E.D. +property moderately_bogus_property Using exhaustive testing. +testing...passed 256 tests. +Q.E.D. +:prove x_eval + Q.E.D. +:prove x_distinct + Q.E.D. +:prove moderately_bogus_property + +Run-time error: cannot evaluatate 'random' with symbolic inputs