Using --memlimit to forbid OOMs

Fix in theta-start.sh Reverted theta-start.sh Updated theta-start.sh Theta-start.sh fixes MDD should not cause more OOMs Fixed specification-transformation.zip Fixed syntax
ftsrg · Nov 14, 2024 · 7ca3c7a · 7ca3c7a
1 parent 2447102
commit 7ca3c7a
Show file tree

Hide file tree

Showing 5 changed files with 44 additions and 31 deletions.
diff --git a/.github/actions/build-spec-transformation/patch.diff b/.github/actions/build-spec-transformation/patch.diff
@@ -9,7 +9,7 @@ index 86a7a74e..56f3336a 100644
 -                [
 -                    f"lib/cpachecker/bin/cpachecker",
 +                [   "java", "-cp",
-+                    f"{os.path.dirname(os.path.dirname(__file__))}/cpachecker/runtime/*:{os.path.dirname(os.path.dirname(__file__))}/cpachecker/cpachecker.jar",
++                    f"{os.path.dirname(os.path.dirname(os.path.dirname(__file__)))}/cpachecker/runtime/*:{os.path.dirname(os.path.dirname(os.path.dirname(__file__)))}/cpachecker/cpachecker.jar",
 +                    "org.sosy_lab.cpachecker.cmdline.CPAMain",
                      "--preprocess",
                      "--option",

diff --git a/scripts/theta-start.sh b/scripts/theta-start.sh
@@ -7,6 +7,11 @@ IN=$1
 export VERIFIER_NAME=TOOL_NAME
 export VERIFIER_VERSION=TOOL_VERSION
 
+if [ "$1" == "--version" ]; then
+    LD_LIBRARY_PATH=$scriptdir/lib java -Xss120m -Xmx14210m -jar "$scriptdir"/theta.jar --version || echo $VERIFIER_VERSION
+    exit
+fi
+
 JAVA_VERSION=17
 JAVA_FALLBACK_PATH="/usr/lib/jvm/java-$JAVA_VERSION-openjdk-amd64/bin/:/usr/lib/jvm/java-$JAVA_VERSION-openjdk/bin/:/usr/lib/jvm/java-$JAVA_VERSION/bin/"
 grep -o "openjdk $JAVA_VERSION" <<< "$(java --version)" >/dev/null || export PATH="$JAVA_FALLBACK_PATH":$PATH
@@ -33,35 +38,31 @@ remove_property() {
     echo "${args[@]}"
 }
 
-if [ "$1" == "--version" ]; then
-    LD_LIBRARY_PATH=$scriptdir/lib java -Xss120m -Xmx14210m -jar "$scriptdir"/theta.jar --version
-else
-    modified_args=$(remove_property "${@:2}")
-    property=$(cat .property && rm .property)
-    echo "Verifying input '$IN' with property '$property' using arguments '$modified_args'"
+modified_args=$(remove_property "${@:2}")
+property=$(cat .property && rm .property)
+echo "Verifying input '$IN' with property '$property' using arguments '$modified_args'"
 
-    if [ "$(basename "$property")" == "termination.prp" ]; then
-        transformed_property=$(dirname "$property")/unreach-call.prp
-        echo "Mapping property '$property' to '$transformed_property'"
-        python3 "$scriptdir"/specification-transformation/src/specification-transformation.py --from-property termination --to-property reachability --algorithm InstrumentationOperator $IN
-        "$scriptdir"/offset.sh "$IN" "output/transformed_program.c" > witness-mapping.yml
-        IN="output/transformed_program.c"
-    elif [ "$(basename "$property")" == "no-overflow.prp" ]; then
-        transformed_property=$(dirname "$property")/unreach-call.prp
-        echo "Mapping property '$property' to '$transformed_property'"
-        python3 "$scriptdir"/specification-transformation/src/specification-transformation.py --from-property no-overflow --to-property reachability --algorithm InstrumentationOperator $IN
-        "$scriptdir"/offset.sh "$IN" "output/transformed_program.c" > witness-mapping.yml
-        IN="output/transformed_program.c"
-    else
-        transformed_property="$property"
-    fi
+if [ "$(basename "$property")" == "termination.prp" ]; then
+    transformed_property=$(dirname "$property")/unreach-call.prp
+    echo "Mapping property '$property' to '$transformed_property'"
+    python3 "$scriptdir"/specification-transformation/src/specification-transformation.py --from-property termination --to-property reachability --algorithm InstrumentationOperator $IN
+    "$scriptdir"/offset.sh "$IN" "output/transformed_program.c" > witness-mapping.yml
+    IN="output/transformed_program.c"
+elif [ "$(basename "$property")" == "no-overflow.prp" ]; then
+    transformed_property=$(dirname "$property")/unreach-call.prp
+    echo "Mapping property '$property' to '$transformed_property'"
+    python3 "$scriptdir"/specification-transformation/src/specification-transformation.py --from-property no-overflow --to-property reachability --algorithm InstrumentationOperator $IN
+    "$scriptdir"/offset.sh "$IN" "output/transformed_program.c" > witness-mapping.yml
+    IN="output/transformed_program.c"
+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
+LD_LIBRARY_PATH="$scriptdir"/lib java -Xss120m -Xmx14210m -jar "$scriptdir"/theta.jar $modified_args --input "$IN" --property "$transformed_property" --smt-home "$scriptdir"/solvers
 
-    if [ "$(basename "$property")" == "termination.prp" ]; then
-        echo "Not yet mapping witnesses from '$transformed_property' to '$property', hoping for the best"
-    elif [ "$(basename "$property")" == "no-overflow.prp" ]; then
-        echo "Not yet mapping witnesses from '$transformed_property' to '$property', hoping for the best"
-    fi
+if [ "$(basename "$property")" == "termination.prp" ]; then
+    echo "Not yet mapping witnesses from '$transformed_property' to '$property', hoping for the best"
+elif [ "$(basename "$property")" == "no-overflow.prp" ]; then
+    echo "Not yet mapping witnesses from '$transformed_property' to '$property', hoping for the best"
 fi
diff --git a/...ojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/InProcessChecker.kt b/...ojects/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
@@ -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
@@ -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 / 5 * 4,
           solverHome = portfolioConfig.backendConfig.solverHome,
           timeoutMs = 0,
           specConfig =
@@ -375,7 +377,8 @@ fun boundedPortfolio25(
     edges.add(Edge(bmcConfig, indConfig, if (inProcess) timeoutOrNotSolvableError else anyError))
     edges.add(Edge(indConfig, imcConfig, if (inProcess) timeoutOrNotSolvableError else anyError))
 
-    return STM(mddConfig, edges)
+    return if (inProcess) STM(mddConfig, edges)
+    else STM(bmcConfig, edges) // mdd should not be run not-in-proc
   }
 
   logger.write(Logger.Level.RESULT, "Using bounded portfolio\n")