stub out a translation validation plugin for LLVM
MODIFY
CMakeLists.txt
CMakeLists.txt
@@ -97,6 +97,9 @@ else()
endif()
if (BUILD_TV)
+ if (CYGWIN)
+ message(FATAL_ERROR "LLVM plugins not supported on cygwin")
+ endif()
message(STATUS "Compiling translation validation plugin")
add_subdirectory(tv)
else()

ADD
tv/CMakeLists.txt
+find_package(LLVM REQUIRED CONFIG)
+
+message(STATUS "Found LLVM ${LLVM_PACKAGE_VERSION}")
+message(STATUS "Using LLVMConfig.cmake in: ${LLVM_DIR}")
+
+if (NOT LLVM_ENABLE_RTTI OR NOT LLVM_ENABLE_EH)
+ message(FATAL_ERROR "LLVM must be built with '-DLLVM_ENABLE_ASSERTIONS=ON -DLLVM_ENABLE_RTTI=ON'")
+endif()
+
+list(APPEND CMAKE_MODULE_PATH "${LLVM_CMAKE_DIR}")
+include(AddLLVM)
+
+include_directories(${LLVM_INCLUDE_DIRS})
+add_definitions(${LLVM_DEFINITIONS})
+
+add_llvm_loadable_module(tv tv.cpp)
+
+target_link_libraries(tv ${ALIVE_LIBS} ${Z3_LIBRARIES})

ADD
tv/tv.cpp
+// Copyright (c) 2018-present The Alive2 Authors.
+// Distributed under the MIT license that can be found in the LICENSE file.
+
+#include "ir/function.h"
+#include "smt/smt.h"
+#include "smt/solver.h"
+#include "tools/transform.h"
+#include "util/config.h"
+#include "llvm/IR/Function.h"
+#include "llvm/Pass.h"
+#include "llvm/Support/raw_ostream.h"
+
+using namespace IR;
+using namespace tools;
+using namespace util;
+using namespace std;
+using namespace llvm;
+
+namespace {
+
+struct TVPass : public FunctionPass {
+ static char ID;
+
+ //smt::smt_initializer smt_init; move out
+ //TransformPrintOpts print_opts;
+ bool FatalErrors = true;
+
+ TVPass() : FunctionPass(ID) {}
+
+ bool runOnFunction(llvm::Function &F) override {
+ outs() << "verifying " << F.getName() << '\n';
+ if (/* !V->verify(F)*/ false && FatalErrors) {
+ errs() << "in function " << F.getName() << '\n';
+ report_fatal_error("Broken function found, compilation aborted!");
+ }
+ return false;
+ }
+
+ void getAnalysisUsage(AnalysisUsage &AU) const override {
+ AU.setPreservesAll();
+ }
+};
+
+}
+
+char TVPass::ID = 0;
+static RegisterPass<TVPass> X("tv", "Translation Validator", false, false);

stub out a translation validation plugin for LLVM