Set F_POINTED_AT during IrField construction

titzer · Nov 27, 2024 · 5a518bc · 5a518bc
1 parent 37ee6ff
commit 5a518bc
Show file tree

Hide file tree

Showing 7 changed files with 35 additions and 4 deletions.
diff --git a/aeneas/src/ir/VstIr.v3 b/aeneas/src/ir/VstIr.v3
@@ -75,6 +75,7 @@ class IrBuilder(ctype: Type, parent: IrClass) {
 	def addVstField(f: VstField, isVariant: bool) {
 		var ir = IrField.new(ctype, f.getType());
 		ir.source = f;
+		if (f.pointedAt) ir.setFact(Fact.F_POINTED_AT);
 		if (f.writability == Writability.READ_ONLY) ir.setFact(Fact.F_VALUE | Fact.O_FOLDABLE);
 		if (isVariant) ir.setFact(Fact.F_VALUE | Fact.O_FOLDABLE | Fact.O_PURE);
 		addIrField(ir);

diff --git a/aeneas/src/main/Version.v3 b/aeneas/src/main/Version.v3
@@ -3,6 +3,6 @@
 
 // Updated by VCS scripts. DO NOT EDIT.
 component Version {
-	def version: string = "III-7.1773";
+	def version: string = "III-7.1774";
 	var buildData: string;
 }
diff --git a/aeneas/src/ssa/VstSsaGen.v3 b/aeneas/src/ssa/VstSsaGen.v3
@@ -881,13 +881,11 @@ 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) => {

diff --git a/aeneas/src/vst/Verifier.v3 b/aeneas/src/vst/Verifier.v3
@@ -1560,12 +1560,14 @@ class TypeChecker(ERROR: ErrorGen, file: VstFile) extends VstVisitor<Type, Type>
 			x: VarExpr => match (x.varbind) {
 				ComponentField(member) => {
 					var receiver = member.receiver.getDeclaredType();
+					member.pointedAt = true;
 					expr.appbind = AppBinding.PtrAtComponentField(receiver, member, ptrType);
 					expr.args = TupleExpr.new(VstList.new(expr.args.range(), null));
 					expr.target = null;
 					return expr.exactType = ptrType;
 				}
 				ObjectField(receiver, member) => {
+					member.pointedAt = true;
 					expr.appbind = AppBinding.PtrAtObjectField(receiver, member, ptrType);
 					expr.args = TupleExpr.new(VstList.new(expr.args.range(), null));
 					expr.target = x.receiver;

diff --git a/aeneas/src/vst/Vst.v3 b/aeneas/src/vst/Vst.v3
@@ -396,10 +396,11 @@ class VstField extends VstMember {
 	def tref: TypeRef;
 	var init: Expr;
 	var paramInit: bool;
+	var synthetic: bool;
+	var pointedAt: bool;
 	var vtype: Type;
 	var initOrder: int;
 	var initEnv: MethodEnv;
-	var synthetic: bool;
 	var enumVals: Record;
 
 	new(isPrivate: bool, writability, name: Token, tref, init, repHints: List<VstRepHint>) super(isPrivate, name) {

diff --git a/test/pointer/Pointer_atField16.v3 b/test/pointer/Pointer_atField16.v3
@@ -0,0 +1,14 @@
+//@execute 0=22; -55=22
+var f: int;
+var p: Pointer;
+
+def setp() {
+	p = Pointer.atField(f);
+}
+
+def main(a: int) -> int {
+	setp();
+	f = a;
+	p.store<int>(11);
+	return f + f;
+}
diff --git a/test/pointer/Pointer_atField17.v3 b/test/pointer/Pointer_atField17.v3
@@ -0,0 +1,15 @@
+//@execute 0=11; -55=-44
+var f: int;
+var p: Pointer;
+
+def setp() {
+	p = Pointer.atField(f);
+}
+
+def main(a: int) -> int {
+	setp();
+	f = a;
+	var x = f;
+	p.store<int>(11);
+	return x + f;
+}