Skip to content

Commit

Permalink
Separation checking for blocks
Browse files Browse the repository at this point in the history 
Check that a capability that gets hidden in the (result-)type of some
definition is not used afterwards in the same or a nested scope.
  • Loading branch information
@odersky
odersky committed Jan 14, 2025
1 parent bc2b33f commit af23b3f
Show file tree
Hide file tree
Showing 15 changed files with 328 additions and 122 deletions.
78 changes: 43 additions & 35 deletions compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -18,7 +18,7 @@ import util.{SimpleIdentitySet, EqHashMap, EqHashSet, SrcPos, Property}
import transform.{Recheck, PreRecheck, CapturedVars}
import Recheck.*
import scala.collection.mutable
import CaptureSet.{withCaptureSetsExplained, IdempotentCaptRefMap, CompareResult, VarState}
import CaptureSet.{withCaptureSetsExplained, IdempotentCaptRefMap, CompareResult}
import CCState.*
import StdNames.nme
import NameKinds.{DefaultGetterName, WildcardParamName, UniqueNameKind}
Expand Down Expand Up @@ -253,6 +253,10 @@ object CheckCaptures:
* the type of the formal paremeter corresponding to the argument.
*/
def formalType: Type

/** The "use set", i.e. the capture set marked as free at this node. */
def markedFree: CaptureSet

end CheckerAPI

class CheckCaptures extends Recheck, SymTransformer:
Expand Down Expand Up @@ -298,9 +302,12 @@ class CheckCaptures extends Recheck, SymTransformer:
*/
private val sepCheckFormals = util.EqHashMap[Tree, Type]()

private val usedSet = util.EqHashMap[Tree, CaptureSet]()

extension [T <: Tree](tree: T)
def needsSepCheck: Boolean = sepCheckFormals.contains(tree)
def formalType: Type = sepCheckFormals.getOrElse(tree, NoType)
def markedFree = usedSet.getOrElse(tree, CaptureSet.empty)

/** Instantiate capture set variables appearing contra-variantly to their
* upper approximation.
Expand Down Expand Up @@ -404,17 +411,17 @@ class CheckCaptures extends Recheck, SymTransformer:
/** Include `sym` in the capture sets of all enclosing environments nested in the
* the environment in which `sym` is defined.
*/
def markFree(sym: Symbol, pos: SrcPos)(using Context): Unit =
markFree(sym, sym.termRef, pos)
def markFree(sym: Symbol, tree: Tree)(using Context): Unit =
markFree(sym, sym.termRef, tree)

def markFree(sym: Symbol, ref: CaptureRef, pos: SrcPos)(using Context): Unit =
if sym.exists && ref.isTracked then markFree(ref.captureSet, pos)
def markFree(sym: Symbol, ref: CaptureRef, tree: Tree)(using Context): Unit =
if sym.exists && ref.isTracked then markFree(ref.captureSet, tree)

/** Make sure the (projected) `cs` is a subset of the capture sets of all enclosing
* environments. At each stage, only include references from `cs` that are outside
* the environment's owner
*/
def markFree(cs: CaptureSet, pos: SrcPos)(using Context): Unit =
def markFree(cs: CaptureSet, tree: Tree)(using Context): Unit =
// A captured reference with the symbol `sym` is visible from the environment
// if `sym` is not defined inside the owner of the environment.
inline def isVisibleFromEnv(sym: Symbol, env: Env) =
Expand All @@ -436,7 +443,7 @@ class CheckCaptures extends Recheck, SymTransformer:
val what = if ref.isType then "Capture set parameter" else "Local reach capability"
report.error(
em"""$what $c leaks into capture scope of ${env.ownerString}.
|To allow this, the ${ref.symbol} should be declared with a @use annotation""", pos)
|To allow this, the ${ref.symbol} should be declared with a @use annotation""", tree.srcPos)
case _ =>

/** Avoid locally defined capability by charging the underlying type
Expand All @@ -456,7 +463,7 @@ class CheckCaptures extends Recheck, SymTransformer:
CaptureSet.ofType(c.widen, followResult = false)
capt.println(i"Widen reach $c to $underlying in ${env.owner}")
underlying.disallowRootCapability: () =>
report.error(em"Local capability $c in ${env.ownerString} cannot have `cap` as underlying capture set", pos)
report.error(em"Local capability $c in ${env.ownerString} cannot have `cap` as underlying capture set", tree.srcPos)
recur(underlying, env, lastEnv)

/** Avoid locally defined capability if it is a reach capability or capture set
Expand All @@ -479,7 +486,7 @@ class CheckCaptures extends Recheck, SymTransformer:
val underlying = CaptureSet.ofTypeDeeply(c1.widen)
capt.println(i"Widen reach $c to $underlying in ${env.owner}")
underlying.disallowRootCapability: () =>
report.error(em"Local reach capability $c leaks into capture scope of ${env.ownerString}", pos)
report.error(em"Local reach capability $c leaks into capture scope of ${env.ownerString}", tree.srcPos)
recur(underlying, env, null)
case c: TypeRef if c.isParamPath =>
checkUseDeclared(c, env, null)
Expand All @@ -496,22 +503,23 @@ class CheckCaptures extends Recheck, SymTransformer:
then avoidLocalCapability(c, env, lastEnv)
else avoidLocalReachCapability(c, env)
isVisible
checkSubset(included, env.captured, pos, provenance(env))
checkSubset(included, env.captured, tree.srcPos, provenance(env))
capt.println(i"Include call or box capture $included from $cs in ${env.owner} --> ${env.captured}")
if !isOfNestedMethod(env) then
recur(included, nextEnvToCharge(env, !_.owner.isStaticOwner), env)
// Don't propagate out of methods inside terms. The use set of these methods
// will be charged when that method is called.

recur(cs, curEnv, null)
usedSet(tree) = tree.markedFree ++ cs
end markFree

/** Include references captured by the called method in the current environment stack */
def includeCallCaptures(sym: Symbol, resType: Type, pos: SrcPos)(using Context): Unit = resType match
def includeCallCaptures(sym: Symbol, resType: Type, tree: Tree)(using Context): Unit = resType match
case _: MethodOrPoly => // wait until method is fully applied
case _ =>
if sym.exists then
if curEnv.isOpen then markFree(capturedVars(sym), pos)
if curEnv.isOpen then markFree(capturedVars(sym), tree)

/** Under the sealed policy, disallow the root capability in type arguments.
* Type arguments come either from a TypeApply node or from an AppliedType
Expand All @@ -535,23 +543,23 @@ class CheckCaptures extends Recheck, SymTransformer:

for case (arg: TypeTree, pname) <- args.lazyZip(paramNames) do
def where = if sym.exists then i" in an argument of $sym" else ""
val (addendum, pos) =
val (addendum, errTree) =
if arg.isInferred
then ("\nThis is often caused by a local capability$where\nleaking as part of its result.", fn.srcPos)
else if arg.span.exists then ("", arg.srcPos)
else ("", fn.srcPos)
then ("\nThis is often caused by a local capability$where\nleaking as part of its result.", fn)
else if arg.span.exists then ("", arg)
else ("", fn)
disallowRootCapabilitiesIn(arg.nuType, NoSymbol,
i"Type variable $pname of $sym", "be instantiated to", addendum, pos)
i"Type variable $pname of $sym", "be instantiated to", addendum, errTree.srcPos)

val param = fn.symbol.paramNamed(pname)
if param.isUseParam then markFree(arg.nuType.deepCaptureSet, pos)
if param.isUseParam then markFree(arg.nuType.deepCaptureSet, errTree)
end disallowCapInTypeArgs

override def recheckIdent(tree: Ident, pt: Type)(using Context): Type =
val sym = tree.symbol
if sym.is(Method) then
// If ident refers to a parameterless method, charge its cv to the environment
includeCallCaptures(sym, sym.info, tree.srcPos)
includeCallCaptures(sym, sym.info, tree)
else if !sym.isStatic then
// Otherwise charge its symbol, but add all selections implied by the e
// expected type `pt`.
Expand All @@ -569,7 +577,7 @@ class CheckCaptures extends Recheck, SymTransformer:
var pathRef: CaptureRef = addSelects(sym.termRef, pt)
if pathRef.derivesFrom(defn.Caps_Mutable) && pt.isValueType && !pt.isMutableType then
pathRef = pathRef.readOnly
markFree(sym, pathRef, tree.srcPos)
markFree(sym, pathRef, tree)
super.recheckIdent(tree, pt)

/** The expected type for the qualifier of a selection. If the selection
Expand Down Expand Up @@ -668,7 +676,7 @@ class CheckCaptures extends Recheck, SymTransformer:
super.recheckFinish(argType, tree, pt)
else
val res = super.recheckApply(tree, pt)
includeCallCaptures(meth, res, tree.srcPos)
includeCallCaptures(meth, res, tree)
res

/** Recheck argument, and, if formal parameter carries a `@use`,
Expand All @@ -681,7 +689,7 @@ class CheckCaptures extends Recheck, SymTransformer:
if formal.hasUseAnnot then
// The @use annotation is added to `formal` by `prepareFunction`
capt.println(i"charging deep capture set of $arg: ${argType} = ${argType.deepCaptureSet}")
markFree(argType.deepCaptureSet, arg.srcPos)
markFree(argType.deepCaptureSet, arg)
if formal.containsCap then
sepCheckFormals(arg) = freshenedFormal
argType
Expand Down Expand Up @@ -815,7 +823,7 @@ class CheckCaptures extends Recheck, SymTransformer:
case fun => fun.symbol
disallowCapInTypeArgs(tree.fun, meth, tree.args)
val res = Existential.toCap(super.recheckTypeApply(tree, pt))
includeCallCaptures(tree.symbol, res, tree.srcPos)
includeCallCaptures(tree.symbol, res, tree)
checkContains(tree)
res
end recheckTypeApply
Expand Down Expand Up @@ -1092,7 +1100,7 @@ class CheckCaptures extends Recheck, SymTransformer:
case AnnotatedType(_, annot) if annot.symbol == defn.RequiresCapabilityAnnot =>
annot.tree match
case Apply(_, cap :: Nil) =>
markFree(cap.symbol, tree.srcPos)
markFree(cap.symbol, tree)
case _ =>
case _ =>
super.recheckTyped(tree)
Expand Down Expand Up @@ -1147,7 +1155,7 @@ class CheckCaptures extends Recheck, SymTransformer:
super.recheck(tree, pt)
finally curEnv = saved
if tree.isTerm && !pt.isBoxedCapturing && pt != LhsProto then
markFree(res.boxedCaptureSet, tree.srcPos)
markFree(res.boxedCaptureSet, tree)
res
end recheck

Expand Down Expand Up @@ -1214,7 +1222,7 @@ class CheckCaptures extends Recheck, SymTransformer:
override def checkConformsExpr(actual: Type, expected: Type, tree: Tree, addenda: Addenda)(using Context): Type =
var expected1 = alignDependentFunction(expected, actual.stripCapturing)
val boxErrors = new mutable.ListBuffer[Message]
val actualBoxed = adapt(actual, expected1, tree.srcPos, boxErrors)
val actualBoxed = adapt(actual, expected1, tree, boxErrors)
//println(i"check conforms $actualBoxed <<< $expected1")

if actualBoxed eq actual then
Expand Down Expand Up @@ -1334,7 +1342,7 @@ class CheckCaptures extends Recheck, SymTransformer:
*
* @param alwaysConst always make capture set variables constant after adaptation
*/
def adaptBoxed(actual: Type, expected: Type, pos: SrcPos, covariant: Boolean, alwaysConst: Boolean, boxErrors: BoxErrors)(using Context): Type =
def adaptBoxed(actual: Type, expected: Type, tree: Tree, covariant: Boolean, alwaysConst: Boolean, boxErrors: BoxErrors)(using Context): Type =

def recur(actual: Type, expected: Type, covariant: Boolean): Type =

Expand Down Expand Up @@ -1401,7 +1409,7 @@ class CheckCaptures extends Recheck, SymTransformer:
if !leaked.subCaptures(cs).isOK then
report.error(
em"""$expected cannot be box-converted to ${actual.capturing(leaked)}
|since the additional capture set $leaked resulted from box conversion is not allowed in $actual""", pos)
|since the additional capture set $leaked resulted from box conversion is not allowed in $actual""", tree.srcPos)
cs

def adaptedType(resultBoxed: Boolean) =
Expand Down Expand Up @@ -1433,11 +1441,11 @@ class CheckCaptures extends Recheck, SymTransformer:
return actual
// Disallow future addition of `cap` to `criticalSet`.
criticalSet.disallowRootCapability: () =>
report.error(msg, pos)
report.error(msg, tree.srcPos)

if !insertBox then // we are unboxing
//debugShowEnvs()
markFree(criticalSet, pos)
markFree(criticalSet, tree)
end if

// Compute the adapted type.
Expand Down Expand Up @@ -1497,14 +1505,14 @@ class CheckCaptures extends Recheck, SymTransformer:
* - narrow nested captures of `x`'s underlying type to `{x*}`
* - do box adaptation
*/
def adapt(actual: Type, expected: Type, pos: SrcPos, boxErrors: BoxErrors)(using Context): Type =
def adapt(actual: Type, expected: Type, tree: Tree, boxErrors: BoxErrors)(using Context): Type =
if expected == LhsProto || expected.isSingleton && actual.isSingleton then
actual
else
val improvedVAR = improveCaptures(actual.widen.dealiasKeepAnnots, actual)
val improvedRO = improveReadOnly(improvedVAR, expected)
val adapted = adaptBoxed(
improvedRO.withReachCaptures(actual), expected, pos,
improvedRO.withReachCaptures(actual), expected, tree,
covariant = true, alwaysConst = false, boxErrors)
if adapted eq improvedVAR // no .rd improvement, no box-adaptation
then actual // might as well use actual instead of improved widened
Expand All @@ -1519,19 +1527,19 @@ class CheckCaptures extends Recheck, SymTransformer:
* But maybe we can then elide the check during the RefChecks phase under captureChecking?
*/
def checkOverrides = new TreeTraverser:
class OverridingPairsCheckerCC(clazz: ClassSymbol, self: Type, srcPos: SrcPos)(using Context) extends OverridingPairsChecker(clazz, self):
class OverridingPairsCheckerCC(clazz: ClassSymbol, self: Type, tree: Tree)(using Context) extends OverridingPairsChecker(clazz, self):
/** Check subtype with box adaptation.
* This function is passed to RefChecks to check the compatibility of overriding pairs.
* @param sym symbol of the field definition that is being checked
*/
override def checkSubType(actual: Type, expected: Type)(using Context): Boolean =
val expected1 = alignDependentFunction(addOuterRefs(expected, actual, srcPos), actual.stripCapturing)
val expected1 = alignDependentFunction(addOuterRefs(expected, actual, tree.srcPos), actual.stripCapturing)
val actual1 =
val saved = curEnv
try
curEnv = Env(clazz, EnvKind.NestedInOwner, capturedVars(clazz), outer0 = curEnv)
val adapted =
adaptBoxed(actual, expected1, srcPos, covariant = true, alwaysConst = true, null)
adaptBoxed(actual, expected1, tree, covariant = true, alwaysConst = true, null)
actual match
case _: MethodType =>
// We remove the capture set resulted from box adaptation for method types,
Expand Down
Loading

0 comments on commit af23b3f

Please sign in to comment.