Add additional array tests

This adds a number of additional tests for arrays, and fixes a few bugs
uncovered by them.

pkg/corset/resolver.go

@@ -558,14 +558,18 @@ func (r *resolver) finaliseArrayAccessInModule(scope LocalScope, expr *ArrayAcce
 	//
 	if !expr.IsResolved() && !scope.Bind(expr) {
 		return nil, r.srcmap.SyntaxErrors(expr, "unknown array column")
-	} else if binding, ok := expr.Binding().(*ColumnBinding); ok {
-		// Found column, now check it is an array.
-		if arr_t, ok := binding.dataType.(*ArrayType); ok {
-			return arr_t.element, nil
-		}
+	} else if binding, ok := expr.Binding().(*ColumnBinding); !ok {
+		return nil, r.srcmap.SyntaxErrors(expr, "unknown array column")
+	} else if arr_t, ok := binding.dataType.(*ArrayType); !ok {
+		return nil, r.srcmap.SyntaxErrors(expr, "expected array column")
+	} else if c := expr.arg.AsConstant(); c == nil {
+		return nil, r.srcmap.SyntaxErrors(expr, "expected constant array index")
+	} else if i := uint(c.Uint64()); i == 0 || i > arr_t.Width() {
+		return nil, r.srcmap.SyntaxErrors(expr, "array access out-of-bounds")
+	} else {
+		// All good
+		return arr_t.element, nil
 	}
-	// Default
-	return nil, r.srcmap.SyntaxErrors(expr, "not an array column")
 }
 
 // Resolve an if condition contained within some expression which, in turn, is

pkg/corset/translator.go

@@ -446,6 +446,9 @@ func (t *translator) translateArrayAccessInModule(expr *ArrayAccess, shift int)
 	// Did we find it?
 	if !ok {
 		errors = append(errors, *t.srcmap.SyntaxError(expr.arg, "invalid array index encountered during translation"))
+	}
+	// Error check
+	if len(errors) > 0 {
 		return nil, errors
 	}
 	// Lookup underlying column info

pkg/test/invalid_corset_test.go

@@ -494,6 +494,29 @@ func Test_Invalid_For_03(t *testing.T) {
 	CheckInvalid(t, "for_invalid_03")
 }
 
+// ===================================================================
+// Arrays
+// ===================================================================
+func Test_Invalid_Array_01(t *testing.T) {
+	CheckInvalid(t, "array_invalid_01")
+}
+
+func Test_Invalid_Array_02(t *testing.T) {
+	CheckInvalid(t, "array_invalid_02")
+}
+
+func Test_Invalid_Array_03(t *testing.T) {
+	CheckInvalid(t, "array_invalid_03")
+}
+
+func Test_Invalid_Array_04(t *testing.T) {
+	CheckInvalid(t, "array_invalid_04")
+}
+
+func Test_Invalid_Array_05(t *testing.T) {
+	CheckInvalid(t, "array_invalid_05")
+}
+
 // ===================================================================
 // Test Helpers
 // ===================================================================

pkg/test/valid_corset_test.go

@@ -648,6 +648,15 @@ func Test_Array_01(t *testing.T) {
 	Check(t, false, "array_01")
 }
 
+/* func Test_Array_02(t *testing.T) {
+	Check(t, false, "array_02")
+}
+*/
+
+func Test_Array_03(t *testing.T) {
+	Check(t, false, "array_03")
+}
+
 // ===================================================================
 // Complex Tests
 // ===================================================================

testdata/array_02.accepts

@@ -0,0 +1,18 @@
+{ "ARG": [], "BIT_4": [], "BIT_3": [], "BIT_2": [], "BIT_1": [] }
+;;
+{ "ARG": [0], "BIT_4": [0], "BIT_3": [0], "BIT_2": [0], "BIT_1": [0] }
+{ "ARG": [1], "BIT_4": [0], "BIT_3": [0], "BIT_2": [0], "BIT_1": [1] }
+{ "ARG": [2], "BIT_4": [0], "BIT_3": [0], "BIT_2": [1], "BIT_1": [0] }
+{ "ARG": [3], "BIT_4": [0], "BIT_3": [0], "BIT_2": [1], "BIT_1": [1] }
+{ "ARG": [4], "BIT_4": [0], "BIT_3": [1], "BIT_2": [0], "BIT_1": [0] }
+{ "ARG": [5], "BIT_4": [0], "BIT_3": [1], "BIT_2": [0], "BIT_1": [1] }
+{ "ARG": [6], "BIT_4": [0], "BIT_3": [1], "BIT_2": [1], "BIT_1": [0] }
+{ "ARG": [7], "BIT_4": [0], "BIT_3": [1], "BIT_2": [1], "BIT_1": [1] }
+{ "ARG": [8], "BIT_4": [1], "BIT_3": [0], "BIT_2": [0], "BIT_1": [0] }
+{ "ARG": [9], "BIT_4": [1], "BIT_3": [0], "BIT_2": [0], "BIT_1": [1] }
+{ "ARG": [10], "BIT_4": [1], "BIT_3": [0], "BIT_2": [1], "BIT_1": [0] }
+{ "ARG": [11], "BIT_4": [1], "BIT_3": [0], "BIT_2": [1], "BIT_1": [1] }
+{ "ARG": [12], "BIT_4": [1], "BIT_3": [1], "BIT_2": [0], "BIT_1": [0] }
+{ "ARG": [13], "BIT_4": [1], "BIT_3": [1], "BIT_2": [0], "BIT_1": [1] }
+{ "ARG": [14], "BIT_4": [1], "BIT_3": [1], "BIT_2": [1], "BIT_1": [0] }
+{ "ARG": [15], "BIT_4": [1], "BIT_3": [1], "BIT_2": [1], "BIT_1": [1] }

testdata/array_02.lisp

@@ -0,0 +1,8 @@
+(defcolumns
+    (BIT :binary@prove :array [4])
+    (ARG :i16@loob))
+
+(defconstraint bits ()
+  (- ARG
+     (reduce +
+      (for i [0:3] (* (^ 2 i) [BIT (+ 1 i)])))))

testdata/array_03.accepts

@@ -0,0 +1,7 @@
+{"ARR_1": [], "ARR_2": []}
+{"ARR_1": [-1], "ARR_2": [1]}
+{"ARR_1": [0], "ARR_2": [0]}
+{"ARR_1": [1], "ARR_2": [-1]}
+{"ARR_1": [0,-1], "ARR_2": [0,1]}
+{"ARR_1": [0,0], "ARR_2": [0,0]}
+{"ARR_1": [0,1], "ARR_2": [0,-1]}

testdata/array_03.lisp

@@ -0,0 +1,3 @@
+(defcolumns (ARR :@loob :array [2]))
+(defconstraint c1 () (+ [ARR 1] [ARR 2]))
+(defconstraint c2 () (+ [ARR 2] [ARR 2]))

testdata/array_03.rejects

@@ -0,0 +1,6 @@
+{"ARR_1": [1], "ARR_2": [0]}
+{"ARR_1": [-1], "ARR_2": [0]}
+{"ARR_1": [0], "ARR_2": [1]}
+{"ARR_1": [0], "ARR_2": [-1]}
+{"ARR_1": [2], "ARR_2": [-1]}
+{"ARR_1": [-2], "ARR_2": [1]}

testdata/array_invalid_01.lisp

@@ -0,0 +1,4 @@
+;;error:4:24-30:not an array column
+(defcolumns (BIT :@loob))
+
+(defconstraint bits () [BIT 1])

testdata/array_invalid_02.lisp

@@ -0,0 +1,4 @@
+;;error:4:24-25:expected loobean constraint (found (𝔽@loob)[4])
+(defcolumns (BIT :@loob :array [4]))
+
+(defconstraint bits () BIT)

testdata/array_invalid_03.lisp

@@ -0,0 +1,4 @@
+;;error:4:24-30:expected constant array index
+(defcolumns X (BIT :@loob :array [4]))
+
+(defconstraint bits () [BIT X])

testdata/array_invalid_04.lisp

@@ -0,0 +1,12 @@
+;;error:12:12-18:out-of-bounds array access
+(defcolumns
+    (BIT :binary@prove :array [3])
+    (ARG :i16@loob))
+
+(defconstraint bits ()
+  (- ARG
+     (+
+      (* 1 [BIT 1])
+      (* 2 [BIT 2])
+      (* 4 [BIT 3])
+      (* 8 [BIT 4]))))

testdata/array_invalid_05.lisp

@@ -0,0 +1,12 @@
+;;error:12:12-18:out-of-bounds array access
+(defcolumns
+    (BIT :binary@prove :array [4])
+    (ARG :i16@loob))
+
+(defconstraint bits ()
+  (- ARG
+     (+
+      (* 1 [BIT 0])
+      (* 2 [BIT 1])
+      (* 4 [BIT 2])
+      (* 8 [BIT 3]))))