Serializable class hierarchy for statements, expressions and types

build.gradle.kts

@@ -29,7 +29,7 @@ buildscript {
 
 allprojects {
     group = "hu.bme.mit.theta"
-    version = "6.17.7"
+    version = "6.18.1"
 
 
     apply(from = rootDir.resolve("gradle/shared-with-buildSrc/mirrors.gradle.kts"))

settings.gradle.kts

@@ -20,6 +20,7 @@ include(
     "common/common",
     "common/core",
     "common/grammar",
+    "common/ksp-processor",
     "common/multi-tests",
     "common/ltl",
     "common/ltl-cli",

subprojects/cfa/cfa-analysis/src/main/kotlin/hu/bme/mit/theta/cfa/analysis/CfaToMonolithicExpr.kt

@@ -21,15 +21,19 @@ import hu.bme.mit.theta.analysis.expl.ExplState
 import hu.bme.mit.theta.cfa.CFA
 import hu.bme.mit.theta.core.decl.Decls
 import hu.bme.mit.theta.core.model.Valuation
-import hu.bme.mit.theta.core.stmt.*
+import hu.bme.mit.theta.core.stmt.AssignStmt
+import hu.bme.mit.theta.core.stmt.AssumeStmt
+import hu.bme.mit.theta.core.stmt.NonDetStmt
+import hu.bme.mit.theta.core.stmt.SequenceStmt
 import hu.bme.mit.theta.core.type.Expr
 import hu.bme.mit.theta.core.type.abstracttype.AbstractExprs.Eq
 import hu.bme.mit.theta.core.type.abstracttype.AbstractExprs.Neq
 import hu.bme.mit.theta.core.type.booltype.BoolExprs.And
 import hu.bme.mit.theta.core.type.booltype.BoolExprs.Bool
 import hu.bme.mit.theta.core.type.booltype.BoolType
 import hu.bme.mit.theta.core.type.bvtype.BvType
-import hu.bme.mit.theta.core.type.fptype.FpExprs.*
+import hu.bme.mit.theta.core.type.fptype.FpExprs.FpAssign
+import hu.bme.mit.theta.core.type.fptype.FpExprs.NaN
 import hu.bme.mit.theta.core.type.fptype.FpType
 import hu.bme.mit.theta.core.type.inttype.IntExprs.Int
 import hu.bme.mit.theta.core.type.inttype.IntLitExpr
@@ -38,7 +42,6 @@ import hu.bme.mit.theta.core.utils.BvUtils
 import hu.bme.mit.theta.core.utils.StmtUtils
 import hu.bme.mit.theta.core.utils.indexings.VarIndexingFactory
 import java.math.BigInteger
-import java.util.*
 
 fun CFA.toMonolithicExpr(): MonolithicExpr {
   Preconditions.checkArgument(this.errorLoc.isPresent)

subprojects/cfa/cfa/src/main/java/hu/bme/mit/theta/cfa/dsl/CfaExpression.java

@@ -15,68 +15,41 @@
  */
 package hu.bme.mit.theta.cfa.dsl;
 
-import static com.google.common.base.Preconditions.checkArgument;
-import static com.google.common.base.Preconditions.checkNotNull;
-import static com.google.common.base.Preconditions.checkState;
+import static com.google.common.base.Preconditions.*;
 import static hu.bme.mit.theta.cfa.dsl.gen.CfaDslParser.*;
-import static hu.bme.mit.theta.common.Utils.head;
-import static hu.bme.mit.theta.common.Utils.singleElementOf;
-import static hu.bme.mit.theta.common.Utils.tail;
+import static hu.bme.mit.theta.common.Utils.*;
 import static hu.bme.mit.theta.core.decl.Decls.Param;
+import static hu.bme.mit.theta.core.type.abstracttype.AbstractExprs.*;
 import static hu.bme.mit.theta.core.type.abstracttype.AbstractExprs.Add;
 import static hu.bme.mit.theta.core.type.abstracttype.AbstractExprs.Div;
 import static hu.bme.mit.theta.core.type.abstracttype.AbstractExprs.Eq;
 import static hu.bme.mit.theta.core.type.abstracttype.AbstractExprs.Geq;
 import static hu.bme.mit.theta.core.type.abstracttype.AbstractExprs.Gt;
-import static hu.bme.mit.theta.core.type.abstracttype.AbstractExprs.Ite;
 import static hu.bme.mit.theta.core.type.abstracttype.AbstractExprs.Leq;
 import static hu.bme.mit.theta.core.type.abstracttype.AbstractExprs.Lt;
-import static hu.bme.mit.theta.core.type.abstracttype.AbstractExprs.Mod;
 import static hu.bme.mit.theta.core.type.abstracttype.AbstractExprs.Mul;
 import static hu.bme.mit.theta.core.type.abstracttype.AbstractExprs.Neg;
 import static hu.bme.mit.theta.core.type.abstracttype.AbstractExprs.Neq;
 import static hu.bme.mit.theta.core.type.abstracttype.AbstractExprs.Pos;
 import static hu.bme.mit.theta.core.type.abstracttype.AbstractExprs.Rem;
 import static hu.bme.mit.theta.core.type.abstracttype.AbstractExprs.Sub;
 import static hu.bme.mit.theta.core.type.anytype.Exprs.Prime;
-import static hu.bme.mit.theta.core.type.arraytype.ArrayExprs.ArrayInit;
-import static hu.bme.mit.theta.core.type.arraytype.ArrayExprs.Read;
-import static hu.bme.mit.theta.core.type.arraytype.ArrayExprs.Write;
+import static hu.bme.mit.theta.core.type.arraytype.ArrayExprs.*;
+import static hu.bme.mit.theta.core.type.booltype.BoolExprs.*;
 import static hu.bme.mit.theta.core.type.booltype.BoolExprs.And;
-import static hu.bme.mit.theta.core.type.booltype.BoolExprs.Bool;
-import static hu.bme.mit.theta.core.type.booltype.BoolExprs.Exists;
-import static hu.bme.mit.theta.core.type.booltype.BoolExprs.False;
-import static hu.bme.mit.theta.core.type.booltype.BoolExprs.Forall;
-import static hu.bme.mit.theta.core.type.booltype.BoolExprs.Iff;
-import static hu.bme.mit.theta.core.type.booltype.BoolExprs.Imply;
 import static hu.bme.mit.theta.core.type.booltype.BoolExprs.Not;
 import static hu.bme.mit.theta.core.type.booltype.BoolExprs.Or;
-import static hu.bme.mit.theta.core.type.booltype.BoolExprs.True;
 import static hu.bme.mit.theta.core.type.booltype.BoolExprs.Xor;
-import static hu.bme.mit.theta.core.type.bvtype.BvExprs.Bv;
-import static hu.bme.mit.theta.core.type.bvtype.BvExprs.Extract;
-import static hu.bme.mit.theta.core.type.bvtype.BvExprs.SExt;
-import static hu.bme.mit.theta.core.type.bvtype.BvExprs.ZExt;
-import static hu.bme.mit.theta.core.type.fptype.FpExprs.Abs;
-import static hu.bme.mit.theta.core.type.fptype.FpExprs.FromBv;
-import static hu.bme.mit.theta.core.type.fptype.FpExprs.IsNan;
-import static hu.bme.mit.theta.core.type.fptype.FpExprs.Max;
-import static hu.bme.mit.theta.core.type.fptype.FpExprs.Min;
-import static hu.bme.mit.theta.core.type.fptype.FpExprs.RoundToIntegral;
-import static hu.bme.mit.theta.core.type.fptype.FpExprs.Sqrt;
-import static hu.bme.mit.theta.core.type.fptype.FpExprs.ToBv;
-import static hu.bme.mit.theta.core.type.fptype.FpExprs.ToFp;
+import static hu.bme.mit.theta.core.type.bvtype.BvExprs.*;
+import static hu.bme.mit.theta.core.type.fptype.FpExprs.*;
 import static hu.bme.mit.theta.core.type.inttype.IntExprs.Int;
 import static hu.bme.mit.theta.core.type.rattype.RatExprs.Rat;
 import static hu.bme.mit.theta.core.utils.ExprUtils.simplify;
-import static hu.bme.mit.theta.core.utils.TypeUtils.cast;
-import static hu.bme.mit.theta.core.utils.TypeUtils.castBv;
-import static hu.bme.mit.theta.core.utils.TypeUtils.castFp;
+import static hu.bme.mit.theta.core.utils.TypeUtils.*;
 import static java.util.stream.Collectors.toList;
 
 import com.google.common.collect.ImmutableList;
 import hu.bme.mit.theta.cfa.dsl.gen.CfaDslBaseVisitor;
-import hu.bme.mit.theta.common.Tuple2;
 import hu.bme.mit.theta.common.dsl.BasicScope;
 import hu.bme.mit.theta.common.dsl.Env;
 import hu.bme.mit.theta.common.dsl.Scope;
@@ -87,29 +60,13 @@
 import hu.bme.mit.theta.core.dsl.ParseException;
 import hu.bme.mit.theta.core.type.Expr;
 import hu.bme.mit.theta.core.type.Type;
-import hu.bme.mit.theta.core.type.abstracttype.AddExpr;
-import hu.bme.mit.theta.core.type.abstracttype.DivExpr;
-import hu.bme.mit.theta.core.type.abstracttype.ModExpr;
-import hu.bme.mit.theta.core.type.abstracttype.MulExpr;
-import hu.bme.mit.theta.core.type.abstracttype.RemExpr;
-import hu.bme.mit.theta.core.type.abstracttype.SubExpr;
+import hu.bme.mit.theta.core.type.abstracttype.*;
 import hu.bme.mit.theta.core.type.anytype.RefExpr;
 import hu.bme.mit.theta.core.type.arraytype.ArrayType;
 import hu.bme.mit.theta.core.type.booltype.BoolType;
 import hu.bme.mit.theta.core.type.booltype.FalseExpr;
 import hu.bme.mit.theta.core.type.booltype.TrueExpr;
-import hu.bme.mit.theta.core.type.bvtype.BvAddExpr;
-import hu.bme.mit.theta.core.type.bvtype.BvConcatExpr;
-import hu.bme.mit.theta.core.type.bvtype.BvExprs;
-import hu.bme.mit.theta.core.type.bvtype.BvLitExpr;
-import hu.bme.mit.theta.core.type.bvtype.BvMulExpr;
-import hu.bme.mit.theta.core.type.bvtype.BvSDivExpr;
-import hu.bme.mit.theta.core.type.bvtype.BvSModExpr;
-import hu.bme.mit.theta.core.type.bvtype.BvSRemExpr;
-import hu.bme.mit.theta.core.type.bvtype.BvSubExpr;
-import hu.bme.mit.theta.core.type.bvtype.BvType;
-import hu.bme.mit.theta.core.type.bvtype.BvUDivExpr;
-import hu.bme.mit.theta.core.type.bvtype.BvURemExpr;
+import hu.bme.mit.theta.core.type.bvtype.*;
 import hu.bme.mit.theta.core.type.fptype.FpExprs;
 import hu.bme.mit.theta.core.type.fptype.FpLitExpr;
 import hu.bme.mit.theta.core.type.fptype.FpRoundingMode;
@@ -118,16 +75,13 @@
 import hu.bme.mit.theta.core.type.inttype.IntLitExpr;
 import hu.bme.mit.theta.core.type.rattype.RatLitExpr;
 import java.math.BigInteger;
-import java.util.Arrays;
-import java.util.Collection;
-import java.util.Collections;
-import java.util.List;
-import java.util.Optional;
+import java.util.*;
 import java.util.regex.Matcher;
 import java.util.regex.Pattern;
 import java.util.stream.Collectors;
 import java.util.stream.IntStream;
 import java.util.stream.Stream;
+import kotlin.Pair;
 import org.antlr.v4.runtime.Token;
 
 final class CfaExpression {
@@ -1105,11 +1059,11 @@ private <T1 extends Type, T2 extends Type> Expr<?> createArrayLitExpr(
             }
             valueType = (T2) ctx.elseExpr.accept(this).getType();
 
-            final List<Tuple2<Expr<T1>, Expr<T2>>> elems =
+            final List<Pair<Expr<T1>, Expr<T2>>> elems =
                     IntStream.range(0, ctx.indexExpr.size())
                             .mapToObj(
                                     i ->
-                                            Tuple2.of(
+                                            new Pair<>(
                                                     cast(
                                                             ctx.indexExpr.get(i).accept(this),
                                                             indexType),

subprojects/cfa/cfa/src/test/java/hu/bme/mit/theta/cfa/CfaTest.java

@@ -15,6 +15,8 @@
  */
 package hu.bme.mit.theta.cfa;
 
+import static org.junit.Assert.assertEquals;
+
 import hu.bme.mit.theta.core.decl.Decls;
 import hu.bme.mit.theta.core.decl.VarDecl;
 import hu.bme.mit.theta.core.stmt.Stmts;
@@ -43,6 +45,7 @@ public void testDuplicateVarName() {
         builder.createEdge(init, loc1, Stmts.Havoc(v1));
         builder.createEdge(init, loc2, Stmts.Havoc(v2));
         builder.setInitLoc(init);
-        builder.build();
+        CFA cfa = builder.build();
+        assertEquals(1, cfa.getVars().size());
     }
 }

subprojects/cfa/cfa/src/test/kotlin/hu/bme/mit/theta/cfa/CFAVarChangerUnitTest.kt

@@ -32,7 +32,7 @@ class CFAVarChangerUnitTest {
     val newVar = Decls.Var("x", IntType.getInstance())
     val newCfa = origCfa.copyWithReplacingVars(listOf(newVar).associateBy { it.name })
 
-    assert(!newCfa.vars.any { origCfa.vars.contains(it) })
-    assert(origCfa.vars.iterator().next() != newCfa.vars.iterator().next())
+    assert(!newCfa.vars.any { it in origCfa.vars })
+    assert(origCfa.vars.first() != newCfa.vars.first())
   }
 }

subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/bounded/AbstractMonolithicExpr.kt

@@ -27,10 +27,11 @@ import hu.bme.mit.theta.core.type.booltype.BoolExprs
 import hu.bme.mit.theta.core.type.booltype.BoolLitExpr
 import hu.bme.mit.theta.core.type.booltype.BoolType
 import hu.bme.mit.theta.core.type.booltype.IffExpr
-import hu.bme.mit.theta.core.type.booltype.SmartBoolExprs.*
+import hu.bme.mit.theta.core.type.booltype.SmartBoolExprs.And
+import hu.bme.mit.theta.core.type.booltype.SmartBoolExprs.Not
+import hu.bme.mit.theta.core.type.booltype.SmartBoolExprs.Or
 import hu.bme.mit.theta.core.utils.ExprUtils
 import hu.bme.mit.theta.core.utils.indexings.VarIndexingFactory
-import java.util.HashMap
 
 fun MonolithicExpr.createAbstract(prec: PredPrec): MonolithicExpr {
   // TODO: handle initOffsetIndex in abstract initExpr
@@ -101,7 +102,7 @@ fun MonolithicExpr.createAbstract(prec: PredPrec): MonolithicExpr {
           .map {
             when ((it.value as BoolLitExpr).value) {
               true -> literalToPred[it.key]
-              false -> Not(literalToPred[it.key])
+              false -> Not(literalToPred[it.key]!!)
             }
           }
           .toList()

subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/bounded/BoundedChecker.kt

@@ -29,8 +29,9 @@ import hu.bme.mit.theta.core.type.Expr
 import hu.bme.mit.theta.core.type.abstracttype.AbstractExprs.Eq
 import hu.bme.mit.theta.core.type.booltype.BoolExprs.True
 import hu.bme.mit.theta.core.type.booltype.BoolType
-import hu.bme.mit.theta.core.type.booltype.SmartBoolExprs
-import hu.bme.mit.theta.core.type.booltype.SmartBoolExprs.*
+import hu.bme.mit.theta.core.type.booltype.SmartBoolExprs.And
+import hu.bme.mit.theta.core.type.booltype.SmartBoolExprs.Not
+import hu.bme.mit.theta.core.type.booltype.SmartBoolExprs.Or
 import hu.bme.mit.theta.core.utils.ExprUtils
 import hu.bme.mit.theta.core.utils.PathUtils
 import hu.bme.mit.theta.core.utils.indexings.VarIndexing
@@ -39,7 +40,6 @@ import hu.bme.mit.theta.solver.ItpSolver
 import hu.bme.mit.theta.solver.Solver
 import hu.bme.mit.theta.solver.utils.WithPushPop
 import java.util.*
-import kotlin.collections.plus
 
 /**
  * A checker for bounded model checking.
@@ -310,7 +310,7 @@ constructor(
           if (needProof) {
             // we enumerate all states explored by previous iteration of BMC
             val expr =
-              SmartBoolExprs.And(
+              And(
                 exprs.subList(0, exprs.size - 1) +
                   //                  loopfree.subList(0, loopfree.size - 1) +
                   unfoldedInitExpr

subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/bounded/MonolithicL2S.kt

@@ -33,8 +33,7 @@ import hu.bme.mit.theta.core.utils.indexings.VarIndexingFactory
 import java.util.*
 
 private val reprEq = { e1: Expr<*>, e2: Expr<*> ->
-  if (e1.getType() is FpType) FpExprs.FpAssign(e1 as Expr<FpType>, e2 as Expr<FpType>)
-  else Eq(e1, e2)
+  if (e1.type is FpType) FpExprs.FpAssign(e1 as Expr<FpType>, e2 as Expr<FpType>) else Eq(e1, e2)
 }
 
 fun MonolithicExpr.createMonolithicL2S(): MonolithicExpr {
@@ -70,7 +69,7 @@ fun MonolithicExpr.createMonolithicL2S(): MonolithicExpr {
   newTransExpr.add(skipOrSave)
 
   // New prop expr
-  var prop: Expr<BoolType?>? = saved.ref
+  var prop: Expr<BoolType> = saved.ref
   for ((key, value) in saveMap) {
     val exp = reprEq(value.ref, key.ref)
     prop = And(exp, prop)

subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/refinement/BoundedUnrollingASGTraceCheckerStrategy.kt

@@ -122,8 +122,8 @@ class BoundedUnrollingASGTraceCheckerStrategy<S : ExprState, A : ExprAction>(
         .map { state ->
           val filtVars =
             usedVariablesPrecision.vars.filter(ExprUtils.getVars(state.toExpr())::contains)
-          val types = filtVars.map(VarDecl<*>::getType)
-          val sizes = types.map(Type::getDomainSize)
+          val types = filtVars.map(VarDecl<*>::type)
+          val sizes = types.map(Type::domainSize)
           val res = sizes.fold(DomainSize.ONE, DomainSize::multiply)
           res
         }

subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/util/VarCollectorStmtVisitor.kt

@@ -70,9 +70,9 @@ class VarCollectorStmtVisitor : StmtVisitor<Set<VarDecl<*>>, Set<VarDecl<*>>> {
   override fun visit(stmt: IfStmt, param: Set<VarDecl<*>>) =
     param + stmt.then.accept(this, param) + stmt.elze.accept(this, param)
 
-  override fun <PtrType : Type?, OffsetType : Type?, DeclType : Type?> visit(
-    stmt: MemoryAssignStmt<PtrType, OffsetType, DeclType>?,
-    param: Set<VarDecl<*>>?,
+  override fun <PtrType : Type, OffsetType : Type, DeclType : Type> visit(
+    stmt: MemoryAssignStmt<PtrType, OffsetType, DeclType>,
+    param: Set<VarDecl<*>>,
   ): Set<VarDecl<*>> {
     TODO("Not yet implemented")
   }

subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/oc/IDLOcChecker.kt

@@ -19,10 +19,14 @@ import hu.bme.mit.theta.core.decl.ConstDecl
 import hu.bme.mit.theta.core.decl.Decls
 import hu.bme.mit.theta.core.decl.VarDecl
 import hu.bme.mit.theta.core.type.Expr
-import hu.bme.mit.theta.core.type.booltype.BoolExprs.*
+import hu.bme.mit.theta.core.type.booltype.BoolExprs.And
+import hu.bme.mit.theta.core.type.booltype.BoolExprs.Bool
+import hu.bme.mit.theta.core.type.booltype.BoolExprs.Imply
 import hu.bme.mit.theta.core.type.booltype.BoolLitExpr
 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.IntExprs.Lt
+import hu.bme.mit.theta.core.type.inttype.IntExprs.Neq
 import hu.bme.mit.theta.core.type.inttype.IntLitExpr
 import hu.bme.mit.theta.core.type.inttype.IntType
 import hu.bme.mit.theta.solver.Solver

subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/oc/OcChecker.kt

@@ -16,7 +16,9 @@
 package hu.bme.mit.theta.analysis.algorithm.oc
 
 import hu.bme.mit.theta.core.decl.VarDecl
-import hu.bme.mit.theta.core.type.booltype.BoolExprs.*
+import hu.bme.mit.theta.core.type.booltype.BoolExprs.And
+import hu.bme.mit.theta.core.type.booltype.BoolExprs.Imply
+import hu.bme.mit.theta.core.type.booltype.BoolExprs.Or
 import hu.bme.mit.theta.solver.Solver
 import hu.bme.mit.theta.solver.SolverStatus
 

subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/ptr/PtrAction.kt

@@ -15,7 +15,6 @@
  */
 package hu.bme.mit.theta.analysis.ptr
 
-import com.google.common.base.Preconditions
 import hu.bme.mit.theta.analysis.expr.StmtAction
 import hu.bme.mit.theta.core.decl.Decls.Var
 import hu.bme.mit.theta.core.decl.VarDecl
@@ -64,26 +63,25 @@ abstract class PtrAction(writeTriples: WriteTriples = emptyMap(), val inCnt: Int
       val postList = ArrayList<Stmt>()
 
       for ((deref, type) in stmt.dereferencesWithAccessTypes) {
-        Preconditions.checkState(
-          deref.uniquenessIdx.isPresent,
-          "Incomplete dereferences (missing uniquenessIdx) are not handled properly.",
-        )
+        requireNotNull(deref.uniquenessIdx) {
+          "Incomplete dereferences (missing uniquenessIdx) are not handled properly."
+        }
         val expr = deref.getIte(nextWriteTriples)
         if (type == AccessType.WRITE) {
           val writeExpr = ExprUtils.simplify(IntExprs.Add(expr, IntExprs.Int(1)))
           nextWriteTriples
             .getOrPut(deref.type) { ArrayList() }
-            .add(Triple(lookup[deref]!!.first, lookup[deref]!!.second, deref.uniquenessIdx.get()))
+            .add(Triple(lookup[deref]!!.first, lookup[deref]!!.second, deref.uniquenessIdx!!))
           postList.add(
             Stmts.Assume(
               ExprUtils.simplify(
-                BoolExprs.And(listOf(AbstractExprs.Eq(writeExpr, deref.uniquenessIdx.get())))
+                BoolExprs.And(listOf(AbstractExprs.Eq(writeExpr, deref.uniquenessIdx!!)))
               )
             )
           )
         } else {
           preList.add(
-            Stmts.Assume(ExprUtils.simplify(AbstractExprs.Eq(expr, deref.uniquenessIdx.get())))
+            Stmts.Assume(ExprUtils.simplify(AbstractExprs.Eq(expr, deref.uniquenessIdx!!)))
           )
         }
         //                postList.add(Stmts.Assume(Eq(vargen("value", deref.type).ref, deref))) //