add --proof-hint flag to krun (#4405)

We add a new command line flag to the krun script which will tell krun
to suppress the usual output and provide the user with a proof hint.

k-distribution/src/main/scripts/bin/krun

@@ -25,6 +25,7 @@ literal=false
 outputMode=pretty
 statistics=false
 executeToBranch=false
+proofHint=false
 smtPrelude=
 smt=
 smtTimeout=
@@ -152,6 +153,8 @@ $KRUN options:
                            also be used without --search to match the output
                            configuration against a pattern and print the
                            substitution. Not supported on LLVM backend.
+      --proof-hint         Generate proof hint instead of final configuration.
+                           Ignores \`--output\`.
       --save-temps         Do not delete temporary files when $KRUN terminates.
       --search             Search for all possible output states after
                            rewriting. Only supported on symbolic backends.
@@ -326,6 +329,10 @@ do
       fi
       ;;
 
+      --proof-hint)
+      proofHint=true
+      ;;
+
       --search)
       search=true
       searchType='FINAL'
@@ -579,6 +586,10 @@ if [ "$backendName" = "llvm" ]; then
     interpreter_flags+=" --execute-to-branch"
   fi
 
+  if $proofHint; then
+    interpreter_flags+=" --proof-output"
+  fi
+
   keepTempsIfDryRun "$tempDir" "$expanded_input_file" "$kore_output"
   if $search || [ -n "$pattern" ]; then
     if [ ! -f "$kompiledDir/search" ] || [ ! -x "$kompiledDir/search" ]; then
@@ -684,6 +695,11 @@ else
   error 1 "Backend $backendName not supported."
 fi
 
+if $proofHint; then
+  output "$outputFile" execute cat "$kore_output"
+  exit ${result}
+fi
+
 # Unparsing
 if ! $dryRun; then
   if [ -f "$kore_output" ]; then

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

@@ -1,22 +1,11 @@
 DEF=test
+EXT=test
+TESTDIR=.
 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 $< > $@
+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
-
-update-results: CHECK=> test.out