Merge pull request #282 from ftsrg/horn-checker

Horn checker

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"))
 }

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")
 }

subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/chc/HornChecker.kt

@@ -0,0 +1,87 @@
+/*
+ *  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<Relation, Expr<BoolType>>) : 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<Relation>,
+    private val hornSolverFactory: SolverFactory,
+    private val logger: Logger,
+) : SafetyChecker<Invariant, CexTree, UnitPrec> {
+
+    override fun check(prec: UnitPrec?): SafetyResult<Invariant, CexTree> {
+        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<BoolType> ?: 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()
+            }
+        }
+    }
+
+}

subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/HornTest.kt

@@ -0,0 +1,62 @@
+/*
+ *  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.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
+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())
+        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() {
+        Assumptions.assumeTrue(OsHelper.getOs().equals(OsHelper.OperatingSystem.LINUX));
+
+        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)
+    }
+}

subprojects/solver/solver-smtlib/src/main/antlr/SMTLIBv2.g4

@@ -573,7 +573,7 @@ GRW_String
 
 Numeral
     : '0'
-    | [1-9] Digit*
+    | '-'? [1-9] Digit*
     ;
 
 Binary