Merge remote-tracking branch 'origin/develop'

Author: rv-auditor

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()) {