From fbbbb8f56f57d97ff85cfae748c529343c01da44 Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Mon, 1 Jul 2024 04:13:36 -0700 Subject: [PATCH] Check for syntactically invalid constraint guards in the parser (#1686) Numeric constraint guards have very particular syntactic requirements: * They must always be used in top-level definitions. * Their definitions must always be accompanied by a top-level type signature. Previously, we checked these requirements in a combination of places in the parser and the typechecker. The checks in the typechecker weren't very thorough, however, and they failed to catch local definitions without type signatures that use constraint guards, as seen in #1685. This patch moves all of these syntactic checks to the parser (in `Cryptol.Parser.ExpandPropGuards`). We now recurse into expressions to check for local definition that use constraint guards and error if we encounter one. This ensures that by the time we reach the typechecker, all constraint guard expressions are at least syntactically valid. Fixes #1685. --- CHANGES.md | 7 + src/Cryptol/Parser/ExpandPropGuards.hs | 160 +++++++++++++++++- src/Cryptol/TypeCheck/Error.hs | 25 --- src/Cryptol/TypeCheck/Infer.hs | 39 +---- tests/constraint-guards/noNested.icry.stdout | 2 +- tests/constraint-guards/noTypeSig.cry | 1 + tests/constraint-guards/noTypeSig.icry | 1 + tests/constraint-guards/noTypeSig.icry.stdout | 7 + tests/constraint-guards/noTypeSigNested.cry | 5 + tests/constraint-guards/noTypeSigNested.icry | 1 + .../noTypeSigNested.icry.stdout | 7 + 11 files changed, 186 insertions(+), 69 deletions(-) create mode 100644 tests/constraint-guards/noTypeSig.cry create mode 100644 tests/constraint-guards/noTypeSig.icry create mode 100644 tests/constraint-guards/noTypeSig.icry.stdout create mode 100644 tests/constraint-guards/noTypeSigNested.cry create mode 100644 tests/constraint-guards/noTypeSigNested.icry create mode 100644 tests/constraint-guards/noTypeSigNested.icry.stdout diff --git a/CHANGES.md b/CHANGES.md index 0903a0a04..c6252000f 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -1,3 +1,10 @@ +# next -- TBA + +## Bug fixes + +* Fix #1685, which caused Cryptol to panic when given a local definition without + a type signature that uses numeric constraint guards. + # 3.1.0 -- 2024-02-05 ## Language changes diff --git a/src/Cryptol/Parser/ExpandPropGuards.hs b/src/Cryptol/Parser/ExpandPropGuards.hs index 5ae1fdad2..79b9b6ddf 100644 --- a/src/Cryptol/Parser/ExpandPropGuards.hs +++ b/src/Cryptol/Parser/ExpandPropGuards.hs @@ -22,6 +22,7 @@ import Control.DeepSeq import Cryptol.Parser.AST import Cryptol.Utils.PP import Cryptol.Utils.Panic (panic) +import Data.Foldable (traverse_) import Data.Text (pack) import GHC.Generics (Generic) @@ -31,15 +32,35 @@ type ExpandPropGuardsM a = Either Error a runExpandPropGuardsM :: ExpandPropGuardsM a -> Either Error a runExpandPropGuardsM m = m --- | Error +-- | Errors that can happen while expanding constraint guards. data Error = NoSignature (Located PName) + -- ^ A declaration using constraints guard lacks an explicit type + -- signature, which is a requirement. + | NestedConstraintGuard (Located PName) + -- ^ Constraint guards appear somewhere other than the top level, + -- which is not allowed. deriving (Show, Generic, NFData) instance PP Error where ppPrec _ err = case err of NoSignature x -> - text "At" <+> pp (srcRange x) <.> colon - <+> text "Declarations using constraint guards require an explicit type signature." + hang + (text "At" <+> pp (srcRange x) <.> colon) + 2 + (vcat [ text "Declaration" <+> backticks (pp (thing x)) <+> + text "lacks a type signature." + , text "Declarations using constraint guards require an" <+> + text "explicit type signature." + ]) + NestedConstraintGuard x -> + hang + (text "At" <+> pp (srcRange x) <.> colon) + 2 + (vcat [ text "Local declaration" <+> backticks (pp (thing x)) <+> + text "may not use constraint guards." + , text "Constraint guards may only appear at the top-level of" <+> + text "a module." + ]) expandPropGuards :: ModuleG mname PName -> ExpandPropGuardsM (ModuleG mname PName) expandPropGuards m = @@ -69,16 +90,23 @@ expandTopDecl topDecl = expandDecl :: Decl PName -> ExpandPropGuardsM [Decl PName] expandDecl decl = case decl of - DBind bind -> do bs <- expandBind bind - pure (map DBind bs) - _ -> pure [decl] + DBind bind -> + do bs <- expandBind bind + pure (map DBind bs) + DLocated d rng -> + do ds <- expandDecl d + pure $ map (`DLocated` rng) ds + _ -> + pure [decl] expandBind :: Bind PName -> ExpandPropGuardsM [Bind PName] expandBind bind = case thing (bDef bind) of DImpl (DPropGuards guards) -> expand (DImpl . DPropGuards) guards DForeign (Just (DPropGuards guards)) -> expand (DForeign . Just . DPropGuards) guards - _ -> pure [bind] + _ -> + do checkNestedGuardsInBind bind + pure [bind] where expand def guards = do @@ -90,6 +118,7 @@ expandBind bind = PropGuardCase PName -> ExpandPropGuardsM (PropGuardCase PName, Bind PName) goGuard (PropGuardCase props' e) = do + checkNestedGuardsInExpr e bName' <- newName (bName bind) (thing <$> props') -- call to generated function tParams <- case bSignature bind of @@ -117,6 +146,123 @@ expandBind bind = bind {bDef = def guards' <$ bDef bind} : binds' +-- | Check for nested uses of constraint guards in an expression (e.g., +-- in a local definition bound with @where@). +checkNestedGuardsInExpr :: Expr PName -> ExpandPropGuardsM () +checkNestedGuardsInExpr expr = + case expr of + EVar {} -> + pure () + ELit {} -> + pure () + EGenerate e -> + checkNestedGuardsInExpr e + ETuple es -> + traverse_ checkNestedGuardsInExpr es + ERecord r -> + traverse_ (checkNestedGuardsInExpr . snd) r + ESel e _ -> + checkNestedGuardsInExpr e + EUpd mbE upds -> + do traverse_ checkNestedGuardsInExpr mbE + traverse_ checkNestedGuardsInUpdField upds + EList es -> + traverse_ checkNestedGuardsInExpr es + EFromTo {} -> + pure () + EFromToBy {} -> + pure () + EFromToDownBy {} -> + pure () + EFromToLessThan {} -> + pure () + EInfFrom _ mbE -> + traverse_ checkNestedGuardsInExpr mbE + EComp e mss -> + do checkNestedGuardsInExpr e + traverse_ (traverse_ checkNestedGuardsInMatch) mss + EApp e1 e2 -> + do checkNestedGuardsInExpr e1 + checkNestedGuardsInExpr e2 + EAppT e _ -> + checkNestedGuardsInExpr e + EIf e1 e2 e3 -> + do checkNestedGuardsInExpr e1 + checkNestedGuardsInExpr e2 + checkNestedGuardsInExpr e3 + EWhere e ds -> + do checkNestedGuardsInExpr e + traverse_ checkNestedGuardsInDecl ds + ETyped e _ -> + checkNestedGuardsInExpr e + ETypeVal _ -> + pure () + EFun _ _ e -> + checkNestedGuardsInExpr e + ELocated e _ -> + checkNestedGuardsInExpr e + ESplit e -> + checkNestedGuardsInExpr e + EParens e -> + checkNestedGuardsInExpr e + EInfix e1 _ _ e2 -> + do checkNestedGuardsInExpr e1 + checkNestedGuardsInExpr e2 + EPrefix _ e -> + checkNestedGuardsInExpr e + ECase e ca -> + do checkNestedGuardsInExpr e + traverse_ checkNestedGuardsInCaseAlt ca + where + checkNestedGuardsInUpdField :: UpdField PName -> ExpandPropGuardsM () + checkNestedGuardsInUpdField (UpdField _ _ e) = + checkNestedGuardsInExpr e + + checkNestedGuardsInMatch :: Match PName -> ExpandPropGuardsM () + checkNestedGuardsInMatch match = + case match of + Match _ e -> + checkNestedGuardsInExpr e + MatchLet b -> + checkNestedGuardsInBind b + + checkNestedGuardsInCaseAlt :: CaseAlt PName -> ExpandPropGuardsM () + checkNestedGuardsInCaseAlt (CaseAlt _ e) = + checkNestedGuardsInExpr e + +-- | Check for nested uses of constraint guards in a local declaration. +checkNestedGuardsInDecl :: Decl PName -> ExpandPropGuardsM () +checkNestedGuardsInDecl decl = + case decl of + DSignature {} -> pure () + DPatBind _ e -> checkNestedGuardsInExpr e + DBind b -> checkNestedGuardsInBind b + DRec bs -> traverse_ checkNestedGuardsInBind bs + DFixity {} -> pure () + DPragma {} -> pure () + DType {} -> pure () + DProp {} -> pure () + DLocated d _ -> checkNestedGuardsInDecl d + +-- | Check for nested uses of constraint guards in a local bind. +checkNestedGuardsInBind :: Bind PName -> ExpandPropGuardsM () +checkNestedGuardsInBind bind = + case thing (bDef bind) of + DPrim -> pure () + DImpl bi -> checkNestedGuardsInBindImpl bi + DForeign mbBi -> traverse_ checkNestedGuardsInBindImpl mbBi + where + nestedConstraintGuards :: ExpandPropGuardsM () + nestedConstraintGuards = Left . NestedConstraintGuard $ bName bind + + checkNestedGuardsInBindImpl :: BindImpl PName -> ExpandPropGuardsM () + checkNestedGuardsInBindImpl bi = + case bi of + DPropGuards _ -> + nestedConstraintGuards + DExpr e -> + checkNestedGuardsInExpr e + patternToExpr :: Pattern PName -> Expr PName patternToExpr (PVar locName) = EVar (thing locName) patternToExpr _ = diff --git a/src/Cryptol/TypeCheck/Error.hs b/src/Cryptol/TypeCheck/Error.hs index f3be5a8a1..8b6a94cd1 100644 --- a/src/Cryptol/TypeCheck/Error.hs +++ b/src/Cryptol/TypeCheck/Error.hs @@ -171,13 +171,6 @@ data Error = KindMismatch (Maybe TypeSource) Kind Kind | UnsupportedFFIType TypeSource FFITypeError -- ^ Type is not supported for FFI - | NestedConstraintGuard Ident - -- ^ Constraint guards may only apper at the top-level - - | DeclarationRequiresSignatureCtrGrd Ident - -- ^ All declarataions in a recursive group involving - -- constraint guards should have signatures - | InvalidConstraintGuard Prop -- ^ The given constraint may not be used as a constraint guard @@ -273,8 +266,6 @@ errorImportance err = UnsupportedFFIType {} -> 7 -- less than UnexpectedTypeWildCard - NestedConstraintGuard {} -> 10 - DeclarationRequiresSignatureCtrGrd {} -> 9 InvalidConstraintGuard {} -> 5 @@ -342,8 +333,6 @@ instance TVars Error where UnsupportedFFIKind {} -> err UnsupportedFFIType src e -> UnsupportedFFIType src !$ apSubst su e - NestedConstraintGuard {} -> err - DeclarationRequiresSignatureCtrGrd {} -> err InvalidConstraintGuard p -> InvalidConstraintGuard $! apSubst su p TemporaryError {} -> err @@ -395,8 +384,6 @@ instance FVS Error where UnsupportedFFIKind {} -> Set.empty UnsupportedFFIType _ t -> fvs t - NestedConstraintGuard {} -> Set.empty - DeclarationRequiresSignatureCtrGrd {} -> Set.empty InvalidConstraintGuard p -> fvs p TemporaryError {} -> Set.empty @@ -688,18 +675,6 @@ instance PP (WithNames Error) where [ ppWithNames names t , "When checking" <+> pp src ] - NestedConstraintGuard d -> - vcat [ "Local declaration" <+> backticks (pp d) - <+> "may not use constraint guards." - , "Constraint guards may only appear at the top-level of a module." - ] - - DeclarationRequiresSignatureCtrGrd d -> - vcat [ "The declaration of" <+> backticks (pp d) <+> - "requires a full type signature," - , "because it is part of a recursive group with constraint guards." - ] - InvalidConstraintGuard p -> let d = case tNoUser p of TCon tc _ -> pp tc diff --git a/src/Cryptol/TypeCheck/Infer.hs b/src/Cryptol/TypeCheck/Infer.hs index c4a20272b..63fa440aa 100644 --- a/src/Cryptol/TypeCheck/Infer.hs +++ b/src/Cryptol/TypeCheck/Infer.hs @@ -956,8 +956,6 @@ inferBinds isTopLevel isRec binds = genCs <- generalize bs1 cs return (done,genCs) - checkNumericConstraintGuardsOK isTopLevel sigs noSigs - rec let exprMap = Map.fromList (map monoUse genBs) (doneBs, genBs) <- check exprMap @@ -985,40 +983,6 @@ inferBinds isTopLevel isRec binds = withQs = foldl' appP withTys qs -{- -Here we also check that: - * Numeric constraint guards appear only at the top level - * All definitions in a recursive groups with numberic constraint guards - have signatures - -The reason is to avoid interference between local constraints coming -from the guards and type inference. It might be possible to -relex these requirements, but this requires some more careful thought on -the interaction between the two, and the effects on pricniple types. --} -checkNumericConstraintGuardsOK :: - Bool -> [P.Bind Name] -> [P.Bind Name] -> InferM () -checkNumericConstraintGuardsOK isTopLevel haveSig noSig = - do unless isTopLevel - (mapM_ (mkErr NestedConstraintGuard) withGuards) - unless (null withGuards) - (mapM_ (mkErr DeclarationRequiresSignatureCtrGrd) noSig) - where - mkErr f b = - do let nm = P.bName b - inRange (srcRange nm) (recordError (f (nameIdent (thing nm)))) - - withGuards = filter hasConstraintGuards haveSig - -- When desugaring constraint guards we check that they have signatures, - -- so no need to look at noSig - - hasConstraintGuards b = - case P.bindImpl b of - Just (P.DPropGuards {}) -> True - _ -> False - - - {- | Come up with a type for recursive calls to a function, and decide how we are going to be checking the binding. Returns: (Name, type or schema, computation to check binding) @@ -1178,6 +1142,9 @@ checkMonoB b t = , dDoc = thing <$> P.bDoc b } + -- The pass in Cryptol.Parser.ExpandPropGuards ensures that by the time + -- we reach this code, all definitions that use constraint guards will + -- have a type signature, so this case should be unreachable. P.DPropGuards _ -> tcPanic "checkMonoB" [ "Used constraint guards without a signature at " diff --git a/tests/constraint-guards/noNested.icry.stdout b/tests/constraint-guards/noNested.icry.stdout index 8def66d58..f9c19b600 100644 --- a/tests/constraint-guards/noNested.icry.stdout +++ b/tests/constraint-guards/noNested.icry.stdout @@ -2,6 +2,6 @@ Loading module Cryptol Loading module Cryptol Loading module Main -[error] at noNested.cry:6:3--6:9: +At noNested.cry:6:3--6:9: Local declaration `nested` may not use constraint guards. Constraint guards may only appear at the top-level of a module. diff --git a/tests/constraint-guards/noTypeSig.cry b/tests/constraint-guards/noTypeSig.cry new file mode 100644 index 000000000..a649b61d4 --- /dev/null +++ b/tests/constraint-guards/noTypeSig.cry @@ -0,0 +1 @@ +f | 0 == 0 => () diff --git a/tests/constraint-guards/noTypeSig.icry b/tests/constraint-guards/noTypeSig.icry new file mode 100644 index 000000000..a6c3d6eae --- /dev/null +++ b/tests/constraint-guards/noTypeSig.icry @@ -0,0 +1 @@ +:load noTypeSig.cry diff --git a/tests/constraint-guards/noTypeSig.icry.stdout b/tests/constraint-guards/noTypeSig.icry.stdout new file mode 100644 index 000000000..fe4755506 --- /dev/null +++ b/tests/constraint-guards/noTypeSig.icry.stdout @@ -0,0 +1,7 @@ +Loading module Cryptol +Loading module Cryptol +Loading module Main + +At noTypeSig.cry:1:1--1:2: + Declaration `f` lacks a type signature. + Declarations using constraint guards require an explicit type signature. diff --git a/tests/constraint-guards/noTypeSigNested.cry b/tests/constraint-guards/noTypeSigNested.cry new file mode 100644 index 000000000..0cbeb9d43 --- /dev/null +++ b/tests/constraint-guards/noTypeSigNested.cry @@ -0,0 +1,5 @@ +// A regression test for #1685. +f : () +f = g + where + g | 0 == 0 => () diff --git a/tests/constraint-guards/noTypeSigNested.icry b/tests/constraint-guards/noTypeSigNested.icry new file mode 100644 index 000000000..6c0a18ebc --- /dev/null +++ b/tests/constraint-guards/noTypeSigNested.icry @@ -0,0 +1 @@ +:load noTypeSigNested.cry diff --git a/tests/constraint-guards/noTypeSigNested.icry.stdout b/tests/constraint-guards/noTypeSigNested.icry.stdout new file mode 100644 index 000000000..95c2462be --- /dev/null +++ b/tests/constraint-guards/noTypeSigNested.icry.stdout @@ -0,0 +1,7 @@ +Loading module Cryptol +Loading module Cryptol +Loading module Main + +At noTypeSigNested.cry:5:5--5:6: + Local declaration `g` may not use constraint guards. + Constraint guards may only appear at the top-level of a module.