GaloisInc/cryptol
1
1
Fork 0
mirror of https://github.com/GaloisInc/cryptol.git synced 2024-12-16 20:03:27 +03:00
Code Issues Projects Releases Wiki Activity

changed errors to panics for better reporting

Browse Source 
Also squashed a couple incomplete patterns when they came up, but
haven't done a full check for all of them.
This commit is contained in:
Adam C. Foltzer 2014-09-02 17:45:39 -07:00
parent 17ee75ea6a
commit 696b96fe12
9 changed files with 83 additions and 42 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -18,6 +18,8 @@ import qualified Data.Text.Lazy as Text
import Data.Char(isSpace)
import System.FilePath(takeExtension)
import Cryptol.Utils.Panic
data PreProc = None | Markdown | LaTeX
knownExts :: [String]
@ -59,7 +61,7 @@ toCryptol (Comment ls) =
in "/* " `Text.append` l1 : more ++ [ l `Text.append` " */" ]
where
splitLast [] = error "splitLats []"
splitLast [] = panic "Cryptol.Parser.Unlit.toCryptol" [ "splitLast []" ]
splitLast [x] = ([], x)
splitLast (x : xs) = let (ys,y) = splitLast xs
in (x:ys,y)

16
src/Cryptol/Prims/Eval.hs
View File

@ -36,14 +36,16 @@ import System.Random (mkStdGen)
-- Utilities -------------------------------------------------------------------
#if __GLASGOW_HASKELL__ < 706
noNum = panic "Cryptol.Prims.Eval"
[ "Num instance for Bool shouldn't be used." ]
instance Num Bool where
_ + _ = error "Num instance for Bool shouldn't be used."
_ * _ = error "Num instance for Bool shouldn't be used."
_ - _ = error "Num instance for Bool shouldn't be used."
negate _ = error "Num instance for Bool shouldn't be used."
abs _ = error "Num instance for Bool shouldn't be used."
signum _ = error "Num instance for Bool shouldn't be used."
fromInteger _ = error "Num instance for Bool shouldn't be used."
_ + _ = noNum
_ * _ = noNum
_ - _ = noNum
negate _ = noNum
abs _ = noNum
signum _ = noNum
fromInteger _ = noNum
#endif
#if __GLASGOW_HASKELL__ < 708

7
src/Cryptol/Symbolic.hs
View File

@ -55,7 +55,8 @@ lookupProver :: String -> SBV.SMTConfig
lookupProver s =
case lookup s proverConfigs of
Just cfg -> cfg
Nothing -> error $ "invalid prover: " ++ s
-- should be caught by UI for setting prover user variable
Nothing -> panic "Cryptol.Symbolic" [ "invalid prover: " ++ s ]
-- | A prover result is either an error message, or potentially a
-- counterexample or satisfying assignment.
@ -141,12 +142,12 @@ parseValues (t : ts) cws = (v : vs, cws'')
(vs, cws'') = parseValues ts cws'
parseValue :: FinType -> [SBV.CW] -> (Eval.Value, [SBV.CW])
parseValue FTBit [] = error "parseValue"
parseValue FTBit [] = panic "Cryptol.Symbolic.parseValue" [ "empty FTBit" ]
parseValue FTBit (cw : cws) = (Eval.VBit (SBV.fromCW cw), cws)
parseValue (FTSeq 0 FTBit) cws = (Eval.VWord (Eval.BV 0 0), cws)
parseValue (FTSeq n FTBit) (cw : cws)
| SBV.isBounded cw = (Eval.VWord (Eval.BV (toInteger n) (SBV.fromCW cw)), cws)
| otherwise = error "parseValue"
| otherwise = panic "Cryptol.Symbolic.parseValue" [ "unbounded concrete word" ]
parseValue (FTSeq n FTBit) cws = (Eval.VSeq True vs, cws')
where (vs, cws') = parseValues (replicate n FTBit) cws
parseValue (FTSeq n t) cws = (Eval.VSeq False vs, cws')

28
src/Cryptol/Symbolic/BitVector.hs
View File

@ -21,6 +21,8 @@ import Data.SBV.Bridge.Yices
import Data.SBV.Internals
import Data.SBV.BitVectors.Data
import Cryptol.Utils.Panic
-- BitVector type --------------------------------------------------------------
data BitVector = BV { signedcxt :: Bool, width :: !Int, val :: !Integer }
@ -46,7 +48,9 @@ signed w x
| otherwise = x
same :: Int -> Int -> Int
same m n = if m == n then m else error $ "BitVector size mismatch: " ++ show (m, n)
same m n | m == n = m
| otherwise = panic "Cryptol.Symbolic.BitVector.same"
[ "BitVector size mismatch: " ++ show (m, n) ]
instance SignCast SWord SWord where
signCast (SBV (KBounded _ w) (Left (cwVal -> (CWInteger x)))) =
@ -56,7 +60,8 @@ instance SignCast SWord SWord where
k = KBounded True w
y st = do xsw <- sbvToSW st x
newExpr st k (SBVApp (Extract (intSizeOf x-1) 0) [xsw])
signCast _ = error "SignCast not called on BitVector value"
signCast _ = panic "Cryptol.Symbolic.BitVector"
[ "signCast called on non-bitvector value" ]
unsignCast (SBV (KBounded _ w) (Left (cwVal -> (CWInteger x)))) =
SBV k (Left (CW k (CWInteger (unsigned w x)))) where
k = KBounded False w
@ -64,9 +69,12 @@ instance SignCast SWord SWord where
k = KBounded False w
y st = do xsw <- sbvToSW st x
newExpr st k (SBVApp (Extract (intSizeOf x-1) 0) [xsw])
unsignCast _ = panic "Cryptol.Symbolic.BitVector"
[ "unsignCast called on non-bitvector value" ]
instance Num BitVector where
fromInteger n = error $ "fromInteger " ++ show n ++ " :: BitVector"
fromInteger n = panic "Cryptol.Symbolic.BitVector"
[ "fromInteger " ++ show n ++ " :: BitVector" ]
BV s m x + BV _ n y = sbv s (same m n) (x + y)
BV s m x - BV _ n y = sbv s (same m n) (x - y)
BV s m x * BV _ n y = sbv s (same m n) (x * y)
@ -82,7 +90,8 @@ instance Bits BitVector where
shift (BV s m x) i = sbv s m (shift x i)
rotate (BV s m x) i = sbv s m (shift x j .|. shift x (j - m))
where j = i `mod` m
bit _i = error "bit: can't determine width"
bit _i = panic "Cryptol.Symbolic.BitVector"
[ "bit: can't determine width" ]
setBit (BV s m x) i = BV s m (setBit x i)
clearBit (BV s m x) i = BV s m (clearBit x i)
complementBit (BV s m x) i = BV s m (complementBit x i)
@ -103,8 +112,10 @@ instance SymWord BitVector where
literal (BV s w x) = SBV k (Left (mkConstCW k x))
where k = KBounded s w
fromCW c@(CW (KBounded s w) _) = BV s w (fromCW c)
fromCW c = error $ "fromCW: Unsupported non-integral value: " ++ show c
mkSymWord _ _ = error "mkSymWord unimplemented for type BitVector"
fromCW c = panic "Cryptol.Symbolic.BitVector"
[ "fromCW: Unsupported non-integral value: " ++ show c ]
mkSymWord _ _ = panic "Cryptol.Symbolic.BitVector"
[ "mkSymWord unimplemented for type BitVector" ]
instance SIntegral BitVector where
@ -132,12 +143,13 @@ extract i j x@(SBV (KBounded s _) _) =
SBV _ (Left cw) ->
case cw of
CW _ (CWInteger v) -> SBV k (Left (normCW (CW k (CWInteger (v `shiftR` j)))))
_ -> error "extract"
_ -> panic "Cryptol.Symbolic.BitVector.extract" [ "non-integer concrete word" ]
_ -> SBV k (Right (cache y))
where y st = do sw <- sbvToSW st x
newExpr st k (SBVApp (Extract i j) [sw])
where
k = KBounded s (i - j + 1)
extract _ _ _ = panic "Cryptol.Symbolic.BitVector.extract" [ "non-bitvector value" ]
cat :: SWord -> SWord -> SWord
cat x y | bitSize x == 0 = y
@ -146,7 +158,7 @@ cat x@(SBV _ (Left a)) y@(SBV _ (Left b)) =
case (a, b) of
(CW _ (CWInteger m), CW _ (CWInteger n)) ->
SBV k (Left (CW k (CWInteger ((m `shiftL` (bitSize y) .|. n)))))
_ -> error "cat"
_ -> panic "Cryptol.Symbolic.BitVector.cat" [ "non-integer concrete word" ]
where k = KBounded False (bitSize x + bitSize y)
cat x y = SBV k (Right (cache z))
where k = KBounded False (bitSize x + bitSize y)

26
src/Cryptol/Symbolic/Prims.hs
View File

@ -20,6 +20,7 @@ import Cryptol.Symbolic.BitVector
import Cryptol.Symbolic.Value
import Cryptol.TypeCheck.AST (Name)
import Cryptol.TypeCheck.Solver.InfNat(Nat'(..), nMul)
import Cryptol.Utils.Panic
import qualified Data.SBV as SBV
import Data.SBV (SBool)
@ -280,7 +281,8 @@ evalECon econ =
zs = take (fromInteger j) (snd (Poly.mdp (reverse xs) (reverse ys)) ++ repeat SBV.false)
in VSeq True (map VBit (reverse zs))
ECRandom -> error "ECRandom"
ECRandom -> panic "Cryptol.Symbolic.Prims.evalECon"
[ "can't symbolically evaluae ECRandom" ]
selectV :: (Integer -> Value) -> Value -> Value
@ -318,14 +320,14 @@ mapV f v =
case v of
VSeq b xs -> VSeq b (map f xs)
VStream xs -> VStream (map f xs)
_ -> error "mapV"
_ -> panic "Cryptol.Symbolic.Prims.mapV" [ "non-mappable value" ]
catV :: Value -> Value -> Value
catV (VWord x) ys = VWord (cat x (fromWord ys))
catV xs (VWord y) = VWord (cat (fromWord xs) y)
catV (VSeq b xs) (VSeq _ ys) = VSeq b (xs ++ ys)
catV (VSeq _ xs) (VStream ys) = VStream (xs ++ ys)
catV _ _ = error "catV"
catV _ _ = panic "Cryptol.Symbolic.Prims.catV" [ "non-concatenable value" ]
dropV :: Integer -> Value -> Value
dropV 0 xs = xs
@ -334,7 +336,7 @@ dropV n xs =
VSeq b xs' -> VSeq b (genericDrop n xs')
VStream xs' -> VStream (genericDrop n xs')
VWord w -> VWord $ extract (bitSize w - 1 - fromInteger n) 0 w
_ -> error "dropV"
_ -> panic "Cryptol.Symbolic.Prims.dropV" [ "non-droppable value" ]
takeV :: Integer -> Value -> Value
takeV n xs =
@ -344,7 +346,7 @@ takeV n xs =
VStream xs' -> VSeq b (genericTake n xs')
where b = case xs' of VBit _ : _ -> True
_ -> False
_ -> error "takeV"
_ -> panic "Cryptol.Symbolic.Prims.takeV" [ "non-takeable value" ]
-- | Make a numeric constant.
-- { val, bits } (fin val, fin bits, bits >= width val) => [bits]
@ -379,7 +381,7 @@ toTypeVal ty
| Just (aty, bty) <- isTFun ty = TVFun (toTypeVal aty) (toTypeVal bty)
| Just (_, tys) <- isTTuple ty = TVTuple (map toTypeVal tys)
| Just fields <- isTRec ty = TVRecord [ (n, toTypeVal aty) | (n, aty) <- fields ]
| otherwise = error "internal error: bad TValue"
| otherwise = panic "Cryptol.Symbolic.Prims.toTypeVal" [ "bad TValue" ]
-- Arith -----------------------------------------------------------------------
@ -443,12 +445,16 @@ cmpValue fb fw = cmp
(VBit b1 , VBit b2 ) -> fb b1 b2 k
(VWord w1 , VWord w2 ) -> fw w1 w2 k
(VSeq _ vs1 , VSeq _ vs2 ) -> cmpValues vs1 vs2 k
(VStream {} , VStream {} ) -> error "Infinite streams are not comparable"
(VFun {} , VFun {} ) -> error "Functions are not comparable"
(VPoly {} , VPoly {} ) -> error "Polymorphic values are not comparable"
(VStream {} , VStream {} ) -> panic "Cryptol.Symbolic.Prims.cmpValue"
[ "Infinite streams are not comparable" ]
(VFun {} , VFun {} ) -> panic "Cryptol.Symbolic.Prims.cmpValue"
[ "Functions are not comparable" ]
(VPoly {} , VPoly {} ) -> panic "Cryptol.Symbolic.Prims.cmpValue"
[ "Polymorphic values are not comparable" ]
(VWord w1 , _ ) -> fw w1 (fromWord v2) k
(_ , VWord w2 ) -> fw (fromWord v1) w2 k
(_ , _ ) -> error "type mismatch"
(_ , _ ) -> panic "Cryptol.Symbolic.Prims.cmpValue"
[ "type mismatch" ]
cmpValues (x1 : xs1) (x2 : xs2) k = cmp x1 x2 (cmpValues xs1 xs2 k)
cmpValues _ _ k = k

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

@ -49,11 +49,13 @@ instance Mergeable Value where
(VPoly f1 , VPoly f2 ) -> VPoly $ symbolicMerge c f1 f2
(VWord w1 , _ ) -> VWord $ symbolicMerge c w1 (fromWord v2)
(_ , VWord w2 ) -> VWord $ symbolicMerge c (fromWord v1) w2
(_ , _ ) -> error "symbolicMerge: incompatible values"
(_ , _ ) -> panic "Cryptol.Symbolic.Value"
[ "symbolicMerge: incompatible values" ]
where
mergeField (n1, x1) (n2, x2)
| n1 == n2 = (n1, symbolicMerge c x1 x2)
| otherwise = error "symbolicMerge: incompatible values"
| otherwise = panic "Cryptol.Symbolic.Value"
[ "symbolicMerge.mergeField: incompatible values" ]
-- Big-endian Words ------------------------------------------------------------

8
src/Cryptol/TypeCheck/Solver/CrySAT.hs
View File

@ -29,7 +29,7 @@ import Data.Either (partitionEithers)
import MonadLib
import Control.Applicative
-- import Cryptol.Utils.Debug
import Cryptol.Utils.Panic
infixr 2 :||
infixr 3 :&&
@ -495,7 +495,8 @@ mkLin :: Expr -> FM SAT.Expr
mkLin ty0 =
cryNoInf ty0 >>= \ty ->
case ty of
K Inf -> error "mkLin: Inf"
K Inf -> panic "Cryptol.TypeCheck.Solver.CrySAT.mkLin"
[ "K Inf after cryNoInf" ]
K (Nat n) -> return (SAT.K n)
Var x -> isFin x >> return (satVar x)
t1 :+ t2 -> (SAT.:+) <$> mkLin t1 <*> mkLin t2
@ -620,7 +621,8 @@ nLg2 0 = 0
nLg2 n = case genLog n 2 of
Just (x,exact) | exact -> x
| otherwise -> x + 1
Nothing -> error "genLog returned Nothing"
Nothing -> panic "Cryptol.TypeCheck.Solver.CrySAT.nLg2"
[ "genLog returned Nothing" ]

8
src/Cryptol/TypeCheck/Solver/InfNat.hs
View File

@ -12,6 +12,8 @@
{-# LANGUAGE Safe #-}
module Cryptol.TypeCheck.Solver.InfNat where
import Cryptol.Utils.Panic
-- | Natural numbers with an infinity element
data Nat' = Nat Integer | Inf
deriving (Show,Eq,Ord)
@ -109,7 +111,8 @@ nLg2 (Nat 0) = Nat 0
nLg2 (Nat n) = case genLog n 2 of
Just (x,exact) | exact -> Nat x
| otherwise -> Nat (x + 1)
Nothing -> error "genLog returned Nothing"
Nothing -> panic "Cryptol.TypeCheck.Solver.InfNat.nLg2"
[ "genLog returned Nothing" ]
-- | @nWidth n@ is number of bits needed to represent all numbers
-- from 0 to n, inclusive. @nWidth x = nLg2 (x + 1)@.
@ -118,7 +121,8 @@ nWidth Inf = Inf
nWidth (Nat 0) = Nat 0
nWidth (Nat n) = case genLog n 2 of
Just (x,_) -> Nat (x + 1)
Nothing -> error "genLog returned Nothing"
Nothing -> panic "Cryptol.TypeCheck.Solver.InfNat.nWidth"
[ "genLog returned Nothing" ]
nLenFromThen :: Nat' -> Nat' -> Nat' -> Maybe Nat'

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

@ -16,6 +16,8 @@ module Cryptol.TypeCheck.TypeOf
import Cryptol.TypeCheck.AST
import Cryptol.TypeCheck.Subst
import Cryptol.Prims.Types (typeOf)
import Cryptol.Utils.Panic
import Cryptol.Utils.PP
import Data.Map (Map)
import qualified Data.Map as Map
@ -37,7 +39,8 @@ fastTypeOf tyenv expr =
EAbs x t e -> tFun t (fastTypeOf (Map.insert x (Forall [] [] t) tyenv) e)
EApp e _ -> case tIsFun (fastTypeOf tyenv e) of
Just (_, t) -> t
Nothing -> error "internal error"
Nothing -> panic "Cryptol.TypeCheck.TypeOf.fastTypeOf"
[ "EApp with non-function operator" ]
ECast _ t -> t
-- Polymorphic fragment
ECon {} -> polymorphic
@ -51,7 +54,8 @@ fastTypeOf tyenv expr =
polymorphic =
case fastSchemaOf tyenv expr of
Forall [] [] ty -> ty
_ -> error "internal error: unexpected polymorphic type"
_ -> panic "Cryptol.TypeCheck.TypeOf.fastTypeOf"
[ "unexpected polymorphic type" ]
fastSchemaOf :: Map QName Schema -> Expr -> Schema
fastSchemaOf tyenv expr =
@ -64,13 +68,18 @@ fastSchemaOf tyenv expr =
ETApp e t -> case fastSchemaOf tyenv e of
Forall (tparam : tparams) props ty -> Forall tparams (apSubst s props) (apSubst s ty)
where s = singleSubst (tpVar tparam) t
_ -> error "internal error"
_ -> panic "Cryptol.TypeCheck.TypeOf.fastSchemaOf"
[ "ETApp body with no type parameters" ]
EProofAbs p e -> case fastSchemaOf tyenv e of
Forall [] props ty -> Forall [] (p : props) ty
_ -> error "internal error"
_ -> panic "Cryptol.TypeCheck.TypeOf.fastSchemaOf"
[ "EProofAbs with polymorphic expression" ]
EProofApp e -> case fastSchemaOf tyenv e of
Forall [] (_ : props) ty -> Forall [] props ty
_ -> error "internal error"
_ -> panic "Cryptol.TypeCheck.TypeOf.fastSchemaOf"
[ "EProofApp with polymorphic expression or"
, "no props in scope"
]
EWhere e dgs -> fastSchemaOf (foldr addDeclGroup tyenv dgs) e
where addDeclGroup (Recursive ds) = flip (foldr addDecl) ds
addDeclGroup (NonRecursive d) = addDecl d
@ -93,4 +102,5 @@ typeSelect :: Type -> Selector -> Type
typeSelect (TCon _tctuple ts) (TupleSel i _) = ts !! (i - 1)
typeSelect (TRec fields) (RecordSel n _) = fromJust (lookup n fields)
typeSelect (TCon _tcseq [_, a]) (ListSel _ _) = a
typeSelect _ _ = error "internal error: typeSelect"
typeSelect ty _ = panic "Cryptol.TypeCheck.TypeOf.typeSelect"
[ "cannot apply selector to value of type", render (pp ty) ]