From cf0967c68382c3a53068d80d668cfb09ad460425 Mon Sep 17 00:00:00 2001
From: Levente Bajczi <bajczilevi@gmail.com>
Date: Thu, 14 Nov 2024 21:33:26 +0100
Subject: [PATCH] Using --memlimit to forbid OOMs

Fix in theta-start.sh

Reverted theta-start.sh

Updated theta-start.sh
---
 scripts/theta-start.sh                                      | 2 +-
 .../hu/bme/mit/theta/xcfa/cli/checkers/InProcessChecker.kt  | 6 +++++-
 .../java/hu/bme/mit/theta/xcfa/cli/params/XcfaConfig.kt     | 5 +++++
 .../java/hu/bme/mit/theta/xcfa/cli/portfolio/bounded25.kt   | 2 ++
 4 files changed, 13 insertions(+), 2 deletions(-)

diff --git a/scripts/theta-start.sh b/scripts/theta-start.sh
index b54acf3c63..18a7ce551c 100755
--- a/scripts/theta-start.sh
+++ b/scripts/theta-start.sh
@@ -34,7 +34,7 @@ remove_property() {
 }
 
 if [ "$1" == "--version" ]; then
-    LD_LIBRARY_PATH=$scriptdir/lib java -Xss120m -Xmx14210m -jar "$scriptdir"/theta.jar --version
+    LD_LIBRARY_PATH=$scriptdir/lib java -Xss120m -Xmx14210m -jar "$scriptdir"/theta.jar --version || echo $VERIFIER_VERSION
 else
     modified_args=$(remove_property "${@:2}")
     property=$(cat .property && rm .property)
diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/InProcessChecker.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/InProcessChecker.kt
index 4022efe510..8ca637dd16 100644
--- a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/InProcessChecker.kt
+++ b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/InProcessChecker.kt
@@ -77,12 +77,16 @@ class InProcessChecker<F : SpecFrontendConfig, B : SpecBackendConfig>(
         getGson(xcfa).toJson(processConfig)
       }
 
+    val heapSize =
+      "-Xmx${if(config.backendConfig.memlimit == 0L) 1420L else config.backendConfig.memlimit/1024/1024 }m"
+    logger.write(Logger.Level.INFO, "Starting process with $heapSize of heap\n")
+
     val pb =
       NuProcessBuilder(
         listOf(
             ProcessHandle.current().info().command().orElse("java"),
             "-Xss120m",
-            "-Xmx14210m",
+            heapSize,
             "-cp",
             File(XcfaCli::class.java.protectionDomain.codeSource.location.toURI()).absolutePath,
             XcfaCli::class.qualifiedName,
diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/params/XcfaConfig.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/params/XcfaConfig.kt
index 73b52dbcda..674954f65a 100644
--- a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/params/XcfaConfig.kt
+++ b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/params/XcfaConfig.kt
@@ -179,6 +179,11 @@ data class BackendConfig<T : SpecBackendConfig>(
   var timeoutMs: Long = 0,
   @Parameter(names = ["--in-process"], description = "Run analysis in process")
   var inProcess: Boolean = false,
+  @Parameter(
+    names = ["--memlimit"],
+    description = "Maximum memory to use when --in-process (in bytes, 0 for default)",
+  )
+  var memlimit: Long = 0L,
   override var specConfig: T? = null,
 ) : SpecializableConfig<T> {
 
diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/portfolio/bounded25.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/portfolio/bounded25.kt
index 5b8d481b8b..97f345f7d8 100644
--- a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/portfolio/bounded25.kt
+++ b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/portfolio/bounded25.kt
@@ -59,6 +59,7 @@ fun boundedPortfolio25(
       backendConfig =
         BackendConfig(
           backend = Backend.BOUNDED,
+          memlimit = portfolioConfig.backendConfig.memlimit,
           solverHome = portfolioConfig.backendConfig.solverHome,
           timeoutMs = 0,
           specConfig =
@@ -93,6 +94,7 @@ fun boundedPortfolio25(
       backendConfig =
         BackendConfig(
           backend = Backend.MDD,
+          memlimit = portfolioConfig.backendConfig.memlimit,
           solverHome = portfolioConfig.backendConfig.solverHome,
           timeoutMs = 0,
           specConfig =