From 212d7c8ffe1e4867d1b7b9d360ef894cd55d2a0e Mon Sep 17 00:00:00 2001 From: Konstantin Chukharev Date: Mon, 18 Aug 2025 19:10:14 +0300 Subject: [PATCH] Support custom EtsStmt in CFG DSL --- .../kotlin/org/jacodb/ets/dsl/BlockCfg.kt | 1 + .../kotlin/org/jacodb/ets/dsl/BlockStmt.kt | 7 ++++ .../src/main/kotlin/org/jacodb/ets/dsl/DSL.kt | 37 +++++++++++++++++++ .../org/jacodb/ets/dsl/LinearizedCfg.kt | 6 ++- .../main/kotlin/org/jacodb/ets/dsl/Node.kt | 7 ++++ .../main/kotlin/org/jacodb/ets/dsl/Program.kt | 2 + .../org/jacodb/ets/dsl/ProgramBuilder.kt | 10 +++++ .../main/kotlin/org/jacodb/ets/dsl/Stmt.kt | 8 ++++ .../main/kotlin/org/jacodb/ets/dsl/ToDot.kt | 4 ++ .../org/jacodb/ets/utils/BlockCfgBuilder.kt | 5 +++ 10 files changed, 86 insertions(+), 1 deletion(-) diff --git a/jacodb-ets/src/main/kotlin/org/jacodb/ets/dsl/BlockCfg.kt b/jacodb-ets/src/main/kotlin/org/jacodb/ets/dsl/BlockCfg.kt index 8fccfaa96..f81e98773 100644 --- a/jacodb-ets/src/main/kotlin/org/jacodb/ets/dsl/BlockCfg.kt +++ b/jacodb-ets/src/main/kotlin/org/jacodb/ets/dsl/BlockCfg.kt @@ -94,6 +94,7 @@ fun Program.toBlockCfg(): BlockCfg { is Assign -> BlockAssign(node.target, node.expr) is Return -> BlockReturn(node.expr) is If -> BlockIf(node.condition) + is CustomEts -> BlockCustomEts(node.toEts) else -> error("Unexpected node: $node") } nodeToStmt[node] = stmt diff --git a/jacodb-ets/src/main/kotlin/org/jacodb/ets/dsl/BlockStmt.kt b/jacodb-ets/src/main/kotlin/org/jacodb/ets/dsl/BlockStmt.kt index fedd15c80..bdabe9714 100644 --- a/jacodb-ets/src/main/kotlin/org/jacodb/ets/dsl/BlockStmt.kt +++ b/jacodb-ets/src/main/kotlin/org/jacodb/ets/dsl/BlockStmt.kt @@ -16,6 +16,9 @@ package org.jacodb.ets.dsl +import org.jacodb.ets.model.EtsStmt +import org.jacodb.ets.model.EtsStmtLocation + sealed interface BlockStmt data object BlockNop : BlockStmt @@ -32,3 +35,7 @@ data class BlockReturn( data class BlockIf( val condition: Expr, ) : BlockStmt + +class BlockCustomEts( + val toEts: (EtsStmtLocation) -> EtsStmt, +) : BlockStmt diff --git a/jacodb-ets/src/main/kotlin/org/jacodb/ets/dsl/DSL.kt b/jacodb-ets/src/main/kotlin/org/jacodb/ets/dsl/DSL.kt index 8afd1bfbd..9de90491c 100644 --- a/jacodb-ets/src/main/kotlin/org/jacodb/ets/dsl/DSL.kt +++ b/jacodb-ets/src/main/kotlin/org/jacodb/ets/dsl/DSL.kt @@ -16,18 +16,33 @@ package org.jacodb.ets.dsl +import org.jacodb.ets.model.EtsAssignStmt +import org.jacodb.ets.model.EtsClassSignature +import org.jacodb.ets.model.EtsFieldSignature +import org.jacodb.ets.model.EtsInstanceFieldRef +import org.jacodb.ets.model.EtsLocal +import org.jacodb.ets.model.EtsNumberConstant +import org.jacodb.ets.model.EtsUnknownType import org.jacodb.ets.utils.view private fun main() { val prog = program { + // i := arg(0) assign(local("i"), param(0)) + // if (i > 10) ifStmt(gt(local("i"), const(10))) { ifStmt(eq(local("i"), const(42))) { + // if (i == 42) { + // return i ret(local("i")) }.elseIf(eq(local("i"), const(20))) { + // } else if (i == 20) { + // return i ret(local("i")) }.`else` { + // } else { + // i := 10 assign(local("i"), const(10)) } nop() @@ -35,12 +50,34 @@ private fun main() { label("loop") ifStmt(gt(local("i"), const(0))) { + // if (i > 0) { + // i := i - 1 + // goto @loop assign(local("i"), sub(local("i"), const(1))) goto("loop") }.`else` { + // } else { + // return i ret(local("i")) } + // x.foo := 35 + customStmt { loc -> + EtsAssignStmt( + location = loc, + lhv = EtsInstanceFieldRef( + instance = EtsLocal("x", EtsUnknownType), + field = EtsFieldSignature( + enclosingClass = EtsClassSignature.UNKNOWN, + name = "foo", + type = EtsUnknownType, + ), + type = EtsUnknownType + ), + rhv = EtsNumberConstant(35.0) + ) + } + ret(const(100)) // unreachable } diff --git a/jacodb-ets/src/main/kotlin/org/jacodb/ets/dsl/LinearizedCfg.kt b/jacodb-ets/src/main/kotlin/org/jacodb/ets/dsl/LinearizedCfg.kt index cc6078de5..53b880dcd 100644 --- a/jacodb-ets/src/main/kotlin/org/jacodb/ets/dsl/LinearizedCfg.kt +++ b/jacodb-ets/src/main/kotlin/org/jacodb/ets/dsl/LinearizedCfg.kt @@ -46,6 +46,10 @@ fun BlockCfg.linearize(): LinearizedCfg { is BlockIf -> { processed += IfStmt(loc++, stmt.condition) } + + is BlockCustomEts -> { + processed += CustomEtsStmt(loc++, stmt.toEts) + } } } if (processed.isEmpty()) { @@ -60,7 +64,7 @@ fun BlockCfg.linearize(): LinearizedCfg { for ((id, statements) in linearizedBlocks) { for ((stmt, next) in statements.zipWithNext()) { - check(next !is ReturnStmt) { "Return statement in the middle of the block: $next" } + check(stmt !is ReturnStmt) { "Return statement in the middle of the block: $stmt" } check(stmt !is IfStmt) { "If statement in the middle of the block: $stmt" } successors[stmt.location] = listOf(next.location) } diff --git a/jacodb-ets/src/main/kotlin/org/jacodb/ets/dsl/Node.kt b/jacodb-ets/src/main/kotlin/org/jacodb/ets/dsl/Node.kt index 817fd814c..ccc2160a9 100644 --- a/jacodb-ets/src/main/kotlin/org/jacodb/ets/dsl/Node.kt +++ b/jacodb-ets/src/main/kotlin/org/jacodb/ets/dsl/Node.kt @@ -16,6 +16,9 @@ package org.jacodb.ets.dsl +import org.jacodb.ets.model.EtsStmt +import org.jacodb.ets.model.EtsStmtLocation + sealed interface Node data object Nop : Node @@ -42,3 +45,7 @@ data class Label( data class Goto( val targetLabel: String, ) : Node + +class CustomEts( + val toEts: (EtsStmtLocation) -> EtsStmt, +) : Node diff --git a/jacodb-ets/src/main/kotlin/org/jacodb/ets/dsl/Program.kt b/jacodb-ets/src/main/kotlin/org/jacodb/ets/dsl/Program.kt index 68e2fda05..2bf8b45a3 100644 --- a/jacodb-ets/src/main/kotlin/org/jacodb/ets/dsl/Program.kt +++ b/jacodb-ets/src/main/kotlin/org/jacodb/ets/dsl/Program.kt @@ -44,6 +44,8 @@ data class Program( is Label -> line("label ${node.name}") is Goto -> line("goto ${node.targetLabel}") + + is CustomEts -> line("???") } } } diff --git a/jacodb-ets/src/main/kotlin/org/jacodb/ets/dsl/ProgramBuilder.kt b/jacodb-ets/src/main/kotlin/org/jacodb/ets/dsl/ProgramBuilder.kt index 8b164434a..634f1ee51 100644 --- a/jacodb-ets/src/main/kotlin/org/jacodb/ets/dsl/ProgramBuilder.kt +++ b/jacodb-ets/src/main/kotlin/org/jacodb/ets/dsl/ProgramBuilder.kt @@ -19,6 +19,8 @@ package org.jacodb.ets.dsl import org.jacodb.ets.model.EtsEntity +import org.jacodb.ets.model.EtsStmt +import org.jacodb.ets.model.EtsStmtLocation interface ProgramBuilder { fun nop() @@ -27,6 +29,8 @@ interface ProgramBuilder { fun label(name: String) fun goto(label: String) fun ifStmt(condition: Expr, block: ProgramBuilder.() -> Unit): IfBuilder + + fun customStmt(toEts: (EtsStmtLocation) -> EtsStmt) } fun ProgramBuilder.local(name: String) = Local(name) @@ -106,6 +110,10 @@ class ProgramBuilderImpl : ProgramBuilder { _nodes += If(condition, builder.thenNodes, builder.elseNodes) return builder } + + override fun customStmt(toEts: (EtsStmtLocation) -> EtsStmt) { + _nodes += CustomEts(toEts) + } } class IfBuilder : ProgramBuilder { @@ -136,4 +144,6 @@ class IfBuilder : ProgramBuilder { override fun ret(expr: Expr) = thenBuilder.ret(expr) override fun label(name: String) = thenBuilder.label(name) override fun goto(label: String) = thenBuilder.goto(label) + + override fun customStmt(toEts: (EtsStmtLocation) -> EtsStmt) = thenBuilder.customStmt(toEts) } diff --git a/jacodb-ets/src/main/kotlin/org/jacodb/ets/dsl/Stmt.kt b/jacodb-ets/src/main/kotlin/org/jacodb/ets/dsl/Stmt.kt index 145857b39..3b7658763 100644 --- a/jacodb-ets/src/main/kotlin/org/jacodb/ets/dsl/Stmt.kt +++ b/jacodb-ets/src/main/kotlin/org/jacodb/ets/dsl/Stmt.kt @@ -16,6 +16,9 @@ package org.jacodb.ets.dsl +import org.jacodb.ets.model.EtsStmt +import org.jacodb.ets.model.EtsStmtLocation + typealias StmtLocation = Int sealed interface Stmt { @@ -41,3 +44,8 @@ data class IfStmt( override val location: StmtLocation, val condition: Expr, ) : Stmt + +class CustomEtsStmt( + override val location: StmtLocation, + val toEts: (EtsStmtLocation) -> EtsStmt, +) : Stmt diff --git a/jacodb-ets/src/main/kotlin/org/jacodb/ets/dsl/ToDot.kt b/jacodb-ets/src/main/kotlin/org/jacodb/ets/dsl/ToDot.kt index ce00d893b..ff0b16ca6 100644 --- a/jacodb-ets/src/main/kotlin/org/jacodb/ets/dsl/ToDot.kt +++ b/jacodb-ets/src/main/kotlin/org/jacodb/ets/dsl/ToDot.kt @@ -16,6 +16,7 @@ package org.jacodb.ets.dsl +import org.jacodb.ets.utils.toDotLabel import java.util.IdentityHashMap private fun Node.toDotLabel() = when (this) { @@ -25,6 +26,7 @@ private fun Node.toDotLabel() = when (this) { is If -> "if ($condition)" is Label -> "label $name" is Goto -> "goto $targetLabel" + is CustomEts -> "???" } fun Program.toDot(): String { @@ -102,6 +104,7 @@ private fun BlockStmt.toDotLabel() = when (this) { is BlockReturn -> "return $expr" is BlockIf -> "if ($condition)" is BlockNop -> "nop" + is BlockCustomEts -> "???" } fun BlockCfg.toDot(): String { @@ -138,6 +141,7 @@ private fun Stmt.toDotLabel() = when (this) { is AssignStmt -> "$target := $expr" is ReturnStmt -> "return $expr" is IfStmt -> "if ($condition)" + is CustomEtsStmt -> "???" } fun LinearizedCfg.toDot(): String { diff --git a/jacodb-ets/src/main/kotlin/org/jacodb/ets/utils/BlockCfgBuilder.kt b/jacodb-ets/src/main/kotlin/org/jacodb/ets/utils/BlockCfgBuilder.kt index 742eb78db..7d4df727e 100644 --- a/jacodb-ets/src/main/kotlin/org/jacodb/ets/utils/BlockCfgBuilder.kt +++ b/jacodb-ets/src/main/kotlin/org/jacodb/ets/utils/BlockCfgBuilder.kt @@ -21,6 +21,7 @@ import org.jacodb.ets.dsl.BinaryOperator import org.jacodb.ets.dsl.Block import org.jacodb.ets.dsl.BlockAssign import org.jacodb.ets.dsl.BlockCfg +import org.jacodb.ets.dsl.BlockCustomEts import org.jacodb.ets.dsl.BlockIf import org.jacodb.ets.dsl.BlockNop import org.jacodb.ets.dsl.BlockReturn @@ -301,6 +302,10 @@ class EtsBlockCfgBuilder( condition = condition, ) } + + is BlockCustomEts -> { + etsStatements += stmt.toEts(stub) + } } }