add reverse verify if the source cpp module is UB; update Printer

xzhseh · Oct 25, 2024 · 3150b36 · 3150b36
1 parent fb7ba13
commit 3150b36
Show file tree

Hide file tree

Showing 2 changed files with 56 additions and 17 deletions.
diff --git a/src/Printer.h b/src/Printer.h
@@ -5,17 +5,39 @@
 
 #include "llvm_util/compare.h"
 
+#define BOLD_YELLOW "\033[1;33m"
+#define BOLD_GREEN "\033[1;32m"
+#define BOLD_RED "\033[1;31m"
+#define BOLD_BLUE "\033[1;34m"
+#define RESET_COLOR "\033[0m"
+
 class Printer {
 public:
     explicit Printer(std::ostream &os) : os(os) {}
 
     /// print verification summary
     void print_summary(const llvm_util::Verifier &verifier) const {
-        os << "----------------------------------------\n";
-        os << "summary:\n"
-           << "  " << verifier.num_correct << " correct translations\n"
-           << "  " << verifier.num_unsound << " incorrect translations\n"
-           << "  " << verifier.num_failed << " failed to prove\n";
+        os << BOLD_BLUE << "========================================\n";
+        os << "SUMMARY:\n"
+           << "  " << BOLD_GREEN << verifier.num_correct << " correct translations\n"
+           << "  " << BOLD_RED << verifier.num_unsound << " incorrect translations\n"
+           << "  " << BOLD_YELLOW << verifier.num_failed << " failed to prove\n";
+        os << RESET_COLOR;
+    }
+
+    void print_src_ub_prompt() const {
+        os << BOLD_YELLOW
+           << "*********************************************************************\n"
+           << "* NOTE: undefined behavior detected in the source cpp module,       *\n"
+           << "*       switching the order of modules and verifying again.         *\n"
+           << "*********************************************************************\n"
+           << RESET_COLOR;
+    }
+
+    void print_error(const std::string &module_name,
+                     const std::string &message) const {
+        os << BOLD_RED << "[" << module_name << "] " << message << RESET_COLOR
+           << "\n";
     }
 
 private:

diff --git a/src/main.cpp b/src/main.cpp
@@ -1,4 +1,5 @@
 #include <iostream>
+#include <sstream>
 
 #include "llvm_util/compare.h"
 #include "llvm_util/llvm2alive.h"
@@ -29,6 +30,7 @@ using namespace std;
 
 constexpr auto CPP_MANGLING_PREFIX = "_Z";
 constexpr auto RUST_MANGLING_PREFIX = "_ZN";
+constexpr auto SRC_UB_PROMPT = "WARNING: Source function is always UB";
 
 #include "Comparer.h"
 #include "Printer.h"
@@ -57,10 +59,6 @@ llvm::cl::opt<std::string> opt_rust_pattern {
 
 }  // namespace
 
-void print_error(const std::string &message) {
-    std::cerr << "[main] " << message << "\n";
-}
-
 auto open_input_file(llvm::LLVMContext &context,
                      const std::string &path) -> std::unique_ptr<llvm::Module> {
     llvm::SMDiagnostic err {};
@@ -80,19 +78,20 @@ int main(int argc, char *argv[]) {
     llvm::InitLLVM init_llvm { argc, argv };
     llvm::EnableDebugBuffering = true;
     llvm::LLVMContext context {};
+    Printer printer { std::cout };
 
     // preprocess the command line arguments
     Preprocessor preprocessor { argc, argv };
     std::vector<char *> preprocessed_argv { argv[0] };
     if (!preprocessor.process(preprocessed_argv)) {
-        print_error("preprocess failed");
+        printer.print_error("main", "preprocess failed");
         return EXIT_FAILURE;
     }
 
     auto cpp_module = open_input_file(context, preprocessed_argv[1]);
     auto rust_module = open_input_file(context, preprocessed_argv[2]);
     if (!cpp_module || !rust_module) {
-        print_error("failed to open input files");
+        printer.print_error("main", "failed to open input files");
         return EXIT_FAILURE;
     }
 
@@ -109,14 +108,32 @@ int main(int argc, char *argv[]) {
 
     // set up the verifier to compare the cpp and rust functions in llvm ir
     // level.
-    llvm_util::Verifier verifier {target_library_info, smt_initializer, std::cout };
+    std::stringstream verifier_buffer {};
+    llvm_util::Verifier verifier { target_library_info, smt_initializer,
+                                  verifier_buffer };
 
-    Comparer comparer {*cpp_module, *rust_module, opt_cpp_pattern,
+    Comparer comparer { *cpp_module, *rust_module, opt_cpp_pattern,
                       opt_rust_pattern, verifier };
     auto results = comparer.compare();
 
-    Printer printer { std::cout };
-    printer.print_summary(verifier);
-
-    return verifier.num_errors > 0;
+    // check for source undefined behavior
+    std::string verifier_output { verifier_buffer.str() };
+    if (verifier_output.find(SRC_UB_PROMPT) != std::string::npos) {
+        printer.print_src_ub_prompt();
+
+        llvm_util::Verifier reversed_verifier { target_library_info,
+                                                 smt_initializer,
+                                                 std::cout };
+
+        // Switch the order of modules
+        Comparer reversed_comparer { *rust_module, *cpp_module, opt_rust_pattern,
+                                       opt_cpp_pattern, reversed_verifier };
+        auto reversed_results = reversed_comparer.compare();
+
+        printer.print_summary(reversed_verifier);
+        return reversed_verifier.num_errors > 0;
+    } else {
+        printer.print_summary(verifier);
+        return verifier.num_errors > 0;
+    }
 }