From 137574d94e1d64f89a93a1ea024fe1bcdb0fb2bf Mon Sep 17 00:00:00 2001 From: Dwight Guth Date: Wed, 26 Jun 2024 11:01:29 -0500 Subject: [PATCH] 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 --- .../proof-instrumentation-debug/.gitignore | 1 + .../proof-instrumentation-debug/Makefile | 11 +++++++++++ .../proof-instrumentation-debug/input.test | 1 + .../proof-instrumentation-debug/input.test.out | Bin 0 -> 1521 bytes .../proof-instrumentation-debug/test.k | 9 +++++++++ .../org/kframework/backend/llvm/LLVMBackend.java | 8 ++++++-- .../backend/llvm/LLVMKompileOptions.java | 7 +++++++ pyk/src/pyk/__main__.py | 5 +++++ pyk/src/pyk/cli/args.py | 10 ++++++++++ pyk/src/pyk/ktool/kompile.py | 6 ++++++ 10 files changed, 56 insertions(+), 2 deletions(-) create mode 100644 k-distribution/tests/regression-new/proof-instrumentation-debug/.gitignore create mode 100644 k-distribution/tests/regression-new/proof-instrumentation-debug/Makefile create mode 100644 k-distribution/tests/regression-new/proof-instrumentation-debug/input.test create mode 100644 k-distribution/tests/regression-new/proof-instrumentation-debug/input.test.out create mode 100644 k-distribution/tests/regression-new/proof-instrumentation-debug/test.k diff --git a/k-distribution/tests/regression-new/proof-instrumentation-debug/.gitignore b/k-distribution/tests/regression-new/proof-instrumentation-debug/.gitignore new file mode 100644 index 00000000000..c75c8d9c4ad --- /dev/null +++ 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 new file mode 100644 index 00000000000..933fb619bce --- /dev/null +++ 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 new file mode 100644 index 00000000000..eb28ef4401b --- /dev/null +++ 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 new file mode 100644 index 0000000000000000000000000000000000000000..0bc6c9ed61a90b495a0a08aa9855d3335195c717 GIT binary patch literal 1521 zcmb_cy-ve05VrZ5m|$i=2+31W%GeDRDMX>DK!6RDrXC8Z9i`5M5D&nc@CrN&&jLRG zgd|O%sd|GQ+vo4T`|g}`|1#V`2z?kEo{o-bLT8i-bTLlIEt||o)07g2I9}+$lDxbk z^kwWXpSR%p1V2b{JeLF7fKn}acmcQ|7Ox@U%5N&~Q5u}`A&ZauQ z8^KdDjM92e<$cSp5_4O|EF;F8#nG>3fT_f5RI7Tbasa#z$yiRS+^yuXoOY#hPo;Do zWi*QforF9c&?Eu%Rv>?9Y%FsJ!+Jt@QRYK|IzZM428NZ}1;c7;X~l-ldT6B?f1gZ@#jdQ1EE!M~JhyHf}0lxxc~wUVp}uF`qM!&Kmp zQ2$~JU&*BnZtL;BSdT#0x42i*rqZVao-;u+(-pl1=*U3Z>D!p12KC3AFf@=<&4DRg sw0+_t%NSGz+t3p 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 index 295e760e86a..ef6b1d4246c 100644 --- 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 index 3646c96efc6..282b58c2f08 100644 --- 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 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 index 4ad22390628..04138b86b44 100644 --- 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 index 3dbea7e72a6..468f7da072a 100644 --- 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 index 6d2f7a87f9e..7b87dc62c5f 100644 --- 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']