Draft: Type Modifier Unification

src/main/scala/viper/gobra/ast/internal/PrettyPrinter.scala

@@ -9,7 +9,7 @@ package viper.gobra.ast.internal
 import org.bitbucket.inkytonik.kiama
 import org.bitbucket.inkytonik.kiama.util.Trampolines.Done
 import viper.gobra.ast.printing.PrettyPrinterCombinators
-import viper.gobra.theory.Addressability
+import viper.gobra.frontend.info.implementation.typing.modifiers.owner.OwnerModifier
 import viper.gobra.util.{Binary, Decimal, Hexadecimal, Octal}
 import viper.silver.ast.{Position => GobraPosition}
 
@@ -373,13 +373,13 @@ class DefaultPrettyPrinter extends PrettyPrinter with kiama.output.PrettyPrinter
   })
 
   def showBlockDecl(x: BlockDeclaration): Doc = x match {
-    case localVar: LocalVar => showVar(localVar) <> ":" <+> showType(localVar.typ) <> showAddressability(localVar.typ.addressability)
+    case localVar: LocalVar => showVar(localVar) <> ":" <+> showType(localVar.typ) <> showOwnerModifier(localVar.typ.ownerModifier)
     case l: LabelProxy => showProxy(l)
   }
 
-  def showAddressability(x: Addressability): Doc = x match {
-    case Addressability.Shared => "@"
-    case Addressability.Exclusive => "°"
+  def showOwnerModifier(x: OwnerModifier): Doc = x match {
+    case OwnerModifier.Shared => "@"
+    case OwnerModifier.Exclusive => "°"
   }
 
   protected def showStmtList[T <: Stmt](list: Vector[T]): Doc =

src/main/scala/viper/gobra/ast/internal/theory/Comparability.scala

@@ -7,7 +7,7 @@
 package viper.gobra.ast.internal.theory
 
 import viper.gobra.ast.internal._
-import viper.gobra.theory.Addressability
+import viper.gobra.frontend.info.implementation.typing.modifiers.owner.OwnerModifier
 import viper.gobra.util.RoseTree
 
 import scala.annotation.tailrec
@@ -38,7 +38,7 @@ object Comparability {
     case TypeHead.PointerHD => Kind.Comparable
 
     case t: TypeHead.DefinedHD =>
-      compareKind(TypeHead.typeHead(reg(DefinedT(t.name, Addressability.Exclusive))))(reg)
+      compareKind(TypeHead.typeHead(reg(DefinedT(t.name, OwnerModifier.Exclusive))))(reg)
 
     case _: TypeHead.StructHD => Kind.Recursive
     case _: TypeHead.FunctionHD => Kind.NonComparable

src/main/scala/viper/gobra/ast/internal/theory/TypeHead.scala

@@ -7,7 +7,7 @@
 package viper.gobra.ast.internal.theory
 
 import viper.gobra.ast.internal._
-import viper.gobra.theory.Addressability
+import viper.gobra.frontend.info.implementation.typing.modifiers.owner.OwnerModifier
 import viper.gobra.translator.Names
 import viper.gobra.util.RoseTree
 import viper.gobra.util.TypeBounds.IntegerKind
@@ -54,8 +54,8 @@ object TypeHead {
     RoseTree(typeHead(typ), children(typ) map typeTree)
 
   /** Returns a tree representation of the type where the addressability information is preserved. */
-  def typeTreeWithAddressability(typ: Type): RoseTree[(TypeHead, Addressability)] =
-    RoseTree((typeHead(typ), typ.addressability), children(typ) map typeTreeWithAddressability)
+  def typeTreeWithAddressability(typ: Type): RoseTree[(TypeHead, OwnerModifier)] =
+    RoseTree((typeHead(typ), typ.ownerModifier), children(typ) map typeTreeWithAddressability)
 
   /** Returns type-head representation of the argument type. */
   def typeHead(typ: Type): TypeHead = typ match {

src/main/scala/viper/gobra/frontend/info/ExternalTypeInfo.scala

@@ -14,8 +14,9 @@ import viper.gobra.frontend.info.base.Type.{AbstractType, InterfaceT, StructT, T
 import viper.gobra.frontend.info.base.SymbolTable
 import viper.gobra.frontend.info.base.SymbolTable.{Embbed, Field, MPredicateImpl, MPredicateSpec, MethodImpl, MethodSpec, Regular, TypeMember}
 import viper.gobra.frontend.info.implementation.resolution.{AdvancedMemberSet, MemberPath}
-import viper.gobra.frontend.info.implementation.typing.ghost.separation.GhostType
 import viper.gobra.reporting.VerifierError
+import viper.gobra.frontend.info.implementation.typing.modifiers.ghost.{GhostModifier, GhostType}
+import viper.gobra.frontend.info.implementation.typing.modifiers.owner.OwnerModifier
 
 trait ExternalTypeInfo {
 
@@ -41,8 +42,6 @@ trait ExternalTypeInfo {
     */
   def tryNonAddressableMethodLikeLookup(typ: Type, id: PIdnUse): Option[(TypeMember, Vector[MemberPath])]
 
-  def isParamGhost(param: PParameter): Boolean
-
   /**
     * Returns true if a symbol table lookup was made through `externalRegular` for the given member
     */
@@ -124,4 +123,8 @@ trait ExternalTypeInfo {
 
   /** returns all global variables declared in the same package as 'n' on which the declaration of 'n' depends */
   def samePkgDepsOfGlobalVar(n: SymbolTable.GlobalVariable): Vector[SymbolTable.GlobalVariable]
+
+  def getGhostModifier(n: PNode): GhostModifier
+
+  def getOwnerModifier(n: PNode): OwnerModifier
 }

src/main/scala/viper/gobra/frontend/info/Info.scala

@@ -18,7 +18,7 @@ import viper.gobra.frontend.PackageResolver.{AbstractImport, AbstractPackage, Bu
 import viper.gobra.frontend.Parser.{ParseResult, ParseSuccessResult}
 import viper.gobra.util.TaskManagerMode.{Lazy, Parallel, Sequential}
 import viper.gobra.frontend.info.implementation.TypeInfoImpl
-import viper.gobra.frontend.info.implementation.typing.ghost.separation.{GhostLessPrinter, GoifyingPrinter}
+import viper.gobra.frontend.info.implementation.typing.modifiers.ghost.{GhostLessPrinter, GoifyingPrinter}
 import viper.gobra.reporting.{CyclicImportError, ParserError, TypeCheckDebugMessage, TypeCheckFailureMessage, TypeCheckSuccessMessage, TypeError, VerifierError}
 import viper.gobra.util.{GobraExecutionContext, Job, TaskManager, Violation}
 
@@ -293,7 +293,7 @@ object Info extends LazyLogging {
   }
 
   private def getErasedGhostCode(pkg: PPackage, info: TypeInfoImpl): String = {
-    new GhostLessPrinter(info).format(pkg)
+    new GhostLessPrinter(info.ghostModifierUnit).format(pkg)
   }
 
   private def getGoifiedGhostCode(program: PPackage, info: TypeInfoImpl): String = {

src/main/scala/viper/gobra/frontend/info/TypeInfo.scala

@@ -11,13 +11,11 @@ import viper.gobra.ast.frontend._
 import viper.gobra.frontend.info.base.SymbolTable.{MethodImpl, MethodSpec, Regular, TypeMember}
 import viper.gobra.frontend.info.base.Type.{InterfaceT, Type}
 import viper.gobra.frontend.info.implementation.resolution.{AdvancedMemberSet, MemberPath}
-import viper.gobra.theory.Addressability
+import viper.gobra.frontend.info.implementation.typing.modifiers.owner.OwnerModifier
 
 trait TypeInfo extends ExternalTypeInfo {
 
   def typOfExprOrType(expr: PExpressionOrType): Type
-  def addressability(expr: PExpression): Addressability
-  def addressableVar(id: PIdnNode): Addressability
 
   def tree: Tree[PNode, PPackage]
 

src/main/scala/viper/gobra/frontend/info/base/SymbolTable.scala

@@ -92,15 +92,15 @@ object SymbolTable extends Environments[Entity] {
   }
 
   sealed trait Variable extends DataEntity {
-    def addressable: Boolean
+    def shared: Boolean
   }
 
   sealed trait ActualVariable extends Variable with ActualDataEntity
 
-  case class SingleLocalVariable(exp: Option[PExpression], opt: Option[PType], rep: PNode, ghost: Boolean, addressable: Boolean, context: ExternalTypeInfo) extends ActualVariable {
+  case class SingleLocalVariable(exp: Option[PExpression], opt: Option[PType], rep: PNode, ghost: Boolean, shared: Boolean, context: ExternalTypeInfo) extends ActualVariable {
     require(exp.isDefined || opt.isDefined)
   }
-  case class MultiLocalVariable(idx: Int, exp: PExpression, ghost: Boolean, addressable: Boolean, context: ExternalTypeInfo) extends ActualVariable {
+  case class MultiLocalVariable(idx: Int, exp: PExpression, ghost: Boolean, shared: Boolean, context: ExternalTypeInfo) extends ActualVariable {
     override def rep: PNode = exp
   }
 
@@ -110,7 +110,7 @@ object SymbolTable extends Environments[Entity] {
                             expOpt: Option[PExpression],
                             typOpt: Option[PType],
                             ghost: Boolean,
-                            override val addressable: Boolean,
+                            override val shared: Boolean,
                             isSingleModeDecl: Boolean,
                             context: ExternalTypeInfo
                            ) extends ActualVariable {
@@ -125,25 +125,25 @@ object SymbolTable extends Environments[Entity] {
     override def ghost: Boolean = false
   }
 
-  case class InParameter(decl: PNamedParameter, ghost: Boolean, addressable: Boolean, context: ExternalTypeInfo) extends ActualVariable {
+  case class InParameter(decl: PNamedParameter, ghost: Boolean, shared: Boolean, context: ExternalTypeInfo) extends ActualVariable {
     override def rep: PNode = decl
   }
-  case class ReceiverParameter(decl: PNamedReceiver, ghost: Boolean, addressable: Boolean, context: ExternalTypeInfo) extends ActualVariable {
+  case class ReceiverParameter(decl: PNamedReceiver, ghost: Boolean, shared: Boolean, context: ExternalTypeInfo) extends ActualVariable {
     override def rep: PNode = decl
   }
-  case class OutParameter(decl: PNamedParameter, ghost: Boolean, addressable: Boolean, context: ExternalTypeInfo) extends ActualVariable {
+  case class OutParameter(decl: PNamedParameter, ghost: Boolean, shared: Boolean, context: ExternalTypeInfo) extends ActualVariable {
     override def rep: PNode = decl
   }
-  case class TypeSwitchVariable(decl: PTypeSwitchStmt, ghost: Boolean, addressable: Boolean, context: ExternalTypeInfo) extends ActualVariable {
+  case class TypeSwitchVariable(decl: PTypeSwitchStmt, ghost: Boolean, shared: Boolean, context: ExternalTypeInfo) extends ActualVariable {
     override def rep: PNode = decl
     override def toString: String = decl.binder.fold("unknown")(_.toString)
   }
-  case class RangeVariable(idx: Int, exp: PRange, ghost: Boolean, addressable: Boolean, context: ExternalTypeInfo) extends ActualVariable {
+  case class RangeVariable(idx: Int, exp: PRange, ghost: Boolean, shared: Boolean, context: ExternalTypeInfo) extends ActualVariable {
     override def rep: PNode = exp
   }
 
   case class RangeEnumerateVariable(exp: PRange, ghost: Boolean, context: ExternalTypeInfo) extends ActualVariable {
-    override def addressable: Boolean = false
+    override def shared: Boolean = false
     override def rep: PNode = exp
   }
 
@@ -229,7 +229,7 @@ object SymbolTable extends Environments[Entity] {
 
   case class BoundVariable(decl: PBoundVariable, context: ExternalTypeInfo) extends GhostVariable {
     override def rep: PNode = decl
-    override def addressable: Boolean = false
+    override def shared: Boolean = false
   }
 
   sealed trait GhostTypeMember extends TypeMember with GhostRegular
@@ -258,7 +258,7 @@ object SymbolTable extends Environments[Entity] {
   case class MatchVariable(decl: PMatchBindVar, p: PNode, context: ExternalTypeInfo) extends GhostVariable {
     override def rep: PNode = decl
 
-    override def addressable: Boolean = false
+    override def shared: Boolean = false
   }
 
   case class AdtClause(decl: PAdtClause, adtDecl: PAdtType, context: ExternalTypeInfo) extends GhostRegular {

src/main/scala/viper/gobra/frontend/info/implementation/Errors.scala

@@ -34,9 +34,7 @@ trait Errors { this: TypeInfoImpl =>
           case _ => noMessages
         }
 
-        val ghostSeparated = wellGhostSeparated(m).out
-
-        wellDef ++ ghostSeparated
+        wellDef ++ wellDefModifiers(m).out
       }
 
       if (partialRes.isEmpty) {

src/main/scala/viper/gobra/frontend/info/implementation/TypeInfoImpl.scala

@@ -17,7 +17,7 @@ import viper.gobra.frontend.info.implementation.property._
 import viper.gobra.frontend.info.implementation.resolution.{AmbiguityResolution, Enclosing, LabelResolution, MemberPath, MemberResolution, NameResolution}
 import viper.gobra.frontend.info.implementation.typing._
 import viper.gobra.frontend.info.implementation.typing.ghost._
-import viper.gobra.frontend.info.implementation.typing.ghost.separation.GhostSeparation
+import viper.gobra.frontend.info.implementation.typing.modifiers.ghost.GhostModifier
 import viper.gobra.frontend.info.{ExternalTypeInfo, Info, TypeInfo}
 import viper.gobra.reporting.VerifierError
 
@@ -39,15 +39,15 @@ class TypeInfoImpl(final val tree: Info.GoTree, final val dependentTypeInfo: Map
   with IdTyping
   with MiscTyping
 
+  with ModifierTyping
+
   with GhostMemberTyping
   with GhostStmtTyping
   with GhostExprTyping
   with GhostTypeTyping
   with GhostIdTyping
   with GhostMiscTyping
 
-  with GhostSeparation
-
   with Convertibility
   with Comparability
   with DependencyAnalysis

src/main/scala/viper/gobra/frontend/info/implementation/property/Addressability.scala

@@ -11,9 +11,6 @@ import viper.gobra.frontend.info.base.SymbolTable.{Constant, GlobalVariable, Var
 import viper.gobra.frontend.info.base.Type.{ArrayT, GhostSliceT, MapT, MathMapT, SequenceT, SliceT, VariadicT}
 import viper.gobra.frontend.info.implementation.TypeInfoImpl
 import viper.gobra.ast.frontend.{AstPattern => ap}
-import viper.gobra.frontend.info.implementation.resolution.MemberPath
-import viper.gobra.theory.{Addressability => AddrMod}
-import viper.gobra.util.Violation
 
 trait Addressability extends BaseProperty { this: TypeInfoImpl =>
 
@@ -29,7 +26,7 @@ trait Addressability extends BaseProperty { this: TypeInfoImpl =>
 
   // depends on: entity, type
   lazy val addressable: Property[PExpression] = createBinaryProperty("addressable") {
-    n => addressability(n) == AddrMod.Shared
+    n => this.modifierUnits.forall(_.addressable(n))
   }
 
   /** checks if argument is addressable according to Go language specification */
@@ -47,93 +44,6 @@ trait Addressability extends BaseProperty { this: TypeInfoImpl =>
     case _ => false
   }
 
-  /** returns addressability modifier of argument expression. See [[viper.gobra.theory.Addressability]] */
-  override def addressability(expr: PExpression): AddrMod = addressabilityAttr(expr)
-
-  private lazy val addressabilityAttr: PExpression => AddrMod =
-    attr[PExpression, AddrMod] {
-      case PNamedOperand(id) => addressableVar(id)
-      case PBlankIdentifier() => AddrMod.defaultValue
-      case _: PTypeExpr => AddrMod.defaultValue
-      case _: PDeref => AddrMod.dereference
-      case PIndexedExp(base, _) =>
-        val baseType = underlyingType(exprType(base))
-        baseType match {
-          case _: SliceT | _: GhostSliceT => AddrMod.sliceLookup
-          case _: VariadicT => AddrMod.variadicLookup
-          case _: ArrayT => AddrMod.arrayLookup(addressability(base))
-          case _: SequenceT => AddrMod.mathDataStructureLookup
-          case _: MathMapT => AddrMod.mathDataStructureLookup
-          case _: MapT => AddrMod.mapLookup
-          case t => Violation.violation(s"Expected slice, array, map, or sequence, but got $t")
-        }
-      case n: PDot => resolve(n) match {
-        case Some(s: ap.FieldSelection) => AddrMod.fieldLookup(addressabilityMemberPath(addressability(s.base), s.path))
-        case Some(_: ap.Constant) => AddrMod.constant
-        case Some(_: ap.ReceivedMethod | _: ap.MethodExpr | _: ap.ReceivedPredicate | _: ap.PredicateExpr | _: ap.AdtField) => AddrMod.rValue
-        case Some(_: ap.NamedType | _: ap.BuiltInType | _: ap.Function | _: ap.Predicate | _: ap.DomainFunction) => AddrMod.rValue
-        case Some(_: ap.ImplicitlyReceivedInterfaceMethod | _: ap.ImplicitlyReceivedInterfacePredicate) => AddrMod.rValue
-        case Some(g: ap.GlobalVariable) => if (g.symb.addressable) AddrMod.Shared else AddrMod.Exclusive
-        case p => Violation.violation(s"Unexpected dot resolve, got $p")
-      }
-      case _: PLiteral => AddrMod.literal
-      case _: PIota => AddrMod.iota
-      case n: PInvoke => resolve(n) match {
-        case Some(_: ap.Conversion) => AddrMod.conversionResult
-        case Some(_: ap.FunctionCall) => AddrMod.callResult
-        case Some(_: ap.ClosureCall) => AddrMod.callResult
-        case Some(_: ap.PredicateCall) => AddrMod.rValue
-        case p => Violation.violation(s"Unexpected invoke resolve, got $p")
-      }
-      case _: PLength | _: PCapacity => AddrMod.callResult
-      case _: PSliceExp => AddrMod.sliceExpr
-      case _: PTypeAssertion => AddrMod.typeAssertionResult
-      case _: PReceive => AddrMod.receive
-      case _: PReference => AddrMod.reference
-      case _: PNegation => AddrMod.rValue
-      case _: PBitNegation => AddrMod.rValue
-      case _: PBinaryExp[_,_] => AddrMod.rValue
-      case _: PGhostEquals => AddrMod.rValue
-      case _: PGhostUnequals => AddrMod.rValue
-      case _: PPermission => AddrMod.rValue
-      case _: PPredConstructor => AddrMod.rValue
-      case n: PUnfolding => AddrMod.unfolding(addressability(n.op))
-      case _: POld | _: PLabeledOld | _: PBefore => AddrMod.old
-      case _: PConditional | _: PImplication | _: PForall | _: PExists => AddrMod.rValue
-      case _: PAccess | _: PPredicateAccess | _: PMagicWand => AddrMod.rValue
-      case _: PClosureImplements => AddrMod.rValue
-      case _: PTypeOf | _: PIsComparable => AddrMod.rValue
-      case _: PIn | _: PMultiplicity | _: PSequenceAppend |
-           _: PGhostCollectionExp | _: PRangeSequence | _: PUnion | _: PIntersection |
-           _: PSetMinus | _: PSubset | _: PMapKeys | _: PMapValues => AddrMod.rValue
-      case _: POptionNone | _: POptionSome | _: POptionGet => AddrMod.rValue
-      case _: PMatchExp => AddrMod.rValue
-      case _: PMake | _: PNew => AddrMod.make
-      case _: PUnpackSlice => AddrMod.rValue
-    }
-
-  def addressabilityMemberPath(base: AddrMod, path: Vector[MemberPath]): AddrMod = {
-    path.foldLeft(base){
-      case (b, MemberPath.Underlying) => b
-      case (b, _: MemberPath.Next) => AddrMod.fieldLookup(b)
-      case (b, _: MemberPath.EmbeddedInterface) => b
-      case (_, MemberPath.Deref) => AddrMod.dereference
-      case (_, MemberPath.Ref) => AddrMod.reference
-    }
-  }
-
-  /** returns addressability modifier of argument variable */
-  override def addressableVar(id: PIdnNode): AddrMod = addressableVarAttr(id)
-
-  private lazy val addressableVarAttr: PIdnNode => AddrMod =
-    attr[PIdnNode, AddrMod] { n => regular(n) match {
-      case g: GlobalVariable => if (g.addressable) AddrMod.sharedVariable else AddrMod.exclusiveVariable
-      case v: Variable => if (v.addressable) AddrMod.sharedVariable else AddrMod.exclusiveVariable
-      case _: Constant => AddrMod.constant
-      case _: Wildcard => AddrMod.defaultValue
-      case e => Violation.violation(s"Expected variable, but got $e")
-    }}
-
   /** a parameter can be used as shared if it is included in the shared clause of the enclosing function or method */
   lazy val canParameterBeUsedAsShared: PParameter => Boolean =
     attr[PParameter, Boolean] {