Several minor fixes (#620)

Author: ThomasHaas

dartagnan/src/main/java/com/dat3m/dartagnan/expression/integers/IntLiteral.java

@@ -31,6 +31,10 @@ public int getValueAsInt() {
         return value.intValueExact();
     }
 
+    public long getValueAsLong() {
+        return value.longValueExact();
+    }
+
     public boolean isOne() { return value.equals(BigInteger.ONE); }
     public boolean isZero() { return value.equals(BigInteger.ZERO); }
 

dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/MemToReg.java

@@ -97,11 +97,11 @@ private void promoteAll(Function function, Matcher matcher) {
             if (event instanceof Load load) {
                 final Register reg = load.getResultRegister();
                 assert load.getUsers().isEmpty();
-                load.replaceBy(EventFactory.newLocal(reg, expressions.makeCast(registers.get(access.offset), reg.getType())));
+                load.replaceBy(EventFactory.newLocal(reg, expressions.makeCast(registers.get((int)access.offset), reg.getType())));
                 loadCount++;
             }
             if (event instanceof Store store) {
-                final Register reg = registers.get(access.offset);
+                final Register reg = registers.get((int)access.offset);
                 assert store.getUsers().isEmpty();
                 store.replaceBy(EventFactory.newLocal(reg, expressions.makeCast(store.getMemValue(), reg.getType())));
                 storeCount++;
@@ -142,14 +142,14 @@ private List<Type> getPrimitiveReplacementTypes(Alloc allocation) {
     }
 
     // Invariant: base != null
-    private record AddressOffset(RegWriter base, int offset) {
-        private AddressOffset increase(int o) {
+    private record AddressOffset(RegWriter base, long offset) {
+        private AddressOffset increase(long o) {
             return o == 0 ? this : new AddressOffset(base, offset + o);
         }
     }
 
     // Invariant: register != null
-    private record RegisterOffset(Register register, int offset) {}
+    private record RegisterOffset(Register register, long offset) {}
 
     // Processes events in program order.
     // Returns a label, if it is program-ordered before the current event and its symbolic state was updated.
@@ -327,14 +327,14 @@ private void publishRegisters(Set<Register> registers) {
         }
 
         private RegisterOffset matchGEP(Expression expression) {
-            int sum = 0;
+            long sum = 0;
             while (!(expression instanceof Register register)) {
                 if (!(expression instanceof IntBinaryExpr bin) ||
                         bin.getKind() != IntBinaryOp.ADD ||
                         !(bin.getRight() instanceof IntLiteral offset)) {
                     return null;
                 }
-                sum += offset.getValueAsInt();
+                sum += offset.getValueAsLong();
                 expression = bin.getLeft();
             }
             return new RegisterOffset(register, sum);

dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/RemoveUnusedMemory.java

@@ -25,10 +25,8 @@ public void run(Program program) {
         program.getThreadEvents(RegReader.class).forEach(r -> r.transformExpressions(collector));
         // Also add MemoryObjects referenced by initial values (this does happen in Litmus code)
         for (MemoryObject obj : memory.getObjects()) {
-            for (int field : obj.getStaticallyInitializedFields()) {
-                if (obj.getInitialValue(field) instanceof MemoryObject memObj) {
-                    collector.memoryObjects.add(memObj);
-                }
+            for (Integer field : obj.getStaticallyInitializedFields()) {
+                obj.getInitialValue(field).accept(collector);
             }
         }
         // FIXME: We should also traverse the program spec for references to memory objects