Skip to content

Commit 390233e

Browse files
committed
Cache ResultCaps
This fixes problems encountered in #15923 where we got infinite recursions caused by infinite streams of new ResultCap instances that were added to capture sets. The analysis of the problem showed that there is a cycle of dependencies involving both forwards and backwards propagations of ResultCap instances between BiMapped capture sets linked by SubstBindingMaps. Each propagation would create a new derived ResultCap instance. We could try to solve the problem by having SubstBindingMaps remember their mappings and have their inverses work backwards. But that could still produce an infinite stream if there was a cycle of SubstBindingMaps of length > 2. So we fix the problem at the root by allowing only one derived ResultCap instance per original ResultCap / binder pair. Fixes #15923
1 parent 1787fb9 commit 390233e

File tree

9 files changed

+150
-62
lines changed

9 files changed

+150
-62
lines changed

compiler/src/dotty/tools/dotc/cc/Capability.scala

Lines changed: 60 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -177,15 +177,54 @@ object Capabilities:
177177
* is expanded.
178178
*/
179179
case class ResultCap(binder: MethodicType) extends RootCapability:
180-
private var myOriginalBinder = binder
181-
def originalBinder: MethodicType = myOriginalBinder
182180

181+
private var myOrigin: RootCapability = GlobalCap
182+
private var variants: SimpleIdentitySet[ResultCap] = SimpleIdentitySet.empty
183+
184+
/** Every ResultCap capability has an origin. This is
185+
* - A FreshCap capability `f`, if the current capability was created as a mirror
186+
* of `f` in the ToResult map.
187+
* - Another ResultCap capability `r`, if the current capability was created
188+
* via a chain of `derivedResult` calls from an original ResultCap `r`
189+
* (which was not created using `derivedResult`).
190+
* - GlobalCap otherwise
191+
*/
192+
def origin: RootCapability = myOrigin
193+
194+
/** Initialize origin of this capability to a FreshCap instance (or to GlobalCap
195+
* if separation checks are turned off).
196+
* @pre The capability's origin was not yet set.
197+
*/
198+
def setOrigin(freshOrigin: FreshCap | GlobalCap.type): Unit =
199+
assert(myOrigin eq GlobalCap)
200+
myOrigin = freshOrigin
201+
202+
/** If the current capability was created via a chain of `derivedResult` calls
203+
* from an original ResultCap `r`, that `r`. Otherwise `this`.
204+
*/
205+
def primaryResultCap: ResultCap = origin match
206+
case origin: ResultCap => origin
207+
case _ => this
208+
209+
def originalBinder: MethodicType = primaryResultCap.binder
210+
211+
/** A ResultCap with given `binder1` derived from this capability.
212+
* This is typically done as a result of a SubstBinding map.
213+
* ResultCaps so created are cached, so that for every pair
214+
* of a ResultCap `r` and a binder `b`, there exists at most one ResultCap
215+
* instance that is derived transitively from `r` and has binder `b`.
216+
*/
183217
def derivedResult(binder1: MethodicType): ResultCap =
184218
if binder1 eq binder then this
185219
else
186-
val res = ResultCap(binder1)
187-
res.myOriginalBinder = myOriginalBinder
188-
res
220+
val primary = primaryResultCap
221+
primary.variants.iterator.find(_.binder eq binder1) match
222+
case Some(rcap) => rcap
223+
case None =>
224+
val rcap = ResultCap(binder1)
225+
rcap.myOrigin = primary
226+
primary.variants += rcap
227+
rcap
189228
end ResultCap
190229

191230
/** A trait for references in CaptureSets. These can be NamedTypes, ThisTypes or ParamRefs,
@@ -718,7 +757,6 @@ object Capabilities:
718757
super.mapOver(t)
719758

720759
object toVar extends CapMap:
721-
private val seen = EqHashMap[RootCapability, ResultCap]()
722760

723761
def apply(t: Type) = t match
724762
case defn.FunctionNOf(args, res, contextual) if t.typeSymbol.name.isImpureFunction =>
@@ -733,7 +771,11 @@ object Capabilities:
733771
override def mapCapability(c: Capability, deep: Boolean) = c match
734772
case c: (FreshCap | GlobalCap.type) =>
735773
if variance > 0 then
736-
seen.getOrElseUpdate(c, ResultCap(mt))
774+
val res = ResultCap(mt)
775+
c match
776+
case c: FreshCap => res.setOrigin(c)
777+
case _ =>
778+
res
737779
else
738780
if variance == 0 then
739781
fail(em"""$tp captures the root capability `cap` in invariant position.
@@ -753,15 +795,17 @@ object Capabilities:
753795
case c @ ResultCap(`mt`) =>
754796
// do a reverse getOrElseUpdate on `seen` to produce the
755797
// `Fresh` assosicated with `t`
756-
val it = seen.iterator
757-
var ref: RootCapability | Null = null
758-
while it.hasNext && ref == null do
759-
val (k, v) = it.next
760-
if v eq c then ref = k
761-
if ref == null then
762-
ref = FreshCap(Origin.Unknown)
763-
seen(ref) = c
764-
ref
798+
if !ccConfig.useSepChecks then
799+
FreshCap(Origin.Unknown) // warning: this can cause cycles
800+
else
801+
val primary = c.primaryResultCap
802+
primary.origin match
803+
case GlobalCap =>
804+
val fresh = FreshCap(Origin.Unknown)
805+
primary.setOrigin(fresh)
806+
fresh
807+
case origin: FreshCap =>
808+
origin
765809
case _ =>
766810
super.mapCapability(c, deep)
767811

compiler/src/dotty/tools/dotc/cc/CaptureSet.scala

Lines changed: 15 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -74,6 +74,9 @@ sealed abstract class CaptureSet extends Showable:
7474
/** Is this capture set definitely non-empty? */
7575
final def isNotEmpty: Boolean = !elems.isEmpty
7676

77+
/** If this is a Var, its `id`, otherwise -1 */
78+
def maybeId: Int = -1
79+
7780
/** Convert to Const. @pre: isConst */
7881
def asConst(using Context): Const = this match
7982
case c: Const => c
@@ -129,7 +132,7 @@ sealed abstract class CaptureSet extends Showable:
129132
* element is not the root capability, try instead to include its underlying
130133
* capture set.
131134
*/
132-
protected def tryInclude(elem: Capability, origin: CaptureSet)(using Context, VarState): CompareResult =
135+
protected def tryInclude(elem: Capability, origin: CaptureSet)(using Context, VarState): CompareResult = reporting.trace(i"try include $elem in $this # ${maybeId}"):
133136
if accountsFor(elem) then CompareResult.OK
134137
else addNewElem(elem)
135138

@@ -518,6 +521,8 @@ object CaptureSet:
518521
ccs.varId += 1
519522
ccs.varId
520523

524+
override def maybeId = id
525+
521526
//assert(id != 8, this)
522527

523528
/** A variable is solved if it is aproximated to a from-then-on constant set.
@@ -607,7 +612,9 @@ object CaptureSet:
607612
val normElem = if isMaybeSet then elem else elem.stripMaybe
608613
// assert(id != 5 || elems.size != 3, this)
609614
val res = (CompareResult.OK /: deps): (r, dep) =>
610-
r.andAlso(dep.tryInclude(normElem, this))
615+
r.andAlso:
616+
reporting.trace(i"forward $normElem from $this # $id to $dep # ${dep.maybeId} of class ${dep.getClass.toString}"):
617+
dep.tryInclude(normElem, this)
611618
if ccConfig.checkSkippedMaps && res.isOK then checkSkippedMaps(elem)
612619
res.orElse:
613620
elems -= elem
@@ -819,12 +826,14 @@ object CaptureSet:
819826
else if accountsFor(elem) then
820827
CompareResult.OK
821828
else
829+
// Propagate backwards to source. The element will be added then by another
830+
// forward propagation from source that hits the first branch `if origin eq source then`.
822831
try
823-
source.tryInclude(bimap.inverse.mapCapability(elem), this)
824-
.showing(i"propagating new elem $elem backward from $this to $source = $result", captDebug)
825-
.andAlso(addNewElem(elem))
832+
reporting.trace(i"prop backwards $elem from $this # $id to $source # ${source.id} via $summarize"):
833+
source.tryInclude(bimap.inverse.mapCapability(elem), this)
834+
.showing(i"propagating new elem $elem backward from $this/$id to $source = $result", captDebug)
826835
catch case ex: AssertionError =>
827-
println(i"fail while prop backwards tryInclude $elem of ${elem.getClass} in $this / ${this.summarize}")
836+
println(i"fail while prop backwards tryInclude $elem of ${elem.getClass} from $this # $id / ${this.summarize} to $source # ${source.id}")
828837
throw ex
829838

830839
/** For a BiTypeMap, supertypes of the mapped type also constrain
Lines changed: 23 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,23 @@
1+
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/i15923.scala:12:21 ---------------------------------------
2+
12 | val leak = withCap(cap => mkId(cap)) // error
3+
| ^^^^^^^^^^^^^^^^
4+
|Found: (lcap: scala.caps.Capability^{cap.rd}) ?->? Cap^{lcap} ->? box Id[box Cap^{cap².rd}]^?
5+
|Required: (lcap: scala.caps.Capability^{cap.rd}) ?-> Cap^{lcap} => box Id[box Cap^?]^?
6+
|
7+
|where: => refers to a root capability associated with the result type of (using lcap: scala.caps.Capability^{cap.rd}): Cap^{lcap} => box Id[box Cap^?]^?
8+
| cap is the universal root capability
9+
| cap² is a root capability associated with the result type of (x$0: Cap^{lcap}): box Id[box Cap^{cap².rd}]^?
10+
|
11+
|
12+
|Note that reference <cap of (x$0: Cap^{lcap}): box Id[box Cap^{cap.rd}]^?>.rd
13+
|cannot be included in outer capture set ?
14+
|
15+
| longer explanation available when compiling with `-explain`
16+
-- Warning: tests/neg-custom-args/captures/i15923.scala:21:56 ----------------------------------------------------------
17+
21 | def withCap[X](op: (lcap: caps.Capability) ?-> Cap^{lcap} => X): X = {
18+
| ^^^^
19+
| redundant capture: test2.Cap already accounts for lcap.type
20+
-- Warning: tests/neg-custom-args/captures/i15923.scala:6:54 -----------------------------------------------------------
21+
6 | def withCap[X](op: (lcap: caps.Capability) ?-> Cap^{lcap} => X): X = {
22+
| ^^^^
23+
| redundant capture: Cap already accounts for lcap.type
Lines changed: 29 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,29 @@
1+
trait Cap { def use(): Int }
2+
class Id[X](val value: [T] -> (op: X => T) -> T)
3+
def mkId[X](x: X): Id[X] = Id([T] => (op: X => T) => op(x))
4+
5+
def bar() = {
6+
def withCap[X](op: (lcap: caps.Capability) ?-> Cap^{lcap} => X): X = {
7+
val cap: Cap = new Cap { def use() = { println("cap is used"); 0 } }
8+
val result = op(using caps.cap)(cap)
9+
result
10+
}
11+
12+
val leak = withCap(cap => mkId(cap)) // error
13+
}
14+
15+
package test2:
16+
trait Cap { def use(): Int }
17+
type Id[X] = [T] -> (op: X => T) -> T
18+
def mkId[X](x: X): Id[X] = [T] => (op: X => T) => op(x)
19+
20+
def bar() = {
21+
def withCap[X](op: (lcap: caps.Capability) ?-> Cap^{lcap} => X): X = {
22+
val cap: Cap = new Cap { def use() = { println("cap is used"); 0 } }
23+
val result = op(using caps.cap)(cap)
24+
result
25+
}
26+
27+
val leak = withCap(cap => mkId(cap)) // no error here since type aliases don't box
28+
leak { cap => cap.use() }
29+
}
Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,16 @@
1+
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/i15923a.scala:7:21 ---------------------------------------
2+
7 | val leak = withCap(lcap => () => mkId(lcap)) // error
3+
| ^^^^^^^^^^^^^^^^^^^^^^^^
4+
|Found: (lcap: Cap^) ->? () ->? box Id[box Cap^²]^?
5+
|Required: (lcap: Cap^) => () =>² box Id[box Cap^?]^?
6+
|
7+
|where: => refers to a fresh root capability created in value leak when checking argument to parameter op of method withCap
8+
| =>² refers to a root capability associated with the result type of (lcap: Cap^): () =>² box Id[box Cap^?]^?
9+
| ^ refers to the universal root capability
10+
| ^² refers to a root capability associated with the result type of (): box Id[box Cap^²]^?
11+
|
12+
|
13+
|Note that reference <cap of (): box Id[box Cap^]^?>
14+
|cannot be included in outer capture set ?
15+
|
16+
| longer explanation available when compiling with `-explain`
Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
import language.experimental.captureChecking
2+
trait Cap
3+
case class Id[X](x: X)
4+
def mkId[X](x: X): Id[X] = Id(x)
5+
def withCap[X](op: (lcap: Cap^) => () => X): X = ???
6+
def bar() =
7+
val leak = withCap(lcap => () => mkId(lcap)) // error

tests/pending/neg-custom-args/captures/i15923.scala

Lines changed: 0 additions & 14 deletions
This file was deleted.

tests/pending/neg-custom-args/captures/i15923a.scala

Lines changed: 0 additions & 13 deletions
This file was deleted.

tests/pending/neg-custom-args/captures/i15923b.scala

Lines changed: 0 additions & 13 deletions
This file was deleted.

0 commit comments

Comments
 (0)