Skip to content

Commit

Permalink
Add F_POINTED_AT fact for IrField (#298)
Browse files Browse the repository at this point in the history
  • Loading branch information
eliotmoss authored Nov 19, 2024
1 parent d8d95a1 commit ed7f584
Show file tree
Hide file tree
Showing 5 changed files with 26 additions and 3 deletions.
3 changes: 2 additions & 1 deletion aeneas/src/core/Opcode.v3
Original file line number Diff line number Diff line change
Expand Up @@ -182,7 +182,8 @@ component Opcodes {
var F = Fact.O_FOLDABLE;
var P = Fact.O_PURE | Fact.O_FOLDABLE; // pure => foldable
var C = Fact.O_COMMUTATIVE;
var A = Fact.O_ASSOCIATIVE;
// var A = Fact.O_ASSOCIATIVE; // not exploited
var A = Facts.NONE; // for now, since needed the bit
var NZ = Fact.V_NON_ZERO;
var NNEG = Fact.V_NON_NEGATIVE;
var NNC = Fact.O_NO_NULL_CHECK;
Expand Down
6 changes: 5 additions & 1 deletion aeneas/src/ir/Facts.v3
Original file line number Diff line number Diff line change
Expand Up @@ -6,6 +6,7 @@ enum Fact {
// facts for fields
F_VALUE, // field is read-only
F_NORM, // the field is an element of a normalized field
F_POINTED_AT, // subject of a Pointer.atField
// facts for methods
M_EQUALS, // method is an equality comparator
M_OVERRIDDEN, // method has been overridden in a subclass
Expand All @@ -29,7 +30,10 @@ enum Fact {
O_PURE, // no side-effects + deterministic
O_FOLDABLE, // can be constant folded
O_COMMUTATIVE, // f(x, y) == f(y, x)
O_ASSOCIATIVE, // f(f(x, y), z) == f(x, f(y, z))
// associative is not exploited at present, and we needed the bit
// in order to add F_POINTED_AT (until compiler fixed to use u64
// for the enum set)
// O_ASSOCIATIVE, // f(f(x, y), z) == f(x, f(y, z))
O_NO_SHIFT_CHECK, // 31 >= y >= 0
O_NO_NULL_CHECK, // x != null, x != NaN for floats
O_NO_BOUNDS_CHECK, // no bounds check required
Expand Down
3 changes: 2 additions & 1 deletion aeneas/src/ir/Normalization.v3
Original file line number Diff line number Diff line change
Expand Up @@ -329,7 +329,8 @@ class ReachabilityNormalizer(config: NormalizerConfig, ra: ReachabilityAnalyzer)
// add normalized field(s) to the vector
var tn = rf.typeNorm;
var facts = if(tn.size > 1, Fact.F_NORM, Facts.NONE);
if (!rf.raFacts.RF_WRITTEN) facts |= (Fact.F_VALUE | Fact.O_FOLDABLE);
if (!rf.raFacts.RF_WRITTEN && !rf.orig.facts.F_POINTED_AT) facts |= (Fact.F_VALUE | Fact.O_FOLDABLE);
if (rf.orig.facts.F_POINTED_AT) facts |= Fact.F_POINTED_AT;
for (i < tn.size) {
var ft = if(tn.sub == null, tn.newType, tn.sub[i]);
var nf = IrField.new(rc.oldType, ft);
Expand Down
13 changes: 13 additions & 0 deletions aeneas/src/ssa/SsaOptimizer.v3
Original file line number Diff line number Diff line change
Expand Up @@ -1955,6 +1955,10 @@ class SsaLoadOptimizer(context: SsaContext) {
}
ClassSetField(field) => return store(apply.input0(), field, apply, apply.input1());
ComponentSetField(field) => return store(null, field, apply, apply.input1());
PtrStore => {
pure.killPointedAt();
impure.killPointedAt();
}
Init,
CallMethod,
CallClassMethod,
Expand Down Expand Up @@ -2022,4 +2026,13 @@ class SsaLoadedFields {
}
length = i;
}
def killPointedAt() {
var i = 0;
for (j < length) {
var t = array[j];
if ((!t.1.facts.F_POINTED_AT) && i != j)
array[i++] = t;
}
length = i;
}
}
4 changes: 4 additions & 0 deletions aeneas/src/ssa/VstSsaGen.v3
Original file line number Diff line number Diff line change
Expand Up @@ -880,10 +880,14 @@ class VstSsaGen extends VstVisitor<VstSsaEnv, SsaInstr> {
}
PtrAtComponentField(receiver, field, ptrType) => {
var spec = specOf(receiver, field, null);
var irFld = spec.asField();
irFld.facts |= Fact.F_POINTED_AT;
return env.addApply(env.source, V3Op.newPtrAtComponentField(spec, ptrType), Ssa.NO_INSTRS);
}
PtrAtObjectField(receiver, field, ptrType) => {
var spec = specOf(receiver, field, null);
var irFld = spec.asField();
irFld.facts |= Fact.F_POINTED_AT;
return env.addApply(env.source, V3Op.newPtrAtObjectField(spec, ptrType), [target]);
}
PtrAtRefLayoutField(receiver, field, ptrType) => {
Expand Down

0 comments on commit ed7f584

Please sign in to comment.