Verify ir during CI (#1145)

I noticed to my dismay that a recent PR had introduced code that passed
tests, but was generating LLVM IR that did not pass the verification
process. This PR does two things:

1. Fixes the bug in the code generator that was leading to code that did
not verify.
2. Introduces code to the regression test suite to test that every
definition we compile generates IR that is valid.

Author: Dwight Guth

bin/llvm-kompile

@@ -44,6 +44,7 @@ Options:
                                     "hidden"
   --profile-matching                Instrument interpeter to emit a profile of time spent in
                                     top-level rule matching on stderr.
+  --verify-ir                       Verify result of IR generation.
   -O[0123]                          Set the optimization level for code generation.
 
 Any option not listed above will be passed through to clang; use '--' to
@@ -89,6 +90,7 @@ llvm_major_version () {
 positional_args=()
 reading_clang_args=false
 codegen_flags=()
+codegen_verify_flags=()
 if [[ -z "${NIX_LLVM_KOMPILE_LIBS}" ]]; then
   kompile_clang_flags=()
 else
@@ -105,6 +107,7 @@ embedded_files=()
 embedded_names=()
 use_opt=false
 emit_ir=false
+verify_ir=false
 frame_pointer=false
 
 export verbose=false
@@ -175,23 +178,32 @@ while [[ $# -gt 0 ]]; do
       ;;
     --proof-hint-instrumentation)
       codegen_flags+=("--proof-hint-instrumentation")
+      codegen_verify_flags+=("--proof-hint-instrumentation")
       shift
       ;;
     --proof-hint-instrumentation-slow)
       codegen_flags+=("--proof-hint-instrumentation-slow")
+      codegen_verify_flags+=("--proof-hint-instrumentation-slow")
       shift
       ;;
     --mutable-bytes)
       codegen_flags+=("--mutable-bytes")
+      codegen_verify_flags+=("--mutable-bytes")
       shift
       ;;
     --hidden-visibility)
       codegen_flags+=("--hidden-visibility")
+      codegen_verify_flags+=("--hidden-visibility")
       kompile_clang_flags+=("--hidden-visibility")
       shift
       ;;
     --profile-matching)
       codegen_flags+=("--profile-matching")
+      codegen_verify_flags+=("--profile-matching")
+      shift
+      ;;
+    --verify-ir)
+      verify_ir=true
       shift
       ;;
     -O*)
@@ -236,17 +248,19 @@ if [[ "$emit_ir" == "false" ]]; then
   codegen_flags+=("--emit-object")
   if [[ "$frame_pointer" == "true" ]]; then
     codegen_flags+=("-fno-omit-frame-pointer")
+    codegen_verify_flags+=("-fno-omit-frame-pointer")
   fi
 else
   codegen_flags+=("--binary-ir")
 fi
 
 mod="$(mktemp tmp.XXXXXXXXXX)"
+modtmp="$(mktemp tmp.XXXXXXXXXX)"
 modopt_tmp="$(mktemp tmp.XXXXXXXXXX)"
 tmpdir="$(mktemp -d tmp.XXXXXXXXXX)"
 modopt="$modopt_tmp"
 if [ "$save_temps" = false ]; then
-  trap 'rm -rf "$mod" "$modopt_tmp" "$tmpdir"' INT TERM EXIT
+  trap 'rm -rf "$mod" "$modtmp" "$modopt_tmp" "$tmpdir"' INT TERM EXIT
 fi
 
 definition="${positional_args[0]}"
@@ -271,19 +285,27 @@ if [[ "$compile" = "default" ]]; then
   # flag.
   if [[ "$main" = "c" ]] || [[ "$main" = "python" ]]; then
     codegen_flags+=("--safe-partial")
+    codegen_verify_flags+=("--safe-partial")
   fi
 
   for arg in "${clang_args[@]}"; do
     case "$arg" in
       -g)
         codegen_flags+=("--debug")
+        codegen_verify_flags+=("--debug")
         ;;
     esac
   done
 
   run "$(dirname "$0")"/llvm-kompile-codegen "${codegen_flags[@]}" \
     "$definition" "$dt_dir"/dt.yaml "$dt_dir" -o "$mod"
 
+  if [[ "$verify_ir" == "true" ]]; then
+    run "$(dirname "$0")"/llvm-kompile-codegen "${codegen_verify_flags[@]}" \
+      "$definition" "$dt_dir"/dt.yaml "$dt_dir" -o "$modtmp" --no-optimize
+    run @OPT@ -passes=verify "$modtmp" -o /dev/null
+  fi
+
   if [[ "$use_opt" = "true" ]]; then
     if [ "$(llvm_major_version)" -ge "16" ]; then
       run @OPT@ -passes='mem2reg,tailcallelim' "$mod" -o "$modopt"

bin/llvm-kompile-testing

@@ -41,4 +41,4 @@ while [ $# -gt 0 ]; do
   shift
 done
 
-llvm-kompile "$definition" "$dt_dir" "$mode" "${llvm_kompile_flags[@]}" "${clang_flags[@]}" -g
+llvm-kompile "$definition" "$dt_dir" "$mode" "${llvm_kompile_flags[@]}" "${clang_flags[@]}" -g --verify-ir

lib/codegen/CreateTerm.cpp

@@ -730,7 +730,7 @@ llvm::Value *create_term::create_hook(
 
     // These do not short circuit when the first argument is true.
     current_block_ = e.short_circuit_hook_argument(
-        args[1], args[0], false, sort_1, current_block_);
+        result, args[0], false, sort_1, current_block_);
   } else if (name == "BOOL.or" || name == "BOOL.orElse") {
     auto const &p = pattern->get_arguments();
     auto *sort_0 = dynamic_cast<kore_composite_sort *>(p[0]->get_sort().get());
@@ -740,7 +740,7 @@ llvm::Value *create_term::create_hook(
 
     // These do not short circuit when the first argument is false.
     current_block_ = e.short_circuit_hook_argument(
-        args[1], args[0], true, sort_1, current_block_);
+        result, args[0], true, sort_1, current_block_);
   } else if (name == "KEQUAL.ite") {
     auto const &p = pattern->get_arguments();
     auto *sort_0 = dynamic_cast<kore_composite_sort *>(p[0]->get_sort().get());
@@ -752,7 +752,7 @@ llvm::Value *create_term::create_hook(
     // The second argument does not short circuit when the first argument is true, while
     // the third argument does not short circuit when the first argument is false.
     current_block_ = e.short_circuit_hook_argument(
-        args[1], args[2], args[0], sort_1, sort_2, current_block_);
+        result, result, args[0], sort_1, sort_2, current_block_);
   } else {
     size_t i = 0;
     for (auto const &p : pattern->get_arguments()) {