From 8d09c79198e546c1d04cd701acc9205735b14b86 Mon Sep 17 00:00:00 2001 From: Levent Erkok Date: Mon, 14 Jan 2019 16:49:19 -0800 Subject: [PATCH 1/8] Make Cryptol compile with SBV 8.0 SBV 8.0 is now on hackage, with several backwards compatibility breaking changes. You'll need this patch to compile cryptol against it. --- cryptol.cabal | 4 +-- src/Cryptol/Symbolic.hs | 52 +++++++++++++++++------------------ src/Cryptol/Symbolic/Value.hs | 14 +++++----- 3 files changed, 35 insertions(+), 35 deletions(-) diff --git a/cryptol.cabal b/cryptol.cabal index 942b6a00..f3b9c182 100644 --- a/cryptol.cabal +++ b/cryptol.cabal @@ -58,7 +58,7 @@ library pretty >= 1.1, process >= 1.2, random >= 1.0.1, - sbv >= 7.7, + sbv >= 8.0, simple-smt >= 0.7.1, strict, text >= 1.1, @@ -264,5 +264,5 @@ benchmark cryptol-bench , deepseq , directory , filepath - , sbv >= 7.7 + , sbv >= 8.0 , text diff --git a/src/Cryptol/Symbolic.hs b/src/Cryptol/Symbolic.hs index 935d52e5..26eaee36 100644 --- a/src/Cryptol/Symbolic.hs +++ b/src/Cryptol/Symbolic.hs @@ -208,8 +208,8 @@ satProve ProverCommand {..} = return $ AllSatResult tevss where mkTevs result = do - let Right (_, cws) = SBV.getModelAssignment result - (vs, _) = parseValues ts cws + let Right (_, cvs) = SBV.getModelAssignment result + (vs, _) = parseValues ts cvs sattys = unFinType <$> ts satexprs <- doEval (zipWithM (Eval.toExpr prims) sattys vs) @@ -265,37 +265,37 @@ protectStack mkErr cmd modEnv = msg = "Symbolic evaluation failed to terminate." handler () = mkErr msg modEnv -parseValues :: [FinType] -> [SBV.CW] -> ([Eval.Value], [SBV.CW]) -parseValues [] cws = ([], cws) -parseValues (t : ts) cws = (v : vs, cws'') - where (v, cws') = parseValue t cws - (vs, cws'') = parseValues ts cws' +parseValues :: [FinType] -> [SBV.CV] -> ([Eval.Value], [SBV.CV]) +parseValues [] cvs = ([], cvs) +parseValues (t : ts) cvs = (v : vs, cvs'') + where (v, cvs') = parseValue t cvs + (vs, cvs'') = parseValues ts cvs' -parseValue :: FinType -> [SBV.CW] -> (Eval.Value, [SBV.CW]) +parseValue :: FinType -> [SBV.CV] -> (Eval.Value, [SBV.CV]) parseValue FTBit [] = panic "Cryptol.Symbolic.parseValue" [ "empty FTBit" ] -parseValue FTBit (cw : cws) = (Eval.VBit (SBV.cwToBool cw), cws) -parseValue FTInteger cws = - case SBV.genParse SBV.KUnbounded cws of - Just (x, cws') -> (Eval.VInteger x, cws') +parseValue FTBit (cv : cvs) = (Eval.VBit (SBV.cvToBool cv), cvs) +parseValue FTInteger cvs = + case SBV.genParse SBV.KUnbounded cvs of + Just (x, cvs') -> (Eval.VInteger x, cvs') Nothing -> panic "Cryptol.Symbolic.parseValue" [ "no integer" ] -parseValue (FTIntMod _) cws = parseValue FTInteger cws -parseValue (FTSeq 0 FTBit) cws = (Eval.word 0 0, cws) -parseValue (FTSeq n FTBit) cws = - case SBV.genParse (SBV.KBounded False n) cws of - Just (x, cws') -> (Eval.word (toInteger n) x, cws') +parseValue (FTIntMod _) cvs = parseValue FTInteger cvs +parseValue (FTSeq 0 FTBit) cvs = (Eval.word 0 0, cvs) +parseValue (FTSeq n FTBit) cvs = + case SBV.genParse (SBV.KBounded False n) cvs of + Just (x, cvs') -> (Eval.word (toInteger n) x, cvs') Nothing -> (VWord (genericLength vs) $ return $ Eval.WordVal $ - Eval.packWord (map fromVBit vs), cws') - where (vs, cws') = parseValues (replicate n FTBit) cws -parseValue (FTSeq n t) cws = + Eval.packWord (map fromVBit vs), cvs') + where (vs, cvs') = parseValues (replicate n FTBit) cvs +parseValue (FTSeq n t) cvs = (Eval.VSeq (toInteger n) $ Eval.finiteSeqMap (map Eval.ready vs) - , cws' + , cvs' ) - where (vs, cws') = parseValues (replicate n t) cws -parseValue (FTTuple ts) cws = (Eval.VTuple (map Eval.ready vs), cws') - where (vs, cws') = parseValues ts cws -parseValue (FTRecord fs) cws = (Eval.VRecord (zip ns (map Eval.ready vs)), cws') + where (vs, cvs') = parseValues (replicate n t) cvs +parseValue (FTTuple ts) cvs = (Eval.VTuple (map Eval.ready vs), cvs') + where (vs, cvs') = parseValues ts cvs +parseValue (FTRecord fs) cvs = (Eval.VRecord (zip ns (map Eval.ready vs)), cvs') where (ns, ts) = unzip fs - (vs, cws') = parseValues ts cws + (vs, cvs') = parseValues ts cvs allDeclGroups :: M.ModuleEnv -> [DeclGroup] allDeclGroups = concatMap mDecls . M.loadedNonParamModules diff --git a/src/Cryptol/Symbolic/Value.hs b/src/Cryptol/Symbolic/Value.hs index 03209d11..8906ea22 100644 --- a/src/Cryptol/Symbolic/Value.hs +++ b/src/Cryptol/Symbolic/Value.hs @@ -34,6 +34,7 @@ import Data.Bits (bit, complement) import Data.List (foldl') import qualified Data.Sequence as Seq +import Data.SBV (symbolicEnv) import Data.SBV.Dynamic --import Cryptol.Eval.Monad @@ -48,7 +49,6 @@ 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 ------------------------------------------------------------- @@ -65,22 +65,22 @@ literalSWord :: Int -> Integer -> SWord literalSWord w i = svInteger (KBounded False w) i forallBV_ :: Int -> Symbolic SWord -forallBV_ w = ask >>= liftIO . svMkSymVar (Just ALL) (KBounded False w) Nothing +forallBV_ w = symbolicEnv >>= liftIO . svMkSymVar (Just ALL) (KBounded False w) Nothing existsBV_ :: Int -> Symbolic SWord -existsBV_ w = ask >>= liftIO . svMkSymVar (Just EX) (KBounded False w) Nothing +existsBV_ w = symbolicEnv >>= liftIO . svMkSymVar (Just EX) (KBounded False w) Nothing forallSBool_ :: Symbolic SBool -forallSBool_ = ask >>= liftIO . svMkSymVar (Just ALL) KBool Nothing +forallSBool_ = symbolicEnv >>= liftIO . svMkSymVar (Just ALL) KBool Nothing existsSBool_ :: Symbolic SBool -existsSBool_ = ask >>= liftIO . svMkSymVar (Just EX) KBool Nothing +existsSBool_ = symbolicEnv >>= liftIO . svMkSymVar (Just EX) KBool Nothing forallSInteger_ :: Symbolic SBool -forallSInteger_ = ask >>= liftIO . svMkSymVar (Just ALL) KUnbounded Nothing +forallSInteger_ = symbolicEnv >>= liftIO . svMkSymVar (Just ALL) KUnbounded Nothing existsSInteger_ :: Symbolic SBool -existsSInteger_ = ask >>= liftIO . svMkSymVar (Just EX) KUnbounded Nothing +existsSInteger_ = symbolicEnv >>= liftIO . svMkSymVar (Just EX) KUnbounded Nothing -- Values ---------------------------------------------------------------------- From 1dfc09e53390c28d492c7daeb70203040cc3dce1 Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Tue, 29 Jan 2019 18:04:15 -0800 Subject: [PATCH 2/8] Export evalSel from Cryptol.Eval This is needed to do eta-expansion of values when using Cryptol as a library. --- src/Cryptol/Eval.hs | 1 + 1 file changed, 1 insertion(+) diff --git a/src/Cryptol/Eval.hs b/src/Cryptol/Eval.hs index a018b1fd..42386027 100644 --- a/src/Cryptol/Eval.hs +++ b/src/Cryptol/Eval.hs @@ -25,6 +25,7 @@ module Cryptol.Eval ( , emptyEnv , evalExpr , evalDecls + , evalSel , EvalError(..) , forceValue ) where From 8ed77c130ddaa9db966046d6f77b61ae72ed4f58 Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Fri, 1 Feb 2019 08:16:44 -0800 Subject: [PATCH 3/8] Update SBV version in Cabal freeze files --- cabal.GHC82.config | 2 +- cabal.GHC84.config | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/cabal.GHC82.config b/cabal.GHC82.config index 614663ce..736d386a 100644 --- a/cabal.GHC82.config +++ b/cabal.GHC82.config @@ -90,7 +90,7 @@ constraints: Cabal -bundled-binary-generic, regex-posix ==0.95.2, regex-posix +newbase +splitbase, rts ==1.0, - sbv ==7.10, + sbv ==8.0, scientific ==0.3.5.2, scientific -bytestring-builder -integer-simple, semigroups ==0.18.4, diff --git a/cabal.GHC84.config b/cabal.GHC84.config index e50fa218..4348c86f 100644 --- a/cabal.GHC84.config +++ b/cabal.GHC84.config @@ -92,7 +92,7 @@ constraints: Cabal ==2.2.0.0, regex-posix ==0.95.2, regex-posix +newbase +splitbase, rts ==1.0, - sbv ==7.10, + sbv ==8.0, scientific ==0.3.5.3, scientific -bytestring-builder -integer-simple, semigroups ==0.18.4, From 016395f403447dfab2094de36f77c2a46a845f27 Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Fri, 1 Feb 2019 08:24:32 -0800 Subject: [PATCH 4/8] Update frozen versions of crackNum --- cabal.GHC80.config | 2 +- cabal.GHC82.config | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/cabal.GHC80.config b/cabal.GHC80.config index 2d99f33e..7dc4124d 100644 --- a/cabal.GHC80.config +++ b/cabal.GHC80.config @@ -372,7 +372,7 @@ constraints: abstract-deque ==0.3, cpuinfo ==0.1.0.1, cql ==3.1.1, cql-io ==0.16.0, - crackNum ==1.9, + crackNum ==2.0, criterion ==1.1.4.0, cron ==0.5.0, crypto-api ==0.13.2, diff --git a/cabal.GHC82.config b/cabal.GHC82.config index 736d386a..edfb3a93 100644 --- a/cabal.GHC82.config +++ b/cabal.GHC82.config @@ -38,7 +38,7 @@ constraints: Cabal -bundled-binary-generic, code-page ==0.1.3, colour ==2.3.4, containers ==0.5.10.2, - crackNum ==1.9, + crackNum ==2.0, criterion ==1.4.0.0, criterion -embed-data-files -fast, cryptol +relocatable -static, From 10e87616a21b42d947c7398ae1bb289e36e92372 Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Fri, 1 Feb 2019 08:51:16 -0800 Subject: [PATCH 5/8] Update frozen versions of crackNum --- cabal.GHC80.config | 2 +- cabal.GHC82.config | 2 +- cabal.GHC84.config | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/cabal.GHC80.config b/cabal.GHC80.config index 7dc4124d..9ca49d21 100644 --- a/cabal.GHC80.config +++ b/cabal.GHC80.config @@ -372,7 +372,7 @@ constraints: abstract-deque ==0.3, cpuinfo ==0.1.0.1, cql ==3.1.1, cql-io ==0.16.0, - crackNum ==2.0, + crackNum ==2.3, criterion ==1.1.4.0, cron ==0.5.0, crypto-api ==0.13.2, diff --git a/cabal.GHC82.config b/cabal.GHC82.config index edfb3a93..5a40a780 100644 --- a/cabal.GHC82.config +++ b/cabal.GHC82.config @@ -38,7 +38,7 @@ constraints: Cabal -bundled-binary-generic, code-page ==0.1.3, colour ==2.3.4, containers ==0.5.10.2, - crackNum ==2.0, + crackNum ==2.3, criterion ==1.4.0.0, criterion -embed-data-files -fast, cryptol +relocatable -static, diff --git a/cabal.GHC84.config b/cabal.GHC84.config index 4348c86f..3ded4640 100644 --- a/cabal.GHC84.config +++ b/cabal.GHC84.config @@ -38,7 +38,7 @@ constraints: Cabal ==2.2.0.0, code-page ==0.1.3, colour ==2.3.4, containers ==0.5.11.0, - crackNum ==2.0, + crackNum ==2.3, criterion ==1.4.0.0, criterion -embed-data-files -fast, cryptol +relocatable -static, From b1edb9e36e182a8f2b29d6b6a98d11bf481ff63d Mon Sep 17 00:00:00 2001 From: Brian Huffman Date: Fri, 8 Feb 2019 09:56:37 -0800 Subject: [PATCH 6/8] No more rebindable syntax. Fixes #568. When syntactic sugar for constants "negate", "complement" or "splitAt" is used, the names of those primitives are now resolved during the type checking phase. This makes them consistent with the handling of other desugared primitives like "fromThen", etc. --- src/Cryptol/ModuleSystem/Renamer.hs | 8 +++++--- src/Cryptol/Parser/AST.hs | 4 ++++ src/Cryptol/Parser/Names.hs | 2 ++ src/Cryptol/Parser/NoPat.hs | 4 ++-- src/Cryptol/TypeCheck/Infer.hs | 22 +++++++++++++++------- 5 files changed, 28 insertions(+), 12 deletions(-) diff --git a/src/Cryptol/ModuleSystem/Renamer.hs b/src/Cryptol/ModuleSystem/Renamer.hs index 996927a2..1dc4356d 100644 --- a/src/Cryptol/ModuleSystem/Renamer.hs +++ b/src/Cryptol/ModuleSystem/Renamer.hs @@ -34,7 +34,7 @@ import Cryptol.Prims.Syntax import Cryptol.Parser.AST import Cryptol.Parser.Position import Cryptol.TypeCheck.Type (TCon(..)) -import Cryptol.Utils.Ident (packInfix,packIdent) +import Cryptol.Utils.Ident (packInfix) import Cryptol.Utils.Panic (panic) import Cryptol.Utils.PP @@ -747,8 +747,9 @@ instance Rename Expr where rename expr = case expr of EVar n -> EVar <$> renameVar n ELit l -> return (ELit l) - ENeg e -> rename (EApp (EVar (mkUnqual (packIdent "negate"))) e) - EComplement e -> rename (EApp (EVar (mkUnqual (packIdent "complement"))) e) + ENeg e -> ENeg <$> rename e + EComplement e -> EComplement + <$> rename e ETuple es -> ETuple <$> traverse rename es ERecord fs -> ERecord <$> traverse (rnNamed rename) fs ESel e' s -> ESel <$> rename e' <*> pure s @@ -777,6 +778,7 @@ instance Rename Expr where ELocated e' r -> withLoc r $ ELocated <$> rename e' <*> pure r + ESplit e -> ESplit <$> rename e EParens p -> EParens <$> rename p EInfix x y _ z-> do op <- renameOp y x' <- rename x diff --git a/src/Cryptol/Parser/AST.hs b/src/Cryptol/Parser/AST.hs index e699d746..6a561949 100644 --- a/src/Cryptol/Parser/AST.hs +++ b/src/Cryptol/Parser/AST.hs @@ -276,6 +276,7 @@ data Expr n = EVar n -- ^ @ x @ | EFun [Pattern n] (Expr n) -- ^ @ \\x y -> x @ | ELocated (Expr n) Range -- ^ position annotation + | ESplit (Expr n) -- ^ @ splitAt x @ (Introduced by NoPat) | EParens (Expr n) -- ^ @ (e) @ (Removed by Fixity) | EInfix (Expr n) (Located n) Fixity (Expr n)-- ^ @ a + b @ (Removed by Fixity) deriving (Eq, Show, Generic, NFData, Functor) @@ -713,6 +714,8 @@ instance (Show name, PPName name) => PP (Expr name) where ELocated e _ -> ppPrec n e + ESplit e -> wrap n 3 (text "splitAt" <+> ppPrec 4 e) + EParens e -> parens (pp e) EInfix e1 op _ e2 -> wrap n 0 (pp e1 <+> ppInfixName (thing op) <+> pp e2) @@ -939,6 +942,7 @@ instance NoPos (Expr name) where EFun x y -> EFun (noPos x) (noPos y) ELocated x _ -> noPos x + ESplit x -> ESplit (noPos x) EParens e -> EParens (noPos e) EInfix x y f z-> EInfix (noPos x) y f (noPos z) diff --git a/src/Cryptol/Parser/Names.hs b/src/Cryptol/Parser/Names.hs index d7e585a6..32b808f2 100644 --- a/src/Cryptol/Parser/Names.hs +++ b/src/Cryptol/Parser/Names.hs @@ -100,6 +100,7 @@ namesE expr = EFun ps e -> boundNames (namesPs ps) (namesE e) ELocated e _ -> namesE e + ESplit e -> namesE e EParens e -> namesE e EInfix a o _ b-> Set.insert (thing o) (Set.union (namesE a) (namesE b)) @@ -241,6 +242,7 @@ tnamesE expr = EFun ps e -> Set.union (Set.unions (map tnamesP ps)) (tnamesE e) ELocated e _ -> tnamesE e + ESplit e -> tnamesE e EParens e -> tnamesE e EInfix a _ _ b-> Set.union (tnamesE a) (tnamesE b) diff --git a/src/Cryptol/Parser/NoPat.hs b/src/Cryptol/Parser/NoPat.hs index dc31c5b2..3e673a5f 100644 --- a/src/Cryptol/Parser/NoPat.hs +++ b/src/Cryptol/Parser/NoPat.hs @@ -120,8 +120,7 @@ noPat pat = x <- newName tmp <- newName r <- getRange - let prim = EVar (mkUnqual (mkIdent "splitAt")) - bTmp = simpleBind (Located r tmp) (EApp prim (EVar x)) + let bTmp = simpleBind (Located r tmp) (ESplit (EVar x)) b1 = sel a1 tmp (TupleSel 0 (Just 2)) b2 = sel a2 tmp (TupleSel 1 (Just 2)) return (pVar r x, bTmp : b1 : b2 : ds1 ++ ds2) @@ -166,6 +165,7 @@ noPatE expr = return (EFun ps1 e1) ELocated e r1 -> ELocated <$> inRange r1 (noPatE e) <*> return r1 + ESplit e -> ESplit <$> noPatE e EParens e -> EParens <$> noPatE e EInfix x y f z-> EInfix <$> noPatE x <*> pure y <*> pure f <*> noPatE z diff --git a/src/Cryptol/TypeCheck/Infer.hs b/src/Cryptol/TypeCheck/Infer.hs index 64dd7656..8cdd4be8 100644 --- a/src/Cryptol/TypeCheck/Infer.hs +++ b/src/Cryptol/TypeCheck/Infer.hs @@ -145,10 +145,6 @@ appTys expr ts tGoal = appTys e ts tGoal - P.ENeg {} -> panic "appTys" ["[bug] renamer bug", "unexpected ENeg" ] - P.EComplement {} -> - panic "appTys" ["[bug] renamer bug", "unexpected EComplement" ] - P.EAppT e fs -> do ps <- mapM inferTyParam fs appTys e (ps ++ ts) tGoal @@ -163,6 +159,9 @@ appTys expr ts tGoal = P.ELocated e r -> inRange r (appTys e ts tGoal) + P.ENeg {} -> mono + P.EComplement {} -> mono + P.ETuple {} -> mono P.ERecord {} -> mono P.ESel {} -> mono @@ -175,6 +174,7 @@ appTys expr ts tGoal = P.ETyped {} -> mono P.ETypeVal {} -> mono P.EFun {} -> mono + P.ESplit {} -> mono P.EParens e -> appTys e ts tGoal P.EInfix a op _ b -> appTys (P.EVar (thing op) `P.EApp` a `P.EApp` b) ts tGoal @@ -228,9 +228,13 @@ checkE expr tGoal = checkHasType t tGoal return e' - P.ENeg {} -> panic "checkE" ["[bug] renamer bug", "unexpected ENeg" ] - P.EComplement {} -> - panic "checkE" ["[bug] renamer bug", "unexpected EComplement" ] + P.ENeg e -> + do prim <- mkPrim "negate" + checkE (P.EApp prim e) tGoal + + P.EComplement e -> + do prim <- mkPrim "complement" + checkE (P.EApp prim e) tGoal P.ELit l@(P.ECNum _ P.DecLit) -> do e <- desugarLiteral False l @@ -382,6 +386,10 @@ checkE expr tGoal = P.ELocated e r -> inRange r (checkE e tGoal) + P.ESplit e -> + do prim <- mkPrim "splitAt" + checkE (P.EApp prim e) tGoal + P.EInfix a op _ b -> checkE (P.EVar (thing op) `P.EApp` a `P.EApp` b) tGoal P.EParens e -> checkE e tGoal From 244848326c8dc74ac5dfb7b1f498b580ed7e6728 Mon Sep 17 00:00:00 2001 From: Brian Huffman Date: Mon, 11 Feb 2019 10:57:29 -0800 Subject: [PATCH 7/8] Special case for `svFromInteger` at bit width 0. Fixes #563. This change ensures that `fromInteger x : [0]` is concrete, even if `x` is symbolic. --- src/Cryptol/Symbolic/Value.hs | 1 + 1 file changed, 1 insertion(+) diff --git a/src/Cryptol/Symbolic/Value.hs b/src/Cryptol/Symbolic/Value.hs index 8906ea22..313684cc 100644 --- a/src/Cryptol/Symbolic/Value.hs +++ b/src/Cryptol/Symbolic/Value.hs @@ -238,6 +238,7 @@ svToInteger w = -- TODO: implement this properly in SBV using "int2bv" svFromInteger :: Integer -> SInteger -> SWord +svFromInteger 0 _ = literalSWord 0 0 svFromInteger n i = case svAsInteger i of Nothing -> svFromIntegral (KBounded False (fromInteger n)) i From fd67463b2bda2eba768664e44b8f4be54c4094d9 Mon Sep 17 00:00:00 2001 From: Iavor Diatchki Date: Tue, 12 Feb 2019 14:38:17 -0800 Subject: [PATCH 8/8] Add a hacky way to get local executable path --- cry | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/cry b/cry index a401393b..b9b08ecd 100755 --- a/cry +++ b/cry @@ -19,6 +19,7 @@ Available commands: build Build Cryptol haddock Generate Haddock documentation test Run some tests + exe-path Print the location of the local executable EOM } @@ -78,6 +79,10 @@ case $COMMAND in show_usage exit 0;; + exe-path) + cabal v2-run exe:cryptol --verbose -- -c ':q' | grep :q | awk '{ print $1 }' + exit 0;; + *) echo Unrecognized command: $COMMAND show_usage