From 852f7febf55e931581e994488cab66d6136300ae Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Mon, 26 Dec 2022 19:35:16 -0800 Subject: [PATCH] fix: Infer (==) for non-null iterator type Fixes #3273 --- Source/DafnyCore/Resolver/Resolver.cs | 8 +++- Test/git-issues/git-issue-3273.dfy | 54 +++++++++++++++++++++++ Test/git-issues/git-issue-3273.dfy.expect | 9 ++++ 3 files changed, 70 insertions(+), 1 deletion(-) create mode 100644 Test/git-issues/git-issue-3273.dfy create mode 100644 Test/git-issues/git-issue-3273.dfy.expect diff --git a/Source/DafnyCore/Resolver/Resolver.cs b/Source/DafnyCore/Resolver/Resolver.cs index e53db64db50..859cf82130e 100644 --- a/Source/DafnyCore/Resolver/Resolver.cs +++ b/Source/DafnyCore/Resolver/Resolver.cs @@ -3059,12 +3059,17 @@ public void ResolveTopLevelDecls_Core(List/*!*/ declarations, if (d is IteratorDecl) { var iter = (IteratorDecl)d; var done = false; - foreach (var tp in iter.TypeArgs) { + var nonnullIter = iter.NonNullTypeDecl; + Contract.Assert(nonnullIter.TypeArgs.Count == iter.TypeArgs.Count); + for (var i = 0; i < iter.TypeArgs.Count; i++) { + var tp = iter.TypeArgs[i]; + var correspondingNonnullIterTypeParameter = nonnullIter.TypeArgs[i]; if (tp.Characteristics.EqualitySupport == TypeParameter.EqualitySupportValue.Unspecified) { // here's our chance to infer the need for equality support foreach (var p in iter.Ins) { if (InferRequiredEqualitySupport(tp, p.Type)) { tp.Characteristics.EqualitySupport = TypeParameter.EqualitySupportValue.InferredRequired; + correspondingNonnullIterTypeParameter.Characteristics.EqualitySupport = TypeParameter.EqualitySupportValue.InferredRequired; done = true; break; } @@ -3076,6 +3081,7 @@ public void ResolveTopLevelDecls_Core(List/*!*/ declarations, if (InferRequiredEqualitySupport(tp, p.Type)) { tp.Characteristics.EqualitySupport = TypeParameter.EqualitySupportValue.InferredRequired; + correspondingNonnullIterTypeParameter.Characteristics.EqualitySupport = TypeParameter.EqualitySupportValue.InferredRequired; break; } } diff --git a/Test/git-issues/git-issue-3273.dfy b/Test/git-issues/git-issue-3273.dfy new file mode 100644 index 00000000000..01ee9b23537 --- /dev/null +++ b/Test/git-issues/git-issue-3273.dfy @@ -0,0 +1,54 @@ +// RUN: %exits-with 2 %dafny "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +iterator Iter(u: set) // this infers Y to be (==) + +method Repro() { + var iter: Iter; // error: K is not (==) +} + +iterator IterA() // this declares X to be (==) + +iterator IterB(u: set) // this infers Y to be (==) + +method Test() { + var a0: IterA; // error: K is not (==) + var a1: IterA; + var b0: IterB; // error: K is not (==) + var b1: IterB; + + var c0: IterA?; // error: K is not (==) + var c1: IterA?; + var d0: IterB?; // error: K is not (==) + var d1: IterB?; +} + +iterator EqIter(u: set, x: Y, y: Y) yields (eq: bool) + yield ensures eq == (x == y) + ensures false +{ + while true { + yield x == y; + } +} + +datatype Dt = Dt(a: int, ghost b: int) + +method Main() { + var d0 := Dt(0, 0); + var d1 := Dt(0, 1); + assert d0 != d1; // clearly + + // The following is error (but was not always detected by Dafny), because EqIter should take a (==) type argument. + var iter: EqIter
; // error: Dt is not an equality-supporting type + // The following does give an error, since the constructor lives in class EqIter whose + // type parameer has been inferred to be (==). + iter := new EqIter({}, d0, d1); // error: Dt is not an equality-supporting type + var more := iter.MoveNext(); + assert more; + assert iter.eq == (d0 == d1) == false; // according to the yield-ensures clause + print iter.eq, "\n"; + if iter.eq { + var ugh := 1 / 0; // according to the verifier, we never get here + } +} diff --git a/Test/git-issues/git-issue-3273.dfy.expect b/Test/git-issues/git-issue-3273.dfy.expect new file mode 100644 index 00000000000..384655391be --- /dev/null +++ b/Test/git-issues/git-issue-3273.dfy.expect @@ -0,0 +1,9 @@ +git-issue-3273.dfy(7,12): Error: type parameter (Y) passed to type Iter must support equality (got K) (perhaps try declaring type parameter 'K' on line 6 as 'K(==)', which says it can only be instantiated with a type that supports equality) +git-issue-3273.dfy(15,10): Error: type parameter (X) passed to type IterA must support equality (got K) (perhaps try declaring type parameter 'K' on line 14 as 'K(==)', which says it can only be instantiated with a type that supports equality) +git-issue-3273.dfy(17,10): Error: type parameter (Y) passed to type IterB must support equality (got K) (perhaps try declaring type parameter 'K' on line 14 as 'K(==)', which says it can only be instantiated with a type that supports equality) +git-issue-3273.dfy(20,10): Error: type parameter (X) passed to type IterA must support equality (got K) (perhaps try declaring type parameter 'K' on line 14 as 'K(==)', which says it can only be instantiated with a type that supports equality) +git-issue-3273.dfy(22,10): Error: type parameter (Y) passed to type IterB must support equality (got K) (perhaps try declaring type parameter 'K' on line 14 as 'K(==)', which says it can only be instantiated with a type that supports equality) +git-issue-3273.dfy(43,12): Error: type parameter (Y) passed to type EqIter must support equality (got Dt) +git-issue-3273.dfy(46,14): Error: type parameter (Y) passed to type EqIter must support equality (got Dt) +git-issue-3273.dfy(46,21): Error: set argument type must support equality (got Dt) +8 resolution/type errors detected in git-issue-3273.dfy