[readonly] Check for readonly assignments and allow basic subsumption (…

…#357)

aeneas/src/main/Version.v3

@@ -3,6 +3,6 @@
 
 // Updated by VCS scripts. DO NOT EDIT.
 component Version {
-	def version: string = "III-9.1799";
+	def version: string = "III-9.1800";
 	var buildData: string;
 }

aeneas/src/v3/TypeSystem.v3

@@ -184,8 +184,8 @@ component TypeSystem {
 				y: ArrayType => {
 					var xe = x.elementType(), ye = y.elementType();
 					if (!y.writeable) {
-						if (isSubtype(xe, ye)) return Conversion.SUBSUME_ARRAY; // covariant upcast
-						if (isSubtype(ye, xe)) return Conversion.CAST_ARRAY;    // downcast
+						if (isElemSubtype(xe, ye)) return Conversion.SUBSUME_ARRAY; // covariant upcast
+						if (isElemSubtype(ye, xe)) return Conversion.CAST_ARRAY;    // downcast
 					}
 					if (xe.open() || ye.open()) {
 						return if(maybeEqual(xe, ye), Conversion.CAST_POLY, Conversion.ILLEGAL);
@@ -195,8 +195,8 @@ component TypeSystem {
 					var xe = x.elementType(), ye = y.elementType();
 					if (xe == ye) return Conversion.PROMOTE_ARRAY_TO_RANGE;
 					if (!y.writeable) {
-						if (isSubtype(xe, ye)) return Conversion.PROMOTE_ARRAY_TO_RANGE;
-						if (isSubtype(ye, xe)) return Conversion.CAST_ARRAY_TO_RANGE;
+						if (isElemSubtype(xe, ye)) return Conversion.PROMOTE_ARRAY_TO_RANGE;
+						if (isElemSubtype(ye, xe)) return Conversion.CAST_ARRAY_TO_RANGE;
 					}
 					if (xe.open() || ye.open()) {
 						return if(maybeEqual(xe, ye), Conversion.CAST_POLY, Conversion.ILLEGAL);
@@ -207,8 +207,8 @@ component TypeSystem {
 				y: RangeType => {
 					var xe = x.elementType(), ye = y.elementType();
 					if (!y.writeable) {
-						if (isSubtype(xe, ye)) return Conversion.SUBSUME_RANGE; // covariant upcast
-						if (isSubtype(ye, xe)) return Conversion.CAST_RANGE;    // downcast
+						if (isElemSubtype(xe, ye)) return Conversion.SUBSUME_RANGE; // covariant upcast
+						if (isElemSubtype(ye, xe)) return Conversion.CAST_RANGE;    // downcast
 					}
 					if (xe.open() || ye.open()) {
 						return if(maybeEqual(xe, ye), Conversion.CAST_POLY, Conversion.ILLEGAL);
@@ -541,6 +541,13 @@ component TypeSystem {
 		if (V3.isArray(toType)) {
 			if (fromType == Null.TYPE) return TypeCast.TRUE;
 			if (AnyRefType.?(fromType)) return TypeCast.TRUE; // TODO: array downcast
+			var att = ArrayType.!(toType);
+			if (!att.writeable) {
+				if (V3.isArray(fromType)) {
+					var aft = ArrayType.!(fromType);
+					return if(isElemSubtype(aft.elementType(), att.elementType()), TypeCast.TRUE, TypeCast.THROW);
+				}
+			}
 			return maybeCast(fromType, toType, TypeCast.TRUE, TypeCast.THROW);
 		}
 		if (V3.isVariant(fromType)) {

aeneas/src/vst/Verifier.v3

@@ -1367,7 +1367,7 @@ class TypeChecker(ERROR: ErrorGen, file: VstFile) extends VstVisitor<Type, Type>
 		return if(outer == null, getErrorType(), outer);
 	}
 	def visitAutoExpr(expr: AutoExpr, outer: Type) -> Type {
-		var t = checkWrite(expr.expr);
+		var t = checkWrite(expr.expr, expr.token);
 		if (IndexExpr.?(expr.expr)) t = checkIndexedRead(IndexExpr.!(expr.expr), outer);
 		var op = expr.op;
 		if (op == null) op = methodEnv.lookupInfix(expr.infix, t, t);
@@ -1747,7 +1747,7 @@ class TypeChecker(ERROR: ErrorGen, file: VstFile) extends VstVisitor<Type, Type>
 		errAtRange(expr.exprs.range()).set("TypeError", Strings.format1("type %s has no [] operator", TYPE(exprType)));
 		return getErrorType();
 	}
-	def checkIndexedWrite(expr: IndexExpr, outer: Type) -> Type {
+	def checkIndexedWrite(expr: IndexExpr, outer: Type, pt: FilePoint) -> Type {
 		var arrayType = if(outer != null, V3Array.newType(outer)); // try using array type for outer
 		var exprType: Type;
 		match (expr.expr) {
@@ -1774,8 +1774,14 @@ class TypeChecker(ERROR: ErrorGen, file: VstFile) extends VstVisitor<Type, Type>
 			}
 		}
 		match (exprType) {
-			x: ArrayType => return visitArrayIndex(expr, x);
-			x: RangeType => return visitArrayIndex(expr, x);
+			x: ArrayType => {
+				if (!x.writeable) errAtPoint(pt).set("AssignError", Strings.format1("illegal assignment to read-only %s element", TYPE(x)));
+				return visitArrayIndex(expr, x);
+			}
+			x: RangeType => {
+				if (!x.writeable) errAtPoint(pt).set("AssignError", Strings.format1("illegal assignment to read-only %s element", TYPE(x)));
+				return visitArrayIndex(expr, x);
+			}
 			x: ClassType => {
 				var varExpr = VarExpr.new(expr, null, VstIdent<TypeRef>.new(null, 0, null));
 				var member = methodEnv.resolveClassMember(varExpr, x, "[]=");
@@ -1890,7 +1896,7 @@ class TypeChecker(ERROR: ErrorGen, file: VstFile) extends VstVisitor<Type, Type>
 		}
 		return t;
 	}
-	def checkWrite(left: Expr) -> Type {
+	def checkWrite(left: Expr, pt: FilePoint) -> Type {
 		var result: Type;
 		match (left) {
 			x: VarExpr => {
@@ -1906,7 +1912,7 @@ class TypeChecker(ERROR: ErrorGen, file: VstFile) extends VstVisitor<Type, Type>
 				}
 			}
 			x: IndexExpr => {
-				result = checkIndexedWrite(x, null);
+				result = checkIndexedWrite(x, null, pt);
 				left.exactType = result;
 				return result;
 			}
@@ -1919,8 +1925,8 @@ class TypeChecker(ERROR: ErrorGen, file: VstFile) extends VstVisitor<Type, Type>
 	}
 	def visitAssign(expr: AssignExpr, outer: Type) -> Type {
 		var left = expr.target;
-		var ltype = checkWrite(left);
 		var infix = expr.infix;
+		var ltype = checkWrite(left, expr.assign);
 		if (infix != null) {
 			if (IndexExpr.?(left)) ltype = checkIndexedRead(IndexExpr.!(left), outer);
 			if (infix.op == null) infix.op = methodEnv.lookupInfix(infix.infix, ltype, null);

test/readonly/alloc_array07.v3

@@ -0,0 +1,5 @@
+//@execute = true
+def main() -> bool {
+	var x: array<byte> = Array<byte>.new(1);
+	return x != null;
+}

test/readonly/alloc_array08.v3

@@ -0,0 +1,6 @@
+//@execute = true
+def main() -> bool {
+	var x: array<byte> = Array<byte>.new(1);
+	var y: array<byte> = Array<byte>.new(1);
+	return x != y;
+}

test/readonly/alloc_array13.v3

@@ -0,0 +1,7 @@
+//@execute = true
+def nn(a: array<byte>) -> bool {
+	return a != null;
+}
+def main() -> bool {
+	return nn(['0']);
+}

test/readonly/array01.v3

@@ -0,0 +1,8 @@
+//@execute 0=997; 1=!BoundsCheckException
+var x: array<int> = [997];
+def main(a: int) -> int {
+	return read(x, a);
+}
+def read(x: array<int>, i: int) -> int {
+	return x[i];
+}

test/readonly/array02.v3

@@ -0,0 +1,8 @@
+//@execute 0=997; 1=!BoundsCheckException
+var x: array<int> = [997];
+def main(a: int) -> int {
+	return read(x, a);
+}
+def read<T>(x: array<T>, i: int) -> T {
+	return x[i];
+}

test/readonly/fail/adhoc02.v3

@@ -0,0 +1,16 @@
+//@execute 0=0; 1=1; 2=2; 3=3; 4=4
+def main(a: int) -> int {
+	if (a == 0) return getType([0]);
+	if (a == 1) return getType(['0']);
+	if (a == 2) return getType([true]);
+	if (a == 3) return getType([()]);
+	var a: array<int>;
+	return getType(a);
+}
+def getType<T>(a: T) -> int {
+	if (array<int>.?(a)) return 0;
+	if (array<byte>.?(a)) return 1;
+	if (array<bool>.?(a)) return 2;
+	if (array<void>.?(a)) return 3;
+	return 4;
+}

test/readonly/fail/adhoc05.v3

@@ -0,0 +1,10 @@
+//@execute 0=0; 1=4
+def main(a: int) -> int {
+	if (a == 0) return getType([0]);
+	var a: array<int>;
+	return getType(a);
+}
+def getType<T>(a: T) -> int {
+	if (array<int>.?(a)) return 0;
+	return 4;
+}

test/readonly/fail/adhoc06.v3

@@ -0,0 +1,12 @@
+//@execute 0=0; 1=4
+def x = [0];
+def main(a: int) -> int {
+	if (a == 0) return getType(x);
+	var a: array<int>;
+	return getType(a);
+}
+def getType<T>(a: T) -> int {
+	if (array<int>.?(a)) return 0;
+	if (array<void>.?(a)) return 3;
+	return 4;
+}

test/readonly/range00.v3

@@ -0,0 +1,5 @@
+//@execute 0=997; 1=!BoundsCheckException
+var x: range<int> = [997];
+def main(a: int) -> int {
+	return x[a];
+}

test/readonly/range01.v3

@@ -0,0 +1,8 @@
+//@execute 0=997; 1=!BoundsCheckException
+var x: range<int> = [997];
+def main(a: int) -> int {
+	return read(x, a);
+}
+def read(x: range<int>, i: int) -> int {
+	return x[i];
+}

test/readonly/range02.v3

@@ -0,0 +1,8 @@
+//@execute 0=997; 1=!BoundsCheckException
+var x: range<int> = [997];
+def main(a: int) -> int {
+	return read(x, a);
+}
+def read<T>(x: range<T>, i: int) -> T {
+	return x[i];
+}

test/readonly/seman/auto03.v3

@@ -0,0 +1,17 @@
+//@seman = AssignError @ 4:31
+def main(a: int) -> bool {
+	var m: array<int> = [a];
+	return post(m[0], m[0]++, m[0])
+		&& post(m[0], m[0]--, m[0])
+		&& pre(m[0], ++m[0], m[0])
+		&& pre(m[0], --m[0], m[0]);
+}
+def post(a: int, b: int, c: int) -> bool {
+	var d = b - c;
+	return a == b && (d * d == 1);
+}
+def pre(a: int, b: int, c: int) -> bool {
+	var d = a - c;
+	return b == c && (d * d == 1);
+}
+

test/readonly/seman/compound_lval22.v3

@@ -0,0 +1,13 @@
+//@seman = AssignError @ 5:25
+var f: int;
+def m() {
+	var a: array<int> = [0];
+	a[f += 1] += 1;
+	a[f -= 1] -= 1;
+	a[f *= 1] *= 1;
+	a[f /= 1] /= 1;
+	a[f %= 1] %= 1;
+	a[f &= 1] &= 1;
+	a[f |= 1] |= 1;
+	a[f ^= 1] ^= 1;
+}

test/readonly/seman/write00.v3

@@ -0,0 +1,4 @@
+//@seman = AssignError @ 3:14
+def f(x: array<int>) {
+	x[0] = 0;
+}

test/readonly/seman/write01.v3

@@ -0,0 +1,4 @@
+//@seman = AssignError @ 3:14
+def f(x: array<int>) {
+	x[0]++ ;
+}

test/readonly/seman/write02.v3

@@ -0,0 +1,4 @@
+//@seman = AssignError @ 3:14
+def f(x: array<int>) {
+	--x[0];
+}

test/readonly/seman/write03.v3

@@ -0,0 +1,4 @@
+//@seman = AssignError @ 3:14
+def f(x: array<int>) {
+	x[0] -= 2;
+}

test/readonly/seman/write04.v3

@@ -0,0 +1,4 @@
+//@seman = AssignError @ 3:14
+def f(x: array<int>) {
+	x[0] |= 2;
+}

test/readonly/seman/write05.v3

@@ -0,0 +1,4 @@
+//@seman = AssignError @ 3:14
+def f(x: array<int>) {
+	x[0] >>= 2;
+}