diff --git a/CHANGES.md b/CHANGES.md --- a/CHANGES.md +++ b/CHANGES.md @@ -1,3 +1,17 @@ +# 2.9.1 + +## Language changes + +* The type of `generate` which is used for `a@i` sequence definitions, + is generalized so that the index type can be any `Integral` type + large enough to index the entire array being defined. + +## Bug Fixes + +* Closed issues #848, #850, #851, #859, and #861. + +* Fixed Windows installer paths. + # 2.9.0 ## Language changes @@ -18,14 +32,14 @@ The new `Field` class contains types representing mathematical fields (or types that are approximately fields). It is currently inhabited by the new `Rational` type, and the `Float` - family of types. It will eventually also contain the + family of types. It will eventually also contain the `Real` type. It has the operation `recip` for reciprocal and `(/.)` for field division (not to be confused for `(/)`, which is Euclidean integral division). There is also a new `Round` class for types that can sensibly be rounded to integers. This class has the methods `floor`, `ceiling`, - `trunc`, `roundToEven` and `roundAway` for performing different + `trunc`, `roundToEven` and `roundAway` for performing different kinds of integer rounding. `Rational` and `Float` inhabit `Round`. The type of `(^^)` is modified to be @@ -33,7 +47,7 @@ that the semantics are iterated multiplication, which makes sense in any ring. - Finally, the `lg2`, `(/$)` and `(%$)` methods of Arith have + Finally, the `lg2`, `(/$)` and `(%$)` methods of `Arith` have had their types specialized so they operate only on bitvectors. * Added an `Eq` class, and moved the equality operations @@ -119,8 +133,9 @@ ## Bug fixes -* Closed issues #346, #444, #614, #617, #636, #660, #662, #663, #664, #667, #670, - #702, #711, #712, #716, #723, #725, #731 +* Closed issues #346, #444, #614, #617, #636, #660, #662, #663, #664, + #667, #670, #702, #711, #712, #716, #723, #725, #731, #835, #836, + #839, #840, and #845 # 2.8.0 (September 4, 2019) diff --git a/cryptol.cabal b/cryptol.cabal --- a/cryptol.cabal +++ b/cryptol.cabal @@ -1,5 +1,5 @@ Name: cryptol -Version: 2.9.0 +Version: 2.9.1 Synopsis: Cryptol: The Language of Cryptography Description: Cryptol is a domain-specific language for specifying cryptographic algorithms. A Cryptol implementation of an algorithm resembles its mathematical specification more closely than an implementation in a general purpose language. For more, see . License: BSD3 @@ -25,7 +25,7 @@ source-repository this type: git location: https://github.com/GaloisInc/cryptol.git - tag: 2.9.0 + tag: 2.9.1 flag static default: False diff --git a/cryptol/Main.hs b/cryptol/Main.hs --- a/cryptol/Main.hs +++ b/cryptol/Main.hs @@ -23,12 +23,10 @@ import REPL.Logo import Cryptol.Utils.PP -import Cryptol.Version (commitHash, commitBranch, commitDirty) -import Paths_cryptol (version) +import Cryptol.Version (displayVersion) import Control.Monad (when) import Data.Maybe (isJust) -import Data.Version (showVersion) import GHC.IO.Encoding (setLocaleEncoding, utf8) import System.Console.GetOpt (OptDescr(..),ArgOrder(..),ArgDescr(..),getOpt,usageInfo) @@ -169,16 +167,6 @@ (ps,[],[]) -> runOptParser defaultOptions (mconcat ps) (_,_,errs) -> Left errs -displayVersion :: IO () -displayVersion = do - let ver = showVersion version - putStrLn ("Cryptol " ++ ver) - putStrLn ("Git commit " ++ commitHash) - putStrLn (" branch " ++ commitBranch ++ dirtyLab) - where - dirtyLab | commitDirty = " (non-committed files present during build)" - | otherwise = "" - displayHelp :: [String] -> IO () displayHelp errs = do prog <- getProgName @@ -213,7 +201,7 @@ Right opts | optHelp opts -> displayHelp [] - | optVersion opts -> displayVersion + | optVersion opts -> displayVersion putStrLn | otherwise -> do (opts', mCleanup) <- setupCmdScript opts status <- repl (optCryptolrc opts') diff --git a/lib/Cryptol.cry b/lib/Cryptol.cry --- a/lib/Cryptol.cry +++ b/lib/Cryptol.cry @@ -874,7 +874,7 @@ * Declarations of the form 'x @ i = e' are syntactic sugar for * 'x = generate (\i -> e)'. */ -generate : {n, a} (fin n, n >= 1) => (Integer -> a) -> [n]a +generate : {n, a, ix} (fin n, n >= 1, Integral ix, Literal (n-1) ix) => (ix -> a) -> [n]a generate f = [ f i | i <- [0 .. n-1] ] diff --git a/src/Cryptol/Eval.hs b/src/Cryptol/Eval.hs --- a/src/Cryptol/Eval.hs +++ b/src/Cryptol/Eval.hs @@ -397,34 +397,47 @@ k -> panic "[Eval] etaDelay" ["invalid kind on type abstraction", show k] go tp x | isReady sym x = x >>= \case - VBit _ -> x - VInteger _ -> x - VWord _ _ -> x - VSeq n xs - | TVSeq _nt el <- tp - -> return $ VSeq n $ IndexSeqMap $ \i -> go el (lookupSeqMap xs i) + VBit{} -> x + VInteger{} -> x + VWord{} -> x + VRational{} -> x + VFloat{} -> x + VSeq n xs -> + case tp of + TVSeq _nt el -> return $ VSeq n $ IndexSeqMap $ \i -> go el (lookupSeqMap xs i) + _ -> evalPanic "type mismatch during eta-expansion" ["Expected sequence type, but got " ++ show tp] - VStream xs - | TVStream el <- tp - -> return $ VStream $ IndexSeqMap $ \i -> go el (lookupSeqMap xs i) + VStream xs -> + case tp of + TVStream el -> return $ VStream $ IndexSeqMap $ \i -> go el (lookupSeqMap xs i) + _ -> evalPanic "type mismatch during eta-expansion" ["Expected stream type, but got " ++ show tp] - VTuple xs - | TVTuple ts <- tp - -> return $ VTuple (zipWith go ts xs) + VTuple xs -> + case tp of + TVTuple ts | length ts == length xs -> return $ VTuple (zipWith go ts xs) + _ -> evalPanic "type mismatch during eta-expansion" ["Expected tuple type with " ++ show (length xs) + ++ " elements, but got " ++ show tp] - VRecord fs - | TVRec fts <- tp - -> do let res = zipRecords (\_ v t -> go t v) fs fts - case res of - Left (Left f) -> evalPanic "type mismatch during eta-expansion" ["missing field " ++ show f] - Left (Right f) -> evalPanic "type mismatch during eta-expansion" ["unexpected field " ++ show f] - Right fs' -> return (VRecord fs') + VRecord fs -> + case tp of + TVRec fts -> + do let res = zipRecords (\_ v t -> go t v) fs fts + case res of + Left (Left f) -> evalPanic "type mismatch during eta-expansion" ["missing field " ++ show f] + Left (Right f) -> evalPanic "type mismatch during eta-expansion" ["unexpected field " ++ show f] + Right fs' -> return (VRecord fs') + _ -> evalPanic "type mismatch during eta-expansion" ["Expected record type, but got " ++ show tp] - VFun f - | TVFun _t1 t2 <- tp - -> return $ VFun $ \a -> go t2 (f a) + VFun f -> + case tp of + TVFun _t1 t2 -> return $ VFun $ \a -> go t2 (f a) + _ -> evalPanic "type mismatch during eta-expansion" ["Expected function type but got " ++ show tp] - _ -> evalPanic "type mismatch during eta-expansion" [] + VPoly{} -> + evalPanic "type mismatch during eta-expansion" ["Encountered polymorphic value"] + + VNumPoly{} -> + evalPanic "type mismatch during eta-expansion" ["Encountered numeric polymorphic value"] go tp v = case tp of diff --git a/src/Cryptol/Eval/Concrete.hs b/src/Cryptol/Eval/Concrete.hs --- a/src/Cryptol/Eval/Concrete.hs +++ b/src/Cryptol/Eval/Concrete.hs @@ -24,7 +24,7 @@ , toExpr ) where -import Control.Monad (join,guard,zipWithM,mzero) +import Control.Monad (join, guard, zipWithM) import Data.Bits (Bits(..)) import Data.Ratio(numerator,denominator) import MonadLib( ChoiceT, findOne, lift ) @@ -55,8 +55,6 @@ -- | Given an expected type, returns an expression that evaluates to -- this value, if we can determine it. --- --- XXX: View patterns would probably clean up this definition a lot. toExpr :: PrimMap -> AST.Type -> Value -> Eval (Maybe AST.Expr) toExpr prims t0 v0 = findOne (go t0 v0) where @@ -65,45 +63,47 @@ go :: AST.Type -> Value -> ChoiceT Eval Expr - go ty val = case (tNoUser ty, val) of - (TRec tfs, VRecord vfs) -> do - -- NB, vfs first argument to keep their display order - res <- zipRecordsM (\_lbl v t -> go t =<< lift v) vfs tfs - case res of - Left _ -> mzero -- different fields - Right efs -> pure (ERec efs) - (TCon (TC (TCTuple tl)) ts, VTuple tvs) -> do - guard (tl == (length tvs)) - ETuple `fmap` (zipWithM go ts =<< lift (sequence tvs)) - (TCon (TC TCBit) [], VBit True ) -> return (prim "True") - (TCon (TC TCBit) [], VBit False) -> return (prim "False") - (TCon (TC TCInteger) [], VInteger i) -> - return $ ETApp (ETApp (prim "number") (tNum i)) ty - (TCon (TC TCIntMod) [_n], VInteger i) -> - return $ ETApp (ETApp (prim "number") (tNum i)) ty - (TCon (TC TCRational) [], VRational (SRational n d)) -> - do let n' = ETApp (ETApp (prim "number") (tNum n)) (TCon (TC TCInteger) []) - d' = ETApp (ETApp (prim "number") (tNum d)) (TCon (TC TCInteger) []) - return $ EApp (EApp (prim "ratio") n') d' - (TCon (TC TCFloat) [eT,pT], VFloat i) -> - pure (floatToExpr prims eT pT (bfValue i)) - - (TCon (TC TCSeq) [a,b], VSeq 0 _) -> do - guard (a == tZero) - return $ EList [] b - (TCon (TC TCSeq) [a,b], VSeq n svs) -> do - guard (a == tNum n) - ses <- mapM (go b) =<< lift (sequence (enumerateSeqMap n svs)) - return $ EList ses b - (TCon (TC TCSeq) [a,(TCon (TC TCBit) [])], VWord _ wval) -> do - BV w v <- lift (asWordVal Concrete =<< wval) - guard (a == tNum w) - return $ ETApp (ETApp (prim "number") (tNum v)) ty - (_, VStream _) -> fail "cannot construct infinite expressions" - (_, VFun _) -> fail "cannot convert function values to expressions" - (_, VPoly _) -> fail "cannot convert polymorphic values to expressions" - _ -> do doc <- lift (ppValue Concrete defaultPPOpts val) - panic "Cryptol.Eval.Concrete.toExpr" + go ty val = + case val of + VRecord vfs -> + do tfs <- maybe mismatch pure (tIsRec ty) + -- NB, vfs first argument to keep their display order + res <- zipRecordsM (\_lbl v t -> go t =<< lift v) vfs tfs + case res of + Left _ -> mismatch -- different fields + Right efs -> pure (ERec efs) + VTuple tvs -> + do ts <- maybe mismatch pure (tIsTuple ty) + guard (length ts == length tvs) + ETuple <$> (zipWithM go ts =<< lift (sequence tvs)) + VBit b -> + pure (prim (if b then "True" else "False")) + VInteger i -> + -- This works uniformly for values of type Integer or Z n + pure $ ETApp (ETApp (prim "number") (tNum i)) ty + VRational (SRational n d) -> + do let n' = ETApp (ETApp (prim "number") (tNum n)) tInteger + let d' = ETApp (ETApp (prim "number") (tNum d)) tInteger + pure $ EApp (EApp (prim "ratio") n') d' + VFloat i -> + do (eT, pT) <- maybe mismatch pure (tIsFloat ty) + pure (floatToExpr prims eT pT (bfValue i)) + VSeq n svs -> + do (_a, b) <- maybe mismatch pure (tIsSeq ty) + ses <- traverse (go b) =<< lift (sequence (enumerateSeqMap n svs)) + pure $ EList ses b + VWord _ wval -> + do BV _ v <- lift (asWordVal Concrete =<< wval) + pure $ ETApp (ETApp (prim "number") (tNum v)) ty + VStream _ -> fail "cannot construct infinite expressions" + VFun _ -> fail "cannot convert function values to expressions" + VPoly _ -> fail "cannot convert polymorphic values to expressions" + VNumPoly _ -> fail "cannot convert polymorphic values to expressions" + where + mismatch :: forall a. ChoiceT Eval a + mismatch = + do doc <- lift (ppValue Concrete defaultPPOpts val) + panic "Cryptol.Eval.Concrete.toExpr" ["type mismatch:" , pretty ty , render doc diff --git a/src/Cryptol/Eval/Generic.hs b/src/Cryptol/Eval/Generic.hs --- a/src/Cryptol/Eval/Generic.hs +++ b/src/Cryptol/Eval/Generic.hs @@ -1407,10 +1407,23 @@ Either (SInteger sym) (WordValue sym) {- ^ Index value -} -> SEval sym () --- Can't index out of bounds for an infinite sequence -assertIndexInBounds _sym Inf _ = - return () +-- All nonnegative integers are in bounds for an infinite sequence +assertIndexInBounds sym Inf (Left idx) = + do ppos <- bitComplement sym =<< intLessThan sym idx =<< integerLit sym 0 + assertSideCondition sym ppos (InvalidIndex (integerAsLit sym idx)) +-- If the index is an integer, test that it +-- is nonnegative and less than the concrete value of n. +assertIndexInBounds sym (Nat n) (Left idx) = + do n' <- integerLit sym n + ppos <- bitComplement sym =<< intLessThan sym idx =<< integerLit sym 0 + pn <- intLessThan sym idx n' + p <- bitAnd sym ppos pn + assertSideCondition sym p (InvalidIndex (integerAsLit sym idx)) + +-- Bitvectors can't index out of bounds for an infinite sequence +assertIndexInBounds _sym Inf (Right _) = return () + -- Can't index out of bounds for a sequence that is -- longer than the expressible index values assertIndexInBounds sym (Nat n) (Right idx) @@ -1418,21 +1431,9 @@ = return () -- If the index is concrete, test it directly -assertIndexInBounds sym (Nat n) (Left idx) - | Just i <- integerAsLit sym idx - = unless (i < n) (raiseError sym (InvalidIndex (Just i))) - --- If the index is concrete, test it directly assertIndexInBounds sym (Nat n) (Right (WordVal idx)) | Just (_w,i) <- wordAsLit sym idx = unless (i < n) (raiseError sym (InvalidIndex (Just i))) - --- If the index is an integer, test that it --- is less than the concrete value of n. -assertIndexInBounds sym (Nat n) (Left idx) = - do n' <- integerLit sym n - p <- intLessThan sym idx n' - assertSideCondition sym p (InvalidIndex Nothing) -- If the index is a packed word, test that it -- is less than the concrete value of n, which diff --git a/src/Cryptol/Eval/Value.hs b/src/Cryptol/Eval/Value.hs --- a/src/Cryptol/Eval/Value.hs +++ b/src/Cryptol/Eval/Value.hs @@ -272,21 +272,21 @@ -- | Select an individual bit from a word value indexWordValue :: Backend sym => sym -> WordValue sym -> Integer -> SEval sym (SBit sym) indexWordValue sym (WordVal w) idx - | idx < wordLen sym w = wordBit sym w idx + | 0 <= idx && idx < wordLen sym w = wordBit sym w idx | otherwise = invalidIndex sym idx indexWordValue sym (LargeBitsVal n xs) idx - | idx < n = fromVBit <$> lookupSeqMap xs idx + | 0 <= idx && idx < n = fromVBit <$> lookupSeqMap xs idx | otherwise = invalidIndex sym idx -- | Produce a new 'WordValue' from the one given by updating the @i@th bit with the -- given bit value. updateWordValue :: Backend sym => sym -> WordValue sym -> Integer -> SEval sym (SBit sym) -> SEval sym (WordValue sym) updateWordValue sym (WordVal w) idx b - | idx >= wordLen sym w = invalidIndex sym idx + | idx < 0 || idx >= wordLen sym w = invalidIndex sym idx | isReady sym b = WordVal <$> (wordUpdate sym w idx =<< b) updateWordValue sym wv idx b - | idx < wordValueSize sym wv = + | 0 <= idx && idx < wordValueSize sym wv = pure $ LargeBitsVal (wordValueSize sym wv) $ updateSeqMap (asBitsMap sym wv) idx (VBit <$> b) | otherwise = invalidIndex sym idx diff --git a/src/Cryptol/Parser/Unlit.hs b/src/Cryptol/Parser/Unlit.hs --- a/src/Cryptol/Parser/Unlit.hs +++ b/src/Cryptol/Parser/Unlit.hs @@ -78,6 +78,7 @@ where comment current [] = mk Comment current comment current (l : ls) + | Just op <- isOpenFence l = mk Comment (l : current) ++ fenced op [] ls | isBlank l = blanks (l : current) ls | otherwise = comment (l : current) ls diff --git a/src/Cryptol/REPL/Command.hs b/src/Cryptol/REPL/Command.hs --- a/src/Cryptol/REPL/Command.hs +++ b/src/Cryptol/REPL/Command.hs @@ -88,6 +88,7 @@ ) import qualified Cryptol.Symbolic.SBV as SBV import qualified Cryptol.Symbolic.What4 as W4 +import Cryptol.Version (displayVersion) import qualified Control.Exception as X import Control.Monad hiding (mapM, mapM) @@ -194,6 +195,9 @@ , CommandDescr [ ":b", ":browse" ] ["[ MODULE ]"] (ModNameArg browseCmd) "Display environment for all loaded modules, or for a specific module." "" + , CommandDescr [ ":version"] [] (NoArg versionCmd) + "Display the version of this Cryptol executable" + "" , CommandDescr [ ":?", ":help" ] ["[ TOPIC ]"] (HelpArg helpCmd) "Display a brief description of a function, type, or command. (e.g. :help :help)" (unlines @@ -1068,9 +1072,11 @@ M.InMem {} -> clearEditPath setDynEnv mempty +versionCmd :: REPL () +versionCmd = displayVersion rPutStrLn + quitCmd :: REPL () quitCmd = stop - browseCmd :: String -> REPL () browseCmd input = do diff --git a/src/Cryptol/TypeCheck/Type.hs b/src/Cryptol/TypeCheck/Type.hs --- a/src/Cryptol/TypeCheck/Type.hs +++ b/src/Cryptol/TypeCheck/Type.hs @@ -393,6 +393,18 @@ TCon (TC TCIntMod) [n] -> Just n _ -> Nothing +tIsRational :: Type -> Bool +tIsRational ty = + case tNoUser ty of + TCon (TC TCRational) [] -> True + _ -> False + +tIsFloat :: Type -> Maybe (Type, Type) +tIsFloat ty = + case tNoUser ty of + TCon (TC TCFloat) [e, p] -> Just (e, p) + _ -> Nothing + tIsTuple :: Type -> Maybe [Type] tIsTuple ty = case tNoUser ty of TCon (TC (TCTuple _)) ts -> Just ts diff --git a/src/Cryptol/Version.hs b/src/Cryptol/Version.hs --- a/src/Cryptol/Version.hs +++ b/src/Cryptol/Version.hs @@ -14,10 +14,12 @@ , commitBranch , commitDirty , version + , displayVersion ) where import Paths_cryptol import qualified GitRev +import Data.Version (showVersion) commitHash :: String commitHash = GitRev.hash @@ -30,3 +32,13 @@ commitDirty :: Bool commitDirty = GitRev.dirty + +displayVersion :: Monad m => (String -> m ()) -> m () +displayVersion putLn = do + let ver = showVersion version + putLn ("Cryptol " ++ ver) + putLn ("Git commit " ++ commitHash) + putLn (" branch " ++ commitBranch ++ dirtyLab) + where + dirtyLab | commitDirty = " (non-committed files present during build)" + | otherwise = ""