diff --git a/RELEASE_NOTES.md b/RELEASE_NOTES.md index 3af43390981..6bad38834ba 100644 --- a/RELEASE_NOTES.md +++ b/RELEASE_NOTES.md @@ -18,6 +18,7 @@ - fix: Check all compiled expressions to be compilable (https://github.com/dafny-lang/dafny/pull/2641) - fix: Better messages on hovering failing postconditions in IDE (https://github.com/dafny-lang/dafny/pull/2654) - fix: Better error reporting on counter-examples if an option is not provided (https://github.com/dafny-lang/dafny/pull/2650) +- feat: Introduced ghost constructors in datatypes. One use of these is when working with uninitialized storage, see https://github.com/dafny-lang/rfcs/pull/11. (https://github.com/dafny-lang/dafny/pull/2666) # 3.8.0 diff --git a/Source/DafnyCore/AST/Expressions.cs b/Source/DafnyCore/AST/Expressions.cs index 96b6d92878a..853c9181964 100644 --- a/Source/DafnyCore/AST/Expressions.cs +++ b/Source/DafnyCore/AST/Expressions.cs @@ -1263,6 +1263,7 @@ public class MemberSelectExpr : Expression { public readonly string MemberName; [FilledInDuringResolution] public MemberDecl Member; // will be a Field or Function [FilledInDuringResolution] public Label /*?*/ AtLabel; // non-null for a two-state selection + [FilledInDuringResolution] public bool InCompiledContext; /// /// TypeApplication_AtEnclosingClass is the list of type arguments used to instantiate the type that @@ -2265,6 +2266,8 @@ public static string OpcodeString(Opcode op) { public Expression E1; public enum AccumulationOperand { None, Left, Right } public AccumulationOperand AccumulatesForTailRecursion = AccumulationOperand.None; // set by Resolver + [FilledInDuringResolution] public bool InCompiledContext; + [ContractInvariantMethod] void ObjectInvariant() { Contract.Invariant(E0 != null); @@ -3908,7 +3911,11 @@ public static Expression MaybeTypeExpr(Expression e, Type t) { public class DatatypeUpdateExpr : ConcreteSyntaxExpression { public readonly Expression Root; public readonly List> Updates; + [FilledInDuringResolution] public List Members; [FilledInDuringResolution] public List LegalSourceConstructors; + [FilledInDuringResolution] public bool InCompiledContext; + [FilledInDuringResolution] public Expression ResolvedCompiledExpression; // see comment for Resolver.ResolveDatatypeUpdate + public DatatypeUpdateExpr(IToken tok, Expression root, List> updates) : base(tok) { Contract.Requires(tok != null); diff --git a/Source/DafnyCore/AST/MemberDecls.cs b/Source/DafnyCore/AST/MemberDecls.cs index c677da50aa9..57c83cd7eca 100644 --- a/Source/DafnyCore/AST/MemberDecls.cs +++ b/Source/DafnyCore/AST/MemberDecls.cs @@ -197,6 +197,16 @@ public override string CompileName { } } +public class DatatypeDiscriminator : SpecialField { + public override string WhatKind { + get { return "discriminator"; } + } + + public DatatypeDiscriminator(IToken tok, string name, ID specialId, object idParam, bool isGhost, Type type, Attributes attributes) + : base(tok, name, specialId, idParam, isGhost, false, false, type, attributes) { + } +} + public class DatatypeDestructor : SpecialField { public readonly List EnclosingCtors = new List(); // is always a nonempty list public readonly List CorrespondingFormals = new List(); // is always a nonempty list @@ -238,18 +248,7 @@ internal string EnclosingCtorNames(string grammaticalConjunction) { static internal string PrintableCtorNameList(List ctors, string grammaticalConjunction) { Contract.Requires(ctors != null); Contract.Requires(grammaticalConjunction != null); - var n = ctors.Count; - if (n == 1) { - return string.Format("'{0}'", ctors[0].Name); - } else if (n == 2) { - return string.Format("'{0}' {1} '{2}'", ctors[0].Name, grammaticalConjunction, ctors[1].Name); - } else { - var s = ""; - for (int i = 0; i < n - 1; i++) { - s += string.Format("'{0}', ", ctors[i].Name); - } - return s + string.Format("{0} '{1}'", grammaticalConjunction, ctors[n - 1].Name); - } + return Util.PrintableNameList(ctors.ConvertAll(ctor => ctor.Name), grammaticalConjunction); } } diff --git a/Source/DafnyCore/AST/Printer.cs b/Source/DafnyCore/AST/Printer.cs index fb6dac1ecf1..4124666d45b 100644 --- a/Source/DafnyCore/AST/Printer.cs +++ b/Source/DafnyCore/AST/Printer.cs @@ -761,7 +761,7 @@ public void PrintDatatype(DatatypeDecl dt, int indent, string fileBeingPrinted) string sep = ""; foreach (DatatypeCtor ctor in dt.Ctors) { wr.Write(sep); - PrintClassMethodHelper("", ctor.Attributes, ctor.Name, new List()); + PrintClassMethodHelper(ctor.IsGhost ? " ghost" : "", ctor.Attributes, ctor.Name, new List()); if (ctor.Formals.Count != 0) { PrintFormals(ctor.Formals, null); } diff --git a/Source/DafnyCore/AST/TopLevelDeclarations.cs b/Source/DafnyCore/AST/TopLevelDeclarations.cs index adb169630d7..244e891c4cf 100644 --- a/Source/DafnyCore/AST/TopLevelDeclarations.cs +++ b/Source/DafnyCore/AST/TopLevelDeclarations.cs @@ -1311,14 +1311,17 @@ public DatatypeDecl(IToken tok, string name, ModuleDefinition module, List ctr.Formals.Count == 0)); } } public bool IsRecordType { - get { return this is IndDatatypeDecl && Ctors.Count == 1; } + get { return this is IndDatatypeDecl && Ctors.Count == 1 && !Ctors[0].IsGhost; } } + public bool HasGhostVariant => Ctors.Any(ctor => ctor.IsGhost); + public TopLevelDecl AsTopLevelDecl => this; public TypeDeclSynonymInfo SynonymInfo { get; set; } @@ -1388,7 +1391,7 @@ public CoDatatypeDecl(IToken tok, string name, ModuleDefinition module, List ctor.IsGhost, Ctors[0]); } } @@ -1430,6 +1433,7 @@ public Type CreateType(List typeArgs) { } public class DatatypeCtor : Declaration, TypeParameter.ParentType { + public readonly bool IsGhost; public readonly List Formals; [ContractInvariantMethod] void ObjectInvariant() { @@ -1445,12 +1449,13 @@ void ObjectInvariant() { [FilledInDuringResolution] public SpecialField QueryField; [FilledInDuringResolution] public List Destructors = new List(); // includes both implicit (not mentionable in source) and explicit destructors - public DatatypeCtor(IToken tok, string name, [Captured] List formals, Attributes attributes) + public DatatypeCtor(IToken tok, string name, bool isGhost, [Captured] List formals, Attributes attributes) : base(tok, name, attributes, false) { Contract.Requires(tok != null); Contract.Requires(name != null); Contract.Requires(cce.NonNullElements(formals)); this.Formals = formals; + this.IsGhost = isGhost; } public string FullName { diff --git a/Source/DafnyCore/AST/TupleTypeDecl.cs b/Source/DafnyCore/AST/TupleTypeDecl.cs index 1b21cbf907c..77716afd4c9 100644 --- a/Source/DafnyCore/AST/TupleTypeDecl.cs +++ b/Source/DafnyCore/AST/TupleTypeDecl.cs @@ -73,7 +73,7 @@ private static List CreateConstructors(List typeArg formals.Add(f); } string ctorName = BuiltIns.TupleTypeCtorName(typeArgs.Count); - var ctor = new DatatypeCtor(Token.NoToken, ctorName, formals, null); + var ctor = new DatatypeCtor(Token.NoToken, ctorName, false, formals, null); return new List() { ctor }; } diff --git a/Source/DafnyCore/AST/Types.cs b/Source/DafnyCore/AST/Types.cs index d2a4f2e442c..a114a33f318 100644 --- a/Source/DafnyCore/AST/Types.cs +++ b/Source/DafnyCore/AST/Types.cs @@ -806,11 +806,21 @@ public OpaqueTypeDecl AsOpaqueType { return udt?.ResolvedClass as OpaqueTypeDecl; } } - public virtual bool SupportsEquality { - get { - return true; - } - } + + /// + /// Returns whether or not any values of the type can be checked for equality in compiled contexts + /// + public virtual bool SupportsEquality => true; + + /// + /// Returns whether or not some values of the type can be checked for equality in compiled contexts. + /// This differs from SupportsEquality for types where the equality operation is partial, e.g., + /// for datatypes where some, but not all, constructors are ghost. + /// Note, whereas SupportsEquality sometimes consults some constituent type for SupportEquality + /// (e.g., seq supports equality if T does), PartiallySupportsEquality does not (because the + /// semantic check would be more complicated and it currently doesn't seem worth the trouble). + /// + public virtual bool PartiallySupportsEquality => SupportsEquality; public bool MayInvolveReferences => ComputeMayInvolveReferences(null); @@ -2475,6 +2485,31 @@ public override bool SupportsEquality { } } + public override bool PartiallySupportsEquality { + get { + var totalEqualitySupport = SupportsEquality; + if (!totalEqualitySupport && ResolvedClass is TypeSynonymDeclBase synonymBase) { + return synonymBase.IsRevealedInScope(Type.GetScope()) && synonymBase.RhsWithArgument(TypeArgs).PartiallySupportsEquality; + } else if (!totalEqualitySupport && ResolvedClass is IndDatatypeDecl dt && dt.IsRevealedInScope(Type.GetScope())) { + // Equality is partially supported (at run time) for a datatype that + // * is inductive (because codatatypes never support equality), and + // * has at least one non-ghost constructor (because if all constructors are ghost, then equality is never supported), and + // * for each non-ghost constructor, every argument totally supports equality (an argument totally supports equality + // if it is non-ghost (because ghost arguments are not available at run time) and has a type that supports equality). + var hasNonGhostConstructor = false; + foreach (var ctor in dt.Ctors.Where(ctor => !ctor.IsGhost)) { + hasNonGhostConstructor = true; + if (!ctor.Formals.All(formal => !formal.IsGhost && formal.Type.SupportsEquality)) { + return false; + } + } + Contract.Assert(dt.HasGhostVariant); // sanity check (if the types of all formals support equality, then either .SupportsEquality or there is a ghost constructor) + return hasNonGhostConstructor; + } + return totalEqualitySupport; + } + } + public override bool ComputeMayInvolveReferences(ISet visitedDatatypes) { if (ResolvedClass is ArrowTypeDecl) { return TypeArgs.Any(ta => ta.ComputeMayInvolveReferences(visitedDatatypes)); diff --git a/Source/DafnyCore/Cloner.cs b/Source/DafnyCore/Cloner.cs index b0d59e9d4ca..8df0096dd6c 100644 --- a/Source/DafnyCore/Cloner.cs +++ b/Source/DafnyCore/Cloner.cs @@ -137,7 +137,7 @@ public TypeParameter.TypeParameterCharacteristics CloneTPChar(TypeParameter.Type } public DatatypeCtor CloneCtor(DatatypeCtor ct) { - return new DatatypeCtor(Tok(ct.tok), ct.Name, ct.Formals.ConvertAll(CloneFormal), CloneAttributes(ct.Attributes)); + return new DatatypeCtor(Tok(ct.tok), ct.Name, ct.IsGhost, ct.Formals.ConvertAll(CloneFormal), CloneAttributes(ct.Attributes)); } public TypeParameter CloneTypeParam(TypeParameter tp) { diff --git a/Source/DafnyCore/Compilers/Compiler-Csharp.cs b/Source/DafnyCore/Compilers/Compiler-Csharp.cs index eb97556d43e..0fde115edbf 100644 --- a/Source/DafnyCore/Compilers/Compiler-Csharp.cs +++ b/Source/DafnyCore/Compilers/Compiler-Csharp.cs @@ -517,15 +517,19 @@ IClassWriter CompileDatatypeBase(DatatypeDecl dt, ConcreteSyntaxTree wr) { } var groundingCtor = dt.GetGroundingCtor(); - if (dt is CoDatatypeDecl) { - var wCo = wDefault; - wDefault = new ConcreteSyntaxTree(); - wCo.Format($"new {dt.CompileName}__Lazy{DtT_TypeArgs}(() => {{ return {wDefault}; }})"); - } + if (groundingCtor.IsGhost) { + wDefault.Write(ForcePlaceboValue(UserDefinedType.FromTopLevelDecl(dt.tok, dt), wDefault, dt.tok)); + } else { + if (dt is CoDatatypeDecl) { + var wCo = wDefault; + wDefault = new ConcreteSyntaxTree(); + wCo.Format($"new {dt.CompileName}__Lazy{DtT_TypeArgs}(() => {{ return {wDefault}; }})"); + } - wDefault.Write(DtCreateName(groundingCtor)); - var nonGhostFormals = groundingCtor.Formals.Where(f => !f.IsGhost); - wDefault.Write($"({nonGhostFormals.Comma(f => DefaultValue(f.Type, wDefault, f.tok))})"); + wDefault.Write(DtCreateName(groundingCtor)); + var nonGhostFormals = groundingCtor.Formals.Where(f => !f.IsGhost); + wDefault.Write($"({nonGhostFormals.Comma(f => DefaultValue(f.Type, wDefault, f.tok))})"); + } EmitTypeDescriptorMethod(dt, wr); @@ -535,7 +539,7 @@ IClassWriter CompileDatatypeBase(DatatypeDecl dt, ConcreteSyntaxTree wr) { } // create methods - foreach (var ctor in dt.Ctors) { + foreach (var ctor in dt.Ctors.Where(ctor => !ctor.IsGhost)) { wr.Write($"public static {DtTypeName(dt)} {DtCreateName(ctor)}("); WriteFormals("", ctor.Formals, wr); var w = wr.NewBlock(")"); @@ -547,7 +551,7 @@ IClassWriter CompileDatatypeBase(DatatypeDecl dt, ConcreteSyntaxTree wr) { if (dt is TupleTypeDecl) { // omit the is_ property for tuples, since it cannot be used syntactically in the language } else { - foreach (var ctor in dt.Ctors) { + foreach (var ctor in dt.Ctors.Where(ctor => !ctor.IsGhost)) { interfaceTree.WriteLine($"bool is_{ctor.CompileName} {{ get; }}"); var returnValue = dt.IsRecordType @@ -566,7 +570,10 @@ IClassWriter CompileDatatypeBase(DatatypeDecl dt, ConcreteSyntaxTree wr) { var wGet = w.NewBlock("get"); foreach (var ctor in dt.Ctors) { Contract.Assert(ctor.Formals.Count == 0); - wGet.WriteLine($"yield return {DtT_protected}.{DtCreateName(ctor)}();"); + var constructor = ctor.IsGhost + ? ForcePlaceboValue(UserDefinedType.FromTopLevelDecl(dt.tok, dt), wGet, dt.tok) + : $"{DtT_protected}.{DtCreateName(ctor)}()"; + wGet.WriteLine($"yield return {constructor};"); } } @@ -697,8 +704,9 @@ private void CompileDatatypeDestructorsAndAddToInterface(DatatypeDecl dt, Concre ConcreteSyntaxTree interfaceTree, string DtT_TypeArgs) { foreach (var ctor in dt.Ctors) { var index = 0; - foreach (var dtor in ctor.Destructors) { - if (dtor.EnclosingCtors[0] == ctor) { + foreach (var dtor in ctor.Destructors.Where(dtor => dtor.EnclosingCtors[0] == ctor)) { + var compiledConstructorCount = dtor.EnclosingCtors.Count(constructor => !constructor.IsGhost); + if (compiledConstructorCount != 0) { var arg = dtor.CorrespondingFormals[0]; if (!arg.IsGhost) { var DtorM = arg.HasName ? "_" + arg.CompileName : FieldName(arg, index); @@ -730,18 +738,23 @@ private void CompileDatatypeDestructorsAndAddToInterface(DatatypeDecl dt, Concre wGet.WriteLine("var d = this;"); } - var n = dtor.EnclosingCtors.Count; - for (int i = 0; i < n - 1; i++) { + var compiledConstructorsProcessed = 0; + for (var i = 0; i < dtor.EnclosingCtors.Count; i++) { var ctor_i = dtor.EnclosingCtors[i]; Contract.Assert(arg.CompileName == dtor.CorrespondingFormals[i].CompileName); + if (ctor_i.IsGhost) { + continue; + } var type = $"{dt.CompileName}_{ctor_i.CompileName}{DtT_TypeArgs}"; // TODO use pattern matching to replace cast. - wGet.WriteLine($"if (d is {type}) {{ return (({type})d).{IdProtect(DtorM)}; }}"); + var returnTheValue = $"return (({type})d).{IdProtect(DtorM)};"; + if (compiledConstructorsProcessed < compiledConstructorCount - 1) { + wGet.WriteLine($"if (d is {type}) {{ {returnTheValue} }}"); + } else { + wGet.WriteLine(returnTheValue); + } + compiledConstructorsProcessed++; } - - Contract.Assert(arg.CompileName == dtor.CorrespondingFormals[n - 1].CompileName); - wGet.WriteLine( - $"return (({dt.CompileName}_{dtor.EnclosingCtors[n - 1].CompileName}{DtT_TypeArgs})d).{IdProtect(DtorM)};"); } index++; } @@ -835,7 +848,7 @@ private void CompileDatatypeConstructors(DatatypeDecl dt, ConcreteSyntaxTree wrx } int constructorIndex = 0; // used to give each constructor a different name - foreach (DatatypeCtor ctor in dt.Ctors) { + foreach (var ctor in dt.Ctors.Where(ctor => !ctor.IsGhost)) { var wr = wrx.NewNamedBlock( $"public class {DtCtorDeclarationName(ctor)}{TypeParameters(nonGhostTypeArgs)} : {IdName(dt)}{typeParams}"); DatatypeFieldsAndConstructor(ctor, constructorIndex, wr); @@ -1029,6 +1042,7 @@ string DtCtorName(DatatypeCtor ctor) { } string DtCreateName(DatatypeCtor ctor) { + Contract.Assert(!ctor.IsGhost); // there should never be an occasion to ask for a ghost constructor if (ctor.EnclosingDatatype.IsRecordType) { return "create"; } else { @@ -1551,7 +1565,8 @@ protected override string TypeInitializationValue(Type type, ConcreteSyntaxTree } } - protected override string TypeName_UDT(string fullCompileName, List variance, List typeArgs, ConcreteSyntaxTree wr, IToken tok) { + protected override string TypeName_UDT(string fullCompileName, List variance, List typeArgs, + ConcreteSyntaxTree wr, IToken tok, bool omitTypeArguments = false) { Contract.Assume(fullCompileName != null); // precondition; this ought to be declared as a Requires in the superclass Contract.Assume(variance != null); // precondition; this ought to be declared as a Requires in the superclass Contract.Assume(typeArgs != null); // precondition; this ought to be declared as a Requires in the superclass @@ -2316,7 +2331,7 @@ private string FullTypeName(UserDefinedType udt, MemberDecl/*?*/ member = null, protected override void EmitThis(ConcreteSyntaxTree wr) { var custom = - (enclosingMethod != null && enclosingMethod.IsTailRecursive) || + (enclosingMethod != null && (enclosingMethod.IsTailRecursive || NeedsCustomReceiver(enclosingMethod))) || (enclosingFunction != null && (enclosingFunction.IsTailRecursive || NeedsCustomReceiver(enclosingFunction))) || thisContext is NewtypeDecl || thisContext is TraitDecl; diff --git a/Source/DafnyCore/Compilers/Compiler-cpp.cs b/Source/DafnyCore/Compilers/Compiler-cpp.cs index 1a9d6f897c1..908627e58a0 100644 --- a/Source/DafnyCore/Compilers/Compiler-cpp.cs +++ b/Source/DafnyCore/Compilers/Compiler-cpp.cs @@ -327,7 +327,7 @@ protected override IClassWriter DeclareDatatype(DatatypeDecl dt, ConcreteSyntaxT } // Optimize a not-uncommon case - if (dt.Ctors.Count == 1) { + if (dt.IsRecordType) { var ctor = dt.Ctors[0]; var ws = wdecl.NewBlock(String.Format("{0}\nstruct {1}", DeclareTemplate(dt.TypeArgs), DtT_protected), ";"); @@ -393,7 +393,7 @@ protected override IClassWriter DeclareDatatype(DatatypeDecl dt, ConcreteSyntaxT } else { /*** Create one struct for each constructor ***/ - foreach (var ctor in dt.Ctors) { + foreach (var ctor in dt.Ctors.Where(ctor => !ctor.IsGhost)) { string structName = DatatypeSubStructName(ctor); var wstruct = wdecl.NewBlock(String.Format("{0}\nstruct {1}", DeclareTemplate(dt.TypeArgs), structName), ";"); // Declare the struct members @@ -1111,7 +1111,8 @@ private string ActualTypeArgs(List typeArgs) { ? String.Format(" <{0}> ", Util.Comma(typeArgs, tp => TypeName(tp, null, null))) : ""; } - protected override string TypeName_UDT(string fullCompileName, List variance, List typeArgs, ConcreteSyntaxTree wr, IToken tok) { + protected override string TypeName_UDT(string fullCompileName, List variance, List typeArgs, + ConcreteSyntaxTree wr, IToken tok, bool omitTypeArguments) { Contract.Assume(fullCompileName != null); // precondition; this ought to be declared as a Requires in the superclass Contract.Assume(typeArgs != null); // precondition; this ought to be declared as a Requires in the superclass string s = IdProtect(fullCompileName); diff --git a/Source/DafnyCore/Compilers/Compiler-go.cs b/Source/DafnyCore/Compilers/Compiler-go.cs index 329f51f6cd2..829add4e7ad 100644 --- a/Source/DafnyCore/Compilers/Compiler-go.cs +++ b/Source/DafnyCore/Compilers/Compiler-go.cs @@ -683,7 +683,7 @@ protected override ConcreteSyntaxTree CreateIterator(IteratorDecl iter, Concrete var staticFieldWriter = wr.NewNamedBlock("type {0} struct", companionTypeName); var staticFieldInitWriter = wr.NewNamedBlock("var {0} = {1}", FormatCompanionName(name), companionTypeName); - foreach (var ctor in dt.Ctors) { + foreach (var ctor in dt.Ctors.Where(ctor => !ctor.IsGhost)) { var ctorStructName = name + "_" + ctor.CompileName; wr.WriteLine(); var wStruct = wr.NewNamedBlock("type {0} struct", ctorStructName); @@ -738,9 +738,13 @@ protected override ConcreteSyntaxTree CreateIterator(IteratorDecl iter, Concrete var wDefault = wr.NewBlock($") {name}"); wDefault.Write("return "); var groundingCtor = dt.GetGroundingCtor(); - var nonGhostFormals = groundingCtor.Formals.Where(f => !f.IsGhost).ToList(); - var arguments = Util.Comma(nonGhostFormals, f => DefaultValue(f.Type, wDefault, f.tok)); - EmitDatatypeValue(dt, groundingCtor, dt is CoDatatypeDecl, arguments, wDefault); + if (groundingCtor.IsGhost) { + wDefault.Write(ForcePlaceboValue(UserDefinedType.FromTopLevelDecl(dt.tok, dt), wDefault, dt.tok)); + } else { + var nonGhostFormals = groundingCtor.Formals.Where(f => !f.IsGhost).ToList(); + var arguments = Util.Comma(nonGhostFormals, f => DefaultValue(f.Type, wDefault, f.tok)); + EmitDatatypeValue(dt, groundingCtor, dt is CoDatatypeDecl, arguments, wDefault); + } wDefault.WriteLine(); } @@ -752,7 +756,7 @@ protected override ConcreteSyntaxTree CreateIterator(IteratorDecl iter, Concrete wSingles.WriteLine("i++"); wSingles = wSingles.NewNamedBlock("switch i"); var i = 0; - foreach (var ctor in dt.Ctors) { + foreach (var ctor in dt.Ctors.Where(ctor => !ctor.IsGhost)) { wSingles.WriteLine("case {0}: return {1}.{2}(), true", i, FormatCompanionName(name), FormatDatatypeConstructorName(ctor.CompileName)); i++; } @@ -761,8 +765,9 @@ protected override ConcreteSyntaxTree CreateIterator(IteratorDecl iter, Concrete // destructors foreach (var ctor in dt.Ctors) { - foreach (var dtor in ctor.Destructors) { - if (dtor.EnclosingCtors[0] == ctor) { + foreach (var dtor in ctor.Destructors.Where(dtor => dtor.EnclosingCtors[0] == ctor)) { + var compiledConstructorCount = dtor.EnclosingCtors.Count(constructor => !constructor.IsGhost); + if (compiledConstructorCount != 0) { var arg = dtor.CorrespondingFormals[0]; if (!arg.IsGhost && arg.HasName) { wr.WriteLine(); @@ -772,13 +777,20 @@ protected override ConcreteSyntaxTree CreateIterator(IteratorDecl iter, Concrete wDtor.WriteLine("return _this.Get().({0}).{1}", structOfCtor(dtor.EnclosingCtors[0]), DatatypeFieldName(arg)); } else { wDtor = wDtor.NewBlock("switch data := _this.Get().(type)"); - for (int i = 0; i < n - 1; i++) { + var compiledConstructorsProcessed = 0; + for (var i = 0; i < n; i++) { var ctor_i = dtor.EnclosingCtors[i]; Contract.Assert(arg.CompileName == dtor.CorrespondingFormals[i].CompileName); - wDtor.WriteLine("case {0}: return data.{1}", structOfCtor(ctor_i), DatatypeFieldName(arg)); + if (ctor_i.IsGhost) { + continue; + } + if (compiledConstructorsProcessed < compiledConstructorCount - 1) { + wDtor.WriteLine("case {0}: return data.{1}", structOfCtor(ctor_i), DatatypeFieldName(arg)); + } else { + wDtor.WriteLine("default: return data.({0}).{1}", structOfCtor(ctor_i), DatatypeFieldName(arg)); + } + compiledConstructorsProcessed++; } - Contract.Assert(arg.CompileName == dtor.CorrespondingFormals[n - 1].CompileName); - wDtor.WriteLine("default: return data.({0}).{1}", structOfCtor(dtor.EnclosingCtors[n - 1]), DatatypeFieldName(arg)); } } } @@ -790,10 +802,10 @@ protected override ConcreteSyntaxTree CreateIterator(IteratorDecl iter, Concrete wr.WriteLine(); var w = wr.NewNamedBlock("func (_this {0}) String() string", name); // TODO Avoid switch if only one branch - var needData = dt is IndDatatypeDecl && dt.Ctors.Exists(ctor => ctor.Formals.Exists(arg => !arg.IsGhost)); + var needData = dt is IndDatatypeDecl && dt.Ctors.Exists(ctor => !ctor.IsGhost && ctor.Formals.Exists(arg => !arg.IsGhost)); w = w.NewNamedBlock("switch {0}_this.Get().(type)", needData ? "data := " : ""); w.WriteLine("case nil: return \"null\""); - foreach (var ctor in dt.Ctors) { + foreach (var ctor in dt.Ctors.Where(ctor => !ctor.IsGhost)) { var wCase = w.NewNamedBlock("case {0}:", structOfCtor(ctor)); var nm = (dt.EnclosingModuleDefinition.IsDefaultModule ? "" : dt.EnclosingModuleDefinition.Name + ".") + dt.Name + "." + ctor.Name; if (dt is CoDatatypeDecl) { @@ -830,10 +842,10 @@ protected override ConcreteSyntaxTree CreateIterator(IteratorDecl iter, Concrete wr.WriteLine(); var wEquals = wr.NewNamedBlock("func (_this {0}) Equals(other {0}) bool", name); // TODO: Way to implement shortcut check for address equality? - var needData1 = dt.Ctors.Exists(ctor => ctor.Formals.Exists(arg => !arg.IsGhost)); + var needData1 = dt.Ctors.Exists(ctor => !ctor.IsGhost && ctor.Formals.Exists(arg => !arg.IsGhost)); wEquals = wEquals.NewNamedBlock("switch {0}_this.Get().(type)", needData1 ? "data1 := " : ""); - foreach (var ctor in dt.Ctors) { + foreach (var ctor in dt.Ctors.Where(ctor => !ctor.IsGhost)) { var wCase = wEquals.NewNamedBlock("case {0}:", structOfCtor(ctor)); var needData2 = ctor.Formals.Exists(arg => !arg.IsGhost); @@ -1107,7 +1119,7 @@ private ConcreteSyntaxTree CreateSubroutine(string name, List variance, List typeArgs, ConcreteSyntaxTree wr, IToken tok) { + protected override string TypeName_UDT(string fullCompileName, List variance, List typeArgs, + ConcreteSyntaxTree wr, IToken tok, bool omitTypeArguments) { Contract.Assume(fullCompileName != null); // precondition; this ought to be declared as a Requires in the superclass Contract.Assume(typeArgs != null); // precondition; this ought to be declared as a Requires in the superclass string s = "*" + IdProtect(fullCompileName); diff --git a/Source/DafnyCore/Compilers/Compiler-java.cs b/Source/DafnyCore/Compilers/Compiler-java.cs index c15db60cfd4..9e9de5eec5c 100644 --- a/Source/DafnyCore/Compilers/Compiler-java.cs +++ b/Source/DafnyCore/Compilers/Compiler-java.cs @@ -711,9 +711,9 @@ private string TypeName(Type type, ConcreteSyntaxTree wr, IToken tok, bool boxed // When accessing a static member, leave off the type arguments if (member != null) { - return TypeName_UDT(s, new List(), new List(), wr, udt.tok); + return TypeName_UDT(s, new List(), new List(), wr, udt.tok, erased); } else { - return TypeName_UDT(s, udt, wr, udt.tok); + return TypeName_UDT(s, udt, wr, udt.tok, erased); } } else if (xType is SetType) { var argType = ((SetType)xType).Arg; @@ -820,13 +820,14 @@ protected override bool DeclareFormal(string prefix, string name, Type type, ITo return true; } - protected override string TypeName_UDT(string fullCompileName, List variance, List typeArgs, ConcreteSyntaxTree wr, IToken tok) { + protected override string TypeName_UDT(string fullCompileName, List variance, List typeArgs, + ConcreteSyntaxTree wr, IToken tok, bool omitTypeArguments) { Contract.Assume(fullCompileName != null); // precondition; this ought to be declared as a Requires in the superclass Contract.Assume(variance != null); // precondition; this ought to be declared as a Requires in the superclass Contract.Assume(typeArgs != null); // precondition; this ought to be declared as a Requires in the superclass Contract.Assume(variance.Count == typeArgs.Count); string s = IdProtect(fullCompileName); - if (typeArgs.Count != 0) { + if (typeArgs.Count != 0 && !omitTypeArguments) { for (var i = 0; i < typeArgs.Count; i++) { var v = variance[i]; var ta = typeArgs[i]; @@ -1137,8 +1138,8 @@ private bool IsJavaPrimitiveType(Type type) { protected override void EmitThis(ConcreteSyntaxTree wr) { var custom = - (enclosingMethod != null && enclosingMethod.IsTailRecursive) || - (enclosingFunction != null && enclosingFunction.IsTailRecursive) || + (enclosingMethod != null && (enclosingMethod.IsTailRecursive || NeedsCustomReceiver(enclosingMethod))) || + (enclosingFunction != null && (enclosingFunction.IsTailRecursive || NeedsCustomReceiver(enclosingFunction))) || thisContext is NewtypeDecl || thisContext is TraitDecl; wr.Write(custom ? "_this" : "this"); @@ -1377,7 +1378,7 @@ protected override string TypeName_Companion(Type type, ConcreteSyntaxTree wr, I if (member != null && (member.IsStatic || NeedsCustomReceiver(member)) && member.EnclosingClass.TypeArgs.Count != 0) { return IdProtect(udt.FullCompanionCompileName); } else { - return TypeName_UDT(udt.FullCompanionCompileName, udt, wr, tok); + return TypeName_UDT(udt.FullCompanionCompileName, udt, wr, tok, false); } } else { return TypeName(type, wr, tok, member); @@ -1772,16 +1773,20 @@ IClassWriter CompileDatatypeBase(DatatypeDecl dt, ConcreteSyntaxTree wr) { w.WriteLine(";"); } var groundingCtor = dt.GetGroundingCtor(); - var nonGhostFormals = groundingCtor.Formals.Where(f => !f.IsGhost).ToList(); - var arguments = nonGhostFormals.Comma(f => DefaultValue(f.Type, wDefault, f.tok)); - EmitDatatypeValue(dt, groundingCtor, null, dt is CoDatatypeDecl, arguments, wDefault); + if (groundingCtor.IsGhost) { + wDefault.Write(ForcePlaceboValue(UserDefinedType.FromTopLevelDecl(dt.tok, dt), wDefault, dt.tok)); + } else { + var nonGhostFormals = groundingCtor.Formals.Where(f => !f.IsGhost).ToList(); + var args = nonGhostFormals.Comma(f => DefaultValue(f.Type, wDefault, f.tok)); + EmitDatatypeValue(dt, groundingCtor, null, dt is CoDatatypeDecl, args, wDefault); + } var targetTypeName = BoxedTypeName(UserDefinedType.FromTopLevelDecl(dt.tok, dt, null), wr, dt.tok); - arguments = usedTypeArgs.Comma(tp => DefaultValue(new UserDefinedType(tp), wDefault, dt.tok, true)); + var arguments = usedTypeArgs.Comma(tp => DefaultValue(new UserDefinedType(tp), wDefault, dt.tok, true)); EmitTypeMethod(dt, IdName(dt), dt.TypeArgs, usedTypeArgs, targetTypeName, $"Default({arguments})", wr); // create methods - foreach (var ctor in dt.Ctors) { + foreach (var ctor in dt.Ctors.Where(ctor => !ctor.IsGhost)) { wr.Write("public static{0} {1} {2}(", justTypeArgs, DtT_protected, DtCreateName(ctor)); WriteFormals("", ctor.Formals, wr); var w = wr.NewBlock(")"); @@ -1799,7 +1804,7 @@ IClassWriter CompileDatatypeBase(DatatypeDecl dt, ConcreteSyntaxTree wr) { } // query properties - foreach (var ctor in dt.Ctors) { + foreach (var ctor in dt.Ctors.Where(ctor => !ctor.IsGhost)) { if (dt.IsRecordType) { wr.WriteLine($"public boolean is_{ctor.CompileName}() {{ return true; }}"); } else { @@ -1816,14 +1821,19 @@ IClassWriter CompileDatatypeBase(DatatypeDecl dt, ConcreteSyntaxTree wr) { w.WriteLine($"java.util.ArrayList<{DtT_protected}> {arraylist} = new java.util.ArrayList<>();"); foreach (var ctor in dt.Ctors) { Contract.Assert(ctor.Formals.Count == 0); - w.WriteLine("{0}.add(new {1}{2}());", arraylist, DtT_protected, dt.IsRecordType ? "" : $"_{ctor.CompileName}"); + if (ctor.IsGhost) { + w.WriteLine("{0}.add({1});", arraylist, ForcePlaceboValue(UserDefinedType.FromTopLevelDecl(dt.tok, dt), w, dt.tok)); + } else { + w.WriteLine("{0}.add(new {1}{2}());", arraylist, DtT_protected, dt.IsRecordType ? "" : $"_{ctor.CompileName}"); + } } w.WriteLine($"return {arraylist};"); } // destructors foreach (var ctor in dt.Ctors) { - foreach (var dtor in ctor.Destructors) { - if (dtor.EnclosingCtors[0] == ctor) { + foreach (var dtor in ctor.Destructors.Where(dtor => dtor.EnclosingCtors[0] == ctor)) { + var compiledConstructorCount = dtor.EnclosingCtors.Count(constructor => !constructor.IsGhost); + if (compiledConstructorCount != 0) { var arg = dtor.CorrespondingFormals[0]; if (!arg.IsGhost && arg.HasName) { var wDtor = wr.NewNamedBlock($"public {TypeName(arg.Type, wr, arg.tok)} dtor_{arg.CompileName}()"); @@ -1831,17 +1841,21 @@ IClassWriter CompileDatatypeBase(DatatypeDecl dt, ConcreteSyntaxTree wr) { wDtor.WriteLine($"return this.{FieldName(arg, 0)};"); } else { wDtor.WriteLine("{0} d = this{1};", DtT_protected, dt is CoDatatypeDecl ? ".Get()" : ""); - var n = dtor.EnclosingCtors.Count; - for (int i = 0; i < n - 1; i++) { + var compiledConstructorsProcessed = 0; + for (var i = 0; i < dtor.EnclosingCtors.Count; i++) { var ctor_i = dtor.EnclosingCtors[i]; Contract.Assert(arg.CompileName == dtor.CorrespondingFormals[i].CompileName); - wDtor.WriteLine("if (d instanceof {0}_{1}) {{ return (({0}_{1}{2})d).{3}; }}", dt.CompileName, - ctor_i.CompileName, DtT_TypeArgs, FieldName(arg, i)); + if (ctor_i.IsGhost) { + continue; + } + if (compiledConstructorsProcessed < compiledConstructorCount - 1) { + wDtor.WriteLine("if (d instanceof {0}_{1}) {{ return (({0}_{1}{2})d).{3}; }}", dt.CompileName, + ctor_i.CompileName, DtT_TypeArgs, FieldName(arg, i)); + } else { + wDtor.WriteLine($"return (({dt.CompileName}_{ctor_i.CompileName}{DtT_TypeArgs})d).{FieldName(arg, 0)};"); + } + compiledConstructorsProcessed++; } - - Contract.Assert(arg.CompileName == dtor.CorrespondingFormals[n - 1].CompileName); - wDtor.WriteLine( - $"return (({dt.CompileName}_{dtor.EnclosingCtors[n - 1].CompileName}{DtT_TypeArgs})d).{FieldName(arg, 0)};"); } } } @@ -1862,7 +1876,7 @@ void CompileDatatypeConstructors(DatatypeDecl dt, ConcreteSyntaxTree wrx) { return; } int constructorIndex = 0; // used to give each constructor a different name - foreach (DatatypeCtor ctor in dt.Ctors) { + foreach (DatatypeCtor ctor in dt.Ctors.Where(ctor => !ctor.IsGhost)) { var filename = $"{ModulePath}/{DtCtorDeclarationName(ctor)}.java"; var wr = wrx.NewFile(filename); FileCount += 1; @@ -2054,6 +2068,7 @@ string DtCtorName(DatatypeCtor ctor) { return dt.IsRecordType ? dtName : dtName + "_" + ctor.CompileName; } string DtCreateName(DatatypeCtor ctor) { + Contract.Assert(!ctor.IsGhost); // there should never be an occasion to ask for a ghost constructor if (ctor.EnclosingDatatype.IsRecordType) { return "create"; } @@ -3117,7 +3132,7 @@ protected override string TypeInitializationValue(Type type, ConcreteSyntaxTree bareArray = $"(Object{Repeat("[]", arrayClass.Dims - 1)}) {TypeDescriptor(elType, wr, tok)}.newArray({Util.Comma(Enumerable.Repeat("0", arrayClass.Dims))})"; } else { - bareArray = $"new {TypeName(elType, wr, tok)}{Repeat("[0]", arrayClass.Dims)}"; + bareArray = $"new {TypeName(elType, wr, tok, false, true)}{Repeat("[0]", arrayClass.Dims)}"; } if (arrayClass.Dims > 1) { arrays.Add(arrayClass.Dims); diff --git a/Source/DafnyCore/Compilers/Compiler-js.cs b/Source/DafnyCore/Compilers/Compiler-js.cs index 58aa10c8021..6e61e88e254 100644 --- a/Source/DafnyCore/Compilers/Compiler-js.cs +++ b/Source/DafnyCore/Compilers/Compiler-js.cs @@ -333,9 +333,9 @@ protected override ConcreteSyntaxTree CreateIterator(IteratorDecl iter, Concrete w0.WriteLine("return this._d"); } - // query properties + // create methods var i = 0; - foreach (var ctor in dt.Ctors) { + foreach (var ctor in dt.Ctors.Where(ctor => !ctor.IsGhost)) { // collect the names of non-ghost arguments var argNames = new List(); var k = 0; @@ -378,7 +378,7 @@ protected override ConcreteSyntaxTree CreateIterator(IteratorDecl iter, Concrete // query properties i = 0; - foreach (var ctor in dt.Ctors) { + foreach (var ctor in dt.Ctors.Where(ctor => !ctor.IsGhost)) { // get is_Ctor0() { return _D is Dt_Ctor0; } wr.WriteLine("get is_{0}() {{ return this.$tag === {1}; }}", ctor.CompileName, i); i++; @@ -394,15 +394,20 @@ protected override ConcreteSyntaxTree CreateIterator(IteratorDecl iter, Concrete var w = wr.NewNamedBlock("static *AllSingletonConstructors_()"); foreach (var ctor in dt.Ctors) { Contract.Assert(ctor.Formals.Count == 0); - w.WriteLine("yield {0}.create_{1}({2});", DtT_protected, ctor.CompileName, dt is CoDatatypeDecl ? "null" : ""); + if (ctor.IsGhost) { + w.WriteLine("yield {0};", ForcePlaceboValue(UserDefinedType.FromTopLevelDecl(dt.tok, dt), w, dt.tok)); + } else { + w.WriteLine("yield {0}.create_{1}({2});", DtT_protected, ctor.CompileName, dt is CoDatatypeDecl ? "null" : ""); + } } } } // destructors foreach (var ctor in dt.Ctors) { - foreach (var dtor in ctor.Destructors) { - if (dtor.EnclosingCtors[0] == ctor) { + foreach (var dtor in ctor.Destructors.Where(dtor => dtor.EnclosingCtors[0] == ctor)) { + var compiledConstructorCount = dtor.EnclosingCtors.Count(constructor => !constructor.IsGhost); + if (compiledConstructorCount != 0) { var arg = dtor.CorrespondingFormals[0]; if (!arg.IsGhost && arg.HasName) { // datatype: get dtor_Dtor0() { return this.Dtor0; } @@ -499,9 +504,13 @@ protected override ConcreteSyntaxTree CreateIterator(IteratorDecl iter, Concrete var wDefault = wr.NewBlock(")"); wDefault.Write("return "); var groundingCtor = dt.GetGroundingCtor(); - var nonGhostFormals = groundingCtor.Formals.Where(f => !f.IsGhost).ToList(); - var arguments = Util.Comma(nonGhostFormals, f => DefaultValue(f.Type, wDefault, f.tok)); - EmitDatatypeValue(dt, groundingCtor, dt is CoDatatypeDecl, arguments, wDefault); + if (groundingCtor.IsGhost) { + wDefault.Write(ForcePlaceboValue(UserDefinedType.FromTopLevelDecl(dt.tok, dt), wDefault, dt.tok)); + } else { + var nonGhostFormals = groundingCtor.Formals.Where(f => !f.IsGhost).ToList(); + var arguments = Util.Comma(nonGhostFormals, f => DefaultValue(f.Type, wDefault, f.tok)); + EmitDatatypeValue(dt, groundingCtor, dt is CoDatatypeDecl, arguments, wDefault); + } wDefault.WriteLine(";"); } @@ -884,12 +893,12 @@ internal override string TypeName(Type type, ConcreteSyntaxTree wr, IToken tok, } protected override string TypeInitializationValue(Type type, ConcreteSyntaxTree wr, IToken tok, bool usePlaceboValue, bool constructTypeParameterDefaultsFromTypeDescriptors) { - var xType = type.NormalizeExpandKeepConstraints(); - if (usePlaceboValue) { return "undefined"; } + var xType = type.NormalizeExpandKeepConstraints(); + if (xType is BoolType) { return "false"; } else if (xType is CharType) { @@ -982,7 +991,8 @@ protected override string TypeInitializationValue(Type type, ConcreteSyntaxTree } - protected override string TypeName_UDT(string fullCompileName, List variance, List typeArgs, ConcreteSyntaxTree wr, IToken tok) { + protected override string TypeName_UDT(string fullCompileName, List variance, List typeArgs, + ConcreteSyntaxTree wr, IToken tok, bool omitTypeArguments) { Contract.Assume(fullCompileName != null); // precondition; this ought to be declared as a Requires in the superclass Contract.Assume(typeArgs != null); // precondition; this ought to be declared as a Requires in the superclass string s = IdProtect(fullCompileName); diff --git a/Source/DafnyCore/Compilers/Compiler-python.cs b/Source/DafnyCore/Compilers/Compiler-python.cs index 53a1636751b..71595c9df25 100644 --- a/Source/DafnyCore/Compilers/Compiler-python.cs +++ b/Source/DafnyCore/Compilers/Compiler-python.cs @@ -255,17 +255,26 @@ protected override IClassWriter DeclareDatatype(DatatypeDecl dt, ConcreteSyntaxT btw.WriteLine($"@{DafnyRuntimeModule}.classproperty"); var w = btw.NewBlockPy( $"def AllSingletonConstructors(cls):"); - w.WriteLine($"return [{dt.Ctors.Select(ctor => $"{DtCtorDeclarationName(ctor, false)}()").Comma()}]"); + var values = dt.Ctors.Select(ctor => + ctor.IsGhost + ? ForcePlaceboValue(UserDefinedType.FromTopLevelDecl(dt.tok, dt), w, dt.tok) + : $"{DtCtorDeclarationName(ctor, false)}()"); + w.WriteLine($"return [{values.Comma()}]"); } btw.WriteLine($"@classmethod"); var wDefault = btw.NewBlockPy($"def default(cls, {UsedTypeParameters(dt).Comma(FormatDefaultTypeParameterValue)}):"); - var arguments = dt.GetGroundingCtor().Formals.Where(f => !f.IsGhost).Comma(f => DefaultValue(f.Type, wDefault, f.tok)); - var constructorCall = $"{DtCtorDeclarationName(dt.GetGroundingCtor(), false)}({arguments})"; - if (dt is CoDatatypeDecl) { - constructorCall = $"{dt.CompileName}__Lazy(lambda: {constructorCall})"; + var groundingCtor = dt.GetGroundingCtor(); + if (groundingCtor.IsGhost) { + wDefault.WriteLine($"return {ForcePlaceboValue(UserDefinedType.FromTopLevelDecl(dt.tok, dt), wDefault, dt.tok)}"); + } else { + var arguments = groundingCtor.Formals.Where(f => !f.IsGhost).Comma(f => DefaultValue(f.Type, wDefault, f.tok)); + var constructorCall = $"{DtCtorDeclarationName(groundingCtor, false)}({arguments})"; + if (dt is CoDatatypeDecl) { + constructorCall = $"{dt.CompileName}__Lazy(lambda: {constructorCall})"; + } + wDefault.WriteLine($"return lambda: {constructorCall}"); } - wDefault.WriteLine($"return lambda: {constructorCall}"); // Ensures the inequality is based on equality defined in the constructor btw.NewBlockPy("def __ne__(self, __o: object) -> bool:") @@ -296,7 +305,7 @@ select IdProtect(arg.CompileName)) { } } - foreach (var ctor in dt.Ctors) { + foreach (var ctor in dt.Ctors.Where(ctor => !ctor.IsGhost)) { var ctorName = IdProtect(ctor.CompileName); // Class-level fields don't work in all python version due to metaclasses. @@ -645,9 +654,14 @@ private string TypeName(Type type, ConcreteSyntaxTree wr, IToken tok, bool boxed protected override string TypeInitializationValue(Type type, ConcreteSyntaxTree wr, IToken tok, bool usePlaceboValue, bool constructTypeParameterDefaultsFromTypeDescriptors) { + + if (usePlaceboValue) { + return "None"; + } + var xType = type.NormalizeExpandKeepConstraints(); - if (usePlaceboValue || xType.IsObjectQ) { + if (xType.IsObjectQ) { return "None"; } @@ -721,7 +735,7 @@ protected override string TypeInitializationValue(Type type, ConcreteSyntaxTree } protected override string TypeName_UDT(string fullCompileName, List variance, - List typeArgs, ConcreteSyntaxTree wr, IToken tok) { + List typeArgs, ConcreteSyntaxTree wr, IToken tok, bool omitTypeArguments) { return fullCompileName; } diff --git a/Source/DafnyCore/Compilers/SinglePassCompiler.cs b/Source/DafnyCore/Compilers/SinglePassCompiler.cs index 6b2f9160b67..da073acbaba 100644 --- a/Source/DafnyCore/Compilers/SinglePassCompiler.cs +++ b/Source/DafnyCore/Compilers/SinglePassCompiler.cs @@ -269,7 +269,7 @@ protected virtual string TypeArgumentName(Type type, ConcreteSyntaxTree wr, ITok /// protected abstract string TypeInitializationValue(Type type, ConcreteSyntaxTree wr, IToken tok, bool usePlaceboValue, bool constructTypeParameterDefaultsFromTypeDescriptors); - protected string TypeName_UDT(string fullCompileName, UserDefinedType udt, ConcreteSyntaxTree wr, IToken tok) { + protected string TypeName_UDT(string fullCompileName, UserDefinedType udt, ConcreteSyntaxTree wr, IToken tok, bool omitTypeArguments = false) { Contract.Requires(fullCompileName != null); Contract.Requires(udt != null); Contract.Requires(wr != null); @@ -278,9 +278,10 @@ protected string TypeName_UDT(string fullCompileName, UserDefinedType udt, Concr var cl = udt.ResolvedClass; var typeParams = SelectNonGhost(cl, cl.TypeArgs); var typeArgs = SelectNonGhost(cl, udt.TypeArgs); - return TypeName_UDT(fullCompileName, typeParams.ConvertAll(tp => tp.Variance), typeArgs, wr, tok); + return TypeName_UDT(fullCompileName, typeParams.ConvertAll(tp => tp.Variance), typeArgs, wr, tok, omitTypeArguments); } - protected abstract string TypeName_UDT(string fullCompileName, List variance, List typeArgs, ConcreteSyntaxTree wr, IToken tok); + protected abstract string TypeName_UDT(string fullCompileName, List variance, List typeArgs, + ConcreteSyntaxTree wr, IToken tok, bool omitTypeArguments); protected abstract string/*?*/ TypeName_Companion(Type type, ConcreteSyntaxTree wr, IToken tok, MemberDecl/*?*/ member); protected string TypeName_Companion(TopLevelDecl cls, ConcreteSyntaxTree wr, IToken tok) { Contract.Requires(cls != null); @@ -1730,10 +1731,18 @@ public virtual bool NeedsCustomReceiver(MemberDecl member) { // One of the limitations in many target language encodings are restrictions to instance members. If an // instance member can't be directly expressed in the target language, we make it a static member with an // additional first argument specifying the `this`, giving it a `CustomReceiver`. - return !member.IsStatic - && (member.EnclosingClass is NewtypeDecl - || (member.EnclosingClass is TraitDecl - && member is ConstantField { Rhs: { } } or Function { Body: { } } or Method { Body: { } })); + if (member.IsStatic) { + return false; + } else if (member.EnclosingClass is NewtypeDecl) { + return true; + } else if (member.EnclosingClass is TraitDecl) { + return member is ConstantField { Rhs: { } } or Function { Body: { } } or Method { Body: { } }; + } else if (member.EnclosingClass is DatatypeDecl datatypeDecl) { + // An undefined value "o" cannot use this o.F(...) form in most languages. + return datatypeDecl.Ctors.Any(ctor => ctor.IsGhost); + } else { + return false; + } } void CompileClassMembers(Program program, TopLevelDeclWithMembers c, IClassWriter classWriter) { @@ -1896,6 +1905,8 @@ void CompileClassMembers(Program program, TopLevelDeclWithMembers c, IClassWrite var wGet = classWriter.CreateGetterSetter(IdName(f), f.Type, f.tok, false, member, out wSet, false); Contract.Assert(wSet == null && wGet == null); // since the previous line specified no body } else { + // A trait field is just declared, not initialized. Any other field gets a default value if field's type is an auto-init type and + // gets a placebo value if the field's type is not an auto-init type. var rhs = c is TraitDecl ? null : PlaceboValue(f.Type, errorWr, f.tok, true); classWriter.DeclareField(IdName(f), c, f.IsStatic, false, f.Type, f.tok, rhs, f); } @@ -2784,7 +2795,18 @@ protected bool ComplicatedTypeParameterForCompilation(TypeParameter.TPVariance v return Util.Comma(types, ty => TypeName(ty, wr, tok)); } + /// + /// If "type" is an auto-init type, then return a default value, else return a placebo value. + /// protected string PlaceboValue(Type type, ConcreteSyntaxTree wr, IToken tok, bool constructTypeParameterDefaultsFromTypeDescriptors = false) { + if (type.HasCompilableValue) { + return DefaultValue(type, wr, tok, constructTypeParameterDefaultsFromTypeDescriptors); + } else { + return ForcePlaceboValue(type, wr, tok, constructTypeParameterDefaultsFromTypeDescriptors); + } + } + + protected string ForcePlaceboValue(Type type, ConcreteSyntaxTree wr, IToken tok, bool constructTypeParameterDefaultsFromTypeDescriptors = false) { Contract.Requires(type != null); Contract.Requires(wr != null); Contract.Requires(tok != null); @@ -2792,20 +2814,19 @@ protected string PlaceboValue(Type type, ConcreteSyntaxTree wr, IToken tok, bool type = type.NormalizeExpandKeepConstraints(); Contract.Assert(type is NonProxyType); // this should never happen, since all types should have been successfully resolved - bool usePlaceboValue = !type.HasCompilableValue; - return TypeInitializationValue(type, wr, tok, usePlaceboValue, constructTypeParameterDefaultsFromTypeDescriptors); + return TypeInitializationValue(type, wr, tok, true, constructTypeParameterDefaultsFromTypeDescriptors); } protected string DefaultValue(Type type, ConcreteSyntaxTree wr, IToken tok, bool constructTypeParameterDefaultsFromTypeDescriptors = false) { Contract.Requires(type != null); - Contract.Requires(type.HasCompilableValue); Contract.Requires(wr != null); Contract.Requires(tok != null); Contract.Ensures(Contract.Result() != null); type = type.NormalizeExpandKeepConstraints(); Contract.Assert(type is NonProxyType); // this should never happen, since all types should have been successfully resolved - return TypeInitializationValue(type, wr, tok, false, constructTypeParameterDefaultsFromTypeDescriptors); + var usePlaceboValue = type.AsDatatype?.GetGroundingCtor().IsGhost == true; + return TypeInitializationValue(type, wr, tok, usePlaceboValue, constructTypeParameterDefaultsFromTypeDescriptors); } // ----- Stmt --------------------------------------------------------------------------------- @@ -4743,7 +4764,7 @@ void writeObj(ConcreteSyntaxTree w) { } else { var w = CreateIIFE1(0, e.Body.Type, e.Body.tok, "_let_dummy_" + GetUniqueAstNumber(e), wr, wStmts); foreach (var bv in e.BoundVars) { - DeclareLocalVar(IdName(bv), bv.Type, bv.tok, false, PlaceboValue(bv.Type, wr, bv.tok, true), w); + DeclareLocalVar(IdName(bv), bv.Type, bv.tok, false, ForcePlaceboValue(bv.Type, wr, bv.tok, true), w); } TrAssignSuchThat(new List(e.BoundVars).ConvertAll(bv => (IVariable)bv), e.RHSs[0], e.Constraint_Bounds, e.tok.line, w, inLetExprBody); EmitReturnExpr(e.Body, e.Body.Type, true, w); diff --git a/Source/DafnyCore/Dafny.atg b/Source/DafnyCore/Dafny.atg index f45c7adc00f..2caf183de27 100644 --- a/Source/DafnyCore/Dafny.atg +++ b/Source/DafnyCore/Dafny.atg @@ -1363,11 +1363,16 @@ DatatypeMemberDecl<.List/*!*/ ctors.> Attributes attrs = null; IToken/*!*/ id; List formals = new List(); + var isGhost = false; .) + // Note, "ghost" is parsed before any attributes. This means that the + // attributes are parsed before the "id", which is consistent with other + // declarations. + [ "ghost" (. isGhost = true; .) ] { Attribute } DatatypeMemberName [ FormalsOptionalIds ] - (. var ctor = new DatatypeCtor(id, id.val, formals, attrs); + (. var ctor = new DatatypeCtor(id, id.val, isGhost, formals, attrs); ctor.StartToken = id; ctor.BodyEndTok = t; ctor.EndToken = t; diff --git a/Source/DafnyCore/Resolver.cs b/Source/DafnyCore/Resolver.cs index e86d548392a..3cb0818c638 100644 --- a/Source/DafnyCore/Resolver.cs +++ b/Source/DafnyCore/Resolver.cs @@ -2145,8 +2145,8 @@ ModuleSignature RegisterTopLevelDecls(ModuleDefinition moduleDef, bool useImport // create and add the query "method" (field, really) string queryName = ctor.Name + "?"; - var query = new SpecialField(ctor.tok, queryName, SpecialField.ID.UseIdParam, "is_" + ctor.CompileName, - false, false, false, Type.Bool, null); + var query = new DatatypeDiscriminator(ctor.tok, queryName, SpecialField.ID.UseIdParam, "is_" + ctor.CompileName, + ctor.IsGhost, Type.Bool, null); query.InheritVisibility(dt); query.EnclosingClass = dt; // resolve here members.Add(queryName, query); @@ -8157,9 +8157,9 @@ protected override bool VisitOneExpr(Expression expr, ref bool inGhostContext) { // that's cool } else if (CanCompareWith(e.E1)) { // oh yeah! - } else if (!t0.SupportsEquality) { + } else if (!t0.PartiallySupportsEquality) { resolver.reporter.Error(MessageSource.Resolver, e.E0, "{0} can only be applied to expressions of types that support equality (got {1}){2}", BinaryExpr.OpcodeString(e.Op), t0, TypeEqualityErrorMessageHint(t0)); - } else if (!t1.SupportsEquality) { + } else if (!t1.PartiallySupportsEquality) { resolver.reporter.Error(MessageSource.Resolver, e.E1, "{0} can only be applied to expressions of types that support equality (got {1}){2}", BinaryExpr.OpcodeString(e.Op), t1, TypeEqualityErrorMessageHint(t1)); } break; @@ -8270,32 +8270,6 @@ bool VisitPattern(CasePattern pat, bool patternGhostContext) { return true; } - private bool CanCompareWith(Expression expr) { - Contract.Requires(expr != null); - if (expr.Type.SupportsEquality) { - return true; - } - expr = expr.Resolved; - if (expr is DatatypeValue) { - var e = (DatatypeValue)expr; - for (int i = 0; i < e.Ctor.Formals.Count; i++) { - if (e.Ctor.Formals[i].IsGhost) { - return false; - } else if (!CanCompareWith(e.Arguments[i])) { - return false; - } - } - return true; - } else if (expr is DisplayExpression) { - var e = (DisplayExpression)expr; - return e.Elements.Count == 0; - } else if (expr is MapDisplayExpr) { - var e = (MapDisplayExpr)expr; - return e.Elements.Count == 0; - } - return false; - } - public void VisitType(IToken tok, Type type, bool inGhostContext) { Contract.Requires(tok != null); Contract.Requires(type != null); @@ -8405,6 +8379,31 @@ string TypeEqualityErrorMessageHint(Type argType) { } } + public static bool CanCompareWith(Expression expr) { + Contract.Requires(expr != null); + if (expr.Type.SupportsEquality) { + return true; + } + expr = expr.Resolved; + if (expr is DatatypeValue datatypeValue && !datatypeValue.Ctor.EnclosingDatatype.HasGhostVariant) { + for (var i = 0; i < datatypeValue.Ctor.Formals.Count; i++) { + if (datatypeValue.Ctor.Formals[i].IsGhost) { + return false; + } else if (!CanCompareWith(datatypeValue.Arguments[i])) { + return false; + } + } + return true; + } else if (expr is DisplayExpression) { + var e = (DisplayExpression)expr; + return e.Elements.Count == 0; + } else if (expr is MapDisplayExpr) { + var e = (MapDisplayExpr)expr; + return e.Elements.Count == 0; + } + return false; + } + #endregion CheckTypeCharacteristics // ------------------------------------------------------------------------------------------------------ @@ -8836,7 +8835,7 @@ public void Visit(Statement stmt, bool mustBeErasable, [CanBeNull] string proofC } else if (stmt is MatchStmt) { var s = (MatchStmt)stmt; - s.IsGhost = mustBeErasable || ExpressionTester.UsesSpecFeatures(s.Source); + s.IsGhost = mustBeErasable || ExpressionTester.UsesSpecFeatures(s.Source) || ExpressionTester.FirstCaseThatDependsOnGhostCtor(s.Cases) != null; if (!mustBeErasable && s.IsGhost) { resolver.reporter.Info(MessageSource.Resolver, s.Tok, "ghost match"); } @@ -9824,9 +9823,11 @@ bool ComputeGroundingCtor(IndDatatypeDecl dt) { } } // this constructor satisfies the requirements, check to see if it is a better fit than the - // one found so far. By "better" it means fewer type arguments. Between the ones with - // the same number of the type arguments, pick the one shows first. - if (groundingCtor == null || typeParametersUsed.Count < lastTypeParametersUsed.Count) { + // one found so far. Here, "better" means + // * a ghost constructor is better than a non-ghost constructor + // * among those, a constructor with fewer type arguments is better + // * among those, the first one is preferred. + if (groundingCtor == null || (!groundingCtor.IsGhost && ctor.IsGhost) || typeParametersUsed.Count < lastTypeParametersUsed.Count) { groundingCtor = ctor; lastTypeParametersUsed = typeParametersUsed; } @@ -9922,12 +9923,24 @@ void DetermineEqualitySupport(IndDatatypeDecl startingPoint, Graph legalSourceConstructors; - var let = ResolveDatatypeUpdate(expr.tok, e.Root, ty.AsDatatype, e.Updates, resolutionContext, out legalSourceConstructors); - if (let != null) { - e.ResolvedExpression = let; + var (ghostLet, compiledLet) = ResolveDatatypeUpdate(expr.tok, e.Root, ty.AsDatatype, e.Updates, resolutionContext, + out var members, out var legalSourceConstructors); + Contract.Assert((ghostLet == null) == (compiledLet == null)); + if (ghostLet != null) { + e.ResolvedExpression = ghostLet; // this might be replaced by e.ResolvedCompiledExpression in CheckIsCompilable + e.ResolvedCompiledExpression = compiledLet; + e.Members = members; e.LegalSourceConstructors = legalSourceConstructors; - expr.Type = let.Type; + expr.Type = ghostLet.Type; } } @@ -15703,9 +15716,18 @@ private void AddXConstraint(IToken tok, string constraintName, Type type, Expres /// Attempts to rewrite a datatype update into more primitive operations, after doing the appropriate resolution checks. /// Upon success, returns that rewritten expression and sets "legalSourceConstructors". /// Upon some resolution error, return null. + /// + /// Actually, the method returns two expressions (or returns "(null, null)"). The first expression is the desugaring to be + /// used when the DatatypeUpdateExpr is used in a ghost context. The second is to be used for a compiled context. In either + /// case, "legalSourceConstructors" contains both ghost and compiled constructors. + /// + /// The reason for computing both desugarings here is that it's too early to tell if the DatatypeUpdateExpr is being used in + /// a ghost or compiled context. This is a consequence of doing the deguaring so early. But it's also convenient to do the + /// desugaring during resolution, because then the desugaring can be constructed as a non-resolved expression on which ResolveExpression + /// is called--this is easier than constructing an already-resolved expression. /// - Expression ResolveDatatypeUpdate(IToken tok, Expression root, DatatypeDecl dt, List> memberUpdates, - ResolutionContext resolutionContext, out List legalSourceConstructors) { + (Expression, Expression) ResolveDatatypeUpdate(IToken tok, Expression root, DatatypeDecl dt, List> memberUpdates, + ResolutionContext resolutionContext, out List members, out List legalSourceConstructors) { Contract.Requires(tok != null); Contract.Requires(root != null); Contract.Requires(dt != null); @@ -15713,6 +15735,7 @@ Expression ResolveDatatypeUpdate(IToken tok, Expression root, DatatypeDecl dt, L Contract.Requires(resolutionContext != null); legalSourceConstructors = null; + members = new List(); // First, compute the list of candidate result constructors, that is, the constructors // that have all of the mentioned destructors. Issue errors for duplicated names and for @@ -15733,6 +15756,7 @@ Expression ResolveDatatypeUpdate(IToken tok, Expression root, DatatypeDecl dt, L } else if (!(member is DatatypeDestructor)) { reporter.Error(MessageSource.Resolver, entry.Item1, "member '{0}' is not a destructor in datatype '{1}'", destructor_str, dt.Name); } else { + members.Add(member); var destructor = (DatatypeDestructor)member; var intersection = new List(candidateResultCtors.Intersect(destructor.EnclosingCtors)); if (intersection.Count == 0) { @@ -15754,7 +15778,7 @@ Expression ResolveDatatypeUpdate(IToken tok, Expression root, DatatypeDecl dt, L } } if (candidateResultCtors.Count == 0) { - return null; + return (null, null); } // Check that every candidate result constructor has given a name to all of its parameters. @@ -15768,26 +15792,42 @@ Expression ResolveDatatypeUpdate(IToken tok, Expression root, DatatypeDecl dt, L } } if (hasError) { - return null; + return (null, null); } // The legal source constructors are the candidate result constructors. (Yep, two names for the same thing.) legalSourceConstructors = candidateResultCtors; Contract.Assert(1 <= legalSourceConstructors.Count); - // Rewrite the datatype update root.(x := X, y := Y, ...) to: - // var d := root; - // var x := X; // EXCEPT: don't do this for ghost fields - // var y := Y; - // .. - // if d.CandidateResultConstructor0 then - // CandidateResultConstructor0(x, y, ..., d.f0, d.f1, ...) // for a ghost field x, use the expression X directly - // else if d.CandidateResultConstructor1 then - // CandidateResultConstructor0(x, y, ..., d.g0, d.g1, ...) - // ... - // else - // CandidateResultConstructorN(x, y, ..., d.k0, d.k1, ...) - // + var desugaringForGhostContext = DesugarDatatypeUpdate(tok, root, dt, candidateResultCtors, rhsBindings, resolutionContext); + var nonGhostConstructors = candidateResultCtors.Where(ctor => !ctor.IsGhost).ToList(); + if (nonGhostConstructors.Count == candidateResultCtors.Count) { + return (desugaringForGhostContext, desugaringForGhostContext); + } + var desugaringForCompiledContext = DesugarDatatypeUpdate(tok, root, dt, nonGhostConstructors, rhsBindings, resolutionContext); + return (desugaringForGhostContext, desugaringForCompiledContext); + } + + /// + // Rewrite the datatype update root.(x := X, y := Y, ...) to: + /// var d := root; + /// var x := X; // EXCEPT: don't do this for ghost fields + /// var y := Y; + /// .. + /// if d.CandidateResultConstructor0 then + /// CandidateResultConstructor0(x, y, ..., d.f0, d.f1, ...) // for a ghost field x, use the expression X directly + /// else if d.CandidateResultConstructor1 then + /// CandidateResultConstructor0(x, y, ..., d.g0, d.g1, ...) + /// ... + /// else + /// CandidateResultConstructorN(x, y, ..., d.k0, d.k1, ...) + /// + private Expression DesugarDatatypeUpdate(IToken tok, Expression root, DatatypeDecl dt, List candidateResultCtors, + Dictionary> rhsBindings, ResolutionContext resolutionContext) { + + if (candidateResultCtors.Count == 0) { + return root; + } Expression rewrite = null; // Create a unique name for d', the variable we introduce in the let expression var dName = FreshTempVarName("dt_update_tmp#", resolutionContext.CodeContext); @@ -15814,7 +15854,9 @@ Expression ResolveDatatypeUpdate(IToken tok, Expression root, DatatypeDecl dt, L actualBindings.Add(new ActualBinding(bindingName, ctorArg)); } var ctor_call = new DatatypeValue(tok, crc.EnclosingDatatype.Name, crc.Name, actualBindings); - ResolveDatatypeValue(resolutionContext, ctor_call, dt, root.Type.NormalizeExpand()); // resolve to root.Type, so that type parameters get filled in appropriately + // in the following line, resolve to root.Type, so that type parameters get filled in appropriately + ResolveDatatypeValue(resolutionContext, ctor_call, dt, root.Type.NormalizeExpand()); + if (body == null) { body = ctor_call; } else { @@ -15823,7 +15865,7 @@ Expression ResolveDatatypeUpdate(IToken tok, Expression root, DatatypeDecl dt, L body = new ITEExpr(tok, false, guard, ctor_call, body); } } - Contract.Assert(body != null); // because there was at least one element in candidateResultCtors + Contract.Assert(body != null); // because there was at least one element in candidateResultCtors // Wrap the let's around body rewrite = body; diff --git a/Source/DafnyCore/Util.cs b/Source/DafnyCore/Util.cs index a89dd2bab55..42e117ac832 100644 --- a/Source/DafnyCore/Util.cs +++ b/Source/DafnyCore/Util.cs @@ -69,6 +69,24 @@ public static string Comma(string comma, int count, Func f) { return res; } + public static string PrintableNameList(List names, string grammaticalConjunction) { + Contract.Requires(names != null); + Contract.Requires(1 <= names.Count); + Contract.Requires(grammaticalConjunction != null); + var n = names.Count; + if (n == 1) { + return string.Format("'{0}'", names[0]); + } else if (n == 2) { + return string.Format("'{0}' {1} '{2}'", names[0], grammaticalConjunction, names[1]); + } else { + var s = ""; + for (int i = 0; i < n - 1; i++) { + s += string.Format("'{0}', ", names[i]); + } + return s + string.Format("{0} '{1}'", grammaticalConjunction, names[n - 1]); + } + } + public static string Repeat(int count, string s) { Contract.Requires(0 <= count); Contract.Requires(s != null); @@ -831,11 +849,41 @@ private bool CheckIsCompilable(Expression expr, ICodeContext codeContext) { } } else if (expr is MemberSelectExpr selectExpr) { + if (reporter != null) { + selectExpr.InCompiledContext = true; + } if (selectExpr.Member != null && selectExpr.Member.IsGhost) { var what = selectExpr.Member.WhatKindMentionGhost; reporter?.Error(MessageSource.Resolver, selectExpr, $"a {what} is allowed only in specification contexts"); return false; + } else if (selectExpr.Member is DatatypeDestructor dtor && dtor.EnclosingCtors.All(ctor => ctor.IsGhost)) { + var what = selectExpr.Member.WhatKind; + reporter?.Error(MessageSource.Resolver, selectExpr, $"{what} '{selectExpr.MemberName}' can be used only in specification contexts"); + return false; + } + + } else if (expr is DatatypeUpdateExpr updateExpr) { + if (resolver != null) { + updateExpr.InCompiledContext = true; + } + isCompilable = CheckIsCompilable(updateExpr.Root, codeContext); + Contract.Assert(updateExpr.Members.Count == updateExpr.Updates.Count); + for (var i = 0; i < updateExpr.Updates.Count; i++) { + var member = (DatatypeDestructor)updateExpr.Members[i]; + if (!member.IsGhost) { + isCompilable = CheckIsCompilable(updateExpr.Updates[i].Item3, codeContext) && isCompilable; + } + } + if (updateExpr.LegalSourceConstructors.All(ctor => ctor.IsGhost)) { + var dtors = Util.PrintableNameList(updateExpr.Members.ConvertAll(dtor => dtor.Name), "and"); + var ctorNames = DatatypeDestructor.PrintableCtorNameList(updateExpr.LegalSourceConstructors, "or"); + reporter?.Error(MessageSource.Resolver, updateExpr, + $"in a compiled context, update of {dtors} cannot be applied to a datatype value of a ghost variant (ghost constructor {ctorNames})"); + isCompilable = false; } + // switch to the desugared expression for compiled contexts, but don't step into it + updateExpr.ResolvedExpression = updateExpr.ResolvedCompiledExpression; + return isCompilable; } else if (expr is FunctionCallExpr callExpr) { if (callExpr.Function != null) { @@ -878,6 +926,10 @@ private bool CheckIsCompilable(Expression expr, ICodeContext codeContext) { return isCompilable; } else if (expr is DatatypeValue value) { + if (value.Ctor.IsGhost) { + reporter?.Error(MessageSource.Resolver, expr, "ghost constructor is allowed only in specification contexts"); + isCompilable = false; + } // check all NON-ghost arguments // note that if resolution is successful, then |e.Arguments| == |e.Ctor.Formals| for (int i = 0; i < value.Arguments.Count; i++) { @@ -910,6 +962,9 @@ private bool CheckIsCompilable(Expression expr, ICodeContext codeContext) { return CheckIsCompilable(stmtExpr.E, codeContext); } else if (expr is BinaryExpr binaryExpr) { + if (reporter != null) { + binaryExpr.InCompiledContext = true; + } switch (binaryExpr.ResolvedOp_PossiblyStillUndetermined) { case BinaryExpr.ResolvedOpcode.RankGt: case BinaryExpr.ResolvedOpcode.RankLt: @@ -997,6 +1052,14 @@ private bool CheckIsCompilable(Expression expr, ICodeContext codeContext) { // We don't care about the different operators; we only want the operands, so let's get them directly from // the chaining expression return chainingExpression.Operands.TrueForAll(ee => CheckIsCompilable(ee, codeContext)); + + } else if (expr is MatchExpr matchExpr) { + var mc = FirstCaseThatDependsOnGhostCtor(matchExpr.Cases); + if (mc != null) { + reporter?.Error(MessageSource.Resolver, mc.tok, "match expression is not compilable, because it depends on a ghost constructor"); + isCompilable = false; + } + // other conditions are checked below } foreach (var ee in expr.SubExpressions) { @@ -1079,6 +1142,10 @@ public static bool UsesSpecFeatures(Expression expr) { return cce.NonNull(e.Var).IsGhost; } else if (expr is DatatypeValue) { var e = (DatatypeValue)expr; + if (e.Ctor.IsGhost) { + return true; + } + // check all NON-ghost arguments // note that if resolution is successful, then |e.Arguments| == |e.Ctor.Formals| for (int i = 0; i < e.Arguments.Count; i++) { @@ -1094,12 +1161,30 @@ public static bool UsesSpecFeatures(Expression expr) { MapDisplayExpr e = (MapDisplayExpr)expr; return e.Elements.Exists(p => UsesSpecFeatures(p.A) || UsesSpecFeatures(p.B)); } else if (expr is MemberSelectExpr) { - MemberSelectExpr e = (MemberSelectExpr)expr; - if (e.Member != null) { - return cce.NonNull(e.Member).IsGhost || UsesSpecFeatures(e.Obj); + var e = (MemberSelectExpr)expr; + if (UsesSpecFeatures(e.Obj)) { + return true; + } else if (e.Member != null && e.Member.IsGhost) { + return true; + } else if (e.Member is DatatypeDestructor dtor) { + return dtor.EnclosingCtors.All(ctor => ctor.IsGhost); } else { return false; } + } else if (expr is DatatypeUpdateExpr updateExpr) { + if (UsesSpecFeatures(updateExpr.Root)) { + return true; + } + Contract.Assert(updateExpr.Members.Count == updateExpr.Updates.Count); + for (var i = 0; i < updateExpr.Updates.Count; i++) { + var member = (DatatypeDestructor)updateExpr.Members[i]; + // note, updating a ghost field does not make the expression ghost (cf. ghost let expressions) + if (!member.IsGhost && UsesSpecFeatures(updateExpr.Updates[i].Item3)) { + return true; + } + } + return updateExpr.LegalSourceConstructors.All(ctor => ctor.IsGhost); + } else if (expr is SeqSelectExpr) { SeqSelectExpr e = (SeqSelectExpr)expr; return UsesSpecFeatures(e.Seq) || @@ -1200,7 +1285,7 @@ public static bool UsesSpecFeatures(Expression expr) { return UsesSpecFeatures(((NestedMatchExpr)expr).ResolvedExpression); } else if (expr is MatchExpr) { MatchExpr me = (MatchExpr)expr; - if (UsesSpecFeatures(me.Source)) { + if (UsesSpecFeatures(me.Source) || FirstCaseThatDependsOnGhostCtor(me.Cases) != null) { return true; } return me.Cases.Exists(mc => UsesSpecFeatures(mc.Body)); @@ -1241,5 +1326,12 @@ static void MakeGhostAsNeeded(CasePattern arg, DatatypeDestructor d) { MakeGhostAsNeeded(arg); } } + + /// + /// Return the first ghost constructor listed in a case, or null, if there is none. + /// + public static MC FirstCaseThatDependsOnGhostCtor(List cases) where MC : MatchCase { + return cases.FirstOrDefault(kees => kees.Ctor.IsGhost, null); + } } } diff --git a/Source/DafnyCore/Verifier/ProofObligationDescription.cs b/Source/DafnyCore/Verifier/ProofObligationDescription.cs index 174625c4386..9c040e92ee3 100644 --- a/Source/DafnyCore/Verifier/ProofObligationDescription.cs +++ b/Source/DafnyCore/Verifier/ProofObligationDescription.cs @@ -1,3 +1,4 @@ +using System.Collections.Generic; using System.Diagnostics.Contracts; using JetBrains.Annotations; @@ -605,6 +606,29 @@ public DestructorValid(string dtorName, string ctorNames) { } } +public class NotGhostVariant : ProofObligationDescription { + public override string SuccessDescription => + $"in a compiled context, {subject} is not applied to a datatype value of a ghost variant (ghost constructor {ctorNames})"; + + public override string FailureDescription => + $"in a compiled context, {subject} cannot be applied to a datatype value of a ghost variant (ghost constructor {ctorNames})"; + + public override string ShortDescription => "not ghost variant"; + + private readonly string subject; + private readonly string ctorNames; + + public NotGhostVariant(string subject, List ctors) { + this.subject = subject; + this.ctorNames = DatatypeDestructor.PrintableCtorNameList(ctors, "or"); + } + + public NotGhostVariant(string whatKind, string dtorNames, List ctors) { + this.subject = $"{whatKind} {dtorNames}"; + this.ctorNames = DatatypeDestructor.PrintableCtorNameList(ctors, "or"); + } +} + //// Misc constraints diff --git a/Source/DafnyCore/Verifier/Translator.ExpressionWellformed.cs b/Source/DafnyCore/Verifier/Translator.ExpressionWellformed.cs index bc6661ada09..5d64a6b6a56 100644 --- a/Source/DafnyCore/Verifier/Translator.ExpressionWellformed.cs +++ b/Source/DafnyCore/Verifier/Translator.ExpressionWellformed.cs @@ -307,8 +307,7 @@ void CheckWellformedWithResult(Expression expr, WFOptions options, Bpl.Expr resu CheckNonNull(expr.tok, e.Obj, builder, etran, options.AssertKv); // Check that the receiver is available in the state in which the dereference occurs } - } else if (e.Member is DatatypeDestructor) { - var dtor = (DatatypeDestructor)e.Member; + } else if (e.Member is DatatypeDestructor dtor) { var correctConstructor = BplOr(dtor.EnclosingCtors.ConvertAll( ctor => FunctionCall(e.tok, ctor.QueryField.FullSanitizedName, Bpl.Type.Bool, etran.TrExpr(e.Obj)))); if (dtor.EnclosingCtors.Count == dtor.EnclosingCtors[0].EnclosingDatatype.Ctors.Count) { @@ -318,6 +317,9 @@ void CheckWellformedWithResult(Expression expr, WFOptions options, Bpl.Expr resu builder.Add(Assert(GetToken(expr), correctConstructor, new PODesc.DestructorValid(dtor.Name, dtor.EnclosingCtorNames("or")))); } + CheckNotGhostVariant(e, "destructor", dtor.EnclosingCtors, builder, etran); + } else if (e.Member is DatatypeDiscriminator discriminator) { + CheckNotGhostVariant(e, "discriminator", ((DatatypeDecl)discriminator.EnclosingClass).Ctors, builder, etran); } if (!e.Member.IsStatic) { if (e.Member is TwoStateFunction) { @@ -895,6 +897,40 @@ void CheckWellformedWithResult(Expression expr, WFOptions options, Bpl.Expr resu builder.Add(Assert(GetToken(expr), Bpl.Expr.Le(Bpl.Expr.Literal(0), etran.TrExpr(e.E1)), positiveDesc, options.AssertKv)); builder.Add(Assert(GetToken(expr), Bpl.Expr.Le(etran.TrExpr(e.E1), Bpl.Expr.Literal(w)), upperDesc, options.AssertKv)); } + } + break; + case BinaryExpr.ResolvedOpcode.EqCommon: + case BinaryExpr.ResolvedOpcode.NeqCommon: + CheckWellformed(e.E1, options, locals, builder, etran); + if (e.InCompiledContext) { + if (Resolver.CanCompareWith(e.E0) || Resolver.CanCompareWith(e.E1)) { + // everything's fine + } else { + Contract.Assert(!e.E0.Type.SupportsEquality); // otherwise, CanCompareWith would have returned "true" above + Contract.Assert(!e.E1.Type.SupportsEquality); // otherwise, CanCompareWith would have returned "true" above + Contract.Assert(e.E0.Type.PartiallySupportsEquality); // otherwise, the code wouldn't have got passed the resolver + Contract.Assert(e.E1.Type.PartiallySupportsEquality); // otherwise, the code wouldn't have got passed the resolver + var dt = e.E0.Type.AsIndDatatype; + Contract.Assert(dt != null); // only inductive datatypes support equality partially + + // to compare the datatype values for equality, there must not be any possibility that either of the datatype + // variants is a ghost constructor + var ghostConstructors = dt.Ctors.Where(ctor => ctor.IsGhost).ToList(); + Contract.Assert(ghostConstructors.Count != 0); + + void checkOperand(Expression operand) { + var value = etran.TrExpr(operand); + var notGhostCtor = BplAnd(ghostConstructors.ConvertAll( + ctor => Bpl.Expr.Not(FunctionCall(expr.tok, ctor.QueryField.FullSanitizedName, Bpl.Type.Bool, value)))); + builder.Add(Assert(GetToken(expr), notGhostCtor, + new PODesc.NotGhostVariant("equality", ghostConstructors))); + } + + checkOperand(e.E0); + checkOperand(e.E1); + } + + } break; default: @@ -1103,6 +1139,9 @@ void CheckWellformedWithResult(Expression expr, WFOptions options, Bpl.Expr resu new PODesc.ValidConstructorNames(DatatypeDestructor.PrintableCtorNameList(e.LegalSourceConstructors, "or")))); } + CheckNotGhostVariant(e.InCompiledContext, expr, e.Root, "update of", e.Members, + e.LegalSourceConstructors, builder, etran); + CheckWellformedWithResult(e.ResolvedExpression, options, result, resultType, locals, builder, etran); result = null; @@ -1178,6 +1217,29 @@ void BuildWithHeapAs(IToken token, Bpl.Expr temporaryHeap, string heapVarSuffix, builder.Add(Bpl.Cmd.SimpleAssign(token, theHeap, tmpHeap)); } + private void CheckNotGhostVariant(MemberSelectExpr expr, string whatKind, List candidateCtors, + BoogieStmtListBuilder builder, ExpressionTranslator etran) { + CheckNotGhostVariant(expr.InCompiledContext, expr, expr.Obj, whatKind, new List() { expr.Member }, + candidateCtors, builder, etran); + } + + private void CheckNotGhostVariant(bool inCompiledContext, Expression exprUsedForToken, Expression datatypeValue, + string whatKind, List members, List candidateCtors, BoogieStmtListBuilder builder, ExpressionTranslator etran) { + if (inCompiledContext) { + // check that there is no possibility that the datatype variant is a ghost constructor + var enclosingGhostConstructors = candidateCtors.Where(ctor => ctor.IsGhost).ToList(); + if (enclosingGhostConstructors.Count != 0) { + var obj = etran.TrExpr(datatypeValue); + var notGhostCtor = BplAnd(enclosingGhostConstructors.ConvertAll( + ctor => Bpl.Expr.Not(FunctionCall(exprUsedForToken.tok, ctor.QueryField.FullSanitizedName, Bpl.Type.Bool, obj)))); + builder.Add(Assert(GetToken(exprUsedForToken), notGhostCtor, + new PODesc.NotGhostVariant(whatKind, + Util.PrintableNameList(members.ConvertAll(member => member.Name), "and"), + enclosingGhostConstructors))); + } + } + } + void CheckWellformedSpecialFunction(FunctionCallExpr expr, WFOptions options, Bpl.Expr result, Type resultType, List locals, BoogieStmtListBuilder builder, ExpressionTranslator etran) { Contract.Requires(expr.Function is SpecialFunction); diff --git a/Test/comp/Datatype.dfy b/Test/comp/Datatype.dfy index 671c46830d0..6ce855db428 100644 --- a/Test/comp/Datatype.dfy +++ b/Test/comp/Datatype.dfy @@ -36,6 +36,8 @@ method Main() { AllBerry(); TestConflictingNames(); TestModule(); + + TestGhostDestructors(); } function method Up(m: nat, n: nat): List @@ -138,3 +140,16 @@ method PrintMaybe(x : Module.OptionInt) { case Some(n) => print n, "\n"; case None => print "None\n"; } + +datatype R = R(x: int, ghost g: int) + +method TestGhostDestructors() { + var a := R(10, 20); + var b := a.(x := a.x + 1); + var c := b.(x := b.x + 1, g := b.g + 1); + var d := c.(g := c.g + 1, x := c.x + 1); + var e := d.(g := d.g + 1); + + assert e == R(13, 23); + expect e.x == 13; +} diff --git a/Test/comp/Datatype.dfy.expect b/Test/comp/Datatype.dfy.expect index 39c50eaf937..5c221597161 100644 --- a/Test/comp/Datatype.dfy.expect +++ b/Test/comp/Datatype.dfy.expect @@ -1,5 +1,5 @@ -Dafny program verifier finished with 11 verified, 0 errors +Dafny program verifier finished with 12 verified, 0 errors Dafny program verifier did not attempt verification List.Nil diff --git a/Test/comp/Uninitialized.dfy b/Test/comp/Uninitialized.dfy new file mode 100644 index 00000000000..094bc280096 --- /dev/null +++ b/Test/comp/Uninitialized.dfy @@ -0,0 +1,214 @@ +// RUN: %dafny /compile:0 "%s" > "%t" +// RUN: %dafny /noVerify /compile:4 /spillTargetCode:2 /compileTarget:cs "%s" >> "%t" +// RUN: %dafny /noVerify /compile:4 /spillTargetCode:2 /compileTarget:js "%s" >> "%t" +// RUN: %dafny /noVerify /compile:4 /spillTargetCode:2 /compileTarget:go "%s" >> "%t" +// RUN: %dafny /noVerify /compile:4 /spillTargetCode:2 /compileTarget:java "%s" >> "%t" +// RUN: %dafny /noVerify /compile:4 /spillTargetCode:2 /compileTarget:py "%s" >> "%t" +// RUN: %diff "%s.expect" "%t" + +module {:options "/functionSyntax:4"} Stacks { + export + reveals Stack + provides Stack.Valid, Stack.Repr, Stack.Elements + reveals Stack.Count + provides Stack.Push, Stack.Pop + + datatype MaybeInitialized = ghost Uninitialized | Initialized(value: T) + + // Note, nothing is assumed about the type parameter T in the following line. In particular, + // it's not assumed to be an auto-init type (and, in fact, may even be empty). + class Stack { + ghost var Repr: set + ghost var Elements: seq + ghost predicate Valid() + reads this, Repr + ensures Valid() ==> this in Repr + { + this in Repr && + arr in Repr && + n == |Elements| <= arr.Length != 0 && + forall i :: 0 <= i < n ==> + arr[i].Initialized? && arr[i].value == Elements[i] + } + + var arr: array> + var n: nat + + constructor () + ensures Valid() && fresh(Repr) && Elements == [] + { + Elements, n := [], 0; + arr := new [20]; + Repr := {this, arr}; + } + + function Count(): nat + requires Valid() + reads Repr + { + |Elements| + } by method { + return n; + } + + method Push(t: T) + requires Valid() + modifies Repr + ensures Valid() && fresh(Repr - old(Repr)) + ensures Elements == old(Elements) + [t] + { + if n == arr.Length { + var a := new [2 * n]; + forall i | 0 <= i < n { + a[i] := arr[i]; + } + arr := a; + Repr := Repr + {a}; + } + arr[n] := Initialized(t); + Elements, n := Elements + [t], n + 1; + } + + method Pop() returns (t: T) + requires Valid() && Elements != [] + modifies Repr + ensures Valid() && fresh(Repr - old(Repr)) + ensures var last := |old(Elements)| - 1; + t == old(Elements)[last] && + Elements == old(Elements)[..last] + { + n := n - 1; + Elements := Elements[..n]; + t := arr[n].value; + } + } +} + +type Empty = x: int | false witness * + +method Main() { + var s := new Stacks.Stack(); + s.Push(10); + s.Push(12); + s.Push(11); + var x := s.Pop(); + assert s.Elements == [10, 12] && x == 11; + var count := s.Count(); + assert count == 2; + print x, " ", count, "\n"; // 11 2 + + var s' := new Stacks.Stack(); + count := s'.Count(); + assert count == 0; + print count, "\n"; // 0 + + EnumerationTests.Test(); + DestructorTests.Test(); +} + +module {:options "/functionSyntax:4"} EnumerationTests { + datatype Enum = ghost EnumA | EnumB + { + const N := 13 + + predicate Is(n: nat) { + N == n + } + } + + datatype AllGhost = ghost Ctor0 | ghost Ctor1 + { + const N := 13 + + predicate Is(n: nat) { + N == n + } + + method CheckIs(n: nat) returns (r: bool) { + r := N == n; + } + } + + method Test() { + var e := PickEnumValue(); + var s: seq; + s := [e]; + print |s|, "\n"; // 1 + + var g, sg; + g := PickAllGhostValue(); + sg := [g]; + print |sg|, "\n"; // 1 + } + + method PickEnumValue() returns (r: Enum) { + if e: Enum :| e.Is(13) { + r := e; + } + } + + method PickAllGhostValue() returns (r: AllGhost) { + if ag: AllGhost :| ag.Is(13) { + r := ag; + } + } +} + +module {:options "/functionSyntax:4"} DestructorTests { + datatype WithCommonDestructors = + | CtorA(a: A, x: int) + | ghost CtorAB(a: A, b: B) + | CtorB(b: B, y: int, ghost z: int) + + method Test() { + var wcd := CtorA(true, 7); + print wcd.a, " "; // true + wcd := wcd.(a := false); + print wcd.a, " ", wcd.x, "\n"; // false 7 + + wcd := CtorB(2.11, 9, 100); + print wcd.b, " "; // 2.11 + wcd := wcd.(b := 2.13); + print wcd.b, " ", wcd.y, "\n"; // 2.13 9 + + wcd := wcd.(y := 11, z := 101); + print wcd.y, " "; // 11 + wcd := wcd.(z := 102, y := 12); + print wcd.y, " "; // 12 + wcd := wcd.(z := 103); + print wcd.y, "\n"; // 12 + } +} + +module {:options "/functionSyntax:4"} WhiteBoxTests { + // The following code tests two conditions in the implementation. + + // The following List does not support equality (because of the ghost parameter) + datatype List = Nil | Nilly(x: int) | Konstig(ghost head: int, tail: List) + type RestrictedList = xs: List | xs == Nilly(2) witness * + + method M(xs: RestrictedList) returns (b: bool) { + // "Resolver.CanCompareWith" returns "true" for the LHS in the following comparison + // and returns "false" for the RHS. This shows that one needs to call "Resolver.CanCompareWith" + // on both operands. If either of them returns true, the comparison can be compiled. + // Additionally, since the type of "xs" is a subset type, this test makes sure that + // "PartiallySupportsEquality" understands subset types. + b := xs == Nilly(2); + } +} + +module ConstraintsAreGhost { + // The constraint of a subset type is ghost. However, the Resolver calls CheckIsCompilable + // to determine if, perhaps, the constraint is compilable after all (because that enables + // the compiler to do some additional things). The .InCompiledContext fields should not be + // set when CheckIsCompilable is called in this mode, as is tested by the following declarations. + + datatype A = ghost MakeA(x: int) + type B = a: A | a.x == 0 ghost witness MakeA(0) + + datatype R = R(ghost x: int) + type S = r: R | r.x == 0 witness R(0) + + datatype List = Nil | ghost Konstig(ghost head: int, tail: List) + type RestrictedList = xs: List | xs.Konstig? ghost witness Konstig(0, Nil) +} diff --git a/Test/comp/Uninitialized.dfy.expect b/Test/comp/Uninitialized.dfy.expect new file mode 100644 index 00000000000..62f6d800ff3 --- /dev/null +++ b/Test/comp/Uninitialized.dfy.expect @@ -0,0 +1,47 @@ + +Dafny program verifier finished with 16 verified, 0 errors + +Dafny program verifier did not attempt verification +11 2 +0 +1 +1 +true false 7 +2.11 2.13 9 +11 12 12 + +Dafny program verifier did not attempt verification +11 2 +0 +1 +1 +true false 7 +2.11 2.13 9 +11 12 12 + +Dafny program verifier did not attempt verification +11 2 +0 +1 +1 +true false 7 +2.11 2.13 9 +11 12 12 + +Dafny program verifier did not attempt verification +11 2 +0 +1 +1 +true false 7 +2.11 2.13 9 +11 12 12 + +Dafny program verifier did not attempt verification +11 2 +0 +1 +1 +true false 7 +2.11 2.13 9 +11 12 12 diff --git a/Test/dafny0/DatatypeUpdateResolution.dfy b/Test/dafny0/DatatypeUpdateResolution.dfy index 18bd5cd16a3..cac2883ab3a 100644 --- a/Test/dafny0/DatatypeUpdateResolution.dfy +++ b/Test/dafny0/DatatypeUpdateResolution.dfy @@ -1,43 +1,98 @@ // RUN: %dafny_0 /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t" // RUN: %diff "%s.expect" "%t" -datatype MyDataType = MyConstructor(myint:int, mybool:bool) - | MyOtherConstructor(otherbool:bool) - | MyNumericConstructor(42:int) -datatype SomeOtherType = S_O_T(non_destructor: int) - -method test(foo:MyDataType, x:int) returns (abc:MyDataType, def:MyDataType, ghi:MyDataType, jkl:MyDataType) - requires foo.MyConstructor? - ensures abc == foo.(myint := x + 2) - ensures jkl == foo.(non_destructor := 5) // error: 'non_destructor' is not a destructor in MyDataType - ensures jkl == foo.(mybool := true, 40 := 100, myint := 200) // error: '40' is not a destructor -{ - abc := MyConstructor(x + 2, foo.mybool).(myint := x + 3); - abc := foo.(myint := x + 2, mybool := true).(mybool := false); // allowed - def := MyOtherConstructor(!foo.mybool).(otherbool := true, otherbool := true); // error: duplicated member - ghi := MyConstructor(2, false).(otherbool := true); // allowed, and will generate verification error - jkl := foo.(42 := 7, otherbool := true); // error: members are from different constructors -} +module MainStuff { + datatype MyDataType = MyConstructor(myint:int, mybool:bool) + | MyOtherConstructor(otherbool:bool) + | MyNumericConstructor(42:int) + datatype SomeOtherType = S_O_T(non_destructor: int) + + method test(foo:MyDataType, x:int) returns (abc:MyDataType, def:MyDataType, ghi:MyDataType, jkl:MyDataType) + requires foo.MyConstructor? + ensures abc == foo.(myint := x + 2) + ensures jkl == foo.(non_destructor := 5) // error: 'non_destructor' is not a destructor in MyDataType + ensures jkl == foo.(mybool := true, 40 := 100, myint := 200) // error: '40' is not a destructor + { + abc := MyConstructor(x + 2, foo.mybool).(myint := x + 3); + abc := foo.(myint := x + 2, mybool := true).(mybool := false); // allowed + def := MyOtherConstructor(!foo.mybool).(otherbool := true, otherbool := true); // error: duplicated member + ghi := MyConstructor(2, false).(otherbool := true); // allowed, and will generate verification error + jkl := foo.(42 := 7, otherbool := true); // error: members are from different constructors + } + + datatype Dt = Make(x: int) + + method Main() + { + var d := Make(5); + d := d.(x := 20); + d := d.(Make? := d); // error: Make? is not a destructor (this previously crashed the resolver) + } + + module Issue214Regression { + datatype GenericType = GenericType(value:T) + + type ConcreteType = GenericType -datatype Dt = Make(x: int) + function F(c:ConcreteType): ConcreteType { + c.(value := 0) + } -method Main() -{ - var d := Make(5); - d := d.(x := 20); - d := d.(Make? := d); // error: Make? is not a destructor (this previously crashed the resolver) + function G(): int { + ConcreteType.GenericType(5).value + } + } } -module Issue214Regression { - datatype GenericType = GenericType(value:T) +module GhostExpressions { + datatype R = R(x: int, ghost y: int) - type ConcreteType = GenericType + // source is ghost + method Test0(ghost r: R, g: int) returns (b: R) { + var a := r.(x := g); // the use of r makes RHS ghost + b := a; // error: RHS is ghost, LHS is not - function F(c:ConcreteType): ConcreteType { - c.(value := 0) + b := r.(x := g); // error: RHS is ghost, LHS is not } - function G(): int { - ConcreteType.GenericType(5).value + // new value is ghost + method Test1(r: R, ghost g: int, h: int) returns (b: R) { + var a := r.(x := g); // the use of g makes RHS ghost + b := a; // error: RHS is ghost, LHS is not + + b := r.(x := g); // error: RHS is ghost, LHS is not + + var c := r.(y := g); + b := c; + b := r.(y := g); + + var d := if r.x == 3 then r.(x := g, y := h) else r.(y := h, x := g); // the use of g makes RHS ghost + b := d; // error: RHS is ghost, LHS is not + b := r.(x := g, y := h); // error: RHS is ghost, LHS is not + b := r.(y := h, x := g); // error: RHS is ghost, LHS is not + + var e := if r.x == 3 then r.(x := h, y := g) else r.(y := g, x := h); + b := e; + b := r.(x := h, y := g); + b := r.(y := g, x := h); + } + + // field is ghost + method Test2(r: R, g: int) returns (b: R) { + // In the following, since y is ghost, the update operations are really just no-ops in the compiled code. + var a := r.(y := g); + b := a; + + b := r.(y := g); + } + + // one of the fields is ghost + method Test3(r: R, g: int) returns (b: R) { + // In the following, since y is ghost, the updates of y are really just no-ops in the compiled code. + var a := if g == 3 then r.(x := g, y := g) else r.(y := g, x := g); + b := a; + + b := r.(x := g, y := g); + b := r.(y := g, x := g); } } diff --git a/Test/dafny0/DatatypeUpdateResolution.dfy.expect b/Test/dafny0/DatatypeUpdateResolution.dfy.expect index bdf030e6679..594b5991441 100644 --- a/Test/dafny0/DatatypeUpdateResolution.dfy.expect +++ b/Test/dafny0/DatatypeUpdateResolution.dfy.expect @@ -1,6 +1,13 @@ -DatatypeUpdateResolution.dfy(12,22): Error: member 'non_destructor' does not exist in datatype 'MyDataType' -DatatypeUpdateResolution.dfy(13,38): Error: member '40' does not exist in datatype 'MyDataType' -DatatypeUpdateResolution.dfy(17,61): Error: duplicate update member 'otherbool' -DatatypeUpdateResolution.dfy(19,23): Error: updated datatype members must belong to the same constructor (unlike the previously mentioned destructors, 'otherbool' does not belong to 'MyNumericConstructor') -DatatypeUpdateResolution.dfy(28,10): Error: member 'Make?' is not a destructor in datatype 'Dt' -5 resolution/type errors detected in DatatypeUpdateResolution.dfy +DatatypeUpdateResolution.dfy(13,24): Error: member 'non_destructor' does not exist in datatype 'MyDataType' +DatatypeUpdateResolution.dfy(14,40): Error: member '40' does not exist in datatype 'MyDataType' +DatatypeUpdateResolution.dfy(18,63): Error: duplicate update member 'otherbool' +DatatypeUpdateResolution.dfy(20,25): Error: updated datatype members must belong to the same constructor (unlike the previously mentioned destructors, 'otherbool' does not belong to 'MyNumericConstructor') +DatatypeUpdateResolution.dfy(29,12): Error: member 'Make?' is not a destructor in datatype 'Dt' +DatatypeUpdateResolution.dfy(53,9): Error: a ghost variable is allowed only in specification contexts +DatatypeUpdateResolution.dfy(55,9): Error: a ghost variable is allowed only in specification contexts +DatatypeUpdateResolution.dfy(61,9): Error: a ghost variable is allowed only in specification contexts +DatatypeUpdateResolution.dfy(63,17): Error: a ghost variable is allowed only in specification contexts +DatatypeUpdateResolution.dfy(70,9): Error: a ghost variable is allowed only in specification contexts +DatatypeUpdateResolution.dfy(71,17): Error: a ghost variable is allowed only in specification contexts +DatatypeUpdateResolution.dfy(72,25): Error: a ghost variable is allowed only in specification contexts +12 resolution/type errors detected in DatatypeUpdateResolution.dfy diff --git a/Test/dafny0/GhostDatatypeConstructors-Resolution.dfy b/Test/dafny0/GhostDatatypeConstructors-Resolution.dfy new file mode 100644 index 00000000000..b8792e217fe --- /dev/null +++ b/Test/dafny0/GhostDatatypeConstructors-Resolution.dfy @@ -0,0 +1,372 @@ +// RUN: %dafny_0 /compile:0 "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +module Types { + datatype XY = + | {:testAttr0} D0(x: int) + | ghost {:testAttr1} G0(y: bool) + | ghost G1(y: bool, z: real, w: char) + | {:testAttr2} D1(z: real) + + datatype Wrapper = Wrapper(A) +} + +module Ghost { + import opened Types + + method M0(xy: XY) { + var x := xy.D0? && xy.x == 3; + ghost var y := xy.G0? && xy.y; + var yy; + yy := xy.G0? && xy.y; // error (x2): RHS is ghost, but LHS is not + } + + method M1(xy: XY) + requires xy.G1? + { + // Even though the verifier will forbid use of .y and .w in compiled contexts, + // the resolver allows them. + var y, z, w; + y := xy.y; // error: .y implies a ghost constructor + w := xy.w; // error: .w implies a ghost constructor + z := xy.z; + + ghost var a, b, c; + a := xy.y; + b := xy.w; + c := xy.z; + } + + method M2(ghost xy: XY) + requires xy.G1? + { + var y, z, w; + y := xy.y; // error: RHS is ghost, but LHS is not + w := xy.w; // error: RHS is ghost, but LHS is not + z := xy.z; // error: RHS is ghost, but LHS is not + + ghost var a, b, c; + a := xy.y; + b := xy.w; + c := xy.z; + } +} + +module {:options "/functionSyntax:4"} Match { + import opened Types + + method M0(xy: XY) returns (r: int) { + match xy + case any => r := 0; + } + + method M1(xy: XY) returns (r: int) { + match xy + case any => + } + + method M2(w: Wrapper) returns (r: int) { + match w + case Wrapper(any) => r := 0; + } + + method M3(w: Wrapper) returns (r: int) { + match w + case Wrapper(_) => r := 0; + } + + method M4(w: Wrapper) returns (r: int) { + match w + case _ => r := 0; + } + + method P0(xy: XY) returns (r: int) { + // the following match statement is ghost, because it indirectly mentions a ghost constructor of type XY + match xy + case D0(_) => r := 0; // error: assignment to r in a ghost context + case any => + } + + method P1(xy: XY) returns (r: int) { + // the following match statement is ghost, because it indirectly mentions a ghost constructor of type XY + match xy + case D0(_) => + case any => + } + + method P2(w: Wrapper) returns (r: int) { + match w + case Wrapper(_) => r := 0; + } + + method P3(w: Wrapper) returns (r: int) { + // the following match statement is ghost, because it mentions a constructor of type XY + match w + case Wrapper(D0(_)) => + case Wrapper(_) => r := 0; // error: assignment to r in a ghost context + } + + function F0(xy: XY): int { + match xy + case any => 0 + } + + ghost function F1(xy: XY): int { + match xy + case any => 0 + } + + function F2(w: Wrapper): int { + match w + case Wrapper(any) => 0 + } + + function F3(w: Wrapper): int { + match w + case Wrapper(_) => 0 + } + + function F4(w: Wrapper): int { + match w + case _ => 0 + } + + function G0(xy: XY): int { + match xy + case D0(_) => 0 + case _ => 0 // error: this case depends on a ghost constructor + } + + ghost function G1(xy: XY): int { + // in a ghost context, this match expression is allowed + match xy + case D0(_) => 0 + case _ => 0 + } + + function G2(w: Wrapper): int { + match w + case Wrapper(_) => 0 + } + + function G3(w: Wrapper): int { + match w + case Wrapper(D0(_)) => 0 + case Wrapper(_) => 0 // error: this case depends on a ghost constructor + } + + method H0(xy: XY) returns (r: int) { + // the following match expression is ghost, because it depends on a ghost constructor + var a := + match xy + case D0(_) => 0 + case _ => 0; + return a; // error: a is ghost + } + + ghost method H1(xy: XY) returns (r: int) { + var a := + match xy + case D0(_) => 0 + case _ => 0; + return a; + } + + method H2(w: Wrapper) returns (r: int) { + var a := + match w + case Wrapper(_) => 0; + return a; + } + + method H3(w: Wrapper) returns (r: int) { + // the following match expression is ghost, because it depends on a ghost constructor + var a := + match w + case Wrapper(D0(_)) => 0 + case Wrapper(_) => 0; + return a; // error: a is ghost + } + + method H4(xy: XY) returns (r: int) { + var a := + match xy + case _ => 0; + return a; + } +} + +module {:options "/functionSyntax:4"} EqualitySupport { + import opened Types + + method M(xy: XY) returns (a: int) { + if xy == xy { // this is okay, because the "if" statement is ghost + } + + if xy == xy { // this is fine (but the verifier would give an error) + a := 3; + } + + if Eq(xy, xy) { // error: XY does not support equality + a := 4; + } + } + + function Eq(x: T, y: T): bool { + x == y + } +} + +module {:options "/functionSyntax:4"} Constructors { + import opened Types + + method M0() returns (xy0: XY, ghost xy1: XY) { + xy0 := D0(2); + xy0 := D1(2.0); + xy0 := G0(true); // error: G0 is a ghost constructor + + xy1 := D0(2); + xy1 := D1(2.0); + xy1 := G0(true); + } + + method M1() returns (xy0: XY, ghost xy1: XY) { + var a := D0(2); + var b := D1(2.0); + var c := G0(true); // this makes c auto-ghost + + xy0 := a; + xy0 := b; + xy0 := c; // error: RHS is ghost + xy1 := a; + xy1 := b; + xy1 := c; + } + + function F(b: bool): XY { + if b then + D0(2) + else + G0(true) // error: G0 is a ghost constructor + } +} + +module StmtExpr { + import opened Types + + method CompiledMethod(xy: XY) returns (a: int) { + a := + calc { + 0; + == { // we're in a ghost context, so the following match constructs are allowed + var x; + x := match xy + case D0(_) => 0 + case _ => 0; + match xy + case D0(_) => x := 0; + case any => + } + 0; + == { if xy.G1? { } else { } } + 0; + } + 20; + } +} + +module Updates { + datatype D = + | D0(c: int, n: int) + | ghost D1(c: int, x: int) + | ghost D2(c: int, x: int, y: int) + | ghost D3(c: int, x: int, y: int) + + method Select0(d: D) returns (r: int) + { + r := d.c; // one constructor enclosing .c is non-ghost, so this is fine + r := d.n; + r := d.x; // error: RHS is ghost, LHS is not + r := d.y; // error: RHS is ghost, LHS is not + } + + method Update0(d: D) returns (r: D) + { + r := d.(c := 2); // one constructor enclosing .c is non-ghost, so this is fine + r := d.(n := 2); + r := d.(x := 2); // error: RHS is ghost, LHS is not + r := d.(y := 2); // error: RHS is ghost, LHS is not + + r := d.(c := 2, x := 2); // error: RHS is ghost, LHS is not + r := d.(c := 2, n := 2); + r := d.(x := 2, y := 2); // error: RHS is ghost, LHS is not + } + + method Select1(d: D) returns (r: int) + { + var a := d.c; + var b := d.n; + var c := d.x; + var e := d.y; + + r := a; + r := b; + r := c; // error: RHS is ghost, LHS is not + r := e; // error: RHS is ghost, LHS is not + } + + method Update1(d: D) returns (r: D) + { + var a := d.(c := 2); + var b := d.(n := 2); + var c := d.(x := 2); + var e := d.(y := 2); + + var f := d.(c := 2, x := 2); + var g := d.(c := 2, n := 2); + var h := d.(x := 2, y := 2); + + r := a; + r := b; + r := c; // error: RHS is ghost, LHS is not + r := e; // error: RHS is ghost, LHS is not + r := f; // error: RHS is ghost, LHS is not + r := g; + r := h; // error: RHS is ghost, LHS is not + } +} + +module {:options "/functionSyntax:4"} EnumTests0 { + datatype Enum = ghost EnumA | EnumB + { + predicate P() { + this != EnumA // error: ghost constructor not allowed in compiled code + } + } + + datatype TotallyGhost = ghost Ctor0 | ghost Ctor1 + { + predicate P() { + this != Ctor0 // error: ghost constructor not allowed in compiled code + } + } +} + +module {:options "/functionSyntax:4"} EnumTests1 { + datatype Enum = ghost EnumA | EnumB + { + predicate P() { + this == this // the resolver is fine with this, but the verifier will complain + } + predicate Q() { + this != EnumB // the resolver is fine with this, but the verifier will complain + } + } + + datatype TotallyGhost = ghost Ctor0 | ghost Ctor1 + { + predicate P() { + this == this // error: ghost equality not allowed in compiled code + } + } +} diff --git a/Test/dafny0/GhostDatatypeConstructors-Resolution.dfy.expect b/Test/dafny0/GhostDatatypeConstructors-Resolution.dfy.expect new file mode 100644 index 00000000000..c8e6202d288 --- /dev/null +++ b/Test/dafny0/GhostDatatypeConstructors-Resolution.dfy.expect @@ -0,0 +1,35 @@ +GhostDatatypeConstructors-Resolution.dfy(21,13): Error: a ghost discriminator is allowed only in specification contexts +GhostDatatypeConstructors-Resolution.dfy(21,23): Error: field 'y' can be used only in specification contexts +GhostDatatypeConstructors-Resolution.dfy(30,12): Error: field 'y' can be used only in specification contexts +GhostDatatypeConstructors-Resolution.dfy(31,12): Error: field 'w' can be used only in specification contexts +GhostDatatypeConstructors-Resolution.dfy(44,12): Error: field 'y' can be used only in specification contexts +GhostDatatypeConstructors-Resolution.dfy(45,12): Error: field 'w' can be used only in specification contexts +GhostDatatypeConstructors-Resolution.dfy(46,9): Error: a ghost variable is allowed only in specification contexts +GhostDatatypeConstructors-Resolution.dfy(86,20): Error: assignment to non-ghost variable is not allowed in this context, because the statement is in a ghost context; e.g., it may be guarded by a specification-only expression +GhostDatatypeConstructors-Resolution.dfy(106,25): Error: assignment to non-ghost variable is not allowed in this context, because the statement is in a ghost context; e.g., it may be guarded by a specification-only expression +GhostDatatypeConstructors-Resolution.dfy(106,25): Error: assignment to non-ghost variable is not allowed in this context, because the statement is in a ghost context; e.g., it may be guarded by a specification-only expression +GhostDatatypeConstructors-Resolution.dfy(106,25): Error: assignment to non-ghost variable is not allowed in this context, because the statement is in a ghost context; e.g., it may be guarded by a specification-only expression +GhostDatatypeConstructors-Resolution.dfy(137,4): Error: match expression is not compilable, because it depends on a ghost constructor +GhostDatatypeConstructors-Resolution.dfy(155,4): Error: match expression is not compilable, because it depends on a ghost constructor +GhostDatatypeConstructors-Resolution.dfy(164,11): Error: a ghost variable is allowed only in specification contexts +GhostDatatypeConstructors-Resolution.dfy(188,11): Error: a ghost variable is allowed only in specification contexts +GhostDatatypeConstructors-Resolution.dfy(210,7): Error: type parameter (T) passed to function Eq must support equality (got XY) +GhostDatatypeConstructors-Resolution.dfy(226,11): Error: ghost constructor is allowed only in specification contexts +GhostDatatypeConstructors-Resolution.dfy(240,11): Error: a ghost variable is allowed only in specification contexts +GhostDatatypeConstructors-Resolution.dfy(250,6): Error: ghost constructor is allowed only in specification contexts +GhostDatatypeConstructors-Resolution.dfy(289,11): Error: field 'x' can be used only in specification contexts +GhostDatatypeConstructors-Resolution.dfy(290,11): Error: field 'y' can be used only in specification contexts +GhostDatatypeConstructors-Resolution.dfy(297,11): Error: in a compiled context, update of 'x' cannot be applied to a datatype value of a ghost variant (ghost constructor 'D3', 'D2', or 'D1') +GhostDatatypeConstructors-Resolution.dfy(298,11): Error: in a compiled context, update of 'y' cannot be applied to a datatype value of a ghost variant (ghost constructor 'D3' or 'D2') +GhostDatatypeConstructors-Resolution.dfy(300,11): Error: in a compiled context, update of 'c' and 'x' cannot be applied to a datatype value of a ghost variant (ghost constructor 'D3', 'D2', or 'D1') +GhostDatatypeConstructors-Resolution.dfy(302,11): Error: in a compiled context, update of 'x' and 'y' cannot be applied to a datatype value of a ghost variant (ghost constructor 'D3' or 'D2') +GhostDatatypeConstructors-Resolution.dfy(314,9): Error: a ghost variable is allowed only in specification contexts +GhostDatatypeConstructors-Resolution.dfy(315,9): Error: a ghost variable is allowed only in specification contexts +GhostDatatypeConstructors-Resolution.dfy(331,9): Error: a ghost variable is allowed only in specification contexts +GhostDatatypeConstructors-Resolution.dfy(332,9): Error: a ghost variable is allowed only in specification contexts +GhostDatatypeConstructors-Resolution.dfy(333,9): Error: a ghost variable is allowed only in specification contexts +GhostDatatypeConstructors-Resolution.dfy(335,9): Error: a ghost variable is allowed only in specification contexts +GhostDatatypeConstructors-Resolution.dfy(343,14): Error: ghost constructor is allowed only in specification contexts +GhostDatatypeConstructors-Resolution.dfy(350,14): Error: ghost constructor is allowed only in specification contexts +GhostDatatypeConstructors-Resolution.dfy(369,6): Error: == can only be applied to expressions of types that support equality (got TotallyGhost) +34 resolution/type errors detected in GhostDatatypeConstructors-Resolution.dfy diff --git a/Test/dafny0/GhostDatatypeConstructors-Verification.dfy b/Test/dafny0/GhostDatatypeConstructors-Verification.dfy new file mode 100644 index 00000000000..7f575d4fd5a --- /dev/null +++ b/Test/dafny0/GhostDatatypeConstructors-Verification.dfy @@ -0,0 +1,201 @@ +// RUN: %dafny_0 /compile:0 "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +module Types { + datatype XY = + | D0(x: int) + | ghost G0(y: bool) + | ghost G1(y: bool, z: real, w: char) + | D1(z: real, y: bool) + + class Cl { } + + datatype G = G(Cl) +} + +module Ghost { + import opened Types + + method M0(xy0: XY, xy1: XY) returns (r: int, ghost s: int) + requires xy0.D0? || xy0.D1? + { + if xy0.D1? { + r := 3; + } + + if xy1.D1? { // fine, since this is a ghost context + s := 3; + } + + if xy1.D1? { // error: xy1 might be of a ghost variant + r := 3; + } + } + + method M1(xy: XY) + requires xy.G1? + { + var x, y, z; + if + case true => + x := xy.x; // error: xy is not a D0 + case true => + y := xy.y; // error: compiled context cannot read .y + case true => + z := xy.z; // error: compiled context cannot read .w of a G1 + } + + method M2(xy: XY) + requires xy.G1? + { + ghost var x, y, z, w; + if + case true => + x := xy.x; // error: xy is not a D0 + case true => + y := xy.y; + case true => + w := xy.w; + case true => + z := xy.z; + } + + method M3(xy: XY) + requires xy.D1? + { + ghost var x, z; + if + case true => + x := xy.x; // error: xy is not a D0 + case true => + z := xy.z; + } + + method Update0(xy: XY) returns (r: XY) + requires xy.G1? + { + if + case true => + r := xy.(x := 2); // error: xy is not a D0 + case true => + r := xy.(y := true); // error: compiled context cannot update .y + } + + method Update1(xy: XY) returns (r: XY) + requires xy.G1? + { + if + case true => + r := xy.(z := 2.2); // error: compiled context cannot update .z of a G1 + case true => + r := xy.(z := 2.2, y := true); // error: compiled context cannot update .z/.y of a G1 + } + + method Update2(xy: XY) returns (ghost r: XY) + requires xy.G1? + { + if + case true => + r := xy.(x := 2); // error: xy is not a D0 + case true => + r := xy.(y := true); + case true => + r := xy.(w := 'w'); + case true => + r := xy.(z := 2.2); + case true => + r := xy.(z := 2.2, y := true); + case true => + r := xy.(z := 2.2, w := 'w', y := true); + } +} + +module Initialization { + import opened Types + + method M0() returns (xy: XY) { // no problem not explicitly initializing xy + } + + method M1() returns (g: G) { + } // error: g requires initialization + + method M2() returns (ghost g: G) { + } // error: g requires initialization +} + +module Members { + datatype DM = ghost A(x: int) | B(x: int, y: int) | C(y: int, z: int) + { + const n := 100 + + function F(): int { + 3 + } + + method M() returns (r: int) { + r := 3; + if * { + r := r + n; // it's fine to use the field "n" + } + } + + method Bad() returns (r: int) { + if C? { // error: cannot ask about C? since ghost variant A? is a possibility + r := z; + } else { + r := x; + } + } + + method Redeemed() returns (r: int) + requires !A? + { + if C? { + r := z; + } else { + r := x; + } + } + } +} + +module {:options "/functionSyntax:4"} EqualitySupport { + import opened Types + + method M(xy: XY, selector: int) returns (a: int) + { + if xy == xy { // this is okay, because the "if" statement is ghost + } + + if xy == xy { // error: XY only partially supports equality + a := 3; + } + } + + method N(xy: XY, selector: int) returns (a: int) + requires xy.D0? || xy.D1? + { + if xy == xy { // fine + a := 3; + } + } + + datatype Enum = ghost EnumA | EnumB + { + predicate P() { + this != EnumB // error: XY only partially supports equality + } + + predicate Q() + requires EnumB? + { + this != EnumB + } + + predicate R() + requires !EnumA? + { + this != EnumB + } + } +} diff --git a/Test/dafny0/GhostDatatypeConstructors-Verification.dfy.expect b/Test/dafny0/GhostDatatypeConstructors-Verification.dfy.expect new file mode 100644 index 00000000000..a161a3ea98f --- /dev/null +++ b/Test/dafny0/GhostDatatypeConstructors-Verification.dfy.expect @@ -0,0 +1,18 @@ +GhostDatatypeConstructors-Verification.dfy(30,11): Error: in a compiled context, discriminator 'D1?' cannot be applied to a datatype value of a ghost variant (ghost constructor 'G0' or 'G1') +GhostDatatypeConstructors-Verification.dfy(41,14): Error: destructor 'x' can only be applied to datatype values constructed by 'D0' +GhostDatatypeConstructors-Verification.dfy(43,14): Error: in a compiled context, destructor 'y' cannot be applied to a datatype value of a ghost variant (ghost constructor 'G0' or 'G1') +GhostDatatypeConstructors-Verification.dfy(45,14): Error: in a compiled context, destructor 'z' cannot be applied to a datatype value of a ghost variant (ghost constructor 'G1') +GhostDatatypeConstructors-Verification.dfy(54,14): Error: destructor 'x' can only be applied to datatype values constructed by 'D0' +GhostDatatypeConstructors-Verification.dfy(69,14): Error: destructor 'x' can only be applied to datatype values constructed by 'D0' +GhostDatatypeConstructors-Verification.dfy(79,14): Error: source of datatype update must be constructed by 'D0' +GhostDatatypeConstructors-Verification.dfy(81,14): Error: in a compiled context, update of 'y' cannot be applied to a datatype value of a ghost variant (ghost constructor 'G1' or 'G0') +GhostDatatypeConstructors-Verification.dfy(89,14): Error: in a compiled context, update of 'z' cannot be applied to a datatype value of a ghost variant (ghost constructor 'G1') +GhostDatatypeConstructors-Verification.dfy(91,14): Error: in a compiled context, update of 'z' and 'y' cannot be applied to a datatype value of a ghost variant (ghost constructor 'G1') +GhostDatatypeConstructors-Verification.dfy(99,14): Error: source of datatype update must be constructed by 'D0' +GhostDatatypeConstructors-Verification.dfy(120,2): Error: out-parameter 'g', which is subject to definite-assignment rules, might be uninitialized at this return point +GhostDatatypeConstructors-Verification.dfy(123,2): Error: out-parameter 'g', which is subject to definite-assignment rules, might be uninitialized at this return point +GhostDatatypeConstructors-Verification.dfy(143,9): Error: in a compiled context, discriminator 'C?' cannot be applied to a datatype value of a ghost variant (ghost constructor 'A') +GhostDatatypeConstructors-Verification.dfy(186,11): Error: in a compiled context, equality cannot be applied to a datatype value of a ghost variant (ghost constructor 'EnumA') +GhostDatatypeConstructors-Verification.dfy(170,10): Error: in a compiled context, equality cannot be applied to a datatype value of a ghost variant (ghost constructor 'G0' or 'G1') + +Dafny program verifier finished with 4 verified, 16 errors