Skip to content

Commit

Permalink
[layouts] Implement #big-endian layouts and fields (#294)
Browse files Browse the repository at this point in the history
  • Loading branch information
@titzer
titzer authored Nov 1, 2024
1 parent 6960299 commit df20140
Show file tree
Hide file tree
Showing 54 changed files with 1,205 additions and 238 deletions.
38 changes: 19 additions & 19 deletions aeneas/src/core/Eval.v3
View file
Original file line number Diff line number Diff line change
Expand Up @@ -863,13 +863,13 @@ def evalOp(op: Operator, args: Arguments) -> Result {
if (ref == null) return ByteArrayOffset.new(null, offset);
return ByteArrayOffset.new(ref.array, ref.offset + offset);
}
RefLayoutGetField(offset) => {
RefLayoutGetField(offset, order) => {
var ref = args.ref(0);
return doRefLayoutGetField(args, args.getTypeArg(1), ref, offset);
return doRefLayoutGetField(args, args.getTypeArg(1), ref, offset, order);
}
RefLayoutSetField(offset) => {
RefLayoutSetField(offset, order) => {
var ref = args.ref(0);
return doRefLayoutSetField(args, args.getTypeArg(1), ref, offset, args.vals[1]);
return doRefLayoutSetField(args, args.getTypeArg(1), ref, offset, order, args.vals[1]);
}
RefLayoutAtRepeatedField(offset, scale, max) => {
var ref = args.ref(0);
Expand All @@ -879,29 +879,29 @@ def evalOp(op: Operator, args: Arguments) -> Result {
if (ref == null) return ByteArrayOffset.new(null, noffset);
return ByteArrayOffset.new(ref.array, ref.offset + noffset);
}
RefLayoutGetRepeatedField(offset, scale, max) => {
RefLayoutGetRepeatedField(offset, scale, max, order) => {
var ref = args.ref(0);
var index = args.i(1);
if (u32.view(index) >= u32.view(max)) return args.throw(V3Exception.BoundsCheck, null);
return doRefLayoutGetField(args, args.getTypeArg(1), ref, offset + scale * index);
return doRefLayoutGetField(args, args.getTypeArg(1), ref, offset + scale * index, order);
}
RefLayoutSetRepeatedField(offset, scale, max) => {
RefLayoutSetRepeatedField(offset, scale, max, order) => {
var ref = args.ref(0);
var index = args.i(1);
if (u32.view(index) >= u32.view(max)) return args.throw(V3Exception.BoundsCheck, null);
return doRefLayoutSetField(args, args.getTypeArg(1), ref, offset + scale * index, args.vals[2]);
return doRefLayoutSetField(args, args.getTypeArg(1), ref, offset + scale * index, order, args.vals[2]);
}
ByteArrayGetField(offset) => {
ByteArrayGetField(offset, order) => {
var array = args.r(0);
var i_offset = if(ArrayRangeStart.?(args.vals[1]), ArrayRangeStart.!(args.vals[1]).start, args.i(1));
// XXX: Refactor so no intermediate ByteArrayOffset object needed
return doRefLayoutGetField(args, args.getTypeArg(0), ByteArrayOffset.new(array, offset), i_offset);
return doRefLayoutGetField(args, args.getTypeArg(0), ByteArrayOffset.new(array, offset), i_offset, order);
}
ByteArraySetField(offset) => {
ByteArraySetField(offset, order) => {
var array = args.r(0);
var i_offset = if(ArrayRangeStart.?(args.vals[1]), ArrayRangeStart.!(args.vals[1]).start, args.i(1));
// XXX: Refactor so no intermediate ByteArrayOffset object needed
return doRefLayoutSetField(args, args.getTypeArg(0), ByteArrayOffset.new(array, offset), i_offset, args.vals[2]);
return doRefLayoutSetField(args, args.getTypeArg(0), ByteArrayOffset.new(array, offset), i_offset, order, args.vals[2]);
}

//----------------------------------------------------------------------------
Expand Down Expand Up @@ -929,15 +929,15 @@ def evalOp(op: Operator, args: Arguments) -> Result {
return args.throw("EvalUnimplemented", op.opcode.name);
}

def doRefLayoutGetField(args: Arguments, fieldType: Type, ref: ByteArrayOffset, offset: int) -> Result {
def doRefLayoutGetField(args: Arguments, fieldType: Type, ref: ByteArrayOffset, offset: int, order: ByteOrder) -> Result {
if (ref == null || ref.array == null) return args.throw(V3Exception.NullCheck, null);
match (fieldType) {
x: BoolType => {
var v = ref.read(false, offset, 1);
var v = ref.read(order, offset, 1);
return Bool.box((v & 1) != 0);
}
x: IntType => {
var v = ref.read(/*TODO:bigEndian=*/false, offset, x.size);
var v = ref.read(order, offset, x.size);
match (x.rank) {
SUBI32 => return Int.box(int.view(v) << x.ishift >> x.ishift);
SUBU32 => return Int.box(int.view(v) << x.ishift >>> x.ishift);
Expand All @@ -948,19 +948,19 @@ def doRefLayoutGetField(args: Arguments, fieldType: Type, ref: ByteArrayOffset,
}
}
x: EnumType => {
var v = ref.read(false, offset, x.packedByteSize());
var v = ref.read(order, offset, x.packedByteSize());
if (v >= x.enumDecl.cases.length) v = 0; // out-of-bounds tag => 0
return Int.box(int.view(v)); // TODO: long enum vals?
}
x: FloatType => {
var v = ref.read(false, offset, x.byteSize());
var v = ref.read(order, offset, x.byteSize());
if (x.is64) return Float64Val.new(v);
else return Float32Val.new(u32.view(v));
}
_ => return args.throw("EvalException", Strings.format1("invalid RefLayoutField type %q", fieldType.render));
}
}
def doRefLayoutSetField(args: Arguments, fieldType: Type, ref: ByteArrayOffset, offset: int, val: Val) -> Result {
def doRefLayoutSetField(args: Arguments, fieldType: Type, ref: ByteArrayOffset, offset: int, order: ByteOrder, val: Val) -> Result {
if (ref == null || ref.array == null) return args.throw(V3Exception.NullCheck, null);
var size = 0, bits: u64 = 0, signed = false;
match (fieldType) {
Expand All @@ -986,7 +986,7 @@ def doRefLayoutSetField(args: Arguments, fieldType: Type, ref: ByteArrayOffset,
v: Float32Val => bits = v.bits;
v: Float64Val => bits = v.bits;
}
ref.write(false, offset, size, bits);
ref.write(order, offset, size, bits);
return Values.BOTTOM;
}

Expand Down
12 changes: 6 additions & 6 deletions aeneas/src/core/Opcode.v3
View file
Original file line number Diff line number Diff line change
Expand Up @@ -132,13 +132,13 @@ type Opcode {
case RefLayoutAt;
case RefLayoutOf;
case RefLayoutIn(offset: int);
case RefLayoutGetField(offset: int);
case RefLayoutSetField(offset: int);
case RefLayoutGetField(offset: int, order: ByteOrder);
case RefLayoutSetField(offset: int, order: ByteOrder);
case RefLayoutAtRepeatedField(offset: int, scale: int, max: int);
case RefLayoutGetRepeatedField(offset: int, scale: int, max: int);
case RefLayoutSetRepeatedField(offset: int, scale: int, max: int);
case ByteArrayGetField(offset: int);
case ByteArraySetField(offset: int);
case RefLayoutGetRepeatedField(offset: int, scale: int, max: int, order: ByteOrder);
case RefLayoutSetRepeatedField(offset: int, scale: int, max: int, order: ByteOrder);
case ByteArrayGetField(offset: int, order: ByteOrder);
case ByteArraySetField(offset: int, order: ByteOrder);
case ForgeRange;
// System operations
case SystemCall(syscall: SystemCall);
Expand Down
35 changes: 19 additions & 16 deletions aeneas/src/core/Operator.v3
View file
Original file line number Diff line number Diff line change
Expand Up @@ -522,31 +522,31 @@ component V3Op {
var at: Array<Type> = [refType, result];
return newOp0(Opcode.RefLayoutIn(offset), at, [refType], result);
}
def newRefLayoutGetField(refType: RefType, offset: int, fieldType: Type) -> Operator {
return newOp0(Opcode.RefLayoutGetField(offset), [refType, fieldType], [refType], fieldType);
def newRefLayoutGetField(refType: RefType, offset: int, fieldType: Type, order: ByteOrder) -> Operator {
return newOp0(Opcode.RefLayoutGetField(offset, order), [refType, fieldType], [refType], fieldType);
}
def newRefLayoutSetField(refType: RefType, offset: int, fieldType: Type) -> Operator {
def newRefLayoutSetField(refType: RefType, offset: int, fieldType: Type, order: ByteOrder) -> Operator {
var at = [refType, fieldType];
return newOp0(Opcode.RefLayoutSetField(offset), at, at, Void.TYPE);
return newOp0(Opcode.RefLayoutSetField(offset, order), at, at, Void.TYPE);
}
def newRefLayoutAtRepeatedField(refType: RefType, offset: int, scale: int, max: int, result: RefType) -> Operator {
var opcode = Opcode.RefLayoutAtRepeatedField(offset, scale, max);
return newOp0(opcode, [refType, result], [refType, Int.TYPE], result);
}
def newRefLayoutGetRepeatedField(refType: RefType, offset: int, scale: int, max: int, fieldType: Type) -> Operator {
var opcode = Opcode.RefLayoutGetRepeatedField(offset, scale, max);
def newRefLayoutGetRepeatedField(refType: RefType, offset: int, scale: int, max: int, fieldType: Type, order: ByteOrder) -> Operator {
var opcode = Opcode.RefLayoutGetRepeatedField(offset, scale, max, order);
return newOp0(opcode, [refType, fieldType], [refType, Int.TYPE], fieldType);
}
def newRefLayoutSetRepeatedField(refType: RefType, offset: int, scale: int, max: int, fieldType: Type) -> Operator {
var opcode = Opcode.RefLayoutSetRepeatedField(offset, scale, max);
def newRefLayoutSetRepeatedField(refType: RefType, offset: int, scale: int, max: int, fieldType: Type, order: ByteOrder) -> Operator {
var opcode = Opcode.RefLayoutSetRepeatedField(offset, scale, max, order);
return newOp0(opcode, [refType, fieldType], [refType, Int.TYPE, fieldType], Void.TYPE);
}
def newByteArrayGetField(offset: int, fieldType: Type, startType: Type) -> Operator {
var opcode = Opcode.ByteArrayGetField(offset);
def newByteArrayGetField(offset: int, fieldType: Type, order: ByteOrder, startType: Type) -> Operator {
var opcode = Opcode.ByteArrayGetField(offset, order);
return newOp0(opcode, [fieldType, startType], [V3.arrayByteType, startType], fieldType);
}
def newByteArraySetField(offset: int, fieldType: Type, startType: Type) -> Operator {
var opcode = Opcode.ByteArraySetField(offset);
def newByteArraySetField(offset: int, fieldType: Type, order: ByteOrder, startType: Type) -> Operator {
var opcode = Opcode.ByteArraySetField(offset, order);
return newOp0(opcode, [fieldType, startType], [V3.arrayByteType, startType, fieldType], Void.TYPE);
}
//----------------------------------------------------------------------------
Expand Down Expand Up @@ -626,10 +626,13 @@ def renderOp(op: Operator, buf: StringBuilder) -> StringBuilder {
CallVariantSelector(selector) => rfunc = selector.render;
CreateClosure(method) => rfunc = method.render;
RefLayoutIn(offset) => rfunc = StringBuilder.putd(_, offset);
RefLayoutGetField(offset) => rfunc = StringBuilder.putd(_, offset);
RefLayoutSetField(offset) => rfunc = StringBuilder.putd(_, offset);
ByteArrayGetField(offset) => rfunc = StringBuilder.putd(_, offset);
ByteArraySetField(offset) => rfunc = StringBuilder.putd(_, offset);
RefLayoutGetField(offset, order) => rfunc = StringBuilder.put2(_, "%d,%s", offset, order.name);
RefLayoutSetField(offset, order) => rfunc = StringBuilder.put2(_, "%d,%s", offset, order.name);
RefLayoutAtRepeatedField(offset, scale, max) => rfunc = StringBuilder.put2(_, "%d,%d", offset, scale);
RefLayoutGetRepeatedField(offset, scale, max, order) => rfunc = StringBuilder.put3(_, "%d,%d,%s", offset, scale, order.name);
RefLayoutSetRepeatedField(offset, scale, max, order) => rfunc = StringBuilder.put3(_, "%d,%d,%s", offset, scale, order.name);
ByteArrayGetField(offset, order) => rfunc = StringBuilder.put2(_, "%d,%s", offset, order.name);
ByteArraySetField(offset, order) => rfunc = StringBuilder.put2(_, "%d,%s", offset, order.name);
ConditionalThrow(exception) => rfunc = StringBuilder.puts(_, exception);
SystemCall(syscall) => rfunc = StringBuilder.puts(_, syscall.name);
VstSugar(op) => rfunc = StringBuilder.puts(_, op.name);
Expand Down
64 changes: 16 additions & 48 deletions aeneas/src/ir/SsaNormalizer.v3
View file
Original file line number Diff line number Diff line change
Expand Up @@ -392,7 +392,7 @@ class SsaRaNormalizer extends SsaRebuilder {
curBlock.opIntAdd(start, newGraph.intConst(offset)));
return mapN(i_old, ai_new);
}
RefLayoutGetField(offset) => {
RefLayoutGetField(offset, order) => {
var an = arrayByteNorm;
var fn = normTypeArg(op, 1);
var ai_new = genRefs(i_old.inputs);
Expand All @@ -401,12 +401,12 @@ class SsaRaNormalizer extends SsaRebuilder {
var result: SsaInstr;

match (fn.oldType) {
x: IntType => result = curBlock.opByteArrayGetField(x, rangeStartType, offset, facts, array, start);
x: FloatType => result = curBlock.opByteArrayGetField(x, rangeStartType, offset, facts, array, start);
x: IntType => result = curBlock.opByteArrayGetField(x, rangeStartType, offset, order, facts, array, start);
x: FloatType => result = curBlock.opByteArrayGetField(x, rangeStartType, offset, order, facts, array, start);
x: EnumType => {
var it = IntType.!(x.enumDecl.tagType);
var wt = Int.getType(false, it.byteSize() * 8);
result = curBlock.opByteArrayGetField(wt, rangeStartType, offset, facts, array, start);
result = curBlock.opByteArrayGetField(wt, rangeStartType, offset, order, facts, array, start);
var caseCount = newGraph.intConst(x.enumDecl.cases.length);
var inBound = curBlock.opIntULt(norm.config.ArrayLengthType, it, result, caseCount);
result = curBlock.opIntViewI0(it, wt, result);
Expand All @@ -416,25 +416,25 @@ class SsaRaNormalizer extends SsaRebuilder {
}
return map1(i_old, result);
}
RefLayoutSetField(offset) => {
RefLayoutSetField(offset, order) => {
var fn = normTypeArg(op, 1);
var ai_new = genRefs(args);
var array = ai_new[0], start = ai_new[1], val = ai_new[2];
var facts: Fact.set = Fact.O_NO_BOUNDS_CHECK;
var result: SsaInstr;

match (fn.oldType) {
x: IntType => result = curBlock.opByteArraySetField(fn.oldType, rangeStartType, offset, facts, array, start, val);
x: FloatType => result = curBlock.opByteArraySetField(fn.oldType, rangeStartType, offset, facts, array, start, val);
x: IntType => result = curBlock.opByteArraySetField(fn.oldType, rangeStartType, offset, order, facts, array, start, val);
x: FloatType => result = curBlock.opByteArraySetField(fn.oldType, rangeStartType, offset, order, facts, array, start, val);
x: EnumType => {
var it = IntType.!(x.enumDecl.tagType);
var wt = Int.getType(false, it.byteSize() * 8);
result = curBlock.opByteArraySetField(wt, rangeStartType, offset, facts, array, start, val);
result = curBlock.opByteArraySetField(wt, rangeStartType, offset, order, facts, array, start, val);
}
}
return map1(i_old, result);
}
RefLayoutGetRepeatedField(offset, scale, max) => {
RefLayoutGetRepeatedField(offset, scale, max, order) => {
var rn = normTypeArg(op, 0), fn = normTypeArg(op, 1);
var ai_new = genRefs(args);
var array = ai_new[0], start = ai_new[1], index = ai_new[2];
Expand All @@ -450,11 +450,11 @@ class SsaRaNormalizer extends SsaRebuilder {
);
var facts: Fact.set = Fact.O_NO_BOUNDS_CHECK;
match (fn.oldType) {
x: IntType => result = curBlock.opByteArrayGetField(x, rangeStartType, offset, facts, array, start);
x: FloatType => result = curBlock.opByteArrayGetField(x, rangeStartType, offset, facts, array, start);
x: IntType => result = curBlock.opByteArrayGetField(x, rangeStartType, offset, order, facts, array, start);
x: FloatType => result = curBlock.opByteArrayGetField(x, rangeStartType, offset, order, facts, array, start);
x: EnumType => {
var it = IntType.!(x.enumDecl.tagType);
result = curBlock.opByteArrayGetField(it, rangeStartType, offset, facts, array, start);
result = curBlock.opByteArrayGetField(it, rangeStartType, offset, order, facts, array, start);
var caseCount = newGraph.intConst(x.enumDecl.cases.length);
var inBound = curBlock.opIntULt(it, it, result, caseCount);
result = curBlock.addSelect(it, inBound, result, newGraph.nullConst(it));
Expand All @@ -463,7 +463,7 @@ class SsaRaNormalizer extends SsaRebuilder {
}
return map1(i_old, result);
}
RefLayoutSetRepeatedField(offset, scale, max) => {
RefLayoutSetRepeatedField(offset, scale, max, order) => {
var rn = normTypeArg(op, 0), fn = normTypeArg(op, 1);
var ai_new = genRefs(args);
var array = ai_new[0], start = ai_new[1], index = ai_new[2], val = ai_new[3];
Expand All @@ -479,11 +479,11 @@ class SsaRaNormalizer extends SsaRebuilder {
var facts: Fact.set = Fact.O_NO_BOUNDS_CHECK;
var result: SsaInstr;
match (fn.oldType) {
x: IntType => result = curBlock.opByteArraySetField(fn.oldType, rangeStartType, offset, facts, array, start, val);
x: FloatType => result = curBlock.opByteArraySetField(fn.oldType, rangeStartType, offset, facts, array, start, val);
x: IntType => result = curBlock.opByteArraySetField(fn.oldType, rangeStartType, offset, order, facts, array, start, val);
x: FloatType => result = curBlock.opByteArraySetField(fn.oldType, rangeStartType, offset, order, facts, array, start, val);
x: EnumType => {
var it = IntType.!(x.enumDecl.tagType);
result = curBlock.opByteArraySetField(it, rangeStartType, offset, facts, array, start, val);
result = curBlock.opByteArraySetField(it, rangeStartType, offset, order, facts, array, start, val);
}
}
return map1(i_old, result);
Expand Down Expand Up @@ -580,38 +580,6 @@ class SsaRaNormalizer extends SsaRebuilder {
}
}
}
def genArrayByteGetMultiple(i_old: SsaApplyOp, it: IntType, array: SsaInstr, i_offset: SsaInstr, offset: int) -> SsaInstr {
// TODO: little-endian only for now
curBlock.at(i_old.source);
var facts: Fact.set = Fact.O_NO_BOUNDS_CHECK;
var size = it.packedByteSize();
var wt = Int.getType(false, it.byteSize() * 8); // rounded to next power of two for efficient shifting
var result: SsaInstr = newGraph.nullConst(wt);
var indexType = norm.config.RangeStartType;
for (i < size) {
var read = curBlock.opArrayGetElem(V3.arrayByteType, indexType, facts,
array, curBlock.opIntAdd(newGraph.intConst(i + offset), i_offset));
read = curBlock.opIntViewI0(Byte.TYPE, wt, read);
var shifted = if(i == 0, read, curBlock.addApplyF(wt.opShl(), [read, newGraph.intConst(8 * i)], Facts.O_SAFE_SHIFT));
result = curBlock.addApplyF(wt.opOr(), [result, shifted], Fact.O_PURE);
facts |= Fact.O_NO_NULL_CHECK;
}
return result;
}
def genArrayByteSetMultiple(i_old: SsaApplyOp, it: IntType, array: SsaInstr, i_offset: SsaInstr, offset: int, val: SsaInstr) {
// TODO: little-endian only for now
curBlock.at(i_old.source);
var size = it.packedByteSize();
var facts: Fact.set = Fact.O_NO_BOUNDS_CHECK;
var indexType = norm.config.RangeStartType;
for (i < size) {
var shifted = curBlock.addApplyF(it.opShr(), [val, newGraph.intConst(8 * i)], Facts.O_SAFE_SHIFT);
var b = curBlock.opIntViewI0(it, Byte.TYPE, shifted);
var write = curBlock.opArraySetElem(array.getType(), indexType, facts,
array, curBlock.opIntAdd(newGraph.intConst(i + offset), i_offset), b);
facts |= Fact.O_NO_NULL_CHECK;
}
}
def normDefault(i_old: SsaApplyOp, op: Operator) {
// normalize a general operator
var newOp = op;
Expand Down
Loading

0 comments on commit df20140

Please sign in to comment.