Fix nullchecks and killing of pointed at

titzer · Nov 24, 2024 · a1b1dad · a1b1dad
1 parent 4670cab
commit a1b1dad
Show file tree

Hide file tree

Showing 10 changed files with 74 additions and 16 deletions.
diff --git a/aeneas/src/ir/Ir.v3 b/aeneas/src/ir/Ir.v3
@@ -5,7 +5,7 @@
 class IrItem {
 	def uid: int = UID.next++;
 	var facts: Fact.set;
-	def setFact(set: Fact.set) { facts = facts | set; }
+	def setFact(set: Fact.set) -> this { facts = facts | set; }
 }
 // boxing modes for variants
 enum Boxing {

diff --git a/aeneas/src/ir/Normalization.v3 b/aeneas/src/ir/Normalization.v3
@@ -314,20 +314,23 @@ class ReachabilityNormalizer(config: NormalizerConfig, ra: ReachabilityAnalyzer)
 			if (rf == null) continue;
 			if (rc.inheritedField(rf)) continue;
 			if (rf.isConst()) continue;
-			if (rf.typeNorm == null && rf.fieldType != null) rf.typeNorm = norm(rf.fieldType);
+			var tn = rf.typeNorm;
+			if (tn == null && rf.fieldType != null) rf.typeNorm = tn = norm(rf.fieldType);
 			if (!rf.raFacts.RF_READ) continue;
 			if (receiver_array == null) receiver_array = [rc.oldType];
 			// add normalized field(s)
-			var startIndex = fields.length;
+			var startIndex = fields.length, facts = Facts.NONE;
+
+			if (tn != null && tn.size > 1) facts |= Fact.F_NORM;
+			if (rf.orig.facts.F_POINTED_AT) facts |= Fact.F_POINTED_AT;
+			else if (!rf.raFacts.RF_WRITTEN) facts |= (Fact.F_VALUE | Fact.O_FOLDABLE);
+
 			if (rf.fieldType == null) {
 				// add single monomorphic field to the vector
+				rf.orig.setFact(facts);
 				fields.put(IrSpec.new(rc.oldType, receiver_array, rf.orig));
 			} else {
 				// add normalized field(s) to the vector
-				var tn = rf.typeNorm;
-				var facts = if(tn.size > 1, Fact.F_NORM, Facts.NONE);
-				if (rf.orig.facts.F_POINTED_AT) facts |= Fact.F_POINTED_AT;
-				else if (!rf.raFacts.RF_WRITTEN) facts |= (Fact.F_VALUE | Fact.O_FOLDABLE);
 				for (i < tn.size) {
 					var ft = if(tn.sub == null, tn.newType, tn.sub[i]);
 					var nf = IrField.new(rc.oldType, ft);

diff --git a/aeneas/src/ssa/SsaOptimizer.v3 b/aeneas/src/ssa/SsaOptimizer.v3
@@ -329,7 +329,7 @@ class SsaBlockState {
 		var v = impure_loads, i = 0;
 		for (j < v.length) {
 			var t = v[i];
-			if (t.1.facts.F_POINTED_AT) {
+			if (!t.1.facts.F_POINTED_AT) {
 				if (i != j) v[i] = t;
 				i++;
 			}
@@ -1039,18 +1039,24 @@ class SsaInstrReducer(context: SsaContext) extends SsaInstrMatcher {
 				if (optimize_loads) state.killArrayElems();
 			}
 			PtrCmpSwp => {
+				nullcheck(i);
 				state.kill();
 			}
 			PtrLoad => {
+				var ptr = nullcheck(i);
 				// XXX: use Fact.O_FOLDABLE to indicate a load of an immutable value
-				if (optimize_loads) return state.load(i.input0(), PTR_FIELD, i);
+				if (optimize_loads) {
+					var valueType = i.op.typeArgs[1]; // XXX, tricky: ptr.load<void> is used to induce a HW nullcheck
+					if (valueType != Void.TYPE) return state.load(ptr, PTR_FIELD, i);
+				}
 			}
 			PtrStore => {
+				var ptr = nullcheck(i);
+				state.killArrayElems();
+				state.killPointedAt();
 				// XXX: use a fact to indicate an initializing store that cannot kill previous loads
 				if (optimize_loads) {
-					state.killArrayElems();
-					state.killPointedAt();
-					state.store(i.input0(), PTR_FIELD, i, i.input1());
+					state.store(ptr, PTR_FIELD, i, i.input1());
 				}
 			}
 			_ => ;

diff --git a/test/core/field39.v3 b/test/core/field39.v3
@@ -0,0 +1,15 @@
+//@execute 0=4; 100=4
+class C {
+	def m() -> int { return [2].length; }
+}
+class D extends C {
+	def m() -> int { return [2, 3].length; }
+}
+def c = C.new();
+def d = D.new();
+def main(x: int) -> int {
+	return sum(c, d, (c, [0]).0);
+}
+def sum(x: C, y: C, z: C) -> int {
+	return x.m() + y.m() + z.m();
+}
diff --git a/test/core/field40.v3 b/test/core/field40.v3
@@ -0,0 +1,16 @@
+//@execute 0=4; 100=4
+class C {
+	def m() -> int { return [2].length; }
+}
+class D extends C {
+	def m() -> int { return [2, 3].length; }
+}
+def c = C.new();
+def d = D.new();
+def a = [0];
+def main(x: int) -> int {
+	return sum(c, d, (c, a).0);
+}
+def sum(x: C, y: C, z: C) -> int {
+	return x.m() + y.m() + z.m();
+}
diff --git a/test/core/field41.v3 b/test/core/field41.v3
@@ -0,0 +1,18 @@
+//@execute 0=4; 100=4
+def c = C.new();
+def d = D.new();
+def a = [0];
+def one = [2];
+def two = [2, 3];
+class C {
+	def m() -> int { return one.length; }
+}
+class D extends C {
+	def m() -> int { return two.length; }
+}
+def main(x: int) -> int {
+	return sum(c, d, (c, a).0);
+}
+def sum(x: C, y: C, z: C) -> int {
+	return x.m() + y.m() + z.m();
+}
diff --git a/test/pointer/opt_load02.v3 b/test/pointer/opt_load02.v3
@@ -1,4 +1,4 @@
-//@execute 0=0; 4=-8; -999=-1998
+//@execute 0=0; 4=-8; -999=1998
 var storage = Array<int>.new(1);
 
 def main(a: int) -> int {

diff --git a/test/pointer/opt_load03.v3 b/test/pointer/opt_load03.v3
@@ -1,4 +1,4 @@
-//@execute 0=0; 4=-8; -999=-1998
+//@execute 0=0; 4=-8; -997=1994
 var storage = Array<int>.new(1);
 
 def main(a: int) -> int {

diff --git a/test/pointer/opt_load04.v3 b/test/pointer/opt_load04.v3
@@ -1,4 +1,4 @@
-//@execute 0=0; 4=-8; -999=-1998
+//@execute 0=0; 4=-8; -998=1996
 var storage = Array<int>.new(1);
 
 def set(a: int) {

diff --git a/test/pointer/opt_load05.v3 b/test/pointer/opt_load05.v3
@@ -1,4 +1,4 @@
-//@execute 0=0; 4=-8; -999=-1998
+//@execute 0=0; 4=-8; -996=1992
 var storage = Array<int>.new(1);
 def c = C.new(storage);