various fixes to parse hardware models

ftsrg · Apr 27, 2024 · 7cb8e3a · 7cb8e3a
1 parent 5a44677
commit 7cb8e3a
Show file tree

Hide file tree

Showing 38 changed files with 243 additions and 144 deletions.
diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/expl/StmtApplier.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/expl/StmtApplier.java
@@ -61,7 +61,7 @@ public static ApplyResult apply(final Stmt stmt, final MutableValuation val,
         if (stmt instanceof AssignStmt) {
             final AssignStmt<?> assignStmt = (AssignStmt<?>) stmt;
             return applyAssign(assignStmt, val, approximate);
-        } else if (stmt instanceof MemoryAssignStmt<?, ?> memoryAssignStmt) {
+        } else if (stmt instanceof MemoryAssignStmt<?, ?, ?> memoryAssignStmt) {
             return applyMemAssign(memoryAssignStmt, val, approximate);
         } else if (stmt instanceof AssumeStmt) {
             final AssumeStmt assumeStmt = (AssumeStmt) stmt;
@@ -91,7 +91,7 @@ public static ApplyResult apply(final Stmt stmt, final MutableValuation val,
         }
     }
 
-    private static ApplyResult applyMemAssign(MemoryAssignStmt<?, ?> stmt, MutableValuation val, boolean approximate) {
+    private static ApplyResult applyMemAssign(MemoryAssignStmt<?, ?, ?> stmt, MutableValuation val, boolean approximate) {
         final var expr = ExprUtils.simplify(stmt.getDeref(), val);
         final var deref = stmt.getDeref();
         final var newOffset = ExprUtils.simplify(deref.getOffset(), val);

diff --git a/...lysis/src/main/java/hu/bme/mit/theta/analysis/expr/refinement/ExprTraceNewtonChecker.java b/...lysis/src/main/java/hu/bme/mit/theta/analysis/expr/refinement/ExprTraceNewtonChecker.java
@@ -284,7 +284,7 @@ public <DeclType extends Type> Stmt visit(AssignStmt<DeclType> stmt, Void param)
             }
 
             @Override
-            public <PtrType extends Type, DeclType extends Type> Stmt visit(MemoryAssignStmt<PtrType, DeclType> stmt, Void param) {
+            public <PtrType extends Type, OffsetType extends Type, DeclType extends Type> Stmt visit(MemoryAssignStmt<PtrType, OffsetType, DeclType> stmt, Void param) {
                 throw new UnsupportedOperationException("MemoryAssignStmt not supported (yet)");
             }
 
@@ -414,7 +414,7 @@ public <DeclType extends Type> Collection<VarDecl<?>> visit(AssignStmt<DeclType>
             }
 
             @Override
-            public <PtrType extends Type, DeclType extends Type> Collection<VarDecl<?>> visit(MemoryAssignStmt<PtrType, DeclType> stmt, Void param) {
+            public <PtrType extends Type, OffsetType extends Type, DeclType extends Type> Collection<VarDecl<?>> visit(MemoryAssignStmt<PtrType, OffsetType, DeclType> stmt, Void param) {
                 throw new UnsupportedOperationException("MemoryAssignStmt not supported (yet)");
             }
 
@@ -467,7 +467,7 @@ public <DeclType extends Type> Collection<VarDecl<?>> visit(AssignStmt<DeclType>
             }
 
             @Override
-            public <PtrType extends Type, DeclType extends Type> Collection<VarDecl<?>> visit(MemoryAssignStmt<PtrType, DeclType> stmt, Void param) {
+            public <PtrType extends Type, OffsetType extends Type, DeclType extends Type> Collection<VarDecl<?>> visit(MemoryAssignStmt<PtrType, OffsetType, DeclType> stmt, Void param) {
                 throw new UnsupportedOperationException("MemoryAssignStmt not supported (yet)");
             }
 
@@ -520,7 +520,7 @@ public <DeclType extends Type> Collection<VarDecl<?>> visit(AssignStmt<DeclType>
             }
 
             @Override
-            public <PtrType extends Type, DeclType extends Type> Collection<VarDecl<?>> visit(MemoryAssignStmt<PtrType, DeclType> stmt, Void param) {
+            public <PtrType extends Type, OffsetType extends Type, DeclType extends Type> Collection<VarDecl<?>> visit(MemoryAssignStmt<PtrType, OffsetType, DeclType> stmt, Void param) {
                 throw new UnsupportedOperationException("MemoryAssignStmt not supported (yet)");
             }
 

diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/ptr/PtrAction.kt b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/ptr/PtrAction.kt
@@ -25,21 +25,21 @@ import hu.bme.mit.theta.core.decl.VarDecl
 import hu.bme.mit.theta.core.stmt.Stmt
 import hu.bme.mit.theta.core.stmt.Stmts
 import hu.bme.mit.theta.core.type.Expr
+import hu.bme.mit.theta.core.type.Type
 import hu.bme.mit.theta.core.type.abstracttype.AbstractExprs
 import hu.bme.mit.theta.core.type.abstracttype.AbstractExprs.Eq
 import hu.bme.mit.theta.core.type.anytype.IteExpr
 import hu.bme.mit.theta.core.type.booltype.BoolExprs
 import hu.bme.mit.theta.core.type.booltype.BoolExprs.*
 import hu.bme.mit.theta.core.type.booltype.BoolType
 import hu.bme.mit.theta.core.type.inttype.IntExprs
-import hu.bme.mit.theta.core.type.inttype.IntExprs.Int
 import hu.bme.mit.theta.core.type.inttype.IntType
 import hu.bme.mit.theta.core.utils.ExprUtils
 import hu.bme.mit.theta.core.utils.PathUtils
 import hu.bme.mit.theta.solver.utils.WithPushPop
 import hu.bme.mit.theta.solver.z3legacy.Z3LegacySolverFactory
 
-private val varList = LinkedHashMap<String, LinkedHashMap<Int, VarDecl<IntType>>>()
+private val varList = LinkedHashMap<Pair<String, Type>, LinkedHashMap<Int, VarDecl<*>>>()
 private val solver = Z3LegacySolverFactory.getInstance().createSolver()
 
 abstract class PtrAction(writeTriples: WriteTriples, val inCnt: Int) : StmtAction() {
@@ -102,11 +102,11 @@ abstract class PtrAction(writeTriples: WriteTriples, val inCnt: Int) : StmtActio
     private fun createStmtList(writeTriples: WriteTriples): Pair<WriteTriples, List<Stmt>> {
         val nextWriteTriples = writeTriples.toMutable()
         val stmtList = ArrayList<Stmt>()
-        val vargen = { it: String ->
+        val vargen = { it: String, type: Type ->
             val current = cnts.getOrDefault(it, inCnt)
             cnts[it] = current + 1
-            val iMap = varList.getOrPut(it) { LinkedHashMap() }
-            iMap.getOrPut(current) { Var("__${it}_$current", Int()) }
+            val iMap = varList.getOrPut(Pair(it, type)) { LinkedHashMap() }
+            iMap.getOrPut(current) { Var("__${it}_$current", type) }
         }
         for (stmt in this.stmtList.map { it.uniqueDereferences(vargen) }) {
             val preList = ArrayList<Stmt>()

diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/ptr/PtrUtils.kt b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/ptr/PtrUtils.kt
@@ -24,6 +24,7 @@ import hu.bme.mit.theta.core.type.Type
 import hu.bme.mit.theta.core.type.abstracttype.AbstractExprs.Eq
 import hu.bme.mit.theta.core.type.anytype.Dereference
 import hu.bme.mit.theta.core.type.anytype.Exprs
+import hu.bme.mit.theta.core.type.inttype.IntExprs.Int
 import hu.bme.mit.theta.core.type.inttype.IntType
 import hu.bme.mit.theta.core.utils.TypeUtils
 
@@ -38,9 +39,9 @@ enum class AccessType {
     READ, WRITE
 }
 
-val Stmt.dereferencesWithAccessTypes: List<Pair<Dereference<*, *>, AccessType>>
+val Stmt.dereferencesWithAccessTypes: List<Pair<Dereference<*, *, *>, AccessType>>
     get() = when (this) {
-        is MemoryAssignStmt<*, *> -> expr.dereferences.map { Pair(it, AccessType.READ) } + listOf(
+        is MemoryAssignStmt<*, *, *> -> expr.dereferences.map { Pair(it, AccessType.READ) } + listOf(
             Pair(deref, AccessType.WRITE))
 
         is AssignStmt<*> -> expr.dereferences.map { Pair(it, AccessType.READ) }
@@ -54,8 +55,8 @@ val Stmt.dereferencesWithAccessTypes: List<Pair<Dereference<*, *>, AccessType>>
         else -> TODO("Not yet implemented for ${this.javaClass.simpleName}")
     }
 
-val Expr<*>.dereferences: List<Dereference<*, *>>
-    get() = if (this is Dereference<*, *>) {
+val Expr<*>.dereferences: List<Dereference<*, *, *>>
+    get() = if (this is Dereference<*, *, *>) {
         listOf(this)
     } else {
         ops.flatMap { it.dereferences }
@@ -71,12 +72,12 @@ fun SequenceStmt.collapse(): Stmt =
         this
     }
 
-fun Stmt.uniqueDereferences(vargen: (String) -> VarDecl<IntType>): Stmt {
+fun Stmt.uniqueDereferences(vargen: (String, Type) -> VarDecl<*>): Stmt {
     val ret = ArrayList<Stmt>()
     val newStmt = when (this) {
-        is MemoryAssignStmt<*, *> -> {
+        is MemoryAssignStmt<*, *, *> -> {
             MemoryAssignStmt.create(
-                deref.uniqueDereferences(vargen).also { ret.addAll(it.first) }.second as Dereference<*, *>,
+                deref.uniqueDereferences(vargen).also { ret.addAll(it.first) }.second as Dereference<*, *, *>,
                 expr.uniqueDereferences(vargen).also { ret.addAll(it.first) }.second)
         }
 
@@ -96,19 +97,20 @@ fun Stmt.uniqueDereferences(vargen: (String) -> VarDecl<IntType>): Stmt {
     return SequenceStmt.of(ret + newStmt).collapse()
 }
 
-fun <T : Type> Expr<T>.uniqueDereferences(vargen: (String) -> VarDecl<IntType>): Pair<List<Stmt>, Expr<T>> =
-    if (this is Dereference<*, T>) {
+fun <T : Type> Expr<T>.uniqueDereferences(vargen: (String, Type) -> VarDecl<*>): Pair<List<Stmt>, Expr<T>> =
+    if (this is Dereference<*, *, T>) {
         val ret = ArrayList<Stmt>()
         Preconditions.checkState(this.uniquenessIdx.isEmpty, "Only non-pretransformed dereferences should be here")
-        val arrayConst = vargen("a")
-        val offsetConst = vargen("o")
+        val arrayConst = vargen("a", array.type)
+        val offsetConst = vargen("o", offset.type)
         val newList = listOf(
             Stmts.Assume(Eq(arrayConst.ref, array.uniqueDereferences(vargen).also { ret.addAll(it.first) }.second)),
             Stmts.Assume(Eq(offsetConst.ref, offset.uniqueDereferences(vargen).also { ret.addAll(it.first) }.second)),
         )
         Pair(
             ret + newList,
-            Exprs.Dereference(arrayConst.ref, offsetConst.ref, type).withUniquenessExpr(vargen("idx").ref))
+            Exprs.Dereference(arrayConst.ref, offsetConst.ref, type)
+                .withUniquenessExpr(vargen("idx", Int()).ref as Expr<IntType>))
     } else {
         val ret = ArrayList<Stmt>()
         Pair(ret, this.withOps(this.ops.map { it.uniqueDereferences(vargen).also { ret.addAll(it.first) }.second }))

diff --git a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/clock/op/ClockOps.java b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/clock/op/ClockOps.java
@@ -176,7 +176,7 @@ public <DeclType extends Type> ClockOp visit(final AssignStmt<DeclType> stmt,
         }
 
         @Override
-        public <PtrType extends Type, DeclType extends Type> ClockOp visit(MemoryAssignStmt<PtrType, DeclType> stmt, Void param) {
+        public <PtrType extends Type, OffsetType extends Type, DeclType extends Type> ClockOp visit(MemoryAssignStmt<PtrType, OffsetType, DeclType> stmt, Void param) {
             throw new UnsupportedOperationException("MemoryAssignStmt not supported (yet)");
         }
 

diff --git a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/dsl/impl/StmtWriter.java b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/dsl/impl/StmtWriter.java
@@ -51,7 +51,7 @@ public <DeclType extends Type> String visit(final AssignStmt<DeclType> stmt, fin
     }
 
     @Override
-    public <PtrType extends Type, DeclType extends Type> String visit(MemoryAssignStmt<PtrType, DeclType> stmt, Void param) {
+    public <PtrType extends Type, OffsetType extends Type, DeclType extends Type> String visit(MemoryAssignStmt<PtrType, OffsetType, DeclType> stmt, Void param) {
         return stmt.getDeref() + " := " + writeExpr(stmt.getExpr());
     }
 

diff --git a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/stmt/MemoryAssignStmt.java b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/stmt/MemoryAssignStmt.java
@@ -29,34 +29,34 @@
  *
  * @param <DeclType>
  */
-public final class MemoryAssignStmt<PtrType extends Type, DeclType extends Type> implements Stmt {
+public final class MemoryAssignStmt<PtrType extends Type, OffsetType extends Type, DeclType extends Type> implements Stmt {
 
     private static final String STMT_LABEL = "memassign";
 
-    private final Dereference<PtrType, DeclType> deref;
+    private final Dereference<PtrType, OffsetType, DeclType> deref;
     private final Expr<DeclType> expr;
 
-    private MemoryAssignStmt(final Dereference<PtrType, DeclType> deref, final Expr<DeclType> expr) {
+    private MemoryAssignStmt(final Dereference<PtrType, OffsetType, DeclType> deref, final Expr<DeclType> expr) {
         this.deref = checkNotNull(deref);
         this.expr = checkNotNull(expr);
     }
 
-    public static <PtrType extends Type, DeclType extends Type> MemoryAssignStmt<PtrType, DeclType> of(
-            final Dereference<PtrType, DeclType> deref,
+    public static <PtrType extends Type, OffsetType extends Type, DeclType extends Type> MemoryAssignStmt<PtrType, OffsetType, DeclType> of(
+            final Dereference<PtrType, OffsetType, DeclType> deref,
             final Expr<DeclType> expr) {
         return new MemoryAssignStmt<>(deref, expr);
     }
 
     @SuppressWarnings("unchecked")
-    public static <PtrType extends Type, DeclType extends Type> MemoryAssignStmt<PtrType, DeclType> create(
-            final Dereference<PtrType, ?> deref,
+    public static <PtrType extends Type, OffsetType extends Type, DeclType extends Type> MemoryAssignStmt<PtrType, OffsetType, DeclType> create(
+            final Dereference<PtrType, OffsetType, ?> deref,
             final Expr<DeclType> expr) {
-        final Dereference<PtrType, DeclType> typedDeref = (Dereference<PtrType, DeclType>) deref;
-        final Expr<DeclType> typedExpr = (Expr<DeclType>) expr;
+        final Dereference<PtrType, OffsetType, DeclType> typedDeref = (Dereference<PtrType, OffsetType, DeclType>) deref;
+        final Expr<DeclType> typedExpr = expr;
         return MemoryAssignStmt.of(typedDeref, typedExpr);
     }
 
-    public Dereference<PtrType, DeclType> getDeref() {
+    public Dereference<PtrType, OffsetType, DeclType> getDeref() {
         return deref;
     }
 
@@ -79,8 +79,8 @@ public boolean equals(final Object obj) {
         if (this == obj) {
             return true;
         } else if (obj != null && this.getClass() == obj.getClass()) {
-            return Objects.equal(deref, ((MemoryAssignStmt<?, ?>) obj).deref) &&
-                    Objects.equal(expr, ((MemoryAssignStmt<?, ?>) obj).expr);
+            return Objects.equal(deref, ((MemoryAssignStmt<?, ?, ?>) obj).deref) &&
+                    Objects.equal(expr, ((MemoryAssignStmt<?, ?, ?>) obj).expr);
         } else {
             return false;
         }

diff --git a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/stmt/StmtVisitor.java b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/stmt/StmtVisitor.java
@@ -25,7 +25,7 @@ public interface StmtVisitor<P, R> {
 
     <DeclType extends Type> R visit(AssignStmt<DeclType> stmt, P param);
 
-    <PtrType extends Type, DeclType extends Type> R visit(MemoryAssignStmt<PtrType, DeclType> stmt, P param);
+    <PtrType extends Type, OffsetType extends Type, DeclType extends Type> R visit(MemoryAssignStmt<PtrType, OffsetType, DeclType> stmt, P param);
 
     <DeclType extends Type> R visit(HavocStmt<DeclType> stmt, P param);
 

diff --git a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/stmt/Stmts.java b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/stmt/Stmts.java
@@ -45,7 +45,7 @@ public static <T extends Type> AssignStmt<T> Assign(final VarDecl<T> lhs, final
         return AssignStmt.of(lhs, rhs);
     }
 
-    public static <P extends Type, T extends Type> MemoryAssignStmt<P, T> MemoryAssign(final Dereference<P, T> deref, final Expr<T> expr) {
+    public static <P extends Type, O extends Type, T extends Type> MemoryAssignStmt<P, O, T> MemoryAssign(final Dereference<P, O, T> deref, final Expr<T> expr) {
         return MemoryAssignStmt.of(deref, expr);
     }
 

diff --git a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/anytype/Dereference.java b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/anytype/Dereference.java
@@ -28,27 +28,25 @@
 import java.util.Optional;
 
 import static com.google.common.base.Preconditions.checkState;
-import static hu.bme.mit.theta.core.utils.TypeUtils.cast;
 
-public final class Dereference<A extends Type, T extends Type> implements Expr<T> {
+public final class Dereference<A extends Type, O extends Type, T extends Type> implements Expr<T> {
 
     private static final String OPERATOR_LABEL = "deref";
-    private static int counter = 0;
     private final Expr<A> array;
-    private final Expr<A> offset;
+    private final Expr<O> offset;
     private final T type;
 
     private final Optional<Expr<IntType>> uniquenessIdx;
 
-    private Dereference(Expr<A> array, Expr<A> offset, T type) {
+    private Dereference(Expr<A> array, Expr<O> offset, T type) {
         this.array = array;
         this.offset = offset;
         this.type = type;
         uniquenessIdx = Optional.empty();
     }
 
 
-    private Dereference(Expr<A> array, Expr<A> offset, Expr<IntType> uniqueness, T type) {
+    private Dereference(Expr<A> array, Expr<O> offset, Expr<IntType> uniqueness, T type) {
         this.array = array;
         this.offset = offset;
         this.type = type;
@@ -59,20 +57,20 @@ public Expr<A> getArray() {
         return array;
     }
 
-    public Expr<A> getOffset() {
+    public Expr<O> getOffset() {
         return offset;
     }
 
 
-    public static <A extends Type, T extends Type> Dereference<A, T> of(Expr<A> array, Expr<A> offset, T type) {
+    public static <A extends Type, O extends Type, T extends Type> Dereference<A, O, T> of(Expr<A> array, Expr<O> offset, T type) {
         return new Dereference<>(array, offset, type);
     }
 
-    private static <A extends Type, T extends Type> Dereference<A, T> of(Expr<A> array, Expr<A> offset, Expr<IntType> uniqueness, T type) {
+    private static <A extends Type, O extends Type, T extends Type> Dereference<A, O, T> of(Expr<A> array, Expr<O> offset, Expr<IntType> uniqueness, T type) {
         return new Dereference<>(array, offset, uniqueness, type);
     }
 
-    public Dereference<A, T> withUniquenessExpr(Expr<IntType> expr) {
+    public Dereference<A, O, T> withUniquenessExpr(Expr<IntType> expr) {
         return Dereference.of(array, offset, expr, type); // TODO: this kills the stuck check
     }
 
@@ -100,11 +98,10 @@ public List<? extends Expr<?>> getOps() {
     @Override
     public Expr<T> withOps(List<? extends Expr<?>> ops) {
         checkState(ops.size() == 3 || ops.size() == 2);
-        @SuppressWarnings("unchecked") final T ptrType = (T) ops.get(0).getType();
         if (ops.size() == 3) {
-            return Dereference.of(cast(ops.get(0), ptrType), cast(ops.get(1), ptrType), (Expr<IntType>) ops.get(2), type);
+            return Dereference.of(ops.get(0), ops.get(1), (Expr<IntType>) ops.get(2), type);
         } else {
-            return Dereference.of(cast(ops.get(0), ptrType), cast(ops.get(1), ptrType), type);
+            return Dereference.of(ops.get(0), ops.get(1), type);
         }
     }
 
@@ -115,7 +112,7 @@ public int hashCode() {
 
     @Override
     public boolean equals(Object obj) {
-        if (obj instanceof Dereference<?, ?> that) {
+        if (obj instanceof Dereference<?, ?, ?> that) {
             return Objects.equals(this.array, that.array) &&
                     Objects.equals(this.offset, that.offset) &&
                     Objects.equals(this.uniquenessIdx, that.uniquenessIdx) &&

diff --git a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/anytype/Exprs.java b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/anytype/Exprs.java
@@ -41,8 +41,8 @@ public static <ExprType extends Type> PrimeExpr<ExprType> Prime(final Expr<ExprT
         return PrimeExpr.of(op);
     }
 
-    public static <ArrType extends Type, ExprType extends Type>
-    Dereference<ArrType, ExprType> Dereference(final Expr<ArrType> arr, final Expr<ArrType> offset, final ExprType type) {
+    public static <ArrType extends Type, OffsetType extends Type, ExprType extends Type>
+    Dereference<ArrType, OffsetType, ExprType> Dereference(final Expr<ArrType> arr, final Expr<OffsetType> offset, final ExprType type) {
         return Dereference.of(arr, offset, type);
     }
 

diff --git a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/utils/ExprSimplifier.java b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/utils/ExprSimplifier.java
@@ -437,7 +437,7 @@ private <ExprType extends Type> Expr<ExprType> simplifyGenericIte(final IteExpr<
         return expr.with(cond, then, elze);
     }
 
-    private Expr<?> simplifyDereference(final Dereference<?, ?> expr, final Valuation val) {
+    private Expr<?> simplifyDereference(final Dereference<?, ?, ?> expr, final Valuation val) {
         return expr.map(it -> simplify(it, val));
     }
 

diff --git a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/utils/SpState.java b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/utils/SpState.java
@@ -149,7 +149,7 @@ public <DeclType extends Type> SpState visit(final AssignStmt<DeclType> stmt,
         }
 
         @Override
-        public <PtrType extends Type, DeclType extends Type> SpState visit(MemoryAssignStmt<PtrType, DeclType> stmt, SpState param) {
+        public <PtrType extends Type, OffsetType extends Type, DeclType extends Type> SpState visit(MemoryAssignStmt<PtrType, OffsetType, DeclType> stmt, SpState param) {
             throw new UnsupportedOperationException("MemoryAssignStmt not supported (yet)");
         }
 

diff --git a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/utils/StmtAtomCollector.java b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/utils/StmtAtomCollector.java
@@ -67,7 +67,7 @@ public <DeclType extends Type> Void visit(AssignStmt<DeclType> stmt,
         }
 
         @Override
-        public <PtrType extends Type, DeclType extends Type> Void visit(MemoryAssignStmt<PtrType, DeclType> stmt, Set<Expr<BoolType>> atoms) {
+        public <PtrType extends Type, OffsetType extends Type, DeclType extends Type> Void visit(MemoryAssignStmt<PtrType, OffsetType, DeclType> stmt, Set<Expr<BoolType>> atoms) {
             final Expr<BoolType> eq = EqExpr.create2(stmt.getDeref(), stmt.getExpr());
             atoms.addAll(ExprUtils.getAtoms(eq));
             return null;

diff --git a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/utils/StmtCounterVisitor.java b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/utils/StmtCounterVisitor.java
@@ -59,7 +59,7 @@ public <DeclType extends Type> Integer visit(AssignStmt<DeclType> stmt, Void par
     }
 
     @Override
-    public <PtrType extends Type, DeclType extends Type> Integer visit(MemoryAssignStmt<PtrType, DeclType> stmt, Void param) {
+    public <PtrType extends Type, OffsetType extends Type, DeclType extends Type> Integer visit(MemoryAssignStmt<PtrType, OffsetType, DeclType> stmt, Void param) {
         return 1;
     }