Improve test harness and test coverage for proof hints (#1046)

Previously the tests for proof hints were rather anemic, not to mention
somewhat non-standard. We make the following changes in order to
canonify a technique for testing proof hints, and also expand the test
coverage of this code path:

1. We remove the kore-proof-hint-test binary which appears to be written
with the intent of being used in one specific integration test. This
seems to be duplicated logic with the test_proof_hint.py python tests,
and I don't see the need to maintain a specific C++ binary just for one
test. We also remove the test associated with this binary since it
appears to be redundant.
2. We clean up the infrastructure for how we test proof hints. We no
longer test proof hints without passing --expand-terms, since this
exposes information that is not particularly meaningful and makes the
tests flaky, like the number of bytes in each kore term in the trace,
which may be subject to change.
3. We codify a set of techniques for testing proof hints. Any test which
uses `%interpreter` and `%check-diff` can be extended by adding the
lines `%proof-interpreter` and `%check-proof-out` to the exact same kore
definition. This allows us to reuse kore files and input files and test
the same tests both with and without the proof hint.
4. We add the proof hint testing harness to a small selection of more
complex tests in the tests directory. If regressions occur in the
future, we can extend the number of tests we do this with, and we can
selectively choose to enable this test coverage on new integration tests
that we create very easily. We do not enable this on all tests because
it does not scale well to long execution traces due to the fact that
this would require very large expected output files to be stored in
source control.

---------

Co-authored-by: rv-jenkins <[email protected]>

Author: Dwight Guth

bin/llvm-kompile-clang

@@ -256,7 +256,7 @@ if $link; then
       mkdir -p "$python_path"
 
       script_name="$(basename "$output_file").py"
-      cp "$LIBDIR/lldb/klldb.py" "$python_path/$script_name"
+      cp -f "$LIBDIR/lldb/klldb.py" "$python_path/$script_name"
     fi
   fi
 fi

test/defn/imp-slow-proof.kore renamed to test/defn/imp-sum-slow.kore

@@ -1,6 +1,5 @@
 // RUN: %proof-slow-interpreter
 // RUN: %check-proof-out
-// RUN: %check-expanded-proof-out
 [topCellInitializer{}(LblinitGeneratedTopCell{}()), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/llvm-backend/src/main/native/llvm-backend/test/defn/k-files/imp.md)")]
 
 module BASIC-K

test/defn/imp-proof.kore renamed to test/defn/imp-sum.kore

@@ -1,6 +1,5 @@
 // RUN: %proof-interpreter
 // RUN: %check-proof-out
-// RUN: %check-expanded-proof-out
 [topCellInitializer{}(LblinitGeneratedTopCell{}()), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/llvm-backend/src/main/native/llvm-backend/test/defn/k-files/imp.md)")]
 
 module BASIC-K

test/defn/imp.kore

@@ -1,5 +1,7 @@
 // RUN: %interpreter
 // RUN: %check-grep
+// RUN: %proof-interpreter
+// RUN: %check-proof-out
 [topCellInitializer{}(LblinitGeneratedTopCell{}()), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/llvm-backend/src/main/native/llvm-backend/test/defn/k-files/imp.md)")]
 
 module BASIC-K

test/defn/kool-static.kore

@@ -1,5 +1,7 @@
 // RUN: %interpreter
 // RUN: %check-diff
+// RUN: %proof-interpreter
+// RUN: %check-proof-out
 [topCellInitializer{}(LblinitGeneratedTopCell{}()), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework-5.0.0/k-distribution/pl-tutorial/2_languages/2_kool/2_typed/2_static/kool-typed-static.md)")]
 
 module BASIC-K

test/defn/test-proof-trace-slow.kore

@@ -151,17 +151,7 @@ def one_line(s):
 
     ('%check-proof-out', one_line('''
         %run-proof-out
-        %kore-proof-trace --verbose %t.out.bin | diff - %test-proof-diff-out
-        result="$?"
-        if [ "$result" -ne 0 ]; then
-            echo "kore-proof-trace error while parsing proof hint trace"
-            exit 1
-        fi
-    ''')),
-
-    ('%check-expanded-proof-out', one_line('''
-        %run-proof-out
-        %kore-proof-trace --verbose --expand-terms %t.out.bin | diff - %test-proof-expanded-diff-out
+        %kore-proof-trace --verbose --expand-terms %t.out.bin | diff - %test-proof-diff-out
         result="$?"
         if [ "$result" -ne 0 ]; then
             echo "kore-proof-trace error while parsing proof hint trace with expanded kore terms"
@@ -185,16 +175,14 @@ def one_line(s):
     ('%test-diff-out', os.path.join('%output-dir', '%test-basename.out.diff')),
     ('%test-dir-out', os.path.join('%output-dir', '%test-basename')),
     ('%test-dir-in', os.path.join('%input-dir', '%test-basename')),
-    ('%test-proof-diff-out', os.path.join('%output-dir', '%test-basename', '%test-basename.out.diff')),
-    ('%test-proof-expanded-diff-out', os.path.join('%output-dir', '%test-basename', '%test-basename.expanded.out.diff')),
+    ('%test-proof-diff-out', os.path.join('%output-dir', '%test-basename.proof.out.diff')),
     ('%test-basename', '`basename %s .kore`'),
 
     ('%allow-pipefail', 'set +o pipefail'),
 
     ('%kore-convert', 'kore-convert'),
 
     ('%kore-proof-trace', 'kore-proof-trace'),
-    ('%kore-proof-trace-test', 'kore-proof-trace-test'),
 ])
 
 config.recursiveExpansionLimit = 10