From 65a1301077c946ae6119acbdf4d4eb2be7bbd73b Mon Sep 17 00:00:00 2001 From: odersky Date: Wed, 29 Jan 2025 23:25:15 +0100 Subject: [PATCH] Check that @consumed prefix capabilities are not re-used Also: Fixes to computations of overlapWith and -- on Refs that take account of pathss, where shorter paths cover deeper ones. --- .../src/dotty/tools/dotc/cc/CaptureRef.scala | 26 ++ .../src/dotty/tools/dotc/cc/SepCheck.scala | 222 +++++++++++------- .../src/scala/collection/View.scala | 4 +- .../mutable/CheckedIndexedSeqView.scala | 28 +-- .../captures/linear-buffer-2.check | 29 +++ .../captures/linear-buffer-2.scala | 42 ++++ .../captures/linear-buffer.check | 20 +- .../captures/path-patmat-should-be-pos.scala | 4 +- .../captures/filter-iterable.scala | 11 + .../colltest5/CollectionStrawManCC5_1.scala | 8 +- 10 files changed, 280 insertions(+), 114 deletions(-) create mode 100644 tests/neg-custom-args/captures/linear-buffer-2.check create mode 100644 tests/neg-custom-args/captures/linear-buffer-2.scala create mode 100644 tests/pos-custom-args/captures/filter-iterable.scala diff --git a/compiler/src/dotty/tools/dotc/cc/CaptureRef.scala b/compiler/src/dotty/tools/dotc/cc/CaptureRef.scala index d969aa7f90db..f95722274258 100644 --- a/compiler/src/dotty/tools/dotc/cc/CaptureRef.scala +++ b/compiler/src/dotty/tools/dotc/cc/CaptureRef.scala @@ -259,6 +259,32 @@ trait CaptureRef extends TypeProxy, ValueType: case ReadOnlyCapability(y1) => this.stripReadOnly.maxSubsumes(y1, canAddHidden) case _ => false + /** `x covers y` if we should retain `y` when computing the overlap of + * two footprints which have `x` respectively `y` as elements. + * We assume that .rd have already been stripped on both sides. + * We have: + * + * x covers x + * x covers y ==> x covers y.f + * x covers y ==> x* covers y*, x? covers y? + * TODO what other clauses from subsumes do we need to port here? + */ + final def covers(y: CaptureRef)(using Context): Boolean = + (this eq y) + || y.match + case y @ TermRef(ypre: CaptureRef, _) if !y.isCap => + this.covers(ypre) + case ReachCapability(y1) => + this match + case ReachCapability(x1) => x1.covers(y1) + case _ => false + case MaybeCapability(y1) => + this match + case MaybeCapability(x1) => x1.covers(y1) + case _ => false + case _ => + false + def assumedContainsOf(x: TypeRef)(using Context): SimpleIdentitySet[CaptureRef] = CaptureSet.assumedContains.getOrElse(x, SimpleIdentitySet.empty) diff --git a/compiler/src/dotty/tools/dotc/cc/SepCheck.scala b/compiler/src/dotty/tools/dotc/cc/SepCheck.scala index a37f0b97d8d8..c2236e702fe4 100644 --- a/compiler/src/dotty/tools/dotc/cc/SepCheck.scala +++ b/compiler/src/dotty/tools/dotc/cc/SepCheck.scala @@ -30,15 +30,28 @@ object SepChecker: else NeedsCheck end Captures - /** The kind of checked type, used for composing error messages */ - enum TypeKind: + /** The role in which a checked type appears, used for composing error messages */ + enum TypeRole: case Result(sym: Symbol, inferred: Boolean) case Argument(arg: Tree) + case Qualifier(qual: Tree, meth: Symbol) + /** If this is a Result tole, the associated symbol, otherwise NoSymbol */ def dclSym = this match case Result(sym, _) => sym case _ => NoSymbol - end TypeKind + + /** A textual description of this role */ + def description(using Context): String = this match + case Result(sym, inferred) => + def inferredStr = if inferred then " inferred" else "" + def resultStr = if sym.info.isInstanceOf[MethodicType] then " result" else "" + i"$sym's$inferredStr$resultStr type" + case TypeRole.Argument(_) => + "the argument's adapted type" + case TypeRole.Qualifier(_, meth) => + i"the type of the qualifier to a call of $meth" + end TypeRole /** A class for segmented sets of consumed references. * References are associated with the source positions where they first appeared. @@ -161,10 +174,29 @@ class SepChecker(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser: private def overlapWith(other: Refs)(using Context): Refs = val refs1 = refs val refs2 = other + + /** Exclusive capabilities in refs1 that are covered by exclusive or + * stripped read-only capabilties in refs2 + * + stripped read-only capabilities in refs1 that are covered by an + * exclusive capability in refs2. + */ def common(refs1: Refs, refs2: Refs) = refs1.filter: ref => - ref.isExclusive && refs2.exists(_.stripReadOnly eq ref) + ref.isExclusive && refs2.exists(ref2 => ref2.stripReadOnly.covers(ref)) + ++ + refs1 + .filter: + case ReadOnlyCapability(ref @ TermRef(prefix: CaptureRef, _)) => + // We can get away testing only references with at least one field selection + // here since stripped readOnly references that equal a reference in refs2 + // are added by the first clause of the symmetric call to common. + !ref.isCap && refs2.exists(ref2 => ref2.covers(prefix)) + case _ => + false + .map(_.stripReadOnly) + common(refs, other) ++ common(other, refs) + end overlapWith private def hidden(using Context): Refs = val seen: util.EqHashSet[CaptureRef] = new util.EqHashSet @@ -179,16 +211,20 @@ class SepChecker(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser: refs.exists: ref => !hiddenByElem(ref, _ => emptySet).isEmpty + private def deduct(others: Refs)(using Context): Refs = + refs.filter: ref => + !others.exists(_.covers(ref)) + /** Deduct the footprint of `sym` and `sym*` from `refs` */ - private def deductSym(sym: Symbol)(using Context) = + private def deductSym(sym: Symbol)(using Context): Refs = val ref = sym.termRef - if ref.isTrackableRef then refs -- CaptureSet(ref, ref.reach).elems.footprint + if ref.isTrackableRef then refs.deduct(CaptureSet(ref, ref.reach).elems.footprint) else refs /** Deduct the footprint of all captures of `deps` from `refs` */ private def deductCapturesOf(deps: List[Tree])(using Context): Refs = deps.foldLeft(refs): (refs, dep) => - refs -- captures(dep).footprint + refs.deduct(captures(dep).footprint) end extension private def hiddenByElem(ref: CaptureRef, recur: Refs => Refs)(using Context): Refs = ref match @@ -249,7 +285,7 @@ class SepChecker(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser: def clashFootprint = clashCaptures.footprint def hiddenFootprint = hiddenCaptures.footprint def declaredFootprint = deps(arg).map(captures(_)).foldLeft(emptySet)(_ ++ _).footprint - def footprintOverlap = hiddenFootprint.overlapWith(clashFootprint) -- declaredFootprint + def footprintOverlap = hiddenFootprint.overlapWith(clashFootprint).deduct(declaredFootprint) report.error( em"""Separation failure: argument of type ${arg.nuType} |to $funStr @@ -289,15 +325,15 @@ class SepChecker(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser: def consumeError(ref: CaptureRef, loc: SrcPos, pos: SrcPos)(using Context): Unit = report.error( - em"""Separation failure: Illegal access to $ref, - |which was passed to a @consume parameter on line ${loc.line + 1} + em"""Separation failure: Illegal access to $ref, which was passed to a + |@consume parameter or was used as a prefix to a @consume method on line ${loc.line + 1} |and therefore is no longer available.""", pos) def consumeInLoopError(ref: CaptureRef, pos: SrcPos)(using Context): Unit = report.error( - em"""Separation failure: $ref appears in a loop, - |therefore it cannot be passed to a @consume parameter.""", + em"""Separation failure: $ref appears in a loop, therefore it cannot + |be passed to a @consume parameter or be used as a prefix of a @consume method call.""", pos) private def checkApply(fn: Tree, args: List[Tree], deps: collection.Map[Tree, List[Tree]])(using Context): Unit = @@ -316,7 +352,7 @@ class SepChecker(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser: for (arg, idx) <- indexedArgs do if arg.needsSepCheck then val ac = formalCaptures(arg) - checkType(arg.formalType, arg.srcPos, TypeKind.Argument(arg)) + checkType(arg.formalType, arg.srcPos, TypeRole.Argument(arg)) val hiddenInArg = ac.hidden.footprint //println(i"check sep $arg: $ac, footprint so far = $footprint, hidden = $hiddenInArg") val overlap = hiddenInArg.overlapWith(footprint).deductCapturesOf(deps(arg)) @@ -331,7 +367,7 @@ class SepChecker(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser: resultType.get(sym) match case Some(tp) if !overlap.isEmpty => val declared = tp.captureSet.elems - overlap -- declared.footprint -- declared.hidden.footprint + overlap.deduct(declared.footprint).deduct(declared.hidden.footprint) case _ => overlap @@ -346,30 +382,79 @@ class SepChecker(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser: val pos = consumed.get(ref) if pos != null then consumeError(ref, pos, tree.srcPos) - def checkType(tpt: Tree, sym: Symbol)(using Context): Unit = - checkType(tpt.nuType, tpt.srcPos, - TypeKind.Result(sym, inferred = tpt.isInstanceOf[InferredTypeTree])) + def explicitRefs(tp: Type): Refs = tp match + case tp: (TermRef | ThisType) => SimpleIdentitySet(tp) + case AnnotatedType(parent, _) => explicitRefs(parent) + case AndType(tp1, tp2) => explicitRefs(tp1) ++ explicitRefs(tp2) + case OrType(tp1, tp2) => explicitRefs(tp1) ** explicitRefs(tp2) + case _ => emptySet - /** Check that all parts of type `tpe` are separated. */ - def checkType(tpe: Type, pos: SrcPos, kind: TypeKind)(using Context): Unit = + def prune(refs: Refs, tpe: Type, role: TypeRole)(using Context): Refs = + refs.deductSym(role.dclSym).deduct(explicitRefs(tpe)) - def typeDescr = kind match - case TypeKind.Result(sym, inferred) => - def inferredStr = if inferred then " inferred" else "" - def resultStr = if sym.info.isInstanceOf[MethodicType] then " result" else "" - i"$sym's$inferredStr$resultStr" - case TypeKind.Argument(_) => - "the argument's adapted" + def checkType(tpt: Tree, sym: Symbol)(using Context): Unit = + checkType(tpt.nuType, tpt.srcPos, + TypeRole.Result(sym, inferred = tpt.isInstanceOf[InferredTypeTree])) + + /** Check validity consumed references `refsToCheck`. The references are consumed + * because they are hidden in a Fresh.Cap result type or they are referred + * to in an argument to a @consume parameter or in a prefix of a @consume method -- + * which one applie is determined by the role parameter. + * @param refsToCheck the referencves to check + * @param tpe the type containing those references + * @param role the role in which the type apears + * @param descr a textual description of the type and its relationship with the checked reference + * @param pos position for error reporting + */ + def checkConsumedRefs(refsToCheck: Refs, tpe: Type, role: TypeRole, descr: => String, pos: SrcPos)(using Context) = + val badParams = mutable.ListBuffer[Symbol]() + def currentOwner = role.dclSym.orElse(ctx.owner) + for hiddenRef <- prune(refsToCheck, tpe, role) do + val proot = hiddenRef.pathRoot + if !proot.widen.derivesFrom(defn.Caps_SharedCapability) then + proot match + case ref: TermRef => + val refSym = ref.symbol + if currentOwner.enclosingMethodOrClass.isProperlyContainedIn(refSym.maybeOwner.enclosingMethodOrClass) then + report.error(em"""Separation failure: $descr non-local $refSym""", pos) + else if refSym.is(TermParam) + && !refSym.hasAnnotation(defn.ConsumeAnnot) + && currentOwner.isContainedIn(refSym.owner) + then + badParams += refSym + case ref: ThisType => + val encl = currentOwner.enclosingMethodOrClass + if encl.isProperlyContainedIn(ref.cls) + && !encl.is(Synthetic) + && !encl.hasAnnotation(defn.ConsumeAnnot) + then + report.error( + em"""Separation failure: $descr non-local this of class ${ref.cls}. + |The access must be in a @consume method to allow this.""", + pos) + case _ => - def explicitRefs(tp: Type): Refs = tp match - case tp: (TermRef | ThisType) => SimpleIdentitySet(tp) - case AnnotatedType(parent, _) => explicitRefs(parent) - case AndType(tp1, tp2) => explicitRefs(tp1) ++ explicitRefs(tp2) - case OrType(tp1, tp2) => explicitRefs(tp1) ** explicitRefs(tp2) - case _ => emptySet + if badParams.nonEmpty then + def paramsStr(params: List[Symbol]): String = (params: @unchecked) match + case p :: Nil => i"${p.name}" + case p :: p2 :: Nil => i"${p.name} and ${p2.name}" + case p :: ps => i"${p.name}, ${paramsStr(ps)}" + val (pluralS, singleS) = if badParams.tail.isEmpty then ("", "s") else ("s", "") + report.error( + em"""Separation failure: $descr parameter$pluralS ${paramsStr(badParams.toList)}. + |The parameter$pluralS need$singleS to be annotated with @consume to allow this.""", + pos) + + role match + case _: TypeRole.Argument | _: TypeRole.Qualifier => + for ref <- refsToCheck do + if !ref.derivesFrom(defn.Caps_SharedCapability) then + consumed.put(ref, pos) + case _ => + end checkConsumedRefs - def prune(refs: Refs): Refs = - refs.deductSym(kind.dclSym) -- explicitRefs(tpe) + /** Check that all parts of type `tpe` are separated. */ + def checkType(tpe: Type, pos: SrcPos, role: TypeRole)(using Context): Unit = def checkParts(parts: List[Type]): Unit = var footprint: Refs = emptySet @@ -391,21 +476,21 @@ class SepChecker(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser: if !globalOverlap.isEmpty then val (prevStr, prevRefs, overlap) = parts.iterator.take(checked) .map: prev => - val prevRefs = prune(mapRefs(prev.deepCaptureSet.elems).footprint) + val prevRefs = prune(mapRefs(prev.deepCaptureSet.elems).footprint, tpe, role) (i", $prev , ", prevRefs, prevRefs.overlapWith(next)) .dropWhile(_._3.isEmpty) .nextOption .getOrElse(("", current, globalOverlap)) report.error( - em"""Separation failure in $typeDescr type $tpe. + em"""Separation failure in ${role.description} $tpe. |One part, $part , $nextRel ${CaptureSet(next)}. |A previous part$prevStr $prevRel ${CaptureSet(prevRefs)}. |The two sets overlap at ${CaptureSet(overlap)}.""", pos) val partRefs = part.deepCaptureSet.elems - val partFootprint = prune(partRefs.footprint) - val partHidden = prune(partRefs.hidden.footprint) -- partFootprint + val partFootprint = prune(partRefs.footprint, tpe, role) + val partHidden = prune(partRefs.hidden.footprint, tpe, role).deduct(partFootprint) checkSep(footprint, partHidden, identity, "references", "hides") checkSep(hiddenSet, partHidden, _.hidden, "also hides", "hides") @@ -451,47 +536,8 @@ class SepChecker(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser: case t => foldOver(c, t) - def checkRefs(refsToCheck: Refs, descr: => String) = - val badParams = mutable.ListBuffer[Symbol]() - def currentOwner = kind.dclSym.orElse(ctx.owner) - for hiddenRef <- prune(refsToCheck) do - val proot = hiddenRef.pathRoot - if !proot.widen.derivesFrom(defn.Caps_SharedCapability) then - proot match - case ref: TermRef => - val refSym = ref.symbol - if currentOwner.enclosingMethodOrClass.isProperlyContainedIn(refSym.maybeOwner.enclosingMethodOrClass) then - report.error(em"""Separation failure: $descr non-local $refSym""", pos) - else if refSym.is(TermParam) - && !refSym.hasAnnotation(defn.ConsumeAnnot) - && currentOwner.isContainedIn(refSym.owner) - then - badParams += refSym - case ref: ThisType => - val encl = currentOwner.enclosingMethodOrClass - if encl.isProperlyContainedIn(ref.cls) - && !encl.is(Synthetic) - && !encl.hasAnnotation(defn.ConsumeAnnot) - then - report.error( - em"""Separation failure: $descr non-local this of class ${ref.cls}. - |The access must be in a @consume method to allow this.""", - pos) - case _ => - - if badParams.nonEmpty then - def paramsStr(params: List[Symbol]): String = (params: @unchecked) match - case p :: Nil => i"${p.name}" - case p :: p2 :: Nil => i"${p.name} and ${p2.name}" - case p :: ps => i"${p.name}, ${paramsStr(ps)}" - val (pluralS, singleS) = if badParams.tail.isEmpty then ("", "s") else ("s", "") - report.error( - em"""Separation failure: $descr parameter$pluralS ${paramsStr(badParams.toList)}. - |The parameter$pluralS need$singleS to be annotated with @consume to allow this.""", - pos) - - def checkLegalRefs() = kind match - case TypeKind.Result(sym, _) => + def checkLegalRefs() = role match + case TypeRole.Result(sym, _) => if !sym.isAnonymousFunction // we don't check return types of anonymous functions && !sym.is(Case) // We don't check so far binders in patterns since they // have inferred universal types. TODO come back to this; @@ -499,15 +545,13 @@ class SepChecker(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser: // "see through them" when we look at hidden sets. then val refs = tpe.deepCaptureSet.elems - val toCheck = refs.hidden.footprint -- refs.footprint - checkRefs(toCheck, i"$typeDescr type $tpe hides") - case TypeKind.Argument(arg) => + val toCheck = refs.hidden.footprint.deduct(refs.footprint) + checkConsumedRefs(toCheck, tpe, role, i"${role.description} $tpe hides", pos) + case TypeRole.Argument(arg) => if tpe.hasAnnotation(defn.ConsumeAnnot) then val capts = captures(arg).footprint - checkRefs(capts, i"argument to @consume parameter with type ${arg.nuType} refers to") - for ref <- capts do - if !ref.derivesFrom(defn.Caps_SharedCapability) then - consumed.put(ref, arg.srcPos) + checkConsumedRefs(capts, tpe, role, i"argument to @consume parameter with type ${arg.nuType} refers to", pos) + case _ => if !tpe.hasAnnotation(defn.UntrackedCapturesAnnot) then traverse(Captures.None, tpe) @@ -569,6 +613,12 @@ class SepChecker(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser: if isUnsafeAssumeSeparate(tree) then return checkUse(tree) tree match + case tree @ Select(qual, _) if tree.symbol.is(Method) && tree.symbol.hasAnnotation(defn.ConsumeAnnot) => + traverseChildren(tree) + checkConsumedRefs( + captures(qual).footprint, qual.nuType, + TypeRole.Qualifier(qual, tree.symbol), + i"call prefix of @consume ${tree.symbol} refers to", qual.srcPos) case tree: GenericApply => traverseChildren(tree) tree.tpe match diff --git a/scala2-library-cc/src/scala/collection/View.scala b/scala2-library-cc/src/scala/collection/View.scala index c5d582eb2a11..b30fa5e508fe 100644 --- a/scala2-library-cc/src/scala/collection/View.scala +++ b/scala2-library-cc/src/scala/collection/View.scala @@ -16,6 +16,7 @@ import scala.annotation.{nowarn, tailrec} import scala.collection.mutable.{ArrayBuffer, Builder} import scala.collection.immutable.LazyList import language.experimental.captureChecking +import caps.unsafe.unsafeAssumeSeparate /** Views are collections whose transformation operations are non strict: the resulting elements * are evaluated only when the view is effectively traversed (e.g. using `foreach` or `foldLeft`), @@ -151,7 +152,8 @@ object View extends IterableFactory[View] { def apply[A](underlying: Iterable[A]^, p: A => Boolean, isFlipped: Boolean): Filter[A]^{underlying, p} = underlying match { case filter: Filter[A]^{underlying} if filter.isFlipped == isFlipped => - new Filter(filter.underlying, a => filter.p(a) && p(a), isFlipped) + unsafeAssumeSeparate: + new Filter(filter.underlying, a => filter.p(a) && p(a), isFlipped) case _ => new Filter(underlying, p, isFlipped) } } diff --git a/scala2-library-cc/src/scala/collection/mutable/CheckedIndexedSeqView.scala b/scala2-library-cc/src/scala/collection/mutable/CheckedIndexedSeqView.scala index 9ce0399e0662..7bfda7972762 100644 --- a/scala2-library-cc/src/scala/collection/mutable/CheckedIndexedSeqView.scala +++ b/scala2-library-cc/src/scala/collection/mutable/CheckedIndexedSeqView.scala @@ -17,7 +17,7 @@ import language.experimental.captureChecking private[mutable] trait CheckedIndexedSeqView[+A] extends IndexedSeqView[A] { - protected val mutationCount: () => Int + protected val mutationCount: () -> Int override def iterator: Iterator[A]^{this} = new CheckedIndexedSeqView.CheckedIterator(this, mutationCount()) override def reverseIterator: Iterator[A]^{this} = new CheckedIndexedSeqView.CheckedReverseIterator(this, mutationCount()) @@ -42,7 +42,7 @@ private[mutable] object CheckedIndexedSeqView { import IndexedSeqView.SomeIndexedSeqOps @SerialVersionUID(3L) - private[mutable] class CheckedIterator[A](self: IndexedSeqView[A]^, mutationCount: => Int) + private[mutable] class CheckedIterator[A](self: IndexedSeqView[A]^, mutationCount: -> Int) extends IndexedSeqView.IndexedSeqViewIterator[A](self) { private[this] val expectedCount = mutationCount override def hasNext: Boolean = { @@ -52,7 +52,7 @@ private[mutable] object CheckedIndexedSeqView { } @SerialVersionUID(3L) - private[mutable] class CheckedReverseIterator[A](self: IndexedSeqView[A]^, mutationCount: => Int) + private[mutable] class CheckedReverseIterator[A](self: IndexedSeqView[A]^, mutationCount: -> Int) extends IndexedSeqView.IndexedSeqViewReverseIterator[A](self) { private[this] val expectedCount = mutationCount override def hasNext: Boolean = { @@ -62,43 +62,43 @@ private[mutable] object CheckedIndexedSeqView { } @SerialVersionUID(3L) - class Id[+A](underlying: SomeIndexedSeqOps[A]^)(protected val mutationCount: () => Int) + class Id[+A](underlying: SomeIndexedSeqOps[A]^)(protected val mutationCount: () -> Int) extends IndexedSeqView.Id(underlying) with CheckedIndexedSeqView[A] @SerialVersionUID(3L) - class Appended[+A](underlying: SomeIndexedSeqOps[A]^, elem: A)(protected val mutationCount: () => Int) + class Appended[+A](underlying: SomeIndexedSeqOps[A]^, elem: A)(protected val mutationCount: () -> Int) extends IndexedSeqView.Appended(underlying, elem) with CheckedIndexedSeqView[A] @SerialVersionUID(3L) - class Prepended[+A](elem: A, underlying: SomeIndexedSeqOps[A]^)(protected val mutationCount: () => Int) + class Prepended[+A](elem: A, underlying: SomeIndexedSeqOps[A]^)(protected val mutationCount: () -> Int) extends IndexedSeqView.Prepended(elem, underlying) with CheckedIndexedSeqView[A] @SerialVersionUID(3L) - class Concat[A](prefix: SomeIndexedSeqOps[A]^, suffix: SomeIndexedSeqOps[A]^)(protected val mutationCount: () => Int) + class Concat[A](prefix: SomeIndexedSeqOps[A]^, suffix: SomeIndexedSeqOps[A]^)(protected val mutationCount: () -> Int) extends IndexedSeqView.Concat[A](prefix, suffix) with CheckedIndexedSeqView[A] @SerialVersionUID(3L) - class Take[A](underlying: SomeIndexedSeqOps[A]^, n: Int)(protected val mutationCount: () => Int) + class Take[A](underlying: SomeIndexedSeqOps[A]^, n: Int)(protected val mutationCount: () -> Int) extends IndexedSeqView.Take(underlying, n) with CheckedIndexedSeqView[A] @SerialVersionUID(3L) - class TakeRight[A](underlying: SomeIndexedSeqOps[A]^, n: Int)(protected val mutationCount: () => Int) + class TakeRight[A](underlying: SomeIndexedSeqOps[A]^, n: Int)(protected val mutationCount: () -> Int) extends IndexedSeqView.TakeRight(underlying, n) with CheckedIndexedSeqView[A] @SerialVersionUID(3L) - class Drop[A](underlying: SomeIndexedSeqOps[A]^, n: Int)(protected val mutationCount: () => Int) + class Drop[A](underlying: SomeIndexedSeqOps[A]^, n: Int)(protected val mutationCount: () -> Int) extends IndexedSeqView.Drop[A](underlying, n) with CheckedIndexedSeqView[A] @SerialVersionUID(3L) - class DropRight[A](underlying: SomeIndexedSeqOps[A]^, n: Int)(protected val mutationCount: () => Int) + class DropRight[A](underlying: SomeIndexedSeqOps[A]^, n: Int)(protected val mutationCount: () -> Int) extends IndexedSeqView.DropRight[A](underlying, n) with CheckedIndexedSeqView[A] @SerialVersionUID(3L) - class Map[A, B](underlying: SomeIndexedSeqOps[A]^, f: A => B)(protected val mutationCount: () => Int) + class Map[A, B](underlying: SomeIndexedSeqOps[A]^, f: A => B)(protected val mutationCount: () -> Int) extends IndexedSeqView.Map(underlying, f) with CheckedIndexedSeqView[B] @SerialVersionUID(3L) - class Reverse[A](underlying: SomeIndexedSeqOps[A]^)(protected val mutationCount: () => Int) + class Reverse[A](underlying: SomeIndexedSeqOps[A]^)(protected val mutationCount: () -> Int) extends IndexedSeqView.Reverse[A](underlying) with CheckedIndexedSeqView[A] { override def reverse: IndexedSeqView[A] = underlying match { case x: IndexedSeqView[A] => x @@ -107,7 +107,7 @@ private[mutable] object CheckedIndexedSeqView { } @SerialVersionUID(3L) - class Slice[A](underlying: SomeIndexedSeqOps[A]^, from: Int, until: Int)(protected val mutationCount: () => Int) + class Slice[A](underlying: SomeIndexedSeqOps[A]^, from: Int, until: Int)(protected val mutationCount: () -> Int) extends AbstractIndexedSeqView[A] with CheckedIndexedSeqView[A] { protected val lo = from max 0 protected val hi = (until max 0) min underlying.length diff --git a/tests/neg-custom-args/captures/linear-buffer-2.check b/tests/neg-custom-args/captures/linear-buffer-2.check new file mode 100644 index 000000000000..3d64c432d116 --- /dev/null +++ b/tests/neg-custom-args/captures/linear-buffer-2.check @@ -0,0 +1,29 @@ +-- Error: tests/neg-custom-args/captures/linear-buffer-2.scala:13:13 --------------------------------------------------- +13 | val buf3 = buf.append(3) // error + | ^^^ + | Separation failure: Illegal access to {buf} which is hidden by the previous definition + | of value buf1 with type Buffer[Int]^. + | This type hides capabilities {buf} +-- Error: tests/neg-custom-args/captures/linear-buffer-2.scala:20:13 --------------------------------------------------- +20 | val buf3 = buf1.append(4) // error + | ^^^^ + | Separation failure: Illegal access to (buf1 : Buffer[Int]^), which was passed to a + | @consume parameter or was used as a prefix to a @consume method on line 18 + | and therefore is no longer available. +-- Error: tests/neg-custom-args/captures/linear-buffer-2.scala:28:13 --------------------------------------------------- +28 | val buf3 = buf1.append(4) // error + | ^^^^ + | Separation failure: Illegal access to (buf1 : Buffer[Int]^), which was passed to a + | @consume parameter or was used as a prefix to a @consume method on line 25 + | and therefore is no longer available. +-- Error: tests/neg-custom-args/captures/linear-buffer-2.scala:38:13 --------------------------------------------------- +38 | val buf3 = buf1.append(4) // error + | ^^^^ + | Separation failure: Illegal access to (buf1 : Buffer[Int]^), which was passed to a + | @consume parameter or was used as a prefix to a @consume method on line 33 + | and therefore is no longer available. +-- Error: tests/neg-custom-args/captures/linear-buffer-2.scala:42:4 ---------------------------------------------------- +42 | buf.append(1) // error + | ^^^ + | Separation failure: (buf : Buffer[Int]^) appears in a loop, therefore it cannot + | be passed to a @consume parameter or be used as a prefix of a @consume method call. diff --git a/tests/neg-custom-args/captures/linear-buffer-2.scala b/tests/neg-custom-args/captures/linear-buffer-2.scala new file mode 100644 index 000000000000..428171c3fab8 --- /dev/null +++ b/tests/neg-custom-args/captures/linear-buffer-2.scala @@ -0,0 +1,42 @@ +import caps.{cap, consume, Mutable} +import language.experimental.captureChecking + +class Buffer[T] extends Mutable: + @consume mut def append(x: T): Buffer[T]^ = this // ok + +def app[T](@consume buf: Buffer[T]^, elem: T): Buffer[T]^ = + buf.append(elem) + +def Test(@consume buf: Buffer[Int]^) = + val buf1: Buffer[Int]^ = buf.append(1) + val buf2 = buf1.append(2) // OK + val buf3 = buf.append(3) // error + +def Test2(@consume buf: Buffer[Int]^) = + val buf1: Buffer[Int]^ = buf.append(1) + val buf2 = + if ??? then buf1.append(2) // OK + else buf1.append(3) // OK + val buf3 = buf1.append(4) // error + +def Test3(@consume buf: Buffer[Int]^) = + val buf1: Buffer[Int]^ = buf.append(1) + val buf2 = (??? : Int) match + case 1 => buf1.append(2) // OK + case 2 => buf1.append(2) + case _ => buf1.append(3) + val buf3 = buf1.append(4) // error + +def Test4(@consume buf: Buffer[Int]^) = + val buf1: Buffer[Int]^ = buf.append(1) + val buf2 = (??? : Int) match + case 1 => buf1.append(2) // OK + case 2 => buf1.append(2) + case 3 => buf1.append(3) + case 4 => buf1.append(4) + case 5 => buf1.append(5) + val buf3 = buf1.append(4) // error + +def Test5(@consume buf: Buffer[Int]^) = + while true do + buf.append(1) // error diff --git a/tests/neg-custom-args/captures/linear-buffer.check b/tests/neg-custom-args/captures/linear-buffer.check index a3a2c2c40fb4..16ba3bd096a2 100644 --- a/tests/neg-custom-args/captures/linear-buffer.check +++ b/tests/neg-custom-args/captures/linear-buffer.check @@ -16,29 +16,29 @@ -- Error: tests/neg-custom-args/captures/linear-buffer.scala:19:17 ----------------------------------------------------- 19 | val buf3 = app(buf, 3) // error | ^^^ - | Separation failure: Illegal access to (buf : Buffer[Int]^), - | which was passed to a @consume parameter on line 17 + | Separation failure: Illegal access to (buf : Buffer[Int]^), which was passed to a + | @consume parameter or was used as a prefix to a @consume method on line 17 | and therefore is no longer available. -- Error: tests/neg-custom-args/captures/linear-buffer.scala:26:17 ----------------------------------------------------- 26 | val buf3 = app(buf1, 4) // error | ^^^^ - | Separation failure: Illegal access to (buf1 : Buffer[Int]^), - | which was passed to a @consume parameter on line 24 + | Separation failure: Illegal access to (buf1 : Buffer[Int]^), which was passed to a + | @consume parameter or was used as a prefix to a @consume method on line 24 | and therefore is no longer available. -- Error: tests/neg-custom-args/captures/linear-buffer.scala:34:17 ----------------------------------------------------- 34 | val buf3 = app(buf1, 4) // error | ^^^^ - | Separation failure: Illegal access to (buf1 : Buffer[Int]^), - | which was passed to a @consume parameter on line 31 + | Separation failure: Illegal access to (buf1 : Buffer[Int]^), which was passed to a + | @consume parameter or was used as a prefix to a @consume method on line 31 | and therefore is no longer available. -- Error: tests/neg-custom-args/captures/linear-buffer.scala:44:17 ----------------------------------------------------- 44 | val buf3 = app(buf1, 4) // error | ^^^^ - | Separation failure: Illegal access to (buf1 : Buffer[Int]^), - | which was passed to a @consume parameter on line 39 + | Separation failure: Illegal access to (buf1 : Buffer[Int]^), which was passed to a + | @consume parameter or was used as a prefix to a @consume method on line 39 | and therefore is no longer available. -- Error: tests/neg-custom-args/captures/linear-buffer.scala:48:8 ------------------------------------------------------ 48 | app(buf, 1) // error | ^^^ - | Separation failure: (buf : Buffer[Int]^) appears in a loop, - | therefore it cannot be passed to a @consume parameter. + | Separation failure: (buf : Buffer[Int]^) appears in a loop, therefore it cannot + | be passed to a @consume parameter or be used as a prefix of a @consume method call. diff --git a/tests/neg-custom-args/captures/path-patmat-should-be-pos.scala b/tests/neg-custom-args/captures/path-patmat-should-be-pos.scala index aca6102204a3..5f434a21cc8b 100644 --- a/tests/neg-custom-args/captures/path-patmat-should-be-pos.scala +++ b/tests/neg-custom-args/captures/path-patmat-should-be-pos.scala @@ -1,6 +1,8 @@ +import caps.cap + class It[A] -class Filter[A](val underlying: It[A]^, val p: A => Boolean) extends It[A] +class Filter[A](val underlying: It[A]^, val p: A ->{cap, underlying} Boolean) extends It[A] object Filter: def apply[A](underlying: It[A]^, p: A => Boolean): Filter[A]^{underlying, p} = underlying match diff --git a/tests/pos-custom-args/captures/filter-iterable.scala b/tests/pos-custom-args/captures/filter-iterable.scala new file mode 100644 index 000000000000..c8e80af4cd73 --- /dev/null +++ b/tests/pos-custom-args/captures/filter-iterable.scala @@ -0,0 +1,11 @@ +import caps.cap + +class It[A] + +class Filter[A](val underlying: It[A]^, val p: A ->{cap, underlying} Boolean) extends It[A] +object Filter: + def apply[A](underlying: It[A]^, p: A => Boolean): Filter[A]^{cap, p, underlying} = + underlying match + case filter: Filter[A]^ => + val x = new Filter(filter.underlying, a => filter.p(a) && p(a)) + x: Filter[A]^{filter, p} \ No newline at end of file diff --git a/tests/run-custom-args/captures/colltest5/CollectionStrawManCC5_1.scala b/tests/run-custom-args/captures/colltest5/CollectionStrawManCC5_1.scala index 4281f7a21128..e12890a9be9b 100644 --- a/tests/run-custom-args/captures/colltest5/CollectionStrawManCC5_1.scala +++ b/tests/run-custom-args/captures/colltest5/CollectionStrawManCC5_1.scala @@ -7,7 +7,7 @@ import annotation.unchecked.{uncheckedVariance, uncheckedCaptures} import annotation.tailrec import caps.cap import caps.untrackedCaptures -import language.`3.7` // sepchecks on +import caps.unsafe.unsafeAssumeSeparate /** A strawman architecture for new collections. It contains some * example collection classes and methods with the intent to expose @@ -460,7 +460,11 @@ object CollectionStrawMan5 { def apply[A](underlying: Iterable[A]^, pp: A => Boolean, isFlipped: Boolean): Filter[A]^{underlying, pp} = underlying match case filter: Filter[A]^{underlying} => - new Filter(filter.underlying, a => filter.p(a) && pp(a)) + unsafeAssumeSeparate: + // See filter-iterable.scala for a test where a variant of Filter + // works without the unsafeAssumeSeparate. But it requires significant + // changes compared to the version here. + new Filter(filter.underlying, a => filter.p(a) && pp(a)) case _ => new Filter(underlying, pp) case class Partition[A](val underlying: Iterable[A]^, p: A => Boolean) {