Builder for Blocks

plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/conversion/ProgramConverter.kt

@@ -377,7 +377,10 @@ class ProgramConverter(val session: FirSession, override val config: PluginConfi
         // One of the simplest solutions is to do is directly in the beginning of the body.
         val unitExtendedBody: ExpEmbedding =
             if (signature.type.returnType != UnitTypeEmbedding) body
-            else Block(Assign(stmtCtx.defaultResolvedReturnTarget.variable, UnitLit), body)
+            else blockOf(
+                Assign(stmtCtx.defaultResolvedReturnTarget.variable, UnitLit),
+                body,
+            )
         val bodyExp = FunctionExp(signature, unitExtendedBody, returnTarget.label)
         val seqnBuilder = SeqnBuilder(declaration.source)
         val linearizer = Linearizer(SharedLinearizationState(anonVarProducer), seqnBuilder, declaration.source)

plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/conversion/StmtConversionContext.kt

@@ -166,14 +166,12 @@ fun StmtConversionContext.insertInlineFunctionCall(
         parent = parentCtx,
     )
     return withMethodCtx(methodCtxFactory) {
-        Block(
-            buildList {
-                add(Declare(returnTarget.variable, null))
-                addAll(declarations)
-                add(FunctionExp(null, convert(body), returnTarget.label))
-                add(returnTarget.variable)
-            }
-        )
+        Block {
+            add(Declare(returnTarget.variable, null))
+            addAll(declarations)
+            add(FunctionExp(null, convert(body), returnTarget.label))
+            add(returnTarget.variable)
+        }
     }
 }
 

plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/conversion/StmtConversionVisitor.kt

@@ -52,11 +52,14 @@ object StmtConversionVisitor : FirVisitor<ExpEmbedding, StmtConversionContext>()
         // returnTarget is null when it is the implicit return of a lambda
         val returnTargetName = returnExpression.target.labelName
         val target = data.resolveReturnTarget(returnTargetName)
-        return Block(Assign(target.variable, expr), Goto(target.label))
+        return blockOf(
+            Assign(target.variable, expr),
+            Goto(target.label)
+        )
     }
 
     override fun visitBlock(block: FirBlock, data: StmtConversionContext): ExpEmbedding =
-        Block(block.statements.map(data::convert))
+        block.statements.map(data::convert).toBlock()
 
     override fun visitLiteralExpression(
         constExpression: FirLiteralExpression,
@@ -114,7 +117,7 @@ object StmtConversionVisitor : FirVisitor<ExpEmbedding, StmtConversionContext>()
             val body = withWhenSubject(subj?.variable) {
                 convertWhenBranches(whenExpression.branches.iterator(), type, this)
             }
-            subj?.let { Block(it, body) } ?: body
+            subj?.let { blockOf(it, body) } ?: body
         }
 
     override fun visitPropertyAccessExpression(
@@ -318,7 +321,15 @@ object StmtConversionVisitor : FirVisitor<ExpEmbedding, StmtConversionContext>()
             withNewScope {
                 val jumps = catchData.blocks.map { catchBlock -> NonDeterministically(Goto(catchBlock.entryLabel)) }
                 val body = convert(tryExpression.tryBlock)
-                GotoChainNode(null, Block(jumps + listOf(body) + jumps), catchData.exitLabel)
+                GotoChainNode(
+                    null,
+                    Block {
+                        addAll(jumps)
+                        add(body)
+                        addAll(jumps)
+                    },
+                    catchData.exitLabel
+                )
             }
         }
         val catches = catchData.blocks.map { catchBlock ->
@@ -328,15 +339,19 @@ object StmtConversionVisitor : FirVisitor<ExpEmbedding, StmtConversionContext>()
                 val paramDecl = declareLocalProperty(parameter.symbol, null)
                 GotoChainNode(
                     catchBlock.entryLabel,
-                    Block(
+                    blockOf(
                         paramDecl,
                         convert(catchBlock.firCatch.block)
                     ),
                     catchData.exitLabel
                 )
             }
         }
-        return Block(listOf(tryBody) + catches + LabelExp(catchData.exitLabel))
+        return Block {
+            add(tryBody)
+            addAll(catches)
+            add(LabelExp(catchData.exitLabel))
+        }
     }
 
     override fun visitElvisExpression(

plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/callables/SpecialKotlinFunction.kt

@@ -110,7 +110,10 @@ object KotlinIntDivFunctionImplementation : KotlinIntSpecialFunction() {
         args: List<ExpEmbedding>,
         ctx: StmtConversionContext,
         // TODO: implement this properly, we don't want to evaluate args[1] twice.
-    ): ExpEmbedding = Block(InhaleDirect(NeCmp(args[1], IntLit(0))), Div(args[0], args[1]))
+    ): ExpEmbedding = blockOf(
+        InhaleDirect(NeCmp(args[1], IntLit(0))),
+        Div(args[0], args[1]),
+    )
 }
 
 abstract class KotlinBooleanSpecialFunction : SpecialKotlinFunction {

plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/expression/ControlFlow.kt

@@ -23,11 +23,20 @@ import org.jetbrains.kotlin.formver.viper.ast.Label
 import org.jetbrains.kotlin.formver.viper.ast.PermExp
 import org.jetbrains.kotlin.formver.viper.ast.Stmt
 
-// TODO: make a nice BlockBuilder interface.
-data class Block(val exps: List<ExpEmbedding>) : OptionalResultExpEmbedding {
-    constructor (vararg exps: ExpEmbedding) : this(exps.toList())
+private data class BlockImpl(override val exps: List<ExpEmbedding>) : Block
 
-    override val type: TypeEmbedding = exps.lastOrNull()?.type ?: buildType { unit() }
+fun blockOf(vararg exps: ExpEmbedding): Block = BlockImpl(exps.toList())
+
+fun List<ExpEmbedding>.toBlock(): Block = BlockImpl(this)
+
+fun Block(actions: MutableList<ExpEmbedding>.() -> Unit): Block = BlockImpl(buildList {
+    actions()
+})
+
+sealed interface Block : OptionalResultExpEmbedding {
+    val exps: List<ExpEmbedding>
+    override val type: TypeEmbedding
+        get() = exps.lastOrNull()?.type ?: buildType { unit() }
 
     override fun toViperMaybeStoringIn(result: VariableEmbedding?, ctx: LinearizationContext) {
         if (exps.isEmpty()) return
@@ -42,6 +51,7 @@ data class Block(val exps: List<ExpEmbedding>) : OptionalResultExpEmbedding {
         get() = BlockNode(exps.map { it.debugTreeView })
 }
 
+
 data class If(val condition: ExpEmbedding, val thenBranch: ExpEmbedding, val elseBranch: ExpEmbedding, override val type: TypeEmbedding) :
     OptionalResultExpEmbedding, DefaultDebugTreeViewImplementation {
     override fun toViperMaybeStoringIn(result: VariableEmbedding?, ctx: LinearizationContext) {