From 02e7dd6f8f4a34c9bb751f460520f9abe526b700 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Bobot?= <francois.bobot@cea.fr>
Date: Fri, 12 Jul 2024 22:24:05 +0200
Subject: [PATCH] Fix local model validation

and raise stack limit for dolmen
---
 smtcomp/main.py             | 35 +++++++++++++++++++++--------------
 smtcomp/model_validation.py | 11 +++++++++--
 2 files changed, 30 insertions(+), 16 deletions(-)

diff --git a/smtcomp/main.py b/smtcomp/main.py
index 17c0492c..6b1c5d9c 100644
--- a/smtcomp/main.py
+++ b/smtcomp/main.py
@@ -19,6 +19,7 @@
 import smtcomp.benchexec as benchexec
 import smtcomp.benchexec
 import smtcomp.defs as defs
+import smtcomp.model_validation
 import smtcomp.results
 import smtcomp.scoring
 import smtcomp.submission as submission
@@ -971,11 +972,18 @@ def check_model_locally(
             for resultdir in resultdirs:
                 l2 = model_validation.check_results_locally(config, cachedir, resultdir, executor, progress)
                 l.extend(filter_map(map_none3(model_validation.is_error), l2))
-    keyfunc = lambda v: v[0].solver
+    if not l:
+        print("[green]All models validated[/green]")
+        return
+
+    def keyfunc(
+        v: tuple[smtcomp.results.RunId, smtcomp.results.Run, smtcomp.model_validation.ValidationError],
+    ) -> str:
+        return v[0].solver
+
     l.sort(key=keyfunc)
-    d = itertools.groupby(l, key=keyfunc)
-    t = Tree("Unvalidated models")
-    for solver, rs in d:
+    t = Tree("[red]Unvalidated models[/red]")
+    for solver, rs in itertools.groupby(l, key=keyfunc):
         t2 = t.add(solver)
         for rid, r, result in rs:
             stderr = result.stderr.strip().replace("\n", ", ")
@@ -983,17 +991,16 @@ def check_model_locally(
             t2.add(f"{basename}: {stderr}")
     print(t)
     if outdir is not None:
-        for solver, models in d:
-            dst = outdir / solver
+        for rid, r, result in l:
+            dst = outdir / rid.solver
             dst.mkdir(parents=True, exist_ok=True)
-            for rid, r, result in models:
-                filedir = benchmark_files_dir(cachedir, rid.track)
-                basename = smtcomp.scramble_benchmarks.scramble_basename(r.scramble_id)
-                basename_model = smtcomp.scramble_benchmarks.scramble_basename(r.scramble_id, suffix="rsmt2")
-                smt2_file = filedir / str(r.logic) / basename
-                (dst / basename).unlink(missing_ok=True)
-                (dst / basename).symlink_to(smt2_file)
-                (dst / basename_model).write_text(result.model)
+            filedir = benchmark_files_dir(cachedir, rid.track)
+            basename = smtcomp.scramble_benchmarks.scramble_basename(r.scramble_id)
+            basename_model = smtcomp.scramble_benchmarks.scramble_basename(r.scramble_id, suffix="rsmt2")
+            smt2_file = filedir / str(r.logic) / basename
+            (dst / basename).unlink(missing_ok=True)
+            (dst / basename).symlink_to(smt2_file.absolute())
+            (dst / basename_model).write_text(result.model)
 
 
 @app.command()
diff --git a/smtcomp/model_validation.py b/smtcomp/model_validation.py
index 2dab0134..145f9c53 100644
--- a/smtcomp/model_validation.py
+++ b/smtcomp/model_validation.py
@@ -1,7 +1,7 @@
 from dataclasses import dataclass
 from pathlib import Path
 import smtcomp.defs as defs
-import subprocess
+import subprocess, resource
 import smtcomp.results as results
 from smtcomp.benchexec import get_suffix
 import smtcomp.scramble_benchmarks
@@ -41,7 +41,7 @@ class ValidationOk:
 class ValidationError:
     status: defs.Status
     stderr: str
-    model: str | None
+    model: str
 
 
 @dataclass
@@ -62,6 +62,12 @@ def is_error(x: Validation) -> ValidationError | None:
             return None
 
 
+def raise_stack_limit() -> None:
+    soft, hard = resource.getrlimit(resource.RLIMIT_STACK)
+    soft = min(40_000_000_000, hard)
+    resource.setrlimit(resource.RLIMIT_STACK, (soft, hard))
+
+
 def check_locally(config: defs.Config, smt2_file: Path, model: str) -> Validation:
     r = subprocess.run(
         [
@@ -75,6 +81,7 @@ def check_locally(config: defs.Config, smt2_file: Path, model: str) -> Validatio
         ],
         input=model.encode(),
         capture_output=True,
+        preexec_fn=raise_stack_limit,
     )
     match r.returncode:
         case 0: