From aabe64ebe8fa5922a80f4c222344c628f04daae0 Mon Sep 17 00:00:00 2001 From: AdamZsofi Date: Sat, 26 Oct 2024 17:24:48 +0200 Subject: [PATCH] wip tracegen to xcfa --- .../tracegeneration/TraceGenerationChecker.kt | 4 +- .../xcfa/cli/checkers/ConfigToChecker.kt | 1 + .../cli/checkers/ConfigToTracegenChecker.kt | 98 +++++++++++++++++++ .../mit/theta/xcfa/cli/params/ParamValues.kt | 6 ++ .../mit/theta/xcfa/cli/params/XcfaConfig.kt | 8 ++ .../tracegeneration/XstsTracegenConfig.kt | 2 +- 6 files changed, 116 insertions(+), 3 deletions(-) create mode 100644 subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToTracegenChecker.kt 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 938ae566f7..178e113396 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 @@ -13,7 +13,7 @@ import hu.bme.mit.theta.common.logging.Logger import java.util.function.Consumer import kotlin.collections.ArrayList -class TraceGenerationChecker( +class TraceGenerationChecker( private val logger: Logger, private val abstractor: Abstractor, private val getFullTraces : Boolean, @@ -21,7 +21,7 @@ class TraceGenerationChecker( private var traces: List> = ArrayList() companion object { - fun create( + fun create( logger: Logger, abstractor: Abstractor, getFullTraces: Boolean 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 4bd2dce149..8ff38051fd 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 @@ -45,6 +45,7 @@ fun getChecker(xcfa: XCFA, mcm: MCM, config: XcfaConfig<*, *>, parseContext: Par Backend.PORTFOLIO -> getPortfolioChecker(xcfa, mcm, config, parseContext, logger, uniqueLogger) Backend.NONE -> SafetyChecker>, XcfaAction>, Trace>, XcfaAction>, XcfaPrec<*>> { _ -> SafetyResult.unknown() } Backend.CHC -> getHornChecker(xcfa, mcm, config, logger) + Backend.TRACEGEN -> getTracegenChecker(xcfa, mcm, config, logger) } } 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 new file mode 100644 index 0000000000..f603565d5d --- /dev/null +++ b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToTracegenChecker.kt @@ -0,0 +1,98 @@ +/* + * 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.xcfa.cli.checkers + +import hu.bme.mit.theta.analysis.PartialOrd +import hu.bme.mit.theta.analysis.Prec +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 +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.CegarChecker +import hu.bme.mit.theta.analysis.algorithm.cegar.Refiner +import hu.bme.mit.theta.analysis.algorithm.cegar.abstractor.StopCriterion +import hu.bme.mit.theta.analysis.algorithm.cegar.abstractor.StopCriterions +import hu.bme.mit.theta.analysis.algorithm.tracegeneration.TraceGenerationChecker +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.expr.ExprAction +import hu.bme.mit.theta.analysis.expr.ExprState +import hu.bme.mit.theta.analysis.expr.refinement.* +import hu.bme.mit.theta.analysis.ptr.PtrState +import hu.bme.mit.theta.analysis.runtimemonitor.CexMonitor +import hu.bme.mit.theta.analysis.runtimemonitor.MonitorCheckpoint +import hu.bme.mit.theta.analysis.waitlist.PriorityWaitlist +import hu.bme.mit.theta.common.logging.Logger +import hu.bme.mit.theta.core.decl.VarDecl +import hu.bme.mit.theta.graphsolver.patterns.constraints.MCM +import hu.bme.mit.theta.solver.SolverFactory +import hu.bme.mit.theta.xcfa.analysis.* +import hu.bme.mit.theta.xcfa.analysis.por.XcfaDporLts +import hu.bme.mit.theta.xcfa.cli.params.* +import hu.bme.mit.theta.xcfa.cli.utils.getSolver +import hu.bme.mit.theta.xcfa.model.XCFA + +fun getTracegenChecker(xcfa: XCFA, mcm: MCM, + config: XcfaConfig<*, *>, + logger: Logger +): Checker, XcfaAction>, XcfaPrec<*>> { + val tracegenConfig = config.backendConfig.specConfig as TracegenConfig + val ignoredVarRegistry = mutableMapOf, MutableSet>() + + val lts = ConeOfInfluenceMode.NO_COI.getLts(xcfa, ignoredVarRegistry, POR.NOPOR) + + val abstractionSolverFactory: SolverFactory = getSolver(tracegenConfig.abstractorConfig.abstractionSolver, + tracegenConfig.abstractorConfig.validateAbstractionSolver) + + val waitlist = PriorityWaitlist.create>, XcfaAction>>( + tracegenConfig.abstractorConfig.search.getComp(xcfa)) + + val abstractionSolverInstance = abstractionSolverFactory.createSolver() + val globalStatePartialOrd: PartialOrd> = tracegenConfig.abstractorConfig.domain.partialOrd( + abstractionSolverInstance) as PartialOrd> + val corePartialOrd: PartialOrd>> = + if (xcfa.isInlined) getPartialOrder(globalStatePartialOrd) + else getStackPartialOrder(globalStatePartialOrd) + val abstractor: Abstractor = tracegenConfig.abstractorConfig.domain.abstractor( + xcfa, + abstractionSolverInstance, + tracegenConfig.abstractorConfig.maxEnum, + waitlist, + StopCriterions.fullExploration(), + logger, + lts, + config.inputConfig.property, + corePartialOrd, + tracegenConfig.abstractorConfig.havocMemory + ) as Abstractor + + 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> + }*/ + } +} \ No newline at end of file diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/params/ParamValues.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/params/ParamValues.kt index ac5b3d3236..359d953a57 100644 --- a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/params/ParamValues.kt +++ b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/params/ParamValues.kt @@ -70,6 +70,7 @@ enum class Backend { OC, LAZY, PORTFOLIO, + TRACEGEN, NONE, } @@ -301,6 +302,11 @@ enum class Search { abstract fun getComp(cfa: XCFA): ArgNodeComparator } +enum class TracegenAbstraction{ + NONE, + // TODO add EXPL +} + enum class InitPrec( val explPrec: (xcfa: XCFA) -> XcfaPrec>, val predPrec: (xcfa: XCFA) -> XcfaPrec>, 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 ef50a1e108..2785ce67f3 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 @@ -169,6 +169,7 @@ data class BackendConfig( Backend.OC -> OcConfig() as T Backend.LAZY -> null Backend.PORTFOLIO -> PortfolioConfig() as T + Backend.TRACEGEN -> TracegenConfig() as T Backend.NONE -> null } } @@ -202,6 +203,13 @@ data class CegarConfig( listOf(abstractorConfig, refinerConfig).map { it.update() }.any { it } } +data class TracegenConfig( + @Parameter(names = ["--abstraction"], description = "Abstraction to be used for trace generation") + var abstraction: TracegenAbstraction = TracegenAbstraction.NONE, + + val abstractorConfig: CegarAbstractorConfig = CegarAbstractorConfig(), +) : SpecBackendConfig + data class CegarAbstractorConfig( @Parameter(names = ["--abstraction-solver"], description = "Abstraction solver name") var abstractionSolver: String = "Z3", diff --git a/subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/tracegeneration/XstsTracegenConfig.kt b/subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/tracegeneration/XstsTracegenConfig.kt index d5799e82a6..eb8123e5bf 100644 --- a/subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/tracegeneration/XstsTracegenConfig.kt +++ b/subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/tracegeneration/XstsTracegenConfig.kt @@ -9,7 +9,7 @@ import hu.bme.mit.theta.analysis.algorithm.tracegeneration.summary.AbstractTrace import hu.bme.mit.theta.analysis.expr.ExprAction import hu.bme.mit.theta.analysis.expr.ExprState -class XstsTracegenConfig private constructor( +class XstsTracegenConfig private constructor( private val checker: TraceGenerationChecker, private val prec: P ) {