diff --git a/CHANGES.md b/CHANGES.md --- a/CHANGES.md +++ b/CHANGES.md @@ -1,3 +1,91 @@ +# 3.3.0 -- 2025-03-21 + +## Language changes + +## Bug fixes + +* Fix a bug where setting at timeout would cause + sbv-yices, sbv-cvc4 and sbc-cvc5 to crash. + Uses a deadman timer workaround for yices, due + to a [known issue](https://github.com/LeventErkok/sbv/issues/735). + ([#1808](https://github.com/GaloisInc/cryptol/issues/1808)) + +* Update Yices build in CI to fix a crash when running + test `issue_1807.icry` on Mac OS X (ARM64). + ([what4-solvers #58](https://github.com/GaloisInc/what4-solvers/issues/58)) + +* Fix a bug where using a timeout with a subset of the what4 solvers + would cause a runtime error. Includes a version bump for what4 to address + a nondeterministic crash when using timeouts with cvc4/5. + ([what4 PR #288](https://github.com/GaloisInc/what4/pull/288)) + ([#1807](https://github.com/GaloisInc/cryptol/issues/1807)) + +* Fix #1437, enforce the VSeq invariant that it is not a sequence of bits. + Replaces the VSeq constructor with a view-only pattern, and smart constructors + `mkSeq` and `finSeq`. + ([#1437](https://github.com/GaloisInc/cryptol/issues/1437)) + +* Fix #1740, removes duplicated width from word values. + Note that since this changes the types, it may require changes to libraries + depending on Cryptol. + +* Fix a bug in which splitting a `[0]` value into type `[inf][0]` would panic. + ([#1749](https://github.com/GaloisInc/cryptol/issues/1749)) + +* Fix a bug in which the free variables of types mentioning newtypes or enums + were incorrectly computed. + ([#1773](https://github.com/GaloisInc/cryptol/issues/1773)) + +* The reference evaluator now evaluates the `toSignedInteger` and `deepseq` + primitives instead of panicking. + +* Fix a bug in which `a ^^ (x ^^ y)` could be incorrectly simplified to + `a ^^ (x * y)` at the type level. + ([#1799](https://github.com/GaloisInc/cryptol/issues/1799)) + +## New features + +* Improved error messages during type inference for bindings. + Adds a specific error message for when a binding has + more arguments than expected, given its type signature. + ([#1744](https://github.com/GaloisInc/cryptol/issues/1744)) + +* Improved warning messages for non-exhaustive guards. + Warnings are now ordered by source location. + ([#1798](https://github.com/GaloisInc/cryptol/issues/1798)) + +* More aggressive exhaustivity check that is less dependent on + guard ordering. + ([#1796](https://github.com/GaloisInc/cryptol/issues/1796)) + +* Improved error messages mentioning module parameters + ([#1560](https://github.com/GaloisInc/cryptol/issues/1560)) + +* Improved the naming convention for anonymous modules generated by the + module system ([#1810](https://github.com/GaloisInc/cryptol/issues/1810)) + +* REPL command `:dumptests ` updated to write to stdout when + invoked as `:dumptests - ` allowing for easier experimentation and + testing. + +* The REPL properly supports tab completion for the `:t` and `:check` commands. + ([#1780](https://github.com/GaloisInc/cryptol/issues/1780)) + +* Add support for incrementally loading projects via cryptol's `--project` + flag as documented in the reference manual. + ([#1641](https://github.com/GaloisInc/cryptol/issues/1641)) + +* Add support for the Bitwuzla SMT solver, which can be selected with + `:set prover=bitwuzla`. If you want to specify a What4 or SBV backend, you can + use `:set prover=w4-bitwuzla` or `:set prover=sbv-bitwuzla`, respectively. + ([#1786](https://github.com/GaloisInc/cryptol/issues/1786)) + +* Add a REPL option `tcSmtFile` that allows writing typechecker-related SMT + solver interactions to a file. + +* The typechecker can now simplify types of the form `width (2^^n)` to `n + 1`. + ([#1802](https://github.com/GaloisInc/cryptol/issues/1802)) + # 3.2.0 -- 2024-08-20 ## Language changes diff --git a/api-tests/Main.hs b/api-tests/Main.hs new file mode 100644 --- /dev/null +++ b/api-tests/Main.hs @@ -0,0 +1,114 @@ +{-# LANGUAGE ScopedTypeVariables #-} +module Main (main) where + +import Data.Foldable (traverse_) +import System.Console.Haskeline.Completion (Completion(..)) +import Test.Tasty +import Test.Tasty.HUnit + +import qualified Cryptol.REPL.Command as REPL +import qualified Cryptol.REPL.Monad as REPL +import Cryptol.REPL.Monad (REPL) +import Cryptol.Utils.Logger (quietLogger) +import Cryptol.Utils.PP (pp) + +import REPL.Haskeline (cryptolCommand) + +main :: IO () +main = defaultMain $ + testGroup "Cryptol API tests" + [ testGroup "Tab completion tests" $ + map (uncurry replTabCompletionTestCase) + [ (":ch", ":check") + , (":check", ":check") + , (":check ", ":check ") + , (":check rev", ":check reverse") + , (":check-docstrings", ":check-docstrings ") + , (":check-docstrings ", ":check-docstrings ") + , (":t", ":t") + , (":t rev", ":t reverse") + , (":time", ":time ") + , (":time ", ":time ") + , (":time rev", ":time reverse") + , (":type", ":type ") + , (":type ", ":type ") + , (":type rev", ":type reverse") + ] + ] + +-- | Assert a property in the 'REPL' monad and turn it into a test case. +replTestCase :: TestName -> REPL () -> TestTree +replTestCase name replAssertion = + testCase name $ + REPL.runREPL + False -- Don't use batch mode + False -- Disable call stacks + quietLogger -- Ignore all log messages + replAssertion + +-- | Assert that the REPL will tab-complete the given input in one specific way. +replTabCompletionTestCase :: + -- | The input before the cursor just prior to hitting the tab key. + String -> + -- | The expected terminal input after hitting the tab key. Note that although + -- this is specified as a single 'String', this may actually correspond to + -- multiple Haskeline 'Completion's under the hood. See the comments below for + -- details on how multiple 'Completion's are resolved to a single 'String'. + String -> + TestTree +replTabCompletionTestCase beforeTab afterTabExpected = + replTestCase (show beforeTab ++ " --> " ++ show afterTabExpected) $ + do -- Load the prelude so that the REPL knows how to tab-complete prelude + -- definitions. + REPL.loadPrelude + -- Perform the actual tab completion. (Oddly, Haskeline requires that the + -- input to the left of the cursor should be reversed.) + (_input, completions) <- cryptolCommand (reverse beforeTab, "") + -- Check that the results match what is expected. We have to do a bit of + -- additional work that Haskeline does not do: + -- + -- 1. If there is exactly one Completion and its replacement value is + -- empty, then Haskeline will add a space character to the end of the + -- input on the terminal. Oddly, this space character is /not/ added in + -- the Completion itself. As such, we have to add this ourselves. + -- + -- 2. If there are multiple completions, then Haskeline will complete the + -- terminal input up to the longest common prefix of all the + -- completions' replacement strings. As such, we compute this longest + -- common prefix ourselves. + REPL.io $ + case completions of + [] -> assertFailure "Expected tab completions, but received none" + [completion] -> + do assertFinished completion + let replace = replacement completion + afterTabActual + | null replace = -- See (1) above + beforeTab ++ " " + | otherwise = beforeTab ++ replace + afterTabExpected @=? afterTabActual + _:_ -> + do traverse_ assertFinished completions + let replaceLcp = + -- See (2) above + longestCommonPrefix (map replacement completions) + afterTabActual = beforeTab ++ replaceLcp + afterTabExpected @=? afterTabActual + `REPL.catch` + -- If something goes wrong run running the REPL, report it as a test + -- failure. + \x -> REPL.io $ assertFailure $ show $ pp x + where + assertFinished :: Completion -> Assertion + assertFinished completion = + assertBool ("Tab completion for " ++ display completion ++ " finished") + (isFinished completion) + +-- | Compute the longest common prefix in a list of lists. +longestCommonPrefix :: forall a. Eq a => [[a]] -> [a] +longestCommonPrefix [] = [] +longestCommonPrefix s = foldr1 lcp s + where + lcp :: [a] -> [a] -> [a] + lcp xs ys = map fst $ takeWhile (uncurry (==)) + $ zip xs ys diff --git a/cryptol-repl-internal/REPL/Haskeline.hs b/cryptol-repl-internal/REPL/Haskeline.hs new file mode 100644 --- /dev/null +++ b/cryptol-repl-internal/REPL/Haskeline.hs @@ -0,0 +1,401 @@ +-- | +-- Module : REPL.Haskeline +-- Copyright : (c) 2013-2016 Galois, Inc. +-- License : BSD3 +-- Maintainer : cryptol@galois.com +-- Stability : provisional +-- Portability : portable + +{-# LANGUAGE CPP #-} +{-# LANGUAGE MultiWayIf #-} +{-# LANGUAGE PatternGuards #-} +{-# LANGUAGE BangPatterns #-} +{-# OPTIONS_GHC -fno-warn-orphans #-} + +module REPL.Haskeline where + +import qualified Cryptol.Project as Project +import Cryptol.REPL.Command +import Cryptol.REPL.Monad +import Cryptol.REPL.Trie +import Cryptol.Utils.PP hiding (()) +import Cryptol.Utils.Logger(stdoutLogger) +import Cryptol.Utils.Ident(modNameToText, interactiveName) + +import qualified Control.Exception as X +import Control.Monad (guard, join) +import qualified Control.Monad.Trans.Class as MTL +#if !MIN_VERSION_haskeline(0,8,0) +import Control.Monad.Trans.Control +#endif +import Data.Char (isAlphaNum, isSpace) +import Data.Function (on) +import Data.List (isPrefixOf,nub,sortBy,sort) +import qualified Data.Set as Set +import qualified Data.Text as T (unpack) +import System.Console.ANSI (setTitle, hSupportsANSI) +import System.Console.Haskeline +import System.Directory ( doesFileExist + , getHomeDirectory + , getCurrentDirectory) +import System.FilePath (()) +import System.IO (stdout) + +import Prelude () +import Prelude.Compat +import Cryptol.Project.Monad (LoadProjectMode) + + +data ReplMode + = InteractiveRepl -- ^ Interactive terminal session + | Batch FilePath -- ^ Execute from a batch file + | InteractiveBatch FilePath + -- ^ Execute from a batch file, but behave as though + -- lines are entered in an interactive session. + deriving (Show, Eq) + +-- | One REPL invocation, either from a file or from the terminal. +crySession :: ReplMode -> Bool -> REPL CommandResult +crySession replMode stopOnError = + do settings <- io (setHistoryFile (replSettings isBatch)) + let act = runInputTBehavior behavior settings (withInterrupt (loop True 1)) + if isBatch then asBatch act else act + where + (isBatch,behavior) = case replMode of + InteractiveRepl -> (False, defaultBehavior) + Batch path -> (True, useFile path) + InteractiveBatch path -> (False, useFile path) + + loop :: Bool -> Int -> InputT REPL CommandResult + loop !success !lineNum = + do ln <- getInputLines =<< MTL.lift getPrompt + case ln of + NoMoreLines -> return emptyCommandResult { crSuccess = success } + Interrupted + | isBatch && stopOnError -> return emptyCommandResult { crSuccess = False } + | otherwise -> loop success lineNum + NextLine ls + | all (all isSpace) ls -> loop success (lineNum + length ls) + | otherwise -> doCommand success lineNum ls + + run lineNum cmd = + case replMode of + InteractiveRepl -> runCommand lineNum Nothing cmd + InteractiveBatch _ -> runCommand lineNum Nothing cmd + Batch path -> runCommand lineNum (Just path) cmd + + doCommand success lineNum txt = + case parseCommand findCommandExact (unlines txt) of + Nothing | isBatch && stopOnError -> return emptyCommandResult { crSuccess = False } + | otherwise -> loop False (lineNum + length txt) -- say somtething? + Just cmd -> join $ MTL.lift $ + do status <- handleInterrupt (handleCtrlC emptyCommandResult { crSuccess = False }) (run lineNum cmd) + case crSuccess status of + False | isBatch && stopOnError -> return (return status) + _ -> do goOn <- shouldContinue + return (if goOn then loop (crSuccess status && success) (lineNum + length txt) else return status) + + +data NextLine = NextLine [String] | NoMoreLines | Interrupted + +getInputLines :: String -> InputT REPL NextLine +getInputLines = handleInterrupt (MTL.lift (handleCtrlC Interrupted)) . loop [] + where + loop ls prompt = + do mb <- fmap (filter (/= '\r')) <$> getInputLine prompt + let newPropmpt = map (\_ -> ' ') prompt + case mb of + Nothing -> return NoMoreLines + Just l + | not (null l) && last l == '\\' -> loop (init l : ls) newPropmpt + | otherwise -> return $ NextLine $ reverse $ l : ls + +loadCryRC :: Cryptolrc -> REPL CommandResult +loadCryRC cryrc = + case cryrc of + CryrcDisabled -> return emptyCommandResult + CryrcDefault -> check [ getCurrentDirectory, getHomeDirectory ] + CryrcFiles opts -> loadMany opts + where + check [] = return emptyCommandResult + check (place : others) = + do dir <- io place + let file = dir ".cryptolrc" + present <- io (doesFileExist file) + if present + then crySession (Batch file) True + else check others + + loadMany [] = return emptyCommandResult + loadMany (f : fs) = do status <- crySession (Batch f) True + if crSuccess status + then loadMany fs + else return status + +-- | Haskeline-specific repl implementation. +repl :: + Cryptolrc -> + Maybe Project.Config -> + LoadProjectMode {- ^ refresh project -} -> + ReplMode -> Bool -> Bool -> REPL () -> IO CommandResult +repl cryrc projectConfig loadProjectMode replMode callStacks stopOnError begin = + runREPL isBatch callStacks stdoutLogger replAction + + where + -- this flag is used to suppress the logo and prompts + isBatch = + case projectConfig of + Just _ -> True + Nothing -> + case replMode of + InteractiveRepl -> False + Batch _ -> True + InteractiveBatch _ -> True + + replAction = + do status <- loadCryRC cryrc + if crSuccess status then do + begin + case projectConfig of + Just config -> loadProjectREPL loadProjectMode config + Nothing -> crySession replMode stopOnError + else return status + +-- | Try to set the history file. +setHistoryFile :: Settings REPL -> IO (Settings REPL) +setHistoryFile ss = + do dir <- getHomeDirectory + return ss { historyFile = Just (dir ".cryptol_history") } + `X.catch` \(X.SomeException {}) -> return ss + +-- | Haskeline settings for the REPL. +replSettings :: Bool -> Settings REPL +replSettings isBatch = Settings + { complete = cryptolCommand + , historyFile = Nothing + , autoAddHistory = not isBatch + } + +-- .cryptolrc ------------------------------------------------------------------ + +-- | Configuration of @.cryptolrc@ file behavior. The default option +-- searches the following locations in order, and evaluates the first +-- file that exists in batch mode on interpreter startup: +-- +-- 1. $PWD/.cryptolrc +-- 2. $HOME/.cryptolrc +-- +-- If files are specified, they will all be evaluated, but none of the +-- default files will be (unless they are explicitly specified). +-- +-- The disabled option inhibits any reading of any .cryptolrc files. +data Cryptolrc = + CryrcDefault + | CryrcDisabled + | CryrcFiles [FilePath] + deriving (Show) + +-- Utilities ------------------------------------------------------------------- + +#if !MIN_VERSION_haskeline(0,8,0) +instance MonadException REPL where + controlIO f = join $ liftBaseWith $ \f' -> + f $ RunIO $ \m -> restoreM <$> (f' m) +#endif + +-- Titles ---------------------------------------------------------------------- + +mkTitle :: Maybe LoadedModule -> String +mkTitle lm = maybe "" (\ m -> pretty m ++ " - ") (lName =<< lm) + ++ "cryptol" + +setREPLTitle :: REPL () +setREPLTitle = do + lm <- getLoadedMod + io (setTitle (mkTitle lm)) + +-- | In certain environments like Emacs, we shouldn't set the terminal +-- title. Note: this does not imply we can't use color output. We can +-- use ANSI color sequences in places like Emacs, but not terminal +-- codes. +-- +-- This checks that @'stdout'@ is a proper terminal handle, and that the +-- terminal mode is not @dumb@, which is set by Emacs and others. +shouldSetREPLTitle :: REPL Bool +shouldSetREPLTitle = io (hSupportsANSI stdout) + +-- | Whether we can display color titles. This checks that @'stdout'@ +-- is a proper terminal handle, and that the terminal mode is not +-- @dumb@, which is set by Emacs and others. +canDisplayColor :: REPL Bool +canDisplayColor = io (hSupportsANSI stdout) + +-- Completion ------------------------------------------------------------------ + +-- | Completion for cryptol commands. +cryptolCommand :: CompletionFunc REPL +cryptolCommand cursor@(l,r) + | ":" `isPrefixOf` l' + , Just (_,cmd,rest) <- splitCommand l' = case nub (findCommand cmd) of + + [c] | cursorRightAfterCmd rest -> + return (l, cmdComp cmd c) + | otherwise -> + completeCmdArgument cmd rest c + + cmds + -- If the command name is a prefix of multiple commands, then as a + -- special case, check if (1) the name matches one command exactly, and + -- (2) there is already some input for an argument. If so, proceed to + -- tab-complete that argument. This ensures that something like + -- `:check rev` will complete to `:check reverse`, even though the + -- command name `:check` is a prefix for both the `:check` and + -- `:check-docstrings` commands (#1781). + | [c] <- nub (findCommandExact cmd) + , not (cursorRightAfterCmd rest) -> + completeCmdArgument cmd rest c + + | otherwise -> + return (l, concat [ cmdComp l' c | c <- cmds ]) + -- Complete all : commands when the line is just a : + | ":" == l' = return (l, concat [ cmdComp l' c | c <- nub (findCommand ":") ]) + | otherwise = completeExpr cursor + where + l' = sanitize (reverse l) + + -- Check if the cursor is positioned immediately after the input for the + -- command, without any command arguments typed in after the command's name. + cursorRightAfterCmd :: + String + {- The rest of the input after the command. -} -> + Bool + cursorRightAfterCmd rest = null rest && not (any isSpace l') + + -- Perform tab completion for a single argument to a command. + completeCmdArgument :: + String + {- The name of the command as a String. -} -> + String + {- The rest of the input after the command. -} -> + CommandDescr + {- The description of the command. -} -> + REPL (String, [Completion]) + completeCmdArgument cmd rest c = + do (rest',cs) <- cmdArgument (cBody c) (reverse (sanitize rest),r) + return (unwords [rest', reverse cmd],cs) + +-- | Generate completions from a REPL command definition. +cmdComp :: String -> CommandDescr -> [Completion] +cmdComp prefix c = do + cName <- cNames c + guard (prefix `isPrefixOf` cName) + return $ nameComp prefix cName + +-- | Dispatch to a completion function based on the kind of completion the +-- command is expecting. +cmdArgument :: CommandBody -> CompletionFunc REPL +cmdArgument ct cursor@(l,_) = case ct of + ExprArg _ -> completeExpr cursor + DeclsArg _ -> (completeExpr +++ completeType) cursor + ExprTypeArg _ -> (completeExpr +++ completeType) cursor + ModNameArg _ -> completeModName cursor + FilenameArg _ -> completeFilename cursor + ShellArg _ -> completeFilename cursor + OptionArg _ -> completeOption cursor + HelpArg _ -> completeHelp cursor + NoArg _ -> return (l,[]) + FileExprArg _ -> completeExpr cursor + +-- | Additional keywords to suggest in the REPL +-- autocompletion list. +keywords :: [String] +keywords = + [ "else" + , "if" + , "let" + , "then" + , "where" + ] + +-- | Complete a name from the expression environment. +completeExpr :: CompletionFunc REPL +completeExpr (l,_) = do + ns <- (keywords++) <$> getExprNames + let n = reverse (takeIdent l) + vars = sort $ filter (n `isPrefixOf`) ns + return (l,map (nameComp n) vars) + +-- | Complete a name from the type synonym environment. +completeType :: CompletionFunc REPL +completeType (l,_) = do + ns <- getTypeNames + let n = reverse (takeIdent l) + vars = filter (n `isPrefixOf`) ns + return (l,map (nameComp n) vars) + +-- | Complete a name for which we can show REPL help documentation. +completeHelp :: CompletionFunc REPL +completeHelp (l, _) = do + ns1 <- getExprNames + ns2 <- getTypeNames + let ns3 = concatMap cNames (nub (findCommand ":")) + let ns = Set.toAscList (Set.fromList (ns1 ++ ns2)) ++ ns3 + let n = reverse l + case break isSpace n of + (":set", _ : n') -> + do let n'' = dropWhile isSpace n' + let vars = map optName (lookupTrie (dropWhile isSpace n') userOptions) + return (l, map (nameComp n'') vars) + _ -> + do let vars = filter (n `isPrefixOf`) ns + return (l, map (nameComp n) vars) + + +-- | Complete a name from the list of loaded modules. +completeModName :: CompletionFunc REPL +completeModName (l, _) = do + ms <- getModNames + let ns = map (T.unpack . modNameToText) (interactiveName : ms) + n = reverse (takeWhile (not . isSpace) l) + vars = filter (n `isPrefixOf`) ns + return (l, map (nameComp n) vars) + +-- | Generate a completion from a prefix and a name. +nameComp :: String -> String -> Completion +nameComp prefix c = Completion + { replacement = drop (length prefix) c + , display = c + , isFinished = True + } + +-- | Return longest identifier (possibly a qualified name) that is a +-- prefix of the given string +takeIdent :: String -> String +takeIdent (c : cs) | isIdentChar c = c : takeIdent cs +takeIdent (':' : ':' : cs) = ':' : ':' : takeIdent cs +takeIdent _ = [] + +isIdentChar :: Char -> Bool +isIdentChar c = isAlphaNum c || c `elem` "_\'" + +-- | Join two completion functions together, merging and sorting their results. +(+++) :: CompletionFunc REPL -> CompletionFunc REPL -> CompletionFunc REPL +(as +++ bs) cursor = do + (_,acs) <- as cursor + (_,bcs) <- bs cursor + return (fst cursor, sortBy (compare `on` replacement) (acs ++ bcs)) + + +-- | Complete an option from the options environment. +-- +-- XXX this can do better, as it has access to the expected form of the value +completeOption :: CompletionFunc REPL +completeOption cursor@(l,_) = return (fst cursor, map comp opts) + where + n = reverse l + opts = lookupTrie n userOptions + comp opt = Completion + { replacement = drop (length n) (optName opt) + , display = optName opt + , isFinished = False + } diff --git a/cryptol-repl-internal/REPL/Logo.hs b/cryptol-repl-internal/REPL/Logo.hs new file mode 100644 --- /dev/null +++ b/cryptol-repl-internal/REPL/Logo.hs @@ -0,0 +1,75 @@ +-- | +-- Module : REPL.Logo +-- Copyright : (c) 2013-2016 Galois, Inc. +-- License : BSD3 +-- Maintainer : cryptol@galois.com +-- Stability : provisional +-- Portability : portable + +module REPL.Logo where + +import Cryptol.REPL.Monad +import Cryptol.Utils.Panic (panic) +import Paths_cryptol (version) + +import Cryptol.Version (commitShortHash,commitDirty) +import Data.Version (showVersion) +import System.Console.ANSI +import Prelude () +import Prelude.Compat + + +type Version = String + +type Logo = [String] + +-- | The list of 'String's returned by the @mk@ function should be non-empty. +logo :: Bool -> (String -> [String]) -> Logo +logo useColor mk = + [ sgr [SetColor Foreground Dull White] ++ l | l <- ws ] + ++ [ sgr [SetColor Foreground Vivid Blue ] ++ l | l <- vs ] + ++ [ sgr [SetColor Foreground Dull Blue ] ++ l | l <- ds ] + ++ [ sgr [Reset] ] + where + sgr | useColor = setSGRCode + | otherwise = const [] + hashText | commitShortHash == "UNKNOWN" = "" + | otherwise = " (" ++ commitShortHash ++ + (if commitDirty then ", modified)" else ")") + versionText = "version " ++ showVersion version ++ hashText + ver = sgr [SetColor Foreground Dull White] + ++ replicate (lineLen - 20 - length versionText) ' ' + ++ versionText ++ "\n" + ++ "https://cryptol.net :? for help" + ls = mk ver + slen = length ls `div` 3 + (ws,rest) = splitAt slen ls + (vs,ds) = splitAt slen rest + line = case ls of + line':_ -> line' + [] -> panic "logo" ["empty lines"] + lineLen = length line + +displayLogo :: Bool -> Bool -> REPL () +displayLogo useColor useUnicode = + unlessBatch (io (mapM_ putStrLn (logo useColor (if useUnicode then logo2 else logo1)))) + +logo1 :: String -> [String] +logo1 ver = + [ " _ _" + , " ___ _ __ _ _ _ __ | |_ ___ | |" + , " / __| \'__| | | | \'_ \\| __/ _ \\| |" + , " | (__| | | |_| | |_) | || (_) | |" + , " \\___|_| \\__, | .__/ \\__\\___/|_|" + , " |___/|_| " ++ ver + ] + +logo2 :: String -> [String] +logo2 ver = + [ "┏━╸┏━┓╻ ╻┏━┓╺┳╸┏━┓╻ " + , "┃ ┣┳┛┗┳┛┣━┛ ┃ ┃ ┃┃ " + , "┗━╸╹┗╸ ╹ ╹ ╹ ┗━┛┗━╸" + , ver + ] + + diff --git a/cryptol.cabal b/cryptol.cabal --- a/cryptol.cabal +++ b/cryptol.cabal @@ -1,21 +1,22 @@ Cabal-version: 2.4 Name: cryptol -Version: 3.2.0 +Version: 3.3.0 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: BSD-3-Clause License-file: LICENSE Author: Galois, Inc. Maintainer: cryptol@galois.com -Homepage: http://www.cryptol.net/ +Homepage: https://tools.galois.com/cryptol Bug-reports: https://github.com/GaloisInc/cryptol/issues -Copyright: 2013-2022 Galois Inc. +Copyright: 2013-2025 Galois Inc. Category: Language Build-type: Simple extra-source-files: bench/data/*.cry - CHANGES.md lib/*.cry lib/*.z3 +extra-doc-files: CHANGES.md + data-files: **/*.cry **/*.z3 data-dir: lib @@ -27,7 +28,7 @@ type: git location: https://github.com/GaloisInc/cryptol.git -- add a tag on release branches - tag: 3.2.0 + tag: 3.3.0 flag static @@ -54,7 +55,7 @@ array >= 0.4, containers >= 0.5, criterion-measurement, - cryptohash-sha1 >= 0.11 && < 0.12, + cryptohash-sha256 >= 0.11 && < 0.12, deepseq >= 1.3, directory >= 1.2.2.0, exceptions, @@ -63,6 +64,7 @@ gitrev >= 1.0, ghc-prim, GraphSCC >= 1.0.4, + heredoc >= 0.2, language-c99, language-c99-simple, libBF >= 0.6 && < 0.7, @@ -75,17 +77,18 @@ pretty-show, process >= 1.2, sbv >= 9.1 && < 10.11, - simple-smt >= 0.9.7, + simple-smt >= 0.9.8, stm >= 2.4, strict, text >= 1.1, tf-random >= 0.5, + toml-parser >= 2.0 && <2.1, transformers-base >= 0.4, vector, mtl >= 2.2.1, time >= 1.6.0.1, panic >= 0.3, - what4 >= 1.4 && < 1.7 + what4 >= 1.6 && < 1.8 if impl(ghc >= 9.0) build-depends: ghc-bignum >= 1.0 && < 1.4 @@ -238,8 +241,15 @@ Cryptol.REPL.Help, Cryptol.REPL.Browse, Cryptol.REPL.Monad, - Cryptol.REPL.Trie + Cryptol.REPL.Trie, + Cryptol.Project + Cryptol.Project.Config + Cryptol.Project.Monad + Cryptol.Project.Cache + Cryptol.Project.WildMatch + + Autogen-modules: Paths_cryptol Other-modules: Cryptol.Parser.LexerUtils, Cryptol.Parser.ParserUtils, Cryptol.Prelude, @@ -254,20 +264,24 @@ if flag(relocatable) cpp-options: -DRELOCATABLE -executable cryptol - Default-language: - Haskell2010 - Main-is: Main.hs - hs-source-dirs: cryptol +-- The portions of the Cryptol REPL that are specific to the Cryptol executable. +-- We factor this out into a separate internal library because (1) it has some +-- dependencies (e.g., ansi-terminal and haskeline) that the Cryptol library +-- does not need to depend on, and (2) we want to be able to test this code in +-- the cryptol-api-tests test suite. +library cryptol-repl-internal + exposed-modules: REPL.Haskeline + REPL.Logo Autogen-modules: Paths_cryptol - - Other-modules: OptParser, - REPL.Haskeline, - REPL.Logo, - Paths_cryptol - + Other-modules: Paths_cryptol + hs-source-dirs: cryptol-repl-internal + default-language: Haskell2010 + GHC-options: -Wall -O2 + if os(linux) && flag(static) + ld-options: -static -pthread + ghc-options: -optl-fuse-ld=bfd build-depends: ansi-terminal - , base + , base >= 4.9 && < 5 , base-compat , containers , cryptol @@ -278,6 +292,19 @@ , monad-control , text , transformers + +executable cryptol + Default-language: + Haskell2010 + Main-is: Main.hs + hs-source-dirs: cryptol + Other-modules: OptParser + build-depends: base >= 4.9 && < 5 + , base-compat + , cryptol + , cryptol-repl-internal + , directory + , filepath GHC-options: -Wall -threaded -rtsopts "-with-rtsopts=-N1 -A64m" -O2 if impl(ghc >= 8.0.1) ghc-options: -Wno-redundant-constraints @@ -291,7 +318,11 @@ Haskell2010 main-is: CryHtml.hs hs-source-dirs: utils - build-depends: base, text, cryptol, blaze-html + build-depends: + base >= 4.9 && < 5, + text, + cryptol, + blaze-html GHC-options: -Wall if os(linux) && flag(static) @@ -304,7 +335,7 @@ Main-is: CheckExercises.hs hs-source-dirs: cryptol build-depends: ansi-terminal - , base + , base >= 4.9 && < 5 , containers , directory , extra @@ -315,6 +346,26 @@ , temporary , text GHC-options: -Wall + +-- Test cases that require the use of the Cryptol API to test effectively. Most +-- other test cases should be added to the integration tests (which only require +-- the Cryptol executable and/or the REPL) under tests/. +test-suite cryptol-api-tests + type: exitcode-stdio-1.0 + main-is: Main.hs + hs-source-dirs: api-tests + default-language: Haskell2010 + GHC-options: -Wall -threaded -rtsopts "-with-rtsopts=-N1 -A64m" -O2 + if os(linux) && flag(static) + ld-options: -static -pthread + ghc-options: -optl-fuse-ld=bfd + build-depends: base >= 4.9 && < 5 + , cryptol + , cryptol-repl-internal + , haskeline + , tasty + , tasty-hunit + benchmark cryptol-bench type: exitcode-stdio-1.0 main-is: Main.hs @@ -326,7 +377,7 @@ if os(linux) && flag(static) ld-options: -static -pthread ghc-options: -optl-fuse-ld=bfd - build-depends: base + build-depends: base >= 4.9 && < 5 , criterion , cryptol , deepseq diff --git a/cryptol/Main.hs b/cryptol/Main.hs --- a/cryptol/Main.hs +++ b/cryptol/Main.hs @@ -8,6 +8,7 @@ {-# LANGUAGE CPP #-} {-# LANGUAGE GeneralizedNewtypeDeriving #-} +{-# LANGUAGE LambdaCase #-} {-# LANGUAGE OverloadedStrings #-} module Main where @@ -18,6 +19,7 @@ io,prependSearchPath,setSearchPath,parseSearchPath) import qualified Cryptol.REPL.Monad as REPL import Cryptol.ModuleSystem.Env(ModulePath(..)) +import qualified Cryptol.Project as Project import REPL.Haskeline import REPL.Logo @@ -26,6 +28,7 @@ import Cryptol.Version (displayVersion) import Control.Monad (when, void) +import Data.Maybe (isJust, isNothing) import GHC.IO.Encoding (setLocaleEncoding, utf8) import System.Console.GetOpt (OptDescr(..),ArgOrder(..),ArgDescr(..),getOpt,usageInfo) @@ -47,6 +50,8 @@ , optVersion :: Bool , optHelp :: Bool , optBatch :: ReplMode + , optProject :: Maybe FilePath + , optProjectRefresh :: Project.LoadProjectMode , optCallStacks :: Bool , optCommands :: [String] , optColorMode :: ColorMode @@ -62,6 +67,8 @@ , optVersion = False , optHelp = False , optBatch = InteractiveRepl + , optProject = Nothing + , optProjectRefresh = Project.ModifiedMode , optCallStacks = True , optCommands = [] , optColorMode = AutoColor @@ -79,6 +86,16 @@ , Option "" ["interactive-batch"] (ReqArg setInteractiveBatchScript "FILE") "run the script provided and exit, but behave as if running an interactive session" + , Option "p" ["project"] (ReqArg setProject "CRYPROJECT") + ("Load and verify a Cryptol project using the provided project " + ++ "configuration file or directory containing 'cryproject.toml'") + + , Option "" ["refresh-project"] (NoArg setProjectRefresh) + "Ignore a pre-existing cache file when loading a project." + + , Option "" ["untested-project"] (NoArg setProjectUntested) + "Load all project files that don't have a test result." + , Option "e" ["stop-on-error"] (NoArg setStopOnError) "stop script execution as soon as an error occurs." @@ -137,6 +154,15 @@ setInteractiveBatchScript :: String -> OptParser Options setInteractiveBatchScript path = modify $ \ opts -> opts { optBatch = InteractiveBatch path } +setProject :: String -> OptParser Options +setProject path = modify $ \opts -> opts { optProject = Just path } + +setProjectRefresh :: OptParser Options +setProjectRefresh = modify $ \opts -> opts { optProjectRefresh = Project.RefreshMode } + +setProjectUntested :: OptParser Options +setProjectUntested = modify $ \opts -> opts { optProjectRefresh = Project.UntestedMode } + -- | Set the color mode of the terminal output. setColorMode :: String -> OptParser Options setColorMode "auto" = modify $ \ opts -> opts { optColorMode = AutoColor } @@ -200,7 +226,7 @@ , "via the `:edit` command" ] ) - , ( "SBV_{ABC,BOOLECTOR,CVC4,CVC5,MATHSAT,YICES,Z3}_OPTIONS" + , ( "SBV_{ABC,BITWUZLA,BOOLECTOR,CVC4,CVC5,MATHSAT,YICES,Z3}_OPTIONS" , [ "A string of command-line arguments to be passed to the" , "corresponding solver invoked for `:sat` and `:prove`" , "when using a prover via SBV" @@ -225,11 +251,14 @@ | optVersion opts -> displayVersion putStrLn | otherwise -> do (opts', mCleanup) <- setupCmdScript opts - status <- repl (optCryptolrc opts') - (optBatch opts') - (optCallStacks opts') - (optStopOnError opts') - (setupREPL opts') + (opts'', mConfig) <- setupProject opts' + status <- repl (optCryptolrc opts'') + mConfig + (optProjectRefresh opts'') + (optBatch opts'') + (optCallStacks opts'') + (optStopOnError opts'') + (setupREPL opts'') case mCleanup of Nothing -> return () Just cmdFile -> removeFile cmdFile @@ -249,8 +278,28 @@ hClose h when (optBatch opts /= InteractiveRepl) $ putStrLn "[warning] --command argument specified; ignoring batch file" - return (opts { optBatch = InteractiveBatch path }, Just path) + when (isJust (optProject opts)) $ + putStrLn $ + "[warning] --command argument specified; " + ++ "ignoring project configuration file" + return + ( opts { optBatch = InteractiveBatch path, optProject = Nothing } + , Just path ) +setupProject :: Options -> IO (Options, Maybe Project.Config) +setupProject opts = + case optProject opts of + Nothing -> pure (opts, Nothing) + Just path -> do + when (optBatch opts /= InteractiveRepl) $ + putStrLn "[warning] --project argument specified; ignoring batch file" + Project.loadConfig path >>= \case + Left err -> do + print $ pp err + exitFailure + Right config -> + pure (opts { optBatch = InteractiveRepl }, Just config) + setupREPL :: Options -> REPL () setupREPL opts = do mCryptolPath <- io $ lookupEnv "CRYPTOLPATH" @@ -281,18 +330,20 @@ Batch file -> prependSearchPath [ takeDirectory file ] _ -> return () - case optLoad opts of - [] -> loadPrelude `REPL.catch` \x -> io $ print $ pp x - [l] -> void (loadCmd l) `REPL.catch` \x -> do - io $ print $ pp x - -- If the requested file fails to load, load the prelude instead... - loadPrelude `REPL.catch` \y -> do - io $ print $ pp y - -- ... but make sure the loaded module is set to the file - -- we tried, instead of the Prelude - REPL.setEditPath l - REPL.setLoadedMod REPL.LoadedModule - { REPL.lFocus = Nothing - , REPL.lPath = InFile l - } - _ -> io $ putStrLn "Only one file may be loaded at the command line." + when (isNothing (optProject opts)) $ + case optLoad opts of + [] -> loadPrelude `REPL.catch` \x -> io $ print $ pp x + [l] -> void (loadCmd l) `REPL.catch` \x -> do + io $ print $ pp x + -- If the requested file fails to load, + -- load the prelude instead... + loadPrelude `REPL.catch` \y -> do + io $ print $ pp y + -- ... but make sure the loaded module is set to the file + -- we tried, instead of the Prelude + REPL.setEditPath l + REPL.setLoadedMod REPL.LoadedModule + { REPL.lFocus = Nothing + , REPL.lPath = InFile l + } + _ -> io $ putStrLn "Only one file may be loaded at the command line." diff --git a/cryptol/REPL/Haskeline.hs b/cryptol/REPL/Haskeline.hs deleted file mode 100644 --- a/cryptol/REPL/Haskeline.hs +++ /dev/null @@ -1,356 +0,0 @@ --- | --- Module : REPL.Haskeline --- Copyright : (c) 2013-2016 Galois, Inc. --- License : BSD3 --- Maintainer : cryptol@galois.com --- Stability : provisional --- Portability : portable - -{-# LANGUAGE CPP #-} -{-# LANGUAGE MultiWayIf #-} -{-# LANGUAGE PatternGuards #-} -{-# LANGUAGE BangPatterns #-} -{-# OPTIONS_GHC -fno-warn-orphans #-} - -module REPL.Haskeline where - -import Cryptol.REPL.Command -import Cryptol.REPL.Monad -import Cryptol.REPL.Trie -import Cryptol.Utils.PP hiding (()) -import Cryptol.Utils.Logger(stdoutLogger) -import Cryptol.Utils.Ident(modNameToText, interactiveName) - -import qualified Control.Exception as X -import Control.Monad (guard, join) -import qualified Control.Monad.Trans.Class as MTL -#if !MIN_VERSION_haskeline(0,8,0) -import Control.Monad.Trans.Control -#endif -import Data.Char (isAlphaNum, isSpace) -import Data.Function (on) -import Data.List (isPrefixOf,nub,sortBy,sort) -import qualified Data.Set as Set -import qualified Data.Text as T (unpack) -import System.Console.ANSI (setTitle, hSupportsANSI) -import System.Console.Haskeline -import System.Directory ( doesFileExist - , getHomeDirectory - , getCurrentDirectory) -import System.FilePath (()) -import System.IO (stdout) - -import Prelude () -import Prelude.Compat - - -data ReplMode - = InteractiveRepl -- ^ Interactive terminal session - | Batch FilePath -- ^ Execute from a batch file - | InteractiveBatch FilePath - -- ^ Execute from a batch file, but behave as though - -- lines are entered in an interactive session. - deriving (Show, Eq) - --- | One REPL invocation, either from a file or from the terminal. -crySession :: ReplMode -> Bool -> REPL CommandResult -crySession replMode stopOnError = - do settings <- io (setHistoryFile (replSettings isBatch)) - let act = runInputTBehavior behavior settings (withInterrupt (loop True 1)) - if isBatch then asBatch act else act - where - (isBatch,behavior) = case replMode of - InteractiveRepl -> (False, defaultBehavior) - Batch path -> (True, useFile path) - InteractiveBatch path -> (False, useFile path) - - loop :: Bool -> Int -> InputT REPL CommandResult - loop !success !lineNum = - do ln <- getInputLines =<< MTL.lift getPrompt - case ln of - NoMoreLines -> return emptyCommandResult { crSuccess = success } - Interrupted - | isBatch && stopOnError -> return emptyCommandResult { crSuccess = False } - | otherwise -> loop success lineNum - NextLine ls - | all (all isSpace) ls -> loop success (lineNum + length ls) - | otherwise -> doCommand success lineNum ls - - run lineNum cmd = - case replMode of - InteractiveRepl -> runCommand lineNum Nothing cmd - InteractiveBatch _ -> runCommand lineNum Nothing cmd - Batch path -> runCommand lineNum (Just path) cmd - - doCommand success lineNum txt = - case parseCommand findCommandExact (unlines txt) of - Nothing | isBatch && stopOnError -> return emptyCommandResult { crSuccess = False } - | otherwise -> loop False (lineNum + length txt) -- say somtething? - Just cmd -> join $ MTL.lift $ - do status <- handleInterrupt (handleCtrlC emptyCommandResult { crSuccess = False }) (run lineNum cmd) - case crSuccess status of - False | isBatch && stopOnError -> return (return status) - _ -> do goOn <- shouldContinue - return (if goOn then loop (crSuccess status && success) (lineNum + length txt) else return status) - - -data NextLine = NextLine [String] | NoMoreLines | Interrupted - -getInputLines :: String -> InputT REPL NextLine -getInputLines = handleInterrupt (MTL.lift (handleCtrlC Interrupted)) . loop [] - where - loop ls prompt = - do mb <- fmap (filter (/= '\r')) <$> getInputLine prompt - let newPropmpt = map (\_ -> ' ') prompt - case mb of - Nothing -> return NoMoreLines - Just l - | not (null l) && last l == '\\' -> loop (init l : ls) newPropmpt - | otherwise -> return $ NextLine $ reverse $ l : ls - -loadCryRC :: Cryptolrc -> REPL CommandResult -loadCryRC cryrc = - case cryrc of - CryrcDisabled -> return emptyCommandResult - CryrcDefault -> check [ getCurrentDirectory, getHomeDirectory ] - CryrcFiles opts -> loadMany opts - where - check [] = return emptyCommandResult - check (place : others) = - do dir <- io place - let file = dir ".cryptolrc" - present <- io (doesFileExist file) - if present - then crySession (Batch file) True - else check others - - loadMany [] = return emptyCommandResult - loadMany (f : fs) = do status <- crySession (Batch f) True - if crSuccess status - then loadMany fs - else return status - --- | Haskeline-specific repl implementation. -repl :: Cryptolrc -> ReplMode -> Bool -> Bool -> REPL () -> IO CommandResult -repl cryrc replMode callStacks stopOnError begin = - runREPL isBatch callStacks stdoutLogger replAction - - where - -- this flag is used to suppress the logo and prompts - isBatch = case replMode of - InteractiveRepl -> False - Batch _ -> True - InteractiveBatch _ -> True - - replAction = - do status <- loadCryRC cryrc - if crSuccess status - then begin >> crySession replMode stopOnError - else return status - --- | Try to set the history file. -setHistoryFile :: Settings REPL -> IO (Settings REPL) -setHistoryFile ss = - do dir <- getHomeDirectory - return ss { historyFile = Just (dir ".cryptol_history") } - `X.catch` \(X.SomeException {}) -> return ss - --- | Haskeline settings for the REPL. -replSettings :: Bool -> Settings REPL -replSettings isBatch = Settings - { complete = cryptolCommand - , historyFile = Nothing - , autoAddHistory = not isBatch - } - --- .cryptolrc ------------------------------------------------------------------ - --- | Configuration of @.cryptolrc@ file behavior. The default option --- searches the following locations in order, and evaluates the first --- file that exists in batch mode on interpreter startup: --- --- 1. $PWD/.cryptolrc --- 2. $HOME/.cryptolrc --- --- If files are specified, they will all be evaluated, but none of the --- default files will be (unless they are explicitly specified). --- --- The disabled option inhibits any reading of any .cryptolrc files. -data Cryptolrc = - CryrcDefault - | CryrcDisabled - | CryrcFiles [FilePath] - deriving (Show) - --- Utilities ------------------------------------------------------------------- - -#if !MIN_VERSION_haskeline(0,8,0) -instance MonadException REPL where - controlIO f = join $ liftBaseWith $ \f' -> - f $ RunIO $ \m -> restoreM <$> (f' m) -#endif - --- Titles ---------------------------------------------------------------------- - -mkTitle :: Maybe LoadedModule -> String -mkTitle lm = maybe "" (\ m -> pretty m ++ " - ") (lName =<< lm) - ++ "cryptol" - -setREPLTitle :: REPL () -setREPLTitle = do - lm <- getLoadedMod - io (setTitle (mkTitle lm)) - --- | In certain environments like Emacs, we shouldn't set the terminal --- title. Note: this does not imply we can't use color output. We can --- use ANSI color sequences in places like Emacs, but not terminal --- codes. --- --- This checks that @'stdout'@ is a proper terminal handle, and that the --- terminal mode is not @dumb@, which is set by Emacs and others. -shouldSetREPLTitle :: REPL Bool -shouldSetREPLTitle = io (hSupportsANSI stdout) - --- | Whether we can display color titles. This checks that @'stdout'@ --- is a proper terminal handle, and that the terminal mode is not --- @dumb@, which is set by Emacs and others. -canDisplayColor :: REPL Bool -canDisplayColor = io (hSupportsANSI stdout) - --- Completion ------------------------------------------------------------------ - --- | Completion for cryptol commands. -cryptolCommand :: CompletionFunc REPL -cryptolCommand cursor@(l,r) - | ":" `isPrefixOf` l' - , Just (_,cmd,rest) <- splitCommand l' = case nub (findCommand cmd) of - - [c] | null rest && not (any isSpace l') -> do - return (l, cmdComp cmd c) - | otherwise -> do - (rest',cs) <- cmdArgument (cBody c) (reverse (sanitize rest),r) - return (unwords [rest', reverse cmd],cs) - - cmds -> - return (l, concat [ cmdComp l' c | c <- cmds ]) - -- Complete all : commands when the line is just a : - | ":" == l' = return (l, concat [ cmdComp l' c | c <- nub (findCommand ":") ]) - | otherwise = completeExpr cursor - where - l' = sanitize (reverse l) - --- | Generate completions from a REPL command definition. -cmdComp :: String -> CommandDescr -> [Completion] -cmdComp prefix c = do - cName <- cNames c - guard (prefix `isPrefixOf` cName) - return $ nameComp prefix cName - --- | Dispatch to a completion function based on the kind of completion the --- command is expecting. -cmdArgument :: CommandBody -> CompletionFunc REPL -cmdArgument ct cursor@(l,_) = case ct of - ExprArg _ -> completeExpr cursor - DeclsArg _ -> (completeExpr +++ completeType) cursor - ExprTypeArg _ -> (completeExpr +++ completeType) cursor - ModNameArg _ -> completeModName cursor - FilenameArg _ -> completeFilename cursor - ShellArg _ -> completeFilename cursor - OptionArg _ -> completeOption cursor - HelpArg _ -> completeHelp cursor - NoArg _ -> return (l,[]) - FileExprArg _ -> completeExpr cursor - --- | Additional keywords to suggest in the REPL --- autocompletion list. -keywords :: [String] -keywords = - [ "else" - , "if" - , "let" - , "then" - , "where" - ] - --- | Complete a name from the expression environment. -completeExpr :: CompletionFunc REPL -completeExpr (l,_) = do - ns <- (keywords++) <$> getExprNames - let n = reverse (takeIdent l) - vars = sort $ filter (n `isPrefixOf`) ns - return (l,map (nameComp n) vars) - --- | Complete a name from the type synonym environment. -completeType :: CompletionFunc REPL -completeType (l,_) = do - ns <- getTypeNames - let n = reverse (takeIdent l) - vars = filter (n `isPrefixOf`) ns - return (l,map (nameComp n) vars) - --- | Complete a name for which we can show REPL help documentation. -completeHelp :: CompletionFunc REPL -completeHelp (l, _) = do - ns1 <- getExprNames - ns2 <- getTypeNames - let ns3 = concatMap cNames (nub (findCommand ":")) - let ns = Set.toAscList (Set.fromList (ns1 ++ ns2)) ++ ns3 - let n = reverse l - case break isSpace n of - (":set", _ : n') -> - do let n'' = dropWhile isSpace n' - let vars = map optName (lookupTrie (dropWhile isSpace n') userOptions) - return (l, map (nameComp n'') vars) - _ -> - do let vars = filter (n `isPrefixOf`) ns - return (l, map (nameComp n) vars) - - --- | Complete a name from the list of loaded modules. -completeModName :: CompletionFunc REPL -completeModName (l, _) = do - ms <- getModNames - let ns = map (T.unpack . modNameToText) (interactiveName : ms) - n = reverse (takeWhile (not . isSpace) l) - vars = filter (n `isPrefixOf`) ns - return (l, map (nameComp n) vars) - --- | Generate a completion from a prefix and a name. -nameComp :: String -> String -> Completion -nameComp prefix c = Completion - { replacement = drop (length prefix) c - , display = c - , isFinished = True - } - --- | Return longest identifier (possibly a qualified name) that is a --- prefix of the given string -takeIdent :: String -> String -takeIdent (c : cs) | isIdentChar c = c : takeIdent cs -takeIdent (':' : ':' : cs) = ':' : ':' : takeIdent cs -takeIdent _ = [] - -isIdentChar :: Char -> Bool -isIdentChar c = isAlphaNum c || c `elem` "_\'" - --- | Join two completion functions together, merging and sorting their results. -(+++) :: CompletionFunc REPL -> CompletionFunc REPL -> CompletionFunc REPL -(as +++ bs) cursor = do - (_,acs) <- as cursor - (_,bcs) <- bs cursor - return (fst cursor, sortBy (compare `on` replacement) (acs ++ bcs)) - - --- | Complete an option from the options environment. --- --- XXX this can do better, as it has access to the expected form of the value -completeOption :: CompletionFunc REPL -completeOption cursor@(l,_) = return (fst cursor, map comp opts) - where - n = reverse l - opts = lookupTrie n userOptions - comp opt = Completion - { replacement = drop (length n) (optName opt) - , display = optName opt - , isFinished = False - } diff --git a/cryptol/REPL/Logo.hs b/cryptol/REPL/Logo.hs deleted file mode 100644 --- a/cryptol/REPL/Logo.hs +++ /dev/null @@ -1,75 +0,0 @@ --- | --- Module : REPL.Logo --- Copyright : (c) 2013-2016 Galois, Inc. --- License : BSD3 --- Maintainer : cryptol@galois.com --- Stability : provisional --- Portability : portable - -module REPL.Logo where - -import Cryptol.REPL.Monad -import Cryptol.Utils.Panic (panic) -import Paths_cryptol (version) - -import Cryptol.Version (commitShortHash,commitDirty) -import Data.Version (showVersion) -import System.Console.ANSI -import Prelude () -import Prelude.Compat - - -type Version = String - -type Logo = [String] - --- | The list of 'String's returned by the @mk@ function should be non-empty. -logo :: Bool -> (String -> [String]) -> Logo -logo useColor mk = - [ sgr [SetColor Foreground Dull White] ++ l | l <- ws ] - ++ [ sgr [SetColor Foreground Vivid Blue ] ++ l | l <- vs ] - ++ [ sgr [SetColor Foreground Dull Blue ] ++ l | l <- ds ] - ++ [ sgr [Reset] ] - where - sgr | useColor = setSGRCode - | otherwise = const [] - hashText | commitShortHash == "UNKNOWN" = "" - | otherwise = " (" ++ commitShortHash ++ - (if commitDirty then ", modified)" else ")") - versionText = "version " ++ showVersion version ++ hashText - ver = sgr [SetColor Foreground Dull White] - ++ replicate (lineLen - 20 - length versionText) ' ' - ++ versionText ++ "\n" - ++ "https://cryptol.net :? for help" - ls = mk ver - slen = length ls `div` 3 - (ws,rest) = splitAt slen ls - (vs,ds) = splitAt slen rest - line = case ls of - line':_ -> line' - [] -> panic "logo" ["empty lines"] - lineLen = length line - -displayLogo :: Bool -> Bool -> REPL () -displayLogo useColor useUnicode = - unlessBatch (io (mapM_ putStrLn (logo useColor (if useUnicode then logo2 else logo1)))) - -logo1 :: String -> [String] -logo1 ver = - [ " _ _" - , " ___ _ __ _ _ _ __ | |_ ___ | |" - , " / __| \'__| | | | \'_ \\| __/ _ \\| |" - , " | (__| | | |_| | |_) | || (_) | |" - , " \\___|_| \\__, | .__/ \\__\\___/|_|" - , " |___/|_| " ++ ver - ] - -logo2 :: String -> [String] -logo2 ver = - [ "┏━╸┏━┓╻ ╻┏━┓╺┳╸┏━┓╻ " - , "┃ ┣┳┛┗┳┛┣━┛ ┃ ┃ ┃┃ " - , "┗━╸╹┗╸ ╹ ╹ ╹ ┗━┛┗━╸" - , ver - ] - - diff --git a/lib/CryptolTC.z3 b/lib/CryptolTC.z3 --- a/lib/CryptolTC.z3 +++ b/lib/CryptolTC.z3 @@ -75,6 +75,15 @@ (cryBool true) ) + +(declare-fun cryPrimeUnknown (Int) Bool) + +(define-fun cryPrime ((x InfNat)) MaybeBool + (ite (isErr x) cryErrProp + (cryBool (and (isFin x) (cryPrimeUnknown (value x))))) +) + + ; ------------------------------------------------------------------------------ ; Basic Cryptol assume/assert @@ -327,14 +336,14 @@ ; (declare-fun L () InfNat) ; (declare-fun w () InfNat) -; +; ; (assert (cryVar L)) ; (assert (cryVar w)) -; +; ; (assert (cryAssume (cryFin w))) ; (assert (cryAssume (cryGeq w (cryNat 1)))) ; (assert (cryAssume (cryGeq (cryMul (cryNat 2) w) (cryWidth L)))) -; +; ; (assert (cryProve ; (cryGeq ; (cryMul @@ -343,7 +352,7 @@ ; (cryMul (cryNat 16) w)) ; (cryMul (cryNat 16) w)) ; (cryAdd (cryNat 1) (cryAdd L (cryMul (cryNat 2) w)))))) -; +; ; (check-sat) diff --git a/src/Cryptol/Backend.hs b/src/Cryptol/Backend.hs --- a/src/Cryptol/Backend.hs +++ b/src/Cryptol/Backend.hs @@ -1,7 +1,9 @@ {-# Language FlexibleContexts #-} {-# Language TypeFamilies #-} +{-# Language ScopedTypeVariables #-} module Cryptol.Backend ( Backend(..) + , wordLen , sDelay , invalidIndex , cryUserError @@ -36,6 +38,7 @@ import qualified Control.Exception as X import Control.Monad.IO.Class import Data.Kind (Type) +import Data.Proxy(Proxy(..)) import Cryptol.Backend.FloatHelpers (BF) import Cryptol.Backend.Monad @@ -295,7 +298,7 @@ bitAsLit :: sym -> SBit sym -> Maybe Bool -- | The number of bits in a word value. - wordLen :: sym -> SWord sym -> Integer + wordLen' :: proxy sym -> SWord sym -> Integer -- | Determine if this symbolic word is a literal. -- If so, return the bit width and value. @@ -813,3 +816,7 @@ SFloat sym -> SFloat sym -> SEval sym (SFloat sym) + +wordLen :: forall sym. Backend sym => sym -> SWord sym -> Integer +wordLen _ x = wordLen' (Proxy :: Proxy sym) x +{-# INLINE wordLen #-} diff --git a/src/Cryptol/Backend/Concrete.hs b/src/Cryptol/Backend/Concrete.hs --- a/src/Cryptol/Backend/Concrete.hs +++ b/src/Cryptol/Backend/Concrete.hs @@ -144,7 +144,9 @@ assertSideCondition _ True _ = return () assertSideCondition sym False err = raiseError sym err - wordLen _ (BV w _) = w + wordLen' _ (BV w _) = w + {-# INLINE wordLen' #-} + wordAsChar _ (BV _ x) = Just $! integerToChar x wordBit _ (BV w x) idx = pure $! testBit x (fromInteger (w - 1 - idx)) diff --git a/src/Cryptol/Backend/SBV.hs b/src/Cryptol/Backend/SBV.hs --- a/src/Cryptol/Backend/SBV.hs +++ b/src/Cryptol/Backend/SBV.hs @@ -201,7 +201,8 @@ SBVResult pz z -> pure $ SBVResult (svAnd (svIte c px py) pz) z - wordLen _ v = toInteger (intSizeOf v) + wordLen' _ v = toInteger (intSizeOf v) + {-# INLINE wordLen' #-} wordAsChar _ v = integerToChar <$> svAsInteger v iteBit _ b x y = pure $! svSymbolicMerge KBool True b x y diff --git a/src/Cryptol/Backend/What4.hs b/src/Cryptol/Backend/What4.hs --- a/src/Cryptol/Backend/What4.hs +++ b/src/Cryptol/Backend/What4.hs @@ -273,7 +273,8 @@ | SW.bvWidth bv == 8 = toEnum . fromInteger <$> SW.bvAsUnsignedInteger bv | otherwise = Nothing - wordLen _ bv = SW.bvWidth bv + wordLen' _ bv = SW.bvWidth bv + {-# INLINE wordLen' #-} bitLit sym b = W4.backendPred (w4 sym) b bitAsLit _ v = W4.asConstantPred v diff --git a/src/Cryptol/Backend/WordValue.hs b/src/Cryptol/Backend/WordValue.hs --- a/src/Cryptol/Backend/WordValue.hs +++ b/src/Cryptol/Backend/WordValue.hs @@ -25,6 +25,7 @@ ( -- * WordValue WordValue , wordVal + , wordValWidth , bitmapWordVal , asWordList , asWordVal @@ -59,6 +60,7 @@ import Control.Monad (unless) import Data.Bits +import Data.Proxy(Proxy(..)) import GHC.Generics (Generic) import Cryptol.Backend @@ -96,6 +98,14 @@ !(SEval sym (SWord sym)) -- ^ Thunk for packing the word !(SeqMap sym (SBit sym)) -- ^ deriving (Generic) + +wordValWidth :: forall sym. Backend sym => WordValue sym -> Integer +wordValWidth val = + case val of + ThunkWordVal n _ -> n + WordVal sv -> wordLen' (Proxy :: Proxy sym) sv + BitmapVal n _ _ -> n +{-# INLINE wordValWidth #-} wordVal :: SWord sym -> WordValue sym wordVal = WordVal diff --git a/src/Cryptol/Eval.hs b/src/Cryptol/Eval.hs --- a/src/Cryptol/Eval.hs +++ b/src/Cryptol/Eval.hs @@ -130,14 +130,14 @@ -- NB, even if the list cannot be packed, we must use `VWord` -- when the element type is `Bit`. | isTBit tyv -> {-# SCC "evalExpr->Elist/bit" #-} - VWord len <$> + VWord <$> (tryFromBits sym vs >>= \case Just w -> pure (wordVal w) Nothing -> do xs <- mapM (\x -> sDelay sym (fromVBit <$> x)) vs bitmapWordVal sym len $ finiteSeqMap sym xs) | otherwise -> {-# SCC "evalExpr->EList" #-} do xs <- mapM (sDelay sym) vs - return $ VSeq len $ finiteSeqMap sym xs + mkSeq sym (Nat len) tyv $ finiteSeqMap sym xs where tyv = evalValType (envTypes env) ty vs = map eval es @@ -594,7 +594,7 @@ case v of VSeq _ vs -> lookupSeqMap vs (toInteger n) VStream vs -> lookupSeqMap vs (toInteger n) - VWord _ wv -> VBit <$> indexWordValue sym wv (toInteger n) + VWord wv -> VBit <$> indexWordValue sym wv (toInteger n) _ -> do vdoc <- ppValue sym defaultPPOpts val evalPanic "Cryptol.Eval.evalSel" [ "Unexpected value in list selection" @@ -608,7 +608,7 @@ sym -> TValue -> GenValue sym -> Selector -> SEval sym (GenValue sym) -> SEval sym (GenValue sym) -evalSetSel sym _tyv e sel v = +evalSetSel sym tyv e sel v = case sel of TupleSel n _ -> setTuple n RecordSel n _ -> setRecord n @@ -641,9 +641,10 @@ setList n = case e of - VSeq i mp -> pure $ VSeq i $ updateSeqMap mp n v + VSeq i mp | TVSeq _ elty <- tyv -> + mkSeq sym (Nat i) elty $ updateSeqMap mp n v VStream mp -> pure $ VStream $ updateSeqMap mp n v - VWord i m -> VWord i <$> updateWordValue sym m n asBit + VWord m -> VWord <$> updateWordValue sym m n asBit _ -> bad "Sequence update on a non-sequence." asBit = do res <- v @@ -781,7 +782,7 @@ let lenv' = lenv { leVars = fmap stutter (leVars lenv) } let vs i = do let (q, r) = i `divMod` nLen lookupSeqMap vss q >>= \case - VWord _ w -> VBit <$> indexWordValue sym w r + VWord w -> VBit <$> indexWordValue sym w r VSeq _ xs' -> lookupSeqMap xs' r VStream xs' -> lookupSeqMap xs' r _ -> evalPanic "evalMatch" ["Not a list value"] @@ -795,7 +796,7 @@ let env = EvalEnv (leStatic lenv) (leTypes lenv) xs <- evalExpr sym env expr let vs i = case xs of - VWord _ w -> VBit <$> indexWordValue sym w i + VWord w -> VBit <$> indexWordValue sym w i VSeq _ xs' -> lookupSeqMap xs' i VStream xs' -> lookupSeqMap xs' i _ -> evalPanic "evalMatch" ["Not a list value"] 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 @@ -134,7 +134,7 @@ (TVSeq _ b, VSeq n svs) -> do ses <- traverse (go b) =<< lift (sequence (enumerateSeqMap n svs)) pure $ EList ses (tValTy b) - (TVSeq n TVBit, VWord _ wval) -> + (TVSeq n TVBit, VWord wval) -> do BV _ v <- lift (asWordVal Concrete wval) pure $ ETApp (ETApp (prim "number") (tNum v)) (tWord (tNum n)) @@ -206,7 +206,7 @@ F2.pmult (fromInteger (u+1)) x y else F2.pmult (fromInteger (v+1)) y x - in return . VWord (1+u+v) . wordVal . mkBv (1+u+v) $! z) + in return . VWord . wordVal . mkBv (1+u+v) $! z) , ("pmod", PFinPoly \_u -> @@ -215,7 +215,7 @@ PWordFun \(BV _ m) -> PPrim do assertSideCondition sym (m /= 0) DivideByZero - return . VWord v . wordVal . mkBv v $! F2.pmod (fromInteger w) x m) + return . VWord . wordVal . mkBv v $! F2.pmod (fromInteger w) x m) , ("pdiv", PFinPoly \_u -> @@ -224,7 +224,7 @@ PWordFun \(BV _ m) -> PPrim do assertSideCondition sym (m /= 0) DivideByZero - return . VWord w . wordVal . mkBv w $! F2.pdiv (fromInteger w) x m) + return . VWord . wordVal . mkBv w $! F2.pdiv (fromInteger w) x m) ] @@ -297,9 +297,9 @@ foldM (\st blk -> seq st (SHA.processSHA256Block st <$> (toSHA256Block =<< blk))) SHA.initialSHA224State blks let f :: Word32 -> Eval Value - f = pure . VWord 32 . wordVal . BV 32 . toInteger + f = pure . VWord . wordVal . BV 32 . toInteger zs = finiteSeqMap Concrete (map f [w0,w1,w2,w3,w4,w5,w6]) - seq zs (pure (VSeq 7 zs))) + seq zs (wordSeq Concrete 7 32 zs)) , ("processSHA2_256", {-# SCC "SuiteB::processSHA2_256" #-} PFinPoly \n -> @@ -310,9 +310,9 @@ foldM (\st blk -> seq st (SHA.processSHA256Block st <$> (toSHA256Block =<< blk))) SHA.initialSHA256State blks let f :: Word32 -> Eval Value - f = pure . VWord 32 . wordVal . BV 32 . toInteger + f = pure . VWord . wordVal . BV 32 . toInteger zs = finiteSeqMap Concrete (map f [w0,w1,w2,w3,w4,w5,w6,w7]) - seq zs (pure (VSeq 8 zs))) + seq zs (wordSeq Concrete 8 32 zs)) , ("processSHA2_384", {-# SCC "SuiteB::processSHA2_384" #-} PFinPoly \n -> @@ -323,9 +323,9 @@ foldM (\st blk -> seq st (SHA.processSHA512Block st <$> (toSHA512Block =<< blk))) SHA.initialSHA384State blks let f :: Word64 -> Eval Value - f = pure . VWord 64 . wordVal . BV 64 . toInteger + f = pure . VWord . wordVal . BV 64 . toInteger zs = finiteSeqMap Concrete (map f [w0,w1,w2,w3,w4,w5]) - seq zs (pure (VSeq 6 zs))) + seq zs (wordSeq Concrete 6 64 zs)) , ("processSHA2_512", {-# SCC "SuiteB::processSHA2_512" #-} PFinPoly \n -> @@ -336,9 +336,9 @@ foldM (\st blk -> seq st (SHA.processSHA512Block st <$> (toSHA512Block =<< blk))) SHA.initialSHA512State blks let f :: Word64 -> Eval Value - f = pure . VWord 64 . wordVal . BV 64 . toInteger + f = pure . VWord . wordVal . BV 64 . toInteger zs = finiteSeqMap Concrete (map f [w0,w1,w2,w3,w4,w5,w6,w7]) - seq zs (pure (VSeq 8 zs))) + seq zs (wordSeq Concrete 8 64 zs)) , ("AESKeyExpand", {-# SCC "SuiteB::AESKeyExpand" #-} PFinPoly \k -> @@ -348,11 +348,11 @@ let toWord :: Integer -> Eval Word32 toWord i = fromInteger. bvVal <$> (fromVWord Concrete "AESInfKeyExpand" =<< lookupSeqMap ss i) let fromWord :: Word32 -> Eval Value - fromWord = pure . VWord 32 . wordVal . BV 32 . toInteger + fromWord = pure . VWord . wordVal . BV 32 . toInteger kws <- mapM toWord [0 .. k-1] let ws = AES.keyExpansionWords k kws let len = 4*(k+7) - pure (VSeq len (finiteSeqMap Concrete (map fromWord ws)))) + wordSeq Concrete len 32 (finiteSeqMap Concrete (map fromWord ws))) , ("AESInvMixColumns", {-# SCC "SuiteB::AESInvMixColumns" #-} PFun \st -> @@ -361,10 +361,10 @@ let toWord :: Integer -> Eval Word32 toWord i = fromInteger. bvVal <$> (fromVWord Concrete "AESInvMixColumns" =<< lookupSeqMap ss i) let fromWord :: Word32 -> Eval Value - fromWord = pure . VWord 32 . wordVal . BV 32 . toInteger + fromWord = pure . VWord . wordVal . BV 32 . toInteger ws <- mapM toWord [0,1,2,3] let ws' = AES.invMixColumns ws - pure . VSeq 4 . finiteSeqMap Concrete . map fromWord $ ws') + wordSeq Concrete 4 32 (finiteSeqMap Concrete . map fromWord $ ws')) , ("AESEncRound", {-# SCC "SuiteB::AESEncRound" #-} PFun \st -> @@ -373,10 +373,10 @@ let toWord :: Integer -> Eval Word32 toWord i = fromInteger. bvVal <$> (fromVWord Concrete "AESEncRound" =<< lookupSeqMap ss i) let fromWord :: Word32 -> Eval Value - fromWord = pure . VWord 32 . wordVal . BV 32 . toInteger + fromWord = pure . VWord . wordVal . BV 32 . toInteger ws <- mapM toWord [0,1,2,3] let ws' = AES.aesRound ws - pure . VSeq 4 . finiteSeqMap Concrete . map fromWord $ ws') + wordSeq Concrete 4 32 (finiteSeqMap Concrete . map fromWord $ ws')) , ("AESEncFinalRound", {-# SCC "SuiteB::AESEncFinalRound" #-} PFun \st -> @@ -385,10 +385,10 @@ let toWord :: Integer -> Eval Word32 toWord i = fromInteger. bvVal <$> (fromVWord Concrete "AESEncFinalRound" =<< lookupSeqMap ss i) let fromWord :: Word32 -> Eval Value - fromWord = pure . VWord 32 . wordVal . BV 32 . toInteger + fromWord = pure . VWord . wordVal . BV 32 . toInteger ws <- mapM toWord [0,1,2,3] let ws' = AES.aesFinalRound ws - pure . VSeq 4 . finiteSeqMap Concrete . map fromWord $ ws') + wordSeq Concrete 4 32 (finiteSeqMap Concrete . map fromWord $ ws')) , ("AESDecRound", {-# SCC "SuiteB::AESDecRound" #-} PFun \st -> @@ -397,10 +397,10 @@ let toWord :: Integer -> Eval Word32 toWord i = fromInteger. bvVal <$> (fromVWord Concrete "AESDecRound" =<< lookupSeqMap ss i) let fromWord :: Word32 -> Eval Value - fromWord = pure . VWord 32 . wordVal . BV 32 . toInteger + fromWord = pure . VWord . wordVal . BV 32 . toInteger ws <- mapM toWord [0,1,2,3] let ws' = AES.aesInvRound ws - pure . VSeq 4 . finiteSeqMap Concrete . map fromWord $ ws') + wordSeq Concrete 4 32 . finiteSeqMap Concrete . map fromWord $ ws') , ("AESDecFinalRound", {-# SCC "SuiteB::AESDecFinalRound" #-} PFun \st -> @@ -409,10 +409,10 @@ let toWord :: Integer -> Eval Word32 toWord i = fromInteger. bvVal <$> (fromVWord Concrete "AESDecFinalRound" =<< lookupSeqMap ss i) let fromWord :: Word32 -> Eval Value - fromWord = pure . VWord 32 . wordVal . BV 32 . toInteger + fromWord = pure . VWord . wordVal . BV 32 . toInteger ws <- mapM toWord [0,1,2,3] let ws' = AES.aesInvFinalRound ws - pure . VSeq 4 . finiteSeqMap Concrete . map fromWord $ ws') + wordSeq Concrete 4 32 . finiteSeqMap Concrete . map fromWord $ ws') ] diff --git a/src/Cryptol/Eval/FFI.hs b/src/Cryptol/Eval/FFI.hs --- a/src/Cryptol/Eval/FFI.hs +++ b/src/Cryptol/Eval/FFI.hs @@ -51,6 +51,7 @@ import Cryptol.Eval.Type import Cryptol.Eval.Value import Cryptol.ModuleSystem.Name +import Cryptol.TypeCheck.Solver.InfNat import Cryptol.Utils.Ident import Cryptol.Utils.RecordMap @@ -269,6 +270,14 @@ let totalSize = fromInteger (product sizes) getResult marshal ptr = do getRetAsOutArgs gr [SomeFFIArg ptr] + let tyv = case bt of + FFIBasicVal bv -> case bv of + FFIWord len _ -> TVSeq len TVBit + FFIFloat e p _ -> TVFloat e p + FFIBasicRef br -> case br of + FFIInteger Nothing -> TVInteger + FFIInteger (Just z) -> TVIntMod $ evalFinType z + FFIRational -> TVRational let build (n:ns) !i = do -- We need to be careful to actually run this here and not just @@ -276,8 +285,11 @@ -- will read from the array after it is deallocated. vs <- for [0 .. fromInteger n - 1] \j -> build ns (i * fromInteger n + j) - pure (VSeq n (finiteSeqMap Concrete (map pure vs))) - build [] !i = peekElemOff ptr i >>= runEval stk . marshal + runEval stk $ + mkSeq Concrete (Nat n) tyv (finiteSeqMap Concrete (map pure vs)) + build [] !i = do + e <- peekElemOff ptr i + runEval stk (marshal e) build sizes 0 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 @@ -222,10 +222,12 @@ lw <- fromVWord sym "ringLeft" l rw <- fromVWord sym "ringRight" r stk <- sGetCallStack sym - VWord w . wordVal <$> (sWithCallStack sym stk (opw w lw rw)) - | otherwise -> VSeq w <$> (join (zipSeqMap sym (loop a) (Nat w) <$> - (fromSeq "ringBinary left" l) <*> - (fromSeq "ringBinary right" r))) + VWord . wordVal <$> (sWithCallStack sym stk (opw w lw rw)) + | otherwise -> do + vals <- (join (zipSeqMap sym (loop a) (Nat w) <$> + (fromSeq "ringBinary left" l) <*> + (fromSeq "ringBinary right" r))) + mkSeq sym (Nat w) a vals TVStream a -> -- streams @@ -305,8 +307,10 @@ | isTBit a -> do wx <- fromVWord sym "ringUnary" v stk <- sGetCallStack sym - VWord w . wordVal <$> sWithCallStack sym stk (opw w wx) - | otherwise -> VSeq w <$> (mapSeqMap sym (loop a) (Nat w) =<< fromSeq "ringUnary" v) + VWord . wordVal <$> sWithCallStack sym stk (opw w wx) + | otherwise -> do + vals <- mapSeqMap sym (loop a) (Nat w) =<< fromSeq "ringUnary" v + mkSeq sym (Nat w) a vals TVStream a -> VStream <$> (mapSeqMap sym (loop a) Inf =<< fromSeq "ringUnary" v) @@ -372,10 +376,10 @@ -- words and finite sequences | isTBit a -> do stk <- sGetCallStack sym - VWord w . wordVal <$> sWithCallStack sym stk (opw w) + VWord . wordVal <$> sWithCallStack sym stk (opw w) | otherwise -> do v <- sDelay sym (loop a) - pure $ VSeq w $ indexSeqMap \_i -> v + mkSeq sym (Nat w) a $ indexSeqMap \_i -> v TVStream a -> do v <- sDelay sym (loop a) @@ -417,7 +421,7 @@ do wl <- fromVWord sym "integralBinary left" l wr <- fromVWord sym "integralBinary right" r stk <- sGetCallStack sym - VWord w . wordVal <$> sWithCallStack sym stk (opw w wl wr) + VWord . wordVal <$> sWithCallStack sym stk (opw w wl wr) _ -> evalPanic "integralBinary" [show ty ++ " not int class `Integral`"] @@ -690,25 +694,25 @@ {-# INLINE lg2V #-} lg2V :: Backend sym => sym -> Prim sym lg2V sym = - PFinPoly \w -> + PFinPoly \_w -> PWordFun \x -> - PPrim (VWord w . wordVal <$> wordLg2 sym x) + PPrim (VWord . wordVal <$> wordLg2 sym x) {-# SPECIALIZE sdivV :: Concrete -> Prim Concrete #-} sdivV :: Backend sym => sym -> Prim sym sdivV sym = - PFinPoly \w -> + PFinPoly \_w -> PWordFun \x -> PWordFun \y -> - PPrim (VWord w . wordVal <$> wordSignedDiv sym x y) + PPrim (VWord . wordVal <$> wordSignedDiv sym x y) {-# SPECIALIZE smodV :: Concrete -> Prim Concrete #-} smodV :: Backend sym => sym -> Prim sym smodV sym = - PFinPoly \w -> + PFinPoly \_w -> PWordFun \x -> PWordFun \y -> - PPrim (VWord w . wordVal <$> wordSignedMod sym x y) + PPrim (VWord . wordVal <$> wordSignedMod sym x y) {-# SPECIALIZE toSignedIntegerV :: Concrete -> Prim Concrete #-} toSignedIntegerV :: Backend sym => sym -> Prim sym @@ -920,7 +924,7 @@ | isTBit ety -> word sym w 0 | otherwise -> do z <- sDelay sym (zeroV sym ety) - pure $ VSeq w (indexSeqMap \_i -> z) + mkSeq sym (Nat w) ety (indexSeqMap \_i -> z) TVStream ety -> do z <- sDelay sym (zeroV sym ety) @@ -969,7 +973,7 @@ joinSeq sym (Nat parts) each TVBit val = do w <- delayWordValue sym (parts*each) (joinWords sym parts each . fmap (fromWordVal "joinV") =<< val) - pure (VWord (parts*each) w) + pure (VWord w) -- infinite sequence of words joinSeq sym Inf each TVBit val @@ -980,19 +984,15 @@ VBit <$> indexWordValue sym ys r -- finite or infinite sequence of non-words -joinSeq _sym parts each _a val - = return $ vSeq $ indexSeqMap $ \i -> do +joinSeq sym parts each a val + = mkSeq sym len a $ indexSeqMap $ \i -> do let (q,r) = divMod i each xs <- val ys <- fromSeq "join seq" =<< lookupSeqMap xs q lookupSeqMap ys r where len = parts `nMul` (Nat each) - vSeq = case len of - Inf -> VStream - Nat n -> VSeq n - {-# INLINE joinV #-} -- | Join a sequence of sequences into a single sequence. @@ -1024,15 +1024,15 @@ case back of Nat back' | isTBit a -> do w <- delayWordValue sym front' (takeWordVal sym front' back' =<< (fromWordVal "takeV" <$> val)) - pure (VWord front' w) + pure (VWord w) Inf | isTBit a -> do w <- delayWordValue sym front' (bitmapWordVal sym front' . fmap fromVBit =<< (fromSeq "takeV" =<< val)) - pure (VWord front' w) + pure (VWord w) _ -> do xs <- delaySeqMap sym (fromSeq "takeV" =<< val) - pure (VSeq front' xs) + mkSeq sym (Nat front') a xs {-# INLINE dropV #-} dropV :: @@ -1047,7 +1047,7 @@ case back of Nat back' | isTBit a -> do w <- delayWordValue sym back' (dropWordVal sym front back' =<< (fromWordVal "dropV" <$> val)) - pure (VWord back' w) + pure (VWord w) _ -> do xs <- delaySeqMap sym (dropSeqMap front <$> (fromSeq "dropV" =<< val)) @@ -1065,32 +1065,49 @@ SEval sym (GenValue sym) -> SEval sym (GenValue sym) splitV sym parts each a val = - case (parts, each) of - (Nat p, e) | isTBit a -> do - val' <- sDelay sym (fromWordVal "splitV" <$> val) - return $ VSeq p $ indexSeqMap $ \i -> - VWord e <$> (extractWordVal sym e ((p-i-1)*e) =<< val') - (Inf, e) | isTBit a -> do - val' <- sDelay sym (fromSeq "splitV" =<< val) - return $ VStream $ indexSeqMap $ \i -> - VWord e <$> bitmapWordVal sym e (indexSeqMap $ \j -> - let idx = i*e + toInteger j - in idx `seq` do - xs <- val' - fromVBit <$> lookupSeqMap xs idx) - (Nat p, e) -> do - val' <- sDelay sym (fromSeq "splitV" =<< val) - return $ VSeq p $ indexSeqMap $ \i -> - return $ VSeq e $ indexSeqMap $ \j -> do - xs <- val' - lookupSeqMap xs (e * i + j) - (Inf , e) -> do - val' <- sDelay sym (fromSeq "splitV" =<< val) - return $ VStream $ indexSeqMap $ \i -> - return $ VSeq e $ indexSeqMap $ \j -> do + case parts of + Nat p + | isTBit a -> + do val' <- sDelay sym (fromWordVal "splitV" <$> val) + mkSeq sym (Nat p) tyv $ indexSeqMap $ \i -> + VWord <$> (extractWordVal sym each ((p-i-1)*each) =<< val') + | otherwise -> + do val' <- sDelay sym (fromSeq "splitV" =<< val) + mkSeq sym (Nat p) tyv $ indexSeqMap $ \i -> + mkSeq sym (Nat each) a $ indexSeqMap $ \j -> do xs <- val' - lookupSeqMap xs (e * i + j) + lookupSeqMap xs (each * i + j) + Inf + -- The return type is [inf][each], (where each is non-zero) and `val` is + -- of type [inf * each], or [inf]. Therefore, `val` is a stream. + | isTBit a, each /= 0 -> + do val' <- sDelay sym (fromSeq "splitV" =<< val) + return $ VStream $ indexSeqMap $ \i -> + VWord <$> bitmapWordVal sym each (indexSeqMap $ \j -> + let idx = i*each + toInteger j + in idx `seq` do + xs <- val' + fromVBit <$> lookupSeqMap xs idx) + -- The return type is [inf][0], and `val` is of type [inf * 0], or [0]. + -- Therefore, `val` is a word. We need to special-case this, because the + -- case directly above this one will panic if `val` is not a stream due to + -- the use of `fromSeq` (#1749). + -- + -- Because `val` is an empty sequence, there is no need to split it apart. + -- Instead, we can just return a stream with infinite copies of `val`. + | isTBit a, each == 0 -> + return $ VStream $ indexSeqMap $ \_i -> val + -- If `a` is not `Bit`, then `val` must be a sequence or a stream (and not + -- a word). + | otherwise -> + do val' <- sDelay sym (fromSeq "splitV" =<< val) + return $ VStream $ indexSeqMap $ \i -> + mkSeq sym (Nat each) a $ indexSeqMap $ \j -> do + xs <- val' + lookupSeqMap xs (each * i + j) + where + tyv = TVSeq each TVBit {-# INLINE reverseV #-} @@ -1104,11 +1121,11 @@ reverseV sym n TVBit val = do w <- delayWordValue sym n (reverseWordVal sym . fromWordVal "reverseV" =<< val) - pure (VWord n w) + pure (VWord w) -reverseV sym n _a val = +reverseV sym n a val = do xs <- delaySeqMap sym (reverseSeqMap n <$> (fromSeq "reverseV" =<< val)) - pure (VSeq n xs) + mkSeq sym (Nat n) a xs {-# INLINE transposeV #-} @@ -1123,42 +1140,38 @@ SEval sym (GenValue sym) transposeV sym a b c xs | isTBit c, Nat na <- a = -- Fin a => [a][b]Bit -> [b][a]Bit - return $ bseq $ indexSeqMap $ \bi -> - VWord na <$> bitmapWordVal sym na (indexSeqMap $ \ai -> + bseq $ indexSeqMap $ \bi -> + VWord <$> bitmapWordVal sym na (indexSeqMap $ \ai -> do xs' <- fromSeq "transposeV" xs ys <- lookupSeqMap xs' ai case ys of VStream ys' -> fromVBit <$> lookupSeqMap ys' bi - VWord _ wv -> indexWordValue sym wv bi + VWord wv -> indexWordValue sym wv bi _ -> evalPanic "transpose" ["expected sequence of bits"]) | isTBit c, Inf <- a = -- [inf][b]Bit -> [b][inf]Bit - return $ bseq $ indexSeqMap $ \bi -> + bseq $ indexSeqMap $ \bi -> return $ VStream $ indexSeqMap $ \ai -> do xs' <- fromSeq "transposeV" xs ys <- lookupSeqMap xs' ai case ys of VStream ys' -> lookupSeqMap ys' bi - VWord _ wv -> VBit <$> indexWordValue sym wv bi + VWord wv -> VBit <$> indexWordValue sym wv bi _ -> evalPanic "transpose" ["expected sequence of bits"] | otherwise = -- [a][b]c -> [b][a]c - return $ bseq $ indexSeqMap $ \bi -> - return $ aseq $ indexSeqMap $ \ai -> do + bseq $ indexSeqMap $ \bi -> + aseq $ indexSeqMap $ \ai -> do xs' <- fromSeq "transposeV 1" xs ys <- fromSeq "transposeV 2" =<< lookupSeqMap xs' ai z <- lookupSeqMap ys bi return z where - bseq = - case b of - Nat nb -> VSeq nb - Inf -> VStream - aseq = - case a of - Nat na -> VSeq na - Inf -> VStream + bseq = case b of + Nat n -> mkSeq sym b (TVSeq n c) + Inf -> mkSeq sym b (TVStream c) + aseq = mkSeq sym a c {-# INLINE ccatV #-} @@ -1179,10 +1192,10 @@ mr <- isReady sym r case (ml, mr) of (Just l', Just r') -> - VWord (front+back) <$> + VWord <$> joinWordVal sym (fromWordVal "ccatV left" l') (fromWordVal "ccatV right" r') _ -> - VWord (front+back) <$> delayWordValue sym (front+back) + VWord <$> delayWordValue sym (front+back) (do l' <- fromWordVal "ccatV left" <$> l r' <- fromWordVal "ccatV right" <$> r joinWordVal sym l' r') @@ -1250,17 +1263,19 @@ TVSeq w aty -- words | isTBit aty - -> VWord w <$> delayWordValue sym w + -> VWord <$> delayWordValue sym w (wordValLogicOp sym opb opw (fromWordVal "logicBinary l" l) (fromWordVal "logicBinary r" r)) -- finite sequences - | otherwise -> VSeq w <$> - (join (zipSeqMap sym (loop aty) (Nat w) <$> - (fromSeq "logicBinary left" l) - <*> (fromSeq "logicBinary right" r))) + | otherwise -> do + vals <- join (zipSeqMap sym (loop aty) (Nat w) <$> + (fromSeq "logicBinary left" l) + <*> (fromSeq "logicBinary right" r)) + mkSeq sym (Nat w) aty vals + TVStream aty -> VStream <$> (join (zipSeqMap sym (loop aty) Inf <$> (fromSeq "logicBinary left" l) <*> @@ -1314,11 +1329,11 @@ TVSeq w ety -- words | isTBit ety - -> VWord w <$> delayWordValue sym w (wordValUnaryOp sym opb opw (fromWordVal "logicUnary" val)) + -> VWord <$> delayWordValue sym w (wordValUnaryOp sym opb opw (fromWordVal "logicUnary" val)) -- finite sequences | otherwise - -> VSeq w <$> (mapSeqMap sym (loop ety) (Nat w) =<< fromSeq "logicUnary" val) + -> mkSeq sym (Nat w) ety =<< (mapSeqMap sym (loop ety) (Nat w) =<< fromSeq "logicUnary" val) -- streams TVStream ety -> @@ -1388,7 +1403,7 @@ PFun \idx -> PPrim do vs <- xs >>= \case - VWord _ w -> return $ indexSeqMap (\i -> VBit <$> indexWordValue sym w i) + VWord w -> return $ indexSeqMap (\i -> VBit <$> indexWordValue sym w i) VSeq _ vs -> return vs VStream vs -> return vs _ -> evalPanic "Expected sequence value" ["indexPrim"] @@ -1421,9 +1436,9 @@ do idx' <- asIndex sym "update" ix <$> idx assertIndexInBounds sym len idx' case (len, eltTy) of - (Nat n, TVBit) -> VWord n <$> delayWordValue sym n + (Nat n, TVBit) -> VWord <$> delayWordValue sym n (do w <- fromWordVal "updatePrim" <$> xs; updateWord len eltTy w idx' val) - (Nat n, _ ) -> VSeq n <$> delaySeqMap sym + (Nat n, _ ) -> mkSeq sym (Nat n) eltTy =<< delaySeqMap sym (do vs <- fromSeq "updatePrim" =<< xs; updateSeq len eltTy vs idx' val) (Inf , _ ) -> VStream <$> delaySeqMap sym (do vs <- fromSeq "updatePrim" =<< xs; updateSeq len eltTy vs idx' val) @@ -1644,8 +1659,8 @@ SEval sym (GenValue sym) intShifter sym nm wop reindex m a xs idx = case xs of - VWord w x -> VWord w <$> shiftWordByInteger sym wop (reindex m) x idx - VSeq w vs -> VSeq w <$> shiftSeqByInteger sym (mergeValue sym) (reindex m) (zeroV sym a) m vs idx + VWord x -> VWord <$> shiftWordByInteger sym wop (reindex m) x idx + VSeq w vs -> mkSeq sym (Nat w) a =<< shiftSeqByInteger sym (mergeValue sym) (reindex m) (zeroV sym a) m vs idx VStream vs -> VStream <$> shiftSeqByInteger sym (mergeValue sym) (reindex m) (zeroV sym a) m vs idx _ -> evalPanic "expected sequence value in shift operation" [nm] @@ -1663,8 +1678,8 @@ SEval sym (GenValue sym) wordShifter sym nm wop reindex m a xs idx = case xs of - VWord w x -> VWord w <$> shiftWordByWord sym wop (reindex m) x idx - VSeq w vs -> VSeq w <$> shiftSeqByWord sym (mergeValue sym) (reindex m) (zeroV sym a) (Nat w) vs idx + VWord x -> VWord <$> shiftWordByWord sym wop (reindex m) x idx + VSeq w vs -> mkSeq sym (Nat w) a =<< shiftSeqByWord sym (mergeValue sym) (reindex m) (zeroV sym a) (Nat w) vs idx VStream vs -> VStream <$> shiftSeqByWord sym (mergeValue sym) (reindex m) (zeroV sym a) Inf vs idx _ -> evalPanic "expected sequence value in shift operation" [nm] @@ -1697,7 +1712,7 @@ case asIndex sym ">>$" ix y of Left i -> do pneg <- intLessThan sym i =<< integerLit sym 0 - VWord n <$> mergeWord' sym + VWord <$> mergeWord' sym pneg (do i' <- shiftShrink sym (Nat n) ix =<< intNegate sym i amt <- wordFromInt sym n i' @@ -1708,7 +1723,7 @@ Right wv -> do amt <- asWordVal sym wv - VWord n . wordVal <$> wordSignedShiftRight sym x amt + VWord . wordVal <$> wordSignedShiftRight sym x amt -- Miscellaneous --------------------------------------------------------------- @@ -1734,7 +1749,7 @@ -- and return the associated character, if it is concrete. -- Otherwise, return a '?' character valueToChar :: Backend sym => sym -> GenValue sym -> SEval sym Char -valueToChar sym (VWord 8 wval) = +valueToChar sym (VWord wval) | wordValWidth wval == 8 = do w <- asWordVal sym wval pure $! fromMaybe '?' (wordAsChar sym w) valueToChar _ _ = evalPanic "valueToChar" ["Not an 8-bit bitvector"] @@ -1756,8 +1771,8 @@ PStrict \v -> PPrim case v of - VSeq n m -> go0 f z (enumerateSeqMap n m) - VWord _n wv -> go0 f z . map (pure . VBit) =<< (enumerateWordValue sym wv) + VSeq n m -> go0 f z (enumerateSeqMap n m) + VWord wv -> go0 f z . map (pure . VBit) =<< (enumerateWordValue sym wv) _ -> panic "Cryptol.Eval.Generic.foldlV" ["Expected finite sequence"] where go0 _f a [] = a @@ -1781,7 +1796,7 @@ PPrim case v of VSeq n m -> go0 f z (enumerateSeqMap n m) - VWord _n wv -> go0 f z . map (pure . VBit) =<< (enumerateWordValue sym wv) + VWord wv -> go0 f z . map (pure . VBit) =<< (enumerateWordValue sym wv) _ -> panic "Cryptol.Eval.Generic.foldlV" ["Expected finite sequence"] where go0 _f a [] = a @@ -1811,7 +1826,7 @@ PPrim do sm <- case v of VSeq _ m -> scan n f z m - VWord _ wv -> scan n f z (VBit <$> asBitsMap sym wv) + VWord wv -> scan n f z (VBit <$> asBitsMap sym wv) VStream m -> scan n f z m _ -> panic "Cryptol.Eval.Generic.scanlV" ["Expected sequence"] mkSeq sym (nAdd (Nat 1) n) a sm @@ -1869,7 +1884,7 @@ xs' <- xs m <- case xs' of - VWord _n w -> + VWord w -> let m = asBitsMap sym w in sparkParMap sym (\x -> f' (VBit <$> x)) n m VSeq _n m -> @@ -1938,8 +1953,8 @@ , "fpPosInf" ~> fpConst (fpPosInf sym) , "fpFromBits" ~> PFinPoly \e -> PFinPoly \p -> PWordFun \w -> PPrim (VFloat <$> fpFromBits sym e p w) - , "fpToBits" ~> PFinPoly \e -> PFinPoly \p -> PFloatFun \x -> PPrim - (VWord (e+p) . wordVal <$> fpToBits sym x) + , "fpToBits" ~> PFinPoly \_e -> PFinPoly \_p -> PFloatFun \x -> PPrim + (VWord . wordVal <$> fpToBits sym x) , "=.=" ~> PFinPoly \_ -> PFinPoly \_ -> PFloatFun \x -> PFloatFun \y -> PPrim (VBit <$> fpLogicalEq sym x y) diff --git a/src/Cryptol/Eval/Reference.lhs b/src/Cryptol/Eval/Reference.lhs --- a/src/Cryptol/Eval/Reference.lhs +++ b/src/Cryptol/Eval/Reference.lhs @@ -247,7 +247,28 @@ > where > g (Nat n) = f n > g Inf = evalPanic "vFinPoly" ["Expected finite numeric type"] - +> +> -- | Reduce a value to normal form. +> forceValue :: Value -> E () +> forceValue v = +> case v of +> -- Values where the field is already is normal form +> VBit{} -> pure () +> VInteger{} -> pure () +> VRational{} -> pure () +> VFloat{} -> pure () +> -- Values with fields containing other values to reduce to normal form +> VList _ xs -> forceValues xs +> VTuple xs -> forceValues xs +> VRecord fs -> forceValues $ map snd fs +> VEnum _ xs -> forceValues xs +> -- Lambdas and other abstractions are already in normal form +> VFun{} -> pure () +> VPoly{} -> pure () +> VNumPoly{} -> pure () +> where +> forceValues :: [E Value] -> E () +> forceValues = mapM_ (\x -> forceValue =<< x) Environments ------------ @@ -758,6 +779,10 @@ > , "lg2" ~> vFinPoly $ \n -> pure $ > VFun $ \v -> > vWord n <$> appOp1 lg2Wrap (fromVWord =<< v) +> , "toSignedInteger" +> ~> vFinPoly $ \_n -> pure $ +> VFun $ \x -> +> VInteger <$> (fromSignedVWord =<< x) > -- Rational > , "ratio" ~> VFun $ \l -> pure $ > VFun $ \r -> @@ -943,6 +968,13 @@ > -- Note: the reference implementation simply > -- executes parmap sequentially > pure $ VList n (map f' xs') +> +> , "deepseq" ~> VPoly $ \_a -> pure $ +> VPoly $ \_b -> pure $ +> VFun $ \x -> pure $ +> VFun $ \y -> +> do forceValue =<< x +> y > > , "error" ~> VPoly $ \_a -> pure $ > VNumPoly $ \_ -> pure $ diff --git a/src/Cryptol/Eval/SBV.hs b/src/Cryptol/Eval/SBV.hs --- a/src/Cryptol/Eval/SBV.hs +++ b/src/Cryptol/Eval/SBV.hs @@ -81,7 +81,7 @@ asWordList sym wvs >>= \case Just ws -> do z <- wordLit sym wlen 0 - return $ VWord wlen $ wordVal $ SBV.svSelect ws z idx + return $ VWord $ wordVal $ SBV.svSelect ws z idx Nothing -> folded' | otherwise = folded' 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 @@ -17,6 +17,7 @@ {-# LANGUAGE LambdaCase #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE PatternGuards #-} +{-# LANGUAGE PatternSynonyms #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE TupleSections #-} @@ -25,7 +26,15 @@ module Cryptol.Eval.Value ( -- * GenericValue - GenValue(..), ConValue + GenValue + (VRecord, VTuple + , VEnum, VBit + , VInteger, VRational + , VFloat, VWord + , VStream, VFun + , VPoly, VNumPoly + , VSeq) -- pattern synonym + , ConValue , forceValue , Backend(..) , asciiMode @@ -38,7 +47,12 @@ , tlam , nlam , ilam + , FinSeq + , toFinSeq + , unsafeToFinSeq + , finSeq , mkSeq + , wordSeq -- ** Value eliminators , fromVBit , fromVInteger @@ -122,15 +136,29 @@ | VInteger !(SInteger sym) -- ^ @ Integer @ or @ Z n @ | VRational !(SRational sym) -- ^ @ Rational @ | VFloat !(SFloat sym) - | VSeq !Integer !(SeqMap sym (GenValue sym)) -- ^ @ [n]a @ - -- Invariant: VSeq is never a sequence of bits - | VWord !Integer !(WordValue sym) -- ^ @ [n]Bit @ + | VSeqCtor !Integer !(SeqMap sym (GenValue sym)) -- ^ @ [n]a @ + -- Invariant: VSeqCtor is never a sequence of bits + -- This constructor is intentionally not exported + -- to preserve the invariant. Use smart constructors + -- such as 'mkSeq' or 'finSeq' instead. + | VWord !(WordValue sym) -- ^ @ [n]Bit @ | VStream !(SeqMap sym (GenValue sym)) -- ^ @ [inf]a @ | VFun CallStack (SEval sym (GenValue sym) -> SEval sym (GenValue sym)) -- ^ functions | VPoly CallStack (TValue -> SEval sym (GenValue sym)) -- ^ polymorphic values (kind *) | VNumPoly CallStack (Nat' -> SEval sym (GenValue sym)) -- ^ polymorphic values (kind #) deriving Generic +-- | A view-only pattern for deconstructing finite sequences. Use +-- 'mkSeq' or 'finSeq' for construction. +pattern VSeq :: Integer -> SeqMap sym (GenValue sym) -> GenValue sym +pattern VSeq len vals <- VSeqCtor len vals + +-- This is all GenValue constructors except for VSeqCtor, which +-- is instead swapped for the view-only VSeq pattern +{-# COMPLETE VRecord, VTuple, VEnum, VBit, VInteger, + VRational, VFloat, VWord, VStream, + VFun, VPoly, VNumPoly, VSeq #-} + type ConValue sym = ConInfo (SEval sym (GenValue sym)) -- | Force the evaluation of a value @@ -144,7 +172,7 @@ VInteger i -> seq i (return ()) VRational q -> seq q (return ()) VFloat f -> seq f (return ()) - VWord _ wv -> forceWordValue wv + VWord wv -> forceWordValue wv VStream _ -> return () VFun{} -> return () VPoly{} -> return () @@ -153,7 +181,7 @@ forceConValue :: Backend sym => ConValue sym -> SEval sym () forceConValue (ConInfo i vs) = i `seq` mapM_ (forceValue =<<) vs -instance Show (GenValue sym) where +instance Backend sym => Show (GenValue sym) where show v = case v of VRecord fs -> "record:" ++ show (displayOrder fs) VTuple xs -> "tuple:" ++ show (length xs) @@ -163,7 +191,7 @@ VRational _ -> "rational" VFloat _ -> "float" VSeq n _ -> "seq:" ++ show n - VWord n _ -> "word:" ++ show n + VWord wv -> "word:" ++ show (wordValWidth wv) VStream _ -> "stream" VFun{} -> "fun" VPoly{} -> "poly" @@ -202,7 +230,7 @@ VRational q -> ppSRational x q VFloat i -> ppSFloat x opts i VSeq sz vals -> ppWordSeq sz vals - VWord _ wv -> ppWordVal wv + VWord wv -> ppWordVal wv VStream vals -> do vals' <- traverse (>>=loop 0) $ enumerateSeqMap (useInfLength opts) vals return $ ppList ( vals' ++ [text "..."] ) VFun{} -> return $ text "" @@ -342,7 +370,7 @@ word :: Backend sym => sym -> Integer -> Integer -> SEval sym (GenValue sym) word sym n i | n >= Arch.maxBigIntWidth = wordTooWide n - | otherwise = VWord n . wordVal <$> wordLit sym n i + | otherwise = VWord . wordVal <$> wordLit sym n i -- | Construct a function value @@ -369,38 +397,77 @@ Nat i -> f i Inf -> panic "ilam" [ "Unexpected `inf`" ]) +-- | A finite sequence of non-VBit values. Used in 'finSeq' to +-- safely construct a 'VSeq'. +newtype FinSeq sym = FinSeq [SEval sym (GenValue sym)] + +-- | Safely wrap a 'GenValue' list as a 'FinSeq'. Returns 'Nothing' +-- if any values are a 'VBit'. +toFinSeq :: Backend sym => [GenValue sym] -> Maybe (FinSeq sym) +toFinSeq xs = FinSeq <$> mapM go xs + where + go x = case x of + VBit _ -> Nothing + _ -> Just (pure x) + +-- | Wrap a 'GenValue' thunk list as a 'FinSeq'. Any 'VBit' elements +-- will raise an runtime error when evaluated. +unsafeToFinSeq :: Backend sym => [SEval sym (GenValue sym)] -> FinSeq sym +unsafeToFinSeq xs = FinSeq (map go xs) + where + go f = f >>= \x -> case x of + VBit _ -> evalPanic "unsafeToFinSeq" [ "Unexpected `VBit`", show x ] + _ -> pure x + +-- | Construct a finite sequence from a 'FinSeq'. In contrast to +-- 'mkSeq' this is a pure function. See 'toFinSeq' or 'unsafeToFinSeq' +-- for creating a 'FinSeq' from a list of values. +finSeq :: Backend sym => sym -> Integer -> FinSeq sym -> GenValue sym +finSeq sym len (FinSeq vs) = VSeqCtor len (finiteSeqMap sym vs) + -- | Construct either a finite sequence, or a stream. In the finite case, -- record whether or not the elements were bits, to aid pretty-printing. mkSeq :: Backend sym => sym -> Nat' -> TValue -> SeqMap sym (GenValue sym) -> SEval sym (GenValue sym) mkSeq sym len elty vals = case len of Nat n - | isTBit elty -> VWord n <$> bitmapWordVal sym n (fromVBit <$> vals) - | otherwise -> pure $ VSeq n vals + | isTBit elty -> VWord <$> bitmapWordVal sym n (fromVBit <$> vals) + | otherwise -> pure $ VSeqCtor n vals Inf -> pure $ VStream vals +-- | Construct a finite sequence of word values. +wordSeq :: + Backend sym => + sym -> + -- | The length of the sequence. + Integer -> + -- | The word size of the element type. + Integer -> + SeqMap sym (GenValue sym) -> + SEval sym (GenValue sym) +wordSeq sym n w vals = mkSeq sym (Nat n) (TVSeq w TVBit) vals -- Value Destructors ----------------------------------------------------------- -- | Extract a bit value. -fromVBit :: GenValue sym -> SBit sym +fromVBit :: Backend sym => GenValue sym -> SBit sym fromVBit val = case val of VBit b -> b _ -> evalPanic "fromVBit" ["not a Bit", show val] -- | Extract an integer value. -fromVInteger :: GenValue sym -> SInteger sym +fromVInteger :: Backend sym => GenValue sym -> SInteger sym fromVInteger val = case val of VInteger i -> i _ -> evalPanic "fromVInteger" ["not an Integer", show val] -- | Extract a rational value. -fromVRational :: GenValue sym -> SRational sym +fromVRational :: Backend sym => GenValue sym -> SRational sym fromVRational val = case val of VRational q -> q _ -> evalPanic "fromVRational" ["not a Rational", show val] -- | Extract a finite sequence value. -fromVSeq :: GenValue sym -> SeqMap sym (GenValue sym) +fromVSeq :: Backend sym => GenValue sym -> SeqMap sym (GenValue sym) fromVSeq val = case val of VSeq _ vs -> vs _ -> evalPanic "fromVSeq" ["not a sequence", show val] @@ -413,24 +480,24 @@ _ -> evalPanic "fromSeq" ["not a sequence", msg, show val] fromWordVal :: Backend sym => String -> GenValue sym -> WordValue sym -fromWordVal _msg (VWord _ wval) = wval +fromWordVal _msg (VWord wval) = wval fromWordVal msg val = evalPanic "fromWordVal" ["not a word value", msg, show val] asIndex :: Backend sym => sym -> String -> TValue -> GenValue sym -> Either (SInteger sym) (WordValue sym) asIndex _sym _msg TVInteger (VInteger i) = Left i -asIndex _sym _msg _ (VWord _ wval) = Right wval +asIndex _sym _msg _ (VWord wval) = Right wval asIndex _sym msg _ val = evalPanic "asIndex" ["not an index value", msg, show val] -- | Extract a packed word. fromVWord :: Backend sym => sym -> String -> GenValue sym -> SEval sym (SWord sym) -fromVWord sym _msg (VWord _ wval) = asWordVal sym wval +fromVWord sym _msg (VWord wval) = asWordVal sym wval fromVWord _ msg val = evalPanic "fromVWord" ["not a word", msg, show val] vWordLen :: Backend sym => GenValue sym -> Maybe Integer vWordLen val = case val of - VWord n _wv -> Just n - _ -> Nothing + VWord wv -> Just (wordValWidth wv) + _ -> Nothing -- | If the given list of values are all fully-evaluated thunks -- containing bits, return a packed word built from the same bits. @@ -466,31 +533,31 @@ _ -> evalPanic "fromVNumPoly" ["not a polymorphic value", show val] -- | Extract a tuple from a value. -fromVTuple :: GenValue sym -> [SEval sym (GenValue sym)] +fromVTuple :: Backend sym => GenValue sym -> [SEval sym (GenValue sym)] fromVTuple val = case val of VTuple vs -> vs _ -> evalPanic "fromVTuple" ["not a tuple", show val] -- | Extract a record from a value. -fromVRecord :: GenValue sym -> RecordMap Ident (SEval sym (GenValue sym)) +fromVRecord :: Backend sym => GenValue sym -> RecordMap Ident (SEval sym (GenValue sym)) fromVRecord val = case val of VRecord fs -> fs _ -> evalPanic "fromVRecord" ["not a record", show val] -fromVEnum :: GenValue sym -> (SInteger sym, IntMap (ConValue sym)) +fromVEnum :: Backend sym => GenValue sym -> (SInteger sym, IntMap (ConValue sym)) fromVEnum val = case val of VEnum c xs -> (c,xs) _ -> evalPanic "fromVEnum" ["not an enum", show val] -fromVFloat :: GenValue sym -> SFloat sym +fromVFloat :: Backend sym => GenValue sym -> SFloat sym fromVFloat val = case val of VFloat x -> x _ -> evalPanic "fromVFloat" ["not a Float", show val] -- | Lookup a field in a record. -lookupRecord :: Ident -> GenValue sym -> SEval sym (GenValue sym) +lookupRecord :: Backend sym => Ident -> GenValue sym -> SEval sym (GenValue sym) lookupRecord f val = case lookupField f (fromVRecord val) of Just x -> x @@ -581,8 +648,8 @@ (VInteger i1 , VInteger i2 ) -> VInteger <$> iteInteger sym c i1 i2 (VRational q1, VRational q2) -> VRational <$> iteRational sym c q1 q2 (VFloat f1 , VFloat f2) -> VFloat <$> iteFloat sym c f1 f2 - (VWord n1 w1 , VWord n2 w2 ) | n1 == n2 -> VWord n1 <$> mergeWord sym c w1 w2 - (VSeq n1 vs1 , VSeq n2 vs2 ) | n1 == n2 -> VSeq n1 <$> memoMap sym (Nat n1) (mergeSeqMapVal sym c vs1 vs2) + (VWord w1 , VWord w2 ) | wordValWidth w1 == wordValWidth w2 -> VWord <$> mergeWord sym c w1 w2 + (VSeqCtor n1 vs1 , VSeqCtor n2 vs2 ) | n1 == n2 -> VSeqCtor n1 <$> memoMap sym (Nat n1) (mergeSeqMapVal sym c vs1 vs2) (VStream vs1 , VStream vs2 ) -> VStream <$> memoMap sym Inf (mergeSeqMapVal sym c vs1 vs2) (f1@VFun{} , f2@VFun{} ) -> lam sym $ \x -> mergeValue' sym c (fromVFun sym f1 x) (fromVFun sym f2 x) (f1@VPoly{} , f2@VPoly{} ) -> tlam sym $ \x -> mergeValue' sym c (fromVPoly sym f1 x) (fromVPoly sym f2 x) diff --git a/src/Cryptol/Eval/What4.hs b/src/Cryptol/Eval/What4.hs --- a/src/Cryptol/Eval/What4.hs +++ b/src/Cryptol/Eval/What4.hs @@ -222,7 +222,7 @@ fn <- liftIO $ getUninterpFn sym ("AESKeyExpand" <> Text.pack (show k)) args (W4.BaseStructRepr ret) z <- liftIO $ W4.applySymFn (w4 sym) fn ws -- compute a sequence that projects the relevant fields from the outout tuple - pure $ VSeq (4*(k+7)) $ indexSeqMap $ \i -> + wordSeq sym (4*(k+7)) 32 $ indexSeqMap $ \i -> case intIndex (fromInteger i) (size ret) of Just (Some idx) | Just W4.Refl <- W4.testEquality (ret!idx) (W4.BaseBVRepr (W4.knownNat @32)) -> fromWord32 =<< liftIO (W4.structField (w4 sym) z idx) @@ -237,7 +237,7 @@ addUninterpWarning sym "SHA-224" initSt <- liftIO (mkSHA256InitialState sym SHA.initialSHA224State) finalSt <- foldM (\st blk -> processSHA256Block sym st =<< blk) initSt blks - pure $ VSeq 7 $ indexSeqMap \i -> + wordSeq sym 7 32 $ indexSeqMap \i -> case intIndex (fromInteger i) (knownSize :: Size SHA256State) of Just (Some idx) -> do z <- liftIO $ W4.structField (w4 sym) finalSt idx @@ -255,7 +255,7 @@ addUninterpWarning sym "SHA-256" initSt <- liftIO (mkSHA256InitialState sym SHA.initialSHA256State) finalSt <- foldM (\st blk -> processSHA256Block sym st =<< blk) initSt blks - pure $ VSeq 8 $ indexSeqMap \i -> + wordSeq sym 8 32 $ indexSeqMap \i -> case intIndex (fromInteger i) (knownSize :: Size SHA256State) of Just (Some idx) -> do z <- liftIO $ W4.structField (w4 sym) finalSt idx @@ -273,7 +273,7 @@ addUninterpWarning sym "SHA-384" initSt <- liftIO (mkSHA512InitialState sym SHA.initialSHA384State) finalSt <- foldM (\st blk -> processSHA512Block sym st =<< blk) initSt blks - pure $ VSeq 6 $ indexSeqMap \i -> + wordSeq sym 6 64 $ indexSeqMap \i -> case intIndex (fromInteger i) (knownSize :: Size SHA512State) of Just (Some idx) -> do z <- liftIO $ W4.structField (w4 sym) finalSt idx @@ -291,7 +291,7 @@ addUninterpWarning sym "SHA-512" initSt <- liftIO (mkSHA512InitialState sym SHA.initialSHA512State) finalSt <- foldM (\st blk -> processSHA512Block sym st =<< blk) initSt blks - pure $ VSeq 8 $ indexSeqMap \i -> + wordSeq sym 8 64 $ indexSeqMap \i -> case intIndex (fromInteger i) (knownSize :: Size SHA512State) of Just (Some idx) -> do z <- liftIO $ W4.structField (w4 sym) finalSt idx @@ -454,7 +454,7 @@ _ -> panic nm ["Unexpected word size", show (SW.bvWidth x)] fromWord32 :: W4.IsSymExprBuilder sym => W4.SymBV sym 32 -> SEval (What4 sym) (Value sym) -fromWord32 = pure . VWord 32 . wordVal . SW.DBV +fromWord32 = pure . VWord . wordVal . SW.DBV toWord64 :: W4.IsSymExprBuilder sym => What4 sym -> String -> SeqMap (What4 sym) (GenValue (What4 sym)) -> Integer -> SEval (What4 sym) (W4.SymBV sym 64) @@ -465,7 +465,7 @@ _ -> panic nm ["Unexpected word size", show (SW.bvWidth x)] fromWord64 :: W4.IsSymExprBuilder sym => W4.SymBV sym 64 -> SEval (What4 sym) (Value sym) -fromWord64 = pure . VWord 64 . wordVal . SW.DBV +fromWord64 = pure . VWord . wordVal . SW.DBV @@ -482,7 +482,7 @@ w3 <- toWord32 sym nm ss 3 fn <- liftIO $ getUninterpFn sym funNm argCtx (W4.BaseStructRepr argCtx) z <- liftIO $ W4.applySymFn (w4 sym) fn (Empty :> w0 :> w1 :> w2 :> w3) - pure $ VSeq 4 $ indexSeqMap \i -> + mkSeq sym (Nat 4) (TVSeq 32 TVBit) $ indexSeqMap \i -> if | i == 0 -> fromWord32 =<< liftIO (W4.structField (w4 sym) z (natIndex @0)) | i == 1 -> fromWord32 =<< liftIO (W4.structField (w4 sym) z (natIndex @1)) | i == 2 -> fromWord32 =<< liftIO (W4.structField (w4 sym) z (natIndex @2)) diff --git a/src/Cryptol/IR/FreeVars.hs b/src/Cryptol/IR/FreeVars.hs --- a/src/Cryptol/IR/FreeVars.hs +++ b/src/Cryptol/IR/FreeVars.hs @@ -159,7 +159,8 @@ TUser _ _ t -> freeVars t TRec fs -> freeVars (recordElements fs) - TNominal nt ts -> freeVars nt <> freeVars ts + TNominal nt ts -> mempty { tyDeps = Set.singleton (ntName nt) } + <> freeVars ts instance FreeVars TVar where freeVars tv = case tv of diff --git a/src/Cryptol/ModuleSystem/Base.hs b/src/Cryptol/ModuleSystem/Base.hs --- a/src/Cryptol/ModuleSystem/Base.hs +++ b/src/Cryptol/ModuleSystem/Base.hs @@ -12,8 +12,8 @@ {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE ImplicitParams #-} {-# LANGUAGE LambdaCase #-} -{-# LANGUAGE RecordWildCards #-} {-# LANGUAGE OverloadedStrings #-} +{-# Language DisambiguateRecordFields #-} {-# LANGUAGE BlockArguments #-} module Cryptol.ModuleSystem.Base where @@ -41,6 +41,7 @@ ) import qualified System.IO.Error as IOE import qualified Data.Map as Map +import qualified Data.Map.Strict as MapS import Prelude () import Prelude.Compat hiding ( (<>) ) @@ -82,7 +83,7 @@ import Cryptol.Utils.Ident ( preludeName, floatName, arrayName, suiteBName, primeECName , preludeReferenceName, interactiveName, modNameChunks - , modNameToNormalModName, Namespace(NSModule) ) + , modNamesMatch, Namespace(NSModule) ) import Cryptol.Utils.PP (pretty, pp, hang, vcat, ($$), (<+>), (<.>), colon) import Cryptol.Utils.Panic (panic) import Cryptol.Utils.Logger(logPutStrLn, logPrint) @@ -133,7 +134,7 @@ fail ("Undefined submodule name: " ++ show (pp pname)) _:_:_ -> do fail ("Ambiguous submodule name: " ++ show (pp pname)) - [name] -> pure (P.ImpNested name) + [n] -> pure (P.ImpNested n) -- NoPat ----------------------------------------------------------------------- @@ -159,7 +160,8 @@ -- Returns a fingerprint of the module, and a set of dependencies due -- to `include` directives. parseModule :: - ModulePath -> ModuleM (Fingerprint, Set FilePath, [P.Module PName]) + ModulePath -> + ModuleM (Fingerprint, MapS.Map FilePath Fingerprint, [P.Module PName]) parseModule path = do getBytes <- getByteReader @@ -175,14 +177,16 @@ | IOE.isDoesNotExistError exn -> cantFindFile p | otherwise -> otherIOError p exn InMem p _ -> panic "parseModule" - [ "IOError for in-memory contetns???" + [ "IOError for in-memory contents???" , "Label: " ++ show p , "Exception: " ++ show exn ] + let fp = fingerprint bytes txt <- case decodeUtf8' bytes of - Right txt -> return $! (T.replace "\r\n" "\n" txt) - Left e -> badUtf8 path e + Right txt -> return $! T.replace "\r\n" "\n" txt + Left e -> badUtf8 path fp e + let cfg = P.defaultConfig { P.cfgSource = case path of InFile p -> p @@ -192,8 +196,7 @@ case P.parseModule cfg txt of Right pms -> - do let fp = fingerprint bytes - (pm1,deps) <- + do (pm1,deps) <- case path of InFile p -> do r <- getByteReader @@ -203,7 +206,7 @@ case mb of Right ok -> pure ok Left err -> noIncludeErrors err - pure (mo, Set.unions d) + pure (mo, MapS.unions d) {- We don't do "include" resolution for in-memory files because at the moment the include resolution pass requires @@ -211,7 +214,7 @@ looking for other inlcude files. This could be generalized, but we can do it once we have a concrete use case as it would help guide the design. -} - InMem {} -> pure (pms, Set.empty) + InMem {} -> pure (pms, MapS.empty) {- case path of @@ -220,7 +223,7 @@ --} fp `seq` return (fp, deps, pm1) - Left err -> moduleParseError path err + Left err -> moduleParseError path fp err -- Top Level Modules and Signatures -------------------------------------------- @@ -248,7 +251,8 @@ case lookupTCEntity n env of -- loadModule will calculate the canonical path again Nothing -> - doLoadModule eval False (FromModule n) (InFile foundPath) fp deps pm + loadModuleAndDeps eval False + (FromModule n) (InFile foundPath) fp deps pm Just lm | path' == loaded -> return (lmData lm) | otherwise -> duplicateModuleName n path' loaded @@ -267,25 +271,38 @@ do path <- findModule n errorInFile path $ do (fp, deps, pms) <- parseModule path - ms <- mapM (doLoadModule True quiet isrc path fp deps) pms + ms <- mapM (loadModuleAndDeps True quiet isrc path fp deps) pms return (path,last ms) -- | Load dependencies, typecheck, and add to the eval environment. -doLoadModule :: +loadModuleAndDeps :: Bool {- ^ evaluate declarations in the module -} -> Bool {- ^ quiet mode: true suppresses the "loading module" message -} -> ImportSource -> ModulePath -> Fingerprint -> - Set FilePath {- ^ `include` dependencies -} -> + MapS.Map FilePath Fingerprint {- ^ `include` dependencies -} -> P.Module PName -> ModuleM T.TCTopEntity -doLoadModule eval quiet isrc path fp incDeps pm0 = +loadModuleAndDeps eval quiet isrc path fp incDeps pm0 = loading isrc $ do let pm = addPrelude pm0 impDeps <- loadDeps pm + fst <$> doLoadModule eval quiet isrc path fp incDeps pm impDeps - let what = case P.mDef pm of +-- | Typecheck and add to the eval environment. +doLoadModule :: + Bool {- ^ evaluate declarations in the module -} -> + Bool {- ^ quiet mode: true suppresses the "loading module" message -} -> + ImportSource -> + ModulePath -> + Fingerprint -> + MapS.Map FilePath Fingerprint {- ^ `include` dependencies -} -> + P.Module PName -> + Set ModName -> + ModuleM (T.TCTopEntity, FileInfo) +doLoadModule eval quiet isrc path fp incDeps pm impDeps = + do let what = case P.mDef pm of P.InterfaceModule {} -> "interface module" _ -> "module" @@ -315,7 +332,7 @@ let fi = fileInfo fp incDeps impDeps foreignSrc loadedModule path fi nameEnv foreignSrc tcm - return tcm + return (tcm, fi) where evalForeign tcm @@ -467,10 +484,26 @@ findDepsOf mpath findDepsOf :: ModulePath -> ModuleM (ModulePath, FileInfo) -findDepsOf mpath = +findDepsOf mpath' = + do mpath <- case mpath' of + InFile file -> InFile <$> io (canonicalizePath file) + InMem {} -> pure mpath' + (fi, _) <- parseWithDeps mpath + pure (mpath, fi) + +{- | Parse the given module path and find its dependencies. +The reason we return a list here, is that sometime files may +contain multiple modules (e.g., due to desugaring `parameter` blocks +in functors. -} +parseWithDeps :: + ModulePath -> + ModuleM (FileInfo, [(Module PName, [ImportSource])]) +parseWithDeps mpath = do (fp, incs, ms) <- parseModule mpath - let (anyF,imps) = mconcat (map (findDeps' . addPrelude) ms) - fdeps <- if getAny anyF + let ms' = map addPrelude ms + depss = map findDeps' ms' + let (anyF,imps) = mconcat depss + fpath <- if getAny anyF then do mb <- io case mpath of InFile path -> foreignLibPath path InMem {} -> pure Nothing @@ -480,13 +513,13 @@ Map.singleton fpath exists else pure Map.empty pure - ( mpath - , FileInfo + ( FileInfo { fiFingerprint = fp , fiIncludeDeps = incs , fiImportDeps = Set.fromList (map importedModule (appEndo imps [])) - , fiForeignDeps = fdeps + , fiForeignDeps = fpath } + , zip ms' $ map ((`appEndo` []) . snd) depss ) -- | Find the set of top-level modules imported by a module. @@ -622,8 +655,7 @@ -- check that the name of the module matches expectations let nm = importedModule isrc - unless (modNameToNormalModName nm == - modNameToNormalModName (thing (P.mName m))) + unless (modNamesMatch nm (thing (P.mName m))) (moduleNameMismatch nm (mName m)) -- remove pattern bindings diff --git a/src/Cryptol/ModuleSystem/Env.hs b/src/Cryptol/ModuleSystem/Env.hs --- a/src/Cryptol/ModuleSystem/Env.hs +++ b/src/Cryptol/ModuleSystem/Env.hs @@ -192,10 +192,10 @@ } -- | Try to focus a loaded module in the module environment. -focusModule :: ModName -> ModuleEnv -> Maybe ModuleEnv +focusModule :: ImpName Name -> ModuleEnv -> Maybe ModuleEnv focusModule n me = do - guard (isLoaded (ImpTop n) (meLoadedModules me)) - return me { meFocusedModule = Just (ImpTop n) } + guard (isLoaded n (meLoadedModules me)) + return me { meFocusedModule = Just n } -- | Get a list of all the loaded modules. Each module in the -- resulting list depends only on other modules that precede it. @@ -360,7 +360,7 @@ -- | The location of a module data ModulePath = InFile FilePath | InMem String ByteString -- ^ Label, content - deriving (Show, Generic, NFData) + deriving (Show, Read, Generic, NFData) -- | In-memory things are compared by label. instance Eq ModulePath where @@ -426,12 +426,19 @@ getLoadedModules :: LoadedModules -> [LoadedModule] getLoadedModules x = lmLoadedParamModules x ++ lmLoadedModules x +getLoadedField :: Ord a => + (forall b. LoadedModuleG b -> a) -> LoadedModules -> Set a +getLoadedField f lm = Set.fromList + $ map f (lmLoadedModules lm) + ++ map f (lmLoadedParamModules lm) + ++ map f (lmLoadedSignatures lm) + getLoadedNames :: LoadedModules -> Set ModName -getLoadedNames lm = Set.fromList - $ map lmName (lmLoadedModules lm) - ++ map lmName (lmLoadedParamModules lm) - ++ map lmName (lmLoadedSignatures lm) +getLoadedNames = getLoadedField lmName +getLoadedIds :: LoadedModules -> Set String +getLoadedIds = getLoadedField lmModuleId + instance Semigroup LoadedModules where l <> r = LoadedModules { lmLoadedModules = List.unionBy ((==) `on` lmName) @@ -503,6 +510,10 @@ Map.member nn (T.mSubmodules m) || any check (T.mFunctors m) +isLoadedStrict :: ImpName Name -> String -> LoadedModules -> Bool +isLoadedStrict mn modId lm = + isLoaded mn lm && modId `Set.member` getLoadedIds lm + -- | Is this a loaded parameterized module. isLoadedParamMod :: ImpName Name -> LoadedModules -> Bool isLoadedParamMod (ImpTop mn) lm = any ((mn ==) . lmName) (lmLoadedParamModules lm) @@ -568,14 +579,21 @@ -- | Try to find a previously loaded module lookupModule :: ModName -> ModuleEnv -> Maybe LoadedModule -lookupModule mn me = search lmLoadedModules `mplus` search lmLoadedParamModules +lookupModule mn = lookupModuleWith ((mn ==) . lmName) + +lookupModuleWith :: (LoadedModule -> Bool) -> ModuleEnv -> Maybe LoadedModule +lookupModuleWith p me = + search lmLoadedModules `mplus` search lmLoadedParamModules where - search how = List.find ((mn ==) . lmName) (how (meLoadedModules me)) + search how = List.find p (how (meLoadedModules me)) lookupSignature :: ModName -> ModuleEnv -> Maybe LoadedSignature -lookupSignature mn me = - List.find ((mn ==) . lmName) (lmLoadedSignatures (meLoadedModules me)) +lookupSignature mn = lookupSignatureWith ((mn ==) . lmName) +lookupSignatureWith :: + (LoadedSignature -> Bool) -> ModuleEnv -> Maybe LoadedSignature +lookupSignatureWith p me = List.find p (lmLoadedSignatures (meLoadedModules me)) + addLoadedSignature :: ModulePath -> String -> FileInfo -> @@ -583,7 +601,7 @@ ModName -> T.ModParamNames -> LoadedModules -> LoadedModules addLoadedSignature path ident fi nameEnv nm si lm - | isLoaded (ImpTop nm) lm = lm + | isLoadedStrict (ImpTop nm) ident lm = lm | otherwise = lm { lmLoadedSignatures = loaded : lmLoadedSignatures lm } where loaded = LoadedModule @@ -605,7 +623,7 @@ Maybe ForeignSrc -> T.Module -> LoadedModules -> LoadedModules addLoadedModule path ident fi nameEnv fsrc tm lm - | isLoaded (ImpTop (T.mName tm)) lm = lm + | isLoadedStrict (ImpTop (T.mName tm)) ident lm = lm | T.isParametrizedModule tm = lm { lmLoadedParamModules = loaded : lmLoadedParamModules lm } | otherwise = lm { lmLoadedModules = @@ -640,15 +658,16 @@ data FileInfo = FileInfo { fiFingerprint :: Fingerprint - , fiIncludeDeps :: Set FilePath + , fiIncludeDeps :: Map FilePath Fingerprint , fiImportDeps :: Set ModName , fiForeignDeps :: Map FilePath Bool + -- ^ The bool indicates if the library for the foreign import exists. } deriving (Show,Generic,NFData) fileInfo :: Fingerprint -> - Set FilePath -> + Map FilePath Fingerprint -> Set ModName -> Maybe ForeignSrc -> FileInfo diff --git a/src/Cryptol/ModuleSystem/Fingerprint.hs b/src/Cryptol/ModuleSystem/Fingerprint.hs --- a/src/Cryptol/ModuleSystem/Fingerprint.hs +++ b/src/Cryptol/ModuleSystem/Fingerprint.hs @@ -14,14 +14,17 @@ ) where import Control.DeepSeq (NFData (rnf)) -import Crypto.Hash.SHA1 (hash) -import Data.ByteString (ByteString) import Control.Exception (try) +import Control.Monad ((<$!>)) +import Crypto.Hash.SHA256 (hash) +import Data.ByteString (ByteString) +import Data.Char (intToDigit, digitToInt, isHexDigit) import qualified Data.ByteString as B -import qualified Data.Vector as Vector +import qualified Toml +import qualified Toml.Schema as Toml newtype Fingerprint = Fingerprint ByteString - deriving (Eq, Show) + deriving (Eq, Ord, Show, Read) instance NFData Fingerprint where rnf (Fingerprint fp) = rnf fp @@ -31,21 +34,34 @@ fingerprint = Fingerprint . hash -- | Attempt to compute the fingerprint of the file at the given path. --- Returns 'Nothing' in the case of an error. -fingerprintFile :: FilePath -> IO (Maybe Fingerprint) +-- Returns 'Left' in the case of an error. +fingerprintFile :: FilePath -> IO (Either IOError Fingerprint) fingerprintFile path = do res <- try (B.readFile path) - return $! - case res :: Either IOError ByteString of - Left{} -> Nothing - Right b -> Just $! fingerprint b + return $! fingerprint <$!> (res :: Either IOError ByteString) fingerprintHexString :: Fingerprint -> String fingerprintHexString (Fingerprint bs) = B.foldr hex "" bs where - digits = Vector.fromList "0123456789ABCDEF" - digit x = digits Vector.! fromIntegral x - hex b cs = let (x,y) = divMod b 16 - in digit x : digit y : cs + hex b cs = let (x,y) = divMod (fromIntegral b) 16 + in intToDigit x : intToDigit y : cs +fingerprintFromHexString :: String -> Maybe Fingerprint +fingerprintFromHexString str = Fingerprint . B.pack <$> go str + where + go [] = Just [] + go (x:y:z) + | isHexDigit x + , isHexDigit y + = (fromIntegral (digitToInt x * 16 + digitToInt y):) <$> go z + go _ = Nothing +instance Toml.ToValue Fingerprint where + toValue = Toml.toValue . fingerprintHexString + +instance Toml.FromValue Fingerprint where + fromValue x = + do str <- Toml.fromValue x + case fingerprintFromHexString str of + Nothing -> Toml.failAt (Toml.valueAnn x) "malformed fingerprint hex-string" + Just fp -> pure fp diff --git a/src/Cryptol/ModuleSystem/Monad.hs b/src/Cryptol/ModuleSystem/Monad.hs --- a/src/Cryptol/ModuleSystem/Monad.hs +++ b/src/Cryptol/ModuleSystem/Monad.hs @@ -26,6 +26,7 @@ import Cryptol.ModuleSystem.Name (FreshM(..),Supply) import Cryptol.ModuleSystem.Renamer (RenamerError(),RenamerWarning()) import Cryptol.ModuleSystem.NamingEnv(NamingEnv) +import Cryptol.ModuleSystem.Fingerprint(Fingerprint) import qualified Cryptol.Parser as Parser import qualified Cryptol.Parser.AST as P import Cryptol.Utils.Panic (panic) @@ -40,6 +41,7 @@ import Cryptol.Utils.Ident (interactiveName, noModuleName) import Cryptol.Utils.PP import Cryptol.Utils.Logger(Logger) +import qualified Cryptol.Project.Config as Proj import qualified Control.Monad.Fail as Fail import Control.Monad.IO.Class @@ -94,11 +96,11 @@ -- ^ Unable to find the module given, tried looking in these paths | CantFindFile FilePath -- ^ Unable to open a file - | BadUtf8 ModulePath UnicodeException + | BadUtf8 ModulePath Fingerprint UnicodeException -- ^ Bad UTF-8 encoding in while decoding this file | OtherIOError FilePath IOException -- ^ Some other IO error occurred while reading this file - | ModuleParseError ModulePath Parser.ParseError + | ModuleParseError ModulePath Fingerprint Parser.ParseError -- ^ Generated this parse error when parsing the file for module m | RecursiveModules [ImportSource] -- ^ Recursive module group discovered @@ -120,11 +122,11 @@ -- ^ Two modules loaded from different files have the same module name | FFILoadErrors P.ModName [FFILoadError] -- ^ Errors loading foreign function implementations - + | ConfigLoadError Proj.ConfigLoadError | ErrorInFile ModulePath ModuleError -- ^ This is just a tag on the error, indicating the file containing it. -- It is convenient when we had to look for the module, and we'd like - -- to communicate the location of pthe problematic module to the handler. + -- to communicate the location of the problematic module to the handler. deriving (Show) @@ -132,9 +134,9 @@ rnf e = case e of ModuleNotFound src path -> src `deepseq` path `deepseq` () CantFindFile path -> path `deepseq` () - BadUtf8 path ue -> rnf (path, ue) + BadUtf8 path fp ue -> rnf (path, fp, ue) OtherIOError path exn -> path `deepseq` exn `seq` () - ModuleParseError source err -> source `deepseq` err `deepseq` () + ModuleParseError source fp err -> rnf (source, fp, err) RecursiveModules mods -> mods `deepseq` () RenamerErrors src errs -> src `deepseq` errs `deepseq` () NoPatErrors src errs -> src `deepseq` errs `deepseq` () @@ -148,6 +150,7 @@ OtherFailure x -> x `deepseq` () FFILoadErrors x errs -> x `deepseq` errs `deepseq` () ErrorInFile x y -> x `deepseq` y `deepseq` () + ConfigLoadError x -> x `seq` () instance PP ModuleError where ppPrec prec e = case e of @@ -165,7 +168,7 @@ text "[error]" <+> text "can't find file:" <+> text path - BadUtf8 path _ue -> + BadUtf8 path _fp _ue -> text "[error]" <+> text "bad utf-8 encoding:" <+> pp path @@ -174,7 +177,7 @@ text "IO error while loading file:" <+> text path <.> colon) 4 (text (show exn)) - ModuleParseError _source err -> Parser.ppError err + ModuleParseError _source _fp err -> Parser.ppError err RecursiveModules mods -> hang (text "[error] module imports form a cycle:") @@ -208,6 +211,8 @@ hang (text "[error] Failed to load foreign implementations for module" <+> pp x <.> colon) 4 (vcat $ map pp errs) + + ConfigLoadError err -> pp err ErrorInFile _ x -> ppPrec prec x @@ -217,15 +222,15 @@ cantFindFile :: FilePath -> ModuleM a cantFindFile path = ModuleT (raise (CantFindFile path)) -badUtf8 :: ModulePath -> UnicodeException -> ModuleM a -badUtf8 path ue = ModuleT (raise (BadUtf8 path ue)) +badUtf8 :: ModulePath -> Fingerprint -> UnicodeException -> ModuleM a +badUtf8 path fp ue = ModuleT (raise (BadUtf8 path fp ue)) otherIOError :: FilePath -> IOException -> ModuleM a otherIOError path exn = ModuleT (raise (OtherIOError path exn)) -moduleParseError :: ModulePath -> Parser.ParseError -> ModuleM a -moduleParseError path err = - ModuleT (raise (ModuleParseError path err)) +moduleParseError :: ModulePath -> Fingerprint -> Parser.ParseError -> ModuleM a +moduleParseError path fp err = + ModuleT (raise (ModuleParseError path fp err)) recursiveModules :: [ImportSource] -> ModuleM a recursiveModules loaded = ModuleT (raise (RecursiveModules loaded)) @@ -274,6 +279,9 @@ ErrorInFile {} -> e _ -> ErrorInFile file e +tryModule :: ModuleM a -> ModuleM (Either ModuleError a) +tryModule (ModuleT m) = ModuleT (handle (Right <$> m) (pure . Left)) + -- Warnings -------------------------------------------------------------------- data ModuleWarning @@ -434,6 +442,11 @@ isLoaded mn = do env <- ModuleT get pure (MEnv.isLoaded (T.ImpTop mn) (meLoadedModules env)) + +isLoadedStrict :: P.ModName -> ModulePath -> ModuleM Bool +isLoadedStrict mn mpath = + do env <- ModuleT get + pure (MEnv.isLoadedStrict (T.ImpTop mn) (modulePathLabel mpath) (meLoadedModules env)) loadingImport :: Located P.Import -> ModuleM a -> ModuleM a loadingImport = loading . FromImport diff --git a/src/Cryptol/ModuleSystem/Renamer.hs b/src/Cryptol/ModuleSystem/Renamer.hs --- a/src/Cryptol/ModuleSystem/Renamer.hs +++ b/src/Cryptol/ModuleSystem/Renamer.hs @@ -1073,12 +1073,12 @@ depsOf (NamedThing (thing n')) do mbSig <- traverse renameSchema (bSignature b) shadowNames (fst `fmap` mbSig) $ - do (patEnv,pats') <- renamePats (bParams b) + do (patEnv,bParams') <- renameBindParams (bParams b) -- NOTE: renamePats will generate warnings, -- so we don't need to trigger them again here. e' <- shadowNames' CheckNone patEnv (rnLocated rename (bDef b)) return b { bName = n' - , bParams = pats' + , bParams = bParams' , bDef = e' , bSignature = snd `fmap` mbSig , bPragmas = bPragmas b @@ -1350,6 +1350,12 @@ return (pe `mappend` env', p':rest') [] -> return (mempty, []) + +-- | Rename patterns used as bind parameters, and collect the new environment that they introduce. +renameBindParams :: BindParams PName -> RenameM (NamingEnv, BindParams Name) +renameBindParams (PatternParams pats) = + (\(env,pats') -> (env, PatternParams pats')) <$> renamePats pats +renameBindParams (DroppedParams rng i) = return (mempty, DroppedParams rng i) patternEnv :: Pattern PName -> RenameM NamingEnv patternEnv = go diff --git a/src/Cryptol/Parser.y b/src/Cryptol/Parser.y --- a/src/Cryptol/Parser.y +++ b/src/Cryptol/Parser.y @@ -173,8 +173,8 @@ top_module :: { [Module PName] } : mbDoc 'module' module_def {% mkTopMods $1 $3 } | 'v{' vmod_body 'v}' {% mkAnonymousModule $2 } - | 'interface' 'module' modName 'where' 'v{' sig_body 'v}' - { mkTopSig $3 $6 } + | mbDoc 'interface' 'module' modName 'where' 'v{' sig_body 'v}' + { mkTopSig $1 $4 $7 } module_def :: { Module PName } @@ -380,7 +380,7 @@ | iapat pat_op iapat '=' expr { at ($1,$5) $ DBind $ Bind { bName = $2 - , bParams = [$1,$3] + , bParams = PatternParams [$1,$3] , bDef = at $5 (Located emptyRange (exprDef $5)) , bSignature = Nothing , bPragmas = [] @@ -410,7 +410,7 @@ | 'let' iapat pat_op iapat '=' expr { at ($2,$6) $ DBind $ Bind { bName = $3 - , bParams = [$2,$4] + , bParams = PatternParams [$2,$4] , bDef = at $6 (Located emptyRange (exprDef $6)) , bSignature = Nothing , bPragmas = [] diff --git a/src/Cryptol/Parser/AST.hs b/src/Cryptol/Parser/AST.hs --- a/src/Cryptol/Parser/AST.hs +++ b/src/Cryptol/Parser/AST.hs @@ -62,7 +62,8 @@ , FixityCmp(..), compareFixity , TySyn(..) , PropSyn(..) - , Bind(..) + , Bind(..), bindParams, bindHeaderLoc + , BindParams(..), dropParams, noParams , BindDef(..), LBindDef , BindImpl(..), bindImpl, exprDef , Pragma(..) @@ -484,7 +485,7 @@ -} data Bind name = Bind { bName :: Located name -- ^ Defined thing - , bParams :: [Pattern name] -- ^ Parameters + , bParams :: BindParams name -- ^ Parameters , bDef :: Located (BindDef name) -- ^ Definition , bSignature :: Maybe (Schema name) -- ^ Optional type sig , bInfix :: Bool -- ^ Infix operator? @@ -495,6 +496,49 @@ , bExport :: !ExportType } deriving (Eq, Generic, NFData, Functor, Show) +bindParams :: Bind name -> [Pattern name] +bindParams b = case bParams b of + PatternParams ps -> ps + DroppedParams _ _ -> [] + +-- | Sets the number of parameters for a binding to zero, noting +-- the original number and source location of the patterns. +-- e.g. when rewriting @let f a b c = \x -> ...@, into +-- @let f = \\a b c x -> ...@ the parameters for @f@ change from +-- @PatternParams [a,b,c]@ to @DroppedParams (getLoc [a,b,c]) 3@ +dropParams :: BindParams name -> BindParams name +dropParams bps = case bps of + PatternParams ps -> DroppedParams (getLoc ps) (length ps) + DroppedParams rng i -> DroppedParams rng i + +-- | Range encompassing the LHS of a binder, its signature, but not +-- its definition. +bindHeaderLoc :: Bind name -> Maybe Range +bindHeaderLoc b = getLoc (bName b, (bSignature b, bParams b)) + +-- | An empty 'BindParams' (i.e. zero parameters). +-- Note that 'dropParams' should be used instead of this +-- when rewriting an existing 'Bind' to have no parameters. +noParams :: BindParams name +noParams = PatternParams [] + +-- | A list of patterns used as parameters to a 'Bind'. +-- This is only used to improve error messages, by retaining +-- information about the original shape of a 'Bind' when +-- rewriting (see 'dropParams'). +data BindParams name = + PatternParams [Pattern name] + -- ^ Parameters that appear in the LHS of a binding equation + -- as patterns. + -- e.g. @[a,b,c]@ in @let f a b c = \x -> ...@ + | DroppedParams (Maybe Range) Int + -- ^ Represents zero parameters to a binding equation that + -- originally had parameters, but was rewritten to have none + -- (see 'Cryptol.Parser.NoPat'). + -- Retains the original source range, and number + -- of dropped parameters (see 'dropParams'). + deriving (Eq, Generic, NFData, Functor, Show) + type LBindDef = Located (BindDef PName) data BindDef name = DPrim @@ -881,7 +925,17 @@ instance HasLoc (PropSyn name) where getLoc (PropSyn x _ _ _) = getLoc x +instance HasLoc (PropGuardCase name) where + getLoc n + | null locs = Nothing + | otherwise = Just (rCombs locs) + where + locs = catMaybes (getLoc (pgcExpr n) : map getLoc (pgcProps n)) +instance HasLoc (BindParams name) where + getLoc bps = case bps of + PatternParams ps -> getLoc ps + DroppedParams rng _ -> rng -------------------------------------------------------------------------------- @@ -1129,9 +1183,9 @@ Nothing -> [] Just s -> [pp (DSignature [f] s)] eq = if bMono b then text ":=" else text "=" - lhs = fsep (ppL f : (map (ppPrec 3) (bParams b))) + lhs = fsep (ppL f : (map (ppPrec 3) (bindParams b))) - lhsOp = case bParams b of + lhsOp = case bindParams b of [x,y] -> pp x <+> ppL f <+> pp y xs -> parens (parens (ppL f) <+> fsep (map (ppPrec 0) xs)) -- _ -> panic "AST" [ "Malformed infix operator", show b ] @@ -1568,6 +1622,11 @@ instance NoPos (EnumCon name) where noPos c = EnumCon { ecName = noPos (ecName c), ecFields = noPos (ecFields c) } + +instance NoPos (BindParams name) where + noPos bp = case bp of + PatternParams ps -> PatternParams (noPos ps) + DroppedParams _ i -> DroppedParams Nothing i instance NoPos (Bind name) where noPos x = Bind { bName = noPos (bName x) diff --git a/src/Cryptol/Parser/ExpandPropGuards.hs b/src/Cryptol/Parser/ExpandPropGuards.hs --- a/src/Cryptol/Parser/ExpandPropGuards.hs +++ b/src/Cryptol/Parser/ExpandPropGuards.hs @@ -127,7 +127,7 @@ typeInsts <- (\(TParam n _ _) -> Right . PosInst $ TUser n []) `traverse` tParams - let e' = foldl EApp (EAppT (EVar $ thing bName') typeInsts) (patternToExpr <$> bParams bind) + let e' = foldl EApp (EAppT (EVar $ thing bName') typeInsts) (patternToExpr <$> bindParams bind) pure ( PropGuardCase props' e', bind diff --git a/src/Cryptol/Parser/Names.hs b/src/Cryptol/Parser/Names.hs --- a/src/Cryptol/Parser/Names.hs +++ b/src/Cryptol/Parser/Names.hs @@ -73,7 +73,7 @@ -- | The names defined and used by a single binding. namesB :: Ord name => Bind name -> ([Located name], Set name) namesB b = - ([bName b], boundLNames (namesPs' (bParams b)) (namesDef (thing (bDef b)))) + ([bName b], boundLNames (namesPs' (bindParams b)) (namesDef (thing (bDef b)))) namesDef :: Ord name => BindDef name -> Set name @@ -216,7 +216,7 @@ tnamesB b = Set.unions [setS, setP, setE] where setS = maybe Set.empty tnamesS (bSignature b) - setP = Set.unions (map tnamesP (bParams b)) + setP = Set.unions (map tnamesP (bindParams b)) setE = tnamesDef (thing (bDef b)) tnamesDef :: Ord name => BindDef name -> Set name diff --git a/src/Cryptol/Parser/NoInclude.hs b/src/Cryptol/Parser/NoInclude.hs --- a/src/Cryptol/Parser/NoInclude.hs +++ b/src/Cryptol/Parser/NoInclude.hs @@ -20,8 +20,8 @@ import qualified Control.Exception as X import qualified Control.Monad.Fail as Fail -import Data.Set(Set) -import qualified Data.Set as Set +import Data.Map.Strict(Map) +import qualified Data.Map.Strict as Map import Data.ByteString (ByteString) import Data.Either (partitionEithers) import Data.Text(Text) @@ -38,12 +38,13 @@ import Cryptol.Parser.LexerUtils (Config(..),defaultConfig) import Cryptol.Parser.ParserUtils import Cryptol.Parser.Unlit (guessPreProc) +import Cryptol.ModuleSystem.Fingerprint removeIncludesModule :: (FilePath -> IO ByteString) -> FilePath -> Module PName -> - IO (Either [IncludeError] (Module PName, Set FilePath)) + IO (Either [IncludeError] (Module PName, Map FilePath Fingerprint)) removeIncludesModule reader modPath m = runNoIncM reader modPath (noIncludeModule m) @@ -82,7 +83,7 @@ IO )) a } -type Deps = Set FilePath +type Deps = Map FilePath Fingerprint data Env = Env { envSeen :: [Located FilePath] -- ^ Files that have been loaded @@ -106,7 +107,7 @@ , envIncPath = incPath , envFileReader = reader } - Set.empty + Map.empty pure do ok <- mb pure (ok,s) @@ -135,10 +136,10 @@ do Env { .. } <- ask return (envIncPath path) -addDep :: FilePath -> NoIncM () -addDep path = M +addDep :: FilePath -> Fingerprint -> NoIncM () +addDep path fp = M do s <- get - let s1 = Set.insert path s + let s1 = Map.insert path fp s s1 `seq` set s1 @@ -247,12 +248,13 @@ readInclude path = do readBytes <- envFileReader <$> M ask file <- fromIncPath (thing path) - addDep file sourceBytes <- readBytes file `failsWith` handler sourceText <- X.evaluate (T.decodeUtf8' sourceBytes) `failsWith` handler case sourceText of Left encodingErr -> M (raise [IncludeDecodeFailed path encodingErr]) - Right txt -> return txt + Right txt -> do + addDep file (fingerprint sourceBytes) + return txt where handler :: X.IOException -> NoIncM a handler _ = includeFailed path diff --git a/src/Cryptol/Parser/NoPat.hs b/src/Cryptol/Parser/NoPat.hs --- a/src/Cryptol/Parser/NoPat.hs +++ b/src/Cryptol/Parser/NoPat.hs @@ -58,7 +58,7 @@ where (m1,errs) = removePatterns m simpleBind :: Located PName -> Expr PName -> Bind PName -simpleBind x e = Bind { bName = x, bParams = [] +simpleBind x e = Bind { bName = x, bParams = noParams , bDef = at e (Located emptyRange (exprDef e)) , bSignature = Nothing, bPragmas = [] , bMono = True, bInfix = False, bFixity = Nothing @@ -68,7 +68,7 @@ sel :: Pattern PName -> PName -> Selector -> Bind PName sel p x s = let (a,ts) = splitSimpleP p - in simpleBind a (foldl ETyped (ESel (EVar x) s) ts) + in simpleBind a (at p (foldl ETyped (ESel (EVar x) s) ts)) -- | Given a pattern, transform it into a simple pattern and a set of bindings. -- Simple patterns may only contain variables and type annotations. @@ -238,12 +238,12 @@ noMatchB b = case thing (bDef b) of - DPrim | null (bParams b) -> return b + DPrim | null (bindParams b) -> return b | otherwise -> panic "NoPat" [ "noMatchB: primitive with params" , show b ] DForeign Nothing - | null (bParams b) -> return b + | null (bindParams b) -> return b | otherwise -> panic "NoPat" [ "noMatchB: foreign with params" , show b ] @@ -255,12 +255,12 @@ noMatchI def i = do i' <- case i of DExpr e -> - DExpr <$> noPatFun (Just (thing (bName b))) 0 (bParams b) e + DExpr <$> noPatFun (Just (thing (bName b))) 0 (bindParams b) e DPropGuards guards -> let nm = thing (bName b) - ps = bParams b + ps = bindParams b in DPropGuards <$> mapM (noPatPropGuardCase nm ps) guards - pure b { bParams = [], bDef = def i' <$ bDef b } + pure b { bParams = dropParams (bParams b), bDef = def i' <$ bDef b } noPatPropGuardCase :: PName -> @@ -286,7 +286,7 @@ e1 <- noPatE e let e2 = foldl ETyped e1 ts return $ DBind Bind { bName = x - , bParams = [] + , bParams = noParams , bDef = at e (Located emptyRange (exprDef e2)) , bSignature = Nothing , bPragmas = [] diff --git a/src/Cryptol/Parser/ParserUtils.hs b/src/Cryptol/Parser/ParserUtils.hs --- a/src/Cryptol/Parser/ParserUtils.hs +++ b/src/Cryptol/Parser/ParserUtils.hs @@ -14,11 +14,11 @@ {-# LANGUAGE PatternGuards #-} {-# LANGUAGE BlockArguments #-} {-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE LambdaCase #-} -- See Note [-Wincomplete-uni-patterns and irrefutable patterns] in Cryptol.TypeCheck.TypePat {-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-} module Cryptol.Parser.ParserUtils where -import qualified Data.Text as Text import Data.Char(isAlphaNum, isSpace) import Data.Maybe(fromMaybe, mapMaybe) import Data.Bits(testBit,setBit) @@ -31,6 +31,7 @@ import qualified Data.Text as T import qualified Data.Map as Map import Text.Read(readMaybe) +import Data.Foldable (for_) import GHC.Generics (Generic) import Control.DeepSeq @@ -45,9 +46,9 @@ import Cryptol.Parser.Position import Cryptol.Parser.Utils (translateExprToNumT,widthIdent) import Cryptol.Utils.Ident( packModName,packIdent,modNameChunks - , identAnonArg, identAnonIfaceMod + , identAnonArg, identAnonIfaceMod, identAnonInstImport , modNameArg, modNameIfaceMod - , modNameToText, modNameIsNormal + , mainModName, modNameIsNormal , modNameToNormalModName , unpackIdent, isUpperIdent ) @@ -73,6 +74,8 @@ newtype ParseM a = P { unP :: Config -> Position -> S -> Either ParseError (a,S) } +askConfig :: ParseM Config +askConfig = P \cfg _ s -> Right (cfg, s) lexerP :: (Located Token -> ParseM a) -> ParseM a lexerP k = P $ \cfg p s -> @@ -786,7 +789,7 @@ mkProperty :: LPName -> [Pattern PName] -> Expr PName -> Decl PName mkProperty f ps e = at (f,e) $ DBind Bind { bName = f - , bParams = reverse ps + , bParams = PatternParams (reverse ps) , bDef = at e (Located emptyRange (exprDef e)) , bSignature = Nothing , bPragmas = [PragmaProperty] @@ -802,7 +805,7 @@ LPName -> ([Pattern PName], [Pattern PName]) -> Expr PName -> Decl PName mkIndexedDecl f (ps, ixs) e = DBind Bind { bName = f - , bParams = reverse ps + , bParams = PatternParams (reverse ps) , bDef = at e (Located emptyRange (exprDef rhs)) , bSignature = Nothing , bPragmas = [] @@ -829,7 +832,7 @@ let gs = reverse guards pure $ DBind Bind { bName = f - , bParams = reverse ps + , bParams = PatternParams (reverse ps) , bDef = Located (srcRange f) (DImpl (DPropGuards gs)) , bSignature = Nothing , bPragmas = [] @@ -920,7 +923,7 @@ mkNoImplDecl def mbDoc ln sig = [ exportDecl Nothing Public $ DBind Bind { bName = ln - , bParams = [] + , bParams = noParams , bDef = at sig (Located emptyRange def) , bSignature = Nothing , bPragmas = [] @@ -1203,10 +1206,22 @@ -- | Make an unnamed module---gets the name @Main@. mkAnonymousModule :: [TopDecl PName] -> ParseM [Module PName] -mkAnonymousModule = mkTopMods Nothing - . mkModule Located { srcRange = emptyRange - , thing = mkModName [T.pack "Main"] - } +mkAnonymousModule ds = + do for_ ds \case + DParamDecl l _ -> mainParamError l + DModParam p -> mainParamError (srcRange (mpSignature p)) + DInterfaceConstraint _ ps -> mainParamError (srcRange ps) + _ -> pure () + src <- cfgSource <$> askConfig + mkTopMods Nothing $ + mkModule Located + { srcRange = emptyRange + , thing = mainModName src + } + ds + where + mainParamError l = errorMessage l + ["Unnamed module cannot be parameterized"] -- | Make a module which defines a functor instance. mkModuleInstanceAnon :: Located ModName -> @@ -1364,12 +1379,12 @@ do (m', ms) <- desugarMod m { mDocTop = doc } pure (ms ++ [m']) -mkTopSig :: Located ModName -> Signature PName -> [Module PName] -mkTopSig nm sig = +mkTopSig :: Maybe (Located Text) -> Located ModName -> Signature PName -> [Module PName] +mkTopSig doc nm sig = [ Module { mName = nm , mDef = InterfaceModule sig , mInScope = mempty - , mDocTop = Nothing + , mDocTop = doc } ] @@ -1378,18 +1393,20 @@ mkAnon :: AnonThing -> t -> t toImpName :: t -> ImpName PName -data AnonThing = AnonArg | AnonIfaceMod +data AnonThing = AnonArg Int Int + -- ^ The ints are line, column used for disambiguation + | AnonIfaceMod instance MkAnon ModName where mkAnon what = case what of - AnonArg -> modNameArg + AnonArg l c -> modNameArg l c AnonIfaceMod -> modNameIfaceMod toImpName = ImpTop instance MkAnon PName where mkAnon what = mkUnqual . case what of - AnonArg -> identAnonArg + AnonArg l c -> const (identAnonArg l c) AnonIfaceMod -> identAnonIfaceMod . getIdent toImpName = ImpNested @@ -1411,7 +1428,8 @@ [ "Instantiation of a parameterized module may not itself be " ++ "parameterized" ] _ -> pure () - let i = mkAnon AnonArg (thing (mName mo)) + let i = mkAnon (AnonArg (line pos) (col pos)) (thing (mName mo)) + pos = from (srcRange nm) nm = Located { srcRange = srcRange (mName mo), thing = i } as' = DefaultInstArg (ModuleArg . toImpName <$> nm) pure ( mo { mDef = FunctorInstance f as' mempty } @@ -1531,15 +1549,9 @@ pure (DImport (newImp <$> i) : map modTop (ms ++ [m])) where - imp = thing i iname = mkUnqual - $ identAnonIfaceMod - $ mkIdent - $ "import of " <> nm <> " at " <> Text.pack (show (pp (srcRange i))) - where - nm = case iModule imp of - ImpTop f -> modNameToText f - ImpNested n -> "submodule " <> Text.pack (show (pp n)) + $ let pos = from (srcRange i) + in identAnonInstImport (line pos) (col pos) newImp d = d { iModule = ImpNested iname , iInst = Nothing diff --git a/src/Cryptol/Parser/Position.hs b/src/Cryptol/Parser/Position.hs --- a/src/Cryptol/Parser/Position.hs +++ b/src/Cryptol/Parser/Position.hs @@ -120,6 +120,10 @@ Nothing -> go (Just l) xs Just l1 -> go (Just (rComb l l1)) xs +instance HasLoc a => HasLoc (Maybe a) where + getLoc Nothing = Nothing + getLoc (Just x) = getLoc x + class HasLoc t => AddLoc t where addLoc :: t -> Range -> t dropLoc :: t -> t diff --git a/src/Cryptol/Project.hs b/src/Cryptol/Project.hs new file mode 100644 --- /dev/null +++ b/src/Cryptol/Project.hs @@ -0,0 +1,244 @@ +{-# LANGUAGE BlockArguments #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE ScopedTypeVariables #-} +module Cryptol.Project + ( Config(..) + , loadConfig + , ScanStatus(..) + , ChangeStatus(..) + , InvalidStatus(..) + , LoadProjectMode(..) + , Parsed + , loadProject + , depMap + ) where + +import Control.Monad (void) +import Data.Foldable +import Data.Map.Strict (Map) +import qualified Data.Map.Strict as Map +import Data.Set (Set) +import qualified Data.Set as Set +import Data.Traversable +import System.Directory +import System.FilePath as FP + +import Cryptol.ModuleSystem.Base as M +import Cryptol.ModuleSystem.Env +import Cryptol.ModuleSystem.Fingerprint +import Cryptol.ModuleSystem.Monad as M +import Cryptol.Project.Config +import Cryptol.Project.Cache +import Cryptol.Project.Monad +import Cryptol.Project.WildMatch +import qualified Cryptol.Parser.AST as P +import Cryptol.Parser.Position (Located(..)) +import Control.Exception (try) + +-- | Load a project. +-- Returns information about the modules that are part of the project. +loadProject :: LoadProjectMode -> Config -> M.ModuleM (Map CacheModulePath FullFingerprint, Map ModulePath ScanStatus, Map CacheModulePath (Maybe Bool)) +loadProject mode cfg = + do (fps, statuses, out) <- runLoadM mode cfg (loadPatterns (modules cfg) >> getOldDocstringResults) + let deps = depMap [p | Scanned _ _ ps <- Map.elems statuses, p <- ps] + + let untested (InMem{}) = False + untested (InFile f) = + case out of + Left _ -> True + Right m -> Map.lookup (CacheInFile f) m /= Just (Just True) + + let needLoad = case mode of + RefreshMode -> [thing (P.mName m) | Scanned _ _ ps <- Map.elems statuses, (m, _) <- ps] + ModifiedMode -> [thing (P.mName m) | Scanned Changed _ ps <- Map.elems statuses, (m, _) <- ps] + UntestedMode -> [thing (P.mName m) | (k, Scanned ch _ ps) <- Map.assocs statuses, ch == Changed || untested k, (m, _) <- ps] + let order = loadOrder deps needLoad + + let modDetails = Map.fromList [(thing (P.mName m), (m, mp, fp)) | (mp, Scanned _ fp ps) <- Map.assocs statuses, (m, _) <- ps] + + let fingerprints = Map.fromList [(path, moduleFingerprint ffp) | (CacheInFile path, ffp) <- Map.assocs fps] + + for_ order \name -> + let (m, path, fp) = modDetails Map.! name in + -- XXX: catch modules that don't load? + doLoadModule + True {- eval -} + False {- quiet -} + (FromModule name) + path + (moduleFingerprint fp) + fingerprints + m + (Map.findWithDefault mempty name deps) + + let oldResults = + case out of + Left{} -> mempty + Right x -> x + pure (fps, statuses, oldResults) + + +-------------------------------------------------------------------------------- + +loadPatterns :: [String] -> LoadM any () +loadPatterns patterns = + do mb <- tryLoadM (doIO (map flatten <$> listDirectoryRecursive [])) + case mb of + Left{} -> pure () + Right files -> + do let files' = filter (\x -> any (`wildmatch` x) patterns) files + for_ files' scanPath + +-- | Process all .cry files in the given path. +scanPath :: FilePath -> LoadM any () +scanPath path = + tryLoadM (doIO (doesDirectoryExist path)) >>= + \case + Left {} -> pure () + + Right True -> + tryLoadM (doIO (listDirectory path)) >>= + \case + Left {} -> pure () + Right entries -> + for_ entries \entry -> scanPath (path FP. entry) + + Right False -> + -- XXX: This should probably handle other extenions + -- (literate Cryptol) + case takeExtension path of + ".cry" -> void (tryLoadM (scanFromPath path)) + -- XXX: failure: file disappeared. + _ -> pure () + + +-- | Process a particular file path. +-- Fails if we can't find the module at this path. +scanFromPath :: FilePath -> LoadM Err ScanStatus +scanFromPath fpath = + liftCallback (withPrependedSearchPath [takeDirectory fpath]) + do foundFPath <- doModule (M.findFile fpath) + mpath <- doIO (InFile <$> canonicalizePath foundFPath) + scan mpath + + +-- | Process the given module, and return information about what happened. +-- Also, saves the status of the module path. +scan :: ModulePath -> LoadM any ScanStatus +scan mpath = + + tryIt $ + do mbStat <- getStatus mpath + case mbStat of + Just status -> pure status + + Nothing -> + do (newFp,parsed) <- doParse mpath + mbOldFP <- getCachedFingerprint mpath + let needLoad = mbOldFP /= Just newFp + let deps = [ dep + | (_,ds) <- parsed + , dep@(_,otherPath) <- ds + , mpath /= otherPath + ] + mb <- checkDeps False deps + case mb of + Left (a,b) -> addScanned mpath (Invalid (InvalidDep a b)) + Right depChanges -> + do let ch = if needLoad || depChanges + then Changed else Unchanged + addScanned mpath (Scanned ch newFp parsed) + where + tryIt m = + do mb <- tryLoadM m + case mb of + Left err -> addScanned mpath (Invalid (InvalidModule err)) + Right a -> pure a + + +-- | Parse a module. +doParse :: ModulePath -> LoadM Err (FullFingerprint, Parsed) +doParse mpath = + do lab <- getModulePathLabel mpath + lPutStrLn ("Scanning " ++ lab) + + (parsed, newFp) <- + doModule + do (fi, parsed) <- parseWithDeps mpath + foreignFps <- getForeignFps (fiForeignDeps fi) + pure ( parsed + , FullFingerprint + { moduleFingerprint = fiFingerprint fi + , includeFingerprints = fiIncludeDeps fi + , foreignFingerprints = foreignFps + } + ) + addFingerprint mpath newFp + ps <- forM parsed \(m,ds) -> + do paths <- mapM findModule' ds + pure (m, zip ds paths) + pure (newFp, ps) + +-- | Get the fingerprints for external libraries. +getForeignFps :: Map FilePath Bool -> ModuleM (Set Fingerprint) +getForeignFps fsrcPaths = + Set.fromList <$> + let foundFiles = Map.keys (Map.filter id fsrcPaths) in + for foundFiles \fsrcPath -> + M.io (fingerprintFile fsrcPath) >>= + \case + Left ioe -> otherIOError fsrcPath ioe + Right fp -> pure fp + +-- | Scan the dependencies of a module. +checkDeps :: + Bool {- ^ Should we load the dependencies -} -> + [(ImportSource,ModulePath)] {- ^ The dependencies -} -> + LoadM err (Either (ImportSource,ModulePath) Bool) + -- ^ Returns `Left bad_dep` if one of the dependencies fails to load. + -- Returns `Right changes` if all dependencies were validated correctly. + -- The boolean flag `changes` indicates if any of the dependencies contain + -- changes and so we should also load the main module. +checkDeps shouldLoad ds = + case ds of + [] -> pure (Right shouldLoad) + (imp, mpath) : more -> + do status <- scan mpath + case status of + Invalid {} -> pure (Left (imp,mpath)) + Scanned ch _ _ -> + case ch of + Changed -> checkDeps True more + Unchanged -> checkDeps shouldLoad more + + +depMap :: Parsed -> Map P.ModName (Set P.ModName) +depMap xs = Map.fromList [(thing (P.mName k), Set.fromList [importedModule i | (i, _) <- v]) | (k, v) <- xs] + +loadOrder :: Map P.ModName (Set P.ModName) -> [P.ModName] -> [P.ModName] +loadOrder deps roots0 = snd (go Set.empty roots0) [] + where + go seen mms = + case mms of + [] -> (seen, id) + m : ms + | Set.member m seen -> go seen ms + | (seen1, out1) <- go (Set.insert m seen) (Set.toList (Map.findWithDefault mempty m deps)) + , (seen2, out2) <- go seen1 ms + -> (seen2, out1 . (m:) . out2) + +-- Similar to listDirectory except directories are expanded +-- when possible instead of returned in the list +listDirectoryRecursive :: [FilePath] -> IO [[FilePath]] +listDirectoryRecursive d = + do localEntries <- listDirectory (flatten d) + concat <$> for localEntries \x -> + do let x' = d ++ [x] + mb <- try (listDirectoryRecursive x') + case mb of + Left (_ :: IOError) -> pure [x'] + Right xs -> pure xs + +flatten :: [String] -> String +flatten [] = "." +flatten xs = foldr1 (\x y -> x ++ "/" ++ y) xs diff --git a/src/Cryptol/Project/Cache.hs b/src/Cryptol/Project/Cache.hs new file mode 100644 --- /dev/null +++ b/src/Cryptol/Project/Cache.hs @@ -0,0 +1,130 @@ +{-# Language OverloadedStrings, BlockArguments #-} +module Cryptol.Project.Cache where + +import Data.Map.Strict (Map) +import qualified Data.Map.Strict as Map +import qualified Data.Set as Set +import qualified Data.Text.IO as Text +import Data.Set (Set) +import System.Directory +import System.FilePath as FP +import System.IO.Error +import qualified Toml +import qualified Toml.Schema as Toml +import Cryptol.ModuleSystem.Fingerprint ( Fingerprint ) +import Cryptol.ModuleSystem.Env + +-- | The load cache. This is what persists across invocations. +newtype LoadCache = LoadCache + { cacheModules :: Map CacheModulePath CacheEntry + } + deriving (Show, Read) + +toCacheModulePath :: ModulePath -> CacheModulePath +toCacheModulePath mpath = + case mpath of + InMem x _ -> CacheInMem x + InFile x -> CacheInFile x + +data CacheModulePath + = CacheInMem String -- ^ module name + | CacheInFile FilePath -- ^ absolute file path + deriving (Show, Read, Ord, Eq) + +instance Toml.ToValue LoadCache where + toValue = Toml.defaultTableToValue + +instance Toml.ToTable LoadCache where + toTable x = Toml.table [ + "version" Toml..= (1 :: Int), -- increase this to invalidate old files + -- also look at the `Toml.FromValue` instance + "modules" Toml..= [ + Toml.table $ [ + case k of + CacheInFile a -> "file" Toml..= a + CacheInMem a -> "memory" Toml..= a, + "fingerprint" Toml..= moduleFingerprint fp, + "foreign_fingerprints" Toml..= Set.toList (foreignFingerprints fp), + "include_fingerprints" Toml..= [ + Toml.table [ + "file" Toml..= k1, + "fingerprint" Toml..= v1 + ] + | (k1, v1) <- Map.assocs (includeFingerprints fp) + ] + ] ++ + [ "docstring_result" Toml..= result + | Just result <- [cacheDocstringResult v] + ] + | (k,v) <- Map.assocs (cacheModules x) + , let fp = cacheFingerprint v + ]] + +instance Toml.FromValue LoadCache where + fromValue = Toml.parseTableFromValue + do 1 <- Toml.reqKey "version" :: Toml.ParseTable l Int + kvs <- Toml.reqKeyOf "modules" + $ Toml.listOf \ _ix -> + Toml.parseTableFromValue + do k <- Toml.pickKey [ + Toml.Key "memory" (fmap CacheInMem . Toml.fromValue), + Toml.Key "file" (fmap CacheInFile . Toml.fromValue) + ] + fp <- Toml.reqKey "fingerprint" + foreigns <- Toml.reqKey "foreign_fingerprints" + includes <- Toml.reqKeyOf "include_fingerprints" + $ Toml.listOf \ _ix -> + Toml.parseTableFromValue + $ (,) <$> Toml.reqKey "file" + <*> Toml.reqKey "fingerprint" + checkResult <- Toml.optKey "docstring_result" + pure (k, CacheEntry + { cacheFingerprint = FullFingerprint + { moduleFingerprint = fp + , foreignFingerprints = Set.fromList foreigns + , includeFingerprints = Map.fromList includes + } + , cacheDocstringResult = checkResult + }) + pure LoadCache { + cacheModules = Map.fromList kvs + } + +data CacheEntry = CacheEntry + { cacheFingerprint :: FullFingerprint + , cacheDocstringResult :: Maybe Bool + } + deriving (Show, Read) + +-- | The full fingerprint hashes the module, but +-- also the contents of included files and foreign libraries. +data FullFingerprint = FullFingerprint + { moduleFingerprint :: Fingerprint + , includeFingerprints :: Map FilePath Fingerprint + , foreignFingerprints :: Set Fingerprint + } + deriving (Eq, Show, Read) + +-- | Directory where to store the project state. +-- XXX: This should probably be a parameter +metaDir :: FilePath +metaDir = ".cryproject" + +loadCachePath :: FilePath +loadCachePath = metaDir FP. "loadcache.toml" + +emptyLoadCache :: LoadCache +emptyLoadCache = LoadCache { cacheModules = mempty } + +loadLoadCache :: IO LoadCache +loadLoadCache = + do txt <- Text.readFile loadCachePath + case Toml.decode txt of + Toml.Success _ c -> pure c + Toml.Failure _ -> pure emptyLoadCache + `catchIOError` \_ -> pure emptyLoadCache + +saveLoadCache :: LoadCache -> IO () +saveLoadCache cache = + do createDirectoryIfMissing False metaDir + writeFile loadCachePath (show (Toml.encode cache)) diff --git a/src/Cryptol/Project/Config.hs b/src/Cryptol/Project/Config.hs new file mode 100644 --- /dev/null +++ b/src/Cryptol/Project/Config.hs @@ -0,0 +1,75 @@ +{-# LANGUAGE BlockArguments #-} +{-# LANGUAGE OverloadedStrings #-} +module Cryptol.Project.Config where + +import Data.Maybe (fromMaybe) +import qualified Data.Text.IO as Text +import Toml +import Toml.Schema +import Data.Bifunctor (first) +import System.Directory +import System.FilePath as FP +import System.IO.Error + +import Cryptol.Utils.PP as PP + +data Config = Config + { root :: FilePath + -- ^ The root of the project. + + , modules :: [String] + -- ^ Git-style patterns describing the files for the project. + } + +data LoadProjectMode + = RefreshMode -- load all files + | ModifiedMode -- load modified files + | UntestedMode -- load files without a successful test result + deriving Show + +instance FromValue Config where + fromValue = + parseTableFromValue + do mbRoot <- optKey "root" + mods <- reqKey "modules" + pure Config + { root = fromMaybe "." mbRoot + , modules = mods + } + +data ConfigLoadError = ConfigLoadError FilePath ConfigLoadErrorInfo + deriving Show + +data ConfigLoadErrorInfo + = ConfigParseError [String] + | SetRootFailed IOError + deriving Show + +instance PP ConfigLoadError where + ppPrec _ (ConfigLoadError path info) = + case info of + ConfigParseError errs -> text (unlines errs) + SetRootFailed ioe -> + hang topMsg + 4 (hang "Failed to set project root:" + 4 (text (show ioe))) + where + topMsg = "Error loading project configuration" <+> text path PP.<.> ":" + +-- | Parse project configuration. +loadConfig :: FilePath -> IO (Either ConfigLoadError Config) +loadConfig path = + do isDir <- doesDirectoryExist path + let filePath = if isDir then path FP. "cryproject.toml" else path + -- Use strict IO since we are writing to the same file later + file <- Text.readFile filePath + first (ConfigLoadError filePath) <$> + case decode file of + Failure errs -> pure (Left (ConfigParseError errs)) + Success _warns config -> + first SetRootFailed <$> + tryIOError + do dir <- canonicalizePath + (takeDirectory filePath FP. root config) + setCurrentDirectory dir + pure config { root = dir } diff --git a/src/Cryptol/Project/Monad.hs b/src/Cryptol/Project/Monad.hs new file mode 100644 --- /dev/null +++ b/src/Cryptol/Project/Monad.hs @@ -0,0 +1,214 @@ +{-# LANGUAGE BlockArguments #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE GeneralizedNewtypeDeriving #-} +module Cryptol.Project.Monad + ( LoadM, Err, NoErr + , ScanStatus(..), ChangeStatus(..), InvalidStatus(..), Parsed + , LoadProjectMode(..) + , runLoadM + , doModule + , doModuleNonFail + , doIO + , tryLoadM + , liftCallback + , addFingerprint + , addScanned + , getModulePathLabel + , getCachedFingerprint + , findModule' + , getStatus + , getFingerprint + , lPutStrLn + , getOldDocstringResults + ) where + +import Data.Map.Strict (Map) +import qualified Data.Map.Strict as Map +import Control.Monad.Reader +import Control.Monad.State +import Control.Monad.Except hiding (tryError) +import System.Directory +import System.FilePath (makeRelative) + +import Cryptol.Utils.Ident +import Cryptol.Parser.AST (Module,PName) +import Cryptol.ModuleSystem.Base as M +import Cryptol.ModuleSystem.Monad as M +import Cryptol.ModuleSystem.Env +import Cryptol.Utils.Logger (logPutStrLn) + +import Cryptol.Project.Config +import Cryptol.Project.Cache + +newtype LoadM err a = + LoadM (ReaderT LoadConfig (ExceptT ModuleError (StateT LoadState ModuleM)) a) + deriving (Functor,Applicative,Monad) + +-- | Computations may raise an error +data Err + +-- | Computations may not raise errors +data NoErr + +type Parsed = [ (Module PName, [(ImportSource, ModulePath)]) ] + +data ScanStatus = + Scanned ChangeStatus FullFingerprint Parsed + | Invalid InvalidStatus + deriving Show + +data ChangeStatus = + Changed -- ^ The module, or one of its dependencies changed. + | Unchanged -- ^ The module did not change. + deriving (Eq, Show) + +data InvalidStatus = + InvalidModule ModuleError + -- ^ Error in one of the modules in this file + + | InvalidDep ImportSource ModulePath + -- ^ Error in one of our dependencies + deriving Show + + +data LoadState = LoadState + { findModuleCache :: Map (ModName, [FilePath]) ModulePath + -- ^ Map (module name, search path) -> module path + + , fingerprints :: Map CacheModulePath FullFingerprint + -- ^ Hashes of known things. + + , scanned :: Map ModulePath ScanStatus + -- ^ Information about the proccessed top-level modules. + } + + +-- | Information about the current project. +data LoadConfig = LoadConfig + { canonRoot :: FilePath + -- ^ Path to the project root, cannoicalized. + + , loadCache :: LoadCache + -- ^ The state of the cache before we started loading the project. + } + + +-- | Do an operation in the module monad. +doModuleNonFail :: M.ModuleM a -> LoadM any a +doModuleNonFail m = + do mb <- LoadM (lift (lift (lift (M.tryModule m)))) + case mb of + Left err -> LoadM (throwError err) + Right a -> pure a + +-- | Do an operation in the module monad. +doModule :: M.ModuleM a -> LoadM Err a +doModule = doModuleNonFail + +-- | Do an operation in the IO monad +doIO :: IO a -> LoadM Err a +doIO m = doModule (M.io m) + +tryLoadM :: LoadM Err a -> LoadM any (Either M.ModuleError a) +tryLoadM (LoadM m) = LoadM (tryError m) + +-- Introduced in mtl-2.3.1 which we can't rely upon yet +tryError :: MonadError e m => m a -> m (Either e a) +tryError action = (Right <$> action) `catchError` (pure . Left) + +-- | Print a line +lPutStrLn :: String -> LoadM any () +lPutStrLn msg = doModuleNonFail (withLogger logPutStrLn msg) + +-- | Lift a module level operation to the LoadM monad. +liftCallback :: (forall a. ModuleM a -> ModuleM a) -> LoadM any b -> LoadM Err b +liftCallback f (LoadM m) = + do r <- LoadM ask + s <- LoadM get + (mb,s1) <- doModule (f (runStateT (runExceptT (runReaderT m r)) s)) + LoadM (put s1) + case mb of + Left err -> LoadM (throwError err) + Right a -> pure a + +-- | Run a LoadM computation using the given configuration. +runLoadM :: + LoadProjectMode {- ^ force a refresh -} -> + Config -> + LoadM NoErr a -> + M.ModuleM (Map CacheModulePath FullFingerprint, Map ModulePath ScanStatus, Either ModuleError a) +runLoadM mode cfg (LoadM m) = + do loadCfg <- + M.io + do path <- canonicalizePath (root cfg) + cache <- case mode of + RefreshMode -> pure emptyLoadCache + UntestedMode -> loadLoadCache + ModifiedMode -> loadLoadCache + pure LoadConfig { canonRoot = path + , loadCache = cache + } + let loadState = LoadState { findModuleCache = mempty + , fingerprints = mempty + , scanned = mempty + } + (result, s) <- runStateT (runExceptT (runReaderT m loadCfg)) loadState + pure (fingerprints s, scanned s, result) + +addFingerprint :: ModulePath -> FullFingerprint -> LoadM any () +addFingerprint mpath fp = + LoadM + (modify' \ls -> ls { fingerprints = Map.insert (toCacheModulePath mpath) fp (fingerprints ls) }) + + +-- | Add information about the status of a module path. +addScanned :: ModulePath -> ScanStatus -> LoadM any ScanStatus +addScanned mpath status = + do LoadM + (modify' \ls -> ls { scanned = Map.insert mpath status (scanned ls) }) + pure status + + +-- | Get a label for the given module path. +-- Typically used for output. +getModulePathLabel :: ModulePath -> LoadM any String +getModulePathLabel mpath = + case mpath of + InFile p -> LoadM (asks ((`makeRelative` p) . canonRoot)) + InMem l _ -> pure l + + +-- | Get the fingerprint for the given module path. +getCachedFingerprint :: ModulePath -> LoadM any (Maybe FullFingerprint) +getCachedFingerprint mpath = + LoadM (asks (fmap cacheFingerprint . Map.lookup (toCacheModulePath mpath) . cacheModules . loadCache)) + + +-- | Module path for the given import +findModule' :: ImportSource -> LoadM Err ModulePath +findModule' isrc = + do ls <- LoadM get + let mname = modNameToNormalModName (importedModule isrc) + searchPath <- doModule M.getSearchPath + case Map.lookup (mname, searchPath) (findModuleCache ls) of + Just mpath -> pure mpath + Nothing -> + do modLoc <- doModule (findModule mname) + mpath <- case modLoc of + InFile path -> InFile <$> doIO (canonicalizePath path) + InMem l c -> pure (InMem l c) + LoadM $ put ls { findModuleCache = Map.insert (mname, searchPath) + mpath (findModuleCache ls) } + pure mpath + +-- | Check if the given file has beein processed. +getStatus :: ModulePath -> LoadM any (Maybe ScanStatus) +getStatus mpath = LoadM (gets (Map.lookup mpath . scanned)) + +-- | Get the fingerpint for the ginve path, if any. +getFingerprint :: ModulePath -> LoadM any (Maybe FullFingerprint) +getFingerprint mpath = LoadM (gets (Map.lookup (toCacheModulePath mpath) . fingerprints)) + +getOldDocstringResults :: LoadM any (Map CacheModulePath (Maybe Bool)) +getOldDocstringResults = + LoadM (asks (fmap cacheDocstringResult . cacheModules . loadCache)) diff --git a/src/Cryptol/Project/WildMatch.hs b/src/Cryptol/Project/WildMatch.hs new file mode 100644 --- /dev/null +++ b/src/Cryptol/Project/WildMatch.hs @@ -0,0 +1,110 @@ +{- | +This module follows the convention found in +-} +module Cryptol.Project.WildMatch (wildmatch) where + +import Data.Char +import System.FilePath + +-- | `wildmatch p x` checks if file `x` matches pattern `p`. +wildmatch :: String -> FilePath -> Bool +wildmatch mbNegP x + -- When a pattern contains a path separator, it matches the whole path + | '/' `elem` p = mbNeg (matchP (ensureLeadingSlash p) (ensureLeadingSlash x)) + -- When the pattern contains no path separator it only matches the filename + | otherwise = mbNeg (matchP p (takeFileName x)) + where + (mbNeg,p) = + case mbNegP of + '!':rest -> (not,rest) + _ -> (id,mbNegP) + + +-- | Normalize a path pattern to start with a leading slash for consistency later +ensureLeadingSlash :: String -> String +ensureLeadingSlash ('/':p) = '/':p +ensureLeadingSlash p = '/':p + +------------------ +-- Path processing +------------------ + +matchP :: String -> FilePath -> Bool + +matchP "/**" _ = True -- Accepts everything + +matchP ('/':'*':'*':'/':p) ('/':xs) = + matchP ('/':p) ('/':xs) || + matchP ('/':'*':'*':'/':p) (dropWhile ('/'/=) xs) + +matchP ('/':'*':'*':'/':_p) _ = False + +-- escaped characters match literally +matchP ('\\':a:p) (x:xs) = a==x && matchP p xs +matchP ('\\':_) "" = False + +-- match zero or more component characters +matchP ('*':p) (x:xs) = matchP p (x:xs) || ('/' /= x) && matchP ('*':p) xs +matchP ('*':p) "" = matchP p "" + +-- match zero or one component characters +matchP ('?':p) (x : xs) = matchP p (x : xs) || ('/' /= x) && matchP p xs +matchP ('?':p) "" = matchP p "" + +-- process a character class +matchP ('[':p) (x:xs) + | x == '/' = False + | Just (f, p') <- parseCharClass p = f x && matchP p' xs +matchP ('[':_) _ = False + +-- literal match +matchP (a:p) (x:xs) = a==x && matchP p xs +matchP (_a:_p) "" = False + +matchP "" xs = null xs + +----------------------------- +-- Character class processing +----------------------------- + +parseCharClass :: String -> Maybe (Char -> Bool, String) + +-- leading ! negates a character class +parseCharClass ('!':p) = + do (f, p') <- parseCharClass1 True p + Just (not . f, p') +parseCharClass p = parseCharClass1 True p + +-- A ] in the first position is a literal match +parseCharClass1 :: Bool -> [Char] -> Maybe (Char -> Bool, [Char]) +parseCharClass1 False (']':p) = + Just (const False, p) + +parseCharClass1 first (x:'-':y:p) + | first || x /= ']', y /= ']' = cc (\c -> x <= c && c <= y) p + +parseCharClass1 _ ('[':':':p) = + case span (\x -> 'a' <= x && x <= 'z') p of + ("alnum", ':':']':p1) -> cc isAlphaNum p1 + ("cntrl", ':':']':p1) -> cc isControl p1 + ("lower", ':':']':p1) -> cc isLower p1 + ("space", ':':']':p1) -> cc isSpace p1 + ("alpha", ':':']':p1) -> cc isAlpha p1 + ("digit", ':':']':p1) -> cc isDigit p1 + ("print", ':':']':p1) -> cc isPrint p1 + ("upper", ':':']':p1) -> cc isUpper p1 + ("blank", ':':']':p1) -> cc (`elem` " \t") p1 + ("graph", ':':']':p1) -> cc (\x -> isAlphaNum x || isPunctuation x) p1 + ("punct", ':':']':p1) -> cc isPunctuation p1 + ("xdigit", ':':']':p1) -> cc isHexDigit p1 + (_ , ':':']':_) -> Nothing + _ -> cc ('['==) (':':p) + +parseCharClass1 _ (x:p) = cc (x==) p +parseCharClass1 _ "" = Nothing + +-- Helper for continuing to build a character class matcher +cc :: (Char -> Bool) -> [Char] -> Maybe (Char -> Bool, [Char]) +cc f p = + do (g, p') <- parseCharClass1 False p + Just (\x -> f x || g x, p') 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 @@ -10,10 +10,10 @@ {-# LANGUAGE BlockArguments #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE LambdaCase #-} -{-# LANGUAGE MultiWayIf #-} {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE PatternGuards #-} {-# LANGUAGE RecordWildCards #-} +{-# LANGUAGE ScopedTypeVariables #-} -- See Note [-Wincomplete-uni-patterns and irrefutable patterns] in Cryptol.TypeCheck.TypePat {-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-} module Cryptol.REPL.Command ( @@ -55,11 +55,14 @@ , handleCtrlC , sanitize , withRWTempFile + , printModuleWarnings -- To support Notebook interface (might need to refactor) , replParse , liftModuleCmd , moduleCmdResult + + , loadProjectREPL ) where import Cryptol.REPL.Monad @@ -74,6 +77,7 @@ import qualified Cryptol.ModuleSystem.NamingEnv as M import qualified Cryptol.ModuleSystem.Renamer as M (RenamerWarning(SymbolShadowed, PrefixAssocChanged)) +import qualified Cryptol.Utils.Logger as Logger import qualified Cryptol.Utils.Ident as M import qualified Cryptol.ModuleSystem.Env as M import Cryptol.ModuleSystem.Fingerprint(fingerprintHexString) @@ -106,6 +110,7 @@ import Cryptol.Utils.Panic(panic) import Cryptol.Utils.RecordMap import qualified Cryptol.Parser.AST as P +import qualified Cryptol.Project as Proj import qualified Cryptol.Transform.Specialize as S import Cryptol.Symbolic ( ProverCommand(..), QueryType(..) @@ -122,6 +127,7 @@ import Text.Read (readMaybe) import Control.Applicative ((<|>)) import qualified Data.Set as Set +import qualified Data.Map.Strict as Map import Data.ByteString (ByteString) import qualified Data.ByteString as BS import qualified Data.ByteString.Char8 as BS8 @@ -129,7 +135,6 @@ import Data.Char (isSpace,isPunctuation,isSymbol,isAlphaNum,isAscii) import Data.Function (on) import Data.List (intercalate, nub, isPrefixOf) -import qualified Data.Map as Map import Data.Maybe (fromMaybe,mapMaybe,isNothing) import System.Environment (lookupEnv) import System.Exit (ExitCode(ExitSuccess)) @@ -146,7 +151,7 @@ import qualified System.Random.TF.Instances as TFI import Numeric (showFFloat) import qualified Data.Text as T -import Data.IORef(newIORef, readIORef, writeIORef, modifyIORef) +import Data.IORef(newIORef, readIORef, writeIORef) import GHC.Float (log1p, expm1) @@ -155,6 +160,8 @@ import qualified Data.SBV.Internals as SBV (showTDiff) import Data.Foldable (foldl') +import qualified Cryptol.Project.Cache as Proj +import Cryptol.Project.Monad (LoadProjectMode) @@ -351,6 +358,7 @@ , "expression into a file. The first column in each line is" , "the expected output, and the remainder are the inputs. The" , "number of tests is determined by the \"tests\" option." + , "Use filename \"-\" to write tests to stdout." ]) "" , CommandDescr [ ":generate-foreign-header" ] ["FILE"] (FilenameArg genHeaderCmd) @@ -473,12 +481,13 @@ Nothing -> raise (TypeNotTestable ty) Just gens -> return gens tests <- withRandomGen (\g -> io $ TestR.returnTests' g gens val testNum) - out <- forM tests $ + outs <- forM tests $ \(args, x) -> do argOut <- mapM (rEval . E.ppValue Concrete ppopts) args resOut <- rEval (E.ppValue Concrete ppopts x) return (renderOneLine resOut ++ "\t" ++ intercalate "\t" (map renderOneLine argOut) ++ "\n") - writeResult <- io $ X.try (writeFile outFile (concat out)) + let out = concat outs + writeResult <- io (X.try (if outFile == "-" then putStr out else writeFile outFile out)) case writeResult of Right{} -> pure emptyCommandResult Left e -> @@ -505,7 +514,7 @@ do let str = nameStr x rPutStr $ "property " ++ str ++ " " let texpr = T.EVar x - let schema = M.ifDeclSig d + let schema = T.dSignature d nd <- M.mctxNameDisp <$> getFocusedEnv let doc = fixNameDisp nd (pp texpr) testReport <- qcExpr qcMode doc texpr schema @@ -827,7 +836,7 @@ then rPutStr $ ":sat " ++ str ++ "\n\t" else rPutStr $ ":prove " ++ str ++ "\n\t" let texpr = T.EVar x - let schema = M.ifDeclSig d + let schema = T.dSignature d nd <- M.mctxNameDisp <$> getFocusedEnv let doc = fixNameDisp nd (pp texpr) success <- proveSatExpr isSat (M.nameLoc x) doc texpr schema @@ -1340,7 +1349,7 @@ Nothing -> do rPutStrLn "Invalid module name." pure emptyCommandResult { crSuccess = False } - + Just pimpName -> do impName <- liftModuleCmd (setFocusedModuleCmd pimpName) mb <- getLoadedMod @@ -1585,25 +1594,12 @@ getPrimMap = liftModuleCmd M.getPrimMap liftModuleCmd :: M.ModuleCmd a -> REPL a -liftModuleCmd cmd = - do evo <- getEvalOptsAction - env <- getModuleEnv - callStacks <- getCallStacks - tcSolver <- getTCSolver - let minp = - M.ModuleInput - { minpCallStacks = callStacks - , minpEvalOpts = evo - , minpByteReader = BS.readFile - , minpModuleEnv = env - , minpTCSolver = tcSolver - } - moduleCmdResult =<< io (cmd minp) +liftModuleCmd cmd = moduleCmdResult =<< io . cmd =<< getModuleInput --- TODO: add filter for my exhaustie prop guards warning here +-- TODO: add filter for my exhaustive prop guards warning here -moduleCmdResult :: M.ModuleRes a -> REPL a -moduleCmdResult (res,ws0) = do +printModuleWarnings :: [M.ModuleWarning] -> REPL () +printModuleWarnings ws0 = do warnDefaulting <- getKnownUser "warnDefaulting" warnShadowing <- getKnownUser "warnShadowing" warnPrefixAssoc <- getKnownUser "warnPrefixAssoc" @@ -1642,6 +1638,10 @@ $ ws0 names <- M.mctxNameDisp <$> getFocusedEnv mapM_ (rPrint . runDoc names . pp) ws + +moduleCmdResult :: M.ModuleRes a -> REPL a +moduleCmdResult (res,ws) = do + printModuleWarnings ws case res of Right (a,me') -> setModuleEnv me' >> return a Left err -> @@ -1653,6 +1653,7 @@ do setEditPath file return e _ -> return err + names <- M.mctxNameDisp <$> getFocusedEnv raise (ModuleSystemError names e) @@ -1985,7 +1986,7 @@ mapM_ (\j -> rPutStrLn (" , " ++ f j)) is rPutStrLn " ]" - depList show "includes" (Set.toList (M.fiIncludeDeps fi)) + depList show "includes" (Map.keys (M.fiIncludeDeps fi)) depList (show . show . pp) "imports" (Set.toList (M.fiImportDeps fi)) depList show "foreign" (Map.toList (M.fiForeignDeps fi)) @@ -2062,58 +2063,88 @@ checkBlock :: [T.Text] {- ^ lines of the code block -} -> REPL [SubcommandResult] -checkBlock = isolated . go +checkBlock = isolated . go . continuedLines where go [] = pure [] - go (line:block) = - case parseCommand (findNbCommand True) (T.unpack line) of - Nothing -> do - pure [SubcommandResult - { srInput = line - , srLog = "Failed to parse command" - , srResult = emptyCommandResult { crSuccess = False } - }] - Just Ambiguous{} -> do - pure [SubcommandResult - { srInput = line - , srLog = "Ambiguous command" - , srResult = emptyCommandResult { crSuccess = False } - }] - Just Unknown{} -> do - pure [SubcommandResult - { srInput = line - , srLog = "Unknown command" - , srResult = emptyCommandResult { crSuccess = False } - }] - Just (Command cmd) -> do - (logtxt, eresult) <- captureLog (Cryptol.REPL.Monad.try (cmd 0 Nothing)) - case eresult of - Left e -> do - let result = SubcommandResult + go (line:block) + | T.all isSpace line = go block + | otherwise = + do let tab n = replicate n ' ' + rPutStrLn (tab 4 ++ T.unpack line) + let doErr msg = + do rPutStrLn (tab 6 ++ msg) + pure [SubcommandResult { srInput = line - , srLog = logtxt ++ show (pp e) ++ "\n" + , srLog = msg , srResult = emptyCommandResult { crSuccess = False } - } - pure [result] - Right result -> do - let subresult = SubcommandResult - { srInput = line - , srLog = logtxt - , srResult = result - } - subresults <- checkBlock block - pure (subresult : subresults) + }] + case parseCommand (findNbCommand True) (T.unpack line) of + Nothing -> doErr "Failed to parse command" + Just Ambiguous{} -> doErr "Ambiguous command" + Just Unknown{} -> doErr "Unknown command" + Just (Command cmd) -> do + (logtxt, eresult) <- captureLog (Cryptol.REPL.Monad.try (cmd 0 Nothing)) + case eresult of + Left e -> do + let result = SubcommandResult + { srInput = line + , srLog = logtxt ++ show (pp e) ++ "\n" + , srResult = emptyCommandResult { crSuccess = False } + } + pure [result] + Right result -> do + let subresult = SubcommandResult + { srInput = line + , srLog = logtxt + , srResult = result + } + subresults <- checkBlock block + pure (subresult : subresults) +-- | Combine lines ending in a backslash with the next line. +continuedLines :: [T.Text] -> [T.Text] +continuedLines xs = + case span ("\\" `T.isSuffixOf`) xs of + ([], []) -> [] + (a, []) -> [concat' (map T.init a)] -- permissive + (a, b:bs) -> concat' (map T.init a ++ [b]) : continuedLines bs + where + -- concat that eats leading whitespace between elements + concat' [] = T.empty + concat' (y:ys) = T.concat (y : map (T.dropWhile isSpace) ys) + + captureLog :: REPL a -> REPL (String, a) captureLog m = do previousLogger <- getLogger outputsRef <- io (newIORef []) - setPutStr (\str -> modifyIORef outputsRef (str:)) + setPutStr $ \str -> + unless (null str) $ + do lns <- readIORef outputsRef + let msg = preTab lns (postTab str) + Logger.logPutStr previousLogger msg + writeIORef outputsRef (str:lns) result <- m `finally` setLogger previousLogger outputs <- io (readIORef outputsRef) let output = interpretControls (concat (reverse outputs)) pure (output, result) + where + tab = replicate 6 ' ' + preTab prevLns msg = + case prevLns of + l : _ + | last l /= '\n' -> msg + _ -> tab ++ msg + + postTab cs = + case cs of + [] -> "" + ['\n'] -> "\n" + '\n' : more -> '\n' : tab ++ postTab more + c : more -> c : postTab more + + -- | Apply control character semantics to the result of the logger interpretControls :: String -> String interpretControls ('\b' : xs) = interpretControls xs @@ -2130,7 +2161,8 @@ -- | Check all the code blocks in a given docstring. checkDocItem :: T.DocItem -> REPL DocstringResult checkDocItem item = - do xs <- case traverse extractCodeBlocks (T.docText item) of + do rPrint (" Docstrings on" <+> pp (T.docFor item)) + xs <- case traverse extractCodeBlocks (T.docText item) of [] -> pure [] -- optimization bs -> Ex.bracket @@ -2150,9 +2182,31 @@ checkDocStrings :: M.LoadedModule -> REPL [DocstringResult] checkDocStrings m = do let dat = M.lmdModule (M.lmData m) + rPrint ("Checking module" <+> pp (T.mName dat)) let ds = T.gatherModuleDocstrings (M.ifaceNameToModuleMap (M.lmInterface m)) dat - traverse checkDocItem ds + results <- traverse checkDocItem ds + updateDocstringCache m (all checkDocstringResult results) + pure results +checkDocstringResult :: DocstringResult -> Bool +checkDocstringResult r = all (all (crSuccess . srResult)) (drFences r) + +updateDocstringCache :: M.LoadedModule -> Bool -> REPL () +updateDocstringCache m result = + do cache <- io Proj.loadLoadCache + case M.lmFilePath m of + M.InMem{} -> pure () + M.InFile fp -> + case Map.lookup (Proj.CacheInFile fp) (Proj.cacheModules cache) of + Nothing -> pure () + Just entry -> + if Proj.moduleFingerprint (Proj.cacheFingerprint entry) /= M.fiFingerprint (M.lmFileInfo m) + then pure () + else + do let entry' = entry { Proj.cacheDocstringResult = Just result } + let cache' = cache { Proj.cacheModules = Map.insert (Proj.CacheInFile fp) entry' (Proj.cacheModules cache) } + io (Proj.saveLoadCache cache') + -- | Evaluate all the docstrings in the specified module. -- -- This command succeeds when: @@ -2169,56 +2223,127 @@ Nothing -> do rPutStrLn "No current module" pure emptyCommandResult { crSuccess = False } - Just mn -> checkModName mn + Just mn -> checkModName 0 mn | otherwise = case parseModName input of Nothing -> do rPutStrLn "Invalid module name" pure emptyCommandResult { crSuccess = False } - Just mn -> checkModName mn + Just mn -> checkModName 0 mn +countOutcomes :: [[SubcommandResult]] -> (Int, Int, Int) +countOutcomes = foldl' countOutcomes1 (0, 0, 0) where + countOutcomes1 (successes, nofences, failures) [] + = (successes, nofences + 1, failures) + countOutcomes1 acc result = foldl' countOutcomes2 acc result - countOutcomes :: [[SubcommandResult]] -> (Int, Int, Int) - countOutcomes = foldl' countOutcomes1 (0, 0, 0) - where - countOutcomes1 (successes, nofences, failures) [] - = (successes, nofences + 1, failures) - countOutcomes1 acc result = foldl' countOutcomes2 acc result + countOutcomes2 (successes, nofences, failures) result + | crSuccess (srResult result) = (successes + 1, nofences, failures) + | otherwise = (successes, nofences, failures + 1) - countOutcomes2 (successes, nofences, failures) result - | crSuccess (srResult result) = (successes + 1, nofences, failures) - | otherwise = (successes, nofences, failures + 1) +checkModName :: Int -> P.ModName -> REPL CommandResult +checkModName ind mn = + do env <- getModuleEnv + case M.lookupModule mn env of + Nothing -> + case M.lookupSignature mn env of + Nothing -> + do rPutStrLn (tab ++ "Module " ++ show mn ++ " is not loaded") + pure emptyCommandResult { crSuccess = False } + Just{} -> + do rPutStrLn (tab ++ "Skipping docstrings on interface module") + pure emptyCommandResult + Just fe + | T.isParametrizedModule (M.lmdModule (M.lmData fe)) -> do + rPutStrLn (tab ++ "Skipping docstrings on parameterized module") + pure emptyCommandResult + | otherwise -> do + results <- checkDocStrings fe + let (successes, nofences, failures) = countOutcomes [concat (drFences r) | r <- results] + rPutStrLn (tab ++ "Successes: " ++ show successes ++ + ", No fences: " ++ show nofences ++ + ", Failures: " ++ show failures) + pure emptyCommandResult { crSuccess = failures == 0 } + where + tab = replicate ind ' ' - checkModName :: P.ModName -> REPL CommandResult - checkModName mn = do - mb <- M.lookupModule mn <$> getModuleEnv - case mb of - Nothing -> do - rPutStrLn ("Module " ++ show input ++ " is not loaded") - pure emptyCommandResult { crSuccess = False } +-- | Load a project. +-- Note that this does not update the Cryptol environment, it only updates +-- the project cache. +loadProjectREPL :: LoadProjectMode -> Proj.Config -> REPL CommandResult +loadProjectREPL mode cfg = + do minp <- getModuleInput + (res, warnings) <- io $ M.runModuleM minp $ Proj.loadProject mode cfg + printModuleWarnings warnings + case res of + Left err -> + do names <- M.mctxNameDisp <$> getFocusedEnv + rPrint (pp (ModuleSystemError names err)) + pure emptyCommandResult { crSuccess = False } - Just fe - | T.isParametrizedModule (M.lmdModule (M.lmData fe)) -> do - rPutStrLn "Skipping docstrings on parameterized module" - pure emptyCommandResult + Right ((fps, mp, docstringResults),env) -> + do setModuleEnv env + let cache0 = fmap (\fp -> Proj.CacheEntry { cacheDocstringResult = Nothing, cacheFingerprint = fp }) fps + (cache, success) <- + foldM (\(fpAcc_, success_) (k, v) -> + case k of + M.InMem{} -> pure (fpAcc_, success_) + M.InFile path -> + case v of + Proj.Invalid e -> + do rPrint ("Failed to process module:" <+> (text path <> ":") $$ + indent 2 (ppInvalidStatus e)) + pure (fpAcc_, False) -- report failure + Proj.Scanned Proj.Unchanged _ ms -> + foldM f (fpAcc_, success_) ms + where + f (fpAcc, success) (m, _) = + do let name = P.thing (P.mName m) + case join (Map.lookup (Proj.CacheInFile path) docstringResults) of + Just True -> + do rPrint ("Checking module" <+> hcat [pp name, ": PASS (cached)"]) + let fpAcc' = Map.adjust (\e -> e{ Proj.cacheDocstringResult = Just True }) (Proj.CacheInFile path) fpAcc + pure (fpAcc', success) -- preserve success - | otherwise -> do - results <- checkDocStrings fe - let (successes, nofences, failures) = countOutcomes [concat (drFences r) | r <- results] + Just False -> + do rPrint ("Checking module" <+> hcat [pp name, ": FAIL (cached)"]) + let fpAcc' = Map.adjust (\e -> e{ Proj.cacheDocstringResult = Just False }) (Proj.CacheInFile path) fpAcc + pure (fpAcc', False) -- preserve failure - forM_ results $ \dr -> - unless (null (drFences dr)) $ - do rPutStrLn "" - rPutStrLn ("\nChecking " ++ show (pp (drName dr))) - forM_ (drFences dr) $ \fence -> - forM_ fence $ \line -> do - rPutStrLn "" - rPutStrLn (T.unpack (srInput line)) - rPutStr (srLog line) + Nothing -> + do checkRes <- checkModName 2 name + let success1 = crSuccess checkRes + let fpAcc' = Map.adjust (\e -> e{ Proj.cacheDocstringResult = Just success1 }) (Proj.CacheInFile path) fpAcc + pure (fpAcc', success && success1) - rPutStrLn "" - rPutStrLn ("Successes: " ++ show successes ++ ", No fences: " ++ show nofences ++ ", Failures: " ++ show failures) + Proj.Scanned Proj.Changed _ ms -> + foldM f (fpAcc_, success_) ms + where + f (fpAcc, success) (m, _) = + do let name = P.thing (P.mName m) + checkRes <- checkModName 2 name + let fpAcc' = Map.adjust (\fp -> fp { Proj.cacheDocstringResult = Just (crSuccess checkRes) }) (Proj.CacheInFile path) fpAcc + pure (fpAcc', success && crSuccess checkRes) - pure emptyCommandResult { crSuccess = failures == 0 } + ) (cache0, True) (Map.assocs mp) + + let (passing, failing, missing) = + foldl + (\(a,b,c) x -> + case Proj.cacheDocstringResult x of + Nothing -> (a,b,c+1) + Just True -> (a+1,b,c) + Just False -> (a,b+1,c)) + (0::Int,0::Int,0::Int) (Map.elems cache) + + rPutStrLn ("Passing: " ++ show passing ++ ", Failing: " ++ show failing ++ ", Missing: " ++ show missing) + + io (Proj.saveLoadCache (Proj.LoadCache cache)) + pure emptyCommandResult { crSuccess = success } + +ppInvalidStatus :: Proj.InvalidStatus -> Doc +ppInvalidStatus = \case + Proj.InvalidModule modErr -> pp modErr + Proj.InvalidDep d _ -> "Error in dependency: " <> pp d diff --git a/src/Cryptol/REPL/Monad.hs b/src/Cryptol/REPL/Monad.hs --- a/src/Cryptol/REPL/Monad.hs +++ b/src/Cryptol/REPL/Monad.hs @@ -63,6 +63,7 @@ , withRandomGen , setRandomGen , getRandomGen + , getModuleInput -- ** Config Options , EnvVal(..) @@ -127,6 +128,7 @@ import qualified Control.Monad.Catch as Ex import Control.Monad.IO.Class import Control.Monad.Trans.Control +import qualified Data.ByteString as BS import Data.Char (isSpace, toLower) import Data.IORef (IORef,newIORef,readIORef,atomicModifyIORef) @@ -248,7 +250,7 @@ | M.isLoadedParamMod m loaded -> modName ++ "(parameterized)" | M.isLoadedInterface m loaded -> modName ++ "(interface)" | otherwise -> modName - where + where modName = pretty m loaded = M.meLoadedModules (eModuleEnv rw) @@ -646,15 +648,29 @@ return (map (show . pp) (Map.keys (M.namespaceMap M.NSType fNames))) -- | Return a list of property names, sorted by position in the file. -getPropertyNames :: REPL ([(M.Name,M.IfaceDecl)],NameDisp) +-- Only properties defined in the current module are returned, including +-- private properties in the current module. Imported properties are not +-- returned. +getPropertyNames :: REPL ([(M.Name, T.Decl)], NameDisp) getPropertyNames = - do fe <- getFocusedEnv - let xs = M.ifDecls (M.mctxDecls fe) - ps = sortBy (comparing (from . M.nameLoc . fst)) - [ (x,d) | (x,d) <- Map.toList xs, - T.PragmaProperty `elem` M.ifDeclPragmas d ] + do fe <- getFocusedEnv + let nd = M.mctxNameDisp fe + mblm <- fmap (lName =<<) getLoadedMod + case mblm of + Nothing -> pure ([], nd) + Just mn -> + do mb <- M.lookupModule mn <$> getModuleEnv + case mb of + Nothing -> pure ([], nd) + Just lm -> pure (ps, nd) + where + ps = + sortBy (comparing (from . M.nameLoc . fst)) + [ (T.dName d,d) + | d <- T.groupDecls =<< T.mDecls (M.lmdModule (M.lmData lm)) + , T.PragmaProperty `elem` T.dPragmas d + ] - return (ps, M.mctxNameDisp fe) getModNames :: REPL [I.ModName] getModNames = @@ -688,6 +704,20 @@ setRandomGen g' pure result +getModuleInput :: REPL (M.ModuleInput IO) +getModuleInput = do + evo <- getEvalOptsAction + env <- getModuleEnv + callStacks <- getCallStacks + tcSolver <- getTCSolver + pure M.ModuleInput + { minpCallStacks = callStacks + , minpEvalOpts = evo + , minpByteReader = BS.readFile + , minpModuleEnv = env + , minpTCSolver = tcSolver + } + -- | Given an existing qualified name, prefix it with a -- relatively-unique string. We make it unique by prefixing with a -- character @#@ that is not lexically valid in a module name. @@ -957,6 +987,17 @@ \case EnvBool b -> do me <- getModuleEnv setModuleEnv me { M.meMonoBinds = b } _ -> return () + + , OptionDescr "tcSmtFile" ["tc-smt-file"] (EnvString "-") noCheck + (unlines + [ "The file to record SMT solver interactions in the type checker (for debugging or offline proving)." + , "Use \"-\" for stdout." ]) $ + \case EnvString fileName -> do let mfile = if fileName == "-" then Nothing else Just fileName + modifyRW_ (\rw -> rw { eTCConfig = (eTCConfig rw) + { T.solverSmtFile = mfile + }}) + resetTCSolver + _ -> return () , OptionDescr "tcSolver" ["tc-solver"] (EnvProg "z3" [ "-smt2", "-in" ]) noCheck -- TODO: check for the program in the path diff --git a/src/Cryptol/Symbolic.hs b/src/Cryptol/Symbolic.hs --- a/src/Cryptol/Symbolic.hs +++ b/src/Cryptol/Symbolic.hs @@ -56,7 +56,6 @@ import Cryptol.Backend import Cryptol.Backend.FloatHelpers(bfValue) -import Cryptol.Backend.SeqMap (finiteSeqMap) import Cryptol.Backend.WordValue (wordVal) import qualified Cryptol.Eval.Concrete as Concrete @@ -268,9 +267,11 @@ VarBit b -> VBit b VarInteger i -> VInteger i VarRational n d -> VRational (SRational n d) - VarWord w -> VWord (wordLen sym w) (wordVal w) + VarWord w -> VWord (wordVal w) VarFloat f -> VFloat f - VarFinSeq n vs -> VSeq n (finiteSeqMap sym (map (pure . varShapeToValue sym) vs)) + VarFinSeq n vs -> case toFinSeq (map (varShapeToValue sym) vs) of + Just vs' -> finSeq sym n vs' + Nothing -> panic "varShapeToValue" ["Unexpected VarBit in VarFinSeq"] VarTuple vs -> VTuple (map (pure . varShapeToValue sym) vs) VarRecord fs -> VRecord (fmap (pure . varShapeToValue sym) fs) VarEnum tag cons -> diff --git a/src/Cryptol/Symbolic/SBV.hs b/src/Cryptol/Symbolic/SBV.hs --- a/src/Cryptol/Symbolic/SBV.hs +++ b/src/Cryptol/Symbolic/SBV.hs @@ -29,6 +29,7 @@ import Control.Applicative +import Control.Concurrent (threadDelay) import Control.Concurrent.Async import Control.Concurrent.MVar import Control.Monad.IO.Class @@ -42,7 +43,7 @@ import LibBF(bfNaN) -import qualified Data.SBV as SBV (sObserve, symbolicEnv) +import qualified Data.SBV as SBV (sObserve, symbolicEnv, SMTReasonUnknown (..)) import qualified Data.SBV.Internals as SBV (SBV(..)) import qualified Data.SBV.Dynamic as SBV import qualified Data.SBV.Trans.Control as SBV (SMTOption(..)) @@ -88,6 +89,7 @@ , ("cvc5" , SBV.cvc5 ) , ("yices" , SBV.yices ) , ("z3" , SBV.z3 ) + , ("bitwuzla" , SBV.bitwuzla ) , ("boolector", SBV.boolector) , ("mathsat" , SBV.mathSAT ) , ("abc" , SBV.abc ) @@ -98,6 +100,7 @@ , ("sbv-cvc5" , SBV.cvc5 ) , ("sbv-yices" , SBV.yices ) , ("sbv-z3" , SBV.z3 ) + , ("sbv-bitwuzla" , SBV.bitwuzla ) , ("sbv-boolector", SBV.boolector) , ("sbv-mathsat" , SBV.mathSAT ) , ("sbv-abc" , SBV.abc ) @@ -108,11 +111,41 @@ setTimeoutSecs :: Int {- ^ seconds -} -> SBV.SMTConfig -> SBV.SMTConfig -setTimeoutSecs s cfg = cfg - { SBV.solverSetOptions = - SBV.OptionKeyword ":timeout" [show (toInteger s * 1000)] : - filter (not . isTimeout) (SBV.solverSetOptions cfg) } +setTimeoutSecs s cfg = case SBV.name (SBV.solver cfg) of + SBV.Yices -> cfg' + -- TODO: although "--timeout" correctly sets the timeout for Yices, + -- SBV crashes due to an unexpected response from Yices after + -- a timeout is hit. + -- As a workaround, we ignore the timeout setting for Yices + -- and instead rely on 'addDeadmanTimer' to kill Yices when the + -- timeout is hit. + -- see: + -- https://github.com/LeventErkok/sbv/issues/735 + -- https://github.com/SRI-CSL/yices2/issues/547 + {- { SBV.extraArgs = + ["--timeout", show (toInteger s)] ++ + SBV.extraArgs cfg' } -} + + -- NOTE: Once Cryptol requires sbv 11.1.5 as a minimum, we + -- can use the new 'SetTimeOut' option for all solvers and + -- the special cases for CVC4 and CVC5 can be dropped. + SBV.CVC4 -> cfg' + { SBV.extraArgs = + ["--tlimit-per", show (toInteger s * 1000)] ++ + SBV.extraArgs cfg' } + SBV.CVC5 -> cfg' + { SBV.extraArgs = + ["--tlimit-per", show (toInteger s * 1000)] ++ + SBV.extraArgs cfg' } + _ -> cfg' + { SBV.solverSetOptions = + SBV.OptionKeyword ":timeout" [show (toInteger s * 1000)] : + (SBV.solverSetOptions cfg') } where + cfg' = cfg + { SBV.solverSetOptions = + filter (not . isTimeout) (SBV.solverSetOptions cfg) } + isTimeout (SBV.OptionKeyword k _) = k == ":timeout" isTimeout _ = False @@ -248,6 +281,29 @@ do forM_ others (\a -> X.throwTo (asyncThreadId a) ExitSuccess) return r +-- | Wrap a solver call with a given timeout. If the timeout is reached, then +-- the default result is returned and the solver call is terminated. +-- This is required to handle timeouts when using Yices due to a known +-- issue (see 'setTimeoutSecs'). +-- However, it can be used with any solver as an additional measure +-- to ensure the timeout is respected. +addDeadmanTimer :: + Int {- ^ timeout in seconds -} -> + (SBV.SMTConfig -> res) {- ^ result to give when a timeout is hit -} -> + (SBV.SMTConfig -> SBV.Symbolic SBV.SVal -> IO res) {- ^ call the SMT solver -} -> + (SBV.SMTConfig -> SBV.Symbolic SBV.SVal -> IO res) +addDeadmanTimer timeoutSecs _defaultRes callProver | timeoutSecs <= 0 = callProver +addDeadmanTimer timeoutSecs defaultRes callProver = + let deadmanTimeoutPeriodMicroSeconds = + (timeoutSecs * 1000000) + -- sec to usec + 1000 -- buffer to wait for solver-native timeout + deadmanTimer = threadDelay deadmanTimeoutPeriodMicroSeconds + in \cfg v -> + do res <- race deadmanTimer (callProver cfg v) + case res of + Left () -> return $ defaultRes cfg + Right a -> return a + -- | Select the appropriate solver or solvers from the given prover command, -- and invoke those solvers on the given symbolic value. runProver :: @@ -275,9 +331,9 @@ ] in case pcQueryType of - ProveQuery -> runMultiProvers pc lPutStrLn ps' SBV.proveWith thmSMTResults x - SafetyQuery -> runMultiProvers pc lPutStrLn ps' SBV.proveWith thmSMTResults x - SatQuery (SomeSat 1) -> runMultiProvers pc lPutStrLn ps' SBV.satWith satSMTResults x + ProveQuery -> runMultiProvers pc lPutStrLn ps' proveWith thmSMTResults x + SafetyQuery -> runMultiProvers pc lPutStrLn ps' proveWith thmSMTResults x + SatQuery (SomeSat 1) -> runMultiProvers pc lPutStrLn ps' satWith satSMTResults x _ -> return (Nothing, [SBV.ProofError p [":sat with option prover=any requires option satNum=1"] @@ -295,11 +351,17 @@ | otherwise = p1 in case pcQueryType of - ProveQuery -> runSingleProver pc lPutStrLn p2 SBV.proveWith thmSMTResults x - SafetyQuery -> runSingleProver pc lPutStrLn p2 SBV.proveWith thmSMTResults x - SatQuery (SomeSat 1) -> runSingleProver pc lPutStrLn p2 SBV.satWith satSMTResults x - SatQuery _ -> runSingleProver pc lPutStrLn p2 SBV.allSatWith allSatSMTResults x - + ProveQuery -> runSingleProver pc lPutStrLn p2 proveWith thmSMTResults x + SafetyQuery -> runSingleProver pc lPutStrLn p2 proveWith thmSMTResults x + SatQuery (SomeSat 1) -> runSingleProver pc lPutStrLn p2 satWith satSMTResults x + SatQuery _ -> runSingleProver pc lPutStrLn p2 allSatWith allSatSMTResults x + where + proveWith = + addDeadmanTimer timeoutSecs (\cfg -> SBV.ThmResult (SBV.Unknown cfg SBV.UnknownTimeOut)) SBV.proveWith + satWith = + addDeadmanTimer timeoutSecs (\cfg -> SBV.SatResult (SBV.Unknown cfg SBV.UnknownTimeOut)) SBV.satWith + allSatWith = + addDeadmanTimer timeoutSecs (\cfg -> SBV.AllSatResult False True False [(SBV.Unknown cfg SBV.UnknownTimeOut)]) SBV.allSatWith -- | Prepare a symbolic query by symbolically simulating the expression found in -- the @ProverQuery@. The result will either be an error or a list of the types diff --git a/src/Cryptol/Symbolic/What4.hs b/src/Cryptol/Symbolic/What4.hs --- a/src/Cryptol/Symbolic/What4.hs +++ b/src/Cryptol/Symbolic/What4.hs @@ -81,6 +81,7 @@ import qualified What4.SFloat as W4 import qualified What4.SWord as SW import What4.Solver +import qualified What4.Solver.Bitwuzla as W4 import qualified What4.Solver.Boolector as W4 import qualified What4.Solver.CVC4 as W4 import qualified What4.Solver.CVC5 as W4 @@ -144,7 +145,37 @@ W4Error err -> liftIO (X.throwIO err) W4Result p x -> pure (p,x) +-- | Wraps a 'W4.ConfigOption' to provide a consistent interface for setting +-- solver goal timeouts (see 'configTimeoutMilliSeconds', 'configTimeoutSeconds', 'setConfigTimeout'). +data ConfigTimeout = + ConfigTimeout + (W4.ConfigOption W4.BaseIntegerType) + -- | Translate a 'W4.SolverGoalTimeout' into the integer backing this config option. + (W4.SolverGoalTimeout -> Integer) +-- | Construct a 'ConfigTimeout' from a 'W4.ConfigOption', where the given +-- option configures a solver-specific timeout measured in milliseconds. +configTimeoutMilliSeconds :: W4.ConfigOption W4.BaseIntegerType -> ConfigTimeout +configTimeoutMilliSeconds opt = ConfigTimeout opt W4.getGoalTimeoutInMilliSeconds + +-- | Construct a 'ConfigTimeout' from a 'W4.ConfigOption', where the given +-- option configures a solver-specific timeout measured in seconds. +-- Rounds up to at least 1 second when setting a non-zero timeout +-- (see 'W4.getGoalTimeoutInSeconds'). +configTimeoutSeconds :: W4.ConfigOption W4.BaseIntegerType -> ConfigTimeout +configTimeoutSeconds opt = ConfigTimeout opt W4.getGoalTimeoutInSeconds + +setConfigTimeout :: + W4.IsExprBuilder sym => + ConfigTimeout -> + W4.SolverGoalTimeout -> + sym -> + IO () +setConfigTimeout (ConfigTimeout opt toOpt) t sym = + do optSetting <- W4.getOptionSetting opt (W4.getConfiguration sym) + _ <- W4.trySetOpt optSetting (toOpt t) + pure () + data AnAdapter = AnAdapter (forall st. SolverAdapter st) | forall s. W4.OnlineSolver s => @@ -152,6 +183,7 @@ String W4.ProblemFeatures [W4.ConfigDesc] + ConfigTimeout (Proxy s) data W4ProverConfig @@ -159,12 +191,19 @@ | W4OfflineConfig | W4Portfolio (NonEmpty AnAdapter) +adapters :: W4ProverConfig -> [AnAdapter] +adapters cfg = case cfg of + W4ProverConfig adpt -> [adpt] + W4OfflineConfig -> [] + W4Portfolio adpts -> NE.toList adpts + proverConfigs :: [(String, W4ProverConfig)] proverConfigs = [ ("w4-cvc4" , W4ProverConfig cvc4OnlineAdapter) , ("w4-cvc5" , W4ProverConfig cvc5OnlineAdapter) , ("w4-yices" , W4ProverConfig yicesOnlineAdapter) , ("w4-z3" , W4ProverConfig z3OnlineAdapter) + , ("w4-bitwuzla" , W4ProverConfig bitwuzlaOnlineAdapter) , ("w4-boolector" , W4ProverConfig boolectorOnlineAdapter) , ("w4-abc" , W4ProverConfig (AnAdapter W4.externalABCAdapter)) @@ -175,27 +214,32 @@ z3OnlineAdapter :: AnAdapter z3OnlineAdapter = - AnOnlineAdapter "Z3" W4.z3Features W4.z3Options + AnOnlineAdapter "Z3" W4.z3Features W4.z3Options (configTimeoutMilliSeconds W4.z3Timeout) (Proxy :: Proxy (W4.Writer W4.Z3)) yicesOnlineAdapter :: AnAdapter yicesOnlineAdapter = - AnOnlineAdapter "Yices" W4.yicesDefaultFeatures W4.yicesOptions + AnOnlineAdapter "Yices" W4.yicesDefaultFeatures W4.yicesOptions (configTimeoutSeconds W4.yicesGoalTimeout) (Proxy :: Proxy W4.Connection) cvc4OnlineAdapter :: AnAdapter cvc4OnlineAdapter = - AnOnlineAdapter "CVC4" W4.cvc4Features W4.cvc4Options + AnOnlineAdapter "CVC4" W4.cvc4Features W4.cvc4Options (configTimeoutMilliSeconds W4.cvc4Timeout) (Proxy :: Proxy (W4.Writer W4.CVC4)) cvc5OnlineAdapter :: AnAdapter cvc5OnlineAdapter = - AnOnlineAdapter "CVC5" W4.cvc5Features W4.cvc5Options + AnOnlineAdapter "CVC5" W4.cvc5Features W4.cvc5Options (configTimeoutMilliSeconds W4.cvc5Timeout) (Proxy :: Proxy (W4.Writer W4.CVC5)) +bitwuzlaOnlineAdapter :: AnAdapter +bitwuzlaOnlineAdapter = + AnOnlineAdapter "Bitwuzla" W4.bitwuzlaFeatures W4.bitwuzlaOptions (configTimeoutMilliSeconds W4.bitwuzlaTimeout) + (Proxy :: Proxy (W4.Writer W4.Bitwuzla)) + boolectorOnlineAdapter :: AnAdapter boolectorOnlineAdapter = - AnOnlineAdapter "Boolector" W4.boolectorFeatures W4.boolectorOptions + AnOnlineAdapter "Boolector" W4.boolectorFeatures W4.boolectorOptions (configTimeoutMilliSeconds W4.boolectorTimeout) (Proxy :: Proxy (W4.Writer W4.Boolector)) allSolvers :: W4ProverConfig @@ -203,6 +247,7 @@ $ z3OnlineAdapter :| [ cvc4OnlineAdapter , cvc5OnlineAdapter + , bitwuzlaOnlineAdapter , boolectorOnlineAdapter , yicesOnlineAdapter , AnAdapter W4.externalABCAdapter @@ -240,7 +285,7 @@ adapterNames [] = [] adapterNames (AnAdapter adpt : ps) = solver_adapter_name adpt : adapterNames ps - adapterNames (AnOnlineAdapter n _ _ _ : ps) = + adapterNames (AnOnlineAdapter n _ _ _ _ : ps) = n : adapterNames ps filterAdapters [] = pure [] @@ -256,7 +301,7 @@ W4.extendConfig (W4.solver_adapter_config_options adpt) (W4.getConfiguration sym) W4.smokeTest sym adpt - tryAdapter (AnOnlineAdapter _ fs opts (_ :: Proxy s)) = test `X.catch` (pure . Just) + tryAdapter (AnOnlineAdapter _ fs opts _ (_ :: Proxy s)) = test `X.catch` (pure . Just) where test = do sym <- W4.newExprBuilder W4.FloatIEEERepr CryptolState globalNonceGenerator @@ -288,7 +333,7 @@ where setupAnAdapter (AnAdapter adpt) = W4.extendConfig (W4.solver_adapter_config_options adpt) (W4.getConfiguration sym) - setupAnAdapter (AnOnlineAdapter _n _fs opts _p) = + setupAnAdapter (AnOnlineAdapter _n _fs opts _ _p) = W4.extendConfig opts (W4.getConfiguration sym) what4FreshFns :: W4.IsSymExprBuilder sym => sym -> FreshVarFns (What4 sym) @@ -411,7 +456,7 @@ globalNonceGenerator setupAdapterOptions solverCfg w4sym when hashConsing (W4.startCaching w4sym) - when (timeoutMs > 0) (setTimeout (fromIntegral timeoutMs) w4sym) + when (timeoutMs > 0) (setTimeout solverCfg (fromIntegral timeoutMs) w4sym) pure w4sym doLog lg () = @@ -512,7 +557,7 @@ fail ("Solver " ++ solver_adapter_name adpt ++ " does not support incremental solving and " ++ "cannot be used for multi-SAT queries.") -multiSATQuery sym (W4ProverConfig (AnOnlineAdapter nm fs _opts (_ :: Proxy s))) +multiSATQuery sym (W4ProverConfig (AnOnlineAdapter nm fs _opts _ (_ :: Proxy s))) ProverCommand{..} primMap _logData ts args query satNum0 = withMaybeFile pcSmtFile WriteMode $ \smtFileHdl -> X.bracket @@ -692,7 +737,7 @@ return (Just (W4.solver_adapter_name adpt), pres) -singleQuery sym (W4ProverConfig (AnOnlineAdapter nm fs _opts (_ :: Proxy s))) +singleQuery sym (W4ProverConfig (AnOnlineAdapter nm fs _opts _ (_ :: Proxy s))) ProverCommand{..} primMap _logData ts args msafe query = withMaybeFile pcSmtFile WriteMode $ \smtFileHdl -> X.bracket @@ -758,17 +803,22 @@ VarEnum <$> W4.groundEval evalFn tag <*> traverse (traverse (varShapeToConcrete evalFn)) cons -symCfg :: (W4.IsExprBuilder sym, W4.Opt t a) => sym -> W4.ConfigOption t -> a -> IO () -symCfg sym x y = - do opt <- W4.getOptionSetting x (W4.getConfiguration sym) - _ <- W4.trySetOpt opt y - pure () +setAdapterTimeout :: + W4.IsExprBuilder sym => + AnAdapter -> + W4.SolverGoalTimeout -> + sym -> + IO () +setAdapterTimeout (AnAdapter _) _timeout _sym = + pure () -- NOTE: this is only externalABC at the moment, which has no timeout option +setAdapterTimeout (AnOnlineAdapter _ _ _ cfgTimeout _) timeout sym = + setConfigTimeout cfgTimeout timeout sym -setTimeout :: W4.IsExprBuilder sym => Integer -> sym -> IO () -setTimeout s sym = - do symCfg sym W4.z3Timeout (1000 * s) - symCfg sym W4.cvc4Timeout (1000 * s) - symCfg sym W4.cvc5Timeout (1000 * s) - symCfg sym W4.boolectorTimeout (1000 * s) - symCfg sym W4.yicesGoalTimeout s -- N.B. yices takes seconds - pure () +setTimeout :: + W4.IsExprBuilder sym => + W4ProverConfig -> + Integer {- ^ timeout in seconds -} -> + sym -> + IO () +setTimeout cfg s sym = forM_ (adapters cfg) $ \adpt -> + setAdapterTimeout adpt (W4.SolverGoalTimeout (1000 * s)) sym diff --git a/src/Cryptol/Testing/Random.hs b/src/Cryptol/Testing/Random.hs --- a/src/Cryptol/Testing/Random.hs +++ b/src/Cryptol/Testing/Random.hs @@ -47,14 +47,14 @@ import Cryptol.Backend.FloatHelpers (floatFromBits) import Cryptol.Backend.Monad (runEval,Eval,EvalErrorEx(..)) import Cryptol.Backend.Concrete -import Cryptol.Backend.SeqMap (indexSeqMap, finiteSeqMap) +import Cryptol.Backend.SeqMap (indexSeqMap) import Cryptol.Backend.WordValue (wordVal) import Cryptol.Eval(evalEnumCon) import Cryptol.Eval.Type ( TValue(..), TNominalTypeValue(..), ConInfo(..) , isNullaryCon ) -import Cryptol.Eval.Value ( GenValue(..), ppValue, defaultPPOpts, fromVFun) -import Cryptol.TypeCheck.Solver.InfNat (widthInteger) +import Cryptol.Eval.Value ( GenValue(..), ppValue, defaultPPOpts, fromVFun, mkSeq, unsafeToFinSeq, finSeq) +import Cryptol.TypeCheck.Solver.InfNat (widthInteger, Nat' (..)) import Cryptol.Utils.Ident (Ident) import Cryptol.Utils.Panic (panic) import Cryptol.Utils.RecordMap @@ -160,7 +160,7 @@ TVSeq n TVBit -> Just (randomWord sym n) TVSeq n el -> do mk <- randomValue sym el - return (randomSequence n mk) + return (randomSequence sym n el mk) TVStream el -> do mk <- randomValue sym el return (randomStream mk) @@ -237,7 +237,7 @@ randomWord :: (Backend sym, RandomGen g) => sym -> Integer -> Gen g sym randomWord sym w _sz g = let (val, g1) = randomR (0,2^w-1) g - in (VWord w . wordVal <$> wordLit sym w val, g1) + in (VWord . wordVal <$> wordLit sym w val, g1) {-# INLINE randomStream #-} @@ -251,14 +251,14 @@ {- | Generate a random sequence. This should be used for sequences other than bits. For sequences of bits use "randomWord". -} -randomSequence :: (Backend sym, RandomGen g) => Integer -> Gen g sym -> Gen g sym -randomSequence w mkElem sz g0 = do +randomSequence :: (Backend sym, RandomGen g) => sym -> Integer -> TValue -> Gen g sym -> Gen g sym +randomSequence sym w elty mkElem sz g0 = do let (g1,g2) = split g0 let f g = let (x,g') = mkElem sz g in seq x (Just (x, g')) let xs = Seq.fromList $ genericTake w $ unfoldr f g1 - let v = VSeq w $ indexSeqMap $ \i -> Seq.index xs (fromInteger i) - seq xs (pure v, g2) + let v = mkSeq sym (Nat w) elty $ indexSeqMap $ \i -> Seq.index xs (fromInteger i) + seq xs (v, g2) {-# INLINE randomTuple #-} @@ -493,11 +493,11 @@ TVArray{} -> [] TVStream{} -> [] TVSeq n TVBit -> - [ VWord n (wordVal (BV n x)) + [ VWord (wordVal (BV n x)) | x <- [ 0 .. 2^n - 1 ] ] TVSeq n el -> - [ VSeq n (finiteSeqMap Concrete (map pure xs)) + [ finSeq Concrete n (unsafeToFinSeq (map pure xs)) -- safe, since the TVBit case is covered above | xs <- sequence (genericReplicate n (typeValues el)) ] TVTuple ts -> diff --git a/src/Cryptol/TypeCheck.hs b/src/Cryptol/TypeCheck.hs --- a/src/Cryptol/TypeCheck.hs +++ b/src/Cryptol/TypeCheck.hs @@ -85,7 +85,7 @@ res <- inferBinds True False [ P.Bind { P.bName = P.Located { P.srcRange = loc, P.thing = fresh } - , P.bParams = [] + , P.bParams = P.noParams , P.bDef = P.Located (inpRange inp) (P.exprDef expr) , P.bPragmas = [] , P.bSignature = Nothing diff --git a/src/Cryptol/TypeCheck/AST.hs b/src/Cryptol/TypeCheck/AST.hs --- a/src/Cryptol/TypeCheck/AST.hs +++ b/src/Cryptol/TypeCheck/AST.hs @@ -13,7 +13,6 @@ {-# LANGUAGE FlexibleInstances, FlexibleContexts #-} {-# LANGUAGE DeriveAnyClass, DeriveGeneric #-} {-# LANGUAGE OverloadedStrings #-} -{-# LANGUAGE NamedFieldPuns #-} {-# LANGUAGE ViewPatterns #-} module Cryptol.TypeCheck.AST ( module Cryptol.TypeCheck.AST @@ -31,6 +30,7 @@ , DocFor(..) ) where +import Data.Maybe(catMaybes) import Cryptol.Utils.Panic(panic) import Cryptol.Utils.Ident (Ident,isInfixIdent,ModName,PrimIdent,prelPrim) import Cryptol.Parser.Position(Located, HasLoc(..), Range) @@ -57,7 +57,7 @@ import qualified Data.IntMap as IntMap import Data.Map (Map) import qualified Data.Map as Map -import Data.Maybe (mapMaybe, maybeToList) +import Data.Maybe (mapMaybe, maybeToList, isJust) import Data.Set (Set) import Data.Text (Text) @@ -227,6 +227,8 @@ | EWhere Expr [DeclGroup] + {- | Use 'ePropGuards' when constructing to get automatic + simplification of trivial constraints -} | EPropGuards [([Prop], Expr)] Type deriving (Show, Generic, NFData) @@ -289,6 +291,20 @@ where v = fromEnum c w = 8 :: Int +-- | Construct a prop guard expression simplifying trivial cases. +ePropGuards :: [([Prop], Expr)] -> Type -> Expr +ePropGuards guards ty = + case check True guards of + Left body -> body + Right guards' -> EPropGuards guards' ty + where + check _ [] = Right [] + check trivial ((p, e):xs) + | trivial, all (null . pSplitAnd) p = Left e + | otherwise = ((p,e):) <$> check trivial' xs + where + trivial' = trivial && any (isJust . tIsError) p + instance PP TCTopEntity where ppPrec _ te = case te of @@ -509,17 +525,25 @@ instance PP n => PP (WithNames (ModuleG n)) where ppPrec _ (WithNames Module { .. } nm) = - vcat [ text "module" <+> pp mName + vcat $ + catMaybes + [ Just (text "module" <+> pp mName) + , Just "" -- XXX: Print exports? - , vcat (map pp' (Map.elems mTySyns)) + , vcat' (map pp' (Map.elems mTySyns)) -- XXX: Print abstarct types/functions - , vcat (map pp' mDecls) + , vcat' (map pp' mDecls) - , vcat (map pp (Map.elems mFunctors)) + , vcat' (map pp (Map.elems mFunctors)) + + , vcat' (map ppSig (Map.toList mSignatures)) ] where mps = map mtpParam (Map.elems mParamTypes) pp' :: PP (WithNames a) => a -> Doc pp' = ppWithNames (addTNames mps nm) + ppSig (x,y) = "interface module" <+> pp x <+> "where" + $$ indent 2 (pp y) + vcat' xs = if null xs then Nothing else Just (vcat xs) instance PP (WithNames TCTopEntity) where ppPrec _ (WithNames ent nm) = diff --git a/src/Cryptol/TypeCheck/Error.hs b/src/Cryptol/TypeCheck/Error.hs --- a/src/Cryptol/TypeCheck/Error.hs +++ b/src/Cryptol/TypeCheck/Error.hs @@ -25,6 +25,11 @@ import Cryptol.ModuleSystem.Name(Name) import Cryptol.Utils.RecordMap +-- | Clean up error messages by: +--- * only reporting one error (most severe) for any given source location +-- * sorting errors by source location (they are accumulated in +-- reverse order by 'recordError') +-- * dropping any errors that are subsumed by another cleanupErrors :: [(Range,Error)] -> [(Range,Error)] cleanupErrors = dropErrorsFromSameLoc . sortBy (compare `on` (cmpR . fst)) -- order errors @@ -56,6 +61,17 @@ in dropSubsumed (err : filter keep survived) (filter keep rest) [] -> survived +-- | Clean up warning messages by sorting them by source location +-- (they are accumulated in reverse order by 'recordWarning'). +cleanupWarnings :: [(Range,Warning)] -> [(Range,Warning)] +cleanupWarnings = + sortBy (compare `on` (cmpR . fst)) -- order warnings + where + cmpR r = ( source r -- First by file + , from r -- Then starting position + , to r -- Finally end position + ) + -- | Should the first error suppress the next one. subsumes :: (Range,Error) -> (Range,Error) -> Bool subsumes (_,NotForAll _ _ x _) (_,NotForAll _ _ y _) = x == y @@ -65,6 +81,8 @@ case err of KindMismatch {} -> r1 == r2 _ -> True +subsumes (_, TooManyParams nm1 _ _ _) (_, TypeMismatch (DefinitionOf nm2) _ _ _) = + nm1 == nm2 subsumes _ _ = False data Warning = DefaultingKind (P.TParam Name) P.Kind @@ -93,6 +111,12 @@ | RecursiveTypeDecls [Name] -- ^ The type synonym declarations are recursive + | TooManyParams Name Type Int Int + -- ^ Name of bind, bind signature, number of patterns given, + -- expected number of parameters from signature. + -- More patterns provided for a bind than expected, + -- given its signature. + | TypeMismatch TypeSource Path Type Type -- ^ Expected type, inferred type @@ -220,6 +244,7 @@ KindMismatch {} -> 10 TyVarWithParams {} -> 9 + TooManyParams{} -> 9 TypeMismatch {} -> 8 EnumTypeMismatch {} -> 7 SchemaMismatch {} -> 7 @@ -296,6 +321,7 @@ RecursiveTypeDecls {} -> err SchemaMismatch i t1 t2 -> SchemaMismatch i !$ (apSubst su t1) !$ (apSubst su t2) + TooManyParams b t i j -> TooManyParams b !$ (apSubst su t) .$ i .$ j TypeMismatch src pa t1 t2 -> TypeMismatch src pa !$ (apSubst su t1) !$ (apSubst su t2) EnumTypeMismatch t -> EnumTypeMismatch !$ apSubst su t InvalidConPat {} -> err @@ -348,6 +374,7 @@ TooFewTyParams {} -> Set.empty RecursiveTypeDecls {} -> Set.empty SchemaMismatch _ t1 t2 -> fvs (t1,t2) + TooManyParams _ t _ _ -> fvs t TypeMismatch _ _ t1 t2 -> fvs (t1,t2) EnumTypeMismatch t -> fvs t InvalidConPat {} -> Set.empty @@ -470,6 +497,14 @@ addTVarsDescsAfter names err $ nested "Recursive type declarations:" (commaSep $ map nm ts) + + TooManyParams n t i j -> + addTVarsDescsAfter names err $ + nested "Type signature mismatch." $ + vcat $ + [ "Expected number of parameters:" <+> int j + , "Actual number of parameters:" <+> int i + , "When defining" <+> quotes ((pp n <> ":") <+> ppWithNames names t) ] TypeMismatch src pa t1 t2 -> addTVarsDescsAfter names err $ @@ -819,6 +854,7 @@ computeFreeVarNames :: [(Range,Warning)] -> [(Range,Error)] -> NameMap computeFreeVarNames warns errs = mkMap numRoots numVaras `IntMap.union` mkMap otherRoots otherVars + `IntMap.union` mpNames {- XXX: Currently we pick the names based on the unique of the variable: smaller uniques get an earlier name (e.g., 100 might get `a` and 200 `b`) @@ -831,20 +867,16 @@ mkName x v = (tvUnique x, v) mkMap roots vs = IntMap.fromList (zipWith mkName vs (variants roots)) - (numVaras,otherVars) = partition ((== KNum) . kindOf) - $ Set.toList - $ Set.filter isFreeTV - $ fvs (map snd warns, map snd errs) + (uvars,non_uvars) = partition isFreeTV + $ Set.toList + $ fvs (map snd warns, map snd errs) + + mpNames = computeModParamNames [ tp | TVBound tp <- non_uvars ] mempty + + (numVaras,otherVars) = partition ((== KNum) . kindOf) uvars otherRoots = [ "a", "b", "c", "d" ] numRoots = [ "m", "n", "u", "v" ] - useUnicode = True - - suff n - | n < 10 && useUnicode = [toEnum (0x2080 + n)] - | otherwise = show n - - variant n x = if n == 0 then x else x ++ suff n + variants roots = [ nameVariant n r | n <- [ 0 .. ], r <- roots ] - variants roots = [ variant n r | n <- [ 0 .. ], r <- roots ] diff --git a/src/Cryptol/TypeCheck/Infer.hs b/src/Cryptol/TypeCheck/Infer.hs --- a/src/Cryptol/TypeCheck/Infer.hs +++ b/src/Cryptol/TypeCheck/Infer.hs @@ -799,6 +799,25 @@ [] -> return () _ -> newGoals CtExactType ps +-- | Check that the number of named parameters in a binding is compatible with +-- the type signature. This specifically catches the case where there +-- are more named parameters in the binding than the type would imply. +checkBindParams :: P.Bind Name -> TypeWithSource -> InferM () +checkBindParams b (WithSource ty0 _src _) = case P.bParams b of + P.PatternParams nbps -> go (length nbps) 0 ty0 + P.DroppedParams _ i -> go i 0 ty0 + where + -- if the signature implies more parameters than we have available, we'll defer + -- this check, since the function body itself may be a lambda + go bindArity _ _ | bindArity <= 0 = return () + go bindArity tyArity ty = case ty of + TUser _ _ ty' -> go bindArity tyArity ty' + TCon (TC TCFun) [_,y] -> go (bindArity-1) (tyArity+1) y + -- signature may imply any number of additional parameters given a free type + TVar TVFree{} -> return () + _ -> when (bindArity > 0) $ + recordErrorLoc (P.bindHeaderLoc b) + (TooManyParams (thing (P.bName b)) ty0 (bindArity + tyArity) tyArity) checkFun :: P.FunDesc Name -> [P.Pattern Name] -> @@ -807,13 +826,12 @@ checkFun (P.FunDesc fun offset) ps e tGoal = inNewScope do let descs = [ TypeOfArg (ArgDescr fun (Just n)) | n <- [ 1 + offset .. ] ] - (tys,tRes) <- expectFun fun (length ps) tGoal let srcs = zipWith3 WithSource tys descs (map getLoc ps) largs <- sequence (zipWith checkP ps srcs) let ds = Map.fromList [ (thing x, x { thing = t }) | (x,t) <- zip largs tys ] e1 <- withMonoTypes ds - (checkE e (WithSource tRes TypeOfRes (twsRange tGoal))) + (checkE e (WithSource tRes (twsSource tGoal) (twsRange tGoal))) let args = [ (thing x, t) | (x,t) <- zip largs tys ] return (foldr (\(x,t) b -> EAbs x t b) e1 args) @@ -1128,7 +1146,8 @@ P.DExpr e -> do let nm = thing (P.bName b) let tGoal = WithSource t (DefinitionOf nm) (getLoc b) - e1 <- checkFun (P.FunDesc (Just nm) 0) (P.bParams b) e tGoal + checkBindParams b tGoal + e1 <- checkFun (P.FunDesc (Just nm) 0) (P.bindParams b) e tGoal let f = thing (P.bName b) return Decl { dName = f , dSignature = Forall [] [] t @@ -1227,7 +1246,7 @@ , foldr ETAbs (foldr EProofAbs e2 asmps) as ) - P.DPropGuards cases0 -> do + P.DPropGuards cases0 -> inRangeMb (getLoc cases0) $ do asmps1 <- applySubstPreds asmps0 t1 <- applySubst t0 cases1 <- mapM (checkPropGuardCase asmps1) cases0 @@ -1247,7 +1266,7 @@ , t1 , foldr ETAbs (foldr EProofAbs - (EPropGuards cases1 t1) + (ePropGuards cases1 t1) asmps1) as ) @@ -1259,7 +1278,8 @@ (e1,cs0) <- collectGoals $ do let nm = thing (P.bName b) tGoal = WithSource t0 (DefinitionOf nm) (getLoc b) - e1 <- checkFun (P.FunDesc (Just nm) 0) (P.bParams b) e0 tGoal + checkBindParams b tGoal + e1 <- checkFun (P.FunDesc (Just nm) 0) (P.bindParams b) e0 tGoal addGoals validSchema () <- simplifyAllConstraints -- XXX: using `asmps` also? return e1 @@ -1320,17 +1340,42 @@ we need to consider a branch for each disjunct --- one branch gets the assumption @~B1@ and another branch gets the assumption @~B2@. Each branch's implications need to be proven independently. - +- If the solver fails to prove any subgoal, but with an error indicating + the subgoal may be provable (i.e. the attempt was terminated due to some partial + heuristic), then pick the next-longest guard as the RHS and re-start. e.g.: + @ + A /\ ~C1 => B1 /\ B2 + A /\ ~C2 => B1 /\ B2 + A /\ ~C3 => B1 /\ B2 + @ + Note that this is sound because the first step (choosing a guard as the RHS) + is heuristic: we can always choose to rewrite @P \/ Q@ + into either @~P => Q@ or @~Q => P@. -} checkExhaustive :: Located Name -> [TParam] -> [Prop] -> [[Prop]] -> InferM Bool checkExhaustive name as asmps guards = - case sortBy cmpByLonger guards of - [] -> pure False -- XXX: we should check the asmps are unsatisfiable - longest : rest -> doGoals (theAlts rest) (map toGoal longest) - + go (sortBy cmpByLonger guards) 0 where + pluck i xs = case splitAt i xs of + (_, []) -> Nothing + (ys,x:xs') -> Just (x, ys ++ xs') + + -- if starting with the longest guard fails with a 'ProofUnknown' result, + -- then re-try with the next guard in descending order. + -- NB: in the worst case this is quadratic in the number of guard predicates, but + -- in practice we expect this number to be low + go [] _ = pure False -- XXX: we should check the asmps are unsatisfiable + go goals i = case pluck i goals of + Just (goalp, rest) -> + do ok <- doGoals (theAlts rest) (map toGoal goalp) + case ok of + ProofSuccess -> pure True + ProofFail -> pure False + ProofUnknown -> go goals (i+1) + Nothing -> pure False + cmpByLonger props1 props2 = compare (length props2) (length props1) - -- reversed, so that longets is first + -- reversed, so that longest is first theAlts :: [[Prop]] -> [[Prop]] theAlts = map concat . sequence . map chooseNeg @@ -1346,11 +1391,13 @@ -- Try to validate all cases doGoals todo gs = case todo of - [] -> pure True + [] -> pure ProofSuccess alt : more -> do ok <- canProve (asmps ++ alt) gs - if ok then doGoals more gs - else pure False + case ok of + ProofSuccess -> doGoals more gs + ProofFail -> pure ProofFail + ProofUnknown -> pure ProofUnknown toGoal :: Prop -> Goal toGoal prop = @@ -1359,10 +1406,29 @@ , goalRange = srcRange name , goal = prop } + + maybeSolvable :: Error -> Bool + maybeSolvable err = case err of + UnsolvedDelayedCt{} -> True + UnsolvedGoals{} -> True + _ -> False - canProve :: [Prop] -> [Goal] -> InferM Bool + canProve :: [Prop] -> [Goal] -> InferM ProofResult canProve asmps' goals = - tryProveImplication (Just (thing name)) as asmps' goals + do res <- tryProveImplication (Just (thing name)) as asmps' goals + case res of + Left errs | all maybeSolvable errs -> return ProofUnknown + Left{} -> return ProofFail + Right{} -> return ProofSuccess + +data ProofResult = + ProofSuccess + -- ^ Proof attempt was successful. + | ProofFail + -- ^ Proof attempt failed, and goal is most likely not provable. + | ProofUnknown + -- ^ Proof attempt failed due to incomplete heuristics, goal may + -- still be provable. {- | Generate type-checked syntax for the code in a PropGuard. For example, consider the following (pre–type-checked) syntax for a guard: diff --git a/src/Cryptol/TypeCheck/InferTypes.hs b/src/Cryptol/TypeCheck/InferTypes.hs --- a/src/Cryptol/TypeCheck/InferTypes.hs +++ b/src/Cryptol/TypeCheck/InferTypes.hs @@ -21,7 +21,7 @@ import Control.Monad(guard) import Cryptol.Parser.Position -import Cryptol.ModuleSystem.Name (asPrim,nameLoc) +import Cryptol.ModuleSystem.Name (asPrim,nameLoc,nameIdent) import Cryptol.TypeCheck.AST import Cryptol.TypeCheck.PP import Cryptol.TypeCheck.Subst @@ -31,10 +31,13 @@ import Cryptol.Utils.Panic(panic) import Cryptol.Utils.Misc(anyJust) +import Data.List(mapAccumL,partition) +import Data.Maybe(mapMaybe) import Data.Set ( Set ) import qualified Data.Set as Set import Data.Map ( Map ) import qualified Data.Map as Map +import qualified Data.IntMap as IntMap import GHC.Generics (Generic) import Control.DeepSeq @@ -45,6 +48,9 @@ , solverVerbose :: Int -- ^ How verbose to be when type-checking , solverPreludePath :: [FilePath] -- ^ Look for the solver prelude in these locations. + , solverSmtFile :: Maybe FilePath + -- ^ The optional file to record SMT solver interactions in the type + -- checker. If 'Nothing', this will print to @stdout@ instead. } deriving (Show, Generic, NFData) @@ -58,6 +64,7 @@ , solverArgs = [ "-smt2", "-in" ] , solverVerbose = 0 , solverPreludePath = searchPath + , solverSmtFile = Nothing } -- | The types of variables in the environment. @@ -319,14 +326,17 @@ _ -> pp ki addTVarsDescsAfter :: FVS t => NameMap -> t -> Doc -> Doc -addTVarsDescsAfter nm t d +addTVarsDescsAfter nm t = addTVarsDescsAfterFVS nm (fvs t) + +addTVarsDescsAfterFVS :: NameMap -> Set TVar -> Doc -> Doc +addTVarsDescsAfterFVS nm vs d | Set.null vs = d -- TODO? use `hang` here instead to indent things after "where" | otherwise = d $$ text "where" $$ vcat (map desc (Set.toList vs)) where - vs = fvs t desc v = ppWithNames nm v <+> text "is" <+> pp (tvInfo v) + addTVarsDescsBefore :: FVS t => NameMap -> t -> Doc -> Doc addTVarsDescsBefore nm t d = vcat (frontMsg ++ [d] ++ backMsg) where @@ -389,13 +399,16 @@ ppPrec _ (WithNames d names) = sig $$ hang "we need to show that" - 2 (vcat ( vars ++ asmps ++ + + 2 (explain (vcat ( vars ++ asmps ++ [ hang "the following constraints hold:" 2 (vcat $ bullets $ map (ppWithNames ns1) - $ dctGoals d )])) + $ dctGoals d )]))) where + + bullets xs = [ "•" <+> x | x <- xs ] sig = case name of @@ -404,7 +417,7 @@ Nothing -> "when checking the module's parameters," name = dctSource d - vars = case dctForall d of + vars = case otherTPs of [] -> [] xs -> ["for any type" <+> commaSep (map (ppWithNames ns1) xs)] asmps = case dctAsmps d of @@ -412,4 +425,51 @@ xs -> [hang "assuming" 2 (vcat (bullets (map (ppWithNames ns1) xs)))] - ns1 = addTNames (dctForall d) names + tvars = fvs (dctAsmps d, dctGoals d) + used = filter ((`Set.member` tvars) . TVBound) (dctForall d) + isModP tp = + case tpFlav tp of + TPModParam {} -> True + _ -> False + (mpTPs,otherTPs) = partition isModP used + explain = addTVarsDescsAfterFVS ns1 (Set.fromList (map TVBound mpTPs)) + + mps = computeModParamNames mpTPs names + ns1 = addTNames otherTPs mps + + + +-- | Add a suffix to a name to make a different label. +nameVariant :: Int -> String -> String +nameVariant n x = if n == 0 then x else x ++ suff + where + useUnicode = True + + suff + | n < 10 && useUnicode = [toEnum (0x2080 + n)] + | otherwise = show n + + + +-- | Pick names for the type parameters that correspond to module parameters, +-- avoiding strings that already appear in the given name map. +-- Returns an extended name map. +computeModParamNames :: [TParam] -> NameMap -> NameMap +computeModParamNames tps names = IntMap.fromList newNames `IntMap.union` names + where + newNames = snd (mapAccumL pickName used0 (mapMaybe isModP tps)) + + used0 = Set.fromList (IntMap.elems names) + + pickName used (u,i) = + let ns = filter (not . (`Set.member` used)) + $ map (`nameVariant` i) [0..] + name = case ns of + x : _ -> x + [] -> panic "computeModParamNames" ["Out of names!"] + in (Set.insert name used, (u,name)) + + isModP tp = + case tpFlav tp of + TPModParam x -> Just (tpUnique tp, show (pp (nameIdent x))) + _ -> Nothing diff --git a/src/Cryptol/TypeCheck/ModuleBacktickInstance.hs b/src/Cryptol/TypeCheck/ModuleBacktickInstance.hs --- a/src/Cryptol/TypeCheck/ModuleBacktickInstance.hs +++ b/src/Cryptol/TypeCheck/ModuleBacktickInstance.hs @@ -376,7 +376,7 @@ ELocated r e -> ELocated r (rew e) EProofAbs p e -> EProofAbs (rewType p) (rew e) EWhere e ds -> EWhere (rew e) (rew ds) - EPropGuards gs t -> EPropGuards gs' (rewType t) + EPropGuards gs t -> ePropGuards gs' (rewType t) where gs' = [ (rewType <$> p, rew e) | (p,e) <- gs ] where diff --git a/src/Cryptol/TypeCheck/Monad.hs b/src/Cryptol/TypeCheck/Monad.hs --- a/src/Cryptol/TypeCheck/Monad.hs +++ b/src/Cryptol/TypeCheck/Monad.hs @@ -51,7 +51,7 @@ , Path, rootPath) import Cryptol.TypeCheck.InferTypes import Cryptol.TypeCheck.Error( Warning(..),Error(..) - , cleanupErrors, computeFreeVarNames + , cleanupErrors, computeFreeVarNames, cleanupWarnings ) import qualified Cryptol.TypeCheck.SimpleSolver as Simple import qualified Cryptol.TypeCheck.Solver.SMT as SMT @@ -184,10 +184,13 @@ errs -> inferFailed warns [(r,apSubst theSu e) | (r,e) <- errs] where - inferOk ws a b c = pure (InferOK (computeFreeVarNames ws []) ws a b c) + inferOk ws a b c = + let ws1 = cleanupWarnings ws + in pure (InferOK (computeFreeVarNames ws1 []) ws1 a b c) inferFailed ws es = let es1 = cleanupErrors es - in pure (InferFailed (computeFreeVarNames ws es1) ws es1) + ws1 = cleanupWarnings ws + in pure (InferFailed (computeFreeVarNames ws1 es1) ws1 es1) rw = RW { iErrors = [] @@ -420,7 +423,9 @@ -- | Report an error. recordErrorLoc :: Maybe Range -> Error -> InferM () recordErrorLoc rng e = - do r <- case rng of + do r' <- curRange + r <- case rng of + Just r | rangeWithin r' r -> pure r' Just r -> pure r Nothing -> case e of AmbiguousSize d _ -> return (tvarSource d) diff --git a/src/Cryptol/TypeCheck/SimpType.hs b/src/Cryptol/TypeCheck/SimpType.hs --- a/src/Cryptol/TypeCheck/SimpType.hs +++ b/src/Cryptol/TypeCheck/SimpType.hs @@ -59,13 +59,16 @@ | Just (n,x1) <- isSumK x = addK n (tAdd x1 y) | Just (n,y1) <- isSumK y = addK n (tAdd x y1) | Just v <- matchMaybe (do (a,b) <- (|-|) y - guard (x == b) - return a) = v + ((guard (x == b) >> return a) + -- added to handle this case: 2 ^^ (1 + h) - 1 == 2 ^^ h - 1 + 2 ^^ h + <|> (same x a >>= \x2 -> return (tSub x2 b))) + ) = v | Just v <- matchMaybe (do (a,b) <- (|-|) x - guard (b == y) - return a) = v + ((guard (b == y) >> return a) + <|> (same y a >>= \y2 -> return (tSub y2 b))) + ) = v - | Just v <- matchMaybe (factor <|> same <|> swapVars) = v + | Just v <- matchMaybe (factor <|> same x y <|> swapVars) = v | otherwise = tf2 TCAdd x y where @@ -101,8 +104,8 @@ guard (a == a') return (tMul a (tAdd b1 b2)) - same = do guard (x == y) - return (tMul (tNum (2 :: Int)) x) + same x1 y1 = do guard (x1 == y1) + return (tMul (tNum (2 :: Int)) x1) swapVars = do a <- aTVar x b <- aTVar y @@ -113,6 +116,13 @@ tSub x y | Just t <- tOp TCSub (op2 nSub) [x,y] = t | tIsInf y = tError (tf2 TCSub x y) + + | tIsInf x = x + {- This assumes that `y` is finite and not error. The first should + follow from the typing on `tSub`, which asserts that the second argument + is finite and less than the first; the second should have been handled + by the first equation above, see `tOp`. -} + | Just 0 <- yNum = x | Just k <- yNum , TCon (TF TCAdd) [a,b] <- tNoUser x @@ -126,6 +136,23 @@ <|> (guard (b == y) >> return a)) = v + -- x^^(n+h) - x^^h + -- ~> (x^^n * x^^h) - x^^h + -- ~> ((x^^n - 1) * x^^h + -- allows subtraction cancelling to occur when + -- (2^^h + 2^^h) has been rewritten into 2^^(1+h) + | Just v <- matchMaybe $ + do (x_base,x_exp) <- (|^|) x + (y_base,y_exp) <- (|^|) y + guard (x_base == y_base) + x_exp_sum <- anAdd x_exp + matchSwap x_exp_sum $ \(h,n) -> + do guard (h == y_exp) + let x_to_n = tExp x_base n + let lhs = tSub x_to_n (tNum (1 :: Int)) + return $ tMul lhs y + = v + | Just v <- matchMaybe (do (a,b) <- (|-|) y return (tSub (tAdd x b) a)) = v @@ -143,7 +170,7 @@ | Just n <- tIsNum y = mulK n x | Just v <- matchMaybe swapVars = v | otherwise = checkExpMul x y - + where mulK 0 _ = tNum (0 :: Int) mulK 1 t = t @@ -167,7 +194,7 @@ b <- aTVar y guard (b < a) return (tf2 TCMul y x) - + -- Check if (K^a * K^b) => K^(a + b) otherwise default to standard mul checkExpMul s t | TCon (TF TCExp) [a,aExp] <- s , Just a' <- tIsNum a @@ -215,7 +242,9 @@ tExp x y | Just t <- tOp TCExp (total (op2 nExp)) [x,y] = t | Just 0 <- tIsNum y = tNum (1 :: Int) - | TCon (TF TCExp) [a,b] <- tNoUser y = tExp x (tMul a b) + -- If `x = (a ^^ b)`, then `(a ^^ b) ^^ y` simplifies to `a ^^ (b * y)`. + -- This even holds if `a == 0`, given that `0 ^^ 0 == 1` in Cryptol. + | TCon (TF TCExp) [a,b] <- tNoUser x = tExp a (tMul b y) | otherwise = tf2 TCExp x y @@ -310,6 +339,10 @@ , Just 1 <- tIsNum b , TCon (TF TCExp) [p,q] <- tNoUser a , Just 2 <- tIsNum p = q + + -- width (2^n) = n + 1 + | TCon (TF TCExp) [m,n] <- tNoUser x + , Just 2 <- tIsNum m = tf2 TCAdd n (tNum (1 :: Int)) | otherwise = tf1 TCWidth x diff --git a/src/Cryptol/TypeCheck/Solve.hs b/src/Cryptol/TypeCheck/Solve.hs --- a/src/Cryptol/TypeCheck/Solve.hs +++ b/src/Cryptol/TypeCheck/Solve.hs @@ -287,13 +287,12 @@ Left errs -> mapM_ recordError errs return su --- | Tries to prove an implication. If proved, then returns `Right (m_su :: --- InferM Subst)` where `m_su` is an `InferM` computation that results in the --- solution substitution, and records any warning invoked during proving. If not --- proved, then returns `Left (m_err :: InferM ())`, which records all errors --- invoked during proving. +-- | Tries to prove an implication. If proved, then returns +-- a (possibly-empty) list of warnings raised during proving. +-- If not proved, then returns `Left errs`, which records all errors +-- raised during proving. tryProveImplication :: - Maybe Name -> [TParam] -> [Prop] -> [Goal] -> InferM Bool + Maybe Name -> [TParam] -> [Prop] -> [Goal] -> InferM (Either [Error] [Warning]) tryProveImplication lnam as ps gs = do evars <- varsWithAsmps solver <- getSolver @@ -301,11 +300,10 @@ extraAs <- (map mtpParam . Map.elems) <$> getParamTypes extra <- map thing <$> getParamConstraints - (mbErr,_su) <- io (proveImplicationIO solver False lnam evars + (res,_su) <- io (proveImplicationIO solver False lnam evars (extraAs ++ as) (extra ++ ps) gs) - case mbErr of - Left {} -> pure False - Right {} -> pure True + return res + proveImplicationIO :: Solver -> Bool -- ^ Whether to remove duplicate goals in errors diff --git a/src/Cryptol/TypeCheck/Solver/Numeric.hs b/src/Cryptol/TypeCheck/Solver/Numeric.hs --- a/src/Cryptol/TypeCheck/Solver/Numeric.hs +++ b/src/Cryptol/TypeCheck/Solver/Numeric.hs @@ -151,12 +151,21 @@ tryGeqThanSub :: Ctxt -> Type -> Type -> Match Solved -tryGeqThanSub _ x y = +tryGeqThanSub ctxt x y = -- t1 >= t1 - t2 - do (a,_) <- (|-|) y - guard (x == a) - return (SolvedIf []) + (do (a,_) <- (|-|) y + guard (x == a) + return (SolvedIf [])) + <|> do + (x1, x2) <- (|-|) x + (y1, y2) <- (|-|) y + let x1Fin = iIsFin (typeInterval (intervals ctxt) x1) + -- (x - z) >= (y - z) only if x >= y + ((guard (x2 == y2) >> return (SolvedIf [x1 >== y1])) + <|> + -- (z - x) >= (z - y) only if y >= x and fin z + (guard (x1 == y1 && x1Fin) >> return (SolvedIf [y2 >== x2]))) tryGeqThanVar :: Ctxt -> Type -> TVar -> Match Solved tryGeqThanVar _ctxt ty x = diff --git a/src/Cryptol/TypeCheck/Solver/SMT.hs b/src/Cryptol/TypeCheck/Solver/SMT.hs --- a/src/Cryptol/TypeCheck/Solver/SMT.hs +++ b/src/Cryptol/TypeCheck/Solver/SMT.hs @@ -41,12 +41,13 @@ import Data.Map ( Map ) import qualified Data.Map as Map import qualified Data.Set as Set -import Data.Maybe(catMaybes) +import Data.Maybe(catMaybes,isJust) import Data.List(partition) import Control.Exception import Control.Monad(msum,zipWithM,void) import Data.Char(isSpace) import Text.Read(readMaybe) +import System.IO(IOMode(..), hClose, openFile) import qualified System.IO.Strict as StrictIO import System.FilePath(()) import System.Directory(doesFileExist) @@ -80,12 +81,38 @@ -- | Start a fresh solver instance startSolver :: IO () -> SolverConfig -> IO Solver startSolver onExit sCfg = - do logger <- if (solverVerbose sCfg) > 0 then SMT.newLogger 0 - - else return quietLogger - let smtDbg = if (solverVerbose sCfg) > 1 then Just logger else Nothing - solver <- SMT.newSolverNotify - (solverPath sCfg) (solverArgs sCfg) smtDbg (Just (const onExit)) + do let smtFileEnabled = isJust (solverSmtFile sCfg) + (logger, mbLoggerCloseHdl) <- + -- There are two scenarios under which we want to explicitly log SMT + -- solver interactions: + -- + -- 1. The user wants to debug-print interactions with the `tcDebug` + -- option + -- 2. The user wants to write interactions to the `tcSmtFile` option + -- + -- We enable logging if either one is true. + if (solverVerbose sCfg) > 0 || smtFileEnabled + then case solverSmtFile sCfg of + Nothing -> + do logger <- SMT.newLogger 0 + pure (logger, Nothing) + Just file -> + do loggerHdl <- openFile file WriteMode + logger <- SMT.newLoggerWithHandle loggerHdl 0 + pure (logger, Just (hClose loggerHdl)) + else pure (quietLogger, Nothing) + let smtDbg = if (solverVerbose sCfg) > 1 || smtFileEnabled + then Just logger + else Nothing + solver <- SMT.newSolverWithConfig + (SMT.defaultConfig (solverPath sCfg) (solverArgs sCfg)) + { SMT.solverOnExit = + Just $ \_exitCode -> + do onExit + sequence_ mbLoggerCloseHdl + , SMT.solverLogger = + maybe SMT.noSolverLogger SMT.smtSolverLogger smtDbg + } let sol = Solver solver logger setupSolver sol sCfg return sol @@ -150,7 +177,7 @@ debugBlock :: Solver -> String -> IO a -> IO a debugBlock s@Solver { .. } name m = - do debugLog s name + do debugLog s (";;; " ++ name) SMT.logTab logger a <- m SMT.logUntab logger @@ -348,7 +375,8 @@ -- | Assumes no 'And' isNumeric :: Prop -> Bool -isNumeric ty = matchDefault False $ msum [ is (|=|), is (|/=|), is (|>=|), is aFin ] +isNumeric ty = matchDefault False $ msum [ is (|=|), is (|/=|), is (|>=|) + , is aFin, is aPrime ] where is f = f ty >> return True @@ -368,6 +396,7 @@ , aNat ~> "cryNat" , aFin ~> "cryFin" + , aPrime ~> "cryPrime" , (|=|) ~> "cryEq" , (|/=|) ~> "cryNeq" , (|>=|) ~> "cryGeq" diff --git a/src/Cryptol/TypeCheck/Subst.hs b/src/Cryptol/TypeCheck/Subst.hs --- a/src/Cryptol/TypeCheck/Subst.hs +++ b/src/Cryptol/TypeCheck/Subst.hs @@ -448,7 +448,7 @@ EWhere e ds -> EWhere !$ (go e) !$ (apSubst su ds) - EPropGuards guards ty -> EPropGuards + EPropGuards guards ty -> ePropGuards !$ (\(props, e) -> (apSubst su `fmap'` props, go e)) `fmap'` guards !$ apSubst su ty 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 @@ -1353,12 +1353,12 @@ let tps = Map.elems (mpnTypes ps) in vcat $ map pp tps ++ - if null (mpnConstraints ps) then [] else [ "type constraint" <+> parens (commaSep (map (pp . thing) (mpnConstraints ps))) + | not (null (mpnConstraints ps)) ] ++ [ pp t | t <- Map.elems (mpnTySyn ps) ] ++ - map pp (Map.elems (mpnFuns ps)) + map pp (Map.elems (mpnFuns ps)) instance PP ModTParam where ppPrec _ p = diff --git a/src/Cryptol/TypeCheck/TypePat.hs b/src/Cryptol/TypeCheck/TypePat.hs --- a/src/Cryptol/TypeCheck/TypePat.hs +++ b/src/Cryptol/TypeCheck/TypePat.hs @@ -24,7 +24,7 @@ , aRec , (|->|) - , aFin, (|=|), (|/=|), (|>=|) + , aFin, aPrime, (|=|), (|/=|), (|>=|) , aAnd , aTrue @@ -164,6 +164,9 @@ aFin :: Pat Prop Type aFin = tp PFin ar1 + +aPrime :: Pat Prop Type +aPrime = tp PPrime ar1 (|=|) :: Pat Prop (Type,Type) (|=|) = tp PEqual ar2 diff --git a/src/Cryptol/Utils/Ident.hs b/src/Cryptol/Utils/Ident.hs --- a/src/Cryptol/Utils/Ident.hs +++ b/src/Cryptol/Utils/Ident.hs @@ -23,6 +23,7 @@ , ModName , modNameToText , textToModName + , mainModName , modNameChunks , modNameChunksText , packModName @@ -40,6 +41,7 @@ , modNameArg , modNameIfaceMod , modNameToNormalModName + , modNamesMatch , modNameIsNormal -- * Identifiers @@ -51,12 +53,12 @@ , mkInfix , isInfixIdent , isUpperIdent + , isAnonIfaceModIdnet , nullIdent , identText - , modParamIdent , identAnonArg , identAnonIfaceMod - , identAnontInstImport + , identAnonInstImport , identIsNormal -- * Namespaces @@ -161,18 +163,22 @@ -------------------------------------------------------------------------------- -- | Top-level Module names are just text. data ModName = ModName Text MaybeAnon + | ModMain FilePath deriving (Eq,Ord,Show,Generic) instance NFData ModName -- | Change a normal module name to a module name to be used for an --- anonnymous argument. -modNameArg :: ModName -> ModName -modNameArg (ModName m fl) = +-- anonnymous argument. The first two ints are the line and column of the +-- name, which are used for name disambiguation. +modNameArg :: Int -> Int -> ModName -> ModName +modNameArg l c (ModName m fl) = case fl of - NormalName -> ModName m AnonModArgName - _ -> panic "modNameArg" ["Name is not normal"] - + NormalName -> ModName m (AnonModArgName l c) + AnonModArgName {} -> panic "modNameArg" ["Name is not normal"] + AnonIfaceModName -> panic "modNameArg" ["Name is not normal", "AnonModArgName" ] + AnonInstImport {} -> panic "modNameArg" ["Name is not normal", "AnonIfaceModName" ] +modNameArg _ _ (ModMain _) = panic "modNameArg" ["Name is not normal", "AnonInstImport"] -- | Change a normal module name to a module name to be used for an -- anonnymous interface. @@ -180,25 +186,42 @@ modNameIfaceMod (ModName m fl) = case fl of NormalName -> ModName m AnonIfaceModName - _ -> panic "modNameIfaceMod" ["Name is not normal"] + AnonModArgName {} -> panic "modNameIfaceMod" ["Name is not normal", "AnonModArgName"] + AnonIfaceModName -> panic "modNameIfaceMod" ["Name is not normal", "AnonIfaceModName" ] + AnonInstImport {} -> panic "modNameIfaceMod" ["Name is not normal", "AnonInstImport" ] +modNameIfaceMod (ModMain _) = panic "modNameIfaceMod" ["Name is not normal"] --- | This is used when we check that the name of a module matches the --- file where it is defined. modNameToNormalModName :: ModName -> ModName modNameToNormalModName (ModName t _) = ModName t NormalName +modNameToNormalModName (ModMain p) = ModMain p +-- | This is used when we check that the name of a module matches the +-- file where it is defined. +modNamesMatch :: ModName -> ModName -> Bool +modNamesMatch (ModName a _) (ModName b _) = a == b +modNamesMatch (ModMain a) (ModMain b) = a == b +modNamesMatch _ _ = False + modNameToText :: ModName -> Text modNameToText (ModName x fl) = maybeAnonText fl x +modNameToText (ModMain _) = "Main" -- | This is useful when we want to hide anonymous modules. modNameIsNormal :: ModName -> Bool modNameIsNormal (ModName _ fl) = isNormal fl +modNameIsNormal (ModMain _) = False --- | Make a normal module name out of text. +-- | Make a normal module name out of text. This function should not +-- be used to build a @Main@ module name. See 'mainModName'. textToModName :: T.Text -> ModName textToModName txt = ModName txt NormalName +mainModName :: FilePath -> ModName +mainModName = ModMain + -- | Break up a module name on the separators, `Text` version. +-- For the main module this will forget the filename that +-- corresponds to this module and will only report @["Main"]@ modNameChunksText :: ModName -> [T.Text] modNameChunksText (ModName x fl) = unfoldr step x where @@ -209,6 +232,7 @@ (a,b) | T.null b -> Just (maybeAnonText fl str, b) | otherwise -> Just (a,T.drop (T.length modSep) b) +modNameChunksText (ModMain _) = ["Main"] -- | Break up a module name on the separators, `String` version modNameChunks :: ModName -> [String] @@ -331,20 +355,25 @@ NormalName | Just (c,_) <- T.uncons t -> isUpper c _ -> False +-- | Is this an ident for an anonymous module interface +-- (i.e., a `parameter` block)? +isAnonIfaceModIdnet :: Ident -> Bool +isAnonIfaceModIdnet (Ident _ ty _) = + case ty of + AnonIfaceModName -> True + _ -> False + nullIdent :: Ident -> Bool nullIdent = T.null . identText identText :: Ident -> T.Text identText (Ident _ mb t) = maybeAnonText mb t -modParamIdent :: Ident -> Ident -modParamIdent (Ident x a t) = - Ident x a (T.append (T.pack "module parameter ") t) - -- | Make an anonymous identifier for the module corresponding to --- a `where` block in a functor instantiation. -identAnonArg :: Ident -> Ident -identAnonArg (Ident b _ txt) = Ident b AnonModArgName txt +-- a `where` block in a functor instantiation. +-- The two ints are the line and column of the definition site. +identAnonArg :: Int -> Int -> Ident +identAnonArg l c = Ident False (AnonModArgName l c) "" -- | Make an anonymous identifier for the interface corresponding to -- a `parameter` declaration. @@ -352,8 +381,9 @@ identAnonIfaceMod (Ident b _ txt) = Ident b AnonIfaceModName txt -- | Make an anonymous identifier for an instantiation in an import. -identAnontInstImport :: Ident -> Ident -identAnontInstImport (Ident b _ txt) = Ident b AnonInstImport txt +-- The two ints are the line and column of the definition site. +identAnonInstImport :: Int -> Int -> Ident +identAnonInstImport l c = Ident False (AnonInstImport l c) "" identIsNormal :: Ident -> Bool identIsNormal (Ident _ mb _) = isNormal mb @@ -362,21 +392,29 @@ -- | Information about anonymous names. data MaybeAnon = NormalName -- ^ Not an anonymous name. - | AnonModArgName -- ^ Anonymous module (from `where`) + | AnonModArgName Int Int-- ^ Anonymous module (line,column) (from `where`) | AnonIfaceModName -- ^ Anonymous interface (from `parameter`) - | AnonInstImport -- ^ Anonymous instance import + | AnonInstImport Int Int + -- ^ Anonymous instance import (line, column) deriving (Eq,Ord,Show,Generic) instance NFData MaybeAnon --- | Modify a name, if it is a nonymous +-- | Modify a name, if it is a nonymous. +-- If we change this, please update the reference manual as well, so that +-- folks know how to refer to these in external tools. maybeAnonText :: MaybeAnon -> Text -> Text maybeAnonText mb txt = case mb of - NormalName -> txt - AnonModArgName -> "`where` argument of " <> txt - AnonIfaceModName -> "`parameter` interface of " <> txt - AnonInstImport -> txt + NormalName -> txt + AnonModArgName l c + | T.null txt -> "where_at__" <> suff l c + | otherwise -> txt <> "__where" + AnonIfaceModName -> txt <> "__parameter" + AnonInstImport l c -> "import_at__" <> suff l c + where + suff l c = T.pack (if c == 1 then show l else show l ++ "_" ++ show c) + isNormal :: MaybeAnon -> Bool isNormal mb = diff --git a/src/Cryptol/Utils/PP.hs b/src/Cryptol/Utils/PP.hs --- a/src/Cryptol/Utils/PP.hs +++ b/src/Cryptol/Utils/PP.hs @@ -174,7 +174,11 @@ fromString = text renderOneLine :: Doc -> String -renderOneLine d = PP.renderString (PP.layoutCompact (runDocWith defaultPPCfg d)) +renderOneLine d = PP.renderString (PP.layoutPretty opts (runDocWith defaultPPCfg d)) + where + opts = PP.LayoutOptions + { PP.layoutPageWidth = PP.Unbounded + } class PP a where ppPrec :: Int -> a -> Doc @@ -411,8 +415,8 @@ Qualified m -> ppQual (TopModule m) (pp (ogName og)) NotInScope -> ppQual (ogModule og) case ogFromParam og of - Just x -> pp x <.> "::" <.> pp (ogName og) - Nothing -> pp (ogName og) + Just x | not (isAnonIfaceModIdnet x) -> pp x <.> "::" <.> pp (ogName og) + _ -> pp (ogName og) where ppQual mo x = case mo of diff --git a/src/Cryptol/Utils/Patterns.hs b/src/Cryptol/Utils/Patterns.hs --- a/src/Cryptol/Utils/Patterns.hs +++ b/src/Cryptol/Utils/Patterns.hs @@ -86,6 +86,10 @@ matchMaybe :: Match a -> Maybe a matchMaybe (Match m) = m Nothing Just +-- | Attempt matching the given pattern against a tuple, +-- making a second attempt with the values swapped if the first fails. +matchSwap :: (a, a) -> Pat (a, a) b -> Match b +matchSwap (x, y) n = n (x, y) <|> n (y, x) list :: [Pat a b] -> Pat [a] [b] list [] = \a ->