Skip to content

Commit

Permalink
Exclusive capabilities (#22218)
Browse files Browse the repository at this point in the history
implement capybara-like mutation checking

 - [x]  Add read-only capabilities `x.rd`
- [x] Add `Mutable` and `SharedCapability` as subclasses of
`Capability`.
 - [x]  Add update methods.
- [x] Implement access rules for `Mutable` types - exclusive if they can
invoke an update method, read-only otherwise.
- [x] Add `Fresh.Cap` as a family of new top-types that keep track of
references that were widened to them
- [x] Add a separation checker that checks that references hidden by a
`Fresh.Cap` don't appear as aliases
     - [x] In applications
     - [x] In sequences of statements and definitions
     - [x] in the same type
 - [x] Introduce @consume annotation for parameters
- [x] Check that hidden references that are parameters are annotated
with `@consume`
- [x] Check that parameter references passed in arguments to @consume
parameters are also annotated with `@consume`.

To be done in a separate PR: Add qualifiers to capture sets so that we
can talk of the read-only part of a `Mutable` type.
  • Loading branch information
odersky authored Feb 5, 2025
2 parents aa9db1f + a41c10f commit a3dde8b
Show file tree
Hide file tree
Showing 156 changed files with 4,075 additions and 744 deletions.
Original file line number Diff line number Diff line change
Expand Up @@ -285,7 +285,7 @@ class BTypesFromSymbols[I <: DottyBackendInterface](val int: I, val frontendAcce
// tests/run/serialize.scala and https://github.com/typelevel/cats-effect/pull/2360).
val privateFlag = !sym.isClass && (sym.is(Private) || (sym.isPrimaryConstructor && sym.owner.isTopLevelModuleClass))

val finalFlag = sym.is(Final) && !toDenot(sym).isClassConstructor && !sym.is(Mutable, butNot = Accessor) && !sym.enclosingClass.is(Trait)
val finalFlag = sym.is(Final) && !toDenot(sym).isClassConstructor && !sym.isMutableVar && !sym.enclosingClass.is(Trait)

import asm.Opcodes.*
import GenBCodeOps.addFlagIf
Expand Down
2 changes: 2 additions & 0 deletions compiler/src/dotty/tools/dotc/ast/Desugar.scala
Original file line number Diff line number Diff line change
Expand Up @@ -2243,6 +2243,8 @@ object desugar {
New(ref(defn.RepeatedAnnot.typeRef), Nil :: Nil))
else if op.name == nme.CC_REACH then
Apply(ref(defn.Caps_reachCapability), t :: Nil)
else if op.name == nme.CC_READONLY then
Apply(ref(defn.Caps_readOnlyCapability), t :: Nil)
else
assert(ctx.mode.isExpr || ctx.reporter.errorsReported || ctx.mode.is(Mode.Interactive), ctx.mode)
Select(t, op.name)
Expand Down
2 changes: 1 addition & 1 deletion compiler/src/dotty/tools/dotc/ast/TreeInfo.scala
Original file line number Diff line number Diff line change
Expand Up @@ -755,7 +755,7 @@ trait TypedTreeInfo extends TreeInfo[Type] { self: Trees.Instance[Type] =>
*/
def isVariableOrGetter(tree: Tree)(using Context): Boolean = {
def sym = tree.symbol
def isVar = sym.is(Mutable)
def isVar = sym.isMutableVarOrAccessor
def isGetter =
mayBeVarGetter(sym) && sym.owner.info.member(sym.name.asTermName.setterName).exists

Expand Down
3 changes: 3 additions & 0 deletions compiler/src/dotty/tools/dotc/ast/untpd.scala
Original file line number Diff line number Diff line change
Expand Up @@ -206,6 +206,8 @@ object untpd extends Trees.Instance[Untyped] with UntypedTreeInfo {

case class Var()(implicit @constructorOnly src: SourceFile) extends Mod(Flags.Mutable)

case class Mut()(implicit @constructorOnly src: SourceFile) extends Mod(Flags.Mutable)

case class Implicit()(implicit @constructorOnly src: SourceFile) extends Mod(Flags.Implicit)

case class Given()(implicit @constructorOnly src: SourceFile) extends Mod(Flags.Given)
Expand Down Expand Up @@ -332,6 +334,7 @@ object untpd extends Trees.Instance[Untyped] with UntypedTreeInfo {

def isEnumCase: Boolean = isEnum && is(Case)
def isEnumClass: Boolean = isEnum && !is(Case)
def isMutableVar: Boolean = is(Mutable) && mods.exists(_.isInstanceOf[Mod.Var])
}

@sharable val EmptyModifiers: Modifiers = Modifiers()
Expand Down
Loading

0 comments on commit a3dde8b

Please sign in to comment.