From 4d4c214600c534a659fcbbb10847c2dcbaf6bbe8 Mon Sep 17 00:00:00 2001
From: Benjamin Lipp <blipp@rosenpass.eu>
Date: Mon, 8 Dec 2025 16:55:45 +0100
Subject: [PATCH] feat: add model name to log entries

---
 marzipan/TODO.md         |  8 +++---
 marzipan/src/__init__.py | 54 ++++++++++++++++++++++++++++++----------
 2 files changed, 46 insertions(+), 16 deletions(-)

diff --git a/marzipan/TODO.md b/marzipan/TODO.md
index 7c58899..b88a184 100644
--- a/marzipan/TODO.md
+++ b/marzipan/TODO.md
@@ -34,15 +34,17 @@
 * ~~refactor filtering in run_proverif (see karo's comment)~~
 * ~configurable target directory~
 * ~lark parser: multiline comments, how???~
+* ~parse errors~
+  * ~error when trying with: `nix run .# -- parse ../target/proverif/01_secrecy.entry.i.pv`~
+    * ~`in(C, Cinit_conf(Ssskm, Spsk, Sspkt, ic));`~
+    * ~                                          ^~
+  * ~04_dos… has a syntax error (see below)~
 
 ## Next Steps
 
 * integrate marzipan.awk into Python, somehow
   * options term special cases (c.f. manual page 133, starting with "fun" term)
     * complete with CryptoVerif options
-  * error when trying with: `nix run .# -- parse ../target/proverif/01_secrecy.entry.i.pv`
-    * `in(C, Cinit_conf(Ssskm, Spsk, Sspkt, ic));`
-    *                                           ^
 * rewrite marzipan.awk into Python/LARK
   * define a LARK grammar for marzipan.awk rules
   * write python code for processing marzipan rules, e.g. alias replacement (step: i.pv->o.pv)
diff --git a/marzipan/src/__init__.py b/marzipan/src/__init__.py
index 66fe42d..aed91c5 100644
--- a/marzipan/src/__init__.py
+++ b/marzipan/src/__init__.py
@@ -14,6 +14,23 @@ console = pkgs.rich.console.Console()
 logger = pkgs.logging.getLogger(__name__)
 
 
+def set_logging_logrecordfactory(filename):
+    old_factory = pkgs.logging.getLogRecordFactory()
+
+    def record_factory(*args, **kwargs):
+        record = old_factory(*args, **kwargs)
+        record.filename = filename
+        return record
+
+    pkgs.logging.setLogRecordFactory(record_factory)
+
+
+#def set_logging_format(max_length):
+#    pass
+#    #format_str = "{levelname:<8} {filename:<" + str(max_length + 2) + "} {message}"
+#    #pkgs.logging.basicConfig(level=pkgs.logging.DEBUG, style="{", format=format_str)
+
+
 @click.group()
 def main():
     pkgs.logging.basicConfig(level=pkgs.logging.DEBUG)
@@ -50,7 +67,7 @@ def clean_line(prev_line, line):
     return prev_line
 
 
-def run_proverif(file, extra_args=[]):
+def run_proverif(file, log_file, extra_args=[]):
     params = ["proverif", "-test", *extra_args, file]
     logger.debug(params)
 
@@ -63,13 +80,15 @@ def run_proverif(file, extra_args=[]):
     )
     try:
         prev_line = None
-        for line in process.stdout:
-            cleaned_line = clean_line(prev_line, line)
-            prev_line = line
-            if cleaned_line is not None:
-                yield cleaned_line
-        if prev_line is not None:
-            yield prev_line
+        with open(log_file, "a") as log:
+            for line in process.stdout:
+                log.write(line)
+                cleaned_line = clean_line(prev_line, line)
+                prev_line = line
+                if cleaned_line is not None:
+                    yield cleaned_line
+            if prev_line is not None:
+                yield prev_line
 
     except Exception as e:
         # When does this happen? Should the error even be ignored? Metaverif should probably just abort here, right? --karo
@@ -83,6 +102,9 @@ def run_proverif(file, extra_args=[]):
             logger.error(
                 f"Proverif exited with a non-zero error code {params}: {return_code}"
             )
+            if prev_line is not None:
+                logger.error(f"Last line of log file {log_file}:")
+                logger.error(f"> {prev_line.rstrip()}")
             exit(return_code)
 
 
@@ -193,7 +215,12 @@ def analyze(repo_path, output):
 
     entries = []
     analysis_dir = pkgs.os.path.join(repo_path, "analysis")
-    entries.extend(sorted(pkgs.glob.glob(str(analysis_dir) + "/*.entry.mpv")))
+    full_paths = sorted(pkgs.glob.glob(str(analysis_dir) + "/*.entry.mpv"))
+    entries.extend(full_paths)
+
+    #modelnames = [pkgs.os.path.basename(path).replace('.entry.mpv', '') for path in full_paths]
+    #max_length = max(len(modelname) for modelname in modelnames) if modelnames else 0
+    #set_logging_format(max_length)
 
     with pkgs.concurrent.futures.ProcessPoolExecutor() as executor:
         futures = {
@@ -231,12 +258,14 @@ def clean(repo_path, output):
 
 
 def metaverif(repo_path, tmpdir, file):
-    print(f"Start metaverif on {file}")
     # Extract the name using regex
-    name_match = pkgs.re.search(r"([^/]*)(?=\.mpv)", file)
+    name_match = pkgs.re.search(r"([^/]*)(?=\.entry\.mpv)", file)
     if name_match:
         name = name_match.group(0)  # Get the matched name
 
+        set_logging_logrecordfactory(name)
+        logger.info(f"Start metaverif on {file}")
+
         # Create the file paths
         cpp_prep = pkgs.os.path.join(tmpdir, f"{name}.i.pv")
         awk_prep = pkgs.os.path.join(tmpdir, f"{name}.o.pv")
@@ -253,9 +282,8 @@ def metaverif(repo_path, tmpdir, file):
 
         ta, res, ctr, expected, descs = pretty_output_init(cpp_prep)
         with open(log_file, "a") as log:
-            generator = run_proverif(awk_prep)
+            generator = run_proverif(awk_prep, log_file)
             for line in generator:
-                log.write(line)
                 # parse-result-line:
                 match = pkgs.re.search(r"^RESULT .* \b(true|false)\b\.$", line)
                 if match: