Skip to content

Commit d96bf10

Browse files
LinyxusLinyxus
committed
Fix separation checking for function results
1 parent cacd117 commit d96bf10

File tree

3 files changed

+132
-41
lines changed

3 files changed

+132
-41
lines changed

‎compiler/src/dotty/tools/dotc/cc/SepCheck.scala‎

Lines changed: 58 additions & 41 deletions
Original file line numberDiff line numberDiff line change
@@ -457,14 +457,16 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser:
457457
* Also check separation via checkType within individual arguments widened to their
458458
* formal paramater types.
459459
*
460-
* @param fn the applied function
461-
* @param args the flattened argument lists
462-
* @param app the entire application tree
463-
* @param deps cross argument dependencies: maps argument trees to
464-
* those other arguments that where mentioned by coorresponding
465-
* formal parameters.
460+
* @param fn the applied function
461+
* @param args the flattened argument lists
462+
* @param app the entire application tree
463+
* @param deps cross argument dependencies: maps argument trees to
464+
* those other arguments that where mentioned by coorresponding
465+
* formal parameters.
466+
* @param resultPeaks peaks in the result type that could interfere with the
467+
* hidden sets of formal parameters
466468
*/
467-
private def checkApply(fn: Tree, args: List[Tree], app: Tree, deps: collection.Map[Tree, List[Tree]])(using Context): Unit =
469+
private def checkApply(fn: Tree, args: List[Tree], app: Tree, deps: collection.Map[Tree, List[Tree]], resultPeaks: Refs)(using Context): Unit =
468470
val (qual, fnCaptures) = methPart(fn) match
469471
case Select(qual, _) => (qual, qual.nuType.captureSet)
470472
case _ => (fn, CaptureSet.empty)
@@ -475,6 +477,7 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser:
475477
i"""check separate $fn($args), fnCaptures = $fnCaptures,
476478
| formalCaptures = ${args.map(arg => CaptureSet(formalCaptures(arg)))},
477479
| actualCaptures = ${args.map(arg => CaptureSet(captures(arg)))},
480+
| resultPeaks = ${resultPeaks},
478481
| deps = ${deps.toList}""")
479482
val parts = qual :: args
480483
var reported: SimpleIdentitySet[Tree] = SimpleIdentitySet.empty
@@ -519,26 +522,10 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser:
519522
currentPeaks.hidden ++ argPeaks.hidden)
520523
end for
521524

522-
def collectRefs(args: List[Type], res: Type) =
523-
args.foldLeft(argCaptures(res)): (refs, arg) =>
524-
refs ++ arg.deepCaptureSet.elems
525-
526-
/** The deep capture sets of all parameters of this type (if it is a function type) */
527-
def argCaptures(tpe: Type): Refs = tpe match
528-
case defn.FunctionOf(args, resultType, isContextual) =>
529-
collectRefs(args, resultType)
530-
case defn.RefinedFunctionOf(mt) =>
531-
collectRefs(mt.paramInfos, mt.resType)
532-
case CapturingType(parent, _) =>
533-
argCaptures(parent)
534-
case _ =>
535-
emptyRefs
536-
537-
if !deps(app).isEmpty then
538-
lazy val appPeaks = argCaptures(app.nuType).peaks
525+
if !resultPeaks.isEmpty then
539526
lazy val partPeaks = partsWithPeaks.toMap
540-
for arg <- deps(app) do
541-
if arg.needsSepCheck && !partPeaks(arg).hidden.sharedWith(appPeaks).isEmpty then
527+
for arg <- args do
528+
if arg.needsSepCheck && !partPeaks(arg).hidden.sharedWith(resultPeaks).isEmpty then
542529
sepApplyError(fn, parts, arg, app)
543530
end checkApply
544531

@@ -816,10 +803,15 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser:
816803
* then the dependencies of an application `f(a, b, c)` of type C^{y} is the map
817804
*
818805
* [ b -> [a]
819-
* , c -> [a, b]
820-
* , f(a, b, c) -> [b]]
806+
* , c -> [a, b] ]
807+
*
808+
* It also returns the interfering peaks of the result of the application. They are the
809+
* peaks of argument captures and deep captures of the result function type, minus the
810+
* those dependent on parameters. For instance,
811+
* if `f` has the type (x: A, y: B, c: C) -> (op: () ->{b} Unit) -> List[() ->{x, y, a} Unit], its interfering
812+
* peaks will be the peaks of `a` and `b`.
821813
*/
822-
private def dependencies(fn: Tree, argss: List[List[Tree]], app: Tree)(using Context): collection.Map[Tree, List[Tree]] =
814+
private def dependencies(fn: Tree, argss: List[List[Tree]], app: Tree)(using Context): (collection.Map[Tree, List[Tree]], Refs) =
823815
def isFunApply(sym: Symbol) =
824816
sym.name == nme.apply && defn.isFunctionClass(sym.owner)
825817
val mtpe =
@@ -831,23 +823,47 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser:
831823
val argMap = mtpsWithArgs.toMap
832824
val deps = mutable.HashMap[Tree, List[Tree]]().withDefaultValue(Nil)
833825

826+
def argOfDep(dep: Capability): Option[Tree] =
827+
dep.stripReach match
828+
case dep: TermParamRef =>
829+
Some(argMap(dep.binder)(dep.paramNum))
830+
case dep: ThisType if dep.cls == fn.symbol.owner =>
831+
val Select(qual, _) = fn: @unchecked // TODO can we use fn instead?
832+
Some(qual)
833+
case _ =>
834+
None
835+
834836
def recordDeps(formal: Type, actual: Tree) =
835-
for dep <- formal.captureSet.elems.toList do
836-
val referred = dep.stripReach match
837-
case dep: TermParamRef =>
838-
argMap(dep.binder)(dep.paramNum) :: Nil
839-
case dep: ThisType if dep.cls == fn.symbol.owner =>
840-
val Select(qual, _) = fn: @unchecked // TODO can we use fn instead?
841-
qual :: Nil
842-
case _ =>
843-
Nil
837+
def captures = formal.captureSet
838+
for dep <- captures.elems.toList do
839+
val referred = argOfDep(dep)
844840
deps(actual) ++= referred
845841

842+
inline def isLocalRef(x: Capability): Boolean = x.isInstanceOf[TermParamRef]
843+
844+
def resultArgCaptures(tpe: Type): Refs =
845+
def collectRefs(args: List[Type], res: Type) =
846+
args.foldLeft(resultArgCaptures(res)): (refs, arg) =>
847+
refs ++ arg.captureSet.elems
848+
tpe match
849+
case defn.FunctionOf(args, resultType, isContextual) =>
850+
collectRefs(args, resultType)
851+
case defn.RefinedFunctionOf(mt) =>
852+
collectRefs(mt.paramInfos, mt.resType)
853+
case CapturingType(parent, refs) =>
854+
resultArgCaptures(parent) ++ tpe.boxedCaptureSet.elems
855+
case _ =>
856+
emptyRefs
857+
846858
for (mt, args) <- mtpsWithArgs; (formal, arg) <- mt.paramInfos.zip(args) do
847859
recordDeps(formal, arg)
848-
recordDeps(mtpe.finalResultType, app)
860+
861+
val resultType = mtpe.finalResultType
862+
val resultCaptures =
863+
(resultArgCaptures(resultType) ++ resultType.deepCaptureSet.elems).filter(!isLocalRef(_))
864+
val resultPeaks = resultCaptures.peaks
849865
capt.println(i"deps for $app = ${deps.toList}")
850-
deps
866+
(deps, resultPeaks)
851867

852868

853869
/** Decompose an application into a function prefix and a list of argument lists.
@@ -860,7 +876,8 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser:
860876
case TypeApply(fn, args) => recur(fn, argss) // skip type arguments
861877
case _ =>
862878
if argss.nestedExists(_.needsSepCheck) then
863-
checkApply(tree, argss.flatten, app, dependencies(tree, argss, app))
879+
val (deps, resultPeaks) = dependencies(tree, argss, app)
880+
checkApply(tree, argss.flatten, app, deps, resultPeaks)
864881
recur(app, Nil)
865882

866883
/** Is `tree` an application of `caps.unsafe.unsafeAssumeSeparate`? */

‎tests/neg-custom-args/captures/i23726.check‎

Lines changed: 51 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,51 @@
1+
-- Error: tests/neg-custom-args/captures/i23726.scala:10:5 -------------------------------------------------------------
2+
10 | f1(a) // error, as expected
3+
| ^
4+
|Separation failure: argument of type (a : Ref^)
5+
|to a function of type (x: Ref^) -> List[() ->{a, x} Unit]
6+
|corresponds to capture-polymorphic formal parameter x of type Ref^²
7+
|and hides capabilities {a}.
8+
|Some of these overlap with the captures of the function result with type List[() ->{a} Unit].
9+
|
10+
| Hidden set of current argument : {a}
11+
| Hidden footprint of current argument : {a}
12+
| Capture set of function result : {a}
13+
| Footprint set of function result : {a}
14+
| The two sets overlap at : {a}
15+
|
16+
|where: ^ refers to a fresh root capability classified as Mutable created in value a when constructing mutable Ref
17+
| ^² refers to a fresh root capability classified as Mutable created in method test1 when checking argument to parameter x of method apply
18+
-- Error: tests/neg-custom-args/captures/i23726.scala:15:5 -------------------------------------------------------------
19+
15 | f3(b) // error
20+
| ^
21+
|Separation failure: argument of type (b : Ref^)
22+
|to a function of type (x: Ref^) -> (op: () ->{b} Unit) -> List[() ->{op} Unit]
23+
|corresponds to capture-polymorphic formal parameter x of type Ref^²
24+
|and hides capabilities {b}.
25+
|Some of these overlap with the captures of the function result with type (op: () ->{b} Unit) -> List[() ->{op} Unit].
26+
|
27+
| Hidden set of current argument : {b}
28+
| Hidden footprint of current argument : {b}
29+
| Capture set of function result : {op}
30+
| Footprint set of function result : {op, b}
31+
| The two sets overlap at : {b}
32+
|
33+
|where: ^ refers to a fresh root capability classified as Mutable created in value b when constructing mutable Ref
34+
| ^² refers to a fresh root capability classified as Mutable created in method test1 when checking argument to parameter x of method apply
35+
-- Error: tests/neg-custom-args/captures/i23726.scala:23:5 -------------------------------------------------------------
36+
23 | f7(a) // error
37+
| ^
38+
|Separation failure: argument of type (a : Ref^)
39+
|to a function of type (x: Ref^) ->{a, b} (y: List[Ref^{a, b}]) ->{a, b} Unit
40+
|corresponds to capture-polymorphic formal parameter x of type Ref^²
41+
|and hides capabilities {a}.
42+
|Some of these overlap with the captures of the function prefix.
43+
|
44+
| Hidden set of current argument : {a}
45+
| Hidden footprint of current argument : {a}
46+
| Capture set of function prefix : {f7*}
47+
| Footprint set of function prefix : {f7*, a, b}
48+
| The two sets overlap at : {a}
49+
|
50+
|where: ^ refers to a fresh root capability classified as Mutable created in value a when constructing mutable Ref
51+
| ^² refers to a fresh root capability classified as Mutable created in method test1 when checking argument to parameter x of method apply

‎tests/neg-custom-args/captures/i23726.scala‎

Lines changed: 23 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,23 @@
1+
import language.experimental.captureChecking
2+
import language.experimental.separationChecking
3+
import caps.*
4+
class Ref extends Mutable
5+
def swap(a: Ref^, b: Ref^): Unit = ()
6+
def test1(): Unit =
7+
val a = Ref()
8+
val b = Ref()
9+
val f1: (x: Ref^) -> List[() ->{a,x} Unit] = ???
10+
f1(a) // error, as expected
11+
val f2: (x: Ref^) -> List[() ->{x} Unit] = ???
12+
f2(a) // ok, as expected
13+
val f3: (x: Ref^) -> (op: () ->{b} Unit) -> List[() ->{op} Unit] = ???
14+
f3(a) // ok
15+
f3(b) // error
16+
val f4: (x: Ref^) -> (y: Ref^{x}) ->{x} Unit = ???
17+
f4(a) // ok
18+
val f5: (x: Ref^) -> (y: List[Ref^{a}]) ->{} Unit = ???
19+
f5(a) // ok
20+
val f6: (x: Ref^) -> (y: List[Ref^{a, b}]) ->{} Unit = ???
21+
f6(b) // ok
22+
val f7: (x: Ref^) ->{a, b} (y: List[Ref^{a, b}]) ->{a, b} Unit = ???
23+
f7(a) // error

0 commit comments

Comments
 (0)