Skip to content

Commit 4cbef94

Browse files
fabiomadgefabiomadge
authored
fix: Change datatype deconstruction in match statements for C# (#1818)
Fixes #1815 by replacing a manual datatype deconstruction by the one we already export though the interface. This made exporting unnamed destructors necessary.
1 parent ec8a2fe commit 4cbef94

File tree

4 files changed

+67
-16
lines changed

4 files changed

+67
-16
lines changed

‎RELEASE_NOTES.md‎

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,10 @@
1+
# Upcoming
2+
3+
- feat: Plugin support in the resolution pipeline (https://github.com/dafny-lang/dafny/pull/1739)
4+
- fix: NullPointerException in the AST (https://github.com/dafny-lang/dafny/pull/1805)
5+
- fix: Change datatype deconstruction in match statements for C# (https://github.com/dafny-lang/dafny/issues/1815)
6+
7+
18
# 3.4
29

310
- For certain classes of changes to a Dafny program, prevent unexpected changes in verification behavior.

‎Source/Dafny/Compilers/Compiler-Csharp.cs‎

Lines changed: 26 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -641,32 +641,38 @@ bool ContainsTyVar(TypeParameter tp, Type ty)
641641
wBody.WriteLine($"return new {className}{uTypeArgs}({constructorArgs});");
642642
}
643643

644+
// Emits getters for both named and unnamed destructors. The named ones are grouped across constructors by their
645+
// name and thus QDtorM = DtorM. This is not possible for unnamed ones, as there is no guarantee about shared return
646+
// types, so they are treated individually and their names (QDtorM) are qualified by their respective constructors.
644647
private void CompileDatatypeDestructorsAndAddToInterface(DatatypeDecl dt, ConcreteSyntaxTree wr,
645-
ConcreteSyntaxTree interfaceTree, string DtT_TypeArgs) {
648+
ConcreteSyntaxTree interfaceTree, string DtT_TypeArgs) {
646649
foreach (var ctor in dt.Ctors) {
650+
var index = 0;
647651
foreach (var dtor in ctor.Destructors) {
648652
if (dtor.EnclosingCtors[0] == ctor) {
649653
var arg = dtor.CorrespondingFormals[0];
650-
if (!arg.IsGhost && arg.HasName) {
651-
// T0 dtor_Dtor0 { get; }
652-
interfaceTree.WriteLine($"{TypeName(arg.Type, wr, arg.tok)} dtor_{arg.CompileName} {{ get; }}");
654+
if (!arg.IsGhost) {
655+
var DtorM = arg.HasName ? arg.CompileName : FormalName(arg, index);
656+
// TN dtor_QDtorM { get; }
657+
interfaceTree.WriteLine($"{TypeName(arg.Type, wr, arg.tok)} {DestructorGetterName(arg, ctor, index)} {{ get; }}");
653658

654-
// public T0 dtor_Dtor0 { get {
659+
// public TN dtor_QDtorM { get {
655660
// var d = this; // for inductive datatypes
656661
// var d = this._Get(); // for co-inductive datatypes
657-
// if (d is DT_Ctor0) { return ((DT_Ctor0)d).Dtor0; }
658-
// if (d is DT_Ctor1) { return ((DT_Ctor1)d).Dtor0; }
662+
// if (d is DT_Ctor0) { return ((DT_Ctor0)d).DtorM; }
663+
// if (d is DT_Ctor1) { return ((DT_Ctor1)d).DtorM; }
659664
// ...
660-
// if (d is DT_Ctor(n-2)) { return ((DT_Ctor(n-2))d).Dtor0; }
661-
// return ((DT_Ctor(n-1))d).Dtor0;
665+
// if (d is DT_Ctor(n-2)) { return ((DT_Ctor(n-2))d).DtorM; }
666+
// return ((DT_Ctor(n-1))d).DtorM;
662667
// }}
663-
var wDtor = wr.NewNamedBlock($"public {TypeName(arg.Type, wr, arg.tok)} dtor_{arg.CompileName}");
668+
var wDtor =
669+
wr.NewNamedBlock($"public {TypeName(arg.Type, wr, arg.tok)} {DestructorGetterName(arg, ctor, index)}");
664670
var wGet = wDtor.NewBlock("get");
665671
if (dt.IsRecordType) {
666672
if (dt is CoDatatypeDecl) {
667-
wGet.WriteLine($"return this._Get().{IdName(arg)};");
673+
wGet.WriteLine($"return this._Get().{IdProtect(DtorM)};");
668674
} else {
669-
wGet.WriteLine($"return this.{IdName(arg)};");
675+
wGet.WriteLine($"return this.{IdProtect(DtorM)};");
670676
}
671677
} else {
672678
if (dt is CoDatatypeDecl) {
@@ -681,13 +687,14 @@ private void CompileDatatypeDestructorsAndAddToInterface(DatatypeDecl dt, Concre
681687
Contract.Assert(arg.CompileName == dtor.CorrespondingFormals[i].CompileName);
682688
var type = $"{dt.CompileName}_{ctor_i.CompileName}{DtT_TypeArgs}";
683689
// TODO use pattern matching to replace cast.
684-
wGet.WriteLine($"if (d is {type}) {{ return (({type})d).{IdName(arg)}; }}");
690+
wGet.WriteLine($"if (d is {type}) {{ return (({type})d).{IdProtect(DtorM)}; }}");
685691
}
686692

687693
Contract.Assert(arg.CompileName == dtor.CorrespondingFormals[n - 1].CompileName);
688694
wGet.WriteLine(
689-
$"return (({dt.CompileName}_{dtor.EnclosingCtors[n - 1].CompileName}{DtT_TypeArgs})d).{IdName(arg)};");
695+
$"return (({dt.CompileName}_{dtor.EnclosingCtors[n - 1].CompileName}{DtT_TypeArgs})d).{IdProtect(DtorM)};");
690696
}
697+
index++;
691698
}
692699
}
693700
}
@@ -2614,8 +2621,11 @@ protected override ConcreteSyntaxTree EmitBetaRedex(List<string> boundVars, List
26142621
}
26152622

26162623
protected override void EmitDestructor(string source, Formal dtor, int formalNonGhostIndex, DatatypeCtor ctor, List<Type> typeArgs, Type bvType, ConcreteSyntaxTree wr) {
2617-
var dtorName = FormalName(dtor, formalNonGhostIndex);
2618-
wr.Write("(({0}){1}{2}).{3}", DtCtorName(ctor, typeArgs, wr), source, ctor.EnclosingDatatype is CoDatatypeDecl ? "._Get()" : "", dtorName);
2624+
wr.Write($"{source}.{DestructorGetterName(dtor, ctor, formalNonGhostIndex)}");
2625+
}
2626+
2627+
private string DestructorGetterName(Formal dtor, DatatypeCtor ctor, int index) {
2628+
return $"dtor_{(dtor.HasName ? dtor.CompileName : ctor.CompileName + FormalName(dtor, index))}";
26192629
}
26202630

26212631
protected override ConcreteSyntaxTree CreateLambda(List<Type> inTypes, Bpl.IToken tok, List<string> inNames, Type resultType, ConcreteSyntaxTree wr, bool untyped = false) {

‎Test/git-issues/git-issue-1815.dfy‎

Lines changed: 21 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,21 @@
1+
// RUN: %dafny /compile:0 "%s" > "%t"
2+
// RUN: %dafny /noVerify /compile:4 /compileTarget:cs "%s" >> "%t"
3+
// RUN: %dafny /noVerify /compile:4 /compileTarget:js "%s" >> "%t"
4+
// RUN: %dafny /noVerify /compile:4 /compileTarget:java "%s" >> "%t"
5+
// RUN: %dafny /noVerify /compile:4 /compileTarget:go "%s" >> "%t"
6+
// RUN: %diff "%s.expect" "%t"
7+
// The Java compiler lacks support for this (see dafny0/RuntimeTypeTests0.dfy).
8+
9+
datatype X<+U> = X(x: U)
10+
11+
trait Tr {}
12+
class Cl extends Tr {
13+
constructor () {}
14+
}
15+
16+
method Main() {
17+
var cl := new Cl();
18+
var e: X<Tr> := X(cl);
19+
match e
20+
case X(tr) => return;
21+
}

‎Test/git-issues/git-issue-1815.dfy.expect‎

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
2+
Dafny program verifier finished with 1 verified, 0 errors
3+
4+
Dafny program verifier did not attempt verification
5+
6+
Dafny program verifier did not attempt verification
7+
8+
Dafny program verifier did not attempt verification
9+
git-issue-1815.dfy(18,11): Error: compilation does not support trait types as a type parameter (got 'Tr'); consider introducing a ghost
10+
git-issue-1815.dfy(18,11): Error: compilation does not support trait types as a type parameter (got 'Tr'); consider introducing a ghost
11+
Wrote textual form of partial target program to git-issue-1815-java/git_issue_1815.java
12+
13+
Dafny program verifier did not attempt verification

0 commit comments

Comments
 (0)