diff --git a/src/Printer.h b/src/Printer.h index fb06350..f2f4127 100644 --- 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 index 18007b3..07a93eb 100644 --- a/src/main.cpp +++ b/src/main.cpp @@ -1,4 +1,5 @@ #include +#include #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 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::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 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; + } }