GaloisInc/cryptol
1
1
Fork 0
mirror of https://github.com/GaloisInc/cryptol.git synced 2025-01-07 08:19:12 +03:00
Code Issues Projects Releases Wiki Activity

Merge branch 'master' into rec-upd

Browse Source
This commit is contained in:
Iavor Diatchki 2019-02-12 14:48:14 -08:00
commit 40642ff43e
13 changed files with 75 additions and 52 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
cabal.GHC80.config
View File

@ -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.3,
criterion ==1.1.4.0,
cron ==0.5.0,
crypto-api ==0.13.2,

4
cabal.GHC82.config
View File

@ -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.3,
criterion ==1.4.0.0,
criterion -embed-data-files -fast,
cryptol +relocatable -static,
@ -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,

4
cabal.GHC84.config
View File

@ -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,
@ -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,

5
cry
View File

@ -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

4
cryptol.cabal
View File

@ -58,7 +58,7 @@ library
pretty >= 1.1,
process >= 1.2,
random >= 1.0.1,
sbv >= 7.7 && < 8,
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 && < 8
, sbv >= 8.0
, text

1
src/Cryptol/Eval.hs
View File

@ -25,6 +25,7 @@ module Cryptol.Eval (
, emptyEnv
, evalExpr
, evalDecls
, evalSel
, EvalError(..)
, forceValue
) where

8
src/Cryptol/ModuleSystem/Renamer.hs
View File

@ -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
@ -750,8 +750,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
@ -781,6 +782,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

4
src/Cryptol/Parser/AST.hs
View File

@ -279,6 +279,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)
@ -726,6 +727,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)
@ -961,6 +964,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)

2
src/Cryptol/Parser/Names.hs
View File

@ -102,6 +102,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))
@ -248,6 +249,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)

4
src/Cryptol/Parser/NoPat.hs
View File

@ -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)
@ -167,6 +166,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

52
src/Cryptol/Symbolic.hs
View File

@ -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

15
src/Cryptol/Symbolic/Value.hs
View File

@ -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 ----------------------------------------------------------------------
@ -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

22
src/Cryptol/TypeCheck/Infer.hs
View File

@ -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