Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Refining and cleaning up Pointer.atField for unboxed fields, with more tests, etc. #342

Merged
merged 16 commits into from
Feb 10, 2025
Merged
Show file tree
Hide file tree
Changes from 13 commits
Commits
Show all changes
16 commits
Select commit Hold shift + click to select a range
61486a1
Small fix to the aeneas script to make it a little more robust
eliotmoss Nov 18, 2024
1c90622
Merge branch 'master' of github.com:eliotmoss/virgil
eliotmoss Nov 19, 2024
a5aae35
Merge branch 'master' of github.com:eliotmoss/virgil
eliotmoss Dec 3, 2024
a3cefa5
Support for poitners to unboxed variant fields (that are not in arrays)
eliotmoss Dec 3, 2024
5aff2a5
Refactor pointer-to-unboxed-field code not to use a VarBinding as par…
eliotmoss Dec 6, 2024
7ef7e65
Revise tests in a way that should fix wasm failures
eliotmoss Dec 7, 2024
1c00260
Remove ovverride of render method - other thigns depended on the orig…
eliotmoss Dec 9, 2024
ad92b89
Remove override of render method - other things depended on the origi…
eliotmoss Dec 9, 2024
6713ee1
Merge branch 'ptr_to_unboxed_field_for_PR' of github.com:eliotmoss/vi…
eliotmoss Dec 9, 2024
005ae90
This patch fixes a flaw that showed up when handling a pointer to and
eliotmoss Jan 28, 2025
3c155be
Follow Ben's suggested improvements
eliotmoss Jan 30, 2025
b868f65
Refined and cleaned up Pointer.atField to unboxed fields, tests and t…
eliotmoss Feb 5, 2025
0b29d90
Merge branch 'master' into ptr_to_unboxed_field_for_PR
eliotmoss Feb 5, 2025
2b9a5ed
Update pointerdAtTypeLegal to use a match on the type, simplify seman…
eliotmoss Feb 6, 2025
069c896
Need also to allow pointers to fields of array type (they're never un…
eliotmoss Feb 6, 2025
7d4ebc9
Adding a test that Pointer.atField on a field of array type is ok
eliotmoss Feb 6, 2025
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
53 changes: 45 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,42 @@ class ReachabilityAnalyzer(compilation: Compilation) {
getEquality(if(rf.fieldType == null, f.fieldType, rf.fieldType), null);
}
}
def getAndSetField(rf: RaField) {
def pointedAtTypeLegal(t: Type) -> bool {
if (PrimType.?(t) && !VoidType.?(t)) return true;
if (ClassType.?(t) && !ClassType.!(t).classDecl.isUnboxed()) return true;
if (PointerType.?(t)) return true;
// add other types here, e.g., Tuple (eventually), and fix error message in getPointerAtField
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 +500,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 +761,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
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;
}
2 changes: 1 addition & 1 deletion test/pointer/seman/Pointer_atFieldUnboxedBad00.v3
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
//@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 {
Expand Down
3 changes: 1 addition & 2 deletions test/pointer/seman/Pointer_atFieldUnboxedBad05.v3
Original file line number Diff line number Diff line change
Expand Up @@ -2,11 +2,10 @@
// 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);
}
}

Expand Down
26 changes: 26 additions & 0 deletions test/pointer/seman/Pointer_atFieldUnboxedBad11.v3
Original file line number Diff line number Diff line change
@@ -0,0 +1,26 @@
//@seman = TypeError @ 16:24
// tests possible issues related to unboxed field and parameterized types

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

class P { }
class Q extends P { }
class R<T> extends Q {
var x: T;
def y: int;
new(x, y) { }
}
class S extends R<B> {
def getPtr() -> Pointer {
return Pointer.atField(x);
}
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;
}
29 changes: 29 additions & 0 deletions test/pointer/seman/Pointer_atFieldUnboxedBad12.v3
Original file line number Diff line number Diff line change
@@ -0,0 +1,29 @@
//@seman=TypeError @ 15:24
// tests possible issues related to unboxed field and parameterized types

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

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

def main(n: int) -> int {
var r = R<A>.new(A(n), 15);
var p = r.getPtrx();
return p.load<int>();
}
35 changes: 35 additions & 0 deletions test/pointer/seman/Pointer_atFieldUnboxedBad13.v3
Original file line number Diff line number Diff line change
@@ -0,0 +1,35 @@
//@seman=TypeError @ 33:17
// tests possible issues related to unboxed field and parameterized types

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

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

def main(n: int) -> int {
var r = R<B>.new(B(A(n, n+1), u32.view(n+2)), n+3);
// keep all the fields around
var pi = Pointer.atField(r.x.a.i);
var pj = Pointer.atField(r.x.a.j);
var pb = Pointer.atField(r.x.b);
var py = Pointer.atField(r.y);
// case actually being tested
var p = Pointer.atField(r.x);
return p.load<int>() + pi.load<int>() + pj.load<int>() + pb.load<int>() + py.load<int>() - (4 * n + 6);
}
Loading