Skip to content

Commit b736c19

Browse files
LinyxusG1ng3r
authored andcommitted
Fix capture set healing
Capture set healing happens at the end of capture checking (in the `postCheck` function), which checks the capture set in each type argument and widen the ill-formed `TermParamRef`s by widening them. However, it is possible that a capture set is healed first, and then get a `TermParamRef` propagated into it later when we are healing another capture set. This lead to unsoundness. This commit installs an handler on capture sets when healing them and will inspect the newly added elements and heal these new elements as well.
1 parent 05cb281 commit b736c19

File tree

6 files changed

+50
-11
lines changed

6 files changed

+50
-11
lines changed

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

Lines changed: 14 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -275,6 +275,11 @@ sealed abstract class CaptureSet extends Showable:
275275
if isUniversal then handler()
276276
this
277277

278+
/** Invoke handler on the elements to check wellformedness of the capture set */
279+
def ensureWellformed(handler: List[CaptureRef] => Context ?=> Unit)(using Context): this.type =
280+
handler(elems.toList)
281+
this
282+
278283
/** An upper approximation of this capture set, i.e. a constant set that is
279284
* subcaptured by this set. If the current set is a variable
280285
* it is the intersection of all upper approximations of known supersets
@@ -375,6 +380,9 @@ object CaptureSet:
375380
/** A handler to be invoked if the root reference `cap` is added to this set */
376381
var rootAddedHandler: () => Context ?=> Unit = () => ()
377382

383+
/** A handler to be invoked when new elems are added to this set */
384+
var newElemAddedHandler: List[CaptureRef] => Context ?=> Unit = _ => ()
385+
378386
var description: String = ""
379387

380388
/** Record current elements in given VarState provided it does not yet
@@ -405,7 +413,8 @@ object CaptureSet:
405413
if !isConst && recordElemsState() then
406414
elems ++= newElems
407415
if isUniversal then rootAddedHandler()
408-
// assert(id != 2 || elems.size != 2, this)
416+
newElemAddedHandler(newElems.toList)
417+
// assert(id != 5 || elems.size != 3, this)
409418
(CompareResult.OK /: deps) { (r, dep) =>
410419
r.andAlso(dep.tryInclude(newElems, this))
411420
}
@@ -425,6 +434,10 @@ object CaptureSet:
425434
rootAddedHandler = handler
426435
super.disallowRootCapability(handler)
427436

437+
override def ensureWellformed(handler: List[CaptureRef] => (Context) ?=> Unit)(using Context): this.type =
438+
newElemAddedHandler = handler
439+
super.ensureWellformed(handler)
440+
428441
private var computingApprox = false
429442

430443
/** Roughly: the intersection of all constant known supersets of this set.

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

Lines changed: 5 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -976,8 +976,11 @@ class CheckCaptures extends Recheck, SymTransformer:
976976
recur(refs, Nil)
977977

978978
private def healCaptureSet(cs: CaptureSet): Unit =
979-
val toInclude = widenParamRefs(cs.elems.toList.filter(!isAllowed(_)).asInstanceOf)
980-
toInclude.foreach(checkSubset(_, cs, tree.srcPos))
979+
def avoidance(elems: List[CaptureRef])(using Context): Unit =
980+
val toInclude = widenParamRefs(elems.filter(!isAllowed(_)).asInstanceOf)
981+
//println(i"HEAL $cs by widening to $toInclude")
982+
toInclude.foreach(checkSubset(_, cs, tree.srcPos))
983+
cs.ensureWellformed(avoidance)
981984

982985
private var allowed: SimpleIdentitySet[TermParamRef] = SimpleIdentitySet.empty
983986

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
-- Error: tests/neg-custom-args/captures/usingLogFile-alt.scala:18:2 ---------------------------------------------------
2+
18 | usingFile( // error
3+
| ^^^^^^^^^
4+
| Sealed type variable T cannot be instantiated to box () => Unit since
5+
| that type captures the root capability `cap`.
6+
| This is often caused by a local capability in the body of method usingFile
7+
| leaking as part of its result.
Lines changed: 23 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,23 @@
1+
// Reported in issue #17517
2+
3+
import language.experimental.captureChecking
4+
import java.io.*
5+
6+
object Test:
7+
class Logger(f: OutputStream^):
8+
def log(msg: String): Unit = ???
9+
10+
def usingFile[sealed T](name: String, op: OutputStream^ => T): T =
11+
val f = new FileOutputStream(name)
12+
val result = op(f)
13+
f.close()
14+
result
15+
16+
def usingLogger[sealed T](f: OutputStream^)(op: Logger^{f} => T): T = ???
17+
18+
usingFile( // error
19+
"foo",
20+
file => {
21+
usingLogger(file)(l => () => l.log("test"))
22+
}
23+
)

tests/neg-custom-args/captures/usingLogFile.check

Lines changed: 0 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -45,10 +45,3 @@
4545
| that type captures the root capability `cap`.
4646
| This is often caused by a local capability in the body of method usingFile
4747
| leaking as part of its result.
48-
-- Error: tests/neg-custom-args/captures/usingLogFile.scala:72:6 -------------------------------------------------------
49-
72 | usingLogger(_, l => () => l.log("test"))) // error
50-
| ^^^^^^^^^^^
51-
| Sealed type variable T cannot be instantiated to box () => Unit since
52-
| that type captures the root capability `cap`.
53-
| This is often caused by a local capability in the body of method usingLogger
54-
| leaking as part of its result.

tests/neg-custom-args/captures/usingLogFile.scala

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -69,5 +69,5 @@ object Test4:
6969

7070
def test =
7171
val later = usingFile("logfile", // error
72-
usingLogger(_, l => () => l.log("test"))) // error
72+
usingLogger(_, l => () => l.log("test"))) // ok, since we can widen `l` to `file` instead of to `cap`
7373
later()

0 commit comments

Comments
 (0)