Add freeze wrapper (2) (#24518)

Revised version of #24423.

Based on #24495.

Author: odersky

compiler/src/dotty/tools/dotc/cc/CaptureOps.scala

@@ -398,6 +398,7 @@ extension (tp: Type)
   def derivesFromStateful(using Context): Boolean = derivesFromCapTrait(defn.Caps_Stateful)
   def derivesFromShared(using Context): Boolean = derivesFromCapTrait(defn.Caps_SharedCapability)
   def derivesFromUnscoped(using Context): Boolean = derivesFromCapTrait(defn.Caps_Unscoped)
+  def derivesFromMutable(using Context): Boolean = derivesFromCapTrait(defn.Caps_Mutable)
 
   /** Drop @retains annotations everywhere */
   def dropAllRetains(using Context): Type = // TODO we should drop retains from inferred types before unpickling

compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala

@@ -790,22 +790,29 @@ 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 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
+        freeze(super.recheckApply(tree, pt), tree.srcPos)
       else
         val res = super.recheckApply(tree, pt)
         includeCallCaptures(meth, res, tree)

compiler/src/dotty/tools/dotc/cc/Mutability.scala

@@ -7,6 +7,7 @@ import Symbols.*, Types.*, Flags.*, Contexts.*, Names.*, Decorators.*
 import Capabilities.*
 import util.SrcPos
 import config.Printers.capt
+import config.Feature
 import ast.tpd.Tree
 import typer.ProtoTypes.LhsProto
 
@@ -249,4 +250,22 @@ object Mutability:
       case improved =>
         improved
 
+  /** Apply `caps.freeze(...)`. Strip all capture sets of covariant Mutable
+   *  types, turning them into `CaptureSet.emptyOfMutable`. Only Mutable types
+   *  that contribute to the overall capture set are considered, since that is the
+   *  set analyzed by consume/use checking. That means that double-flip covariant
+   *  and boxed capture sets are not dropped.
+   */
+  def freeze(tp: Type, pos: SrcPos)(using Context): Type = tp.widen match
+    case tpw @ CapturingType(parent, refs)
+    if parent.derivesFromMutable && !tpw.isBoxed =>
+      if !Feature.enabled(Feature.separationChecking) then
+        report.warning(
+          em"""freeze is safe only if separation checking is enabled.
+              |You can enable separation checking with the language import
+              |
+              |   import language.experimental.separationChecking""",
+          pos)
+      tpw.derivedCapturingType(parent, CaptureSet.emptyOfStateful)
+    case _ => tp
 end Mutability

compiler/src/dotty/tools/dotc/core/Definitions.scala

@@ -1028,6 +1028,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")
 
@@ -2098,7 +2099,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)
 

docs/_docs/reference/experimental/capture-checking/mutability.md

@@ -444,3 +444,4 @@ The subcapturing theory for sets is then as before, with the following additiona
  - `C₁.reader <: C₂.reader` if `C₍ <: C₂`
  - `{x, ...}.reader = {x.rd, ...}.reader`
  - `{x.rd, ...} <: {x, ...}`
+

docs/_docs/reference/experimental/capture-checking/separation-checking.md

@@ -235,3 +235,36 @@ val c = b += 3
 ```
 This code is equivalent to functional append with `+`, and is at the same time more efficient since it re-uses the storage of the argument buffer.
 
+## 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] =
+  val a = Arr[String](2)
+  a(0) = "hello"
+  a(1) = "world"
+  freeze(a)
+```
+The `freeze` method is defined in `caps` like this:
+```scala
+def freeze(consume x: Mutable): x.type = x
+```
+It consumes a value of `Mutable` type with arbitrary capture set (since any capture set conforms to the implied `{cap.rd}`). The actual signature of
+`consume` declares that `x.type` is returned, but the actual return type after capture checking is special. Instead of `x.type` it is the underlying `Mutable` type with its top-level capture set
+mapped to `{}`. Applications of `freeze` are safe only if separation checking is enabled.
+

library/src/scala/caps/package.scala

@@ -141,6 +141,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
@@ -190,6 +191,12 @@ object internal:
 
 end internal
 
+/** 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(@internal.consume x: Mutable): x.type = x
+
 @experimental
 object unsafe:
   /** Two usages:

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"),
       ),
 
     )

tests/neg-custom-args/captures/boxed-consume.check

@@ -0,0 +1,12 @@
+-- Error: tests/neg-custom-args/captures/boxed-consume.scala:10:52 -----------------------------------------------------
+10 |  def h(consume x: (Object^, Object^)): Object^ = x._1  // error: local reach leak
+   |                                                  ^^^^
+   |                           Local reach capability x._1* leaks into capture scope of method h.
+   |                           You could try to abstract the capabilities referred to by x._1* in a capset variable.
+-- Error: tests/neg-custom-args/captures/boxed-consume.scala:16:10 -----------------------------------------------------
+16 |  println(d) // error
+   |          ^
+   |        Separation failure: Illegal access to (d : Object^), which was passed as a consume parameter to method g
+   |        on line 15 and therefore is no longer available.
+   |
+   |        where:    ^ refers to a fresh root capability in the type of value d

tests/neg-custom-args/captures/boxed-consume.scala

@@ -0,0 +1,22 @@
+import caps.*
+
+def Test =
+  val c: Object^ = "a"
+  val d: Object^ = "a"
+  val e1, e2: Object^ = "a"
+  val falseDeps: Object^ = "a"
+  def f[T](consume x: T): Unit = ()
+  def g(consume x: Object^): Unit = ()
+  def h(consume x: (Object^, Object^)): Object^ = x._1  // error: local reach leak
+  val cc = (c, c)
+  f(cc)  // no consume, it's boxed
+  f(c)   // no consume, it's boxed
+  println(c)  // ok
+  g(d)   // consume
+  println(d) // error
+  h((e1, e2))  // no consume, still boxed
+  println(e1)  // ok
+
+
+
+