Skip to content

Commit

Permalink
[readonly] Fix casts and add tests with ranges (#360)
Browse files Browse the repository at this point in the history
  • Loading branch information
titzer authored Feb 26, 2025
1 parent 1dd55b8 commit b43df73
Show file tree
Hide file tree
Showing 166 changed files with 1,771 additions and 7 deletions.
2 changes: 1 addition & 1 deletion aeneas/src/main/Version.v3
Original file line number Diff line number Diff line change
Expand Up @@ -3,6 +3,6 @@

// Updated by VCS scripts. DO NOT EDIT.
component Version {
def version: string = "III-9.1800";
def version: string = "III-9.1801";
var buildData: string;
}
21 changes: 15 additions & 6 deletions aeneas/src/v3/TypeSystem.v3
Original file line number Diff line number Diff line change
Expand Up @@ -14,7 +14,7 @@ component TypeSystem {
// for downcasts is involved; variance for element types is only enabled by a command-line
// flag.
private def isElemSubtype(xt: Type, yt: Type) -> bool {
return (xt == yt || (CLOptions.COVARIANT_ARRAYS.val && isSubtype(xt, yt)));
return xt == yt || (CLOptions.COVARIANT_ARRAYS.val && isSubtype(xt, yt));
}
// Check if type {xt} is promotable (i.e. with conversion operation) to type {yt}.
def isPromotable(xt: Type, yt: Type) -> bool {
Expand Down Expand Up @@ -541,11 +541,12 @@ 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);
var tt = ArrayType.!(toType);
match (fromType) {
ft: ArrayType => if (!tt.writeable) {
var fte = ft.elementType(), tte = tt.elementType();
if (isElemSubtype(fte, tte)) return TypeCast.TRUE;
return maybeCast(fte, tte, TypeCast.TRUE, TypeCast.THROW);
}
}
return maybeCast(fromType, toType, TypeCast.TRUE, TypeCast.THROW);
Expand Down Expand Up @@ -578,6 +579,14 @@ component TypeSystem {
if (V3.isArray(fromType)) {
return maybeCast(fromType.nested.head, toType.nested.head, TypeCast.RANGE_PROMOTE_ARRAY, TypeCast.THROW);
}
var tt = RangeType.!(toType);
match (fromType) {
ft: RangeType => if (!tt.writeable) {
var fte = ft.elementType(), tte = tt.elementType();
if (isElemSubtype(fte, tte)) return TypeCast.TRUE;
return maybeCast(fte, tte, TypeCast.TRUE, TypeCast.THROW);
}
}
return maybeCast(fromType, toType, TypeCast.TRUE, TypeCast.THROW);
}
if (V3.isRef(fromType)) {
Expand Down
3 changes: 3 additions & 0 deletions test/core/seman/array_cast00.v3
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
//@seman
var x: Array<int>;
var y = Array<int>.!(x);
3 changes: 3 additions & 0 deletions test/core/seman/array_cast01.v3
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
//@seman = TypeError @ 3:22
var x: Array<bool>;
var y = Array<int>.!(x);
12 changes: 12 additions & 0 deletions test/core/seman/array_cast02.v3
Original file line number Diff line number Diff line change
@@ -0,0 +1,12 @@
//@seman
var x0: Array<byte>;
var y0 = Array<byte>.!(x0);

var x1: Array<u32>;
var y1 = Array<u32>.!(x1);

var x2: Array<string>;
var y2 = Array<string>.!(x2);

var x3: Array<void>;
var y3 = Array<void>.!(x3);
23 changes: 23 additions & 0 deletions test/readonly/bm01.v3
Original file line number Diff line number Diff line change
@@ -0,0 +1,23 @@
//@execute =1

// An efficient data structure for a matrix of boolean values.
class BitMatrix(var numrows: int, var numcols: int) {
private var width: int = (numcols + 31) >>> 5; // width (in integers) of each row
private var bits = Array<int>.new(numrows * width); // array that stores the data
def rowInts(index: int) -> range<int> {
if (index >= numrows) return null;
return bits[(index * width) ..+ width];
}
}

var arr: array<int> = [];
def assert(b: bool) {
if (!b) var x = arr[2];
}

def main() -> int {
var b = BitMatrix.new(10, 62);
var x = b.rowInts(2);
var y = b.rowInts(5);
return 1;
}
6 changes: 6 additions & 0 deletions test/readonly/cast00.v3
Original file line number Diff line number Diff line change
@@ -0,0 +1,6 @@
//@execute 0=0; 4=4
def main(a: int) -> int {
var x = Array<int>.new(a);
var y: range<int> = range<int>.!(x);
return y.length;
}
6 changes: 6 additions & 0 deletions test/readonly/cast01.v3
Original file line number Diff line number Diff line change
@@ -0,0 +1,6 @@
//@execute 0=44; 4=44
var x = Array<int>.new(44);
def main(a: int) -> int {
var y: range<int> = range<int>.!(x);
return y.length;
}
6 changes: 6 additions & 0 deletions test/readonly/cast01b.v3
Original file line number Diff line number Diff line change
@@ -0,0 +1,6 @@
//@execute 0=44; 4=44
var x = Array<int>.new(44);
def main(a: int) -> int {
var y: range<int> = Range<int>.!(x);
return y.length;
}
6 changes: 6 additions & 0 deletions test/readonly/cast02.v3
Original file line number Diff line number Diff line change
@@ -0,0 +1,6 @@
//@execute -1=!LengthCheckException; 0=0; 2=2
def main(a: int) -> int {
var x = Array<int>.new(a);
var y = range<int>.!(x);
return y.length;
}
5 changes: 5 additions & 0 deletions test/readonly/cast03.v3
Original file line number Diff line number Diff line change
@@ -0,0 +1,5 @@
//@execute true=1; false=0
def main(a: bool) -> int {
var x: range<int> = range<int>.!(if(a, Array<int>.new(1)));
return x.length;
}
5 changes: 5 additions & 0 deletions test/readonly/cast03b.v3
Original file line number Diff line number Diff line change
@@ -0,0 +1,5 @@
//@execute true=1; false=0
def main(a: bool) -> int {
var x: range<int> = Range<int>.!(if(a, Array<int>.new(1)));
return x.length;
}
6 changes: 6 additions & 0 deletions test/readonly/cast04.v3
Original file line number Diff line number Diff line change
@@ -0,0 +1,6 @@
//@execute true=1; false=0
def main(a: bool) -> int {
var x: Array<int> = if(a, Array<int>.new(1));
var y: range<int> = range<int>.!(x);
return y.length;
}
6 changes: 6 additions & 0 deletions test/readonly/cast04b.v3
Original file line number Diff line number Diff line change
@@ -0,0 +1,6 @@
//@execute true=1; false=0
def main(a: bool) -> int {
var x: Array<int> = if(a, Array<int>.new(1));
var y: range<int> = Range<int>.!(x);
return y.length;
}
5 changes: 5 additions & 0 deletions test/readonly/del_length00.v3
Original file line number Diff line number Diff line change
@@ -0,0 +1,5 @@
//@execute 0=3
def x = [5555, 6666, 7777];
def main(a: int) -> int {
return range<int>.length(x);
}
5 changes: 5 additions & 0 deletions test/readonly/del_length01.v3
Original file line number Diff line number Diff line change
@@ -0,0 +1,5 @@
//@execute 0=0; 1=1; 2=2; 3=3
def x = [5555, 6666, 7777];
def main(a: int) -> int {
return range<int>.length(x[0 ..+ a]);
}
6 changes: 6 additions & 0 deletions test/readonly/del_length02.v3
Original file line number Diff line number Diff line change
@@ -0,0 +1,6 @@
//@execute 0=0; 1=1; 2=2; 3=3
def x = [5555, 6666, 7777];
def f = range<int>.length;
def main(a: int) -> int {
return f(x[0 ..+ a]);
}
6 changes: 6 additions & 0 deletions test/readonly/del_length03.v3
Original file line number Diff line number Diff line change
@@ -0,0 +1,6 @@
//@execute 0=0; 1=1; 2=2; 3=3
def x = [5555, 6666, 7777];
def f = range<int>.length;
def main(a: int) -> int {
return f(x[0 ... a]);
}
6 changes: 6 additions & 0 deletions test/readonly/del_length04.v3
Original file line number Diff line number Diff line change
@@ -0,0 +1,6 @@
//@execute 0=!LengthCheckException; 1=0; 2=1; 3=2
def x = [5555, 6666, 7777];
def f = range<int>.length;
def main(a: int) -> int {
return f(x[1 ... a]);
}
5 changes: 5 additions & 0 deletions test/readonly/empty00.v3
Original file line number Diff line number Diff line change
@@ -0,0 +1,5 @@
//@execute = true
def main() -> bool {
var x: range<int>;
return x == null;
}
5 changes: 5 additions & 0 deletions test/readonly/equal06.v3
Original file line number Diff line number Diff line change
@@ -0,0 +1,5 @@
//@execute = false
def x = [33, 44];
def main() -> bool {
return range<int>.==(x[0 ...], null);
}
5 changes: 5 additions & 0 deletions test/readonly/equal07.v3
Original file line number Diff line number Diff line change
@@ -0,0 +1,5 @@
//@execute 0=true; 1=false; 3=false; 4=!BoundsCheckException
def x = [33, 44, 55];
def main(a: int) -> bool {
return range<int>.==(x[0 ...], x[a ...]);
}
6 changes: 6 additions & 0 deletions test/readonly/equal08.v3
Original file line number Diff line number Diff line change
@@ -0,0 +1,6 @@
//@execute 0=false; 1=false; 3=false; 4=!BoundsCheckException
def x = [33, 44, 55];
def y = [33, 44, 55];
def main(a: int) -> bool {
return range<int>.==(x[0 ...], y[a ...]);
}
5 changes: 5 additions & 0 deletions test/readonly/equal09.v3
Original file line number Diff line number Diff line change
@@ -0,0 +1,5 @@
//@execute 0=false; 1=false; 2=true; 3=!BoundsCheckException
def x = [33, 44];
def main(a: int) -> bool {
return range<int>.==(x, x[0 ... a]);
}
5 changes: 5 additions & 0 deletions test/readonly/equal10.v3
Original file line number Diff line number Diff line change
@@ -0,0 +1,5 @@
//@execute 0=false; 1=false; 2=true; 3=!LengthCheckException
def x = [33, 44];
def main(a: int) -> bool {
return range<int>.==(x, x[0 ..+ a]);
}
20 changes: 20 additions & 0 deletions test/readonly/fail/downcast00.v3
Original file line number Diff line number Diff line change
@@ -0,0 +1,20 @@
//@execute 0=2; 1=!TypeCheckException; 2=!TypeCheckException; 3=3; 4=47
class A { }
class B extends A { }
def castAA = range<A>.!<range<A>>;
def castAB = range<A>.!<range<B>>;
def castBA = range<B>.!<range<A>>;
def castBB = range<B>.!<range<B>>;

def x: range<A> = [A.new(), B.new()];
def y: range<B> = [B.new(), B.new(), B.new()];

def main(a: int) -> int {
match (a) {
0 => return castAA(x).length;
1 => return castAB(y).length;
2 => return castBA(x).length;
3 => return castBB(y).length;
}
return 47;
}
19 changes: 19 additions & 0 deletions test/readonly/fail/downcast01.v3
Original file line number Diff line number Diff line change
@@ -0,0 +1,19 @@
//@execute 0=2; 1=!TypeCheckException; 2=!TypeCheckException; 3=3; 4=47
class A { }
class B extends A { }

def x: range<A> = [A.new(), B.new()];
def y: range<B> = [B.new(), B.new(), B.new()];

def main(a: int) -> int {
match (a) {
0 => return cast<A, A>(x).length;
1 => return cast<B, A>(y).length;
2 => return cast<A, B>(x).length;
3 => return cast<B, B>(y).length;
}
return 47;
}
def cast<F, T>(x: range<F>) -> range<T> {
return range<T>.!(x);
}
6 changes: 6 additions & 0 deletions test/readonly/get00.v3
Original file line number Diff line number Diff line change
@@ -0,0 +1,6 @@
//@execute 0=3; 1=4; 2=!BoundsCheckException
def x = [3, 4];
def y: range<int> = x;
def main(a: int) -> int {
return y[a];
}
6 changes: 6 additions & 0 deletions test/readonly/get02.v3
Original file line number Diff line number Diff line change
@@ -0,0 +1,6 @@
//@execute 0=4; 1=5; 2=6; 3=!BoundsCheckException
def x = [3, 4, 5, 6];
def y: range<int> = x[1 ...];
def main(a: int) -> int {
return y[a];
}
6 changes: 6 additions & 0 deletions test/readonly/get03.v3
Original file line number Diff line number Diff line change
@@ -0,0 +1,6 @@
//@execute 0=4; 1=5; 2=!BoundsCheckException
def x = [3, 4, 5, 6];
def y: range<int> = x[1 ... 3];
def main(a: int) -> int {
return y[a];
}
8 changes: 8 additions & 0 deletions test/readonly/get05.v3
Original file line number Diff line number Diff line change
@@ -0,0 +1,8 @@
//@execute 0=42; 1=!BoundsCheckException; 3=!BoundsCheckException; -1=!BoundsCheckException
def x: array<void> = [(), (), ()];
def y: range<void> = x[1 ... 2];

def main(a: int) -> int {
var d = y[a];
return 42;
}
8 changes: 8 additions & 0 deletions test/readonly/get_void00.v3
Original file line number Diff line number Diff line change
@@ -0,0 +1,8 @@
//@execute 0=42; 1=42; 2=42; 3=!BoundsCheckException; -1=!BoundsCheckException
def x: array<void> = [(), (), ()];
def y: range<void> = x;

def main(a: int) -> int {
var d = y[a];
return 42;
}
8 changes: 8 additions & 0 deletions test/readonly/get_void01.v3
Original file line number Diff line number Diff line change
@@ -0,0 +1,8 @@
//@execute 0=42; 1=42; 2=42; 3=!BoundsCheckException; -1=!BoundsCheckException
def x: array<void> = [(), (), ()];
def y: range<void> = x;

def main(a: int) -> int {
var d = y[a];
return 42;
}
5 changes: 5 additions & 0 deletions test/readonly/length00.v3
Original file line number Diff line number Diff line change
@@ -0,0 +1,5 @@
//@execute =2
def x: range<int> = [0, 0];
def main() -> int {
return x.length;
}
6 changes: 6 additions & 0 deletions test/readonly/length01.v3
Original file line number Diff line number Diff line change
@@ -0,0 +1,6 @@
//@execute =2
def x: range<int> = [0, 0];
def f = range<int>.length;
def main() -> int {
return f(x);
}
5 changes: 5 additions & 0 deletions test/readonly/length02.v3
Original file line number Diff line number Diff line change
@@ -0,0 +1,5 @@
//@execute =2
def x: range<(int, byte)> = [(0, 1), (2, 3)];
def main() -> int {
return x.length;
}
6 changes: 6 additions & 0 deletions test/readonly/length03.v3
Original file line number Diff line number Diff line change
@@ -0,0 +1,6 @@
//@execute =2
def x: range<(int, string)> = [(0, "ff"), (0, "gg")];
def f = range<(int, string)>.length;
def main() -> int {
return f(x);
}
6 changes: 6 additions & 0 deletions test/readonly/length04.v3
Original file line number Diff line number Diff line change
@@ -0,0 +1,6 @@
//@execute =2
def x: range<(int, void, string, bool)> = [(0, (), "ff", true), (0, (), "gg", false)];
def f = range<(int, void, string, bool)>.length;
def main() -> int {
return f(x);
}
9 changes: 9 additions & 0 deletions test/readonly/long03.v3
Original file line number Diff line number Diff line change
@@ -0,0 +1,9 @@
//@execute 0=0; 1=!BoundsCheckException
def x: range<int> = [33, 44];
def main(a: int) -> int {
for (shift: u6 < 62) {
var i = long.view(a) << shift;
var s = x[i];
}
return a;
}
8 changes: 8 additions & 0 deletions test/readonly/long_oob10c.v3
Original file line number Diff line number Diff line change
@@ -0,0 +1,8 @@
//@execute (-1, 2)=!BoundsCheckException; (0, 2)=2; (1, 2)=1; (-1, 3)=!BoundsCheckException; (0, 3)=3; (1, 3)=2; (-1, 4)=!BoundsCheckException; (0, 4)=!BoundsCheckException; (1, 4)=!BoundsCheckException
def x: range<byte> = "abc";
def main(a: int, b: int) -> int {
return sub(x, a, b).length;
}
def sub<T>(r: range<T>, a: long, b: long) -> range<T> {
return r[a ... b];
}
8 changes: 8 additions & 0 deletions test/readonly/long_oob11c.v3
Original file line number Diff line number Diff line change
@@ -0,0 +1,8 @@
//@execute (-2147483648, 66)=!BoundsCheckException; (0, 66)=66; (1, 66)=65; (-2147483648, 88)=!BoundsCheckException; (0, 88)=88; (1, 88)=87; (-2147483648, 89)=!BoundsCheckException; (0, 89)=!BoundsCheckException; (1, 89)=!BoundsCheckException
def x: range<void> = Array<void>.new(88);
def main(a: int, b: int) -> int {
return sub(x, a, b).length;
}
def sub<T>(r: range<T>, a: long, b: long) -> range<T> {
return r[a ... b];
}
8 changes: 8 additions & 0 deletions test/readonly/long_oob12.v3
Original file line number Diff line number Diff line change
@@ -0,0 +1,8 @@
//@execute 0=!BoundsCheckException; 1=!BoundsCheckException; -1=!BoundsCheckException
def x: range<byte> = "perf";
def main(a: int) -> int {
return sub(x, 0x1_0000_0000L | a, x.length).length;
}
def sub<T>(r: range<T>, a: long, b: long) -> range<T> {
return r[a ... b];
}
8 changes: 8 additions & 0 deletions test/readonly/long_oob13.v3
Original file line number Diff line number Diff line change
@@ -0,0 +1,8 @@
//@execute 0=!BoundsCheckException; 1=!BoundsCheckException; -1=!BoundsCheckException
def x: range<byte> = "perf";
def main(a: int) -> int {
return sub(x, 0, a | 0x16273_0000_0000L).length;
}
def sub<T>(r: range<T>, a: long, b: long) -> range<T> {
return r[a ... b];
}
8 changes: 8 additions & 0 deletions test/readonly/long_oob14.v3
Original file line number Diff line number Diff line change
@@ -0,0 +1,8 @@
//@execute 0=!BoundsCheckException; 1=!BoundsCheckException; -1=!BoundsCheckException
def x: range<byte> = "perf";
def main(a: int) -> int {
return sub(x, 0x1_0000_0000L | a, x.length).length;
}
def sub<T>(r: range<T>, a: long, b: long) -> range<T> {
return r[a ..+ b];
}
Loading

0 comments on commit b43df73

Please sign in to comment.