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 40beac15bd..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 @@ -462,6 +462,7 @@ private fun postVerificationLogging( ), parseContext, witnessFile, + config.inputConfig.property, ) val yamlWitnessFile = File(resultFolder, "witness.yml") YmlWitnessWriter() 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..b8d9c6acd8 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 @@ -24,15 +24,17 @@ import hu.bme.mit.theta.analysis.algorithm.chc.HornChecker 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.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,10 +62,44 @@ 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()) + 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) + } + + SafetyResult.unsafe(Trace.of(states.reversed(), actions.reversed()), EmptyProof.getInstance()) } else { SafetyResult.unknown() } 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 841e1b57f7..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 @@ -81,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( 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(