From 4f2e22e4557e4413ec202b1862b53ffdbe2feebb Mon Sep 17 00:00:00 2001
From: Konstantin Chukharev <lipen00@gmail.com>
Date: Wed, 29 Jan 2025 15:30:07 +0300
Subject: [PATCH 01/16] Add CFG DSL

---
 .../kotlin/org/jacodb/ets/graph/CfgDsl.kt     | 692 ++++++++++++++++++
 .../org/jacodb/ets/graph/EtsBlockCfg.kt       | 380 ++++++++++
 .../org/jacodb/ets/utils/EtsCfgToDot.kt       |  73 ++
 .../jacodb/ets/utils/{Dot.kt => RenderDot.kt} |   0
 .../kotlin/org/jacodb/ets/utils/ViewDot.kt    |  44 ++
 5 files changed, 1189 insertions(+)
 create mode 100644 jacodb-ets/src/main/kotlin/org/jacodb/ets/graph/CfgDsl.kt
 create mode 100644 jacodb-ets/src/main/kotlin/org/jacodb/ets/graph/EtsBlockCfg.kt
 create mode 100644 jacodb-ets/src/main/kotlin/org/jacodb/ets/utils/EtsCfgToDot.kt
 rename jacodb-ets/src/main/kotlin/org/jacodb/ets/utils/{Dot.kt => RenderDot.kt} (100%)
 create mode 100644 jacodb-ets/src/main/kotlin/org/jacodb/ets/utils/ViewDot.kt

diff --git a/jacodb-ets/src/main/kotlin/org/jacodb/ets/graph/CfgDsl.kt b/jacodb-ets/src/main/kotlin/org/jacodb/ets/graph/CfgDsl.kt
new file mode 100644
index 000000000..6d93feb3c
--- /dev/null
+++ b/jacodb-ets/src/main/kotlin/org/jacodb/ets/graph/CfgDsl.kt
@@ -0,0 +1,692 @@
+/*
+ *  Copyright 2022 UnitTestBot contributors (utbot.org)
+ * <p>
+ *  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
+ * <p>
+ *  http://www.apache.org/licenses/LICENSE-2.0
+ * <p>
+ *  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.
+ */
+
+@file:Suppress("UnusedReceiverParameter")
+
+package org.jacodb.ets.graph
+
+import org.jacodb.ets.utils.view
+import java.util.IdentityHashMap
+
+sealed interface Expr
+
+data class Local(val name: String) : Expr {
+    override fun toString() = name
+}
+
+data class Parameter(val index: Int) : Expr {
+    override fun toString() = "param($index)"
+}
+
+object ThisRef : Expr {
+    override fun toString() = "this"
+}
+
+data class Constant(val value: Double) : Expr {
+    override fun toString() = "const($value)"
+}
+
+enum class BinaryOperator {
+    AND, OR,
+    EQ, NEQ, LT, LTE, GT, GTE,
+    ADD, SUB, MUL, DIV
+}
+
+data class BinaryExpr(
+    val operator: BinaryOperator,
+    val left: Expr,
+    val right: Expr,
+) : Expr {
+    override fun toString() = "${operator.name.lowercase()}($left, $right)"
+}
+
+enum class UnaryOperator { NOT, NEG }
+
+data class UnaryExpr(
+    val operator: UnaryOperator,
+    val expr: Expr,
+) : Expr {
+    override fun toString() = "${operator.name.lowercase()}($expr)"
+}
+
+sealed interface ProgramNode
+
+data object ProgramNop : ProgramNode
+
+data class ProgramAssign(
+    val target: Local,
+    val expr: Expr,
+) : ProgramNode
+
+data class ProgramReturn(
+    val expr: Expr,
+) : ProgramNode
+
+data class ProgramIf(
+    val condition: Expr,
+    val thenBranch: List<ProgramNode>,
+    val elseBranch: List<ProgramNode>,
+) : ProgramNode
+
+data class ProgramLabel(
+    val name: String,
+) : ProgramNode
+
+data class ProgramGoto(
+    val targetLabel: String,
+) : ProgramNode
+
+data class Program(
+    val nodes: List<ProgramNode>,
+) {
+    fun toText(): String {
+        val lines = mutableListOf<String>()
+        val indentStep = 2
+
+        fun process(nodes: List<ProgramNode>, indent: Int = 0) {
+            fun line(line: String) {
+                lines += " ".repeat(indent) + line
+            }
+
+            for (node in nodes) {
+                when (node) {
+                    is ProgramNop -> line("nop")
+                    is ProgramAssign -> line("${node.target} := ${node.expr}")
+                    is ProgramReturn -> line("return ${node.expr}")
+                    is ProgramIf -> {
+                        line("if (${node.condition}) {")
+                        process(node.thenBranch, indent + indentStep)
+                        if (node.elseBranch.isNotEmpty()) {
+                            line("} else {")
+                            process(node.elseBranch, indent + indentStep)
+                        }
+                        line("}")
+                    }
+
+                    is ProgramLabel -> line("label ${node.name}")
+                    is ProgramGoto -> line("goto ${node.targetLabel}")
+                }
+            }
+        }
+
+        process(nodes)
+
+        return lines.joinToString("\n")
+    }
+}
+
+fun program(block: ProgramBuilder.() -> Unit): Program {
+    val builder = ProgramBuilderImpl()
+    builder.block()
+    return builder.build()
+}
+
+interface ProgramBuilder {
+    fun assign(target: Local, expr: Expr)
+    fun ret(expr: Expr)
+    fun ifStmt(condition: Expr, block: IfBuilder.() -> Unit)
+    fun nop()
+    fun label(name: String)
+    fun goto(label: String)
+}
+
+fun ProgramBuilder.local(name: String): Local = Local(name)
+fun ProgramBuilder.param(index: Int): Parameter = Parameter(index)
+fun ProgramBuilder.thisRef(): Expr = ThisRef
+fun ProgramBuilder.const(value: Double): Constant = Constant(value)
+
+fun ProgramBuilder.and(left: Expr, right: Expr): Expr = BinaryExpr(BinaryOperator.AND, left, right)
+fun ProgramBuilder.or(left: Expr, right: Expr): Expr = BinaryExpr(BinaryOperator.OR, left, right)
+fun ProgramBuilder.eq(left: Expr, right: Expr): Expr = BinaryExpr(BinaryOperator.EQ, left, right)
+fun ProgramBuilder.neq(left: Expr, right: Expr): Expr = BinaryExpr(BinaryOperator.NEQ, left, right)
+fun ProgramBuilder.lt(left: Expr, right: Expr): Expr = BinaryExpr(BinaryOperator.LT, left, right)
+fun ProgramBuilder.leq(left: Expr, right: Expr): Expr = BinaryExpr(BinaryOperator.LTE, left, right)
+fun ProgramBuilder.gt(left: Expr, right: Expr): Expr = BinaryExpr(BinaryOperator.GT, left, right)
+fun ProgramBuilder.geq(left: Expr, right: Expr): Expr = BinaryExpr(BinaryOperator.GTE, left, right)
+fun ProgramBuilder.add(left: Expr, right: Expr): Expr = BinaryExpr(BinaryOperator.ADD, left, right)
+fun ProgramBuilder.sub(left: Expr, right: Expr): Expr = BinaryExpr(BinaryOperator.SUB, left, right)
+fun ProgramBuilder.mul(left: Expr, right: Expr): Expr = BinaryExpr(BinaryOperator.MUL, left, right)
+fun ProgramBuilder.div(left: Expr, right: Expr): Expr = BinaryExpr(BinaryOperator.DIV, left, right)
+
+fun ProgramBuilder.not(expr: Expr): Expr = UnaryExpr(UnaryOperator.NOT, expr)
+fun ProgramBuilder.neg(expr: Expr): Expr = UnaryExpr(UnaryOperator.NEG, expr)
+
+class ProgramBuilderImpl : ProgramBuilder {
+    private val _nodes: MutableList<ProgramNode> = mutableListOf()
+    val nodes: List<ProgramNode> get() = _nodes
+
+    fun build(): Program {
+        return Program(nodes)
+    }
+
+    override fun nop() {
+        _nodes += ProgramNop
+    }
+
+    override fun label(name: String) {
+        _nodes += ProgramLabel(name)
+    }
+
+    override fun goto(label: String) {
+        _nodes += ProgramGoto(label)
+    }
+
+    override fun ret(expr: Expr) {
+        _nodes += ProgramReturn(expr)
+    }
+
+    override fun assign(target: Local, expr: Expr) {
+        _nodes += ProgramAssign(target, expr)
+    }
+
+    override fun ifStmt(condition: Expr, block: IfBuilder.() -> Unit) {
+        val builder = IfBuilder().apply(block)
+        _nodes += ProgramIf(condition, builder.thenNodes, builder.elseNodes)
+    }
+}
+
+class IfBuilder : ProgramBuilder {
+    private val thenBuilder = ProgramBuilderImpl()
+    private val elseBuilder = ProgramBuilderImpl()
+    private var elseEntered = false
+
+    val thenNodes: List<ProgramNode> get() = thenBuilder.nodes
+    val elseNodes: List<ProgramNode> get() = elseBuilder.nodes
+
+    fun `else`(block: ProgramBuilder.() -> Unit) {
+        check(!elseEntered) { "Multiple else branches" }
+        elseEntered = true
+        elseBuilder.apply(block)
+    }
+
+    override fun assign(target: Local, expr: Expr) = thenBuilder.assign(target, expr)
+    override fun ifStmt(condition: Expr, block: IfBuilder.() -> Unit) = thenBuilder.ifStmt(condition, block)
+    override fun ret(expr: Expr) = thenBuilder.ret(expr)
+    override fun nop() = thenBuilder.nop()
+    override fun goto(label: String) = thenBuilder.goto(label)
+    override fun label(name: String) = thenBuilder.label(name)
+}
+
+private fun ProgramNode.toDotLabel() = when (this) {
+    is ProgramAssign -> "$target := $expr"
+    is ProgramReturn -> "return $expr"
+    is ProgramIf -> "if ($condition)"
+    is ProgramNop -> "nop"
+    is ProgramLabel -> "label $name"
+    is ProgramGoto -> "goto $targetLabel"
+}
+
+fun Program.toDot(): String {
+    val lines = mutableListOf<String>()
+    lines += "digraph cfg {"
+    lines += "  node [shape=rect fontname=\"monospace\"]"
+
+    val labelMap: MutableMap<String, ProgramLabel> = hashMapOf()
+    val nodeToId: MutableMap<ProgramNode, Int> = IdentityHashMap()
+    var freeId = 0
+
+    fun processForNodes(nodes: List<ProgramNode>) {
+        for (node in nodes) {
+            val id = nodeToId.computeIfAbsent(node) { freeId++ }
+            lines += "  $id [label=\"${node.toDotLabel()}\"]"
+            if (node is ProgramIf) {
+                processForNodes(node.thenBranch)
+                processForNodes(node.elseBranch)
+            }
+            if (node is ProgramLabel) {
+                check(node.name !in labelMap) { "Duplicate label: ${node.name}" }
+                labelMap[node.name] = node
+            }
+        }
+    }
+
+    processForNodes(nodes)
+
+    fun processForEdges(nodes: List<ProgramNode>) {
+        for (node in nodes) {
+            val id = nodeToId[node] ?: error("No ID for $node")
+            when (node) {
+                is ProgramIf -> {
+                    if (node.thenBranch.isNotEmpty()) {
+                        val thenNode = node.thenBranch.first()
+                        val thenId = nodeToId[thenNode] ?: error("No ID for $thenNode")
+                        lines += "  $id -> $thenId [label=\"true\"]"
+                        processForEdges(node.thenBranch)
+                    }
+                    if (node.elseBranch.isNotEmpty()) {
+                        val elseNode = node.elseBranch.first()
+                        val elseId = nodeToId[elseNode] ?: error("No ID for $elseNode")
+                        lines += "  $id -> $elseId [label=\"false\"]"
+                        processForEdges(node.elseBranch)
+                    }
+                }
+
+                is ProgramGoto -> {
+                    val labelNode = labelMap[node.targetLabel] ?: error("Unknown label: ${node.targetLabel}")
+                    val labelId = nodeToId[labelNode] ?: error("No ID for $labelNode")
+                    lines += "  $id -> $labelId"
+                }
+
+                else -> {
+                    // See below.
+                }
+            }
+        }
+
+        for ((cur, next) in nodes.zipWithNext()) {
+            val curId = nodeToId[cur] ?: error("No ID for $cur")
+            val nextId = nodeToId[next] ?: error("No ID for $next")
+            lines += "  $curId -> $nextId"
+        }
+    }
+    processForEdges(nodes)
+
+    lines += "}"
+    return lines.joinToString("\n")
+}
+
+//----- CFG -----
+
+sealed interface BlockStmt
+// TODO: merge BlockStmt and Stmt (add location to BlockStmt, initialize with -1)
+
+data object BlockNop : BlockStmt
+
+data class BlockAssign(
+    val target: Local,
+    val expr: Expr,
+) : BlockStmt
+
+data class BlockReturn(
+    val expr: Expr,
+) : BlockStmt
+
+data class BlockIf(
+    val condition: Expr,
+) : BlockStmt
+
+data class Block(
+    val id: Int,
+    val statements: List<BlockStmt>,
+)
+
+data class BlockCfg(
+    val blocks: List<Block>,
+    val successors: Map<Int, List<Int>>,
+)
+
+fun Program.toBlockCfg(): BlockCfg {
+    val labelToNode: MutableMap<String, ProgramNode> = hashMapOf()
+    val targets: MutableSet<ProgramNode> = hashSetOf()
+
+    fun findLabels(nodes: List<ProgramNode>) {
+        if (nodes.lastOrNull() is ProgramLabel) {
+            error("Label at the end of the block: $nodes")
+        }
+        for ((stmt, next) in nodes.zipWithNext()) {
+            if (stmt is ProgramLabel) {
+                check(next !is ProgramLabel) { "Two labels in a row: $stmt, $next" }
+                check(next !is ProgramGoto) { "Label followed by goto: $stmt, $next" }
+                check(stmt.name !in labelToNode) { "Duplicate label: ${stmt.name}" }
+                labelToNode[stmt.name] = next
+            }
+        }
+        for (node in nodes) {
+            if (node is ProgramIf) {
+                findLabels(node.thenBranch)
+                findLabels(node.elseBranch)
+            }
+            if (node is ProgramGoto) {
+                targets += labelToNode[node.targetLabel] ?: error("Unknown label: ${node.targetLabel}")
+            }
+        }
+    }
+
+    findLabels(nodes)
+
+    val blocks: MutableList<Block> = mutableListOf()
+    val successors: MutableMap<Int, List<Int>> = hashMapOf()
+    val stmtToBlock: MutableMap<BlockStmt, Int> = IdentityHashMap()
+    val nodeToStmt: MutableMap<ProgramNode, BlockStmt> = IdentityHashMap()
+
+    fun buildBlocks(nodes: List<ProgramNode>): Pair<Int, Int>? {
+        if (nodes.isEmpty()) return null
+
+        lateinit var currentBlock: MutableList<BlockStmt>
+
+        fun newBlock(): Block {
+            currentBlock = mutableListOf()
+            val block = Block(blocks.size, currentBlock)
+            blocks += block
+            return block
+        }
+
+        var block = newBlock()
+        val firstBlockId = block.id
+
+        for (node in nodes) {
+            if (node is ProgramLabel) continue
+
+            if (node in targets && currentBlock.isNotEmpty()) {
+                block.statements.forEach { stmtToBlock[it] = block.id }
+                val prevBlock = block
+                block = newBlock()
+                successors[prevBlock.id] = listOf(block.id)
+            }
+
+            if (node !is ProgramGoto) {
+                val stmt = when (node) {
+                    ProgramNop -> BlockNop
+                    is ProgramAssign -> BlockAssign(node.target, node.expr)
+                    is ProgramReturn -> BlockReturn(node.expr)
+                    is ProgramIf -> BlockIf(node.condition)
+                    else -> error("Unexpected node: $node")
+                }
+                nodeToStmt[node] = stmt
+                currentBlock += stmt
+            }
+
+            if (node is ProgramIf) {
+                block.statements.forEach { stmtToBlock[it] = block.id }
+                val ifBlock = block
+                block = newBlock()
+
+                val thenBlocks = buildBlocks(node.thenBranch)
+                val elseBlocks = buildBlocks(node.elseBranch)
+
+                when {
+                    thenBlocks != null && elseBlocks != null -> {
+                        val (thenStart, thenEnd) = thenBlocks
+                        val (elseStart, elseEnd) = elseBlocks
+                        successors[ifBlock.id] = listOf(thenStart, elseStart) // (true, false) branches
+                        when (blocks[thenEnd].statements.lastOrNull()) {
+                            is BlockReturn -> {}
+                            is BlockIf -> error("Unexpected if statement at the end of the block")
+                            else -> successors[thenEnd] = listOf(block.id)
+                        }
+                        when (blocks[elseEnd].statements.lastOrNull()) {
+                            is BlockReturn -> {}
+                            is BlockIf -> error("Unexpected if statement at the end of the block")
+                            else -> successors[elseEnd] = listOf(block.id)
+                        }
+                    }
+
+                    thenBlocks != null -> {
+                        val (thenStart, thenEnd) = thenBlocks
+                        successors[ifBlock.id] = listOf(thenStart, block.id) // (true, false) branches
+                        when (blocks[thenEnd].statements.lastOrNull()) {
+                            is BlockReturn -> {}
+                            is BlockIf -> error("Unexpected if statement at the end of the block")
+                            else -> successors[thenEnd] = listOf(block.id)
+                        }
+                    }
+
+                    elseBlocks != null -> {
+                        val (elseStart, elseEnd) = elseBlocks
+                        successors[ifBlock.id] = listOf(block.id, elseStart) // (true, false) branches
+                        when (blocks[elseEnd].statements.lastOrNull()) {
+                            is BlockReturn -> {}
+                            is BlockIf -> error("Unexpected if statement at the end of the block")
+                            else -> successors[elseEnd] = listOf(block.id)
+                        }
+                    }
+
+                    else -> {
+                        successors[ifBlock.id] = listOf(block.id)
+                    }
+                }
+            } else if (node is ProgramGoto) {
+                val targetNode = labelToNode[node.targetLabel] ?: error("Unknown label: ${node.targetLabel}")
+                val target = nodeToStmt[targetNode] ?: error("No statement for $targetNode")
+                val targetBlockId = stmtToBlock[target] ?: error("No block for $target")
+                successors[block.id] = listOf(targetBlockId)
+                block.statements.forEach { stmtToBlock[it] = block.id }
+                block = newBlock()
+            } else if (node is ProgramReturn) {
+                successors[block.id] = emptyList()
+                break
+            }
+        }
+
+        block.statements.forEach { stmtToBlock[it] = block.id }
+        val lastBlockId = block.id
+
+        return Pair(firstBlockId, lastBlockId)
+    }
+
+    buildBlocks(nodes)
+
+    return BlockCfg(blocks, successors)
+}
+
+private fun BlockStmt.toDotLabel() = when (this) {
+    is BlockAssign -> "$target := $expr"
+    is BlockReturn -> "return $expr"
+    is BlockIf -> "if ($condition)"
+    is BlockNop -> "nop"
+}
+
+fun BlockCfg.toDot(): String {
+    val lines = mutableListOf<String>()
+    lines += "digraph cfg {"
+    lines += "  node [shape=rect fontname=\"monospace\"]"
+
+    // Nodes
+    for (block in blocks) {
+        val s = block.statements.joinToString("") { it.toDotLabel() + "\\l" }
+        lines += "  ${block.id} [label=\"Block #${block.id}\\n${s}\"]"
+    }
+
+    // Edges
+    for (block in blocks) {
+        val succs = successors[block.id] ?: error("No successors for block ${block.id}")
+        if (succs.isEmpty()) continue
+        if (succs.size == 1) {
+            lines += "  ${block.id} -> ${succs.single()}"
+        } else {
+            check(succs.size == 2)
+            val (trueBranch, falseBranch) = succs // Note the order of successors: (true, false) branches
+            lines += "  ${block.id} -> $trueBranch [label=\"true\"]"
+            lines += "  ${block.id} -> $falseBranch [label=\"false\"]"
+        }
+    }
+
+    lines += "}"
+    return lines.joinToString("\n")
+}
+
+typealias StmtLocation = Int
+
+sealed interface Stmt {
+    val location: StmtLocation
+}
+
+data class NopStmt(
+    override val location: StmtLocation,
+) : Stmt
+
+data class AssignStmt(
+    override val location: StmtLocation,
+    val target: Local,
+    val expr: Expr,
+) : Stmt
+
+data class ReturnStmt(
+    override val location: StmtLocation,
+    val expr: Expr,
+) : Stmt
+
+data class IfStmt(
+    override val location: StmtLocation,
+    val condition: Expr,
+) : Stmt
+
+data class LinearizedCfg(
+    val statements: List<Stmt>,
+    val successors: Map<StmtLocation, List<StmtLocation>>,
+)
+
+fun BlockCfg.linearize(): LinearizedCfg {
+    val linearized: MutableList<Stmt> = mutableListOf()
+    val successors: MutableMap<StmtLocation, List<StmtLocation>> = hashMapOf()
+
+    fun process(statements: List<BlockStmt>): List<Stmt> {
+        val processed: MutableList<Stmt> = mutableListOf()
+        var loc = linearized.size
+        for (stmt in statements) {
+            when (stmt) {
+                is BlockNop -> {
+                    // Note: ignore NOP statements
+                    // processed += NopStmt(loc++)
+                }
+
+                is BlockAssign -> {
+                    // TODO: three-address code
+                    processed += AssignStmt(loc++, stmt.target, stmt.expr)
+                }
+
+                is BlockReturn -> {
+                    // TODO: three-address code
+                    processed += ReturnStmt(loc++, stmt.expr)
+                }
+
+                is BlockIf -> {
+                    // TODO: three-address code
+                    processed += IfStmt(loc++, stmt.condition)
+                }
+            }
+        }
+        if (processed.isEmpty()) {
+            processed += NopStmt(loc++)
+        }
+        linearized += processed
+        check(linearized.size == loc)
+        return processed
+    }
+
+    val linearizedBlocks = blocks.associate { it.id to process(it.statements) }
+
+    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 IfStmt) { "If statement in the middle of the block: $stmt" }
+            successors[stmt.location] = listOf(next.location)
+        }
+        if (statements.isNotEmpty()) {
+            val last = statements.last()
+            val nextBlocks = this@linearize.successors[id] ?: error("No successors for block $id")
+            // TODO: handle empty blocks (next)
+            successors[last.location] = nextBlocks.map { linearizedBlocks.getValue(it).first().location }
+        }
+    }
+
+    return LinearizedCfg(linearized, successors)
+}
+
+private fun Stmt.toDotLabel() = when (this) {
+    is NopStmt -> "nop"
+    is AssignStmt -> "$target := $expr"
+    is ReturnStmt -> "return $expr"
+    is IfStmt -> "if ($condition)"
+}
+
+fun LinearizedCfg.toDot(): String {
+    val lines = mutableListOf<String>()
+    lines += "digraph cfg {"
+    lines += "  node [shape=rect fontname=\"monospace\"]"
+
+    // Nodes
+    for (stmt in statements) {
+        lines += "  ${stmt.location} [label=\"${stmt.location}: ${stmt.toDotLabel()}\"]"
+    }
+
+    // Edges
+    for (stmt in statements) {
+        when (stmt) {
+            is IfStmt -> {
+                val succs = successors[stmt.location] ?: error("No successors for $stmt")
+                check(succs.size == 2) {
+                    "Expected two successors for $stmt, but it has ${succs.size}: $succs"
+                }
+                val (thenBranch, elseBranch) = succs
+                lines += "  ${stmt.location} -> $thenBranch [label=\"then\"]"
+                lines += "  ${stmt.location} -> $elseBranch [label=\"else\"]"
+            }
+
+            else -> {
+                val succs = successors[stmt.location] ?: error("No successors for $stmt")
+                if (succs.isNotEmpty()) {
+                    check(succs.size == 1) {
+                        "Expected one successor for $stmt, but it has ${succs.size}: $succs"
+                    }
+                    val target = succs.single()
+                    lines += "  ${stmt.location} -> $target"
+                }
+            }
+        }
+    }
+
+    lines += "}"
+    return lines.joinToString("\n")
+}
+
+private fun main() {
+    val prog = program {
+        assign(local("i"), param(0))
+
+        ifStmt(gt(local("i"), const(10.0))) {
+            ifStmt(eq(local("i"), const(42.0))) {
+                ret(local("i"))
+                `else` {
+                    assign(local("i"), const(10.0))
+                }
+            }
+            nop()
+        }
+
+        label("loop")
+        ifStmt(gt(local("i"), const(0.0))) {
+            assign(local("i"), sub(local("i"), const(1.0)))
+            goto("loop")
+            `else` {
+                ret(local("i"))
+            }
+        }
+
+        ret(const(42.0)) // unreachable
+    }
+
+    val doView = false
+
+    println("PROGRAM:")
+    println("-----")
+    println(prog.toText())
+    println("-----")
+
+    println("=== PROGRAM:")
+    println(prog.toDot())
+    if (doView) view(prog.toDot(), name = "program")
+
+    val blockCfg = prog.toBlockCfg()
+    println("=== BLOCK CFG:")
+    println(blockCfg.toDot())
+    if (doView) view(blockCfg.toDot(), name = "block")
+
+    val linearCfg = blockCfg.linearize()
+    println("=== LINEARIZED CFG:")
+    println(linearCfg.toDot())
+    if (doView) view(linearCfg.toDot(), name = "linear")
+}
diff --git a/jacodb-ets/src/main/kotlin/org/jacodb/ets/graph/EtsBlockCfg.kt b/jacodb-ets/src/main/kotlin/org/jacodb/ets/graph/EtsBlockCfg.kt
new file mode 100644
index 000000000..b66e2e2b8
--- /dev/null
+++ b/jacodb-ets/src/main/kotlin/org/jacodb/ets/graph/EtsBlockCfg.kt
@@ -0,0 +1,380 @@
+/*
+ *  Copyright 2022 UnitTestBot contributors (utbot.org)
+ * <p>
+ *  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
+ * <p>
+ *  http://www.apache.org/licenses/LICENSE-2.0
+ * <p>
+ *  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 org.jacodb.ets.graph
+
+import org.jacodb.ets.base.EtsAddExpr
+import org.jacodb.ets.base.EtsAndExpr
+import org.jacodb.ets.base.EtsAssignStmt
+import org.jacodb.ets.base.EtsClassType
+import org.jacodb.ets.base.EtsDivExpr
+import org.jacodb.ets.base.EtsEntity
+import org.jacodb.ets.base.EtsEqExpr
+import org.jacodb.ets.base.EtsGtEqExpr
+import org.jacodb.ets.base.EtsGtExpr
+import org.jacodb.ets.base.EtsIfStmt
+import org.jacodb.ets.base.EtsInstLocation
+import org.jacodb.ets.base.EtsLocal
+import org.jacodb.ets.base.EtsLtEqExpr
+import org.jacodb.ets.base.EtsLtExpr
+import org.jacodb.ets.base.EtsMulExpr
+import org.jacodb.ets.base.EtsNegExpr
+import org.jacodb.ets.base.EtsNopStmt
+import org.jacodb.ets.base.EtsNotEqExpr
+import org.jacodb.ets.base.EtsNotExpr
+import org.jacodb.ets.base.EtsNumberConstant
+import org.jacodb.ets.base.EtsOrExpr
+import org.jacodb.ets.base.EtsParameterRef
+import org.jacodb.ets.base.EtsReturnStmt
+import org.jacodb.ets.base.EtsStmt
+import org.jacodb.ets.base.EtsSubExpr
+import org.jacodb.ets.base.EtsThis
+import org.jacodb.ets.base.EtsType
+import org.jacodb.ets.base.EtsUnknownType
+import org.jacodb.ets.base.EtsValue
+import org.jacodb.ets.model.EtsClassSignature
+import org.jacodb.ets.model.EtsMethod
+import org.jacodb.ets.model.EtsMethodImpl
+import org.jacodb.ets.model.EtsMethodParameter
+import org.jacodb.ets.model.EtsMethodSignature
+import org.jacodb.ets.utils.toDot
+import org.jacodb.ets.utils.view
+import java.util.IdentityHashMap
+
+data class EtsBasicBlock(
+    val id: Int,
+    val statements: List<EtsStmt>,
+)
+
+class EtsBlockCfg(
+    val blocks: List<EtsBasicBlock>,
+    val successors: Map<Int, List<Int>>,
+)
+
+class EtsBlockCfgBuilder(
+    val method: EtsMethod,
+) {
+    fun build(blockCfg: BlockCfg): EtsBlockCfg {
+        return EtsBlockCfg(
+            blocks = blockCfg.blocks.map { it.toEtsBasicBlock() },
+            successors = blockCfg.successors,
+        )
+    }
+
+    private var freeTempLocal: Int = 0
+    private fun newTempLocal(type: EtsType): EtsLocal {
+        return EtsLocal(
+            name = "_tmp${freeTempLocal++}",
+            type = type,
+        )
+    }
+
+    private fun Block.toEtsBasicBlock(): EtsBasicBlock {
+        val etsStatements: MutableList<EtsStmt> = mutableListOf()
+
+        fun ensureSingleAddress(entity: EtsEntity): EtsValue {
+            if (entity is EtsValue) {
+                return entity
+            }
+            val newLocal = newTempLocal(entity.type)
+            etsStatements += EtsAssignStmt(
+                location = stub,
+                lhv = newLocal,
+                rhv = entity,
+            )
+            return newLocal
+        }
+
+        for (stmt in statements) {
+            when (stmt) {
+                BlockNop -> {
+                    etsStatements += EtsNopStmt(location = stub)
+                }
+
+                is BlockAssign -> {
+                    etsStatements += EtsAssignStmt(
+                        location = stub,
+                        lhv = stmt.target.toEtsEntity() as EtsLocal, // safe cast
+                        rhv = stmt.expr.toEtsEntity(),
+                    )
+                }
+
+                is BlockReturn -> {
+                    val returnValue = ensureSingleAddress(stmt.expr.toEtsEntity())
+                    etsStatements += EtsReturnStmt(
+                        location = stub,
+                        returnValue = returnValue,
+                    )
+                }
+
+                is BlockIf -> {
+                    etsStatements += EtsIfStmt(
+                        location = stub,
+                        condition = stmt.condition.toEtsEntity(),
+                    )
+                }
+            }
+        }
+
+        return EtsBasicBlock(
+            id = id,
+            statements = etsStatements,
+        )
+    }
+
+    private val stub = EtsInstLocation(method, -1)
+
+    private fun Expr.toEtsEntity(): EtsEntity = when (this) {
+        is Local -> EtsLocal(
+            name = name,
+            type = EtsUnknownType,
+        )
+
+        is Parameter -> EtsParameterRef(
+            index = index,
+            type = EtsUnknownType,
+        )
+
+        ThisRef -> EtsThis(type = EtsClassType(EtsClassSignature.DEFAULT))
+
+        is Constant -> EtsNumberConstant(value = value)
+
+        is UnaryExpr -> when (operator) {
+            UnaryOperator.NOT -> {
+                EtsNotExpr(arg = expr.toEtsEntity())
+            }
+
+            UnaryOperator.NEG -> {
+                EtsNegExpr(arg = expr.toEtsEntity(), type = EtsUnknownType)
+            }
+        }
+
+        is BinaryExpr -> when (operator) {
+            BinaryOperator.AND -> EtsAndExpr(
+                left = left.toEtsEntity(),
+                right = right.toEtsEntity(),
+                type = EtsUnknownType,
+            )
+
+            BinaryOperator.OR -> EtsOrExpr(
+                left = left.toEtsEntity(),
+                right = right.toEtsEntity(),
+                type = EtsUnknownType,
+            )
+
+            BinaryOperator.EQ -> EtsEqExpr(
+                left = left.toEtsEntity(),
+                right = right.toEtsEntity(),
+            )
+
+            BinaryOperator.NEQ -> EtsNotEqExpr(
+                left = left.toEtsEntity(),
+                right = right.toEtsEntity(),
+            )
+
+            BinaryOperator.LT -> EtsLtExpr(
+                left = left.toEtsEntity(),
+                right = right.toEtsEntity(),
+            )
+
+            BinaryOperator.LTE -> EtsLtEqExpr(
+                left = left.toEtsEntity(),
+                right = right.toEtsEntity(),
+            )
+
+            BinaryOperator.GT -> EtsGtExpr(
+                left = left.toEtsEntity(),
+                right = right.toEtsEntity(),
+            )
+
+            BinaryOperator.GTE -> EtsGtEqExpr(
+                left = left.toEtsEntity(),
+                right = right.toEtsEntity(),
+            )
+
+            BinaryOperator.ADD -> EtsAddExpr(
+                left = left.toEtsEntity(),
+                right = right.toEtsEntity(),
+                type = EtsUnknownType,
+            )
+
+            BinaryOperator.SUB -> EtsSubExpr(
+                left = left.toEtsEntity(),
+                right = right.toEtsEntity(),
+                type = EtsUnknownType,
+            )
+
+            BinaryOperator.MUL -> EtsMulExpr(
+                left = left.toEtsEntity(),
+                right = right.toEtsEntity(),
+                type = EtsUnknownType,
+            )
+
+            BinaryOperator.DIV -> EtsDivExpr(
+                left = left.toEtsEntity(),
+                right = right.toEtsEntity(),
+                type = EtsUnknownType,
+            )
+        }
+    }
+}
+
+fun EtsBlockCfg.linearize(): EtsCfg {
+    val linearized: MutableList<EtsStmt> = mutableListOf()
+    val successorMap: MutableMap<EtsStmt, List<EtsStmt>> = hashMapOf()
+    val stmtMap: MutableMap<EtsStmt, EtsStmt> = IdentityHashMap() // original -> linearized (with location)
+
+    val queue = ArrayDeque<EtsBasicBlock>()
+    val visited: MutableSet<EtsBasicBlock> = hashSetOf()
+
+    if (blocks.isNotEmpty()) {
+        queue.add(blocks.first())
+    }
+
+    while (queue.isNotEmpty()) {
+        val block = queue.removeFirst()
+        if (!visited.add(block)) continue
+
+        for (stmt in block.statements) {
+            val newStmt = when (stmt) {
+                is EtsNopStmt -> stmt.copy(location = stmt.location.copy(index = linearized.size))
+                is EtsAssignStmt -> stmt.copy(location = stmt.location.copy(index = linearized.size))
+                is EtsReturnStmt -> stmt.copy(location = stmt.location.copy(index = linearized.size))
+                is EtsIfStmt -> stmt.copy(location = stmt.location.copy(index = linearized.size))
+                else -> error("Unsupported statement type: $stmt")
+            }
+            stmtMap[stmt] = newStmt
+            linearized += newStmt
+        }
+
+        val successors = successors[block.id] ?: error("No successors for block ${block.id}")
+        for (succId in successors.asReversed()) {
+            val succ = blocks[succId]
+            queue.addFirst(succ)
+        }
+    }
+
+    for (block in blocks) {
+        check(block.statements.isNotEmpty()) {
+            "Block ${block.id} is empty"
+        }
+
+        for ((stmt, next) in block.statements.zipWithNext()) {
+            successorMap[stmtMap.getValue(stmt)] = listOf(stmtMap.getValue(next))
+        }
+
+        val successors = successors[block.id] ?: error("No successors for block ${block.id}")
+        val last = stmtMap.getValue(block.statements.last())
+        successorMap[last] = successors.map {
+            stmtMap.getValue(blocks[it].statements.first())
+        }
+    }
+
+    return EtsCfg(linearized, successorMap)
+}
+
+private fun EtsStmt.toDotLabel(): String = when (this) {
+    is EtsNopStmt -> "nop"
+    is EtsAssignStmt -> "$lhv := $rhv"
+    is EtsReturnStmt -> "return $returnValue"
+    is EtsIfStmt -> "if ($condition)"
+    else -> this.toString()
+}
+
+fun EtsBlockCfg.toDot(): String {
+    val useHtml = true
+
+    fun String.htmlEncode(): String = this
+        .replace("&", "&amp;")
+        .replace("<", "&lt;")
+        .replace(">", "&gt;")
+        .replace("\"", "&quot;")
+
+    val lines = mutableListOf<String>()
+    lines += "digraph cfg {"
+    lines += "  node [shape=${if (useHtml) "none" else "rect"} fontname=\"monospace\"]"
+
+    // Nodes
+    blocks.forEach { block ->
+        if (useHtml) {
+            val s = block.statements.joinToString("") {
+                "<tr><td align=\"left\">" + it.toDotLabel().htmlEncode() + "</td></tr>"
+            }
+            val h =
+                "<table border=\"0\" cellborder=\"1\" cellspacing=\"0\"><tr><td><b>Block #${block.id}</b></td></tr>${s}</table>"
+            lines += "  ${block.id} [label=<${h}>]"
+        } else {
+            val s = block.statements.joinToString("") { it.toDotLabel() + "\\l" }
+            lines += "  ${block.id} [label=\"Block #${block.id}\\n$s\"]"
+        }
+    }
+
+    // Edges
+    blocks.forEach { block ->
+        val succs = successors[block.id]
+        if (succs != null) {
+            if (succs.isEmpty()) return@forEach
+            if (succs.size == 1) {
+                lines += "  ${block.id} -> ${succs.single()}"
+            } else {
+                check(succs.size == 2)
+                val (trueBranch, falseBranch) = succs
+                lines += "  ${block.id} -> $trueBranch [label=\"true\"]"
+                lines += "  ${block.id} -> $falseBranch [label=\"false\"]"
+            }
+        }
+    }
+
+    lines += "}"
+    return lines.joinToString("\n")
+}
+
+private fun main() {
+    val method = EtsMethodImpl(
+        EtsMethodSignature(
+            enclosingClass = EtsClassSignature.DEFAULT,
+            name = "foo",
+            parameters = listOf(
+                EtsMethodParameter(
+                    index = 0,
+                    name = "x",
+                    type = EtsUnknownType,
+                ),
+                EtsMethodParameter(
+                    index = 1,
+                    name = "y",
+                    type = EtsUnknownType,
+                ),
+            ),
+            returnType = EtsUnknownType,
+        )
+    )
+    val p = program {
+        assign(local("x"), param(0))
+        assign(local("y"), param(1))
+        ifStmt(and(local("x"), local("y"))) {
+            ret(add(local("x"), local("y")))
+        }
+        ret(const(0.0))
+    }
+    val blockCfg = p.toBlockCfg()
+    val etsBlockCfg = EtsBlockCfgBuilder(method).build(blockCfg)
+    println(etsBlockCfg.toDot())
+    view(etsBlockCfg.toDot(), name = "etsBlockCfg")
+    val etsCfg = etsBlockCfg.linearize()
+    println(etsCfg.toDot())
+    view(etsCfg.toDot(), name = "etsCfg")
+}
diff --git a/jacodb-ets/src/main/kotlin/org/jacodb/ets/utils/EtsCfgToDot.kt b/jacodb-ets/src/main/kotlin/org/jacodb/ets/utils/EtsCfgToDot.kt
new file mode 100644
index 000000000..e63394f04
--- /dev/null
+++ b/jacodb-ets/src/main/kotlin/org/jacodb/ets/utils/EtsCfgToDot.kt
@@ -0,0 +1,73 @@
+/*
+ *  Copyright 2022 UnitTestBot contributors (utbot.org)
+ * <p>
+ *  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
+ * <p>
+ *  http://www.apache.org/licenses/LICENSE-2.0
+ * <p>
+ *  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 org.jacodb.ets.utils
+
+import org.jacodb.ets.base.EtsAssignStmt
+import org.jacodb.ets.base.EtsIfStmt
+import org.jacodb.ets.base.EtsNopStmt
+import org.jacodb.ets.base.EtsReturnStmt
+import org.jacodb.ets.base.EtsStmt
+import org.jacodb.ets.graph.EtsCfg
+
+private fun EtsStmt.toDotLabel(): String = when (this) {
+    is EtsNopStmt -> "nop"
+    is EtsAssignStmt -> "$lhv := $rhv"
+    is EtsReturnStmt -> "return $returnValue"
+    is EtsIfStmt -> "if ($condition)"
+    else -> this.toString() // TODO: support more statement types
+}
+
+fun EtsCfg.toDot(): String {
+    val lines = mutableListOf<String>()
+    lines += "digraph cfg {"
+    lines += "  node [shape=rect fontname=\"monospace\"]"
+
+    // Nodes
+    stmts.forEach { stmt ->
+        lines += "  ${stmt.location.index} [label=\"\\N: ${stmt.toDotLabel()}\"]"
+    }
+
+    // Edges
+    stmts.forEach { stmt ->
+        when (stmt) {
+            is EtsIfStmt -> {
+                val succs = successors(stmt)
+                check(succs.size == 2) {
+                    "Expected two successors for $stmt, but it has ${succs.size}: $succs"
+                }
+                // val (thenBranch, elseBranch) = succs.toList()
+                val (thenBranch, elseBranch) = succs.toList().reversed() // TODO: check order of successors
+                lines += "  ${stmt.location.index} -> ${thenBranch.location.index} [label=\"then\"]"
+                lines += "  ${stmt.location.index} -> ${elseBranch.location.index} [label=\"else\"]"
+            }
+
+            else -> {
+                val succs = successors(stmt)
+                if (succs.isNotEmpty()) {
+                    check(succs.size == 1) {
+                        "Expected one successor for $stmt, but it has ${succs.size}: $succs"
+                    }
+                    val target = succs.single()
+                    lines += "  ${stmt.location.index} -> ${target.location.index}"
+                }
+            }
+        }
+    }
+
+    lines += "}"
+    return lines.joinToString("\n")
+}
diff --git a/jacodb-ets/src/main/kotlin/org/jacodb/ets/utils/Dot.kt b/jacodb-ets/src/main/kotlin/org/jacodb/ets/utils/RenderDot.kt
similarity index 100%
rename from jacodb-ets/src/main/kotlin/org/jacodb/ets/utils/Dot.kt
rename to jacodb-ets/src/main/kotlin/org/jacodb/ets/utils/RenderDot.kt
diff --git a/jacodb-ets/src/main/kotlin/org/jacodb/ets/utils/ViewDot.kt b/jacodb-ets/src/main/kotlin/org/jacodb/ets/utils/ViewDot.kt
new file mode 100644
index 000000000..76e79dac2
--- /dev/null
+++ b/jacodb-ets/src/main/kotlin/org/jacodb/ets/utils/ViewDot.kt
@@ -0,0 +1,44 @@
+/*
+ *  Copyright 2022 UnitTestBot contributors (utbot.org)
+ * <p>
+ *  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
+ * <p>
+ *  http://www.apache.org/licenses/LICENSE-2.0
+ * <p>
+ *  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 org.jacodb.ets.utils
+
+import java.nio.file.Path
+import kotlin.io.path.createTempDirectory
+import kotlin.io.path.div
+import kotlin.io.path.writeText
+
+fun view(
+    dot: String,
+    viewerCmd: String = when {
+        System.getProperty("os.name").startsWith("Mac") -> "open"
+        System.getProperty("os.name").startsWith("Win") -> "cmd /c start"
+        else -> "xdg-open"
+    },
+    dotCmd: String = "dot",
+    outputFormat: String = "svg",
+    name: String = "graph",
+    tempDir: Path = createTempDirectory("dot"),
+) {
+    val dotFile = tempDir / "$name.dot"
+    println("Writing DOT file to $dotFile")
+    dotFile.writeText(dot)
+    val outputFile = tempDir / "$name.$outputFormat"
+    println("Rendering ${outputFormat.uppercase()} to '$outputFile'...")
+    Runtime.getRuntime().exec("$dotCmd -T$outputFormat -o $outputFile $dotFile").waitFor()
+    println("Opening rendered file '$outputFile'...")
+    Runtime.getRuntime().exec("$viewerCmd $outputFile").waitFor()
+}

From 941589583e33b1ca0f399e667cb57bfd42252d54 Mon Sep 17 00:00:00 2001
From: Konstantin Chukharev <lipen00@gmail.com>
Date: Thu, 30 Jan 2025 14:29:58 +0300
Subject: [PATCH 02/16] Use type of method parameter

---
 jacodb-ets/src/main/kotlin/org/jacodb/ets/graph/EtsBlockCfg.kt | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/jacodb-ets/src/main/kotlin/org/jacodb/ets/graph/EtsBlockCfg.kt b/jacodb-ets/src/main/kotlin/org/jacodb/ets/graph/EtsBlockCfg.kt
index b66e2e2b8..258cb805f 100644
--- a/jacodb-ets/src/main/kotlin/org/jacodb/ets/graph/EtsBlockCfg.kt
+++ b/jacodb-ets/src/main/kotlin/org/jacodb/ets/graph/EtsBlockCfg.kt
@@ -145,7 +145,7 @@ class EtsBlockCfgBuilder(
 
         is Parameter -> EtsParameterRef(
             index = index,
-            type = EtsUnknownType,
+            type = method.parameters[index].type,
         )
 
         ThisRef -> EtsThis(type = EtsClassType(EtsClassSignature.DEFAULT))

From 89478044b1e2ed9e214a1ff6fa2860fa60444d8e Mon Sep 17 00:00:00 2001
From: Konstantin Chukharev <lipen00@gmail.com>
Date: Thu, 30 Jan 2025 14:30:13 +0300
Subject: [PATCH 03/16] Extract vars

---
 .../src/main/kotlin/org/jacodb/ets/graph/EtsBlockCfg.kt  | 9 ++++++---
 1 file changed, 6 insertions(+), 3 deletions(-)

diff --git a/jacodb-ets/src/main/kotlin/org/jacodb/ets/graph/EtsBlockCfg.kt b/jacodb-ets/src/main/kotlin/org/jacodb/ets/graph/EtsBlockCfg.kt
index 258cb805f..98f166b9c 100644
--- a/jacodb-ets/src/main/kotlin/org/jacodb/ets/graph/EtsBlockCfg.kt
+++ b/jacodb-ets/src/main/kotlin/org/jacodb/ets/graph/EtsBlockCfg.kt
@@ -105,10 +105,12 @@ class EtsBlockCfgBuilder(
                 }
 
                 is BlockAssign -> {
+                    val lhv = stmt.target.toEtsEntity() as EtsLocal // safe cast
+                    val rhv = stmt.expr.toEtsEntity()
                     etsStatements += EtsAssignStmt(
                         location = stub,
-                        lhv = stmt.target.toEtsEntity() as EtsLocal, // safe cast
-                        rhv = stmt.expr.toEtsEntity(),
+                        lhv = lhv,
+                        rhv = rhv,
                     )
                 }
 
@@ -121,9 +123,10 @@ class EtsBlockCfgBuilder(
                 }
 
                 is BlockIf -> {
+                    val condition = stmt.condition.toEtsEntity()
                     etsStatements += EtsIfStmt(
                         location = stub,
-                        condition = stmt.condition.toEtsEntity(),
+                        condition = condition,
                     )
                 }
             }

From 147f719598d541b648d4f966bb62942363c4edcf Mon Sep 17 00:00:00 2001
From: Konstantin Chukharev <lipen00@gmail.com>
Date: Thu, 30 Jan 2025 14:34:41 +0300
Subject: [PATCH 04/16] Fix order of successors for EtsCfg

---
 .../src/main/kotlin/org/jacodb/ets/graph/EtsBlockCfg.kt    | 7 +++++--
 jacodb-ets/src/main/kotlin/org/jacodb/ets/graph/EtsCfg.kt  | 2 +-
 2 files changed, 6 insertions(+), 3 deletions(-)

diff --git a/jacodb-ets/src/main/kotlin/org/jacodb/ets/graph/EtsBlockCfg.kt b/jacodb-ets/src/main/kotlin/org/jacodb/ets/graph/EtsBlockCfg.kt
index 98f166b9c..abab28ca0 100644
--- a/jacodb-ets/src/main/kotlin/org/jacodb/ets/graph/EtsBlockCfg.kt
+++ b/jacodb-ets/src/main/kotlin/org/jacodb/ets/graph/EtsBlockCfg.kt
@@ -61,7 +61,7 @@ data class EtsBasicBlock(
 
 class EtsBlockCfg(
     val blocks: List<EtsBasicBlock>,
-    val successors: Map<Int, List<Int>>,
+    val successors: Map<Int, List<Int>>, // for 'if-stmt' block, successors are (true, false) branches
 )
 
 class EtsBlockCfgBuilder(
@@ -281,7 +281,10 @@ fun EtsBlockCfg.linearize(): EtsCfg {
 
         val successors = successors[block.id] ?: error("No successors for block ${block.id}")
         val last = stmtMap.getValue(block.statements.last())
-        successorMap[last] = successors.map {
+        // Note: reverse the order of successors, because in all CFGs, except EtsCfg,
+        //       the successors for the if-stmt are (true, false) branches,
+        //       and only the EtsCfg (which we are building here) has the (false, true) order.
+        successorMap[last] = successors.asReversed().map {
             stmtMap.getValue(blocks[it].statements.first())
         }
     }
diff --git a/jacodb-ets/src/main/kotlin/org/jacodb/ets/graph/EtsCfg.kt b/jacodb-ets/src/main/kotlin/org/jacodb/ets/graph/EtsCfg.kt
index 48de74a06..75f495524 100644
--- a/jacodb-ets/src/main/kotlin/org/jacodb/ets/graph/EtsCfg.kt
+++ b/jacodb-ets/src/main/kotlin/org/jacodb/ets/graph/EtsCfg.kt
@@ -22,7 +22,7 @@ import org.jacodb.impl.cfg.graphs.GraphDominators
 
 class EtsCfg(
     val stmts: List<EtsStmt>,
-    private val successorMap: Map<EtsStmt, List<EtsStmt>>,
+    private val successorMap: Map<EtsStmt, List<EtsStmt>>, // Note: EtsIfStmt successors are (false, true) branches
 ) : EtsBytecodeGraph<EtsStmt> {
 
     private val predecessorMap: Map<EtsStmt, Set<EtsStmt>> by lazy {

From bbc8181a8993863a9ecbb37db8d075026228b377 Mon Sep 17 00:00:00 2001
From: Konstantin Chukharev <lipen00@gmail.com>
Date: Thu, 30 Jan 2025 14:49:04 +0300
Subject: [PATCH 05/16] Customize indent in Program.toText

---
 .../src/main/kotlin/org/jacodb/ets/graph/CfgDsl.kt    | 11 +++++------
 1 file changed, 5 insertions(+), 6 deletions(-)

diff --git a/jacodb-ets/src/main/kotlin/org/jacodb/ets/graph/CfgDsl.kt b/jacodb-ets/src/main/kotlin/org/jacodb/ets/graph/CfgDsl.kt
index 6d93feb3c..6e375a0e1 100644
--- a/jacodb-ets/src/main/kotlin/org/jacodb/ets/graph/CfgDsl.kt
+++ b/jacodb-ets/src/main/kotlin/org/jacodb/ets/graph/CfgDsl.kt
@@ -92,13 +92,12 @@ data class ProgramGoto(
 data class Program(
     val nodes: List<ProgramNode>,
 ) {
-    fun toText(): String {
+    fun toText(indent: Int = 2): String {
         val lines = mutableListOf<String>()
-        val indentStep = 2
 
-        fun process(nodes: List<ProgramNode>, indent: Int = 0) {
+        fun process(nodes: List<ProgramNode>, currentIndent: Int = 0) {
             fun line(line: String) {
-                lines += " ".repeat(indent) + line
+                lines += " ".repeat(currentIndent) + line
             }
 
             for (node in nodes) {
@@ -108,10 +107,10 @@ data class Program(
                     is ProgramReturn -> line("return ${node.expr}")
                     is ProgramIf -> {
                         line("if (${node.condition}) {")
-                        process(node.thenBranch, indent + indentStep)
+                        process(node.thenBranch, currentIndent + indent)
                         if (node.elseBranch.isNotEmpty()) {
                             line("} else {")
-                            process(node.elseBranch, indent + indentStep)
+                            process(node.elseBranch, currentIndent + indent)
                         }
                         line("}")
                     }

From 325c7b5b0493c1930759cfbd49beee8993e1dfda Mon Sep 17 00:00:00 2001
From: Konstantin Chukharev <lipen00@gmail.com>
Date: Thu, 30 Jan 2025 14:49:32 +0300
Subject: [PATCH 06/16] Add test for cfg dsl

---
 .../org/jacodb/ets/test/EtsCfgDslTest.kt      | 99 +++++++++++++++++++
 1 file changed, 99 insertions(+)
 create mode 100644 jacodb-ets/src/test/kotlin/org/jacodb/ets/test/EtsCfgDslTest.kt

diff --git a/jacodb-ets/src/test/kotlin/org/jacodb/ets/test/EtsCfgDslTest.kt b/jacodb-ets/src/test/kotlin/org/jacodb/ets/test/EtsCfgDslTest.kt
new file mode 100644
index 000000000..4bd6e3e7f
--- /dev/null
+++ b/jacodb-ets/src/test/kotlin/org/jacodb/ets/test/EtsCfgDslTest.kt
@@ -0,0 +1,99 @@
+/*
+ *  Copyright 2022 UnitTestBot contributors (utbot.org)
+ * <p>
+ *  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
+ * <p>
+ *  http://www.apache.org/licenses/LICENSE-2.0
+ * <p>
+ *  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 org.jacodb.ets.test
+
+import org.jacodb.ets.base.EtsAssignStmt
+import org.jacodb.ets.base.EtsBooleanType
+import org.jacodb.ets.base.EtsLocal
+import org.jacodb.ets.base.EtsNumberType
+import org.jacodb.ets.base.EtsUnknownType
+import org.jacodb.ets.graph.EtsBlockCfgBuilder
+import org.jacodb.ets.graph.add
+import org.jacodb.ets.graph.const
+import org.jacodb.ets.graph.linearize
+import org.jacodb.ets.graph.local
+import org.jacodb.ets.graph.lt
+import org.jacodb.ets.graph.param
+import org.jacodb.ets.graph.program
+import org.jacodb.ets.graph.toBlockCfg
+import org.jacodb.ets.graph.toDot
+import org.jacodb.ets.model.EtsClassSignature
+import org.jacodb.ets.model.EtsFileSignature
+import org.jacodb.ets.model.EtsMethodImpl
+import org.jacodb.ets.model.EtsMethodParameter
+import org.jacodb.ets.model.EtsMethodSignature
+import org.jacodb.ets.utils.toDot
+import org.junit.jupiter.api.Test
+
+class EtsCfgDslTest {
+    @Test
+    fun `test simple program`() {
+        val prog = program {
+            val i = local("i")
+
+            // i := arg(0)
+            assign(i, param(0))
+
+            // if (i < 10) i += 50
+            ifStmt(lt(i, const(10.0))) {
+                assign(i, add(i, const(50.0)))
+            }
+
+            // return i
+            ret(i)
+        }
+        println("program:\n${prog.toText()}")
+        val blockCfg = prog.toBlockCfg()
+        println("blockCfg:\n${blockCfg.toDot()}")
+
+        val locals = mutableListOf<EtsLocal>()
+        val method = EtsMethodImpl(
+            signature = EtsMethodSignature(
+                enclosingClass = EtsClassSignature(
+                    name = "Test",
+                    file = EtsFileSignature(
+                        projectName = "TestProject",
+                        fileName = "Test.ts",
+                    ),
+                ),
+                name = "testMethod",
+                parameters = listOf(
+                    EtsMethodParameter(0, "a", EtsUnknownType),
+                ),
+                returnType = EtsNumberType,
+            ),
+            locals = locals,
+        )
+
+        val etsBlockCfg = EtsBlockCfgBuilder(method).build(blockCfg)
+        println("etsBlockCfg:\n${etsBlockCfg.toDot()}")
+        val etsCfg = etsBlockCfg.linearize()
+        println("etsCfg:\n${etsCfg.toDot()}")
+
+        method._cfg = etsCfg
+        locals += etsCfg.stmts
+            .filterIsInstance<EtsAssignStmt>()
+            .mapNotNull {
+                val left = it.lhv
+                if (left is EtsLocal) {
+                    left
+                } else {
+                    null
+                }
+            }
+    }
+}

From 5900f1086093bdbc0faa5c3246553c9383a6255d Mon Sep 17 00:00:00 2001
From: Konstantin Chukharev <lipen00@gmail.com>
Date: Thu, 30 Jan 2025 14:52:10 +0300
Subject: [PATCH 07/16] Use \N for node id in DOT

---
 jacodb-ets/src/main/kotlin/org/jacodb/ets/graph/CfgDsl.kt     | 4 ++--
 .../src/main/kotlin/org/jacodb/ets/graph/EtsBlockCfg.kt       | 4 ++--
 2 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/jacodb-ets/src/main/kotlin/org/jacodb/ets/graph/CfgDsl.kt b/jacodb-ets/src/main/kotlin/org/jacodb/ets/graph/CfgDsl.kt
index 6e375a0e1..c5582426f 100644
--- a/jacodb-ets/src/main/kotlin/org/jacodb/ets/graph/CfgDsl.kt
+++ b/jacodb-ets/src/main/kotlin/org/jacodb/ets/graph/CfgDsl.kt
@@ -486,7 +486,7 @@ fun BlockCfg.toDot(): String {
     // Nodes
     for (block in blocks) {
         val s = block.statements.joinToString("") { it.toDotLabel() + "\\l" }
-        lines += "  ${block.id} [label=\"Block #${block.id}\\n${s}\"]"
+        lines += "  ${block.id} [label=\"Block #\\N\\n${s}\"]"
     }
 
     // Edges
@@ -609,7 +609,7 @@ fun LinearizedCfg.toDot(): String {
 
     // Nodes
     for (stmt in statements) {
-        lines += "  ${stmt.location} [label=\"${stmt.location}: ${stmt.toDotLabel()}\"]"
+        lines += "  ${stmt.location} [label=\"\\N: ${stmt.toDotLabel()}\"]"
     }
 
     // Edges
diff --git a/jacodb-ets/src/main/kotlin/org/jacodb/ets/graph/EtsBlockCfg.kt b/jacodb-ets/src/main/kotlin/org/jacodb/ets/graph/EtsBlockCfg.kt
index abab28ca0..d28a7b950 100644
--- a/jacodb-ets/src/main/kotlin/org/jacodb/ets/graph/EtsBlockCfg.kt
+++ b/jacodb-ets/src/main/kotlin/org/jacodb/ets/graph/EtsBlockCfg.kt
@@ -320,11 +320,11 @@ fun EtsBlockCfg.toDot(): String {
                 "<tr><td align=\"left\">" + it.toDotLabel().htmlEncode() + "</td></tr>"
             }
             val h =
-                "<table border=\"0\" cellborder=\"1\" cellspacing=\"0\"><tr><td><b>Block #${block.id}</b></td></tr>${s}</table>"
+                "<table border=\"0\" cellborder=\"1\" cellspacing=\"0\"><tr><td><b>Block #\\N</b></td></tr>${s}</table>"
             lines += "  ${block.id} [label=<${h}>]"
         } else {
             val s = block.statements.joinToString("") { it.toDotLabel() + "\\l" }
-            lines += "  ${block.id} [label=\"Block #${block.id}\\n$s\"]"
+            lines += "  ${block.id} [label=\"Block #\\N\\n$s\"]"
         }
     }
 

From 8a571ea1e8f4eece0dc6f8d99f09cf726875940c Mon Sep 17 00:00:00 2001
From: Konstantin Chukharev <lipen00@gmail.com>
Date: Thu, 30 Jan 2025 14:54:05 +0300
Subject: [PATCH 08/16] Extract useHtml as parameter

---
 .../kotlin/org/jacodb/ets/graph/EtsBlockCfg.kt     | 14 ++++++--------
 1 file changed, 6 insertions(+), 8 deletions(-)

diff --git a/jacodb-ets/src/main/kotlin/org/jacodb/ets/graph/EtsBlockCfg.kt b/jacodb-ets/src/main/kotlin/org/jacodb/ets/graph/EtsBlockCfg.kt
index d28a7b950..1a85f64c2 100644
--- a/jacodb-ets/src/main/kotlin/org/jacodb/ets/graph/EtsBlockCfg.kt
+++ b/jacodb-ets/src/main/kotlin/org/jacodb/ets/graph/EtsBlockCfg.kt
@@ -300,15 +300,13 @@ private fun EtsStmt.toDotLabel(): String = when (this) {
     else -> this.toString()
 }
 
-fun EtsBlockCfg.toDot(): String {
-    val useHtml = true
-
-    fun String.htmlEncode(): String = this
-        .replace("&", "&amp;")
-        .replace("<", "&lt;")
-        .replace(">", "&gt;")
-        .replace("\"", "&quot;")
+private fun String.htmlEncode(): String = this
+    .replace("&", "&amp;")
+    .replace("<", "&lt;")
+    .replace(">", "&gt;")
+    .replace("\"", "&quot;")
 
+fun EtsBlockCfg.toDot(useHtml: Boolean = true): String {
     val lines = mutableListOf<String>()
     lines += "digraph cfg {"
     lines += "  node [shape=${if (useHtml) "none" else "rect"} fontname=\"monospace\"]"

From 7b2aad59f16d848fac9d41f1338d34b3a787868e Mon Sep 17 00:00:00 2001
From: Konstantin Chukharev <lipen00@gmail.com>
Date: Thu, 30 Jan 2025 15:03:45 +0300
Subject: [PATCH 09/16] Fix html labels

---
 .../src/main/kotlin/org/jacodb/ets/graph/EtsBlockCfg.kt   | 8 +++++---
 1 file changed, 5 insertions(+), 3 deletions(-)

diff --git a/jacodb-ets/src/main/kotlin/org/jacodb/ets/graph/EtsBlockCfg.kt b/jacodb-ets/src/main/kotlin/org/jacodb/ets/graph/EtsBlockCfg.kt
index 1a85f64c2..93c7cb320 100644
--- a/jacodb-ets/src/main/kotlin/org/jacodb/ets/graph/EtsBlockCfg.kt
+++ b/jacodb-ets/src/main/kotlin/org/jacodb/ets/graph/EtsBlockCfg.kt
@@ -315,10 +315,12 @@ fun EtsBlockCfg.toDot(useHtml: Boolean = true): String {
     blocks.forEach { block ->
         if (useHtml) {
             val s = block.statements.joinToString("") {
-                "<tr><td align=\"left\">" + it.toDotLabel().htmlEncode() + "</td></tr>"
+                it.toDotLabel().htmlEncode() + "<br/>"
             }
-            val h =
-                "<table border=\"0\" cellborder=\"1\" cellspacing=\"0\"><tr><td><b>Block #\\N</b></td></tr>${s}</table>"
+            val h = "<table border=\"0\" cellborder=\"1\" cellspacing=\"0\">" +
+                "<tr><td>" + "<b>Block #\\N</b>" + "</td></tr>" +
+                "<tr><td balign=\"left\">" + s + "</td></tr>" +
+                "</table>"
             lines += "  ${block.id} [label=<${h}>]"
         } else {
             val s = block.statements.joinToString("") { it.toDotLabel() + "\\l" }

From 38109b3c31171b90acd2138b7c8cdbb9ab43ed44 Mon Sep 17 00:00:00 2001
From: Konstantin Chukharev <lipen00@gmail.com>
Date: Thu, 30 Jan 2025 16:50:28 +0300
Subject: [PATCH 10/16] Initialize EtsCfg.EMPTY once

---
 jacodb-ets/src/main/kotlin/org/jacodb/ets/graph/EtsCfg.kt    | 4 ++--
 jacodb-ets/src/main/kotlin/org/jacodb/ets/model/EtsMethod.kt | 2 +-
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/jacodb-ets/src/main/kotlin/org/jacodb/ets/graph/EtsCfg.kt b/jacodb-ets/src/main/kotlin/org/jacodb/ets/graph/EtsCfg.kt
index 75f495524..9a444b58b 100644
--- a/jacodb-ets/src/main/kotlin/org/jacodb/ets/graph/EtsCfg.kt
+++ b/jacodb-ets/src/main/kotlin/org/jacodb/ets/graph/EtsCfg.kt
@@ -61,8 +61,8 @@ class EtsCfg(
     }
 
     companion object {
-        fun empty(): EtsCfg {
-            return EtsCfg(emptyList(), emptyMap())
+        val EMPTY: EtsCfg by lazy {
+            EtsCfg(emptyList(), emptyMap())
         }
     }
 }
diff --git a/jacodb-ets/src/main/kotlin/org/jacodb/ets/model/EtsMethod.kt b/jacodb-ets/src/main/kotlin/org/jacodb/ets/model/EtsMethod.kt
index fb294301c..4e5993aa1 100644
--- a/jacodb-ets/src/main/kotlin/org/jacodb/ets/model/EtsMethod.kt
+++ b/jacodb-ets/src/main/kotlin/org/jacodb/ets/model/EtsMethod.kt
@@ -61,7 +61,7 @@ class EtsMethodImpl(
     var _cfg: EtsCfg? = null
 
     override val cfg: EtsCfg
-        get() = _cfg ?: EtsCfg.empty()
+        get() = _cfg ?: EtsCfg.EMPTY
 
     override fun toString(): String {
         return signature.toString()

From 0e564ae69f6e6b67c47c4c698ee01417b8eb1382 Mon Sep 17 00:00:00 2001
From: Konstantin Chukharev <lipen00@gmail.com>
Date: Thu, 30 Jan 2025 16:50:54 +0300
Subject: [PATCH 11/16] Remove comment

---
 jacodb-ets/src/main/kotlin/org/jacodb/ets/model/EtsMethod.kt | 1 -
 1 file changed, 1 deletion(-)

diff --git a/jacodb-ets/src/main/kotlin/org/jacodb/ets/model/EtsMethod.kt b/jacodb-ets/src/main/kotlin/org/jacodb/ets/model/EtsMethod.kt
index 4e5993aa1..a2410b529 100644
--- a/jacodb-ets/src/main/kotlin/org/jacodb/ets/model/EtsMethod.kt
+++ b/jacodb-ets/src/main/kotlin/org/jacodb/ets/model/EtsMethod.kt
@@ -23,7 +23,6 @@ import org.jacodb.ets.base.EtsLocal
 import org.jacodb.ets.base.EtsType
 import org.jacodb.ets.graph.EtsCfg
 
-// TODO: typeParameters
 interface EtsMethod : EtsBaseModel, CommonMethod {
     val signature: EtsMethodSignature
     val typeParameters: List<EtsType>

From 9373a40b7b0c6fe17441dc2543c6cd426f112d76 Mon Sep 17 00:00:00 2001
From: Konstantin Chukharev <lipen00@gmail.com>
Date: Thu, 30 Jan 2025 18:03:40 +0300
Subject: [PATCH 12/16] Split and move

---
 .../kotlin/org/jacodb/ets/dsl/BlockCfg.kt     | 174 +++++
 .../kotlin/org/jacodb/ets/dsl/BlockStmt.kt    |  34 +
 .../src/main/kotlin/org/jacodb/ets/dsl/DSL.kt |  67 ++
 .../main/kotlin/org/jacodb/ets/dsl/Expr.kt    |  60 ++
 .../org/jacodb/ets/dsl/LinearizedCfg.kt       |  76 ++
 .../main/kotlin/org/jacodb/ets/dsl/Node.kt    |  44 ++
 .../main/kotlin/org/jacodb/ets/dsl/Program.kt |  61 ++
 .../org/jacodb/ets/dsl/ProgramBuilder.kt      | 105 +++
 .../main/kotlin/org/jacodb/ets/dsl/Stmt.kt    |  43 ++
 .../main/kotlin/org/jacodb/ets/dsl/ToDot.kt   | 181 +++++
 .../kotlin/org/jacodb/ets/graph/CfgDsl.kt     | 691 ------------------
 .../org/jacodb/ets/graph/EtsBlockCfg.kt       |  24 +-
 .../org/jacodb/ets/utils/IdentityHashSet.kt   |  35 +
 .../org/jacodb/ets/test/EtsCfgDslTest.kt      |  16 +-
 14 files changed, 911 insertions(+), 700 deletions(-)
 create mode 100644 jacodb-ets/src/main/kotlin/org/jacodb/ets/dsl/BlockCfg.kt
 create mode 100644 jacodb-ets/src/main/kotlin/org/jacodb/ets/dsl/BlockStmt.kt
 create mode 100644 jacodb-ets/src/main/kotlin/org/jacodb/ets/dsl/DSL.kt
 create mode 100644 jacodb-ets/src/main/kotlin/org/jacodb/ets/dsl/Expr.kt
 create mode 100644 jacodb-ets/src/main/kotlin/org/jacodb/ets/dsl/LinearizedCfg.kt
 create mode 100644 jacodb-ets/src/main/kotlin/org/jacodb/ets/dsl/Node.kt
 create mode 100644 jacodb-ets/src/main/kotlin/org/jacodb/ets/dsl/Program.kt
 create mode 100644 jacodb-ets/src/main/kotlin/org/jacodb/ets/dsl/ProgramBuilder.kt
 create mode 100644 jacodb-ets/src/main/kotlin/org/jacodb/ets/dsl/Stmt.kt
 create mode 100644 jacodb-ets/src/main/kotlin/org/jacodb/ets/dsl/ToDot.kt
 delete mode 100644 jacodb-ets/src/main/kotlin/org/jacodb/ets/graph/CfgDsl.kt
 create mode 100644 jacodb-ets/src/main/kotlin/org/jacodb/ets/utils/IdentityHashSet.kt

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
new file mode 100644
index 000000000..de876ffc5
--- /dev/null
+++ b/jacodb-ets/src/main/kotlin/org/jacodb/ets/dsl/BlockCfg.kt
@@ -0,0 +1,174 @@
+/*
+ *  Copyright 2022 UnitTestBot contributors (utbot.org)
+ * <p>
+ *  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
+ * <p>
+ *  http://www.apache.org/licenses/LICENSE-2.0
+ * <p>
+ *  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 org.jacodb.ets.dsl
+
+import org.jacodb.ets.utils.IdentityHashSet
+import java.util.IdentityHashMap
+
+data class Block(
+    val id: Int,
+    val statements: List<BlockStmt>,
+)
+
+data class BlockCfg(
+    val blocks: List<Block>,
+    val successors: Map<Int, List<Int>>,
+)
+
+fun Program.toBlockCfg(): BlockCfg {
+    val labelToNode: MutableMap<String, Node> = hashMapOf()
+    val targets: MutableSet<Node> = IdentityHashSet()
+
+    fun findLabels(nodes: List<Node>) {
+        if (nodes.lastOrNull() is Label) {
+            error("Label at the end of the block: $nodes")
+        }
+        for ((stmt, next) in nodes.zipWithNext()) {
+            if (stmt is Label) {
+                check(next !is Label) { "Two labels in a row: $stmt, $next" }
+                check(next !is Goto) { "Label followed by goto: $stmt, $next" }
+                check(stmt.name !in labelToNode) { "Duplicate label: ${stmt.name}" }
+                labelToNode[stmt.name] = next
+            }
+        }
+        for (node in nodes) {
+            if (node is If) {
+                findLabels(node.thenBranch)
+                findLabels(node.elseBranch)
+            }
+            if (node is Goto) {
+                targets += labelToNode[node.targetLabel] ?: error("Unknown label: ${node.targetLabel}")
+            }
+        }
+    }
+
+    findLabels(nodes)
+
+    val blocks: MutableList<Block> = mutableListOf()
+    val successors: MutableMap<Int, List<Int>> = hashMapOf()
+    val stmtToBlock: MutableMap<BlockStmt, Int> = IdentityHashMap()
+    val nodeToStmt: MutableMap<Node, BlockStmt> = IdentityHashMap()
+
+    fun buildBlocks(nodes: List<Node>): Pair<Int, Int>? {
+        if (nodes.isEmpty()) return null
+
+        lateinit var currentBlock: MutableList<BlockStmt>
+
+        fun newBlock(): Block {
+            currentBlock = mutableListOf()
+            val block = Block(blocks.size, currentBlock)
+            blocks += block
+            return block
+        }
+
+        var block = newBlock()
+        val firstBlockId = block.id
+
+        for (node in nodes) {
+            if (node is Label) continue
+
+            if (node in targets && currentBlock.isNotEmpty()) {
+                block.statements.forEach { stmtToBlock[it] = block.id }
+                val prevBlock = block
+                block = newBlock()
+                successors[prevBlock.id] = listOf(block.id)
+            }
+
+            if (node !is Goto) {
+                val stmt = when (node) {
+                    Nop -> BlockNop
+                    is Assign -> BlockAssign(node.target, node.expr)
+                    is Return -> BlockReturn(node.expr)
+                    is If -> BlockIf(node.condition)
+                    else -> error("Unexpected node: $node")
+                }
+                nodeToStmt[node] = stmt
+                currentBlock += stmt
+            }
+
+            if (node is If) {
+                block.statements.forEach { stmtToBlock[it] = block.id }
+                val ifBlock = block
+                block = newBlock()
+
+                val thenBlocks = buildBlocks(node.thenBranch)
+                val elseBlocks = buildBlocks(node.elseBranch)
+
+                when {
+                    thenBlocks != null && elseBlocks != null -> {
+                        val (thenStart, thenEnd) = thenBlocks
+                        val (elseStart, elseEnd) = elseBlocks
+                        successors[ifBlock.id] = listOf(thenStart, elseStart) // (true, false) branches
+                        when (blocks[thenEnd].statements.lastOrNull()) {
+                            is BlockReturn -> {}
+                            is BlockIf -> error("Unexpected if statement at the end of the block")
+                            else -> successors[thenEnd] = listOf(block.id)
+                        }
+                        when (blocks[elseEnd].statements.lastOrNull()) {
+                            is BlockReturn -> {}
+                            is BlockIf -> error("Unexpected if statement at the end of the block")
+                            else -> successors[elseEnd] = listOf(block.id)
+                        }
+                    }
+
+                    thenBlocks != null -> {
+                        val (thenStart, thenEnd) = thenBlocks
+                        successors[ifBlock.id] = listOf(thenStart, block.id) // (true, false) branches
+                        when (blocks[thenEnd].statements.lastOrNull()) {
+                            is BlockReturn -> {}
+                            is BlockIf -> error("Unexpected if statement at the end of the block")
+                            else -> successors[thenEnd] = listOf(block.id)
+                        }
+                    }
+
+                    elseBlocks != null -> {
+                        val (elseStart, elseEnd) = elseBlocks
+                        successors[ifBlock.id] = listOf(block.id, elseStart) // (true, false) branches
+                        when (blocks[elseEnd].statements.lastOrNull()) {
+                            is BlockReturn -> {}
+                            is BlockIf -> error("Unexpected if statement at the end of the block")
+                            else -> successors[elseEnd] = listOf(block.id)
+                        }
+                    }
+
+                    else -> {
+                        successors[ifBlock.id] = listOf(block.id)
+                    }
+                }
+            } else if (node is Goto) {
+                val targetNode = labelToNode[node.targetLabel] ?: error("Unknown label: ${node.targetLabel}")
+                val target = nodeToStmt[targetNode] ?: error("No statement for $targetNode")
+                val targetBlockId = stmtToBlock[target] ?: error("No block for $target")
+                successors[block.id] = listOf(targetBlockId)
+                block.statements.forEach { stmtToBlock[it] = block.id }
+                block = newBlock()
+            } else if (node is Return) {
+                successors[block.id] = emptyList()
+                break
+            }
+        }
+
+        block.statements.forEach { stmtToBlock[it] = block.id }
+        val lastBlockId = block.id
+
+        return Pair(firstBlockId, lastBlockId)
+    }
+
+    buildBlocks(nodes)
+
+    return BlockCfg(blocks, successors)
+}
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
new file mode 100644
index 000000000..fedd15c80
--- /dev/null
+++ b/jacodb-ets/src/main/kotlin/org/jacodb/ets/dsl/BlockStmt.kt
@@ -0,0 +1,34 @@
+/*
+ *  Copyright 2022 UnitTestBot contributors (utbot.org)
+ * <p>
+ *  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
+ * <p>
+ *  http://www.apache.org/licenses/LICENSE-2.0
+ * <p>
+ *  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 org.jacodb.ets.dsl
+
+sealed interface BlockStmt
+
+data object BlockNop : BlockStmt
+
+data class BlockAssign(
+    val target: Local,
+    val expr: Expr,
+) : BlockStmt
+
+data class BlockReturn(
+    val expr: Expr,
+) : BlockStmt
+
+data class BlockIf(
+    val condition: Expr,
+) : 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
new file mode 100644
index 000000000..2e09b3b87
--- /dev/null
+++ b/jacodb-ets/src/main/kotlin/org/jacodb/ets/dsl/DSL.kt
@@ -0,0 +1,67 @@
+/*
+ *  Copyright 2022 UnitTestBot contributors (utbot.org)
+ * <p>
+ *  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
+ * <p>
+ *  http://www.apache.org/licenses/LICENSE-2.0
+ * <p>
+ *  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 org.jacodb.ets.dsl
+
+import org.jacodb.ets.utils.view
+
+private fun main() {
+    val prog = program {
+        assign(local("i"), param(0))
+
+        ifStmt(gt(local("i"), const(10.0))) {
+            ifStmt(eq(local("i"), const(42.0))) {
+                ret(local("i"))
+                `else` {
+                    assign(local("i"), const(10.0))
+                }
+            }
+            nop()
+        }
+
+        label("loop")
+        ifStmt(gt(local("i"), const(0.0))) {
+            assign(local("i"), sub(local("i"), const(1.0)))
+            goto("loop")
+            `else` {
+                ret(local("i"))
+            }
+        }
+
+        ret(const(42.0)) // unreachable
+    }
+
+    val doView = false
+
+    println("PROGRAM:")
+    println("-----")
+    println(prog.toText())
+    println("-----")
+
+    println("=== PROGRAM:")
+    println(prog.toDot())
+    if (doView) view(prog.toDot(), name = "program")
+
+    val blockCfg = prog.toBlockCfg()
+    println("=== BLOCK CFG:")
+    println(blockCfg.toDot())
+    if (doView) view(blockCfg.toDot(), name = "block")
+
+    val linearCfg = blockCfg.linearize()
+    println("=== LINEARIZED CFG:")
+    println(linearCfg.toDot())
+    if (doView) view(linearCfg.toDot(), name = "linear")
+}
diff --git a/jacodb-ets/src/main/kotlin/org/jacodb/ets/dsl/Expr.kt b/jacodb-ets/src/main/kotlin/org/jacodb/ets/dsl/Expr.kt
new file mode 100644
index 000000000..ca7acc420
--- /dev/null
+++ b/jacodb-ets/src/main/kotlin/org/jacodb/ets/dsl/Expr.kt
@@ -0,0 +1,60 @@
+/*
+ *  Copyright 2022 UnitTestBot contributors (utbot.org)
+ * <p>
+ *  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
+ * <p>
+ *  http://www.apache.org/licenses/LICENSE-2.0
+ * <p>
+ *  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 org.jacodb.ets.dsl
+
+sealed interface Expr
+
+data class Local(val name: String) : Expr {
+    override fun toString() = name
+}
+
+data class Parameter(val index: Int) : Expr {
+    override fun toString() = "param($index)"
+}
+
+object ThisRef : Expr {
+    override fun toString() = "this"
+}
+
+data class Constant(val value: Double) : Expr {
+    override fun toString() = "const($value)"
+}
+
+enum class BinaryOperator {
+    AND, OR,
+    EQ, NEQ, LT, LTE, GT, GTE,
+    ADD, SUB, MUL, DIV
+}
+
+data class BinaryExpr(
+    val operator: BinaryOperator,
+    val left: Expr,
+    val right: Expr,
+) : Expr {
+    override fun toString() = "${operator.name.lowercase()}($left, $right)"
+}
+
+enum class UnaryOperator {
+    NOT, NEG
+}
+
+data class UnaryExpr(
+    val operator: UnaryOperator,
+    val expr: Expr,
+) : Expr {
+    override fun toString() = "${operator.name.lowercase()}($expr)"
+}
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
new file mode 100644
index 000000000..cc6078de5
--- /dev/null
+++ b/jacodb-ets/src/main/kotlin/org/jacodb/ets/dsl/LinearizedCfg.kt
@@ -0,0 +1,76 @@
+/*
+ *  Copyright 2022 UnitTestBot contributors (utbot.org)
+ * <p>
+ *  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
+ * <p>
+ *  http://www.apache.org/licenses/LICENSE-2.0
+ * <p>
+ *  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 org.jacodb.ets.dsl
+
+data class LinearizedCfg(
+    val statements: List<Stmt>,
+    val successors: Map<StmtLocation, List<StmtLocation>>,
+)
+
+fun BlockCfg.linearize(): LinearizedCfg {
+    val linearized: MutableList<Stmt> = mutableListOf()
+    val successors: MutableMap<StmtLocation, List<StmtLocation>> = hashMapOf()
+
+    fun process(statements: List<BlockStmt>): List<Stmt> {
+        val processed: MutableList<Stmt> = mutableListOf()
+        var loc = linearized.size
+        for (stmt in statements) {
+            when (stmt) {
+                is BlockNop -> {
+                    // Note: ignore NOP statements
+                    // processed += NopStmt(loc++)
+                }
+
+                is BlockAssign -> {
+                    processed += AssignStmt(loc++, stmt.target, stmt.expr)
+                }
+
+                is BlockReturn -> {
+                    processed += ReturnStmt(loc++, stmt.expr)
+                }
+
+                is BlockIf -> {
+                    processed += IfStmt(loc++, stmt.condition)
+                }
+            }
+        }
+        if (processed.isEmpty()) {
+            processed += NopStmt(loc++)
+        }
+        linearized += processed
+        check(linearized.size == loc)
+        return processed
+    }
+
+    val linearizedBlocks = blocks.associate { it.id to process(it.statements) }
+
+    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 IfStmt) { "If statement in the middle of the block: $stmt" }
+            successors[stmt.location] = listOf(next.location)
+        }
+        if (statements.isNotEmpty()) {
+            val last = statements.last()
+            val nextBlocks = this@linearize.successors[id] ?: error("No successors for block $id")
+            // TODO: handle empty blocks (next)
+            successors[last.location] = nextBlocks.map { linearizedBlocks.getValue(it).first().location }
+        }
+    }
+
+    return LinearizedCfg(linearized, successors)
+}
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
new file mode 100644
index 000000000..817fd814c
--- /dev/null
+++ b/jacodb-ets/src/main/kotlin/org/jacodb/ets/dsl/Node.kt
@@ -0,0 +1,44 @@
+/*
+ *  Copyright 2022 UnitTestBot contributors (utbot.org)
+ * <p>
+ *  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
+ * <p>
+ *  http://www.apache.org/licenses/LICENSE-2.0
+ * <p>
+ *  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 org.jacodb.ets.dsl
+
+sealed interface Node
+
+data object Nop : Node
+
+data class Assign(
+    val target: Local,
+    val expr: Expr,
+) : Node
+
+data class Return(
+    val expr: Expr,
+) : Node
+
+data class If(
+    val condition: Expr,
+    val thenBranch: List<Node>,
+    val elseBranch: List<Node>,
+) : Node
+
+data class Label(
+    val name: String,
+) : Node
+
+data class Goto(
+    val targetLabel: String,
+) : 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
new file mode 100644
index 000000000..68e2fda05
--- /dev/null
+++ b/jacodb-ets/src/main/kotlin/org/jacodb/ets/dsl/Program.kt
@@ -0,0 +1,61 @@
+/*
+ *  Copyright 2022 UnitTestBot contributors (utbot.org)
+ * <p>
+ *  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
+ * <p>
+ *  http://www.apache.org/licenses/LICENSE-2.0
+ * <p>
+ *  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 org.jacodb.ets.dsl
+
+data class Program(
+    val nodes: List<Node>,
+) {
+    fun toText(indent: Int = 2): String {
+        val lines = mutableListOf<String>()
+
+        fun process(nodes: List<Node>, currentIndent: Int = 0) {
+            fun line(line: String) {
+                lines += " ".repeat(currentIndent) + line
+            }
+
+            for (node in nodes) {
+                when (node) {
+                    is Nop -> line("nop")
+                    is Assign -> line("${node.target} := ${node.expr}")
+                    is Return -> line("return ${node.expr}")
+                    is If -> {
+                        line("if (${node.condition}) {")
+                        process(node.thenBranch, currentIndent + indent)
+                        if (node.elseBranch.isNotEmpty()) {
+                            line("} else {")
+                            process(node.elseBranch, currentIndent + indent)
+                        }
+                        line("}")
+                    }
+
+                    is Label -> line("label ${node.name}")
+                    is Goto -> line("goto ${node.targetLabel}")
+                }
+            }
+        }
+
+        process(nodes)
+
+        return lines.joinToString("\n")
+    }
+}
+
+fun program(block: ProgramBuilder.() -> Unit): Program {
+    val builder = ProgramBuilderImpl()
+    builder.block()
+    return builder.build()
+}
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
new file mode 100644
index 000000000..d8347ad2f
--- /dev/null
+++ b/jacodb-ets/src/main/kotlin/org/jacodb/ets/dsl/ProgramBuilder.kt
@@ -0,0 +1,105 @@
+/*
+ *  Copyright 2022 UnitTestBot contributors (utbot.org)
+ * <p>
+ *  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
+ * <p>
+ *  http://www.apache.org/licenses/LICENSE-2.0
+ * <p>
+ *  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.
+ */
+
+@file:Suppress("UnusedReceiverParameter")
+
+package org.jacodb.ets.dsl
+
+interface ProgramBuilder {
+    fun assign(target: Local, expr: Expr)
+    fun ret(expr: Expr)
+    fun ifStmt(condition: Expr, block: IfBuilder.() -> Unit)
+    fun nop()
+    fun label(name: String)
+    fun goto(label: String)
+}
+
+fun ProgramBuilder.local(name: String): Local = Local(name)
+fun ProgramBuilder.param(index: Int): Parameter = Parameter(index)
+fun ProgramBuilder.thisRef(): Expr = ThisRef
+fun ProgramBuilder.const(value: Double): Constant = Constant(value)
+
+fun ProgramBuilder.and(left: Expr, right: Expr): Expr = BinaryExpr(BinaryOperator.AND, left, right)
+fun ProgramBuilder.or(left: Expr, right: Expr): Expr = BinaryExpr(BinaryOperator.OR, left, right)
+fun ProgramBuilder.eq(left: Expr, right: Expr): Expr = BinaryExpr(BinaryOperator.EQ, left, right)
+fun ProgramBuilder.neq(left: Expr, right: Expr): Expr = BinaryExpr(BinaryOperator.NEQ, left, right)
+fun ProgramBuilder.lt(left: Expr, right: Expr): Expr = BinaryExpr(BinaryOperator.LT, left, right)
+fun ProgramBuilder.leq(left: Expr, right: Expr): Expr = BinaryExpr(BinaryOperator.LTE, left, right)
+fun ProgramBuilder.gt(left: Expr, right: Expr): Expr = BinaryExpr(BinaryOperator.GT, left, right)
+fun ProgramBuilder.geq(left: Expr, right: Expr): Expr = BinaryExpr(BinaryOperator.GTE, left, right)
+fun ProgramBuilder.add(left: Expr, right: Expr): Expr = BinaryExpr(BinaryOperator.ADD, left, right)
+fun ProgramBuilder.sub(left: Expr, right: Expr): Expr = BinaryExpr(BinaryOperator.SUB, left, right)
+fun ProgramBuilder.mul(left: Expr, right: Expr): Expr = BinaryExpr(BinaryOperator.MUL, left, right)
+fun ProgramBuilder.div(left: Expr, right: Expr): Expr = BinaryExpr(BinaryOperator.DIV, left, right)
+
+fun ProgramBuilder.not(expr: Expr): Expr = UnaryExpr(UnaryOperator.NOT, expr)
+fun ProgramBuilder.neg(expr: Expr): Expr = UnaryExpr(UnaryOperator.NEG, expr)
+
+class ProgramBuilderImpl : ProgramBuilder {
+    private val _nodes: MutableList<Node> = mutableListOf()
+    val nodes: List<Node> get() = _nodes
+
+    fun build(): Program {
+        return Program(nodes)
+    }
+
+    override fun nop() {
+        _nodes += Nop
+    }
+
+    override fun label(name: String) {
+        _nodes += Label(name)
+    }
+
+    override fun goto(label: String) {
+        _nodes += Goto(label)
+    }
+
+    override fun ret(expr: Expr) {
+        _nodes += Return(expr)
+    }
+
+    override fun assign(target: Local, expr: Expr) {
+        _nodes += Assign(target, expr)
+    }
+
+    override fun ifStmt(condition: Expr, block: IfBuilder.() -> Unit) {
+        val builder = IfBuilder().apply(block)
+        _nodes += If(condition, builder.thenNodes, builder.elseNodes)
+    }
+}
+
+class IfBuilder : ProgramBuilder {
+    private val thenBuilder = ProgramBuilderImpl()
+    private val elseBuilder = ProgramBuilderImpl()
+    private var elseEntered = false
+
+    val thenNodes: List<Node> get() = thenBuilder.nodes
+    val elseNodes: List<Node> get() = elseBuilder.nodes
+
+    fun `else`(block: ProgramBuilder.() -> Unit) {
+        check(!elseEntered) { "Multiple else branches" }
+        elseEntered = true
+        elseBuilder.apply(block)
+    }
+
+    override fun assign(target: Local, expr: Expr) = thenBuilder.assign(target, expr)
+    override fun ifStmt(condition: Expr, block: IfBuilder.() -> Unit) = thenBuilder.ifStmt(condition, block)
+    override fun ret(expr: Expr) = thenBuilder.ret(expr)
+    override fun nop() = thenBuilder.nop()
+    override fun goto(label: String) = thenBuilder.goto(label)
+    override fun label(name: String) = thenBuilder.label(name)
+}
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
new file mode 100644
index 000000000..145857b39
--- /dev/null
+++ b/jacodb-ets/src/main/kotlin/org/jacodb/ets/dsl/Stmt.kt
@@ -0,0 +1,43 @@
+/*
+ *  Copyright 2022 UnitTestBot contributors (utbot.org)
+ * <p>
+ *  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
+ * <p>
+ *  http://www.apache.org/licenses/LICENSE-2.0
+ * <p>
+ *  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 org.jacodb.ets.dsl
+
+typealias StmtLocation = Int
+
+sealed interface Stmt {
+    val location: StmtLocation
+}
+
+data class NopStmt(
+    override val location: StmtLocation,
+) : Stmt
+
+data class AssignStmt(
+    override val location: StmtLocation,
+    val target: Local,
+    val expr: Expr,
+) : Stmt
+
+data class ReturnStmt(
+    override val location: StmtLocation,
+    val expr: Expr,
+) : Stmt
+
+data class IfStmt(
+    override val location: StmtLocation,
+    val condition: Expr,
+) : 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
new file mode 100644
index 000000000..8e04506b3
--- /dev/null
+++ b/jacodb-ets/src/main/kotlin/org/jacodb/ets/dsl/ToDot.kt
@@ -0,0 +1,181 @@
+/*
+ *  Copyright 2022 UnitTestBot contributors (utbot.org)
+ * <p>
+ *  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
+ * <p>
+ *  http://www.apache.org/licenses/LICENSE-2.0
+ * <p>
+ *  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 org.jacodb.ets.dsl
+
+import java.util.IdentityHashMap
+
+private fun Node.toDotLabel() = when (this) {
+    is Assign -> "$target := $expr"
+    is Return -> "return $expr"
+    is If -> "if ($condition)"
+    is Nop -> "nop"
+    is Label -> "label $name"
+    is Goto -> "goto $targetLabel"
+}
+
+fun Program.toDot(): String {
+    val lines = mutableListOf<String>()
+    lines += "digraph cfg {"
+    lines += "  node [shape=rect fontname=\"monospace\"]"
+
+    val labelMap: MutableMap<String, Label> = hashMapOf()
+    val nodeToId: MutableMap<Node, Int> = IdentityHashMap()
+    var freeId = 0
+
+    fun processForNodes(nodes: List<Node>) {
+        for (node in nodes) {
+            val id = nodeToId.computeIfAbsent(node) { freeId++ }
+            lines += "  $id [label=\"${node.toDotLabel()}\"]"
+            if (node is If) {
+                processForNodes(node.thenBranch)
+                processForNodes(node.elseBranch)
+            }
+            if (node is Label) {
+                check(node.name !in labelMap) { "Duplicate label: ${node.name}" }
+                labelMap[node.name] = node
+            }
+        }
+    }
+
+    processForNodes(nodes)
+
+    fun processForEdges(nodes: List<Node>) {
+        for (node in nodes) {
+            val id = nodeToId[node] ?: error("No ID for $node")
+            when (node) {
+                is If -> {
+                    if (node.thenBranch.isNotEmpty()) {
+                        val thenNode = node.thenBranch.first()
+                        val thenId = nodeToId[thenNode] ?: error("No ID for $thenNode")
+                        lines += "  $id -> $thenId [label=\"true\"]"
+                        processForEdges(node.thenBranch)
+                    }
+                    if (node.elseBranch.isNotEmpty()) {
+                        val elseNode = node.elseBranch.first()
+                        val elseId = nodeToId[elseNode] ?: error("No ID for $elseNode")
+                        lines += "  $id -> $elseId [label=\"false\"]"
+                        processForEdges(node.elseBranch)
+                    }
+                }
+
+                is Goto -> {
+                    val labelNode = labelMap[node.targetLabel] ?: error("Unknown label: ${node.targetLabel}")
+                    val labelId = nodeToId[labelNode] ?: error("No ID for $labelNode")
+                    lines += "  $id -> $labelId"
+                }
+
+                else -> {
+                    // See below.
+                }
+            }
+        }
+
+        for ((cur, next) in nodes.zipWithNext()) {
+            val curId = nodeToId[cur] ?: error("No ID for $cur")
+            val nextId = nodeToId[next] ?: error("No ID for $next")
+            lines += "  $curId -> $nextId"
+        }
+    }
+    processForEdges(nodes)
+
+    lines += "}"
+    return lines.joinToString("\n")
+}
+
+private fun BlockStmt.toDotLabel() = when (this) {
+    is BlockAssign -> "$target := $expr"
+    is BlockReturn -> "return $expr"
+    is BlockIf -> "if ($condition)"
+    is BlockNop -> "nop"
+}
+
+fun BlockCfg.toDot(): String {
+    val lines = mutableListOf<String>()
+    lines += "digraph cfg {"
+    lines += "  node [shape=rect fontname=\"monospace\"]"
+
+    // Nodes
+    for (block in blocks) {
+        val s = block.statements.joinToString("") { it.toDotLabel() + "\\l" }
+        lines += "  ${block.id} [label=\"Block #${block.id}\\n${s}\"]"
+    }
+
+    // Edges
+    for (block in blocks) {
+        val succs = successors[block.id] ?: error("No successors for block ${block.id}")
+        if (succs.isEmpty()) continue
+        if (succs.size == 1) {
+            lines += "  ${block.id} -> ${succs.single()}"
+        } else {
+            check(succs.size == 2)
+            val (trueBranch, falseBranch) = succs // Note the order of successors: (true, false) branches
+            lines += "  ${block.id} -> $trueBranch [label=\"true\"]"
+            lines += "  ${block.id} -> $falseBranch [label=\"false\"]"
+        }
+    }
+
+    lines += "}"
+    return lines.joinToString("\n")
+}
+
+private fun Stmt.toDotLabel() = when (this) {
+    is NopStmt -> "nop"
+    is AssignStmt -> "$target := $expr"
+    is ReturnStmt -> "return $expr"
+    is IfStmt -> "if ($condition)"
+}
+
+fun LinearizedCfg.toDot(): String {
+    val lines = mutableListOf<String>()
+    lines += "digraph cfg {"
+    lines += "  node [shape=rect fontname=\"monospace\"]"
+
+    // Nodes
+    for (stmt in statements) {
+        val id = stmt.location
+        lines += "  $id [label=\"$id: ${stmt.toDotLabel()}\"]"
+    }
+
+    // Edges
+    for (stmt in statements) {
+        when (stmt) {
+            is IfStmt -> {
+                val succs = successors[stmt.location] ?: error("No successors for $stmt")
+                check(succs.size == 2) {
+                    "Expected two successors for $stmt, but it has ${succs.size}: $succs"
+                }
+                val (thenBranch, elseBranch) = succs
+                lines += "  ${stmt.location} -> $thenBranch [label=\"then\"]"
+                lines += "  ${stmt.location} -> $elseBranch [label=\"else\"]"
+            }
+
+            else -> {
+                val succs = successors[stmt.location] ?: error("No successors for $stmt")
+                if (succs.isNotEmpty()) {
+                    check(succs.size == 1) {
+                        "Expected one successor for $stmt, but it has ${succs.size}: $succs"
+                    }
+                    val target = succs.single()
+                    lines += "  ${stmt.location} -> $target"
+                }
+            }
+        }
+    }
+
+    lines += "}"
+    return lines.joinToString("\n")
+}
diff --git a/jacodb-ets/src/main/kotlin/org/jacodb/ets/graph/CfgDsl.kt b/jacodb-ets/src/main/kotlin/org/jacodb/ets/graph/CfgDsl.kt
deleted file mode 100644
index c5582426f..000000000
--- a/jacodb-ets/src/main/kotlin/org/jacodb/ets/graph/CfgDsl.kt
+++ /dev/null
@@ -1,691 +0,0 @@
-/*
- *  Copyright 2022 UnitTestBot contributors (utbot.org)
- * <p>
- *  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
- * <p>
- *  http://www.apache.org/licenses/LICENSE-2.0
- * <p>
- *  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.
- */
-
-@file:Suppress("UnusedReceiverParameter")
-
-package org.jacodb.ets.graph
-
-import org.jacodb.ets.utils.view
-import java.util.IdentityHashMap
-
-sealed interface Expr
-
-data class Local(val name: String) : Expr {
-    override fun toString() = name
-}
-
-data class Parameter(val index: Int) : Expr {
-    override fun toString() = "param($index)"
-}
-
-object ThisRef : Expr {
-    override fun toString() = "this"
-}
-
-data class Constant(val value: Double) : Expr {
-    override fun toString() = "const($value)"
-}
-
-enum class BinaryOperator {
-    AND, OR,
-    EQ, NEQ, LT, LTE, GT, GTE,
-    ADD, SUB, MUL, DIV
-}
-
-data class BinaryExpr(
-    val operator: BinaryOperator,
-    val left: Expr,
-    val right: Expr,
-) : Expr {
-    override fun toString() = "${operator.name.lowercase()}($left, $right)"
-}
-
-enum class UnaryOperator { NOT, NEG }
-
-data class UnaryExpr(
-    val operator: UnaryOperator,
-    val expr: Expr,
-) : Expr {
-    override fun toString() = "${operator.name.lowercase()}($expr)"
-}
-
-sealed interface ProgramNode
-
-data object ProgramNop : ProgramNode
-
-data class ProgramAssign(
-    val target: Local,
-    val expr: Expr,
-) : ProgramNode
-
-data class ProgramReturn(
-    val expr: Expr,
-) : ProgramNode
-
-data class ProgramIf(
-    val condition: Expr,
-    val thenBranch: List<ProgramNode>,
-    val elseBranch: List<ProgramNode>,
-) : ProgramNode
-
-data class ProgramLabel(
-    val name: String,
-) : ProgramNode
-
-data class ProgramGoto(
-    val targetLabel: String,
-) : ProgramNode
-
-data class Program(
-    val nodes: List<ProgramNode>,
-) {
-    fun toText(indent: Int = 2): String {
-        val lines = mutableListOf<String>()
-
-        fun process(nodes: List<ProgramNode>, currentIndent: Int = 0) {
-            fun line(line: String) {
-                lines += " ".repeat(currentIndent) + line
-            }
-
-            for (node in nodes) {
-                when (node) {
-                    is ProgramNop -> line("nop")
-                    is ProgramAssign -> line("${node.target} := ${node.expr}")
-                    is ProgramReturn -> line("return ${node.expr}")
-                    is ProgramIf -> {
-                        line("if (${node.condition}) {")
-                        process(node.thenBranch, currentIndent + indent)
-                        if (node.elseBranch.isNotEmpty()) {
-                            line("} else {")
-                            process(node.elseBranch, currentIndent + indent)
-                        }
-                        line("}")
-                    }
-
-                    is ProgramLabel -> line("label ${node.name}")
-                    is ProgramGoto -> line("goto ${node.targetLabel}")
-                }
-            }
-        }
-
-        process(nodes)
-
-        return lines.joinToString("\n")
-    }
-}
-
-fun program(block: ProgramBuilder.() -> Unit): Program {
-    val builder = ProgramBuilderImpl()
-    builder.block()
-    return builder.build()
-}
-
-interface ProgramBuilder {
-    fun assign(target: Local, expr: Expr)
-    fun ret(expr: Expr)
-    fun ifStmt(condition: Expr, block: IfBuilder.() -> Unit)
-    fun nop()
-    fun label(name: String)
-    fun goto(label: String)
-}
-
-fun ProgramBuilder.local(name: String): Local = Local(name)
-fun ProgramBuilder.param(index: Int): Parameter = Parameter(index)
-fun ProgramBuilder.thisRef(): Expr = ThisRef
-fun ProgramBuilder.const(value: Double): Constant = Constant(value)
-
-fun ProgramBuilder.and(left: Expr, right: Expr): Expr = BinaryExpr(BinaryOperator.AND, left, right)
-fun ProgramBuilder.or(left: Expr, right: Expr): Expr = BinaryExpr(BinaryOperator.OR, left, right)
-fun ProgramBuilder.eq(left: Expr, right: Expr): Expr = BinaryExpr(BinaryOperator.EQ, left, right)
-fun ProgramBuilder.neq(left: Expr, right: Expr): Expr = BinaryExpr(BinaryOperator.NEQ, left, right)
-fun ProgramBuilder.lt(left: Expr, right: Expr): Expr = BinaryExpr(BinaryOperator.LT, left, right)
-fun ProgramBuilder.leq(left: Expr, right: Expr): Expr = BinaryExpr(BinaryOperator.LTE, left, right)
-fun ProgramBuilder.gt(left: Expr, right: Expr): Expr = BinaryExpr(BinaryOperator.GT, left, right)
-fun ProgramBuilder.geq(left: Expr, right: Expr): Expr = BinaryExpr(BinaryOperator.GTE, left, right)
-fun ProgramBuilder.add(left: Expr, right: Expr): Expr = BinaryExpr(BinaryOperator.ADD, left, right)
-fun ProgramBuilder.sub(left: Expr, right: Expr): Expr = BinaryExpr(BinaryOperator.SUB, left, right)
-fun ProgramBuilder.mul(left: Expr, right: Expr): Expr = BinaryExpr(BinaryOperator.MUL, left, right)
-fun ProgramBuilder.div(left: Expr, right: Expr): Expr = BinaryExpr(BinaryOperator.DIV, left, right)
-
-fun ProgramBuilder.not(expr: Expr): Expr = UnaryExpr(UnaryOperator.NOT, expr)
-fun ProgramBuilder.neg(expr: Expr): Expr = UnaryExpr(UnaryOperator.NEG, expr)
-
-class ProgramBuilderImpl : ProgramBuilder {
-    private val _nodes: MutableList<ProgramNode> = mutableListOf()
-    val nodes: List<ProgramNode> get() = _nodes
-
-    fun build(): Program {
-        return Program(nodes)
-    }
-
-    override fun nop() {
-        _nodes += ProgramNop
-    }
-
-    override fun label(name: String) {
-        _nodes += ProgramLabel(name)
-    }
-
-    override fun goto(label: String) {
-        _nodes += ProgramGoto(label)
-    }
-
-    override fun ret(expr: Expr) {
-        _nodes += ProgramReturn(expr)
-    }
-
-    override fun assign(target: Local, expr: Expr) {
-        _nodes += ProgramAssign(target, expr)
-    }
-
-    override fun ifStmt(condition: Expr, block: IfBuilder.() -> Unit) {
-        val builder = IfBuilder().apply(block)
-        _nodes += ProgramIf(condition, builder.thenNodes, builder.elseNodes)
-    }
-}
-
-class IfBuilder : ProgramBuilder {
-    private val thenBuilder = ProgramBuilderImpl()
-    private val elseBuilder = ProgramBuilderImpl()
-    private var elseEntered = false
-
-    val thenNodes: List<ProgramNode> get() = thenBuilder.nodes
-    val elseNodes: List<ProgramNode> get() = elseBuilder.nodes
-
-    fun `else`(block: ProgramBuilder.() -> Unit) {
-        check(!elseEntered) { "Multiple else branches" }
-        elseEntered = true
-        elseBuilder.apply(block)
-    }
-
-    override fun assign(target: Local, expr: Expr) = thenBuilder.assign(target, expr)
-    override fun ifStmt(condition: Expr, block: IfBuilder.() -> Unit) = thenBuilder.ifStmt(condition, block)
-    override fun ret(expr: Expr) = thenBuilder.ret(expr)
-    override fun nop() = thenBuilder.nop()
-    override fun goto(label: String) = thenBuilder.goto(label)
-    override fun label(name: String) = thenBuilder.label(name)
-}
-
-private fun ProgramNode.toDotLabel() = when (this) {
-    is ProgramAssign -> "$target := $expr"
-    is ProgramReturn -> "return $expr"
-    is ProgramIf -> "if ($condition)"
-    is ProgramNop -> "nop"
-    is ProgramLabel -> "label $name"
-    is ProgramGoto -> "goto $targetLabel"
-}
-
-fun Program.toDot(): String {
-    val lines = mutableListOf<String>()
-    lines += "digraph cfg {"
-    lines += "  node [shape=rect fontname=\"monospace\"]"
-
-    val labelMap: MutableMap<String, ProgramLabel> = hashMapOf()
-    val nodeToId: MutableMap<ProgramNode, Int> = IdentityHashMap()
-    var freeId = 0
-
-    fun processForNodes(nodes: List<ProgramNode>) {
-        for (node in nodes) {
-            val id = nodeToId.computeIfAbsent(node) { freeId++ }
-            lines += "  $id [label=\"${node.toDotLabel()}\"]"
-            if (node is ProgramIf) {
-                processForNodes(node.thenBranch)
-                processForNodes(node.elseBranch)
-            }
-            if (node is ProgramLabel) {
-                check(node.name !in labelMap) { "Duplicate label: ${node.name}" }
-                labelMap[node.name] = node
-            }
-        }
-    }
-
-    processForNodes(nodes)
-
-    fun processForEdges(nodes: List<ProgramNode>) {
-        for (node in nodes) {
-            val id = nodeToId[node] ?: error("No ID for $node")
-            when (node) {
-                is ProgramIf -> {
-                    if (node.thenBranch.isNotEmpty()) {
-                        val thenNode = node.thenBranch.first()
-                        val thenId = nodeToId[thenNode] ?: error("No ID for $thenNode")
-                        lines += "  $id -> $thenId [label=\"true\"]"
-                        processForEdges(node.thenBranch)
-                    }
-                    if (node.elseBranch.isNotEmpty()) {
-                        val elseNode = node.elseBranch.first()
-                        val elseId = nodeToId[elseNode] ?: error("No ID for $elseNode")
-                        lines += "  $id -> $elseId [label=\"false\"]"
-                        processForEdges(node.elseBranch)
-                    }
-                }
-
-                is ProgramGoto -> {
-                    val labelNode = labelMap[node.targetLabel] ?: error("Unknown label: ${node.targetLabel}")
-                    val labelId = nodeToId[labelNode] ?: error("No ID for $labelNode")
-                    lines += "  $id -> $labelId"
-                }
-
-                else -> {
-                    // See below.
-                }
-            }
-        }
-
-        for ((cur, next) in nodes.zipWithNext()) {
-            val curId = nodeToId[cur] ?: error("No ID for $cur")
-            val nextId = nodeToId[next] ?: error("No ID for $next")
-            lines += "  $curId -> $nextId"
-        }
-    }
-    processForEdges(nodes)
-
-    lines += "}"
-    return lines.joinToString("\n")
-}
-
-//----- CFG -----
-
-sealed interface BlockStmt
-// TODO: merge BlockStmt and Stmt (add location to BlockStmt, initialize with -1)
-
-data object BlockNop : BlockStmt
-
-data class BlockAssign(
-    val target: Local,
-    val expr: Expr,
-) : BlockStmt
-
-data class BlockReturn(
-    val expr: Expr,
-) : BlockStmt
-
-data class BlockIf(
-    val condition: Expr,
-) : BlockStmt
-
-data class Block(
-    val id: Int,
-    val statements: List<BlockStmt>,
-)
-
-data class BlockCfg(
-    val blocks: List<Block>,
-    val successors: Map<Int, List<Int>>,
-)
-
-fun Program.toBlockCfg(): BlockCfg {
-    val labelToNode: MutableMap<String, ProgramNode> = hashMapOf()
-    val targets: MutableSet<ProgramNode> = hashSetOf()
-
-    fun findLabels(nodes: List<ProgramNode>) {
-        if (nodes.lastOrNull() is ProgramLabel) {
-            error("Label at the end of the block: $nodes")
-        }
-        for ((stmt, next) in nodes.zipWithNext()) {
-            if (stmt is ProgramLabel) {
-                check(next !is ProgramLabel) { "Two labels in a row: $stmt, $next" }
-                check(next !is ProgramGoto) { "Label followed by goto: $stmt, $next" }
-                check(stmt.name !in labelToNode) { "Duplicate label: ${stmt.name}" }
-                labelToNode[stmt.name] = next
-            }
-        }
-        for (node in nodes) {
-            if (node is ProgramIf) {
-                findLabels(node.thenBranch)
-                findLabels(node.elseBranch)
-            }
-            if (node is ProgramGoto) {
-                targets += labelToNode[node.targetLabel] ?: error("Unknown label: ${node.targetLabel}")
-            }
-        }
-    }
-
-    findLabels(nodes)
-
-    val blocks: MutableList<Block> = mutableListOf()
-    val successors: MutableMap<Int, List<Int>> = hashMapOf()
-    val stmtToBlock: MutableMap<BlockStmt, Int> = IdentityHashMap()
-    val nodeToStmt: MutableMap<ProgramNode, BlockStmt> = IdentityHashMap()
-
-    fun buildBlocks(nodes: List<ProgramNode>): Pair<Int, Int>? {
-        if (nodes.isEmpty()) return null
-
-        lateinit var currentBlock: MutableList<BlockStmt>
-
-        fun newBlock(): Block {
-            currentBlock = mutableListOf()
-            val block = Block(blocks.size, currentBlock)
-            blocks += block
-            return block
-        }
-
-        var block = newBlock()
-        val firstBlockId = block.id
-
-        for (node in nodes) {
-            if (node is ProgramLabel) continue
-
-            if (node in targets && currentBlock.isNotEmpty()) {
-                block.statements.forEach { stmtToBlock[it] = block.id }
-                val prevBlock = block
-                block = newBlock()
-                successors[prevBlock.id] = listOf(block.id)
-            }
-
-            if (node !is ProgramGoto) {
-                val stmt = when (node) {
-                    ProgramNop -> BlockNop
-                    is ProgramAssign -> BlockAssign(node.target, node.expr)
-                    is ProgramReturn -> BlockReturn(node.expr)
-                    is ProgramIf -> BlockIf(node.condition)
-                    else -> error("Unexpected node: $node")
-                }
-                nodeToStmt[node] = stmt
-                currentBlock += stmt
-            }
-
-            if (node is ProgramIf) {
-                block.statements.forEach { stmtToBlock[it] = block.id }
-                val ifBlock = block
-                block = newBlock()
-
-                val thenBlocks = buildBlocks(node.thenBranch)
-                val elseBlocks = buildBlocks(node.elseBranch)
-
-                when {
-                    thenBlocks != null && elseBlocks != null -> {
-                        val (thenStart, thenEnd) = thenBlocks
-                        val (elseStart, elseEnd) = elseBlocks
-                        successors[ifBlock.id] = listOf(thenStart, elseStart) // (true, false) branches
-                        when (blocks[thenEnd].statements.lastOrNull()) {
-                            is BlockReturn -> {}
-                            is BlockIf -> error("Unexpected if statement at the end of the block")
-                            else -> successors[thenEnd] = listOf(block.id)
-                        }
-                        when (blocks[elseEnd].statements.lastOrNull()) {
-                            is BlockReturn -> {}
-                            is BlockIf -> error("Unexpected if statement at the end of the block")
-                            else -> successors[elseEnd] = listOf(block.id)
-                        }
-                    }
-
-                    thenBlocks != null -> {
-                        val (thenStart, thenEnd) = thenBlocks
-                        successors[ifBlock.id] = listOf(thenStart, block.id) // (true, false) branches
-                        when (blocks[thenEnd].statements.lastOrNull()) {
-                            is BlockReturn -> {}
-                            is BlockIf -> error("Unexpected if statement at the end of the block")
-                            else -> successors[thenEnd] = listOf(block.id)
-                        }
-                    }
-
-                    elseBlocks != null -> {
-                        val (elseStart, elseEnd) = elseBlocks
-                        successors[ifBlock.id] = listOf(block.id, elseStart) // (true, false) branches
-                        when (blocks[elseEnd].statements.lastOrNull()) {
-                            is BlockReturn -> {}
-                            is BlockIf -> error("Unexpected if statement at the end of the block")
-                            else -> successors[elseEnd] = listOf(block.id)
-                        }
-                    }
-
-                    else -> {
-                        successors[ifBlock.id] = listOf(block.id)
-                    }
-                }
-            } else if (node is ProgramGoto) {
-                val targetNode = labelToNode[node.targetLabel] ?: error("Unknown label: ${node.targetLabel}")
-                val target = nodeToStmt[targetNode] ?: error("No statement for $targetNode")
-                val targetBlockId = stmtToBlock[target] ?: error("No block for $target")
-                successors[block.id] = listOf(targetBlockId)
-                block.statements.forEach { stmtToBlock[it] = block.id }
-                block = newBlock()
-            } else if (node is ProgramReturn) {
-                successors[block.id] = emptyList()
-                break
-            }
-        }
-
-        block.statements.forEach { stmtToBlock[it] = block.id }
-        val lastBlockId = block.id
-
-        return Pair(firstBlockId, lastBlockId)
-    }
-
-    buildBlocks(nodes)
-
-    return BlockCfg(blocks, successors)
-}
-
-private fun BlockStmt.toDotLabel() = when (this) {
-    is BlockAssign -> "$target := $expr"
-    is BlockReturn -> "return $expr"
-    is BlockIf -> "if ($condition)"
-    is BlockNop -> "nop"
-}
-
-fun BlockCfg.toDot(): String {
-    val lines = mutableListOf<String>()
-    lines += "digraph cfg {"
-    lines += "  node [shape=rect fontname=\"monospace\"]"
-
-    // Nodes
-    for (block in blocks) {
-        val s = block.statements.joinToString("") { it.toDotLabel() + "\\l" }
-        lines += "  ${block.id} [label=\"Block #\\N\\n${s}\"]"
-    }
-
-    // Edges
-    for (block in blocks) {
-        val succs = successors[block.id] ?: error("No successors for block ${block.id}")
-        if (succs.isEmpty()) continue
-        if (succs.size == 1) {
-            lines += "  ${block.id} -> ${succs.single()}"
-        } else {
-            check(succs.size == 2)
-            val (trueBranch, falseBranch) = succs // Note the order of successors: (true, false) branches
-            lines += "  ${block.id} -> $trueBranch [label=\"true\"]"
-            lines += "  ${block.id} -> $falseBranch [label=\"false\"]"
-        }
-    }
-
-    lines += "}"
-    return lines.joinToString("\n")
-}
-
-typealias StmtLocation = Int
-
-sealed interface Stmt {
-    val location: StmtLocation
-}
-
-data class NopStmt(
-    override val location: StmtLocation,
-) : Stmt
-
-data class AssignStmt(
-    override val location: StmtLocation,
-    val target: Local,
-    val expr: Expr,
-) : Stmt
-
-data class ReturnStmt(
-    override val location: StmtLocation,
-    val expr: Expr,
-) : Stmt
-
-data class IfStmt(
-    override val location: StmtLocation,
-    val condition: Expr,
-) : Stmt
-
-data class LinearizedCfg(
-    val statements: List<Stmt>,
-    val successors: Map<StmtLocation, List<StmtLocation>>,
-)
-
-fun BlockCfg.linearize(): LinearizedCfg {
-    val linearized: MutableList<Stmt> = mutableListOf()
-    val successors: MutableMap<StmtLocation, List<StmtLocation>> = hashMapOf()
-
-    fun process(statements: List<BlockStmt>): List<Stmt> {
-        val processed: MutableList<Stmt> = mutableListOf()
-        var loc = linearized.size
-        for (stmt in statements) {
-            when (stmt) {
-                is BlockNop -> {
-                    // Note: ignore NOP statements
-                    // processed += NopStmt(loc++)
-                }
-
-                is BlockAssign -> {
-                    // TODO: three-address code
-                    processed += AssignStmt(loc++, stmt.target, stmt.expr)
-                }
-
-                is BlockReturn -> {
-                    // TODO: three-address code
-                    processed += ReturnStmt(loc++, stmt.expr)
-                }
-
-                is BlockIf -> {
-                    // TODO: three-address code
-                    processed += IfStmt(loc++, stmt.condition)
-                }
-            }
-        }
-        if (processed.isEmpty()) {
-            processed += NopStmt(loc++)
-        }
-        linearized += processed
-        check(linearized.size == loc)
-        return processed
-    }
-
-    val linearizedBlocks = blocks.associate { it.id to process(it.statements) }
-
-    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 IfStmt) { "If statement in the middle of the block: $stmt" }
-            successors[stmt.location] = listOf(next.location)
-        }
-        if (statements.isNotEmpty()) {
-            val last = statements.last()
-            val nextBlocks = this@linearize.successors[id] ?: error("No successors for block $id")
-            // TODO: handle empty blocks (next)
-            successors[last.location] = nextBlocks.map { linearizedBlocks.getValue(it).first().location }
-        }
-    }
-
-    return LinearizedCfg(linearized, successors)
-}
-
-private fun Stmt.toDotLabel() = when (this) {
-    is NopStmt -> "nop"
-    is AssignStmt -> "$target := $expr"
-    is ReturnStmt -> "return $expr"
-    is IfStmt -> "if ($condition)"
-}
-
-fun LinearizedCfg.toDot(): String {
-    val lines = mutableListOf<String>()
-    lines += "digraph cfg {"
-    lines += "  node [shape=rect fontname=\"monospace\"]"
-
-    // Nodes
-    for (stmt in statements) {
-        lines += "  ${stmt.location} [label=\"\\N: ${stmt.toDotLabel()}\"]"
-    }
-
-    // Edges
-    for (stmt in statements) {
-        when (stmt) {
-            is IfStmt -> {
-                val succs = successors[stmt.location] ?: error("No successors for $stmt")
-                check(succs.size == 2) {
-                    "Expected two successors for $stmt, but it has ${succs.size}: $succs"
-                }
-                val (thenBranch, elseBranch) = succs
-                lines += "  ${stmt.location} -> $thenBranch [label=\"then\"]"
-                lines += "  ${stmt.location} -> $elseBranch [label=\"else\"]"
-            }
-
-            else -> {
-                val succs = successors[stmt.location] ?: error("No successors for $stmt")
-                if (succs.isNotEmpty()) {
-                    check(succs.size == 1) {
-                        "Expected one successor for $stmt, but it has ${succs.size}: $succs"
-                    }
-                    val target = succs.single()
-                    lines += "  ${stmt.location} -> $target"
-                }
-            }
-        }
-    }
-
-    lines += "}"
-    return lines.joinToString("\n")
-}
-
-private fun main() {
-    val prog = program {
-        assign(local("i"), param(0))
-
-        ifStmt(gt(local("i"), const(10.0))) {
-            ifStmt(eq(local("i"), const(42.0))) {
-                ret(local("i"))
-                `else` {
-                    assign(local("i"), const(10.0))
-                }
-            }
-            nop()
-        }
-
-        label("loop")
-        ifStmt(gt(local("i"), const(0.0))) {
-            assign(local("i"), sub(local("i"), const(1.0)))
-            goto("loop")
-            `else` {
-                ret(local("i"))
-            }
-        }
-
-        ret(const(42.0)) // unreachable
-    }
-
-    val doView = false
-
-    println("PROGRAM:")
-    println("-----")
-    println(prog.toText())
-    println("-----")
-
-    println("=== PROGRAM:")
-    println(prog.toDot())
-    if (doView) view(prog.toDot(), name = "program")
-
-    val blockCfg = prog.toBlockCfg()
-    println("=== BLOCK CFG:")
-    println(blockCfg.toDot())
-    if (doView) view(blockCfg.toDot(), name = "block")
-
-    val linearCfg = blockCfg.linearize()
-    println("=== LINEARIZED CFG:")
-    println(linearCfg.toDot())
-    if (doView) view(linearCfg.toDot(), name = "linear")
-}
diff --git a/jacodb-ets/src/main/kotlin/org/jacodb/ets/graph/EtsBlockCfg.kt b/jacodb-ets/src/main/kotlin/org/jacodb/ets/graph/EtsBlockCfg.kt
index 93c7cb320..59f6f578f 100644
--- a/jacodb-ets/src/main/kotlin/org/jacodb/ets/graph/EtsBlockCfg.kt
+++ b/jacodb-ets/src/main/kotlin/org/jacodb/ets/graph/EtsBlockCfg.kt
@@ -45,6 +45,28 @@ import org.jacodb.ets.base.EtsThis
 import org.jacodb.ets.base.EtsType
 import org.jacodb.ets.base.EtsUnknownType
 import org.jacodb.ets.base.EtsValue
+import org.jacodb.ets.dsl.BinaryExpr
+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.BlockIf
+import org.jacodb.ets.dsl.BlockNop
+import org.jacodb.ets.dsl.BlockReturn
+import org.jacodb.ets.dsl.Constant
+import org.jacodb.ets.dsl.Expr
+import org.jacodb.ets.dsl.Local
+import org.jacodb.ets.dsl.Parameter
+import org.jacodb.ets.dsl.ThisRef
+import org.jacodb.ets.dsl.UnaryExpr
+import org.jacodb.ets.dsl.UnaryOperator
+import org.jacodb.ets.dsl.add
+import org.jacodb.ets.dsl.and
+import org.jacodb.ets.dsl.const
+import org.jacodb.ets.dsl.local
+import org.jacodb.ets.dsl.param
+import org.jacodb.ets.dsl.program
+import org.jacodb.ets.dsl.toBlockCfg
 import org.jacodb.ets.model.EtsClassSignature
 import org.jacodb.ets.model.EtsMethod
 import org.jacodb.ets.model.EtsMethodImpl
@@ -100,7 +122,7 @@ class EtsBlockCfgBuilder(
 
         for (stmt in statements) {
             when (stmt) {
-                BlockNop -> {
+                org.jacodb.ets.dsl.BlockNop -> {
                     etsStatements += EtsNopStmt(location = stub)
                 }
 
diff --git a/jacodb-ets/src/main/kotlin/org/jacodb/ets/utils/IdentityHashSet.kt b/jacodb-ets/src/main/kotlin/org/jacodb/ets/utils/IdentityHashSet.kt
new file mode 100644
index 000000000..1688d4ca8
--- /dev/null
+++ b/jacodb-ets/src/main/kotlin/org/jacodb/ets/utils/IdentityHashSet.kt
@@ -0,0 +1,35 @@
+/*
+ *  Copyright 2022 UnitTestBot contributors (utbot.org)
+ * <p>
+ *  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
+ * <p>
+ *  http://www.apache.org/licenses/LICENSE-2.0
+ * <p>
+ *  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 org.jacodb.ets.utils
+
+import java.util.IdentityHashMap
+
+class IdentityHashSet <T>(
+    private val map: IdentityHashMap<T, Unit> = IdentityHashMap()
+) : AbstractMutableSet<T>() {
+
+    override val size: Int
+        get() = map.size
+
+    override fun add(element: T): Boolean {
+        return map.put(element, Unit) == null
+    }
+
+    override fun iterator(): MutableIterator<T> {
+        return map.keys.iterator()
+    }
+}
diff --git a/jacodb-ets/src/test/kotlin/org/jacodb/ets/test/EtsCfgDslTest.kt b/jacodb-ets/src/test/kotlin/org/jacodb/ets/test/EtsCfgDslTest.kt
index 4bd6e3e7f..4e9214e07 100644
--- a/jacodb-ets/src/test/kotlin/org/jacodb/ets/test/EtsCfgDslTest.kt
+++ b/jacodb-ets/src/test/kotlin/org/jacodb/ets/test/EtsCfgDslTest.kt
@@ -17,19 +17,19 @@
 package org.jacodb.ets.test
 
 import org.jacodb.ets.base.EtsAssignStmt
-import org.jacodb.ets.base.EtsBooleanType
 import org.jacodb.ets.base.EtsLocal
 import org.jacodb.ets.base.EtsNumberType
 import org.jacodb.ets.base.EtsUnknownType
 import org.jacodb.ets.graph.EtsBlockCfgBuilder
-import org.jacodb.ets.graph.add
-import org.jacodb.ets.graph.const
+import org.jacodb.ets.dsl.add
+import org.jacodb.ets.dsl.const
+import org.jacodb.ets.dsl.local
+import org.jacodb.ets.dsl.lt
+import org.jacodb.ets.dsl.param
+import org.jacodb.ets.dsl.program
+import org.jacodb.ets.dsl.toBlockCfg
+import org.jacodb.ets.dsl.toDot
 import org.jacodb.ets.graph.linearize
-import org.jacodb.ets.graph.local
-import org.jacodb.ets.graph.lt
-import org.jacodb.ets.graph.param
-import org.jacodb.ets.graph.program
-import org.jacodb.ets.graph.toBlockCfg
 import org.jacodb.ets.graph.toDot
 import org.jacodb.ets.model.EtsClassSignature
 import org.jacodb.ets.model.EtsFileSignature

From aa6c330936700d9c9d5dab213fe34eb964b4f836 Mon Sep 17 00:00:00 2001
From: Konstantin Chukharev <lipen00@gmail.com>
Date: Thu, 30 Jan 2025 18:29:43 +0300
Subject: [PATCH 13/16] Use id instead of \\N

---
 .../src/main/kotlin/org/jacodb/ets/graph/EtsBlockCfg.kt       | 4 ++--
 .../src/main/kotlin/org/jacodb/ets/utils/EtsCfgToDot.kt       | 3 ++-
 2 files changed, 4 insertions(+), 3 deletions(-)

diff --git a/jacodb-ets/src/main/kotlin/org/jacodb/ets/graph/EtsBlockCfg.kt b/jacodb-ets/src/main/kotlin/org/jacodb/ets/graph/EtsBlockCfg.kt
index 59f6f578f..8ed86969a 100644
--- a/jacodb-ets/src/main/kotlin/org/jacodb/ets/graph/EtsBlockCfg.kt
+++ b/jacodb-ets/src/main/kotlin/org/jacodb/ets/graph/EtsBlockCfg.kt
@@ -340,13 +340,13 @@ fun EtsBlockCfg.toDot(useHtml: Boolean = true): String {
                 it.toDotLabel().htmlEncode() + "<br/>"
             }
             val h = "<table border=\"0\" cellborder=\"1\" cellspacing=\"0\">" +
-                "<tr><td>" + "<b>Block #\\N</b>" + "</td></tr>" +
+                "<tr><td>" + "<b>Block #${block.id}</b>" + "</td></tr>" +
                 "<tr><td balign=\"left\">" + s + "</td></tr>" +
                 "</table>"
             lines += "  ${block.id} [label=<${h}>]"
         } else {
             val s = block.statements.joinToString("") { it.toDotLabel() + "\\l" }
-            lines += "  ${block.id} [label=\"Block #\\N\\n$s\"]"
+            lines += "  ${block.id} [label=\"Block #${block.id}\\n$s\"]"
         }
     }
 
diff --git a/jacodb-ets/src/main/kotlin/org/jacodb/ets/utils/EtsCfgToDot.kt b/jacodb-ets/src/main/kotlin/org/jacodb/ets/utils/EtsCfgToDot.kt
index e63394f04..18a4a6b80 100644
--- a/jacodb-ets/src/main/kotlin/org/jacodb/ets/utils/EtsCfgToDot.kt
+++ b/jacodb-ets/src/main/kotlin/org/jacodb/ets/utils/EtsCfgToDot.kt
@@ -38,7 +38,8 @@ fun EtsCfg.toDot(): String {
 
     // Nodes
     stmts.forEach { stmt ->
-        lines += "  ${stmt.location.index} [label=\"\\N: ${stmt.toDotLabel()}\"]"
+        val id= stmt.location.index
+        lines += "  $id [label=\"$id: ${stmt.toDotLabel()}\"]"
     }
 
     // Edges

From be1d35315d0db2733deda855e698b27322b1939c Mon Sep 17 00:00:00 2001
From: Konstantin Chukharev <lipen00@gmail.com>
Date: Fri, 31 Jan 2025 18:14:30 +0300
Subject: [PATCH 14/16] Add BlockCfg.toEtsBlockCfg extension

---
 .../src/main/kotlin/org/jacodb/ets/graph/EtsBlockCfg.kt     | 6 +++++-
 .../src/test/kotlin/org/jacodb/ets/test/EtsCfgDslTest.kt    | 4 ++--
 2 files changed, 7 insertions(+), 3 deletions(-)

diff --git a/jacodb-ets/src/main/kotlin/org/jacodb/ets/graph/EtsBlockCfg.kt b/jacodb-ets/src/main/kotlin/org/jacodb/ets/graph/EtsBlockCfg.kt
index 8ed86969a..e9c1edbd2 100644
--- a/jacodb-ets/src/main/kotlin/org/jacodb/ets/graph/EtsBlockCfg.kt
+++ b/jacodb-ets/src/main/kotlin/org/jacodb/ets/graph/EtsBlockCfg.kt
@@ -86,6 +86,10 @@ class EtsBlockCfg(
     val successors: Map<Int, List<Int>>, // for 'if-stmt' block, successors are (true, false) branches
 )
 
+fun BlockCfg.toEtsBlockCfg(method: EtsMethod): EtsBlockCfg {
+    return EtsBlockCfgBuilder(method).build(this)
+}
+
 class EtsBlockCfgBuilder(
     val method: EtsMethod,
 ) {
@@ -399,7 +403,7 @@ private fun main() {
         ret(const(0.0))
     }
     val blockCfg = p.toBlockCfg()
-    val etsBlockCfg = EtsBlockCfgBuilder(method).build(blockCfg)
+    val etsBlockCfg = blockCfg.toEtsBlockCfg(method)
     println(etsBlockCfg.toDot())
     view(etsBlockCfg.toDot(), name = "etsBlockCfg")
     val etsCfg = etsBlockCfg.linearize()
diff --git a/jacodb-ets/src/test/kotlin/org/jacodb/ets/test/EtsCfgDslTest.kt b/jacodb-ets/src/test/kotlin/org/jacodb/ets/test/EtsCfgDslTest.kt
index 4e9214e07..d410c083e 100644
--- a/jacodb-ets/src/test/kotlin/org/jacodb/ets/test/EtsCfgDslTest.kt
+++ b/jacodb-ets/src/test/kotlin/org/jacodb/ets/test/EtsCfgDslTest.kt
@@ -20,7 +20,6 @@ import org.jacodb.ets.base.EtsAssignStmt
 import org.jacodb.ets.base.EtsLocal
 import org.jacodb.ets.base.EtsNumberType
 import org.jacodb.ets.base.EtsUnknownType
-import org.jacodb.ets.graph.EtsBlockCfgBuilder
 import org.jacodb.ets.dsl.add
 import org.jacodb.ets.dsl.const
 import org.jacodb.ets.dsl.local
@@ -31,6 +30,7 @@ import org.jacodb.ets.dsl.toBlockCfg
 import org.jacodb.ets.dsl.toDot
 import org.jacodb.ets.graph.linearize
 import org.jacodb.ets.graph.toDot
+import org.jacodb.ets.graph.toEtsBlockCfg
 import org.jacodb.ets.model.EtsClassSignature
 import org.jacodb.ets.model.EtsFileSignature
 import org.jacodb.ets.model.EtsMethodImpl
@@ -79,7 +79,7 @@ class EtsCfgDslTest {
             locals = locals,
         )
 
-        val etsBlockCfg = EtsBlockCfgBuilder(method).build(blockCfg)
+        val etsBlockCfg = blockCfg.toEtsBlockCfg(method)
         println("etsBlockCfg:\n${etsBlockCfg.toDot()}")
         val etsCfg = etsBlockCfg.linearize()
         println("etsCfg:\n${etsCfg.toDot()}")

From 3b000f52e18a5021c156d4a69ceb9f0418176dde Mon Sep 17 00:00:00 2001
From: Konstantin Chukharev <lipen00@gmail.com>
Date: Fri, 31 Jan 2025 18:14:43 +0300
Subject: [PATCH 15/16] Simplify

---
 jacodb-ets/src/main/kotlin/org/jacodb/ets/graph/EtsBlockCfg.kt | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/jacodb-ets/src/main/kotlin/org/jacodb/ets/graph/EtsBlockCfg.kt b/jacodb-ets/src/main/kotlin/org/jacodb/ets/graph/EtsBlockCfg.kt
index e9c1edbd2..3a07eef86 100644
--- a/jacodb-ets/src/main/kotlin/org/jacodb/ets/graph/EtsBlockCfg.kt
+++ b/jacodb-ets/src/main/kotlin/org/jacodb/ets/graph/EtsBlockCfg.kt
@@ -126,7 +126,7 @@ class EtsBlockCfgBuilder(
 
         for (stmt in statements) {
             when (stmt) {
-                org.jacodb.ets.dsl.BlockNop -> {
+                BlockNop -> {
                     etsStatements += EtsNopStmt(location = stub)
                 }
 

From b75a49495c4906b9e4b4128dbd70320316530864 Mon Sep 17 00:00:00 2001
From: Konstantin Chukharev <lipen00@gmail.com>
Date: Fri, 31 Jan 2025 18:14:58 +0300
Subject: [PATCH 16/16] Add NOP to empty block

---
 .../src/main/kotlin/org/jacodb/ets/graph/EtsBlockCfg.kt       | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/jacodb-ets/src/main/kotlin/org/jacodb/ets/graph/EtsBlockCfg.kt b/jacodb-ets/src/main/kotlin/org/jacodb/ets/graph/EtsBlockCfg.kt
index 3a07eef86..2a675aeeb 100644
--- a/jacodb-ets/src/main/kotlin/org/jacodb/ets/graph/EtsBlockCfg.kt
+++ b/jacodb-ets/src/main/kotlin/org/jacodb/ets/graph/EtsBlockCfg.kt
@@ -158,6 +158,10 @@ class EtsBlockCfgBuilder(
             }
         }
 
+        if (etsStatements.isEmpty()) {
+            etsStatements += EtsNopStmt(location = stub)
+        }
+
         return EtsBasicBlock(
             id = id,
             statements = etsStatements,