From 99d7e5ba751dc04fc73e5127e8bbace3e199ad0a Mon Sep 17 00:00:00 2001 From: Fabio Madge Date: Sun, 31 Aug 2025 03:53:10 +0200 Subject: [PATCH 01/11] feat: Stop boxing byte sequences in Go --- .../DafnyRuntimeGo-gomod/dafny/dafny.go | 134 ++++++++++++++---- .../DafnyRuntimeGo/dafny/dafny.go | 134 ++++++++++++++---- 2 files changed, 208 insertions(+), 60 deletions(-) diff --git a/Source/DafnyRuntime/DafnyRuntimeGo-gomod/dafny/dafny.go b/Source/DafnyRuntime/DafnyRuntimeGo-gomod/dafny/dafny.go index aca8225ea75..c9b87eedaef 100644 --- a/Source/DafnyRuntime/DafnyRuntimeGo-gomod/dafny/dafny.go +++ b/Source/DafnyRuntime/DafnyRuntimeGo-gomod/dafny/dafny.go @@ -82,15 +82,34 @@ func (_static *CompanionStruct_Sequence_) EqualUpTo(left Sequence, right Sequenc return true } - l := left.ToArray().(GoNativeArray).contents - r := right.ToArray().(GoNativeArray).contents - if IsEqualityComparable(l[0]) { - return slices.Equal(l[:index], r[:index]) - } else { - for i := uint32(0); i < index; i++ { - if !AreEqual(l[i], r[i]) { - return false + leftArr, rightArr := left.ToArray(), right.ToArray() + + // Fast path for ByteNativeArray + if l, ok := leftArr.(ByteNativeArray); ok { + if r, ok := rightArr.(ByteNativeArray); ok { + return slices.Equal(l.contents[:index], r.contents[:index]) + } + } + + // Fast path for GoNativeArray (preserve original optimization) + if l, ok := leftArr.(GoNativeArray); ok { + if r, ok := rightArr.(GoNativeArray); ok { + if IsEqualityComparable(l.contents[0]) { + return slices.Equal(l.contents[:index], r.contents[:index]) } + for i := uint32(0); i < index; i++ { + if !AreEqual(l.contents[i], r.contents[i]) { + return false + } + } + return true + } + } + + // Generic fallback + for i := uint32(0); i < index; i++ { + if !AreEqual(leftArr.Select(i), rightArr.Select(i)) { + return false } } return true @@ -531,24 +550,28 @@ var EmptySeq = SeqOf() // for the compiler to coerce the init function to a // func (uint32) interface{}. func SeqCreate(n uint32, init func(Int) interface{}) Sequence { + if seq, ok := tryByteSeqInit(n, init); ok { + return seq + } return Companion_Sequence_.Create(n, func(index uint32) interface{} { return init(IntOfUint32(index)) }) } func SeqFromArray(contents []interface{}, isString bool) Sequence { - arr := GoNativeArray{ - contents: contents, + if seq, ok := tryByteSeq(contents); ok && !isString { + return seq } result := New_ArraySequence_() - result.Ctor__(arr, isString) + result.Ctor__(GoNativeArray{contents: contents}, isString) return result } // SeqOf returns a sequence containing the given values. func SeqOf(values ...interface{}) Sequence { - // Making a defensive copy here because variadic functions can get hinky - // if someone says SeqOf(slice...) and then mutates slice. + if seq, ok := tryByteSeq(values); ok { + return seq + } arr := make([]interface{}, len(values)) copy(arr, values) return SeqFromArray(arr, false) @@ -564,11 +587,7 @@ func SeqOfChars(values ...Char) Sequence { } func SeqOfBytes(values []byte) Sequence { - arr := make([]interface{}, len(values)) - for i, v := range values { - arr[i] = v - } - return SeqFromArray(arr, false) + return newByteSeq(values) } // SeqOfString converts the given string into a sequence of characters. @@ -734,18 +753,73 @@ func (seq *LazySequence) ToByteArray() []byte { } func ToByteArray(x Sequence) []byte { - nativeArray := x.ToArray().(GoNativeArray) - arr := make([]byte, len(nativeArray.contents)) - for i, v := range nativeArray.contents { - arr[i] = v.(byte) + if arr, ok := x.ToArray().(ByteNativeArray); ok { + return arr.contents } - return arr + arr := x.ToArray() + result := make([]byte, arr.Length()) + for i := uint32(0); i < arr.Length(); i++ { + result[i] = arr.Select(i).(byte) + } + return result } /****************************************************************************** * Arrays ******************************************************************************/ +// ByteNativeArray - optimized for uint8 sequences +type ByteNativeArray struct{ contents []byte } + +func (a ByteNativeArray) Length() uint32 { return uint32(len(a.contents)) } +func (a ByteNativeArray) Select(i uint32) interface{} { return a.contents[i] } +func (a ByteNativeArray) Update(i uint32, t interface{}) { a.contents[i] = t.(uint8) } +func (a ByteNativeArray) UpdateSubarray(i uint32, other ImmutableArray) { + for j := uint32(0); j < other.Length(); j++ { + a.contents[i+j] = other.Select(j).(uint8) + } +} +func (a ByteNativeArray) Freeze(size uint32) ImmutableArray { return a.Subarray(0, size) } +func (a ByteNativeArray) Subarray(lo, hi uint32) ImmutableArray { + return ByteNativeArray{contents: a.contents[lo:hi]} +} +func (a ByteNativeArray) String() string { return "ByteNativeArray" } + +// Helper to create byte sequences +func newByteSeq(data []byte) Sequence { + result := New_ArraySequence_() + result.Ctor__(ByteNativeArray{contents: data}, false) + return result +} + +// Helper to try creating optimized uint8 sequence from slice +func tryByteSeq(contents []interface{}) (Sequence, bool) { + if len(contents) > 0 { + if _, ok := contents[0].(uint8); ok { + data := make([]byte, len(contents)) + for i, v := range contents { + data[i] = v.(uint8) + } + return newByteSeq(data), true + } + } + return nil, false +} + +// Helper to try creating optimized uint8 sequence from init function +func tryByteSeqInit(n uint32, init func(Int) interface{}) (Sequence, bool) { + if n > 0 { + if _, ok := init(Zero).(uint8); ok { + data := make([]byte, n) + for i := uint32(0); i < n; i++ { + data[i] = init(IntOfUint32(i)).(uint8) + } + return newByteSeq(data), true + } + } + return nil, false +} + // A GoNativeArray is a single dimensional Go slice, // wrapped up for the benefit of dafnyRuntime.dfy. // We should refactor to wrap an Array interface as defined below @@ -772,12 +846,11 @@ func (CompanionStruct_NativeArray_) MakeWithInit(length uint32, init func(uint32 } func (CompanionStruct_NativeArray_) Copy(other ImmutableArray) NativeArray { - otherArray := other.(GoNativeArray) - contents := make([]interface{}, otherArray.Length()) - copy(contents, otherArray.contents) - return GoNativeArray{ - contents: contents, + contents := make([]interface{}, other.Length()) + for i := uint32(0); i < other.Length(); i++ { + contents[i] = other.Select(i) } + return GoNativeArray{contents: contents} } func (array GoNativeArray) Length() uint32 { @@ -793,8 +866,9 @@ func (array GoNativeArray) Update(i uint32, t interface{}) { } func (array GoNativeArray) UpdateSubarray(i uint32, other ImmutableArray) { - otherArray := other.(GoNativeArray) - copy(array.contents[i:(i+otherArray.Length())], otherArray.contents) + for j := uint32(0); j < other.Length(); j++ { + array.contents[i+j] = other.Select(j) + } } func (array GoNativeArray) Freeze(size uint32) ImmutableArray { diff --git a/Source/DafnyRuntime/DafnyRuntimeGo/dafny/dafny.go b/Source/DafnyRuntime/DafnyRuntimeGo/dafny/dafny.go index aca8225ea75..c9b87eedaef 100644 --- a/Source/DafnyRuntime/DafnyRuntimeGo/dafny/dafny.go +++ b/Source/DafnyRuntime/DafnyRuntimeGo/dafny/dafny.go @@ -82,15 +82,34 @@ func (_static *CompanionStruct_Sequence_) EqualUpTo(left Sequence, right Sequenc return true } - l := left.ToArray().(GoNativeArray).contents - r := right.ToArray().(GoNativeArray).contents - if IsEqualityComparable(l[0]) { - return slices.Equal(l[:index], r[:index]) - } else { - for i := uint32(0); i < index; i++ { - if !AreEqual(l[i], r[i]) { - return false + leftArr, rightArr := left.ToArray(), right.ToArray() + + // Fast path for ByteNativeArray + if l, ok := leftArr.(ByteNativeArray); ok { + if r, ok := rightArr.(ByteNativeArray); ok { + return slices.Equal(l.contents[:index], r.contents[:index]) + } + } + + // Fast path for GoNativeArray (preserve original optimization) + if l, ok := leftArr.(GoNativeArray); ok { + if r, ok := rightArr.(GoNativeArray); ok { + if IsEqualityComparable(l.contents[0]) { + return slices.Equal(l.contents[:index], r.contents[:index]) } + for i := uint32(0); i < index; i++ { + if !AreEqual(l.contents[i], r.contents[i]) { + return false + } + } + return true + } + } + + // Generic fallback + for i := uint32(0); i < index; i++ { + if !AreEqual(leftArr.Select(i), rightArr.Select(i)) { + return false } } return true @@ -531,24 +550,28 @@ var EmptySeq = SeqOf() // for the compiler to coerce the init function to a // func (uint32) interface{}. func SeqCreate(n uint32, init func(Int) interface{}) Sequence { + if seq, ok := tryByteSeqInit(n, init); ok { + return seq + } return Companion_Sequence_.Create(n, func(index uint32) interface{} { return init(IntOfUint32(index)) }) } func SeqFromArray(contents []interface{}, isString bool) Sequence { - arr := GoNativeArray{ - contents: contents, + if seq, ok := tryByteSeq(contents); ok && !isString { + return seq } result := New_ArraySequence_() - result.Ctor__(arr, isString) + result.Ctor__(GoNativeArray{contents: contents}, isString) return result } // SeqOf returns a sequence containing the given values. func SeqOf(values ...interface{}) Sequence { - // Making a defensive copy here because variadic functions can get hinky - // if someone says SeqOf(slice...) and then mutates slice. + if seq, ok := tryByteSeq(values); ok { + return seq + } arr := make([]interface{}, len(values)) copy(arr, values) return SeqFromArray(arr, false) @@ -564,11 +587,7 @@ func SeqOfChars(values ...Char) Sequence { } func SeqOfBytes(values []byte) Sequence { - arr := make([]interface{}, len(values)) - for i, v := range values { - arr[i] = v - } - return SeqFromArray(arr, false) + return newByteSeq(values) } // SeqOfString converts the given string into a sequence of characters. @@ -734,18 +753,73 @@ func (seq *LazySequence) ToByteArray() []byte { } func ToByteArray(x Sequence) []byte { - nativeArray := x.ToArray().(GoNativeArray) - arr := make([]byte, len(nativeArray.contents)) - for i, v := range nativeArray.contents { - arr[i] = v.(byte) + if arr, ok := x.ToArray().(ByteNativeArray); ok { + return arr.contents } - return arr + arr := x.ToArray() + result := make([]byte, arr.Length()) + for i := uint32(0); i < arr.Length(); i++ { + result[i] = arr.Select(i).(byte) + } + return result } /****************************************************************************** * Arrays ******************************************************************************/ +// ByteNativeArray - optimized for uint8 sequences +type ByteNativeArray struct{ contents []byte } + +func (a ByteNativeArray) Length() uint32 { return uint32(len(a.contents)) } +func (a ByteNativeArray) Select(i uint32) interface{} { return a.contents[i] } +func (a ByteNativeArray) Update(i uint32, t interface{}) { a.contents[i] = t.(uint8) } +func (a ByteNativeArray) UpdateSubarray(i uint32, other ImmutableArray) { + for j := uint32(0); j < other.Length(); j++ { + a.contents[i+j] = other.Select(j).(uint8) + } +} +func (a ByteNativeArray) Freeze(size uint32) ImmutableArray { return a.Subarray(0, size) } +func (a ByteNativeArray) Subarray(lo, hi uint32) ImmutableArray { + return ByteNativeArray{contents: a.contents[lo:hi]} +} +func (a ByteNativeArray) String() string { return "ByteNativeArray" } + +// Helper to create byte sequences +func newByteSeq(data []byte) Sequence { + result := New_ArraySequence_() + result.Ctor__(ByteNativeArray{contents: data}, false) + return result +} + +// Helper to try creating optimized uint8 sequence from slice +func tryByteSeq(contents []interface{}) (Sequence, bool) { + if len(contents) > 0 { + if _, ok := contents[0].(uint8); ok { + data := make([]byte, len(contents)) + for i, v := range contents { + data[i] = v.(uint8) + } + return newByteSeq(data), true + } + } + return nil, false +} + +// Helper to try creating optimized uint8 sequence from init function +func tryByteSeqInit(n uint32, init func(Int) interface{}) (Sequence, bool) { + if n > 0 { + if _, ok := init(Zero).(uint8); ok { + data := make([]byte, n) + for i := uint32(0); i < n; i++ { + data[i] = init(IntOfUint32(i)).(uint8) + } + return newByteSeq(data), true + } + } + return nil, false +} + // A GoNativeArray is a single dimensional Go slice, // wrapped up for the benefit of dafnyRuntime.dfy. // We should refactor to wrap an Array interface as defined below @@ -772,12 +846,11 @@ func (CompanionStruct_NativeArray_) MakeWithInit(length uint32, init func(uint32 } func (CompanionStruct_NativeArray_) Copy(other ImmutableArray) NativeArray { - otherArray := other.(GoNativeArray) - contents := make([]interface{}, otherArray.Length()) - copy(contents, otherArray.contents) - return GoNativeArray{ - contents: contents, + contents := make([]interface{}, other.Length()) + for i := uint32(0); i < other.Length(); i++ { + contents[i] = other.Select(i) } + return GoNativeArray{contents: contents} } func (array GoNativeArray) Length() uint32 { @@ -793,8 +866,9 @@ func (array GoNativeArray) Update(i uint32, t interface{}) { } func (array GoNativeArray) UpdateSubarray(i uint32, other ImmutableArray) { - otherArray := other.(GoNativeArray) - copy(array.contents[i:(i+otherArray.Length())], otherArray.contents) + for j := uint32(0); j < other.Length(); j++ { + array.contents[i+j] = other.Select(j) + } } func (array GoNativeArray) Freeze(size uint32) ImmutableArray { From 5670e52edaddce64acb8389247db641f68b517d1 Mon Sep 17 00:00:00 2001 From: Fabio Madge Date: Wed, 3 Sep 2025 02:42:59 +0200 Subject: [PATCH 02/11] review --- .../DafnyRuntimeGo-gomod/dafny/dafny.go | 195 ++++++++++++------ .../DafnyRuntimeGo-gomod/dafny/dafny_test.go | 124 ++++++++++- .../DafnyRuntimeGo/dafny/dafny.go | 195 ++++++++++++------ .../DafnyRuntimeGo/dafny/dafny_test.go | 172 ++++++++++++--- 4 files changed, 524 insertions(+), 162 deletions(-) diff --git a/Source/DafnyRuntime/DafnyRuntimeGo-gomod/dafny/dafny.go b/Source/DafnyRuntime/DafnyRuntimeGo-gomod/dafny/dafny.go index c9b87eedaef..f3a2979cf43 100644 --- a/Source/DafnyRuntime/DafnyRuntimeGo-gomod/dafny/dafny.go +++ b/Source/DafnyRuntime/DafnyRuntimeGo-gomod/dafny/dafny.go @@ -84,21 +84,23 @@ func (_static *CompanionStruct_Sequence_) EqualUpTo(left Sequence, right Sequenc leftArr, rightArr := left.ToArray(), right.ToArray() - // Fast path for ByteNativeArray + // Fast path for ByteNativeArray (byte sequence optimization) if l, ok := leftArr.(ByteNativeArray); ok { if r, ok := rightArr.(ByteNativeArray); ok { - return slices.Equal(l.contents[:index], r.contents[:index]) + return slices.Equal(l.underlying.contents[:index], r.underlying.contents[:index]) } } // Fast path for GoNativeArray (preserve original optimization) if l, ok := leftArr.(GoNativeArray); ok { if r, ok := rightArr.(GoNativeArray); ok { - if IsEqualityComparable(l.contents[0]) { - return slices.Equal(l.contents[:index], r.contents[:index]) + lSlice := l.underlying.anySlice(Zero, IntOfUint32(index)) + rSlice := r.underlying.anySlice(Zero, IntOfUint32(index)) + if len(lSlice) > 0 && IsEqualityComparable(lSlice[0]) { + return slices.Equal(lSlice, rSlice) } for i := uint32(0); i < index; i++ { - if !AreEqual(l.contents[i], r.contents[i]) { + if !AreEqual(lSlice[i], rSlice[i]) { return false } } @@ -563,7 +565,8 @@ func SeqFromArray(contents []interface{}, isString bool) Sequence { return seq } result := New_ArraySequence_() - result.Ctor__(GoNativeArray{contents: contents}, isString) + underlying := &arrayStruct{contents: contents, dims: []int{len(contents)}} + result.Ctor__(GoNativeArray{underlying: underlying}, isString) return result } @@ -754,7 +757,7 @@ func (seq *LazySequence) ToByteArray() []byte { func ToByteArray(x Sequence) []byte { if arr, ok := x.ToArray().(ByteNativeArray); ok { - return arr.contents + return arr.underlying.contents } arr := x.ToArray() result := make([]byte, arr.Length()) @@ -768,31 +771,100 @@ func ToByteArray(x Sequence) []byte { * Arrays ******************************************************************************/ -// ByteNativeArray - optimized for uint8 sequences -type ByteNativeArray struct{ contents []byte } +/****************************************************************************** + * Arrays + ******************************************************************************/ + +// GoNativeArray wraps the Array interface for external compatibility +// while allowing optimized implementations internally +type GoNativeArray struct { + underlying Array +} + +// GoNativeArray methods delegate to underlying Array implementation +func (g GoNativeArray) Length() uint32 { + return uint32(g.underlying.dimensionLength(0)) +} -func (a ByteNativeArray) Length() uint32 { return uint32(len(a.contents)) } -func (a ByteNativeArray) Select(i uint32) interface{} { return a.contents[i] } -func (a ByteNativeArray) Update(i uint32, t interface{}) { a.contents[i] = t.(uint8) } -func (a ByteNativeArray) UpdateSubarray(i uint32, other ImmutableArray) { +func (g GoNativeArray) Select(i uint32) interface{} { + return g.underlying.ArrayGet1(int(i)) +} + +func (g GoNativeArray) Update(i uint32, t interface{}) { + g.underlying.ArraySet1(t, int(i)) +} + +func (g GoNativeArray) UpdateSubarray(i uint32, other ImmutableArray) { for j := uint32(0); j < other.Length(); j++ { - a.contents[i+j] = other.Select(j).(uint8) + g.underlying.ArraySet1(other.Select(j), int(i+j)) + } +} + +func (g GoNativeArray) Freeze(size uint32) ImmutableArray { + return g.Subarray(0, size) +} + +func (g GoNativeArray) Subarray(lo, hi uint32) ImmutableArray { + slice := g.underlying.anySlice(IntOfUint32(lo), IntOfUint32(hi)) + return GoNativeArray{underlying: &arrayStruct{contents: slice, dims: []int{len(slice)}}} +} + +func (g GoNativeArray) String() string { + return "dafny.GoNativeArray" +} + +// ByteNativeArray wraps arrayForByte for byte sequence optimization +type ByteNativeArray struct { + underlying *arrayForByte +} + +func (b ByteNativeArray) Length() uint32 { + return uint32(b.underlying.dimensionLength(0)) +} + +func (b ByteNativeArray) Select(i uint32) interface{} { + return b.underlying.ArrayGet1Byte(int(i)) +} + +func (b ByteNativeArray) Update(i uint32, t interface{}) { + b.underlying.ArraySet1Byte(t.(uint8), int(i)) +} + +func (b ByteNativeArray) UpdateSubarray(i uint32, other ImmutableArray) { + // Fast path for ByteNativeArray + if otherByte, ok := other.(ByteNativeArray); ok { + copy(b.underlying.contents[i:], otherByte.underlying.contents) + } else { + for j := uint32(0); j < other.Length(); j++ { + b.underlying.ArraySet1Byte(other.Select(j).(uint8), int(i+j)) + } } } -func (a ByteNativeArray) Freeze(size uint32) ImmutableArray { return a.Subarray(0, size) } -func (a ByteNativeArray) Subarray(lo, hi uint32) ImmutableArray { - return ByteNativeArray{contents: a.contents[lo:hi]} + +func (b ByteNativeArray) Freeze(size uint32) ImmutableArray { + return b.Subarray(0, size) +} + +func (b ByteNativeArray) Subarray(lo, hi uint32) ImmutableArray { + return ByteNativeArray{underlying: &arrayForByte{ + contents: b.underlying.contents[lo:hi], + dims: []int{int(hi - lo)}, + }} +} + +func (b ByteNativeArray) String() string { + return "dafny.ByteNativeArray" } -func (a ByteNativeArray) String() string { return "ByteNativeArray" } -// Helper to create byte sequences +// Helper to create byte sequences using ByteNativeArray wrapper func newByteSeq(data []byte) Sequence { result := New_ArraySequence_() - result.Ctor__(ByteNativeArray{contents: data}, false) + underlying := &arrayForByte{contents: data, dims: []int{len(data)}} + result.Ctor__(ByteNativeArray{underlying: underlying}, false) return result } -// Helper to try creating optimized uint8 sequence from slice +// Helper to try creating optimized uint8 sequence func tryByteSeq(contents []interface{}) (Sequence, bool) { if len(contents) > 0 { if _, ok := contents[0].(uint8); ok { @@ -820,69 +892,56 @@ func tryByteSeqInit(n uint32, init func(Int) interface{}) (Sequence, bool) { return nil, false } -// A GoNativeArray is a single dimensional Go slice, -// wrapped up for the benefit of dafnyRuntime.dfy. -// We should refactor to wrap an Array interface as defined below -// to get the same optimization benefits for sequences of bytes and chars/CodePoints. -type GoNativeArray struct { - contents []interface{} -} - -func (CompanionStruct_NativeArray_) Make(length uint32) NativeArray { - contents := make([]interface{}, length) - return GoNativeArray{ - contents: contents, +// CompanionStruct_NativeArray_ functions work with Array interface through GoNativeArray wrapper +func (CompanionStruct_NativeArray_) Make(length uint32) ImmutableArray { + underlying := &arrayStruct{ + contents: make([]interface{}, length), + dims: []int{int(length)}, } + return GoNativeArray{underlying: underlying} } -func (CompanionStruct_NativeArray_) MakeWithInit(length uint32, init func(uint32) interface{}) NativeArray { +func (CompanionStruct_NativeArray_) MakeWithInit(length uint32, init func(uint32) interface{}) ImmutableArray { contents := make([]interface{}, length) for i := uint32(0); i < length; i++ { contents[i] = init(i) } - return GoNativeArray{ + underlying := &arrayStruct{ contents: contents, + dims: []int{int(length)}, } + return GoNativeArray{underlying: underlying} } -func (CompanionStruct_NativeArray_) Copy(other ImmutableArray) NativeArray { - contents := make([]interface{}, other.Length()) - for i := uint32(0); i < other.Length(); i++ { - contents[i] = other.Select(i) +func (CompanionStruct_NativeArray_) Copy(other ImmutableArray) ImmutableArray { + // Fast path: if it's already a GoNativeArray, use the underlying Array + if goArray, ok := other.(GoNativeArray); ok { + slice := goArray.underlying.anySlice(Zero, IntOfUint32(other.Length())) + underlying := &arrayStruct{ + contents: append([]interface{}(nil), slice...), + dims: []int{len(slice)}, + } + return GoNativeArray{underlying: underlying} } - return GoNativeArray{contents: contents} -} - -func (array GoNativeArray) Length() uint32 { - return uint32(len(array.contents)) -} - -func (array GoNativeArray) Select(i uint32) interface{} { - return array.contents[i] -} - -func (array GoNativeArray) Update(i uint32, t interface{}) { - array.contents[i] = t -} -func (array GoNativeArray) UpdateSubarray(i uint32, other ImmutableArray) { - for j := uint32(0); j < other.Length(); j++ { - array.contents[i+j] = other.Select(j) + // Fast path: if it's a ByteNativeArray, copy efficiently + if byteArray, ok := other.(ByteNativeArray); ok { + data := make([]byte, len(byteArray.underlying.contents)) + copy(data, byteArray.underlying.contents) + underlying := &arrayForByte{contents: data, dims: []int{len(data)}} + return ByteNativeArray{underlying: underlying} } -} - -func (array GoNativeArray) Freeze(size uint32) ImmutableArray { - return array.Subarray(0, size) -} -func (array GoNativeArray) Subarray(lo uint32, hi uint32) ImmutableArray { - return GoNativeArray{ - contents: array.contents[lo:hi], + // Generic path: copy through interface + contents := make([]interface{}, other.Length()) + for i := uint32(0); i < other.Length(); i++ { + contents[i] = other.Select(i) } -} - -func (array GoNativeArray) String() string { - return "dafny.GoNativeArray" + underlying := &arrayStruct{ + contents: contents, + dims: []int{len(contents)}, + } + return GoNativeArray{underlying: underlying} } // Array is the general interface for arrays. Conceptually, it contains some diff --git a/Source/DafnyRuntime/DafnyRuntimeGo-gomod/dafny/dafny_test.go b/Source/DafnyRuntime/DafnyRuntimeGo-gomod/dafny/dafny_test.go index d2d73049353..23c1f273b45 100644 --- a/Source/DafnyRuntime/DafnyRuntimeGo-gomod/dafny/dafny_test.go +++ b/Source/DafnyRuntime/DafnyRuntimeGo-gomod/dafny/dafny_test.go @@ -12,7 +12,11 @@ func TestArraySequence(t *testing.T) { } func MakeArraySequence() Sequence { - arr := GoNativeArray{} + underlying := &arrayStruct{ + contents: []interface{}{}, + dims: []int{0}, + } + arr := GoNativeArray{underlying: underlying} arrSeq := New_ArraySequence_() arrSeq.Ctor__(arr, false) return arrSeq @@ -37,6 +41,124 @@ func TestLazySequence(t *testing.T) { AssertImplementsSequence(lazySeq, t) } +// Test byte sequence optimization using ByteNativeArray wrapper +func TestByteSequenceOptimization(t *testing.T) { + // Test creating byte sequence from slice + data := []byte{1, 2, 3, 4, 5} + seq := newByteSeq(data) + + // Verify it implements Sequence interface + AssertImplementsSequence(seq, t) + + // Verify ToArray returns ByteNativeArray + arr := seq.ToArray() + if byteArr, ok := arr.(ByteNativeArray); ok { + if byteArr.Length() != 5 { + t.Errorf("Expected length 5, got %d", byteArr.Length()) + } + if byteArr.Select(0).(uint8) != 1 { + t.Errorf("Expected first element 1, got %v", byteArr.Select(0)) + } + } else { + t.Errorf("Expected ByteNativeArray, got %T", arr) + } +} + +// Test optimization detection for uint8 vs non-uint8 +func TestTryByteSeq(t *testing.T) { + // Test uint8 slice - should optimize + uint8Contents := []interface{}{uint8(1), uint8(2), uint8(3)} + seq, optimized := tryByteSeq(uint8Contents) + if !optimized { + t.Error("Expected optimization for uint8 slice") + } + if seq == nil { + t.Error("Expected non-nil sequence") + } + + // Verify it returns ByteNativeArray + arr := seq.ToArray() + if _, ok := arr.(ByteNativeArray); !ok { + t.Errorf("Expected ByteNativeArray, got %T", arr) + } + + // Test non-uint8 slice - should not optimize + intContents := []interface{}{1, 2, 3} + seq2, optimized2 := tryByteSeq(intContents) + if optimized2 { + t.Error("Expected no optimization for int slice") + } + if seq2 != nil { + t.Error("Expected nil sequence for non-optimized case") + } + + // Test empty slice - should not optimize + emptyContents := []interface{}{} + seq3, optimized3 := tryByteSeq(emptyContents) + if optimized3 { + t.Error("Expected no optimization for empty slice") + } + if seq3 != nil { + t.Error("Expected nil sequence for empty case") + } +} + +// Test refactored CompanionStruct_NativeArray_ functions +func TestNativeArrayFunctions(t *testing.T) { + // Test Make function + arr := Companion_NativeArray_.Make(3) + if goArr, ok := arr.(GoNativeArray); ok { + if goArr.Length() != 3 { + t.Errorf("Expected length 3, got %d", goArr.Length()) + } + } else { + t.Errorf("Expected GoNativeArray, got %T", arr) + } + + // Test MakeWithInit function + initFunc := func(i uint32) interface{} { return int(i * 2) } + arr2 := Companion_NativeArray_.MakeWithInit(3, initFunc) + if goArr2, ok := arr2.(GoNativeArray); ok { + if goArr2.Length() != 3 { + t.Errorf("Expected length 3, got %d", goArr2.Length()) + } + if goArr2.Select(1) != 2 { + t.Errorf("Expected element at index 1 to be 2, got %v", goArr2.Select(1)) + } + } else { + t.Errorf("Expected GoNativeArray, got %T", arr2) + } + + // Test Copy function with GoNativeArray + arr3 := Companion_NativeArray_.Copy(arr2) + if goArr3, ok := arr3.(GoNativeArray); ok { + if goArr3.Length() != 3 { + t.Errorf("Expected length 3, got %d", goArr3.Length()) + } + if goArr3.Select(1) != 2 { + t.Errorf("Expected element at index 1 to be 2, got %v", goArr3.Select(1)) + } + } else { + t.Errorf("Expected GoNativeArray, got %T", arr3) + } + + // Test Copy function with ByteNativeArray + data := []byte{10, 20, 30} + byteSeq := newByteSeq(data) + byteArr := byteSeq.ToArray() + arr4 := Companion_NativeArray_.Copy(byteArr) + if byteArr4, ok := arr4.(ByteNativeArray); ok { + if byteArr4.Length() != 3 { + t.Errorf("Expected length 3, got %d", byteArr4.Length()) + } + if byteArr4.Select(1).(uint8) != 20 { + t.Errorf("Expected element at index 1 to be 20, got %v", byteArr4.Select(1)) + } + } else { + t.Errorf("Expected ByteNativeArray, got %T", arr4) + } +} + func AssertImplementsSequence(s interface{}, t *testing.T) { _, ok := s.(Sequence) if !ok { diff --git a/Source/DafnyRuntime/DafnyRuntimeGo/dafny/dafny.go b/Source/DafnyRuntime/DafnyRuntimeGo/dafny/dafny.go index c9b87eedaef..f3a2979cf43 100644 --- a/Source/DafnyRuntime/DafnyRuntimeGo/dafny/dafny.go +++ b/Source/DafnyRuntime/DafnyRuntimeGo/dafny/dafny.go @@ -84,21 +84,23 @@ func (_static *CompanionStruct_Sequence_) EqualUpTo(left Sequence, right Sequenc leftArr, rightArr := left.ToArray(), right.ToArray() - // Fast path for ByteNativeArray + // Fast path for ByteNativeArray (byte sequence optimization) if l, ok := leftArr.(ByteNativeArray); ok { if r, ok := rightArr.(ByteNativeArray); ok { - return slices.Equal(l.contents[:index], r.contents[:index]) + return slices.Equal(l.underlying.contents[:index], r.underlying.contents[:index]) } } // Fast path for GoNativeArray (preserve original optimization) if l, ok := leftArr.(GoNativeArray); ok { if r, ok := rightArr.(GoNativeArray); ok { - if IsEqualityComparable(l.contents[0]) { - return slices.Equal(l.contents[:index], r.contents[:index]) + lSlice := l.underlying.anySlice(Zero, IntOfUint32(index)) + rSlice := r.underlying.anySlice(Zero, IntOfUint32(index)) + if len(lSlice) > 0 && IsEqualityComparable(lSlice[0]) { + return slices.Equal(lSlice, rSlice) } for i := uint32(0); i < index; i++ { - if !AreEqual(l.contents[i], r.contents[i]) { + if !AreEqual(lSlice[i], rSlice[i]) { return false } } @@ -563,7 +565,8 @@ func SeqFromArray(contents []interface{}, isString bool) Sequence { return seq } result := New_ArraySequence_() - result.Ctor__(GoNativeArray{contents: contents}, isString) + underlying := &arrayStruct{contents: contents, dims: []int{len(contents)}} + result.Ctor__(GoNativeArray{underlying: underlying}, isString) return result } @@ -754,7 +757,7 @@ func (seq *LazySequence) ToByteArray() []byte { func ToByteArray(x Sequence) []byte { if arr, ok := x.ToArray().(ByteNativeArray); ok { - return arr.contents + return arr.underlying.contents } arr := x.ToArray() result := make([]byte, arr.Length()) @@ -768,31 +771,100 @@ func ToByteArray(x Sequence) []byte { * Arrays ******************************************************************************/ -// ByteNativeArray - optimized for uint8 sequences -type ByteNativeArray struct{ contents []byte } +/****************************************************************************** + * Arrays + ******************************************************************************/ + +// GoNativeArray wraps the Array interface for external compatibility +// while allowing optimized implementations internally +type GoNativeArray struct { + underlying Array +} + +// GoNativeArray methods delegate to underlying Array implementation +func (g GoNativeArray) Length() uint32 { + return uint32(g.underlying.dimensionLength(0)) +} -func (a ByteNativeArray) Length() uint32 { return uint32(len(a.contents)) } -func (a ByteNativeArray) Select(i uint32) interface{} { return a.contents[i] } -func (a ByteNativeArray) Update(i uint32, t interface{}) { a.contents[i] = t.(uint8) } -func (a ByteNativeArray) UpdateSubarray(i uint32, other ImmutableArray) { +func (g GoNativeArray) Select(i uint32) interface{} { + return g.underlying.ArrayGet1(int(i)) +} + +func (g GoNativeArray) Update(i uint32, t interface{}) { + g.underlying.ArraySet1(t, int(i)) +} + +func (g GoNativeArray) UpdateSubarray(i uint32, other ImmutableArray) { for j := uint32(0); j < other.Length(); j++ { - a.contents[i+j] = other.Select(j).(uint8) + g.underlying.ArraySet1(other.Select(j), int(i+j)) + } +} + +func (g GoNativeArray) Freeze(size uint32) ImmutableArray { + return g.Subarray(0, size) +} + +func (g GoNativeArray) Subarray(lo, hi uint32) ImmutableArray { + slice := g.underlying.anySlice(IntOfUint32(lo), IntOfUint32(hi)) + return GoNativeArray{underlying: &arrayStruct{contents: slice, dims: []int{len(slice)}}} +} + +func (g GoNativeArray) String() string { + return "dafny.GoNativeArray" +} + +// ByteNativeArray wraps arrayForByte for byte sequence optimization +type ByteNativeArray struct { + underlying *arrayForByte +} + +func (b ByteNativeArray) Length() uint32 { + return uint32(b.underlying.dimensionLength(0)) +} + +func (b ByteNativeArray) Select(i uint32) interface{} { + return b.underlying.ArrayGet1Byte(int(i)) +} + +func (b ByteNativeArray) Update(i uint32, t interface{}) { + b.underlying.ArraySet1Byte(t.(uint8), int(i)) +} + +func (b ByteNativeArray) UpdateSubarray(i uint32, other ImmutableArray) { + // Fast path for ByteNativeArray + if otherByte, ok := other.(ByteNativeArray); ok { + copy(b.underlying.contents[i:], otherByte.underlying.contents) + } else { + for j := uint32(0); j < other.Length(); j++ { + b.underlying.ArraySet1Byte(other.Select(j).(uint8), int(i+j)) + } } } -func (a ByteNativeArray) Freeze(size uint32) ImmutableArray { return a.Subarray(0, size) } -func (a ByteNativeArray) Subarray(lo, hi uint32) ImmutableArray { - return ByteNativeArray{contents: a.contents[lo:hi]} + +func (b ByteNativeArray) Freeze(size uint32) ImmutableArray { + return b.Subarray(0, size) +} + +func (b ByteNativeArray) Subarray(lo, hi uint32) ImmutableArray { + return ByteNativeArray{underlying: &arrayForByte{ + contents: b.underlying.contents[lo:hi], + dims: []int{int(hi - lo)}, + }} +} + +func (b ByteNativeArray) String() string { + return "dafny.ByteNativeArray" } -func (a ByteNativeArray) String() string { return "ByteNativeArray" } -// Helper to create byte sequences +// Helper to create byte sequences using ByteNativeArray wrapper func newByteSeq(data []byte) Sequence { result := New_ArraySequence_() - result.Ctor__(ByteNativeArray{contents: data}, false) + underlying := &arrayForByte{contents: data, dims: []int{len(data)}} + result.Ctor__(ByteNativeArray{underlying: underlying}, false) return result } -// Helper to try creating optimized uint8 sequence from slice +// Helper to try creating optimized uint8 sequence func tryByteSeq(contents []interface{}) (Sequence, bool) { if len(contents) > 0 { if _, ok := contents[0].(uint8); ok { @@ -820,69 +892,56 @@ func tryByteSeqInit(n uint32, init func(Int) interface{}) (Sequence, bool) { return nil, false } -// A GoNativeArray is a single dimensional Go slice, -// wrapped up for the benefit of dafnyRuntime.dfy. -// We should refactor to wrap an Array interface as defined below -// to get the same optimization benefits for sequences of bytes and chars/CodePoints. -type GoNativeArray struct { - contents []interface{} -} - -func (CompanionStruct_NativeArray_) Make(length uint32) NativeArray { - contents := make([]interface{}, length) - return GoNativeArray{ - contents: contents, +// CompanionStruct_NativeArray_ functions work with Array interface through GoNativeArray wrapper +func (CompanionStruct_NativeArray_) Make(length uint32) ImmutableArray { + underlying := &arrayStruct{ + contents: make([]interface{}, length), + dims: []int{int(length)}, } + return GoNativeArray{underlying: underlying} } -func (CompanionStruct_NativeArray_) MakeWithInit(length uint32, init func(uint32) interface{}) NativeArray { +func (CompanionStruct_NativeArray_) MakeWithInit(length uint32, init func(uint32) interface{}) ImmutableArray { contents := make([]interface{}, length) for i := uint32(0); i < length; i++ { contents[i] = init(i) } - return GoNativeArray{ + underlying := &arrayStruct{ contents: contents, + dims: []int{int(length)}, } + return GoNativeArray{underlying: underlying} } -func (CompanionStruct_NativeArray_) Copy(other ImmutableArray) NativeArray { - contents := make([]interface{}, other.Length()) - for i := uint32(0); i < other.Length(); i++ { - contents[i] = other.Select(i) +func (CompanionStruct_NativeArray_) Copy(other ImmutableArray) ImmutableArray { + // Fast path: if it's already a GoNativeArray, use the underlying Array + if goArray, ok := other.(GoNativeArray); ok { + slice := goArray.underlying.anySlice(Zero, IntOfUint32(other.Length())) + underlying := &arrayStruct{ + contents: append([]interface{}(nil), slice...), + dims: []int{len(slice)}, + } + return GoNativeArray{underlying: underlying} } - return GoNativeArray{contents: contents} -} - -func (array GoNativeArray) Length() uint32 { - return uint32(len(array.contents)) -} - -func (array GoNativeArray) Select(i uint32) interface{} { - return array.contents[i] -} - -func (array GoNativeArray) Update(i uint32, t interface{}) { - array.contents[i] = t -} -func (array GoNativeArray) UpdateSubarray(i uint32, other ImmutableArray) { - for j := uint32(0); j < other.Length(); j++ { - array.contents[i+j] = other.Select(j) + // Fast path: if it's a ByteNativeArray, copy efficiently + if byteArray, ok := other.(ByteNativeArray); ok { + data := make([]byte, len(byteArray.underlying.contents)) + copy(data, byteArray.underlying.contents) + underlying := &arrayForByte{contents: data, dims: []int{len(data)}} + return ByteNativeArray{underlying: underlying} } -} - -func (array GoNativeArray) Freeze(size uint32) ImmutableArray { - return array.Subarray(0, size) -} -func (array GoNativeArray) Subarray(lo uint32, hi uint32) ImmutableArray { - return GoNativeArray{ - contents: array.contents[lo:hi], + // Generic path: copy through interface + contents := make([]interface{}, other.Length()) + for i := uint32(0); i < other.Length(); i++ { + contents[i] = other.Select(i) } -} - -func (array GoNativeArray) String() string { - return "dafny.GoNativeArray" + underlying := &arrayStruct{ + contents: contents, + dims: []int{len(contents)}, + } + return GoNativeArray{underlying: underlying} } // Array is the general interface for arrays. Conceptually, it contains some diff --git a/Source/DafnyRuntime/DafnyRuntimeGo/dafny/dafny_test.go b/Source/DafnyRuntime/DafnyRuntimeGo/dafny/dafny_test.go index 5b5e779bcda..23c1f273b45 100644 --- a/Source/DafnyRuntime/DafnyRuntimeGo/dafny/dafny_test.go +++ b/Source/DafnyRuntime/DafnyRuntimeGo/dafny/dafny_test.go @@ -6,40 +6,162 @@ import "testing" // between the manually-written and Dafny-generated Go code, // but could easily be expanded to include more unit tests in the future. -func TestArraySequence(t *testing.T){ - arrSeq := MakeArraySequence() - AssertImplementsSequence(arrSeq, t) +func TestArraySequence(t *testing.T) { + arrSeq := MakeArraySequence() + AssertImplementsSequence(arrSeq, t) } func MakeArraySequence() Sequence { - arr := GoNativeArray{} - arrSeq := New_ArraySequence_() - arrSeq.Ctor__(arr, false) - return arrSeq + underlying := &arrayStruct{ + contents: []interface{}{}, + dims: []int{0}, + } + arr := GoNativeArray{underlying: underlying} + arrSeq := New_ArraySequence_() + arrSeq.Ctor__(arr, false) + return arrSeq } func TestConcatSequence(t *testing.T) { - left := MakeArraySequence() - right := MakeArraySequence() - - concatSeq := New_ConcatSequence_() - concatSeq.Ctor__(left, right) - - AssertImplementsSequence(concatSeq, t) + left := MakeArraySequence() + right := MakeArraySequence() + + concatSeq := New_ConcatSequence_() + concatSeq.Ctor__(left, right) + + AssertImplementsSequence(concatSeq, t) } func TestLazySequence(t *testing.T) { - arrSeq := MakeArraySequence() - - lazySeq := New_LazySequence_() - lazySeq.Ctor__(arrSeq) - - AssertImplementsSequence(lazySeq, t) + arrSeq := MakeArraySequence() + + lazySeq := New_LazySequence_() + lazySeq.Ctor__(arrSeq) + + AssertImplementsSequence(lazySeq, t) +} + +// Test byte sequence optimization using ByteNativeArray wrapper +func TestByteSequenceOptimization(t *testing.T) { + // Test creating byte sequence from slice + data := []byte{1, 2, 3, 4, 5} + seq := newByteSeq(data) + + // Verify it implements Sequence interface + AssertImplementsSequence(seq, t) + + // Verify ToArray returns ByteNativeArray + arr := seq.ToArray() + if byteArr, ok := arr.(ByteNativeArray); ok { + if byteArr.Length() != 5 { + t.Errorf("Expected length 5, got %d", byteArr.Length()) + } + if byteArr.Select(0).(uint8) != 1 { + t.Errorf("Expected first element 1, got %v", byteArr.Select(0)) + } + } else { + t.Errorf("Expected ByteNativeArray, got %T", arr) + } +} + +// Test optimization detection for uint8 vs non-uint8 +func TestTryByteSeq(t *testing.T) { + // Test uint8 slice - should optimize + uint8Contents := []interface{}{uint8(1), uint8(2), uint8(3)} + seq, optimized := tryByteSeq(uint8Contents) + if !optimized { + t.Error("Expected optimization for uint8 slice") + } + if seq == nil { + t.Error("Expected non-nil sequence") + } + + // Verify it returns ByteNativeArray + arr := seq.ToArray() + if _, ok := arr.(ByteNativeArray); !ok { + t.Errorf("Expected ByteNativeArray, got %T", arr) + } + + // Test non-uint8 slice - should not optimize + intContents := []interface{}{1, 2, 3} + seq2, optimized2 := tryByteSeq(intContents) + if optimized2 { + t.Error("Expected no optimization for int slice") + } + if seq2 != nil { + t.Error("Expected nil sequence for non-optimized case") + } + + // Test empty slice - should not optimize + emptyContents := []interface{}{} + seq3, optimized3 := tryByteSeq(emptyContents) + if optimized3 { + t.Error("Expected no optimization for empty slice") + } + if seq3 != nil { + t.Error("Expected nil sequence for empty case") + } +} + +// Test refactored CompanionStruct_NativeArray_ functions +func TestNativeArrayFunctions(t *testing.T) { + // Test Make function + arr := Companion_NativeArray_.Make(3) + if goArr, ok := arr.(GoNativeArray); ok { + if goArr.Length() != 3 { + t.Errorf("Expected length 3, got %d", goArr.Length()) + } + } else { + t.Errorf("Expected GoNativeArray, got %T", arr) + } + + // Test MakeWithInit function + initFunc := func(i uint32) interface{} { return int(i * 2) } + arr2 := Companion_NativeArray_.MakeWithInit(3, initFunc) + if goArr2, ok := arr2.(GoNativeArray); ok { + if goArr2.Length() != 3 { + t.Errorf("Expected length 3, got %d", goArr2.Length()) + } + if goArr2.Select(1) != 2 { + t.Errorf("Expected element at index 1 to be 2, got %v", goArr2.Select(1)) + } + } else { + t.Errorf("Expected GoNativeArray, got %T", arr2) + } + + // Test Copy function with GoNativeArray + arr3 := Companion_NativeArray_.Copy(arr2) + if goArr3, ok := arr3.(GoNativeArray); ok { + if goArr3.Length() != 3 { + t.Errorf("Expected length 3, got %d", goArr3.Length()) + } + if goArr3.Select(1) != 2 { + t.Errorf("Expected element at index 1 to be 2, got %v", goArr3.Select(1)) + } + } else { + t.Errorf("Expected GoNativeArray, got %T", arr3) + } + + // Test Copy function with ByteNativeArray + data := []byte{10, 20, 30} + byteSeq := newByteSeq(data) + byteArr := byteSeq.ToArray() + arr4 := Companion_NativeArray_.Copy(byteArr) + if byteArr4, ok := arr4.(ByteNativeArray); ok { + if byteArr4.Length() != 3 { + t.Errorf("Expected length 3, got %d", byteArr4.Length()) + } + if byteArr4.Select(1).(uint8) != 20 { + t.Errorf("Expected element at index 1 to be 20, got %v", byteArr4.Select(1)) + } + } else { + t.Errorf("Expected ByteNativeArray, got %T", arr4) + } } func AssertImplementsSequence(s interface{}, t *testing.T) { - _, ok := s.(Sequence) - if (!ok) { - t.Errorf("Expected %v to implement the Sequence interface", s) - } -} \ No newline at end of file + _, ok := s.(Sequence) + if !ok { + t.Errorf("Expected %v to implement the Sequence interface", s) + } +} From ed00827ba5c7ce72926e37f53ec0c8190ce59898 Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Thu, 4 Sep 2025 12:44:12 -0700 Subject: [PATCH 03/11] Squashed commit of the following: Refactor to push more into the Array interface --- .../DafnyRuntimeGo-gomod/dafny/dafny.go | 439 ++++++++++-------- .../DafnyRuntimeGo-gomod/dafny/dafny_test.go | 78 ++-- .../DafnyRuntimeGo/dafny/dafny.go | 439 ++++++++++-------- .../DafnyRuntimeGo/dafny/dafny_test.go | 78 ++-- 4 files changed, 604 insertions(+), 430 deletions(-) diff --git a/Source/DafnyRuntime/DafnyRuntimeGo-gomod/dafny/dafny.go b/Source/DafnyRuntime/DafnyRuntimeGo-gomod/dafny/dafny.go index f3a2979cf43..c0b442da651 100644 --- a/Source/DafnyRuntime/DafnyRuntimeGo-gomod/dafny/dafny.go +++ b/Source/DafnyRuntime/DafnyRuntimeGo-gomod/dafny/dafny.go @@ -83,38 +83,7 @@ func (_static *CompanionStruct_Sequence_) EqualUpTo(left Sequence, right Sequenc } leftArr, rightArr := left.ToArray(), right.ToArray() - - // Fast path for ByteNativeArray (byte sequence optimization) - if l, ok := leftArr.(ByteNativeArray); ok { - if r, ok := rightArr.(ByteNativeArray); ok { - return slices.Equal(l.underlying.contents[:index], r.underlying.contents[:index]) - } - } - - // Fast path for GoNativeArray (preserve original optimization) - if l, ok := leftArr.(GoNativeArray); ok { - if r, ok := rightArr.(GoNativeArray); ok { - lSlice := l.underlying.anySlice(Zero, IntOfUint32(index)) - rSlice := r.underlying.anySlice(Zero, IntOfUint32(index)) - if len(lSlice) > 0 && IsEqualityComparable(lSlice[0]) { - return slices.Equal(lSlice, rSlice) - } - for i := uint32(0); i < index; i++ { - if !AreEqual(lSlice[i], rSlice[i]) { - return false - } - } - return true - } - } - - // Generic fallback - for i := uint32(0); i < index; i++ { - if !AreEqual(leftArr.Select(i), rightArr.Select(i)) { - return false - } - } - return true + return leftArr.(GoNativeArray).underlying.ArrayEqualUpTo(rightArr.(GoNativeArray).underlying, int(index)) } func IsDafnyNull(x interface{}) bool { @@ -552,45 +521,39 @@ var EmptySeq = SeqOf() // for the compiler to coerce the init function to a // func (uint32) interface{}. func SeqCreate(n uint32, init func(Int) interface{}) Sequence { - if seq, ok := tryByteSeqInit(n, init); ok { - return seq - } return Companion_Sequence_.Create(n, func(index uint32) interface{} { return init(IntOfUint32(index)) }) } func SeqFromArray(contents []interface{}, isString bool) Sequence { - if seq, ok := tryByteSeq(contents); ok && !isString { - return seq - } result := New_ArraySequence_() - underlying := &arrayStruct{contents: contents, dims: []int{len(contents)}} + underlying := newArrayWithValues(contents...) result.Ctor__(GoNativeArray{underlying: underlying}, isString) return result } // SeqOf returns a sequence containing the given values. func SeqOf(values ...interface{}) Sequence { - if seq, ok := tryByteSeq(values); ok { - return seq - } - arr := make([]interface{}, len(values)) - copy(arr, values) - return SeqFromArray(arr, false) + result := New_ArraySequence_() + underlying := newArrayWithValues(values...) + result.Ctor__(GoNativeArray{underlying: underlying}, false) + return result } // SeqOfChars returns a sequence containing the given character values. func SeqOfChars(values ...Char) Sequence { - arr := make([]interface{}, len(values)) - for i, v := range values { - arr[i] = v - } - return SeqFromArray(arr, true) + result := New_ArraySequence_() + underlying := NewArrayFromCharArray(values) + result.Ctor__(GoNativeArray{underlying: underlying}, false) + return result } func SeqOfBytes(values []byte) Sequence { - return newByteSeq(values) + result := New_ArraySequence_() + underlying := NewArrayFromByteArray(values) + result.Ctor__(GoNativeArray{underlying: underlying}, false) + return result } // SeqOfString converts the given string into a sequence of characters. @@ -756,21 +719,12 @@ func (seq *LazySequence) ToByteArray() []byte { } func ToByteArray(x Sequence) []byte { - if arr, ok := x.ToArray().(ByteNativeArray); ok { - return arr.underlying.contents - } arr := x.ToArray() result := make([]byte, arr.Length()) - for i := uint32(0); i < arr.Length(); i++ { - result[i] = arr.Select(i).(byte) - } + copy(result, arr.(GoNativeArray).underlying.(arrayForByte).contents) return result } -/****************************************************************************** - * Arrays - ******************************************************************************/ - /****************************************************************************** * Arrays ******************************************************************************/ @@ -795,9 +749,7 @@ func (g GoNativeArray) Update(i uint32, t interface{}) { } func (g GoNativeArray) UpdateSubarray(i uint32, other ImmutableArray) { - for j := uint32(0); j < other.Length(); j++ { - g.underlying.ArraySet1(other.Select(j), int(i+j)) - } + g.underlying.ArraySetRange1(int(i), other.(GoNativeArray).underlying) } func (g GoNativeArray) Freeze(size uint32) ImmutableArray { @@ -805,93 +757,13 @@ func (g GoNativeArray) Freeze(size uint32) ImmutableArray { } func (g GoNativeArray) Subarray(lo, hi uint32) ImmutableArray { - slice := g.underlying.anySlice(IntOfUint32(lo), IntOfUint32(hi)) - return GoNativeArray{underlying: &arrayStruct{contents: slice, dims: []int{len(slice)}}} + return GoNativeArray{underlying: g.underlying.ArrayGetRange1(int(lo), int(hi))} } func (g GoNativeArray) String() string { return "dafny.GoNativeArray" } -// ByteNativeArray wraps arrayForByte for byte sequence optimization -type ByteNativeArray struct { - underlying *arrayForByte -} - -func (b ByteNativeArray) Length() uint32 { - return uint32(b.underlying.dimensionLength(0)) -} - -func (b ByteNativeArray) Select(i uint32) interface{} { - return b.underlying.ArrayGet1Byte(int(i)) -} - -func (b ByteNativeArray) Update(i uint32, t interface{}) { - b.underlying.ArraySet1Byte(t.(uint8), int(i)) -} - -func (b ByteNativeArray) UpdateSubarray(i uint32, other ImmutableArray) { - // Fast path for ByteNativeArray - if otherByte, ok := other.(ByteNativeArray); ok { - copy(b.underlying.contents[i:], otherByte.underlying.contents) - } else { - for j := uint32(0); j < other.Length(); j++ { - b.underlying.ArraySet1Byte(other.Select(j).(uint8), int(i+j)) - } - } -} - -func (b ByteNativeArray) Freeze(size uint32) ImmutableArray { - return b.Subarray(0, size) -} - -func (b ByteNativeArray) Subarray(lo, hi uint32) ImmutableArray { - return ByteNativeArray{underlying: &arrayForByte{ - contents: b.underlying.contents[lo:hi], - dims: []int{int(hi - lo)}, - }} -} - -func (b ByteNativeArray) String() string { - return "dafny.ByteNativeArray" -} - -// Helper to create byte sequences using ByteNativeArray wrapper -func newByteSeq(data []byte) Sequence { - result := New_ArraySequence_() - underlying := &arrayForByte{contents: data, dims: []int{len(data)}} - result.Ctor__(ByteNativeArray{underlying: underlying}, false) - return result -} - -// Helper to try creating optimized uint8 sequence -func tryByteSeq(contents []interface{}) (Sequence, bool) { - if len(contents) > 0 { - if _, ok := contents[0].(uint8); ok { - data := make([]byte, len(contents)) - for i, v := range contents { - data[i] = v.(uint8) - } - return newByteSeq(data), true - } - } - return nil, false -} - -// Helper to try creating optimized uint8 sequence from init function -func tryByteSeqInit(n uint32, init func(Int) interface{}) (Sequence, bool) { - if n > 0 { - if _, ok := init(Zero).(uint8); ok { - data := make([]byte, n) - for i := uint32(0); i < n; i++ { - data[i] = init(IntOfUint32(i)).(uint8) - } - return newByteSeq(data), true - } - } - return nil, false -} - // CompanionStruct_NativeArray_ functions work with Array interface through GoNativeArray wrapper func (CompanionStruct_NativeArray_) Make(length uint32) ImmutableArray { underlying := &arrayStruct{ @@ -902,46 +774,12 @@ func (CompanionStruct_NativeArray_) Make(length uint32) ImmutableArray { } func (CompanionStruct_NativeArray_) MakeWithInit(length uint32, init func(uint32) interface{}) ImmutableArray { - contents := make([]interface{}, length) - for i := uint32(0); i < length; i++ { - contents[i] = init(i) - } - underlying := &arrayStruct{ - contents: contents, - dims: []int{int(length)}, - } + underlying := newArrayWithInitFn(init, int(length)) return GoNativeArray{underlying: underlying} } func (CompanionStruct_NativeArray_) Copy(other ImmutableArray) ImmutableArray { - // Fast path: if it's already a GoNativeArray, use the underlying Array - if goArray, ok := other.(GoNativeArray); ok { - slice := goArray.underlying.anySlice(Zero, IntOfUint32(other.Length())) - underlying := &arrayStruct{ - contents: append([]interface{}(nil), slice...), - dims: []int{len(slice)}, - } - return GoNativeArray{underlying: underlying} - } - - // Fast path: if it's a ByteNativeArray, copy efficiently - if byteArray, ok := other.(ByteNativeArray); ok { - data := make([]byte, len(byteArray.underlying.contents)) - copy(data, byteArray.underlying.contents) - underlying := &arrayForByte{contents: data, dims: []int{len(data)}} - return ByteNativeArray{underlying: underlying} - } - - // Generic path: copy through interface - contents := make([]interface{}, other.Length()) - for i := uint32(0); i < other.Length(); i++ { - contents[i] = other.Select(i) - } - underlying := &arrayStruct{ - contents: contents, - dims: []int{len(contents)}, - } - return GoNativeArray{underlying: underlying} + return GoNativeArray{underlying: other.(GoNativeArray).underlying.ArrayCopy()} } // Array is the general interface for arrays. Conceptually, it contains some @@ -958,7 +796,11 @@ type Array interface { dimensionLength(dim int) int ArrayGet1(index int) interface{} ArraySet1(value interface{}, index int) + ArrayGetRange1(lo, hi int) Array + ArraySetRange1(index int, other Array) anySlice(lo, hi Int) []interface{} + ArrayCopy() Array + ArrayEqualUpTo(other Array, index int) bool // specializations ArrayGet1Byte(index int) byte ArraySet1Byte(value byte, index int) @@ -968,6 +810,27 @@ type Array interface { ArraySet1CodePoint(value CodePoint, index int) } +func defaultArrayEqualUpTo(left Array, right Array, index uint32) bool { + lSlice := left.anySlice(Zero, IntOfUint32(index)) + rSlice := right.anySlice(Zero, IntOfUint32(index)) + if len(lSlice) > 0 && IsEqualityComparable(lSlice[0]) { + return slices.Equal(lSlice, rSlice) + } + for i := uint32(0); i < index; i++ { + if !AreEqual(lSlice[i], rSlice[i]) { + return false + } + } + return true +} + +func defaultArraySetRange1(left Array, right Array, index int) { + rightLength := right.dimensionLength(0) + for j := 0; j < rightLength; j++ { + left.ArraySet1(right.ArrayGet1(j), int(index+j)) + } +} + /***** newArray *****/ // Multiply the numbers in "dims" and return the product as an "int". @@ -987,6 +850,25 @@ func computeTotalArrayLength(dims ...Int) int { return totalLength } +func NewArrayFromCharArray(values []Char) Array { + contents := make([]Char, len(values)) + copy(contents, values) + return &arrayForChar{ + contents: contents, + dims: []int{len(values)}, + } +} + +func NewArrayFromByteArray(values []byte) Array { + contents := make([]byte, len(values)) + copy(contents, values) + return &arrayForByte{ + contents: contents, + dims: []int{len(values)}, + } +} + + // NewArrayFromExample returns a new Array. // If "init" is non-nil, it is used to initialize all elements of the array. // "example" is used only to figure out the right kind of Array to return. @@ -1071,8 +953,8 @@ func newZeroLengthArray(intDims []int) Array { } } -// newArrayWithValues returns a new one-dimensional Array with the given initial -// values. It is only used internally, by *Builder.ToArray(). +// newArrayWithValues returns a new one-dimensional Array with the initial values. +// It is currently only used internally, by *Builder.ToArray(). func newArrayWithValues(values ...interface{}) Array { totalLength := len(values) intDims := []int{totalLength} @@ -1111,6 +993,53 @@ func newArrayWithValues(values ...interface{}) Array { } } +// newArrayWithInitFn returns a new one-dimensional Array with the given initial values. +// It is currently only used internally, by CompanionStruct_NativeArray_.MakeWithInit. +// It could potentially be used in the translation of Dafny array instantiations with initializing lambdas, +// but that is currently rewritten by the single-pass compiler instead. +func newArrayWithInitFn(init func(uint32) interface{}, length int) Array { + intDims := []int{length} + if length == 0 { + return newZeroLengthArray(intDims) + } + + // Inspect the type of the first initial value to consider Array specialization + value0 := init(0) + if _, ok := value0.(byte); ok { + arr := make([]byte, length) + arr[0] = value0.(byte) + for i := range arr[1:] { + arr[i] = init(uint32(i)).(byte) + } + return &arrayForByte{ + contents: arr, + dims: intDims, + } + } + if _, ok := value0.(Char); ok { + arr := make([]Char, length) + arr[0] = value0.(Char) + for i := range arr { + arr[i] = init(uint32(i)).(Char) + } + return &arrayForChar{ + contents: arr, + dims: intDims, + } + } + + // Use the default representation + arr := make([]interface{}, length) + arr[0] = value0 + for i := range arr[1:] { + arr[i] = init(uint32(i)) + } + return &arrayStruct{ + contents: arr, + dims: intDims, + } +} + // NewArrayWithValue returns a new Array full of the given initial value. func NewArrayWithValue(init interface{}, dims ...Int) Array { return NewArrayFromExample(init, init, dims...) @@ -1144,6 +1073,39 @@ func (_this arrayStruct) ArraySet1(value interface{}, index int) { _this.contents[index] = value } +func (_this arrayStruct) ArrayGetRange1(lo, hi int) Array { + newContents := _this.contents[lo:hi] + return &arrayStruct{ + contents: newContents, + dims: []int{int(hi - lo)}, + } +} + +func (_this arrayStruct) ArraySetRange1(index int, other Array) { + // Optimize for the same type of content array + if otherStruct, ok := other.(arrayStruct); ok { + copy(_this.contents[index:], otherStruct.contents) + } else { + defaultArraySetRange1(_this, other, index) + } +} + +func (_this arrayStruct) ArrayCopy() Array { + newContents := make([]interface{}, len(_this.contents)) + copy(newContents, _this.contents) + return &arrayStruct{ + contents: newContents, + // TODO: Does dims have to be copied as well? + dims: _this.dims, + } +} + +func (_this arrayStruct) ArrayEqualUpTo(other Array, index int) bool { + // Not much point in optimizing for the same type of content array + // since anySlice is cheap on arrayStructs. + return defaultArrayEqualUpTo(_this, other, uint32(index)) +} + func (_this arrayStruct) ArrayGet1Byte(index int) byte { panic("Expected specialized array type that contains bytes, but found general-purpose array of interface{}") } @@ -1214,6 +1176,43 @@ func (_this arrayForByte) ArraySet1(value interface{}, index int) { _this.contents[index] = value.(byte) } +func (_this arrayForByte) ArrayGetRange1(lo, hi int) Array { + newContents := _this.contents[lo:hi] + return &arrayForByte{ + contents: newContents, + dims: []int{int(hi - lo)}, + } +} + +func (_this arrayForByte) ArraySetRange1(index int, other Array) { + // Optimize for the same type of content array + if otherByte, ok := other.(arrayForByte); ok { + copy(_this.contents[index:], otherByte.contents) + } else { + defaultArraySetRange1(_this, other, index) + } +} + +func (_this arrayForByte) ArrayCopy() Array { + newContents := make([]byte, len(_this.contents)) + copy(newContents, _this.contents) + return &arrayForByte{ + contents: newContents, + // TODO: Does dims have to be copied as well? + dims: _this.dims, + } +} + +func (_this arrayForByte) ArrayEqualUpTo(other Array, index int) bool { + // Optimize for the same type of content array + if otherByte, ok := other.(arrayForByte); ok { + return slices.Equal(_this.contents[:index], otherByte.contents[:index]) + } else { + // Generic fallback + return defaultArrayEqualUpTo(_this, other, uint32(index)) + } +} + func (_this arrayForByte) ArrayGet1Byte(index int) byte { return _this.contents[index] } @@ -1286,6 +1285,43 @@ func (_this arrayForChar) ArraySet1(value interface{}, index int) { _this.contents[index] = value.(Char) } +func (_this arrayForChar) ArrayGetRange1(lo, hi int) Array { + newContents := _this.contents[lo:hi] + return &arrayForChar{ + contents: newContents, + dims: []int{int(hi - lo)}, + } +} + +func (_this arrayForChar) ArraySetRange1(index int, other Array) { + // Optimize for the same type of content array + if otherByte, ok := other.(arrayForChar); ok { + copy(_this.contents[index:], otherByte.contents) + } else { + defaultArraySetRange1(_this, other, index) + } +} + +func (_this arrayForChar) ArrayCopy() Array { + newContents := make([]Char, len(_this.contents)) + copy(newContents, _this.contents) + return &arrayForChar{ + contents: newContents, + // TODO: Does dims have to be copied as well? + dims: _this.dims, + } +} + +func (_this arrayForChar) ArrayEqualUpTo(other Array, index int) bool { + // Optimize for the same type of content array + if otherChar, ok := other.(arrayForChar); ok { + return slices.Equal(_this.contents[:index], otherChar.contents[:index]) + } else { + // Generic fallback + return defaultArrayEqualUpTo(_this, other, uint32(index)) + } +} + func (_this arrayForChar) ArrayGet1Byte(index int) byte { panic("Expected specialized array type that contains bytes, but found general-purpose array of interface{}") } @@ -1358,6 +1394,43 @@ func (_this arrayForCodePoint) ArraySet1(value interface{}, index int) { _this.contents[index] = value.(CodePoint) } +func (_this arrayForCodePoint) ArrayGetRange1(lo, hi int) Array { + newContents := _this.contents[lo:hi] + return &arrayForCodePoint{ + contents: newContents, + dims: []int{int(hi - lo)}, + } +} + +func (_this arrayForCodePoint) ArraySetRange1(index int, other Array) { + // Optimize for the same type of content array + if otherCodePoint, ok := other.(arrayForCodePoint); ok { + copy(_this.contents[index:], otherCodePoint.contents) + } else { + defaultArraySetRange1(_this, other, index) + } +} + +func (_this arrayForCodePoint) ArrayCopy() Array { + newContents := make([]CodePoint, len(_this.contents)) + copy(newContents, _this.contents) + return &arrayForCodePoint{ + contents: newContents, + // TODO: Does dims have to be copied as well? + dims: _this.dims, + } +} + +func (_this arrayForCodePoint) ArrayEqualUpTo(other Array, index int) bool { + // Optimize for the same type of content array + if otherCodePoint, ok := other.(arrayForCodePoint); ok { + return slices.Equal(_this.contents[:index], otherCodePoint.contents[:index]) + } else { + // Generic fallback + return defaultArrayEqualUpTo(_this, other, uint32(index)) + } +} + func (_this arrayForCodePoint) ArrayGet1Byte(index int) byte { panic("Expected specialized array type that contains bytes, but found general-purpose array of interface{}") } diff --git a/Source/DafnyRuntime/DafnyRuntimeGo-gomod/dafny/dafny_test.go b/Source/DafnyRuntime/DafnyRuntimeGo-gomod/dafny/dafny_test.go index 23c1f273b45..9a3975f0e7e 100644 --- a/Source/DafnyRuntime/DafnyRuntimeGo-gomod/dafny/dafny_test.go +++ b/Source/DafnyRuntime/DafnyRuntimeGo-gomod/dafny/dafny_test.go @@ -45,62 +45,54 @@ func TestLazySequence(t *testing.T) { func TestByteSequenceOptimization(t *testing.T) { // Test creating byte sequence from slice data := []byte{1, 2, 3, 4, 5} - seq := newByteSeq(data) + seq := SeqOf(data) // Verify it implements Sequence interface AssertImplementsSequence(seq, t) // Verify ToArray returns ByteNativeArray - arr := seq.ToArray() - if byteArr, ok := arr.(ByteNativeArray); ok { - if byteArr.Length() != 5 { - t.Errorf("Expected length 5, got %d", byteArr.Length()) - } - if byteArr.Select(0).(uint8) != 1 { - t.Errorf("Expected first element 1, got %v", byteArr.Select(0)) - } - } else { - t.Errorf("Expected ByteNativeArray, got %T", arr) - } + // arr := seq.ToArray() + // if byteArr, ok := arr.(ByteNativeArray); ok { + // if byteArr.Length() != 5 { + // t.Errorf("Expected length 5, got %d", byteArr.Length()) + // } + // if byteArr.Select(0).(uint8) != 1 { + // t.Errorf("Expected first element 1, got %v", byteArr.Select(0)) + // } + // } else { + // t.Errorf("Expected ByteNativeArray, got %T", arr) + // } } // Test optimization detection for uint8 vs non-uint8 -func TestTryByteSeq(t *testing.T) { +func TestSeqOf(t *testing.T) { // Test uint8 slice - should optimize uint8Contents := []interface{}{uint8(1), uint8(2), uint8(3)} - seq, optimized := tryByteSeq(uint8Contents) - if !optimized { + seq := SeqFromArray(uint8Contents, false) + AssertSequenceIsBackedByByteArray(seq, t) + if !SequenceIsBackedByByteArray(seq) { t.Error("Expected optimization for uint8 slice") } - if seq == nil { - t.Error("Expected non-nil sequence") - } // Verify it returns ByteNativeArray arr := seq.ToArray() - if _, ok := arr.(ByteNativeArray); !ok { + if _, ok := arr.(GoNativeArray); !ok { t.Errorf("Expected ByteNativeArray, got %T", arr) } // Test non-uint8 slice - should not optimize intContents := []interface{}{1, 2, 3} - seq2, optimized2 := tryByteSeq(intContents) - if optimized2 { + seq2 := SeqFromArray(intContents, false) + if SequenceIsBackedByByteArray(seq2) { t.Error("Expected no optimization for int slice") } - if seq2 != nil { - t.Error("Expected nil sequence for non-optimized case") - } // Test empty slice - should not optimize emptyContents := []interface{}{} - seq3, optimized3 := tryByteSeq(emptyContents) - if optimized3 { + seq3 := SeqFromArray(emptyContents, false) + if SequenceIsBackedByByteArray(seq3) { t.Error("Expected no optimization for empty slice") } - if seq3 != nil { - t.Error("Expected nil sequence for empty case") - } } // Test refactored CompanionStruct_NativeArray_ functions @@ -144,10 +136,10 @@ func TestNativeArrayFunctions(t *testing.T) { // Test Copy function with ByteNativeArray data := []byte{10, 20, 30} - byteSeq := newByteSeq(data) + byteSeq := SeqOfBytes(data) byteArr := byteSeq.ToArray() arr4 := Companion_NativeArray_.Copy(byteArr) - if byteArr4, ok := arr4.(ByteNativeArray); ok { + if byteArr4, ok := arr4.(GoNativeArray); ok { if byteArr4.Length() != 3 { t.Errorf("Expected length 3, got %d", byteArr4.Length()) } @@ -155,7 +147,7 @@ func TestNativeArrayFunctions(t *testing.T) { t.Errorf("Expected element at index 1 to be 20, got %v", byteArr4.Select(1)) } } else { - t.Errorf("Expected ByteNativeArray, got %T", arr4) + t.Errorf("Expected GoNativeArray, got %T", arr4) } } @@ -165,3 +157,25 @@ func AssertImplementsSequence(s interface{}, t *testing.T) { t.Errorf("Expected %v to implement the Sequence interface", s) } } + +func SequenceIsBackedByByteArray(seq Sequence) bool { + _, ok := seq.(*ArraySequence)._values.(GoNativeArray).underlying.(*arrayForByte) + return ok +} + +func AssertSequenceIsBackedByByteArray(seq Sequence, t *testing.T) { + as, ok := seq.(*ArraySequence) + if !ok { + t.Errorf("Expected %v to be an *ArraySequence", seq) + } + + gna, ok := as._values.(GoNativeArray) + if !ok { + t.Errorf("Expected %v to implement the GoNativeArray interface", as._values) + } + + _, ok = gna.underlying.(*arrayForByte) + if !ok { + t.Errorf("Expected %v to be an arrayForByte", gna.underlying) + } +} diff --git a/Source/DafnyRuntime/DafnyRuntimeGo/dafny/dafny.go b/Source/DafnyRuntime/DafnyRuntimeGo/dafny/dafny.go index f3a2979cf43..c0b442da651 100644 --- a/Source/DafnyRuntime/DafnyRuntimeGo/dafny/dafny.go +++ b/Source/DafnyRuntime/DafnyRuntimeGo/dafny/dafny.go @@ -83,38 +83,7 @@ func (_static *CompanionStruct_Sequence_) EqualUpTo(left Sequence, right Sequenc } leftArr, rightArr := left.ToArray(), right.ToArray() - - // Fast path for ByteNativeArray (byte sequence optimization) - if l, ok := leftArr.(ByteNativeArray); ok { - if r, ok := rightArr.(ByteNativeArray); ok { - return slices.Equal(l.underlying.contents[:index], r.underlying.contents[:index]) - } - } - - // Fast path for GoNativeArray (preserve original optimization) - if l, ok := leftArr.(GoNativeArray); ok { - if r, ok := rightArr.(GoNativeArray); ok { - lSlice := l.underlying.anySlice(Zero, IntOfUint32(index)) - rSlice := r.underlying.anySlice(Zero, IntOfUint32(index)) - if len(lSlice) > 0 && IsEqualityComparable(lSlice[0]) { - return slices.Equal(lSlice, rSlice) - } - for i := uint32(0); i < index; i++ { - if !AreEqual(lSlice[i], rSlice[i]) { - return false - } - } - return true - } - } - - // Generic fallback - for i := uint32(0); i < index; i++ { - if !AreEqual(leftArr.Select(i), rightArr.Select(i)) { - return false - } - } - return true + return leftArr.(GoNativeArray).underlying.ArrayEqualUpTo(rightArr.(GoNativeArray).underlying, int(index)) } func IsDafnyNull(x interface{}) bool { @@ -552,45 +521,39 @@ var EmptySeq = SeqOf() // for the compiler to coerce the init function to a // func (uint32) interface{}. func SeqCreate(n uint32, init func(Int) interface{}) Sequence { - if seq, ok := tryByteSeqInit(n, init); ok { - return seq - } return Companion_Sequence_.Create(n, func(index uint32) interface{} { return init(IntOfUint32(index)) }) } func SeqFromArray(contents []interface{}, isString bool) Sequence { - if seq, ok := tryByteSeq(contents); ok && !isString { - return seq - } result := New_ArraySequence_() - underlying := &arrayStruct{contents: contents, dims: []int{len(contents)}} + underlying := newArrayWithValues(contents...) result.Ctor__(GoNativeArray{underlying: underlying}, isString) return result } // SeqOf returns a sequence containing the given values. func SeqOf(values ...interface{}) Sequence { - if seq, ok := tryByteSeq(values); ok { - return seq - } - arr := make([]interface{}, len(values)) - copy(arr, values) - return SeqFromArray(arr, false) + result := New_ArraySequence_() + underlying := newArrayWithValues(values...) + result.Ctor__(GoNativeArray{underlying: underlying}, false) + return result } // SeqOfChars returns a sequence containing the given character values. func SeqOfChars(values ...Char) Sequence { - arr := make([]interface{}, len(values)) - for i, v := range values { - arr[i] = v - } - return SeqFromArray(arr, true) + result := New_ArraySequence_() + underlying := NewArrayFromCharArray(values) + result.Ctor__(GoNativeArray{underlying: underlying}, false) + return result } func SeqOfBytes(values []byte) Sequence { - return newByteSeq(values) + result := New_ArraySequence_() + underlying := NewArrayFromByteArray(values) + result.Ctor__(GoNativeArray{underlying: underlying}, false) + return result } // SeqOfString converts the given string into a sequence of characters. @@ -756,21 +719,12 @@ func (seq *LazySequence) ToByteArray() []byte { } func ToByteArray(x Sequence) []byte { - if arr, ok := x.ToArray().(ByteNativeArray); ok { - return arr.underlying.contents - } arr := x.ToArray() result := make([]byte, arr.Length()) - for i := uint32(0); i < arr.Length(); i++ { - result[i] = arr.Select(i).(byte) - } + copy(result, arr.(GoNativeArray).underlying.(arrayForByte).contents) return result } -/****************************************************************************** - * Arrays - ******************************************************************************/ - /****************************************************************************** * Arrays ******************************************************************************/ @@ -795,9 +749,7 @@ func (g GoNativeArray) Update(i uint32, t interface{}) { } func (g GoNativeArray) UpdateSubarray(i uint32, other ImmutableArray) { - for j := uint32(0); j < other.Length(); j++ { - g.underlying.ArraySet1(other.Select(j), int(i+j)) - } + g.underlying.ArraySetRange1(int(i), other.(GoNativeArray).underlying) } func (g GoNativeArray) Freeze(size uint32) ImmutableArray { @@ -805,93 +757,13 @@ func (g GoNativeArray) Freeze(size uint32) ImmutableArray { } func (g GoNativeArray) Subarray(lo, hi uint32) ImmutableArray { - slice := g.underlying.anySlice(IntOfUint32(lo), IntOfUint32(hi)) - return GoNativeArray{underlying: &arrayStruct{contents: slice, dims: []int{len(slice)}}} + return GoNativeArray{underlying: g.underlying.ArrayGetRange1(int(lo), int(hi))} } func (g GoNativeArray) String() string { return "dafny.GoNativeArray" } -// ByteNativeArray wraps arrayForByte for byte sequence optimization -type ByteNativeArray struct { - underlying *arrayForByte -} - -func (b ByteNativeArray) Length() uint32 { - return uint32(b.underlying.dimensionLength(0)) -} - -func (b ByteNativeArray) Select(i uint32) interface{} { - return b.underlying.ArrayGet1Byte(int(i)) -} - -func (b ByteNativeArray) Update(i uint32, t interface{}) { - b.underlying.ArraySet1Byte(t.(uint8), int(i)) -} - -func (b ByteNativeArray) UpdateSubarray(i uint32, other ImmutableArray) { - // Fast path for ByteNativeArray - if otherByte, ok := other.(ByteNativeArray); ok { - copy(b.underlying.contents[i:], otherByte.underlying.contents) - } else { - for j := uint32(0); j < other.Length(); j++ { - b.underlying.ArraySet1Byte(other.Select(j).(uint8), int(i+j)) - } - } -} - -func (b ByteNativeArray) Freeze(size uint32) ImmutableArray { - return b.Subarray(0, size) -} - -func (b ByteNativeArray) Subarray(lo, hi uint32) ImmutableArray { - return ByteNativeArray{underlying: &arrayForByte{ - contents: b.underlying.contents[lo:hi], - dims: []int{int(hi - lo)}, - }} -} - -func (b ByteNativeArray) String() string { - return "dafny.ByteNativeArray" -} - -// Helper to create byte sequences using ByteNativeArray wrapper -func newByteSeq(data []byte) Sequence { - result := New_ArraySequence_() - underlying := &arrayForByte{contents: data, dims: []int{len(data)}} - result.Ctor__(ByteNativeArray{underlying: underlying}, false) - return result -} - -// Helper to try creating optimized uint8 sequence -func tryByteSeq(contents []interface{}) (Sequence, bool) { - if len(contents) > 0 { - if _, ok := contents[0].(uint8); ok { - data := make([]byte, len(contents)) - for i, v := range contents { - data[i] = v.(uint8) - } - return newByteSeq(data), true - } - } - return nil, false -} - -// Helper to try creating optimized uint8 sequence from init function -func tryByteSeqInit(n uint32, init func(Int) interface{}) (Sequence, bool) { - if n > 0 { - if _, ok := init(Zero).(uint8); ok { - data := make([]byte, n) - for i := uint32(0); i < n; i++ { - data[i] = init(IntOfUint32(i)).(uint8) - } - return newByteSeq(data), true - } - } - return nil, false -} - // CompanionStruct_NativeArray_ functions work with Array interface through GoNativeArray wrapper func (CompanionStruct_NativeArray_) Make(length uint32) ImmutableArray { underlying := &arrayStruct{ @@ -902,46 +774,12 @@ func (CompanionStruct_NativeArray_) Make(length uint32) ImmutableArray { } func (CompanionStruct_NativeArray_) MakeWithInit(length uint32, init func(uint32) interface{}) ImmutableArray { - contents := make([]interface{}, length) - for i := uint32(0); i < length; i++ { - contents[i] = init(i) - } - underlying := &arrayStruct{ - contents: contents, - dims: []int{int(length)}, - } + underlying := newArrayWithInitFn(init, int(length)) return GoNativeArray{underlying: underlying} } func (CompanionStruct_NativeArray_) Copy(other ImmutableArray) ImmutableArray { - // Fast path: if it's already a GoNativeArray, use the underlying Array - if goArray, ok := other.(GoNativeArray); ok { - slice := goArray.underlying.anySlice(Zero, IntOfUint32(other.Length())) - underlying := &arrayStruct{ - contents: append([]interface{}(nil), slice...), - dims: []int{len(slice)}, - } - return GoNativeArray{underlying: underlying} - } - - // Fast path: if it's a ByteNativeArray, copy efficiently - if byteArray, ok := other.(ByteNativeArray); ok { - data := make([]byte, len(byteArray.underlying.contents)) - copy(data, byteArray.underlying.contents) - underlying := &arrayForByte{contents: data, dims: []int{len(data)}} - return ByteNativeArray{underlying: underlying} - } - - // Generic path: copy through interface - contents := make([]interface{}, other.Length()) - for i := uint32(0); i < other.Length(); i++ { - contents[i] = other.Select(i) - } - underlying := &arrayStruct{ - contents: contents, - dims: []int{len(contents)}, - } - return GoNativeArray{underlying: underlying} + return GoNativeArray{underlying: other.(GoNativeArray).underlying.ArrayCopy()} } // Array is the general interface for arrays. Conceptually, it contains some @@ -958,7 +796,11 @@ type Array interface { dimensionLength(dim int) int ArrayGet1(index int) interface{} ArraySet1(value interface{}, index int) + ArrayGetRange1(lo, hi int) Array + ArraySetRange1(index int, other Array) anySlice(lo, hi Int) []interface{} + ArrayCopy() Array + ArrayEqualUpTo(other Array, index int) bool // specializations ArrayGet1Byte(index int) byte ArraySet1Byte(value byte, index int) @@ -968,6 +810,27 @@ type Array interface { ArraySet1CodePoint(value CodePoint, index int) } +func defaultArrayEqualUpTo(left Array, right Array, index uint32) bool { + lSlice := left.anySlice(Zero, IntOfUint32(index)) + rSlice := right.anySlice(Zero, IntOfUint32(index)) + if len(lSlice) > 0 && IsEqualityComparable(lSlice[0]) { + return slices.Equal(lSlice, rSlice) + } + for i := uint32(0); i < index; i++ { + if !AreEqual(lSlice[i], rSlice[i]) { + return false + } + } + return true +} + +func defaultArraySetRange1(left Array, right Array, index int) { + rightLength := right.dimensionLength(0) + for j := 0; j < rightLength; j++ { + left.ArraySet1(right.ArrayGet1(j), int(index+j)) + } +} + /***** newArray *****/ // Multiply the numbers in "dims" and return the product as an "int". @@ -987,6 +850,25 @@ func computeTotalArrayLength(dims ...Int) int { return totalLength } +func NewArrayFromCharArray(values []Char) Array { + contents := make([]Char, len(values)) + copy(contents, values) + return &arrayForChar{ + contents: contents, + dims: []int{len(values)}, + } +} + +func NewArrayFromByteArray(values []byte) Array { + contents := make([]byte, len(values)) + copy(contents, values) + return &arrayForByte{ + contents: contents, + dims: []int{len(values)}, + } +} + + // NewArrayFromExample returns a new Array. // If "init" is non-nil, it is used to initialize all elements of the array. // "example" is used only to figure out the right kind of Array to return. @@ -1071,8 +953,8 @@ func newZeroLengthArray(intDims []int) Array { } } -// newArrayWithValues returns a new one-dimensional Array with the given initial -// values. It is only used internally, by *Builder.ToArray(). +// newArrayWithValues returns a new one-dimensional Array with the initial values. +// It is currently only used internally, by *Builder.ToArray(). func newArrayWithValues(values ...interface{}) Array { totalLength := len(values) intDims := []int{totalLength} @@ -1111,6 +993,53 @@ func newArrayWithValues(values ...interface{}) Array { } } +// newArrayWithInitFn returns a new one-dimensional Array with the given initial values. +// It is currently only used internally, by CompanionStruct_NativeArray_.MakeWithInit. +// It could potentially be used in the translation of Dafny array instantiations with initializing lambdas, +// but that is currently rewritten by the single-pass compiler instead. +func newArrayWithInitFn(init func(uint32) interface{}, length int) Array { + intDims := []int{length} + if length == 0 { + return newZeroLengthArray(intDims) + } + + // Inspect the type of the first initial value to consider Array specialization + value0 := init(0) + if _, ok := value0.(byte); ok { + arr := make([]byte, length) + arr[0] = value0.(byte) + for i := range arr[1:] { + arr[i] = init(uint32(i)).(byte) + } + return &arrayForByte{ + contents: arr, + dims: intDims, + } + } + if _, ok := value0.(Char); ok { + arr := make([]Char, length) + arr[0] = value0.(Char) + for i := range arr { + arr[i] = init(uint32(i)).(Char) + } + return &arrayForChar{ + contents: arr, + dims: intDims, + } + } + + // Use the default representation + arr := make([]interface{}, length) + arr[0] = value0 + for i := range arr[1:] { + arr[i] = init(uint32(i)) + } + return &arrayStruct{ + contents: arr, + dims: intDims, + } +} + // NewArrayWithValue returns a new Array full of the given initial value. func NewArrayWithValue(init interface{}, dims ...Int) Array { return NewArrayFromExample(init, init, dims...) @@ -1144,6 +1073,39 @@ func (_this arrayStruct) ArraySet1(value interface{}, index int) { _this.contents[index] = value } +func (_this arrayStruct) ArrayGetRange1(lo, hi int) Array { + newContents := _this.contents[lo:hi] + return &arrayStruct{ + contents: newContents, + dims: []int{int(hi - lo)}, + } +} + +func (_this arrayStruct) ArraySetRange1(index int, other Array) { + // Optimize for the same type of content array + if otherStruct, ok := other.(arrayStruct); ok { + copy(_this.contents[index:], otherStruct.contents) + } else { + defaultArraySetRange1(_this, other, index) + } +} + +func (_this arrayStruct) ArrayCopy() Array { + newContents := make([]interface{}, len(_this.contents)) + copy(newContents, _this.contents) + return &arrayStruct{ + contents: newContents, + // TODO: Does dims have to be copied as well? + dims: _this.dims, + } +} + +func (_this arrayStruct) ArrayEqualUpTo(other Array, index int) bool { + // Not much point in optimizing for the same type of content array + // since anySlice is cheap on arrayStructs. + return defaultArrayEqualUpTo(_this, other, uint32(index)) +} + func (_this arrayStruct) ArrayGet1Byte(index int) byte { panic("Expected specialized array type that contains bytes, but found general-purpose array of interface{}") } @@ -1214,6 +1176,43 @@ func (_this arrayForByte) ArraySet1(value interface{}, index int) { _this.contents[index] = value.(byte) } +func (_this arrayForByte) ArrayGetRange1(lo, hi int) Array { + newContents := _this.contents[lo:hi] + return &arrayForByte{ + contents: newContents, + dims: []int{int(hi - lo)}, + } +} + +func (_this arrayForByte) ArraySetRange1(index int, other Array) { + // Optimize for the same type of content array + if otherByte, ok := other.(arrayForByte); ok { + copy(_this.contents[index:], otherByte.contents) + } else { + defaultArraySetRange1(_this, other, index) + } +} + +func (_this arrayForByte) ArrayCopy() Array { + newContents := make([]byte, len(_this.contents)) + copy(newContents, _this.contents) + return &arrayForByte{ + contents: newContents, + // TODO: Does dims have to be copied as well? + dims: _this.dims, + } +} + +func (_this arrayForByte) ArrayEqualUpTo(other Array, index int) bool { + // Optimize for the same type of content array + if otherByte, ok := other.(arrayForByte); ok { + return slices.Equal(_this.contents[:index], otherByte.contents[:index]) + } else { + // Generic fallback + return defaultArrayEqualUpTo(_this, other, uint32(index)) + } +} + func (_this arrayForByte) ArrayGet1Byte(index int) byte { return _this.contents[index] } @@ -1286,6 +1285,43 @@ func (_this arrayForChar) ArraySet1(value interface{}, index int) { _this.contents[index] = value.(Char) } +func (_this arrayForChar) ArrayGetRange1(lo, hi int) Array { + newContents := _this.contents[lo:hi] + return &arrayForChar{ + contents: newContents, + dims: []int{int(hi - lo)}, + } +} + +func (_this arrayForChar) ArraySetRange1(index int, other Array) { + // Optimize for the same type of content array + if otherByte, ok := other.(arrayForChar); ok { + copy(_this.contents[index:], otherByte.contents) + } else { + defaultArraySetRange1(_this, other, index) + } +} + +func (_this arrayForChar) ArrayCopy() Array { + newContents := make([]Char, len(_this.contents)) + copy(newContents, _this.contents) + return &arrayForChar{ + contents: newContents, + // TODO: Does dims have to be copied as well? + dims: _this.dims, + } +} + +func (_this arrayForChar) ArrayEqualUpTo(other Array, index int) bool { + // Optimize for the same type of content array + if otherChar, ok := other.(arrayForChar); ok { + return slices.Equal(_this.contents[:index], otherChar.contents[:index]) + } else { + // Generic fallback + return defaultArrayEqualUpTo(_this, other, uint32(index)) + } +} + func (_this arrayForChar) ArrayGet1Byte(index int) byte { panic("Expected specialized array type that contains bytes, but found general-purpose array of interface{}") } @@ -1358,6 +1394,43 @@ func (_this arrayForCodePoint) ArraySet1(value interface{}, index int) { _this.contents[index] = value.(CodePoint) } +func (_this arrayForCodePoint) ArrayGetRange1(lo, hi int) Array { + newContents := _this.contents[lo:hi] + return &arrayForCodePoint{ + contents: newContents, + dims: []int{int(hi - lo)}, + } +} + +func (_this arrayForCodePoint) ArraySetRange1(index int, other Array) { + // Optimize for the same type of content array + if otherCodePoint, ok := other.(arrayForCodePoint); ok { + copy(_this.contents[index:], otherCodePoint.contents) + } else { + defaultArraySetRange1(_this, other, index) + } +} + +func (_this arrayForCodePoint) ArrayCopy() Array { + newContents := make([]CodePoint, len(_this.contents)) + copy(newContents, _this.contents) + return &arrayForCodePoint{ + contents: newContents, + // TODO: Does dims have to be copied as well? + dims: _this.dims, + } +} + +func (_this arrayForCodePoint) ArrayEqualUpTo(other Array, index int) bool { + // Optimize for the same type of content array + if otherCodePoint, ok := other.(arrayForCodePoint); ok { + return slices.Equal(_this.contents[:index], otherCodePoint.contents[:index]) + } else { + // Generic fallback + return defaultArrayEqualUpTo(_this, other, uint32(index)) + } +} + func (_this arrayForCodePoint) ArrayGet1Byte(index int) byte { panic("Expected specialized array type that contains bytes, but found general-purpose array of interface{}") } diff --git a/Source/DafnyRuntime/DafnyRuntimeGo/dafny/dafny_test.go b/Source/DafnyRuntime/DafnyRuntimeGo/dafny/dafny_test.go index 23c1f273b45..9a3975f0e7e 100644 --- a/Source/DafnyRuntime/DafnyRuntimeGo/dafny/dafny_test.go +++ b/Source/DafnyRuntime/DafnyRuntimeGo/dafny/dafny_test.go @@ -45,62 +45,54 @@ func TestLazySequence(t *testing.T) { func TestByteSequenceOptimization(t *testing.T) { // Test creating byte sequence from slice data := []byte{1, 2, 3, 4, 5} - seq := newByteSeq(data) + seq := SeqOf(data) // Verify it implements Sequence interface AssertImplementsSequence(seq, t) // Verify ToArray returns ByteNativeArray - arr := seq.ToArray() - if byteArr, ok := arr.(ByteNativeArray); ok { - if byteArr.Length() != 5 { - t.Errorf("Expected length 5, got %d", byteArr.Length()) - } - if byteArr.Select(0).(uint8) != 1 { - t.Errorf("Expected first element 1, got %v", byteArr.Select(0)) - } - } else { - t.Errorf("Expected ByteNativeArray, got %T", arr) - } + // arr := seq.ToArray() + // if byteArr, ok := arr.(ByteNativeArray); ok { + // if byteArr.Length() != 5 { + // t.Errorf("Expected length 5, got %d", byteArr.Length()) + // } + // if byteArr.Select(0).(uint8) != 1 { + // t.Errorf("Expected first element 1, got %v", byteArr.Select(0)) + // } + // } else { + // t.Errorf("Expected ByteNativeArray, got %T", arr) + // } } // Test optimization detection for uint8 vs non-uint8 -func TestTryByteSeq(t *testing.T) { +func TestSeqOf(t *testing.T) { // Test uint8 slice - should optimize uint8Contents := []interface{}{uint8(1), uint8(2), uint8(3)} - seq, optimized := tryByteSeq(uint8Contents) - if !optimized { + seq := SeqFromArray(uint8Contents, false) + AssertSequenceIsBackedByByteArray(seq, t) + if !SequenceIsBackedByByteArray(seq) { t.Error("Expected optimization for uint8 slice") } - if seq == nil { - t.Error("Expected non-nil sequence") - } // Verify it returns ByteNativeArray arr := seq.ToArray() - if _, ok := arr.(ByteNativeArray); !ok { + if _, ok := arr.(GoNativeArray); !ok { t.Errorf("Expected ByteNativeArray, got %T", arr) } // Test non-uint8 slice - should not optimize intContents := []interface{}{1, 2, 3} - seq2, optimized2 := tryByteSeq(intContents) - if optimized2 { + seq2 := SeqFromArray(intContents, false) + if SequenceIsBackedByByteArray(seq2) { t.Error("Expected no optimization for int slice") } - if seq2 != nil { - t.Error("Expected nil sequence for non-optimized case") - } // Test empty slice - should not optimize emptyContents := []interface{}{} - seq3, optimized3 := tryByteSeq(emptyContents) - if optimized3 { + seq3 := SeqFromArray(emptyContents, false) + if SequenceIsBackedByByteArray(seq3) { t.Error("Expected no optimization for empty slice") } - if seq3 != nil { - t.Error("Expected nil sequence for empty case") - } } // Test refactored CompanionStruct_NativeArray_ functions @@ -144,10 +136,10 @@ func TestNativeArrayFunctions(t *testing.T) { // Test Copy function with ByteNativeArray data := []byte{10, 20, 30} - byteSeq := newByteSeq(data) + byteSeq := SeqOfBytes(data) byteArr := byteSeq.ToArray() arr4 := Companion_NativeArray_.Copy(byteArr) - if byteArr4, ok := arr4.(ByteNativeArray); ok { + if byteArr4, ok := arr4.(GoNativeArray); ok { if byteArr4.Length() != 3 { t.Errorf("Expected length 3, got %d", byteArr4.Length()) } @@ -155,7 +147,7 @@ func TestNativeArrayFunctions(t *testing.T) { t.Errorf("Expected element at index 1 to be 20, got %v", byteArr4.Select(1)) } } else { - t.Errorf("Expected ByteNativeArray, got %T", arr4) + t.Errorf("Expected GoNativeArray, got %T", arr4) } } @@ -165,3 +157,25 @@ func AssertImplementsSequence(s interface{}, t *testing.T) { t.Errorf("Expected %v to implement the Sequence interface", s) } } + +func SequenceIsBackedByByteArray(seq Sequence) bool { + _, ok := seq.(*ArraySequence)._values.(GoNativeArray).underlying.(*arrayForByte) + return ok +} + +func AssertSequenceIsBackedByByteArray(seq Sequence, t *testing.T) { + as, ok := seq.(*ArraySequence) + if !ok { + t.Errorf("Expected %v to be an *ArraySequence", seq) + } + + gna, ok := as._values.(GoNativeArray) + if !ok { + t.Errorf("Expected %v to implement the GoNativeArray interface", as._values) + } + + _, ok = gna.underlying.(*arrayForByte) + if !ok { + t.Errorf("Expected %v to be an arrayForByte", gna.underlying) + } +} From ec60bcff6bee3e889a5c8b1e205d9c1aad25c940 Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Thu, 4 Sep 2025 14:30:57 -0700 Subject: [PATCH 04/11] Fix for loops --- Source/DafnyRuntime/DafnyRuntimeGo/dafny/dafny.go | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/Source/DafnyRuntime/DafnyRuntimeGo/dafny/dafny.go b/Source/DafnyRuntime/DafnyRuntimeGo/dafny/dafny.go index c0b442da651..079b49f8c76 100644 --- a/Source/DafnyRuntime/DafnyRuntimeGo/dafny/dafny.go +++ b/Source/DafnyRuntime/DafnyRuntimeGo/dafny/dafny.go @@ -1008,7 +1008,7 @@ func newArrayWithInitFn(init func(uint32) interface{}, length int) Array { if _, ok := value0.(byte); ok { arr := make([]byte, length) arr[0] = value0.(byte) - for i := range arr[1:] { + for i := 1; i < length; i++ { arr[i] = init(uint32(i)).(byte) } return &arrayForByte{ @@ -1019,7 +1019,7 @@ func newArrayWithInitFn(init func(uint32) interface{}, length int) Array { if _, ok := value0.(Char); ok { arr := make([]Char, length) arr[0] = value0.(Char) - for i := range arr { + for i := 1; i < length; i++ { arr[i] = init(uint32(i)).(Char) } return &arrayForChar{ @@ -1031,7 +1031,7 @@ func newArrayWithInitFn(init func(uint32) interface{}, length int) Array { // Use the default representation arr := make([]interface{}, length) arr[0] = value0 - for i := range arr[1:] { + for i := 1; i < length; i++ { arr[i] = init(uint32(i)) } return &arrayStruct{ From 5a420907de50bae2386076d5807b0c1934d1d568 Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Thu, 4 Sep 2025 15:35:35 -0700 Subject: [PATCH 05/11] cleanup --- .../DafnyRuntimeGo/dafny/dafny.go | 93 +++++++++---------- 1 file changed, 45 insertions(+), 48 deletions(-) diff --git a/Source/DafnyRuntime/DafnyRuntimeGo/dafny/dafny.go b/Source/DafnyRuntime/DafnyRuntimeGo/dafny/dafny.go index 079b49f8c76..fbb9291dde3 100644 --- a/Source/DafnyRuntime/DafnyRuntimeGo/dafny/dafny.go +++ b/Source/DafnyRuntime/DafnyRuntimeGo/dafny/dafny.go @@ -83,7 +83,7 @@ func (_static *CompanionStruct_Sequence_) EqualUpTo(left Sequence, right Sequenc } leftArr, rightArr := left.ToArray(), right.ToArray() - return leftArr.(GoNativeArray).underlying.ArrayEqualUpTo(rightArr.(GoNativeArray).underlying, int(index)) + return leftArr.(GoNativeArray).underlying.arrayEqualUpTo(rightArr.(GoNativeArray).underlying, int(index)) } func IsDafnyNull(x interface{}) bool { @@ -729,13 +729,31 @@ func ToByteArray(x Sequence) []byte { * Arrays ******************************************************************************/ +// A GoNativeArray is a single dimensional Array, +// wrapped up for the benefit of dafnyRuntime.dfy. // GoNativeArray wraps the Array interface for external compatibility -// while allowing optimized implementations internally +// while allowing optimized implementations internally. type GoNativeArray struct { underlying Array } -// GoNativeArray methods delegate to underlying Array implementation +func (CompanionStruct_NativeArray_) Make(length uint32) ImmutableArray { + underlying := &arrayStruct{ + contents: make([]interface{}, length), + dims: []int{int(length)}, + } + return GoNativeArray{underlying: underlying} +} + +func (CompanionStruct_NativeArray_) MakeWithInit(length uint32, init func(uint32) interface{}) ImmutableArray { + underlying := newArrayWithInitFn(init, int(length)) + return GoNativeArray{underlying: underlying} +} + +func (CompanionStruct_NativeArray_) Copy(other ImmutableArray) ImmutableArray { + return GoNativeArray{underlying: other.(GoNativeArray).underlying.arrayCopy()} +} + func (g GoNativeArray) Length() uint32 { return uint32(g.underlying.dimensionLength(0)) } @@ -749,7 +767,7 @@ func (g GoNativeArray) Update(i uint32, t interface{}) { } func (g GoNativeArray) UpdateSubarray(i uint32, other ImmutableArray) { - g.underlying.ArraySetRange1(int(i), other.(GoNativeArray).underlying) + g.underlying.arraySetRange1(int(i), other.(GoNativeArray).underlying) } func (g GoNativeArray) Freeze(size uint32) ImmutableArray { @@ -757,31 +775,13 @@ func (g GoNativeArray) Freeze(size uint32) ImmutableArray { } func (g GoNativeArray) Subarray(lo, hi uint32) ImmutableArray { - return GoNativeArray{underlying: g.underlying.ArrayGetRange1(int(lo), int(hi))} + return GoNativeArray{underlying: g.underlying.arrayGetRange1(int(lo), int(hi))} } func (g GoNativeArray) String() string { return "dafny.GoNativeArray" } -// CompanionStruct_NativeArray_ functions work with Array interface through GoNativeArray wrapper -func (CompanionStruct_NativeArray_) Make(length uint32) ImmutableArray { - underlying := &arrayStruct{ - contents: make([]interface{}, length), - dims: []int{int(length)}, - } - return GoNativeArray{underlying: underlying} -} - -func (CompanionStruct_NativeArray_) MakeWithInit(length uint32, init func(uint32) interface{}) ImmutableArray { - underlying := newArrayWithInitFn(init, int(length)) - return GoNativeArray{underlying: underlying} -} - -func (CompanionStruct_NativeArray_) Copy(other ImmutableArray) ImmutableArray { - return GoNativeArray{underlying: other.(GoNativeArray).underlying.ArrayCopy()} -} - // Array is the general interface for arrays. Conceptually, it contains some // underlying storage (a slice) of elements, together with a record of the length // of each dimension. Thus, this general interface supports 1- and multi-dimensional @@ -796,11 +796,11 @@ type Array interface { dimensionLength(dim int) int ArrayGet1(index int) interface{} ArraySet1(value interface{}, index int) - ArrayGetRange1(lo, hi int) Array - ArraySetRange1(index int, other Array) + arrayGetRange1(lo, hi int) Array + arraySetRange1(index int, other Array) anySlice(lo, hi Int) []interface{} - ArrayCopy() Array - ArrayEqualUpTo(other Array, index int) bool + arrayCopy() Array + arrayEqualUpTo(other Array, index int) bool // specializations ArrayGet1Byte(index int) byte ArraySet1Byte(value byte, index int) @@ -953,8 +953,8 @@ func newZeroLengthArray(intDims []int) Array { } } -// newArrayWithValues returns a new one-dimensional Array with the initial values. -// It is currently only used internally, by *Builder.ToArray(). +// newArrayWithValues returns a new one-dimensional Array with the given initial +// values. It is only used internally, by *Builder.ToArray(). func newArrayWithValues(values ...interface{}) Array { totalLength := len(values) intDims := []int{totalLength} @@ -1073,7 +1073,7 @@ func (_this arrayStruct) ArraySet1(value interface{}, index int) { _this.contents[index] = value } -func (_this arrayStruct) ArrayGetRange1(lo, hi int) Array { +func (_this arrayStruct) arrayGetRange1(lo, hi int) Array { newContents := _this.contents[lo:hi] return &arrayStruct{ contents: newContents, @@ -1081,7 +1081,7 @@ func (_this arrayStruct) ArrayGetRange1(lo, hi int) Array { } } -func (_this arrayStruct) ArraySetRange1(index int, other Array) { +func (_this arrayStruct) arraySetRange1(index int, other Array) { // Optimize for the same type of content array if otherStruct, ok := other.(arrayStruct); ok { copy(_this.contents[index:], otherStruct.contents) @@ -1090,7 +1090,7 @@ func (_this arrayStruct) ArraySetRange1(index int, other Array) { } } -func (_this arrayStruct) ArrayCopy() Array { +func (_this arrayStruct) arrayCopy() Array { newContents := make([]interface{}, len(_this.contents)) copy(newContents, _this.contents) return &arrayStruct{ @@ -1100,7 +1100,7 @@ func (_this arrayStruct) ArrayCopy() Array { } } -func (_this arrayStruct) ArrayEqualUpTo(other Array, index int) bool { +func (_this arrayStruct) arrayEqualUpTo(other Array, index int) bool { // Not much point in optimizing for the same type of content array // since anySlice is cheap on arrayStructs. return defaultArrayEqualUpTo(_this, other, uint32(index)) @@ -1176,7 +1176,7 @@ func (_this arrayForByte) ArraySet1(value interface{}, index int) { _this.contents[index] = value.(byte) } -func (_this arrayForByte) ArrayGetRange1(lo, hi int) Array { +func (_this arrayForByte) arrayGetRange1(lo, hi int) Array { newContents := _this.contents[lo:hi] return &arrayForByte{ contents: newContents, @@ -1184,7 +1184,7 @@ func (_this arrayForByte) ArrayGetRange1(lo, hi int) Array { } } -func (_this arrayForByte) ArraySetRange1(index int, other Array) { +func (_this arrayForByte) arraySetRange1(index int, other Array) { // Optimize for the same type of content array if otherByte, ok := other.(arrayForByte); ok { copy(_this.contents[index:], otherByte.contents) @@ -1193,7 +1193,7 @@ func (_this arrayForByte) ArraySetRange1(index int, other Array) { } } -func (_this arrayForByte) ArrayCopy() Array { +func (_this arrayForByte) arrayCopy() Array { newContents := make([]byte, len(_this.contents)) copy(newContents, _this.contents) return &arrayForByte{ @@ -1203,12 +1203,11 @@ func (_this arrayForByte) ArrayCopy() Array { } } -func (_this arrayForByte) ArrayEqualUpTo(other Array, index int) bool { +func (_this arrayForByte) arrayEqualUpTo(other Array, index int) bool { // Optimize for the same type of content array if otherByte, ok := other.(arrayForByte); ok { return slices.Equal(_this.contents[:index], otherByte.contents[:index]) } else { - // Generic fallback return defaultArrayEqualUpTo(_this, other, uint32(index)) } } @@ -1285,7 +1284,7 @@ func (_this arrayForChar) ArraySet1(value interface{}, index int) { _this.contents[index] = value.(Char) } -func (_this arrayForChar) ArrayGetRange1(lo, hi int) Array { +func (_this arrayForChar) arrayGetRange1(lo, hi int) Array { newContents := _this.contents[lo:hi] return &arrayForChar{ contents: newContents, @@ -1293,7 +1292,7 @@ func (_this arrayForChar) ArrayGetRange1(lo, hi int) Array { } } -func (_this arrayForChar) ArraySetRange1(index int, other Array) { +func (_this arrayForChar) arraySetRange1(index int, other Array) { // Optimize for the same type of content array if otherByte, ok := other.(arrayForChar); ok { copy(_this.contents[index:], otherByte.contents) @@ -1302,7 +1301,7 @@ func (_this arrayForChar) ArraySetRange1(index int, other Array) { } } -func (_this arrayForChar) ArrayCopy() Array { +func (_this arrayForChar) arrayCopy() Array { newContents := make([]Char, len(_this.contents)) copy(newContents, _this.contents) return &arrayForChar{ @@ -1312,12 +1311,11 @@ func (_this arrayForChar) ArrayCopy() Array { } } -func (_this arrayForChar) ArrayEqualUpTo(other Array, index int) bool { +func (_this arrayForChar) arrayEqualUpTo(other Array, index int) bool { // Optimize for the same type of content array if otherChar, ok := other.(arrayForChar); ok { return slices.Equal(_this.contents[:index], otherChar.contents[:index]) } else { - // Generic fallback return defaultArrayEqualUpTo(_this, other, uint32(index)) } } @@ -1394,7 +1392,7 @@ func (_this arrayForCodePoint) ArraySet1(value interface{}, index int) { _this.contents[index] = value.(CodePoint) } -func (_this arrayForCodePoint) ArrayGetRange1(lo, hi int) Array { +func (_this arrayForCodePoint) arrayGetRange1(lo, hi int) Array { newContents := _this.contents[lo:hi] return &arrayForCodePoint{ contents: newContents, @@ -1402,7 +1400,7 @@ func (_this arrayForCodePoint) ArrayGetRange1(lo, hi int) Array { } } -func (_this arrayForCodePoint) ArraySetRange1(index int, other Array) { +func (_this arrayForCodePoint) arraySetRange1(index int, other Array) { // Optimize for the same type of content array if otherCodePoint, ok := other.(arrayForCodePoint); ok { copy(_this.contents[index:], otherCodePoint.contents) @@ -1411,7 +1409,7 @@ func (_this arrayForCodePoint) ArraySetRange1(index int, other Array) { } } -func (_this arrayForCodePoint) ArrayCopy() Array { +func (_this arrayForCodePoint) arrayCopy() Array { newContents := make([]CodePoint, len(_this.contents)) copy(newContents, _this.contents) return &arrayForCodePoint{ @@ -1421,12 +1419,11 @@ func (_this arrayForCodePoint) ArrayCopy() Array { } } -func (_this arrayForCodePoint) ArrayEqualUpTo(other Array, index int) bool { +func (_this arrayForCodePoint) arrayEqualUpTo(other Array, index int) bool { // Optimize for the same type of content array if otherCodePoint, ok := other.(arrayForCodePoint); ok { return slices.Equal(_this.contents[:index], otherCodePoint.contents[:index]) } else { - // Generic fallback return defaultArrayEqualUpTo(_this, other, uint32(index)) } } From 3b1e5a315b2052f82b3fa6fd2e20870e50490e84 Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Thu, 4 Sep 2025 15:37:38 -0700 Subject: [PATCH 06/11] More cleanup --- Source/DafnyRuntime/DafnyRuntimeGo/dafny/dafny.go | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/Source/DafnyRuntime/DafnyRuntimeGo/dafny/dafny.go b/Source/DafnyRuntime/DafnyRuntimeGo/dafny/dafny.go index fbb9291dde3..804680f9349 100644 --- a/Source/DafnyRuntime/DafnyRuntimeGo/dafny/dafny.go +++ b/Source/DafnyRuntime/DafnyRuntimeGo/dafny/dafny.go @@ -737,7 +737,7 @@ type GoNativeArray struct { underlying Array } -func (CompanionStruct_NativeArray_) Make(length uint32) ImmutableArray { +func (CompanionStruct_NativeArray_) Make(length uint32) NativeArray { underlying := &arrayStruct{ contents: make([]interface{}, length), dims: []int{int(length)}, @@ -745,12 +745,12 @@ func (CompanionStruct_NativeArray_) Make(length uint32) ImmutableArray { return GoNativeArray{underlying: underlying} } -func (CompanionStruct_NativeArray_) MakeWithInit(length uint32, init func(uint32) interface{}) ImmutableArray { +func (CompanionStruct_NativeArray_) MakeWithInit(length uint32, init func(uint32) interface{}) NativeArray { underlying := newArrayWithInitFn(init, int(length)) return GoNativeArray{underlying: underlying} } -func (CompanionStruct_NativeArray_) Copy(other ImmutableArray) ImmutableArray { +func (CompanionStruct_NativeArray_) Copy(other ImmutableArray) NativeArray { return GoNativeArray{underlying: other.(GoNativeArray).underlying.arrayCopy()} } From f3c9137702c3d61e31e485e2e218440592d3cae9 Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Thu, 4 Sep 2025 16:15:49 -0700 Subject: [PATCH 07/11] Optimize ArrayRangeToSeq too --- .../DafnyRuntimeGo/dafny/dafny.go | 65 ++++++++++++++----- .../DafnyRuntimeGo/dafny/dafny_test.go | 2 +- 2 files changed, 50 insertions(+), 17 deletions(-) diff --git a/Source/DafnyRuntime/DafnyRuntimeGo/dafny/dafny.go b/Source/DafnyRuntime/DafnyRuntimeGo/dafny/dafny.go index 804680f9349..eb35537704c 100644 --- a/Source/DafnyRuntime/DafnyRuntimeGo/dafny/dafny.go +++ b/Source/DafnyRuntime/DafnyRuntimeGo/dafny/dafny.go @@ -775,7 +775,7 @@ func (g GoNativeArray) Freeze(size uint32) ImmutableArray { } func (g GoNativeArray) Subarray(lo, hi uint32) ImmutableArray { - return GoNativeArray{underlying: g.underlying.arrayGetRange1(int(lo), int(hi))} + return GoNativeArray{underlying: g.underlying.arrayGetRange1(IntOfUint32(lo), IntOfUint32(hi))} } func (g GoNativeArray) String() string { @@ -796,7 +796,7 @@ type Array interface { dimensionLength(dim int) int ArrayGet1(index int) interface{} ArraySet1(value interface{}, index int) - arrayGetRange1(lo, hi int) Array + arrayGetRange1(lo, hi Int) Array arraySetRange1(index int, other Array) anySlice(lo, hi Int) []interface{} arrayCopy() Array @@ -1073,11 +1073,19 @@ func (_this arrayStruct) ArraySet1(value interface{}, index int) { _this.contents[index] = value } -func (_this arrayStruct) arrayGetRange1(lo, hi int) Array { - newContents := _this.contents[lo:hi] +func (_this arrayStruct) arrayGetRange1(lo, hi Int) Array { + if lo.IsNilInt() { + lo = Zero + } + if hi.IsNilInt() { + hi = IntOf(len(_this.contents)) + } + iLo := lo.Int() + iHi := hi.Int() + newContents := _this.contents[iLo:iHi] return &arrayStruct{ contents: newContents, - dims: []int{int(hi - lo)}, + dims: []int{int(iHi - iLo)}, } } @@ -1176,11 +1184,19 @@ func (_this arrayForByte) ArraySet1(value interface{}, index int) { _this.contents[index] = value.(byte) } -func (_this arrayForByte) arrayGetRange1(lo, hi int) Array { - newContents := _this.contents[lo:hi] +func (_this arrayForByte) arrayGetRange1(lo, hi Int) Array { + if lo.IsNilInt() { + lo = Zero + } + if hi.IsNilInt() { + hi = IntOf(len(_this.contents)) + } + iLo := lo.Int() + iHi := hi.Int() + newContents := _this.contents[iLo:iHi] return &arrayForByte{ contents: newContents, - dims: []int{int(hi - lo)}, + dims: []int{int(iHi - iLo)}, } } @@ -1284,11 +1300,19 @@ func (_this arrayForChar) ArraySet1(value interface{}, index int) { _this.contents[index] = value.(Char) } -func (_this arrayForChar) arrayGetRange1(lo, hi int) Array { - newContents := _this.contents[lo:hi] +func (_this arrayForChar) arrayGetRange1(lo, hi Int) Array { + if lo.IsNilInt() { + lo = Zero + } + if hi.IsNilInt() { + hi = IntOf(len(_this.contents)) + } + iLo := lo.Int() + iHi := hi.Int() + newContents := _this.contents[iLo:iHi] return &arrayForChar{ contents: newContents, - dims: []int{int(hi - lo)}, + dims: []int{int(iHi - iLo)}, } } @@ -1392,11 +1416,19 @@ func (_this arrayForCodePoint) ArraySet1(value interface{}, index int) { _this.contents[index] = value.(CodePoint) } -func (_this arrayForCodePoint) arrayGetRange1(lo, hi int) Array { - newContents := _this.contents[lo:hi] +func (_this arrayForCodePoint) arrayGetRange1(lo, hi Int) Array { + if lo.IsNilInt() { + lo = Zero + } + if hi.IsNilInt() { + hi = IntOf(len(_this.contents)) + } + iLo := lo.Int() + iHi := hi.Int() + newContents := _this.contents[iLo:iHi] return &arrayForCodePoint{ contents: newContents, - dims: []int{int(hi - lo)}, + dims: []int{int(iHi - iLo)}, } } @@ -1532,8 +1564,9 @@ func ArrayRangeToSeq(array Array, lo, hi Int) Sequence { _, isString = array.ArrayGet1(0).(Char) } - anySlice := array.anySlice(lo, hi) - seq := SeqOf(anySlice...) + seq := New_ArraySequence_() + underlying := array.arrayGetRange1(lo, hi).arrayCopy() + seq.Ctor__(GoNativeArray{underlying: underlying}, false) seq.IsString_set_(isString) return seq } diff --git a/Source/DafnyRuntime/DafnyRuntimeGo/dafny/dafny_test.go b/Source/DafnyRuntime/DafnyRuntimeGo/dafny/dafny_test.go index 9a3975f0e7e..93b079dd7e4 100644 --- a/Source/DafnyRuntime/DafnyRuntimeGo/dafny/dafny_test.go +++ b/Source/DafnyRuntime/DafnyRuntimeGo/dafny/dafny_test.go @@ -122,7 +122,7 @@ func TestNativeArrayFunctions(t *testing.T) { } // Test Copy function with GoNativeArray - arr3 := Companion_NativeArray_.Copy(arr2) + arr3 := Companion_NativeArray_.Copy(arr2.(GoNativeArray)) if goArr3, ok := arr3.(GoNativeArray); ok { if goArr3.Length() != 3 { t.Errorf("Expected length 3, got %d", goArr3.Length()) From 362ea7919c26fbacde8d1db67fd28bbbc85d8a42 Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Thu, 4 Sep 2025 16:53:49 -0700 Subject: [PATCH 08/11] Fix ToByteArray --- Source/DafnyRuntime/DafnyRuntimeGo/dafny/dafny.go | 13 +++++++++++-- 1 file changed, 11 insertions(+), 2 deletions(-) diff --git a/Source/DafnyRuntime/DafnyRuntimeGo/dafny/dafny.go b/Source/DafnyRuntime/DafnyRuntimeGo/dafny/dafny.go index eb35537704c..97b554d45a4 100644 --- a/Source/DafnyRuntime/DafnyRuntimeGo/dafny/dafny.go +++ b/Source/DafnyRuntime/DafnyRuntimeGo/dafny/dafny.go @@ -720,8 +720,17 @@ func (seq *LazySequence) ToByteArray() []byte { func ToByteArray(x Sequence) []byte { arr := x.ToArray() - result := make([]byte, arr.Length()) - copy(result, arr.(GoNativeArray).underlying.(arrayForByte).contents) + + length := arr.Length() + result := make([]byte, length) + // Optimize for the same kind of content array + if arrayByte, ok := arr.(GoNativeArray).underlying.(*arrayForByte); ok { + copy(result, arrayByte.contents) + } else { + for i := uint32(0); i < length; i++ { + result[i] = arr.Select(i).(byte) + } + } return result } From 55839578c428eac2d8b9356a672a15fad5ec8dd3 Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Thu, 4 Sep 2025 16:59:02 -0700 Subject: [PATCH 09/11] Uncomment test --- .../DafnyRuntimeGo-gomod/dafny/dafny.go | 165 +++++++++++------- .../DafnyRuntimeGo-gomod/dafny/dafny_test.go | 54 ++---- .../DafnyRuntimeGo/dafny/dafny_test.go | 52 ++---- 3 files changed, 137 insertions(+), 134 deletions(-) diff --git a/Source/DafnyRuntime/DafnyRuntimeGo-gomod/dafny/dafny.go b/Source/DafnyRuntime/DafnyRuntimeGo-gomod/dafny/dafny.go index c0b442da651..97b554d45a4 100644 --- a/Source/DafnyRuntime/DafnyRuntimeGo-gomod/dafny/dafny.go +++ b/Source/DafnyRuntime/DafnyRuntimeGo-gomod/dafny/dafny.go @@ -83,7 +83,7 @@ func (_static *CompanionStruct_Sequence_) EqualUpTo(left Sequence, right Sequenc } leftArr, rightArr := left.ToArray(), right.ToArray() - return leftArr.(GoNativeArray).underlying.ArrayEqualUpTo(rightArr.(GoNativeArray).underlying, int(index)) + return leftArr.(GoNativeArray).underlying.arrayEqualUpTo(rightArr.(GoNativeArray).underlying, int(index)) } func IsDafnyNull(x interface{}) bool { @@ -720,8 +720,17 @@ func (seq *LazySequence) ToByteArray() []byte { func ToByteArray(x Sequence) []byte { arr := x.ToArray() - result := make([]byte, arr.Length()) - copy(result, arr.(GoNativeArray).underlying.(arrayForByte).contents) + + length := arr.Length() + result := make([]byte, length) + // Optimize for the same kind of content array + if arrayByte, ok := arr.(GoNativeArray).underlying.(*arrayForByte); ok { + copy(result, arrayByte.contents) + } else { + for i := uint32(0); i < length; i++ { + result[i] = arr.Select(i).(byte) + } + } return result } @@ -729,13 +738,31 @@ func ToByteArray(x Sequence) []byte { * Arrays ******************************************************************************/ +// A GoNativeArray is a single dimensional Array, +// wrapped up for the benefit of dafnyRuntime.dfy. // GoNativeArray wraps the Array interface for external compatibility -// while allowing optimized implementations internally +// while allowing optimized implementations internally. type GoNativeArray struct { underlying Array } -// GoNativeArray methods delegate to underlying Array implementation +func (CompanionStruct_NativeArray_) Make(length uint32) NativeArray { + underlying := &arrayStruct{ + contents: make([]interface{}, length), + dims: []int{int(length)}, + } + return GoNativeArray{underlying: underlying} +} + +func (CompanionStruct_NativeArray_) MakeWithInit(length uint32, init func(uint32) interface{}) NativeArray { + underlying := newArrayWithInitFn(init, int(length)) + return GoNativeArray{underlying: underlying} +} + +func (CompanionStruct_NativeArray_) Copy(other ImmutableArray) NativeArray { + return GoNativeArray{underlying: other.(GoNativeArray).underlying.arrayCopy()} +} + func (g GoNativeArray) Length() uint32 { return uint32(g.underlying.dimensionLength(0)) } @@ -749,7 +776,7 @@ func (g GoNativeArray) Update(i uint32, t interface{}) { } func (g GoNativeArray) UpdateSubarray(i uint32, other ImmutableArray) { - g.underlying.ArraySetRange1(int(i), other.(GoNativeArray).underlying) + g.underlying.arraySetRange1(int(i), other.(GoNativeArray).underlying) } func (g GoNativeArray) Freeze(size uint32) ImmutableArray { @@ -757,31 +784,13 @@ func (g GoNativeArray) Freeze(size uint32) ImmutableArray { } func (g GoNativeArray) Subarray(lo, hi uint32) ImmutableArray { - return GoNativeArray{underlying: g.underlying.ArrayGetRange1(int(lo), int(hi))} + return GoNativeArray{underlying: g.underlying.arrayGetRange1(IntOfUint32(lo), IntOfUint32(hi))} } func (g GoNativeArray) String() string { return "dafny.GoNativeArray" } -// CompanionStruct_NativeArray_ functions work with Array interface through GoNativeArray wrapper -func (CompanionStruct_NativeArray_) Make(length uint32) ImmutableArray { - underlying := &arrayStruct{ - contents: make([]interface{}, length), - dims: []int{int(length)}, - } - return GoNativeArray{underlying: underlying} -} - -func (CompanionStruct_NativeArray_) MakeWithInit(length uint32, init func(uint32) interface{}) ImmutableArray { - underlying := newArrayWithInitFn(init, int(length)) - return GoNativeArray{underlying: underlying} -} - -func (CompanionStruct_NativeArray_) Copy(other ImmutableArray) ImmutableArray { - return GoNativeArray{underlying: other.(GoNativeArray).underlying.ArrayCopy()} -} - // Array is the general interface for arrays. Conceptually, it contains some // underlying storage (a slice) of elements, together with a record of the length // of each dimension. Thus, this general interface supports 1- and multi-dimensional @@ -796,11 +805,11 @@ type Array interface { dimensionLength(dim int) int ArrayGet1(index int) interface{} ArraySet1(value interface{}, index int) - ArrayGetRange1(lo, hi int) Array - ArraySetRange1(index int, other Array) + arrayGetRange1(lo, hi Int) Array + arraySetRange1(index int, other Array) anySlice(lo, hi Int) []interface{} - ArrayCopy() Array - ArrayEqualUpTo(other Array, index int) bool + arrayCopy() Array + arrayEqualUpTo(other Array, index int) bool // specializations ArrayGet1Byte(index int) byte ArraySet1Byte(value byte, index int) @@ -953,8 +962,8 @@ func newZeroLengthArray(intDims []int) Array { } } -// newArrayWithValues returns a new one-dimensional Array with the initial values. -// It is currently only used internally, by *Builder.ToArray(). +// newArrayWithValues returns a new one-dimensional Array with the given initial +// values. It is only used internally, by *Builder.ToArray(). func newArrayWithValues(values ...interface{}) Array { totalLength := len(values) intDims := []int{totalLength} @@ -1008,7 +1017,7 @@ func newArrayWithInitFn(init func(uint32) interface{}, length int) Array { if _, ok := value0.(byte); ok { arr := make([]byte, length) arr[0] = value0.(byte) - for i := range arr[1:] { + for i := 1; i < length; i++ { arr[i] = init(uint32(i)).(byte) } return &arrayForByte{ @@ -1019,7 +1028,7 @@ func newArrayWithInitFn(init func(uint32) interface{}, length int) Array { if _, ok := value0.(Char); ok { arr := make([]Char, length) arr[0] = value0.(Char) - for i := range arr { + for i := 1; i < length; i++ { arr[i] = init(uint32(i)).(Char) } return &arrayForChar{ @@ -1031,7 +1040,7 @@ func newArrayWithInitFn(init func(uint32) interface{}, length int) Array { // Use the default representation arr := make([]interface{}, length) arr[0] = value0 - for i := range arr[1:] { + for i := 1; i < length; i++ { arr[i] = init(uint32(i)) } return &arrayStruct{ @@ -1073,15 +1082,23 @@ func (_this arrayStruct) ArraySet1(value interface{}, index int) { _this.contents[index] = value } -func (_this arrayStruct) ArrayGetRange1(lo, hi int) Array { - newContents := _this.contents[lo:hi] +func (_this arrayStruct) arrayGetRange1(lo, hi Int) Array { + if lo.IsNilInt() { + lo = Zero + } + if hi.IsNilInt() { + hi = IntOf(len(_this.contents)) + } + iLo := lo.Int() + iHi := hi.Int() + newContents := _this.contents[iLo:iHi] return &arrayStruct{ contents: newContents, - dims: []int{int(hi - lo)}, + dims: []int{int(iHi - iLo)}, } } -func (_this arrayStruct) ArraySetRange1(index int, other Array) { +func (_this arrayStruct) arraySetRange1(index int, other Array) { // Optimize for the same type of content array if otherStruct, ok := other.(arrayStruct); ok { copy(_this.contents[index:], otherStruct.contents) @@ -1090,7 +1107,7 @@ func (_this arrayStruct) ArraySetRange1(index int, other Array) { } } -func (_this arrayStruct) ArrayCopy() Array { +func (_this arrayStruct) arrayCopy() Array { newContents := make([]interface{}, len(_this.contents)) copy(newContents, _this.contents) return &arrayStruct{ @@ -1100,7 +1117,7 @@ func (_this arrayStruct) ArrayCopy() Array { } } -func (_this arrayStruct) ArrayEqualUpTo(other Array, index int) bool { +func (_this arrayStruct) arrayEqualUpTo(other Array, index int) bool { // Not much point in optimizing for the same type of content array // since anySlice is cheap on arrayStructs. return defaultArrayEqualUpTo(_this, other, uint32(index)) @@ -1176,15 +1193,23 @@ func (_this arrayForByte) ArraySet1(value interface{}, index int) { _this.contents[index] = value.(byte) } -func (_this arrayForByte) ArrayGetRange1(lo, hi int) Array { - newContents := _this.contents[lo:hi] +func (_this arrayForByte) arrayGetRange1(lo, hi Int) Array { + if lo.IsNilInt() { + lo = Zero + } + if hi.IsNilInt() { + hi = IntOf(len(_this.contents)) + } + iLo := lo.Int() + iHi := hi.Int() + newContents := _this.contents[iLo:iHi] return &arrayForByte{ contents: newContents, - dims: []int{int(hi - lo)}, + dims: []int{int(iHi - iLo)}, } } -func (_this arrayForByte) ArraySetRange1(index int, other Array) { +func (_this arrayForByte) arraySetRange1(index int, other Array) { // Optimize for the same type of content array if otherByte, ok := other.(arrayForByte); ok { copy(_this.contents[index:], otherByte.contents) @@ -1193,7 +1218,7 @@ func (_this arrayForByte) ArraySetRange1(index int, other Array) { } } -func (_this arrayForByte) ArrayCopy() Array { +func (_this arrayForByte) arrayCopy() Array { newContents := make([]byte, len(_this.contents)) copy(newContents, _this.contents) return &arrayForByte{ @@ -1203,12 +1228,11 @@ func (_this arrayForByte) ArrayCopy() Array { } } -func (_this arrayForByte) ArrayEqualUpTo(other Array, index int) bool { +func (_this arrayForByte) arrayEqualUpTo(other Array, index int) bool { // Optimize for the same type of content array if otherByte, ok := other.(arrayForByte); ok { return slices.Equal(_this.contents[:index], otherByte.contents[:index]) } else { - // Generic fallback return defaultArrayEqualUpTo(_this, other, uint32(index)) } } @@ -1285,15 +1309,23 @@ func (_this arrayForChar) ArraySet1(value interface{}, index int) { _this.contents[index] = value.(Char) } -func (_this arrayForChar) ArrayGetRange1(lo, hi int) Array { - newContents := _this.contents[lo:hi] +func (_this arrayForChar) arrayGetRange1(lo, hi Int) Array { + if lo.IsNilInt() { + lo = Zero + } + if hi.IsNilInt() { + hi = IntOf(len(_this.contents)) + } + iLo := lo.Int() + iHi := hi.Int() + newContents := _this.contents[iLo:iHi] return &arrayForChar{ contents: newContents, - dims: []int{int(hi - lo)}, + dims: []int{int(iHi - iLo)}, } } -func (_this arrayForChar) ArraySetRange1(index int, other Array) { +func (_this arrayForChar) arraySetRange1(index int, other Array) { // Optimize for the same type of content array if otherByte, ok := other.(arrayForChar); ok { copy(_this.contents[index:], otherByte.contents) @@ -1302,7 +1334,7 @@ func (_this arrayForChar) ArraySetRange1(index int, other Array) { } } -func (_this arrayForChar) ArrayCopy() Array { +func (_this arrayForChar) arrayCopy() Array { newContents := make([]Char, len(_this.contents)) copy(newContents, _this.contents) return &arrayForChar{ @@ -1312,12 +1344,11 @@ func (_this arrayForChar) ArrayCopy() Array { } } -func (_this arrayForChar) ArrayEqualUpTo(other Array, index int) bool { +func (_this arrayForChar) arrayEqualUpTo(other Array, index int) bool { // Optimize for the same type of content array if otherChar, ok := other.(arrayForChar); ok { return slices.Equal(_this.contents[:index], otherChar.contents[:index]) } else { - // Generic fallback return defaultArrayEqualUpTo(_this, other, uint32(index)) } } @@ -1394,15 +1425,23 @@ func (_this arrayForCodePoint) ArraySet1(value interface{}, index int) { _this.contents[index] = value.(CodePoint) } -func (_this arrayForCodePoint) ArrayGetRange1(lo, hi int) Array { - newContents := _this.contents[lo:hi] +func (_this arrayForCodePoint) arrayGetRange1(lo, hi Int) Array { + if lo.IsNilInt() { + lo = Zero + } + if hi.IsNilInt() { + hi = IntOf(len(_this.contents)) + } + iLo := lo.Int() + iHi := hi.Int() + newContents := _this.contents[iLo:iHi] return &arrayForCodePoint{ contents: newContents, - dims: []int{int(hi - lo)}, + dims: []int{int(iHi - iLo)}, } } -func (_this arrayForCodePoint) ArraySetRange1(index int, other Array) { +func (_this arrayForCodePoint) arraySetRange1(index int, other Array) { // Optimize for the same type of content array if otherCodePoint, ok := other.(arrayForCodePoint); ok { copy(_this.contents[index:], otherCodePoint.contents) @@ -1411,7 +1450,7 @@ func (_this arrayForCodePoint) ArraySetRange1(index int, other Array) { } } -func (_this arrayForCodePoint) ArrayCopy() Array { +func (_this arrayForCodePoint) arrayCopy() Array { newContents := make([]CodePoint, len(_this.contents)) copy(newContents, _this.contents) return &arrayForCodePoint{ @@ -1421,12 +1460,11 @@ func (_this arrayForCodePoint) ArrayCopy() Array { } } -func (_this arrayForCodePoint) ArrayEqualUpTo(other Array, index int) bool { +func (_this arrayForCodePoint) arrayEqualUpTo(other Array, index int) bool { // Optimize for the same type of content array if otherCodePoint, ok := other.(arrayForCodePoint); ok { return slices.Equal(_this.contents[:index], otherCodePoint.contents[:index]) } else { - // Generic fallback return defaultArrayEqualUpTo(_this, other, uint32(index)) } } @@ -1535,8 +1573,9 @@ func ArrayRangeToSeq(array Array, lo, hi Int) Sequence { _, isString = array.ArrayGet1(0).(Char) } - anySlice := array.anySlice(lo, hi) - seq := SeqOf(anySlice...) + seq := New_ArraySequence_() + underlying := array.arrayGetRange1(lo, hi).arrayCopy() + seq.Ctor__(GoNativeArray{underlying: underlying}, false) seq.IsString_set_(isString) return seq } diff --git a/Source/DafnyRuntime/DafnyRuntimeGo-gomod/dafny/dafny_test.go b/Source/DafnyRuntime/DafnyRuntimeGo-gomod/dafny/dafny_test.go index 9a3975f0e7e..c5a4d2da4f6 100644 --- a/Source/DafnyRuntime/DafnyRuntimeGo-gomod/dafny/dafny_test.go +++ b/Source/DafnyRuntime/DafnyRuntimeGo-gomod/dafny/dafny_test.go @@ -41,27 +41,27 @@ func TestLazySequence(t *testing.T) { AssertImplementsSequence(lazySeq, t) } -// Test byte sequence optimization using ByteNativeArray wrapper +// Test byte sequence optimization using arrayForByte wrapper func TestByteSequenceOptimization(t *testing.T) { // Test creating byte sequence from slice data := []byte{1, 2, 3, 4, 5} - seq := SeqOf(data) + seq := SeqOfBytes(data) // Verify it implements Sequence interface AssertImplementsSequence(seq, t) - // Verify ToArray returns ByteNativeArray - // arr := seq.ToArray() - // if byteArr, ok := arr.(ByteNativeArray); ok { - // if byteArr.Length() != 5 { - // t.Errorf("Expected length 5, got %d", byteArr.Length()) - // } - // if byteArr.Select(0).(uint8) != 1 { - // t.Errorf("Expected first element 1, got %v", byteArr.Select(0)) - // } - // } else { - // t.Errorf("Expected ByteNativeArray, got %T", arr) - // } + // Verify ToArray returns GoNativeArray + arr := seq.ToArray() + if byteArr, ok := arr.(GoNativeArray); ok { + if byteArr.Length() != 5 { + t.Errorf("Expected length 5, got %d", byteArr.Length()) + } + if byteArr.Select(0).(uint8) != 1 { + t.Errorf("Expected first element 1, got %v", byteArr.Select(0)) + } + } else { + t.Errorf("Expected GoNativeArray, got %T", arr) + } } // Test optimization detection for uint8 vs non-uint8 @@ -69,15 +69,14 @@ func TestSeqOf(t *testing.T) { // Test uint8 slice - should optimize uint8Contents := []interface{}{uint8(1), uint8(2), uint8(3)} seq := SeqFromArray(uint8Contents, false) - AssertSequenceIsBackedByByteArray(seq, t) if !SequenceIsBackedByByteArray(seq) { t.Error("Expected optimization for uint8 slice") } - // Verify it returns ByteNativeArray + // Verify it returns GoNativeArray arr := seq.ToArray() if _, ok := arr.(GoNativeArray); !ok { - t.Errorf("Expected ByteNativeArray, got %T", arr) + t.Errorf("Expected GoNativeArray, got %T", arr) } // Test non-uint8 slice - should not optimize @@ -122,7 +121,7 @@ func TestNativeArrayFunctions(t *testing.T) { } // Test Copy function with GoNativeArray - arr3 := Companion_NativeArray_.Copy(arr2) + arr3 := Companion_NativeArray_.Copy(arr2.(GoNativeArray)) if goArr3, ok := arr3.(GoNativeArray); ok { if goArr3.Length() != 3 { t.Errorf("Expected length 3, got %d", goArr3.Length()) @@ -134,7 +133,7 @@ func TestNativeArrayFunctions(t *testing.T) { t.Errorf("Expected GoNativeArray, got %T", arr3) } - // Test Copy function with ByteNativeArray + // Test Copy function with GoNativeArray data := []byte{10, 20, 30} byteSeq := SeqOfBytes(data) byteArr := byteSeq.ToArray() @@ -162,20 +161,3 @@ func SequenceIsBackedByByteArray(seq Sequence) bool { _, ok := seq.(*ArraySequence)._values.(GoNativeArray).underlying.(*arrayForByte) return ok } - -func AssertSequenceIsBackedByByteArray(seq Sequence, t *testing.T) { - as, ok := seq.(*ArraySequence) - if !ok { - t.Errorf("Expected %v to be an *ArraySequence", seq) - } - - gna, ok := as._values.(GoNativeArray) - if !ok { - t.Errorf("Expected %v to implement the GoNativeArray interface", as._values) - } - - _, ok = gna.underlying.(*arrayForByte) - if !ok { - t.Errorf("Expected %v to be an arrayForByte", gna.underlying) - } -} diff --git a/Source/DafnyRuntime/DafnyRuntimeGo/dafny/dafny_test.go b/Source/DafnyRuntime/DafnyRuntimeGo/dafny/dafny_test.go index 93b079dd7e4..c5a4d2da4f6 100644 --- a/Source/DafnyRuntime/DafnyRuntimeGo/dafny/dafny_test.go +++ b/Source/DafnyRuntime/DafnyRuntimeGo/dafny/dafny_test.go @@ -41,27 +41,27 @@ func TestLazySequence(t *testing.T) { AssertImplementsSequence(lazySeq, t) } -// Test byte sequence optimization using ByteNativeArray wrapper +// Test byte sequence optimization using arrayForByte wrapper func TestByteSequenceOptimization(t *testing.T) { // Test creating byte sequence from slice data := []byte{1, 2, 3, 4, 5} - seq := SeqOf(data) + seq := SeqOfBytes(data) // Verify it implements Sequence interface AssertImplementsSequence(seq, t) - // Verify ToArray returns ByteNativeArray - // arr := seq.ToArray() - // if byteArr, ok := arr.(ByteNativeArray); ok { - // if byteArr.Length() != 5 { - // t.Errorf("Expected length 5, got %d", byteArr.Length()) - // } - // if byteArr.Select(0).(uint8) != 1 { - // t.Errorf("Expected first element 1, got %v", byteArr.Select(0)) - // } - // } else { - // t.Errorf("Expected ByteNativeArray, got %T", arr) - // } + // Verify ToArray returns GoNativeArray + arr := seq.ToArray() + if byteArr, ok := arr.(GoNativeArray); ok { + if byteArr.Length() != 5 { + t.Errorf("Expected length 5, got %d", byteArr.Length()) + } + if byteArr.Select(0).(uint8) != 1 { + t.Errorf("Expected first element 1, got %v", byteArr.Select(0)) + } + } else { + t.Errorf("Expected GoNativeArray, got %T", arr) + } } // Test optimization detection for uint8 vs non-uint8 @@ -69,15 +69,14 @@ func TestSeqOf(t *testing.T) { // Test uint8 slice - should optimize uint8Contents := []interface{}{uint8(1), uint8(2), uint8(3)} seq := SeqFromArray(uint8Contents, false) - AssertSequenceIsBackedByByteArray(seq, t) if !SequenceIsBackedByByteArray(seq) { t.Error("Expected optimization for uint8 slice") } - // Verify it returns ByteNativeArray + // Verify it returns GoNativeArray arr := seq.ToArray() if _, ok := arr.(GoNativeArray); !ok { - t.Errorf("Expected ByteNativeArray, got %T", arr) + t.Errorf("Expected GoNativeArray, got %T", arr) } // Test non-uint8 slice - should not optimize @@ -134,7 +133,7 @@ func TestNativeArrayFunctions(t *testing.T) { t.Errorf("Expected GoNativeArray, got %T", arr3) } - // Test Copy function with ByteNativeArray + // Test Copy function with GoNativeArray data := []byte{10, 20, 30} byteSeq := SeqOfBytes(data) byteArr := byteSeq.ToArray() @@ -162,20 +161,3 @@ func SequenceIsBackedByByteArray(seq Sequence) bool { _, ok := seq.(*ArraySequence)._values.(GoNativeArray).underlying.(*arrayForByte) return ok } - -func AssertSequenceIsBackedByByteArray(seq Sequence, t *testing.T) { - as, ok := seq.(*ArraySequence) - if !ok { - t.Errorf("Expected %v to be an *ArraySequence", seq) - } - - gna, ok := as._values.(GoNativeArray) - if !ok { - t.Errorf("Expected %v to implement the GoNativeArray interface", as._values) - } - - _, ok = gna.underlying.(*arrayForByte) - if !ok { - t.Errorf("Expected %v to be an arrayForByte", gna.underlying) - } -} From 7b97964f597647e7891bec7b3977d3f862a0490b Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Fri, 5 Sep 2025 10:48:33 -0700 Subject: [PATCH 10/11] Change SeqFromArray back to not copy, address TODOs --- .../DafnyRuntimeGo-gomod/dafny/dafny.go | 52 +++++++++++-------- .../DafnyRuntimeGo-gomod/dafny/dafny_test.go | 37 ++++++++++--- .../DafnyRuntimeGo/dafny/dafny.go | 52 +++++++++++-------- .../DafnyRuntimeGo/dafny/dafny_test.go | 37 ++++++++++--- 4 files changed, 120 insertions(+), 58 deletions(-) diff --git a/Source/DafnyRuntime/DafnyRuntimeGo-gomod/dafny/dafny.go b/Source/DafnyRuntime/DafnyRuntimeGo-gomod/dafny/dafny.go index 97b554d45a4..1e8ceb9d5e1 100644 --- a/Source/DafnyRuntime/DafnyRuntimeGo-gomod/dafny/dafny.go +++ b/Source/DafnyRuntime/DafnyRuntimeGo-gomod/dafny/dafny.go @@ -526,33 +526,29 @@ func SeqCreate(n uint32, init func(Int) interface{}) Sequence { }) } +// WARNING: This function uses the given array directly without making a defensive copy. +// This is only safe if the array never changes afterward. func SeqFromArray(contents []interface{}, isString bool) Sequence { - result := New_ArraySequence_() - underlying := newArrayWithValues(contents...) - result.Ctor__(GoNativeArray{underlying: underlying}, isString) - return result + return unsafeSeqWrappingDafnyArray(unsafeWrapArray(contents), false) } // SeqOf returns a sequence containing the given values. func SeqOf(values ...interface{}) Sequence { - result := New_ArraySequence_() - underlying := newArrayWithValues(values...) - result.Ctor__(GoNativeArray{underlying: underlying}, false) - return result + return unsafeSeqWrappingDafnyArray(newArrayWithValues(values...), false) } // SeqOfChars returns a sequence containing the given character values. func SeqOfChars(values ...Char) Sequence { - result := New_ArraySequence_() - underlying := NewArrayFromCharArray(values) - result.Ctor__(GoNativeArray{underlying: underlying}, false) - return result + return unsafeSeqWrappingDafnyArray(newArrayFromCharArray(values), true) } func SeqOfBytes(values []byte) Sequence { + return unsafeSeqWrappingDafnyArray(newArrayFromByteArray(values), false) +} + +func unsafeSeqWrappingDafnyArray(array Array, isString bool) Sequence { result := New_ArraySequence_() - underlying := NewArrayFromByteArray(values) - result.Ctor__(GoNativeArray{underlying: underlying}, false) + result.Ctor__(GoNativeArray{underlying: array}, isString) return result } @@ -859,7 +855,7 @@ func computeTotalArrayLength(dims ...Int) int { return totalLength } -func NewArrayFromCharArray(values []Char) Array { +func newArrayFromCharArray(values []Char) Array { contents := make([]Char, len(values)) copy(contents, values) return &arrayForChar{ @@ -868,7 +864,7 @@ func NewArrayFromCharArray(values []Char) Array { } } -func NewArrayFromByteArray(values []byte) Array { +func newArrayFromByteArray(values []byte) Array { contents := make([]byte, len(values)) copy(contents, values) return &arrayForByte{ @@ -877,6 +873,15 @@ func NewArrayFromByteArray(values []byte) Array { } } +// Uses the given array directly. +// Only safe if this array is not used anywhere else afterwards! +// Currently only used to support the existing publish SeqFromArray. +func unsafeWrapArray(values []interface{}) Array { + return &arrayStruct{ + contents: values, + dims: []int{len(values)}, + } +} // NewArrayFromExample returns a new Array. // If "init" is non-nil, it is used to initialize all elements of the array. @@ -1110,10 +1115,11 @@ func (_this arrayStruct) arraySetRange1(index int, other Array) { func (_this arrayStruct) arrayCopy() Array { newContents := make([]interface{}, len(_this.contents)) copy(newContents, _this.contents) + newDims := make([]int, len(_this.dims)) + copy(newDims, _this.dims) return &arrayStruct{ contents: newContents, - // TODO: Does dims have to be copied as well? - dims: _this.dims, + dims: newDims, } } @@ -1221,10 +1227,11 @@ func (_this arrayForByte) arraySetRange1(index int, other Array) { func (_this arrayForByte) arrayCopy() Array { newContents := make([]byte, len(_this.contents)) copy(newContents, _this.contents) + newDims := make([]int, len(_this.dims)) + copy(newDims, _this.dims) return &arrayForByte{ contents: newContents, - // TODO: Does dims have to be copied as well? - dims: _this.dims, + dims: newDims, } } @@ -1337,10 +1344,11 @@ func (_this arrayForChar) arraySetRange1(index int, other Array) { func (_this arrayForChar) arrayCopy() Array { newContents := make([]Char, len(_this.contents)) copy(newContents, _this.contents) + newDims := make([]int, len(_this.dims)) + copy(newDims, _this.dims) return &arrayForChar{ contents: newContents, - // TODO: Does dims have to be copied as well? - dims: _this.dims, + dims: newDims, } } diff --git a/Source/DafnyRuntime/DafnyRuntimeGo-gomod/dafny/dafny_test.go b/Source/DafnyRuntime/DafnyRuntimeGo-gomod/dafny/dafny_test.go index c5a4d2da4f6..8569886d890 100644 --- a/Source/DafnyRuntime/DafnyRuntimeGo-gomod/dafny/dafny_test.go +++ b/Source/DafnyRuntime/DafnyRuntimeGo-gomod/dafny/dafny_test.go @@ -2,10 +2,6 @@ package dafny import "testing" -// These tests are currently just useful sanity checks on the interface -// between the manually-written and Dafny-generated Go code, -// but could easily be expanded to include more unit tests in the future. - func TestArraySequence(t *testing.T) { arrSeq := MakeArraySequence() AssertImplementsSequence(arrSeq, t) @@ -68,7 +64,7 @@ func TestByteSequenceOptimization(t *testing.T) { func TestSeqOf(t *testing.T) { // Test uint8 slice - should optimize uint8Contents := []interface{}{uint8(1), uint8(2), uint8(3)} - seq := SeqFromArray(uint8Contents, false) + seq := SeqOf(uint8Contents...) if !SequenceIsBackedByByteArray(seq) { t.Error("Expected optimization for uint8 slice") } @@ -81,19 +77,36 @@ func TestSeqOf(t *testing.T) { // Test non-uint8 slice - should not optimize intContents := []interface{}{1, 2, 3} - seq2 := SeqFromArray(intContents, false) + seq2 := SeqOf(intContents...) if SequenceIsBackedByByteArray(seq2) { t.Error("Expected no optimization for int slice") } // Test empty slice - should not optimize emptyContents := []interface{}{} - seq3 := SeqFromArray(emptyContents, false) + seq3 := SeqOf(emptyContents...) if SequenceIsBackedByByteArray(seq3) { t.Error("Expected no optimization for empty slice") } } +func TestSeqFromArray(t *testing.T) { + // Test uint8 slice - should not optimize + // (in fact it should use the array without copying) + uint8Contents := []interface{}{uint8(1), uint8(2), uint8(3)} + seq := SeqFromArray(uint8Contents, false) + if SequenceIsBackedByByteArray(seq) { + t.Error("Expected no optimization for int slice") + } + + // Mutate the array (exactly as you're not supposed to :) + // and check the sequence changes. + uint8Contents[1] = uint8(42) + if seq.Select(1) != uint8(42) { + t.Errorf("Expected element at index 1 to be 42, got %v", seq.Select(1)) + } +} + // Test refactored CompanionStruct_NativeArray_ functions func TestNativeArrayFunctions(t *testing.T) { // Test Make function @@ -150,6 +163,14 @@ func TestNativeArrayFunctions(t *testing.T) { } } +func TestArrayCopy(t *testing.T) { + arr := NewArray(Five) + copy := arr.arrayCopy() + if arr.(EqualsGeneric).EqualsGeneric(copy) { + t.Errorf("Expected array to not compare EqualsGeneric to its copy") + } +} + func AssertImplementsSequence(s interface{}, t *testing.T) { _, ok := s.(Sequence) if !ok { @@ -161,3 +182,5 @@ func SequenceIsBackedByByteArray(seq Sequence) bool { _, ok := seq.(*ArraySequence)._values.(GoNativeArray).underlying.(*arrayForByte) return ok } + + diff --git a/Source/DafnyRuntime/DafnyRuntimeGo/dafny/dafny.go b/Source/DafnyRuntime/DafnyRuntimeGo/dafny/dafny.go index 97b554d45a4..1e8ceb9d5e1 100644 --- a/Source/DafnyRuntime/DafnyRuntimeGo/dafny/dafny.go +++ b/Source/DafnyRuntime/DafnyRuntimeGo/dafny/dafny.go @@ -526,33 +526,29 @@ func SeqCreate(n uint32, init func(Int) interface{}) Sequence { }) } +// WARNING: This function uses the given array directly without making a defensive copy. +// This is only safe if the array never changes afterward. func SeqFromArray(contents []interface{}, isString bool) Sequence { - result := New_ArraySequence_() - underlying := newArrayWithValues(contents...) - result.Ctor__(GoNativeArray{underlying: underlying}, isString) - return result + return unsafeSeqWrappingDafnyArray(unsafeWrapArray(contents), false) } // SeqOf returns a sequence containing the given values. func SeqOf(values ...interface{}) Sequence { - result := New_ArraySequence_() - underlying := newArrayWithValues(values...) - result.Ctor__(GoNativeArray{underlying: underlying}, false) - return result + return unsafeSeqWrappingDafnyArray(newArrayWithValues(values...), false) } // SeqOfChars returns a sequence containing the given character values. func SeqOfChars(values ...Char) Sequence { - result := New_ArraySequence_() - underlying := NewArrayFromCharArray(values) - result.Ctor__(GoNativeArray{underlying: underlying}, false) - return result + return unsafeSeqWrappingDafnyArray(newArrayFromCharArray(values), true) } func SeqOfBytes(values []byte) Sequence { + return unsafeSeqWrappingDafnyArray(newArrayFromByteArray(values), false) +} + +func unsafeSeqWrappingDafnyArray(array Array, isString bool) Sequence { result := New_ArraySequence_() - underlying := NewArrayFromByteArray(values) - result.Ctor__(GoNativeArray{underlying: underlying}, false) + result.Ctor__(GoNativeArray{underlying: array}, isString) return result } @@ -859,7 +855,7 @@ func computeTotalArrayLength(dims ...Int) int { return totalLength } -func NewArrayFromCharArray(values []Char) Array { +func newArrayFromCharArray(values []Char) Array { contents := make([]Char, len(values)) copy(contents, values) return &arrayForChar{ @@ -868,7 +864,7 @@ func NewArrayFromCharArray(values []Char) Array { } } -func NewArrayFromByteArray(values []byte) Array { +func newArrayFromByteArray(values []byte) Array { contents := make([]byte, len(values)) copy(contents, values) return &arrayForByte{ @@ -877,6 +873,15 @@ func NewArrayFromByteArray(values []byte) Array { } } +// Uses the given array directly. +// Only safe if this array is not used anywhere else afterwards! +// Currently only used to support the existing publish SeqFromArray. +func unsafeWrapArray(values []interface{}) Array { + return &arrayStruct{ + contents: values, + dims: []int{len(values)}, + } +} // NewArrayFromExample returns a new Array. // If "init" is non-nil, it is used to initialize all elements of the array. @@ -1110,10 +1115,11 @@ func (_this arrayStruct) arraySetRange1(index int, other Array) { func (_this arrayStruct) arrayCopy() Array { newContents := make([]interface{}, len(_this.contents)) copy(newContents, _this.contents) + newDims := make([]int, len(_this.dims)) + copy(newDims, _this.dims) return &arrayStruct{ contents: newContents, - // TODO: Does dims have to be copied as well? - dims: _this.dims, + dims: newDims, } } @@ -1221,10 +1227,11 @@ func (_this arrayForByte) arraySetRange1(index int, other Array) { func (_this arrayForByte) arrayCopy() Array { newContents := make([]byte, len(_this.contents)) copy(newContents, _this.contents) + newDims := make([]int, len(_this.dims)) + copy(newDims, _this.dims) return &arrayForByte{ contents: newContents, - // TODO: Does dims have to be copied as well? - dims: _this.dims, + dims: newDims, } } @@ -1337,10 +1344,11 @@ func (_this arrayForChar) arraySetRange1(index int, other Array) { func (_this arrayForChar) arrayCopy() Array { newContents := make([]Char, len(_this.contents)) copy(newContents, _this.contents) + newDims := make([]int, len(_this.dims)) + copy(newDims, _this.dims) return &arrayForChar{ contents: newContents, - // TODO: Does dims have to be copied as well? - dims: _this.dims, + dims: newDims, } } diff --git a/Source/DafnyRuntime/DafnyRuntimeGo/dafny/dafny_test.go b/Source/DafnyRuntime/DafnyRuntimeGo/dafny/dafny_test.go index c5a4d2da4f6..8569886d890 100644 --- a/Source/DafnyRuntime/DafnyRuntimeGo/dafny/dafny_test.go +++ b/Source/DafnyRuntime/DafnyRuntimeGo/dafny/dafny_test.go @@ -2,10 +2,6 @@ package dafny import "testing" -// These tests are currently just useful sanity checks on the interface -// between the manually-written and Dafny-generated Go code, -// but could easily be expanded to include more unit tests in the future. - func TestArraySequence(t *testing.T) { arrSeq := MakeArraySequence() AssertImplementsSequence(arrSeq, t) @@ -68,7 +64,7 @@ func TestByteSequenceOptimization(t *testing.T) { func TestSeqOf(t *testing.T) { // Test uint8 slice - should optimize uint8Contents := []interface{}{uint8(1), uint8(2), uint8(3)} - seq := SeqFromArray(uint8Contents, false) + seq := SeqOf(uint8Contents...) if !SequenceIsBackedByByteArray(seq) { t.Error("Expected optimization for uint8 slice") } @@ -81,19 +77,36 @@ func TestSeqOf(t *testing.T) { // Test non-uint8 slice - should not optimize intContents := []interface{}{1, 2, 3} - seq2 := SeqFromArray(intContents, false) + seq2 := SeqOf(intContents...) if SequenceIsBackedByByteArray(seq2) { t.Error("Expected no optimization for int slice") } // Test empty slice - should not optimize emptyContents := []interface{}{} - seq3 := SeqFromArray(emptyContents, false) + seq3 := SeqOf(emptyContents...) if SequenceIsBackedByByteArray(seq3) { t.Error("Expected no optimization for empty slice") } } +func TestSeqFromArray(t *testing.T) { + // Test uint8 slice - should not optimize + // (in fact it should use the array without copying) + uint8Contents := []interface{}{uint8(1), uint8(2), uint8(3)} + seq := SeqFromArray(uint8Contents, false) + if SequenceIsBackedByByteArray(seq) { + t.Error("Expected no optimization for int slice") + } + + // Mutate the array (exactly as you're not supposed to :) + // and check the sequence changes. + uint8Contents[1] = uint8(42) + if seq.Select(1) != uint8(42) { + t.Errorf("Expected element at index 1 to be 42, got %v", seq.Select(1)) + } +} + // Test refactored CompanionStruct_NativeArray_ functions func TestNativeArrayFunctions(t *testing.T) { // Test Make function @@ -150,6 +163,14 @@ func TestNativeArrayFunctions(t *testing.T) { } } +func TestArrayCopy(t *testing.T) { + arr := NewArray(Five) + copy := arr.arrayCopy() + if arr.(EqualsGeneric).EqualsGeneric(copy) { + t.Errorf("Expected array to not compare EqualsGeneric to its copy") + } +} + func AssertImplementsSequence(s interface{}, t *testing.T) { _, ok := s.(Sequence) if !ok { @@ -161,3 +182,5 @@ func SequenceIsBackedByByteArray(seq Sequence) bool { _, ok := seq.(*ArraySequence)._values.(GoNativeArray).underlying.(*arrayForByte) return ok } + + From d5e7ee212284e885afffffb0df918a75f6a653c7 Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Fri, 5 Sep 2025 12:02:53 -0700 Subject: [PATCH 11/11] Typo --- Source/DafnyRuntime/DafnyRuntimeGo-gomod/dafny/dafny.go | 2 +- Source/DafnyRuntime/DafnyRuntimeGo/dafny/dafny.go | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/Source/DafnyRuntime/DafnyRuntimeGo-gomod/dafny/dafny.go b/Source/DafnyRuntime/DafnyRuntimeGo-gomod/dafny/dafny.go index 1e8ceb9d5e1..465992abc4d 100644 --- a/Source/DafnyRuntime/DafnyRuntimeGo-gomod/dafny/dafny.go +++ b/Source/DafnyRuntime/DafnyRuntimeGo-gomod/dafny/dafny.go @@ -529,7 +529,7 @@ func SeqCreate(n uint32, init func(Int) interface{}) Sequence { // WARNING: This function uses the given array directly without making a defensive copy. // This is only safe if the array never changes afterward. func SeqFromArray(contents []interface{}, isString bool) Sequence { - return unsafeSeqWrappingDafnyArray(unsafeWrapArray(contents), false) + return unsafeSeqWrappingDafnyArray(unsafeWrapArray(contents), isString) } // SeqOf returns a sequence containing the given values. diff --git a/Source/DafnyRuntime/DafnyRuntimeGo/dafny/dafny.go b/Source/DafnyRuntime/DafnyRuntimeGo/dafny/dafny.go index 1e8ceb9d5e1..465992abc4d 100644 --- a/Source/DafnyRuntime/DafnyRuntimeGo/dafny/dafny.go +++ b/Source/DafnyRuntime/DafnyRuntimeGo/dafny/dafny.go @@ -529,7 +529,7 @@ func SeqCreate(n uint32, init func(Int) interface{}) Sequence { // WARNING: This function uses the given array directly without making a defensive copy. // This is only safe if the array never changes afterward. func SeqFromArray(contents []interface{}, isString bool) Sequence { - return unsafeSeqWrappingDafnyArray(unsafeWrapArray(contents), false) + return unsafeSeqWrappingDafnyArray(unsafeWrapArray(contents), isString) } // SeqOf returns a sequence containing the given values.