Added ptrtracking param

subprojects/common/analysis/build.gradle.kts

@@ -24,7 +24,9 @@ dependencies {
     implementation(project(":theta-solver"))
     implementation(Deps.javasmt)
     implementation(project(":theta-solver-javasmt"))
+    implementation(project(":theta-solver-z3-legacy"))
     implementation(project(":theta-graph-solver"))
+    implementation(project(mapOf("path" to ":theta-solver-z3-legacy")))
     testImplementation(project(":theta-solver-z3-legacy"))
     implementation("com.corundumstudio.socketio:netty-socketio:2.0.6")
 }

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

@@ -17,21 +17,30 @@
 package hu.bme.mit.theta.analysis.ptr
 
 import com.google.common.base.Preconditions
+import hu.bme.mit.theta.analysis.expl.ExplState
+import hu.bme.mit.theta.analysis.expr.ExprState
 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
 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.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 solver = Z3LegacySolverFactory.getInstance().createSolver()
 
 abstract class PtrAction(writeTriples: WriteTriples, val inCnt: Int) : StmtAction() {
 
@@ -40,8 +49,53 @@ abstract class PtrAction(writeTriples: WriteTriples, val inCnt: Int) : StmtActio
     private val expanded by lazy { createStmtList(writeTriples) }
 
     internal var cnts = LinkedHashMap<String, Int>()
-    fun nextWriteTriples(tracked: Collection<Expr<*>> = TopCollection): WriteTriples =
-        expanded.first.map { Pair(it.key, it.value.filter { it.toList().any(tracked::contains) }) }.toMap()
+    fun nextWriteTriples(tracked: Collection<Expr<*>> = TopCollection,
+        trackingStyle: PtrTracking = PtrTracking.ALWAYS_TOP, s: ExprState = ExplState.top()): WriteTriples =
+        expanded.first.filter(tracked, trackingStyle, s)
+
+    private fun WriteTriples.filter(tracked: Collection<Expr<*>>, trackingStyle: PtrTracking,
+        s: ExprState): WriteTriples =
+        when (trackingStyle) {
+            PtrTracking.ALWAYS_TOP -> this
+            PtrTracking.ANY_MATCH -> expanded.first.map {
+                Pair(it.key, it.value.filterIndexed { i, triple ->
+                    triple.toList().any(tracked::contains) && !triple.isPossiblyOverwrittenBy(
+                        it.value.subList(i + 1, it.value.size).filter { !it.toList().any(tracked::contains) }, s)
+                })
+            }.toMap()
+
+            PtrTracking.ALL_MATCH -> expanded.first.map {
+                Pair(it.key, it.value.filterIndexed { i, triple ->
+                    triple.toList().all(tracked::contains) && !triple.isPossiblyOverwrittenBy(
+                        it.value.subList(i + 1, it.value.size).filter { !it.toList().all(tracked::contains) }, s)
+                })
+            }.toMap()
+
+            PtrTracking.NONE -> emptyMap()
+        }
+
+    private fun Triple<Expr<*>, Expr<*>, Expr<IntType>>.isPossiblyOverwrittenBy(
+        thatList: List<Triple<Expr<*>, Expr<*>, Expr<IntType>>>, s: ExprState): Boolean {
+        if (thatList.isEmpty()) return false
+
+        var expr: Expr<BoolType> = Or(
+            thatList.map { that -> And(Eq(this.first, that.first), Eq(this.second, that.second)) })
+        expr = if (s is ExplState) {
+            ExprUtils.simplify(expr, s.`val`)
+        } else {
+            ExprUtils.simplify(expr)
+        }
+        if (expr == True()) return true
+        else if (expr == False()) return false
+
+        WithPushPop(solver).use {
+            val state = PathUtils.unfold(s.toExpr(), 0)
+            val expr = PathUtils.unfold(expr, 0)
+            solver.add(state)
+            solver.add(expr)
+            return solver.check().isSat
+        }
+    }
 
     final override fun getStmts(): List<Stmt> = expanded.second
 

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

@@ -33,14 +33,16 @@ import hu.bme.mit.theta.analysis.expr.ExprState
  *
  */
 
-class PtrAnalysis<S : ExprState, P : Prec>(private val innerAnalysis: Analysis<S, ExprAction, P>) :
+class PtrAnalysis<S : ExprState, P : Prec>(private val innerAnalysis: Analysis<S, ExprAction, P>,
+    private val trackingStyle: PtrTracking = PtrTracking.ALWAYS_TOP) :
     Analysis<PtrState<S>, PtrAction, PtrPrec<P>> {
 
     override fun getPartialOrd(): PartialOrd<PtrState<S>> = innerAnalysis.partialOrd.getPtrPartialOrd()
 
     override fun getInitFunc(): InitFunc<PtrState<S>, PtrPrec<P>> = innerAnalysis.initFunc.getPtrInitFunc()
 
-    override fun getTransFunc(): TransFunc<PtrState<S>, PtrAction, PtrPrec<P>> = innerAnalysis.transFunc.getPtrTransFunc()
+    override fun getTransFunc(): TransFunc<PtrState<S>, PtrAction, PtrPrec<P>> = innerAnalysis.transFunc.getPtrTransFunc(
+        trackingStyle)
 }
 
 fun <S : ExprState> PartialOrd<S>.getPtrPartialOrd(): PartialOrd<PtrState<S>> = PartialOrd { state1, state2 ->
@@ -54,9 +56,10 @@ fun <S : ExprState, P : Prec> InitFunc<S, P>.getPtrInitFunc(): InitFunc<PtrState
     getInitStates(prec.innerPrec).map { PtrState(it) }
 }
 
-fun <S : ExprState, P : Prec> TransFunc<S, in ExprAction, P>.getPtrTransFunc(): TransFunc<PtrState<S>, PtrAction, PtrPrec<P>> = TransFunc { state, action, prec ->
+fun <S : ExprState, P : Prec> TransFunc<S, in ExprAction, P>.getPtrTransFunc(
+    trackingStyle: PtrTracking = PtrTracking.ALWAYS_TOP): TransFunc<PtrState<S>, PtrAction, PtrPrec<P>> = TransFunc { state, action, prec ->
     getSuccStates(state.innerState, action, prec.innerPrec).map {
-        PtrState(it, action.nextWriteTriples(/*prec.trackedDerefParams*/),
+        PtrState(it, action.nextWriteTriples(prec.trackedDerefParams, trackingStyle, it),
             action.cnts.values.maxOrNull() ?: action.inCnt)
     }
 }

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

@@ -126,3 +126,10 @@ object TopCollection: Collection<Expr<*>> {
 
     override fun iterator(): Iterator<Expr<*>> = error("TopCollection not iterable")
 }
+
+enum class PtrTracking {
+    ALWAYS_TOP, // always keep track of all pointer accesses
+    ANY_MATCH, // if any of the arguments match, keep track
+    ALL_MATCH, // if all of the arguments match, keep track
+    NONE // do not keep track of any pointer acceses
+}

subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaAnalysis.kt

@@ -30,10 +30,7 @@ import hu.bme.mit.theta.analysis.expr.ExprState
 import hu.bme.mit.theta.analysis.expr.StmtAction
 import hu.bme.mit.theta.analysis.pred.*
 import hu.bme.mit.theta.analysis.pred.PredAbstractors.PredAbstractor
-import hu.bme.mit.theta.analysis.ptr.PtrPrec
-import hu.bme.mit.theta.analysis.ptr.PtrState
-import hu.bme.mit.theta.analysis.ptr.getPtrInitFunc
-import hu.bme.mit.theta.analysis.ptr.getPtrTransFunc
+import hu.bme.mit.theta.analysis.ptr.*
 import hu.bme.mit.theta.analysis.waitlist.Waitlist
 import hu.bme.mit.theta.common.Try
 import hu.bme.mit.theta.common.logging.Logger
@@ -247,10 +244,10 @@ private fun getExplXcfaInitFunc(xcfa: XCFA,
     }
 }
 
-private fun getExplXcfaTransFunc(solver: Solver,
-    maxEnum: Int): (XcfaState<PtrState<ExplState>>, XcfaAction, XcfaPrec<PtrPrec<ExplPrec>>) -> List<XcfaState<PtrState<ExplState>>> {
+private fun getExplXcfaTransFunc(solver: Solver, maxEnum: Int, ptrTracking: PtrTracking):
+    (XcfaState<PtrState<ExplState>>, XcfaAction, XcfaPrec<PtrPrec<ExplPrec>>) -> List<XcfaState<PtrState<ExplState>>> {
     val explTransFunc = (ExplStmtTransFunc.create(solver,
-        maxEnum) as TransFunc<ExplState, ExprAction, ExplPrec>).getPtrTransFunc()
+        maxEnum) as TransFunc<ExplState, ExprAction, ExplPrec>).getPtrTransFunc(ptrTracking)
     return { s, a, p ->
         val (newSt, newAct) = s.apply(a)
         explTransFunc.getSuccStates(newSt.sGlobal, newAct, p.p.addVars(
@@ -260,10 +257,11 @@ private fun getExplXcfaTransFunc(solver: Solver,
 }
 
 class ExplXcfaAnalysis(xcfa: XCFA, solver: Solver, maxEnum: Int,
-    partialOrd: PartialOrd<XcfaState<PtrState<ExplState>>>) : XcfaAnalysis<ExplState, PtrPrec<ExplPrec>>(
+    partialOrd: PartialOrd<XcfaState<PtrState<ExplState>>>, ptrTracking: PtrTracking) :
+    XcfaAnalysis<ExplState, PtrPrec<ExplPrec>>(
     corePartialOrd = partialOrd,
     coreInitFunc = getExplXcfaInitFunc(xcfa, solver),
-    coreTransFunc = getExplXcfaTransFunc(solver, maxEnum)
+        coreTransFunc = getExplXcfaTransFunc(solver, maxEnum, ptrTracking)
 )
 
 /// PRED
@@ -282,10 +280,10 @@ private fun getPredXcfaInitFunc(xcfa: XCFA,
     }
 }
 
-private fun getPredXcfaTransFunc(
-    predAbstractor: PredAbstractors.PredAbstractor): (XcfaState<PtrState<PredState>>, XcfaAction, XcfaPrec<PtrPrec<PredPrec>>) -> List<XcfaState<PtrState<PredState>>> {
+private fun getPredXcfaTransFunc(predAbstractor: PredAbstractors.PredAbstractor, ptrTracking: PtrTracking):
+    (XcfaState<PtrState<PredState>>, XcfaAction, XcfaPrec<PtrPrec<PredPrec>>) -> List<XcfaState<PtrState<PredState>>> {
     val predTransFunc = (PredTransFunc.create<StmtAction>(
-        predAbstractor) as TransFunc<PredState, ExprAction, PredPrec>).getPtrTransFunc()
+        predAbstractor) as TransFunc<PredState, ExprAction, PredPrec>).getPtrTransFunc(ptrTracking)
     return { s, a, p ->
         val (newSt, newAct) = s.apply(a)
         predTransFunc.getSuccStates(newSt.sGlobal, newAct, p.p.addVars(
@@ -295,8 +293,9 @@ private fun getPredXcfaTransFunc(
 }
 
 class PredXcfaAnalysis(xcfa: XCFA, solver: Solver, predAbstractor: PredAbstractor,
-    partialOrd: PartialOrd<XcfaState<PtrState<PredState>>>) : XcfaAnalysis<PredState, PtrPrec<PredPrec>>(
+    partialOrd: PartialOrd<XcfaState<PtrState<PredState>>>, ptrTracking: PtrTracking) :
+    XcfaAnalysis<PredState, PtrPrec<PredPrec>>(
     corePartialOrd = partialOrd,
     coreInitFunc = getPredXcfaInitFunc(xcfa, predAbstractor),
-    coreTransFunc = getPredXcfaTransFunc(predAbstractor)
+        coreTransFunc = getPredXcfaTransFunc(predAbstractor, ptrTracking)
 )

subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaSingeExprTraceRefiner.kt

@@ -23,7 +23,6 @@ import hu.bme.mit.theta.analysis.algorithm.cegar.RefinerResult
 import hu.bme.mit.theta.analysis.expr.ExprAction
 import hu.bme.mit.theta.analysis.expr.ExprState
 import hu.bme.mit.theta.analysis.expr.refinement.*
-import hu.bme.mit.theta.analysis.ptr.TopCollection
 import hu.bme.mit.theta.analysis.ptr.WriteTriples
 import hu.bme.mit.theta.common.logging.Logger
 import java.util.*
@@ -74,7 +73,7 @@ class XcfaSingleExprTraceRefiner<S : ExprState, A : ExprAction, P : Prec, R : Re
             Pair(emptyMap(),
                 listOf())) { (wTriple: WriteTriples, list: List<A>): Pair<WriteTriples, List<A>>, a: A ->
             val newA = (a as XcfaAction).withLastWrites(wTriple)
-            Pair(newA.nextWriteTriples(TopCollection), list + (newA as A))
+            Pair(newA.nextWriteTriples(), list + (newA as A))
         }.second
         val traceToConcretize = Trace.of(rawTrace.states, actions)
 

subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToCegarChecker.kt

@@ -79,7 +79,8 @@ fun getCegarChecker(xcfa: XCFA, mcm: MCM,
             XcfaDporLts.getPartialOrder(corePartialOrd)
         } else {
             corePartialOrd
-        }
+        },
+        cegarConfig.abstractorConfig.ptrTtracking
     ) as Abstractor<ExprState, ExprAction, Prec>
 
     val ref: ExprTraceChecker<Refutation> =

subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/params/ParamValues.kt

@@ -34,10 +34,7 @@ import hu.bme.mit.theta.analysis.expr.ExprState
 import hu.bme.mit.theta.analysis.expr.refinement.*
 import hu.bme.mit.theta.analysis.pred.*
 import hu.bme.mit.theta.analysis.pred.ExprSplitters.ExprSplitter
-import hu.bme.mit.theta.analysis.ptr.ItpRefToPtrPrec
-import hu.bme.mit.theta.analysis.ptr.PtrPrec
-import hu.bme.mit.theta.analysis.ptr.PtrState
-import hu.bme.mit.theta.analysis.ptr.getPtrPartialOrd
+import hu.bme.mit.theta.analysis.ptr.*
 import hu.bme.mit.theta.analysis.waitlist.Waitlist
 import hu.bme.mit.theta.common.logging.Logger
 import hu.bme.mit.theta.core.decl.VarDecl
@@ -102,7 +99,8 @@ enum class Domain(
         logger: Logger,
         lts: LTS<XcfaState<out PtrState<out ExprState>>, XcfaAction>,
         errorDetectionType: ErrorDetection,
-        partialOrd: PartialOrd<out XcfaState<out PtrState<out ExprState>>>
+        partialOrd: PartialOrd<out XcfaState<out PtrState<out ExprState>>>,
+        ptrTrackingStyle: PtrTracking
     ) -> Abstractor<out ExprState, out ExprAction, out Prec>,
     val itpPrecRefiner: (exprSplitter: ExprSplitter) -> PrecRefiner<out ExprState, out ExprAction, out Prec, out Refutation>,
     val initPrec: (XCFA, InitPrec) -> XcfaPrec<out PtrPrec<*>>,
@@ -112,8 +110,8 @@ enum class Domain(
 ) {
 
     EXPL(
-        abstractor = { a, b, c, d, e, f, g, h, i ->
-            getXcfaAbstractor(ExplXcfaAnalysis(a, b, c, i as PartialOrd<XcfaState<PtrState<ExplState>>>), d,
+        abstractor = { a, b, c, d, e, f, g, h, i, j ->
+            getXcfaAbstractor(ExplXcfaAnalysis(a, b, c, i as PartialOrd<XcfaState<PtrState<ExplState>>>, j), d,
                 e, f, g, h)
         },
         itpPrecRefiner = {
@@ -125,9 +123,9 @@ enum class Domain(
         stateType = TypeToken.get(ExplState::class.java).type
     ),
     PRED_BOOL(
-        abstractor = { a, b, c, d, e, f, g, h, i ->
+        abstractor = { a, b, c, d, e, f, g, h, i, j ->
             getXcfaAbstractor(PredXcfaAnalysis(a, b, PredAbstractors.booleanAbstractor(b),
-                i as PartialOrd<XcfaState<PtrState<PredState>>>), d, e, f, g, h)
+                i as PartialOrd<XcfaState<PtrState<PredState>>>, j), d, e, f, g, h)
         },
         itpPrecRefiner = { a ->
             XcfaPrecRefiner<PtrState<PredState>, PredPrec, ItpRefutation>(ItpRefToPtrPrec(ItpRefToPredPrec(a)))
@@ -138,9 +136,9 @@ enum class Domain(
         stateType = TypeToken.get(PredState::class.java).type
     ),
     PRED_CART(
-        abstractor = { a, b, c, d, e, f, g, h, i ->
+        abstractor = { a, b, c, d, e, f, g, h, i, j ->
             getXcfaAbstractor(PredXcfaAnalysis(a, b, PredAbstractors.cartesianAbstractor(b),
-                i as PartialOrd<XcfaState<PtrState<PredState>>>), d, e, f, g, h)
+                i as PartialOrd<XcfaState<PtrState<PredState>>>, j), d, e, f, g, h)
         },
         itpPrecRefiner = { a ->
             XcfaPrecRefiner<PtrState<PredState>, PredPrec, ItpRefutation>(ItpRefToPtrPrec(ItpRefToPredPrec(a)))
@@ -151,9 +149,9 @@ enum class Domain(
         stateType = TypeToken.get(PredState::class.java).type
     ),
     PRED_SPLIT(
-        abstractor = { a, b, c, d, e, f, g, h, i ->
+        abstractor = { a, b, c, d, e, f, g, h, i, j ->
             getXcfaAbstractor(PredXcfaAnalysis(a, b, PredAbstractors.booleanSplitAbstractor(b),
-                i as PartialOrd<XcfaState<PtrState<PredState>>>), d, e, f, g, h)
+                i as PartialOrd<XcfaState<PtrState<PredState>>>, j), d, e, f, g, h)
         },
         itpPrecRefiner = { a ->
             XcfaPrecRefiner<PtrState<PredState>, PredPrec, ItpRefutation>(ItpRefToPtrPrec(ItpRefToPredPrec(a)))

subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/params/XcfaConfig.kt

@@ -18,6 +18,7 @@ package hu.bme.mit.theta.xcfa.cli.params
 
 import com.beust.jcommander.Parameter
 import hu.bme.mit.theta.analysis.expr.refinement.PruneStrategy
+import hu.bme.mit.theta.analysis.ptr.PtrTracking
 import hu.bme.mit.theta.common.logging.Logger
 import hu.bme.mit.theta.frontend.ParseContext
 import hu.bme.mit.theta.frontend.chc.ChcFrontend
@@ -208,6 +209,9 @@ data class CegarAbstractorConfig(
 
     @Parameter(names = ["--search"], description = "Search strategy")
     var search: Search = Search.ERR,
+
+    @Parameter(names = ["--ptr-tracking"], description = "How to track pointers in the transition function")
+    var ptrTtracking: PtrTracking = PtrTracking.ALWAYS_TOP
 ) : Config
 
 data class CegarRefinerConfig(