Skip to content

Commit

Permalink
Refining and cleaning up Pointer.atField for unboxed fields, with mor…
Browse files Browse the repository at this point in the history
…e tests, etc. (#342)
  • Loading branch information
eliotmoss authored Feb 10, 2025
1 parent 8ad1a24 commit f0dc9ce
Show file tree
Hide file tree
Showing 31 changed files with 468 additions and 88 deletions.
57 changes: 49 additions & 8 deletions aeneas/src/ir/Reachability.v3
Original file line number Diff line number Diff line change
Expand Up @@ -329,10 +329,10 @@ class ReachabilityAnalyzer(compilation: Compilation) {
CallClassMethod(method) => getMethod(op, opMethod(op, method, context));
CallClassVirtual(method) => getVirtual(opMethod(op, method, context));
CallVariantVirtual(method) => getVirtual(opMethod(op, method, context));
PtrAtObjectField(field) => if (op.useList != null) getAndSetField(makeField(op, field, context));
PtrAtComponentField(field) => if (op.useList != null) getAndSetField(makeField(op, field, context));
PtrAtUnboxedObjectField(specs) => if (op.useList != null) getAndSetUnboxedField(op, specs, context);
PtrAtUnboxedComponentField(specs) => if (op.useList != null) getAndSetUnboxedField(op, specs, context);
PtrAtObjectField(field) => if (op.useList != null) getPointerAtField(makeField(op, field, context), op, true);
PtrAtComponentField(field) => if (op.useList != null) getPointerAtField(makeField(op, field, context), op, true);
PtrAtUnboxedObjectField(specs) => if (op.useList != null) getPointerAtUnboxedField(op, specs, context);
PtrAtUnboxedComponentField(specs) => if (op.useList != null) getPointerAtUnboxedField(op, specs, context);
_ => ;
}
}
Expand Down Expand Up @@ -415,18 +415,46 @@ class ReachabilityAnalyzer(compilation: Compilation) {
getEquality(if(rf.fieldType == null, f.fieldType, rf.fieldType), null);
}
}
def getAndSetField(rf: RaField) {
def pointedAtTypeLegal(t: Type) -> bool {
match (t) {
x: VoidType => return false; // must come before PrimType
x: PrimType => return true;
x: ClassType => return !x.classDecl.isUnboxed();
x: PointerType => return true;
x: ArrayType => return true;
// x: TupleType => return true; // add when handled
}
return false;
}
def getPointerAtField(rf: RaField, op: SsaApplyOp, checkType: bool) {
if (checkType) {
var ft = rf.fieldType;
if (ft == null) ft = rf.orig.fieldType;
if (!pointedAtTypeLegal(ft)) {
var ERROR = compilation.prog.ERROR;
var msg = Strings.format1("field must be of non-void primitive type or boxed class type (type is %q)", ft.render);
ERROR.addError(op.source.range, null, "TypeError", msg);
}
}
// Treat the field as both read and written, with unknown values
getField(rf);
rf.raFacts |= RaFact.RF_WRITTEN;
var none: Fact.set;
rf.writeFacts = none;
rf.setFact(RaFact.RF_VAL_MANY);
}
def getAndSetUnboxedField(op: SsaApplyOp, specs: List<IrSpec>, context: IrSpec) {
def getPointerAtUnboxedField(op: SsaApplyOp, specs: List<IrSpec>, context: IrSpec) {
var prevType: Type;
prevType = if(specs != null, specs.head.receiver);
for (l = specs; l != null; l = l.tail) {
var spec = l.head;
var rf = makeField(op, spec.asField(), context);
getAndSetField(rf);
var fld = spec.asField();
var rf = makeField3(prevType, fld, context);
prevType = rf.fieldType;
if (prevType == null) prevType = rf.orig.fieldType;
// check only the last type in the range, since the intermediates
// are not pointed at
getPointerAtField(rf, op, l.tail == null);
}
}
def setField(op: SsaApplyOp, rf: RaField) {
Expand Down Expand Up @@ -476,6 +504,16 @@ class ReachabilityAnalyzer(compilation: Compilation) {
// make a polymorphic field
return makePolyField(raType, f);
}
def makeField3(rcvrType: Type, f: IrField, context: IrSpec) -> RaField {
var rf = f.raField;
if (rf != null) return rf;
// try to make a simple field first
var receiver = f.receiver;
if (!receiver.open()) return makeSimpleField(makeClass(receiver), f);
// get polymorphic receiver type from operator
receiver = mono(rcvrType, context);
return makePolyField(makeClass(receiver), f);
}
def makePolyField(raType: RaClass, f: IrField) -> RaField {
var rf = raType.fields[f.index];
if (rf == null) {
Expand Down Expand Up @@ -727,6 +765,9 @@ class RaField(receiver: Type, orig: IrField, fieldType: Type) extends RaItem {
var rc = ra.getClass(receiver);
return normOf(rc.liveFields);
}
def getClosedType() -> Type {
return if(fieldType == null, orig.fieldType, fieldType);
}
}
// Information about a method, including any specialization, whether it is reusable
// across normalization, etc.
Expand Down
52 changes: 34 additions & 18 deletions aeneas/src/ir/SsaNormalizer.v3
Original file line number Diff line number Diff line change
Expand Up @@ -534,13 +534,27 @@ class SsaRaNormalizer extends SsaRebuilder {
var receiver = genRef1(i_old.inputs[0]);
var raField = extractFieldRef(i_old, field);
var nf = raField.liveFields(norm.ra);
if (nf.length == 0) {
// can happen because of user's code, so not a compiler failure;
// checked in Reachability
var result = SsaInstr.!(newGraph.intConst(0));
return map1(i_old, result);
}
var ft = nf[0].asField().fieldType;
var i_new = curBlock.addApply(curBlock.source,
V3Op.newPtrAtObjectField(nf[0], i_old.op.sig.returnType()), [receiver]);
map1(i_old, i_new);
}
PtrAtComponentField(field) => {
var raField = extractFieldRef(i_old, field);
var nf = raField.liveFields(norm.ra);
if (nf.length == 0) {
// can happen because of user's code, so not a compiler failure;
// checked in Reachability
var result = SsaInstr.!(newGraph.intConst(0));
return map1(i_old, result);
}
var ft = nf[0].asField().fieldType;
var i_new = curBlock.addApply(curBlock.source,
V3Op.newPtrAtComponentField(nf[0], i_old.op.sig.returnType()), Ssa.NO_INSTRS);
map1(i_old, i_new);
Expand Down Expand Up @@ -1336,31 +1350,33 @@ class SsaRaNormalizer extends SsaRebuilder {
var rc = norm.ra.getClass(raField.receiver);
var nf = raField.normOf(rc.liveFields);
normType(raField.receiver); // XXX: normType() side-effect of flattening
var prevType = raField.getClosedType();
// now, iterate winnowing down the fields
for (elt = specs.tail; elt != null && nf.length != 0; elt = elt.tail) {
var spec = elt.head;
var rcvr = spec.asField().receiver;
var rc = norm.ra.getClass(rcvr);
raField = norm.ra.makeField2(rc, spec.asField());
var ctxt = if (specSet != null, specSet.first(), context.spec);
raField = norm.ra.makeField3(prevType, spec.asField(), ctxt);
prevType = raField.getClosedType();
nf = raField.normOf(nf);
}
// now should have a single field that we can do Pointer.atField
if (nf.length > 0) {
var op_out: Operator;
match (boxKind) {
OBJECT =>
op_out = V3Op.newPtrAtObjectField(nf[0], i_old.op.sig.returnType());
COMPONENT =>
op_out = V3Op.newPtrAtComponentField(nf[0], i_old.op.sig.returnType());
}
var new_inputs = if(ai_new.length == 0, Ssa.NO_INSTRS, [ai_new[0]]);
var i_new = curBlock.addApply(curBlock.source, op_out, new_inputs);
return map1(i_old, i_new);
} else {
// Not sure what to do if no fields remain ...
if (nf.length == 0) {
// can happen because of user's code, so not a compiler failure;
// checked in Reachability
var result = SsaInstr.!(newGraph.intConst(0));
return map1(i_old, result);
}
var result = SsaInstr.!(newGraph.intConst(0));
return map1(i_old, result);
var ft = nf[0].asField().fieldType;
var op_out: Operator;
match (boxKind) {
OBJECT =>
op_out = V3Op.newPtrAtObjectField(nf[0], i_old.op.sig.returnType());
COMPONENT =>
op_out = V3Op.newPtrAtComponentField(nf[0], i_old.op.sig.returnType());
}
var new_inputs = if(ai_new.length == 0, Ssa.NO_INSTRS, [ai_new[0]]);
var i_new = curBlock.addApply(curBlock.source, op_out, new_inputs);
return map1(i_old, i_new);
}
def normClassSetField(i_old: SsaApplyOp, field: IrField, op: Operator, init: bool) {
// XXX: propagate O_NO_NULL_CHECK
Expand Down
12 changes: 12 additions & 0 deletions test/pointer/Pointer_atField18.v3
Original file line number Diff line number Diff line change
@@ -0,0 +1,12 @@
//@execute 11=11; -55=-55
component C {
var a: Array<int>;
}

def main(n: int) -> int {
C.a = [14];
var p = Pointer.atField(C.a);
var aa: Array<int> = [n];
p.cmpswp(C.a, aa);
return C.a[0];
}
5 changes: 2 additions & 3 deletions test/pointer/Pointer_atUnboxedField24.v3
Original file line number Diff line number Diff line change
Expand Up @@ -13,14 +13,13 @@ class R<T> extends Q {
}
class S extends R<B> {
def getPtr() -> Pointer {
return Pointer.atField(x);
return Pointer.atField(x.a.i);
}
new(x: B, y: int) super(x, y) { }
}

def main(n: int) -> int {
var s = S.new(B(A(n), 17), 5);
var p = s.getPtr();
// make sure field is not optimized away - though that should be another test
return p.load<int>() + s.x.a.i - n;
return p.load<int>();
}
19 changes: 8 additions & 11 deletions test/pointer/Pointer_atUnboxedField25.v3
Original file line number Diff line number Diff line change
@@ -1,25 +1,22 @@
//@execute 0=0; 6=6
//@execute 0=0; 12=12
// tests possible issues related to unboxed field and parameterized types

type A(i: int) #unboxed { }
type B(a: A, b: u32) #unboxed { }
type A<T>(i: T) #unboxed { }
type B<T>(a: A<T>, b: u32) #unboxed { }

class P { }
class Q extends P { }
class R<T> extends Q {
var x: T;
var x: B<T>;
def y: int;
new(x, y) { }
}
class S extends R<B> {
def getPtr() -> Pointer {
def getPtrx() -> Pointer {
// legality depends on what T is
return Pointer.atField(x.a.i);
}
new(x: B, y: int) super(x, y) { }
}

def main(n: int) -> int {
var s = S.new(B(A(n), 17), 5);
var p = s.getPtr();
var r = R<int>.new(B<int>(A<int>(n), 13), 15);
var p = r.getPtrx();
return p.load<int>();
}
17 changes: 17 additions & 0 deletions test/pointer/Pointer_atUnboxedField26.v3
Original file line number Diff line number Diff line change
@@ -0,0 +1,17 @@
//@execute 6=6; 10=10
// tests possible issues related to unboxed field and parameterized types

class C #unboxed {
var x: int;
new(x) { }
}
class D {
var c: C;
new(x: int) { c = C.new(x); }
}

def main(n: int) -> int {
var d = D.new(n);
var p = Pointer.atField(d.c.x);
return p.load<int>() + d.c.x - n;
}
17 changes: 17 additions & 0 deletions test/pointer/Pointer_atUnboxedField27.v3
Original file line number Diff line number Diff line change
@@ -0,0 +1,17 @@
//@execute 6=6; 10=10
// tests possible issues related to unboxed field and parameterized types

class C #unboxed {
var x: int;
new(x) { }
}

component CC {
var c: C;
}

def main(n: int) -> int {
CC.c = C.new(n);
var p = Pointer.atField(CC.c.x);
return p.load<int>() + CC.c.x - n;
}
6 changes: 2 additions & 4 deletions test/pointer/seman/Pointer_atFieldUnboxedBad00.v3
Original file line number Diff line number Diff line change
@@ -1,10 +1,8 @@
//@seman = TypeError @ 7:33
// Disallow pointer to *boxed* field of a global variable
// Disallow pointer to *boxed* field of a local variable
type V(x: int);

def main() -> int {
component C {
var v = V(13);
var p = Pointer.atField(v.x);
p.store<int>(17);
return v.x;
}
9 changes: 2 additions & 7 deletions test/pointer/seman/Pointer_atFieldUnboxedBad01.v3
Original file line number Diff line number Diff line change
@@ -1,13 +1,8 @@
//@seman = TypeError @ 10:33
//@seman = TypeError @ 7:33
// Disallow pointer to *boxed* field of a component

type V(x: int);
component C {
var v = V(13);
}

def main() -> int {
var p = Pointer.atField(C.v.x);
p.store<int>(17);
return C.v.x;
var p = Pointer.atField(v.x);
}
7 changes: 2 additions & 5 deletions test/pointer/seman/Pointer_atFieldUnboxedBad02.v3
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
//@seman = TypeError @ 14:33
//@seman = TypeError @ 13:33
// Disallow pointer to *boxed* field of a class

type V(x: int);
Expand All @@ -8,10 +8,7 @@ class C {
v = V(i);
}
}

def main() -> int {
component Comp {
var c = C.new(13);
var p = Pointer.atField(c.v.x);
p.store<int>(17);
return c.v.x;
}
4 changes: 1 addition & 3 deletions test/pointer/seman/Pointer_atFieldUnboxedBad03.v3
Original file line number Diff line number Diff line change
Expand Up @@ -2,9 +2,7 @@
// Disallow pointer to *packed* field of a local variable
type V(x: u4, y: u4) #packing 0b_xxxxyyyy;

def main() -> int {
component C {
var v = V(13, 7);
var p = Pointer.atField(v.x);
p.store<int>(11);
return v.x;
}
9 changes: 2 additions & 7 deletions test/pointer/seman/Pointer_atFieldUnboxedBad04.v3
Original file line number Diff line number Diff line change
@@ -1,13 +1,8 @@
//@seman = TypeError @ 10:33
//@seman = TypeError @ 7:33
// Disallow pointer to *packed* field of a global variable
type V(x: u4, y: u4) #packing 0b_xxxxyyyy;

component C {
var v = V(13, 7);
}

def main() -> int {
var p = Pointer.atField(C.v.x);
p.store<int>(17);
return C.v.x;
var p = Pointer.atField(v.x);
}
9 changes: 3 additions & 6 deletions test/pointer/seman/Pointer_atFieldUnboxedBad05.v3
Original file line number Diff line number Diff line change
@@ -1,18 +1,15 @@
//@seman = TypeError @ 15:33
//@seman = TypeError @ 14:33
// Disallow pointer to *packed* field of a local variable
type V(x: u4, y: u4) #packing 0b_xxxxyyyy;

type V(x: int);
class C {
var v: V;
new(i: int) {
v = V(i, 3);
v = V(u4.view(i), 3);
}
}

def main() -> int {
component Comp {
var c = C.new(13);
var p = Pointer.atField(c.v.x);
p.store<int>(17);
return c.v.x;
}
4 changes: 1 addition & 3 deletions test/pointer/seman/Pointer_atFieldUnboxedBad06.v3
Original file line number Diff line number Diff line change
Expand Up @@ -2,8 +2,6 @@
// Disallow pointer to global tuple
var tup = (1, 13);

def main() -> int {
component C {
var p = Pointer.atField(tup.1);
p.store<int>(17);
return tup.1;
}
9 changes: 2 additions & 7 deletions test/pointer/seman/Pointer_atFieldUnboxedBad07.v3
Original file line number Diff line number Diff line change
@@ -1,11 +1,6 @@
//@seman = TypeError @ 8:33
//@seman = TypeError @ 5:33
// Disallow pointer to component tuple
component C {
var tup = (1, 13);
}

def main() -> int {
var p = Pointer.atField(C.tup.1);
p.store<int>(17);
return C.tup.1;
var p = Pointer.atField(tup.1);
}
Loading

0 comments on commit f0dc9ce

Please sign in to comment.