From aca4930a7502a8a9fedfb4fc107d9732fe3d8a9a 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

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

diff --git a/scripts/theta-start.sh b/scripts/theta-start.sh
index b54acf3c63..fcf6321a18 100755
--- a/scripts/theta-start.sh
+++ b/scripts/theta-start.sh
@@ -15,6 +15,23 @@ grep -o "openjdk $JAVA_VERSION" <<< "$(java --version)" >/dev/null || {
     exit 1
 }
 
+
+determine_memlimit() {
+  cgroup_file="/proc/self/cgroup"
+  if [[ -f "$cgroup_file" ]]; then
+      memory_cgroup=$(grep memory "$cgroup_file" | cut -d: -f3)
+      if [[ ! -z "$memory_cgroup" ]]; then
+        echo $memory_cgroup
+        memory_limit_file="/sys/fs/cgroup/memory${memory_cgroup}/memory.limit_in_bytes"
+        if [[ -f "$memory_limit_file" ]]; then
+          cat "$memory_limit_file"
+          return 0
+        fi
+      fi
+  fi
+  echo 0
+}
+
 remove_property() {
     local args=()
     local skip=0
@@ -34,7 +51,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 -jar "$scriptdir"/theta.jar --version
 else
     modified_args=$(remove_property "${@:2}")
     property=$(cat .property && rm .property)
@@ -56,8 +73,8 @@ else
         transformed_property="$property"
     fi
 
-    echo LD_LIBRARY_PATH="$scriptdir"/lib java -Xss120m -Xmx14210m -jar "$scriptdir"/theta.jar $modified_args --input "$IN" --property "$transformed_property" --smt-home "$scriptdir"/solvers
-    LD_LIBRARY_PATH="$scriptdir"/lib java -Xss120m -Xmx14210m -jar "$scriptdir"/theta.jar $modified_args --input "$IN" --property "$transformed_property" --smt-home "$scriptdir"/solvers
+    echo LD_LIBRARY_PATH="$scriptdir"/lib java -Xss120m -Xmx14210m -jar "$scriptdir"/theta.jar $modified_args --input "$IN" --property "$transformed_property" --smt-home "$scriptdir"/solvers --memlimit "$(determine_memlimit)"
+    LD_LIBRARY_PATH="$scriptdir"/lib java -Xss120m -Xmx14210m -jar "$scriptdir"/theta.jar $modified_args --input "$IN" --property "$transformed_property" --smt-home "$scriptdir"/solvers --memlimit "$(determine_memlimit)"
 
     if [ "$(basename "$property")" == "termination.prp" ]; then
         echo "Not yet mapping witnesses from '$transformed_property' to '$property', hoping for the best"
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 =