From 713c008092967474d9396756f0bf72629f6aafcf Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Thu, 5 Sep 2024 17:32:42 -0500 Subject: [PATCH 1/3] Chore: increase runtime coverage --- Source/DafnyCore/Backends/BoogieExtractor.cs | 2 +- Source/DafnyDriver/Commands/VerifyCommand.cs | 2 +- Source/DafnyRuntime.Tests/CsRuntimeTest.cs | 549 +++++++++++++++++++ Source/DafnyRuntime.Tests/TupleTest.cs | 415 +++++++++++++- Source/DafnyRuntime/AssemblyInfo.cs | 2 + Source/DafnyRuntime/DafnyRuntime.cs | 6 +- Source/DafnyRuntime/DafnyRuntime.csproj | 4 +- 7 files changed, 954 insertions(+), 26 deletions(-) create mode 100644 Source/DafnyRuntime.Tests/CsRuntimeTest.cs create mode 100644 Source/DafnyRuntime/AssemblyInfo.cs diff --git a/Source/DafnyCore/Backends/BoogieExtractor.cs b/Source/DafnyCore/Backends/BoogieExtractor.cs index 86b110d7091..7d5c7b868e3 100644 --- a/Source/DafnyCore/Backends/BoogieExtractor.cs +++ b/Source/DafnyCore/Backends/BoogieExtractor.cs @@ -187,7 +187,7 @@ public override void VisitMethod(Method method) { } private QKeyValue? GetKeyValues(IToken tok, Attributes attributes) { - Boogie.QKeyValue kv = null; + QKeyValue? kv = null; var extractAttributes = Attributes.FindAllExpressions(attributes, AttributeAttribute); if (extractAttributes != null) { if (extractAttributes.Count == 0) { diff --git a/Source/DafnyDriver/Commands/VerifyCommand.cs b/Source/DafnyDriver/Commands/VerifyCommand.cs index 6fcdf1965ae..5bd4344ac6d 100644 --- a/Source/DafnyDriver/Commands/VerifyCommand.cs +++ b/Source/DafnyDriver/Commands/VerifyCommand.cs @@ -98,7 +98,7 @@ public static async Task HandleVerification(DafnyOptions options) { var extractedProgram = BoogieExtractor.Extract(resolution.ResolvedProgram); engine.PrintBplFile(options.BoogieExtractionTargetFile, extractedProgram, true, pretty: true); } catch (ExtractorError extractorError) { - options.OutputWriter.WriteLine($"Boogie axiom extraction error: {extractorError.Message}"); + await options.OutputWriter.WriteLineAsync($"Boogie axiom extraction error: {extractorError.Message}"); return 1; } } diff --git a/Source/DafnyRuntime.Tests/CsRuntimeTest.cs b/Source/DafnyRuntime.Tests/CsRuntimeTest.cs new file mode 100644 index 00000000000..dbae79751fd --- /dev/null +++ b/Source/DafnyRuntime.Tests/CsRuntimeTest.cs @@ -0,0 +1,549 @@ +using System; +using System.Collections.Generic; +using System.Collections.Immutable; +using System.Linq; +using System.Numerics; +using System.Threading; +using Xunit; +using Dafny; + +namespace DafnyRuntime.Tests; + +public class RuntimeTest { + [Fact] + public void TestConcatSequence() { + var c = new ConcatSequence(Sequence.FromElements(1, 2), Sequence.FromElements(3, 4)); + var x = c.ImmutableElements; + c.ComputeElements(); // For coverage + var left = new ConcatSequence(Sequence.FromElements(1), Sequence.FromElements(2)); + var tree = new ConcatSequence(left, Sequence.FromElements(3, 4)); + left.left = null; // For coverage, we simulate multithreading + Thread t = new Thread(delegate () { + left.right = null; + Thread.Sleep(100); // Ensure ComputeElements() does not work immediately + left.elmts = new List() { 1, 2 }.ToImmutableArray(); + }); + t.Start(); + var result = tree.ComputeElements(); // Without the thread, will loop forever + Assert.Equal(Sequence.FromArray(result.ToArray()), Sequence.FromArray(x.ToArray())); + } + + class Dummy { } + + [Fact] + public void TestSetAndCoverage() { + var x = Set.FromCollectionPlusOne(new List() { new Dummy(), null }, new Dummy()); + var y = Set.FromCollectionPlusOne(new List() { new Dummy(), new Dummy() }, new Dummy()); + var z = Set.FromCollectionPlusOne(new List() { new Dummy(), new Dummy() }, null); + Assert.Equal(3, x.Count); + Assert.Equal(3, y.Count); + Assert.Equal(3, z.Count); + Assert.Equal(3, x.LongCount); + Assert.Equal(3, y.LongCount); + Assert.Equal(3, z.LongCount); + Assert.Equal(8, x.AllSubsets.ToList().Count); + Assert.Equal(8, y.AllSubsets.ToList().Count); + Assert.Equal(8, z.AllSubsets.ToList().Count); + Dafny.ISet? n = null; + Assert.False(x.Equals(n)); + object? nObject = null; + Assert.False(x.Equals(nObject)); + Assert.False(x.EqualsAux(n)); + Assert.NotEqual(0, x.GetHashCode()); + } + + [Fact] + public void TestMapAndCoverage() { + Map? n = null; + var x = Map.FromElements( + new Pair(new Dummy(), new Dummy()), + new Pair(null, new Dummy()), + new Pair(new Dummy(), null)); + + var nn = Map.FromElements( + new Pair(new Dummy(), new Dummy())); + Assert.Equal(3, x.Count); + Assert.Equal(3, x.LongCount); + Assert.Equal(1, nn.Count); + Assert.Equal(1, nn.LongCount); + Assert.False(nn.Equals(n)); + + var oo = Map.FromElements( + new Pair(new Dummy(), new Dummy()), + new Pair(null, new Dummy()), + new Pair(new Dummy(), null)); + Assert.True(oo.EqualsObjObj(oo)); + // TBC + } + + [Fact] + public void TestHaltException() { + var x = new HaltException("Test failed"); + Assert.Equal("Test failed", x.Message); + } + + [Fact] + public void RuneTest() { + Assert.Throws(() => new Rune(0xD801)); + Assert.Throws(() => new Rune(0x11_0000)); + Assert.False(new Rune(65).Equals(null)); + Assert.True(new Rune(65).Equals(new Rune(65))); + Assert.Equal(-1, new Rune(65).CompareTo(new Rune(66))); + Assert.Equal(0, new Rune(65).CompareTo(new Rune(65))); + Assert.Equal(1, new Rune(65).CompareTo(new Rune(64))); + IComparable c = new Rune(65); + Assert.Equal(1, c.CompareTo(null)); + Assert.Equal(0, c.CompareTo(new Rune(65))); + Assert.Throws(() => c.CompareTo("abc")); + var input = "\uD800"; // High surrogate but no low surrogate afterward + Assert.Throws(() => Rune.Enumerate(input).ToList()); + input = "\uDC00"; // Low surrogate + Assert.Throws(() => Rune.Enumerate(input).ToList()); + input = "\uD800\uD800"; // High surrogate twice + Assert.Throws(() => Rune.Enumerate(input).ToList()); + } + + [Fact] + public void DowncastClone0() { + Func originalFunc = () => 42; + var clonedFunc = originalFunc.DowncastClone(i => i.ToString()); + Assert.Equal("42", clonedFunc()); + } + + [Fact] + public void DowncastClone1() { + Func originalFunc = x => x * 2.5; + var clonedFunc = originalFunc.DowncastClone(int.Parse, d => d.ToString("F2")); + Assert.Equal("5.00", clonedFunc("2")); + } + + [Fact] + public void DowncastClone2() { + Func originalFunc = (x, y) => x + y; + var clonedFunc = originalFunc.DowncastClone(int.Parse, int.Parse, sum => sum.ToString()); + Assert.Equal("7", clonedFunc("3", "4")); + } + + [Fact] + public void DowncastClone3() { + Func originalFunc = (x, y, z) => x + y + z; + var clonedFunc = originalFunc.DowncastClone(int.Parse, int.Parse, int.Parse, sum => sum.ToString()); + Assert.Equal("10", clonedFunc("2", "3", "5")); + } + + [Fact] + public void DowncastClone4() { + Func originalFunc = (a, b, c, d) => a + b + c + d; + var clonedFunc = originalFunc.DowncastClone(int.Parse, int.Parse, int.Parse, int.Parse, sum => sum.ToString()); + Assert.Equal("10", clonedFunc("1", "2", "3", "4")); + } + + [Fact] + public void DowncastClone5() { + Func originalFunc = (a, b, c, d, e) => a + b + c + d + e; + var clonedFunc = originalFunc.DowncastClone(int.Parse, int.Parse, int.Parse, int.Parse, int.Parse, sum => sum.ToString()); + Assert.Equal("15", clonedFunc("1", "2", "3", "4", "5")); + } + + [Fact] + public void DowncastClone6() { + Func originalFunc = (a, b, c, d, e, f) => a + b + c + d + e + f; + var clonedFunc = originalFunc.DowncastClone(int.Parse, int.Parse, int.Parse, int.Parse, int.Parse, int.Parse, sum => sum.ToString()); + Assert.Equal("21", clonedFunc("1", "2", "3", "4", "5", "6")); + } + + [Fact] + public void DowncastClone7() { + Func originalFunc = (a, b, c, d, e, f, g) => a + b + c + d + e + f + g; + var clonedFunc = originalFunc.DowncastClone(int.Parse, int.Parse, int.Parse, int.Parse, int.Parse, int.Parse, int.Parse, sum => sum.ToString()); + Assert.Equal("28", clonedFunc("1", "2", "3", "4", "5", "6", "7")); + } + + [Fact] + public void DowncastClone8() { + Func originalFunc = (a, b, c, d, e, f, g, h) => a + b + c + d + e + f + g + h; + var clonedFunc = originalFunc.DowncastClone(int.Parse, int.Parse, int.Parse, int.Parse, int.Parse, int.Parse, int.Parse, int.Parse, sum => sum.ToString()); + Assert.Equal("36", clonedFunc("1", "2", "3", "4", "5", "6", "7", "8")); + } + + [Fact] + public void DowncastClone9() { + Func originalFunc = (a, b, c, d, e, f, g, h, i) => a + b + c + d + e + f + g + h + i; + var clonedFunc = originalFunc.DowncastClone(int.Parse, int.Parse, int.Parse, int.Parse, int.Parse, int.Parse, int.Parse, int.Parse, int.Parse, sum => sum.ToString()); + Assert.Equal("45", clonedFunc("1", "2", "3", "4", "5", "6", "7", "8", "9")); + } + + [Fact] + public void DowncastClone10() { + Func originalFunc = (a, b, c, d, e, f, g, h, i, j) => a + b + c + d + e + f + g + h + i + j; + var clonedFunc = originalFunc.DowncastClone(int.Parse, int.Parse, int.Parse, int.Parse, int.Parse, int.Parse, int.Parse, int.Parse, int.Parse, int.Parse, sum => sum.ToString()); + Assert.Equal("55", clonedFunc("1", "2", "3", "4", "5", "6", "7", "8", "9", "10")); + } + + [Fact] + public void DowncastClone11() { + Func originalFunc = (a, b, c, d, e, f, g, h, i, j, k) => a + b + c + d + e + f + g + h + i + j + k; + var clonedFunc = originalFunc.DowncastClone(int.Parse, int.Parse, int.Parse, int.Parse, int.Parse, int.Parse, int.Parse, int.Parse, int.Parse, int.Parse, int.Parse, sum => sum.ToString()); + Assert.Equal("66", clonedFunc("1", "2", "3", "4", "5", "6", "7", "8", "9", "10", "11")); + } + + [Fact] + public void DowncastClone12() { + Func originalFunc = (a, b, c, d, e, f, g, h, i, j, k, l) => a + b + c + d + e + f + g + h + i + j + k + l; + var clonedFunc = originalFunc.DowncastClone(int.Parse, int.Parse, int.Parse, int.Parse, int.Parse, int.Parse, int.Parse, int.Parse, int.Parse, int.Parse, int.Parse, int.Parse, sum => sum.ToString()); + Assert.Equal("78", clonedFunc("1", "2", "3", "4", "5", "6", "7", "8", "9", "10", "11", "12")); + } + + [Fact] + public void DowncastClone13() { + Func originalFunc = (a, b, c, d, e, f, g, h, i, j, k, l, m) => a + b + c + d + e + f + g + h + i + j + k + l + m; + var clonedFunc = originalFunc.DowncastClone(int.Parse, int.Parse, int.Parse, int.Parse, int.Parse, int.Parse, int.Parse, int.Parse, int.Parse, int.Parse, int.Parse, int.Parse, int.Parse, sum => sum.ToString()); + Assert.Equal("91", clonedFunc("1", "2", "3", "4", "5", "6", "7", "8", "9", "10", "11", "12", "13")); + } + + [Fact] + public void DowncastClone14() { + Func originalFunc = (a, b, c, d, e, f, g, h, i, j, k, l, m, n) => a + b + c + d + e + f + g + h + i + j + k + l + m + n; + var clonedFunc = originalFunc.DowncastClone(int.Parse, int.Parse, int.Parse, int.Parse, int.Parse, int.Parse, int.Parse, int.Parse, int.Parse, int.Parse, int.Parse, int.Parse, int.Parse, int.Parse, sum => sum.ToString()); + Assert.Equal("105", clonedFunc("1", "2", "3", "4", "5", "6", "7", "8", "9", "10", "11", "12", "13", "14")); + } + + [Fact] + public void DowncastClone15() { + Func originalFunc = (a, b, c, d, e, f, g, h, i, j, k, l, m, n, o) => a + b + c + d + e + f + g + h + i + j + k + l + m + n + o; + var clonedFunc = originalFunc.DowncastClone(int.Parse, int.Parse, int.Parse, int.Parse, int.Parse, int.Parse, int.Parse, int.Parse, int.Parse, int.Parse, int.Parse, int.Parse, int.Parse, int.Parse, int.Parse, sum => sum.ToString()); + Assert.Equal("120", clonedFunc("1", "2", "3", "4", "5", "6", "7", "8", "9", "10", "11", "12", "13", "14", "15")); + } + + [Fact] + public void DowncastClone16() { + Func originalFunc = (a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) => a + b + c + d + e + f + g + h + i + j + k + l + m + n + o + p; + var clonedFunc = originalFunc.DowncastClone( + int.Parse, int.Parse, int.Parse, int.Parse, int.Parse, int.Parse, int.Parse, int.Parse, + int.Parse, int.Parse, int.Parse, int.Parse, int.Parse, int.Parse, int.Parse, int.Parse, + sum => sum.ToString() + ); + Assert.Equal("136", clonedFunc("1", "2", "3", "4", "5", "6", "7", "8", "9", "10", "11", "12", "13", "14", "15", "16")); + } + + + [Fact] + public void InitNewArray1Test() { + var a = ArrayHelpers.InitNewArray1('a', + new BigInteger(2)); + Assert.Equal(2, a.Length); + Assert.Equal('a', a[0]); + Assert.Equal('a', a[1]); + } + + [Fact] + public void InitNewArray2Test() { + var a = ArrayHelpers.InitNewArray2('a', + new BigInteger(1), + new BigInteger(2)); + for (var i = 0; i < 2; i++) { + Assert.Equal(i == 1 ? 2 : 1, a.GetLength(i)); + } + Assert.Equal('a', a[0, 0]); + Assert.Equal('a', a[0, 1]); + } + + [Fact] + public void InitNewArray3Test() { + var a = ArrayHelpers.InitNewArray3('a', + new BigInteger(1), + new BigInteger(1), + new BigInteger(2)); + for (var i = 0; i < 3; i++) { + Assert.Equal(i == 2 ? 2 : 1, a.GetLength(i)); + } + Assert.Equal('a', a[0, 0, 0]); + Assert.Equal('a', a[0, 0, 1]); + } + + [Fact] + public void InitNewArray4Test() { + var a = ArrayHelpers.InitNewArray4( + 'a', + new BigInteger(1), + new BigInteger(1), + new BigInteger(1), + new BigInteger(2) + ); + for (var i = 0; i < 4; i++) { + Assert.Equal(i == 3 ? 2 : 1, a.GetLength(i)); + } + Assert.Equal('a', a[0, 0, 0, 0]); + Assert.Equal('a', a[0, 0, 0, 1]); + } + + [Fact] + public void InitNewArray5Test() { + var a = ArrayHelpers.InitNewArray5( + 'a', + new BigInteger(1), + new BigInteger(1), + new BigInteger(1), + new BigInteger(1), + new BigInteger(2) + ); + for (var i = 0; i < 5; i++) { + Assert.Equal(i == 4 ? 2 : 1, a.GetLength(i)); + } + Assert.Equal('a', a[0, 0, 0, 0, 0]); + Assert.Equal('a', a[0, 0, 0, 0, 1]); + } + + [Fact] + public void InitNewArray6Test() { + var a = ArrayHelpers.InitNewArray6( + 'a', + new BigInteger(1), + new BigInteger(1), + new BigInteger(1), + new BigInteger(1), + new BigInteger(1), + new BigInteger(2) + ); + for (var i = 0; i < 6; i++) { + Assert.Equal(i == 5 ? 2 : 1, a.GetLength(i)); + } + Assert.Equal('a', a[0, 0, 0, 0, 0, 0]); + Assert.Equal('a', a[0, 0, 0, 0, 0, 1]); + } + + [Fact] + public void InitNewArray7Test() { + var a = ArrayHelpers.InitNewArray7( + 'a', + new BigInteger(1), + new BigInteger(1), + new BigInteger(1), + new BigInteger(1), + new BigInteger(1), + new BigInteger(1), + new BigInteger(2) + ); + for (var i = 0; i < 7; i++) { + Assert.Equal(i == 6 ? 2 : 1, a.GetLength(i)); + } + Assert.Equal('a', a[0, 0, 0, 0, 0, 0, 0]); + Assert.Equal('a', a[0, 0, 0, 0, 0, 0, 1]); + } + + [Fact] + public void InitNewArray8Test() { + var a = ArrayHelpers.InitNewArray8( + 'a', + new BigInteger(1), + new BigInteger(1), + new BigInteger(1), + new BigInteger(1), + new BigInteger(1), + new BigInteger(1), + new BigInteger(1), + new BigInteger(2) + ); + for (var i = 0; i < 8; i++) { + Assert.Equal(i == 7 ? 2 : 1, a.GetLength(i)); + } + Assert.Equal('a', a[0, 0, 0, 0, 0, 0, 0, 0]); + Assert.Equal('a', a[0, 0, 0, 0, 0, 0, 0, 1]); + } + + [Fact] + public void InitNewArray9Test() { + var a = ArrayHelpers.InitNewArray9( + 'a', + new BigInteger(1), + new BigInteger(1), + new BigInteger(1), + new BigInteger(1), + new BigInteger(1), + new BigInteger(1), + new BigInteger(1), + new BigInteger(1), + new BigInteger(2) + ); + for (var i = 0; i < 9; i++) { + Assert.Equal(i == 8 ? 2 : 1, a.GetLength(i)); + } + Assert.Equal('a', a[0, 0, 0, 0, 0, 0, 0, 0, 0]); + Assert.Equal('a', a[0, 0, 0, 0, 0, 0, 0, 0, 1]); + } + + [Fact] + public void InitNewArray10Test() { + var a = ArrayHelpers.InitNewArray10( + 'a', + new BigInteger(1), + new BigInteger(1), + new BigInteger(1), + new BigInteger(1), + new BigInteger(1), + new BigInteger(1), + new BigInteger(1), + new BigInteger(1), + new BigInteger(1), + new BigInteger(2) + ); + for (var i = 0; i < 10; i++) { + Assert.Equal(i == 9 ? 2 : 1, a.GetLength(i)); + } + Assert.Equal('a', a[0, 0, 0, 0, 0, 0, 0, 0, 0, 0]); + Assert.Equal('a', a[0, 0, 0, 0, 0, 0, 0, 0, 0, 1]); + } + + [Fact] + public void InitNewArray11Test() { + var a = ArrayHelpers.InitNewArray11( + 'a', + new BigInteger(1), + new BigInteger(1), + new BigInteger(1), + new BigInteger(1), + new BigInteger(1), + new BigInteger(1), + new BigInteger(1), + new BigInteger(1), + new BigInteger(1), + new BigInteger(1), + new BigInteger(2) + ); + for (var i = 0; i < 11; i++) { + Assert.Equal(i == 10 ? 2 : 1, a.GetLength(i)); + } + Assert.Equal('a', a[0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]); + Assert.Equal('a', a[0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1]); + } + + [Fact] + public void InitNewArray12Test() { + var a = ArrayHelpers.InitNewArray12( + 'a', + new BigInteger(1), + new BigInteger(1), + new BigInteger(1), + new BigInteger(1), + new BigInteger(1), + new BigInteger(1), + new BigInteger(1), + new BigInteger(1), + new BigInteger(1), + new BigInteger(1), + new BigInteger(1), + new BigInteger(2) + ); + for (var i = 0; i < 12; i++) { + Assert.Equal(i == 11 ? 2 : 1, a.GetLength(i)); + } + Assert.Equal('a', a[0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]); + Assert.Equal('a', a[0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1]); + } + + [Fact] + public void InitNewArray13Test() { + var a = ArrayHelpers.InitNewArray13( + 'a', + new BigInteger(1), + new BigInteger(1), + new BigInteger(1), + new BigInteger(1), + new BigInteger(1), + new BigInteger(1), + new BigInteger(1), + new BigInteger(1), + new BigInteger(1), + new BigInteger(1), + new BigInteger(1), + new BigInteger(1), + new BigInteger(2) + ); + for (var i = 0; i < 13; i++) { + Assert.Equal(i == 12 ? 2 : 1, a.GetLength(i)); + } + Assert.Equal('a', a[0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]); + Assert.Equal('a', a[0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1]); + } + + [Fact] + public void InitNewArray14Test() { + var a = ArrayHelpers.InitNewArray14( + 'a', + new BigInteger(1), + new BigInteger(1), + new BigInteger(1), + new BigInteger(1), + new BigInteger(1), + new BigInteger(1), + new BigInteger(1), + new BigInteger(1), + new BigInteger(1), + new BigInteger(1), + new BigInteger(1), + new BigInteger(1), + new BigInteger(1), + new BigInteger(2) + ); + for (var i = 0; i < 14; i++) { + Assert.Equal(i == 13 ? 2 : 1, a.GetLength(i)); + } + Assert.Equal('a', a[0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]); + Assert.Equal('a', a[0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1]); + } + + [Fact] + public void InitNewArray15Test() { + var a = ArrayHelpers.InitNewArray15( + 'a', + new BigInteger(1), + new BigInteger(1), + new BigInteger(1), + new BigInteger(1), + new BigInteger(1), + new BigInteger(1), + new BigInteger(1), + new BigInteger(1), + new BigInteger(1), + new BigInteger(1), + new BigInteger(1), + new BigInteger(1), + new BigInteger(1), + new BigInteger(1), + new BigInteger(2) + ); + for (var i = 0; i < 15; i++) { + Assert.Equal(i == 14 ? 2 : 1, a.GetLength(i)); + } + Assert.Equal('a', a[0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]); + Assert.Equal('a', a[0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1]); + } + + [Fact] + public void InitNewArray16Test() { + var a = ArrayHelpers.InitNewArray16( + 'a', + new BigInteger(1), + new BigInteger(1), + new BigInteger(1), + new BigInteger(1), + new BigInteger(1), + new BigInteger(1), + new BigInteger(1), + new BigInteger(1), + new BigInteger(1), + new BigInteger(1), + new BigInteger(1), + new BigInteger(1), + new BigInteger(1), + new BigInteger(1), + new BigInteger(1), + new BigInteger(2) + ); + for (var i = 0; i < 16; i++) { + Assert.Equal(i == 15 ? 2 : 1, a.GetLength(i)); + } + Assert.Equal('a', a[0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]); + Assert.Equal('a', a[0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1]); + } +} \ No newline at end of file diff --git a/Source/DafnyRuntime.Tests/TupleTest.cs b/Source/DafnyRuntime.Tests/TupleTest.cs index dd6025c9e5e..ac047f3c50c 100644 --- a/Source/DafnyRuntime.Tests/TupleTest.cs +++ b/Source/DafnyRuntime.Tests/TupleTest.cs @@ -5,13 +5,56 @@ namespace DafnyRuntime.Tests { public class TupleTests { - public Func C = (int i) => i; + public Func C = (int i) => i.ToString(); + public Func I = (int i) => i; public Dafny.TypeDescriptor D = new Dafny.TypeDescriptor(0); + [Fact] + public void TestTuple0() { + var t = new _System.Tuple0(); + Assert.False(t.Equals(null)); + Assert.True(t.Equals(new _System.Tuple0())); + Assert.Equal(t, t.DowncastClone()); + Assert.NotEqual(0, t.GetHashCode()); + Assert.Equal("()", t.ToString()); + Assert.Equal(t, _System.Tuple0.Default()); + Assert.Equal(t, _System.Tuple0.create____hMake0()); + Assert.Equal(_System.Tuple0.create(), _System.Tuple0._TypeDescriptor().Default()); + } + + [Fact] + public void TestTuple1() { + var t = new _System.Tuple1(0); + Assert.False(t.Equals(null)); + for (var i = 0; i <= 1; i++) { + Assert.Equal(i == 1, t.Equals( + new _System.Tuple1( + i <= 0 ? 1 : 0))); + } + + Assert.Equal(new _System.Tuple1("0"), t.DowncastClone(C)); + Assert.Equal(t, t.DowncastClone(I)); + Assert.NotEqual(0, t.GetHashCode()); + Assert.Equal("(0)", t.ToString()); + Assert.Equal(t, _System.Tuple1.Default(0)); + Assert.Equal(t, _System.Tuple1.create____hMake1(0)); + Assert.Equal(_System.Tuple1.create(0), _System.Tuple1._TypeDescriptor(D).Default()); + Assert.Equal(0, t.dtor__0); + } + [Fact] public void TestTuple2() { var t = new _System.Tuple2(0, 1); - Assert.Equal(t, t.DowncastClone(C, C)); + Assert.False(t.Equals(null)); + for (var i = 0; i <= 2; i++) { + Assert.Equal(i == 2, t.Equals( + new _System.Tuple2( + i <= 0 ? 1 : 0, + i <= 1 ? 2 : 1))); + } + + Assert.Equal(new _System.Tuple2("0", "1"), t.DowncastClone(C, C)); + Assert.Equal(t, t.DowncastClone(I, I)); Assert.NotEqual(0, t.GetHashCode()); Assert.Equal("(0, 1)", t.ToString()); Assert.Equal(t, _System.Tuple2.Default(0, 1)); @@ -25,7 +68,17 @@ public void TestTuple2() { [Fact] public void TestTuple3() { var t = new _System.Tuple3(0, 1, 2); - Assert.Equal(t, t.DowncastClone(C, C, C)); + Assert.False(t.Equals(null)); + for (var i = 0; i <= 3; i++) { + Assert.Equal(i == 3, t.Equals( + new _System.Tuple3( + i <= 0 ? 1 : 0, + i <= 1 ? 2 : 1, + i <= 2 ? 3 : 2))); + } + + Assert.Equal(new _System.Tuple3("0", "1", "2"), t.DowncastClone(C, C, C)); + Assert.Equal(t, t.DowncastClone(I, I, I)); Assert.NotEqual(0, t.GetHashCode()); Assert.Equal("(0, 1, 2)", t.ToString()); Assert.Equal(t, _System.Tuple3.Default(0, 1, 2)); @@ -40,7 +93,18 @@ public void TestTuple3() { [Fact] public void TestTuple4() { var t = new _System.Tuple4(0, 1, 2, 3); - Assert.Equal(t, t.DowncastClone(C, C, C, C)); + Assert.False(t.Equals(null)); + for (var i = 0; i <= 4; i++) { + Assert.Equal(i == 4, t.Equals( + new _System.Tuple4( + i <= 0 ? 1 : 0, + i <= 1 ? 2 : 1, + i <= 2 ? 3 : 2, + i <= 3 ? 4 : 3))); + } + + Assert.Equal(new _System.Tuple4("0", "1", "2", "3"), t.DowncastClone(C, C, C, C)); + Assert.Equal(t, t.DowncastClone(I, I, I, I)); Assert.NotEqual(0, t.GetHashCode()); Assert.Equal("(0, 1, 2, 3)", t.ToString()); Assert.Equal(t, _System.Tuple4.Default(0, 1, 2, 3)); @@ -56,7 +120,19 @@ public void TestTuple4() { [Fact] public void TestTuple5() { var t = new _System.Tuple5(0, 1, 2, 3, 4); - Assert.Equal(t, t.DowncastClone(C, C, C, C, C)); + Assert.False(t.Equals(null)); + for (var i = 0; i <= 5; i++) { + Assert.Equal(i == 5, t.Equals( + new _System.Tuple5( + i <= 0 ? 1 : 0, + i <= 1 ? 2 : 1, + i <= 2 ? 3 : 2, + i <= 3 ? 4 : 3, + i <= 4 ? 5 : 4))); + } + + Assert.Equal(new _System.Tuple5("0", "1", "2", "3", "4"), t.DowncastClone(C, C, C, C, C)); + Assert.Equal(t, t.DowncastClone(I, I, I, I, I)); Assert.NotEqual(0, t.GetHashCode()); Assert.Equal("(0, 1, 2, 3, 4)", t.ToString()); Assert.Equal(t, _System.Tuple5.Default(0, 1, 2, 3, 4)); @@ -73,7 +149,20 @@ public void TestTuple5() { [Fact] public void TestTuple6() { var t = new _System.Tuple6(0, 1, 2, 3, 4, 5); - Assert.Equal(t, t.DowncastClone(C, C, C, C, C, C)); + Assert.False(t.Equals(null)); + for (var i = 0; i <= 6; i++) { + Assert.Equal(i == 6, t.Equals( + new _System.Tuple6( + i <= 0 ? 1 : 0, + i <= 1 ? 2 : 1, + i <= 2 ? 3 : 2, + i <= 3 ? 4 : 3, + i <= 4 ? 5 : 4, + i <= 5 ? 6 : 5))); + } + + Assert.Equal(new _System.Tuple6("0", "1", "2", "3", "4", "5"), t.DowncastClone(C, C, C, C, C, C)); + Assert.Equal(t, t.DowncastClone(I, I, I, I, I, I)); Assert.NotEqual(0, t.GetHashCode()); Assert.Equal("(0, 1, 2, 3, 4, 5)", t.ToString()); Assert.Equal(t, _System.Tuple6.Default(0, 1, 2, 3, 4, 5)); @@ -91,7 +180,21 @@ public void TestTuple6() { [Fact] public void TestTuple7() { var t = new _System.Tuple7(0, 1, 2, 3, 4, 5, 6); - Assert.Equal(t, t.DowncastClone(C, C, C, C, C, C, C)); + Assert.False(t.Equals(null)); + for (var i = 0; i <= 7; i++) { + Assert.Equal(i == 7, t.Equals( + new _System.Tuple7( + i <= 0 ? 1 : 0, + i <= 1 ? 2 : 1, + i <= 2 ? 3 : 2, + i <= 3 ? 4 : 3, + i <= 4 ? 5 : 4, + i <= 5 ? 6 : 5, + i <= 6 ? 7 : 6))); + } + + Assert.Equal(new _System.Tuple7("0", "1", "2", "3", "4", "5", "6"), t.DowncastClone(C, C, C, C, C, C, C)); + Assert.Equal(t, t.DowncastClone(I, I, I, I, I, I, I)); Assert.NotEqual(0, t.GetHashCode()); Assert.Equal("(0, 1, 2, 3, 4, 5, 6)", t.ToString()); Assert.Equal(t, _System.Tuple7.Default(0, 1, 2, 3, 4, 5, 6)); @@ -110,7 +213,22 @@ public void TestTuple7() { [Fact] public void TestTuple8() { var t = new _System.Tuple8(0, 1, 2, 3, 4, 5, 6, 7); - Assert.Equal(t, t.DowncastClone(C, C, C, C, C, C, C, C)); + Assert.False(t.Equals(null)); + for (var i = 0; i <= 8; i++) { + Assert.Equal(i == 8, t.Equals( + new _System.Tuple8( + i <= 0 ? 1 : 0, + i <= 1 ? 2 : 1, + i <= 2 ? 3 : 2, + i <= 3 ? 4 : 3, + i <= 4 ? 5 : 4, + i <= 5 ? 6 : 5, + i <= 6 ? 7 : 6, + i <= 7 ? 8 : 7))); + } + + Assert.Equal(new _System.Tuple8("0", "1", "2", "3", "4", "5", "6", "7"), t.DowncastClone(C, C, C, C, C, C, C, C)); + Assert.Equal(t, t.DowncastClone(I, I, I, I, I, I, I, I)); Assert.NotEqual(0, t.GetHashCode()); Assert.Equal("(0, 1, 2, 3, 4, 5, 6, 7)", t.ToString()); Assert.Equal(t, _System.Tuple8.Default(0, 1, 2, 3, 4, 5, 6, 7)); @@ -130,7 +248,23 @@ public void TestTuple8() { [Fact] public void TestTuple9() { var t = new _System.Tuple9(0, 1, 2, 3, 4, 5, 6, 7, 8); - Assert.Equal(t, t.DowncastClone(C, C, C, C, C, C, C, C, C)); + Assert.False(t.Equals(null)); + for (var i = 0; i <= 9; i++) { + Assert.Equal(i == 9, t.Equals( + new _System.Tuple9( + i <= 0 ? 1 : 0, + i <= 1 ? 2 : 1, + i <= 2 ? 3 : 2, + i <= 3 ? 4 : 3, + i <= 4 ? 5 : 4, + i <= 5 ? 6 : 5, + i <= 6 ? 7 : 6, + i <= 7 ? 8 : 7, + i <= 8 ? 9 : 8))); + } + + Assert.Equal(new _System.Tuple9("0", "1", "2", "3", "4", "5", "6", "7", "8"), t.DowncastClone(C, C, C, C, C, C, C, C, C)); + Assert.Equal(t, t.DowncastClone(I, I, I, I, I, I, I, I, I)); Assert.NotEqual(0, t.GetHashCode()); Assert.Equal("(0, 1, 2, 3, 4, 5, 6, 7, 8)", t.ToString()); Assert.Equal(t, _System.Tuple9.Default(0, 1, 2, 3, 4, 5, 6, 7, 8)); @@ -151,7 +285,24 @@ public void TestTuple9() { [Fact] public void TestTuple10() { var t = new _System.Tuple10(0, 1, 2, 3, 4, 5, 6, 7, 8, 9); - Assert.Equal(t, t.DowncastClone(C, C, C, C, C, C, C, C, C, C)); + Assert.False(t.Equals(null)); + for (var i = 0; i <= 10; i++) { + Assert.Equal(i == 10, t.Equals( + new _System.Tuple10( + i <= 0 ? 1 : 0, + i <= 1 ? 2 : 1, + i <= 2 ? 3 : 2, + i <= 3 ? 4 : 3, + i <= 4 ? 5 : 4, + i <= 5 ? 6 : 5, + i <= 6 ? 7 : 6, + i <= 7 ? 8 : 7, + i <= 8 ? 9 : 8, + i <= 9 ? 10 : 9))); + } + + Assert.Equal(new _System.Tuple10("0", "1", "2", "3", "4", "5", "6", "7", "8", "9"), t.DowncastClone(C, C, C, C, C, C, C, C, C, C)); + Assert.Equal(t, t.DowncastClone(I, I, I, I, I, I, I, I, I, I)); Assert.NotEqual(0, t.GetHashCode()); Assert.Equal("(0, 1, 2, 3, 4, 5, 6, 7, 8, 9)", t.ToString()); Assert.Equal(t, _System.Tuple10.Default(0, 1, 2, 3, 4, 5, 6, 7, 8, 9)); @@ -173,7 +324,25 @@ public void TestTuple10() { [Fact] public void TestTuple11() { var t = new _System.Tuple11(0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10); - Assert.Equal(t, t.DowncastClone(C, C, C, C, C, C, C, C, C, C, C)); + Assert.False(t.Equals(null)); + for (var i = 0; i <= 11; i++) { + Assert.Equal(i == 11, t.Equals( + new _System.Tuple11( + i <= 0 ? 1 : 0, + i <= 1 ? 2 : 1, + i <= 2 ? 3 : 2, + i <= 3 ? 4 : 3, + i <= 4 ? 5 : 4, + i <= 5 ? 6 : 5, + i <= 6 ? 7 : 6, + i <= 7 ? 8 : 7, + i <= 8 ? 9 : 8, + i <= 9 ? 10 : 9, + i <= 10 ? 11 : 10))); + } + + Assert.Equal(new _System.Tuple11("0", "1", "2", "3", "4", "5", "6", "7", "8", "9", "10"), t.DowncastClone(C, C, C, C, C, C, C, C, C, C, C)); + Assert.Equal(t, t.DowncastClone(I, I, I, I, I, I, I, I, I, I, I)); Assert.NotEqual(0, t.GetHashCode()); Assert.Equal("(0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10)", t.ToString()); Assert.Equal(t, _System.Tuple11.Default(0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10)); @@ -196,7 +365,26 @@ public void TestTuple11() { [Fact] public void TestTuple12() { var t = new _System.Tuple12(0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11); - Assert.Equal(t, t.DowncastClone(C, C, C, C, C, C, C, C, C, C, C, C)); + Assert.False(t.Equals(null)); + for (var i = 0; i <= 12; i++) { + Assert.Equal(i == 12, t.Equals( + new _System.Tuple12( + i <= 0 ? 1 : 0, + i <= 1 ? 2 : 1, + i <= 2 ? 3 : 2, + i <= 3 ? 4 : 3, + i <= 4 ? 5 : 4, + i <= 5 ? 6 : 5, + i <= 6 ? 7 : 6, + i <= 7 ? 8 : 7, + i <= 8 ? 9 : 8, + i <= 9 ? 10 : 9, + i <= 10 ? 11 : 10, + i <= 11 ? 12 : 11))); + } + + Assert.Equal(new _System.Tuple12("0", "1", "2", "3", "4", "5", "6", "7", "8", "9", "10", "11"), t.DowncastClone(C, C, C, C, C, C, C, C, C, C, C, C)); + Assert.Equal(t, t.DowncastClone(I, I, I, I, I, I, I, I, I, I, I, I)); Assert.NotEqual(0, t.GetHashCode()); Assert.Equal("(0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11)", t.ToString()); Assert.Equal(t, _System.Tuple12.Default(0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11)); @@ -220,7 +408,26 @@ public void TestTuple12() { [Fact] public void TestTuple13() { var t = new _System.Tuple13(0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12); - Assert.Equal(t, t.DowncastClone(C, C, C, C, C, C, C, C, C, C, C, C, C)); + Assert.False(t.Equals(null)); + for (var i = 0; i <= 13; i++) { + Assert.Equal(i == 13, t.Equals( + new _System.Tuple13( + i <= 0 ? 1 : 0, + i <= 1 ? 2 : 1, + i <= 2 ? 3 : 2, + i <= 3 ? 4 : 3, + i <= 4 ? 5 : 4, + i <= 5 ? 6 : 5, + i <= 6 ? 7 : 6, + i <= 7 ? 8 : 7, + i <= 8 ? 9 : 8, + i <= 9 ? 10 : 9, + i <= 10 ? 11 : 10, + i <= 11 ? 12 : 11, + i <= 12 ? 13 : 12))); + } + Assert.Equal(new _System.Tuple13("0", "1", "2", "3", "4", "5", "6", "7", "8", "9", "10", "11", "12"), t.DowncastClone(C, C, C, C, C, C, C, C, C, C, C, C, C)); + Assert.Equal(t, t.DowncastClone(I, I, I, I, I, I, I, I, I, I, I, I, I)); Assert.NotEqual(0, t.GetHashCode()); Assert.Equal("(0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12)", t.ToString()); Assert.Equal(t, _System.Tuple13.Default(0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12)); @@ -245,7 +452,28 @@ public void TestTuple13() { [Fact] public void TestTuple14() { var t = new _System.Tuple14(0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13); - Assert.Equal(t, t.DowncastClone(C, C, C, C, C, C, C, C, C, C, C, C, C, C)); + Assert.False(t.Equals(null)); + for (var i = 0; i <= 14; i++) { + Assert.Equal(i == 14, t.Equals( + new _System.Tuple14( + i <= 0 ? 1 : 0, + i <= 1 ? 2 : 1, + i <= 2 ? 3 : 2, + i <= 3 ? 4 : 3, + i <= 4 ? 5 : 4, + i <= 5 ? 6 : 5, + i <= 6 ? 7 : 6, + i <= 7 ? 8 : 7, + i <= 8 ? 9 : 8, + i <= 9 ? 10 : 9, + i <= 10 ? 11 : 10, + i <= 11 ? 12 : 11, + i <= 12 ? 13 : 12, + i <= 13 ? 14 : 13))); + } + + Assert.Equal(new _System.Tuple14("0", "1", "2", "3", "4", "5", "6", "7", "8", "9", "10", "11", "12", "13"), t.DowncastClone(C, C, C, C, C, C, C, C, C, C, C, C, C, C)); + Assert.Equal(t, t.DowncastClone(I, I, I, I, I, I, I, I, I, I, I, I, I, I)); Assert.NotEqual(0, t.GetHashCode()); Assert.Equal("(0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13)", t.ToString()); Assert.Equal(t, _System.Tuple14.Default(0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13)); @@ -271,7 +499,29 @@ public void TestTuple14() { [Fact] public void TestTuple15() { var t = new _System.Tuple15(0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14); - Assert.Equal(t, t.DowncastClone(C, C, C, C, C, C, C, C, C, C, C, C, C, C, C)); + Assert.False(t.Equals(null)); + for (var i = 0; i <= 15; i++) { + Assert.Equal(i == 15, t.Equals( + new _System.Tuple15( + i <= 0 ? 1 : 0, + i <= 1 ? 2 : 1, + i <= 2 ? 3 : 2, + i <= 3 ? 4 : 3, + i <= 4 ? 5 : 4, + i <= 5 ? 6 : 5, + i <= 6 ? 7 : 6, + i <= 7 ? 8 : 7, + i <= 8 ? 9 : 8, + i <= 9 ? 10 : 9, + i <= 10 ? 11 : 10, + i <= 11 ? 12 : 11, + i <= 12 ? 13 : 12, + i <= 13 ? 14 : 13, + i <= 14 ? 15 : 14))); + } + + Assert.Equal(new _System.Tuple15("0", "1", "2", "3", "4", "5", "6", "7", "8", "9", "10", "11", "12", "13", "14"), t.DowncastClone(C, C, C, C, C, C, C, C, C, C, C, C, C, C, C)); + Assert.Equal(t, t.DowncastClone(I, I, I, I, I, I, I, I, I, I, I, I, I, I, I)); Assert.NotEqual(0, t.GetHashCode()); Assert.Equal("(0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14)", t.ToString()); Assert.Equal(t, _System.Tuple15.Default(0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14)); @@ -297,7 +547,30 @@ public void TestTuple15() { [Fact] public void TestTuple16() { var t = new _System.Tuple16(0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15); - Assert.Equal(t, t.DowncastClone(C, C, C, C, C, C, C, C, C, C, C, C, C, C, C, C)); + Assert.False(t.Equals(null)); + for (var i = 0; i <= 16; i++) { + Assert.Equal(i == 16, t.Equals( + new _System.Tuple16( + i <= 0 ? 1 : 0, + i <= 1 ? 2 : 1, + i <= 2 ? 3 : 2, + i <= 3 ? 4 : 3, + i <= 4 ? 5 : 4, + i <= 5 ? 6 : 5, + i <= 6 ? 7 : 6, + i <= 7 ? 8 : 7, + i <= 8 ? 9 : 8, + i <= 9 ? 10 : 9, + i <= 10 ? 11 : 10, + i <= 11 ? 12 : 11, + i <= 12 ? 13 : 12, + i <= 13 ? 14 : 13, + i <= 14 ? 15 : 14, + i <= 15 ? 16 : 15))); + } + + Assert.Equal(new _System.Tuple16("0", "1", "2", "3", "4", "5", "6", "7", "8", "9", "10", "11", "12", "13", "14", "15"), t.DowncastClone(C, C, C, C, C, C, C, C, C, C, C, C, C, C, C, C)); + Assert.Equal(t, t.DowncastClone(I, I, I, I, I, I, I, I, I, I, I, I, I, I, I, I)); Assert.NotEqual(0, t.GetHashCode()); Assert.Equal("(0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15)", t.ToString()); Assert.Equal(t, _System.Tuple16.Default(0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15)); @@ -325,7 +598,31 @@ public void TestTuple16() { [Fact] public void TestTuple17() { var t = new _System.Tuple17(0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16); - Assert.Equal(t, t.DowncastClone(C, C, C, C, C, C, C, C, C, C, C, C, C, C, C, C, C)); + Assert.False(t.Equals(null)); + for (var i = 0; i <= 17; i++) { + Assert.Equal(i == 17, t.Equals( + new _System.Tuple17( + i <= 0 ? 1 : 0, + i <= 1 ? 2 : 1, + i <= 2 ? 3 : 2, + i <= 3 ? 4 : 3, + i <= 4 ? 5 : 4, + i <= 5 ? 6 : 5, + i <= 6 ? 7 : 6, + i <= 7 ? 8 : 7, + i <= 8 ? 9 : 8, + i <= 9 ? 10 : 9, + i <= 10 ? 11 : 10, + i <= 11 ? 12 : 11, + i <= 12 ? 13 : 12, + i <= 13 ? 14 : 13, + i <= 14 ? 15 : 14, + i <= 15 ? 16 : 15, + i <= 16 ? 17 : 16))); + } + + Assert.Equal(new _System.Tuple17("0", "1", "2", "3", "4", "5", "6", "7", "8", "9", "10", "11", "12", "13", "14", "15", "16"), t.DowncastClone(C, C, C, C, C, C, C, C, C, C, C, C, C, C, C, C, C)); + Assert.Equal(t, t.DowncastClone(I, I, I, I, I, I, I, I, I, I, I, I, I, I, I, I, I)); Assert.NotEqual(0, t.GetHashCode()); Assert.Equal("(0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16)", t.ToString()); Assert.Equal(t, _System.Tuple17.Default(0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16)); @@ -354,7 +651,32 @@ public void TestTuple17() { [Fact] public void TestTuple18() { var t = new _System.Tuple18(0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17); - Assert.Equal(t, t.DowncastClone(C, C, C, C, C, C, C, C, C, C, C, C, C, C, C, C, C, C)); + Assert.False(t.Equals(null)); + for (var i = 0; i <= 18; i++) { + Assert.Equal(i == 18, t.Equals( + new _System.Tuple18( + i <= 0 ? 1 : 0, + i <= 1 ? 2 : 1, + i <= 2 ? 3 : 2, + i <= 3 ? 4 : 3, + i <= 4 ? 5 : 4, + i <= 5 ? 6 : 5, + i <= 6 ? 7 : 6, + i <= 7 ? 8 : 7, + i <= 8 ? 9 : 8, + i <= 9 ? 10 : 9, + i <= 10 ? 11 : 10, + i <= 11 ? 12 : 11, + i <= 12 ? 13 : 12, + i <= 13 ? 14 : 13, + i <= 14 ? 15 : 14, + i <= 15 ? 16 : 15, + i <= 16 ? 17 : 16, + i <= 17 ? 18 : 17))); + } + + Assert.Equal(new _System.Tuple18("0", "1", "2", "3", "4", "5", "6", "7", "8", "9", "10", "11", "12", "13", "14", "15", "16", "17"), t.DowncastClone(C, C, C, C, C, C, C, C, C, C, C, C, C, C, C, C, C, C)); + Assert.Equal(t, t.DowncastClone(I, I, I, I, I, I, I, I, I, I, I, I, I, I, I, I, I, I)); Assert.NotEqual(0, t.GetHashCode()); Assert.Equal("(0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17)", t.ToString()); Assert.Equal(t, _System.Tuple18.Default(0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17)); @@ -384,7 +706,33 @@ public void TestTuple18() { [Fact] public void TestTuple19() { var t = new _System.Tuple19(0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18); - Assert.Equal(t, t.DowncastClone(C, C, C, C, C, C, C, C, C, C, C, C, C, C, C, C, C, C, C)); + Assert.False(t.Equals(null)); + for (var i = 0; i <= 19; i++) { + Assert.Equal(i == 19, t.Equals( + new _System.Tuple19( + i <= 0 ? 1 : 0, + i <= 1 ? 2 : 1, + i <= 2 ? 3 : 2, + i <= 3 ? 4 : 3, + i <= 4 ? 5 : 4, + i <= 5 ? 6 : 5, + i <= 6 ? 7 : 6, + i <= 7 ? 8 : 7, + i <= 8 ? 9 : 8, + i <= 9 ? 10 : 9, + i <= 10 ? 11 : 10, + i <= 11 ? 12 : 11, + i <= 12 ? 13 : 12, + i <= 13 ? 14 : 13, + i <= 14 ? 15 : 14, + i <= 15 ? 16 : 15, + i <= 16 ? 17 : 16, + i <= 17 ? 18 : 17, + i <= 18 ? 19 : 18))); + } + + Assert.Equal(new _System.Tuple19("0", "1", "2", "3", "4", "5", "6", "7", "8", "9", "10", "11", "12", "13", "14", "15", "16", "17", "18"), t.DowncastClone(C, C, C, C, C, C, C, C, C, C, C, C, C, C, C, C, C, C, C)); + Assert.Equal(t, t.DowncastClone(I, I, I, I, I, I, I, I, I, I, I, I, I, I, I, I, I, I, I)); Assert.NotEqual(0, t.GetHashCode()); Assert.Equal("(0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18)", t.ToString()); Assert.Equal(t, _System.Tuple19.Default(0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18)); @@ -415,7 +763,34 @@ public void TestTuple19() { [Fact] public void TestTuple20() { var t = new _System.Tuple20(0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19); - Assert.Equal(t, t.DowncastClone(C, C, C, C, C, C, C, C, C, C, C, C, C, C, C, C, C, C, C, C)); + Assert.False(t.Equals(null)); + for (var i = 0; i <= 20; i++) { + Assert.Equal(i == 20, t.Equals( + new _System.Tuple20( + i <= 0 ? 1 : 0, + i <= 1 ? 2 : 1, + i <= 2 ? 3 : 2, + i <= 3 ? 4 : 3, + i <= 4 ? 5 : 4, + i <= 5 ? 6 : 5, + i <= 6 ? 7 : 6, + i <= 7 ? 8 : 7, + i <= 8 ? 9 : 8, + i <= 9 ? 10 : 9, + i <= 10 ? 11 : 10, + i <= 11 ? 12 : 11, + i <= 12 ? 13 : 12, + i <= 13 ? 14 : 13, + i <= 14 ? 15 : 14, + i <= 15 ? 16 : 15, + i <= 16 ? 17 : 16, + i <= 17 ? 18 : 17, + i <= 18 ? 19 : 18, + i <= 19 ? 20 : 19))); + } + + Assert.Equal(new _System.Tuple20("0", "1", "2", "3", "4", "5", "6", "7", "8", "9", "10", "11", "12", "13", "14", "15", "16", "17", "18", "19"), t.DowncastClone(C, C, C, C, C, C, C, C, C, C, C, C, C, C, C, C, C, C, C, C)); + Assert.Equal(t, t.DowncastClone(I, I, I, I, I, I, I, I, I, I, I, I, I, I, I, I, I, I, I, I)); Assert.NotEqual(0, t.GetHashCode()); Assert.Equal("(0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19)", t.ToString()); Assert.Equal(t, _System.Tuple20.Default(0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19)); diff --git a/Source/DafnyRuntime/AssemblyInfo.cs b/Source/DafnyRuntime/AssemblyInfo.cs new file mode 100644 index 00000000000..0a7798c9929 --- /dev/null +++ b/Source/DafnyRuntime/AssemblyInfo.cs @@ -0,0 +1,2 @@ +using System.Runtime.CompilerServices; +[assembly: InternalsVisibleTo("DafnyRuntime.Tests")] \ No newline at end of file diff --git a/Source/DafnyRuntime/DafnyRuntime.cs b/Source/DafnyRuntime/DafnyRuntime.cs index ecb24f16fe4..675bd4155e3 100755 --- a/Source/DafnyRuntime/DafnyRuntime.cs +++ b/Source/DafnyRuntime/DafnyRuntime.cs @@ -1280,8 +1280,8 @@ public override int Count { internal class ConcatSequence : Sequence { // INVARIANT: Either left != null, right != null, and elmts's underlying array == null or // left == null, right == null, and elmts's underlying array != null - private volatile ISequence left, right; - private ImmutableArray elmts; + internal volatile ISequence left, right; + internal ImmutableArray elmts; private readonly int count; internal ConcatSequence(ISequence left, ISequence right) { @@ -1311,7 +1311,7 @@ public override int Count { } } - private ImmutableArray ComputeElements() { + internal ImmutableArray ComputeElements() { // Traverse the tree formed by all descendants which are ConcatSequences var ansBuilder = ImmutableArray.CreateBuilder(count); var toVisit = new Stack>(); diff --git a/Source/DafnyRuntime/DafnyRuntime.csproj b/Source/DafnyRuntime/DafnyRuntime.csproj index 153128a1d80..336bad0466b 100644 --- a/Source/DafnyRuntime/DafnyRuntime.csproj +++ b/Source/DafnyRuntime/DafnyRuntime.csproj @@ -25,7 +25,9 @@ - + + + PreserveNewest From d56a781f2401c0f00b097fa3629e0411f7fc6158 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Mika=C3=ABl=20Mayer?= Date: Mon, 9 Sep 2024 15:47:24 -0500 Subject: [PATCH 2/3] Update Source/DafnyRuntime.Tests/CsRuntimeTest.cs --- Source/DafnyRuntime.Tests/CsRuntimeTest.cs | 1 + 1 file changed, 1 insertion(+) diff --git a/Source/DafnyRuntime.Tests/CsRuntimeTest.cs b/Source/DafnyRuntime.Tests/CsRuntimeTest.cs index dbae79751fd..08f5c2a28ee 100644 --- a/Source/DafnyRuntime.Tests/CsRuntimeTest.cs +++ b/Source/DafnyRuntime.Tests/CsRuntimeTest.cs @@ -103,6 +103,7 @@ public void RuneTest() { Assert.Throws(() => Rune.Enumerate(input).ToList()); } + // The code below was partially generated by ChatGPT and reviewed manually. To regenerate this code, provide ChatGPT or any performant LLM with the first three tests and ask to generate the remaining. [Fact] public void DowncastClone0() { Func originalFunc = () => 42; From 5ad79caa64b8e664ca60542f9c322dc54a98d7b1 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Mika=C3=ABl=20Mayer?= Date: Mon, 9 Sep 2024 15:48:15 -0500 Subject: [PATCH 3/3] Apply suggestions from code review --- Source/DafnyRuntime.Tests/CsRuntimeTest.cs | 1 + Source/DafnyRuntime.Tests/TupleTest.cs | 1 + 2 files changed, 2 insertions(+) diff --git a/Source/DafnyRuntime.Tests/CsRuntimeTest.cs b/Source/DafnyRuntime.Tests/CsRuntimeTest.cs index 08f5c2a28ee..001d5ed93e1 100644 --- a/Source/DafnyRuntime.Tests/CsRuntimeTest.cs +++ b/Source/DafnyRuntime.Tests/CsRuntimeTest.cs @@ -228,6 +228,7 @@ public void DowncastClone16() { } + // The code was partially generated by ChatGPT and reviewed manually. To regenerate this code, provide ChatGPT or any performant LLM with the first three tests and ask to generate the remaining [Fact] public void InitNewArray1Test() { var a = ArrayHelpers.InitNewArray1('a', diff --git a/Source/DafnyRuntime.Tests/TupleTest.cs b/Source/DafnyRuntime.Tests/TupleTest.cs index ac047f3c50c..8373de145fc 100644 --- a/Source/DafnyRuntime.Tests/TupleTest.cs +++ b/Source/DafnyRuntime.Tests/TupleTest.cs @@ -9,6 +9,7 @@ public class TupleTests { public Func I = (int i) => i; public Dafny.TypeDescriptor D = new Dafny.TypeDescriptor(0); + // The code below was partially generated by ChatGPT and reviewed manually. To regenerate this code, provide ChatGPT or any performant LLM with the first three tests and ask to generate the remaining. [Fact] public void TestTuple0() { var t = new _System.Tuple0();