From 5ea52be2ef946ea4f48a9c2cb8691e6802abf431 Mon Sep 17 00:00:00 2001 From: Levente Bajczi Date: Tue, 16 Jul 2024 12:26:41 +0200 Subject: [PATCH 1/7] Added HornChecker --- .../analysis/algorithm/chc/HornChecker.kt | 83 +++++++++++++++++++ .../mit/theta/solver/z3/Z3SolverManager.java | 9 ++ .../hu/bme/mit/theta/solver/ProofNode.java | 4 + .../xcfa/cli/checkers/ConfigToChecker.kt | 1 + .../xcfa/cli/checkers/ConfigToHornChecker.kt | 68 +++++++++++++++ .../mit/theta/xcfa/cli/params/ParamValues.kt | 1 + .../mit/theta/xcfa/cli/params/XcfaConfig.kt | 11 +++ 7 files changed, 177 insertions(+) create mode 100644 subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/chc/HornChecker.kt create mode 100644 subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToHornChecker.kt diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/chc/HornChecker.kt b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/chc/HornChecker.kt new file mode 100644 index 0000000000..0abb39e445 --- /dev/null +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/chc/HornChecker.kt @@ -0,0 +1,83 @@ +/* + * 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.chc + +import hu.bme.mit.theta.analysis.Cex +import hu.bme.mit.theta.analysis.algorithm.SafetyChecker +import hu.bme.mit.theta.analysis.algorithm.SafetyResult +import hu.bme.mit.theta.analysis.algorithm.Witness +import hu.bme.mit.theta.analysis.unit.UnitPrec +import hu.bme.mit.theta.common.logging.Logger +import hu.bme.mit.theta.core.Relation +import hu.bme.mit.theta.core.type.Expr +import hu.bme.mit.theta.core.type.booltype.BoolExprs.True +import hu.bme.mit.theta.core.type.booltype.BoolType +import hu.bme.mit.theta.solver.ProofNode +import hu.bme.mit.theta.solver.SolverFactory +import hu.bme.mit.theta.solver.SolverStatus + +data class Invariant(val lookup: Map>) : Witness + +data class CexTree(val proofNode: ProofNode) : Cex { + override fun length(): Int = proofNode.depth() +} + +/** + * A checker for CHC-based verification. + */ +class HornChecker( + private val relations: List, + private val hornSolverFactory: SolverFactory, + private val logger: Logger, +) : SafetyChecker { + + override fun check(prec: UnitPrec?): SafetyResult { + val solver = hornSolverFactory.createHornSolver() + logger.write(Logger.Level.MAINSTEP, "Starting encoding\n") + solver.add(relations) + logger.write(Logger.Level.DETAIL, "Relations:\n\t${ + relations.joinToString("\n\t") { + it.constDecl.toString() + } + }\n") + logger.write(Logger.Level.DETAIL, "Rules:\n\t${ + solver.assertions.joinToString("\n\t") { + it.toString().replace(Regex("[\r\n\t ]+"), " ") + } + }\n") + logger.write(Logger.Level.MAINSTEP, "Added constraints to solver\n") + solver.check() + logger.write(Logger.Level.MAINSTEP, "Check() finished (result: ${solver.status})\n") + return when (solver.status) { + SolverStatus.SAT -> { + logger.write(Logger.Level.MAINSTEP, "Proof (model) found\n") + val model = solver.model.toMap() + SafetyResult.safe(Invariant(relations.associateWith { model[it.constDecl] as? Expr ?: True() })) + } + SolverStatus.UNSAT -> { + logger.write(Logger.Level.MAINSTEP, "Counterexample found\n") + val proof = solver.proof + SafetyResult.unsafe(CexTree(proof), Invariant(emptyMap())) + } + else -> { + logger.write(Logger.Level.MAINSTEP, "No solution found.\n") + SafetyResult.unknown() + } + } + } + +} \ No newline at end of file diff --git a/subprojects/solver/solver-z3/src/main/java/hu/bme/mit/theta/solver/z3/Z3SolverManager.java b/subprojects/solver/solver-z3/src/main/java/hu/bme/mit/theta/solver/z3/Z3SolverManager.java index 22a4b2768d..890408b304 100644 --- a/subprojects/solver/solver-z3/src/main/java/hu/bme/mit/theta/solver/z3/Z3SolverManager.java +++ b/subprojects/solver/solver-z3/src/main/java/hu/bme/mit/theta/solver/z3/Z3SolverManager.java @@ -15,6 +15,7 @@ */ package hu.bme.mit.theta.solver.z3; +import hu.bme.mit.theta.solver.HornSolver; import hu.bme.mit.theta.solver.ItpSolver; import hu.bme.mit.theta.solver.Solver; import hu.bme.mit.theta.solver.SolverBase; @@ -92,5 +93,13 @@ public ItpSolver createItpSolver() { instantiatedSolvers.add(solver); return solver; } + + @Override + public HornSolver createHornSolver() { + checkState(!closed, "Solver manager was closed"); + final var solver = solverFactory.createHornSolver(); + instantiatedSolvers.add(solver); + return solver; + } } } diff --git a/subprojects/solver/solver/src/main/java/hu/bme/mit/theta/solver/ProofNode.java b/subprojects/solver/solver/src/main/java/hu/bme/mit/theta/solver/ProofNode.java index 9cf1ade5e0..847816ce07 100644 --- a/subprojects/solver/solver/src/main/java/hu/bme/mit/theta/solver/ProofNode.java +++ b/subprojects/solver/solver/src/main/java/hu/bme/mit/theta/solver/ProofNode.java @@ -32,6 +32,10 @@ public AndExpr toExpr() { return And(Stream.concat(Stream.of(expr), children.stream().flatMap(it -> it.toExpr().getOps().stream())).toList()); } + public int depth() { + return children.stream().map(ProofNode::depth).max(Integer::compareTo).orElse(0); + } + public String toString() { final var sj = new StringJoiner(", "); children.stream().map(ProofNode::id).forEach(it -> sj.add(it.toString())); 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 74877fecaf..4bd2dce149 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 @@ -44,6 +44,7 @@ fun getChecker(xcfa: XCFA, mcm: MCM, config: XcfaConfig<*, *>, parseContext: Par Backend.LAZY -> TODO() 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) } } 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 new file mode 100644 index 0000000000..c181a63429 --- /dev/null +++ b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToHornChecker.kt @@ -0,0 +1,68 @@ +/* + * 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.Trace +import hu.bme.mit.theta.analysis.algorithm.EmptyWitness +import hu.bme.mit.theta.analysis.algorithm.SafetyChecker +import hu.bme.mit.theta.analysis.algorithm.SafetyResult +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.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.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.xcfa2chc.toCHC +import org.abego.treelayout.internal.util.Contract.checkState + +fun getHornChecker(xcfa: XCFA, mcm: MCM, config: XcfaConfig<*, *>, logger: Logger): + SafetyChecker>, XcfaAction>, XcfaPrec<*>> { + + checkState(xcfa.isInlined, "Only inlined XCFAs work right now") + checkState(xcfa.initProcedures.size == 1, "Only one-procedure XCFAs work right now") + + val hornConfig = config.backendConfig.specConfig as HornConfig + + val checker = HornChecker( + relations = xcfa.initProcedures[0].first.toCHC(), + hornSolverFactory = getSolver(hornConfig.solver, hornConfig.validateSolver), + logger = logger, + ) + + return SafetyChecker>, XcfaAction>, XcfaPrec<*>> { + val result = checker.check(null) + + if(result.isSafe) { + SafetyResult.safe(EmptyWitness.getInstance()) + } else if (result.isUnsafe) { + val proof = result.asUnsafe().cex + val state = XcfaState>(xcfa, mapOf(), PtrState(PredState.of(proof.proofNode.expr))) + //TODO: actual counterexample + SafetyResult.unsafe(Trace.of(listOf(state), listOf()), EmptyWitness.getInstance()) + } else{ + SafetyResult.unknown() + } + } + +} \ 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 14ec7e6bec..ac5b3d3236 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 @@ -66,6 +66,7 @@ enum class InputType { enum class Backend { CEGAR, BOUNDED, + CHC, OC, LAZY, PORTFOLIO, 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 5c5af6f576..ef50a1e108 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 @@ -165,6 +165,7 @@ data class BackendConfig( specConfig = when (backend) { Backend.CEGAR -> CegarConfig() as T Backend.BOUNDED -> BoundedConfig() as T + Backend.CHC -> HornConfig() as T Backend.OC -> OcConfig() as T Backend.LAZY -> null Backend.PORTFOLIO -> PortfolioConfig() as T @@ -242,6 +243,16 @@ data class CegarRefinerConfig( var pruneStrategy: PruneStrategy = PruneStrategy.LAZY, ) : Config +data class HornConfig( + @Parameter(names = ["--solver"], description = "Solver to use.") + var solver: String = "Z3:4.13", + @Parameter( + names = ["--validate-solver"], + description = "Activates a wrapper, which validates the assertions in the solver in each (SAT) check. Filters some solver issues." + ) + var validateSolver: Boolean = false, +) : SpecBackendConfig + data class BoundedConfig( @Parameter(names = ["--max-bound"], description = "Maximum bound to check. Use 0 for no limit.") var maxBound: Int = 0, From f2fd0ffdb3780c7468db93bd5a96c918dcef6714 Mon Sep 17 00:00:00 2001 From: Levente Bajczi Date: Thu, 18 Jul 2024 00:15:00 +0200 Subject: [PATCH 2/7] Added negative number paring and changed bimap to stack --- .../solver-smtlib/src/main/antlr/SMTLIBv2.g4 | 2 +- .../generic/GenericSmtLibTermTransformer.java | 61 +++++++++---------- 2 files changed, 30 insertions(+), 33 deletions(-) diff --git a/subprojects/solver/solver-smtlib/src/main/antlr/SMTLIBv2.g4 b/subprojects/solver/solver-smtlib/src/main/antlr/SMTLIBv2.g4 index d58649115c..5047b6aca2 100644 --- a/subprojects/solver/solver-smtlib/src/main/antlr/SMTLIBv2.g4 +++ b/subprojects/solver/solver-smtlib/src/main/antlr/SMTLIBv2.g4 @@ -573,7 +573,7 @@ GRW_String Numeral : '0' - | [1-9] Digit* + | '-'? [1-9] Digit* ; Binary diff --git a/subprojects/solver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/impl/generic/GenericSmtLibTermTransformer.java b/subprojects/solver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/impl/generic/GenericSmtLibTermTransformer.java index 47bea40577..22402fba62 100644 --- a/subprojects/solver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/impl/generic/GenericSmtLibTermTransformer.java +++ b/subprojects/solver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/impl/generic/GenericSmtLibTermTransformer.java @@ -15,15 +15,12 @@ */ package hu.bme.mit.theta.solver.smtlib.impl.generic; -import com.google.common.collect.BiMap; -import com.google.common.collect.HashBiMap; import com.google.common.collect.ImmutableList; import com.google.common.collect.Lists; import hu.bme.mit.theta.common.QuadFunction; import hu.bme.mit.theta.common.TernaryOperator; import hu.bme.mit.theta.common.TriFunction; import hu.bme.mit.theta.common.Tuple2; -import hu.bme.mit.theta.core.decl.Decl; import hu.bme.mit.theta.core.decl.ParamDecl; import hu.bme.mit.theta.core.model.BasicSubstitution; import hu.bme.mit.theta.core.type.Expr; @@ -81,7 +78,6 @@ import hu.bme.mit.theta.core.type.bvtype.BvURemExpr; import hu.bme.mit.theta.core.type.bvtype.BvXorExpr; import hu.bme.mit.theta.core.type.bvtype.BvZExtExpr; -import hu.bme.mit.theta.core.type.enumtype.EnumLitExpr; import hu.bme.mit.theta.core.type.enumtype.EnumType; import hu.bme.mit.theta.core.type.fptype.FpAbsExpr; import hu.bme.mit.theta.core.type.fptype.FpAddExpr; @@ -110,6 +106,8 @@ import hu.bme.mit.theta.core.type.rattype.RatToIntExpr; import hu.bme.mit.theta.core.utils.BvUtils; import hu.bme.mit.theta.core.utils.ExprUtils; +import hu.bme.mit.theta.solver.Stack; +import hu.bme.mit.theta.solver.impl.StackImpl; import hu.bme.mit.theta.solver.smtlib.dsl.gen.SMTLIBv2Lexer; import hu.bme.mit.theta.solver.smtlib.dsl.gen.SMTLIBv2Parser; import hu.bme.mit.theta.solver.smtlib.solver.SmtLibEnumStrategy; @@ -296,7 +294,7 @@ private Expr toFuncLitExpr(final String funcLitImpl, final SmtLibModel model) parser.removeErrorListeners(); parser.addErrorListener(new ThrowExceptionErrorListener()); - return transformFuncDef(parser.function_def(), model, HashBiMap.create()); + return transformFuncDef(parser.function_def(), model, new StackImpl<>()); } @Override @@ -314,7 +312,7 @@ private Expr toExpr(final String term, final SmtLibModel model) { parser.removeErrorListeners(); parser.addErrorListener(new ThrowExceptionErrorListener()); - return transformTerm(parser.term(), model, HashBiMap.create()); + return transformTerm(parser.term(), model, new StackImpl<>()); } @Override @@ -346,7 +344,7 @@ private Expr toLitExpr(final String litImpl, final SmtLibModel model) { .map(sv -> Param(sv.symbol().getText(), transformSort(sv.sort()))) .collect(toList()); - final var vars = HashBiMap., String>create(); + final var vars = new StackImpl>(); pushParams(paramDecls, vars); final var expr = transformTerm(funcDef.term(), model, vars); popParams(paramDecls, vars); @@ -410,7 +408,7 @@ public LitExpr toBvLitExpr(final String bvLitImpl, final BvType type, /* Visitor implementation */ protected Expr transformFuncDef(final SMTLIBv2Parser.Function_defContext ctx, - final SmtLibModel model, final BiMap, String> vars) { + final SmtLibModel model, final Stack> vars) { assert model != null; assert vars != null; @@ -428,7 +426,7 @@ protected Expr transformFuncDef(final SMTLIBv2Parser.Function_defContext ctx, } protected Expr transformTerm(final TermContext ctx, final SmtLibModel model, - final BiMap, String> vars) { + final Stack> vars) { assert model != null; assert vars != null; @@ -454,7 +452,7 @@ protected Expr transformTerm(final TermContext ctx, final SmtLibModel model, } protected Expr transformSpecConstant(final Spec_constantContext ctx, final SmtLibModel model, - final BiMap, String> vars) { + final Stack> vars) { assert model != null; assert vars != null; @@ -474,7 +472,7 @@ protected Expr transformSpecConstant(final Spec_constantContext ctx, final Sm } protected Expr transformQualIdentifier(final Qual_identifierContext ctx, - final SmtLibModel model, final BiMap, String> vars) { + final SmtLibModel model, final Stack> vars) { assert model != null; assert vars != null; @@ -482,7 +480,7 @@ protected Expr transformQualIdentifier(final Qual_identifierContext ctx, } protected Expr transformGenericTerm(final Generic_termContext ctx, final SmtLibModel model, - final BiMap, String> vars) { + final Stack> vars) { assert model != null; assert vars != null; @@ -521,7 +519,7 @@ private Expr createArrayLitExpr(final Expr Expr createFuncAppExpr(final String funName, final List funAppParams, final SmtLibModel model, - final BiMap, String> vars) { + final Stack> vars) { final Expr funcExpr; if (symbolTable.definesSymbol(funName)) { funcExpr = checkNotNull(symbolTable.getConst(funName).getRef()); @@ -538,7 +536,7 @@ private

Expr createFuncAppExpr(final String } protected Expr transformLetTerm(final Let_termContext ctx, final SmtLibModel model, - final BiMap, String> vars) { + final Stack> vars) { assert model != null; assert vars != null; @@ -565,7 +563,7 @@ protected Expr transformLetTerm(final Let_termContext ctx, final SmtLibModel } protected Expr transformForallTerm(final Forall_termContext ctx, final SmtLibModel model, - final BiMap, String> vars) { + final Stack> vars) { assert model != null; assert vars != null; @@ -582,7 +580,7 @@ protected Expr transformForallTerm(final Forall_termContext ctx, final SmtLib } protected Expr transformExistsTerm(final Exists_termContext ctx, final SmtLibModel model, - final BiMap, String> vars) { + final Stack> vars) { assert model != null; assert vars != null; @@ -599,7 +597,7 @@ protected Expr transformExistsTerm(final Exists_termContext ctx, final SmtLib } protected Expr transformIdentifier(final IdentifierContext ctx, final SmtLibModel model, - final BiMap, String> vars) { + final Stack> vars) { assert model != null; assert vars != null; @@ -633,7 +631,7 @@ protected Expr transformIdentifier(final IdentifierContext ctx, final SmtLibM } protected Expr transformSymbol(final SymbolContext ctx, final SmtLibModel model, - final BiMap, String> vars) { + final Stack> vars) { assert model != null; assert vars != null; @@ -644,8 +642,9 @@ protected Expr transformSymbol(final SymbolContext ctx, final SmtLibModel mod case "false": return BoolExprs.False(); default: - if (vars.containsValue(value)) { - final var decl = vars.inverse().get(value); + final var filter = vars.toCollection().stream().filter(it -> it.getName().equals(value)).toList(); + if (!filter.isEmpty()) { + final var decl = filter.get(filter.size() - 1); return decl.getRef(); } else if (symbolTable.definesSymbol(value)) { return symbolTable.getConst(value).getRef(); @@ -658,7 +657,7 @@ protected Expr transformSymbol(final SymbolContext ctx, final SmtLibModel mod } protected Expr transformNumeral(final NumeralContext ctx, final SmtLibModel model, - final BiMap, String> vars) { + final Stack> vars) { assert model != null; assert vars != null; @@ -666,7 +665,7 @@ protected Expr transformNumeral(final NumeralContext ctx, final SmtLibModel m } protected Expr transformDecimal(final DecimalContext ctx, final SmtLibModel model, - final BiMap, String> vars) { + final Stack> vars) { assert model != null; assert vars != null; @@ -679,7 +678,7 @@ protected Expr transformDecimal(final DecimalContext ctx, final SmtLibModel m } protected Expr transformHexadecimal(final HexadecimalContext ctx, final SmtLibModel model, - final BiMap, String> vars) { + final Stack> vars) { assert model != null; assert vars != null; @@ -689,7 +688,7 @@ protected Expr transformHexadecimal(final HexadecimalContext ctx, final SmtLi } protected Expr transformBinary(final BinaryContext ctx, final SmtLibModel model, - final BiMap, String> vars) { + final Stack> vars) { assert model != null; assert vars != null; @@ -723,16 +722,14 @@ protected Type transformSort(final SortContext ctx) { /* Variable scope handling */ protected void pushParams(final List> paramDecls, - BiMap, String> vars) { - vars.putAll(paramDecls.stream() - .collect(Collectors.toUnmodifiableMap(Function.identity(), Decl::getName))); + Stack> vars) { + vars.push(); + vars.add(paramDecls); } protected void popParams(final List> paramDecls, - BiMap, String> vars) { - for (final var paramDecl : paramDecls) { - vars.remove(paramDecl, paramDecl.getName()); - } + Stack> vars) { + vars.pop(); } /* Utilities */ @@ -971,7 +968,7 @@ private interface OperatorCreatorFunction extends QuadFunction< List, // Parameters List, // Operands SmtLibModel, // The model - BiMap, String>, // The variable (param) store + Stack>, // The variable (param) store Expr // Return type > { From 60206a25d1f1c3dbf56d7609e6e2fc43d46a0384 Mon Sep 17 00:00:00 2001 From: Levente Bajczi Date: Thu, 18 Jul 2024 00:16:11 +0200 Subject: [PATCH 3/7] Removed comment --- .../hu/bme/mit/theta/xcfa/cli/checkers/ConfigToHornChecker.kt | 1 - 1 file changed, 1 deletion(-) 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 c181a63429..f4b8633912 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 @@ -58,7 +58,6 @@ fun getHornChecker(xcfa: XCFA, mcm: MCM, config: XcfaConfig<*, *>, logger: Logge } else if (result.isUnsafe) { val proof = result.asUnsafe().cex val state = XcfaState>(xcfa, mapOf(), PtrState(PredState.of(proof.proofNode.expr))) - //TODO: actual counterexample SafetyResult.unsafe(Trace.of(listOf(state), listOf()), EmptyWitness.getInstance()) } else{ SafetyResult.unknown() From 810bf29ae4816d8ecddc39ce640bf25deb886e5c Mon Sep 17 00:00:00 2001 From: "ThetaBotMaintainer[bot]" <139346997+ThetaBotMaintainer[bot]@users.noreply.github.com> Date: Wed, 17 Jul 2024 22:19:48 +0000 Subject: [PATCH 4/7] Version bump --- build.gradle.kts | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/build.gradle.kts b/build.gradle.kts index 834767ac52..6d975998c8 100644 --- a/build.gradle.kts +++ b/build.gradle.kts @@ -28,7 +28,7 @@ buildscript { allprojects { group = "hu.bme.mit.theta" - version = "6.0.0" + version = "6.1.0" apply(from = rootDir.resolve("gradle/shared-with-buildSrc/mirrors.gradle.kts")) } From 7706018e1ddd6da07458e799420e447cacad7ad0 Mon Sep 17 00:00:00 2001 From: "ThetaBotMaintainer[bot]" <139346997+ThetaBotMaintainer[bot]@users.noreply.github.com> Date: Wed, 17 Jul 2024 22:22:00 +0000 Subject: [PATCH 5/7] Reformatted code --- .../hu/bme/mit/theta/analysis/algorithm/chc/HornChecker.kt | 6 +++++- .../bme/mit/theta/xcfa/cli/checkers/ConfigToHornChecker.kt | 4 ++-- 2 files changed, 7 insertions(+), 3 deletions(-) diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/chc/HornChecker.kt b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/chc/HornChecker.kt index 0abb39e445..0c083b7cd0 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/chc/HornChecker.kt +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/chc/HornChecker.kt @@ -33,6 +33,7 @@ import hu.bme.mit.theta.solver.SolverStatus data class Invariant(val lookup: Map>) : Witness data class CexTree(val proofNode: ProofNode) : Cex { + override fun length(): Int = proofNode.depth() } @@ -66,13 +67,16 @@ class HornChecker( SolverStatus.SAT -> { logger.write(Logger.Level.MAINSTEP, "Proof (model) found\n") val model = solver.model.toMap() - SafetyResult.safe(Invariant(relations.associateWith { model[it.constDecl] as? Expr ?: True() })) + SafetyResult.safe( + Invariant(relations.associateWith { model[it.constDecl] as? Expr ?: True() })) } + SolverStatus.UNSAT -> { logger.write(Logger.Level.MAINSTEP, "Counterexample found\n") val proof = solver.proof SafetyResult.unsafe(CexTree(proof), Invariant(emptyMap())) } + else -> { logger.write(Logger.Level.MAINSTEP, "No solution found.\n") SafetyResult.unknown() 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 f4b8633912..dd63b5eb48 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 @@ -53,13 +53,13 @@ fun getHornChecker(xcfa: XCFA, mcm: MCM, config: XcfaConfig<*, *>, logger: Logge return SafetyChecker>, XcfaAction>, XcfaPrec<*>> { val result = checker.check(null) - if(result.isSafe) { + if (result.isSafe) { SafetyResult.safe(EmptyWitness.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()), EmptyWitness.getInstance()) - } else{ + } else { SafetyResult.unknown() } } From e79bd009c798a5bb7403338eb528209010616e02 Mon Sep 17 00:00:00 2001 From: Levente Bajczi Date: Thu, 18 Jul 2024 01:07:54 +0200 Subject: [PATCH 6/7] Added tests --- subprojects/common/analysis/build.gradle.kts | 1 + .../mit/theta/analysis/algorithm/HornTest.kt | 56 +++++++++++++++++++ 2 files changed, 57 insertions(+) create mode 100644 subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/HornTest.kt diff --git a/subprojects/common/analysis/build.gradle.kts b/subprojects/common/analysis/build.gradle.kts index b11621e1c0..f8205f008d 100644 --- a/subprojects/common/analysis/build.gradle.kts +++ b/subprojects/common/analysis/build.gradle.kts @@ -29,5 +29,6 @@ dependencies { implementation(project(":theta-graph-solver")) implementation(project(mapOf("path" to ":theta-solver-z3-legacy"))) testImplementation(project(":theta-solver-z3-legacy")) + testImplementation(project(":theta-solver-z3")) implementation("com.corundumstudio.socketio:netty-socketio:2.0.6") } diff --git a/subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/HornTest.kt b/subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/HornTest.kt new file mode 100644 index 0000000000..89993cfc8e --- /dev/null +++ b/subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/HornTest.kt @@ -0,0 +1,56 @@ +/* + * 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 + +import hu.bme.mit.theta.analysis.algorithm.chc.HornChecker +import hu.bme.mit.theta.common.logging.NullLogger +import hu.bme.mit.theta.core.Relation +import hu.bme.mit.theta.core.decl.Decls.Param +import hu.bme.mit.theta.core.plus +import hu.bme.mit.theta.core.type.inttype.IntExprs.* +import hu.bme.mit.theta.solver.z3.Z3SolverFactory +import org.junit.jupiter.api.Assertions +import org.junit.jupiter.api.Test + +class HornTest { + + @Test + fun testHornUnsafe() { + val inv = Relation("inv", Int()) + val p0 = Param("P0", Int()) + val p1 = Param("P1", Int()) + inv(p0.ref) += Eq(p0.ref, Int(0)) + inv(p1.ref) += inv(p0.ref).expr + Eq(p1.ref, Add(p0.ref, Int(1))) + !(inv(p0.ref) with Eq(p0.ref, Int(5))) + + val checker = HornChecker(listOf(inv), Z3SolverFactory.getInstance(), NullLogger.getInstance()) + Assertions.assertTrue(checker.check().isUnsafe) + } + + @Test + fun testHornSafe() { + val inv = Relation("inv", Int()) + val p0 = Param("P0", Int()) + val p1 = Param("P1", Int()) + inv(p0.ref) += Eq(p0.ref, Int(0)) + inv(p1.ref) += inv(p0.ref).expr + Eq(p1.ref, Add(p0.ref, Int(2))) + !(inv(p0.ref) with Eq(p0.ref, Int(5))) + + val checker = HornChecker(listOf(inv), Z3SolverFactory.getInstance(), NullLogger.getInstance()) + Assertions.assertTrue(checker.check().isSafe) + } +} \ No newline at end of file From 242d55e1aa6abbc6ca4e49343dc9957cb2422f5f Mon Sep 17 00:00:00 2001 From: Levente Bajczi Date: Thu, 18 Jul 2024 01:31:51 +0200 Subject: [PATCH 7/7] Added more tests --- .../mit/theta/analysis/algorithm/HornTest.kt | 6 ++++ .../mit/theta/xcfa/cli/XcfaCliVerifyTest.kt | 30 +++++++++++++++++++ 2 files changed, 36 insertions(+) diff --git a/subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/HornTest.kt b/subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/HornTest.kt index 89993cfc8e..c0eee6f1f3 100644 --- a/subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/HornTest.kt +++ b/subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/HornTest.kt @@ -17,6 +17,7 @@ package hu.bme.mit.theta.analysis.algorithm import hu.bme.mit.theta.analysis.algorithm.chc.HornChecker +import hu.bme.mit.theta.common.OsHelper import hu.bme.mit.theta.common.logging.NullLogger import hu.bme.mit.theta.core.Relation import hu.bme.mit.theta.core.decl.Decls.Param @@ -24,12 +25,15 @@ import hu.bme.mit.theta.core.plus import hu.bme.mit.theta.core.type.inttype.IntExprs.* import hu.bme.mit.theta.solver.z3.Z3SolverFactory import org.junit.jupiter.api.Assertions +import org.junit.jupiter.api.Assumptions import org.junit.jupiter.api.Test class HornTest { @Test fun testHornUnsafe() { + Assumptions.assumeTrue(OsHelper.getOs().equals(OsHelper.OperatingSystem.LINUX)); + val inv = Relation("inv", Int()) val p0 = Param("P0", Int()) val p1 = Param("P1", Int()) @@ -43,6 +47,8 @@ class HornTest { @Test fun testHornSafe() { + Assumptions.assumeTrue(OsHelper.getOs().equals(OsHelper.OperatingSystem.LINUX)); + val inv = Relation("inv", Int()) val p0 = Param("P0", Int()) val p1 = Param("P1", Int()) 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 18fcb28e58..335211363e 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 @@ -15,9 +15,11 @@ */ package hu.bme.mit.theta.xcfa.cli +import hu.bme.mit.theta.common.OsHelper import hu.bme.mit.theta.frontend.chc.ChcFrontend import hu.bme.mit.theta.xcfa.cli.XcfaCli.Companion.main import org.junit.jupiter.api.Assertions +import org.junit.jupiter.api.Assumptions import org.junit.jupiter.api.Test import org.junit.jupiter.params.ParameterizedTest import org.junit.jupiter.params.provider.Arguments @@ -87,6 +89,19 @@ class XcfaCliVerifyTest { ) } + @JvmStatic + fun cFilesShortInt(): Stream { + return Stream.of( + Arguments.of("/c/litmustest/singlethread/00assignment.c", null), + Arguments.of("/c/litmustest/singlethread/01cast.c", null), + Arguments.of("/c/litmustest/singlethread/02types.c", null), + Arguments.of("/c/litmustest/singlethread/15addition.c", null), + Arguments.of("/c/litmustest/singlethread/20testinline.c", null), + Arguments.of("/c/litmustest/singlethread/21namecollision.c", null), + Arguments.of("/c/litmustest/singlethread/22nondet.c", null), + ) + } + @JvmStatic fun chcFiles(): Stream { return Stream.of( @@ -239,4 +254,19 @@ class XcfaCliVerifyTest { main(params) } + @ParameterizedTest + @MethodSource("cFilesShortInt") + fun testCVerifyCHC(filePath: String, extraArgs: String?) { + Assumptions.assumeTrue(OsHelper.getOs().equals(OsHelper.OperatingSystem.LINUX)); + + val params = arrayOf( + "--backend", "CHC", + "--input-type", "C", + "--input", javaClass.getResource(filePath)!!.path, + "--stacktrace", + "--debug" + ) + main(params) + } + }