From 162a95e3ced78fc7d1e577b517d28faecc1bac6b Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Wed, 19 Apr 2023 18:04:22 -0700 Subject: [PATCH 01/12] Add test cases --- Test/git-issues/git-issue-3883.dfy | 54 +++++++++++++++++++++++ Test/git-issues/git-issue-3883.dfy.expect | 6 +++ 2 files changed, 60 insertions(+) create mode 100644 Test/git-issues/git-issue-3883.dfy create mode 100644 Test/git-issues/git-issue-3883.dfy.expect diff --git a/Test/git-issues/git-issue-3883.dfy b/Test/git-issues/git-issue-3883.dfy new file mode 100644 index 00000000000..f30a1a4838d --- /dev/null +++ b/Test/git-issues/git-issue-3883.dfy @@ -0,0 +1,54 @@ +// RUN: %testDafnyForEachCompiler "%s" + +type MyType = x: T | true witness * +type MyInt = x: int | true witness * + +method Main() { + var a: MyType := 13; // NOTE: this used to not verify + TestMyTest(a, 14); // 13 14 // NOTE: this used to crash the resolved + var b: MyType := true; + TestMyTest(b, false); // true false + print a, " ", b, "\n"; // 13 true + + var c: MyInt := 18; + var d: MyInt := 19; + print c, " ", d, "\n"; // 18 19 + + TestOthers(); + + DoIt(); +} + +method TestMyTest(m: MyType, u: U) { + var w: U := u; + var n: MyType := m; + w := m; + n := u; + print m, " ", u, "\n"; +} + +datatype ABC = MakeABC(X) +datatype XYZ = MakeXYZ(A) +type SSS = s: seq | |s| <= 10 + +method TestOthers() { + var a := MakeABC(10); + var b := MakeXYZ(null); + var c: SSS := [false, true, false]; + print a, " ", b, " ", c, "\n"; // 10 null [false, true, false] +} + +type ST0 = x: int | x % 5 == 0 +type ST1 = x: int | (if var m: map := map[]; m == map[] then 0 else 8) <= x + +method DoIt() { + var t0: ST0; + var t1: ST1; + Print(t0, " "); // 0-0 + Print(t1, "\n"); // 0-0 +} + +method Print(x: X, suffix: string) { + var y: X; + print x, "-", y, suffix; +} diff --git a/Test/git-issues/git-issue-3883.dfy.expect b/Test/git-issues/git-issue-3883.dfy.expect new file mode 100644 index 00000000000..0413bc9c8b9 --- /dev/null +++ b/Test/git-issues/git-issue-3883.dfy.expect @@ -0,0 +1,6 @@ +13 14 +true false +13 true +18 19 +10 null [false, true, false] +0-0 0-0 From d2dca994e2827887018d7b80c7359784d2b042e9 Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Wed, 19 Apr 2023 18:06:03 -0700 Subject: [PATCH 02/12] fix: Improve Subrange verification to reduce a completeness issue Fixes #3891 --- Source/DafnyCore/Verifier/Translator.cs | 11 ++++++++--- 1 file changed, 8 insertions(+), 3 deletions(-) diff --git a/Source/DafnyCore/Verifier/Translator.cs b/Source/DafnyCore/Verifier/Translator.cs index b535d475124..9bf9c11c8e9 100644 --- a/Source/DafnyCore/Verifier/Translator.cs +++ b/Source/DafnyCore/Verifier/Translator.cs @@ -7108,7 +7108,7 @@ class BoilerplateTriple { // a triple that is now a quintuple } } - public Bpl.Expr CondApplyBox(IToken tok, Bpl.Expr e, Type fromType, Type toType) { + public Bpl.Expr CondApplyBox(Bpl.IToken tok, Bpl.Expr e, Type fromType, Type toType) { Contract.Requires(tok != null); Contract.Requires(e != null); Contract.Requires(fromType != null); @@ -7136,7 +7136,7 @@ class BoilerplateTriple { // a triple that is now a quintuple } } - public Bpl.Expr BoxIfNecessary(IToken tok, Bpl.Expr e, Type fromType) { + public Bpl.Expr BoxIfNecessary(Bpl.IToken tok, Bpl.Expr e, Type fromType) { Contract.Requires(tok != null); Contract.Requires(e != null); Contract.Requires(fromType != null); @@ -9051,8 +9051,13 @@ public ForceCheckToken(IToken tok) return null; } targetType = targetType.NormalizeExpandKeepConstraints(); - var cre = MkIs(bSource, targetType); var udt = targetType as UserDefinedType; + Bpl.Expr cre; + if (udt?.ResolvedClass is RedirectingTypeDecl redirectingTypeDecl && ModeledAsBoxType(redirectingTypeDecl.Var.Type)) { + cre = MkIs(BoxIfNecessary(bSource.tok, bSource, sourceType), TypeToTy(targetType), true); + } else { + cre = MkIs(bSource, targetType); + } if (udt != null && udt.IsRefType) { var s = sourceType.NormalizeExpandKeepConstraints(); var certain = false; From 1035bedbcdb01eda2657af7c66451d671b3fc30d Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Wed, 19 Apr 2023 18:06:18 -0700 Subject: [PATCH 03/12] fix: Crash in resolver --- Source/DafnyCore/Resolver/NameResolutionAndTypeInference.cs | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/Source/DafnyCore/Resolver/NameResolutionAndTypeInference.cs b/Source/DafnyCore/Resolver/NameResolutionAndTypeInference.cs index 6978dcc4348..79b68e3ae4b 100644 --- a/Source/DafnyCore/Resolver/NameResolutionAndTypeInference.cs +++ b/Source/DafnyCore/Resolver/NameResolutionAndTypeInference.cs @@ -1633,7 +1633,11 @@ public partial class Resolver { case TypeProxy.Family.Ordinal: case TypeProxy.Family.BitVector: if (super.Equals(sub)) { - return new List(); + if (sub is UserDefinedType subUserDefinedType) { + return subUserDefinedType.ResolvedClass.TypeArgs.ConvertAll(tp => TypeParameter.Direction(tp.Variance)); + } else { + return new List(); + } } else { return null; } From 4bd98036cd8deb7e37ca5ffcb6fbdc262881923a Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Thu, 20 Apr 2023 18:44:01 -0700 Subject: [PATCH 04/12] fix: For Java Fixes #3883 --- .../DafnyCore/Compilers/Java/Compiler-java.cs | 45 +++++++++++++------ .../src/main/java/dafny/TypeDescriptor.java | 5 +++ 2 files changed, 37 insertions(+), 13 deletions(-) diff --git a/Source/DafnyCore/Compilers/Java/Compiler-java.cs b/Source/DafnyCore/Compilers/Java/Compiler-java.cs index e9928214117..1624b32ba51 100644 --- a/Source/DafnyCore/Compilers/Java/Compiler-java.cs +++ b/Source/DafnyCore/Compilers/Java/Compiler-java.cs @@ -931,8 +931,7 @@ protected class ClassWriter : IClassWriter { // make sure the (static fields associated with the) type method come after the Witness static field var wTypeMethod = wBody; var wRestOfBody = wBody.Fork(); - var targetTypeName = BoxedTypeName(UserDefinedType.FromTopLevelDecl(cls.tok, cls, null), wTypeMethod, cls.tok); - EmitTypeMethod(cls, javaName, typeParameters, typeParameters, targetTypeName, null, wTypeMethod); + EmitTypeDescriptorMethod(cls, typeParameters, null, null, wTypeMethod); if (fullPrintName != null) { // By emitting a toString() method, printing an object will give the same output as with other target languages. @@ -951,14 +950,24 @@ protected class ClassWriter : IClassWriter { /// /// Generate the "_typeDescriptor" method for a generated class. /// "enclosingType" is allowed to be "null", in which case the target values are assumed to be references. + /// If "enclosingType" is null, then "targetTypeName" is expected to be the name of the Java type representing the type. + /// If "enclosingType" is non-null, then "targetTypeName" is expected to be null. /// - private void EmitTypeMethod(TopLevelDecl/*?*/ enclosingTypeDecl, string typeName, List typeParams, List usedTypeParams, string targetTypeName, string/*?*/ initializer, ConcreteSyntaxTree wr) { - string typeDescriptorExpr = null; + private void EmitTypeDescriptorMethod([CanBeNull] TopLevelDecl enclosingTypeDecl, List typeParams, string targetTypeName, + [CanBeNull] string initializer, ConcreteSyntaxTree wr) { + Contract.Requires((enclosingTypeDecl != null) != (targetTypeName != null)); + + string typeDescriptorExpr; if (enclosingTypeDecl == null) { + Contract.Assert(targetTypeName != null); // use reference type typeDescriptorExpr = $"{DafnyTypeDescriptor}.referenceWithInitializer({StripTypeParameters(targetTypeName)}.class, () -> {initializer ?? "null"})"; } else { - var targetType = DatatypeWrapperEraser.SimplifyType(Options, UserDefinedType.FromTopLevelDecl(enclosingTypeDecl.tok, enclosingTypeDecl), true); + Contract.Assert(targetTypeName == null); + var enclosingTypeWithItsOwnTypeArguments = UserDefinedType.FromTopLevelDecl(enclosingTypeDecl.tok, enclosingTypeDecl); + var targetType = DatatypeWrapperEraser.SimplifyType(Options, enclosingTypeWithItsOwnTypeArguments, true); + var targetTypeIgnoringConstraints = DatatypeWrapperEraser.SimplifyType(Options, enclosingTypeWithItsOwnTypeArguments, false); + targetTypeName = BoxedTypeName(targetTypeIgnoringConstraints, wr, enclosingTypeDecl.tok); var w = (enclosingTypeDecl as RedirectingTypeDecl)?.Witness != null ? "Witness" : null; switch (AsJavaNativeType(targetType)) { case JavaNativeType.Byte: @@ -982,13 +991,24 @@ protected class ClassWriter : IClassWriter { } else { typeDescriptorExpr = $"{DafnyTypeDescriptor}.charWithDefault({w ?? CharType.DefaultValueAsString})"; } - } else if (targetType.IsTypeParameter) { - typeDescriptorExpr = TypeDescriptor(targetType, wr, enclosingTypeDecl.tok); } else { - var d = initializer ?? DefaultValue(targetType, wr, enclosingTypeDecl.tok); - typeDescriptorExpr = $"{DafnyTypeDescriptor}.referenceWithInitializer({StripTypeParameters(targetTypeName)}.class, () -> {d})"; + var d = initializer ?? DefaultValue(targetType, wr, enclosingTypeDecl.tok, true); + // We'd like to say, essentially, targetTypeName.class. But this is not legal Java if targetTypeName is a type parameter. + // So, we detect that case here and use the corresponding type descriptor instead (because method + // referenceWithInitializerAndTypeDescriptor will use the .boxedClass of that type descriptor, which gives the Class object + // we're looking for). + var tp = targetTypeIgnoringConstraints.AsTypeParameter; + if (tp == null) { + typeDescriptorExpr = $"{DafnyTypeDescriptor}.referenceWithInitializer({StripTypeParameters(targetTypeName)}.class, () -> {d})"; + } else { + var td = FormatTypeDescriptorVariable(tp.GetCompileName(Options)); + typeDescriptorExpr = $"{DafnyTypeDescriptor}.referenceWithInitializerAndTypeDescriptor({td}, () -> {d})"; + } } break; + default: + Contract.Assert(false); // unexpected case + throw new cce.UnreachableException(); } } @@ -1832,9 +1852,8 @@ protected class ClassWriter : IClassWriter { dt is CoDatatypeDecl, args, wDefault); } - var targetTypeName = BoxedTypeName(UserDefinedType.FromTopLevelDecl(dt.tok, dt, null), wr, dt.tok); var arguments = usedTypeArgs.Comma(tp => DefaultValue(new UserDefinedType(tp), wDefault, dt.tok, true)); - EmitTypeMethod(dt, IdName(dt), dt.TypeArgs, usedTypeArgs, targetTypeName, $"Default({arguments})", wr); + EmitTypeDescriptorMethod(dt, dt.TypeArgs, null, $"Default({arguments})", wr); // create methods foreach (var ctor in dt.Ctors.Where(ctor => !ctor.IsGhost)) { @@ -2936,7 +2955,7 @@ protected class ClassWriter : IClassWriter { } var typeParamString = TypeParameters(typeParams); var initializer = string.Format("Default({0})", Util.Comma(i, j => $"_td_T{j}.defaultValue()")); - EmitTypeMethod(null, $"Tuple{i}", typeParams, typeParams, $"Tuple{i}{typeParamString}", initializer, wr); + EmitTypeDescriptorMethod(null, typeParams, $"Tuple{i}{typeParamString}", initializer, wr); // public static Tuple4 Default(dafny.TypeDescriptor _td_T0, dafny.TypeDescriptor _td_T1, dafny.TypeDescriptor _td_T2, dafny.TypeDescriptor _td_T3) { // return new Tuple4<>(_td_T0.defaultValue(), _td_T1.defaultValue(), _td_T2.defaultValue(), _td_T3.defaultValue()); @@ -3180,7 +3199,7 @@ protected class ClassWriter : IClassWriter { var staticMemberWriter = w.NewBlock(""); var ctorBodyWriter = staticMemberWriter.NewBlock($"public _Companion_{name}()"); - EmitTypeMethod(null, name, typeParameters, typeParameters, name + typeParamString, initializer: null, staticMemberWriter); + EmitTypeDescriptorMethod(null, typeParameters, name + typeParamString, initializer: null, wr: staticMemberWriter); return new ClassWriter(this, instanceMemberWriter, ctorBodyWriter, staticMemberWriter); } diff --git a/Source/DafnyRuntime/DafnyRuntimeJava/src/main/java/dafny/TypeDescriptor.java b/Source/DafnyRuntime/DafnyRuntimeJava/src/main/java/dafny/TypeDescriptor.java index 52a6d299049..441272ae4cd 100644 --- a/Source/DafnyRuntime/DafnyRuntimeJava/src/main/java/dafny/TypeDescriptor.java +++ b/Source/DafnyRuntime/DafnyRuntimeJava/src/main/java/dafny/TypeDescriptor.java @@ -98,6 +98,11 @@ public static TypeDescriptor referenceWithInitializer( return new ReferenceType(javaClass, initializer); } + public static TypeDescriptor referenceWithInitializerAndTypeDescriptor( + TypeDescriptor typeDescriptor, Initializer initializer) { + return new ReferenceType(typeDescriptor.boxedClass, initializer); + } + public static TypeDescriptor byteWithDefault(byte d) { return new ByteType(d); } From 079dde223f66fbfcf63bafaaf4455b697956f2cc Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Fri, 21 Apr 2023 11:17:58 -0700 Subject: [PATCH 05/12] fix: For C# --- .../DafnyCore/Compilers/CSharp/Compiler-Csharp.cs | 13 +++---------- 1 file changed, 3 insertions(+), 10 deletions(-) diff --git a/Source/DafnyCore/Compilers/CSharp/Compiler-Csharp.cs b/Source/DafnyCore/Compilers/CSharp/Compiler-Csharp.cs index 623bdb932cb..c5f0627b032 100644 --- a/Source/DafnyCore/Compilers/CSharp/Compiler-Csharp.cs +++ b/Source/DafnyCore/Compilers/CSharp/Compiler-Csharp.cs @@ -310,7 +310,7 @@ public class CsharpCompiler : SinglePassCompiler { if (enclosingTypeDecl is DatatypeDecl dtDecl) { typeDescriptorParams = UsedTypeParameters(dtDecl); } else { - typeDescriptorParams = enclosingTypeDecl.TypeArgs.Where(NeedsTypeDescriptor).ToList(); + typeDescriptorParams = enclosingTypeDecl.TypeArgs; } var parameters = typeDescriptorParams.Comma(tp => $"{DafnyTypeDescriptor}<{tp.GetCompileName(Options)}> {FormatTypeDescriptorVariable(tp.GetCompileName(Options))}"); @@ -1656,17 +1656,10 @@ protected class ClassWriter : IClassWriter { } List relevantTypeArgs; - if (type.IsBuiltinArrowType) { - relevantTypeArgs = type.TypeArgs; - } else if (cl is DatatypeDecl dt) { + if (cl is DatatypeDecl dt) { relevantTypeArgs = UsedTypeParameters(dt, udt.TypeArgs).ConvertAll(ta => ta.Actual); } else { - relevantTypeArgs = new List(); - for (int i = 0; i < cl.TypeArgs.Count; i++) { - if (NeedsTypeDescriptor(cl.TypeArgs[i])) { - relevantTypeArgs.Add(udt.TypeArgs[i]); - } - } + relevantTypeArgs = type.TypeArgs; } return AddTypeDescriptorArgs(FullTypeName(udt, ignoreInterface: true), udt, relevantTypeArgs, wr, tok); From 34a2db0fa837fc5e31348f6a530e489f5e80edfc Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Fri, 21 Apr 2023 11:18:25 -0700 Subject: [PATCH 06/12] fix: For Go --- .../DafnyCore/Compilers/GoLang/Compiler-go.cs | 39 ++++++++++++------- 1 file changed, 26 insertions(+), 13 deletions(-) diff --git a/Source/DafnyCore/Compilers/GoLang/Compiler-go.cs b/Source/DafnyCore/Compilers/GoLang/Compiler-go.cs index 94a37929256..b33c07d1f68 100644 --- a/Source/DafnyCore/Compilers/GoLang/Compiler-go.cs +++ b/Source/DafnyCore/Compilers/GoLang/Compiler-go.cs @@ -964,7 +964,7 @@ private struct Import { } // RTD { - CreateRTD(IdName(sst), null, out var wDefaultBody, wr); + CreateRTD(IdName(sst), sst.TypeArgs, out var wDefaultBody, wr); var udt = UserDefinedType.FromTopLevelDecl(sst.tok, sst); var d = TypeInitializationValue(udt, wr, sst.tok, false, true); wDefaultBody.WriteLine("return {0}", d); @@ -1325,7 +1325,15 @@ protected class ClassWriter : IClassWriter { } else if (xType.IsTypeParameter) { var tp = type.AsTypeParameter; Contract.Assert(tp != null); - return string.Format("{0}{1}", thisContext != null && tp.Parent is ClassDecl && !(tp.Parent is TraitDecl) ? "_this." : "", FormatRTDName(tp.GetCompileName(Options))); + string th; + if (thisContext != null && tp.Parent is ClassDecl and not TraitDecl) { + th = "_this."; + } else if (thisContext == null && tp.Parent is SubsetTypeDecl) { + th = "_this."; + } else { + th = ""; + } + return string.Format("{0}{1}", th, FormatRTDName(tp.GetCompileName(Options))); } else if (xType.IsBuiltinArrowType) { return string.Format("_dafny.CreateStandardTypeDescriptor({0})", TypeInitializationValue(xType, wr, tok, false, true)); } else if (xType is UserDefinedType udt) { @@ -1334,20 +1342,21 @@ protected class ClassWriter : IClassWriter { bool isHandle = true; if (Attributes.ContainsBool(cl.Attributes, "handle", ref isHandle) && isHandle) { return "_dafny.Int64Type"; - } else if (cl is ClassDecl || cl is DatatypeDecl) { - var w = new ConcreteSyntaxTree(); - w.Write("{0}(", cl is TupleTypeDecl ? "_dafny.TupleType" : TypeName_RTD(xType, w, tok)); - var typeArgs = cl is DatatypeDecl dt ? UsedTypeParameters(dt, udt.TypeArgs) : TypeArgumentInstantiation.ListFromClass(cl, udt.TypeArgs); - EmitTypeDescriptorsActuals(typeArgs, udt.tok, w, true); - w.Write(")"); - return w.ToString(); - } else if (xType.IsNonNullRefType) { + } + + if (xType.IsNonNullRefType) { + Contract.Assert(false); // KRML: do we ever get here? // what we emit here will only be used to construct a dummy value that programmer-supplied code will overwrite later return "_dafny.PossiblyNullType/*not used*/"; - } else { - Contract.Assert(cl is NewtypeDecl || cl is SubsetTypeDecl); - return TypeName_RTD(xType, wr, udt.tok) + "()"; } + + var w = new ConcreteSyntaxTree(); + w.Write("{0}(", cl is TupleTypeDecl ? "_dafny.TupleType" : TypeName_RTD(xType, w, tok)); + var typeArgs = cl is DatatypeDecl dt ? UsedTypeParameters(dt, udt.TypeArgs) : TypeArgumentInstantiation.ListFromClass(cl, udt.TypeArgs); + EmitTypeDescriptorsActuals(typeArgs, udt.tok, w, true); + w.Write(")"); + return w.ToString(); + } else { Contract.Assert(false); throw new cce.UnreachableException(); // unexpected type } @@ -1555,6 +1564,10 @@ protected class ClassWriter : IClassWriter { } } else if (cl is DatatypeDecl) { var dt = (DatatypeDecl)cl; + if (DatatypeWrapperEraser.GetInnerTypeOfErasableDatatypeWrapper(Options, dt, out var innerType)) { + var typeSubstMap = TypeParameter.SubstitutionMap(dt.TypeArgs, udt.TypeArgs); + return TypeInitializationValue(innerType.Subst(typeSubstMap), wr, tok, usePlaceboValue, constructTypeParameterDefaultsFromTypeDescriptors); + } // In an auto-init context (like a field initializer), we may not have // access to all the type descriptors, so we can't construct the // default value, but then an empty structure is an acceptable default, since From 59e1a3221cd650085da0f9ab778bc0e691a02041 Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Fri, 21 Apr 2023 11:18:43 -0700 Subject: [PATCH 07/12] fix: Add cast required by Java for functions Fixes #3892 --- Source/DafnyCore/Compilers/Java/Compiler-java.cs | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/Source/DafnyCore/Compilers/Java/Compiler-java.cs b/Source/DafnyCore/Compilers/Java/Compiler-java.cs index 1624b32ba51..57d5bd16c0a 100644 --- a/Source/DafnyCore/Compilers/Java/Compiler-java.cs +++ b/Source/DafnyCore/Compilers/Java/Compiler-java.cs @@ -999,7 +999,7 @@ protected class ClassWriter : IClassWriter { // we're looking for). var tp = targetTypeIgnoringConstraints.AsTypeParameter; if (tp == null) { - typeDescriptorExpr = $"{DafnyTypeDescriptor}.referenceWithInitializer({StripTypeParameters(targetTypeName)}.class, () -> {d})"; + typeDescriptorExpr = $"{DafnyTypeDescriptor}.referenceWithInitializer({StripTypeParameters(targetTypeName)}.class, () -> ({targetTypeName}){d})"; } else { var td = FormatTypeDescriptorVariable(tp.GetCompileName(Options)); typeDescriptorExpr = $"{DafnyTypeDescriptor}.referenceWithInitializerAndTypeDescriptor({td}, () -> {d})"; @@ -3128,6 +3128,10 @@ protected class ClassWriter : IClassWriter { return $"({BoxedTypeName(xType, wr, udt.tok)}) null"; } } else if (cl is DatatypeDecl dt) { + if (DatatypeWrapperEraser.GetInnerTypeOfErasableDatatypeWrapper(Options, dt, out var innerType)) { + var typeSubstMap = TypeParameter.SubstitutionMap(dt.TypeArgs, udt.TypeArgs); + return TypeInitializationValue(innerType.Subst(typeSubstMap), wr, tok, usePlaceboValue, constructTypeParameterDefaultsFromTypeDescriptors); + } var s = FullTypeName(udt); var typeargs = ""; var nonGhostTypeArgs = SelectNonGhost(cl, udt.TypeArgs); From 0b6ecd4664caf3f2eedd2dd3061855f1b4d678fb Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Fri, 21 Apr 2023 11:18:52 -0700 Subject: [PATCH 08/12] Add tests --- Test/git-issues/git-issue-3883.dfy | 44 +++++++++++++++++++++-- Test/git-issues/git-issue-3883.dfy.expect | 2 +- 2 files changed, 43 insertions(+), 3 deletions(-) diff --git a/Test/git-issues/git-issue-3883.dfy b/Test/git-issues/git-issue-3883.dfy index f30a1a4838d..ea36ad12489 100644 --- a/Test/git-issues/git-issue-3883.dfy +++ b/Test/git-issues/git-issue-3883.dfy @@ -17,6 +17,10 @@ method Main() { TestOthers(); DoIt(); + + Arrows(); + + MoreTests.Placebo(); } method TestMyTest(m: MyType, u: U) { @@ -38,13 +42,13 @@ method TestOthers() { print a, " ", b, " ", c, "\n"; // 10 null [false, true, false] } -type ST0 = x: int | x % 5 == 0 +type ST0 = x: int | x % 5 == 1 witness 16 type ST1 = x: int | (if var m: map := map[]; m == map[] then 0 else 8) <= x method DoIt() { var t0: ST0; var t1: ST1; - Print(t0, " "); // 0-0 + Print(t0, " "); // 16-16 Print(t1, "\n"); // 0-0 } @@ -52,3 +56,39 @@ method Print(x: X, suffix: string) { var y: X; print x, "-", y, suffix; } + +type pos = x | 1 <= x witness 9 +type Fn = f: int -> R | true witness * + +method Arrows() { + var f: Fn; + var g: Fn; +} + +module MoreTests { + datatype BSingle = BPlop(bool) + type BMyTypeWrapper = x: BSingle | true witness * + datatype BD = BD(BMyTypeWrapper) + + datatype XSingle = XPlop(X) + type XMyTypeWrapper = x: XSingle | true witness * + datatype XD = XD(XMyTypeWrapper) + + datatype IntCell = IntCell(int) + type ConstrainedIntCell = c: IntCell | true witness * + type GurgleInt = ConstrainedIntCell + datatype WrappedInt = WrappedInt(GurgleInt) + type MyTypeAroundInt = x: WrappedInt | true witness * + + datatype UCell = UCell(U) + type ConstrainedUCell = u: UCell | true witness * + type GurgleU = ConstrainedUCell + datatype WrappedU = WrappedU(GurgleU) + type MyTypeAroundU = x: WrappedU | true witness * + + method Placebo() { + var a: XSingle; + var b: XMyTypeWrapper; + var c: XD; + } +} diff --git a/Test/git-issues/git-issue-3883.dfy.expect b/Test/git-issues/git-issue-3883.dfy.expect index 0413bc9c8b9..0de72addffe 100644 --- a/Test/git-issues/git-issue-3883.dfy.expect +++ b/Test/git-issues/git-issue-3883.dfy.expect @@ -3,4 +3,4 @@ true false 13 true 18 19 10 null [false, true, false] -0-0 0-0 +16-16 0-0 From 8973cd7855d52ce961f3130594683d8a39803017 Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Fri, 21 Apr 2023 14:30:58 -0700 Subject: [PATCH 09/12] Remove apparently unreachable code --- Source/DafnyCore/Compilers/GoLang/Compiler-go.cs | 6 ------ 1 file changed, 6 deletions(-) diff --git a/Source/DafnyCore/Compilers/GoLang/Compiler-go.cs b/Source/DafnyCore/Compilers/GoLang/Compiler-go.cs index b33c07d1f68..fdbf2d58294 100644 --- a/Source/DafnyCore/Compilers/GoLang/Compiler-go.cs +++ b/Source/DafnyCore/Compilers/GoLang/Compiler-go.cs @@ -1344,12 +1344,6 @@ protected class ClassWriter : IClassWriter { return "_dafny.Int64Type"; } - if (xType.IsNonNullRefType) { - Contract.Assert(false); // KRML: do we ever get here? - // what we emit here will only be used to construct a dummy value that programmer-supplied code will overwrite later - return "_dafny.PossiblyNullType/*not used*/"; - } - var w = new ConcreteSyntaxTree(); w.Write("{0}(", cl is TupleTypeDecl ? "_dafny.TupleType" : TypeName_RTD(xType, w, tok)); var typeArgs = cl is DatatypeDecl dt ? UsedTypeParameters(dt, udt.TypeArgs) : TypeArgumentInstantiation.ListFromClass(cl, udt.TypeArgs); From f65ec61bbf61c6b6c293aa6b0460d397ffdbb06d Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Fri, 21 Apr 2023 14:59:22 -0700 Subject: [PATCH 10/12] Update tests --- Test/git-issues/git-issue-3883.dfy | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/Test/git-issues/git-issue-3883.dfy b/Test/git-issues/git-issue-3883.dfy index ea36ad12489..78bf7e7ee5b 100644 --- a/Test/git-issues/git-issue-3883.dfy +++ b/Test/git-issues/git-issue-3883.dfy @@ -1,11 +1,11 @@ // RUN: %testDafnyForEachCompiler "%s" -type MyType = x: T | true witness * +type MyType = x: T | true witness * // this used to not compile (C#, Java, Go) -- issue #3883 type MyInt = x: int | true witness * method Main() { - var a: MyType := 13; // NOTE: this used to not verify - TestMyTest(a, 14); // 13 14 // NOTE: this used to crash the resolved + var a: MyType := 13; // this used to not verify (issue #3891) + TestMyTest(a, 14); // 13 14 // this used to crash the resolved var b: MyType := true; TestMyTest(b, false); // true false print a, " ", b, "\n"; // 13 true @@ -58,7 +58,7 @@ method Print(x: X, suffix: string) { } type pos = x | 1 <= x witness 9 -type Fn = f: int -> R | true witness * +type Fn = f: int -> R | true witness * // this used to generate malformed Java code (issue #3892) method Arrows() { var f: Fn; From aa15dc9f6259823fa6d5cf27cb81a45b416d0c1e Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Fri, 21 Apr 2023 15:02:43 -0700 Subject: [PATCH 11/12] Add release notes --- docs/dev/news/3893.fix | 1 + 1 file changed, 1 insertion(+) create mode 100644 docs/dev/news/3893.fix diff --git a/docs/dev/news/3893.fix b/docs/dev/news/3893.fix new file mode 100644 index 00000000000..1cf3cb5963b --- /dev/null +++ b/docs/dev/news/3893.fix @@ -0,0 +1 @@ +Fixes several compilation issues, mostly related to subset types defined by one of its type parameter From dc7fb514c7aefbb57761558b216096ff00bdd777 Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Fri, 21 Apr 2023 17:27:23 -0700 Subject: [PATCH 12/12] Update 3892-fix to cover additional bugs --- .../DafnyCore/Compilers/Java/Compiler-java.cs | 21 +++++++++++++------ Test/git-issues/git-issue-3883.dfy | 11 ++++++++++ 2 files changed, 26 insertions(+), 6 deletions(-) diff --git a/Source/DafnyCore/Compilers/Java/Compiler-java.cs b/Source/DafnyCore/Compilers/Java/Compiler-java.cs index 57d5bd16c0a..0bd83cd33bf 100644 --- a/Source/DafnyCore/Compilers/Java/Compiler-java.cs +++ b/Source/DafnyCore/Compilers/Java/Compiler-java.cs @@ -399,7 +399,11 @@ private enum JavaNativeType { Byte, Short, Int, Long } cw.DeclareField("Witness", sst, true, true, sst.Rhs, sst.tok, witness, null); witness = "Witness"; } - var w = cw.StaticMemberWriter.NewBlock($"public static {TypeParameters(sst.TypeArgs, " ")}{typeName} defaultValue()"); + cw.StaticMemberWriter.Write($"public static {TypeParameters(sst.TypeArgs, " ")}{typeName} defaultValue("); + var typeDescriptorParams = sst.TypeArgs.Where(NeedsTypeDescriptor); + cw.StaticMemberWriter.Write(typeDescriptorParams.Comma(tp => + $"{DafnyTypeDescriptor}<{tp.GetCompileName(Options)}> {FormatTypeDescriptorVariable(tp.GetCompileName(Options))}")); + var w = cw.StaticMemberWriter.NewBlock(")"); w.WriteLine($"return {witness};"); } } @@ -1018,10 +1022,8 @@ protected class ClassWriter : IClassWriter { typeDescriptorExpr = "_TYPE"; } wr.Write($"public static {TypeParameters(typeParams, " ")}{DafnyTypeDescriptor}<{targetTypeName}> {TypeMethodName}("); - if (typeParams.Count != 0) { - var typeDescriptorParams = typeParams.Where(tp => NeedsTypeDescriptor(tp)).ToList(); - wr.Write(typeDescriptorParams.Comma(tp => $"{DafnyTypeDescriptor}<{tp.GetCompileName(Options)}> {FormatTypeDescriptorVariable(tp.GetCompileName(Options))}")); - } + var typeDescriptorParams = typeParams.Where(NeedsTypeDescriptor); + wr.Write(typeDescriptorParams.Comma(tp => $"{DafnyTypeDescriptor}<{tp.GetCompileName(Options)}> {FormatTypeDescriptorVariable(tp.GetCompileName(Options))}")); var wTypeMethodBody = wr.NewBlock(")", ""); var typeDescriptorCast = $"({DafnyTypeDescriptor}<{targetTypeName}>) ({DafnyTypeDescriptor})"; wTypeMethodBody.WriteLine($"return {typeDescriptorCast} {typeDescriptorExpr};"); @@ -3085,7 +3087,14 @@ protected class ClassWriter : IClassWriter { } else if (cl is SubsetTypeDecl) { var td = (SubsetTypeDecl)cl; if (td.WitnessKind == SubsetTypeDecl.WKind.Compiled) { - return FullTypeName(udt) + ".defaultValue()"; + var relevantTypeArgs = new List(); + for (int i = 0; i < td.TypeArgs.Count; i++) { + if (NeedsTypeDescriptor(td.TypeArgs[i])) { + relevantTypeArgs.Add(udt.TypeArgs[i]); + } + } + string typeParameters = Util.Comma(relevantTypeArgs, arg => TypeDescriptor(arg, wr, tok)); + return $"{FullTypeName(udt)}.defaultValue({typeParameters})"; } else if (td.WitnessKind == SubsetTypeDecl.WKind.Special) { // WKind.Special is only used with -->, ->, and non-null types: Contract.Assert(ArrowType.IsPartialArrowTypeName(td.Name) || ArrowType.IsTotalArrowTypeName(td.Name) || td is NonNullTypeDecl); diff --git a/Test/git-issues/git-issue-3883.dfy b/Test/git-issues/git-issue-3883.dfy index 78bf7e7ee5b..aaed6ae9512 100644 --- a/Test/git-issues/git-issue-3883.dfy +++ b/Test/git-issues/git-issue-3883.dfy @@ -60,9 +60,20 @@ method Print(x: X, suffix: string) { type pos = x | 1 <= x witness 9 type Fn = f: int -> R | true witness * // this used to generate malformed Java code (issue #3892) +datatype Option = Some(t: T) | None +type Fn0 = f: int -> Option | true witness PartialFnWitness // this used to generate malformed Java code (issue #3892) +type Fn1 = f: int -> Option | true witness PartialFnWitness // this used to generate malformed Java code (issue #3892) + +function PartialFnWitness(x: int): Option { + None +} + method Arrows() { var f: Fn; var g: Fn; + + var h: Fn0; + var k: Fn1; } module MoreTests {