From cf720436132daea72341cfdbb86fb5fc881de879 Mon Sep 17 00:00:00 2001 From: AdamZsofi Date: Sun, 23 Jul 2023 17:09:55 +0200 Subject: [PATCH] Added sort and const visitors --- .../btor2-frontend/src/main/antlr/Btor2.g4 | 55 +++++------ .../hu/bme/mit/theta/frontend/Btor2Visitor.kt | 95 ------------------- .../theta/frontend/model/Btor2Declarations.kt | 13 ++- .../bme/mit/theta/frontend/model/Btor2Node.kt | 2 +- .../theta/frontend/model/Btor2Operators.kt | 10 +- .../theta/frontend/visitor/Btor2Visitor.kt | 67 +++++++++++++ .../theta/frontend/visitor/ConstantVisitor.kt | 46 +++++++++ .../mit/theta/frontend/visitor/IdVisitor.kt | 23 +++++ .../frontend/visitor/OperationVisitor.kt | 43 +++++++++ .../mit/theta/frontend/visitor/SortVisitor.kt | 26 +++++ 10 files changed, 242 insertions(+), 138 deletions(-) delete mode 100644 subprojects/frontends/btor2-frontend/src/main/java/hu/bme/mit/theta/frontend/Btor2Visitor.kt create mode 100644 subprojects/frontends/btor2-frontend/src/main/java/hu/bme/mit/theta/frontend/visitor/Btor2Visitor.kt create mode 100644 subprojects/frontends/btor2-frontend/src/main/java/hu/bme/mit/theta/frontend/visitor/ConstantVisitor.kt create mode 100644 subprojects/frontends/btor2-frontend/src/main/java/hu/bme/mit/theta/frontend/visitor/IdVisitor.kt create mode 100644 subprojects/frontends/btor2-frontend/src/main/java/hu/bme/mit/theta/frontend/visitor/OperationVisitor.kt create mode 100644 subprojects/frontends/btor2-frontend/src/main/java/hu/bme/mit/theta/frontend/visitor/SortVisitor.kt diff --git a/subprojects/frontends/btor2-frontend/src/main/antlr/Btor2.g4 b/subprojects/frontends/btor2-frontend/src/main/antlr/Btor2.g4 index 91ebc6fe7d..384e0ecb4e 100644 --- a/subprojects/frontends/btor2-frontend/src/main/antlr/Btor2.g4 +++ b/subprojects/frontends/btor2-frontend/src/main/antlr/Btor2.g4 @@ -29,50 +29,41 @@ line: ( comment | node (symbol)? (comment)? ) '\n'; comment: COMMENT; -nid: NUM; // TODO semantic check nid/sid for >0 -sid: NUM; // TODO semantic check nid/sid for >0 +nid: NUM; +sid: NUM; -node: ( array_sort | bitvec_sort ) // sort declaration - | (input | state) // input or state declaration - | opidx // indexed operator node - | op // non-indexed operator node - | (init | next) // init/next node - | property; // property node - // | nid 'justice' NUM (nid)+; // justice node // TODO we can not model check justice nodes (not reachability) +node: ( array_sort | bitvec_sort ) #sort // sort declaration + | (input | state | init | next | property) #other + | (opidx | op) #operation + | (filled_constant | constant | constant_d | constant_h) #constantNode; + // | nid 'justice' NUM (nid)+; // justice node // TODO we can not modelcheck justice nodes (not reachability) opidx: ext | slice; -ext: nid ('uext'|'sext') sid nid w=NUM; -slice: nid 'slice' sid nid u=NUM l=NUM; +ext: id=nid ('uext'|'sext') sid opd1=nid w=NUM; +slice: id=nid 'slice' sid opd1=nid u=NUM l=NUM; op: binop | unop | terop; -binop: nid BINOP sid opd1=nid opd2=nid; -unop: nid UNARYOP sid opd1=nid; -terop: nid TERNARYOP sid opd1=nid opd2=nid opd3=nid; +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: nid ('input' sid - | 'one' sid - | 'ones' sid - | 'zero' sid - | constant - | constant_d - | constant_h); +input: id=nid ('input') sid; -init: nid 'init' sid nid nid; -next: nid 'next' sid nid nid; +init: id=nid 'init' sid param1=nid param2=nid; +next: id=nid 'next' sid param1=nid param2=nid; -state: nid 'state' sid; +state: id=nid 'state' sid; -property: nid ('bad' | 'constraint' | 'fair' | 'output') nid; +property: id=nid ('bad' | 'constraint' | 'fair' | 'output') param=nid; -array_sort: sid 'sort array' sid sid; -bitvec_sort: sid 'sort bitvec' NUM; // TODO semantic check for >0 +array_sort: id=sid 'sort array' sid1=sid sid2=sid; +bitvec_sort: id=sid 'sort bitvec' width=NUM; // TODO semantic check for >0 -constant: 'const' sid bin=NUM; // TODO semantic check that really binary - -constant_d: 'constd' sid (MINUS)? dec=NUM; // TODO semantic check that really uint - -constant_h: 'consth' sid hex=SYMBOL; // TODO semantic check that really hex +constant: id=nid 'const' sid bin=NUM; // TODO semantic check that really binary +constant_d: id=nid 'constd' sid (MINUS)? dec=NUM; // TODO semantic check that really uint +constant_h: id=nid 'consth' sid hex=SYMBOL; // TODO semantic check that really hex +filled_constant: id=nid ('one' | 'ones' | 'zero') sid; symbol: SYMBOL; diff --git a/subprojects/frontends/btor2-frontend/src/main/java/hu/bme/mit/theta/frontend/Btor2Visitor.kt b/subprojects/frontends/btor2-frontend/src/main/java/hu/bme/mit/theta/frontend/Btor2Visitor.kt deleted file mode 100644 index dae99c743b..0000000000 --- a/subprojects/frontends/btor2-frontend/src/main/java/hu/bme/mit/theta/frontend/Btor2Visitor.kt +++ /dev/null @@ -1,95 +0,0 @@ -package hu.bme.mit.theta.frontend -import hu.bme.mit.theta.btor2.frontend.dsl.gen.Btor2BaseVisitor -import hu.bme.mit.theta.btor2.frontend.dsl.gen.Btor2Parser -import hu.bme.mit.theta.btor2.frontend.dsl.gen.Btor2Parser.Constant_dContext -import org.antlr.v4.runtime.tree.TerminalNode - -class Btor2Visitor : Btor2BaseVisitor() { - - override fun visitBtor2(ctx: Btor2Parser.Btor2Context) { - // TODO: Implement logic for visiting the btor2 rule - println("visitBtor2") - super.visitBtor2(ctx) - } - - override fun visitLine(ctx: Btor2Parser.LineContext) { - println("visitLine") - // TODO: Implement logic for visiting the line rule - super.visitLine(ctx) - } - - override fun visitNode(ctx: Btor2Parser.NodeContext) { - println("visit node") - // TODO: Implement logic for visiting the node rule - super.visitNode(ctx) - } - - override fun visitInput(ctx: Btor2Parser.InputContext) { - // TODO: Implement logic for visiting the input rule - super.visitInput(ctx) - } - - override fun visitState(ctx: Btor2Parser.StateContext) { - // TODO: Implement logic for visiting the state rule - super.visitState(ctx) - } - - override fun visitArray_sort(ctx: Btor2Parser.Array_sortContext) { - // TODO: Implement logic for visiting the array_sort rule - super.visitArray_sort(ctx) - } - - override fun visitBitvec_sort(ctx: Btor2Parser.Bitvec_sortContext) { - // TODO: Implement logic for visiting the bitvec_sort rule - super.visitBitvec_sort(ctx) - } - - override fun visitOpidx(ctx: Btor2Parser.OpidxContext) { - // TODO: Implement logic for visiting the opidx rule - super.visitOpidx(ctx) - } - - override fun visitOp(ctx: Btor2Parser.OpContext) { - // TODO: Implement logic for visiting the op rule - super.visitOp(ctx) - } - - override fun visitConstant(ctx: Btor2Parser.ConstantContext) { - // TODO: Implement logic for visiting the const rule - super.visitConstant(ctx) - } - - override fun visitConstant_d(ctx: Constant_dContext) { - // TODO: Implement logic for visiting the constd rule - super.visitConstant_d(ctx) - } - - override fun visitConstant_h(ctx: Btor2Parser.Constant_hContext) { - // TODO: Implement logic for visiting the consth rule - super.visitConstant_h(ctx) - } - - override fun visitSymbol(ctx: Btor2Parser.SymbolContext) { - // TODO: Implement logic for visiting the symbol rule - super.visitSymbol(ctx) - } - - override fun visitTerminal(node: TerminalNode) { - // TODO: Implement logic for visiting terminal nodes - super.visitTerminal(node) - } -} - -// Example usage -/* -fun main() { - val btor2Code = // Your BTOR2 code here - - val lexer = Btor2Lexer(CharStreams.fromString(btor2Code)) - val tokens = CommonTokenStream(lexer) - val parser = Btor2Parser(tokens) - - val visitor = Btor2Visitor() - visitor.visit(parser.btor2()) -} -*/ \ No newline at end of file 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 b341da03a7..706c021c20 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,14 +1,17 @@ import hu.bme.mit.theta.frontend.model.Btor2Node +import java.math.BigInteger // Declarations +abstract class Btor2Sort(open val sid : Int) : Btor2Node(sid) + // TODO start supporting arrays -//data class Btor2ArrayDeclaration(val id: Int, val indexSort: Btor2SortDeclaration, val elementSort: Btor2SortDeclaration) -data class Btor2BvSortDeclaration(val id: Int, val width: Int) : Btor2Node(id) +// data class Btor2ArrayDeclaration(val id: Int, val indexSort: Btor2SortDeclaration, val elementSort: Btor2SortDeclaration) +data class Btor2BvSort(override val sid: Int, val width: Int) : Btor2Sort(sid) // Constants -data class Btor2ConstDeclaration(val id: Int, val value: Int, val type: Btor2BvSortDeclaration) : Btor2Node(id) // 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: Int, val value: BigInteger, val type: Btor2BvSort) : Btor2Node(nid) // it can be in binary, decimal or hex in the circuit, but we extract the actual value to the int from that // Inputs and States -data class Btor2InputDeclaration(val id: Int, val type: Btor2BvSortDeclaration) : Btor2Node(id) -data class Btor2StateDeclaration(val id: Int, val type: Btor2BvSortDeclaration) : Btor2Node(id) \ No newline at end of file +data class Btor2Input(override val nid: Int, val type: Btor2BvSort) : Btor2Node(nid) +data class Btor2State(override val nid: Int, val type: Btor2BvSort) : Btor2Node(nid) \ 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 8ff5e83200..dbbba0b456 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 @@ -1,3 +1,3 @@ package hu.bme.mit.theta.frontend.model -open class Btor2Node(val nid: Int) +open class Btor2Node(open val nid: Int) 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 01cf570bfa..c02d1c5970 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 @@ -1,12 +1,12 @@ package hu.bme.mit.theta.frontend.model -import Btor2BvSortDeclaration -import Btor2ConstDeclaration -import Btor2StateDeclaration +import Btor2BvSort +import Btor2Const +import Btor2State // Operator Nodes -data class Btor2InitNode(val id: Int, val nodeType: Btor2BvSortDeclaration, val sortId: Btor2BvSortDeclaration, val state: Btor2StateDeclaration, val value: Btor2ConstDeclaration) : Btor2Node(id) -data class Btor2NextNode(val id: Int, val nodeType: Btor2BvSortDeclaration, val sortId: Btor2BvSortDeclaration, val state: Btor2StateDeclaration, val value: Btor2Node) : Btor2Node(id) +data class Btor2InitNode(val id: Int, val nodeType: Btor2BvSort, val sortId: Btor2BvSort, val state: Btor2State, val value: Btor2Const) : Btor2Node(id) +data class Btor2NextNode(val id: Int, val nodeType: Btor2BvSort, val sortId: Btor2BvSort, val state: Btor2State, val value: Btor2Node) : Btor2Node(id) // TODO support justice nodes...? (not reachability, but an invariant) // data class Btor2JusticeNode(val id: Int, val num: Int, val children: List) : Btor2Node(id) data class Btor2BadNode(val id: Int, val operand: Btor2Node) : Btor2Node(id) diff --git a/subprojects/frontends/btor2-frontend/src/main/java/hu/bme/mit/theta/frontend/visitor/Btor2Visitor.kt b/subprojects/frontends/btor2-frontend/src/main/java/hu/bme/mit/theta/frontend/visitor/Btor2Visitor.kt new file mode 100644 index 0000000000..bfdaaa0375 --- /dev/null +++ b/subprojects/frontends/btor2-frontend/src/main/java/hu/bme/mit/theta/frontend/visitor/Btor2Visitor.kt @@ -0,0 +1,67 @@ +package hu.bme.mit.theta.frontend.visitor + +import Btor2Sort +import hu.bme.mit.theta.btor2.frontend.dsl.gen.Btor2BaseVisitor +import hu.bme.mit.theta.btor2.frontend.dsl.gen.Btor2Parser +import hu.bme.mit.theta.frontend.model.Btor2Node +import java.util.LinkedHashMap + +class Btor2Visitor : Btor2BaseVisitor() { + val idVisitor = IdVisitor() + val sortVisitor = SortVisitor(idVisitor) + val sorts = LinkedHashMap() + val constantVisitor = ConstantVisitor(idVisitor, sorts) + + // Parser rules + override fun visitBtor2(ctx: Btor2Parser.Btor2Context): Btor2Node { + return visitChildren(ctx) // TODO + } + + override fun visitLine(ctx: Btor2Parser.LineContext): Btor2Node { + return visitChildren(ctx) // TODO + } + + override fun visitSort(ctx: Btor2Parser.SortContext): Btor2Node { + val newSort = sortVisitor.visit(ctx) + check(!sorts.containsKey(newSort.nid)) + sorts[newSort.nid] = newSort + return newSort + } + + override fun visitConstantNode(ctx: Btor2Parser.ConstantNodeContext): Btor2Node { + val newConstant = constantVisitor.visit(ctx) + return newConstant + } + + //////////////////// + + override fun visitInput(ctx: Btor2Parser.InputContext): Btor2Node { + // Implementation for visiting input rule + throw NotImplementedError() + } + + override fun visitInit(ctx: Btor2Parser.InitContext): Btor2Node { + // Implementation for visiting init rule + throw NotImplementedError() + } + + override fun visitNext(ctx: Btor2Parser.NextContext): Btor2Node { + // Implementation for visiting next rule + throw NotImplementedError() + } + + override fun visitState(ctx: Btor2Parser.StateContext): Btor2Node { + // Implementation for visiting state rule + throw NotImplementedError() + } + + override fun visitProperty(ctx: Btor2Parser.PropertyContext): Btor2Node { + // Implementation for visiting property rule + throw NotImplementedError() + } + + override fun visitSymbol(ctx: Btor2Parser.SymbolContext): Btor2Node { + // Implementation for visiting symbol rule + throw NotImplementedError() + } +} diff --git a/subprojects/frontends/btor2-frontend/src/main/java/hu/bme/mit/theta/frontend/visitor/ConstantVisitor.kt b/subprojects/frontends/btor2-frontend/src/main/java/hu/bme/mit/theta/frontend/visitor/ConstantVisitor.kt new file mode 100644 index 0000000000..334d0d334a --- /dev/null +++ b/subprojects/frontends/btor2-frontend/src/main/java/hu/bme/mit/theta/frontend/visitor/ConstantVisitor.kt @@ -0,0 +1,46 @@ +package hu.bme.mit.theta.frontend.visitor + +import Btor2BvSort +import Btor2Const +import Btor2Sort +import hu.bme.mit.theta.btor2.frontend.dsl.gen.Btor2BaseVisitor +import hu.bme.mit.theta.btor2.frontend.dsl.gen.Btor2Parser +import java.math.BigInteger + +class ConstantVisitor(val idVisitor : IdVisitor, val sorts : Map) : Btor2BaseVisitor() { + override fun visitConstantNode(ctx: Btor2Parser.ConstantNodeContext): Btor2Const { + check(ctx.childCount==1) + return ctx.children[0].accept(this) + } + + override fun visitConstant(ctx: Btor2Parser.ConstantContext): Btor2Const { + val nid = idVisitor.visit(ctx.nid()) + val sid = idVisitor.visit(ctx.sid()) + val sort : Btor2BvSort = sorts[sid] as Btor2BvSort + + val value = BigInteger(ctx.bin.text, 2) + val node = Btor2Const(nid, value, sort) + return node + } + + override fun visitConstant_d(ctx: Btor2Parser.Constant_dContext): Btor2Const { + val nid = idVisitor.visit(ctx.nid()) + val sid = idVisitor.visit(ctx.sid()) + val sort : Btor2BvSort = sorts[sid] as Btor2BvSort + + var value = BigInteger(ctx.dec.text) + ctx.MINUS()?.let{ value = value.multiply(BigInteger("-1")) } + val node = Btor2Const(nid, value, sort) + return node + } + + override fun visitConstant_h(ctx: Btor2Parser.Constant_hContext): Btor2Const { + val nid = idVisitor.visit(ctx.nid()) + val sid = idVisitor.visit(ctx.sid()) + val sort : Btor2BvSort = sorts[sid] as Btor2BvSort + + val value = BigInteger(ctx.hex.text, 16) + val node = Btor2Const(nid, value, sort) + return node + } +} \ No newline at end of file diff --git a/subprojects/frontends/btor2-frontend/src/main/java/hu/bme/mit/theta/frontend/visitor/IdVisitor.kt b/subprojects/frontends/btor2-frontend/src/main/java/hu/bme/mit/theta/frontend/visitor/IdVisitor.kt new file mode 100644 index 0000000000..a33682a1c0 --- /dev/null +++ b/subprojects/frontends/btor2-frontend/src/main/java/hu/bme/mit/theta/frontend/visitor/IdVisitor.kt @@ -0,0 +1,23 @@ +package hu.bme.mit.theta.frontend.visitor + +import hu.bme.mit.theta.btor2.frontend.dsl.gen.Btor2BaseVisitor +import hu.bme.mit.theta.btor2.frontend.dsl.gen.Btor2Parser + +class IdVisitor : Btor2BaseVisitor() { + override fun visitNid(ctx: Btor2Parser.NidContext): Int { + val nid = ctx.NUM().text.toInt() + if (nid <= 0) { + throw RuntimeException("nid should be bigger than 0") + } + return nid + } + + override fun visitSid(ctx: Btor2Parser.SidContext): Int { + val sid = ctx.NUM().text.toInt() + if (sid <= 0) { + throw RuntimeException("nid should be bigger than 0") + } + return sid + } + +} \ No newline at end of file diff --git a/subprojects/frontends/btor2-frontend/src/main/java/hu/bme/mit/theta/frontend/visitor/OperationVisitor.kt b/subprojects/frontends/btor2-frontend/src/main/java/hu/bme/mit/theta/frontend/visitor/OperationVisitor.kt new file mode 100644 index 0000000000..4d8afbed6d --- /dev/null +++ b/subprojects/frontends/btor2-frontend/src/main/java/hu/bme/mit/theta/frontend/visitor/OperationVisitor.kt @@ -0,0 +1,43 @@ +package hu.bme.mit.theta.frontend.visitor + +import hu.bme.mit.theta.btor2.frontend.dsl.gen.Btor2BaseVisitor +import hu.bme.mit.theta.btor2.frontend.dsl.gen.Btor2Parser +import hu.bme.mit.theta.frontend.model.Btor2Node + +class OperationVisitor : Btor2BaseVisitor() { + override fun visitOpidx(ctx: Btor2Parser.OpidxContext): Btor2Node { + // Implementation for visiting opidx rule + throw NotImplementedError() + } + + override fun visitExt(ctx: Btor2Parser.ExtContext): Btor2Node { + // Implementation for visiting ext rule + throw NotImplementedError() + } + + override fun visitSlice(ctx: Btor2Parser.SliceContext): Btor2Node { + // Implementation for visiting slice rule + throw NotImplementedError() + } + + override fun visitOp(ctx: Btor2Parser.OpContext): Btor2Node { + // Implementation for visiting op rule + throw NotImplementedError() + } + + override fun visitBinop(ctx: Btor2Parser.BinopContext): Btor2Node { + // Implementation for visiting binop rule + throw NotImplementedError() + } + + override fun visitUnop(ctx: Btor2Parser.UnopContext): Btor2Node { + // Implementation for visiting unop rule + throw NotImplementedError() + } + + override fun visitTerop(ctx: Btor2Parser.TeropContext): Btor2Node { + // Implementation for visiting terop rule + throw NotImplementedError() + } + +} \ No newline at end of file diff --git a/subprojects/frontends/btor2-frontend/src/main/java/hu/bme/mit/theta/frontend/visitor/SortVisitor.kt b/subprojects/frontends/btor2-frontend/src/main/java/hu/bme/mit/theta/frontend/visitor/SortVisitor.kt new file mode 100644 index 0000000000..a81e5659fb --- /dev/null +++ b/subprojects/frontends/btor2-frontend/src/main/java/hu/bme/mit/theta/frontend/visitor/SortVisitor.kt @@ -0,0 +1,26 @@ +package hu.bme.mit.theta.frontend.visitor + +import Btor2BvSort +import Btor2Sort +import hu.bme.mit.theta.btor2.frontend.dsl.gen.Btor2BaseVisitor +import hu.bme.mit.theta.btor2.frontend.dsl.gen.Btor2Parser + +class SortVisitor(val idVisitor: IdVisitor) : Btor2BaseVisitor() { + override fun visitSort(ctx: Btor2Parser.SortContext): Btor2Sort { + check(ctx.childCount==1) + return ctx.children[0].accept(this) + } + + override fun visitArray_sort(ctx: Btor2Parser.Array_sortContext): Btor2Sort { + throw NotImplementedError() + } + + override fun visitBitvec_sort(ctx: Btor2Parser.Bitvec_sortContext): Btor2Sort { + val sid = idVisitor.visit(ctx.id) + val width = ctx.width.text.toInt() + if(width <= 0) { + throw RuntimeException("Bitvector width should be bigger than 0") + } + return Btor2BvSort(sid, width) + } +} \ No newline at end of file