From 55203605edc45b345b7f50c70b0b7f71e070b88c Mon Sep 17 00:00:00 2001 From: AdamZsofi Date: Sun, 27 Oct 2024 20:20:03 +0100 Subject: [PATCH] tracegen added to xcfa execute config --- .../tracegeneration/DoubleEndNodeRemover.kt | 121 +++ .../tracegeneration/TraceGenerationChecker.kt | 16 +- .../XstsDoubleEndNodeRemover.java | 112 --- .../summary/AbstractTraceSummary.kt | 4 +- .../summary/TraceGenerationResult.kt | 4 +- .../bme/mit/theta/xcfa/cli/ExecuteConfig.kt | 736 ++++++++++-------- .../xcfa/cli/checkers/ConfigToChecker.kt | 3 +- .../cli/checkers/ConfigToTracegenChecker.kt | 18 +- .../tracegeneration/XstsTracegenBuilder.kt | 12 +- 9 files changed, 561 insertions(+), 465 deletions(-) create mode 100644 subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/tracegeneration/DoubleEndNodeRemover.kt delete mode 100644 subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/tracegeneration/XstsDoubleEndNodeRemover.java diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/tracegeneration/DoubleEndNodeRemover.kt b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/tracegeneration/DoubleEndNodeRemover.kt new file mode 100644 index 0000000000..12680f3bd4 --- /dev/null +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/tracegeneration/DoubleEndNodeRemover.kt @@ -0,0 +1,121 @@ +/* + * Copyright 2024 Budapest University of Technology and Economics + * + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ + +package hu.bme.mit.theta.analysis.algorithm.tracegeneration + +import hu.bme.mit.theta.analysis.Action +import hu.bme.mit.theta.analysis.State +import hu.bme.mit.theta.analysis.Trace +import hu.bme.mit.theta.analysis.algorithm.arg.ARG +import hu.bme.mit.theta.analysis.algorithm.arg.ArgNode +import hu.bme.mit.theta.analysis.expr.StmtAction +import java.io.BufferedReader +import java.io.IOException +import java.io.StringReader + +class DoubleEndNodeRemover { + + private fun isLastInternal(node: ArgNode): Boolean { + return node.state.toString().contains("last_internal") + } + + private fun isBadLeaf(node: ArgNode): Boolean { + if (isLastInternal(node)) { + if (node.parent.isEmpty) return false + val parent = node.parent.get() + if (parent.parent.isEmpty) return false + val grandParent = node.parent.get().parent.get() + return if (node.isCovered && parent.parent.get() == node.coveringNode.get()) { // node is covered and parent is checked above + // bad node + true + } else { + false + } + } else { + var transitionFired = false + if (node.parent.isPresent && node.parent.get().parent.isPresent) { + val grandParent = node.parent.get().parent.get() + if (!(node.isCovered && node.coveringNode.get() == grandParent)) return false + + val state = node.parent.get().state.toString() + val bufReader = BufferedReader(StringReader(state)) + var line: String? = null + try { + while ((bufReader.readLine().also { line = it }) != null) { + if (line!!.trim { it <= ' ' } + .matches("^.*\\(__id_.*__.*\\strue\\).*$".toRegex())) transitionFired = true + } + } catch (e: IOException) { + e.printStackTrace() + } + return !transitionFired // if no transition was fired (and state not changed), this is a superfluous node + } else { + return false + } + } + } + + companion object { + + /** + * Mainly of use for XSTS! + * Collecting nodes that look like there should be traces to it, but shouldn't ("not firing anything" nodes) + * This should most likely note come up with other formalisms. This removal is executed on them anyways. + */ + fun collectBadLeaves(arg: ARG): List> { + val instance = DoubleEndNodeRemover() + val badNodes: MutableList> = ArrayList() + arg.nodes.filter { obj: ArgNode -> obj.isLeaf }.forEach { node: ArgNode -> + if (instance.isBadLeaf(node)) { + badNodes.add(node) + } + } + return badNodes + } + + fun filterSuperfluousEndNode(trace: Trace): Trace { + if (trace.states.size > 3) { + var transitionFired = false + val size = trace.states.size + if (trace.getState(size - 1).toString() == trace.getState(size - 3).toString()) { + val bufReader = BufferedReader(StringReader(trace.getState(size - 2).toString())) + var line: String? = null + try { + while ((bufReader.readLine().also { line = it }) != null) { + if (line!!.trim { it <= ' ' } + .matches("^\\(__id_.*__.*\\strue\\)*$".toRegex())) transitionFired = true + } + } catch (e: IOException) { + e.printStackTrace() + } + } + if (!transitionFired) { + val newStates = ArrayList(trace.states) + newStates.removeAt(newStates.size - 1) + newStates.removeAt(newStates.size - 1) + val newActions = ArrayList(trace.actions) + newActions.removeAt(newActions.size - 1) + newActions.removeAt(newActions.size - 1) + return Trace.of(newStates, newActions) + } else { + return trace + } + } else { + return trace + } + } + } +} \ No newline at end of file diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/tracegeneration/TraceGenerationChecker.kt b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/tracegeneration/TraceGenerationChecker.kt index 178e113396..24f48b10a7 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/tracegeneration/TraceGenerationChecker.kt +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/tracegeneration/TraceGenerationChecker.kt @@ -5,7 +5,7 @@ import hu.bme.mit.theta.analysis.* import hu.bme.mit.theta.analysis.algorithm.* import hu.bme.mit.theta.analysis.algorithm.arg.ArgNode import hu.bme.mit.theta.analysis.algorithm.arg.ArgTrace -import hu.bme.mit.theta.analysis.algorithm.cegar.Abstractor +import hu.bme.mit.theta.analysis.algorithm.cegar.BasicArgAbstractor import hu.bme.mit.theta.analysis.algorithm.tracegeneration.summary.TraceGenerationResult import hu.bme.mit.theta.analysis.algorithm.tracegeneration.summary.AbstractSummaryBuilder import hu.bme.mit.theta.analysis.algorithm.tracegeneration.summary.AbstractTraceSummary @@ -15,7 +15,7 @@ import kotlin.collections.ArrayList class TraceGenerationChecker( private val logger: Logger, - private val abstractor: Abstractor, + private val abstractor: BasicArgAbstractor, private val getFullTraces : Boolean, ) : Checker, P> { private var traces: List> = ArrayList() @@ -23,7 +23,7 @@ class TraceGenerationChecker( companion object { fun create( logger: Logger, - abstractor: Abstractor, + abstractor: BasicArgAbstractor, getFullTraces: Boolean ): TraceGenerationChecker { return TraceGenerationChecker(logger, abstractor, getFullTraces) @@ -34,17 +34,15 @@ class TraceGenerationChecker( logger.write(Logger.Level.SUBSTEP, "Printing prec for trace generation...\n" + System.lineSeparator()) logger.write(Logger.Level.SUBSTEP, prec.toString()) - val arg = abstractor.createArg() + val arg = abstractor.createProof() abstractor.check(arg, prec) - logger.write(Logger.Level.SUBSTEP, "ARG done, fetching traces...\n") - // TODO remove xsts specific parts - - // bad node: XSTS specific thing, that the last state (last_env nodes) doubles up and the leaf is covered by the + // bad node: mostly XSTS specific thing, that the last state (last_env nodes) doubles up and the leaf is covered by the // last_env before which is superfluous. // Possible side effect if not handled: possibly a "non-existing leaf" and superfluous traces or just traces that are 1 longer than they should be - val badNodes = XstsDoubleEndNodeRemover.collectBadLeaves(arg) + val badNodes = DoubleEndNodeRemover.collectBadLeaves(arg) + logger.write(Logger.Level.INFO, "Number of bad nodes filtered out: ${badNodes.size}") // leaves val endNodes = arg.nodes.filter { obj: ArgNode -> obj.isLeaf } diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/tracegeneration/XstsDoubleEndNodeRemover.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/tracegeneration/XstsDoubleEndNodeRemover.java deleted file mode 100644 index ebd89505aa..0000000000 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/tracegeneration/XstsDoubleEndNodeRemover.java +++ /dev/null @@ -1,112 +0,0 @@ -/* - * Copyright 2024 Budapest University of Technology and Economics - * - * Licensed under the Apache License, Version 2.0 (the "License"); - * you may not use this file except in compliance with the License. - * You may obtain a copy of the License at - * - * http://www.apache.org/licenses/LICENSE-2.0 - * - * Unless required by applicable law or agreed to in writing, software - * distributed under the License is distributed on an "AS IS" BASIS, - * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. - * See the License for the specific language governing permissions and - * limitations under the License. - */ - -package hu.bme.mit.theta.analysis.algorithm.tracegeneration; - -import hu.bme.mit.theta.analysis.Action; -import hu.bme.mit.theta.analysis.State; -import hu.bme.mit.theta.analysis.Trace; -import hu.bme.mit.theta.analysis.algorithm.arg.ARG; -import hu.bme.mit.theta.analysis.algorithm.arg.ArgNode; -import hu.bme.mit.theta.analysis.expr.StmtAction; - -import java.io.BufferedReader; -import java.io.IOException; -import java.io.StringReader; -import java.util.ArrayList; -import java.util.List; - -public class XstsDoubleEndNodeRemover { - static List> collectBadLeaves(ARG arg) { - // TODO XSTS SPECIFIC for now! collecting nodes that look like there should be traces to it, but shouldn't ("not firing anything" nodes) - XstsDoubleEndNodeRemover instance = new XstsDoubleEndNodeRemover(); - List> badNodes = new ArrayList<>(); - arg.getNodes().filter(ArgNode::isLeaf).forEach(node -> { - if(instance.isBadLeaf(node)) { badNodes.add(node); } - } ); - return badNodes; - } - - private boolean isLastInternal(ArgNode node) { - return node.getState().toString().contains("last_internal"); - } - - private boolean isBadLeaf(ArgNode node) { - if(isLastInternal(node)) { - if(node.getParent().isEmpty()) return false; - ArgNode parent = node.getParent().get(); - if(parent.getParent().isEmpty()) return false; - ArgNode grandParent = node.getParent().get().getParent().get(); - if(node.isCovered() && parent.getParent().get() == node.getCoveringNode().get()) { // node is covered and parent is checked above - // bad node - return true; - } else { - return false; - } - } else { - boolean transitionFired = false; - if(node.getParent().isPresent() && node.getParent().get().getParent().isPresent()) { - ArgNode grandParent = node.getParent().get().getParent().get(); - if(!(node.isCovered() && node.getCoveringNode().get()==grandParent)) return false; - - String state = node.getParent().get().getState().toString(); - BufferedReader bufReader = new BufferedReader(new StringReader(state)); - String line=null; - try { - while( (line=bufReader.readLine()) != null ) { - if(line.trim().matches("^.*\\(__id_.*__.*\strue\\).*$")) transitionFired=true; - } - } catch (IOException e) { - e.printStackTrace(); - } - return !transitionFired; // if no transition was fired (and state not changed), this is a superfluous node - } else { - return false; - } - } - } - - static Trace filterSuperfluousEndNode(Trace trace) { - if(trace.getStates().size()>3) { - boolean transitionFired = false; - int size = trace.getStates().size(); - if(trace.getState(size-1).toString().equals(trace.getState(size-3).toString())) { - BufferedReader bufReader = new BufferedReader(new StringReader(trace.getState(size-2).toString())); - String line=null; - try { - while( (line=bufReader.readLine()) != null ) { - if(line.trim().matches("^\\(__id_.*__.*\strue\\)*$")) transitionFired=true; - } - } catch (IOException e) { - e.printStackTrace(); - } - } - if(!transitionFired) { - ArrayList newStates = new ArrayList<>(trace.getStates()); - newStates.remove(newStates.size()-1); - newStates.remove(newStates.size()-1); - ArrayList newActions = new ArrayList<>(trace.getActions()); - newActions.remove(newActions.size()-1); - newActions.remove(newActions.size()-1); - return Trace.of(newStates, newActions); - } else { - return trace; - } - } else { - return trace; - } - } -} diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/tracegeneration/summary/AbstractTraceSummary.kt b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/tracegeneration/summary/AbstractTraceSummary.kt index 13a5200383..5c84757109 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/tracegeneration/summary/AbstractTraceSummary.kt +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/tracegeneration/summary/AbstractTraceSummary.kt @@ -19,7 +19,7 @@ package hu.bme.mit.theta.analysis.algorithm.tracegeneration.summary import com.google.common.base.Preconditions.checkState import hu.bme.mit.theta.analysis.Action import hu.bme.mit.theta.analysis.State -import hu.bme.mit.theta.analysis.algorithm.Witness +import hu.bme.mit.theta.analysis.algorithm.Proof import hu.bme.mit.theta.analysis.algorithm.arg.ArgEdge import hu.bme.mit.theta.analysis.algorithm.arg.ArgNode import hu.bme.mit.theta.analysis.algorithm.arg.ArgTrace @@ -110,7 +110,7 @@ data class AbstractTraceSummary ( val abstractSummaryEdges : Collection>, val summaryNodes : Collection>, val initNode : AbstractSummaryNode - ) : Witness { + ) : Proof { } /** diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/tracegeneration/summary/TraceGenerationResult.kt b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/tracegeneration/summary/TraceGenerationResult.kt index f638d9d503..ce633b2c7a 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/tracegeneration/summary/TraceGenerationResult.kt +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/tracegeneration/summary/TraceGenerationResult.kt @@ -22,9 +22,9 @@ import hu.bme.mit.theta.analysis.algorithm.Result import hu.bme.mit.theta.analysis.algorithm.Statistics import java.util.* -class TraceGenerationResult, S : State, A : Action>(val summary : W) : Result { +class TraceGenerationResult, S : State, A : Action>(val summary : Pr) : Result { - override fun getWitness(): W { + override fun getProof(): Pr { return summary } 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 c7027914fc..ec37a3bf42 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 @@ -22,12 +22,18 @@ import hu.bme.mit.theta.analysis.Action import hu.bme.mit.theta.analysis.EmptyCex import hu.bme.mit.theta.analysis.State import hu.bme.mit.theta.analysis.Trace -import hu.bme.mit.theta.analysis.algorithm.EmptyProof -import hu.bme.mit.theta.analysis.algorithm.SafetyResult +import hu.bme.mit.theta.analysis.algorithm.* import hu.bme.mit.theta.analysis.algorithm.arg.ARG import hu.bme.mit.theta.analysis.algorithm.arg.debug.ARGWebDebugger +import hu.bme.mit.theta.analysis.algorithm.tracegeneration.TraceGenerationChecker +import hu.bme.mit.theta.analysis.algorithm.tracegeneration.summary.AbstractSummaryNode +import hu.bme.mit.theta.analysis.algorithm.tracegeneration.summary.AbstractTraceSummary +import hu.bme.mit.theta.analysis.algorithm.tracegeneration.summary.TraceGenerationResult +import hu.bme.mit.theta.analysis.expl.ExplPrec import hu.bme.mit.theta.analysis.expl.ExplState +import hu.bme.mit.theta.analysis.ptr.PtrPrec import hu.bme.mit.theta.analysis.ptr.PtrState +import hu.bme.mit.theta.analysis.utils.AbstractTraceSummaryVisualizer import hu.bme.mit.theta.analysis.utils.ArgVisualizer import hu.bme.mit.theta.analysis.utils.TraceVisualizer import hu.bme.mit.theta.c2xcfa.CMetaData @@ -42,6 +48,7 @@ import hu.bme.mit.theta.frontend.ParseContext import hu.bme.mit.theta.graphsolver.patterns.constraints.MCM import hu.bme.mit.theta.xcfa.analysis.ErrorDetection 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.coi.ConeOfInfluence import hu.bme.mit.theta.xcfa.analysis.coi.XcfaCoiMultiThread @@ -52,6 +59,7 @@ import hu.bme.mit.theta.xcfa.cli.checkers.getChecker import hu.bme.mit.theta.xcfa.cli.params.* import hu.bme.mit.theta.xcfa.cli.utils.* import hu.bme.mit.theta.xcfa.cli.witnesses.XcfaTraceConcretizer +import hu.bme.mit.theta.xcfa.collectVars import hu.bme.mit.theta.xcfa.getFlatLabels import hu.bme.mit.theta.xcfa.model.XCFA import hu.bme.mit.theta.xcfa.model.XcfaLabel @@ -67,379 +75,463 @@ import java.util.concurrent.TimeUnit import kotlin.random.Random fun runConfig( - config: XcfaConfig<*, *>, - logger: Logger, - uniqueLogger: Logger, - throwDontExit: Boolean, -): SafetyResult<*, *> { - propagateInputOptions(config, logger, uniqueLogger) + config: XcfaConfig<*, *>, + logger: Logger, + uniqueLogger: Logger, + throwDontExit: Boolean, +): Result<*> { + propagateInputOptions(config, logger, uniqueLogger) - registerAllSolverManagers(config.backendConfig.solverHome, logger) + registerAllSolverManagers(config.backendConfig.solverHome, logger) - validateInputOptions(config, logger, uniqueLogger) + validateInputOptions(config, logger, uniqueLogger) - val (xcfa, mcm, parseContext) = frontend(config, logger, uniqueLogger) + val (xcfa, mcm, parseContext) = frontend(config, logger, uniqueLogger) - preVerificationLogging(xcfa, mcm, parseContext, config, logger, uniqueLogger) + preAnalysisLogging(xcfa, mcm, parseContext, config, logger, uniqueLogger) - val result = backend(xcfa, mcm, parseContext, config, logger, uniqueLogger, throwDontExit) + val result = backend(xcfa, mcm, parseContext, config, logger, uniqueLogger, throwDontExit) - postVerificationLogging(result, mcm, parseContext, config, logger, uniqueLogger) + // TODO tracegen: write to file and log + postAnalysisLogging(result, mcm, parseContext, config, logger, uniqueLogger) - return result + return result } private fun propagateInputOptions(config: XcfaConfig<*, *>, logger: Logger, uniqueLogger: Logger) { - config.inputConfig.property = determineProperty(config, logger) - LbePass.level = config.frontendConfig.lbeLevel - StaticCoiPass.enabled = config.frontendConfig.staticCoi - if (config.backendConfig.backend == Backend.CEGAR) { - val cegarConfig = config.backendConfig.specConfig - cegarConfig as CegarConfig - val random = Random(cegarConfig.porRandomSeed) - XcfaSporLts.random = random - XcfaDporLts.random = random - } - if (config.debugConfig.argToFile) { - WebDebuggerLogger.enableWebDebuggerLogger() - WebDebuggerLogger.getInstance().setTitle(config.inputConfig.input?.name) - } - - LoopUnrollPass.UNROLL_LIMIT = config.frontendConfig.loopUnroll - LoopUnrollPass.FORCE_UNROLL_LIMIT = config.frontendConfig.forceUnroll - FetchExecuteWriteback.enabled = config.frontendConfig.enableFew - ARGWebDebugger.on = config.debugConfig.argdebug + config.inputConfig.property = determineProperty(config, logger) + LbePass.level = config.frontendConfig.lbeLevel + StaticCoiPass.enabled = config.frontendConfig.staticCoi + if (config.backendConfig.backend == Backend.CEGAR) { + val cegarConfig = config.backendConfig.specConfig + cegarConfig as CegarConfig + val random = Random(cegarConfig.porRandomSeed) + XcfaSporLts.random = random + XcfaDporLts.random = random + } + if (config.debugConfig.argToFile) { + WebDebuggerLogger.enableWebDebuggerLogger() + WebDebuggerLogger.getInstance().setTitle(config.inputConfig.input?.name) + } + + LoopUnrollPass.UNROLL_LIMIT = config.frontendConfig.loopUnroll + LoopUnrollPass.FORCE_UNROLL_LIMIT = config.frontendConfig.forceUnroll + FetchExecuteWriteback.enabled = config.frontendConfig.enableFew + ARGWebDebugger.on = config.debugConfig.argdebug } private fun validateInputOptions(config: XcfaConfig<*, *>, logger: Logger, uniqueLogger: Logger) { - rule("NoCoiWhenDataRace") { - config.backendConfig.backend == Backend.CEGAR && - (config.backendConfig.specConfig as? CegarConfig)?.coi != ConeOfInfluenceMode.NO_COI && - config.inputConfig.property == ErrorDetection.DATA_RACE - } - rule("NoAaporWhenDataRace") { - (config.backendConfig.specConfig as? CegarConfig)?.porLevel?.isAbstractionAware == true && - config.inputConfig.property == ErrorDetection.DATA_RACE - } - rule("DPORWithoutDFS") { - (config.backendConfig.specConfig as? CegarConfig)?.porLevel?.isDynamic == true && - (config.backendConfig.specConfig as? CegarConfig)?.abstractorConfig?.search != Search.DFS - } - rule("SensibleLoopUnrollLimits") { - config.frontendConfig.loopUnroll != -1 && - config.frontendConfig.loopUnroll < config.frontendConfig.forceUnroll - } - rule("NoPredSplitUntilFixed(https://github.com/ftsrg/theta/issues/267)") { - (config.backendConfig.specConfig as? CegarConfig)?.abstractorConfig?.domain == Domain.PRED_SPLIT - } + rule("NoCoiWhenDataRace") { + config.backendConfig.backend == Backend.CEGAR && + (config.backendConfig.specConfig as? CegarConfig)?.coi != ConeOfInfluenceMode.NO_COI && + config.inputConfig.property == ErrorDetection.DATA_RACE + } + rule("NoAaporWhenDataRace") { + (config.backendConfig.specConfig as? CegarConfig)?.porLevel?.isAbstractionAware == true && + config.inputConfig.property == ErrorDetection.DATA_RACE + } + rule("DPORWithoutDFS") { + (config.backendConfig.specConfig as? CegarConfig)?.porLevel?.isDynamic == true && + (config.backendConfig.specConfig as? CegarConfig)?.abstractorConfig?.search != Search.DFS + } + rule("SensibleLoopUnrollLimits") { + config.frontendConfig.loopUnroll != -1 && + config.frontendConfig.loopUnroll < config.frontendConfig.forceUnroll + } + rule("NoPredSplitUntilFixed(https://github.com/ftsrg/theta/issues/267)") { + (config.backendConfig.specConfig as? CegarConfig)?.abstractorConfig?.domain == Domain.PRED_SPLIT + } } fun frontend( - config: XcfaConfig<*, *>, - logger: Logger, - uniqueLogger: Logger, + config: XcfaConfig<*, *>, + logger: Logger, + uniqueLogger: Logger, ): Triple { - if (config.inputConfig.xcfaWCtx != null) { - val xcfa = config.inputConfig.xcfaWCtx!!.first - ConeOfInfluence = - if (config.inputConfig.xcfaWCtx!!.third.multiThreading) { - XcfaCoiMultiThread(xcfa) - } else { - XcfaCoiSingleThread(xcfa) - } - return config.inputConfig.xcfaWCtx!! - } - - val stopwatch = Stopwatch.createStarted() - - val input = config.inputConfig.input!! - logger.write( - Logger.Level.INFO, - "Parsing the input $input as ${config.frontendConfig.inputType}\n", - ) - - val parseContext = ParseContext() - - if (config.frontendConfig.inputType == InputType.C) { - val cConfig = config.frontendConfig.specConfig - cConfig as CFrontendConfig - parseContext.arithmetic = cConfig.arithmetic - parseContext.architecture = cConfig.architecture - } - - val xcfa = getXcfa(config, parseContext, logger, uniqueLogger) - - val mcm = - if (config.inputConfig.catFile != null) { - CatDslManager.createMCM(config.inputConfig.catFile!!) - } else { - emptySet() + if (config.inputConfig.xcfaWCtx != null) { + val xcfa = config.inputConfig.xcfaWCtx!!.first + ConeOfInfluence = + if (config.inputConfig.xcfaWCtx!!.third.multiThreading) { + XcfaCoiMultiThread(xcfa) + } else { + XcfaCoiSingleThread(xcfa) + } + return config.inputConfig.xcfaWCtx!! } - ConeOfInfluence = - if (parseContext.multiThreading) XcfaCoiMultiThread(xcfa) else XcfaCoiSingleThread(xcfa) - - if ( - parseContext.multiThreading && - (config.backendConfig.specConfig as? CegarConfig)?.let { - it.abstractorConfig.search == Search.ERR - } == true - ) { - val cConfig = config.backendConfig.specConfig as CegarConfig - cConfig.abstractorConfig.search = Search.DFS - uniqueLogger.write(INFO, "Multithreaded program found, using DFS instead of ERR.") - } - - logger.write( - Logger.Level.INFO, - "Frontend finished: ${xcfa.name} (in ${ - stopwatch.elapsed(TimeUnit.MILLISECONDS) - } ms)\n", - ) - - logger.write(RESULT, "ParsingResult Success\n") - logger.write( - RESULT, - "Alias graph size: ${xcfa.pointsToGraph.size} -> ${xcfa.pointsToGraph.values.map { it.size }.toList()}\n", - ) - - return Triple(xcfa, mcm, parseContext) -} + val stopwatch = Stopwatch.createStarted() + + val input = config.inputConfig.input!! + logger.write( + Logger.Level.INFO, + "Parsing the input $input as ${config.frontendConfig.inputType}\n", + ) + + val parseContext = ParseContext() + + if (config.frontendConfig.inputType == InputType.C) { + val cConfig = config.frontendConfig.specConfig + cConfig as CFrontendConfig + parseContext.arithmetic = cConfig.arithmetic + parseContext.architecture = cConfig.architecture + } + + val xcfa = getXcfa(config, parseContext, logger, uniqueLogger) + + val mcm = + if (config.inputConfig.catFile != null) { + CatDslManager.createMCM(config.inputConfig.catFile!!) + } else { + emptySet() + } + + ConeOfInfluence = + if (parseContext.multiThreading) XcfaCoiMultiThread(xcfa) else XcfaCoiSingleThread(xcfa) -private fun backend( - xcfa: XCFA, - mcm: MCM, - parseContext: ParseContext, - config: XcfaConfig<*, *>, - logger: Logger, - uniqueLogger: Logger, - throwDontExit: Boolean, -): SafetyResult<*, *> = - if (config.backendConfig.backend == Backend.NONE) { - SafetyResult.unknown() - } else { if ( - xcfa.procedures.all { - it.errorLoc.isEmpty && config.inputConfig.property == ErrorDetection.ERROR_LOCATION - } + parseContext.multiThreading && + (config.backendConfig.specConfig as? CegarConfig)?.let { + it.abstractorConfig.search == Search.ERR + } == true ) { - val result = SafetyResult.safe(EmptyProof.getInstance()) - logger.write(Logger.Level.INFO, "Input is trivially safe\n") - - logger.write(RESULT, result.toString() + "\n") - result - } else { - val stopwatch = Stopwatch.createStarted() + val cConfig = config.backendConfig.specConfig as CegarConfig + cConfig.abstractorConfig.search = Search.DFS + uniqueLogger.write(INFO, "Multithreaded program found, using DFS instead of ERR.") + } - logger.write( + logger.write( Logger.Level.INFO, - "Starting verification of ${if (xcfa.name == "") "UnnamedXcfa" else xcfa.name} using ${config.backendConfig.backend}\n", - ) + "Frontend finished: ${xcfa.name} (in ${ + stopwatch.elapsed(TimeUnit.MILLISECONDS) + } ms)\n", + ) + + logger.write(RESULT, "ParsingResult Success\n") + logger.write( + RESULT, + "Alias graph size: ${xcfa.pointsToGraph.size} -> ${xcfa.pointsToGraph.values.map { it.size }.toList()}\n", + ) + + return Triple(xcfa, mcm, parseContext) +} - val checker = getChecker(xcfa, mcm, config, parseContext, logger, uniqueLogger) - val result = - exitOnError(config.debugConfig.stacktrace, config.debugConfig.debug || throwDontExit) { - checker.check() - } - .let { result -> - when { - result.isSafe && - LoopUnrollPass.FORCE_UNROLL_USED -> { // cannot report safe if force unroll was used - logger.write(RESULT, "Incomplete loop unroll used: safe result is unreliable.\n") - SafetyResult.unknown() - } - - else -> result - } - } +private fun backend( + xcfa: XCFA, + mcm: MCM, + parseContext: ParseContext, + config: XcfaConfig<*, *>, + logger: Logger, + uniqueLogger: Logger, + throwDontExit: Boolean, +): Result<*> = + when(config.backendConfig.backend) { + Backend.TRACEGEN -> tracegenBackend(xcfa, mcm, parseContext, config, logger, uniqueLogger, throwDontExit) + Backend.NONE -> SafetyResult.unknown() + else -> safetyBackend(xcfa, mcm, parseContext, config, logger, uniqueLogger, throwDontExit) // safety analysis + } - logger.write( +private fun tracegenBackend( + xcfa: XCFA, + mcm: MCM, + parseContext: ParseContext, + config: XcfaConfig<*, *>, + logger: Logger, + uniqueLogger: Logger, + throwDontExit: Boolean, +): Result<*> { + val stopwatch = Stopwatch.createStarted() + val checker = getChecker(xcfa, mcm, config, parseContext, logger, uniqueLogger) as TraceGenerationChecker, XcfaAction, XcfaPrec<*>> + val result = + exitOnError(config.debugConfig.stacktrace, config.debugConfig.debug || throwDontExit) { + checker.check(XcfaPrec(PtrPrec(ExplPrec.of(xcfa.collectVars()), emptySet()))) + } + logger.write( Logger.Level.INFO, "Backend finished (in ${ + stopwatch.elapsed(TimeUnit.MILLISECONDS) + } ms)\n", + ) + + logger.write(RESULT, result.toString() + "\n") + return result +} + +private fun safetyBackend( + xcfa: XCFA, + mcm: MCM, + parseContext: ParseContext, + config: XcfaConfig<*, *>, + logger: Logger, + uniqueLogger: Logger, + throwDontExit: Boolean, +): Result<*> { + if ( + xcfa.procedures.all { + it.errorLoc.isEmpty && config.inputConfig.property == ErrorDetection.ERROR_LOCATION + } + ) { + val result = SafetyResult.safe(EmptyProof.getInstance()) + logger.write(Logger.Level.INFO, "Input is trivially safe\n") + + logger.write(RESULT, result.toString() + "\n") + return result + } else { + val stopwatch = Stopwatch.createStarted() + val checker = getChecker(xcfa, mcm, config, parseContext, logger, uniqueLogger) as SafetyChecker<*, *, XcfaPrec<*>> + val result = + exitOnError(config.debugConfig.stacktrace, config.debugConfig.debug || throwDontExit) { + checker.check() + } + .let { result -> + when { + result.isSafe && + LoopUnrollPass.FORCE_UNROLL_USED -> { // cannot report safe if force unroll was used + logger.write(RESULT, "Incomplete loop unroll used: safe result is unreliable.\n") + SafetyResult.unknown() + } + + else -> result + } + } + + logger.write( + Logger.Level.INFO, + "Backend finished (in ${ stopwatch.elapsed(TimeUnit.MILLISECONDS) } ms)\n", - ) + ) - logger.write(RESULT, result.toString() + "\n") - result + logger.write(RESULT, result.toString() + "\n") + return result } - } - -private fun preVerificationLogging( - xcfa: XCFA, - mcm: MCM, - parseContext: ParseContext, - config: XcfaConfig<*, *>, - logger: Logger, - uniqueLogger: Logger, +} + +private fun preAnalysisLogging( + xcfa: XCFA, + mcm: MCM, + parseContext: ParseContext, + config: XcfaConfig<*, *>, + logger: Logger, + uniqueLogger: Logger, ) { - if (config.outputConfig.enableOutput) { - try { - val resultFolder = config.outputConfig.resultFolder - resultFolder.mkdirs() + if (config.outputConfig.enableOutput) { + try { + val resultFolder = config.outputConfig.resultFolder + resultFolder.mkdirs() - logger.write( - Logger.Level.INFO, - "Writing pre-verification artifacts to directory ${resultFolder.absolutePath}\n", - ) - - if (!config.outputConfig.chcOutputConfig.disable) { - xcfa.procedures.forEach { - try { - val chcFile = File(resultFolder, "xcfa-${it.name}.smt2") - chcFile.writeText(it.toSMT2CHC()) - } catch (e: Exception) { - logger.write(INFO, "Could not write CHC file: " + e.stackTraceToString()) - } - } - } + logger.write( + Logger.Level.INFO, + "Writing pre-verification artifacts to directory ${resultFolder.absolutePath}\n", + ) - if (!config.outputConfig.xcfaOutputConfig.disable) { - val xcfaDotFile = File(resultFolder, "xcfa.dot") - xcfaDotFile.writeText(xcfa.toDot()) + if (!config.outputConfig.chcOutputConfig.disable) { + xcfa.procedures.forEach { + try { + val chcFile = File(resultFolder, "xcfa-${it.name}.smt2") + chcFile.writeText(it.toSMT2CHC()) + } catch (e: Exception) { + logger.write(INFO, "Could not write CHC file: " + e.stackTraceToString()) + } + } + } - val xcfaJsonFile = File(resultFolder, "xcfa.json") - val uglyJson = getGson(xcfa).toJson(xcfa) - val create = GsonBuilder().setPrettyPrinting().create() - xcfaJsonFile.writeText(create.toJson(JsonParser.parseString(uglyJson))) - } + if (!config.outputConfig.xcfaOutputConfig.disable) { + val xcfaDotFile = File(resultFolder, "xcfa.dot") + xcfaDotFile.writeText(xcfa.toDot()) - if (!config.outputConfig.cOutputConfig.disable) { - try { - val xcfaCFile = File(resultFolder, "xcfa.c") - xcfaCFile.writeText( - xcfa.toC( - parseContext, - config.outputConfig.cOutputConfig.useArr, - config.outputConfig.cOutputConfig.useExArr, - config.outputConfig.cOutputConfig.useRange, - ) - ) + val xcfaJsonFile = File(resultFolder, "xcfa.json") + val uglyJson = getGson(xcfa).toJson(xcfa) + val create = GsonBuilder().setPrettyPrinting().create() + xcfaJsonFile.writeText(create.toJson(JsonParser.parseString(uglyJson))) + } + + if (!config.outputConfig.cOutputConfig.disable) { + try { + val xcfaCFile = File(resultFolder, "xcfa.c") + xcfaCFile.writeText( + xcfa.toC( + parseContext, + config.outputConfig.cOutputConfig.useArr, + config.outputConfig.cOutputConfig.useExArr, + config.outputConfig.cOutputConfig.useRange, + ) + ) + } catch (e: Throwable) { + logger.write(Logger.Level.VERBOSE, "Could not emit C file\n") + } + } } catch (e: Throwable) { - logger.write(Logger.Level.VERBOSE, "Could not emit C file\n") + logger.write(Logger.Level.INFO, "Could not output files: ${e.stackTraceToString()}\n") } - } - } catch (e: Throwable) { - logger.write(Logger.Level.INFO, "Could not output files: ${e.stackTraceToString()}\n") } - } +} + +private fun postAnalysisLogging( + safetyResult: Result<*>, + mcm: MCM, + parseContext: ParseContext, + config: XcfaConfig<*, *>, + logger: Logger, + uniqueLogger: Logger, +) = when(config.backendConfig.backend) { + Backend.TRACEGEN -> postTraceGenerationLogging(safetyResult as TraceGenerationResult, XcfaAction>, XcfaState<*>, XcfaAction>, mcm, parseContext, config, logger, uniqueLogger) + else -> postVerificationLogging(safetyResult as SafetyResult<*, *>, mcm, parseContext, config, logger, uniqueLogger) // safety analysis (or none) } private fun postVerificationLogging( - safetyResult: SafetyResult<*, *>, - mcm: MCM, - parseContext: ParseContext, - config: XcfaConfig<*, *>, - logger: Logger, - uniqueLogger: Logger, + safetyResult: SafetyResult<*, *>, + mcm: MCM, + parseContext: ParseContext, + config: XcfaConfig<*, *>, + logger: Logger, + uniqueLogger: Logger, ) { - if (config.outputConfig.enableOutput) { - try { - // we only want to log the files if the current configuration is not --in-process or portfolio - if (config.backendConfig.inProcess || config.backendConfig.backend == Backend.PORTFOLIO) { - return - } + if (config.outputConfig.enableOutput) { + try { + // we only want to log the files if the current configuration is not --in-process or portfolio + if (config.backendConfig.inProcess || config.backendConfig.backend == Backend.PORTFOLIO) { + return + } - val resultFolder = config.outputConfig.resultFolder - resultFolder.mkdirs() + val resultFolder = config.outputConfig.resultFolder + resultFolder.mkdirs() - logger.write( - Logger.Level.INFO, - "Writing post-verification artifacts to directory ${resultFolder.absolutePath}\n", - ) - - // TODO eliminate the need for the instanceof check - if ( - !config.outputConfig.argConfig.disable && safetyResult.proof is ARG? - ) { - val argFile = File(resultFolder, "arg-${safetyResult.isSafe}.dot") - val g: Graph = - ArgVisualizer.getDefault().visualize(safetyResult.proof as ARG?) - argFile.writeText(GraphvizWriter.getInstance().writeString(g)) - } - - if (!config.outputConfig.witnessConfig.disable) { - if ( - safetyResult.isUnsafe && - safetyResult.asUnsafe().cex != null && - !config.outputConfig.witnessConfig.svcomp - ) { - val concrTrace: Trace, XcfaAction> = - XcfaTraceConcretizer.concretize( - safetyResult.asUnsafe().cex as Trace>, XcfaAction>?, - getSolver( - config.outputConfig.witnessConfig.concretizerSolver, - config.outputConfig.witnessConfig.validateConcretizerSolver, - ), - parseContext, + logger.write( + Logger.Level.INFO, + "Writing post-verification artifacts to directory ${resultFolder.absolutePath}\n", ) - val traceFile = File(resultFolder, "trace.dot") - val traceG: Graph = TraceVisualizer.getDefault().visualize(concrTrace) - traceFile.writeText(GraphvizWriter.getInstance().writeString(traceG)) - - val sequenceFile = File(resultFolder, "trace.plantuml") - writeSequenceTrace( - sequenceFile, - safetyResult.asUnsafe().cex as Trace, XcfaAction>, - ) { (_, act) -> - act.label.getFlatLabels().map(XcfaLabel::toString) - } - - val optSequenceFile = File(resultFolder, "trace-optimized.plantuml") - writeSequenceTrace(optSequenceFile, concrTrace) { (_, act) -> - act.label.getFlatLabels().map(XcfaLabel::toString) - } - - val cSequenceFile = File(resultFolder, "trace-c.plantuml") - writeSequenceTrace(cSequenceFile, concrTrace) { (state, act) -> - val proc = state.processes[act.pid] - val loc = proc?.locs?.peek() - (loc?.metadata as? CMetaData)?.sourceText?.split("\n") ?: listOf("") - } + // TODO eliminate the need for the instanceof check + if ( + !config.outputConfig.argConfig.disable && safetyResult.proof is ARG? + ) { + val argFile = File(resultFolder, "arg-${safetyResult.isSafe}.dot") + val g: Graph = + ArgVisualizer.getDefault().visualize(safetyResult.proof as ARG?) + argFile.writeText(GraphvizWriter.getInstance().writeString(g)) + } + + if (!config.outputConfig.witnessConfig.disable) { + if ( + safetyResult.isUnsafe && + safetyResult.asUnsafe().cex != null && + !config.outputConfig.witnessConfig.svcomp + ) { + val concrTrace: Trace, XcfaAction> = + XcfaTraceConcretizer.concretize( + safetyResult.asUnsafe().cex as Trace>, XcfaAction>?, + getSolver( + config.outputConfig.witnessConfig.concretizerSolver, + config.outputConfig.witnessConfig.validateConcretizerSolver, + ), + parseContext, + ) + + val traceFile = File(resultFolder, "trace.dot") + val traceG: Graph = TraceVisualizer.getDefault().visualize(concrTrace) + traceFile.writeText(GraphvizWriter.getInstance().writeString(traceG)) + + val sequenceFile = File(resultFolder, "trace.plantuml") + writeSequenceTrace( + sequenceFile, + safetyResult.asUnsafe().cex as Trace, XcfaAction>, + ) { (_, act) -> + act.label.getFlatLabels().map(XcfaLabel::toString) + } + + val optSequenceFile = File(resultFolder, "trace-optimized.plantuml") + writeSequenceTrace(optSequenceFile, concrTrace) { (_, act) -> + act.label.getFlatLabels().map(XcfaLabel::toString) + } + + val cSequenceFile = File(resultFolder, "trace-c.plantuml") + writeSequenceTrace(cSequenceFile, concrTrace) { (state, act) -> + val proc = state.processes[act.pid] + val loc = proc?.locs?.peek() + (loc?.metadata as? CMetaData)?.sourceText?.split("\n") ?: listOf("") + } + } + val witnessFile = File(resultFolder, "witness.graphml") + XcfaWitnessWriter() + .writeWitness( + safetyResult, + config.inputConfig.input!!, + getSolver( + config.outputConfig.witnessConfig.concretizerSolver, + config.outputConfig.witnessConfig.validateConcretizerSolver, + ), + parseContext, + witnessFile, + ) + } + } catch (e: Throwable) { + logger.write(Logger.Level.INFO, "Could not output files: ${e.stackTraceToString()}\n") } - val witnessFile = File(resultFolder, "witness.graphml") - XcfaWitnessWriter() - .writeWitness( - safetyResult, - config.inputConfig.input!!, - getSolver( - config.outputConfig.witnessConfig.concretizerSolver, - config.outputConfig.witnessConfig.validateConcretizerSolver, - ), - parseContext, - witnessFile, - ) - } - } catch (e: Throwable) { - logger.write(Logger.Level.INFO, "Could not output files: ${e.stackTraceToString()}\n") } - } } private fun writeSequenceTrace( - sequenceFile: File, - trace: Trace, XcfaAction>, - printer: (Pair, XcfaAction>) -> List, + sequenceFile: File, + trace: Trace, XcfaAction>, + printer: (Pair, XcfaAction>) -> List, ) { - sequenceFile.writeText("@startuml\n") - var maxWidth = 0 - trace.actions.forEachIndexed { i, it -> - val stateBefore = trace.states[i] - sequenceFile.appendText("hnote over ${it.pid}\n") - val labelStrings = printer(Pair(stateBefore, it)) - if (maxWidth < (labelStrings.maxOfOrNull { it.length } ?: 0)) { - maxWidth = labelStrings.maxOfOrNull { it.length } ?: 0 - } - sequenceFile.appendText("${labelStrings.joinToString("\n")}\n") - sequenceFile.appendText("endhnote\n") - } - trace.actions - .map { it.pid } - .distinct() - .reduce { acc, current -> - sequenceFile.appendText("$acc --> $current: \"${" ".repeat(maxWidth)}\"\n") - current + sequenceFile.writeText("@startuml\n") + var maxWidth = 0 + trace.actions.forEachIndexed { i, it -> + val stateBefore = trace.states[i] + sequenceFile.appendText("hnote over ${it.pid}\n") + val labelStrings = printer(Pair(stateBefore, it)) + if (maxWidth < (labelStrings.maxOfOrNull { it.length } ?: 0)) { + maxWidth = labelStrings.maxOfOrNull { it.length } ?: 0 + } + sequenceFile.appendText("${labelStrings.joinToString("\n")}\n") + sequenceFile.appendText("endhnote\n") } - sequenceFile.appendText("@enduml\n") + trace.actions + .map { it.pid } + .distinct() + .reduce { acc, current -> + sequenceFile.appendText("$acc --> $current: \"${" ".repeat(maxWidth)}\"\n") + current + } + sequenceFile.appendText("@enduml\n") } + +private fun postTraceGenerationLogging( + result: TraceGenerationResult, XcfaAction>, XcfaState<*>, XcfaAction>, + mcm: MCM, + parseContext: ParseContext, + config: XcfaConfig<*, *>, + logger: Logger, + uniqueLogger: Logger, +) { + TODO() +// logger.write(Logger.Level.RESULT, "Successfully generated a summary of ${abstractSummary.sourceTraces.size} traces in ${totalTimeMs}ms\n") +// // TODO print coverage (full or not)? +// +// val resultFolder = config.outputConfig.resultFolder +// resultFolder.mkdirs() +// +// logger.write( +// Logger.Level.INFO, +// "Writing post-verification artifacts to directory ${resultFolder.absolutePath}\n", +// ) +// +// val modelName = config.inputConfig.input!!.name +// val graph = AbstractTraceSummaryVisualizer.visualize(abstractSummary) +// val visFile = traceDirPath.absolutePath + File.separator + modelName + ".abstract-trace-summary.png" +// GraphvizWriter.getInstance().writeFileAutoConvert(graph, visFile) +// logger.write(Logger.Level.SUBSTEP, "Abstract trace summary was visualized in ${visFile}") +// +// val concreteSummaryFile = traceDirPath.absolutePath + File.separator + modelName + ".cexs" +// +// /* +// val cexsString = toCexs(concretizationResult) +// PrintWriter(File(concreteSummaryFile)).use { printWriter -> +// printWriter.write(cexsString) +// } +// */ +// +// logger.write(Logger.Level.SUBSTEP, "Concrete trace summary exported to ${concreteSummaryFile}") +} + diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToChecker.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToChecker.kt index 8ff38051fd..984324dc82 100644 --- a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToChecker.kt +++ b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToChecker.kt @@ -17,6 +17,7 @@ package hu.bme.mit.theta.xcfa.cli.checkers import hu.bme.mit.theta.analysis.Trace +import hu.bme.mit.theta.analysis.algorithm.Checker import hu.bme.mit.theta.analysis.algorithm.SafetyChecker import hu.bme.mit.theta.analysis.algorithm.SafetyResult import hu.bme.mit.theta.analysis.algorithm.arg.ARG @@ -33,7 +34,7 @@ import hu.bme.mit.theta.xcfa.model.XCFA fun getChecker(xcfa: XCFA, mcm: MCM, config: XcfaConfig<*, *>, parseContext: ParseContext, logger: Logger, - uniqueLogger: Logger): SafetyChecker<*, *, XcfaPrec<*>> = + uniqueLogger: Logger): Checker<*, XcfaPrec<*>> = if (config.backendConfig.inProcess) { InProcessChecker(xcfa, config, parseContext, logger) } else { diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToTracegenChecker.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToTracegenChecker.kt index f603565d5d..039c03c5ec 100644 --- a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToTracegenChecker.kt +++ b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToTracegenChecker.kt @@ -22,9 +22,11 @@ import hu.bme.mit.theta.analysis.Trace import hu.bme.mit.theta.analysis.algorithm.Checker import hu.bme.mit.theta.analysis.algorithm.SafetyChecker import hu.bme.mit.theta.analysis.algorithm.SafetyResult +import hu.bme.mit.theta.analysis.algorithm.Result import hu.bme.mit.theta.analysis.algorithm.arg.ARG import hu.bme.mit.theta.analysis.algorithm.arg.ArgNode import hu.bme.mit.theta.analysis.algorithm.cegar.Abstractor +import hu.bme.mit.theta.analysis.algorithm.cegar.BasicArgAbstractor import hu.bme.mit.theta.analysis.algorithm.cegar.CegarChecker import hu.bme.mit.theta.analysis.algorithm.cegar.Refiner import hu.bme.mit.theta.analysis.algorithm.cegar.abstractor.StopCriterion @@ -70,7 +72,7 @@ fun getTracegenChecker(xcfa: XCFA, mcm: MCM, val corePartialOrd: PartialOrd>> = if (xcfa.isInlined) getPartialOrder(globalStatePartialOrd) else getStackPartialOrder(globalStatePartialOrd) - val abstractor: Abstractor = tracegenConfig.abstractorConfig.domain.abstractor( + val abstractor: BasicArgAbstractor = tracegenConfig.abstractorConfig.domain.abstractor( xcfa, abstractionSolverInstance, tracegenConfig.abstractorConfig.maxEnum, @@ -81,18 +83,12 @@ fun getTracegenChecker(xcfa: XCFA, mcm: MCM, config.inputConfig.property, corePartialOrd, tracegenConfig.abstractorConfig.havocMemory - ) as Abstractor + ) as BasicArgAbstractor val tracegenChecker = TraceGenerationChecker.create(logger, abstractor, false) - return tracegenChecker - - /*object: - Checker, XcfaAction, XcfaPrec<*>> { - override fun check( - prec: XcfaPrec<*>): TraceGenerationResult, XcfaAction>, XcfaState<*>, XcfaAction> { - return tracegenChecker.check( - prec) as TraceGenerationResult, XcfaAction>, XcfaState<*>, XcfaAction> - }*/ + return Checker, XcfaAction>, XcfaPrec<*>> { prec -> + tracegenChecker.check(prec) + as Result, XcfaAction>> } } \ No newline at end of file diff --git a/subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/tracegeneration/XstsTracegenBuilder.kt b/subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/tracegeneration/XstsTracegenBuilder.kt index 8ff17ee3d6..ff80008361 100644 --- a/subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/tracegeneration/XstsTracegenBuilder.kt +++ b/subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/tracegeneration/XstsTracegenBuilder.kt @@ -6,7 +6,7 @@ import hu.bme.mit.theta.analysis.Prec import hu.bme.mit.theta.analysis.State import hu.bme.mit.theta.analysis.algorithm.arg.ArgBuilder import hu.bme.mit.theta.analysis.algorithm.cegar.Abstractor -import hu.bme.mit.theta.analysis.algorithm.cegar.BasicAbstractor +import hu.bme.mit.theta.analysis.algorithm.cegar.BasicArgAbstractor import hu.bme.mit.theta.analysis.algorithm.cegar.abstractor.StopCriterions import hu.bme.mit.theta.analysis.algorithm.tracegeneration.TraceGenerationChecker.Companion.create import hu.bme.mit.theta.analysis.expl.* @@ -69,8 +69,8 @@ class XstsTracegenBuilder( val argBuilder = ArgBuilder.create(lts, analysis, target, true) if (abstraction==TracegenerationAbstraction.VARLIST) { - val abstractor: Abstractor, XstsAction, ExplPrec> = - BasicAbstractor.builder(argBuilder) + val abstractor: BasicArgAbstractor, XstsAction, ExplPrec> = + BasicArgAbstractor.builder(argBuilder) .waitlist(PriorityWaitlist.create(XstsConfigBuilder.Search.DFS.comparator)) .stopCriterion(StopCriterions.fullExploration()) .logger(logger).build() @@ -105,8 +105,8 @@ class XstsTracegenBuilder( } } else { assert(abstraction==TracegenerationAbstraction.NONE) - val abstractor: Abstractor, XstsAction, ExplPrec> = - BasicAbstractor.builder(argBuilder) + val abstractor: BasicArgAbstractor, XstsAction, ExplPrec> = + BasicArgAbstractor.builder(argBuilder) .waitlist(PriorityWaitlist.create(XstsConfigBuilder.Search.DFS.comparator)) .stopCriterion(StopCriterions.fullExploration()) .logger(logger).build() @@ -141,7 +141,7 @@ class XstsTracegenBuilder( val argBuilder = ArgBuilder.create(lts, analysis, target, true) val abstractor: Abstractor?, XstsAction?, PredPrec?> = - BasicAbstractor.builder(argBuilder) + BasicArgAbstractor.builder(argBuilder) .waitlist(PriorityWaitlist.create(XstsConfigBuilder.Search.DFS.comparator)) .stopCriterion(StopCriterions.fullExploration()) .logger(logger).build()