mirror of
https://github.com/GaloisInc/cryptol.git
synced 2024-09-11 14:06:13 +03:00
merge in the 2.2.6 changes, including z3 switch
This commit is contained in:
commit
9c07fe1006
26
README.md
26
README.md
@ -37,17 +37,17 @@ On Mac OS X, Cryptol is also available via
|
||||
[Homebrew](http://brew.sh/). Simply run `brew update && brew install
|
||||
cryptol` to get the latest stable version.
|
||||
|
||||
## Getting CVC4
|
||||
## Getting Z3
|
||||
|
||||
Cryptol currently depends on the
|
||||
[CVC4 SMT solver](http://cvc4.cs.nyu.edu/) to solve constraints during
|
||||
type checking, and as the default solver for the `:sat` and `:prove`
|
||||
commands. You can download CVC4 binaries for a variety of platforms
|
||||
from their [download page](http://cvc4.cs.nyu.edu/downloads/). Note
|
||||
that if you install Cryptol using Homebrew, CVC4 will be installed
|
||||
automatically.
|
||||
Cryptol currently uses Microsoft Research's
|
||||
[Z3 SMT solver](https://github.com/Z3Prover/z3) by default to solve
|
||||
constraints during type checking, and as the default solver for the
|
||||
`:sat` and `:prove` commands. You can download Z3 binaries for a
|
||||
variety of platforms from their
|
||||
[releases page](https://github.com/Z3Prover/z3/releases). Note that if you
|
||||
install Cryptol using Homebrew, Z3 will be installed automatically.
|
||||
|
||||
After installation, make sure that `cvc4` (or `cvc4.exe` on Windows)
|
||||
After installation, make sure that `z3` (or `z3.exe` on Windows)
|
||||
is on your PATH.
|
||||
|
||||
# Building Cryptol From Source
|
||||
@ -64,9 +64,9 @@ Windows. We regularly build and test it in the following environments:
|
||||
|
||||
## Prerequisites
|
||||
|
||||
Cryptol is developed using GHC 7.8.4 and cabal-install 1.22. The
|
||||
easiest way to get the correct versions is to follow the instructions
|
||||
on the
|
||||
Cryptol is developed using GHC 7.10.2 and cabal-install 1.22, though
|
||||
it is still tested with the previous major version of GHC. The easiest
|
||||
way to get the correct versions is to follow the instructions on the
|
||||
[haskell.org downloads page](https://www.haskell.org/downloads).
|
||||
|
||||
Some supporting non-Haskell libraries are required to build
|
||||
@ -76,7 +76,7 @@ you may need to install the following:
|
||||
- [The GNU Multiple Precision Arithmetic Library (GMP)](https://gmplib.org/)
|
||||
- [ncurses](https://www.gnu.org/software/ncurses/)
|
||||
|
||||
You'll also need [CVC4](#getting-cvc4) installed when running Cryptol.
|
||||
You'll also need [Z3](#getting-z3) installed when running Cryptol.
|
||||
|
||||
## Building Cryptol
|
||||
|
||||
|
@ -61,7 +61,7 @@ library
|
||||
process >= 1.2,
|
||||
QuickCheck >= 2.7,
|
||||
random >= 1.0.1,
|
||||
sbv >= 5.6,
|
||||
sbv >= 5.7,
|
||||
smtLib >= 1.0.7,
|
||||
simple-smt >= 0.6.0,
|
||||
syb >= 0.4,
|
||||
|
Binary file not shown.
@ -349,13 +349,13 @@ user the proof is complete.\indQED\indProve
|
||||
\nb{Cryptol uses off-the-shelf SAT\glosSAT and SMT\glosSMT solvers to
|
||||
perform these formal
|
||||
proofs~\cite{erkok-matthews-cryptolEqChecking-09}. By default,
|
||||
Cryptol will use the CVC4 SMT solver~\cite{cvc4WWW} under the hood,
|
||||
Cryptol will use Microsoft Research's Z3 SMT solver under the hood,
|
||||
but it can be configured to use other SAT/SMT solvers as well, such
|
||||
as SRI's Yices~\cite{YicesWWW}\indYices, or Microsoft Research's
|
||||
Z3~\cite{Z3WWW}\footnote{To do this, first install the package(s)
|
||||
as SRI's Yices~\cite{YicesWWW}\indYices, or CVC4
|
||||
~\cite{cvc4WWW}\footnote{To do this, first install the package(s)
|
||||
from the URLs provided in the bibliography. Once a prover has been
|
||||
installed you can activate it with, for example, {\tt :set
|
||||
prover=z3}.}. Note that the {\tt :prove} command is a
|
||||
prover=cvc4}.}. Note that the {\tt :prove} command is a
|
||||
push-button tool: once the proof starts there is no user
|
||||
involvement. Of course, the external tool used may not be able to
|
||||
complete all the proofs in a feasible amount of time, naturally.
|
||||
|
@ -261,7 +261,7 @@ aliases you have defined, along with their types.
|
||||
\texttt{base} & \texttt{10} & numeric base for printing words \\
|
||||
\texttt{debug} & \texttt{off} & whether to print verbose debugging information \\
|
||||
\texttt{infLength} & \texttt{5} & number of elements to show from an infinite sequence \\
|
||||
\texttt{prover} & \texttt{cvc4} & which SMT solver to use for \texttt{:prove} \\
|
||||
\texttt{prover} & \texttt{z3} & which SMT solver to use for \texttt{:prove} \\
|
||||
\texttt{tests} & \texttt{100} & number of tests to run for \texttt{:check} \\
|
||||
\texttt{warnDefaulting} & \texttt{on} & \todo[inline]{talk to Iavor} \\
|
||||
\hline
|
||||
|
@ -116,8 +116,8 @@ initialModuleEnv = do
|
||||
, meDynEnv = mempty
|
||||
, meMonoBinds = True
|
||||
, meSolverConfig = T.SolverConfig
|
||||
{ T.solverPath = "cvc4"
|
||||
, T.solverArgs = [ "--lang=smt2", "--incremental", "--rewrite-divk" ]
|
||||
{ T.solverPath = "z3"
|
||||
, T.solverArgs = [ "-smt2", "-in" ]
|
||||
, T.solverVerbose = 0
|
||||
}
|
||||
, meCoreLint = NoCoreLint
|
||||
|
@ -605,7 +605,7 @@ userOptions = mkOptionMap
|
||||
"The number of random tests to try."
|
||||
, simpleOpt "satNum" (EnvString "1") checkSatNum
|
||||
"The maximum number of :sat solutions to display (\"all\" for no limit)."
|
||||
, simpleOpt "prover" (EnvString "cvc4") checkProver $
|
||||
, simpleOpt "prover" (EnvString "z3") checkProver $
|
||||
"The external SMT solver for :prove and :sat (" ++ proverListString ++ ")."
|
||||
, simpleOpt "warnDefaulting" (EnvBool True) (const $ return Nothing)
|
||||
"Choose if we should display warnings when defaulting."
|
||||
@ -619,9 +619,7 @@ userOptions = mkOptionMap
|
||||
setModuleEnv me { M.meMonoBinds = b }
|
||||
_ -> return ()
|
||||
|
||||
, OptionDescr "tc-solver" (EnvProg "cvc4" [ "--lang=smt2"
|
||||
, "--incremental"
|
||||
, "--rewrite-divk" ])
|
||||
, OptionDescr "tc-solver" (EnvProg "z3" [ "-smt2", "-in" ])
|
||||
(const (return Nothing)) -- 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
|
||||
@ -709,27 +707,27 @@ whenDebug m = do
|
||||
smokeTest :: REPL [Smoke]
|
||||
smokeTest = catMaybes <$> sequence tests
|
||||
where
|
||||
tests = [ cvc4exists ]
|
||||
tests = [ z3exists ]
|
||||
|
||||
type SmokeTest = REPL (Maybe Smoke)
|
||||
|
||||
data Smoke
|
||||
= CVC4NotFound
|
||||
= Z3NotFound
|
||||
deriving (Show, Eq)
|
||||
|
||||
instance PP Smoke where
|
||||
ppPrec _ smoke =
|
||||
case smoke of
|
||||
CVC4NotFound -> text . intercalate " " $ [
|
||||
"[error] cvc4 is required to run Cryptol, but was not found in the"
|
||||
, "system path. See the Cryptol README for more on how to install cvc4."
|
||||
Z3NotFound -> text . intercalate " " $ [
|
||||
"[error] z3 is required to run Cryptol, but was not found in the"
|
||||
, "system path. See the Cryptol README for more on how to install z3."
|
||||
]
|
||||
|
||||
cvc4exists :: SmokeTest
|
||||
cvc4exists = do
|
||||
mPath <- io $ findExecutable "cvc4"
|
||||
z3exists :: SmokeTest
|
||||
z3exists = do
|
||||
mPath <- io $ findExecutable "z3"
|
||||
case mPath of
|
||||
Nothing -> return (Just CVC4NotFound)
|
||||
Nothing -> return (Just Z3NotFound)
|
||||
Just _ -> return Nothing
|
||||
|
||||
|
||||
|
@ -6,6 +6,7 @@
|
||||
-- Stability : provisional
|
||||
-- Portability : portable
|
||||
|
||||
{-# LANGUAGE FlexibleContexts #-}
|
||||
{-# LANGUAGE PatternGuards #-}
|
||||
{-# LANGUAGE RecordWildCards #-}
|
||||
{-# LANGUAGE ScopedTypeVariables #-}
|
||||
@ -19,7 +20,6 @@ import Data.List (transpose, intercalate)
|
||||
import qualified Data.Map as Map
|
||||
import qualified Control.Exception as X
|
||||
|
||||
import Data.SBV (intSizeOf)
|
||||
import qualified Data.SBV.Dynamic as SBV
|
||||
|
||||
import qualified Cryptol.ModuleSystem as M hiding (getPrimMap)
|
||||
@ -223,7 +223,7 @@ protectStack mkErr cmd modEnv =
|
||||
where isOverflow X.StackOverflow = Just ()
|
||||
isOverflow _ = Nothing
|
||||
msg = "Symbolic evaluation failed to terminate."
|
||||
handler () = mkErr msg modEnv -- (Right (ProverError msg, modEnv), [])
|
||||
handler () = mkErr msg modEnv
|
||||
|
||||
parseValues :: [FinType] -> [SBV.CW] -> ([Eval.Value], [SBV.CW])
|
||||
parseValues [] cws = ([], cws)
|
||||
@ -405,7 +405,7 @@ evalSel sel v =
|
||||
|
||||
ListSel n _ -> case v of
|
||||
VWord s -> VBit (SBV.svTestBit s i)
|
||||
where i = intSizeOf s - 1 - n
|
||||
where i = SBV.intSizeOf s - 1 - n
|
||||
_ -> fromSeq v !! n -- 0-based indexing
|
||||
|
||||
-- Declarations ----------------------------------------------------------------
|
||||
|
@ -640,8 +640,8 @@ _testSimpGoals = Num.withSolver cfg $ \s ->
|
||||
Right _ -> debugLog s "End of test"
|
||||
Left _ -> debugLog s "Impossible"
|
||||
where
|
||||
cfg = SolverConfig { solverPath = "cvc4"
|
||||
, solverArgs = [ "--lang=smt2", "--incremental", "--rewrite-divk" ]
|
||||
cfg = SolverConfig { solverPath = "z3"
|
||||
, solverArgs = [ "-smt2", "-in" ]
|
||||
, solverVerbose = 1
|
||||
}
|
||||
|
||||
|
@ -4,9 +4,9 @@ it : {result : Bit, arg1 : [4]}
|
||||
|
||||
Run-time error: no counterexample available
|
||||
True
|
||||
f 0x0 = False
|
||||
f 0xc = False
|
||||
it : {result : Bit, arg1 : [4]}
|
||||
{result = False, arg1 = 0x0}
|
||||
{result = False, arg1 = 0xc}
|
||||
False
|
||||
f 0x3 = True
|
||||
it : {result : Bit, arg1 : [4]}
|
||||
@ -16,9 +16,9 @@ Unsatisfiable
|
||||
it : {result : Bit, arg1 : [4]}
|
||||
|
||||
Run-time error: no satisfying assignment available
|
||||
g {x = 0x00000000, y = 0x00000001} = False
|
||||
g {x = 0xffffffff, y = 0x00000000} = False
|
||||
it : {result : Bit, arg1 : {x : [32], y : [32]}}
|
||||
{result = False, arg1 = {x = 0x00000000, y = 0x00000001}}
|
||||
{result = False, arg1 = {x = 0xffffffff, y = 0x00000000}}
|
||||
g {x = 0x00000000, y = 0x00000000} = True
|
||||
it : {result : Bit, arg1 : {x : [32], y : [32]}}
|
||||
{result = True, arg1 = {x = 0x00000000, y = 0x00000000}}
|
||||
|
@ -1,30 +1,30 @@
|
||||
Loading module Cryptol
|
||||
(\x -> x > 0x4) 0x5 = True
|
||||
it : {result : Bit, arg1 : [4]}
|
||||
{result = True, arg1 = 0x5}
|
||||
(\x -> x > 0x4) 0x5 = True
|
||||
(\x -> x > 0x4) 0x6 = True
|
||||
(\x -> x > 0x4) 0x7 = True
|
||||
it : {result : Bit, arg1 : [4]}
|
||||
{result = True, arg1 = 0x6}
|
||||
(\x -> x > 0x4) 0x6 = True
|
||||
(\x -> x > 0x4) 0x8 = True
|
||||
(\x -> x > 0x4) 0x5 = True
|
||||
(\x -> x > 0x4) 0x7 = True
|
||||
(\x -> x > 0x4) 0xd = True
|
||||
(\x -> x > 0x4) 0xc = True
|
||||
(\x -> x > 0x4) 0x9 = True
|
||||
(\x -> x > 0x4) 0xa = True
|
||||
(\x -> x > 0x4) 0xb = True
|
||||
(\x -> x > 0x4) 0xc = True
|
||||
(\x -> x > 0x4) 0xd = True
|
||||
(\x -> x > 0x4) 0xe = True
|
||||
(\x -> x > 0x4) 0xf = True
|
||||
(\x -> x > 0x4) 0xb = True
|
||||
it : [11]{result : Bit, arg1 : [4]}
|
||||
[{result = True, arg1 = 0x5}, {result = True, arg1 = 0x6},
|
||||
{result = True, arg1 = 0x7}, {result = True, arg1 = 0x8},
|
||||
[{result = True, arg1 = 0x6}, {result = True, arg1 = 0x8},
|
||||
{result = True, arg1 = 0x5}, {result = True, arg1 = 0x7},
|
||||
{result = True, arg1 = 0xd}, {result = True, arg1 = 0xc},
|
||||
{result = True, arg1 = 0x9}, {result = True, arg1 = 0xa},
|
||||
{result = True, arg1 = 0xb}, {result = True, arg1 = 0xc},
|
||||
{result = True, arg1 = 0xd}, {result = True, arg1 = 0xe},
|
||||
{result = True, arg1 = 0xf}]
|
||||
{result = True, arg1 = 0xe}, {result = True, arg1 = 0xf},
|
||||
{result = True, arg1 = 0xb}]
|
||||
must be an integer > 0 or "all"
|
||||
must be an integer > 0 or "all"
|
||||
(\x -> x > 0x4) 0x5 = True
|
||||
(\x -> x > 0x4) 0x6 = True
|
||||
(\x -> x > 0x4) 0x7 = True
|
||||
(\x -> x > 0x4) 0x8 = True
|
||||
(\x -> x > 0x4) 0x5 = True
|
||||
it : [3]{result : Bit, arg1 : [4]}
|
||||
[{result = True, arg1 = 0x5}, {result = True, arg1 = 0x6},
|
||||
{result = True, arg1 = 0x7}]
|
||||
[{result = True, arg1 = 0x6}, {result = True, arg1 = 0x8},
|
||||
{result = True, arg1 = 0x5}]
|
||||
|
@ -27,4 +27,4 @@ Coverage: 0.00% (100 of 2^^64 values)
|
||||
:sat t1
|
||||
t1 0x00000000 = True
|
||||
:sat t2
|
||||
t2 0x00000000 0x00000000 = True
|
||||
t2 0xfffffffe 0xffffffff = True
|
||||
|
@ -2,5 +2,5 @@ Loading module Cryptol
|
||||
Loading module Cryptol
|
||||
Loading module Main
|
||||
Q.E.D.
|
||||
av1 0xc00001c9 0xbfffffd5 = False
|
||||
av1 0xfdffffe0 0x7fffffe0 = False
|
||||
Q.E.D.
|
||||
|
@ -1,5 +1,5 @@
|
||||
Loading module Cryptol
|
||||
Loading module Cryptol
|
||||
Loading module r03
|
||||
(nQueens : Solution 5) [0x4, 0x2, 0x0, 0x3, 0x1] = True
|
||||
(nQueens : Solution 5) [0x3, 0x1, 0x4, 0x2, 0x0] = True
|
||||
(nQueensProve : Solution 4) [0x2, 0x0, 0x3, 0x1] = False
|
||||
|
Loading…
Reference in New Issue
Block a user