diff --git a/Source/DafnyRuntime/DafnyRuntimeGo-gomod/dafny/dafny.go b/Source/DafnyRuntime/DafnyRuntimeGo-gomod/dafny/dafny.go index aca8225ea75..465992abc4d 100644 --- a/Source/DafnyRuntime/DafnyRuntimeGo-gomod/dafny/dafny.go +++ b/Source/DafnyRuntime/DafnyRuntimeGo-gomod/dafny/dafny.go @@ -82,18 +82,8 @@ 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 - } - } - } - return true + leftArr, rightArr := left.ToArray(), right.ToArray() + return leftArr.(GoNativeArray).underlying.arrayEqualUpTo(rightArr.(GoNativeArray).underlying, int(index)) } func IsDafnyNull(x interface{}) bool { @@ -536,39 +526,30 @@ 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 { - arr := GoNativeArray{ - contents: contents, - } - result := New_ArraySequence_() - result.Ctor__(arr, isString) - return result + return unsafeSeqWrappingDafnyArray(unsafeWrapArray(contents), isString) } // 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. - arr := make([]interface{}, len(values)) - copy(arr, values) - return SeqFromArray(arr, false) + return unsafeSeqWrappingDafnyArray(newArrayWithValues(values...), false) } // 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) + return unsafeSeqWrappingDafnyArray(newArrayFromCharArray(values), true) } func SeqOfBytes(values []byte) Sequence { - arr := make([]interface{}, len(values)) - for i, v := range values { - arr[i] = v - } - return SeqFromArray(arr, false) + return unsafeSeqWrappingDafnyArray(newArrayFromByteArray(values), false) +} + +func unsafeSeqWrappingDafnyArray(array Array, isString bool) Sequence { + result := New_ArraySequence_() + result.Ctor__(GoNativeArray{underlying: array}, isString) + return result } // SeqOfString converts the given string into a sequence of characters. @@ -734,80 +715,75 @@ 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) + arr := x.ToArray() + + 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 arr + return result } /****************************************************************************** * Arrays ******************************************************************************/ -// A GoNativeArray is a single dimensional Go slice, +// A GoNativeArray is a single dimensional Array, // 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. +// GoNativeArray wraps the Array interface for external compatibility +// while allowing optimized implementations internally. type GoNativeArray struct { - contents []interface{} + underlying Array } func (CompanionStruct_NativeArray_) Make(length uint32) NativeArray { - contents := make([]interface{}, length) - return GoNativeArray{ - contents: contents, + 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 { - contents := make([]interface{}, length) - for i := uint32(0); i < length; i++ { - contents[i] = init(i) - } - return GoNativeArray{ - contents: contents, - } + underlying := newArrayWithInitFn(init, int(length)) + return GoNativeArray{underlying: underlying} } func (CompanionStruct_NativeArray_) Copy(other ImmutableArray) NativeArray { - otherArray := other.(GoNativeArray) - contents := make([]interface{}, otherArray.Length()) - copy(contents, otherArray.contents) - return GoNativeArray{ - contents: contents, - } + return GoNativeArray{underlying: other.(GoNativeArray).underlying.arrayCopy()} } -func (array GoNativeArray) Length() uint32 { - return uint32(len(array.contents)) +func (g GoNativeArray) Length() uint32 { + return uint32(g.underlying.dimensionLength(0)) } -func (array GoNativeArray) Select(i uint32) interface{} { - return array.contents[i] +func (g GoNativeArray) Select(i uint32) interface{} { + return g.underlying.ArrayGet1(int(i)) } -func (array GoNativeArray) Update(i uint32, t interface{}) { - array.contents[i] = t +func (g GoNativeArray) Update(i uint32, t interface{}) { + g.underlying.ArraySet1(t, int(i)) } -func (array GoNativeArray) UpdateSubarray(i uint32, other ImmutableArray) { - otherArray := other.(GoNativeArray) - copy(array.contents[i:(i+otherArray.Length())], otherArray.contents) +func (g GoNativeArray) UpdateSubarray(i uint32, other ImmutableArray) { + g.underlying.arraySetRange1(int(i), other.(GoNativeArray).underlying) } -func (array GoNativeArray) Freeze(size uint32) ImmutableArray { - return array.Subarray(0, size) +func (g GoNativeArray) Freeze(size uint32) ImmutableArray { + return g.Subarray(0, size) } -func (array GoNativeArray) Subarray(lo uint32, hi uint32) ImmutableArray { - return GoNativeArray{ - contents: array.contents[lo:hi], - } +func (g GoNativeArray) Subarray(lo, hi uint32) ImmutableArray { + return GoNativeArray{underlying: g.underlying.arrayGetRange1(IntOfUint32(lo), IntOfUint32(hi))} } -func (array GoNativeArray) String() string { +func (g GoNativeArray) String() string { return "dafny.GoNativeArray" } @@ -825,7 +801,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) @@ -835,6 +815,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". @@ -854,6 +855,34 @@ 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)}, + } +} + +// 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. // "example" is used only to figure out the right kind of Array to return. @@ -978,6 +1007,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 := 1; i < length; i++ { + 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 := 1; i < length; i++ { + 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 := 1; i < length; i++ { + 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...) @@ -1011,6 +1087,48 @@ func (_this arrayStruct) ArraySet1(value interface{}, index int) { _this.contents[index] = value } +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(iHi - iLo)}, + } +} + +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) + newDims := make([]int, len(_this.dims)) + copy(newDims, _this.dims) + return &arrayStruct{ + contents: newContents, + dims: newDims, + } +} + +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{}") } @@ -1081,6 +1199,51 @@ func (_this arrayForByte) ArraySet1(value interface{}, index int) { _this.contents[index] = value.(byte) } +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(iHi - iLo)}, + } +} + +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) + newDims := make([]int, len(_this.dims)) + copy(newDims, _this.dims) + return &arrayForByte{ + contents: newContents, + dims: newDims, + } +} + +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 { + return defaultArrayEqualUpTo(_this, other, uint32(index)) + } +} + func (_this arrayForByte) ArrayGet1Byte(index int) byte { return _this.contents[index] } @@ -1153,6 +1316,51 @@ func (_this arrayForChar) ArraySet1(value interface{}, index int) { _this.contents[index] = value.(Char) } +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(iHi - iLo)}, + } +} + +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) + newDims := make([]int, len(_this.dims)) + copy(newDims, _this.dims) + return &arrayForChar{ + contents: newContents, + dims: newDims, + } +} + +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 { + 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{}") } @@ -1225,6 +1433,50 @@ func (_this arrayForCodePoint) ArraySet1(value interface{}, index int) { _this.contents[index] = value.(CodePoint) } +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(iHi - iLo)}, + } +} + +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 { + 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{}") } @@ -1329,8 +1581,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 d2d73049353..8569886d890 100644 --- a/Source/DafnyRuntime/DafnyRuntimeGo-gomod/dafny/dafny_test.go +++ b/Source/DafnyRuntime/DafnyRuntimeGo-gomod/dafny/dafny_test.go @@ -2,17 +2,17 @@ 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) } 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,9 +37,150 @@ func TestLazySequence(t *testing.T) { AssertImplementsSequence(lazySeq, t) } +// 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 := SeqOfBytes(data) + + // Verify it implements Sequence interface + AssertImplementsSequence(seq, t) + + // 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 +func TestSeqOf(t *testing.T) { + // Test uint8 slice - should optimize + uint8Contents := []interface{}{uint8(1), uint8(2), uint8(3)} + seq := SeqOf(uint8Contents...) + if !SequenceIsBackedByByteArray(seq) { + t.Error("Expected optimization for uint8 slice") + } + + // Verify it returns GoNativeArray + arr := seq.ToArray() + if _, ok := arr.(GoNativeArray); !ok { + t.Errorf("Expected GoNativeArray, got %T", arr) + } + + // Test non-uint8 slice - should not optimize + intContents := []interface{}{1, 2, 3} + seq2 := SeqOf(intContents...) + if SequenceIsBackedByByteArray(seq2) { + t.Error("Expected no optimization for int slice") + } + + // Test empty slice - should not optimize + emptyContents := []interface{}{} + 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 + 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.(GoNativeArray)) + 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 GoNativeArray + data := []byte{10, 20, 30} + byteSeq := SeqOfBytes(data) + byteArr := byteSeq.ToArray() + arr4 := Companion_NativeArray_.Copy(byteArr) + if byteArr4, ok := arr4.(GoNativeArray); 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 GoNativeArray, got %T", arr4) + } +} + +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 { t.Errorf("Expected %v to implement the Sequence interface", s) } } + +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 aca8225ea75..465992abc4d 100644 --- a/Source/DafnyRuntime/DafnyRuntimeGo/dafny/dafny.go +++ b/Source/DafnyRuntime/DafnyRuntimeGo/dafny/dafny.go @@ -82,18 +82,8 @@ 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 - } - } - } - return true + leftArr, rightArr := left.ToArray(), right.ToArray() + return leftArr.(GoNativeArray).underlying.arrayEqualUpTo(rightArr.(GoNativeArray).underlying, int(index)) } func IsDafnyNull(x interface{}) bool { @@ -536,39 +526,30 @@ 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 { - arr := GoNativeArray{ - contents: contents, - } - result := New_ArraySequence_() - result.Ctor__(arr, isString) - return result + return unsafeSeqWrappingDafnyArray(unsafeWrapArray(contents), isString) } // 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. - arr := make([]interface{}, len(values)) - copy(arr, values) - return SeqFromArray(arr, false) + return unsafeSeqWrappingDafnyArray(newArrayWithValues(values...), false) } // 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) + return unsafeSeqWrappingDafnyArray(newArrayFromCharArray(values), true) } func SeqOfBytes(values []byte) Sequence { - arr := make([]interface{}, len(values)) - for i, v := range values { - arr[i] = v - } - return SeqFromArray(arr, false) + return unsafeSeqWrappingDafnyArray(newArrayFromByteArray(values), false) +} + +func unsafeSeqWrappingDafnyArray(array Array, isString bool) Sequence { + result := New_ArraySequence_() + result.Ctor__(GoNativeArray{underlying: array}, isString) + return result } // SeqOfString converts the given string into a sequence of characters. @@ -734,80 +715,75 @@ 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) + arr := x.ToArray() + + 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 arr + return result } /****************************************************************************** * Arrays ******************************************************************************/ -// A GoNativeArray is a single dimensional Go slice, +// A GoNativeArray is a single dimensional Array, // 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. +// GoNativeArray wraps the Array interface for external compatibility +// while allowing optimized implementations internally. type GoNativeArray struct { - contents []interface{} + underlying Array } func (CompanionStruct_NativeArray_) Make(length uint32) NativeArray { - contents := make([]interface{}, length) - return GoNativeArray{ - contents: contents, + 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 { - contents := make([]interface{}, length) - for i := uint32(0); i < length; i++ { - contents[i] = init(i) - } - return GoNativeArray{ - contents: contents, - } + underlying := newArrayWithInitFn(init, int(length)) + return GoNativeArray{underlying: underlying} } func (CompanionStruct_NativeArray_) Copy(other ImmutableArray) NativeArray { - otherArray := other.(GoNativeArray) - contents := make([]interface{}, otherArray.Length()) - copy(contents, otherArray.contents) - return GoNativeArray{ - contents: contents, - } + return GoNativeArray{underlying: other.(GoNativeArray).underlying.arrayCopy()} } -func (array GoNativeArray) Length() uint32 { - return uint32(len(array.contents)) +func (g GoNativeArray) Length() uint32 { + return uint32(g.underlying.dimensionLength(0)) } -func (array GoNativeArray) Select(i uint32) interface{} { - return array.contents[i] +func (g GoNativeArray) Select(i uint32) interface{} { + return g.underlying.ArrayGet1(int(i)) } -func (array GoNativeArray) Update(i uint32, t interface{}) { - array.contents[i] = t +func (g GoNativeArray) Update(i uint32, t interface{}) { + g.underlying.ArraySet1(t, int(i)) } -func (array GoNativeArray) UpdateSubarray(i uint32, other ImmutableArray) { - otherArray := other.(GoNativeArray) - copy(array.contents[i:(i+otherArray.Length())], otherArray.contents) +func (g GoNativeArray) UpdateSubarray(i uint32, other ImmutableArray) { + g.underlying.arraySetRange1(int(i), other.(GoNativeArray).underlying) } -func (array GoNativeArray) Freeze(size uint32) ImmutableArray { - return array.Subarray(0, size) +func (g GoNativeArray) Freeze(size uint32) ImmutableArray { + return g.Subarray(0, size) } -func (array GoNativeArray) Subarray(lo uint32, hi uint32) ImmutableArray { - return GoNativeArray{ - contents: array.contents[lo:hi], - } +func (g GoNativeArray) Subarray(lo, hi uint32) ImmutableArray { + return GoNativeArray{underlying: g.underlying.arrayGetRange1(IntOfUint32(lo), IntOfUint32(hi))} } -func (array GoNativeArray) String() string { +func (g GoNativeArray) String() string { return "dafny.GoNativeArray" } @@ -825,7 +801,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) @@ -835,6 +815,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". @@ -854,6 +855,34 @@ 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)}, + } +} + +// 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. // "example" is used only to figure out the right kind of Array to return. @@ -978,6 +1007,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 := 1; i < length; i++ { + 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 := 1; i < length; i++ { + 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 := 1; i < length; i++ { + 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...) @@ -1011,6 +1087,48 @@ func (_this arrayStruct) ArraySet1(value interface{}, index int) { _this.contents[index] = value } +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(iHi - iLo)}, + } +} + +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) + newDims := make([]int, len(_this.dims)) + copy(newDims, _this.dims) + return &arrayStruct{ + contents: newContents, + dims: newDims, + } +} + +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{}") } @@ -1081,6 +1199,51 @@ func (_this arrayForByte) ArraySet1(value interface{}, index int) { _this.contents[index] = value.(byte) } +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(iHi - iLo)}, + } +} + +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) + newDims := make([]int, len(_this.dims)) + copy(newDims, _this.dims) + return &arrayForByte{ + contents: newContents, + dims: newDims, + } +} + +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 { + return defaultArrayEqualUpTo(_this, other, uint32(index)) + } +} + func (_this arrayForByte) ArrayGet1Byte(index int) byte { return _this.contents[index] } @@ -1153,6 +1316,51 @@ func (_this arrayForChar) ArraySet1(value interface{}, index int) { _this.contents[index] = value.(Char) } +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(iHi - iLo)}, + } +} + +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) + newDims := make([]int, len(_this.dims)) + copy(newDims, _this.dims) + return &arrayForChar{ + contents: newContents, + dims: newDims, + } +} + +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 { + 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{}") } @@ -1225,6 +1433,50 @@ func (_this arrayForCodePoint) ArraySet1(value interface{}, index int) { _this.contents[index] = value.(CodePoint) } +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(iHi - iLo)}, + } +} + +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 { + 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{}") } @@ -1329,8 +1581,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 5b5e779bcda..8569886d890 100644 --- a/Source/DafnyRuntime/DafnyRuntimeGo/dafny/dafny_test.go +++ b/Source/DafnyRuntime/DafnyRuntimeGo/dafny/dafny_test.go @@ -2,44 +2,185 @@ 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) +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 arrayForByte wrapper +func TestByteSequenceOptimization(t *testing.T) { + // Test creating byte sequence from slice + data := []byte{1, 2, 3, 4, 5} + seq := SeqOfBytes(data) + + // Verify it implements Sequence interface + AssertImplementsSequence(seq, t) + + // 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 +func TestSeqOf(t *testing.T) { + // Test uint8 slice - should optimize + uint8Contents := []interface{}{uint8(1), uint8(2), uint8(3)} + seq := SeqOf(uint8Contents...) + if !SequenceIsBackedByByteArray(seq) { + t.Error("Expected optimization for uint8 slice") + } + + // Verify it returns GoNativeArray + arr := seq.ToArray() + if _, ok := arr.(GoNativeArray); !ok { + t.Errorf("Expected GoNativeArray, got %T", arr) + } + + // Test non-uint8 slice - should not optimize + intContents := []interface{}{1, 2, 3} + seq2 := SeqOf(intContents...) + if SequenceIsBackedByByteArray(seq2) { + t.Error("Expected no optimization for int slice") + } + + // Test empty slice - should not optimize + emptyContents := []interface{}{} + 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 + 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.(GoNativeArray)) + 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 GoNativeArray + data := []byte{10, 20, 30} + byteSeq := SeqOfBytes(data) + byteArr := byteSeq.ToArray() + arr4 := Companion_NativeArray_.Copy(byteArr) + if byteArr4, ok := arr4.(GoNativeArray); 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 GoNativeArray, got %T", arr4) + } +} + +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) { - 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) + } +} + +func SequenceIsBackedByByteArray(seq Sequence) bool { + _, ok := seq.(*ArraySequence)._values.(GoNativeArray).underlying.(*arrayForByte) + return ok +} + +