adds support for method receivers of ghost pointer type, minimizes diff

src/main/scala/viper/gobra/ast/frontend/Ast.scala

@@ -731,19 +731,19 @@ case class PEmbeddedDecl(typ: PEmbeddedType, id: PIdnDef) extends PActualStructC
   require(id.name == typ.name)
 }
 
-sealed trait PMethodRecvType extends PActualType { // TODO: will have to be removed for packages
+sealed trait PMethodRecvType extends PType { // TODO: will have to be removed for packages
   def typ: PNamedOperand
 }
 
-case class PMethodReceiveName(typ: PNamedOperand) extends PMethodRecvType
+case class PMethodReceiveName(typ: PNamedOperand) extends PMethodRecvType with PActualType
 
 trait PMethodReceivePointer extends PMethodRecvType {
   def typ: PNamedOperand
 }
 
-case class PMethodReceiveActualPointer(typ: PNamedOperand) extends PMethodReceivePointer
+case class PMethodReceiveActualPointer(typ: PNamedOperand) extends PMethodReceivePointer with PActualType
 
-case class PMethodReceiveGhostPointer(typ: PNamedOperand) extends PMethodReceivePointer with PGhostNode
+case class PMethodReceiveGhostPointer(typ: PNamedOperand) extends PMethodReceivePointer with PGhostType
 
 // TODO: Named type is not allowed to be an interface
 

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

@@ -641,10 +641,7 @@ class DefaultPrettyPrinter extends PrettyPrinter with kiama.output.PrettyPrinter
           ssep(pspec map showInterfaceClause, line)
       )
     case PMethodReceiveName(t) => showType(t)
-    case r: PMethodReceivePointer => r match {
-      case PMethodReceiveActualPointer(t) => "*" <> showType(t)
-      case PMethodReceiveGhostPointer(t) => "gpointer" <> brackets(showType(t))
-    }
+    case PMethodReceiveActualPointer(t) => "*" <> showType(t)
   }
 
   def showGhostType(typ : PGhostType) : Doc = typ match {
@@ -660,6 +657,7 @@ class DefaultPrettyPrinter extends PrettyPrinter with kiama.output.PrettyPrinter
         ssep((funcs ++ axioms) map showMisc, line)
       )
     case PAdtType(clauses) => "adt" <> block(ssep(clauses map showMisc, line))
+    case PMethodReceiveGhostPointer(t) => "gpointer" <> brackets(showType(t))
   }
 
   def showStructClause(c: PStructClause): Doc = c match {

src/main/scala/viper/gobra/frontend/Desugar.scala

@@ -3750,7 +3750,7 @@ object Desugar extends LazyLogging {
         in.MapT(keysD, valuesD, addrMod)
       case Type.GhostSliceT(elem) => in.SliceT(typeD(elem, Addressability.sliceElement)(src), addrMod)
       case Type.OptionT(elem) => in.OptionT(typeD(elem, Addressability.mathDataStructureElement)(src), addrMod)
-      case p: Type.PointerT => registerType(in.PointerT(typeD(p.elem, Addressability.pointerBase)(src), addrMod))
+      case Type.PointerT(elem) => registerType(in.PointerT(typeD(elem, Addressability.pointerBase)(src), addrMod))
       case Type.ChannelT(elem, _) => in.ChannelT(typeD(elem, Addressability.channelElement)(src), addrMod)
       case Type.SequenceT(elem) => in.SequenceT(typeD(elem, Addressability.mathDataStructureElement)(src), addrMod)
       case Type.SetT(elem) => in.SetT(typeD(elem, Addressability.mathDataStructureElement)(src), addrMod)

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

@@ -9,7 +9,7 @@ package viper.gobra.frontend.info.implementation.property
 import viper.gobra.ast.frontend.{PDeref, PDot, PEmbeddedName, PEmbeddedPointer, PEmbeddedType, PInterfaceType, PNamedOperand, PStructType, PType, PTypeDecl}
 import viper.gobra.frontend.info.ExternalTypeInfo
 import viper.gobra.frontend.info.base.BuiltInMemberTag.BuiltInTypeTag
-import viper.gobra.frontend.info.base.Type.{ActualPointerT, BooleanT, ChannelT, DeclaredT, FunctionT, GhostSliceT, IntT, InterfaceT, MapT, NilType, PointerT, Single, SliceT, StringT, StructT, Type}
+import viper.gobra.frontend.info.base.Type.{BooleanT, ChannelT, DeclaredT, FunctionT, GhostSliceT, IntT, InterfaceT, MapT, NilType, PointerT, Single, SliceT, StringT, StructT, Type}
 import viper.gobra.frontend.info.base.{SymbolTable => st}
 import viper.gobra.frontend.info.implementation.TypeInfoImpl
 
@@ -65,7 +65,7 @@ trait UnderlyingType { this: TypeInfoImpl =>
   lazy val derefType: Type => Option[Type] =
     attr[Type, Option[Type]] {
       case Single(DeclaredT(t: PTypeDecl, context: ExternalTypeInfo)) => derefType(context.symbType(t.right))
-      case Single(p: PointerT) => Some(p.elem)
+      case Single(PointerT(elem)) => Some(elem)
       case _ => None
     }
 
@@ -200,7 +200,7 @@ trait UnderlyingType { this: TypeInfoImpl =>
 
   lazy val isReceiverType: Property[Type] = createBinaryProperty("not a receiver type") {
     case _: DeclaredT => true
-    case ActualPointerT(t) => t.isInstanceOf[DeclaredT]
+    case PointerT(t) => t.isInstanceOf[DeclaredT]
     case _ => false
   }
 

src/main/scala/viper/gobra/frontend/info/implementation/typing/TypeTyping.scala

@@ -130,10 +130,7 @@ trait TypeTyping extends BaseTyping { this: TypeInfoImpl =>
 
     case PMethodReceiveName(t) => typeSymbType(t)
 
-    case r: PMethodReceivePointer => r match {
-      case PMethodReceiveActualPointer(t) => ActualPointerT(typeSymbType(t))
-      case PMethodReceiveGhostPointer(t) => GhostPointerT(typeSymbType(t))
-    }
+    case PMethodReceiveActualPointer(t) => ActualPointerT(typeSymbType(t))
 
     case PFunctionType(args, r) => FunctionT(args map miscType, miscType(r))
 

src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostTypeTyping.scala

@@ -23,6 +23,7 @@ trait GhostTypeTyping extends BaseTyping { this : TypeInfoImpl =>
     case POptionType(elem) => isType(elem).out
     case PGhostPointerType(elem) => isType(elem).out
     case n: PGhostSliceType => isType(n.elem).out
+    case n: PMethodReceivePointer => isType(n.typ).out
 
     case _: PDomainType => noMessages
     case n: PAdtType => n match {
@@ -42,6 +43,7 @@ trait GhostTypeTyping extends BaseTyping { this : TypeInfoImpl =>
     case POptionType(elem) => OptionT(typeSymbType(elem))
     case PGhostPointerType(elem) => GhostPointerT(typeSymbType(elem))
     case PGhostSliceType(elem) => GhostSliceT(typeSymbType(elem))
+    case PMethodReceiveGhostPointer(t) => GhostPointerT(typeSymbType(t))
     case t: PDomainType => DomainT(t, this)
     case a: PAdtType => adtSymbType(a)
   }

src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/separation/GhostAssignability.scala

@@ -11,7 +11,6 @@ import viper.gobra.ast.frontend._
 import viper.gobra.frontend.info.implementation.TypeInfoImpl
 import viper.gobra.ast.frontend.{AstPattern => ap}
 import viper.gobra.frontend.info.ExternalTypeInfo
-import viper.gobra.frontend.info.base.Type
 import viper.gobra.frontend.info.implementation.property.{AssignMode, NonStrictAssignMode}
 import viper.gobra.frontend.info.implementation.typing.ghost.separation.GhostType.ghost
 import viper.gobra.util.Violation
@@ -107,7 +106,7 @@ trait GhostAssignability {
       error(left, "ghost error: ghost cannot be assigned to non-ghost", isRightGhost && !ghostIdClassification(id))
 
     case n: PDot => exprOrType(n.base) match {
-      case Left(base) => // x.f := e ~ ghost(e) ==> ghostassignee(x.f)
+      case Left(_) => // x.f := e ~ ghost(e) ==> ghostassignee(x.f)
         error(left, "ghost error: ghost cannot be assigned to non-ghost location", isRightGhost && !ghostLocationClassification(left))
       case _ if resolve(n).exists(_.isInstanceOf[ap.GlobalVariable]) =>
         error(left, "ghost error: ghost cannot be assigned to a global variable", isRightGhost)

src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/separation/GhostWellDef.scala

@@ -46,6 +46,9 @@ trait GhostWellDef { this: TypeInfoImpl =>
 
     case m if isEnclosingGhost(m) => noMessages
 
+    case m: PMethodDecl => error(m, "ghost error: expected an actual receiver type",
+      isTypeGhost(m.receiver.typ) && !isEnclosingGhost(m))
+
     case _ => noMessages
   }
 

src/test/resources/regressions/features/ghost_pointer/ghost-pointer-receiver-fail01.gobra

@@ -0,0 +1,32 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+package GhostPointerReceiverFail01
+
+type Foo struct {
+    field int
+}
+
+ghost
+decreases
+func GhostFunc() {
+    p := &Foo{ 42 }
+    p.bar1()
+    //:: ExpectedOutput(type_error)
+    p.bar2() // bar2 is not defined on a ghost pointer
+}
+
+decreases
+//:: ExpectedOutput(type_error)
+func (r gpointer[Foo]) bar1() int { // ghostpointer is only allowed for ghost methods
+    r.field = 0
+    return 42
+}
+
+ghost
+decreases
+func (r *Foo) bar2() int {
+    //:: ExpectedOutput(type_error)
+    r.field = 0 // fails since we're trying to modify actual memory
+    return r.field
+}

src/test/resources/regressions/features/ghost_pointer/ghost-pointer-receiver-simple01.gobra

@@ -0,0 +1,47 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+package GhostPointerReceiverSimple01
+
+type Foo struct {
+    field int
+}
+
+ghost
+decreases
+preserves acc(p)
+func GhostFunc(p *Foo) {
+    gp := &Foo{ 42 }
+    gp.bar1()
+
+    p.bar2()
+    (*p).bar3()
+    (*gp).bar3()
+}
+
+ghost
+decreases
+preserves acc(r)
+func (r gpointer[Foo]) bar1() int {
+    r.field = 0
+    return r.field
+}
+
+decreases
+preserves acc(r)
+func (r *Foo) bar2() int {
+    r.field = 0
+    return r.field
+}
+
+ghost
+decreases
+func (r Foo) bar3() int {
+    r.field = 42
+    return r.field
+}
+
+func (r Foo) bar4() int {
+    r.field = 42
+    return r.field
+}