From 2283de3d963bca08759f5e310d7c9a2949e98a81 Mon Sep 17 00:00:00 2001 From: odersky Date: Wed, 25 Oct 2023 11:00:52 +0200 Subject: [PATCH 1/2] Drop outdated config settings --- .../src/dotty/tools/dotc/cc/CaptureOps.scala | 49 ++----------------- .../src/dotty/tools/dotc/cc/CaptureSet.scala | 3 +- .../src/dotty/tools/dotc/config/Config.scala | 11 ----- .../tools/dotc/core/tasty/TreeUnpickler.scala | 17 ++----- .../core/unpickleScala2/Scala2Unpickler.scala | 4 +- .../tools/dotc/printing/RefinedPrinter.scala | 2 +- 6 files changed, 12 insertions(+), 74 deletions(-) diff --git a/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala b/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala index 68dd0ac0c79a..dccf07ba199e 100644 --- a/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala +++ b/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala @@ -19,11 +19,11 @@ private val Captures: Key[CaptureSet] = Key() object ccConfig: - /** Switch whether unpickled function types and byname types should be mapped to - * impure types. With the new gradual typing using Fluid capture sets, this should - * be no longer needed. Also, it has bad interactions with pickling tests. + /** If true, allow mappping capture set variables under captureChecking with maps that are neither + * bijective nor idempotent. We currently do now know how to do this correctly in all + * cases, though. */ - private[cc] val adaptUnpickledFunctionTypes = false + inline val allowUnsoundMaps = false /** If true, use `sealed` as encapsulation mechanism instead of the * previous global retriction that `cap` can't be boxed or unboxed. @@ -48,7 +48,7 @@ def isCaptureCheckingOrSetup(using Context): Boolean = */ def depFun(args: List[Type], resultType: Type, isContextual: Boolean, paramNames: List[TermName] = Nil)(using Context): Type = val make = MethodType.companion(isContextual = isContextual) - val mt = + val mt = if paramNames.length == args.length then make(paramNames, args, resultType) else make(args, resultType) mt.toFunctionType(alwaysDependent = true) @@ -106,22 +106,6 @@ extension (tree: Tree) case Apply(_, Typed(SeqLiteral(elems, _), _) :: Nil) => elems case _ => Nil - /** Under pureFunctions, add a @retainsByName(*)` annotation to the argument of - * a by name parameter type, turning the latter into an impure by name parameter type. - */ - def adaptByNameArgUnderPureFuns(using Context): Tree = - if ccConfig.adaptUnpickledFunctionTypes && Feature.pureFunsEnabledSomewhere then - val rbn = defn.RetainsByNameAnnot - Annotated(tree, - New(rbn.typeRef).select(rbn.primaryConstructor).appliedTo( - Typed( - SeqLiteral(ref(defn.captureRoot) :: Nil, TypeTree(defn.AnyType)), - TypeTree(defn.RepeatedParamType.appliedTo(defn.AnyType)) - ) - ) - ) - else tree - extension (tp: Type) /** @pre `tp` is a CapturingType */ @@ -199,29 +183,6 @@ extension (tp: Type) case _ => tp - /** Under pureFunctions, map regular function type to impure function type - */ - def adaptFunctionTypeUnderPureFuns(using Context): Type = tp match - case AppliedType(fn, args) - if ccConfig.adaptUnpickledFunctionTypes && Feature.pureFunsEnabledSomewhere && defn.isFunctionClass(fn.typeSymbol) => - val fname = fn.typeSymbol.name - defn.FunctionType( - fname.functionArity, - isContextual = fname.isContextFunction, - isImpure = true).appliedTo(args) - case _ => - tp - - /** Under pureFunctions, add a @retainsByName(*)` annotation to the argument of - * a by name parameter type, turning the latter into an impure by name parameter type. - */ - def adaptByNameArgUnderPureFuns(using Context): Type = - if ccConfig.adaptUnpickledFunctionTypes && Feature.pureFunsEnabledSomewhere then - AnnotatedType(tp, - CaptureAnnotation(CaptureSet.universal, boxed = false)(defn.RetainsByNameAnnot)) - else - tp - /** Is type known to be always pure by its class structure, * so that adding a capture set to it would not make sense? */ diff --git a/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala b/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala index a08230c6a198..6a0b8c6e55ed 100644 --- a/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala +++ b/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala @@ -16,7 +16,6 @@ import util.{SimpleIdentitySet, Property} import typer.ErrorReporting.Addenda import util.common.alwaysTrue import scala.collection.mutable -import config.Config.ccAllowUnsoundMaps /** A class for capture sets. Capture sets can be constants or variables. * Capture sets support inclusion constraints <:< where <:< is subcapturing. @@ -667,7 +666,7 @@ object CaptureSet: private def mapIsIdempotent = tm.isInstanceOf[IdempotentCaptRefMap] - assert(ccAllowUnsoundMaps || mapIsIdempotent, tm.getClass) + assert(ccConfig.allowUnsoundMaps || mapIsIdempotent, tm.getClass) private def whereCreated(using Context): String = if stack == null then "" diff --git a/compiler/src/dotty/tools/dotc/config/Config.scala b/compiler/src/dotty/tools/dotc/config/Config.scala index 247fa28efbda..2746476261e5 100644 --- a/compiler/src/dotty/tools/dotc/config/Config.scala +++ b/compiler/src/dotty/tools/dotc/config/Config.scala @@ -235,15 +235,4 @@ object Config { */ inline val checkLevelsOnConstraints = false inline val checkLevelsOnInstantiation = true - - /** If true, print capturing types in the form `{c} T`. - * If false, print them in the form `T @retains(c)`. - */ - inline val printCaptureSetsAsPrefix = true - - /** If true, allow mappping capture set variables under captureChecking with maps that are neither - * bijective nor idempotent. We currently do now know how to do this correctly in all - * cases, though. - */ - inline val ccAllowUnsoundMaps = false } diff --git a/compiler/src/dotty/tools/dotc/core/tasty/TreeUnpickler.scala b/compiler/src/dotty/tools/dotc/core/tasty/TreeUnpickler.scala index 7c0f1ac5518b..1748b1edd08e 100644 --- a/compiler/src/dotty/tools/dotc/core/tasty/TreeUnpickler.scala +++ b/compiler/src/dotty/tools/dotc/core/tasty/TreeUnpickler.scala @@ -32,7 +32,6 @@ import ast.{Trees, tpd, untpd} import Trees._ import Decorators._ import transform.SymUtils._ -import cc.{adaptFunctionTypeUnderPureFuns, adaptByNameArgUnderPureFuns} import dotty.tools.dotc.quoted.QuotePatterns import dotty.tools.tasty.{TastyBuffer, TastyReader} @@ -383,7 +382,7 @@ class TreeUnpickler(reader: TastyReader, // Note that the lambda "rt => ..." is not equivalent to a wildcard closure! // Eta expansion of the latter puts readType() out of the expression. case APPLIEDtype => - postProcessFunction(readType().appliedTo(until(end)(readType()))) + readType().appliedTo(until(end)(readType())) case TYPEBOUNDS => val lo = readType() if nothingButMods(end) then @@ -460,8 +459,7 @@ class TreeUnpickler(reader: TastyReader, val ref = readAddr() typeAtAddr.getOrElseUpdate(ref, forkAt(ref).readType()) case BYNAMEtype => - val arg = readType() - ExprType(if withPureFuns then arg else arg.adaptByNameArgUnderPureFuns) + ExprType(readType()) case _ => ConstantType(readConstant(tag)) } @@ -495,12 +493,6 @@ class TreeUnpickler(reader: TastyReader, def readTreeRef()(using Context): TermRef = readType().asInstanceOf[TermRef] - /** Under pureFunctions, map all function types to impure function types, - * unless the unpickled class was also compiled with pureFunctions. - */ - private def postProcessFunction(tp: Type)(using Context): Type = - if withPureFuns then tp else tp.adaptFunctionTypeUnderPureFuns - // ------ Reading definitions ----------------------------------------------------- private def nothingButMods(end: Addr): Boolean = @@ -1240,8 +1232,7 @@ class TreeUnpickler(reader: TastyReader, case SINGLETONtpt => SingletonTypeTree(readTree()) case BYNAMEtpt => - val arg = readTpt() - ByNameTypeTree(if withPureFuns then arg else arg.adaptByNameArgUnderPureFuns) + ByNameTypeTree(readTpt()) case NAMEDARG => NamedArg(readName(), readTree()) case EXPLICITtpt => @@ -1453,7 +1444,7 @@ class TreeUnpickler(reader: TastyReader, val args = until(end)(readTpt()) val tree = untpd.AppliedTypeTree(tycon, args) val ownType = ctx.typeAssigner.processAppliedType(tree, tycon.tpe.safeAppliedTo(args.tpes)) - tree.withType(postProcessFunction(ownType)) + tree.withType(ownType) case ANNOTATEDtpt => Annotated(readTpt(), readTree()) case LAMBDAtpt => diff --git a/compiler/src/dotty/tools/dotc/core/unpickleScala2/Scala2Unpickler.scala b/compiler/src/dotty/tools/dotc/core/unpickleScala2/Scala2Unpickler.scala index a2bba7e708b2..3e211e75b73b 100644 --- a/compiler/src/dotty/tools/dotc/core/unpickleScala2/Scala2Unpickler.scala +++ b/compiler/src/dotty/tools/dotc/core/unpickleScala2/Scala2Unpickler.scala @@ -33,7 +33,6 @@ import scala.collection.mutable import scala.collection.mutable.ListBuffer import scala.annotation.switch import reporting._ -import cc.{adaptFunctionTypeUnderPureFuns, adaptByNameArgUnderPureFuns} object Scala2Unpickler { @@ -824,7 +823,7 @@ class Scala2Unpickler(bytes: Array[Byte], classRoot: ClassDenotation, moduleClas } val tycon = select(pre, sym) val args = until(end, () => readTypeRef()) - if (sym == defn.ByNameParamClass2x) ExprType(args.head.adaptByNameArgUnderPureFuns) + if (sym == defn.ByNameParamClass2x) ExprType(args.head) else if (ctx.settings.scalajs.value && args.length == 2 && sym.owner == JSDefinitions.jsdefn.ScalaJSJSPackageClass && sym == JSDefinitions.jsdefn.PseudoUnionClass) { // Treat Scala.js pseudo-unions as real unions, this requires a @@ -833,7 +832,6 @@ class Scala2Unpickler(bytes: Array[Byte], classRoot: ClassDenotation, moduleClas } else if args.nonEmpty then tycon.safeAppliedTo(EtaExpandIfHK(sym.typeParams, args.map(translateTempPoly))) - .adaptFunctionTypeUnderPureFuns else if (sym.typeParams.nonEmpty) tycon.EtaExpand(sym.typeParams) else tycon case TYPEBOUNDStpe => diff --git a/compiler/src/dotty/tools/dotc/printing/RefinedPrinter.scala b/compiler/src/dotty/tools/dotc/printing/RefinedPrinter.scala index 4f63bfb38691..ede3900167e0 100644 --- a/compiler/src/dotty/tools/dotc/printing/RefinedPrinter.scala +++ b/compiler/src/dotty/tools/dotc/printing/RefinedPrinter.scala @@ -640,7 +640,7 @@ class RefinedPrinter(_ctx: Context) extends PlainPrinter(_ctx) { try changePrec(GlobalPrec)(toText(arg) ~ "^" ~ toTextCaptureSet(captureSet)) catch case ex: IllegalCaptureRef => toTextAnnot if annot.symbol.maybeOwner == defn.RetainsAnnot - && Feature.ccEnabled && Config.printCaptureSetsAsPrefix && !printDebug + && Feature.ccEnabled && !printDebug then toTextRetainsAnnot else toTextAnnot case EmptyTree => From 468955b7f6f61e9bd4b287b739c82dfcfacc216c Mon Sep 17 00:00:00 2001 From: odersky Date: Wed, 25 Oct 2023 12:06:09 +0200 Subject: [PATCH 2/2] Fix potential soundness hole when adding references to a mapped set Fix soundness hole when adding references to a set that is the image of an idempotent `tm` map `tm`. If the element `ref` did not come from the source of the set, we still assumed that `tm(ref) = ref`, so that we simply added the reference to the set and also back-propagated it to source. But that is not necessarily the case (although it is the case in our complete test suite, so I am not sure this case can actually arise in practice. Nevertheless, it's better to not leave a potential soundness hole here. In the new implementation, we test whether `tm(ref) = ref`, and only proceed as before if that's the case. If not there are two sub-cases: - `{ref} <:< tm(ref)` and the variance of the set is positive. In that case we can soundly add `tm(ref)` to the set while back-propagating `ref` as before. - Otherwise there's nothing obvious left to do except fail (which is always sound. --- .../src/dotty/tools/dotc/cc/CaptureSet.scala | 40 +++++++++++++++++-- 1 file changed, 37 insertions(+), 3 deletions(-) diff --git a/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala b/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala index 6a0b8c6e55ed..2586d449dfd4 100644 --- a/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala +++ b/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala @@ -682,7 +682,9 @@ object CaptureSet: // `r` is _one_ possible solution in `source` that would make an `r` appear in this set. // It's not necessarily the only possible solution, so the scheme is incomplete. source.tryInclude(elem, this) - else if !mapIsIdempotent && variance <= 0 && !origin.isConst && (origin ne initial) && (origin ne source) then + else if ccConfig.allowUnsoundMaps && !mapIsIdempotent + && variance <= 0 && !origin.isConst && (origin ne initial) && (origin ne source) + then // The map is neither a BiTypeMap nor an idempotent type map. // In that case there's no much we can do. // The scheme then does not propagate added elements back to source and rejects adding @@ -696,8 +698,11 @@ object CaptureSet: def propagateIf(cond: Boolean): CompareResult = if cond then propagate else CompareResult.OK - if origin eq source then // elements have to be mapped - val mapped = extrapolateCaptureRef(elem, tm, variance) + val mapped = extrapolateCaptureRef(elem, tm, variance) + def isFixpoint = + mapped.isConst && mapped.elems.size == 1 && mapped.elems.contains(elem) + + def addMapped = val added = mapped.elems.filter(!accountsFor(_)) addNewElems(added) .andAlso: @@ -706,6 +711,35 @@ object CaptureSet: else CompareResult.Fail(this :: Nil) .andAlso: propagateIf(!added.isEmpty) + + def failNoFixpoint = + val reason = + if variance <= 0 then i"the set's variance is $variance" + else i"$elem gets mapped to $mapped, which is not a supercapture." + report.warning(em"""trying to add $elem from unrecognized source $origin of mapped set $this$whereCreated + |The reference cannot be added since $reason""") + CompareResult.Fail(this :: Nil) + + if origin eq source then // elements have to be mapped + addMapped + .andAlso: + if mapped.isConst then CompareResult.OK + else if mapped.asVar.recordDepsState() then { addAsDependentTo(mapped); CompareResult.OK } + else CompareResult.Fail(this :: Nil) + else if !isFixpoint then + // We did not yet observe the !isFixpoint condition in our tests, but it's a + // theoretical possibility. In that case, it would be inconsistent to both + // add `elem` to the set and back-propagate it. But if `{elem} <:< tm(elem)` + // and the variance of the set is positive, we can soundly add `tm(ref)` to + // the set while back-propagating `ref` as before. Otherwise there's nothing + // obvious left to do except fail (which is always sound). + if variance > 0 + && elem.singletonCaptureSet.subCaptures(mapped, frozen = true).isOK then + // widen to fixpoint. mapped is known to be a fixpoint since tm is idempotent. + // The widening is sound, but loses completeness. + addMapped + else + failNoFixpoint else if accountsFor(elem) then CompareResult.OK else