Skip to content

Commit

Permalink
Add serializability check for interface payloads in Haskell (#12560)
Browse files Browse the repository at this point in the history
* Add serializability check for interface payloads in Haskell

changelog_begin
changelog_end

* .

changelog_begin
changelog_end

* .

changelog_begin
changelog_end

* cleanup

changelog_begin
changelog_end

* .

changelog_begin
changelog_end
  • Loading branch information
cocreature authored Jan 25, 2022
1 parent aced78f commit ce06eb0
Show file tree
Hide file tree
Showing 4 changed files with 44 additions and 9 deletions.
5 changes: 3 additions & 2 deletions compiler/daml-lf-tools/src/DA/Daml/LF/InferSerializability.hs
Original file line number Diff line number Diff line change
Expand Up @@ -12,17 +12,18 @@ import qualified Data.NameMap as NM
import Data.Semigroup.FixedPoint (leastFixedPointBy)

import DA.Daml.LF.Ast
import DA.Daml.LF.TypeChecker.Serializability (serializabilityConditionsDataType)
import DA.Daml.LF.TypeChecker.Serializability (CurrentModule(..), serializabilityConditionsDataType)

inferModule :: World -> Version -> Module -> Either String Module
inferModule world0 version mod0 = do
let modName = moduleName mod0
let dataTypes = moduleDataTypes mod0
let interfaces = NM.namesSet (moduleInterfaces mod0)
let eqs =
[ (dataTypeCon dataType, serializable, deps)
| dataType <- NM.toList dataTypes
, let (serializable, deps) =
case serializabilityConditionsDataType world0 version (Just modName) dataType of
case serializabilityConditionsDataType world0 version (Just $ CurrentModule modName interfaces) dataType of
Left _ -> (False, [])
Right deps0 -> (True, HS.toList deps0)
]
Expand Down
2 changes: 2 additions & 0 deletions compiler/daml-lf-tools/src/DA/Daml/LF/TypeChecker/Error.hs
Original file line number Diff line number Diff line change
Expand Up @@ -76,6 +76,7 @@ data UnserializabilityReason
| URTypeRep -- ^ It contains a value of type TypeRep.
| URTypeSyn -- ^ It contains a type synonym.
| URExperimental -- ^ It contains a experimental type
| URInterface -- ^ It constains an interface

data Error
= EUnknownTypeVar !TypeVarName
Expand Down Expand Up @@ -226,6 +227,7 @@ instance Pretty UnserializabilityReason where
URRoundingMode -> "RoundingMode"
URBigNumeric -> "BigNumeric"
URExperimental -> "experimental type"
URInterface -> "interface"

instance Pretty Error where
pPrint = \case
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -15,6 +15,7 @@
module DA.Daml.LF.TypeChecker.Serializability
( serializabilityConditionsDataType
, checkModule
, CurrentModule(..)
) where

import Control.Lens (matching, toListOf)
Expand All @@ -29,26 +30,37 @@ import DA.Daml.LF.Ast.Optics (_PRSelfModule, dataConsType)
import DA.Daml.LF.TypeChecker.Env
import DA.Daml.LF.TypeChecker.Error

-- This is only used during serializability inference. During typechecking the world
-- contains the current module.
data CurrentModule = CurrentModule
{ modName :: ModuleName
, modInterfaces :: HS.HashSet TypeConName
}

-- | Determine whether a type is serializable. When a module name is given,
-- data types in this module are returned rather than lookup up in the world.
-- If no module name is given, the returned set is always empty.
serializabilityConditionsType
:: World
-> Version
-> Maybe ModuleName
-> Maybe CurrentModule
-- ^ See description on `serializabilityConditionsDataType`.
-> HS.HashSet TypeVarName
-- ^ Type variables that are bound by a surrounding data type definition
-- if any. The check that all of them are of kind '*' must be performed by
-- the caller.
-> Type
-> Either UnserializabilityReason (HS.HashSet TypeConName)
serializabilityConditionsType world0 _version mbModName vars = go
serializabilityConditionsType world0 _version mbCurrentModule vars = go
where
noConditions = Right HS.empty
go = \case
-- This is the only way 'ContractId's, 'List's and 'Optional's are allowed. Other cases handled below.
TContractId typ -> go typ
TContractId typ
-- While an interface payload I is not serializable, ContractId I
-- is so specialcase this here.
| isInterface typ -> noConditions
| otherwise -> go typ
TList typ -> go typ
TOptional typ -> go typ
TTextMap typ -> go typ
Expand All @@ -67,7 +79,7 @@ serializabilityConditionsType world0 _version mbModName vars = go
| otherwise -> Left (URFreeVar v)
TSynApp{} -> Left URTypeSyn
TCon tcon
| Just modName <- mbModName
| Just CurrentModule { modName } <- mbCurrentModule
, Right tconName <- matching (_PRSelfModule modName) tcon ->
Right (HS.singleton tconName)
| isSerializable tcon -> noConditions
Expand Down Expand Up @@ -104,14 +116,23 @@ serializabilityConditionsType world0 _version mbModName vars = go
BTBigNumeric -> Left URBigNumeric
TForall{} -> Left URForall
TStruct{} -> Left URStruct
isInterface (TCon con) = case (lookupDataType con world0, mbCurrentModule) of
(Right t, _) -> case dataCons t of
DataInterface -> True
_ -> False
(Left _, Just currentModule)
| Right tconName <- matching (_PRSelfModule $ modName currentModule) con
-> tconName `HS.member` modInterfaces currentModule
(Left err, _) -> error $ showString "Serializability.serializabilityConditionsDataTyp: " $ show err
isInterface _ = False

-- | Determine whether a data type preserves serializability. When a module
-- name is given, -- data types in this module are returned rather than lookup
-- up in the world. If no module name is given, the returned set is always empty.
serializabilityConditionsDataType
:: World
-> Version
-> Maybe ModuleName
-> Maybe CurrentModule
-- ^ We invoke this function in two different ways: During serializability inference
-- world excludes the current module and this will be `Just`. In that case, any type
-- in the current module becomes a condition.
Expand All @@ -120,15 +141,16 @@ serializabilityConditionsDataType
-- in the current modules is taking from `dataSerializable`.
-> DefDataType
-> Either UnserializabilityReason (HS.HashSet TypeConName)
serializabilityConditionsDataType world0 version mbModName (DefDataType _loc _ _ params cons) =
serializabilityConditionsDataType world0 version mbCurrentModule (DefDataType _loc _ _ params cons) =
case find (\(_, k) -> k /= KStar) params of
Just (v, k) -> Left (URHigherKinded v k)
Nothing
| DataVariant [] <- cons -> Left URUninhabitatedType
| DataEnum [] <- cons -> Left URUninhabitatedType
| DataInterface <- cons -> Left URInterface
| otherwise -> do
let vars = HS.fromList (map fst params)
mconcatMapM (serializabilityConditionsType world0 version mbModName vars) (toListOf dataConsType cons)
mconcatMapM (serializabilityConditionsType world0 version mbCurrentModule vars) (toListOf dataConsType cons)

-- | Check whether a type is serializable.
checkType :: MonadGamma m => SerializabilityRequirement -> Type -> m ()
Expand Down
Original file line number Diff line number Diff line change
@@ -0,0 +1,10 @@
-- @SINCE-LF-FEATURE DAML_INTERFACE
-- @ERROR expected serializable type
module InterfaceSerializabilityPayload where

-- Test that the interface serializability payload itself is not serializable.
interface Gettable where
nonconsuming choice Get : Gettable
with anyActor : Party
controller anyActor
do return this

0 comments on commit ce06eb0

Please sign in to comment.