Skip to content

Commit

Permalink
Added const visitor
Browse files Browse the repository at this point in the history
  • Loading branch information
@AdamZsofi
AdamZsofi committed Jul 25, 2023
1 parent 5530c11 commit 36dcfc2
Show file tree
Hide file tree
Showing 6 changed files with 114 additions and 73 deletions.
28 changes: 22 additions & 6 deletions ...ontends/btor2-frontend/src/main/java/hu/bme/mit/theta/frontend/model/Btor2Declarations.kt
View file
Original file line number Diff line number Diff line change
@@ -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 <R> accept(visitor: Btor2NodeVisitor<R>): 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 <R, P> accept(visitor: Btor2NodeVisitor<R, P>, 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 <R> accept(visitor: Btor2NodeVisitor<R>): R {
return visitor.visit(this)
private val constVar = Var("node_" + nid, sort.getType())
override fun <R, P> accept(visitor: Btor2NodeVisitor<R, P>, param : P): R {
return visitor.visit(this, param)
}

fun getVar(): VarDecl<BvType> {
return constVar
}
}
2 changes: 1 addition & 1 deletion ...jects/frontends/btor2-frontend/src/main/java/hu/bme/mit/theta/frontend/model/Btor2Node.kt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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 <R> accept(visitor: Btor2NodeVisitor<R>): R
abstract fun <R, P> accept(visitor: Btor2NodeVisitor<R, P>, param : P): R
}
30 changes: 15 additions & 15 deletions ...rontends/btor2-frontend/src/main/java/hu/bme/mit/theta/frontend/model/Btor2NodeVisitor.kt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3,19 +3,19 @@ package hu.bme.mit.theta.frontend.model
import Btor2BvSort
import Btor2Const

public interface Btor2NodeVisitor<R> {
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<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: 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
}
20 changes: 10 additions & 10 deletions .../frontends/btor2-frontend/src/main/java/hu/bme/mit/theta/frontend/model/Btor2Operators.kt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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 <R> accept(visitor: Btor2NodeVisitor<R>): R {
return visitor.visit(this)
override fun <R, P> accept(visitor: Btor2NodeVisitor<R, P>, 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 <R> accept(visitor: Btor2NodeVisitor<R>): R {
return visitor.visit(this)
override fun <R, P> accept(visitor: Btor2NodeVisitor<R, P>, 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 <R> accept(visitor: Btor2NodeVisitor<R>): R {
return visitor.visit(this)
override fun <R, P> accept(visitor: Btor2NodeVisitor<R, P>, 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 <R> accept(visitor: Btor2NodeVisitor<R>): R {
return visitor.visit(this)
override fun <R, P> accept(visitor: Btor2NodeVisitor<R, P>, 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 <R> accept(visitor: Btor2NodeVisitor<R>): R {
return visitor.visit(this)
override fun <R, P> accept(visitor: Btor2NodeVisitor<R, P>, param : P): R {
return visitor.visit(this, param)
}
}
enum class Btor2UnaryOperator {
Expand Down
28 changes: 14 additions & 14 deletions ...frontends/btor2-frontend/src/main/java/hu/bme/mit/theta/frontend/model/Btor2StateNodes.kt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -5,40 +5,40 @@ import Btor2Sort

// Inputs and States
data class Btor2Input(override val nid: UInt, override val sort: Btor2Sort) : Btor2Node(nid) {
override fun <R> accept(visitor: Btor2NodeVisitor<R>): R {
return visitor.visit(this)
override fun <R, P> accept(visitor: Btor2NodeVisitor<R, P>, param : P): R {
return visitor.visit(this, param)
}
}
data class Btor2State(override val nid: UInt, override val sort: Btor2Sort) : Btor2Node(nid) {
override fun <R> accept(visitor: Btor2NodeVisitor<R>): R {
return visitor.visit(this)
override fun <R, P> accept(visitor: Btor2NodeVisitor<R, P>, 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 <R> accept(visitor: Btor2NodeVisitor<R>): R {
return visitor.visit(this)
override fun <R, P> accept(visitor: Btor2NodeVisitor<R, P>, 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 <R> accept(visitor: Btor2NodeVisitor<R>): R {
return visitor.visit(this)
override fun <R, P> accept(visitor: Btor2NodeVisitor<R, P>, param : P): R {
return visitor.visit(this, param)
}
}

// Property Nodes
// data class Btor2JusticeNode(val id: Int, val num: Int, val children: List<Btor2Node>) : Btor2Node(id)
data class Btor2Bad(override val nid: UInt, val operand: Btor2Node) : Btor2Node(nid) {
override fun <R> accept(visitor: Btor2NodeVisitor<R>): R {
return visitor.visit(this)
override fun <R, P> accept(visitor: Btor2NodeVisitor<R, P>, param : P): R {
return visitor.visit(this, param)
}
}
data class Btor2Constraint(override val nid: UInt, val operand: Btor2Node) : Btor2Node(nid) {
override fun <R> accept(visitor: Btor2NodeVisitor<R>): R {
return visitor.visit(this)
override fun <R, P> accept(visitor: Btor2NodeVisitor<R, P>, param : P): R {
return visitor.visit(this, param)
}
}
data class Btor2Output(override val nid: UInt, val operand: Btor2Node) : Btor2Node(nid) {
override fun <R> accept(visitor: Btor2NodeVisitor<R>): R {
return visitor.visit(this)
override fun <R, P> accept(visitor: Btor2NodeVisitor<R, P>, param : P): R {
return visitor.visit(this, param)
}
}
79 changes: 52 additions & 27 deletions ...cts/xcfa/btor22xcfa/src/main/java/hu/bme/mit/theta/btor22xcfa/Btor2FrontendXcfaBuilder.kt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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.*
Expand All @@ -26,13 +33,12 @@ import java.util.*
import kotlin.collections.LinkedHashSet

class Btor2FrontendXcfaBuilder(val sorts : HashMap<UInt, Btor2Sort>, val nodes : HashMap<UInt, Btor2Node>) :
Btor2NodeVisitor<XcfaLocation> {
Btor2NodeVisitor<XcfaLocation, ParamPack> {
private val locationLut: MutableMap<Btor2Node, XcfaLocation> = LinkedHashMap()
private val visitedNodes = LinkedHashSet<Btor2Node>()
private val builder = XcfaBuilder("TODO")

fun buildXcfa(): XcfaBuilder {
val builder = XcfaBuilder("TODO")

for (node in nodes.values) {
if (!visitedNodes.contains(node)) {
node.accept(this)
Expand All @@ -43,68 +49,87 @@ class Btor2FrontendXcfaBuilder(val sorts : HashMap<UInt, Btor2Sort>, 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
}
}

0 comments on commit 36dcfc2

Please sign in to comment.