@@ -15,63 +15,58 @@ class SepChecker(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser:
15
15
import tpd .*
16
16
import checker .*
17
17
18
- extension (cs : CaptureSet )
19
- def footprint (using Context ): CaptureSet . Const =
20
- def recur (elems : CaptureSet . Refs , newElems : List [CaptureRef ]): CaptureSet . Refs = newElems match
18
+ extension (refs : Refs )
19
+ def footprint (using Context ): Refs =
20
+ def recur (elems : Refs , newElems : List [CaptureRef ]): Refs = newElems match
21
21
case newElem :: newElems1 =>
22
22
val superElems = newElem.captureSetOfInfo.elems.filter: superElem =>
23
23
! superElem.isMaxCapability && ! elems.contains(superElem)
24
24
recur(elems ++ superElems, newElems1 ++ superElems.toList)
25
25
case Nil => elems
26
- val elems : CaptureSet . Refs = cs.elems .filter(! _.isMaxCapability)
27
- CaptureSet ( recur(elems, elems.toList) )
26
+ val elems : Refs = refs .filter(! _.isMaxCapability)
27
+ recur(elems, elems.toList)
28
28
29
- def overlapWith (other : CaptureSet )(using Context ): CaptureSet . Refs =
30
- val refs1 = cs.elems
31
- val refs2 = other.elems
32
- def common (refs1 : CaptureSet . Refs , refs2 : CaptureSet . Refs ) =
29
+ def overlapWith (other : Refs )(using Context ): Refs =
30
+ val refs1 = refs
31
+ val refs2 = other
32
+ def common (refs1 : Refs , refs2 : Refs ) =
33
33
refs1.filter: ref =>
34
34
ref.isExclusive && refs2.exists(_.stripReadOnly eq ref)
35
- common(refs1, refs2 ) ++ common(refs2, refs1 )
35
+ common(refs, other ) ++ common(other, refs )
36
36
37
- private def hidden (elem : CaptureRef )(using Context ): CaptureSet .Refs = elem match
38
- case Fresh .Cap (hcs) => hcs.elems.filter(! _.isRootCapability) ++ hidden(hcs)
39
- case ReadOnlyCapability (ref) => hidden(ref).map(_.readOnly)
40
- case _ => emptySet
41
-
42
- private def hidden (cs : CaptureSet )(using Context ): CaptureSet .Refs =
37
+ private def hidden (refs : Refs )(using Context ): Refs =
43
38
val seen : util.EqHashSet [CaptureRef ] = new util.EqHashSet
44
39
45
- def hiddenByElem (elem : CaptureRef ): CaptureSet . Refs =
40
+ def hiddenByElem (elem : CaptureRef ): Refs =
46
41
if seen.add(elem) then elem match
47
- case Fresh .Cap (hcs) => hcs.elems.filter(! _.isRootCapability) ++ recur(hcs)
42
+ case Fresh .Cap (hcs) => hcs.elems.filter(! _.isRootCapability) ++ recur(hcs.elems )
48
43
case ReadOnlyCapability (ref) => hiddenByElem(ref).map(_.readOnly)
49
44
case _ => emptySet
50
45
else emptySet
51
46
52
- def recur (cs : CaptureSet ): CaptureSet . Refs =
53
- (emptySet /: cs.elems ): (elems, elem) =>
47
+ def recur (cs : Refs ): Refs =
48
+ (emptySet /: cs): (elems, elem) =>
54
49
elems ++ hiddenByElem(elem)
55
50
56
- recur(cs )
51
+ recur(refs )
57
52
end hidden
58
53
59
54
/** The captures of an argument or prefix widened to the formal parameter, if
60
55
* the latter contains a cap.
61
56
*/
62
- def formalCaptures (arg : Tree )(using Context ): CaptureSet . Const =
57
+ def formalCaptures (arg : Tree )(using Context ): Refs =
63
58
val argType = arg.nuType
64
59
(if argType.hasUseAnnot then argType.deepCaptureSet else argType.captureSet)
65
- .toConst
60
+ .elems
66
61
67
62
/** The captures of an argument of prefix. No widening takes place */
68
- def actualCaptures (arg : Tree )(using Context ): CaptureSet . Const =
63
+ def actualCaptures (arg : Tree )(using Context ): Refs =
69
64
val argType = arg.actualType.orElse(arg.nuType)
70
65
(if arg.nuType.hasUseAnnot then argType.deepCaptureSet else argType.captureSet)
71
- .toConst
66
+ .elems
72
67
73
68
private def sepError (fn : Tree , args : List [Tree ], argIdx : Int ,
74
- overlap : Refs , hiddenInArg : CaptureSet , footprints : List [(CaptureSet , Int )],
69
+ overlap : Refs , hiddenInArg : Refs , footprints : List [(Refs , Int )],
75
70
deps : collection.Map [Tree , List [Tree ]])(using Context ): Unit =
76
71
val arg = args(argIdx)
77
72
def paramName (mt : Type , idx : Int ): Option [Name ] = mt match
@@ -102,53 +97,48 @@ class SepChecker(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser:
102
97
def clashType =
103
98
clashTree.actualType.orElse(clashTree.nuType)
104
99
def clashCaptures = actualCaptures(clashTree)
105
- def clashHidden = CaptureSet (hidden(formalCaptures(clashTree)))
106
- def hiddenCaptures = CaptureSet (hidden(formalCaptures(arg)))
100
+ def hiddenCaptures = hidden(formalCaptures(arg))
107
101
def clashFootprint = clashCaptures.footprint
108
102
def hiddenFootprint = hiddenCaptures.footprint
109
- def declaredFootprint = CaptureSet (deps(arg).map(actualCaptures(_).elems).foldLeft(emptySet)(_ ++ _)).footprint
110
- def footprintOverlap = CaptureSet (hiddenFootprint.overlapWith(clashFootprint) -- declaredFootprint.elems)
111
- def clashHiddenStr =
112
- if clashTree.needsSepCheck then
113
- i " \n Hidden set of $whereStr : $clashHidden"
114
- else " "
103
+ def declaredFootprint = deps(arg).map(actualCaptures(_)).foldLeft(emptySet)(_ ++ _).footprint
104
+ def footprintOverlap = hiddenFootprint.overlapWith(clashFootprint) -- declaredFootprint
115
105
report.error(
116
106
em """ Separation failure: argument of type ${arg.actualType}
117
107
|to $funStr
118
108
|corresponds to capture-polymorphic formal parameter ${formalName}of type ${arg.nuType}
119
109
|and captures ${CaptureSet (overlap)}, but $whatStr also passed separately
120
110
|in the ${whereStr.trim} with type $clashType.
121
111
|
122
- | Capture set of $whereStr : $clashCaptures
123
- | Hidden set of current argument : $hiddenCaptures
124
- | Footprint of $whereStr : $clashFootprint
125
- | Hidden footprint of current argument : $hiddenFootprint
126
- | Declared footprint of current argument: $declaredFootprint
127
- | Undeclared overlap of footprints : $footprintOverlap""" ,
112
+ | Capture set of $whereStr : ${ CaptureSet ( clashCaptures)}
113
+ | Hidden set of current argument : ${ CaptureSet ( hiddenCaptures)}
114
+ | Footprint of $whereStr : ${ CaptureSet ( clashFootprint)}
115
+ | Hidden footprint of current argument : ${ CaptureSet ( hiddenFootprint)}
116
+ | Declared footprint of current argument: ${ CaptureSet ( declaredFootprint)}
117
+ | Undeclared overlap of footprints : ${ CaptureSet ( footprintOverlap)} """ ,
128
118
arg.srcPos)
129
119
end sepError
130
120
131
121
private def checkApply (fn : Tree , args : List [Tree ], deps : collection.Map [Tree , List [Tree ]])(using Context ): Unit =
132
122
val fnCaptures = methPart(fn) match
133
123
case Select (qual, _) => qual.nuType.captureSet
134
124
case _ => CaptureSet .empty
135
- capt.println(i " check separate $fn( $args), fnCaptures = $fnCaptures, argCaptures = ${args.map(formalCaptures)}, deps = ${deps.toList}" )
136
- var footprint = fnCaptures.footprint
137
- val footprints = mutable.ListBuffer [(CaptureSet , Int )]((footprint, 0 ))
125
+ capt.println(i " check separate $fn( $args), fnCaptures = $fnCaptures, argCaptures = ${args.map(arg => CaptureSet ( formalCaptures(arg)) )}, deps = ${deps.toList}" )
126
+ var footprint = fnCaptures.elems. footprint
127
+ val footprints = mutable.ListBuffer [(Refs , Int )]((footprint, 0 ))
138
128
val indexedArgs = args.zipWithIndex
139
129
140
130
def subtractDeps (elems : Refs , arg : Tree ): Refs =
141
131
deps(arg).foldLeft(elems): (elems, dep) =>
142
- elems -- actualCaptures(dep).footprint.elems
132
+ elems -- actualCaptures(dep).footprint
143
133
144
134
for (arg, idx) <- indexedArgs do
145
135
if ! arg.needsSepCheck then
146
- footprint = footprint ++ CaptureSet ( subtractDeps(actualCaptures(arg).footprint.elems , arg) )
136
+ footprint = footprint ++ subtractDeps(actualCaptures(arg).footprint, arg)
147
137
footprints += ((footprint, idx + 1 ))
148
138
for (arg, idx) <- indexedArgs do
149
139
if arg.needsSepCheck then
150
140
val ac = formalCaptures(arg)
151
- val hiddenInArg = CaptureSet ( hidden(ac) ).footprint
141
+ val hiddenInArg = hidden(ac).footprint
152
142
// println(i"check sep $arg: $ac, footprint so far = $footprint, hidden = $hiddenInArg")
153
143
val overlap = subtractDeps(hiddenInArg.overlapWith(footprint), arg)
154
144
if ! overlap.isEmpty then
0 commit comments