mirror of
https://github.com/GaloisInc/cryptol.git
synced 2024-11-28 01:13:34 +03:00
Modifications to make cryptol compile with SBV 7.0
Also, bumped up the version to 2.4.1
This commit is contained in:
Levent Erkok
parent
25e2ba01c6
commit
5857477ab2
@ -1,5 +1,5 @@
|
||||
Name: cryptol
|
||||
Version: 2.4.0
|
||||
Version: 2.4.1
|
||||
Synopsis: Cryptol: The Language of Cryptography
|
||||
Description: Cryptol is a domain-specific language for specifying cryptographic algorithms. A Cryptol implementation of an algorithm resembles its mathematical specification more closely than an implementation in a general purpose language. For more, see <http://www.cryptol.net/>.
|
||||
License: BSD3
|
||||
@ -61,7 +61,7 @@ library
|
||||
process >= 1.2,
|
||||
QuickCheck >= 2.7,
|
||||
random >= 1.0.1,
|
||||
sbv >= 5.15,
|
||||
sbv >= 7.0,
|
||||
smtLib >= 1.0.7,
|
||||
simple-smt >= 0.7.0,
|
||||
syb >= 0.4,
|
||||
@ -70,7 +70,9 @@ library
|
||||
tf-random >= 0.5,
|
||||
transformers >= 0.3,
|
||||
transformers-base >= 0.4,
|
||||
utf8-string >= 0.3
|
||||
utf8-string >= 0.3,
|
||||
mtl >= 2.2.1,
|
||||
time >= 1.6.0.1
|
||||
|
||||
Build-tools: alex, happy
|
||||
hs-source-dirs: src
|
||||
@ -204,7 +206,7 @@ executable cryptol
|
||||
, monad-control
|
||||
, process
|
||||
, random
|
||||
, sbv
|
||||
, sbv >= 7.0
|
||||
, tf-random
|
||||
, transformers
|
||||
GHC-options: -Wall -O2 -threaded -rtsopts "-with-rtsopts=-N1 -A64m"
|
||||
@ -263,5 +265,5 @@ benchmark cryptol-bench
|
||||
, deepseq
|
||||
, directory
|
||||
, filepath
|
||||
, sbv
|
||||
, sbv >= 7.0
|
||||
, text
|
||||
|
||||
@ -104,7 +104,8 @@ import Data.IORef(newIORef,readIORef)
|
||||
import Prelude ()
|
||||
import Prelude.Compat
|
||||
|
||||
import Data.SBV(TimedStep(..),showTDiff,Solver)
|
||||
import qualified Data.SBV as SBV (Solver)
|
||||
import qualified Data.SBV.Internals as SBV (showTDiff)
|
||||
|
||||
-- Commands --------------------------------------------------------------------
|
||||
|
||||
@ -396,18 +397,13 @@ satCmd, proveCmd :: String -> REPL ()
|
||||
satCmd = cmdProveSat True
|
||||
proveCmd = cmdProveSat False
|
||||
|
||||
showProverStats :: Maybe Solver -> ProverStats -> REPL ()
|
||||
showProverStats mprover = rPutStrLn
|
||||
. ('\n':) . parns
|
||||
. intercalate ", " . map sh . Map.toList
|
||||
showProverStats :: Maybe SBV.Solver -> ProverStats -> REPL ()
|
||||
showProverStats mprover stat = rPutStrLn
|
||||
. ('\n':) . parns
|
||||
. intercalate ", " . map sh $ [("Total Elapsed Time", stat)]
|
||||
where
|
||||
lab ProblemConstruction = "simulation"
|
||||
lab Translation = "export"
|
||||
lab (WorkByProver x) = case mprover of
|
||||
Just prover | x == show prover -> '*' : x
|
||||
_ -> x
|
||||
|
||||
sh (x, y) = lab x ++ ":" ++ showTDiff y
|
||||
sh (x, y) = x ++ ": " ++ SBV.showTDiff y
|
||||
|
||||
parns x = '(' : x ++ ")"
|
||||
|
||||
@ -496,7 +492,7 @@ cmdProveSat isSat str = do
|
||||
|
||||
onlineProveSat :: Bool
|
||||
-> String -> Maybe FilePath
|
||||
-> REPL (Maybe Solver,Symbolic.ProverResult,ProverStats)
|
||||
-> REPL (Maybe SBV.Solver,Symbolic.ProverResult,ProverStats)
|
||||
onlineProveSat isSat str mfile = do
|
||||
EnvString proverName <- getUser "prover"
|
||||
EnvBool verbose <- getUser "debug"
|
||||
@ -504,7 +500,7 @@ onlineProveSat isSat str mfile = do
|
||||
parseExpr <- replParseExpr str
|
||||
(_, expr, schema) <- replCheckExpr parseExpr
|
||||
decls <- fmap M.deDecls getDynEnv
|
||||
timing <- io (newIORef Map.empty)
|
||||
timing <- io (newIORef 0)
|
||||
let cmd = Symbolic.ProverCommand {
|
||||
pcQueryType = if isSat then SatQuery satNum else ProveQuery
|
||||
, pcProverName = proverName
|
||||
@ -525,7 +521,7 @@ offlineProveSat isSat str mfile = do
|
||||
parseExpr <- replParseExpr str
|
||||
(_, expr, schema) <- replCheckExpr parseExpr
|
||||
decls <- fmap M.deDecls getDynEnv
|
||||
timing <- io (newIORef Map.empty)
|
||||
timing <- io (newIORef 0)
|
||||
let cmd = Symbolic.ProverCommand {
|
||||
pcQueryType = if isSat then SatQuery (SomeSat 0) else ProveQuery
|
||||
, pcProverName = "offline"
|
||||
|
||||
@ -23,7 +23,8 @@ import Data.IORef(IORef)
|
||||
import qualified Control.Exception as X
|
||||
|
||||
import qualified Data.SBV.Dynamic as SBV
|
||||
import Data.SBV (Timing(SaveTiming),TimingInfo)
|
||||
import Data.SBV (Timing(SaveTiming))
|
||||
import Data.SBV.Internals (showTDiff)
|
||||
|
||||
import qualified Cryptol.ModuleSystem as M hiding (getPrimMap)
|
||||
import qualified Cryptol.ModuleSystem.Env as M
|
||||
@ -46,6 +47,8 @@ import Cryptol.Utils.Panic(panic)
|
||||
import Prelude ()
|
||||
import Prelude.Compat
|
||||
|
||||
import Data.Time (NominalDiffTime)
|
||||
|
||||
type EvalEnv = GenEvalEnv SBool SWord
|
||||
|
||||
|
||||
@ -101,7 +104,7 @@ data ProverCommand = ProverCommand {
|
||||
-- ^ The 'Schema' of @pcExpr@
|
||||
}
|
||||
|
||||
type ProverStats = TimingInfo
|
||||
type ProverStats = NominalDiffTime
|
||||
|
||||
-- | A prover result is either an error message, an empty result (eg
|
||||
-- for the offline prover), a counterexample or a lazy list of
|
||||
@ -115,7 +118,7 @@ satSMTResults :: SBV.SatResult -> [SBV.SMTResult]
|
||||
satSMTResults (SBV.SatResult r) = [r]
|
||||
|
||||
allSatSMTResults :: SBV.AllSatResult -> [SBV.SMTResult]
|
||||
allSatSMTResults (SBV.AllSatResult (_, rs)) = rs
|
||||
allSatSMTResults (SBV.AllSatResult (_, _, rs)) = rs
|
||||
|
||||
thmSMTResults :: SBV.ThmResult -> [SBV.SMTResult]
|
||||
thmSMTResults (SBV.ThmResult r) = [r]
|
||||
@ -137,7 +140,7 @@ satProve ProverCommand {..} =
|
||||
provers <-
|
||||
case pcProverName of
|
||||
"any" -> M.io SBV.sbvAvailableSolvers
|
||||
_ -> return [(lookupProver pcProverName) { SBV.smtFile = pcSmtFile }]
|
||||
_ -> return [(lookupProver pcProverName) { SBV.transcript = pcSmtFile }]
|
||||
|
||||
|
||||
let provers' = [ p { SBV.timing = SaveTiming pcProverStats, SBV.verbose = pcVerbose } | p <- provers ]
|
||||
@ -146,10 +149,10 @@ satProve ProverCommand {..} =
|
||||
case provers of
|
||||
[prover] -> do
|
||||
when pcVerbose $ M.io $
|
||||
putStrLn $ "Trying proof with " ++ show prover
|
||||
putStrLn $ "Trying proof with " ++ show (SBV.name (SBV.solver prover))
|
||||
res <- M.io (fn prover e)
|
||||
when pcVerbose $ M.io $
|
||||
putStrLn $ "Got result from " ++ show prover
|
||||
putStrLn $ "Got result from " ++ show (SBV.name (SBV.solver prover))
|
||||
return (Nothing, tag res) -- TODO: can identify prover here
|
||||
_ ->
|
||||
return ( Nothing
|
||||
@ -161,10 +164,10 @@ satProve ProverCommand {..} =
|
||||
runProvers fn tag e = do
|
||||
when pcVerbose $ M.io $
|
||||
putStrLn $ "Trying proof with " ++
|
||||
intercalate ", " (map show provers)
|
||||
(firstProver, res) <- M.io (fn provers' e)
|
||||
intercalate ", " (map (show . SBV.name . SBV.solver) provers)
|
||||
(firstProver, timeElapsed, res) <- M.io (fn provers' e)
|
||||
when pcVerbose $ M.io $
|
||||
putStrLn $ "Got result from " ++ show firstProver
|
||||
putStrLn $ "Got result from " ++ show firstProver ++ ", time: " ++ showTDiff timeElapsed
|
||||
return (Just firstProver, tag res)
|
||||
let runFn = case pcQueryType of
|
||||
ProveQuery -> runProvers SBV.proveWithAny thmSMTResults
|
||||
@ -193,7 +196,7 @@ satProve ProverCommand {..} =
|
||||
return $ AllSatResult tevss
|
||||
where
|
||||
mkTevs result = do
|
||||
let Right (_, cws) = SBV.getModel result
|
||||
let Right (_, cws) = SBV.getModelAssignment result
|
||||
(vs, _) = parseValues ts cws
|
||||
sattys = unFinType <$> ts
|
||||
satexprs <- liftIO $ Eval.runEval
|
||||
@ -210,7 +213,7 @@ satProve ProverCommand {..} =
|
||||
[] -> return $ ThmResult (unFinType <$> ts)
|
||||
-- otherwise something is wrong
|
||||
_ -> return $ ProverError (rshow results)
|
||||
where rshow | isSat = show . SBV.AllSatResult . (boom,)
|
||||
where rshow | isSat = show . SBV.AllSatResult . (boom,boom,)
|
||||
| otherwise = show . SBV.ThmResult . head
|
||||
boom = panic "Cryptol.Symbolic.sat"
|
||||
[ "attempted to evaluate bogus boolean for pretty-printing" ]
|
||||
@ -231,7 +234,7 @@ satProveOffline ProverCommand {..} =
|
||||
v <- liftIO $ Eval.runEval $
|
||||
do env <- Eval.evalDecls extDgs mempty
|
||||
Eval.evalExpr env pcExpr
|
||||
smtlib <- SBV.compileToSMTLib SBV.SMTLib2 isSat $ do
|
||||
smtlib <- SBV.generateSMTBenchmark isSat $ do
|
||||
args <- mapM tyFn ts
|
||||
liftIO $ Eval.runEval
|
||||
(fromVBit <$> foldM fromVFun v (map Eval.ready args))
|
||||
|
||||
@ -44,6 +44,9 @@ import Cryptol.Eval.Value ( GenValue(..), BitWord(..), lam, tlam, toStream,
|
||||
import Cryptol.Utils.Panic (panic)
|
||||
import Cryptol.Utils.PP
|
||||
|
||||
import Control.Monad.Reader (ask)
|
||||
import Control.Monad.Trans (liftIO)
|
||||
|
||||
-- SBool and SWord -------------------------------------------------------------
|
||||
|
||||
type SBool = SVal
|
||||
@ -57,16 +60,16 @@ literalSWord :: Int -> Integer -> SWord
|
||||
literalSWord w i = svInteger (KBounded False w) i
|
||||
|
||||
forallBV_ :: Int -> Symbolic SWord
|
||||
forallBV_ w = svMkSymVar (Just ALL) (KBounded False w) Nothing
|
||||
forallBV_ w = ask >>= liftIO . svMkSymVar (Just ALL) (KBounded False w) Nothing
|
||||
|
||||
existsBV_ :: Int -> Symbolic SWord
|
||||
existsBV_ w = svMkSymVar (Just EX) (KBounded False w) Nothing
|
||||
existsBV_ w = ask >>= liftIO . svMkSymVar (Just EX) (KBounded False w) Nothing
|
||||
|
||||
forallSBool_ :: Symbolic SBool
|
||||
forallSBool_ = svMkSymVar (Just ALL) KBool Nothing
|
||||
forallSBool_ = ask >>= liftIO . svMkSymVar (Just ALL) KBool Nothing
|
||||
|
||||
existsSBool_ :: Symbolic SBool
|
||||
existsSBool_ = svMkSymVar (Just EX) KBool Nothing
|
||||
existsSBool_ = ask >>= liftIO . svMkSymVar (Just EX) KBool Nothing
|
||||
|
||||
-- Values ----------------------------------------------------------------------
|
||||
|
||||
|
||||
Loading…
Reference in New Issue
Block a user