>,
) : XcfaSporLts(xcfa) {
- override fun getEnabledActionsFor(
- state: XcfaState>,
- exploredActions: Collection,
- prec: P
- ): Set {
- // Collecting enabled actions
- val allEnabledActions = simpleXcfaLts.getEnabledActionsFor(state, exploredActions, prec)
+ override fun getEnabledActionsFor(
+ state: XcfaState>,
+ exploredActions: Collection,
+ prec: P,
+ ): Set {
+ // Collecting enabled actions
+ val allEnabledActions = simpleXcfaLts.getEnabledActionsFor(state, exploredActions, prec)
- // Calculating the source set starting from every (or some of the) enabled transition or from exploredActions if it is not empty
- // The minimal source set is stored
- var minimalSourceSet = mutableSetOf()
- val sourceSetFirstActions = if (exploredActions.isEmpty()) {
- getSourceSetFirstActions(state, allEnabledActions)
- } else {
- setOf(exploredActions)
- }
- var finalIgnoredVars = setOf>()
+ // Calculating the source set starting from every (or some of the) enabled transition or from
+ // exploredActions if it is not empty
+ // The minimal source set is stored
+ var minimalSourceSet = mutableSetOf()
+ val sourceSetFirstActions =
+ if (exploredActions.isEmpty()) {
+ getSourceSetFirstActions(state, allEnabledActions)
+ } else {
+ setOf(exploredActions)
+ }
+ var finalIgnoredVars = setOf>()
- // Calculate source sets from all possible starting action set
- for (firstActions in sourceSetFirstActions) {
- // Variables that have been ignored (if they would be in the precision, more actions have had to be added to the source set)
- val ignoredVars = mutableSetOf>()
- val sourceSet = calculateSourceSet(state, allEnabledActions, firstActions, prec, ignoredVars)
- if (minimalSourceSet.isEmpty() || sourceSet.size < minimalSourceSet.size) {
- minimalSourceSet = sourceSet.toMutableSet()
- finalIgnoredVars = ignoredVars
- }
- }
- finalIgnoredVars.forEach { ignoredVar ->
- if (ignoredVar !in ignoredVarRegistry) {
- ignoredVarRegistry[ignoredVar] = mutableSetOf()
- }
- checkNotNull(ignoredVarRegistry[ignoredVar]).add(state)
- }
- minimalSourceSet.removeAll(exploredActions.toSet())
- return minimalSourceSet
+ // Calculate source sets from all possible starting action set
+ for (firstActions in sourceSetFirstActions) {
+ // Variables that have been ignored (if they would be in the precision, more actions have had
+ // to be added to the source set)
+ val ignoredVars = mutableSetOf>()
+ val sourceSet = calculateSourceSet(state, allEnabledActions, firstActions, prec, ignoredVars)
+ if (minimalSourceSet.isEmpty() || sourceSet.size < minimalSourceSet.size) {
+ minimalSourceSet = sourceSet.toMutableSet()
+ finalIgnoredVars = ignoredVars
+ }
+ }
+ finalIgnoredVars.forEach { ignoredVar ->
+ if (ignoredVar !in ignoredVarRegistry) {
+ ignoredVarRegistry[ignoredVar] = mutableSetOf()
+ }
+ checkNotNull(ignoredVarRegistry[ignoredVar]).add(state)
}
+ minimalSourceSet.removeAll(exploredActions.toSet())
+ return minimalSourceSet
+ }
- /**
- * Calculates a source set of enabled actions starting from a set of particular actions.
- *
- * @param enabledActions the enabled actions in the present state
- * @param firstActions the actions that will be added to the source set as the first actions
- * @param prec the precision of the current abstraction
- * @param ignoredVars variables that have been ignored (if they would be in the precision, more actions have had to be added to the source set)
- * @return a source set of enabled actions in the current abstraction
- */
- private fun calculateSourceSet(
- state: XcfaState>,
- enabledActions: Collection, firstActions: Collection,
- prec: Prec, ignoredVars: MutableSet>
- ): Set {
- if (firstActions.any { it.isBackward }) {
- return enabledActions.toSet()
- }
+ /**
+ * Calculates a source set of enabled actions starting from a set of particular actions.
+ *
+ * @param enabledActions the enabled actions in the present state
+ * @param firstActions the actions that will be added to the source set as the first actions
+ * @param prec the precision of the current abstraction
+ * @param ignoredVars variables that have been ignored (if they would be in the precision, more
+ * actions have had to be added to the source set)
+ * @return a source set of enabled actions in the current abstraction
+ */
+ private fun calculateSourceSet(
+ state: XcfaState>,
+ enabledActions: Collection,
+ firstActions: Collection,
+ prec: Prec,
+ ignoredVars: MutableSet>,
+ ): Set {
+ if (firstActions.any { it.isBackward }) {
+ return enabledActions.toSet()
+ }
- val sourceSet = firstActions.toMutableSet()
- val otherActions = enabledActions.toMutableSet() // actions not in the source set
- firstActions.forEach(otherActions::remove)
- val ignoredVarsByAction = otherActions.associateWith { mutableSetOf>() }
+ val sourceSet = firstActions.toMutableSet()
+ val otherActions = enabledActions.toMutableSet() // actions not in the source set
+ firstActions.forEach(otherActions::remove)
+ val ignoredVarsByAction = otherActions.associateWith { mutableSetOf>() }
- var addedNewAction = true
- while (addedNewAction) {
- addedNewAction = false
- val actionsToRemove = mutableSetOf()
- for (action in otherActions) {
- // for every action that is not in the source set it is checked whether it should be added to the source set
- // (because it is dependent with an action already in the source set)
- val potentialIgnoredVars = mutableSetOf>()
- if (sourceSet.any { areDependents(state, it, action, prec, potentialIgnoredVars) }) {
- if (action.isBackward) {
- return enabledActions.toSet() // see POR algorithm for the reason of handling backward edges this way
- }
- sourceSet.add(action)
- actionsToRemove.add(action)
- addedNewAction = true
- } else {
- // the action is not added to the source set because we ignore variables in potentialIgnoredVars
- checkNotNull(ignoredVarsByAction[action]).addAll(potentialIgnoredVars)
- }
- }
- actionsToRemove.forEach(otherActions::remove)
+ var addedNewAction = true
+ while (addedNewAction) {
+ addedNewAction = false
+ val actionsToRemove = mutableSetOf()
+ for (action in otherActions) {
+ // for every action that is not in the source set it is checked whether it should be added
+ // to the source set
+ // (because it is dependent with an action already in the source set)
+ val potentialIgnoredVars = mutableSetOf>()
+ if (sourceSet.any { areDependents(state, it, action, prec, potentialIgnoredVars) }) {
+ if (action.isBackward) {
+ return enabledActions
+ .toSet() // see POR algorithm for the reason of handling backward edges this way
+ }
+ sourceSet.add(action)
+ actionsToRemove.add(action)
+ addedNewAction = true
+ } else {
+ // the action is not added to the source set because we ignore variables in
+ // potentialIgnoredVars
+ checkNotNull(ignoredVarsByAction[action]).addAll(potentialIgnoredVars)
}
- otherActions.forEach { action -> ignoredVars.addAll(checkNotNull(ignoredVarsByAction[action])) }
- return sourceSet
+ }
+ actionsToRemove.forEach(otherActions::remove)
}
+ otherActions.forEach { action -> ignoredVars.addAll(checkNotNull(ignoredVarsByAction[action])) }
+ return sourceSet
+ }
+
+ private fun areDependents(
+ state: XcfaState>,
+ sourceSetAction: XcfaAction,
+ action: XcfaAction,
+ prec: Prec,
+ ignoredVariables: MutableSet>,
+ ): Boolean {
+ if (sourceSetAction.pid == action.pid) return true
+ val sourceSetActionVars = getCachedUsedVars(getEdge(sourceSetAction))
+ val influencedVars = getInfluencedVars(getEdge(action))
+ val sourceSetMemLocs = getCachedMemLocs(getEdge(sourceSetAction))
+ val influencedMemLocs = getInfluencedMemLocs(getEdge(action))
- private fun areDependents(
- state: XcfaState>,
- sourceSetAction: XcfaAction, action: XcfaAction, prec: Prec,
- ignoredVariables: MutableSet>
- ): Boolean {
- if (sourceSetAction.pid == action.pid) return true
- val sourceSetActionVars = getCachedUsedVars(getEdge(sourceSetAction))
- val influencedVars = getInfluencedVars(getEdge(action))
+ if (
+ (influencedMemLocs.filter(MemLoc::isLit) intersect sourceSetMemLocs.filter(MemLoc::isLit))
+ .isNotEmpty()
+ )
+ return true // memlocs aren't necessarily in the prec
- val precVars = prec.usedVars
- for (varDecl in influencedVars) {
- if (varDecl in sourceSetActionVars) {
- if (varDecl !in precVars && varDecl !in fenceVars.values) {
- // the actions would be dependent, but we may have a chance to ignore it in the current abstraction
- ignoredVariables.add(varDecl)
- continue
- }
- return true
- }
+ val precVars = prec.usedVars
+ for (varDecl in influencedVars) {
+ if (varDecl in sourceSetActionVars) {
+ if (varDecl !in precVars && varDecl !in fenceVars.values) {
+ // the actions would be dependent, but we may have a chance to ignore it in the current
+ // abstraction
+ ignoredVariables.add(varDecl)
+ continue
}
- return indirectlyDependent(state, sourceSetAction, sourceSetActionVars, influencedVars)
+ return true
+ }
}
-}
\ No newline at end of file
+ return indirectlyDependent(
+ state,
+ sourceSetAction,
+ sourceSetActionVars,
+ influencedVars,
+ sourceSetMemLocs,
+ influencedMemLocs,
+ )
+ }
+}
diff --git a/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/por/XcfaSporLts.kt b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/por/XcfaSporLts.kt
index 3e0e45d2ea..82ebfb0545 100644
--- a/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/por/XcfaSporLts.kt
+++ b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/por/XcfaSporLts.kt
@@ -22,6 +22,7 @@ import hu.bme.mit.theta.analysis.ptr.PtrState
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.LitExpr
import hu.bme.mit.theta.core.type.abstracttype.AbstractExprs.Eq
import hu.bme.mit.theta.core.type.booltype.BoolExprs.*
import hu.bme.mit.theta.core.type.booltype.BoolType
@@ -39,6 +40,10 @@ import java.util.*
import java.util.function.Predicate
import kotlin.random.Random
+typealias MemLoc = Pair, Expr<*>>
+
+internal fun MemLoc.isLit() = first is LitExpr<*> && second is LitExpr<*>
+
/**
* LTS with a POR (Partial Order Reduction) algorithm applied as a filter when returning enabled
* actions. The algorithm is similar to the static source-set based POR algorithm described in the
@@ -63,11 +68,14 @@ open class XcfaSporLts(protected val xcfa: XCFA) :
/** Global variables used by an edge. */
private val usedVars: MutableMap>> = mutableMapOf()
+ private val usedMemLocs: MutableMap> = mutableMapOf()
+
/**
* Global variables that are used by the key edge or by edges reachable from the current state via
* a given edge.
*/
private val influencedVars: MutableMap>> = mutableMapOf()
+ private val influencedMemLocs: MutableMap> = mutableMapOf()
/** Backward edges in the CFA (an edge of a loop). */
private val backwardEdges: MutableSet> = mutableSetOf()
@@ -235,17 +243,43 @@ open class XcfaSporLts(protected val xcfa: XCFA) :
val influencedVars = getInfluencedVars(getEdge(action))
if ((influencedVars intersect sourceSetActionVars).isNotEmpty()) return true
- return indirectlyDependent(state, sourceSetAction, sourceSetActionVars, influencedVars)
+ val sourceSetMemLocs = getCachedMemLocs(getEdge(sourceSetAction))
+ val influencedMemLocs = getInfluencedMemLocs(getEdge(action))
+ if (
+ (influencedMemLocs.filter(MemLoc::isLit) intersect
+ sourceSetMemLocs.filter(MemLoc::isLit).toSet())
+ .isNotEmpty()
+ )
+ return true
+
+ return indirectlyDependent(
+ state,
+ sourceSetAction,
+ sourceSetActionVars,
+ influencedVars,
+ sourceSetMemLocs,
+ influencedMemLocs,
+ )
}
+ /**
+ * Currently, the check only tests the first argument of (deref arr off), and deems two actions
+ * dependent if the array values may overlap. This should probably be extended for offsets as
+ * well.
+ */
protected fun indirectlyDependent(
state: XcfaState>,
sourceSetAction: XcfaAction,
sourceSetActionVars: Set>,
influencedVars: Set>,
+ sourceSetMemLocs: Set,
+ inflMemLocs: Set,
): Boolean {
- val sourceSetActionMemLocs = sourceSetActionVars.pointsTo(xcfa)
- val influencedMemLocs = influencedVars.pointsTo(xcfa)
+ val sourceSetActionMemLocs =
+ sourceSetActionVars.pointsTo(xcfa) +
+ sourceSetMemLocs.map { it.first }.filterIsInstance>()
+ val influencedMemLocs =
+ influencedVars.pointsTo(xcfa) + inflMemLocs.map { it.first }.filterIsInstance>()
val intersection = sourceSetActionMemLocs intersect influencedMemLocs
if (intersection.isEmpty())
return false // they cannot point to the same memory location even based on static info
@@ -290,6 +324,19 @@ open class XcfaSporLts(protected val xcfa: XCFA) :
}
}
+ /**
+ * Returns the base-offset pairs that an edge uses (it is present in one of its labels).
+ *
+ * @param edge whose base-offset pairs are to be returned
+ * @return the set of used global variables
+ */
+ private fun getDirectlyUsedMemLocs(edge: XcfaEdge): Set {
+ return edge
+ .getFlatLabels()
+ .flatMap { label -> label.dereferences.map { Pair(it.array, it.offset) } }
+ .toSet()
+ }
+
/**
* Returns the global variables that an edge uses or if it is the start of an atomic block the
* global variables that are used in the atomic block. The result is cached.
@@ -312,6 +359,27 @@ open class XcfaSporLts(protected val xcfa: XCFA) :
return vars
}
+ /**
+ * Returns the base-offset pairs that an edge uses. The result is cached.
+ *
+ * @param edge whose base-offset pairs are collected
+ * @return the set of directly or indirectly used base-offset pairs
+ */
+ protected fun getCachedMemLocs(edge: XcfaEdge): Set {
+ if (edge in usedMemLocs) return usedMemLocs[edge]!!
+ val flatLabels = edge.getFlatLabels()
+ val mutexes =
+ flatLabels.filterIsInstance().flatMap { it.acquiredMutexes }.toMutableSet()
+ val vars =
+ if (mutexes.isEmpty()) {
+ getDirectlyUsedMemLocs(edge)
+ } else {
+ getMemLocsWithBFS(edge) { it.mutexOperations(mutexes) }.toSet()
+ }
+ usedMemLocs[edge] = vars
+ return vars
+ }
+
/**
* Returns the global variables used by the given edge or by edges that are reachable via the
* given edge ("influenced vars").
@@ -326,6 +394,20 @@ open class XcfaSporLts(protected val xcfa: XCFA) :
return vars
}
+ /**
+ * Returns the base-offset pairs used by the given edge or by edges that are reachable via the
+ * given edge ("influenced memlocs").
+ *
+ * @param edge whose successor edges' base-offset pairs are to be returned.
+ * @return the set of influenced global variables
+ */
+ protected fun getInfluencedMemLocs(edge: XcfaEdge): Set {
+ if (edge in influencedMemLocs) return influencedMemLocs[edge]!!
+ val vars = getMemLocsWithBFS(edge) { true }
+ influencedMemLocs[edge] = vars
+ return vars
+ }
+
/**
* Returns global variables encountered in a search starting from a given edge.
*
@@ -355,6 +437,35 @@ open class XcfaSporLts(protected val xcfa: XCFA) :
return vars
}
+ /**
+ * Returns base-offset pairs encountered in a search starting from a given edge.
+ *
+ * @param startEdge the start point of the search
+ * @param goFurther the predicate that tells whether more edges have to be explored through this
+ * edge
+ * @return the set of encountered base-offset variables
+ */
+ private fun getMemLocsWithBFS(startEdge: XcfaEdge, goFurther: Predicate): Set {
+ val memLocs = mutableSetOf()
+ val exploredEdges = mutableListOf()
+ val edgesToExplore = mutableListOf()
+ edgesToExplore.add(startEdge)
+ while (edgesToExplore.isNotEmpty()) {
+ val exploring = edgesToExplore.removeFirst()
+ memLocs.addAll(getDirectlyUsedMemLocs(exploring))
+ if (goFurther.test(exploring)) {
+ val successiveEdges = getSuccessiveEdges(exploring)
+ for (newEdge in successiveEdges) {
+ if (newEdge !in exploredEdges) {
+ edgesToExplore.add(newEdge)
+ }
+ }
+ }
+ exploredEdges.add(exploring)
+ }
+ return memLocs
+ }
+
/**
* Returns the xcfa edge of the given action.
*
diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/ExecuteConfig.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/ExecuteConfig.kt
index db963f6bf9..686cc42c92 100644
--- a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/ExecuteConfig.kt
+++ b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/ExecuteConfig.kt
@@ -455,19 +455,20 @@ private fun postVerificationLogging(
GraphmlWitnessWriter()
.writeWitness(
safetyResult,
- config.inputConfig.input!!,
+ config.outputConfig.witnessConfig.inputFileForWitness ?: config.inputConfig.input!!,
getSolver(
config.outputConfig.witnessConfig.concretizerSolver,
config.outputConfig.witnessConfig.validateConcretizerSolver,
),
parseContext,
witnessFile,
+ config.inputConfig.property,
)
val yamlWitnessFile = File(resultFolder, "witness.yml")
YmlWitnessWriter()
.writeWitness(
safetyResult,
- config.inputConfig.input!!,
+ config.outputConfig.witnessConfig.inputFileForWitness ?: config.inputConfig.input!!,
config.inputConfig.property,
(config.frontendConfig.specConfig as? CFrontendConfig)?.architecture,
getSolver(
diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToHornChecker.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToHornChecker.kt
index 90494c4979..2e73009d5f 100644
--- a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToHornChecker.kt
+++ b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToHornChecker.kt
@@ -20,19 +20,24 @@ import hu.bme.mit.theta.analysis.Trace
import hu.bme.mit.theta.analysis.algorithm.EmptyProof
import hu.bme.mit.theta.analysis.algorithm.SafetyChecker
import hu.bme.mit.theta.analysis.algorithm.SafetyResult
+import hu.bme.mit.theta.analysis.algorithm.chc.CexTree
import hu.bme.mit.theta.analysis.algorithm.chc.HornChecker
+import hu.bme.mit.theta.analysis.algorithm.chc.Invariant
import hu.bme.mit.theta.analysis.pred.PredState
import hu.bme.mit.theta.analysis.ptr.PtrState
import hu.bme.mit.theta.common.logging.Logger
+import hu.bme.mit.theta.core.type.Expr
+import hu.bme.mit.theta.core.type.anytype.RefExpr
+import hu.bme.mit.theta.core.type.booltype.BoolExprs.True
+import hu.bme.mit.theta.core.type.functype.FuncAppExpr
import hu.bme.mit.theta.graphsolver.patterns.constraints.MCM
-import hu.bme.mit.theta.xcfa.analysis.XcfaAction
-import hu.bme.mit.theta.xcfa.analysis.XcfaPrec
-import hu.bme.mit.theta.xcfa.analysis.XcfaState
-import hu.bme.mit.theta.xcfa.analysis.isInlined
+import hu.bme.mit.theta.solver.ProofNode
+import hu.bme.mit.theta.xcfa.analysis.*
import hu.bme.mit.theta.xcfa.cli.params.HornConfig
import hu.bme.mit.theta.xcfa.cli.params.XcfaConfig
import hu.bme.mit.theta.xcfa.cli.utils.getSolver
import hu.bme.mit.theta.xcfa.model.XCFA
+import hu.bme.mit.theta.xcfa.model.XcfaLocation
import hu.bme.mit.theta.xcfa2chc.toCHC
fun getHornChecker(
@@ -60,12 +65,72 @@ fun getHornChecker(
if (result.isSafe) {
SafetyResult.safe(EmptyProof.getInstance())
} else if (result.isUnsafe) {
- val proof = result.asUnsafe().cex
- val state =
- XcfaState>(xcfa, mapOf(), PtrState(PredState.of(proof.proofNode.expr)))
- SafetyResult.unsafe(Trace.of(listOf(state), listOf()), EmptyProof.getInstance())
+ try {
+ getProperTrace(xcfa, result)
+ } catch (t: Throwable) {
+ SafetyResult.unsafe(
+ Trace.of(
+ listOf(
+ XcfaState(
+ xcfa,
+ xcfa.initProcedures.get(0).first.errorLoc.get(),
+ PtrState(PredState.of(True())),
+ )
+ ),
+ listOf(),
+ ),
+ EmptyProof.getInstance(),
+ )
+ }
} else {
SafetyResult.unknown()
}
}
}
+
+private fun getProperTrace(
+ xcfa: XCFA,
+ result: SafetyResult,
+): SafetyResult.Unsafe>, XcfaAction>>? {
+ val getName = { s: String ->
+ val split = s.split("_")
+ val allButLast = split.subList(0, split.size - 1)
+ allButLast.joinToString("_")
+ }
+ val loc = { proofNode: ProofNode ->
+ if (proofNode.expr is FuncAppExpr<*, *>) {
+ var func: Expr<*> = proofNode.expr
+ while (func is FuncAppExpr<*, *>) {
+ func = func.func
+ }
+ func as RefExpr<*>
+ xcfa.procedures.flatMap { it.locs }.first { it.name == getName(func.decl.name) }
+ } else null
+ }
+ val states = mutableListOf>>()
+ val actions = mutableListOf()
+ var proofNode: ProofNode? = result.asUnsafe().cex.proofNode
+ var lastLoc: XcfaLocation? = null
+ while (proofNode != null) {
+ loc(proofNode)?.also { currentLoc ->
+ states.add(XcfaState(xcfa, currentLoc, PtrState(PredState.of())))
+ lastLoc?.also {
+ actions.add(
+ XcfaAction(
+ 0,
+ xcfa.procedures
+ .flatMap { it.edges }
+ .first { it.source == currentLoc && it.target == lastLoc },
+ )
+ )
+ }
+ lastLoc = currentLoc
+ }
+ proofNode = proofNode.children.getOrNull(0)
+ }
+
+ return SafetyResult.unsafe(
+ Trace.of(states.reversed(), actions.reversed()),
+ EmptyProof.getInstance(),
+ )
+}
diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/InProcessChecker.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/InProcessChecker.kt
index 4022efe510..8ca637dd16 100644
--- a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/InProcessChecker.kt
+++ b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/InProcessChecker.kt
@@ -77,12 +77,16 @@ class InProcessChecker(
getGson(xcfa).toJson(processConfig)
}
+ val heapSize =
+ "-Xmx${if(config.backendConfig.memlimit == 0L) 1420L else config.backendConfig.memlimit/1024/1024 }m"
+ logger.write(Logger.Level.INFO, "Starting process with $heapSize of heap\n")
+
val pb =
NuProcessBuilder(
listOf(
ProcessHandle.current().info().command().orElse("java"),
"-Xss120m",
- "-Xmx14210m",
+ heapSize,
"-cp",
File(XcfaCli::class.java.protectionDomain.codeSource.location.toURI()).absolutePath,
XcfaCli::class.qualifiedName,
diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/params/XcfaConfig.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/params/XcfaConfig.kt
index 73b52dbcda..1675afa4a6 100644
--- a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/params/XcfaConfig.kt
+++ b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/params/XcfaConfig.kt
@@ -179,6 +179,11 @@ data class BackendConfig(
var timeoutMs: Long = 0,
@Parameter(names = ["--in-process"], description = "Run analysis in process")
var inProcess: Boolean = false,
+ @Parameter(
+ names = ["--memlimit"],
+ description = "Maximum memory to use when --in-process (in bytes, 0 for default)",
+ )
+ var memlimit: Long = 0L,
override var specConfig: T? = null,
) : SpecializableConfig {
@@ -470,6 +475,7 @@ data class WitnessConfig(
"Activates a wrapper, which validates the assertions in the solver in each (SAT) check. Filters some solver issues.",
)
var validateConcretizerSolver: Boolean = false,
+ @Parameter(names = ["--input-file-for-witness"]) var inputFileForWitness: File? = null,
) : Config
data class ArgConfig(
diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/portfolio/bounded25.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/portfolio/bounded25.kt
index 5b8d481b8b..95f9cced5c 100644
--- a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/portfolio/bounded25.kt
+++ b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/portfolio/bounded25.kt
@@ -59,6 +59,7 @@ fun boundedPortfolio25(
backendConfig =
BackendConfig(
backend = Backend.BOUNDED,
+ memlimit = portfolioConfig.backendConfig.memlimit,
solverHome = portfolioConfig.backendConfig.solverHome,
timeoutMs = 0,
specConfig =
@@ -79,6 +80,9 @@ fun boundedPortfolio25(
disable = false,
concretizerSolver = "Z3",
validateConcretizerSolver = false,
+ inputFileForWitness =
+ portfolioConfig.outputConfig.witnessConfig.inputFileForWitness
+ ?: portfolioConfig.inputConfig.input,
),
argConfig = ArgConfig(disable = true),
enableOutput = portfolioConfig.outputConfig.enableOutput,
@@ -93,6 +97,7 @@ fun boundedPortfolio25(
backendConfig =
BackendConfig(
backend = Backend.MDD,
+ memlimit = portfolioConfig.backendConfig.memlimit / 5 * 4,
solverHome = portfolioConfig.backendConfig.solverHome,
timeoutMs = 0,
specConfig =
@@ -375,7 +380,8 @@ fun boundedPortfolio25(
edges.add(Edge(bmcConfig, indConfig, if (inProcess) timeoutOrNotSolvableError else anyError))
edges.add(Edge(indConfig, imcConfig, if (inProcess) timeoutOrNotSolvableError else anyError))
- return STM(mddConfig, edges)
+ return if (inProcess) STM(mddConfig, edges)
+ else STM(bmcConfig, edges) // mdd should not be run not-in-proc
}
logger.write(Logger.Level.RESULT, "Using bounded portfolio\n")
diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/portfolio/complex25.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/portfolio/complex25.kt
index 03cff34e47..738b0da018 100644
--- a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/portfolio/complex25.kt
+++ b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/portfolio/complex25.kt
@@ -117,6 +117,9 @@ fun complexPortfolio25(
disable = false,
concretizerSolver = "Z3",
validateConcretizerSolver = false,
+ inputFileForWitness =
+ portfolioConfig.outputConfig.witnessConfig.inputFileForWitness
+ ?: portfolioConfig.inputConfig.input,
),
argConfig = ArgConfig(disable = true),
enableOutput = portfolioConfig.outputConfig.enableOutput,
@@ -135,7 +138,7 @@ fun complexPortfolio25(
BackendConfig(
backend = OC,
solverHome = baseConfig.backendConfig.solverHome,
- timeoutMs = 400_000,
+ timeoutMs = 500_000,
inProcess = inProcess,
specConfig = OcConfig(autoConflict = RF_WS_FR),
),
diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/portfolio/horn25.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/portfolio/horn25.kt
index 04293c36bb..749a43d6da 100644
--- a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/portfolio/horn25.kt
+++ b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/portfolio/horn25.kt
@@ -71,6 +71,9 @@ fun hornPortfolio25(
disable = false,
concretizerSolver = "Z3",
validateConcretizerSolver = false,
+ inputFileForWitness =
+ portfolioConfig.outputConfig.witnessConfig.inputFileForWitness
+ ?: portfolioConfig.inputConfig.input,
),
argConfig = ArgConfig(disable = true),
enableOutput = portfolioConfig.outputConfig.enableOutput,
diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/utils/GraphmlWitnessWriter.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/utils/GraphmlWitnessWriter.kt
index 264f014285..cf7a650b0b 100644
--- a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/utils/GraphmlWitnessWriter.kt
+++ b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/utils/GraphmlWitnessWriter.kt
@@ -21,6 +21,7 @@ import hu.bme.mit.theta.analysis.expl.ExplState
import hu.bme.mit.theta.analysis.ptr.PtrState
import hu.bme.mit.theta.frontend.ParseContext
import hu.bme.mit.theta.solver.SolverFactory
+import hu.bme.mit.theta.xcfa.analysis.ErrorDetection
import hu.bme.mit.theta.xcfa.analysis.XcfaAction
import hu.bme.mit.theta.xcfa.analysis.XcfaState
import hu.bme.mit.theta.xcfa.cli.witnesses.GraphmlWitness
@@ -42,6 +43,7 @@ class GraphmlWitnessWriter {
cexSolverFactory: SolverFactory,
parseContext: ParseContext,
witnessfile: File,
+ property: ErrorDetection,
) {
// TODO eliminate the need for the instanceof check
if (safetyResult.isUnsafe && safetyResult.asUnsafe().cex is Trace<*, *>) {
@@ -52,7 +54,8 @@ class GraphmlWitnessWriter {
parseContext,
)
- val witnessTrace = traceToWitness(trace = concrTrace, parseContext = parseContext)
+ val witnessTrace =
+ traceToWitness(trace = concrTrace, parseContext = parseContext, property = property)
val graphmlWitness = GraphmlWitness(witnessTrace, inputFile)
val xml = graphmlWitness.toPrettyXml()
witnessfile.writeText(xml)
diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/utils/YmlWitnessWriter.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/utils/YmlWitnessWriter.kt
index f1d2efd0fb..e0d79da9eb 100644
--- a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/utils/YmlWitnessWriter.kt
+++ b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/utils/YmlWitnessWriter.kt
@@ -36,6 +36,7 @@ import hu.bme.mit.theta.xcfa.model.MetaData
import hu.bme.mit.theta.xcfa.toC
import java.io.File
import java.util.*
+import kotlinx.serialization.encodeToString
class YmlWitnessWriter {
@@ -61,7 +62,7 @@ class YmlWitnessWriter {
task =
Task(
inputFiles = listOf(inputFile.name),
- inputFileHashes = listOf(createTaskHash(inputFile.path)),
+ inputFileHashes = mapOf(Pair(inputFile.path, createTaskHash(inputFile.path))),
specification = property.name,
dataModel =
architecture?.let {
@@ -80,7 +81,8 @@ class YmlWitnessWriter {
parseContext,
)
- val witnessTrace = traceToWitness(trace = concrTrace, parseContext = parseContext)
+ val witnessTrace =
+ traceToWitness(trace = concrTrace, parseContext = parseContext, property = property)
val witness =
YamlWitness(
@@ -97,7 +99,7 @@ class YmlWitnessWriter {
},
)
- witnessfile.writeText(WitnessYamlConfig.encodeToString(YamlWitness.serializer(), witness))
+ witnessfile.writeText(WitnessYamlConfig.encodeToString(listOf(witness)))
} else if (safetyResult.isSafe) {
val witness =
@@ -107,7 +109,7 @@ class YmlWitnessWriter {
content = safetyResult.asSafe().proof.toContent(inputFile, parseContext),
)
- witnessfile.writeText(WitnessYamlConfig.encodeToString(YamlWitness.serializer(), witness))
+ witnessfile.writeText(WitnessYamlConfig.encodeToString(listOf(witness)))
}
}
}
@@ -141,7 +143,7 @@ private fun WitnessNode.toSegment(witnessEdge: WitnessEdge?, inputFile: File): C
?: getLocation(inputFile, witnessEdge?.edge?.metadata)
?: return null
return ContentItem(
- Segment(Waypoint(type = WaypointType.TARGET, location = locLoc, action = Action.FOLLOW))
+ WaypointContent(type = WaypointType.TARGET, location = locLoc, action = Action.FOLLOW)
)
} else {
return null
@@ -179,7 +181,7 @@ private fun WitnessEdge.toSegment(inputFile: File): ContentItem? {
Triple(endLoc, Constraint(value = returnFromFunction), WaypointType.FUNCTION_RETURN)
} else return null
return ContentItem(
- Segment(Waypoint(type = type, constraint = constraint, location = loc, action = Action.FOLLOW))
+ WaypointContent(type = type, constraint = constraint, location = loc, action = Action.FOLLOW)
)
}
diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/witnesses/TraceToWitness.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/witnesses/TraceToWitness.kt
index 48c1ea369b..eb224355de 100644
--- a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/witnesses/TraceToWitness.kt
+++ b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/witnesses/TraceToWitness.kt
@@ -18,6 +18,7 @@ package hu.bme.mit.theta.xcfa.cli.witnesses
import com.google.common.collect.Lists
import hu.bme.mit.theta.analysis.Trace
import hu.bme.mit.theta.analysis.expl.ExplState
+import hu.bme.mit.theta.analysis.ptr.PtrState
import hu.bme.mit.theta.c2xcfa.getCMetaData
import hu.bme.mit.theta.core.model.Valuation
import hu.bme.mit.theta.core.stmt.HavocStmt
@@ -25,8 +26,10 @@ import hu.bme.mit.theta.core.type.LitExpr
import hu.bme.mit.theta.core.type.bvtype.BvLitExpr
import hu.bme.mit.theta.core.type.fptype.FpLitExpr
import hu.bme.mit.theta.frontend.ParseContext
+import hu.bme.mit.theta.xcfa.analysis.ErrorDetection
import hu.bme.mit.theta.xcfa.analysis.XcfaAction
import hu.bme.mit.theta.xcfa.analysis.XcfaState
+import hu.bme.mit.theta.xcfa.analysis.getXcfaErrorPredicate
import hu.bme.mit.theta.xcfa.model.*
import java.math.BigInteger
@@ -41,10 +44,13 @@ fun traceToWitness(
verbosity: Verbosity = Verbosity.SOURCE_EXISTS,
trace: Trace, XcfaAction>,
parseContext: ParseContext,
+ property: ErrorDetection,
): Trace {
val newStates = ArrayList()
val newActions = ArrayList()
+ val isError = getXcfaErrorPredicate(property)
+
var lastNode =
WitnessNode(id = "N${newStates.size}", entry = true, sink = false, violation = false)
newStates.add(lastNode)
@@ -59,7 +65,17 @@ fun traceToWitness(
id = "N${newStates.size}",
entry = false,
sink = false,
- violation = state.processes.any { it.value.locs.any(XcfaLocation::error) },
+ violation =
+ isError.test( // this is a hack so that a simple explstate can become a ptrstate
+ XcfaState(
+ state.xcfa,
+ state.processes,
+ PtrState(state.sGlobal),
+ state.mutexes,
+ state.threadLookup,
+ state.bottom,
+ )
+ ),
xcfaLocations = state.processes.map { Pair(it.key, it.value.locs) }.toMap(),
cSources =
state.processes
@@ -113,7 +129,17 @@ fun traceToWitness(
id = "N${newStates.size}",
entry = false,
sink = false,
- violation = lastState.processes.any { it.value.locs.any(XcfaLocation::error) },
+ violation =
+ isError.test( // this is a hack so that a simple explstate can become a ptrstate
+ XcfaState(
+ lastState.xcfa,
+ lastState.processes,
+ PtrState(lastState.sGlobal),
+ lastState.mutexes,
+ lastState.threadLookup,
+ lastState.bottom,
+ )
+ ),
xcfaLocations = lastState.processes.map { Pair(it.key, it.value.locs) }.toMap(),
cSources =
lastState.processes
diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/witnesses/XcfaTraceConcretizer.java b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/witnesses/XcfaTraceConcretizer.java
index ab8faa04bd..6bcc2f9eff 100644
--- a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/witnesses/XcfaTraceConcretizer.java
+++ b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/witnesses/XcfaTraceConcretizer.java
@@ -91,7 +91,7 @@ public static Trace, XcfaAction> concretize(
for (int i = 0; i < sbeTrace.getStates().size(); ++i) {
cfaStates.add(
new XcfaState<>(
- null,
+ sbeTrace.getState(i).getXcfa(),
sbeTrace.getState(i).getProcesses(),
ExplState.of(
ImmutableValuation.from(
diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/witnesses/YamlWitness.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/witnesses/YamlWitness.kt
index 15fa63eada..e99e41771b 100644
--- a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/witnesses/YamlWitness.kt
+++ b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/witnesses/YamlWitness.kt
@@ -107,7 +107,7 @@ data class Producer(
@Serializable
data class Task(
@SerialName("input_files") val inputFiles: List,
- @SerialName("input_file_hashes") val inputFileHashes: List,
+ @SerialName("input_file_hashes") val inputFileHashes: Map,
val specification: String,
@SerialName("data_model") val dataModel: DataModel,
val language: Language,
@@ -156,9 +156,13 @@ enum class Language {
* a mapping that describes one invariant.
*/
@Serializable
-data class ContentItem(val segment: Segment? = null, val invariant: Invariant? = null)
+data class ContentItem(val segment: Segment? = null, val invariant: Invariant? = null) {
+ constructor(wpContent: WaypointContent) : this(listOf(Waypoint(wpContent)))
+}
+
+typealias Segment = List
-@Serializable data class Segment(val waypoint: Waypoint)
+@Serializable data class Waypoint(val waypoint: WaypointContent)
/**
* The `waypoint` elements are the basic building block of violation witnesses. They have the form
@@ -223,7 +227,7 @@ data class ContentItem(val segment: Segment? = null, val invariant: Invariant? =
* means that the waypoint should be avoided.
*/
@Serializable
-data class Waypoint(
+data class WaypointContent(
val type: WaypointType,
val constraint: Constraint? = null,
val location: Location,
diff --git a/subprojects/xcfa/xcfa-cli/src/test/java/hu/bme/mit/theta/xcfa/cli/YamlParseTest.kt b/subprojects/xcfa/xcfa-cli/src/test/java/hu/bme/mit/theta/xcfa/cli/YamlParseTest.kt
index 6744a352b0..43cc33b88a 100644
--- a/subprojects/xcfa/xcfa-cli/src/test/java/hu/bme/mit/theta/xcfa/cli/YamlParseTest.kt
+++ b/subprojects/xcfa/xcfa-cli/src/test/java/hu/bme/mit/theta/xcfa/cli/YamlParseTest.kt
@@ -36,7 +36,7 @@ class YamlParseTest {
task =
Task(
inputFiles = listOf("example.c"),
- inputFileHashes = listOf("hash"),
+ inputFileHashes = mapOf(Pair("example.c", "hash")),
specification = "unreach_call",
dataModel = DataModel.LP64,
language = Language.C,
@@ -45,13 +45,11 @@ class YamlParseTest {
content =
listOf(
ContentItem(
- Segment(
- Waypoint(
- type = WaypointType.ASSUMPTION,
- constraint = Constraint(value = "1 < x", format = Format.C_EXPRESSION),
- location = Location(fileName = "example.c", line = 15),
- action = Action.FOLLOW,
- )
+ WaypointContent(
+ type = WaypointType.ASSUMPTION,
+ constraint = Constraint(value = "1 < x", format = Format.C_EXPRESSION),
+ location = Location(fileName = "example.c", line = 15),
+ action = Action.FOLLOW,
)
)
),