diff --git a/src/main/antlr4/GobraParser.g4 b/src/main/antlr4/GobraParser.g4 index 7daa704ce..df2b51739 100644 --- a/src/main/antlr4/GobraParser.g4 +++ b/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_ diff --git a/src/main/scala/viper/gobra/ast/frontend/Ast.scala b/src/main/scala/viper/gobra/ast/frontend/Ast.scala index f4368af9a..1e83156a9 100644 --- a/src/main/scala/viper/gobra/ast/frontend/Ast.scala +++ b/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 diff --git a/src/main/scala/viper/gobra/ast/frontend/PrettyPrinter.scala b/src/main/scala/viper/gobra/ast/frontend/PrettyPrinter.scala index 14db0b55b..7ceebfc79 100644 --- a/src/main/scala/viper/gobra/ast/frontend/PrettyPrinter.scala +++ b/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,12 +645,14 @@ 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( @@ -660,6 +660,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 { diff --git a/src/main/scala/viper/gobra/ast/internal/Program.scala b/src/main/scala/viper/gobra/ast/internal/Program.scala index c140330f3..66e417efb 100644 --- a/src/main/scala/viper/gobra/ast/internal/Program.scala +++ b/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 { diff --git a/src/main/scala/viper/gobra/ast/internal/transform/CGEdgesTerminationTransform.scala b/src/main/scala/viper/gobra/ast/internal/transform/CGEdgesTerminationTransform.scala index af4eb1036..f22134a38 100644 --- a/src/main/scala/viper/gobra/ast/internal/transform/CGEdgesTerminationTransform.scala +++ b/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") } diff --git a/src/main/scala/viper/gobra/frontend/Desugar.scala b/src/main/scala/viper/gobra/frontend/Desugar.scala index c924753fd..9b185a529 100644 --- a/src/main/scala/viper/gobra/frontend/Desugar.scala +++ b/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) diff --git a/src/main/scala/viper/gobra/frontend/ParseTreeTranslator.scala b/src/main/scala/viper/gobra/frontend/ParseTreeTranslator.scala index fe69309fa..f38cd8aef 100644 --- a/src/main/scala/viper/gobra/frontend/ParseTreeTranslator.scala +++ b/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 } + * + *

The default implementation returns the result of calling + * {@link # visitChildren} on {@code ctx}.

+ */ + 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 diff --git a/src/main/scala/viper/gobra/frontend/Parser.scala b/src/main/scala/viper/gobra/frontend/Parser.scala index 96515b5ba..377ec45ee 100644 --- a/src/main/scala/viper/gobra/frontend/Parser.scala +++ b/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] = { diff --git a/src/main/scala/viper/gobra/frontend/info/base/SymbolTable.scala b/src/main/scala/viper/gobra/frontend/info/base/SymbolTable.scala index 79c948a97..57f5df1be 100644 --- a/src/main/scala/viper/gobra/frontend/info/base/SymbolTable.scala +++ b/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 } diff --git a/src/main/scala/viper/gobra/frontend/info/base/Type.scala b/src/main/scala/viper/gobra/frontend/info/base/Type.scala index c8d6ccd55..ee97ee787 100644 --- a/src/main/scala/viper/gobra/frontend/info/base/Type.scala +++ b/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("; ")} }" } } diff --git a/src/main/scala/viper/gobra/frontend/info/implementation/property/TypeIdentity.scala b/src/main/scala/viper/gobra/frontend/info/implementation/property/TypeIdentity.scala index 7b8154519..ea7be1337 100644 --- a/src/main/scala/viper/gobra/frontend/info/implementation/property/TypeIdentity.scala +++ b/src/main/scala/viper/gobra/frontend/info/implementation/property/TypeIdentity.scala @@ -40,9 +40,9 @@ trait TypeIdentity extends BaseProperty { this: TypeInfoImpl => case (l: DomainT, r: DomainT) => l == r case (l: AdtT, r: AdtT) => l == r - case (StructT(clausesL, _, contextL), StructT(clausesR, _, contextR)) => - contextL == contextR && clausesL.size == clausesR.size && clausesL.zip(clausesR).forall { - case ((lId, lc), (rId, rc)) => lId == rId && identicalTypes(lc.typ, rc.typ) && ((lc, rc) match { + case (StructT(clausesL, isGhostL, _, contextL), StructT(clausesR, isGhostR, _, contextR)) => + isGhostL == isGhostR && contextL == contextR && clausesL.size == clausesR.size && clausesL.zip(clausesR).forall { + case ((lId, lc), (rId, rc)) => lId == rId && lc.isGhost == rc.isGhost && identicalTypes(lc.typ, rc.typ) && ((lc, rc) match { case (_: StructFieldT, _: StructFieldT) => true case (_: StructEmbeddedT, _: StructEmbeddedT) => true case _ => false diff --git a/src/main/scala/viper/gobra/frontend/info/implementation/resolution/AmbiguityResolution.scala b/src/main/scala/viper/gobra/frontend/info/implementation/resolution/AmbiguityResolution.scala index a6597b7e5..5d48d91d6 100644 --- a/src/main/scala/viper/gobra/frontend/info/implementation/resolution/AmbiguityResolution.scala +++ b/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)) diff --git a/src/main/scala/viper/gobra/frontend/info/implementation/resolution/NameResolution.scala b/src/main/scala/viper/gobra/frontend/info/implementation/resolution/NameResolution.scala index b70fd10a5..83399fe8c 100644 --- a/src/main/scala/viper/gobra/frontend/info/implementation/resolution/NameResolution.scala +++ b/src/main/scala/viper/gobra/frontend/info/implementation/resolution/NameResolution.scala @@ -69,8 +69,14 @@ trait NameResolution { // therefore, we do not use `isGhost` but `spec.isGhost`: MethodSpec(spec, tdef, spec.isGhost, this) - case decl: PFieldDecl => Field(decl, isGhost, this) - case decl: PEmbeddedDecl => Embbed(decl, isGhost, this) + case tree.parent.pair(decl: PFieldDecl, tree.parent.pair(_: PFieldDecls, _: PExplicitGhostStructClause)) => + // this field declaration has an explicit ghost modifier + Field(decl, ghost = true, this) + case decl: PFieldDecl => Field(decl, ghost = false, this) + case tree.parent.pair(decl: PEmbeddedDecl, _: PExplicitGhostStructClause) => + // this embedded declaration has an explicit ghost modifier + Embbed(decl, ghost = true, this) + case decl: PEmbeddedDecl => Embbed(decl, ghost = false, this) case tree.parent.pair(decl: PNamedParameter, _: PResult) => OutParameter(decl, isGhost, canParameterBeUsedAsShared(decl), this) case decl: PNamedParameter => InParameter(decl, isGhost, canParameterBeUsedAsShared(decl), this) diff --git a/src/main/scala/viper/gobra/frontend/info/implementation/typing/TypeTyping.scala b/src/main/scala/viper/gobra/frontend/info/implementation/typing/TypeTyping.scala index d91a5f68b..50631f6f9 100644 --- a/src/main/scala/viper/gobra/frontend/info/implementation/typing/TypeTyping.scala +++ b/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,17 +53,15 @@ 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))) ++ - error(n, s"map key $key cannot contain ghost fields", isStructTypeWithGhostFields(typeSymbType(key))) + error(n, s"map key $key can neither be a ghost struct nor contain ghost fields", isStructTypeWithGhostFields(typeSymbType(key))) - case t: PStructType => - t.embedded.flatMap(e => isNotPointerTypePE.errors(e.typ)(e)) ++ - t.fields.flatMap(f => isType(f.typ).out ++ isNotPointerTypeP.errors(f.typ)(f)) ++ - structMemberSet(structSymbType(t)).errors(t) ++ addressableMethodSet(structSymbType(t)).errors(t) ++ - error(t, "invalid recursive struct", cyclicStructDef(t)) + case t: PStructType => t match { + case tree.parent(_: PExplicitGhostStructType) => noMessages // this case is handled in `wellDefGhostType` + case _ => wellDefStructType(t, isGhost = false) + } case t: PInterfaceType => val isRecursiveInterface = error(t, "invalid recursive interface", cyclicInterfaceDef(t)) @@ -77,6 +75,21 @@ trait TypeTyping extends BaseTyping { this: TypeInfoImpl => case t: PExpressionAndType => wellDefExprAndType(t).out ++ isType(t).out } + private[typing] def wellDefStructType(t: PStructType, isGhost: Boolean): Messages = { + val noGhostEmbeddings: Messages = { + val firstGhostEmbedding: Option[PExplicitGhostStructClause] = t.clauses.collectFirst { + case n@PExplicitGhostStructClause(_: PEmbeddedDecl) => n + } + firstGhostEmbedding.fold(noMessages)(error(_, "embeddings cannot be ghost in a non-ghost struct", !isGhost)) + } + + t.embedded.flatMap(e => isNotPointerTypePE.errors(e.typ)(e)) ++ + noGhostEmbeddings ++ + t.fields.flatMap(f => isType(f.typ).out ++ isNotPointerTypeP.errors(f.typ)(f)) ++ + structMemberSet(structSymbType(t, isGhost = isGhost)).errors(t) ++ addressableMethodSet(structSymbType(t, isGhost = isGhost)).errors(t) ++ + error(t, "invalid recursive struct", cyclicStructDef(t)) + } + def isStructTypeWithGhostFields(t: Type): Boolean = t match { case Single(st) => underlyingType(st) match { case t: StructT => @@ -123,7 +136,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) @@ -142,7 +154,7 @@ trait TypeTyping extends BaseTyping { this: TypeInfoImpl => case PRecvChannelType(elem) => ChannelT(typeSymbType(elem), ChannelModus.Recv) - case t: PStructType => structSymbType(t) + case t: PStructType => structSymbType(t, isGhost = false) case PMethodReceiveName(t) => typeSymbType(t) @@ -150,8 +162,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) @@ -179,22 +189,25 @@ trait TypeTyping extends BaseTyping { this: TypeInfoImpl => } } - private def structSymbType(t: PStructType): Type = { - def infoFromFieldDecl(f: PFieldDecl, isGhost: Boolean): StructFieldT = StructFieldT(typeSymbType(f.typ), isGhost) + private[typing] def structSymbType(t: PStructType, isGhost: Boolean): StructT = { + def infoFromFieldDecl(f: PFieldDecl, isFieldGhost: Boolean): StructFieldT = StructFieldT(typeSymbType(f.typ), isFieldGhost) - def makeFields(x: PFieldDecls, isGhost: Boolean): ListMap[String, StructClauseT] = { - x.fields.foldLeft(ListMap[String, StructClauseT]()) { case (prev, f) => prev + (f.id.name -> infoFromFieldDecl(f, isGhost)) } + def makeFields(x: PFieldDecls, areFieldsGhost: Boolean): ListMap[String, StructClauseT] = { + x.fields.foldLeft(ListMap[String, StructClauseT]()) { case (prev, f) => prev + (f.id.name -> infoFromFieldDecl(f, areFieldsGhost)) } } - def makeEmbedded(x: PEmbeddedDecl, isGhost: Boolean): ListMap[String, StructClauseT] = - ListMap(x.id.name -> StructEmbeddedT(miscType(x.typ), isGhost)) + def makeEmbedded(x: PEmbeddedDecl, isEmbeddedGhost: Boolean): ListMap[String, StructClauseT] = + ListMap(x.id.name -> StructEmbeddedT(miscType(x.typ), isEmbeddedGhost)) + + // we do not propagate a struct's ghostness to its fields. This will be taken care of by the access path when + // performing a field lookup val clauses = t.clauses.foldLeft(ListMap[String, StructClauseT]()) { - case (prev, x: PFieldDecls) => prev ++ makeFields(x, isGhost = false) - case (prev, PExplicitGhostStructClause(x: PFieldDecls)) => prev ++ makeFields(x, isGhost = true) - case (prev, x: PEmbeddedDecl) => prev ++ makeEmbedded(x, isGhost = false) - case (prev, PExplicitGhostStructClause(x: PEmbeddedDecl)) => prev ++ makeEmbedded(x, isGhost = true) + case (prev, x: PFieldDecls) => prev ++ makeFields(x, areFieldsGhost = false) + case (prev, PExplicitGhostStructClause(x: PFieldDecls)) => prev ++ makeFields(x, areFieldsGhost = true) + case (prev, x: PEmbeddedDecl) => prev ++ makeEmbedded(x, isEmbeddedGhost = false) + case (prev, PExplicitGhostStructClause(x: PEmbeddedDecl)) => prev ++ makeEmbedded(x, isEmbeddedGhost = true) } - StructT(clauses, t, this) + StructT(clauses, isGhost = isGhost, t, this) } /** diff --git a/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostExprTyping.scala b/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostExprTyping.scala index 310e8b9c4..0c5877e96 100644 --- a/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostExprTyping.scala +++ b/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostExprTyping.scala @@ -480,6 +480,7 @@ trait GhostExprTyping extends BaseTyping { this: TypeInfoImpl => case _: PGhostSliceType => false case _: PAdtType | _: PDomainType | _: PMathematicalMapType | _: PMultisetType | _: POptionType | _: PSequenceType | _: PSetType => true + case _: PExplicitGhostStructType => true } case _: PArrayType | _: PStructType => true case _: PMapType | _: PSliceType => false diff --git a/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostTypeTyping.scala b/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostTypeTyping.scala index ac2c76e9c..0c107ceaf 100644 --- a/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostTypeTyping.scala +++ b/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostTypeTyping.scala @@ -16,12 +16,14 @@ 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 case PMathematicalMapType(key, value) => isType(key).out ++ isType(value).out case POptionType(elem) => isType(elem).out case PGhostPointerType(elem) => isType(elem).out + case PExplicitGhostStructType(actual) => wellDefStructType(actual, isGhost = true) case n: PGhostSliceType => isType(n.elem).out case PMethodReceiveGhostPointer(t) => isType(t).out @@ -33,19 +35,23 @@ 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)) case PMathematicalMapType(keys, values) => MathMapT(typeSymbType(keys), typeSymbType(values)) case POptionType(elem) => OptionT(typeSymbType(elem)) case PGhostPointerType(elem) => GhostPointerT(typeSymbType(elem)) + case PExplicitGhostStructType(actual) => structSymbType(actual, isGhost = true) case PGhostSliceType(elem) => GhostSliceT(typeSymbType(elem)) 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. */ diff --git a/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/separation/GhostTyping.scala b/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/separation/GhostTyping.scala index df187e262..0093e3c53 100644 --- a/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/separation/GhostTyping.scala +++ b/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 _: PStructType => false // `PExplicitGhostStructType` is already captured by the `PGhostType` case above + 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 */ diff --git a/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/separation/GhostWellDef.scala b/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/separation/GhostWellDef.scala index ad1b2d94f..a1671babd 100644 --- a/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/separation/GhostWellDef.scala +++ b/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 { @@ -44,6 +40,14 @@ trait GhostWellDef { this: TypeInfoImpl => case None => noMessages } + case n: PTypeDecl => + error(n, s"ghost error: expected an actual type but found ${n.right}", isTypeGhost(n.right) && !isEnclosingGhost(n)) ++ + // to avoid confusion about how equality works for this type declaration, we require that the type declaration + // is ghost iff its RHS is a ghost type. + // An alternative implementation could permit all types on the RHS for which the definition of `===` matches `==`. + // This alternative would permit, e.g., a ghost type definition with `int` on the RHS. + error(n, s"ghost error: expected a ghost type but found ${n.right}", !isTypeGhost(n.right) && isEnclosingGhost(n)) + case m if isEnclosingGhost(m) => noMessages case m: PMethodDecl => error(m, "ghost error: expected an actual receiver type", @@ -166,7 +170,8 @@ trait GhostWellDef { this: TypeInfoImpl => isTypeGhost(f.typ) && !isEnclosingGhost(f)) }) case _: PInterfaceType => noMessages - case n: PType => error(n, "ghost error: Found ghost child expression, but expected none", !noGhostPropagationFromChildren(n)) + case n: PType => error(n, "ghost error: Found ghost child expression, but expected none", + !isEnclosingGhost(n) && !noGhostPropagationFromChildren(n)) } private lazy val idGhostSeparation: WellDefinedness[PIdnNode] = createWellDefWithValidityMessages { diff --git a/src/main/scala/viper/gobra/translator/Names.scala b/src/main/scala/viper/gobra/translator/Names.scala index 943ed0089..e74d21107 100644 --- a/src/main/scala/viper/gobra/translator/Names.scala +++ b/src/main/scala/viper/gobra/translator/Names.scala @@ -72,7 +72,7 @@ object Names { // we use a dollar sign to mark the beginning and end of the type list to avoid that `Tuple(Tuple(X), Y)` and `Tuple(Tuple(X, Y))` map to the same name: case in.TupleT(ts, addr) => s"Tuple$$${ts.map(serializeType).mkString("")}$$${serializeAddressability(addr)}" case in.PredT(ts, addr) => s"Pred$$${ts.map(serializeType).mkString("")}$$${serializeAddressability(addr)}" - case in.StructT(fields, addr) => s"Struct${serializeFields(fields)}${serializeAddressability(addr)}" + case in.StructT(fields, _, addr) => s"Struct${serializeFields(fields)}${serializeAddressability(addr)}" case in.FunctionT(args, res, addr) => s"Func$$${args.map(serializeType).mkString("")}$$${res.map(serializeType).mkString("")}$$${serializeAddressability(addr)}" case in.InterfaceT(name, addr) => s"Interface$name${serializeAddressability(addr)}" case in.ChannelT(elemT, addr) => s"Channel${serializeType(elemT)}${serializeAddressability(addr)}" diff --git a/src/main/scala/viper/gobra/translator/encodings/structs/StructEncoding.scala b/src/main/scala/viper/gobra/translator/encodings/structs/StructEncoding.scala index f3f4e78e2..1441590dc 100644 --- a/src/main/scala/viper/gobra/translator/encodings/structs/StructEncoding.scala +++ b/src/main/scala/viper/gobra/translator/encodings/structs/StructEncoding.scala @@ -148,7 +148,18 @@ class StructEncoding extends TypeEncoding { * * [(lhs: Struct{F}) == rhs: Struct{_}] -> AND f in actual(F): [lhs.f == rhs.f] (NOTE: f ranges only over actual fields since `goEqual` corresponds to actual comparison) */ - override def goEqual(ctx: Context): (in.Expr, in.Expr, in.Node) ==> CodeWriter[vpr.Exp] = default(super.goEqual(ctx))(structEqual(ctx, useGoEquality = true)) + override def goEqual(ctx: Context): (in.Expr, in.Expr, in.Node) ==> CodeWriter[vpr.Exp] = default(super.goEqual(ctx)) { + case (lhs :: ctx.Struct(_), rhs :: ctx.Struct(_), src) => + def hasGhostStructType(e: in.Expr): Boolean = underlyingType(e.typ)(ctx) match { + case t: in.StructT => t.ghost + case _ => false + } + + // if lhs is a ghost struct (_not_ an actual struct contains just ghost fields) then we use ghost equality + val isGhostStructComparison = hasGhostStructType(lhs) + require(isGhostStructComparison == hasGhostStructType(rhs), "operands of equality operation do not agree on their ghostness") + structEqual(ctx, useGoEquality = !isGhostStructComparison)(lhs, rhs, src) + } /** * Encodes equality of two struct values under consideration of either the Go or Gobra/ghost semantics @@ -275,7 +286,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 } @@ -287,7 +298,7 @@ class StructEncoding extends TypeEncoding { */ private val shDfltFunc: FunctionGenerator[Vector[in.Field]] = new FunctionGenerator[Vector[in.Field]] { override def genFunction(fs: Vector[in.Field])(ctx: Context): vpr.Function = { - val resType = in.StructT(fs, Shared) + val resType = in.StructT(fs, ghost = false, Shared) // ghostness does not matter as the resulting Viper type is the same val vResType = typ(ctx)(resType) val src = in.DfltVal(resType)(Source.Parser.Internal) // variable name does not matter because it is turned into a vpr.Result diff --git a/src/test/resources/regressions/features/adts/fields1.gobra b/src/test/resources/regressions/features/adts/fields1.gobra index e409e7f2c..635771b0e 100644 --- a/src/test/resources/regressions/features/adts/fields1.gobra +++ b/src/test/resources/regressions/features/adts/fields1.gobra @@ -3,7 +3,7 @@ package adts -type tree adt { +ghost type tree adt { Node { val int @@ -20,7 +20,7 @@ type tree adt { } -type list adt { +ghost type list adt { Cons { head int @@ -33,7 +33,7 @@ type list adt { } -type expression adt { +ghost type expression adt { Add { lA, rA expression @@ -49,7 +49,7 @@ type expression adt { } func testTree(){ - var t tree = Node{1, Node{2, EmptyLeaf{}, EmptyLeaf{}}, Node{3, Leaf{4}, EmptyLeaf{}}} + ghost var t tree = Node{1, Node{2, EmptyLeaf{}, EmptyLeaf{}}, Node{3, Leaf{4}, EmptyLeaf{}}} assert t.val == 1 assert t.isNode @@ -65,7 +65,7 @@ func testTree(){ } func testList() { - var l list = Cons{1, Cons{2, Cons{3, Cons{4, Nil{}}}}} + ghost var l list = Cons{1, Cons{2, Cons{3, Cons{4, Nil{}}}}} assert l.head == 1 assert l.isCons @@ -81,7 +81,7 @@ func testList() { } func testExpression() { - var e expression = Add{Mul{Lit{2}, Lit{3}}, Add{Lit{4}, Lit{20}}} + ghost var e expression = Add{Mul{Lit{2}, Lit{3}}, Add{Lit{4}, Lit{20}}} assert e.lA.lM.val == 2 assert e.isAdd diff --git a/src/test/resources/regressions/features/adts/simple-match1.gobra b/src/test/resources/regressions/features/adts/simple-match1.gobra index e98cfb9ff..1f29e7bba 100644 --- a/src/test/resources/regressions/features/adts/simple-match1.gobra +++ b/src/test/resources/regressions/features/adts/simple-match1.gobra @@ -3,7 +3,7 @@ package adts -type tree adt { +ghost type tree adt { Node { val int left, right tree @@ -11,7 +11,7 @@ type tree adt { Leaf{} } -type list adt { +ghost type list adt { Cons { head int tail list @@ -20,11 +20,15 @@ type list adt { } ghost +decreases ensures a > b ==> a == res ensures a <= b ==> b == res -pure func max (a, b int) (res int) +pure func max (a, b int) (res int) { + return a > b ? a : b +} ghost +decreases len(t) pure func depth(t tree) (res int) { return match t { case Node{_, ?l, ?r}: 1 + max(depth(l), depth(r)) @@ -33,6 +37,7 @@ pure func depth(t tree) (res int) { } ghost +decreases len(t) pure func count(t tree) (res int) { return match t { case Node{_, ?l, ?r}: 1 + count(l) + count(r) @@ -42,6 +47,7 @@ pure func count(t tree) (res int) { ghost +decreases len(t) ensures count(t) >= 0 && depth(t) >= 0 ensures count(t) >= depth(t) func proof1(t tree) { @@ -54,6 +60,7 @@ func proof1(t tree) { ghost +decreases len(l1) pure func concat(l1, l2 list) list { return match l1 { case Nil{}: l2 @@ -67,6 +74,7 @@ pred allNatrual(xs list) { } ghost +decreases n requires n >= 0 pure func rep(n, v int) list { return match n { @@ -77,6 +85,7 @@ pure func rep(n, v int) list { ghost +decreases allNatrual(xs) requires allNatrual(xs) pure func dec(xs list) list { return match xs { @@ -90,6 +99,7 @@ pure func dec(xs list) list { } ghost +decreases len(xs) pure func srclen(xs list) int { return match xs { case Nil{}: 0 @@ -99,6 +109,7 @@ pure func srclen(xs list) int { } ghost +decreases len(xs) pure func length(xs list) int { return match xs { case Nil{}: 0 @@ -107,14 +118,17 @@ pure func length(xs list) int { } ghost +decreases ensures forall xs, ys list :: {length(concat(xs, ys))} length(concat(xs, ys)) == length(xs) + length(ys) func lemma1() ghost +decreases ensures forall x, y int :: {length(rep(x,y))} x >= 0 ==> length(rep(x, y)) == x func lemma2() ghost +decreases len(xs) requires allNatrual(xs) ensures allNatrual(xs) ensures length(dec(xs)) == srclen(xs) @@ -132,4 +146,3 @@ func proof2 (xs list) { fold allNatrual(xs); } } - diff --git a/src/test/resources/regressions/features/adts/simple1.gobra b/src/test/resources/regressions/features/adts/simple1.gobra index 9ba5f50d0..2b6ec73d3 100644 --- a/src/test/resources/regressions/features/adts/simple1.gobra +++ b/src/test/resources/regressions/features/adts/simple1.gobra @@ -3,7 +3,7 @@ package pkg -type tree adt{ +ghost type tree adt{ leaf{ value int } node{ left, right tree } } @@ -16,7 +16,7 @@ func test1() { assert y.isleaf } -func test2(x tree) { +func test2(ghost x tree) { ghost var y int match x { case node{leaf{5}, _}: y = 4 diff --git a/src/test/resources/regressions/features/adts/stateMachine1.gobra b/src/test/resources/regressions/features/adts/stateMachine1.gobra index adc55b686..04d4382c4 100644 --- a/src/test/resources/regressions/features/adts/stateMachine1.gobra +++ b/src/test/resources/regressions/features/adts/stateMachine1.gobra @@ -3,25 +3,25 @@ package adts -type State adt { +ghost type State adt { Modified{} Shared{} Invalid{} } -type ProcessorSignal adt { +ghost type ProcessorSignal adt { PrWr{} PrRd{} } -type BusSignal adt { +ghost type BusSignal adt { BusRd{} BusRdX{} BusUpgr{} NoSig{} } -type BusOpt adt { +ghost type BusOpt adt { Some { sig BusSignal } @@ -38,6 +38,7 @@ pred (m *Machine) isMachine() { } ghost +decreases requires m.isMachine() pure func (m *Machine) stateOfMachine() State { return unfolding m.isMachine() in ( @@ -49,6 +50,7 @@ pure func (m *Machine) stateOfMachine() State { } ghost +decreases requires i >= -1 && i <= 2 pure func busSigToAdt(i int) BusSignal { return (match i { @@ -61,6 +63,7 @@ pure func busSigToAdt(i int) BusSignal { ghost +decreases requires i >= 0 && i <= 1 pure func prSigToAdt(i int) ProcessorSignal { return (match i { diff --git a/src/test/resources/regressions/features/adts/termination-fail1.gobra b/src/test/resources/regressions/features/adts/termination-fail1.gobra index 99d5a4b77..d4e3c6e80 100644 --- a/src/test/resources/regressions/features/adts/termination-fail1.gobra +++ b/src/test/resources/regressions/features/adts/termination-fail1.gobra @@ -3,15 +3,14 @@ package pkg -type tree adt{ +ghost type tree adt{ leaf{ value int } node{ left, right tree } } ghost -pure decreases // cause: wrong termination measure -func leafCount(t tree) int { +pure func leafCount(t tree) int { return match t { case leaf{_}: 1 //:: ExpectedOutput(pure_function_termination_error) @@ -19,7 +18,7 @@ func leafCount(t tree) int { } } -type list adt { +ghost type list adt { Empty{} Cons{ @@ -38,4 +37,4 @@ func length(l list) int { //:: ExpectedOutput(function_termination_error) return 1 + length(l) // cause: pass l to length instead of t } -} \ No newline at end of file +} diff --git a/src/test/resources/regressions/features/adts/termination-success1.gobra b/src/test/resources/regressions/features/adts/termination-success1.gobra index d38649dbb..7c2f8fff2 100644 --- a/src/test/resources/regressions/features/adts/termination-success1.gobra +++ b/src/test/resources/regressions/features/adts/termination-success1.gobra @@ -3,22 +3,21 @@ package pkg -type tree adt{ +ghost type tree adt{ leaf{ value int } node{ left, right tree } } ghost -pure decreases len(t) -func leafCount(t tree) int { +pure func leafCount(t tree) int { return match t { case leaf{_}: 1 case node{?l, ?r}: leafCount(l) + leafCount(r) } } -type list adt { +ghost type list adt { Empty{} Cons{ @@ -53,4 +52,4 @@ func testSubSubList(l, r list) { assert len(l.tail.tail) < len(l) testSubSubList(l.tail.tail, r) } -} \ No newline at end of file +} diff --git a/src/test/resources/regressions/features/defunc/pred-construct-fail1.gobra b/src/test/resources/regressions/features/defunc/pred-construct-fail1.gobra index aa0418b0b..82404636d 100644 --- a/src/test/resources/regressions/features/defunc/pred-construct-fail1.gobra +++ b/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!) // Predicate expressions are not allowed in predicate constructors + f((*T).AccInv!) } 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!) -} \ No newline at end of file +} diff --git a/src/test/resources/regressions/features/domains/intPair.gobra b/src/test/resources/regressions/features/domains/intPair.gobra index 2c85c8a1f..59a8f4249 100644 --- a/src/test/resources/regressions/features/domains/intPair.gobra +++ b/src/test/resources/regressions/features/domains/intPair.gobra @@ -3,7 +3,7 @@ package main -type intPair domain { +ghost type intPair domain { func fst(intPair) int func snd(intPair) int func pair(int, int) intPair diff --git a/src/test/resources/regressions/features/fractional_permissions/perm-fail1.gobra b/src/test/resources/regressions/features/fractional_permissions/perm-fail1.gobra index fda7cbbf2..6094fe15a 100644 --- a/src/test/resources/regressions/features/fractional_permissions/perm-fail1.gobra +++ b/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 } diff --git a/src/test/resources/regressions/features/fractional_permissions/perm-simple1.gobra b/src/test/resources/regressions/features/fractional_permissions/perm-simple1.gobra index 0902f25f9..d13013fb3 100644 --- a/src/test/resources/regressions/features/fractional_permissions/perm-simple1.gobra +++ b/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) diff --git a/src/test/resources/regressions/features/ghost_field/ghost-embedding-fail01.gobra b/src/test/resources/regressions/features/ghost_field/ghost-embedding-fail01.gobra index 7575e2751..9b2686f6c 100644 --- a/src/test/resources/regressions/features/ghost_field/ghost-embedding-fail01.gobra +++ b/src/test/resources/regressions/features/ghost_field/ghost-embedding-fail01.gobra @@ -17,7 +17,8 @@ type TestWithActualEmbedding struct { } type TestWithGhostEmbedding struct { - ghost Embedded + //:: ExpectedOutput(type_error) + ghost Embedded // invalid as an embedding changes struct's method set and this cannot be ghost actualField2 int ghost ghostField2 int } @@ -38,19 +39,3 @@ func foo(s *TestWithActualEmbedding) { s.ghostField2 = 42 } - -ghost -decreases -preserves acc(s) -func foo2(s *TestWithGhostEmbedding) { - // writing to an actual field is forbidden in ghost code but writing to fields treated as ghost is fine - - s.actualEmbeddedField = 42 // this is fine as it's a ghost embedding - - s.ghostEmbeddedField = 42 - - //:: ExpectedOutput(type_error) - s.actualField2 = 42 - - s.ghostField2 = 42 -} diff --git a/src/test/resources/regressions/features/ghost_field/ghost-embedding-simple01.gobra b/src/test/resources/regressions/features/ghost_field/ghost-embedding-simple01.gobra index 1ac3a78e2..5dc2570dc 100644 --- a/src/test/resources/regressions/features/ghost_field/ghost-embedding-simple01.gobra +++ b/src/test/resources/regressions/features/ghost_field/ghost-embedding-simple01.gobra @@ -16,12 +16,6 @@ type TestWithActualEmbedding struct { ghost ghostField2 int } -type TestWithGhostEmbedding struct { - ghost Embedded - actualField2 int - ghost ghostField2 int -} - ghost decreases preserves acc(s) @@ -33,17 +27,3 @@ func foo(s *TestWithActualEmbedding) { //:: ExpectedOutput(assert_error:assertion_error) assert false } - -ghost -decreases -preserves acc(s) -func foo2(s *TestWithGhostEmbedding) { - // writing to an actual field is forbidden in ghost code but writing to fields treated as ghost is fine - - s.actualEmbeddedField = 42 // this is fine as it's a ghost embedding - s.ghostEmbeddedField = 42 - s.ghostField2 = 42 - - //:: ExpectedOutput(assert_error:assertion_error) - assert false -} diff --git a/src/test/resources/regressions/features/ghost_members/ghost-method-fail01.gobra b/src/test/resources/regressions/features/ghost_members/ghost-method-fail01.gobra new file mode 100644 index 000000000..50fe0a98c --- /dev/null +++ b/src/test/resources/regressions/features/ghost_members/ghost-method-fail01.gobra @@ -0,0 +1,34 @@ +// Any copyright is dedicated to the Public Domain. +// http://creativecommons.org/publicdomain/zero/1.0/ + +package ghostmethodfail01 + +// tests that actual methods cannot have a ghost receiver + +ghost type GhostStruct ghost struct { + Value int +} + +decreases +//:: ExpectedOutput(type_error) +func (a GhostStruct) ActualMethodForNonPointerReceiver() int { // fails as this _actual_ method has a _ghost_ receiver + return 42 +} + +decreases +//:: ExpectedOutput(type_error) +func (a *GhostStruct) ActualMethodForPointerReceiver() int { // fails as this _actual_ method has a _ghost_ receiver + return 42 +} + +ghost +decreases +func (a GhostStruct) GhostMethodForNonPointerReceiver() int { + return 42 +} + +ghost +decreases +func (a *GhostStruct) GhostMethodForPointerReceiver() int { + return 42 +} diff --git a/src/test/resources/regressions/features/ghost_members/ghost-method-simple01.gobra b/src/test/resources/regressions/features/ghost_members/ghost-method-simple01.gobra new file mode 100644 index 000000000..cbf8d86d4 --- /dev/null +++ b/src/test/resources/regressions/features/ghost_members/ghost-method-simple01.gobra @@ -0,0 +1,48 @@ +// Any copyright is dedicated to the Public Domain. +// http://creativecommons.org/publicdomain/zero/1.0/ + +package ghostmethodsimple01 + +// tests that ghost methods can have a ghost or actual receiver + +type ActualStruct struct { + Value int +} + +decreases +func (a ActualStruct) ActualMethodForNonPointerReceiver() int { + return 42 +} + +decreases +func (a *ActualStruct) ActualMethodForPointerReceiver() int { + return 42 +} + +ghost +decreases +func (a ActualStruct) GhostMethodForNonPointerReceiver() int { + return 42 +} + +ghost +decreases +func (a *ActualStruct) GhostMethodForPointerReceiver() int { + return 42 +} + +ghost type GhostStruct ghost struct { + Value int +} + +ghost +decreases +func (a GhostStruct) GhostMethodForNonPointerReceiver() int { + return 42 +} + +ghost +decreases +func (a *GhostStruct) GhostMethodForPointerReceiver() int { + return 42 +} diff --git a/src/test/resources/regressions/features/ghost_type/ghost-struct-comparison-fail01.gobra b/src/test/resources/regressions/features/ghost_type/ghost-struct-comparison-fail01.gobra new file mode 100644 index 000000000..49e47d7cb --- /dev/null +++ b/src/test/resources/regressions/features/ghost_type/ghost-struct-comparison-fail01.gobra @@ -0,0 +1,49 @@ +// Any copyright is dedicated to the Public Domain. +// http://creativecommons.org/publicdomain/zero/1.0/ + +package GhostStructComparison01 + +// a ghost struct cannot be compared to an actual struct + +ghost type GhostStructDef ghost struct { + f int +} + +type ActualStructDef struct { + ghost f int +} + +func foo(x ActualStructDef, ghost y GhostStructDef) { + //:: ExpectedOutput(type_error) + assert x == y // fails because x and y are different types + //:: ExpectedOutput(type_error) + assert x === y // fails because x and y are different types +} + +ghost type GhostStructAlias = ghost struct { + f int +} + +type ActualStructAlias = struct { + f int +} + +ghost +decreases +func bar(x ActualStructAlias, y struct { f int }) bool { + // type-checks because x and y have the same underlying type + return x == y && x === y +} + +type ActualStructAliasWithGhostField = struct { + ghost f int +} + +ghost +decreases +func bar2(x ActualStructAliasWithGhostField, y GhostStructAlias) { + //:: ExpectedOutput(type_error) + assert x == y // fails because the underlying types of x and y are different + //:: ExpectedOutput(type_error) + assert x === y // fails because the underlying types of x and y are different +} diff --git a/src/test/resources/regressions/features/ghost_type/ghost-struct-comparison-fail02.gobra b/src/test/resources/regressions/features/ghost_type/ghost-struct-comparison-fail02.gobra new file mode 100644 index 000000000..e6ea98301 --- /dev/null +++ b/src/test/resources/regressions/features/ghost_type/ghost-struct-comparison-fail02.gobra @@ -0,0 +1,22 @@ +// Any copyright is dedicated to the Public Domain. +// http://creativecommons.org/publicdomain/zero/1.0/ + +package GhostStructComparisonFail02 + +// tests that a ghost struct literal is not comparable to an actual struct literal + +ensures res == ghost struct {Number int}{Number: 42} +func foo() (ghost res ghost struct {Number int}) + +func main() { + res1 := foo() + //:: ExpectedOutput(type_error) + assert res1 == struct {Number int}{42} + res2 := foo() + //:: ExpectedOutput(type_error) + assert res2 == struct {Number int;}{42} + res3 := foo() + assert res3 == ghost struct {Number int}{42} + res4 := foo() + assert res4 == ghost struct {Number int;}{42} +} \ No newline at end of file diff --git a/src/test/resources/regressions/features/ghost_type/ghost-struct-comparison-simple01.gobra b/src/test/resources/regressions/features/ghost_type/ghost-struct-comparison-simple01.gobra new file mode 100644 index 000000000..ec405976e --- /dev/null +++ b/src/test/resources/regressions/features/ghost_type/ghost-struct-comparison-simple01.gobra @@ -0,0 +1,20 @@ +// Any copyright is dedicated to the Public Domain. +// http://creativecommons.org/publicdomain/zero/1.0/ + +package GhostStructComparison01 + +// when comparing ghost structs, ghost equality should be used. I.e., `==` behaves like `===`. + +ghost type GhostStruct ghost struct { + f int +} + +func test1(ghost x, y GhostStruct) { + //:: ExpectedOutput(assert_error:assertion_error) + assert x == y +} + +func test2(ghost x, y GhostStruct) { + //:: ExpectedOutput(assert_error:assertion_error) + assert x === y +} diff --git a/src/test/resources/regressions/features/ghost_type/ghost-struct-embedding-fail01.gobra b/src/test/resources/regressions/features/ghost_type/ghost-struct-embedding-fail01.gobra new file mode 100644 index 000000000..4e6f8e6ea --- /dev/null +++ b/src/test/resources/regressions/features/ghost_type/ghost-struct-embedding-fail01.gobra @@ -0,0 +1,26 @@ +// Any copyright is dedicated to the Public Domain. +// http://creativecommons.org/publicdomain/zero/1.0/ + +package GhostStructEmbeddingFail01 + +type T1 struct { + val int +} + +func (t T1) F() int { + return 42 +} + +type T struct { + //:: ExpectedOutput(type_error) + ghost T1 // ghost embedding; this is currently disallowed to fix the issue outlined in `test` below +} + +ghost type GhostT ghost struct { + ghost T1 // ghost embedding; this is okay as GhostT is a ghost struct +} + +func test(t T) { + //:: ExpectedOutput(type_error) + t.F() // this should be rejected by Gobra, because the fact that T has a method F() comes from a ghost embedding, and we are in actual code +} diff --git a/src/test/resources/regressions/features/ghost_type/ghost-struct-literal-simple01.gobra b/src/test/resources/regressions/features/ghost_type/ghost-struct-literal-simple01.gobra new file mode 100644 index 000000000..6cf915d6a --- /dev/null +++ b/src/test/resources/regressions/features/ghost_type/ghost-struct-literal-simple01.gobra @@ -0,0 +1,24 @@ +// Any copyright is dedicated to the Public Domain. +// http://creativecommons.org/publicdomain/zero/1.0/ + +package GhostStructLiteralSimple02 + +// tests that we can mix ghost struct literal and ghost struct type declarations + +ghost type GhostStruct ghost struct { + Value int +} + +ensures res == ghost struct {Value int}{Value: 42} +func foo() (ghost res GhostStruct) { + return GhostStruct{ 42 } +} + +func main() { + res1 := foo() + assert res1 == ghost struct {Value int}{42} + res2 := foo() + assert res2 == GhostStruct{42} + //:: ExpectedOutput(assert_error:assertion_error) + assert false +} diff --git a/src/test/resources/regressions/features/ghost_type/ghost-struct-type-fail01.gobra b/src/test/resources/regressions/features/ghost_type/ghost-struct-type-fail01.gobra new file mode 100644 index 000000000..61d504891 --- /dev/null +++ b/src/test/resources/regressions/features/ghost_type/ghost-struct-type-fail01.gobra @@ -0,0 +1,26 @@ +// Any copyright is dedicated to the Public Domain. +// http://creativecommons.org/publicdomain/zero/1.0/ + +package GhostStructTypeFail01 + +// tests the invalid combinations compared to `ghost-struct-type-simple01.gobra` + +//:: ExpectedOutput(type_error) +type ActualNamedGhostStruct ghost struct { // actual type definition with ghost type is not allowed + Value int +} + +//:: ExpectedOutput(type_error) +type ActualAliasGhostStruct = ghost struct { // actual type definition with ghost type is not allowed + Value int +} + +//:: ExpectedOutput(type_error) +ghost type GhostNamedActualStruct struct { // ghost type definition with actual type is not allowed + Value int +} + +//:: ExpectedOutput(type_error) +ghost type GhostAliasActualStruct = struct { // ghost type definition with actual type is not allowed + Value int +} diff --git a/src/test/resources/regressions/features/ghost_type/ghost-struct-type-fail02.gobra b/src/test/resources/regressions/features/ghost_type/ghost-struct-type-fail02.gobra new file mode 100644 index 000000000..1564e2601 --- /dev/null +++ b/src/test/resources/regressions/features/ghost_type/ghost-struct-type-fail02.gobra @@ -0,0 +1,20 @@ +// Any copyright is dedicated to the Public Domain. +// http://creativecommons.org/publicdomain/zero/1.0/ + +package GhostStructTypeFail02 + +// checks that fields of a ghost struct type are treated as ghost fields + +ghost type GhostStruct ghost struct { + f int +} + +func foo(ghost s GhostStruct) int { + s.f = 42 + //:: ExpectedOutput(type_error) + checkThatArgIsActual(s.f) +} + +func checkThatArgIsActual(input int) int { + return input +} diff --git a/src/test/resources/regressions/features/ghost_type/ghost-struct-type-simple01.gobra b/src/test/resources/regressions/features/ghost_type/ghost-struct-type-simple01.gobra new file mode 100644 index 000000000..11f92d85b --- /dev/null +++ b/src/test/resources/regressions/features/ghost_type/ghost-struct-type-simple01.gobra @@ -0,0 +1,50 @@ +// Any copyright is dedicated to the Public Domain. +// http://creativecommons.org/publicdomain/zero/1.0/ + +package GhostStructTypeSimple01 + +// This testcase test valid combinations of ghost / actual type def and actual / ghost underlying types. +// Combinations that are invalid are in `ghost-struct-type-fail01.gobra` + +type ActualNamedActualStruct struct { + Value int +} + +// invalid +// type ActualNamedGhostStruct ghost struct { +// Value int +// } + +// invalid +// ghost type GhostNamedActualStruct struct { +// Value int +// } + +ghost type GhostNamedGhostStruct ghost struct { + Value int +} + +decreases +func actualFn(a ActualNamedActualStruct, ghost b GhostNamedGhostStruct) { + a.Value = 42 + assert a.Value == 42 + + b.Value = 42 + assert b.Value == 42 + + //:: ExpectedOutput(assert_error:assertion_error) + assert false +} + +ghost +decreases +func ghostFn(a ActualNamedActualStruct, b GhostNamedGhostStruct) { + a.Value = 42 + assert a.Value == 42 + + b.Value = 42 + assert b.Value == 42 + + //:: ExpectedOutput(assert_error:assertion_error) + assert false +} diff --git a/src/test/resources/regressions/features/ghost_type/ghost-type-decl-fail01.gobra b/src/test/resources/regressions/features/ghost_type/ghost-type-decl-fail01.gobra new file mode 100644 index 000000000..a0545219e --- /dev/null +++ b/src/test/resources/regressions/features/ghost_type/ghost-type-decl-fail01.gobra @@ -0,0 +1,21 @@ +// Any copyright is dedicated to the Public Domain. +// http://creativecommons.org/publicdomain/zero/1.0/ + +package GhostTypeDeclFail01 + +//:: ExpectedOutput(type_error) +ghost type GhostIntDef int // int is not a ghost type +//:: ExpectedOutput(type_error) +ghost type GhostIntAlias = int // int is not a ghost type +ghost type GhostSetDef set[int] +ghost type GhostSetAlias = set[int] + +//:: ExpectedOutput(type_error) +func bar1(i GhostSetDef) { // i must be a ghost parameter + +} + +//:: ExpectedOutput(type_error) +func bar2(i GhostSetAlias) { // i must be a ghost parameter + +} diff --git a/src/test/resources/regressions/features/ghost_type/ghost-type-decl-fail02.gobra b/src/test/resources/regressions/features/ghost_type/ghost-type-decl-fail02.gobra new file mode 100644 index 000000000..7f072c180 --- /dev/null +++ b/src/test/resources/regressions/features/ghost_type/ghost-type-decl-fail02.gobra @@ -0,0 +1,35 @@ +// Any copyright is dedicated to the Public Domain. +// http://creativecommons.org/publicdomain/zero/1.0/ + +package GhostTypeDeclSimple02 + +// tests that ghost type declarations are treated as being ghost + +ghost type NamedGhostStructDef ghost struct { + Value int +} +ghost type NamedGhostStructAlias = ghost struct { + Value int +} +ghost type SetDef set[int] +ghost type SetAlias = set[int] + +//:: ExpectedOutput(type_error) +func actualFn1a(a NamedGhostStructDef) // fails as `a` must be ghost + +func actualFn1b(ghost a NamedGhostStructDef) + +//:: ExpectedOutput(type_error) +func actualFn2a(a NamedGhostStructAlias) // fails as `a` must be ghost + +func actualFn2b(ghost a NamedGhostStructAlias) + +//:: ExpectedOutput(type_error) +func actualFn3a(a SetDef) // fails as `a` must be ghost + +func actualFn3b(ghost a SetDef) + +//:: ExpectedOutput(type_error) +func actualFn4a(a SetAlias) // fails as `a` must be ghost + +func actualFn4b(ghost a SetAlias) diff --git a/src/test/resources/regressions/features/ghost_type/ghost-type-decl-fail03.gobra b/src/test/resources/regressions/features/ghost_type/ghost-type-decl-fail03.gobra new file mode 100644 index 000000000..8578a1402 --- /dev/null +++ b/src/test/resources/regressions/features/ghost_type/ghost-type-decl-fail03.gobra @@ -0,0 +1,13 @@ +// Any copyright is dedicated to the Public Domain. +// http://creativecommons.org/publicdomain/zero/1.0/ + +package GhostTypeDeclSimple03 + +//:: ExpectedOutput(type_error) +ghost type GhostIntDef int // int is not a ghost type +//:: ExpectedOutput(type_error) +ghost type GhostIntAlias = int // int is not a ghost type +//:: ExpectedOutput(type_error) +type SetDef set[int] // set[int] is not an actual type +//:: ExpectedOutput(type_error) +type SetAlias = set[int] // set[int] is not an actual type diff --git a/src/test/resources/regressions/features/ghost_type/ghost-type-decl-simple01.gobra b/src/test/resources/regressions/features/ghost_type/ghost-type-decl-simple01.gobra new file mode 100644 index 000000000..04cf19335 --- /dev/null +++ b/src/test/resources/regressions/features/ghost_type/ghost-type-decl-simple01.gobra @@ -0,0 +1,20 @@ +// Any copyright is dedicated to the Public Domain. +// http://creativecommons.org/publicdomain/zero/1.0/ + +package GhostTypeDeclSimple01 + +// checks that assignments work irrespective of actual / ghost parameters being type definitions or aliases + +type ActualIntDef int +type ActualIntAlias = int + +decreases +func actualFn(a ActualIntDef, ghost b ActualIntDef, c ActualIntAlias, ghost d ActualIntAlias) { + a = 42 + b = 42 + c = 42 + d = 42 + + //:: ExpectedOutput(assert_error:assertion_error) + assert false +} diff --git a/src/test/resources/regressions/features/ghost_type/ghost-type-decl-simple02.gobra b/src/test/resources/regressions/features/ghost_type/ghost-type-decl-simple02.gobra new file mode 100644 index 000000000..c7f798c78 --- /dev/null +++ b/src/test/resources/regressions/features/ghost_type/ghost-type-decl-simple02.gobra @@ -0,0 +1,23 @@ +// Any copyright is dedicated to the Public Domain. +// http://creativecommons.org/publicdomain/zero/1.0/ + +package GhostTypeDeclSimple02 + +// tests that ghost type declarations can be used as ghost parameters + +ghost type SetDef set[int] + +ghost type SetAlias = set[int] + +ghost +decreases +func ghostFn2(a SetDef, b SetAlias) { + a = set[int]{ 42 } + assert a == set[int]{ 42 } + + b = set[int]{ 42 } + assert b == set[int]{ 42 } + + //:: ExpectedOutput(assert_error:assertion_error) + assert false +} diff --git a/src/test/resources/regressions/features/import/error_reporting_import3/foo/foo.gobra b/src/test/resources/regressions/features/import/error_reporting_import3/foo/foo.gobra new file mode 100644 index 000000000..91cc85de6 --- /dev/null +++ b/src/test/resources/regressions/features/import/error_reporting_import3/foo/foo.gobra @@ -0,0 +1,9 @@ +// Any copyright is dedicated to the Public Domain. +// http://creativecommons.org/publicdomain/zero/1.0/ + +package foo + +//:: ExpectedOutput(type_error) +type ErroneousType adt { // invalid as this must be a _ghost_ type definition + None {} +} diff --git a/src/test/resources/regressions/features/import/error_reporting_import3/main.gobra b/src/test/resources/regressions/features/import/error_reporting_import3/main.gobra new file mode 100644 index 000000000..2803154d8 --- /dev/null +++ b/src/test/resources/regressions/features/import/error_reporting_import3/main.gobra @@ -0,0 +1,27 @@ +// Any copyright is dedicated to the Public Domain. +// http://creativecommons.org/publicdomain/zero/1.0/ + +package ErrorReportingImport2 + +// this test triggers a special case within `getTypeFromCtxt` namely where typing the base of a PInvoke +// returns UnknownType as the invoked function contains a type error. +// However, this has been addressed by PR #855 that stops this package from getting type-checked in the first place +// as foo contains a type error. Thus, the only error occurring in this file is located at the import clause (as +// opposed to reporting an error for the pure function's definition or its use). + +// ##(-I ./) + +//:: ExpectedOutput(type_error) +import foo "foo" + +const ConstantForWhichTypeMustBeInferred = 42 + +ghost +decreases +pure func ErroneousFunction(paramTriggeringIntResolution int) foo.ErroneousType { + return foo.None{} +} + +func triggerGetTypeFromCtxtCornerCase() { + assert ErroneousFunction(0) == foo.None{} +} diff --git a/src/test/resources/regressions/features/maps/maps-fail3.gobra b/src/test/resources/regressions/features/maps/maps-fail3.gobra new file mode 100644 index 000000000..f094091a5 --- /dev/null +++ b/src/test/resources/regressions/features/maps/maps-fail3.gobra @@ -0,0 +1,29 @@ +// Any copyright is dedicated to the Public Domain. +// http://creativecommons.org/publicdomain/zero/1.0/ + +package mapsfail3 + +// tests that neither structs with ghost fields, ghost structs, nor other ghost types can serve as a map's key + +type ActualStruct struct { + ghost f int +} + +ghost type GhostStruct ghost struct { + f int +} + +//:: ExpectedOutput(type_error) +func test1(m map[ActualStruct]int) int { + return 42 +} + +//:: ExpectedOutput(type_error) +func test2(m map[GhostStruct]int) int { + return 42 +} + +//:: ExpectedOutput(type_error) +func test3(m map[seq[int]]int) int { + return 42 +} diff --git a/src/test/resources/regressions/issues/000228-1.gobra b/src/test/resources/regressions/issues/000228-1.gobra index 668f8a065..438e57b82 100644 --- a/src/test/resources/regressions/issues/000228-1.gobra +++ b/src/test/resources/regressions/issues/000228-1.gobra @@ -6,9 +6,9 @@ package types type TSlice []int type TArray [2]int type TMap map[int]string -type TSeq seq[int] -type TSet set[int] -type TMSet mset[int] +ghost type TSeq seq[int] +ghost type TSet set[int] +ghost type TMSet mset[int] // Cannot parse a dict type in a type declaration // type TDict dict[int]int diff --git a/src/test/resources/regressions/issues/000228-2.gobra b/src/test/resources/regressions/issues/000228-2.gobra index 3c855cad1..d56030975 100644 --- a/src/test/resources/regressions/issues/000228-2.gobra +++ b/src/test/resources/regressions/issues/000228-2.gobra @@ -6,9 +6,9 @@ package types type TSlice = []int type TArray = [2]int type TMap = map[int]string -type TSeq = seq[int] -type TSet = set[int] -type TMSet = mset[int] +ghost type TSeq = seq[int] +ghost type TSet = set[int] +ghost type TMSet = mset[int] // Cannot parse a dict type in a type declaration // type TDict = dict[int]int diff --git a/src/test/resources/regressions/issues/000589.gobra b/src/test/resources/regressions/issues/000589.gobra index 207b2d8d4..a47e00d1d 100644 --- a/src/test/resources/regressions/issues/000589.gobra +++ b/src/test/resources/regressions/issues/000589.gobra @@ -3,7 +3,7 @@ package pkg -type list adt { +ghost type list adt { Empty{} Cons{ @@ -23,4 +23,4 @@ func length(l list) int { default: return 0 } -} \ No newline at end of file +} diff --git a/src/test/resources/regressions/issues/000641.gobra b/src/test/resources/regressions/issues/000641.gobra index 7477f710f..bdc40bbf5 100644 --- a/src/test/resources/regressions/issues/000641.gobra +++ b/src/test/resources/regressions/issues/000641.gobra @@ -3,17 +3,20 @@ package pkg -type X adt { +ghost type X adt { C{ c int } } ghost +decreases func foo1(x X) +// ADTs can also be used as receivers: ghost +decreases func (x X) bar1() func client() { foo1(C{}) C{}.bar1() -} \ No newline at end of file +} diff --git a/src/test/resources/regressions/issues/000651.gobra b/src/test/resources/regressions/issues/000651.gobra index d199f9546..8c3ce2c15 100644 --- a/src/test/resources/regressions/issues/000651.gobra +++ b/src/test/resources/regressions/issues/000651.gobra @@ -3,7 +3,7 @@ package test -type A adt { +ghost type A adt { A_ { a uint b set[int] @@ -22,4 +22,4 @@ pure func f(x A) A { c: x.c, d: x.d, e: x.e} -} \ No newline at end of file +} diff --git a/src/test/resources/regressions/issues/000655.gobra b/src/test/resources/regressions/issues/000655.gobra index 72202eb71..9b6123b9c 100644 --- a/src/test/resources/regressions/issues/000655.gobra +++ b/src/test/resources/regressions/issues/000655.gobra @@ -7,6 +7,7 @@ package test import "pkg" ghost +decreases len(x) pure func foo(x pkg.List) bool { return match x { case pkg.Nil{}: true @@ -16,6 +17,7 @@ pure func foo(x pkg.List) bool { } ghost +decreases func foo2() { var x pkg.Tree = pkg.Branch{} y := pkg.Branch{Left: x} @@ -24,7 +26,6 @@ func foo2() { /* // should work in the future: - ghost pure func foo3(x pkg.Tree) bool { return match x { @@ -34,4 +35,4 @@ pure func foo3(x pkg.Tree) bool { case _: false } } -*/ \ No newline at end of file +*/ diff --git a/src/test/resources/regressions/issues/000655/pkg/f.gobra b/src/test/resources/regressions/issues/000655/pkg/f.gobra index 6df472b61..56370835d 100644 --- a/src/test/resources/regressions/issues/000655/pkg/f.gobra +++ b/src/test/resources/regressions/issues/000655/pkg/f.gobra @@ -3,7 +3,7 @@ package pkg -type List adt { +ghost type List adt { Cons { head int tail List @@ -12,11 +12,10 @@ type List adt { Nil {} } -type Tree adt { +ghost type Tree adt { Leaf{} Branch{ Left, Right Tree } } func Leaf() { } - diff --git a/src/test/resources/regressions/issues/000685.gobra b/src/test/resources/regressions/issues/000685.gobra index 98a8388b2..d3ece380b 100644 --- a/src/test/resources/regressions/issues/000685.gobra +++ b/src/test/resources/regressions/issues/000685.gobra @@ -3,7 +3,7 @@ package pkg -type X adt { +ghost type X adt { C{ c any } } diff --git a/src/test/resources/regressions/issues/000686-1.gobra b/src/test/resources/regressions/issues/000686-1.gobra index 8c76b33ee..ac16f6c24 100644 --- a/src/test/resources/regressions/issues/000686-1.gobra +++ b/src/test/resources/regressions/issues/000686-1.gobra @@ -3,7 +3,7 @@ package pkg -type X adt { +ghost type X adt { A { a int } B { b bool } } diff --git a/src/test/resources/regressions/issues/000686-2.gobra b/src/test/resources/regressions/issues/000686-2.gobra index c7a30bfe0..72307ba8e 100644 --- a/src/test/resources/regressions/issues/000686-2.gobra +++ b/src/test/resources/regressions/issues/000686-2.gobra @@ -3,7 +3,7 @@ package pkg -type X adt { +ghost type X adt { A { a int } B { b bool } } diff --git a/src/test/resources/regressions/issues/000686-3.gobra b/src/test/resources/regressions/issues/000686-3.gobra index c145f4ba5..109f1939d 100644 --- a/src/test/resources/regressions/issues/000686-3.gobra +++ b/src/test/resources/regressions/issues/000686-3.gobra @@ -3,7 +3,7 @@ package pkg -type X adt { +ghost type X adt { A { int } B { bool; bool } C {} diff --git a/src/test/resources/regressions/issues/000686-4.gobra b/src/test/resources/regressions/issues/000686-4.gobra index 435cb1095..eb30fb5eb 100644 --- a/src/test/resources/regressions/issues/000686-4.gobra +++ b/src/test/resources/regressions/issues/000686-4.gobra @@ -3,13 +3,15 @@ package pkg -type X seq[int] +ghost type X seq[int] ghost +decreases requires x == x ++ y func client1(x seq[int], y X) ghost +decreases requires typeOf(y) == type[X] requires x == x ++ y.(X) func client2(x seq[int], y any) diff --git a/src/test/resources/regressions/issues/000686-5.gobra b/src/test/resources/regressions/issues/000686-5.gobra index 435cb1095..eb30fb5eb 100644 --- a/src/test/resources/regressions/issues/000686-5.gobra +++ b/src/test/resources/regressions/issues/000686-5.gobra @@ -3,13 +3,15 @@ package pkg -type X seq[int] +ghost type X seq[int] ghost +decreases requires x == x ++ y func client1(x seq[int], y X) ghost +decreases requires typeOf(y) == type[X] requires x == x ++ y.(X) func client2(x seq[int], y any) diff --git a/src/test/scala/viper/gobra/erasing/GhostErasureUnitTests.scala b/src/test/scala/viper/gobra/erasing/GhostErasureUnitTests.scala index bd39c248d..8f00dcb46 100644 --- a/src/test/scala/viper/gobra/erasing/GhostErasureUnitTests.scala +++ b/src/test/scala/viper/gobra/erasing/GhostErasureUnitTests.scala @@ -315,6 +315,30 @@ class GhostErasureUnitTests extends AnyFunSuite with Matchers with Inside { frontend.testProg(input, expected) } + test("Ghost Erasure: ghost types should be erased") { + val input = + s""" + |package pkg + |type Struct struct { + | f int + | ghost g int + |} + |ghost type GhostStruct struct { + | f int + |} + |ghost type GhostIntDef int + |ghost type GhostIntAlias = int + |""".stripMargin + val expected = + s""" + |package pkg + |type Struct struct { + | f int + |} + |""".stripMargin + frontend.testProg(input, expected) + } + /* ** Stubs, mocks, and other test setup */ class TestFrontend { diff --git a/src/test/scala/viper/gobra/parsing/ParserTestFrontend.scala b/src/test/scala/viper/gobra/parsing/ParserTestFrontend.scala index 66fdb06ae..e9699c2e4 100644 --- a/src/test/scala/viper/gobra/parsing/ParserTestFrontend.scala +++ b/src/test/scala/viper/gobra/parsing/ParserTestFrontend.scala @@ -34,6 +34,6 @@ class ParserTestFrontend { def parseType(source : String) : Either[Vector[ParserError], PType] = parse(source, Parser.parseType) def parseTypeOrFail(source : String) : PType = parseOrFail(source, Parser.parseType) def parseImportDecl(source: String): Vector[PImport] = parseOrFail(source, Parser.parseImportDecl) - def parseFunctionDecl(source: String, specOnly: Boolean = false): PMember = parseOrFail(source, (s: Source) => Parser.parseFunction(s, specOnly = specOnly)) - -} \ No newline at end of file + def parseMember(source: String, specOnly: Boolean = false): Either[Vector[ParserError], Vector[PMember]] = parse(source, (s: Source) => Parser.parseMember(s, specOnly = specOnly)) + def parseMemberOrFail(source: String, specOnly: Boolean = false): Vector[PMember] = parseOrFail(source, (s: Source) => Parser.parseMember(s, specOnly = specOnly)) +} diff --git a/src/test/scala/viper/gobra/parsing/ParserUnitTests.scala b/src/test/scala/viper/gobra/parsing/ParserUnitTests.scala index bd9fd62c7..5f9992921 100644 --- a/src/test/scala/viper/gobra/parsing/ParserUnitTests.scala +++ b/src/test/scala/viper/gobra/parsing/ParserUnitTests.scala @@ -119,20 +119,20 @@ class ParserUnitTests extends AnyFunSuite with Matchers with Inside { } test("Parser: spec only function") { - frontend.parseFunctionDecl("func foo() { b.bar() }", specOnly = true) should matchPattern { - case PFunctionDecl(PIdnDef("foo"), Vector(), PResult(Vector()), PFunctionSpec(Vector(), Vector(), Vector(), Vector(), Vector(), false, false, false), None) => + frontend.parseMemberOrFail("func foo() { b.bar() }", specOnly = true) should matchPattern { + case Vector(PFunctionDecl(PIdnDef("foo"), Vector(), PResult(Vector()), PFunctionSpec(Vector(), Vector(), Vector(), Vector(), Vector(), false, false, false), None)) => } } test("Parser: spec only function with nested blocks") { - frontend.parseFunctionDecl("func foo() { if(true) { b.bar() } else { foo() } }", specOnly = true) should matchPattern { - case PFunctionDecl(PIdnDef("foo"), Vector(), PResult(Vector()), PFunctionSpec(Vector(), Vector(), Vector(), Vector(), Vector(), false, false, false), None) => + frontend.parseMemberOrFail("func foo() { if(true) { b.bar() } else { foo() } }", specOnly = true) should matchPattern { + case Vector(PFunctionDecl(PIdnDef("foo"), Vector(), PResult(Vector()), PFunctionSpec(Vector(), Vector(), Vector(), Vector(), Vector(), false, false, false), None)) => } } test("Parser: spec only function with incomplete nested blocks") { an [TestFailedException] should be thrownBy - frontend.parseFunctionDecl("func foo() { if(true) { b.bar() } else { foo() }", specOnly = true) + frontend.parseMemberOrFail("func foo() { if(true) { b.bar() } else { foo() }", specOnly = true) } test("Parser: imported struct initialization") { @@ -158,8 +158,8 @@ class ParserUnitTests extends AnyFunSuite with Matchers with Inside { test("Parser: abstract function") { val modes: Set[Boolean] = Set(false, true) modes.foreach(specOnly => { - frontend.parseFunctionDecl("func bar()", specOnly) should matchPattern { - case PFunctionDecl(PIdnDef("bar"), Vector(), PResult(Vector()), PFunctionSpec(Vector(), Vector(), Vector(), Vector(), Vector(), false, false, false), None) => + frontend.parseMemberOrFail("func bar()", specOnly) should matchPattern { + case Vector(PFunctionDecl(PIdnDef("bar"), Vector(), PResult(Vector()), PFunctionSpec(Vector(), Vector(), Vector(), Vector(), Vector(), false, false, false), None)) => } }) } @@ -2642,20 +2642,20 @@ class ParserUnitTests extends AnyFunSuite with Matchers with Inside { } test("Parser: should be able to parse normal termination measure") { - frontend.parseFunctionDecl("decreases n; func factorial (n int) int") should matchPattern { - case PFunctionDecl(PIdnDef("factorial"), Vector(PNamedParameter(PIdnDef("n"), PIntType())), PResult(Vector(PUnnamedParameter(PIntType()))), PFunctionSpec(Vector(), Vector(), Vector(), Vector(PTupleTerminationMeasure(Vector(PNamedOperand(PIdnUse("n"))), None)), Vector(), false, false, false), None) => + frontend.parseMemberOrFail("decreases n; func factorial (n int) int") should matchPattern { + case Vector(PFunctionDecl(PIdnDef("factorial"), Vector(PNamedParameter(PIdnDef("n"), PIntType())), PResult(Vector(PUnnamedParameter(PIntType()))), PFunctionSpec(Vector(), Vector(), Vector(), Vector(PTupleTerminationMeasure(Vector(PNamedOperand(PIdnUse("n"))), None)), Vector(), false, false, false), None)) => } } test("Parser: should be able to parse underscore termination measure") { - frontend.parseFunctionDecl("decreases _; func factorial (n int) int") should matchPattern { - case PFunctionDecl(PIdnDef("factorial"), Vector(PNamedParameter(PIdnDef("n"), PIntType())), PResult(Vector(PUnnamedParameter(PIntType()))), PFunctionSpec(Vector(), Vector(), Vector(), Vector(PWildcardMeasure(None)), Vector(), false, false, false), None) => + frontend.parseMemberOrFail("decreases _; func factorial (n int) int") should matchPattern { + case Vector(PFunctionDecl(PIdnDef("factorial"), Vector(PNamedParameter(PIdnDef("n"), PIntType())), PResult(Vector(PUnnamedParameter(PIntType()))), PFunctionSpec(Vector(), Vector(), Vector(), Vector(PWildcardMeasure(None)), Vector(), false, false, false), None)) => } } test("Parser: should be able to parse conditional termination measure" ) { - frontend.parseFunctionDecl("decreases n if n>1; decreases _ if n<2; func factorial (n int) int") should matchPattern { - case PFunctionDecl(PIdnDef("factorial"), Vector(PNamedParameter(PIdnDef("n"), PIntType())), PResult(Vector(PUnnamedParameter(PIntType()))), PFunctionSpec(Vector(), Vector(), Vector(), Vector(PTupleTerminationMeasure(Vector(PNamedOperand(PIdnUse("n"))), Some(PGreater(PNamedOperand(PIdnUse("n")), PIntLit(one, Decimal)))), PWildcardMeasure(Some(PLess(PNamedOperand(PIdnUse("n")), PIntLit(two, Decimal))))), Vector(), false, false, false), None) if one == 1 && two == 2 => + frontend.parseMemberOrFail("decreases n if n>1; decreases _ if n<2; func factorial (n int) int") should matchPattern { + case Vector(PFunctionDecl(PIdnDef("factorial"), Vector(PNamedParameter(PIdnDef("n"), PIntType())), PResult(Vector(PUnnamedParameter(PIntType()))), PFunctionSpec(Vector(), Vector(), Vector(), Vector(PTupleTerminationMeasure(Vector(PNamedOperand(PIdnUse("n"))), Some(PGreater(PNamedOperand(PIdnUse("n")), PIntLit(one, Decimal)))), PWildcardMeasure(Some(PLess(PNamedOperand(PIdnUse("n")), PIntLit(two, Decimal))))), Vector(), false, false, false), None)) if one == 1 && two == 2 => } } @@ -2685,8 +2685,8 @@ class ParserUnitTests extends AnyFunSuite with Matchers with Inside { } test("Parser: should be able to parse a labeled continue statement") { - frontend.parseFunctionDecl("func main() {continue l}") should matchPattern { - case PFunctionDecl(_, _, _, _, Some((_, PBlock(Vector(PContinue(Some(p))))))) if p.name == "l" => + frontend.parseMemberOrFail("func main() {continue l}") should matchPattern { + case Vector(PFunctionDecl(_, _, _, _, Some((_, PBlock(Vector(PContinue(Some(p)))))))) if p.name == "l" => } } @@ -2696,4 +2696,29 @@ class ParserUnitTests extends AnyFunSuite with Matchers with Inside { if varname == "x" && value == PIntLit(42) => } } + + test("Parser: should be able to parse an int ghost type declaration") { + frontend.parseMemberOrFail("ghost type MyInt int") should matchPattern { + case Vector(PExplicitGhostMember(PTypeDef(PIntType(), PIdnDef("MyInt")))) => + } + } + + test("Parser: should be able to parse a struct ghost type declaration") { + frontend.parseMemberOrFail("ghost type MyStruct struct { Value int }") should matchPattern { + case Vector(PExplicitGhostMember(PTypeDef(PStructType(Vector(PFieldDecls(Vector(PFieldDecl(PIdnDef("Value"), PIntType()))))), PIdnDef("MyStruct")))) => + } + } + + test("Parser: should be able to parse a ghost struct type declaration") { + // this definition will fail type checking but in order to provide better error messages, we nevertheless parse it + frontend.parseMemberOrFail("type MyStruct ghost struct { Value int }") should matchPattern { + case Vector(PTypeDef(PExplicitGhostStructType(PStructType(Vector(PFieldDecls(Vector(PFieldDecl(PIdnDef("Value"), PIntType())))))), PIdnDef("MyStruct"))) => + } + } + + test("Parser: should be able to parse a ghost struct ghost type declaration") { + frontend.parseMemberOrFail("ghost type MyStruct ghost struct { Value int }") should matchPattern { + case Vector(PExplicitGhostMember(PTypeDef(PExplicitGhostStructType(PStructType(Vector(PFieldDecls(Vector(PFieldDecl(PIdnDef("Value"), PIntType())))))), PIdnDef("MyStruct")))) => + } + } } diff --git a/src/test/scala/viper/gobra/typing/MemberTypingUnitTests.scala b/src/test/scala/viper/gobra/typing/MemberTypingUnitTests.scala new file mode 100644 index 000000000..aca8e4272 --- /dev/null +++ b/src/test/scala/viper/gobra/typing/MemberTypingUnitTests.scala @@ -0,0 +1,131 @@ +// This Source Code Form is subject to the terms of the Mozilla Public +// License, v. 2.0. If a copy of the MPL was not distributed with this +// file, You can obtain one at http://mozilla.org/MPL/2.0/. +// +// Copyright (c) 2011-2025 ETH Zurich. + +package viper.gobra.typing + +import org.bitbucket.inkytonik.kiama.util.Positions +import org.scalatest.Inside +import org.scalatest.funsuite.AnyFunSuite +import org.scalatest.matchers.should.Matchers +import viper.gobra.ast.frontend.{PExplicitGhostMember, PExplicitGhostStructType, PFieldDecl, PFieldDecls, PGhostifier, PIdnDef, PIdnNode, PIdnUse, PIntType, PMember, PNamedOperand, PPackage, PPackageClause, PPkgDef, PProgram, PStructType, PTypeDecl, PTypeDef, PVarDecl, PositionManager} +import viper.gobra.frontend.info.Info +import viper.gobra.frontend.info.base.{SymbolTable, Type} +import viper.gobra.frontend.info.implementation.TypeInfoImpl +import viper.gobra.frontend.{Config, PackageInfo} + +class MemberTypingUnitTests extends AnyFunSuite with Matchers with Inside { + val frontend = new TestFrontend() + + test("Typing: An int ghost type declaration is ghost") { + // syntax: "ghost type MyInt int" + val idnDef = PIdnDef("MyInt") + val typ = PTypeDef(PIntType(), idnDef) + val decl = PExplicitGhostMember(typ) + frontend.symbolTableEntry(decl)(idnDef) should matchPattern { + case SymbolTable.NamedType(typDef, true, _) if typDef == typ => + } + } + + test("Typing: a struct ghost type declaration is ghost") { + // syntax: "ghost type MyStruct struct { Value int }" + val idnDef = PIdnDef("MyStruct") + val typ = PTypeDef(PStructType(Vector(PFieldDecls(Vector(PFieldDecl(PIdnDef("Value"), PIntType()))))), idnDef) + val decl = PExplicitGhostMember(typ) + frontend.symbolTableEntry(decl)(idnDef) should matchPattern { + case SymbolTable.NamedType(typDef, true, _) if typDef == typ => + } + } + + test("Typing: a ghost struct type declaration is not ghost") { + // syntax: "type MyStruct ghost struct { Value int }" + val idnDef = PIdnDef("MyStruct") + val typ = PTypeDef(PExplicitGhostStructType(PStructType(Vector(PFieldDecls(Vector(PFieldDecl(PIdnDef("Value"), PIntType())))))), idnDef) + frontend.symbolTableEntry(typ)(idnDef) should matchPattern { + case SymbolTable.NamedType(typDef, false, _) if typDef == typ => + } + frontend.typeDeclUnderlyingTyp(typ) should matchPattern { + case Type.StructT(_, true, _, _) => + } + } + + test("Typing: a ghost struct ghost type declaration is ghost") { + // syntax: "ghost type MyStruct ghost struct { Value int }" + val idnDef = PIdnDef("MyStruct") + val typ = PTypeDef(PExplicitGhostStructType(PStructType(Vector(PFieldDecls(Vector(PFieldDecl(PIdnDef("Value"), PIntType())))))), idnDef) + frontend.symbolTableEntry(PExplicitGhostMember(typ))(idnDef) should matchPattern { + case SymbolTable.NamedType(typDef, true, _) if typDef == typ => + } + frontend.typeDeclUnderlyingTyp(typ) should matchPattern { + case Type.StructT(_, true, _, _) => + } + } + + + class TestFrontend { + + /** + * Creates the program: + * + * package pkg + * + * + * var x // if idnUse is provided + * + * and returns the program as well as x's PIdnDef (if it got inserted) + */ + def singleMemberProgram(member: PMember, idnUse: Option[PIdnUse]): (PProgram, Option[PIdnDef]) = { + val idnDefX = PIdnDef("x") + val optVarDecl = idnUse.map(id => PVarDecl(Some(PNamedOperand(id)), Vector.empty, Vector(idnDefX), Vector(false))) + val members = optVarDecl.map(varDecl => Vector(member, varDecl)).getOrElse(Vector(member)) + val prog = PProgram( + PPackageClause(PPkgDef("pkg")), + Vector(), + Vector(), + members + ) + (prog, idnUse.map(_ => idnDefX)) + } + + def singleMemberTypeInfoAndIdnDef(member: PMember, idnUse: Option[PIdnUse] = None): (TypeInfoImpl, Option[PIdnDef]) = { + val (program, idnDef) = singleMemberProgram(member, idnUse) + val positions = new Positions + val pkg = PPackage( + PPackageClause(PPkgDef("pkg")), + Vector(program), + new PositionManager(positions), + new PackageInfo("pkg", "pkg", false) + ) + val tree = new Info.GoTree(pkg) + val config = Config() + (new TypeInfoImpl(tree, Map.empty)(config), idnDef) + } + + def singleMemberTypeInfo(member: PMember, idnUse: Option[PIdnUse] = None): TypeInfoImpl = + singleMemberTypeInfoAndIdnDef(member, idnUse)._1 + + def wellDefMember(member: PMember) = + singleMemberTypeInfo(member).wellDefMember(member) + + def symbolTableEntry(member: PMember)(id: PIdnNode): SymbolTable.Regular = + singleMemberTypeInfo(member).regular(id) + + def typeDeclUnderlyingTyp(typeDecl: PTypeDecl): Type.Type = { + val idnUse = PIdnUse(typeDecl.left.name) + val (info, optIdnDef) = singleMemberTypeInfoAndIdnDef(typeDecl, Some(idnUse)) + val idnDef = optIdnDef.get + val typ = info.typ(idnDef) + info.underlyingType(typ) + } + + def ghostTypeDeclUnderlyingTyp(typeDecl: PGhostifier[PTypeDecl] with PMember): Type.Type = { + val idnUse = PIdnUse(typeDecl.actual.left.name) + val (info, optIdnDef) = singleMemberTypeInfoAndIdnDef(typeDecl, Some(idnUse)) + val idnDef = optIdnDef.get + val typ = info.typ(idnDef) + info.underlyingType(typ) + } + } +}