mikhail.ramalho updated this revision to Diff 191305. mikhail.ramalho added a comment.
Fix copy-and-paste error. CHANGES SINCE LAST ACTION https://reviews.llvm.org/D54978/new/ https://reviews.llvm.org/D54978 Files: clang/CMakeLists.txt clang/cmake/modules/FindZ3.cmake clang/include/clang/Config/config.h.cmake clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTAPI.h clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h clang/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp clang/lib/StaticAnalyzer/Core/CMakeLists.txt clang/lib/StaticAnalyzer/Core/SMTConstraintManager.cpp clang/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp clang/test/CMakeLists.txt clang/test/lit.site.cfg.py.in llvm/CMakeLists.txt llvm/cmake/modules/FindZ3.cmake llvm/cmake/modules/LLVMConfig.cmake.in llvm/include/llvm/Config/config.h.cmake llvm/include/llvm/Support/SMTAPI.h llvm/lib/Support/CMakeLists.txt llvm/lib/Support/Z3Solver.cpp
Index: llvm/lib/Support/Z3Solver.cpp =================================================================== --- llvm/lib/Support/Z3Solver.cpp +++ llvm/lib/Support/Z3Solver.cpp @@ -1,4 +1,4 @@ -//== Z3ConstraintManager.cpp --------------------------------*- C++ -*--==// +//== Z3Solver.cpp -----------------------------------------------*- C++ -*--==// // // Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions. // See https://llvm.org/LICENSE.txt for license information. @@ -6,18 +6,14 @@ // //===----------------------------------------------------------------------===// -#include "clang/Basic/TargetInfo.h" -#include "clang/StaticAnalyzer/Core/PathSensitive/ExprEngine.h" -#include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h" -#include "clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h" -#include "clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h" +#include "llvm/ADT/Twine.h" +#include "llvm/Config/config.h" +#include "llvm/Support/SMTAPI.h" +#include <set> -#include "clang/Config/config.h" +using namespace llvm; -using namespace clang; -using namespace ento; - -#if CLANG_ANALYZER_WITH_Z3 +#if LLVM_WITH_Z3 #include <z3.h> @@ -818,18 +814,13 @@ #endif -SMTSolverRef clang::ento::CreateZ3Solver() { -#if CLANG_ANALYZER_WITH_Z3 +llvm::SMTSolverRef llvm::CreateZ3Solver() { +#if LLVM_WITH_Z3 return llvm::make_unique<Z3Solver>(); #else llvm::report_fatal_error("Clang was not compiled with Z3 support, rebuild " - "with -DCLANG_ANALYZER_ENABLE_Z3_SOLVER=ON", + "with -DLLVM_ENABLE_Z3_SOLVER=ON", false); return nullptr; #endif } - -std::unique_ptr<ConstraintManager> -ento::CreateZ3ConstraintManager(ProgramStateManager &StMgr, SubEngine *Eng) { - return llvm::make_unique<SMTConstraintManager>(Eng, StMgr.getSValBuilder()); -} Index: llvm/lib/Support/CMakeLists.txt =================================================================== --- llvm/lib/Support/CMakeLists.txt +++ llvm/lib/Support/CMakeLists.txt @@ -44,6 +44,13 @@ set (delayload_flags delayimp -delayload:shell32.dll -delayload:ole32.dll) endif() +# Link Z3 if the user wants to build it. +if(LLVM_WITH_Z3) + set(Z3_LINK_FILES ${Z3_LIBRARIES}) +else() + set(Z3_LINK_FILES "") +endif() + add_llvm_library(LLVMSupport AArch64TargetParser.cpp ARMTargetParser.cpp @@ -152,6 +159,7 @@ regfree.c regstrlcpy.c xxhash.cpp + Z3Solver.cpp # System Atomic.cpp @@ -177,7 +185,14 @@ ${LLVM_MAIN_INCLUDE_DIR}/llvm/ADT ${LLVM_MAIN_INCLUDE_DIR}/llvm/Support ${Backtrace_INCLUDE_DIRS} - LINK_LIBS ${system_libs} ${delayload_flags} + LINK_LIBS ${system_libs} ${delayload_flags} ${Z3_LINK_FILES} ) set_property(TARGET LLVMSupport PROPERTY LLVM_SYSTEM_LIBS "${system_libs}") + +if(LLVM_WITH_Z3) + target_include_directories(LLVMSupport SYSTEM + PRIVATE + ${Z3_INCLUDE_DIR} + ) +endif() Index: llvm/include/llvm/Support/SMTAPI.h =================================================================== --- llvm/include/llvm/Support/SMTAPI.h +++ llvm/include/llvm/Support/SMTAPI.h @@ -11,15 +11,16 @@ // //===----------------------------------------------------------------------===// -#ifndef LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTSOLVER_H -#define LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTSOLVER_H +#ifndef LLVM_SUPPORT_SMTAPI_H +#define LLVM_SUPPORT_SMTAPI_H -#include "clang/Basic/TargetInfo.h" +#include "llvm/ADT/APFloat.h" #include "llvm/ADT/APSInt.h" #include "llvm/ADT/FoldingSet.h" +#include "llvm/Support/raw_ostream.h" +#include <memory> -namespace clang { -namespace ento { +namespace llvm { /// Generic base class for SMT sorts class SMTSort { @@ -399,7 +400,6 @@ /// Convenience method to create and Z3Solver object SMTSolverRef CreateZ3Solver(); -} // namespace ento -} // namespace clang +} // namespace llvm #endif Index: llvm/include/llvm/Config/config.h.cmake =================================================================== --- llvm/include/llvm/Config/config.h.cmake +++ llvm/include/llvm/Config/config.h.cmake @@ -347,6 +347,9 @@ /* Whether GlobalISel rule coverage is being collected */ #cmakedefine01 LLVM_GISEL_COV_ENABLED +/* Define if we have z3 and want to build it */ +#cmakedefine LLVM_WITH_Z3 ${LLVM_WITH_Z3} + /* Define to the default GlobalISel coverage file prefix */ #cmakedefine LLVM_GISEL_COV_PREFIX "${LLVM_GISEL_COV_PREFIX}" Index: llvm/cmake/modules/LLVMConfig.cmake.in =================================================================== --- llvm/cmake/modules/LLVMConfig.cmake.in +++ llvm/cmake/modules/LLVMConfig.cmake.in @@ -44,6 +44,8 @@ set(LLVM_LIBXML2_ENABLED @LLVM_LIBXML2_ENABLED@) +set(LLVM_WITH_Z3 @LLVM_WITH_Z3@) + set(LLVM_ENABLE_DIA_SDK @LLVM_ENABLE_DIA_SDK@) set(LLVM_NATIVE_ARCH @LLVM_NATIVE_ARCH@) Index: llvm/cmake/modules/FindZ3.cmake =================================================================== --- /dev/null +++ llvm/cmake/modules/FindZ3.cmake @@ -0,0 +1,110 @@ +INCLUDE(CheckCXXSourceRuns) + +# Function to check Z3's version +function(check_z3_version z3_include z3_lib) + # The program that will be executed to print Z3's version. + file(WRITE ${CMAKE_BINARY_DIR}${CMAKE_FILES_DIRECTORY}/CMakeTmp/testz3.c + "#include <assert.h> + #include <z3.h> + int main() { + unsigned int major, minor, build, rev; + Z3_get_version(&major, &minor, &build, &rev); + printf(\"%u.%u.%u\", major, minor, build); + return 0; + }") + + # Get lib path + get_filename_component(z3_lib_path ${z3_lib} PATH) + + try_run( + Z3_RETURNCODE + Z3_COMPILED + ${CMAKE_BINARY_DIR} + ${CMAKE_BINARY_DIR}${CMAKE_FILES_DIRECTORY}/CMakeTmp/testz3.c + COMPILE_DEFINITIONS -I"${z3_include}" + LINK_LIBRARIES -L${z3_lib_path} -lz3 + RUN_OUTPUT_VARIABLE SRC_OUTPUT + ) + + if(Z3_COMPILED) + string(REGEX REPLACE "([0-9]*\\.[0-9]*\\.[0-9]*\\.[0-9]*)" "\\1" + z3_version "${SRC_OUTPUT}") + set(Z3_VERSION_STRING ${z3_version} PARENT_SCOPE) + endif() +endfunction(check_z3_version) + +# Looking for Z3 in LLVM_Z3_INSTALL_DIR +find_path(Z3_INCLUDE_DIR NAMES z3.h + NO_DEFAULT_PATH + PATHS ${LLVM_Z3_INSTALL_DIR}/include + PATH_SUFFIXES libz3 z3 + ) + +find_library(Z3_LIBRARIES NAMES z3 libz3 + NO_DEFAULT_PATH + PATHS ${LLVM_Z3_INSTALL_DIR} + PATH_SUFFIXES lib bin + ) + +# If Z3 has not been found in LLVM_Z3_INSTALL_DIR look in the default directories +find_path(Z3_INCLUDE_DIR NAMES z3.h + PATH_SUFFIXES libz3 z3 + ) + +find_library(Z3_LIBRARIES NAMES z3 libz3 + PATH_SUFFIXES lib bin + ) + +# Searching for the version of the Z3 library is a best-effort task +unset(Z3_VERSION_STRING) + +# First, try to check it dynamically, by compiling a small program that +# prints Z3's version +if(Z3_INCLUDE_DIR AND Z3_LIBRARIES) + # We do not have the Z3 binary to query for a version. Try to use + # a small C++ program to detect it via the Z3_get_version() API call. + check_z3_version(${Z3_INCLUDE_DIR} ${Z3_LIBRARIES}) +endif() + +# If the dynamic check fails, we might be cross compiling: if that's the case, +# check the version in the headers, otherwise, fail with a message +if(NOT Z3_VERSION_STRING AND (CMAKE_CROSSCOMPILING AND + Z3_INCLUDE_DIR AND + EXISTS "${Z3_INCLUDE_DIR}/z3_version.h")) + # TODO: print message warning that we couldn't find a compatible lib? + + # Z3 4.8.1+ has the version is in a public header. + file(STRINGS "${Z3_INCLUDE_DIR}/z3_version.h" + z3_version_str REGEX "^#define[\t ]+Z3_MAJOR_VERSION[\t ]+.*") + string(REGEX REPLACE "^.*Z3_MAJOR_VERSION[\t ]+([0-9]).*$" "\\1" + Z3_MAJOR "${z3_version_str}") + + file(STRINGS "${Z3_INCLUDE_DIR}/z3_version.h" + z3_version_str REGEX "^#define[\t ]+Z3_MINOR_VERSION[\t ]+.*") + string(REGEX REPLACE "^.*Z3_MINOR_VERSION[\t ]+([0-9]).*$" "\\1" + Z3_MINOR "${z3_version_str}") + + file(STRINGS "${Z3_INCLUDE_DIR}/z3_version.h" + z3_version_str REGEX "^#define[\t ]+Z3_BUILD_NUMBER[\t ]+.*") + string(REGEX REPLACE "^.*Z3_BUILD_VERSION[\t ]+([0-9]).*$" "\\1" + Z3_BUILD "${z3_version_str}") + + set(Z3_VERSION_STRING ${Z3_MAJOR}.${Z3_MINOR}.${Z3_BUILD}) + unset(z3_version_str) +endif() + +if(NOT Z3_VERSION_STRING) + # Give up: we are unable to obtain a version of the Z3 library. Be + # conservative and force the found version to 0.0.0 to make version + # checks always fail. + set(Z3_VERSION_STRING "0.0.0") +endif() + +# handle the QUIETLY and REQUIRED arguments and set Z3_FOUND to TRUE if +# all listed variables are TRUE +include(FindPackageHandleStandardArgs) +FIND_PACKAGE_HANDLE_STANDARD_ARGS(Z3 + REQUIRED_VARS Z3_LIBRARIES Z3_INCLUDE_DIR + VERSION_VAR Z3_VERSION_STRING) + +mark_as_advanced(Z3_INCLUDE_DIR Z3_LIBRARIES) Index: llvm/CMakeLists.txt =================================================================== --- llvm/CMakeLists.txt +++ llvm/CMakeLists.txt @@ -377,6 +377,31 @@ option(LLVM_ENABLE_ZLIB "Use zlib for compression/decompression if available." ON) +set(LLVM_Z3_INSTALL_DIR "" CACHE STRING "Install directory of the Z3 solver.") + +find_package(Z3 4.7.1) + +if (LLVM_Z3_INSTALL_DIR) + if (NOT Z3_FOUND) + message(FATAL_ERROR "Z3 >= 4.7.1 has not been found in LLVM_Z3_INSTALL_DIR: ${LLVM_Z3_INSTALL_DIR}.") + endif() +endif() + +set(LLVM_ENABLE_Z3_SOLVER_DEFAULT "${Z3_FOUND}") + +option(LLVM_ENABLE_Z3_SOLVER + "Enable Support for the Z3 constraint solver in LLVM." + ${LLVM_ENABLE_Z3_SOLVER_DEFAULT} +) + +if (LLVM_ENABLE_Z3_SOLVER) + if (NOT Z3_FOUND) + message(FATAL_ERROR "LLVM_ENABLE_Z3_SOLVER cannot be enabled when Z3 is not available.") + endif() + + set(LLVM_WITH_Z3 1) +endif() + if( LLVM_TARGETS_TO_BUILD STREQUAL "all" ) set( LLVM_TARGETS_TO_BUILD ${LLVM_ALL_TARGETS} ) endif() Index: clang/test/lit.site.cfg.py.in =================================================================== --- clang/test/lit.site.cfg.py.in +++ clang/test/lit.site.cfg.py.in @@ -20,7 +20,7 @@ config.clang_arcmt = @CLANG_ENABLE_ARCMT@ config.clang_default_cxx_stdlib = "@CLANG_DEFAULT_CXX_STDLIB@" config.clang_staticanalyzer = @CLANG_ENABLE_STATIC_ANALYZER@ -config.clang_staticanalyzer_z3 = "@CLANG_ANALYZER_WITH_Z3@" +config.clang_staticanalyzer_z3 = "@LLVM_WITH_Z3@" config.clang_examples = @CLANG_BUILD_EXAMPLES@ config.enable_shared = @ENABLE_SHARED@ config.enable_backtrace = @ENABLE_BACKTRACES@ Index: clang/test/CMakeLists.txt =================================================================== --- clang/test/CMakeLists.txt +++ clang/test/CMakeLists.txt @@ -144,7 +144,7 @@ set_target_properties(check-clang-analyzer PROPERTIES FOLDER "Clang tests") - if (CLANG_ANALYZER_WITH_Z3) + if (LLVM_WITH_Z3) add_lit_testsuite(check-clang-analyzer-z3 "Running the Clang analyzer tests, using Z3 as a solver" ${CMAKE_CURRENT_BINARY_DIR}/Analysis PARAMS ${ANALYZER_TEST_PARAMS_Z3} Index: clang/lib/StaticAnalyzer/Core/SMTConstraintManager.cpp =================================================================== --- /dev/null +++ clang/lib/StaticAnalyzer/Core/SMTConstraintManager.cpp @@ -0,0 +1,18 @@ +//== SMTConstraintManager.cpp -----------------------------------*- C++ -*--==// +// +// The LLVM Compiler Infrastructure +// +// This file is distributed under the University of Illinois Open Source +// License. See LICENSE.TXT for details. +// +//===----------------------------------------------------------------------===// + +#include "clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h" + +using namespace clang; +using namespace ento; + +std::unique_ptr<ConstraintManager> +ento::CreateZ3ConstraintManager(ProgramStateManager &StMgr, SubEngine *Eng) { + return llvm::make_unique<SMTConstraintManager>(Eng, StMgr.getSValBuilder()); +} Index: clang/lib/StaticAnalyzer/Core/CMakeLists.txt =================================================================== --- clang/lib/StaticAnalyzer/Core/CMakeLists.txt +++ clang/lib/StaticAnalyzer/Core/CMakeLists.txt @@ -1,12 +1,5 @@ set(LLVM_LINK_COMPONENTS support) -# Link Z3 if the user wants to build it. -if(CLANG_ANALYZER_WITH_Z3) - set(Z3_LINK_FILES ${Z3_LIBRARIES}) -else() - set(Z3_LINK_FILES "") -endif() - add_clang_library(clangStaticAnalyzerCore APSIntType.cpp AnalysisManager.cpp @@ -46,6 +39,7 @@ SarifDiagnostics.cpp SimpleConstraintManager.cpp SimpleSValBuilder.cpp + SMTConstraintManager.cpp Store.cpp SubEngine.cpp SValBuilder.cpp @@ -53,7 +47,6 @@ SymbolManager.cpp TaintManager.cpp WorkList.cpp - Z3ConstraintManager.cpp LINK_LIBS clangAST @@ -63,12 +56,5 @@ clangCrossTU clangLex clangRewrite - ${Z3_LINK_FILES} ) -if(CLANG_ANALYZER_WITH_Z3) - target_include_directories(clangStaticAnalyzerCore SYSTEM - PRIVATE - ${Z3_INCLUDE_DIR} - ) -endif() Index: clang/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp =================================================================== --- clang/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp +++ clang/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp @@ -2442,7 +2442,7 @@ VisitNode(EndPathNode, BRC, BR); // Create a refutation manager - SMTSolverRef RefutationSolver = CreateZ3Solver(); + llvm::SMTSolverRef RefutationSolver = llvm::CreateZ3Solver(); ASTContext &Ctx = BRC.getASTContext(); // Add constraints to the solver @@ -2450,7 +2450,7 @@ const SymbolRef Sym = I.first; auto RangeIt = I.second.begin(); - SMTExprRef Constraints = SMTConv::getRangeExpr( + llvm::SMTExprRef Constraints = SMTConv::getRangeExpr( RefutationSolver, Ctx, Sym, RangeIt->From(), RangeIt->To(), /*InRange=*/true); while ((++RangeIt) != I.second.end()) { Index: clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h =================================================================== --- clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h +++ clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h @@ -15,8 +15,8 @@ #include "clang/AST/Expr.h" #include "clang/StaticAnalyzer/Core/PathSensitive/APSIntType.h" -#include "clang/StaticAnalyzer/Core/PathSensitive/SMTAPI.h" #include "clang/StaticAnalyzer/Core/PathSensitive/SymbolManager.h" +#include "llvm/Support/SMTAPI.h" namespace clang { namespace ento { @@ -24,8 +24,8 @@ class SMTConv { public: // Returns an appropriate sort, given a QualType and it's bit width. - static inline SMTSortRef mkSort(SMTSolverRef &Solver, const QualType &Ty, - unsigned BitWidth) { + static inline llvm::SMTSortRef mkSort(llvm::SMTSolverRef &Solver, + const QualType &Ty, unsigned BitWidth) { if (Ty->isBooleanType()) return Solver->getBoolSort(); @@ -35,10 +35,10 @@ return Solver->getBitvectorSort(BitWidth); } - /// Constructs an SMTExprRef from an unary operator. - static inline SMTExprRef fromUnOp(SMTSolverRef &Solver, - const UnaryOperator::Opcode Op, - const SMTExprRef &Exp) { + /// Constructs an SMTSolverRef from an unary operator. + static inline llvm::SMTExprRef fromUnOp(llvm::SMTSolverRef &Solver, + const UnaryOperator::Opcode Op, + const llvm::SMTExprRef &Exp) { switch (Op) { case UO_Minus: return Solver->mkBVNeg(Exp); @@ -54,10 +54,10 @@ llvm_unreachable("Unimplemented opcode"); } - /// Constructs an SMTExprRef from a floating-point unary operator. - static inline SMTExprRef fromFloatUnOp(SMTSolverRef &Solver, - const UnaryOperator::Opcode Op, - const SMTExprRef &Exp) { + /// Constructs an SMTSolverRef from a floating-point unary operator. + static inline llvm::SMTExprRef fromFloatUnOp(llvm::SMTSolverRef &Solver, + const UnaryOperator::Opcode Op, + const llvm::SMTExprRef &Exp) { switch (Op) { case UO_Minus: return Solver->mkFPNeg(Exp); @@ -70,27 +70,28 @@ llvm_unreachable("Unimplemented opcode"); } - /// Construct an SMTExprRef from a n-ary binary operator. - static inline SMTExprRef fromNBinOp(SMTSolverRef &Solver, - const BinaryOperator::Opcode Op, - const std::vector<SMTExprRef> &ASTs) { + /// Construct an SMTSolverRef from a n-ary binary operator. + static inline llvm::SMTExprRef + fromNBinOp(llvm::SMTSolverRef &Solver, const BinaryOperator::Opcode Op, + const std::vector<llvm::SMTExprRef> &ASTs) { assert(!ASTs.empty()); if (Op != BO_LAnd && Op != BO_LOr) llvm_unreachable("Unimplemented opcode"); - SMTExprRef res = ASTs.front(); + llvm::SMTExprRef res = ASTs.front(); for (std::size_t i = 1; i < ASTs.size(); ++i) res = (Op == BO_LAnd) ? Solver->mkAnd(res, ASTs[i]) : Solver->mkOr(res, ASTs[i]); return res; } - /// Construct an SMTExprRef from a binary operator. - static inline SMTExprRef fromBinOp(SMTSolverRef &Solver, - const SMTExprRef &LHS, - const BinaryOperator::Opcode Op, - const SMTExprRef &RHS, bool isSigned) { + /// Construct an SMTSolverRef from a binary operator. + static inline llvm::SMTExprRef fromBinOp(llvm::SMTSolverRef &Solver, + const llvm::SMTExprRef &LHS, + const BinaryOperator::Opcode Op, + const llvm::SMTExprRef &RHS, + bool isSigned) { assert(*Solver->getSort(LHS) == *Solver->getSort(RHS) && "AST's must have the same sort!"); @@ -162,9 +163,10 @@ llvm_unreachable("Unimplemented opcode"); } - /// Construct an SMTExprRef from a special floating-point binary operator. - static inline SMTExprRef - fromFloatSpecialBinOp(SMTSolverRef &Solver, const SMTExprRef &LHS, + /// Construct an SMTSolverRef from a special floating-point binary + /// operator. + static inline llvm::SMTExprRef + fromFloatSpecialBinOp(llvm::SMTSolverRef &Solver, const llvm::SMTExprRef &LHS, const BinaryOperator::Opcode Op, const llvm::APFloat::fltCategory &RHS) { switch (Op) { @@ -195,11 +197,11 @@ llvm_unreachable("Unimplemented opcode"); } - /// Construct an SMTExprRef from a floating-point binary operator. - static inline SMTExprRef fromFloatBinOp(SMTSolverRef &Solver, - const SMTExprRef &LHS, - const BinaryOperator::Opcode Op, - const SMTExprRef &RHS) { + /// Construct an SMTSolverRef from a floating-point binary operator. + static inline llvm::SMTExprRef fromFloatBinOp(llvm::SMTSolverRef &Solver, + const llvm::SMTExprRef &LHS, + const BinaryOperator::Opcode Op, + const llvm::SMTExprRef &RHS) { assert(*Solver->getSort(LHS) == *Solver->getSort(RHS) && "AST's must have the same sort!"); @@ -253,11 +255,13 @@ llvm_unreachable("Unimplemented opcode"); } - /// Construct an SMTExprRef from a QualType FromTy to a QualType ToTy, and - /// their bit widths. - static inline SMTExprRef fromCast(SMTSolverRef &Solver, const SMTExprRef &Exp, - QualType ToTy, uint64_t ToBitWidth, - QualType FromTy, uint64_t FromBitWidth) { + /// Construct an SMTSolverRef from a QualType FromTy to a QualType ToTy, + /// and their bit widths. + static inline llvm::SMTExprRef fromCast(llvm::SMTSolverRef &Solver, + const llvm::SMTExprRef &Exp, + QualType ToTy, uint64_t ToBitWidth, + QualType FromTy, + uint64_t FromBitWidth) { if ((FromTy->isIntegralOrEnumerationType() && ToTy->isIntegralOrEnumerationType()) || (FromTy->isAnyPointerType() ^ ToTy->isAnyPointerType()) || @@ -291,7 +295,7 @@ } if (FromTy->isIntegralOrEnumerationType() && ToTy->isRealFloatingType()) { - SMTSortRef Sort = Solver->getFloatSort(ToBitWidth); + llvm::SMTSortRef Sort = Solver->getFloatSort(ToBitWidth); return FromTy->isSignedIntegerOrEnumerationType() ? Solver->mkSBVtoFP(Exp, Sort) : Solver->mkUBVtoFP(Exp, Sort); @@ -306,7 +310,7 @@ } // Callback function for doCast parameter on APSInt type. - static inline llvm::APSInt castAPSInt(SMTSolverRef &Solver, + static inline llvm::APSInt castAPSInt(llvm::SMTSolverRef &Solver, const llvm::APSInt &V, QualType ToTy, uint64_t ToWidth, QualType FromTy, uint64_t FromWidth) { @@ -314,30 +318,32 @@ return TargetType.convert(V); } - /// Construct an SMTExprRef from a SymbolData. - static inline SMTExprRef fromData(SMTSolverRef &Solver, const SymbolID ID, - const QualType &Ty, uint64_t BitWidth) { + /// Construct an SMTSolverRef from a SymbolData. + static inline llvm::SMTExprRef fromData(llvm::SMTSolverRef &Solver, + const SymbolID ID, const QualType &Ty, + uint64_t BitWidth) { llvm::Twine Name = "$" + llvm::Twine(ID); return Solver->mkSymbol(Name.str().c_str(), mkSort(Solver, Ty, BitWidth)); } - // Wrapper to generate SMTExprRef from SymbolCast data. - static inline SMTExprRef getCastExpr(SMTSolverRef &Solver, ASTContext &Ctx, - const SMTExprRef &Exp, QualType FromTy, - QualType ToTy) { + // Wrapper to generate SMTSolverRef from SymbolCast data. + static inline llvm::SMTExprRef getCastExpr(llvm::SMTSolverRef &Solver, + ASTContext &Ctx, + const llvm::SMTExprRef &Exp, + QualType FromTy, QualType ToTy) { return fromCast(Solver, Exp, ToTy, Ctx.getTypeSize(ToTy), FromTy, Ctx.getTypeSize(FromTy)); } - // Wrapper to generate SMTExprRef from unpacked binary symbolic expression. - // Sets the RetTy parameter. See getSMTExprRef(). - static inline SMTExprRef getBinExpr(SMTSolverRef &Solver, ASTContext &Ctx, - const SMTExprRef &LHS, QualType LTy, - BinaryOperator::Opcode Op, - const SMTExprRef &RHS, QualType RTy, - QualType *RetTy) { - SMTExprRef NewLHS = LHS; - SMTExprRef NewRHS = RHS; + // Wrapper to generate SMTSolverRef from unpacked binary symbolic + // expression. Sets the RetTy parameter. See getSMTSolverRef(). + static inline llvm::SMTExprRef + getBinExpr(llvm::SMTSolverRef &Solver, ASTContext &Ctx, + const llvm::SMTExprRef &LHS, QualType LTy, + BinaryOperator::Opcode Op, const llvm::SMTExprRef &RHS, + QualType RTy, QualType *RetTy) { + llvm::SMTExprRef NewLHS = LHS; + llvm::SMTExprRef NewRHS = RHS; doTypeConversion(Solver, Ctx, NewLHS, NewRHS, LTy, RTy); // Update the return type parameter if the output type has changed. @@ -365,36 +371,40 @@ LTy->isSignedIntegerOrEnumerationType()); } - // Wrapper to generate SMTExprRef from BinarySymExpr. - // Sets the hasComparison and RetTy parameters. See getSMTExprRef(). - static inline SMTExprRef getSymBinExpr(SMTSolverRef &Solver, ASTContext &Ctx, - const BinarySymExpr *BSE, - bool *hasComparison, QualType *RetTy) { + // Wrapper to generate SMTSolverRef from BinarySymExpr. + // Sets the hasComparison and RetTy parameters. See getSMTSolverRef(). + static inline llvm::SMTExprRef getSymBinExpr(llvm::SMTSolverRef &Solver, + ASTContext &Ctx, + const BinarySymExpr *BSE, + bool *hasComparison, + QualType *RetTy) { QualType LTy, RTy; BinaryOperator::Opcode Op = BSE->getOpcode(); if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(BSE)) { - SMTExprRef LHS = + llvm::SMTExprRef LHS = getSymExpr(Solver, Ctx, SIE->getLHS(), <y, hasComparison); llvm::APSInt NewRInt; std::tie(NewRInt, RTy) = fixAPSInt(Ctx, SIE->getRHS()); - SMTExprRef RHS = Solver->mkBitvector(NewRInt, NewRInt.getBitWidth()); + llvm::SMTExprRef RHS = + Solver->mkBitvector(NewRInt, NewRInt.getBitWidth()); return getBinExpr(Solver, Ctx, LHS, LTy, Op, RHS, RTy, RetTy); } if (const IntSymExpr *ISE = dyn_cast<IntSymExpr>(BSE)) { llvm::APSInt NewLInt; std::tie(NewLInt, LTy) = fixAPSInt(Ctx, ISE->getLHS()); - SMTExprRef LHS = Solver->mkBitvector(NewLInt, NewLInt.getBitWidth()); - SMTExprRef RHS = + llvm::SMTExprRef LHS = + Solver->mkBitvector(NewLInt, NewLInt.getBitWidth()); + llvm::SMTExprRef RHS = getSymExpr(Solver, Ctx, ISE->getRHS(), &RTy, hasComparison); return getBinExpr(Solver, Ctx, LHS, LTy, Op, RHS, RTy, RetTy); } if (const SymSymExpr *SSM = dyn_cast<SymSymExpr>(BSE)) { - SMTExprRef LHS = + llvm::SMTExprRef LHS = getSymExpr(Solver, Ctx, SSM->getLHS(), <y, hasComparison); - SMTExprRef RHS = + llvm::SMTExprRef RHS = getSymExpr(Solver, Ctx, SSM->getRHS(), &RTy, hasComparison); return getBinExpr(Solver, Ctx, LHS, LTy, Op, RHS, RTy, RetTy); } @@ -404,9 +414,10 @@ // Recursive implementation to unpack and generate symbolic expression. // Sets the hasComparison and RetTy parameters. See getExpr(). - static inline SMTExprRef getSymExpr(SMTSolverRef &Solver, ASTContext &Ctx, - SymbolRef Sym, QualType *RetTy, - bool *hasComparison) { + static inline llvm::SMTExprRef getSymExpr(llvm::SMTSolverRef &Solver, + ASTContext &Ctx, SymbolRef Sym, + QualType *RetTy, + bool *hasComparison) { if (const SymbolData *SD = dyn_cast<SymbolData>(Sym)) { if (RetTy) *RetTy = Sym->getType(); @@ -420,7 +431,7 @@ *RetTy = Sym->getType(); QualType FromTy; - SMTExprRef Exp = + llvm::SMTExprRef Exp = getSymExpr(Solver, Ctx, SC->getOperand(), &FromTy, hasComparison); // Casting an expression with a comparison invalidates it. Note that this @@ -432,7 +443,8 @@ } if (const BinarySymExpr *BSE = dyn_cast<BinarySymExpr>(Sym)) { - SMTExprRef Exp = getSymBinExpr(Solver, Ctx, BSE, hasComparison, RetTy); + llvm::SMTExprRef Exp = + getSymBinExpr(Solver, Ctx, BSE, hasComparison, RetTy); // Set the hasComparison parameter, in post-order traversal order. if (hasComparison) *hasComparison = BinaryOperator::isComparisonOp(BSE->getOpcode()); @@ -442,13 +454,14 @@ llvm_unreachable("Unsupported SymbolRef type!"); } - // Generate an SMTExprRef that represents the given symbolic expression. + // Generate an SMTSolverRef that represents the given symbolic expression. // Sets the hasComparison parameter if the expression has a comparison // operator. Sets the RetTy parameter to the final return type after // promotions and casts. - static inline SMTExprRef getExpr(SMTSolverRef &Solver, ASTContext &Ctx, - SymbolRef Sym, QualType *RetTy = nullptr, - bool *hasComparison = nullptr) { + static inline llvm::SMTExprRef getExpr(llvm::SMTSolverRef &Solver, + ASTContext &Ctx, SymbolRef Sym, + QualType *RetTy = nullptr, + bool *hasComparison = nullptr) { if (hasComparison) { *hasComparison = false; } @@ -456,11 +469,11 @@ return getSymExpr(Solver, Ctx, Sym, RetTy, hasComparison); } - // Generate an SMTExprRef that compares the expression to zero. - static inline SMTExprRef getZeroExpr(SMTSolverRef &Solver, ASTContext &Ctx, - const SMTExprRef &Exp, QualType Ty, - bool Assumption) { - + // Generate an SMTSolverRef that compares the expression to zero. + static inline llvm::SMTExprRef getZeroExpr(llvm::SMTSolverRef &Solver, + ASTContext &Ctx, + const llvm::SMTExprRef &Exp, + QualType Ty, bool Assumption) { if (Ty->isRealFloatingType()) { llvm::APFloat Zero = llvm::APFloat::getZero(Ctx.getFloatTypeSemantics(Ty)); @@ -485,21 +498,21 @@ llvm_unreachable("Unsupported type for zero value!"); } - // Wrapper to generate SMTExprRef from a range. If From == To, an equality - // will be created instead. - static inline SMTExprRef getRangeExpr(SMTSolverRef &Solver, ASTContext &Ctx, - SymbolRef Sym, const llvm::APSInt &From, - const llvm::APSInt &To, bool InRange) { + // Wrapper to generate SMTSolverRef from a range. If From == To, an + // equality will be created instead. + static inline llvm::SMTExprRef + getRangeExpr(llvm::SMTSolverRef &Solver, ASTContext &Ctx, SymbolRef Sym, + const llvm::APSInt &From, const llvm::APSInt &To, bool InRange) { // Convert lower bound QualType FromTy; llvm::APSInt NewFromInt; std::tie(NewFromInt, FromTy) = fixAPSInt(Ctx, From); - SMTExprRef FromExp = + llvm::SMTExprRef FromExp = Solver->mkBitvector(NewFromInt, NewFromInt.getBitWidth()); // Convert symbol QualType SymTy; - SMTExprRef Exp = getExpr(Solver, Ctx, Sym, &SymTy); + llvm::SMTExprRef Exp = getExpr(Solver, Ctx, Sym, &SymTy); // Construct single (in)equality if (From == To) @@ -509,16 +522,17 @@ QualType ToTy; llvm::APSInt NewToInt; std::tie(NewToInt, ToTy) = fixAPSInt(Ctx, To); - SMTExprRef ToExp = Solver->mkBitvector(NewToInt, NewToInt.getBitWidth()); + llvm::SMTExprRef ToExp = + Solver->mkBitvector(NewToInt, NewToInt.getBitWidth()); assert(FromTy == ToTy && "Range values have different types!"); // Construct two (in)equalities, and a logical and/or - SMTExprRef LHS = + llvm::SMTExprRef LHS = getBinExpr(Solver, Ctx, Exp, SymTy, InRange ? BO_GE : BO_LT, FromExp, FromTy, /*RetTy=*/nullptr); - SMTExprRef RHS = getBinExpr(Solver, Ctx, Exp, SymTy, - InRange ? BO_LE : BO_GT, ToExp, ToTy, - /*RetTy=*/nullptr); + llvm::SMTExprRef RHS = getBinExpr(Solver, Ctx, Exp, SymTy, + InRange ? BO_LE : BO_GT, ToExp, ToTy, + /*RetTy=*/nullptr); return fromBinOp(Solver, LHS, InRange ? BO_LAnd : BO_LOr, RHS, SymTy->isSignedIntegerOrEnumerationType()); @@ -550,23 +564,24 @@ // Perform implicit type conversion on binary symbolic expressions. // May modify all input parameters. // TODO: Refactor to use built-in conversion functions - static inline void doTypeConversion(SMTSolverRef &Solver, ASTContext &Ctx, - SMTExprRef &LHS, SMTExprRef &RHS, - QualType <y, QualType &RTy) { + static inline void doTypeConversion(llvm::SMTSolverRef &Solver, + ASTContext &Ctx, llvm::SMTExprRef &LHS, + llvm::SMTExprRef &RHS, QualType <y, + QualType &RTy) { assert(!LTy.isNull() && !RTy.isNull() && "Input type is null!"); // Perform type conversion if ((LTy->isIntegralOrEnumerationType() && RTy->isIntegralOrEnumerationType()) && (LTy->isArithmeticType() && RTy->isArithmeticType())) { - SMTConv::doIntTypeConversion<SMTExprRef, &fromCast>(Solver, Ctx, LHS, LTy, - RHS, RTy); + SMTConv::doIntTypeConversion<llvm::SMTExprRef, &fromCast>( + Solver, Ctx, LHS, LTy, RHS, RTy); return; } if (LTy->isRealFloatingType() || RTy->isRealFloatingType()) { - SMTConv::doFloatTypeConversion<SMTExprRef, &fromCast>(Solver, Ctx, LHS, - LTy, RHS, RTy); + SMTConv::doFloatTypeConversion<llvm::SMTExprRef, &fromCast>( + Solver, Ctx, LHS, LTy, RHS, RTy); return; } @@ -624,12 +639,11 @@ // Perform implicit integer type conversion. // May modify all input parameters. // TODO: Refactor to use Sema::handleIntegerConversion() - template <typename T, T (*doCast)(SMTSolverRef &Solver, const T &, QualType, - uint64_t, QualType, uint64_t)> - static inline void doIntTypeConversion(SMTSolverRef &Solver, ASTContext &Ctx, - T &LHS, QualType <y, T &RHS, - QualType &RTy) { - + template <typename T, T (*doCast)(llvm::SMTSolverRef &Solver, const T &, + QualType, uint64_t, QualType, uint64_t)> + static inline void doIntTypeConversion(llvm::SMTSolverRef &Solver, + ASTContext &Ctx, T &LHS, QualType <y, + T &RHS, QualType &RTy) { uint64_t LBitWidth = Ctx.getTypeSize(LTy); uint64_t RBitWidth = Ctx.getTypeSize(RTy); @@ -707,12 +721,11 @@ // Perform implicit floating-point type conversion. // May modify all input parameters. // TODO: Refactor to use Sema::handleFloatConversion() - template <typename T, T (*doCast)(SMTSolverRef &Solver, const T &, QualType, - uint64_t, QualType, uint64_t)> + template <typename T, T (*doCast)(llvm::SMTSolverRef &Solver, const T &, + QualType, uint64_t, QualType, uint64_t)> static inline void - doFloatTypeConversion(SMTSolverRef &Solver, ASTContext &Ctx, T &LHS, + doFloatTypeConversion(llvm::SMTSolverRef &Solver, ASTContext &Ctx, T &LHS, QualType <y, T &RHS, QualType &RTy) { - uint64_t LBitWidth = Ctx.getTypeSize(LTy); uint64_t RBitWidth = Ctx.getTypeSize(RTy); @@ -749,4 +762,4 @@ } // namespace ento } // namespace clang -#endif \ No newline at end of file +#endif Index: clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h =================================================================== --- clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h +++ clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h @@ -18,7 +18,7 @@ #include "clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h" typedef llvm::ImmutableSet< - std::pair<clang::ento::SymbolRef, const clang::ento::SMTExpr *>> + std::pair<clang::ento::SymbolRef, const llvm::SMTExpr *>> ConstraintSMTType; REGISTER_TRAIT_WITH_PROGRAMSTATE(ConstraintSMT, ConstraintSMTType) @@ -26,7 +26,7 @@ namespace ento { class SMTConstraintManager : public clang::ento::SimpleConstraintManager { - mutable SMTSolverRef Solver = CreateZ3Solver(); + mutable llvm::SMTSolverRef Solver = llvm::CreateZ3Solver(); public: SMTConstraintManager(clang::ento::SubEngine *SE, clang::ento::SValBuilder &SB) @@ -44,7 +44,8 @@ QualType RetTy; bool hasComparison; - SMTExprRef Exp = SMTConv::getExpr(Solver, Ctx, Sym, &RetTy, &hasComparison); + llvm::SMTExprRef Exp = + SMTConv::getExpr(Solver, Ctx, Sym, &RetTy, &hasComparison); // Create zero comparison for implicit boolean cast, with reversed // assumption @@ -80,12 +81,12 @@ QualType RetTy; // The expression may be casted, so we cannot call getZ3DataExpr() directly - SMTExprRef VarExp = SMTConv::getExpr(Solver, Ctx, Sym, &RetTy); - SMTExprRef Exp = + llvm::SMTExprRef VarExp = SMTConv::getExpr(Solver, Ctx, Sym, &RetTy); + llvm::SMTExprRef Exp = SMTConv::getZeroExpr(Solver, Ctx, VarExp, RetTy, /*Assumption=*/true); // Negate the constraint - SMTExprRef NotExp = + llvm::SMTExprRef NotExp = SMTConv::getZeroExpr(Solver, Ctx, VarExp, RetTy, /*Assumption=*/false); ConditionTruthVal isSat = checkModel(State, Sym, Exp); @@ -118,7 +119,7 @@ // this method tries to get the interpretation (the actual value) from // the solver, which is currently not cached. - SMTExprRef Exp = + llvm::SMTExprRef Exp = SMTConv::fromData(Solver, SD->getSymbolID(), Ty, Ctx.getTypeSize(Ty)); Solver->reset(); @@ -134,7 +135,7 @@ return nullptr; // A value has been obtained, check if it is the only value - SMTExprRef NotExp = SMTConv::fromBinOp( + llvm::SMTExprRef NotExp = SMTConv::fromBinOp( Solver, Exp, BO_NE, Ty->isBooleanType() ? Solver->mkBoolean(Value.getBoolValue()) : Solver->mkBitvector(Value, Value.getBitWidth()), @@ -277,7 +278,7 @@ protected: // Check whether a new model is satisfiable, and update the program state. virtual ProgramStateRef assumeExpr(ProgramStateRef State, SymbolRef Sym, - const SMTExprRef &Exp) { + const llvm::SMTExprRef &Exp) { // Check the model, avoid simplifying AST to save time if (checkModel(State, Sym, Exp).isConstrainedTrue()) return State->add<ConstraintSMT>(std::make_pair(Sym, Exp)); @@ -294,9 +295,9 @@ // Construct the logical AND of all the constraints if (I != IE) { - std::vector<SMTExprRef> ASTs; + std::vector<llvm::SMTExprRef> ASTs; - SMTExprRef Constraint = I++->second; + llvm::SMTExprRef Constraint = I++->second; while (I != IE) { Constraint = Solver->mkAnd(Constraint, I++->second); } @@ -307,7 +308,7 @@ // Generate and check a Z3 model, using the given constraint. ConditionTruthVal checkModel(ProgramStateRef State, SymbolRef Sym, - const SMTExprRef &Exp) const { + const llvm::SMTExprRef &Exp) const { ProgramStateRef NewState = State->add<ConstraintSMT>(std::make_pair(Sym, Exp)); Index: clang/include/clang/Config/config.h.cmake =================================================================== --- clang/include/clang/Config/config.h.cmake +++ clang/include/clang/Config/config.h.cmake @@ -54,9 +54,6 @@ /* Define if we have libxml2 */ #cmakedefine CLANG_HAVE_LIBXML ${CLANG_HAVE_LIBXML} -/* Define if we have z3 and want to build it */ -#cmakedefine CLANG_ANALYZER_WITH_Z3 ${CLANG_ANALYZER_WITH_Z3} - /* Define if we have sys/resource.h (rlimits) */ #cmakedefine CLANG_HAVE_RLIMITS ${CLANG_HAVE_RLIMITS} Index: clang/cmake/modules/FindZ3.cmake =================================================================== --- clang/cmake/modules/FindZ3.cmake +++ clang/cmake/modules/FindZ3.cmake @@ -1,51 +0,0 @@ -# Looking for Z3 in CLANG_ANALYZER_Z3_INSTALL_DIR -find_path(Z3_INCLUDE_DIR NAMES z3.h - NO_DEFAULT_PATH - PATHS ${CLANG_ANALYZER_Z3_INSTALL_DIR}/include - PATH_SUFFIXES libz3 z3 - ) - -find_library(Z3_LIBRARIES NAMES z3 libz3 - NO_DEFAULT_PATH - PATHS ${CLANG_ANALYZER_Z3_INSTALL_DIR} - PATH_SUFFIXES lib bin - ) - -find_program(Z3_EXECUTABLE z3 - NO_DEFAULT_PATH - PATHS ${CLANG_ANALYZER_Z3_INSTALL_DIR} - PATH_SUFFIXES bin - ) - -# If Z3 has not been found in CLANG_ANALYZER_Z3_INSTALL_DIR look in the default directories -find_path(Z3_INCLUDE_DIR NAMES z3.h - PATH_SUFFIXES libz3 z3 - ) - -find_library(Z3_LIBRARIES NAMES z3 libz3 - PATH_SUFFIXES lib bin - ) - -find_program(Z3_EXECUTABLE z3 - PATH_SUFFIXES bin - ) - -if(Z3_INCLUDE_DIR AND Z3_LIBRARIES AND Z3_EXECUTABLE) - execute_process (COMMAND ${Z3_EXECUTABLE} -version - OUTPUT_VARIABLE libz3_version_str - ERROR_QUIET - OUTPUT_STRIP_TRAILING_WHITESPACE) - - string(REGEX REPLACE "^Z3 version ([0-9.]+)" "\\1" - Z3_VERSION_STRING "${libz3_version_str}") - unset(libz3_version_str) -endif() - -# handle the QUIETLY and REQUIRED arguments and set Z3_FOUND to TRUE if -# all listed variables are TRUE -include(FindPackageHandleStandardArgs) -FIND_PACKAGE_HANDLE_STANDARD_ARGS(Z3 - REQUIRED_VARS Z3_LIBRARIES Z3_INCLUDE_DIR - VERSION_VAR Z3_VERSION_STRING) - -mark_as_advanced(Z3_INCLUDE_DIR Z3_LIBRARIES) Index: clang/CMakeLists.txt =================================================================== --- clang/CMakeLists.txt +++ clang/CMakeLists.txt @@ -428,34 +428,9 @@ option(CLANG_ENABLE_ARCMT "Build ARCMT." ON) option(CLANG_ENABLE_STATIC_ANALYZER "Build static analyzer." ON) -set(CLANG_ANALYZER_Z3_INSTALL_DIR "" CACHE STRING "Install directory of the Z3 solver.") - -find_package(Z3 4.7.1) - -if (CLANG_ANALYZER_Z3_INSTALL_DIR) - if (NOT Z3_FOUND) - message(FATAL_ERROR "Z3 4.7.1 has not been found in CLANG_ANALYZER_Z3_INSTALL_DIR: ${CLANG_ANALYZER_Z3_INSTALL_DIR}.") - endif() -endif() - -set(CLANG_ANALYZER_ENABLE_Z3_SOLVER_DEFAULT "${Z3_FOUND}") - -option(CLANG_ANALYZER_ENABLE_Z3_SOLVER - "Enable Support for the Z3 constraint solver in the Clang Static Analyzer." - ${CLANG_ANALYZER_ENABLE_Z3_SOLVER_DEFAULT} -) - -if (CLANG_ANALYZER_ENABLE_Z3_SOLVER) - if (NOT Z3_FOUND) - message(FATAL_ERROR "CLANG_ANALYZER_ENABLE_Z3_SOLVER cannot be enabled when Z3 is not available.") - endif() - - set(CLANG_ANALYZER_WITH_Z3 1) -endif() - option(CLANG_ENABLE_PROTO_FUZZER "Build Clang protobuf fuzzer." OFF) -if(NOT CLANG_ENABLE_STATIC_ANALYZER AND (CLANG_ENABLE_ARCMT OR CLANG_ANALYZER_ENABLE_Z3_SOLVER)) +if(NOT CLANG_ENABLE_STATIC_ANALYZER AND CLANG_ENABLE_ARCMT) message(FATAL_ERROR "Cannot disable static analyzer while enabling ARCMT or Z3") endif()
_______________________________________________ cfe-commits mailing list cfe-commits@lists.llvm.org https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
