diff --git a/subprojects/cfa/cfa-analysis/src/main/kotlin/hu/bme/mit/theta/cfa/analysis/CfaToMonolithicExpr.kt b/subprojects/cfa/cfa-analysis/src/main/kotlin/hu/bme/mit/theta/cfa/analysis/CfaToMonolithicExpr.kt index 616386abee..37529a6bfc 100644 --- a/subprojects/cfa/cfa-analysis/src/main/kotlin/hu/bme/mit/theta/cfa/analysis/CfaToMonolithicExpr.kt +++ b/subprojects/cfa/cfa-analysis/src/main/kotlin/hu/bme/mit/theta/cfa/analysis/CfaToMonolithicExpr.kt @@ -47,7 +47,11 @@ fun CFA.toMonolithicExpr(): MonolithicExpr { for ((i, x) in this.locs.withIndex()) { map[x] = i } - val locVar = Decls.Var("__loc__", Int()) + val locVar = + Decls.Var( + "__loc__", + Int(), + ) // TODO: add edge var as well, to avoid parallel edges causing problems val tranList = this.edges .map { e -> diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/bounded/AbstractMonolithicExpr.kt b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/bounded/AbstractMonolithicExpr.kt index 04427ecfac..c3a7bcd2ce 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/bounded/AbstractMonolithicExpr.kt +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/bounded/AbstractMonolithicExpr.kt @@ -53,9 +53,11 @@ fun MonolithicExpr.createAbstract(prec: PredPrec): MonolithicExpr { } var indexingBuilder = VarIndexingFactory.indexingBuilder(1) - this.vars./*filter { it !in ctrlVars }.*/ forEach { decl -> - repeat(transOffsetIndex.get(decl)) { indexingBuilder = indexingBuilder.inc(decl) } - } + this.vars + .filter { it !in ctrlVars } + .forEach { decl -> + repeat(transOffsetIndex.get(decl)) { indexingBuilder = indexingBuilder.inc(decl) } + } return MonolithicExpr( initExpr = And(And(lambdaList), initExpr), @@ -63,13 +65,14 @@ fun MonolithicExpr.createAbstract(prec: PredPrec): MonolithicExpr { propExpr = Not(And(And(lambdaList), Not(propExpr))), transOffsetIndex = indexingBuilder.build(), initOffsetIndex = VarIndexingFactory.indexing(0), - vars = activationLiterals /* + ctrlVars*/, + vars = activationLiterals + ctrlVars, valToState = { valuation: Valuation -> PredState.of( valuation .toMap() .entries .stream() + .filter { it.key !in ctrlVars } .map { when ((it.value as BoolLitExpr).value) { true -> literalToPred[it.key] @@ -80,5 +83,6 @@ fun MonolithicExpr.createAbstract(prec: PredPrec): MonolithicExpr { ) }, biValToAction = this.biValToAction, + ctrlVars = ctrlVars, ) } diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/bounded/MonolithicExprCegarChecker.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/bounded/MonolithicExprCegarChecker.java index 9024d2ebd9..2457715f91 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/bounded/MonolithicExprCegarChecker.java +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/bounded/MonolithicExprCegarChecker.java @@ -15,7 +15,7 @@ */ package hu.bme.mit.theta.analysis.algorithm.bounded; -import static hu.bme.mit.theta.core.type.booltype.SmartBoolExprs.Not; +import static hu.bme.mit.theta.core.type.booltype.BoolExprs.True; import com.google.common.base.Preconditions; import hu.bme.mit.theta.analysis.*; @@ -31,16 +31,12 @@ import hu.bme.mit.theta.analysis.pred.PredPrec; import hu.bme.mit.theta.analysis.unit.UnitPrec; import hu.bme.mit.theta.common.logging.Logger; -import hu.bme.mit.theta.core.model.Valuation; import hu.bme.mit.theta.solver.SolverFactory; -import java.util.ArrayList; import java.util.List; -import java.util.function.BiFunction; import java.util.function.Function; -public class MonolithicExprCegarChecker< - W extends Proof, S extends ExprState, A extends ExprAction, P extends Prec> - implements SafetyChecker, PredPrec> { +public class MonolithicExprCegarChecker + implements SafetyChecker, PredPrec> { private final MonolithicExpr model; private final Function< MonolithicExpr, @@ -50,9 +46,6 @@ public class MonolithicExprCegarChecker< UnitPrec>> checkerFactory; - private final Function valToState; - private final BiFunction biValToAction; - private final SolverFactory solverFactory; private final Logger logger; @@ -66,32 +59,31 @@ public MonolithicExprCegarChecker( ? extends Trace, UnitPrec>> checkerFactory, - Function valToState, - BiFunction biValToAction, Logger logger, SolverFactory solverFactory) { this.model = model; this.checkerFactory = checkerFactory; - this.valToState = valToState; - this.biValToAction = biValToAction; this.logger = logger; this.solverFactory = solverFactory; } - public SafetyResult> check(PredPrec initPrec) { + public SafetyResult> check( + PredPrec initPrec) { var predPrec = initPrec == null ? PredPrec.of(List.of(model.getInitExpr(), model.getPropExpr())) : initPrec; while (true) { + logger.write(Logger.Level.SUBSTEP, "Current prec: %s\n", predPrec); + final var abstractMonolithicExpr = AbstractMonolithicExprKt.createAbstract(model, predPrec); final var checker = checkerFactory.apply(abstractMonolithicExpr); final var result = checker.check(); if (result.isSafe()) { - logger.write(Logger.Level.INFO, "Model is safe, stopping CEGAR"); + logger.write(Logger.Level.MAINSTEP, "Model is safe, stopping CEGAR"); return SafetyResult.safe(result.getProof()); } else { Preconditions.checkState(result.isUnsafe()); @@ -100,35 +92,22 @@ public SafetyResult> check(PredPrec initPrec) { final ExprTraceChecker exprTraceFwBinItpChecker = ExprTraceFwBinItpChecker.create( - model.getInitExpr(), - Not(model.getPropExpr()), - solverFactory.createItpSolver()); + True(), True(), solverFactory.createItpSolver()); if (trace != null) { + logger.write(Logger.Level.VERBOSE, "\tFound trace: %s\n", trace); final ExprTraceStatus concretizationResult = exprTraceFwBinItpChecker.check(trace); if (concretizationResult.isFeasible()) { - logger.write(Logger.Level.INFO, "Model is unsafe, stopping CEGAR"); - - final var valTrace = concretizationResult.asFeasible().getValuations(); - Valuation lastValuation = null; - final ArrayList states = new ArrayList<>(); - final ArrayList actions = new ArrayList<>(); - for (var val : valTrace.getStates()) { - states.add(valToState.apply(val)); - if (lastValuation != null) { - actions.add(biValToAction.apply(lastValuation, val)); - } - lastValuation = val; - } + logger.write(Logger.Level.MAINSTEP, "Model is unsafe, stopping CEGAR\n"); - return SafetyResult.unsafe(Trace.of(states, actions), result.getProof()); + return SafetyResult.unsafe(trace, result.getProof()); } else { final var ref = concretizationResult.asInfeasible().getRefutation(); final var newPred = ref.get(ref.getPruneIndex()); final var newPrec = PredPrec.of(newPred); predPrec = predPrec.join(newPrec); - logger.write(Logger.Level.INFO, "Added new predicate " + newPrec); + logger.write(Logger.Level.INFO, "Added new predicate " + newPrec + "\n"); } } } diff --git a/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/grammar/function/FunctionVisitor.java b/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/grammar/function/FunctionVisitor.java index d45fe00e83..c4ae8ea4de 100644 --- a/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/grammar/function/FunctionVisitor.java +++ b/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/grammar/function/FunctionVisitor.java @@ -481,6 +481,10 @@ public CStatement visitBodyDeclaration(CParser.BodyDeclarationContext ctx) { ctx.declaration().declarationSpecifiers(), ctx.declaration().initDeclaratorList()); CCompound compound = new CCompound(parseContext); + final var preCompound = new CCompound(parseContext); + final var postCompound = new CCompound(parseContext); + compound.setPreStatements(preCompound); + compound.setPostStatements(postCompound); for (CDeclaration declaration : declarations) { if (declaration.getInitExpr() != null) { createVars(declaration); @@ -546,16 +550,12 @@ public CStatement visitBodyDeclaration(CParser.BodyDeclarationContext ctx) { recordMetadata(ctx, cAssignment); compound.getcStatementList().add(cAssignment); if (declaration.getInitExpr() instanceof CCompound compoundInitExpr) { - final var preCompound = new CCompound(parseContext); - final var postCompound = new CCompound(parseContext); final var preStatements = collectPreStatements(compoundInitExpr); preCompound.getcStatementList().addAll(preStatements); final var postStatements = collectPostStatements(compoundInitExpr); postCompound.getcStatementList().addAll(postStatements); resetPreStatements(compoundInitExpr); resetPostStatements(compoundInitExpr); - compound.setPreStatements(preCompound); - compound.setPostStatements(postCompound); } } } diff --git a/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaState.kt b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaState.kt index c3f66a25fe..41b35eccc3 100644 --- a/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaState.kt +++ b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaState.kt @@ -43,6 +43,18 @@ constructor( val bottom: Boolean = false, ) : ExprState { + constructor( + xcfa: XCFA, + loc: XcfaLocation, + state: S, + ) : this( + xcfa = xcfa, + processes = + mapOf(Pair(0, XcfaProcessState(locs = LinkedList(listOf(loc)), varLookup = LinkedList()))), + state, + mutexes = emptyMap(), + ) + override fun isBottom(): Boolean { return bottom || sGlobal.isBottom } diff --git a/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaToMonolithicExpr.kt b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaToMonolithicExpr.kt index 1667c21267..4911eb780b 100644 --- a/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaToMonolithicExpr.kt +++ b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaToMonolithicExpr.kt @@ -30,8 +30,7 @@ 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.abstracttype.AbstractExprs.Neq -import hu.bme.mit.theta.core.type.booltype.BoolExprs.And -import hu.bme.mit.theta.core.type.booltype.BoolExprs.Bool +import hu.bme.mit.theta.core.type.booltype.BoolExprs.* import hu.bme.mit.theta.core.type.booltype.BoolType import hu.bme.mit.theta.core.type.bvtype.BvLitExpr import hu.bme.mit.theta.core.type.bvtype.BvType @@ -48,10 +47,7 @@ import hu.bme.mit.theta.core.utils.indexings.VarIndexingFactory import hu.bme.mit.theta.frontend.ParseContext import hu.bme.mit.theta.frontend.transformation.model.types.complex.integer.cint.CInt import hu.bme.mit.theta.xcfa.getFlatLabels -import hu.bme.mit.theta.xcfa.model.StmtLabel -import hu.bme.mit.theta.xcfa.model.XCFA -import hu.bme.mit.theta.xcfa.model.XcfaEdge -import hu.bme.mit.theta.xcfa.model.XcfaLocation +import hu.bme.mit.theta.xcfa.model.* import java.math.BigInteger import java.util.* import org.kframework.mpfr.BigFloat @@ -64,7 +60,7 @@ private val LitExpr<*>.value: Int else -> error("Unknown integer type: $type") } -fun XCFA.toMonolithicExpr(parseContext: ParseContext): MonolithicExpr { +fun XCFA.toMonolithicExpr(parseContext: ParseContext, initValues: Boolean = false): MonolithicExpr { val intType = CInt.getUnsignedInt(parseContext).smtType fun int(value: Int): Expr<*> = @@ -83,19 +79,26 @@ fun XCFA.toMonolithicExpr(parseContext: ParseContext): MonolithicExpr { ) Preconditions.checkArgument(proc.errorLoc.isPresent) - val map = mutableMapOf() + val locMap = mutableMapOf() for ((i, x) in proc.locs.withIndex()) { - map[x] = i + locMap[x] = i + } + val edgeMap = mutableMapOf() + for ((i, x) in proc.edges.withIndex()) { + edgeMap[x] = i } val locVar = Decls.Var("__loc_", intType) + val edgeVar = Decls.Var("__edge_", intType) val tranList = proc.edges - .map { (source, target, label): XcfaEdge -> + .map { edge: XcfaEdge -> + val (source, target, label) = edge SequenceStmt.of( listOf( - AssumeStmt.of(Eq(locVar.ref, int(map[source]!!))), + AssumeStmt.of(Eq(locVar.ref, int(locMap[source]!!))), label.toStmt(), - AssignStmt.of(locVar, cast(int(map[target]!!), locVar.type)), + AssignStmt.of(locVar, cast(int(locMap[target]!!), locVar.type)), + AssignStmt.of(edgeVar, cast(int(edgeMap[edge]!!), edgeVar.type)), ) ) } @@ -104,46 +107,55 @@ fun XCFA.toMonolithicExpr(parseContext: ParseContext): MonolithicExpr { val transUnfold = StmtUtils.toExpr(trans, VarIndexingFactory.indexing(0)) val defaultValues = - StmtUtils.getVars(trans) - .map { - when (it.type) { - is IntType -> Eq(it.ref, int(0)) - is BoolType -> Eq(it.ref, Bool(false)) - is BvType -> - Eq( - it.ref, - BvUtils.bigIntegerToNeutralBvLitExpr(BigInteger.ZERO, (it.type as BvType).size), - ) - is FpType -> - FpAssign( - it.ref as Expr, - FpUtils.bigFloatToFpLitExpr( - BigFloat.zero((it.type as FpType).significand), - it.type as FpType, - ), - ) - else -> throw IllegalArgumentException("Unsupported type") + if (initValues) + StmtUtils.getVars(trans) + .map { + when (it.type) { + is IntType -> Eq(it.ref, int(0)) + is BoolType -> Eq(it.ref, Bool(false)) + is BvType -> + Eq( + it.ref, + BvUtils.bigIntegerToNeutralBvLitExpr(BigInteger.ZERO, (it.type as BvType).size), + ) + is FpType -> + FpAssign( + it.ref as Expr, + FpUtils.bigFloatToFpLitExpr( + BigFloat.zero((it.type as FpType).significand), + it.type as FpType, + ), + ) + else -> throw IllegalArgumentException("Unsupported type") + } } - } - .toList() - .let { And(it) } + .toList() + .let { And(it) } + else True() return MonolithicExpr( - initExpr = And(Eq(locVar.ref, int(map[proc.initLoc]!!)), defaultValues), + initExpr = + And(Eq(locVar.ref, int(locMap[proc.initLoc]!!)), Eq(edgeVar.ref, int(-1)), defaultValues), transExpr = And(transUnfold.exprs), - propExpr = Neq(locVar.ref, int(map[proc.errorLoc.get()]!!)), + propExpr = Neq(locVar.ref, int(locMap[proc.errorLoc.get()]!!)), transOffsetIndex = transUnfold.indexing, vars = (StmtUtils.getVars(trans) + listOf(locVar)).toList(), + valToState = { valToState(it) }, + biValToAction = { val1, val2 -> valToAction(val1, val2) }, + ctrlVars = listOf(locVar, edgeVar), ) } fun XCFA.valToAction(val1: Valuation, val2: Valuation): XcfaAction { - val val1Map = val1.toMap() val val2Map = val2.toMap() - var i = 0 - val map: MutableMap = HashMap() - for (x in this.procedures.first { it.name == "main" }.locs) { - map[x] = i++ + val proc = this.procedures.first { it.name == "main" } + val locMap = mutableMapOf() + for ((i, x) in proc.locs.withIndex()) { + locMap[x] = i + } + val edgeMap = mutableMapOf() + for ((i, x) in proc.edges.withIndex()) { + edgeMap[x] = i } return XcfaAction( pid = 0, @@ -152,34 +164,21 @@ fun XCFA.valToAction(val1: Valuation, val2: Valuation): XcfaAction { .first { it.name == "main" } .edges .first { edge -> - map[edge.source] == (val1Map[val1Map.keys.first { it.name == "__loc_" }])?.value ?: -1 && - map[edge.target] == (val2Map[val2Map.keys.first { it.name == "__loc_" }])?.value ?: -1 + edgeMap[edge] == (val2Map[val2Map.keys.first { it.name == "__edge_" }]?.value ?: -1) }, ) } fun XCFA.valToState(val1: Valuation): XcfaState> { val valMap = val1.toMap() - var i = 0 - val map: MutableMap = HashMap() - for (x in this.procedures.first { it.name == "main" }.locs) { - map[i++] = x + val proc = this.procedures.first { it.name == "main" } + val locMap = mutableMapOf() + for ((i, x) in proc.locs.withIndex()) { + locMap[i] = x } return XcfaState( - xcfa = this, - processes = - mapOf( - Pair( - 0, - XcfaProcessState( - locs = - LinkedList( - listOf(map[(valMap[valMap.keys.first { it.name == "__loc_" }])?.value ?: -1]) - ), - varLookup = LinkedList(), - ), - ) - ), + this, + locMap[(valMap[valMap.keys.first { it.name == "__loc_" }])?.value ?: -1]!!, PtrState( ExplState.of( ImmutableValuation.from( @@ -191,8 +190,5 @@ fun XCFA.valToState(val1: Valuation): XcfaState> { ) ) ), - mutexes = emptyMap(), - threadLookup = emptyMap(), - bottom = false, ) } diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToBoundedChecker.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToBoundedChecker.kt index 6ed1be6c97..1f928b4ab3 100644 --- a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToBoundedChecker.kt +++ b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToBoundedChecker.kt @@ -18,7 +18,11 @@ package hu.bme.mit.theta.xcfa.cli.checkers 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.bounded.BoundedChecker +import hu.bme.mit.theta.analysis.algorithm.SafetyResult +import hu.bme.mit.theta.analysis.algorithm.bounded.* +import hu.bme.mit.theta.analysis.pred.PredPrec +import hu.bme.mit.theta.analysis.pred.PredState +import hu.bme.mit.theta.analysis.ptr.PtrPrec import hu.bme.mit.theta.analysis.ptr.PtrState import hu.bme.mit.theta.common.logging.Logger import hu.bme.mit.theta.frontend.ParseContext @@ -29,6 +33,7 @@ import hu.bme.mit.theta.xcfa.cli.params.BoundedConfig 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 java.util.* fun getBoundedChecker( xcfa: XCFA, @@ -40,25 +45,75 @@ fun getBoundedChecker( val boundedConfig = config.backendConfig.specConfig as BoundedConfig - return BoundedChecker( - monolithicExpr = xcfa.toMonolithicExpr(parseContext), - bmcSolver = - tryGetSolver(boundedConfig.bmcConfig.bmcSolver, boundedConfig.bmcConfig.validateBMCSolver) - ?.createSolver(), - bmcEnabled = { !boundedConfig.bmcConfig.disable }, - lfPathOnly = { !boundedConfig.bmcConfig.nonLfPath }, - itpSolver = - tryGetSolver(boundedConfig.itpConfig.itpSolver, boundedConfig.itpConfig.validateItpSolver) - ?.createItpSolver(), - imcEnabled = { !boundedConfig.itpConfig.disable }, - indSolver = - tryGetSolver(boundedConfig.indConfig.indSolver, boundedConfig.indConfig.validateIndSolver) - ?.createSolver(), - kindEnabled = { !boundedConfig.indConfig.disable }, - valToState = { xcfa.valToState(it) }, - biValToAction = { val1, val2 -> xcfa.valToAction(val1, val2) }, - logger = logger, - ) + val monolithicExpr = + xcfa.toMonolithicExpr(parseContext).let { + if (boundedConfig.reversed) it.createReversed() else it + } + + val baseChecker = { monolithicExpr: MonolithicExpr -> + BoundedChecker( + monolithicExpr = monolithicExpr, + bmcSolver = + tryGetSolver(boundedConfig.bmcConfig.bmcSolver, boundedConfig.bmcConfig.validateBMCSolver) + ?.createSolver(), + bmcEnabled = { !boundedConfig.bmcConfig.disable }, + lfPathOnly = { !boundedConfig.bmcConfig.nonLfPath }, + itpSolver = + tryGetSolver(boundedConfig.itpConfig.itpSolver, boundedConfig.itpConfig.validateItpSolver) + ?.createItpSolver(), + imcEnabled = { !boundedConfig.itpConfig.disable }, + indSolver = + tryGetSolver(boundedConfig.indConfig.indSolver, boundedConfig.indConfig.validateIndSolver) + ?.createSolver(), + kindEnabled = { !boundedConfig.indConfig.disable }, + valToState = monolithicExpr.valToState, + biValToAction = monolithicExpr.biValToAction, + logger = logger, + ) + } + + val checker = + if (boundedConfig.cegar) { + val cegarChecker = + MonolithicExprCegarChecker( + monolithicExpr, + baseChecker, + logger, + getSolver(boundedConfig.bmcConfig.bmcSolver, false), + ) + object : + SafetyChecker< + EmptyProof, + Trace>, XcfaAction>, + XcfaPrec>, + > { + override fun check( + initPrec: XcfaPrec> + ): SafetyResult>, XcfaAction>> { + val result = + cegarChecker.check(initPrec.p.innerPrec) // states are PredState, actions are XcfaAction + if (result.isUnsafe) { + val cex = result.asUnsafe().cex as Trace + val locs = + (0 until cex.length()).map { i -> cex.actions[i].source } + + cex.actions[cex.length() - 1].target + val states = locs.mapIndexed { i, it -> XcfaState(xcfa, it, PtrState(cex.states[i])) } + return SafetyResult.unsafe(Trace.of(states, cex.actions), result.proof) + } else + return result + as SafetyResult>, XcfaAction>> + } + + override fun check(): + SafetyResult>, XcfaAction>> { + return check(boundedConfig.initPrec.predPrec(xcfa)) + } + } + } else { + baseChecker(monolithicExpr) + } + + return checker as SafetyChecker>, XcfaAction>, XcfaPrec<*>> } diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToMddChecker.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToMddChecker.kt index 27f9157197..d54ef19b04 100644 --- a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToMddChecker.kt +++ b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToMddChecker.kt @@ -16,6 +16,8 @@ package hu.bme.mit.theta.xcfa.cli.checkers import hu.bme.mit.theta.analysis.algorithm.SafetyChecker +import hu.bme.mit.theta.analysis.algorithm.bounded.createAbstract +import hu.bme.mit.theta.analysis.algorithm.bounded.createReversed import hu.bme.mit.theta.analysis.algorithm.mdd.MddCex import hu.bme.mit.theta.analysis.algorithm.mdd.MddChecker import hu.bme.mit.theta.analysis.algorithm.mdd.MddProof @@ -41,7 +43,14 @@ fun getMddChecker( val refinementSolverFactory: SolverFactory = getSolver(mddConfig.solver, mddConfig.validateSolver) - val monolithicExpr = xcfa.toMonolithicExpr(parseContext) + val monolithicExpr = + xcfa + .toMonolithicExpr(parseContext, initValues = true) + .let { if (mddConfig.reversed) it.createReversed() else it } + .let { + if (mddConfig.cegar) it.createAbstract(mddConfig.initPrec.predPrec(xcfa).p.innerPrec) + else it + } val initRel = monolithicExpr.initExpr val initIndexing = monolithicExpr.initOffsetIndex 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 3fdef63de1..73b52dbcda 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 @@ -284,6 +284,12 @@ data class HornConfig( data class BoundedConfig( @Parameter(names = ["--max-bound"], description = "Maximum bound to check. Use 0 for no limit.") var maxBound: Int = 0, + @Parameter(names = ["--reversed"], description = "Create a reversed monolithic expression") + var reversed: Boolean = false, + @Parameter(names = ["--cegar"], description = "Wrap the check in a predicate-based CEGAR loop") + var cegar: Boolean = false, + @Parameter(names = ["--initprec"], description = "Wrap the check in a predicate-based CEGAR loop") + var initPrec: InitPrec = InitPrec.EMPTY, val bmcConfig: BMCConfig = BMCConfig(), val indConfig: InductionConfig = InductionConfig(), val itpConfig: InterpolationConfig = InterpolationConfig(), @@ -393,6 +399,12 @@ data class MddConfig( description = "Iteration strategy for the MDD checker", ) var iterationStrategy: IterationStrategy = IterationStrategy.GSAT, + @Parameter(names = ["--reversed"], description = "Create a reversed monolithic expression") + var reversed: Boolean = false, + @Parameter(names = ["--cegar"], description = "Wrap the check in a predicate-based CEGAR loop") + var cegar: Boolean = false, + @Parameter(names = ["--initprec"], description = "Wrap the check in a predicate-based CEGAR loop") + var initPrec: InitPrec = InitPrec.EMPTY, ) : SpecBackendConfig data class OutputConfig( diff --git a/subprojects/xcfa/xcfa-cli/src/test/java/hu/bme/mit/theta/xcfa/cli/XcfaCliVerifyTest.kt b/subprojects/xcfa/xcfa-cli/src/test/java/hu/bme/mit/theta/xcfa/cli/XcfaCliVerifyTest.kt index 9b793c9136..0d767337e5 100644 --- a/subprojects/xcfa/xcfa-cli/src/test/java/hu/bme/mit/theta/xcfa/cli/XcfaCliVerifyTest.kt +++ b/subprojects/xcfa/xcfa-cli/src/test/java/hu/bme/mit/theta/xcfa/cli/XcfaCliVerifyTest.kt @@ -22,6 +22,7 @@ import hu.bme.mit.theta.frontend.chc.ChcFrontend import hu.bme.mit.theta.solver.smtlib.SmtLibSolverManager import hu.bme.mit.theta.xcfa.cli.XcfaCli.Companion.main import java.nio.file.Path +import java.util.concurrent.TimeUnit import java.util.stream.Stream import kotlin.io.path.absolutePathString import kotlin.io.path.createTempDirectory @@ -30,6 +31,7 @@ import org.junit.jupiter.api.Assertions import org.junit.jupiter.api.Assumptions import org.junit.jupiter.api.BeforeAll import org.junit.jupiter.api.Test +import org.junit.jupiter.api.Timeout import org.junit.jupiter.params.ParameterizedTest import org.junit.jupiter.params.provider.Arguments import org.junit.jupiter.params.provider.MethodSource @@ -113,6 +115,16 @@ class XcfaCliVerifyTest { ) } + @JvmStatic + fun finiteStateSpaceC(): Stream { + return Stream.of( + Arguments.of("/c/litmustest/singlethread/00assignment.c", null), + Arguments.of("/c/litmustest/singlethread/13typedef.c", "--domain PRED_CART"), + Arguments.of("/c/litmustest/singlethread/15addition.c", null), + Arguments.of("/c/litmustest/singlethread/20testinline.c", null), + ) + } + @JvmStatic fun cFilesShort(): Stream { return Stream.of( @@ -305,7 +317,8 @@ class XcfaCliVerifyTest { } @ParameterizedTest - @MethodSource("singleThreadedCFiles") + @MethodSource("finiteStateSpaceC") + @Timeout(value = 10, unit = TimeUnit.SECONDS, threadMode = Timeout.ThreadMode.SEPARATE_THREAD) fun testCVerifyMDD(filePath: String, extraArgs: String?) { val params = arrayOf(