diff --git a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala index 083d467a96a2..0803fc62578a 100644 --- a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala +++ b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala @@ -790,22 +790,64 @@ class CheckCaptures extends Recheck, SymTransformer: selType }//.showing(i"recheck sel $tree, $qualType = $result") - /** Recheck applications, with special handling of unsafeAssumePure. + /** Recheck `caps.unsafe.unsafeAssumePure(...)` */ + def applyAssumePure(tree: Apply, pt: Type)(using Context): Type = + val arg :: Nil = tree.args: @unchecked + val argType0 = recheck(arg, pt.stripCapturing.capturing(FreshCap(Origin.UnsafeAssumePure))) + val argType = + if argType0.captureSet.isAlwaysEmpty then argType0 + else argType0.widen.stripCapturing + capt.println(i"rechecking unsafeAssumePure of $arg with $pt: $argType") + super.recheckFinish(argType, tree, pt) + + /** Recheck `caps.freeze(...)`. + * + * Capture-check the body of a `freeze` operation and transforms its + * result to be immutable. + * + * `freeze` takes an operation of type `-> T`, where `T` is generic. + * It leverages the fact that the operation is pure, therefore the returned + * mutable types in `T` must be freshly created. It is thus safe to freeze the + * mutable parts in `T` into its immutable version. */ + def applyFreeze(tree: Apply)(using Context): Type = + val arg :: Nil = tree.args: @unchecked + def imm = new TypeMap: + def apply(t: Type) = t match + case t if variance <= 0 => + // Skip double-flip occurrences of mutable types. + // Example: tests/neg-custom-args/captures/freeze-double-flip.scala. + t + case t @ CapturingType(parent, refs) => + // If the capturing type is boxed, we skip it. Since it could capture + // existing values of a mutable type without charging anything to the + // operation passed to `freeze`. + val boxed = t.isBoxed + val parent1 = if boxed then parent else apply(parent) + val refs1 = + if !boxed && parent.derivesFromMutable && variance > 0 then + CaptureSet.emptyOfMutable + else refs + t.derivedCapturingType(parent1, refs1) + case _ => + mapOver(t) + val opProto = // () ?-> + defn.FunctionType(0, isContextual = true).appliedTo(WildcardType) + recheck(arg, opProto).stripCapturing match + case defn.ContextFunctionType(Nil, resType) => imm(resType) + + /** Recheck applications, with special handling of unsafeAssumePure, + * unsafeDiscardUses, and freeze. * More work is done in `recheckApplication`, `recheckArg` and `instantiate` below. */ override def recheckApply(tree: Apply, pt: Type)(using Context): Type = val meth = tree.fun.symbol if meth == defn.Caps_unsafeAssumePure then - val arg :: Nil = tree.args: @unchecked - val argType0 = recheck(arg, pt.stripCapturing.capturing(FreshCap(Origin.UnsafeAssumePure))) - val argType = - if argType0.captureSet.isAlwaysEmpty then argType0 - else argType0.widen.stripCapturing - capt.println(i"rechecking unsafeAssumePure of $arg with $pt: $argType") - super.recheckFinish(argType, tree, pt) + applyAssumePure(tree, pt) else if meth == defn.Caps_unsafeDiscardUses then val arg :: Nil = tree.args: @unchecked withDiscardedUses(recheck(arg, pt)) + else if meth == defn.Caps_freeze then + applyFreeze(tree) else val res = super.recheckApply(tree, pt) includeCallCaptures(meth, res, tree) diff --git a/compiler/src/dotty/tools/dotc/core/Definitions.scala b/compiler/src/dotty/tools/dotc/core/Definitions.scala index d2e4348c96fc..74383308e182 100644 --- a/compiler/src/dotty/tools/dotc/core/Definitions.scala +++ b/compiler/src/dotty/tools/dotc/core/Definitions.scala @@ -1031,6 +1031,7 @@ class Definitions { @tu lazy val Caps_ContainsTrait: TypeSymbol = CapsModule.requiredType("Contains") @tu lazy val Caps_ContainsModule: Symbol = requiredModule("scala.caps.Contains") @tu lazy val Caps_containsImpl: TermSymbol = Caps_ContainsModule.requiredMethod("containsImpl") + @tu lazy val Caps_freeze: TermSymbol = CapsModule.requiredMethod("freeze") @tu lazy val PureClass: ClassSymbol = requiredClass("scala.caps.Pure") @@ -2100,7 +2101,7 @@ class Definitions { RequiresCapabilityAnnot, captureRoot, Caps_CapSet, Caps_ContainsTrait, Caps_ContainsModule, Caps_ContainsModule.moduleClass, ConsumeAnnot, UseAnnot, ReserveAnnot, - CapsUnsafeModule, CapsUnsafeModule.moduleClass, + CapsUnsafeModule, CapsUnsafeModule.moduleClass, Caps_freeze, CapsInternalModule, CapsInternalModule.moduleClass, RetainsAnnot, RetainsCapAnnot, RetainsByNameAnnot) diff --git a/docs/_docs/reference/experimental/capture-checking/mutability.md b/docs/_docs/reference/experimental/capture-checking/mutability.md index 177dc7e18a23..bd30a51d7964 100644 --- a/docs/_docs/reference/experimental/capture-checking/mutability.md +++ b/docs/_docs/reference/experimental/capture-checking/mutability.md @@ -339,3 +339,34 @@ The subcapturing theory for sets is then as before, with the following additiona - `{x, ...}.RD = {x.rd, ...}.RD` - `{x.rd, ...} <: {x, ...}` +## The `freeze` Wrapper + +We often want to create a mutable data structure like an array, initialize by assigning to its elements and then return the array as an immutable type that does not +capture any capabilities. This can be achieved using the `freeze` wrapper. + +As an example, consider a class `Arr` which is modelled after `Array` and its immutable counterpart `IArr`: + +```scala +class Arr[T: reflect.ClassTag](len: Int) extends Mutable: + private val arr: Array[T] = new Array[T](len) + def get(i: Int): T = arr(i) + update def update(i: Int, x: T): Unit = arr(i) = x +type IArr[T] = Arr[T]^{} +``` + +The `freeze` wrapper allows us to go from an `Arr` to an `IArr`, safely: +```scala +import caps.freeze + +val f: IArr[String] = freeze: + val a = Arr[String](2) + a(0) = "hello" + a(1) = "world" + a +``` +The `freeze` method is defined in `caps` like this: +```scala +def freeze[T](op: -> T): T = op +``` +It takes a pure by-name parameter and returns its result. But the actual return type after capture checking is special. Instead of just `T` as in the declaration above suggests, it's `T` where every covariant occurrence of a `Mutable` type gets its capture set mapped to `{}`. + diff --git a/library/src/scala/caps/package.scala b/library/src/scala/caps/package.scala index 6fbb0a9a0f93..fc6c722df6b9 100644 --- a/library/src/scala/caps/package.scala +++ b/library/src/scala/caps/package.scala @@ -123,6 +123,7 @@ final class reserve extends annotation.StaticAnnotation * environment. */ @experimental +@deprecated(since = "3.8.0") final class use extends annotation.StaticAnnotation /** A trait that used to allow expressing existential types. Replaced by @@ -132,6 +133,12 @@ final class use extends annotation.StaticAnnotation @deprecated sealed trait Exists extends Capability +/** A wrapper that strips all covariant capture sets from Mutable types in the + * result of pure operation `op`, turning them into immutable types. + */ +@experimental +def freeze[T](op: -> T): T = op + @experimental object internal: diff --git a/project/MiMaFilters.scala b/project/MiMaFilters.scala index e45558f044b3..575a20af629a 100644 --- a/project/MiMaFilters.scala +++ b/project/MiMaFilters.scala @@ -32,6 +32,7 @@ object MiMaFilters { ProblemFilters.exclude[MissingClassProblem]("scala.caps.Classifier"), ProblemFilters.exclude[MissingClassProblem]("scala.caps.SharedCapability"), ProblemFilters.exclude[MissingClassProblem]("scala.caps.Control"), + ProblemFilters.exclude[DirectMissingMethodProblem]("scala.caps.package#package.freeze"), ), ) diff --git a/tests/neg-custom-args/captures/freeze-boxes.check b/tests/neg-custom-args/captures/freeze-boxes.check new file mode 100644 index 000000000000..ee8660ac3a66 --- /dev/null +++ b/tests/neg-custom-args/captures/freeze-boxes.check @@ -0,0 +1,35 @@ +-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/freeze-boxes.scala:22:4 ---------------------------------- +21 | val xs: Box[Ref^{}] = freeze: +22 | Box(a) // error + | ^ + | Found: Box[Ref^{a.rd}]^'s1 + | Required: Box[Ref^{}] + | + | Note that capability a.rd is not included in capture set {}. + | + | longer explanation available when compiling with `-explain` +-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/freeze-boxes.scala:36:4 ---------------------------------- +36 | a // error, sanity check + | ^ + | Found: () ?->{a} Ref^{a} + | Required: () ?-> + | + | Note that capability a is not included in capture set {}. + | + | longer explanation available when compiling with `-explain` +-- Error: tests/neg-custom-args/captures/freeze-boxes.scala:31:6 ------------------------------------------------------- +31 | par(() => a.set(42), () => println(b.get)) // error + | ^^^^^^^^^^^^^^^ + |Separation failure: argument of type () ->{a} Unit + |to method par: (op1: () => Unit, op2: () => Unit): Unit + |corresponds to capture-polymorphic formal parameter op1 of type () => Unit + |and hides capabilities {a}. + |Some of these overlap with the captures of the second argument with type () ->{b.rd} Unit. + | + | Hidden set of current argument : {a} + | Hidden footprint of current argument : {a} + | Capture set of second argument : {b.rd} + | Footprint set of second argument : {b.rd, a.rd} + | The two sets overlap at : {a} + | + |where: => refers to a fresh root capability created in method test2 when checking argument to parameter op1 of method par diff --git a/tests/neg-custom-args/captures/freeze-boxes.scala b/tests/neg-custom-args/captures/freeze-boxes.scala new file mode 100644 index 000000000000..99b0dcd876eb --- /dev/null +++ b/tests/neg-custom-args/captures/freeze-boxes.scala @@ -0,0 +1,37 @@ +import language.experimental.captureChecking +import language.experimental.separationChecking +import caps.{Mutable, freeze} + +// A mutable ref and its immutable version +class Ref extends Mutable: + private var data: Int = 0 + def get: Int = data + update def set(x: Int): Unit = data = x +def allocRef(): Ref^ = Ref() +type IRef = Ref^{} + +// Boxes +case class Box[+T](unbox: T) + +// Parallelism +def par(op1: () => Unit, op2: () => Unit): Unit = () + +def test1(): Unit = + val a = allocRef() + val xs: Box[Ref^{}] = freeze: + Box(a) // error + val b = xs.unbox + par(() => a.set(42), () => println(b.get)) + +def test2(): Unit = + val a = allocRef() + val xs = freeze: + Box(a) + val b = xs.unbox + par(() => a.set(42), () => println(b.get)) // error + +def test3(): Unit = + val a = allocRef() + val b = freeze: + a // error, sanity check + par(() => a.set(42), () => println(b.get)) diff --git a/tests/neg-custom-args/captures/freeze-double-flip.check b/tests/neg-custom-args/captures/freeze-double-flip.check new file mode 100644 index 000000000000..4203080b61b1 --- /dev/null +++ b/tests/neg-custom-args/captures/freeze-double-flip.check @@ -0,0 +1,13 @@ +-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/freeze-double-flip.scala:16:48 --------------------------- +16 | val reallybad: Ref^ -> Ref^{} = x => magic(x)(x => x) // error + | ^^^^^^ + |Found: (x: Ref^'s1) ->'s2 Ref^{x.rd} + |Required: Ref^ => Ref^{cap.rd} + | + |Note that capability x.rd is not included in capture set {cap.rd}. + | + |where: => refers to a fresh root capability created in anonymous function of type (x: Ref^): Ref^{} when checking argument to parameter x$0 of method apply + | ^ refers to the universal root capability + | cap is a fresh root capability created in anonymous function of type (x: Ref^): Ref^{} when checking argument to parameter x$0 of method apply + | + | longer explanation available when compiling with `-explain` diff --git a/tests/neg-custom-args/captures/freeze-double-flip.scala b/tests/neg-custom-args/captures/freeze-double-flip.scala new file mode 100644 index 000000000000..9e8a5b10787e --- /dev/null +++ b/tests/neg-custom-args/captures/freeze-double-flip.scala @@ -0,0 +1,16 @@ +import language.experimental.captureChecking +import language.experimental.separationChecking +import caps.{Mutable, freeze} + +// A mutable ref and its immutable version +class Ref extends Mutable: + private var data: Int = 0 + def get: Int = data + update def set(x: Int): Unit = data = x +def allocRef(): Ref^ = Ref() +type IRef = Ref^{} + +def test1(): Unit = + val magic = freeze: + (x: Ref^) => (op: Ref^ => IRef) => op(x) + val reallybad: Ref^ -> Ref^{} = x => magic(x)(x => x) // error diff --git a/tests/neg-custom-args/captures/freeze-tuple.check b/tests/neg-custom-args/captures/freeze-tuple.check new file mode 100644 index 000000000000..1fc47d2fd758 --- /dev/null +++ b/tests/neg-custom-args/captures/freeze-tuple.check @@ -0,0 +1,33 @@ +-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/freeze-tuple.scala:15:4 ---------------------------------- +14 | val (a, b) = freeze: +15 | val t1 = allocRef() // error + | ^ + | Capability cap outlives its scope: it leaks into outer capture set 's1 which is owned by value x1. + | The leakage occurred when trying to match the following types: + | + | Found: (Ref^{cap}, Ref^{cap²})^'s2 + | Required: (Ref^'s1, Ref^'s3)^'s4 + | + | where: cap and cap² refer to a root capability associated with the result type of (): (Ref^, Ref^²)^'s2 +16 | val t2 = allocRef() +17 | (t1, t2) + | + | longer explanation available when compiling with `-explain` +-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/freeze-tuple.scala:22:16 --------------------------------- +22 | val (a: Ref^{}, b: Ref^{}) = freeze: // error // error + | ^ + | Found: Ref^{a0.rd} + | Required: Ref^{} + | + | Note that capability a0.rd is not included in capture set {}. + | + | longer explanation available when compiling with `-explain` +-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/freeze-tuple.scala:22:27 --------------------------------- +22 | val (a: Ref^{}, b: Ref^{}) = freeze: // error // error + | ^ + | Found: Ref^{b0.rd} + | Required: Ref^{} + | + | Note that capability b0.rd is not included in capture set {}. + | + | longer explanation available when compiling with `-explain` diff --git a/tests/neg-custom-args/captures/freeze-tuple.scala b/tests/neg-custom-args/captures/freeze-tuple.scala new file mode 100644 index 000000000000..bd3b7cd034c7 --- /dev/null +++ b/tests/neg-custom-args/captures/freeze-tuple.scala @@ -0,0 +1,23 @@ +import language.experimental.captureChecking +import language.experimental.separationChecking +import caps.{Mutable, freeze} + +// A mutable ref and its immutable version +class Ref extends Mutable: + private var data: Int = 0 + def get: Int = data + update def set(x: Int): Unit = data = x +def allocRef(): Ref^ = Ref() +type IRef = Ref^{} + +def test1(): Unit = + val (a, b) = freeze: + val t1 = allocRef() // error + val t2 = allocRef() + (t1, t2) + +def test2(): Unit = + val a0 = allocRef() + val b0 = allocRef() + val (a: Ref^{}, b: Ref^{}) = freeze: // error // error + (a0, b0) diff --git a/tests/neg-custom-args/captures/freeze.check b/tests/neg-custom-args/captures/freeze.check new file mode 100644 index 000000000000..0be68f99acba --- /dev/null +++ b/tests/neg-custom-args/captures/freeze.check @@ -0,0 +1,19 @@ +-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/freeze.scala:19:4 ---------------------------------------- +18 | val a2 = freeze: +19 | val a = Arr[String](2) // error + | ^ + |Capability cap outlives its scope: it leaks into outer capture set 's1 of value a2. + |The leakage occurred when trying to match the following types: + | + |Found: (Arr[String]^{cap}, Arr[String]^{cap²})^'s2 + |Required: (Arr[String]^'s1, Arr[String]^'s3)^'s4 + | + |where: cap and cap² refer to a root capability associated with the result type of (): (Arr[String]^, Arr[String]^²)^'s2 +20 | val b = Arr[String](2) +21 | a(0) = "1" +22 | a(1) = "2" +23 | b(0) = "1" +24 | b(1) = "2" +25 | (a, b) + | + | longer explanation available when compiling with `-explain` diff --git a/tests/neg-custom-args/captures/freeze.scala b/tests/neg-custom-args/captures/freeze.scala new file mode 100644 index 000000000000..48f20edd2557 --- /dev/null +++ b/tests/neg-custom-args/captures/freeze.scala @@ -0,0 +1,26 @@ +import language.experimental.captureChecking +import caps.* + +class Arr[T: reflect.ClassTag](len: Int) extends Mutable: + private val arr: Array[T] = new Array[T](len) + def get(i: Int): T = arr(i) + update def update(i: Int, x: T): Unit = arr(i) = x + + +def test2 = + val a = freeze: + val a = Arr[String](2) + a(0) = "1" + a(1) = "2" + a + val _: Arr[String]^{} = a + + val a2 = freeze: + val a = Arr[String](2) // error + val b = Arr[String](2) + a(0) = "1" + a(1) = "2" + b(0) = "1" + b(1) = "2" + (a, b) + val _: (Arr[String]^{}, Arr[String]^{}) = a2 diff --git a/tests/pending/pos-custom-args/captures/freeze-cycle.scala b/tests/pending/pos-custom-args/captures/freeze-cycle.scala new file mode 100644 index 000000000000..043b59173ccb --- /dev/null +++ b/tests/pending/pos-custom-args/captures/freeze-cycle.scala @@ -0,0 +1,15 @@ +import caps.* + +class Node(val payload: Int) extends Mutable: + var next: Node = ??? + + +type INode = Node^{} + +def cycle(x: Int, y: Int): (INode, INode) = + freeze: + val a = Node(x) + val b = Node(y) + a.next = b + b.next = a + (a, b) diff --git a/tests/run-tasty-inspector/stdlibExperimentalDefinitions.scala b/tests/run-tasty-inspector/stdlibExperimentalDefinitions.scala index c249721f6a6d..cc9b002623a5 100644 --- a/tests/run-tasty-inspector/stdlibExperimentalDefinitions.scala +++ b/tests/run-tasty-inspector/stdlibExperimentalDefinitions.scala @@ -46,6 +46,7 @@ val experimentalDefinitionInLibrary = Set( "scala.caps.unsafe$", "scala.caps.use", "scala.caps.reserve", + "scala.caps.package$package$.freeze", "scala.caps.package$package$.Exclusive", "scala.caps.package$package$.Shared",