GaloisInc/cryptol
1
1
Fork 0
mirror of https://github.com/GaloisInc/cryptol.git synced 2024-09-11 14:06:13 +03:00
Code Issues Projects Releases Wiki Activity

Rename the runtime-settable options to use a consistent style.

Browse Source 
Options are now all named in camelCase style.  However, multiword
options may still be set using the old hypenated names as aliases,
so interaction scripts and the test suite do not have to be
changed. In addition, option lookup is altered to be case insensitive.

Thus, the canonical option name for the output SMT file when
an offline prover is selected is `smtFile`, which is what will
show up when running `:set` with no arguments, and what will be
suggested for tab-completion.  However, the option may be set
using the strings `smtfile` `SMTFile`, `smt-file`, `SMT-file`, etc.

Fixes #656
This commit is contained in:
Rob Dockins 2021-02-11 14:47:32 -08:00
parent bcc7612b76
commit 3e0cf3e167
5 changed files with 56 additions and 48 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -545,7 +545,7 @@ ppReport tys _ (TestReport exprDoc failure _testNum _testPossible) =
ppFailure :: [E.TValue] -> Doc -> TestResult -> REPL ()
ppFailure tys exprDoc failure = do
~(EnvBool showEx) <- getUser "show-examples"
~(EnvBool showEx) <- getUser "showExamples"
vs <- case failure of
FailFalse vs ->
@ -641,7 +641,7 @@ rethrowErrorCall m = REPL (\r -> unREPL m r `X.catches` hs)
safeCmd :: String -> (Int,Int) -> Maybe FilePath -> REPL ()
safeCmd str pos fnm = do
proverName <- getKnownUser "prover"
fileName <- getKnownUser "smtfile"
fileName <- getKnownUser "smtFile"
let mfile = if fileName == "-" then Nothing else Just fileName
pexpr <- replParseExpr str pos fnm
nd <- M.mctxNameDisp <$> getFocusedEnv
@ -669,7 +669,7 @@ safeCmd str pos fnm = do
(t,e) <- mkSolverResult "counterexample" rng False (Right tes)
~(EnvBool yes) <- getUser "show-examples"
~(EnvBool yes) <- getUser "showExamples"
when yes $ printCounterexample cexType exprDoc vs
when yes $ printSafetyViolation texpr schema vs
@ -723,7 +723,7 @@ proveSatExpr isSat rng exprDoc texpr schema = do
| otherwise = "counterexample"
qtype <- if isSat then SatQuery <$> getUserSatNum else pure ProveQuery
proverName <- getKnownUser "prover"
fileName <- getKnownUser "smtfile"
fileName <- getKnownUser "smtFile"
let mfile = if fileName == "-" then Nothing else Just fileName
if proverName `elem` ["offline","sbv-offline","w4-offline"] then
@ -748,7 +748,7 @@ proveSatExpr isSat rng exprDoc texpr schema = do
(t,e) <- mkSolverResult cexStr rng isSat (Right tes)
~(EnvBool yes) <- getUser "show-examples"
~(EnvBool yes) <- getUser "showExamples"
when yes $ printCounterexample cexType exprDoc vs
-- if there's a safety violation, evalute the counterexample to
@ -778,7 +778,7 @@ proveSatExpr isSat rng exprDoc texpr schema = do
[(t, e)] -> (t, [e])
_ -> collectTes resultRecs
~(EnvBool yes) <- getUser "show-examples"
~(EnvBool yes) <- getUser "showExamples"
when yes $ forM_ vss (printSatisfyingModel exprDoc)
case exprs of
@ -812,7 +812,7 @@ onlineProveSat proverName qtype expr schema mfile = do
validEvalContext schema
decls <- fmap M.deDecls getDynEnv
timing <- io (newIORef 0)
~(EnvBool ignoreSafety) <- getUser "ignore-safety"
~(EnvBool ignoreSafety) <- getUser "ignoreSafety"
let cmd = ProverCommand {
pcQueryType = qtype
, pcProverName = proverName
@ -828,7 +828,7 @@ onlineProveSat proverName qtype expr schema mfile = do
(firstProver, res) <- getProverConfig >>= \case
Left sbvCfg -> liftModuleCmd $ SBV.satProve sbvCfg cmd
Right w4Cfg ->
do ~(EnvBool hashConsing) <- getUser "hash-consing"
do ~(EnvBool hashConsing) <- getUser "hashConsing"
~(EnvBool warnUninterp) <- getUser "warnUninterp"
liftModuleCmd $ W4.satProve w4Cfg hashConsing warnUninterp cmd
@ -842,7 +842,7 @@ offlineProveSat proverName qtype expr schema mfile = do
decls <- fmap M.deDecls getDynEnv
timing <- io (newIORef 0)
~(EnvBool ignoreSafety) <- getUser "ignore-safety"
~(EnvBool ignoreSafety) <- getUser "ignoreSafety"
let cmd = ProverCommand {
pcQueryType = qtype
, pcProverName = proverName
@ -882,7 +882,7 @@ offlineProveSat proverName qtype expr schema mfile = do
Nothing -> rPutStr smtlib
Right w4Cfg ->
do ~(EnvBool hashConsing) <- getUser "hash-consing"
do ~(EnvBool hashConsing) <- getUser "hashConsing"
~(EnvBool warnUninterp) <- getUser "warnUninterp"
result <- liftModuleCmd $ W4.satProveOffline w4Cfg hashConsing warnUninterp cmd $ \f ->
do displayMsg

65
src/Cryptol/REPL/Monad.hs
View File

@ -60,6 +60,7 @@ module Cryptol.REPL.Monad (
, OptionDescr(..)
, setUser, getUser, getKnownUser, tryGetUser
, userOptions
, userOptionsWithAliases
, getUserSatNum
, getUserShowProverStats
, getUserProverValidate
@ -399,8 +400,8 @@ getPPValOpts =
ascii <- getKnownUser "ascii"
infLength <- getKnownUser "infLength"
fpBase <- getKnownUser "fp-base"
fpFmtTxt <- getKnownUser "fp-format"
fpBase <- getKnownUser "fpBase"
fpFmtTxt <- getKnownUser "fpFormat"
let fpFmt = case parsePPFloatFormat fpFmtTxt of
Just f -> f
Nothing -> panic "getPPOpts"
@ -637,7 +638,7 @@ mkUserEnv opts = Map.fromList $ do
-- | Set a user option.
setUser :: String -> String -> REPL ()
setUser name val = case lookupTrieExact name userOptions of
setUser name val = case lookupTrieExact name userOptionsWithAliases of
[opt] -> setUserOpt opt
[] -> rPutStrLn ("Unknown env value `" ++ name ++ "`")
@ -740,10 +741,10 @@ badIsEnv x = panic "fromEnvVal" [ "[REPL] Expected a `" ++ x ++ "` value." ]
getUserShowProverStats :: REPL Bool
getUserShowProverStats = getKnownUser "prover-stats"
getUserShowProverStats = getKnownUser "proverStats"
getUserProverValidate :: REPL Bool
getUserProverValidate = getKnownUser "prover-validate"
getUserProverValidate = getKnownUser "proverValidate"
-- Environment Options ---------------------------------------------------------
@ -765,47 +766,53 @@ noWarns mb = return (mb, [])
data OptionDescr = OptionDescr
{ optName :: String
, optAliases :: [String]
, optDefault :: EnvVal
, optCheck :: Checker
, optHelp :: String
, optEff :: EnvVal -> REPL ()
}
simpleOpt :: String -> EnvVal -> Checker -> String -> OptionDescr
simpleOpt optName optDefault optCheck optHelp =
simpleOpt :: String -> [String] -> EnvVal -> Checker -> String -> OptionDescr
simpleOpt optName optAliases optDefault optCheck optHelp =
OptionDescr { optEff = \ _ -> return (), .. }
userOptionsWithAliases :: OptionMap
userOptionsWithAliases = foldl insert userOptions (leaves userOptions)
where
insert m d = foldl (\m' n -> insertTrie n d m') m (optAliases d)
userOptions :: OptionMap
userOptions = mkOptionMap
[ simpleOpt "base" (EnvNum 16) checkBase
[ simpleOpt "base" [] (EnvNum 16) checkBase
"The base to display words at (2, 8, 10, or 16)."
, simpleOpt "debug" (EnvBool False) noCheck
, simpleOpt "debug" [] (EnvBool False) noCheck
"Enable debugging output."
, simpleOpt "ascii" (EnvBool False) noCheck
, simpleOpt "ascii" [] (EnvBool False) noCheck
"Whether to display 7- or 8-bit words using ASCII notation."
, simpleOpt "infLength" (EnvNum 5) checkInfLength
, simpleOpt "infLength" ["inf-length"] (EnvNum 5) checkInfLength
"The number of elements to display for infinite sequences."
, simpleOpt "tests" (EnvNum 100) noCheck
, simpleOpt "tests" [] (EnvNum 100) noCheck
"The number of random tests to try with ':check'."
, simpleOpt "satNum" (EnvString "1") checkSatNum
, simpleOpt "satNum" ["sat-num"] (EnvString "1") checkSatNum
"The maximum number of :sat solutions to display (\"all\" for no limit)."
, simpleOpt "prover" (EnvString "z3") checkProver $
, simpleOpt "prover" [] (EnvString "z3") checkProver $
"The external SMT solver for ':prove' and ':sat'\n(" ++ proverListString ++ ")."
, simpleOpt "warnDefaulting" (EnvBool False) noCheck
, simpleOpt "warnDefaulting" ["warn-defaulting"] (EnvBool False) noCheck
"Choose whether to display warnings when defaulting."
, simpleOpt "warnShadowing" (EnvBool True) noCheck
, simpleOpt "warnShadowing" ["warn-shadowing"] (EnvBool True) noCheck
"Choose whether to display warnings when shadowing symbols."
, simpleOpt "warnUninterp" (EnvBool True) noCheck
, simpleOpt "warnUninterp" ["warn-uninterp"] (EnvBool True) noCheck
"Choose whether to issue a warning when uninterpreted functions are used to implement primitives in the symbolic simulator."
, simpleOpt "smtfile" (EnvString "-") noCheck
, simpleOpt "smtFile" ["smt-file"] (EnvString "-") noCheck
"The file to use for SMT-Lib scripts (for debugging or offline proving).\nUse \"-\" for stdout."
, OptionDescr "mono-binds" (EnvBool True) noCheck
, OptionDescr "monoBinds" ["mono-binds"] (EnvBool True) noCheck
"Whether or not to generalize bindings in a 'where' clause." $
\case EnvBool b -> do me <- getModuleEnv
setModuleEnv me { M.meMonoBinds = b }
_ -> return ()
, OptionDescr "tc-solver" (EnvProg "z3" [ "-smt2", "-in" ])
, OptionDescr "tcSolver" ["tc-solver"] (EnvProg "z3" [ "-smt2", "-in" ])
noCheck -- TODO: check for the program in the path
"The solver that will be used by the type checker." $
\case EnvProg prog args -> do me <- getModuleEnv
@ -815,7 +822,7 @@ userOptions = mkOptionMap
, T.solverArgs = args } }
_ -> return ()
, OptionDescr "tc-debug" (EnvNum 0)
, OptionDescr "tcDebug" ["tc-debug"] (EnvNum 0)
noCheck
(unlines
[ "Enable type-checker debugging output:"
@ -826,7 +833,7 @@ userOptions = mkOptionMap
let cfg = M.meSolverConfig me
setModuleEnv me { M.meSolverConfig = cfg{ T.solverVerbose = n } }
_ -> return ()
, OptionDescr "core-lint" (EnvBool False)
, OptionDescr "coreLint" ["core-lint"] (EnvBool False)
noCheck
"Enable sanity checking of type-checker." $
let setIt x = do me <- getModuleEnv
@ -835,22 +842,22 @@ userOptions = mkOptionMap
EnvBool False -> setIt M.NoCoreLint
_ -> return ()
, simpleOpt "hash-consing" (EnvBool True) noCheck
, simpleOpt "hashConsing" ["hash-consing"] (EnvBool True) noCheck
"Enable hash-consing in the What4 symbolic backends."
, simpleOpt "prover-stats" (EnvBool True) noCheck
, simpleOpt "proverStats" ["prover-stats"] (EnvBool True) noCheck
"Enable prover timing statistics."
, simpleOpt "prover-validate" (EnvBool False) noCheck
, simpleOpt "proverValidate" ["prover-validate"] (EnvBool False) noCheck
"Validate :sat examples and :prove counter-examples for correctness."
, simpleOpt "show-examples" (EnvBool True) noCheck
, simpleOpt "showExamples" ["show-examples"] (EnvBool True) noCheck
"Print the (counter) example after :sat or :prove"
, simpleOpt "fp-base" (EnvNum 16) checkBase
, simpleOpt "fpBase" ["fp-base"] (EnvNum 16) checkBase
"The base to display floating point numbers at (2, 8, 10, or 16)."
, simpleOpt "fp-format" (EnvString "free") checkPPFloatFormat
, simpleOpt "fpFormat" ["fp-format"] (EnvString "free") checkPPFloatFormat
$ unlines
[ "Specifies the format to use when showing floating point numbers:"
, " * free show using as many digits as needed"
@ -860,7 +867,7 @@ userOptions = mkOptionMap
, " * NUM+exp like NUM but always show exponent"
]
, simpleOpt "ignore-safety" (EnvBool False) noCheck
, simpleOpt "ignoreSafety" ["ignore-safety"] (EnvBool False) noCheck
"Ignore safety predicates when performing :sat or :prove checks"
]

11
src/Cryptol/REPL/Trie.hs
View File

@ -9,6 +9,7 @@
module Cryptol.REPL.Trie where
import Cryptol.Utils.Panic (panic)
import Data.Char (toLower)
import qualified Data.Map as Map
import Data.Maybe (fromMaybe,maybeToList)
@ -20,13 +21,13 @@ data Trie a = Node (Map.Map Char (Trie a)) (Maybe a)
emptyTrie :: Trie a
emptyTrie = Node Map.empty Nothing
-- | Insert a value into the Trie. Will call `panic` if a value already exists
-- with that key.
-- | Insert a value into the Trie, forcing the key value to lower case.
-- Will call `panic` if a value already exists with that key.
insertTrie :: String -> a -> Trie a -> Trie a
insertTrie k a = loop k
where
loop key (Node m mb) = case key of
c:cs -> Node (Map.alter (Just . loop cs . fromMaybe emptyTrie) c m) mb
c:cs -> Node (Map.alter (Just . loop cs . fromMaybe emptyTrie) (toLower c) m) mb
[] -> case mb of
Nothing -> Node m (Just a)
Just _ -> panic "[REPL] Trie" ["key already exists:", "\t" ++ k]
@ -35,7 +36,7 @@ insertTrie k a = loop k
lookupTrie :: String -> Trie a -> [a]
lookupTrie key t@(Node mp _) = case key of
c:cs -> case Map.lookup c mp of
c:cs -> case Map.lookup (toLower c) mp of
Just m' -> lookupTrie cs m'
Nothing -> []
@ -47,7 +48,7 @@ lookupTrieExact :: String -> Trie a -> [a]
lookupTrieExact [] (Node _ (Just x)) = return x
lookupTrieExact [] t = leaves t
lookupTrieExact (c:cs) (Node mp _) =
case Map.lookup c mp of
case Map.lookup (toLower c) mp of
Just m' -> lookupTrieExact cs m'
Nothing -> []

4
tests/regression/float.icry
View File

@ -2,8 +2,8 @@
:set ascii=on
section "Float Formatting"
:help :set fp-base
:help :set fp-format
:help :set fpBase
:help :set fpFormat
:set fp-base=2
10.25 : Medium

4
tests/regression/float.icry.stdout
View File

@ -4,14 +4,14 @@ Loading module Float
Loading module FloatTests
"-- Float Formatting-----------------------------------------------------------"
fp-base = 16
fpBase = 16
Default value: 16
The base to display floating point numbers at (2, 8, 10, or 16).
fp-format = free
fpFormat = free
Default value: free