mv default alignmentExpr to TypeFactory

Author: tonghaining

dartagnan/src/main/java/com/dat3m/dartagnan/expression/ExpressionFactory.java

@@ -27,18 +27,14 @@ public final class ExpressionFactory {
     private final BooleanType booleanType = types.getBooleanType();
     private final BoolLiteral falseConstant = new BoolLiteral(booleanType, false);
     private final BoolLiteral trueConstant = new BoolLiteral(booleanType, true);
-    private final Expression defaultAlignment = makeValue(8, types.getArchType());
 
-    private ExpressionFactory() {}
+    private ExpressionFactory() {
+    }
 
     public static ExpressionFactory getInstance() {
         return instance;
     }
 
-    public Expression getDefaultAlignment() {
-        return defaultAlignment;
-    }
-
     // -----------------------------------------------------------------------------------------------------------------
     // Boolean
 

dartagnan/src/main/java/com/dat3m/dartagnan/expression/type/TypeFactory.java

@@ -1,5 +1,7 @@
 package com.dat3m.dartagnan.expression.type;
 
+import com.dat3m.dartagnan.expression.Expression;
+import com.dat3m.dartagnan.expression.ExpressionFactory;
 import com.dat3m.dartagnan.expression.Type;
 import com.dat3m.dartagnan.utils.Normalizer;
 import com.google.common.math.IntMath;
@@ -34,6 +36,10 @@ public static TypeFactory getInstance() {
         return instance;
     }
 
+    public Expression getDefaultAlignment() {
+        return ExpressionFactory.getInstance().makeValue(getMemorySizeInBytes(getArchType()), getArchType());
+    }
+
     public BooleanType getBooleanType() {
         return booleanType;
     }

dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/spirv/VisitorOpsFunction.java

@@ -13,7 +13,6 @@
 import com.dat3m.dartagnan.parsers.program.visitors.spirv.builders.ProgramBuilder;
 import com.dat3m.dartagnan.parsers.program.visitors.spirv.decorations.Alignment;
 import com.dat3m.dartagnan.parsers.program.visitors.spirv.helpers.HelperInputs;
-import com.dat3m.dartagnan.parsers.program.visitors.spirv.helpers.HelperTypes;
 import com.dat3m.dartagnan.program.Function;
 import com.dat3m.dartagnan.program.Register;
 import com.dat3m.dartagnan.program.event.EventFactory;
@@ -193,7 +192,7 @@ private void checkFunctionType(String id, Function function, Type type) {
     private Expression createEntryPointParameter(String id, Type type) {
         Integer alignmentNum = alignment.getValue(id);
         Expression alignmentExpr = alignmentNum == null ?
-                expressions.getDefaultAlignment() : expressions.makeValue(alignmentNum, types.getArchType());
+                types.getDefaultAlignment() : expressions.makeValue(alignmentNum, types.getArchType());
         Expression value = createEntryPointParameterValue(id, type);
         if (type instanceof ScopedPointerType pType) {
             String ptrId = HelperInputs.castPointerId(id);

dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/spirv/VisitorOpsMemory.java

@@ -123,7 +123,7 @@ public Event visitOpVariable(SpirvParser.OpVariableContext ctx) {
             Type type = pointerType.getPointedType();
             Integer alignmentNum = alignment.getValue(id);
             Expression alignmentExpr = alignmentNum == null ?
-                    expressions.getDefaultAlignment() : expressions.makeValue(alignmentNum, types.getArchType());
+                    types.getDefaultAlignment() : expressions.makeValue(alignmentNum, types.getArchType());
             if (alignmentNum != null) {
                 type = HelperTypes.getAlignedType(type, alignmentNum);
             }

dartagnan/src/main/java/com/dat3m/dartagnan/program/memory/Memory.java

@@ -16,12 +16,13 @@ public class Memory {
     private final ArrayList<MemoryObject> objects = new ArrayList<>();
     private final Type ptrType = TypeFactory.getInstance().getPointerType();
     private final IntegerType archType = TypeFactory.getInstance().getArchType();
+    private final TypeFactory types = TypeFactory.getInstance();
 
     private int nextIndex = 1;
 
     // Generates a new, statically allocated memory object.
     public MemoryObject allocate(int size) {
-        final Expression defaultAlignment = ExpressionFactory.getInstance().getDefaultAlignment();
+        final Expression defaultAlignment = types.getDefaultAlignment();
         return allocate(size, defaultAlignment);
     }
 
@@ -43,7 +44,7 @@ public MemoryObject allocate(Alloc allocationSite) {
     }
 
     public VirtualMemoryObject allocateVirtual(int size, boolean generic, VirtualMemoryObject alias) {
-        return allocateVirtual(size, generic, ExpressionFactory.getInstance().getDefaultAlignment(), alias);
+        return allocateVirtual(size, generic, types.getDefaultAlignment(), alias);
     }
 
     public VirtualMemoryObject allocateVirtual(int size, boolean generic, Expression alignment,

dartagnan/src/test/java/com/dat3m/dartagnan/parsers/program/visitors/spirv/VisitorOpsMemoryTest.java

@@ -233,8 +233,8 @@ public void testAlignedVariable() {
         builder.mockVectorType("%arr", "%int", 3);
         builder.mockPtrType("%int_ptr", "%int", "Uniform");
         builder.mockPtrType("%arr_ptr", "%arr", "Uniform");
-        builder.mockPointerAlignment("%v1", 128);
-        builder.mockPointerAlignment("%v2", 512);
+        builder.mockPointerAlignment("%v1", 32);
+        builder.mockPointerAlignment("%v2", 64);
 
 
         // when
@@ -243,11 +243,11 @@ public void testAlignedVariable() {
         // then
         ScopedPointerVariable v1 = (ScopedPointerVariable) builder.getExpression("%v1");
         assertNotNull(v1);
-        assertEquals(128, v1.getAddress().getKnownAlignment());
-        assertEquals(128, ((IntegerType) v1.getInnerType()).getBitWidth());
+        assertEquals(32, v1.getAddress().getKnownAlignment());
+        assertEquals(256, ((IntegerType) v1.getInnerType()).getBitWidth());
         ScopedPointerVariable v2 = (ScopedPointerVariable) builder.getExpression("%v2");
         assertNotNull(v2);
-        assertEquals(512, ((AggregateType) v2.getInnerType()).getFields().get(1).offset());
+        assertEquals(64, ((AggregateType) v2.getInnerType()).getFields().get(1).offset());
     }
 
     @Test