add command line flag to enable debug info in proof trace (#4483)

This PR adds a flag to `kompile` which propogates the effect of a
lower-level flag to `llvm-kompile` which assists with debugging the
proof hints that are created.

Co-authored-by: rv-jenkins <[email protected]>

k-distribution/tests/regression-new/proof-instrumentation-debug/.gitignore

@@ -0,0 +1 @@
+out.hint

k-distribution/tests/regression-new/proof-instrumentation-debug/Makefile

@@ -0,0 +1,11 @@
+DEF=test
+EXT=test
+TESTDIR=.
+KOMPILE_BACKEND=llvm
+KOMPILE_FLAGS+=--gen-glr-bison-parser --llvm-proof-hint-debugging
+KRUN_FLAGS=--proof-hint
+
+include ../../../include/kframework/ktest.mak
+
+clean:
+	rm -rf out.hint test.kore $(KOMPILED_DIR) .depend-tmp .depend .kompile-* .krun-* .kprove-* kore-exec.tar.gz

k-distribution/tests/regression-new/proof-instrumentation-debug/input.test

@@ -0,0 +1 @@
+foo()

k-distribution/tests/regression-new/proof-instrumentation-debug/test.k

@@ -0,0 +1,9 @@
+// Copyright (c) Runtime Verification, Inc. All Rights Reserved.
+module TEST-SYNTAX
+  syntax Foo ::= foo() | bar()
+endmodule
+
+module TEST
+  imports TEST-SYNTAX
+  rule foo() => bar()
+endmodule

llvm-backend/src/main/java/org/kframework/backend/llvm/LLVMBackend.java

@@ -131,8 +131,12 @@ private void llvmKompile(String type, String executable) {
       args.add(files.resolveKompiled("dt").getCanonicalPath());
       args.add(type);
 
-      if (options.enableProofHints) {
-        args.add("--proof-hint-instrumentation");
+      if (options.enableProofHints || options.enableProofHintDebugging) {
+        if (options.enableProofHintDebugging) {
+          args.add("--proof-hint-instrumentation-slow");
+        } else {
+          args.add("--proof-hint-instrumentation");
+        }
       }
 
       if (options.llvmMutableBytes) {

llvm-backend/src/main/java/org/kframework/backend/llvm/LLVMKompileOptions.java

@@ -107,6 +107,13 @@ public List<String> convert(String str) {
       hidden = true)
   public boolean enableProofHints;
 
+  @Parameter(
+      names = "--llvm-proof-hint-debugging",
+      description =
+          "Enables additional debugging information in proof hints generated by the LLVM backend",
+      hidden = true)
+  public boolean enableProofHintDebugging;
+
   @Parameter(
       names = "--llvm-mutable-bytes",
       description = "Use a faster, unsound representation for byte arrays on the LLVM backend",

pyk/src/pyk/__main__.py

@@ -323,6 +323,7 @@ def exec_kompile(options: KompileCommandOptions) -> None:
         kompile_dict['llvm_kompile_type'] = options.llvm_kompile_type
         kompile_dict['llvm_kompile_output'] = options.llvm_kompile_output
         kompile_dict['llvm_proof_hint_instrumentation'] = options.llvm_proof_hint_instrumentation
+        kompile_dict['llvm_proof_hint_debugging'] = options.llvm_proof_hint_debugging
     elif len(options.ccopts) > 0:
         raise ValueError(f'Option `-ccopt` requires `--backend llvm`, not: --backend {options.backend.value}')
     elif options.enable_search:
@@ -339,6 +340,10 @@ def exec_kompile(options: KompileCommandOptions) -> None:
         raise ValueError(
             f'Option `--llvm-proof-hint-intrumentation` requires `--backend llvm`, not: --backend {options.backend.value}'
         )
+    elif options.llvm_proof_hint_debugging:
+        raise ValueError(
+            f'Option `--llvm-proof-hint-debugging` requires `--backend llvm`, not: --backend {options.backend.value}'
+        )
 
     try:
         Kompile.from_dict(kompile_dict)(

pyk/src/pyk/cli/args.py

@@ -193,6 +193,7 @@ class KompileOptions(Options):
     llvm_kompile_type: LLVMKompileType | None
     llvm_kompile_output: Path | None
     llvm_proof_hint_instrumentation: bool
+    llvm_proof_hint_debugging: bool
     read_only: bool
     o0: bool
     o1: bool
@@ -218,6 +219,7 @@ def default() -> dict[str, Any]:
             'llvm_kompile_type': None,
             'llvm_kompile_output': None,
             'llvm_proof_hint_instrumentation': False,
+            'llvm_proof_hint_debugging': False,
             'read_only': False,
             'o0': False,
             'o1': False,
@@ -470,6 +472,14 @@ def kompile_args(self) -> ArgumentParser:
             action='store_true',
             help='Enable proof hint generation in LLVM backend kompilation.',
         )
+        args.add_argument(
+            '--llvm-proof-hint-debugging',
+            dest='llvm_proof_hint_debugging',
+            default=None,
+            action='store_true',
+            help='Enable additional proof hint debugging information in LLVM backend kompilation.',
+        )
+
         args.add_argument(
             '--no-exc-wrap',
             dest='no_exc_wrap',

pyk/src/pyk/ktool/kompile.py

@@ -431,6 +431,7 @@ class LLVMKompile(Kompile):
     enable_search: bool
     enable_llvm_debug: bool
     llvm_proof_hint_instrumentation: bool
+    llvm_proof_hint_debugging: bool
     llvm_mutable_bytes: bool
     iterated_threshold: Fraction | None
     heuristic: str | None
@@ -447,6 +448,7 @@ def __init__(
         enable_search: bool = False,
         enable_llvm_debug: bool = False,
         llvm_proof_hint_instrumentation: bool = False,
+        llvm_proof_hint_debugging: bool = False,
         llvm_mutable_bytes: bool = False,
         iterated_threshold: Fraction | None = None,
         heuristic: str | None = None,
@@ -469,6 +471,7 @@ def __init__(
         object.__setattr__(self, 'enable_search', enable_search)
         object.__setattr__(self, 'enable_llvm_debug', enable_llvm_debug)
         object.__setattr__(self, 'llvm_proof_hint_instrumentation', llvm_proof_hint_instrumentation)
+        object.__setattr__(self, 'llvm_proof_hint_debugging', llvm_proof_hint_debugging)
         object.__setattr__(self, 'llvm_mutable_bytes', llvm_mutable_bytes)
         object.__setattr__(self, 'iterated_threshold', iterated_threshold)
         object.__setattr__(self, 'heuristic', heuristic)
@@ -505,6 +508,9 @@ def args(self) -> list[str]:
         if self.llvm_proof_hint_instrumentation:
             args += ['--llvm-proof-hint-instrumentation']
 
+        if self.llvm_proof_hint_debugging:
+            args += ['--llvm-proof-hint-debugging']
+
         if self.llvm_mutable_bytes:
             args += ['--llvm-mutable-bytes']