Merge branch 'permit-cell-collection' of github.com:runtimeverificati…

…on/k into permit-cell-collection
runtimeverification · Jun 27, 2024 · 85b530a · 85b530a
2 parents d0f6b49 + 9051ac5
commit 85b530a
Show file tree

Hide file tree

Showing 11 changed files with 57 additions and 3 deletions.
diff --git a/k-distribution/tests/regression-new/proof-instrumentation-debug/.gitignore b/k-distribution/tests/regression-new/proof-instrumentation-debug/.gitignore
@@ -0,0 +1 @@
+out.hint
diff --git a/k-distribution/tests/regression-new/proof-instrumentation-debug/Makefile b/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
diff --git a/k-distribution/tests/regression-new/proof-instrumentation-debug/input.test b/k-distribution/tests/regression-new/proof-instrumentation-debug/input.test
@@ -0,0 +1 @@
+foo()
diff --git a/k-distribution/tests/regression-new/proof-instrumentation-debug/input.test.out b/k-distribution/tests/regression-new/proof-instrumentation-debug/input.test.out
diff --git a/k-distribution/tests/regression-new/proof-instrumentation-debug/test.k b/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
diff --git a/llvm-backend/src/main/java/org/kframework/backend/llvm/LLVMBackend.java b/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) {

diff --git a/llvm-backend/src/main/java/org/kframework/backend/llvm/LLVMKompileOptions.java b/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",

diff --git a/pyk/src/pyk/__main__.py b/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)(

diff --git a/pyk/src/pyk/cli/args.py b/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',

diff --git a/pyk/src/pyk/ktool/kompile.py b/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']
 

diff --git a/web/toc.md b/web/toc.md
@@ -17,7 +17,7 @@ output:
 
 - [Homepage](/web/pages/index.md)
 - [Install K](https://github.com/runtimeverification/k/releases/latest)
-- [Pyk Documentation](/pyk)
+- [Pyk Documentation](https://kframework.org/pyk)
 - [K Tutorial](/k-distribution/k-tutorial/README.md)
   - [Section 1: Basic K Concepts](/k-distribution/k-tutorial/1_basic/README.md)
     - [Lesson 1.1: Setting up a K Environment](/k-distribution/k-tutorial/1_basic/01_installing/README.md)