From 00103e944e3c2ed990ad4214554a78cf9cc794cf Mon Sep 17 00:00:00 2001
From: Alexey Menshutin <alex.menshutin99@gmail.com>
Date: Thu, 25 May 2023 15:01:33 +0300
Subject: [PATCH] Implement `close` functions for UMachine and USolver classes

---
 usvm-core/src/main/kotlin/org/usvm/Machine.kt               | 2 +-
 usvm-core/src/main/kotlin/org/usvm/solver/Solver.kt         | 6 +++++-
 .../src/main/kotlin/org/usvm/interpreter/SampleMachine.kt   | 5 +++++
 3 files changed, 11 insertions(+), 2 deletions(-)

diff --git a/usvm-core/src/main/kotlin/org/usvm/Machine.kt b/usvm-core/src/main/kotlin/org/usvm/Machine.kt
index 09530ef19c..b48432dbf3 100644
--- a/usvm-core/src/main/kotlin/org/usvm/Machine.kt
+++ b/usvm-core/src/main/kotlin/org/usvm/Machine.kt
@@ -6,7 +6,7 @@ package org.usvm
  *
  * @see [run]
  */
-abstract class UMachine<State : UState<*, *, *, *>, Target> {
+abstract class UMachine<State : UState<*, *, *, *>, Target> : AutoCloseable {
     /**
      * The main entry point. Template method for running the machine on a specified [target].
      *
diff --git a/usvm-core/src/main/kotlin/org/usvm/solver/Solver.kt b/usvm-core/src/main/kotlin/org/usvm/solver/Solver.kt
index fd8af5936b..dcc6c687a9 100644
--- a/usvm-core/src/main/kotlin/org/usvm/solver/Solver.kt
+++ b/usvm-core/src/main/kotlin/org/usvm/solver/Solver.kt
@@ -21,7 +21,7 @@ open class UUnsatResult<Model> : USolverResult<Model>
 
 open class UUnknownResult<Model> : USolverResult<Model>
 
-abstract class USolver<in PathCondition, out Model> {
+abstract class USolver<in PathCondition, out Model> : AutoCloseable {
     abstract fun check(pc: PathCondition, useSoftConstraints: Boolean): USolverResult<Model>
 }
 
@@ -135,4 +135,8 @@ open class USolverBase<Field, Type, Method>(
 
     fun emptyModel(): UModelBase<Field, Type> =
         (checkWithSoftConstraints(UPathConstraints(ctx)) as USatResult<UModelBase<Field, Type>>).model
+
+    override fun close() {
+        smtSolver.close()
+    }
 }
\ No newline at end of file
diff --git a/usvm-sample-language/src/main/kotlin/org/usvm/interpreter/SampleMachine.kt b/usvm-sample-language/src/main/kotlin/org/usvm/interpreter/SampleMachine.kt
index 27ce496b8b..a7d5845443 100644
--- a/usvm-sample-language/src/main/kotlin/org/usvm/interpreter/SampleMachine.kt
+++ b/usvm-sample-language/src/main/kotlin/org/usvm/interpreter/SampleMachine.kt
@@ -60,4 +60,9 @@ class SampleMachine(
     private fun isInterestingState(state: SampleState): Boolean {
         return state.callStack.isNotEmpty() && state.exceptionRegister == null
     }
+
+    override fun close() {
+        solver.close()
+        ctx.close()
+    }
 }
\ No newline at end of file