From 36dcfc2b0d085e5d738eefc839288878502950bb Mon Sep 17 00:00:00 2001 From: AdamZsofi Date: Tue, 25 Jul 2023 16:57:43 +0200 Subject: [PATCH] Added const visitor --- .../theta/frontend/model/Btor2Declarations.kt | 28 +++++-- .../bme/mit/theta/frontend/model/Btor2Node.kt | 2 +- .../theta/frontend/model/Btor2NodeVisitor.kt | 30 +++---- .../theta/frontend/model/Btor2Operators.kt | 20 ++--- .../theta/frontend/model/Btor2StateNodes.kt | 28 +++---- .../btor22xcfa/Btor2FrontendXcfaBuilder.kt | 79 ++++++++++++------- 6 files changed, 114 insertions(+), 73 deletions(-) diff --git a/subprojects/frontends/btor2-frontend/src/main/java/hu/bme/mit/theta/frontend/model/Btor2Declarations.kt b/subprojects/frontends/btor2-frontend/src/main/java/hu/bme/mit/theta/frontend/model/Btor2Declarations.kt index 3cb1f5b4ec..615f8c0335 100644 --- a/subprojects/frontends/btor2-frontend/src/main/java/hu/bme/mit/theta/frontend/model/Btor2Declarations.kt +++ b/subprojects/frontends/btor2-frontend/src/main/java/hu/bme/mit/theta/frontend/model/Btor2Declarations.kt @@ -1,23 +1,39 @@ +import hu.bme.mit.theta.core.decl.Decls.Var +import hu.bme.mit.theta.core.decl.VarDecl +import hu.bme.mit.theta.core.type.Type +import hu.bme.mit.theta.core.type.bvtype.BvType import hu.bme.mit.theta.frontend.model.Btor2Node import hu.bme.mit.theta.frontend.model.Btor2NodeVisitor import java.math.BigInteger // Declarations -abstract class Btor2Sort(override val nid: UInt) : Btor2Node(nid) +// TODO needs to be generalized if arrays are added +abstract class Btor2Sort(override val nid: UInt, open val width: UInt) : Btor2Node(nid) { + abstract fun getType() : BvType +} // TODO start supporting arrays // data class Btor2ArrayDeclaration(val id: Int, val indexSort: Btor2SortDeclaration, val elementSort: Btor2SortDeclaration) -data class Btor2BvSort(override val nid: UInt, val width: UInt) : Btor2Sort(nid) { - fun accept(visitor: Btor2NodeVisitor): R { - return visitor.visit(this) +data class Btor2BvSort(override val nid: UInt, override val width: UInt) : Btor2Sort(nid, width) { + override fun getType(): BvType { + return BvType.of(width.toInt()) + } + + override fun accept(visitor: Btor2NodeVisitor, param : P): R { + return visitor.visit(this, param) } } // Constants // it can be in binary, decimal or hex in the circuit, but we extract the actual value to the int from that data class Btor2Const(override val nid: UInt, val value: BigInteger, override val sort: Btor2Sort) : Btor2Node(nid) { - fun accept(visitor: Btor2NodeVisitor): R { - return visitor.visit(this) + private val constVar = Var("node_" + nid, sort.getType()) + override fun accept(visitor: Btor2NodeVisitor, param : P): R { + return visitor.visit(this, param) + } + + fun getVar(): VarDecl { + return constVar } } \ No newline at end of file diff --git a/subprojects/frontends/btor2-frontend/src/main/java/hu/bme/mit/theta/frontend/model/Btor2Node.kt b/subprojects/frontends/btor2-frontend/src/main/java/hu/bme/mit/theta/frontend/model/Btor2Node.kt index 2ae1f8552a..f70cd1cea4 100644 --- a/subprojects/frontends/btor2-frontend/src/main/java/hu/bme/mit/theta/frontend/model/Btor2Node.kt +++ b/subprojects/frontends/btor2-frontend/src/main/java/hu/bme/mit/theta/frontend/model/Btor2Node.kt @@ -3,5 +3,5 @@ package hu.bme.mit.theta.frontend.model import Btor2Sort abstract class Btor2Node(open val nid: UInt, open val sort: Btor2Sort? = null) { - abstract fun accept(visitor: Btor2NodeVisitor): R + abstract fun accept(visitor: Btor2NodeVisitor, param : P): R } diff --git a/subprojects/frontends/btor2-frontend/src/main/java/hu/bme/mit/theta/frontend/model/Btor2NodeVisitor.kt b/subprojects/frontends/btor2-frontend/src/main/java/hu/bme/mit/theta/frontend/model/Btor2NodeVisitor.kt index 25fc2c1f9c..bf9bae874c 100644 --- a/subprojects/frontends/btor2-frontend/src/main/java/hu/bme/mit/theta/frontend/model/Btor2NodeVisitor.kt +++ b/subprojects/frontends/btor2-frontend/src/main/java/hu/bme/mit/theta/frontend/model/Btor2NodeVisitor.kt @@ -3,19 +3,19 @@ package hu.bme.mit.theta.frontend.model import Btor2BvSort import Btor2Const -public interface Btor2NodeVisitor { - fun visit(node : Btor2UnaryOperation) : R - fun visit(node : Btor2BinaryOperation) : R - fun visit(node : Btor2TernaryOperation) : R - fun visit(node : Btor2SliceOperation) : R - fun visit(node : Btor2ExtOperation) : R - fun visit(node : Btor2Const) : R - fun visit(node : Btor2BvSort) : R - fun visit(node : Btor2Input) : R - fun visit(node : Btor2State) : R - fun visit(node : Btor2Init) : R - fun visit(node : Btor2Next) : R - fun visit(node : Btor2Bad) : R - fun visit(node : Btor2Constraint) : R - fun visit(node : Btor2Output) : R +public interface Btor2NodeVisitor { + 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: Btor2Const, param: P) : R + fun visit(node: Btor2BvSort, 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: Btor2Constraint, param: P) : R + fun visit(node: Btor2Output, param: P) : R } \ No newline at end of file diff --git a/subprojects/frontends/btor2-frontend/src/main/java/hu/bme/mit/theta/frontend/model/Btor2Operators.kt b/subprojects/frontends/btor2-frontend/src/main/java/hu/bme/mit/theta/frontend/model/Btor2Operators.kt index a93d5abee5..456441e206 100644 --- a/subprojects/frontends/btor2-frontend/src/main/java/hu/bme/mit/theta/frontend/model/Btor2Operators.kt +++ b/subprojects/frontends/btor2-frontend/src/main/java/hu/bme/mit/theta/frontend/model/Btor2Operators.kt @@ -6,28 +6,28 @@ abstract class Btor2Operator(id: UInt) : Btor2Node(id) // Operators data class Btor2UnaryOperation(override val nid: UInt, override val sort : Btor2Sort, val operator: Btor2UnaryOperator, val operand: Btor2Node) : Btor2Operator(nid) { - override fun accept(visitor: Btor2NodeVisitor): R { - return visitor.visit(this) + override fun accept(visitor: Btor2NodeVisitor, param : P): R { + return visitor.visit(this, param) } } data class Btor2ExtOperation(override val nid: UInt, override val sort : Btor2Sort, val operand: Btor2Node, val w : UInt) : Btor2Operator(nid) { - override fun accept(visitor: Btor2NodeVisitor): R { - return visitor.visit(this) + override fun accept(visitor: Btor2NodeVisitor, param : P): R { + return visitor.visit(this, param) } } data class Btor2SliceOperation(override val nid: UInt, override val sort : Btor2Sort, val operand: Btor2Node, val u : UInt, val l : UInt) : Btor2Operator(nid) { - override fun accept(visitor: Btor2NodeVisitor): R { - return visitor.visit(this) + override fun accept(visitor: Btor2NodeVisitor, param : P): R { + return visitor.visit(this, param) } } data class Btor2BinaryOperation(override val nid: UInt, override val sort : Btor2Sort, val operator: Btor2BinaryOperator, val operand1: Btor2Node, val operand2: Btor2Node) : Btor2Operator(nid) { - override fun accept(visitor: Btor2NodeVisitor): R { - return visitor.visit(this) + override fun accept(visitor: Btor2NodeVisitor, param : P): R { + return visitor.visit(this, param) } } data class Btor2TernaryOperation(override val nid: UInt, override val sort : Btor2Sort, val operator: Btor2TernaryOperator, val condition: Btor2Node, val trueValue: Btor2Node, val falseValue: Btor2Node) : Btor2Operator(nid) { - override fun accept(visitor: Btor2NodeVisitor): R { - return visitor.visit(this) + override fun accept(visitor: Btor2NodeVisitor, param : P): R { + return visitor.visit(this, param) } } enum class Btor2UnaryOperator { diff --git a/subprojects/frontends/btor2-frontend/src/main/java/hu/bme/mit/theta/frontend/model/Btor2StateNodes.kt b/subprojects/frontends/btor2-frontend/src/main/java/hu/bme/mit/theta/frontend/model/Btor2StateNodes.kt index b71d081c07..843943e86f 100644 --- a/subprojects/frontends/btor2-frontend/src/main/java/hu/bme/mit/theta/frontend/model/Btor2StateNodes.kt +++ b/subprojects/frontends/btor2-frontend/src/main/java/hu/bme/mit/theta/frontend/model/Btor2StateNodes.kt @@ -5,40 +5,40 @@ import Btor2Sort // Inputs and States data class Btor2Input(override val nid: UInt, override val sort: Btor2Sort) : Btor2Node(nid) { - override fun accept(visitor: Btor2NodeVisitor): R { - return visitor.visit(this) + override fun accept(visitor: Btor2NodeVisitor, param : P): R { + return visitor.visit(this, param) } } data class Btor2State(override val nid: UInt, override val sort: Btor2Sort) : Btor2Node(nid) { - override fun accept(visitor: Btor2NodeVisitor): R { - return visitor.visit(this) + override fun accept(visitor: Btor2NodeVisitor, param : P): R { + return visitor.visit(this, param) } } data class Btor2Init(override val nid: UInt, override val sort: Btor2Sort, val state: Btor2State, val value: Btor2Const) : Btor2Node(nid) { - override fun accept(visitor: Btor2NodeVisitor): R { - return visitor.visit(this) + override fun accept(visitor: Btor2NodeVisitor, param : P): R { + return visitor.visit(this, param) } } data class Btor2Next(override val nid: UInt, override val sort: Btor2Sort, val state: Btor2State, val value: Btor2Node) : Btor2Node(nid) { - override fun accept(visitor: Btor2NodeVisitor): R { - return visitor.visit(this) + override fun accept(visitor: Btor2NodeVisitor, param : P): R { + return visitor.visit(this, param) } } // Property Nodes // data class Btor2JusticeNode(val id: Int, val num: Int, val children: List) : Btor2Node(id) data class Btor2Bad(override val nid: UInt, val operand: Btor2Node) : Btor2Node(nid) { - override fun accept(visitor: Btor2NodeVisitor): R { - return visitor.visit(this) + override fun accept(visitor: Btor2NodeVisitor, param : P): R { + return visitor.visit(this, param) } } data class Btor2Constraint(override val nid: UInt, val operand: Btor2Node) : Btor2Node(nid) { - override fun accept(visitor: Btor2NodeVisitor): R { - return visitor.visit(this) + override fun accept(visitor: Btor2NodeVisitor, param : P): R { + return visitor.visit(this, param) } } data class Btor2Output(override val nid: UInt, val operand: Btor2Node) : Btor2Node(nid) { - override fun accept(visitor: Btor2NodeVisitor): R { - return visitor.visit(this) + override fun accept(visitor: Btor2NodeVisitor, param : P): R { + return visitor.visit(this, param) } } diff --git a/subprojects/xcfa/btor22xcfa/src/main/java/hu/bme/mit/theta/btor22xcfa/Btor2FrontendXcfaBuilder.kt b/subprojects/xcfa/btor22xcfa/src/main/java/hu/bme/mit/theta/btor22xcfa/Btor2FrontendXcfaBuilder.kt index 29b5af70fc..18fc04f88d 100644 --- a/subprojects/xcfa/btor22xcfa/src/main/java/hu/bme/mit/theta/btor22xcfa/Btor2FrontendXcfaBuilder.kt +++ b/subprojects/xcfa/btor22xcfa/src/main/java/hu/bme/mit/theta/btor22xcfa/Btor2FrontendXcfaBuilder.kt @@ -15,9 +15,16 @@ */ package hu.bme.mit.theta.btor22xcfa +import Btor2BvSort +import Btor2Const import Btor2Sort +import hu.bme.mit.theta.core.stmt.Stmts +import hu.bme.mit.theta.core.type.Expr import hu.bme.mit.theta.core.type.arraytype.* import hu.bme.mit.theta.core.type.booltype.BoolExprs.* +import hu.bme.mit.theta.core.type.bvtype.BvExprs.Bv +import hu.bme.mit.theta.core.type.bvtype.BvLitExpr +import hu.bme.mit.theta.core.utils.BvUtils import hu.bme.mit.theta.frontend.model.* import hu.bme.mit.theta.frontend.model.Btor2NodeVisitor import hu.bme.mit.theta.frontend.transformation.model.statements.* @@ -26,13 +33,12 @@ import java.util.* import kotlin.collections.LinkedHashSet class Btor2FrontendXcfaBuilder(val sorts : HashMap, val nodes : HashMap) : - Btor2NodeVisitor { + Btor2NodeVisitor { private val locationLut: MutableMap = LinkedHashMap() private val visitedNodes = LinkedHashSet() + private val builder = XcfaBuilder("TODO") fun buildXcfa(): XcfaBuilder { - val builder = XcfaBuilder("TODO") - for (node in nodes.values) { if (!visitedNodes.contains(node)) { node.accept(this) @@ -43,68 +49,87 @@ class Btor2FrontendXcfaBuilder(val sorts : HashMap, val nodes : } } - override fun visit(node: Btor2UnaryOperation): XcfaLocation { - val opd = node.operand - val op = node.operator - - if (!visitedNodes.contains(opd)) { - XcfaLocation = node.accept(this) - } else { - - } + override fun visit(node: Btor2UnaryOperation, param: ParamPack): XcfaLocation { TODO("Not yet implemented") } - override fun visit(node: Btor2BinaryOperation): XcfaLocation { + override fun visit(node: Btor2BinaryOperation, param: ParamPack): XcfaLocation { TODO("Not yet implemented") } - override fun visit(node: Btor2TernaryOperation): XcfaLocation { + override fun visit(node: Btor2TernaryOperation, param: ParamPack): XcfaLocation { TODO("Not yet implemented") } - override fun visit(node: Btor2SliceOperation): XcfaLocation { + override fun visit(node: Btor2SliceOperation, param: ParamPack): XcfaLocation { TODO("Not yet implemented") } - override fun visit(node: Btor2ExtOperation): XcfaLocation { + override fun visit(node: Btor2ExtOperation, param: ParamPack): XcfaLocation { TODO("Not yet implemented") } - override fun visit(node: Btor2Const): XcfaLocation { - TODO("Not yet implemented") + override fun visit(node: Btor2Const, param: ParamPack): XcfaLocation { + // TODO I will have to think more about what variables will be global in the end + val constVar = node.getVar() + param.builder.addVar(constVar) + val newLoc = XcfaLocation("const_node_loc_"+node.nid) + param.builder.addLoc(newLoc) + param.builder.addEdge(XcfaEdge(param.lastLoc, newLoc, + StmtLabel(Stmts.Assign( + constVar, + BvUtils.bigIntegerToNeutralBvLitExpr(node.value, node.sort.width.toInt()) + ), metadata = EmptyMetaData))) + return newLoc } - override fun visit(node: Btor2Output): XcfaLocation { + override fun visit(node: Btor2BvSort, param: ParamPack): XcfaLocation { TODO("Not yet implemented") } - override fun visit(node: Btor2Constraint): XcfaLocation { + override fun visit(node: Btor2Input, param: ParamPack): XcfaLocation { TODO("Not yet implemented") } - override fun visit(node: Btor2Bad): XcfaLocation { + override fun visit(node: Btor2State, param: ParamPack): XcfaLocation { TODO("Not yet implemented") } - override fun visit(node: Btor2Next): XcfaLocation { + override fun visit(node: Btor2Init, param: ParamPack): XcfaLocation { TODO("Not yet implemented") } - override fun visit(node: Btor2Init): XcfaLocation { + override fun visit(node: Btor2Next, param: ParamPack): XcfaLocation { TODO("Not yet implemented") } - override fun visit(node: Btor2State): XcfaLocation { + override fun visit(node: Btor2Bad, param: ParamPack): XcfaLocation { TODO("Not yet implemented") } - override fun visit(node: Btor2Input): XcfaLocation { + override fun visit(node: Btor2Constraint, param: ParamPack): XcfaLocation { TODO("Not yet implemented") } - override fun visit(node: Btor2BvSort): XcfaLocation { + override fun visit(node: Btor2Output, param: ParamPack): XcfaLocation { TODO("Not yet implemented") } - +} + +class ParamPack(builder: XcfaProcedureBuilder, lastLoc: XcfaLocation, breakLoc: XcfaLocation?, + continueLoc: XcfaLocation?, returnLoc: XcfaLocation?) { + + val builder: XcfaProcedureBuilder + val lastLoc: XcfaLocation + val breakLoc: XcfaLocation? + val continueLoc: XcfaLocation? + val returnLoc: XcfaLocation? + + init { + this.builder = builder + this.lastLoc = lastLoc + this.breakLoc = breakLoc + this.continueLoc = continueLoc + this.returnLoc = returnLoc + } } \ No newline at end of file