|
| 1 | +package dotty.tools |
| 2 | +package dotc |
| 3 | +package cc |
| 4 | +import ast.tpd |
| 5 | +import collection.mutable |
| 6 | + |
| 7 | +import core.* |
| 8 | +import Symbols.*, Types.* |
| 9 | +import Contexts.*, Names.*, Flags.*, Symbols.*, Decorators.* |
| 10 | +import CaptureSet.{Refs, emptySet} |
| 11 | +import config.Printers.capt |
| 12 | +import StdNames.nme |
| 13 | + |
| 14 | +class SepChecker(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser: |
| 15 | + import tpd.* |
| 16 | + import checker.* |
| 17 | + |
| 18 | + extension (cs: CaptureSet) |
| 19 | + def footprint(using Context): CaptureSet = |
| 20 | + def recur(elems: CaptureSet.Refs, newElems: List[CaptureRef]): CaptureSet.Refs = newElems match |
| 21 | + case newElem :: newElems1 => |
| 22 | + val superElems = newElem.captureSetOfInfo.elems.filter: superElem => |
| 23 | + !superElem.isMaxCapability && !elems.contains(superElem) |
| 24 | + recur(superElems ++ elems, superElems.toList ++ newElems1) |
| 25 | + case Nil => elems |
| 26 | + val elems: CaptureSet.Refs = cs.elems.filter(!_.isMaxCapability) |
| 27 | + CaptureSet(recur(elems, elems.toList)) |
| 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) = |
| 33 | + refs1.filter: ref => |
| 34 | + ref.isExclusive && refs2.exists(_.stripReadOnly eq ref) |
| 35 | + common(refs1, refs2) ++ common(refs2, refs1) |
| 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 = |
| 43 | + val seen: util.EqHashSet[CaptureRef] = new util.EqHashSet |
| 44 | + |
| 45 | + def hiddenByElem(elem: CaptureRef): CaptureSet.Refs = |
| 46 | + if seen.add(elem) then elem match |
| 47 | + case Fresh.Cap(hcs) => hcs.elems.filter(!_.isRootCapability) ++ recur(hcs) |
| 48 | + case ReadOnlyCapability(ref) => hiddenByElem(ref).map(_.readOnly) |
| 49 | + case _ => emptySet |
| 50 | + else emptySet |
| 51 | + |
| 52 | + def recur(cs: CaptureSet): CaptureSet.Refs = |
| 53 | + (emptySet /: cs.elems): (elems, elem) => |
| 54 | + elems ++ hiddenByElem(elem) |
| 55 | + |
| 56 | + recur(cs) |
| 57 | + end hidden |
| 58 | + |
| 59 | + private def checkApply(fn: Tree, args: List[Tree])(using Context): Unit = |
| 60 | + val fnCaptures = fn.nuType.deepCaptureSet |
| 61 | + |
| 62 | + def captures(arg: Tree) = |
| 63 | + val argType = arg.nuType |
| 64 | + argType match |
| 65 | + case AnnotatedType(formal1, ann) if ann.symbol == defn.UseAnnot => |
| 66 | + argType.deepCaptureSet |
| 67 | + case _ => |
| 68 | + argType.captureSet |
| 69 | + |
| 70 | + val argCaptures = args.map(captures) |
| 71 | + capt.println(i"check separate $fn($args), fnCaptures = $fnCaptures, argCaptures = $argCaptures") |
| 72 | + var footprint = argCaptures.foldLeft(fnCaptures.footprint): (fp, ac) => |
| 73 | + fp ++ ac.footprint |
| 74 | + val paramNames = fn.nuType.widen match |
| 75 | + case MethodType(pnames) => pnames |
| 76 | + case _ => args.indices.map(nme.syntheticParamName(_)) |
| 77 | + for (arg, ac, pname) <- args.lazyZip(argCaptures).lazyZip(paramNames) do |
| 78 | + if arg.needsSepCheck then |
| 79 | + val hiddenInArg = CaptureSet(hidden(ac)) |
| 80 | + //println(i"check sep $arg / $footprint / $hiddenInArg") |
| 81 | + val overlap = hiddenInArg.footprint.overlapWith(footprint) |
| 82 | + if !overlap.isEmpty then |
| 83 | + def whatStr = if overlap.size == 1 then "this capability" else "these capabilities" |
| 84 | + def funStr = |
| 85 | + if fn.symbol.exists then i"${fn.symbol}" |
| 86 | + else "the function" |
| 87 | + report.error( |
| 88 | + em"""Separation failure: argument to capture-polymorphic parameter $pname: ${arg.nuType} |
| 89 | + |captures ${CaptureSet(overlap)} and also passes $whatStr separately to $funStr""", |
| 90 | + arg.srcPos) |
| 91 | + footprint ++= hiddenInArg |
| 92 | + |
| 93 | + private def traverseApply(tree: Tree, argss: List[List[Tree]])(using Context): Unit = tree match |
| 94 | + case Apply(fn, args) => traverseApply(fn, args :: argss) |
| 95 | + case TypeApply(fn, args) => traverseApply(fn, argss) // skip type arguments |
| 96 | + case _ => |
| 97 | + if argss.nestedExists(_.needsSepCheck) then |
| 98 | + checkApply(tree, argss.flatten) |
| 99 | + |
| 100 | + def traverse(tree: Tree)(using Context): Unit = |
| 101 | + tree match |
| 102 | + case tree: GenericApply => |
| 103 | + if tree.symbol != defn.Caps_unsafeAssumeSeparate then |
| 104 | + tree.tpe match |
| 105 | + case _: MethodOrPoly => |
| 106 | + case _ => traverseApply(tree, Nil) |
| 107 | + traverseChildren(tree) |
| 108 | + case _ => |
| 109 | + traverseChildren(tree) |
| 110 | +end SepChecker |
| 111 | + |
| 112 | + |
| 113 | + |
| 114 | + |
| 115 | + |
| 116 | + |
0 commit comments