Add proof hint generation flag (#3821)

This flag exists in `llvm-kompile` already, but we want consumers that
compile via the K frontend to be able to use the proof hint
instrumentation feature.

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

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

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

@@ -0,0 +1,22 @@
+DEF=test
+KOMPILE_BACKEND=llvm
+KOMPILE_FLAGS+=--gen-glr-bison-parser --llvm-proof-hint-instrumentation
+LLVM_KRUN_FLAGS=-d ./test-kompiled --proof-hints
+
+check: out.hint
+	head -c4 out.hint | diff - <(echo -n 'HINT')
+
+out.hint: test.kore
+	rm -f $@
+	$(LLVM_KRUN) $(LLVM_KRUN_FLAGS) \
+		-c PGM $< Foo korefile -o $@
+
+test.kore: test.in kompile
+	./test-kompiled/parser_PGM $< > $@
+
+include ../../../include/kframework/ktest.mak
+
+clean:
+	rm -rf out.hint test.kore $(KOMPILED_DIR) .depend-tmp .depend .kompile-* .krun-* .kprove-* kore-exec.tar.gz
+
+update-results: CHECK=> test.out

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

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

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

@@ -0,0 +1,9 @@
+// Copyright (c) K Team. 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

@@ -124,6 +124,10 @@ private void llvmKompile(String type, String executable) {
       args.add(files.resolveKompiled("dt").getCanonicalPath());
       args.add(type);
 
+      if (options.enableProofHints) {
+        args.add("--proof-hint-instrumentation");
+      }
+
       // Arguments after this point are passed on to Clang.
       args.add("--");
 

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

@@ -100,4 +100,10 @@ public List<String> convert(String str) {
       descriptionKey = "file",
       hidden = true)
   public String llvmKompileOutput = null;
+
+  @Parameter(
+      names = "--llvm-proof-hint-instrumentation",
+      description = "Emit proof hint instrumentation code into the generated interpreter",
+      hidden = true)
+  public boolean enableProofHints;
 }