Proper memory access typing & updated compilation (#502)

* Updated memory events to have the correct access type (we defaulted to the arch type). Updated the compilation schemes to never explicitly use the arch type when generating code. * Added automatic extension when encoding equality of BVs of different sizes. * Changed LKMMLock/Unlock to use i32
hernanponcedeleon · Aug 20, 2023 · 30ade2b · 30ade2b
1 parent 859a3f9
commit 30ade2b
Show file tree

Hide file tree

Showing 22 changed files with 58 additions and 52 deletions.
diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/EncodingContext.java b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/EncodingContext.java
@@ -198,6 +198,10 @@ public BooleanFormula dependency(Event first, Event second) {
     }
 
     public BooleanFormula equal(Formula left, Formula right) {
+        //FIXME: We should avoid the automatic conversion, or standardize what conversion we expect.
+        // For example, when encoding rf(w, r), we always want to convert the store value type to the read value type
+        // for otherwise, we might get an under-constrained value for val(r) (e.g., its upper bits might be unconstrained,
+        // if we truncate it to smaller size of the store value).
         if (left instanceof IntegerFormula l) {
             IntegerFormulaManager integerFormulaManager = formulaManager.getIntegerFormulaManager();
             return integerFormulaManager.equal(l, toInteger(right));
@@ -236,15 +240,17 @@ private IntegerFormula toInteger(Formula formula) {
             BitvectorFormulaManager bitvectorFormulaManager = formulaManager.getBitvectorFormulaManager();
             return bitvectorFormulaManager.toIntegerFormula(f, false);
         }
-        throw new UnsupportedOperationException(String.format("Unkown type for toInteger(%s).", formula));
+        throw new UnsupportedOperationException(String.format("Unknown type for toInteger(%s).", formula));
     }
 
     private BitvectorFormula toBitvector(Formula formula, int length) {
         BitvectorFormulaManager bitvectorFormulaManager = formulaManager.getBitvectorFormulaManager();
         if (formula instanceof BitvectorFormula f) {
             int formulaLength = bitvectorFormulaManager.getLength(f);
-            // Signedness may be wrong here:
-            return formulaLength >= length ? f : bitvectorFormulaManager.extend(f, length - formulaLength, false);
+            // FIXME: Signedness may be wrong here.
+            return formulaLength >= length ?
+                    bitvectorFormulaManager.extract(f, length - 1, 0)
+                    : bitvectorFormulaManager.extend(f, length - formulaLength, false);
         }
         if (formula instanceof BooleanFormula f) {
             BitvectorFormula zero = bitvectorFormulaManager.makeBitvector(length, 0);

diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/common/LoadBase.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/common/LoadBase.java
@@ -13,7 +13,7 @@ public abstract class LoadBase extends SingleAccessMemoryEvent implements RegWri
     protected Register resultRegister;
 
     public LoadBase(Register register, Expression address, String mo) {
-        super(address, mo);
+        super(address, register.getType(), mo);
         this.resultRegister = register;
         addTags(Tag.READ);
     }

diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/common/RMWCmpXchgBase.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/common/RMWCmpXchgBase.java
@@ -21,7 +21,7 @@ public abstract class RMWCmpXchgBase extends SingleAccessMemoryEvent implements
 
     protected RMWCmpXchgBase(Register register, Expression address, Expression expectedValue, Expression storeValue,
                              boolean isStrong, String mo) {
-        super(address, mo);
+        super(address, register.getType(), mo);
         this.resultRegister = register;
         this.expectedValue = expectedValue;
         this.storeValue = storeValue;

diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/common/RMWOpBase.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/common/RMWOpBase.java
@@ -20,7 +20,7 @@ public abstract class RMWOpBase extends SingleAccessMemoryEvent {
     protected Expression operand;
 
     protected RMWOpBase(Expression address, IOpBin operator, Expression operand, String mo) {
-        super(address, mo);
+        super(address, operand.getType(), mo);
         this.operator = operator;
         this.operand = operand;
         addTags(READ, WRITE, RMW);

diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/common/RMWXchgBase.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/common/RMWXchgBase.java
@@ -17,7 +17,7 @@ public abstract class RMWXchgBase extends SingleAccessMemoryEvent implements Reg
     protected Expression storeValue;
 
     protected RMWXchgBase(Register register, Expression address, Expression value, String mo) {
-        super(address, mo);
+        super(address, register.getType(), mo);
         this.resultRegister = register;
         this.storeValue = value;
         addTags(READ, WRITE, RMW);

diff --git a/...agnan/src/main/java/com/dat3m/dartagnan/program/event/common/SingleAccessMemoryEvent.java b/...agnan/src/main/java/com/dat3m/dartagnan/program/event/common/SingleAccessMemoryEvent.java
@@ -3,7 +3,6 @@
 import com.dat3m.dartagnan.expression.Expression;
 import com.dat3m.dartagnan.expression.processing.ExpressionVisitor;
 import com.dat3m.dartagnan.expression.type.Type;
-import com.dat3m.dartagnan.expression.type.TypeFactory;
 import com.dat3m.dartagnan.program.event.MemoryAccess;
 import com.dat3m.dartagnan.program.event.core.AbstractEvent;
 import com.dat3m.dartagnan.program.event.core.MemoryEvent;
@@ -31,12 +30,11 @@ public abstract class SingleAccessMemoryEvent extends AbstractEvent implements M
     protected String mo;
 
     // The empty string means no memory order 
-    public SingleAccessMemoryEvent(Expression address, String mo) {
+    public SingleAccessMemoryEvent(Expression address, Type accessType, String mo) {
         Preconditions.checkNotNull(mo, "The memory ordering cannot be null");
         this.address = address;
         this.mo = mo;
-        // TODO: Add proper typing.
-        this.accessType = TypeFactory.getInstance().getArchType();
+        this.accessType = accessType;
         addTags(VISIBLE, MEMORY);
         if (!mo.isEmpty()) {
             addTags(mo);

diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/common/StoreBase.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/common/StoreBase.java
@@ -14,7 +14,7 @@ public abstract class StoreBase extends SingleAccessMemoryEvent {
     protected Expression value;
 
     public StoreBase(Expression address, Expression value, String mo) {
-        super(address, mo);
+        super(address, value.getType(), mo);
         this.value = value;
         addTags(Tag.WRITE);
     }

diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/AbstractMemoryCoreEvent.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/AbstractMemoryCoreEvent.java
@@ -3,7 +3,6 @@
 import com.dat3m.dartagnan.expression.Expression;
 import com.dat3m.dartagnan.expression.processing.ExpressionVisitor;
 import com.dat3m.dartagnan.expression.type.Type;
-import com.dat3m.dartagnan.expression.type.TypeFactory;
 import com.dat3m.dartagnan.program.event.common.NoInterface;
 import com.google.common.base.Preconditions;
 
@@ -19,9 +18,9 @@ public abstract class AbstractMemoryCoreEvent extends AbstractEvent implements M
     protected Expression address;
     protected Type accessType;
 
-    public AbstractMemoryCoreEvent(Expression address) {
+    public AbstractMemoryCoreEvent(Expression address, Type accessType) {
         this.address = Preconditions.checkNotNull(address);
-        this.accessType = TypeFactory.getInstance().getArchType(); // TODO: Add proper typing
+        this.accessType = accessType;
         addTags(VISIBLE, MEMORY);
     }
 

diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/GenericMemoryEvent.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/GenericMemoryEvent.java
@@ -1,6 +1,7 @@
 package com.dat3m.dartagnan.program.event.core;
 
 import com.dat3m.dartagnan.expression.Expression;
+import com.dat3m.dartagnan.expression.type.TypeFactory;
 import com.dat3m.dartagnan.program.event.MemoryAccess;
 
 import java.util.List;
@@ -16,7 +17,7 @@ public class GenericMemoryEvent extends AbstractMemoryCoreEvent implements Memor
     private final String displayName;
 
     public GenericMemoryEvent(Expression address, String displayName) {
-        super(address);
+        super(address, TypeFactory.getInstance().getArchType()); // TODO: Maybe a void type would be fine here
         this.displayName = displayName;
     }
 

diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/Load.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/Load.java
@@ -15,7 +15,7 @@ public class Load extends AbstractMemoryCoreEvent implements RegWriter {
     protected Register resultRegister;
 
     public Load(Register register, Expression address) {
-        super(address);
+        super(address, register.getType());
         this.resultRegister = register;
         addTags(Tag.READ);
     }

diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/Store.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/Store.java
@@ -16,7 +16,7 @@ public class Store extends AbstractMemoryCoreEvent {
     protected Expression value;
 
     public Store(Expression address, Expression value) {
-        super(address);
+        super(address, value.getType());
         this.value = value;
         addTags(Tag.WRITE);
     }

diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/catomic/AtomicCmpXchg.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/catomic/AtomicCmpXchg.java
@@ -27,7 +27,7 @@ public class AtomicCmpXchg extends SingleAccessMemoryEvent implements RegWriter
     private boolean isStrong;
 
     public AtomicCmpXchg(Register register, Expression address, Expression expectedAddr, Expression value, String mo, boolean isStrong) {
-        super(address, mo);
+        super(address, register.getType(), mo);
         Preconditions.checkArgument(!mo.isEmpty(), "Atomic events cannot have empty memory order");
         this.resultRegister = register;
         this.expectedAddr = expectedAddr;

diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/linux/LKMMAddUnless.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/linux/LKMMAddUnless.java
@@ -20,7 +20,7 @@ public class LKMMAddUnless extends SingleAccessMemoryEvent implements RegWriter
     private Expression cmp;
 
     public LKMMAddUnless(Register register, Expression address, Expression operand, Expression cmp) {
-        super(address, Tag.Linux.MO_MB);
+        super(address, register.getType(), Tag.Linux.MO_MB);
         this.resultRegister = register;
         this.operand = operand;
         this.cmp = cmp;
@@ -79,8 +79,8 @@ public LKMMAddUnless getCopy(){
 
     @Override
     public <T> T accept(EventVisitor<T> visitor) {
-		return visitor.visitLKMMAddUnless(this);
-	}
+        return visitor.visitLKMMAddUnless(this);
+    }
 
     @Override
     public MemoryAccess getMemoryAccess() {

diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/linux/LKMMLock.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/linux/LKMMLock.java
@@ -1,6 +1,7 @@
 package com.dat3m.dartagnan.program.event.lang.linux;
 
 import com.dat3m.dartagnan.expression.Expression;
+import com.dat3m.dartagnan.expression.type.TypeFactory;
 import com.dat3m.dartagnan.program.event.MemoryAccess;
 import com.dat3m.dartagnan.program.event.common.SingleAccessMemoryEvent;
 import com.dat3m.dartagnan.program.event.visitors.EventVisitor;
@@ -10,7 +11,7 @@ public class LKMMLock extends SingleAccessMemoryEvent {
     public LKMMLock(Expression lock) {
         // This event will be compiled to LKMMLockRead + LKMMLockWrite
         // and each of those will be assigned a proper memory ordering
-        super(lock, "");
+        super(lock, TypeFactory.getInstance().getIntegerType(32), "");
     }
 
     protected LKMMLock(LKMMLock other) {

diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/linux/LKMMUnlock.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/linux/LKMMUnlock.java
@@ -23,7 +23,7 @@ public class LKMMUnlock extends StoreBase {
     });
 
     public LKMMUnlock(Expression lock) {
-        super(lock, ExpressionFactory.getInstance().makeZero(TypeFactory.getInstance().getArchType()), MO_RELEASE);
+        super(lock, ExpressionFactory.getInstance().makeZero(TypeFactory.getInstance().getIntegerType(32)), MO_RELEASE);
         addTags(Tag.Linux.UNLOCK);
     }
 

diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorArm8.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorArm8.java
@@ -57,7 +57,7 @@ public List<Event> visitInitLock(InitLock e) {
 
     @Override
     public List<Event> visitLock(Lock e) {
-        IntegerType type = types.getArchType();
+        IntegerType type = (IntegerType)e.getAccessType();
         Expression zero = expressions.makeZero(type);
         Expression one = expressions.makeOne(type);
         Register dummy = e.getFunction().newRegister(type);
@@ -74,7 +74,7 @@ public List<Event> visitLock(Lock e) {
     @Override
     public List<Event> visitUnlock(Unlock e) {
         return eventSequence(
-                newStoreWithMo(e.getAddress(), expressions.makeZero(types.getArchType()), ARMv8.MO_REL)
+                newStoreWithMo(e.getAddress(), expressions.makeZero((IntegerType)e.getAccessType()), ARMv8.MO_REL)
         );
     }
 
@@ -453,7 +453,7 @@ public List<Event> visitLKMMXchg(LKMMXchg e) {
     public List<Event> visitLKMMOpNoReturn(LKMMOpNoReturn e) {
         Expression address = e.getAddress();
 
-        Register dummy = e.getFunction().newRegister(types.getArchType());
+        Register dummy = e.getFunction().newRegister(e.getAccessType());
         Expression storeValue = expressions.makeBinary(dummy, e.getOperator(), e.getOperand());
         Load load = newRMWLoadExclusive(dummy, address);
         Store store = newRMWStoreExclusive(address, storeValue, true);
@@ -573,7 +573,7 @@ public List<Event> visitLKMMOpAndTest(LKMMOpAndTest e) {
         Register resultRegister = e.getResultRegister();
         Expression address = e.getAddress();
         String mo = e.getMo();
-        Register dummy = e.getFunction().newRegister(types.getArchType());
+        Register dummy = e.getFunction().newRegister(e.getAccessType());
         Expression testResult = expressions.makeNot(expressions.makeBooleanCast(dummy));
 
         Load load = newRMWLoadExclusiveWithMo(dummy, address, ARMv8.extractLoadMoFromLKMo(mo));
@@ -599,7 +599,7 @@ public List<Event> visitLKMMOpAndTest(LKMMOpAndTest e) {
 
     @Override
     public List<Event> visitLKMMLock(LKMMLock e) {
-        IntegerType type = types.getArchType();
+        IntegerType type = (IntegerType) e.getAccessType();
         Expression zero = expressions.makeZero(type);
         Expression one = expressions.makeOne(type);
         Register dummy = e.getFunction().newRegister(type);
@@ -615,7 +615,7 @@ public List<Event> visitLKMMLock(LKMMLock e) {
 
     @Override
     public List<Event> visitLKMMUnlock(LKMMUnlock e) {
-        Expression zero = expressions.makeZero(types.getArchType());
+        Expression zero = expressions.makeZero((IntegerType)e.getAccessType());
         return eventSequence(
                 newStoreWithMo(e.getAddress(), zero, ARMv8.MO_REL)
         );

diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorBase.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorBase.java
@@ -58,7 +58,7 @@ public List<Event> visitInitLock(InitLock e) {
 
     @Override
     public List<Event> visitLock(Lock e) {
-        IntegerType type = types.getArchType(); // TODO: Boolean should be sufficient
+        IntegerType type = (IntegerType) e.getAccessType(); // TODO: Boolean should be sufficient
         Register dummy = e.getFunction().newRegister(type);
         Expression zero = expressions.makeZero(type);
         Expression one = expressions.makeOne(type);
@@ -74,7 +74,7 @@ public List<Event> visitLock(Lock e) {
 
     @Override
     public List<Event> visitUnlock(Unlock e) {
-        IntegerType type = types.getArchType(); // TODO: Boolean should be sufficient
+        IntegerType type = (IntegerType) e.getAccessType(); // TODO: Boolean should be sufficient
         Register dummy = e.getFunction().newRegister(type);
         Expression zero = expressions.makeZero(type);
         Expression one = expressions.makeOne(type);

diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorLKMM.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorLKMM.java
@@ -3,7 +3,7 @@
 import com.dat3m.dartagnan.expression.BNonDet;
 import com.dat3m.dartagnan.expression.Expression;
 import com.dat3m.dartagnan.expression.ExpressionFactory;
-import com.dat3m.dartagnan.expression.type.TypeFactory;
+import com.dat3m.dartagnan.expression.type.IntegerType;
 import com.dat3m.dartagnan.program.Register;
 import com.dat3m.dartagnan.program.event.EventFactory;
 import com.dat3m.dartagnan.program.event.Tag;
@@ -100,7 +100,7 @@ public List<Event> visitLKMMFetchOp(LKMMFetchOp e) {
     public List<Event> visitLKMMOpNoReturn(LKMMOpNoReturn e) {
         Expression address = e.getAddress();
 
-        Register dummy = e.getFunction().newRegister(types.getArchType());
+        Register dummy = e.getFunction().newRegister(e.getAccessType());
         Expression storeValue = expressions.makeBinary(dummy, e.getOperator(), e.getOperand());
         Load load = newRMWLoadWithMo(dummy, address, Tag.Linux.MO_ONCE);
         load.addTags(Tag.Linux.NORETURN);
@@ -194,7 +194,7 @@ public List<Event> visitLKMMXchg(LKMMXchg e) {
 
     @Override
     public List<Event> visitLKMMLock(LKMMLock e) {
-        Register dummy = e.getFunction().newRegister(types.getArchType());
+        Register dummy = e.getFunction().newRegister(e.getAccessType());
         Expression nonzeroDummy = expressions.makeBooleanCast(dummy);
 
         Load lockRead = newLockRead(dummy, e.getLock());
@@ -243,7 +243,7 @@ private static Load newLockRead(Register dummy, Expression lockAddr) {
     }
 
     private static RMWStore newLockWrite(Load lockRead, Expression lockAddr) {
-        Expression one = ExpressionFactory.getInstance().makeOne(TypeFactory.getInstance().getArchType());
+        Expression one = ExpressionFactory.getInstance().makeOne((IntegerType) lockRead.getAccessType());
         RMWStore lockWrite = newRMWStoreWithMo(lockRead, lockAddr, one, Tag.Linux.MO_ONCE);
         lockWrite.addTags(Tag.Linux.LOCK_WRITE);
         return lockWrite;

diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorPTX.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorPTX.java
@@ -36,7 +36,7 @@ public List<Event> visitPtxAtomOp(PTXAtomOp e) {
     @Override
     public List<Event> visitPtxRedOp(PTXRedOp e) {
         Expression address = e.getAddress();
-        Register dummy = e.getFunction().newRegister(types.getArchType());
+        Register dummy = e.getFunction().newRegister(e.getAccessType());
         Load load = newRMWLoadWithMo(dummy, address, Tag.PTX.loadMO(e.getMo()));
         RMWStore store = newRMWStoreWithMo(load, address,
                 expressions.makeBinary(dummy, e.getOperator(), e.getOperand()), Tag.PTX.storeMO(e.getMo()));

diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorPower.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorPower.java
@@ -52,14 +52,15 @@ public List<Event> visitInitLock(InitLock e) {
 
     @Override
     public List<Event> visitLock(Lock e) {
-        Register dummy = e.getFunction().newRegister(types.getArchType());
+        IntegerType type = (IntegerType) e.getAccessType();
+        Register dummy = e.getFunction().newRegister(type);
         Label label = newLabel("FakeDep");
         // We implement locks as spinlocks which are guaranteed to succeed, i.e. we can
         // use assumes. The fake control dependency + isync guarantee acquire semantics.
         return eventSequence(
                 newRMWLoadExclusive(dummy, e.getAddress()),
                 newAssume(expressions.makeNot(expressions.makeBooleanCast(dummy))),
-                Power.newRMWStoreConditional(e.getAddress(), expressions.makeOne(types.getArchType()), true),
+                Power.newRMWStoreConditional(e.getAddress(), expressions.makeOne(type), true),
                 // Fake dependency to guarantee acquire semantics
                 newFakeCtrlDep(dummy, label),
                 label,
@@ -70,7 +71,7 @@ public List<Event> visitLock(Lock e) {
     public List<Event> visitUnlock(Unlock e) {
         return eventSequence(
                 Power.newLwSyncBarrier(),
-                newStore(e.getAddress(), expressions.makeZero(types.getArchType())));
+                newStore(e.getAddress(), expressions.makeZero((IntegerType)e.getAccessType())));
     }
 
     // =============================================================================================
@@ -737,7 +738,7 @@ public List<Event> visitLKMMOpNoReturn(LKMMOpNoReturn e) {
         Expression address = e.getAddress();
         String mo = e.getMo();
 
-        Register dummy = e.getFunction().newRegister(types.getArchType());
+        Register dummy = e.getFunction().newRegister(e.getAccessType());
         Expression storeValue = expressions.makeBinary(dummy, e.getOperator(), e.getOperand());
         // Power does not have mo tags, thus we use the empty string
         Load load = newRMWLoadExclusive(dummy, address);
@@ -877,7 +878,7 @@ public List<Event> visitLKMMOpAndTest(LKMMOpAndTest e) {
         Register resultRegister = e.getResultRegister();
         Expression address = e.getAddress();
         String mo = e.getMo();
-        Register dummy = e.getFunction().newRegister(types.getArchType());
+        Register dummy = e.getFunction().newRegister(e.getAccessType());
         Expression testResult = expressions.makeNot(expressions.makeBooleanCast(dummy));
 
         Load load = newRMWLoadExclusive(dummy, address);
@@ -909,7 +910,7 @@ public List<Event> visitLKMMOpAndTest(LKMMOpAndTest e) {
 
     @Override
     public List<Event> visitLKMMLock(LKMMLock e) {
-        IntegerType type = types.getArchType();
+        IntegerType type = (IntegerType)e.getAccessType();
         Expression zero = expressions.makeZero(type);
         Expression one = expressions.makeOne(type);
         Register dummy = e.getFunction().newRegister(type);
@@ -930,7 +931,7 @@ public List<Event> visitLKMMLock(LKMMLock e) {
     public List<Event> visitLKMMUnlock(LKMMUnlock e) {
         return eventSequence(
                 Power.newLwSyncBarrier(),
-                newStore(e.getAddress(), expressions.makeZero(types.getArchType()))
+                newStore(e.getAddress(), expressions.makeZero((IntegerType)e.getAccessType()))
         );
     }