From cbeab4b672310d04889dbcff165ebe434b2965c4 Mon Sep 17 00:00:00 2001 From: Sofia Faro Date: Thu, 9 Dec 2021 14:27:15 +0000 Subject: [PATCH] interfaces: Prevent circular and non-closed requirements. (#12073) * interfaces: Prevent circular and non-closed reqs Updates the haskell side to be more strict about requirements: - requirements must be transitively closed, so if A requires B, and B requires C, then A requires C. - no circular requirements allowed The logic for circular requirements is a bit duplicated to get a better error message. Part of https://github.com/digital-asset/daml/issues/11978 changelog_begin changelog_end * Update compiler/daml-lf-tools/src/DA/Daml/LF/TypeChecker/Check.hs Co-authored-by: Moritz Kiefer * take a list in NotClosed error Co-authored-by: Moritz Kiefer --- .../src/DA/Daml/LF/TypeChecker/Check.hs | 49 ++++++++++++------- .../src/DA/Daml/LF/TypeChecker/Error.hs | 13 +++++ .../InterfaceRequiresCircular.daml | 15 ++++++ .../InterfaceRequiresCircularIndirect.daml | 20 ++++++++ .../InterfaceRequiresNotClosed.daml | 22 +++++++++ 5 files changed, 100 insertions(+), 19 deletions(-) create mode 100644 compiler/damlc/tests/daml-test-files/InterfaceRequiresCircular.daml create mode 100644 compiler/damlc/tests/daml-test-files/InterfaceRequiresCircularIndirect.daml create mode 100644 compiler/damlc/tests/daml-test-files/InterfaceRequiresNotClosed.daml diff --git a/compiler/daml-lf-tools/src/DA/Daml/LF/TypeChecker/Check.hs b/compiler/daml-lf-tools/src/DA/Daml/LF/TypeChecker/Check.hs index 13d0224ad4d..d1d45e685c5 100644 --- a/compiler/daml-lf-tools/src/DA/Daml/LF/TypeChecker/Check.hs +++ b/compiler/daml-lf-tools/src/DA/Daml/LF/TypeChecker/Check.hs @@ -43,6 +43,7 @@ import Data.List.Extended import Data.Generics.Uniplate.Data (para) import qualified Data.Set as S import qualified Data.HashSet as HS +import Data.Maybe (listToMaybe) import qualified Data.Map.Strict as Map import qualified Data.NameMap as NM import qualified Data.IntSet as IntSet @@ -828,18 +829,32 @@ checkDefTypeSyn DefTypeSyn{synParams,synType} = do where base = checkType synType KStar + -- | Check that an interface definition is well defined. checkIface :: MonadGamma m => Module -> DefInterface -> m () -checkIface m DefInterface{..} = do - checkUnique (EDuplicateInterfaceChoiceName intName) $ NM.names intFixedChoices - checkUnique (EDuplicateInterfaceMethodName intName) $ NM.names intMethods - forM_ intRequires (inWorld . lookupInterface) -- verify that required interface exists - forM_ intMethods checkIfaceMethod +checkIface m iface = do + let tcon = Qualified PRSelf (moduleName m) (intName iface) - let tcon = Qualified PRSelf (moduleName m) intName - introExprVar intParam (TCon tcon) $ do - forM_ intFixedChoices (checkTemplateChoice tcon) - checkExpr intPrecondition TBool + -- check requires + when (tcon `S.member` intRequires iface) $ + throwWithContext (ECircularInterfaceRequires (intName iface) Nothing) + forM_ (intRequires iface) $ \requiredIfaceId -> do + requiredIface <- inWorld (lookupInterface requiredIfaceId) + when (tcon `S.member` intRequires requiredIface) $ + throwWithContext (ECircularInterfaceRequires (intName iface) (Just requiredIfaceId)) + let missing = intRequires requiredIface `S.difference` intRequires iface + unless (S.null missing) $ throwWithContext $ + ENotClosedInterfaceRequires (intName iface) requiredIfaceId (S.toList missing) + + -- check methods + checkUnique (EDuplicateInterfaceMethodName (intName iface)) $ NM.names (intMethods iface) + forM_ (intMethods iface) checkIfaceMethod + + -- check choices + checkUnique (EDuplicateInterfaceChoiceName (intName iface)) $ NM.names (intFixedChoices iface) + introExprVar (intParam iface) (TCon tcon) $ do + forM_ (intFixedChoices iface) (checkTemplateChoice tcon) + checkExpr (intPrecondition iface) TBool checkIfaceMethod :: MonadGamma m => InterfaceMethod -> m () checkIfaceMethod InterfaceMethod{ifmType} = do @@ -910,10 +925,8 @@ checkIfaceImplementation Template{tplImplements} tplTcon TemplateImplements{..} -- check requires let missingRequires = S.difference intRequires (S.fromList (NM.names tplImplements)) - case S.toList missingRequires of - [] -> pure () - (missingInterface:_) -> - throwWithContext (EMissingRequiredInterface tplName tpiInterface missingInterface) + whenJust (listToMaybe (S.toList missingRequires)) $ \missingInterface -> + throwWithContext (EMissingRequiredInterface tplName tpiInterface missingInterface) -- check fixed choices let inheritedChoices = S.fromList (NM.names intFixedChoices) @@ -922,9 +935,8 @@ checkIfaceImplementation Template{tplImplements} tplTcon TemplateImplements{..} -- check methods let missingMethods = HS.difference (NM.namesSet intMethods) (NM.namesSet tpiMethods) - case HS.toList missingMethods of - [] -> pure () - (methodName:_) -> throwWithContext (EMissingInterfaceMethod tplName tpiInterface methodName) + whenJust (listToMaybe (HS.toList missingMethods)) $ \methodName -> + throwWithContext (EMissingInterfaceMethod tplName tpiInterface methodName) forM_ tpiMethods $ \TemplateImplementsMethod{tpiMethodName, tpiMethodExpr} -> do case NM.lookup tpiMethodName intMethods of Nothing -> throwWithContext (EUnknownInterfaceMethod tplName tpiInterface tpiMethodName) @@ -952,9 +964,8 @@ checkDefException m DefException{..} = do unless (null tyParams) $ throwWithContext (EExpectedExceptionTypeHasNoParams modName exnName) checkExpr exnMessage (TCon tcon :-> TText) _ <- match _DataRecord (EExpectedExceptionTypeIsRecord modName exnName) dataCons - case NM.lookup exnName (moduleTemplates m) of - Nothing -> pure () - Just _ -> throwWithContext (EExpectedExceptionTypeIsNotTemplate modName exnName) + whenJust (NM.lookup exnName (moduleTemplates m)) $ \_ -> + throwWithContext (EExpectedExceptionTypeIsNotTemplate modName exnName) -- NOTE(MH): It is important that the data type definitions are checked first. -- The type checker for expressions relies on the fact that data type diff --git a/compiler/daml-lf-tools/src/DA/Daml/LF/TypeChecker/Error.hs b/compiler/daml-lf-tools/src/DA/Daml/LF/TypeChecker/Error.hs index 56e1bcec1f3..dcc7d8d993a 100644 --- a/compiler/daml-lf-tools/src/DA/Daml/LF/TypeChecker/Error.hs +++ b/compiler/daml-lf-tools/src/DA/Daml/LF/TypeChecker/Error.hs @@ -134,6 +134,8 @@ data Error | EDuplicateInterfaceChoiceName !TypeConName !ChoiceName | EDuplicateInterfaceMethodName !TypeConName !MethodName | EUnknownInterface !TypeConName + | ECircularInterfaceRequires !TypeConName !(Maybe (Qualified TypeConName)) + | ENotClosedInterfaceRequires !TypeConName !(Qualified TypeConName) ![Qualified TypeConName] | EMissingRequiredInterface { emriTemplate :: !TypeConName, emriRequiringInterface :: !(Qualified TypeConName), emriRequiredInterface :: !(Qualified TypeConName) } | EBadInheritedChoices { ebicInterface :: !(Qualified TypeConName), ebicExpected :: ![ChoiceName], ebicGot :: ![ChoiceName] } | EMissingInterfaceChoice !ChoiceName @@ -380,6 +382,17 @@ instance Pretty Error where EDuplicateInterfaceMethodName iface method -> "Duplicate method name '" <> pretty method <> "' in interface definition for " <> pretty iface EUnknownInterface tcon -> "Unknown interface: " <> pretty tcon + ECircularInterfaceRequires iface Nothing -> + "Circular interface requirement is not allowed: interface " <> pretty iface <> " requires itself." + ECircularInterfaceRequires iface (Just otherIface) -> + "Circular interface requirement is not allowed: interface " + <> pretty iface <> " requires " + <> pretty otherIface <> " requires " + <> pretty iface + ENotClosedInterfaceRequires iface ifaceRequired ifaceMissing -> + "Interface " <> pretty iface + <> " is missing requirement " <> pretty ifaceMissing + <> " required by " <> pretty ifaceRequired EMissingRequiredInterface {..} -> "Template " <> pretty emriTemplate <> " is missing an implementation of interface " <> pretty emriRequiredInterface <> diff --git a/compiler/damlc/tests/daml-test-files/InterfaceRequiresCircular.daml b/compiler/damlc/tests/daml-test-files/InterfaceRequiresCircular.daml new file mode 100644 index 00000000000..e903ce98a85 --- /dev/null +++ b/compiler/damlc/tests/daml-test-files/InterfaceRequiresCircular.daml @@ -0,0 +1,15 @@ +-- Copyright (c) 2021 Digital Asset (Switzerland) GmbH and/or its affiliates. All rights reserved. +-- SPDX-License-Identifier: Apache-2.0 + +-- @SINCE-LF-FEATURE DAML_INTERFACE +-- @ERROR Circular interface requirement is not allowed: interface A requires itself. + +-- | Check that an interface cannot require itself. +module InterfaceRequiresCircular where + +interface A where + +-- TODO https://github.com/digital-asset/daml/issues/11978 +-- Implement "requires" syntax. +_requires_A_A : DA.Internal.Desugar.RequiresT A A +_requires_A_A = DA.Internal.Desugar.RequiresT diff --git a/compiler/damlc/tests/daml-test-files/InterfaceRequiresCircularIndirect.daml b/compiler/damlc/tests/daml-test-files/InterfaceRequiresCircularIndirect.daml new file mode 100644 index 00000000000..e32b9641922 --- /dev/null +++ b/compiler/damlc/tests/daml-test-files/InterfaceRequiresCircularIndirect.daml @@ -0,0 +1,20 @@ +-- Copyright (c) 2021 Digital Asset (Switzerland) GmbH and/or its affiliates. All rights reserved. +-- SPDX-License-Identifier: Apache-2.0 + +-- @SINCE-LF-FEATURE DAML_INTERFACE +-- @ERROR Circular interface requirement is not allowed: interface A requires InterfaceRequiresCircularIndirect:B requires A + +-- | Check that an interface cannot require itself indirectly. +module InterfaceRequiresCircularIndirect where + +interface A where + +interface B where + +-- TODO https://github.com/digital-asset/daml/issues/11978 +-- Implement "requires" syntax. +_requires_A_B : DA.Internal.Desugar.RequiresT A B +_requires_A_B = DA.Internal.Desugar.RequiresT + +_requires_B_A : DA.Internal.Desugar.RequiresT B A +_requires_B_A = DA.Internal.Desugar.RequiresT diff --git a/compiler/damlc/tests/daml-test-files/InterfaceRequiresNotClosed.daml b/compiler/damlc/tests/daml-test-files/InterfaceRequiresNotClosed.daml new file mode 100644 index 00000000000..046fa4eff8c --- /dev/null +++ b/compiler/damlc/tests/daml-test-files/InterfaceRequiresNotClosed.daml @@ -0,0 +1,22 @@ +-- Copyright (c) 2021 Digital Asset (Switzerland) GmbH and/or its affiliates. All rights reserved. +-- SPDX-License-Identifier: Apache-2.0 + +-- @SINCE-LF-FEATURE DAML_INTERFACE +-- @ERROR Interface C is missing requirement [InterfaceRequiresNotClosed:A] required by InterfaceRequiresNotClosed:B + +-- | Check that interface requirements are transitively closed. +module InterfaceRequiresNotClosed where + +interface A where + +interface B where + +interface C where + +-- TODO https://github.com/digital-asset/daml/issues/11978 +-- Implement "requires" syntax. +_requires_B_A : DA.Internal.Desugar.RequiresT B A +_requires_B_A = DA.Internal.Desugar.RequiresT + +_requires_C_B : DA.Internal.Desugar.RequiresT C B +_requires_C_B = DA.Internal.Desugar.RequiresT