Support for Ghost Types

src/main/antlr4/GobraParser.g4

@@ -35,7 +35,7 @@ maybeAddressableIdentifier: IDENTIFIER ADDR_MOD?;
 
 sourceFile:
   (initPost eos)* packageClause eos (importDecl eos)* (
-    (specMember | declaration | ghostMember) eos
+    member eos
   )* EOF;
 
 // `preamble` is a second entry point allowing us to parse only the top of a source.
@@ -50,6 +50,8 @@ importSpec: (importPre eos)* alias = (DOT | IDENTIFIER)? importPath;
 
 importDecl: (importPre eos)* (IMPORT importSpec | IMPORT L_PAREN (importSpec eos)* R_PAREN);
 
+member: specMember | declaration | ghostMember;
+
 ghostMember: implementationProof
   | fpredicateDecl
   | mpredicateDecl
@@ -141,7 +143,7 @@ seqUpdClause: expression ASSIGN expression;
 
 // Ghost Type Literals
 
-ghostTypeLit: sqType | ghostSliceType | ghostPointerType | domainType | adtType;
+ghostTypeLit: sqType | ghostSliceType | ghostPointerType | ghostStructType | domainType | adtType;
 
 domainType: DOM L_CURLY (domainClause eos)* R_CURLY;
 
@@ -157,6 +159,8 @@ ghostSliceType: GHOST L_BRACKET R_BRACKET elementType;
 
 ghostPointerType: GPOINTER L_BRACKET elementType R_BRACKET;
 
+ghostStructType: GHOST structType;
+
 // copy of `fieldDecl` from GoParser.g4 extended with an optional `GHOST` modifier for fields and embedded fields:
 fieldDecl: GHOST? (
 		identifierList type_

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

@@ -172,7 +172,7 @@ sealed trait PFunctionOrClosureDecl extends PScope {
   def body: Option[(PBodyParameterInfo, PBlock)]
 }
 
-sealed trait PFunctionOrMethodDecl extends PNode with PScope {
+sealed trait PFunctionOrMethodDecl extends PActualMember with PScope {
   def id: PIdnDef
 }
 
@@ -182,7 +182,7 @@ case class PFunctionDecl(
                           result: PResult,
                           spec: PFunctionSpec,
                           body: Option[(PBodyParameterInfo, PBlock)]
-                        ) extends PFunctionOrClosureDecl with PActualMember with PCodeRootWithResult with PWithBody with PGhostifiableMember with PFunctionOrMethodDecl
+                        ) extends PFunctionOrClosureDecl with PFunctionOrMethodDecl with PCodeRootWithResult with PWithBody with PGhostifiableMember
 
 case class PMethodDecl(
                         id: PIdnDef,
@@ -191,7 +191,7 @@ case class PMethodDecl(
                         result: PResult,
                         spec: PFunctionSpec,
                         body: Option[(PBodyParameterInfo, PBlock)]
-                      ) extends PActualMember with PDependentDef with PScope with PCodeRootWithResult with PWithBody with PGhostifiableMember with PFunctionOrMethodDecl
+                      ) extends PFunctionOrMethodDecl with PDependentDef with PScope with PCodeRootWithResult with PWithBody with PGhostifiableMember
 
 sealed trait PTypeDecl extends PActualMember with PActualStatement with PGhostifiableStatement with PGhostifiableMember with PDeclaration {
 
@@ -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],
@@ -1267,6 +1267,8 @@ case class POptionType(elem : PType) extends PGhostLiteralType
 /** The type of ghost pointers */
 case class PGhostPointerType(elem: PType) extends PGhostLiteralType
 
+case class PExplicitGhostStructType(actual: PStructType) extends PGhostLiteralType with PGhostifier[PStructType]
+
 /** The type of ADT types */
 case class PAdtType(clauses: Vector[PAdtClause]) extends PGhostLiteralType with PUnorderedScope
 
@@ -1285,6 +1287,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

@@ -606,7 +606,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"
@@ -635,7 +634,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) <>
@@ -647,19 +645,22 @@ 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))
     case PMathematicalMapType(keys, values) => "dict" <> brackets(showType(keys)) <> showType(values)
     case POptionType(elem) => "option" <> brackets(showType(elem))
     case PGhostPointerType(elem) => "gpointer" <> brackets(showType(elem))
+    case PExplicitGhostStructType(actual) => "ghost" <+> showType(actual)
     case PGhostSliceType(elem) => "ghost" <+> brackets(emptyDoc) <> showType(elem)
     case PDomainType(funcs, axioms) =>
       "domain" <+> block(
         ssep((funcs ++ axioms) map showMisc, line)
       )
     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/ast/internal/Program.scala

@@ -1387,14 +1387,6 @@ case class SliceT(elems : Type, addressability: Addressability) extends PrettyTy
   * The (composite) type of maps from type `keys` to type `values`.
   */
 case class MapT(keys: Type, values: Type, addressability: Addressability) extends PrettyType(s"map[$keys]$values") {
-  def hasGhostField(k: Type): Boolean = k match {
-    case StructT(fields, _) => fields exists (_.ghost)
-    case _ => false
-  }
-  // this check must be done here instead of at the type system level because the concrete AST does not support
-  // ghost fields yet
-  require(!hasGhostField(keys))
-
   override def equalsWithoutMod(t: Type): Boolean = t match {
     case MapT(otherKeys, otherValues, _) => keys.equalsWithoutMod(otherKeys) && values.equalsWithoutMod(otherValues)
     case _ => false
@@ -1513,14 +1505,14 @@ case class PredT(args: Vector[Type], addressability: Addressability) extends Pre
 
 // StructT does not have a name because equality of two StructT does not depend at all on their declaration site but
 // only on their structure, i.e. whether the fields (and addressability) are equal
-case class StructT(fields: Vector[Field], addressability: Addressability) extends PrettyType(fields.mkString("struct{", ", ", "}")) with TopType {
+case class StructT(fields: Vector[Field], ghost: Boolean, addressability: Addressability) extends PrettyType(fields.mkString(if (ghost) "ghost " else "" + "struct{", ", ", "}")) with TopType {
   override def equalsWithoutMod(t: Type): Boolean = t match {
-    case StructT(otherFields, _) => fields.zip(otherFields).forall{ case (l, r) => l.typ.equalsWithoutMod(r.typ) }
+    case StructT(otherFields, otherGhost, _) => ghost == otherGhost && fields.zip(otherFields).forall{ case (l, r) => l.name == r.name && l.ghost == r.ghost && l.typ.equalsWithoutMod(r.typ) }
     case _ => false
   }
 
   override def withAddressability(newAddressability: Addressability): StructT =
-    StructT(fields.map(f => Field(f.name, f.typ.withAddressability(Addressability.field(newAddressability)), f.ghost)(f.info)), newAddressability)
+    StructT(fields.map(f => Field(f.name, f.typ.withAddressability(Addressability.field(newAddressability)), f.ghost)(f.info)), ghost = ghost, newAddressability)
 }
 
 case class InterfaceT(name: String, addressability: Addressability) extends PrettyType(s"interface{ name is $name }") with TopType {

src/main/scala/viper/gobra/ast/internal/transform/CGEdgesTerminationTransform.scala

@@ -240,7 +240,7 @@ object CGEdgesTerminationTransform extends InternalTransform {
       case in.DefinedT(name, _) => in.DefinedTExpr(name)(src)
       case in.PointerT(t, _) => in.PointerTExpr(typeAsExpr(t)(src))(src)
       case in.TupleT(ts, _) => in.TupleTExpr(ts map(typeAsExpr(_)(src)))(src)
-      case in.StructT(fields: Vector[in.Field], _) =>
+      case in.StructT(fields: Vector[in.Field], _, _) =>
         in.StructTExpr(fields.map(field => (field.name, typeAsExpr(field.typ)(src), field.ghost)))(src)
       case _ => Violation.violation(s"no corresponding type expression matched: $t")
     }

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

@@ -3780,7 +3780,7 @@ object Desugar extends LazyLogging {
 
       case t: Type.StructT =>
         val inFields: Vector[in.Field] = structD(t, addrMod)(src)
-        registerType(in.StructT(inFields, addrMod))
+        registerType(in.StructT(inFields, ghost = t.isGhost, addrMod))
 
       case t: Type.AdtT =>
         val adtName = nm.adt(t.declaredType)

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

@@ -516,6 +516,17 @@ class ParseTreeTranslator(pom: PositionManager, source: Source, specOnly : Boole
     PGhostPointerType(typ).at(ctx)
   }
 
+  /**
+    * {@inheritDoc }
+    *
+    * <p>The default implementation returns the result of calling
+    * {@link #   visitChildren} on {@code ctx}.</p>
+    */
+  override def visitGhostStructType(ctx: GhostStructTypeContext): PExplicitGhostStructType = {
+    val actual = visitNode[PStructType](ctx.structType())
+    PExplicitGhostStructType(actual).at(ctx)
+  }
+
   /**
     * {@inheritDoc  }
     *
@@ -848,7 +859,7 @@ class ParseTreeTranslator(pom: PositionManager, source: Source, specOnly : Boole
       (for (expr <- ctx.expression().asScala.toVector) yield visitNode[PExpression](expr)).at(ctx)
   }
 
-  override def visitSpecMember(ctx: SpecMemberContext): AnyRef = super.visitSpecMember(ctx) match {
+  override def visitSpecMember(ctx: SpecMemberContext): PFunctionOrMethodDecl = super.visitSpecMember(ctx) match {
     case Vector(spec : PFunctionSpec, (id: PIdnDef, args: Vector[PParameter@unchecked], result: PResult, body: Option[(PBodyParameterInfo, PBlock)@unchecked]))
       => PFunctionDecl(id, args, result, spec, body)
     case Vector(spec : PFunctionSpec, (id: PIdnDef, receiver: PReceiver, args: Vector[PParameter@unchecked], result: PResult, body: Option[(PBodyParameterInfo, PBlock)@unchecked]))
@@ -939,6 +950,21 @@ class ParseTreeTranslator(pom: PositionManager, source: Source, specOnly : Boole
   }
 
   //region Ghost members
+
+  /**
+    * Visits the rule
+    * ghostMember: implementationProof
+    *   | fpredicateDecl
+    *   | mpredicateDecl
+    *   | explicitGhostMember;
+    *
+    * @param ctx the parse tree
+    */
+  override def visitGhostMember(ctx: GhostMemberContext): Vector[PMember] = super.visitGhostMember(ctx) match {
+    case v: Vector[PMember@unchecked] => v // note: we have to resort to PMember as an implementation proof is not a PGhostMember
+    case m: PMember => Vector(m)
+  }
+
   /**
     * Visits the rule
     * explicitGhostMember: GHOST (methodDecl | functionDecl | declaration);
@@ -2251,12 +2277,8 @@ class ParseTreeTranslator(pom: PositionManager, source: Source, specOnly : Boole
     val packageClause: PPackageClause = visitNode(ctx.packageClause())
     val initPosts: Vector[PExpression] = visitListNode[PExpression](ctx.initPost())
     val importDecls = ctx.importDecl().asScala.toVector.flatMap(visitImportDecl)
-
-    // Don't parse functions/methods if the identifier is blank
-    val members = visitListNode[PMember](ctx.specMember())
-    val ghostMembers = ctx.ghostMember().asScala.flatMap(visitNode[Vector[PGhostMember]])
-    val decls = ctx.declaration().asScala.toVector.flatMap(visitDeclaration(_).asInstanceOf[Vector[PDeclaration]])
-    PProgram(packageClause, initPosts, importDecls, members ++ decls ++ ghostMembers).at(ctx)
+    val members = ctx.member().asScala.toVector.flatMap(visitMember)
+    PProgram(packageClause, initPosts, importDecls, members).at(ctx)
   }
 
   override def visitPreamble(ctx: GobraParser.PreambleContext): PPreamble = {
@@ -2366,7 +2388,16 @@ class ParseTreeTranslator(pom: PositionManager, source: Source, specOnly : Boole
     }
   }
 
-
+  /**
+    * Visit the rule "member: specMember | declaration | ghostMember;"
+    *
+    * @param ctx the parse tree
+    * @return the visitor result
+    */
+  override def visitMember(ctx: GobraParser.MemberContext): Vector[PMember] = super.visitMember(ctx) match {
+    case v: Vector[PMember@unchecked] => v
+    case m: PMember => Vector(m)
+  }
   //endregion
 
 

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

@@ -18,7 +18,7 @@ import org.antlr.v4.runtime.atn.PredictionMode
 import org.antlr.v4.runtime.misc.ParseCancellationException
 import scalaz.EitherT
 import scalaz.Scalaz.futureInstance
-import viper.gobra.frontend.GobraParser.{ExprOnlyContext, ImportDeclContext, PreambleContext, SourceFileContext, SpecMemberContext, StmtOnlyContext, TypeOnlyContext}
+import viper.gobra.frontend.GobraParser.{ExprOnlyContext, ImportDeclContext, MemberContext, PreambleContext, SourceFileContext, StmtOnlyContext, TypeOnlyContext}
 import viper.gobra.frontend.PackageResolver.{AbstractImport, AbstractPackage, BuiltInImport, RegularImport, RegularPackage}
 import viper.gobra.util.{GobraExecutionContext, Job, TaskManager, Violation}
 import viper.silver.ast.SourcePosition
@@ -372,11 +372,11 @@ object Parser extends LazyLogging {
     parser.parse(parser.sourceFile())
   }
 
-  def parseFunction(source: Source, specOnly: Boolean = false): Either[Vector[ParserError], PMember] = {
+  def parseMember(source: Source, specOnly: Boolean = false): Either[Vector[ParserError], Vector[PMember]] = {
     val positions = new Positions
     val pom = new PositionManager(positions)
-    val parser = new SyntaxAnalyzer[SpecMemberContext, PMember](source, ListBuffer.empty[ParserError], pom, specOnly)
-    parser.parse(parser.specMember())
+    val parser = new SyntaxAnalyzer[MemberContext, Vector[PMember]](source, ListBuffer.empty[ParserError], pom, specOnly)
+    parser.parse(parser.member())
   }
 
   def parseStmt(source: Source): Either[Vector[ParserError], PStatement] = {

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/base/Type.scala

@@ -109,7 +109,7 @@ object Type {
 
   case class StructEmbeddedT(typ: Type, isGhost: Boolean) extends StructClauseT
 
-  case class StructT(clauses: ListMap[String, StructClauseT], decl: PStructType, context: ExternalTypeInfo) extends ContextualType {
+  case class StructT(clauses: ListMap[String, StructClauseT], isGhost: Boolean, decl: PStructType, context: ExternalTypeInfo) extends ContextualType {
     lazy val fieldsAndEmbedded: ListMap[String, Type] = clauses.map(extractTyp)
     lazy val fields: ListMap[String, Type] = clauses.filter(isField).map(extractTyp)
     lazy val embedded: ListMap[String, Type] = clauses.filterNot(isField).map(extractTyp)
@@ -122,8 +122,8 @@ object Type {
     private def extractTyp(clause: (String, StructClauseT)): (String, Type) = (clause._1, clause._2.typ)
 
     override lazy val toString: String = {
-      val fields = clauses.map { case (n, i) => s"$n: $i" }
-      s"struct{ ${fields.mkString("; ")}}"
+      val fields = clauses.map { case (n, i) => s"${if (i.isGhost) "ghost " else ""}$n $i" }
+      s"${if (isGhost) "ghost " else ""}struct{ ${fields.mkString("; ")} }"
     }
   }