Btor2Xcfa

settings.gradle.kts

@@ -25,6 +25,7 @@ include(
     "common/ltl-cli",
 
     "frontends/c-frontend",
+    "frontends/btor2-frontend",
     "frontends/petrinet-frontend/petrinet-model",
     "frontends/petrinet-frontend/petrinet-analysis",
     "frontends/petrinet-frontend/petrinet-xsts",
@@ -42,6 +43,7 @@ include(
     "xcfa/xcfa",
     "xcfa/cat",
     "xcfa/c2xcfa",
+    "xcfa/btor2xcfa",
     "xcfa/litmus2xcfa",
     "xcfa/llvm2xcfa",
     "xcfa/xcfa2chc",

subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/oc/OcChecker.kt

@@ -117,7 +117,7 @@ abstract class OcCheckerBase<E : Event> : OcChecker<E> {
     if (from == to) return reason // cycle (self-loop) found
     val toClose = mutableListOf(from to to to reason)
     while (toClose.isNotEmpty()) {
-      val (fromTo, r) = toClose.removeFirst()
+      val (fromTo, r) = toClose.removeAt(0)
       val (i1, i2) = fromTo
       check(i1 != i2)
       if (rels[i1][i2] != null) continue
@@ -160,7 +160,7 @@ abstract class OcCheckerBase<E : Event> : OcChecker<E> {
     val unassignedCopy = unassignedWss.toMutableList()
     val pairs = mutableListOf<Pair<Relation<E>, Relation<E>>>()
     while (unassignedCopy.isNotEmpty()) {
-      val ws = unassignedCopy.removeFirst()
+      val ws = unassignedCopy.removeAt(0)
       val pair = unassignedCopy.find { it.from == ws.to || it.to == ws.from }
       if (pair != null) {
         pairs.add(ws to pair)

subprojects/frontends/btor2-frontend/README.md

@@ -0,0 +1 @@
+Soon...

subprojects/frontends/btor2-frontend/build.gradle.kts

@@ -0,0 +1,24 @@
+/*
+ *  Copyright 2025 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.
+ */
+plugins {
+    id("kotlin-common")
+    id("antlr-grammar")
+}
+dependencies {
+    implementation(project(":theta-core"))
+    implementation(project(":theta-common"))
+    implementation(project(":theta-grammar"))
+}

subprojects/frontends/btor2-frontend/src/main/antlr/Btor2.g4

@@ -0,0 +1,74 @@
+// WARNING: this grammar is NOT an official BTOR2 grammar and will accept invalid btor2 circuits.
+// Check your circuit with catbtor before using this grammar!
+grammar Btor2;
+
+// Lexer rules
+WS: [ ]+ -> skip;
+UNARYOP: 'not'
+         | 'inc' | 'dec' | 'neg'
+         | 'redand' | 'redor' | 'redxor';
+TERNARYOP: 'ite' | 'write';
+BINOP: 'and' | 'nand' | 'nor' | 'or' | 'xnor' | 'xor' | 'iff' | 'implies'
+    | 'eq' | 'neq'
+    | 'slt' | 'slte' | 'sgt' | 'sgte'
+    | 'ult' | 'ulte' | 'ugt' | 'ugte'
+    | 'concat' | 'add' | 'mul' | 'sub'
+    | 'udiv' | 'urem'
+    | 'sdiv' | 'srem' | 'smod'
+    | 'saddo' | 'sdivo' | 'smulo' | 'ssubo'
+    | 'uaddo' | 'umulo' | 'usubo'
+    | 'rol' | 'ror' | 'sll' | 'sra' | 'srl' | 'read';
+NUM: (MINUS)? (HEX | BIN | DEC);
+HEX: [0-9a-fA-F]+;
+BIN: [0-1]+;
+DEC: [0-9]+;
+PLUS: '+';
+MINUS: '-';
+COMMENT: ';' ~[\r\n]+;
+SYMBOL: ~[ \r\n]+;
+NEWLINE: [\r\n]+;
+
+// Parser rules
+btor2: (line NEWLINE)* line (NEWLINE)* EOF;
+
+line: comment | node (symbol)? (comment)?;
+
+comment: COMMENT;
+
+nid: NUM;
+sid: NUM;
+
+node: ( array_sort | bitvec_sort ) #sort // sort declaration
+    | (input | state | init | next | property) #stateful
+    | (opidx | op) #operation
+    | (filled_constant | constant | constant_d | constant_h) #constantNode;
+
+opidx: ext | slice;
+
+ext: id=nid operator=('uext'|'sext') sid opd1=nid w=NUM;
+slice: id=nid 'slice' sid opd1=nid u=NUM l=NUM;
+
+op: binop | unop | terop;
+
+binop: id=nid BINOP sid opd1=nid opd2=nid;
+unop: id=nid UNARYOP sid opd1=nid;
+terop: id=nid TERNARYOP sid opd1=nid opd2=nid opd3=nid;
+
+input: id=nid ('input') sid;
+
+init: id=nid 'init' sid param1=nid param2=nid;
+next: id=nid 'next' sid param1=nid param2=nid;
+
+state: id=nid 'state' sid;
+
+property: id=nid property_type=('bad' | 'constraint' | 'fair' | 'output' | 'justice' ) param=nid;
+
+array_sort: id=sid 'sort array' sid1=sid sid2=sid;
+bitvec_sort: id=sid 'sort bitvec' width=NUM;
+
+constant: id=nid 'const' sid bin=NUM;
+constant_d: id=nid 'constd' sid dec=NUM;
+constant_h: id=nid 'consth' sid hex=NUM;
+filled_constant: id=nid fill=('one' | 'ones' | 'zero') sid;
+
+symbol: (SYMBOL | NUM);

subprojects/frontends/btor2-frontend/src/main/java/hu/bme/mit/theta/frontend/models/Btor2Const.kt

@@ -0,0 +1,42 @@
+/*
+ *  Copyright 2025 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.frontend.models
+
+import hu.bme.mit.theta.core.decl.Decls
+import hu.bme.mit.theta.core.decl.VarDecl
+import hu.bme.mit.theta.core.type.Expr
+import hu.bme.mit.theta.core.type.bvtype.BvExprs
+import hu.bme.mit.theta.core.type.bvtype.BvType
+
+data class Btor2Const(
+  override val nid: UInt,
+  val value: BooleanArray,
+  override val sort: Btor2Sort,
+) : Btor2Node(nid, sort) {
+  val declsVar = Decls.Var("const_$nid", BvExprs.BvType(sort.width.toInt()))
+
+  override fun getVar(): VarDecl<*>? {
+    return declsVar
+  }
+
+  override fun getExpr(): Expr<BvType> {
+    return declsVar.ref as Expr<BvType>
+  }
+
+  override fun <R, P> accept(visitor: Btor2NodeVisitor<R, P>, param: P): R {
+    return visitor.visit(this, param)
+  }
+}

subprojects/frontends/btor2-frontend/src/main/java/hu/bme/mit/theta/frontend/models/Btor2Model.kt

@@ -0,0 +1,114 @@
+/*
+ *  Copyright 2025 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.frontend.models
+
+import hu.bme.mit.theta.core.decl.VarDecl
+import hu.bme.mit.theta.core.type.Expr
+
+interface Btor2NodeVisitor<R, P> {
+  fun visit(node: Btor2UnaryOperation, param: P): R
+
+  fun visit(node: Btor2BinaryOperation, param: P): R
+
+  fun visit(node: Btor2TernaryOperation, param: P): R
+
+  fun visit(node: Btor2SliceOperation, param: P): R
+
+  fun visit(node: Btor2ExtOperation, param: P): R
+
+  fun visit(node: Btor2Comparison, param: P): R
+
+  fun visit(node: Btor2Boolean, param: P): R
+
+  fun visit(node: Btor2BitvecSort, param: P): R
+
+  fun visit(node: Btor2Input, param: P): R
+
+  fun visit(node: Btor2State, param: P): R
+
+  fun visit(node: Btor2Init, param: P): R
+
+  fun visit(node: Btor2Next, param: P): R
+
+  fun visit(node: Btor2Bad, param: P): R
+
+  fun visit(node: Btor2Const, param: P): R
+}
+
+object Btor2Circuit {
+  private val _nodes = mutableMapOf<UInt, Btor2Node>()
+  private val _sorts = mutableMapOf<UInt, Btor2Sort>()
+  private val _constants = mutableMapOf<UInt, Btor2Const>()
+  private val _ops = mutableMapOf<UInt, Btor2Operation>()
+  private val _states = mutableMapOf<UInt, Btor2Stateful>()
+  private val _properties = mutableMapOf<UInt, Btor2Bad>()
+
+  val nodes: Map<UInt, Btor2Node>
+    get() = _nodes
+
+  val sorts: Map<UInt, Btor2Sort>
+    get() = _sorts
+
+  val constants: Map<UInt, Btor2Const>
+    get() = _constants
+
+  val ops: Map<UInt, Btor2Operation>
+    get() = _ops
+
+  val states: Map<UInt, Btor2Stateful>
+    get() = _states
+
+  val properties: Map<UInt, Btor2Bad>
+    get() = _properties
+
+  fun addSort(sort: Btor2Sort) {
+    _sorts[sort.sid] = sort
+  }
+
+  fun addNode(node: Btor2Node) {
+    _nodes[node.nid] = node
+    when (node) {
+      is Btor2Const -> _constants[node.nid] = node
+      is Btor2Operation -> _ops[node.nid] = node
+      is Btor2Stateful -> _states[node.nid] = node
+      is Btor2Bad -> _properties[node.nid] = node
+      else -> error("Btor2Circuit cannot sort this type: ${node.javaClass}")
+    }
+  }
+}
+
+// sortID lookup in Btor2Sort
+abstract class Btor2Node(id: UInt, btor2Sort: Btor2Sort? = null) {
+  abstract val nid: UInt
+  abstract val sort: Btor2Sort?
+
+  open fun getVar(): VarDecl<*>? {
+    return null
+  }
+
+  abstract fun <R, P> accept(visitor: Btor2NodeVisitor<R, P>, param: P): R
+
+  abstract fun getExpr(): Expr<*>
+}
+
+abstract class Btor2Sort(sid: UInt, width: UInt) {
+  abstract val sid: UInt
+  abstract val width: UInt
+}
+
+// Ezt egyelőre nem használjuk mert csak bitvektoraink vannak
+data class Btor2BitvecSort(override val sid: UInt, override val width: UInt) :
+  Btor2Sort(sid, width)