Support for Ghost Types

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

@@ -628,7 +628,7 @@ sealed trait PLiteralType extends PNode
   * Represents a named type in Go.
   * @see [[https://go.dev/ref/spec#TypeName]]
   **/
-sealed trait PTypeName extends PActualType {
+sealed trait PTypeName extends PType {
   def id : PUseLikeId
   val name: String = id.name
 }
@@ -651,33 +651,37 @@ object PUnqualifiedTypeName {
   *
   * @param name The identifier associated with this type
   */
-sealed abstract class PPredeclaredType(override val name: String) extends PUnqualifiedTypeName with PUseLikeId {
+sealed abstract class PActualPredeclaredType(override val name: String) extends PUnqualifiedTypeName with PUseLikeId with PActualType {
   override def id: PUseLikeId = this
 }
 
-case class PBoolType() extends PPredeclaredType("bool")
-case class PStringType() extends PPredeclaredType("string")
-case class PPermissionType() extends PPredeclaredType("perm")
+sealed abstract class PGhostPredeclaredType(override val name: String) extends PUnqualifiedTypeName with PUseLikeId with PGhostType {
+  override def id: PUseLikeId = this
+}
+
+case class PBoolType() extends PActualPredeclaredType("bool")
+case class PStringType() extends PActualPredeclaredType("string")
+case class PPermissionType() extends PGhostPredeclaredType("perm")
 
 sealed trait PIntegerType extends PType
-case class PIntType() extends PPredeclaredType("int") with PIntegerType
-case class PInt8Type() extends PPredeclaredType("int8") with PIntegerType
-case class PInt16Type() extends PPredeclaredType("int16") with PIntegerType
-case class PInt32Type() extends PPredeclaredType("int32") with PIntegerType
-case class PInt64Type() extends PPredeclaredType("int64") with PIntegerType
-case class PRune() extends PPredeclaredType("rune") with PIntegerType
-
-case class PUIntType() extends PPredeclaredType("uint") with PIntegerType
-case class PUInt8Type() extends PPredeclaredType("uint8") with PIntegerType
-case class PUInt16Type() extends PPredeclaredType("uint16") with PIntegerType
-case class PUInt32Type() extends PPredeclaredType("uint32") with PIntegerType
-case class PUInt64Type() extends PPredeclaredType("uint64") with PIntegerType
-case class PByte() extends PPredeclaredType("byte") with PIntegerType
-case class PUIntPtr() extends PPredeclaredType("uintptr") with PIntegerType
+case class PIntType() extends PActualPredeclaredType("int") with PIntegerType
+case class PInt8Type() extends PActualPredeclaredType("int8") with PIntegerType
+case class PInt16Type() extends PActualPredeclaredType("int16") with PIntegerType
+case class PInt32Type() extends PActualPredeclaredType("int32") with PIntegerType
+case class PInt64Type() extends PActualPredeclaredType("int64") with PIntegerType
+case class PRune() extends PActualPredeclaredType("rune") with PIntegerType
+
+case class PUIntType() extends PActualPredeclaredType("uint") with PIntegerType
+case class PUInt8Type() extends PActualPredeclaredType("uint8") with PIntegerType
+case class PUInt16Type() extends PActualPredeclaredType("uint16") with PIntegerType
+case class PUInt32Type() extends PActualPredeclaredType("uint32") with PIntegerType
+case class PUInt64Type() extends PActualPredeclaredType("uint64") with PIntegerType
+case class PByte() extends PActualPredeclaredType("byte") with PIntegerType
+case class PUIntPtr() extends PActualPredeclaredType("uintptr") with PIntegerType
 
 sealed trait PFloatType extends PType
-case class PFloat32() extends PPredeclaredType("float32") with PFloatType
-case class PFloat64() extends PPredeclaredType("float64") with PFloatType
+case class PFloat32() extends PActualPredeclaredType("float32") with PFloatType
+case class PFloat64() extends PActualPredeclaredType("float64") with PFloatType
 
 // TODO: add more types
 
@@ -739,9 +743,7 @@ sealed trait PMethodRecvType extends PType { // TODO: will have to be removed fo
 
 case class PMethodReceiveName(typ: PNamedOperand) extends PMethodRecvType with PActualType
 
-trait PMethodReceivePointer extends PMethodRecvType {
-  def typ: PNamedOperand
-}
+trait PMethodReceivePointer extends PMethodRecvType
 
 case class PMethodReceiveActualPointer(typ: PNamedOperand) extends PMethodReceivePointer with PActualType
 
@@ -752,8 +754,6 @@ case class PMethodReceiveGhostPointer(typ: PNamedOperand) extends PMethodReceive
 
 case class PFunctionType(args: Vector[PParameter], result: PResult) extends PTypeLit with PScope
 
-case class PPredType(args: Vector[PType]) extends PTypeLit
-
 case class PInterfaceType(
                            embedded: Vector[PInterfaceName],
                            methSpecs: Vector[PMethodSig],
@@ -1283,6 +1283,8 @@ case class PDomainFunction(id: PIdnDef,
 
 case class PDomainAxiom(exp: PExpression) extends PGhostMisc with PScope with PCodeRoot with PDomainClause
 
+case class PPredType(args: Vector[PType]) extends PGhostLiteralType
+
 
 /**
   * Miscellaneous

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

@@ -605,7 +605,6 @@ class DefaultPrettyPrinter extends PrettyPrinter with kiama.output.PrettyPrinter
     case PNamedOperand(id) => showId(id)
     case PBoolType() => "bool"
     case PStringType() => "string"
-    case PPermissionType() => "perm"
     case PIntType() => "int"
     case PInt8Type() => "int8"
     case PInt16Type() => "int16"
@@ -634,7 +633,6 @@ class DefaultPrettyPrinter extends PrettyPrinter with kiama.output.PrettyPrinter
     }
     case PStructType(clauses) => "struct" <+> block(ssep(clauses map showStructClause, line))
     case PFunctionType(args, result) => "func" <> parens(showParameterList(args)) <> showResult(result)
-    case PPredType(args) => "pred" <> parens(showTypeList(args))
     case PInterfaceType(embedded, mspec, pspec) =>
       "interface" <+> block(
         ssep(embedded map showInterfaceClause, line) <>
@@ -646,6 +644,7 @@ class DefaultPrettyPrinter extends PrettyPrinter with kiama.output.PrettyPrinter
   }
 
   def showGhostType(typ : PGhostType) : Doc = typ match {
+    case PPermissionType() => "perm"
     case PSequenceType(elem) => "seq" <> brackets(showType(elem))
     case PSetType(elem) => "set" <> brackets(showType(elem))
     case PMultisetType(elem) => "mset" <> brackets(showType(elem))
@@ -659,6 +658,7 @@ class DefaultPrettyPrinter extends PrettyPrinter with kiama.output.PrettyPrinter
       )
     case PAdtType(clauses) => "adt" <> block(ssep(clauses map showMisc, line))
     case PMethodReceiveGhostPointer(t) => "gpointer" <> brackets(showType(t))
+    case PPredType(args) => "pred" <> parens(showTypeList(args))
   }
 
   def showStructClause(c: PStructClause): Doc = c match {

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

@@ -155,11 +155,9 @@ object SymbolTable extends Environments[Entity] {
   }
 
   case class NamedType(decl: PTypeDef, ghost: Boolean, context: ExternalTypeInfo) extends ActualTypeEntity {
-    require(!ghost, "type entities are not supported to be ghost yet") // TODO
     override def rep: PNode = decl
   }
   case class TypeAlias(decl: PTypeAlias, ghost: Boolean, context: ExternalTypeInfo) extends ActualTypeEntity {
-    require(!ghost, "type entities are not supported to be ghost yet") // TODO
     override def rep: PNode = decl
   }
 

src/main/scala/viper/gobra/frontend/info/implementation/resolution/AmbiguityResolution.scala

@@ -51,7 +51,7 @@ trait AmbiguityResolution { this: TypeInfoImpl =>
     case n: PNamedOperand =>
       entity(n.id) match {
         case s: st.Import => Some(ap.Import(n.id, s))
-        case s: st.NamedType => Some(ap.NamedType(n.id, s))
+        case s: st.ActualTypeEntity => Some(ap.NamedType(n.id, s))
         case s: st.Variable => s match {
           case g: st.GlobalVariable => Some(ap.GlobalVariable(n.id, g))
           case _ => Some(ap.LocalVariable(n.id, s))

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

@@ -36,7 +36,7 @@ trait TypeTyping extends BaseTyping { this: TypeInfoImpl =>
 
   private[typing] def wellDefActualType(typ: PActualType): Messages = typ match {
 
-    case _: PBoolType | _: PIntegerType | _: PFloatType | _: PStringType | _: PPermissionType => noMessages
+    case _: PBoolType | _: PIntegerType | _: PFloatType | _: PStringType => noMessages
 
     case n @ PArrayType(len, t) => isType(t).out ++ {
       intConstantEval(len) match {
@@ -53,7 +53,6 @@ trait TypeTyping extends BaseTyping { this: TypeInfoImpl =>
     case n: PMethodReceiveName => isType(n.typ).out
     case n: PMethodReceivePointer => isType(n.typ).out
     case _: PFunctionType => noMessages // parameters and result is implied by well definedness of children
-    case _: PPredType => noMessages // well definedness implied by well definedness of children
 
     case n@ PMapType(key, elem) => isType(key).out ++ isType(elem).out ++
       error(n, s"map key $key is not comparable", !comparableType(typeSymbType(key))) ++
@@ -123,7 +122,6 @@ trait TypeTyping extends BaseTyping { this: TypeInfoImpl =>
     case PFloat32() => Float32T
     case PFloat64() => Float64T
     case PStringType() => StringT
-    case PPermissionType() => PermissionT
 
     case PArrayType(len, elem) =>
       val lenOpt = intConstantEval(len)
@@ -150,8 +148,6 @@ trait TypeTyping extends BaseTyping { this: TypeInfoImpl =>
 
     case PFunctionType(args, r) => FunctionT(args map miscType, miscType(r))
 
-    case PPredType(args) => PredT(args map typeSymbType)
-
     case t: PInterfaceType =>
       val res = InterfaceT(t, this)
       addDemandedEmbeddedInterfaceImplements(res)
@@ -188,10 +184,11 @@ trait TypeTyping extends BaseTyping { this: TypeInfoImpl =>
     def makeEmbedded(x: PEmbeddedDecl, isGhost: Boolean): ListMap[String, StructClauseT] =
       ListMap(x.id.name -> StructEmbeddedT(miscType(x.typ), isGhost))
 
+    val isStructTypeGhost = isEnclosingGhost(t)
     val clauses = t.clauses.foldLeft(ListMap[String, StructClauseT]()) {
-      case (prev, x: PFieldDecls) => prev ++ makeFields(x, isGhost = false)
+      case (prev, x: PFieldDecls) => prev ++ makeFields(x, isGhost = isStructTypeGhost)
       case (prev, PExplicitGhostStructClause(x: PFieldDecls)) => prev ++ makeFields(x, isGhost = true)
-      case (prev, x: PEmbeddedDecl) => prev ++ makeEmbedded(x, isGhost = false)
+      case (prev, x: PEmbeddedDecl) => prev ++ makeEmbedded(x, isGhost = isStructTypeGhost)
       case (prev, PExplicitGhostStructClause(x: PEmbeddedDecl)) => prev ++ makeEmbedded(x, isGhost = true)
     }
     StructT(clauses, t, this)

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

@@ -16,6 +16,7 @@ import viper.gobra.util.Violation
 trait GhostTypeTyping extends BaseTyping { this : TypeInfoImpl =>
 
   private[typing] def wellDefGhostType(typ : PGhostType) : Messages = typ match {
+    case _: PPermissionType => noMessages
     case PSequenceType(elem) => isType(elem).out
     case PSetType(elem) => isType(elem).out
     case PMultisetType(elem) => isType(elem).out
@@ -33,9 +34,11 @@ trait GhostTypeTyping extends BaseTyping { this : TypeInfoImpl =>
 
       case _ => error(n, "Adt types are only allowed within type declarations.")
     }
+    case _: PPredType => noMessages // well definedness implied by well definedness of children
   }
 
   private[typing] def ghostTypeSymbType(typ : PGhostType) : Type = typ match {
+    case PPermissionType() => PermissionT
     case PSequenceType(elem) => SequenceT(typeSymbType(elem))
     case PSetType(elem) => SetT(typeSymbType(elem))
     case PMultisetType(elem) => MultisetT(typeSymbType(elem))
@@ -46,6 +49,7 @@ trait GhostTypeTyping extends BaseTyping { this : TypeInfoImpl =>
     case PMethodReceiveGhostPointer(t) => GhostPointerT(typeSymbType(t))
     case t: PDomainType => DomainT(t, this)
     case a: PAdtType => adtSymbType(a)
+    case PPredType(args) => PredT(args map typeSymbType)
   }
 
   /** Requires that the parent of a is PTypeDef. */

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

@@ -7,7 +7,7 @@
 package viper.gobra.frontend.info.implementation.typing.ghost.separation
 
 import viper.gobra.ast.frontend._
-import viper.gobra.frontend.info.base.SymbolTable.{Closure, MultiLocalVariable, Regular, SingleLocalVariable}
+import viper.gobra.frontend.info.base.SymbolTable.{Closure, MultiLocalVariable, NamedType, Regular, SingleLocalVariable, TypeAlias}
 import viper.gobra.frontend.info.base.Type
 import viper.gobra.frontend.info.implementation.TypeInfoImpl
 import viper.gobra.ast.frontend.{AstPattern => ap}
@@ -164,11 +164,28 @@ trait GhostTyping extends GhostClassifier { this: TypeInfoImpl =>
   }
 
   /** returns true iff type is classified as ghost */
-  private[separation] lazy val ghostTypeClassification: PType => Boolean = createGhostClassification[PType]{
-    case _: PGhostType => true // TODO: This check seems insufficient to me in the long run. What if a type definition is ghost?
-    case PArrayType(_, t) => isTypeGhost(t)
-    case PSliceType(t) => isTypeGhost(t)
-    case _ => false
+  private[separation] lazy val ghostTypeClassification: PType => Boolean = createGhostClassification[PType] {
+    case _: PGhostType => true
+    case _: PBoolType | _: PIntegerType | _: PFloatType | _: PStringType | _: PFunctionType | _: PInterfaceType => false
+    case PArrayType(_, elem) => isTypeGhost(elem)
+    case PSliceType(elem) => isTypeGhost(elem)
+    case PMapType(key, elem) => isTypeGhost(key) && isTypeGhost(elem)
+    case t: PChannelType => isTypeGhost(t.elem)
+    case t: PMethodRecvType => isTypeGhost(t.typ)
+    case t: PTypeDecl => entity(t.left) match {
+      case nt: NamedType => nt.ghost
+      case at: TypeAlias => at.ghost
+      case _ => false
+    }
+    case t: PStructType => isEnclosingGhost(t)
+    case PVariadicType(elem) => isTypeGhost(elem)
+    case t @ (_: PNamedOperand | _: PDeref | _: PDot) => resolve(t) match {
+      case Some(tp: ap.Type) => tp match {
+        case sp: ap.Symbolic => sp.symb.ghost
+        case ap.PointerType(base) => isTypeGhost(base)
+      }
+      case _ => false
+    }
   }
 
   /** returns true iff identifier is classified as ghost */

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

@@ -31,11 +31,7 @@ trait GhostWellDef { this: TypeInfoImpl =>
   }{ n => isWellDefined(n) && children(n).forall(selfWellGhostSeparated) }
 
   private def memberGhostSeparation(member: PMember): Messages = member match {
-    case m: PExplicitGhostMember => m.actual match {
-      case _: PTypeDecl => error(m, "ghost types are currently not supported") // TODO
-      case _ => noMessages
-    }
-
+    case _: PExplicitGhostMember => noMessages
     case _: PGhostMember => noMessages
 
     case n : PVarDecl => n.typ match {

src/main/scala/viper/gobra/translator/encodings/structs/StructEncoding.scala

@@ -275,7 +275,7 @@ class StructEncoding extends TypeEncoding {
 
   private def indexOfField(fs: Vector[in.Field], f: in.Field): Int = {
     val idx = fs.indexOf(f)
-    Violation.violation(idx >= 0, s"$idx, ${f.typ.addressability}, ${fs.map(_.typ.addressability)} - Did not find field $f in $fs")
+    Violation.violation(idx >= 0, s"$idx, ${f.typ.addressability}, ${fs.map(_.typ.addressability)}, ${f.ghost}, ${fs.map(_.ghost)} - Did not find field $f in $fs")
     idx
   }
 

src/test/resources/regressions/features/defunc/pred-construct-fail1.gobra

@@ -11,13 +11,12 @@ pred (rec *T) AccInv() {
 	acc(rec)
 }
 
-func f(p pred())
+func f(ghost p pred())
 
 func error1() {
 	v := &T{}
 	fold v.AccInv()
-	//:: ExpectedOutput(type_error)
-	f((*T).AccInv!<v!>) // Predicate expressions are not allowed in predicate constructors
+	f((*T).AccInv!<v!>)
 }
 
 func g(x int)
@@ -28,4 +27,4 @@ func error2() {
 	// base, and examples like this would not throw a type error
 	//:: ExpectedOutput(type_error)
 	f(g!<x!>)
-}
+}

src/test/resources/regressions/features/fractional_permissions/perm-fail1.gobra

@@ -69,7 +69,7 @@ func test9() {
 }
 
 func test10() {
-	var m5 perm = 1/2
+	ghost var m5 perm = 1/2
 	//:: ExpectedOutput(assert_error)
 	assert m5 + 1/2 == 1/2
 }

src/test/resources/regressions/features/fractional_permissions/perm-simple1.gobra

@@ -52,7 +52,7 @@ func test6() {
 	m4 := 1/2 + 1/2
 	assert m4 == noPerm
 
-	var m5 perm = 1/2
+	ghost var m5 perm = 1/2
 	assert m5 + 1/2 == writePerm
 
 	m6 := perm((1/2)/1)

src/test/resources/regressions/features/ghost_type/ghost-type-fail01.gobra

@@ -0,0 +1,33 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+// checks that fields of a ghost struct type as treated as ghost fields
+
+package GhostNamedTypeFail01
+
+ghost type GhostStruct struct {
+    f int
+}
+
+ghost type GhostIntDef int
+ghost type GhostIntAlias = int
+
+func foo(ghost s GhostStruct) {
+    s.f = 42
+    //:: ExpectedOutput(type_error)
+    identity(s.f)
+}
+
+func identity(input int) int {
+    return input
+}
+
+//:: ExpectedOutput(type_error)
+func bar1(i GhostIntDef) { // i must be a ghost parameter
+    i = 42
+}
+
+//:: ExpectedOutput(type_error)
+func bar2(i GhostIntAlias) { // i must be a ghost parameter
+    i = 42
+}

src/test/resources/regressions/features/ghost_type/ghost-type-simple01.gobra

@@ -0,0 +1,24 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+package GhostNamedTypeSimple01
+
+ghost type GhostStruct struct {
+    f int
+}
+
+ghost type GhostIntDef int
+ghost type GhostIntAlias = int
+
+func foo(ghost s GhostStruct) {
+    s.f = 42
+    assert s.f == 42
+}
+
+func bar1(ghost i GhostIntDef) {
+    i = 42
+}
+
+func bar2(ghost i GhostIntAlias) {
+    i = 42
+}