Merge branch 'develop' into _update-deps/runtimeverification/llvm-bac…

…kend

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;
 }

nix/k.nix

@@ -1,7 +1,7 @@
 { src, maven, mvnHash, manualMvnArtifacts, clang, stdenv, lib, runCommand
 , makeWrapper, bison, flex, gcc, git, gmp, jdk, jre, jre_minimal, mpfr, ncurses
 , pkgconfig, python3, z3, haskell-backend, booster, prelude-kore, llvm-backend
-, debugger, version, llvm-kompile-libs }:
+, debugger, version, llvm-kompile-libs, runtimeShell }:
 
 let
   runtimeInputs = [
@@ -26,6 +26,13 @@ let
     llvm-backend
   ] ++ lib.optional (debugger != null) debugger;
   runtimePath = lib.makeBinPath runtimeInputs;
+
+  which-python = ''
+      #!${runtimeShell}
+      echo "${lib.makeBinPath [python3]}/python3"
+      '';
+
+
   k = current-llvm-kompile-libs:
     maven.buildMavenPackage rec {
       pname = "k";
@@ -46,6 +53,9 @@ let
       installPhase = ''
         mkdir -p $out/bin-unwrapped
         mkdir -p $out/bin
+        echo -n "${which-python}" > $out/bin/k-which-python
+        chmod +x $out/bin/k-which-python
+
         cp -r k-distribution/target/release/k/bin/* $out/bin-unwrapped/
         cp -r k-distribution/target/release/k/{include,lib} $out/