Skip to content

Navigation Menu

Sign in
Appearance settings

Search code, repositories, users, issues, pull requests...

Provide feedback

We read every piece of feedback, and take your input very seriously.

Saved searches

Use saved searches to filter your results more quickly

Sign up
Appearance settings

Commit e78c54c

Browse files
LinyxusWojciechMazur
authored andcommitted
Fix separation checking for function results
[Cherry-picked d96bf10]
1 parent 2909320 commit e78c54c

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`? */
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^2
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+
| ^2 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^2
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+
| ^2 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^2
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+
| ^2 refers to a fresh root capability classified as Mutable created in method test1 when checking argument to parameter x of method apply
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)

AltStyle によって変換されたページ (->オリジナル) /