maxjhandsome
/
llvm-project
forked from OSchip/llvm-project
1
0
Fork 0
Code Issues Pull Requests Packages Releases Wiki Activity

This reverts commit 1440a848a635849b97f7a5cfa0ecc40d37451f5b. 

and commit a1853e834c65751f92521f7481b15cf0365e796b.

They broke arm and aarch64

llvm-svn: 353590
This commit is contained in:
Mikhail R. Gadelha 2019-02-09 00:46:12 +00:00
parent c230c13d4b
commit 3289ccd848
16 changed files with 201 additions and 235 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

27
clang/CMakeLists.txt
View File

@ -411,9 +411,34 @@ option(CLANG_BUILD_TOOLS
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)
if(NOT CLANG_ENABLE_STATIC_ANALYZER AND (CLANG_ENABLE_ARCMT OR CLANG_ANALYZER_ENABLE_Z3_SOLVER))
message(FATAL_ERROR "Cannot disable static analyzer while enabling ARCMT or Z3")
endif()

10
llvm/cmake/modules/FindZ3.cmake → clang/cmake/modules/FindZ3.cmake
View File

@ -1,23 +1,23 @@
# Looking for Z3 in LLVM_Z3_INSTALL_DIR
# Looking for Z3 in CLANG_ANALYZER_Z3_INSTALL_DIR
find_path(Z3_INCLUDE_DIR NAMES z3.h
NO_DEFAULT_PATH
PATHS ${LLVM_Z3_INSTALL_DIR}/include
PATHS ${CLANG_ANALYZER_Z3_INSTALL_DIR}/include
PATH_SUFFIXES libz3 z3
)
find_library(Z3_LIBRARIES NAMES z3 libz3
NO_DEFAULT_PATH
PATHS ${LLVM_Z3_INSTALL_DIR}
PATHS ${CLANG_ANALYZER_Z3_INSTALL_DIR}
PATH_SUFFIXES lib bin
)
find_program(Z3_EXECUTABLE z3
NO_DEFAULT_PATH
PATHS ${LLVM_Z3_INSTALL_DIR}
PATHS ${CLANG_ANALYZER_Z3_INSTALL_DIR}
PATH_SUFFIXES bin
)
# If Z3 has not been found in LLVM_Z3_INSTALL_DIR look in the default directories
# 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
)

3
clang/include/clang/Config/config.h.cmake
View File

@ -54,6 +54,9 @@
/* 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}

21
llvm/include/llvm/Support/SMTAPI.h → clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTAPI.h
View File

@ -11,16 +11,14 @@
//
//===----------------------------------------------------------------------===//
#ifndef LLVM_SUPPORT_SMTAPI_H
#define LLVM_SUPPORT_SMTAPI_H
#ifndef LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTSOLVER_H
#define LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTSOLVER_H
#include "llvm/ADT/APFloat.h"
#include "clang/Basic/TargetInfo.h"
#include "llvm/ADT/APSInt.h"
#include "llvm/ADT/FoldingSet.h"
#include "llvm/Support/raw_ostream.h"
#include <memory>
namespace llvm {
namespace clang {
namespace ento {
/// Generic base class for SMT sorts
class SMTSort {
@ -70,7 +68,7 @@ public:
virtual void print(raw_ostream &OS) const = 0;
LLVM_DUMP_METHOD void dump() const;
LLVM_DUMP_METHOD void dump() const { print(llvm::errs()); }
protected:
/// Query the SMT solver and returns true if two sorts are equal (same kind
@ -117,7 +115,7 @@ public:
virtual void print(raw_ostream &OS) const = 0;
LLVM_DUMP_METHOD void dump() const;
LLVM_DUMP_METHOD void dump() const { print(llvm::errs()); }
protected:
/// Query the SMT solver and returns true if two sorts are equal (same kind
@ -138,7 +136,7 @@ public:
SMTSolver() = default;
virtual ~SMTSolver() = default;
LLVM_DUMP_METHOD void dump() const;
LLVM_DUMP_METHOD void dump() const { print(llvm::errs()); }
// Returns an appropriate floating-point sort for the given bitwidth.
SMTSortRef getFloatSort(unsigned BitWidth) {
@ -400,6 +398,7 @@ using SMTSolverRef = std::shared_ptr<SMTSolver>;
/// Convenience method to create and Z3Solver object
SMTSolverRef CreateZ3Solver();
} // namespace llvm
} // namespace ento
} // namespace clang
#endif

25
clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h
View File

@ -18,7 +18,7 @@
#include "clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h"
typedef llvm::ImmutableSet<
std::pair<clang::ento::SymbolRef, const llvm::SMTExpr *>>
std::pair<clang::ento::SymbolRef, const clang::ento::SMTExpr *>>
ConstraintSMTTy;
REGISTER_TRAIT_WITH_PROGRAMSTATE(ConstraintSMT, ConstraintSMTTy)
@ -26,7 +26,7 @@ namespace clang {
namespace ento {
class SMTConstraintManager : public clang::ento::SimpleConstraintManager {
mutable llvm::SMTSolverRef Solver = llvm::CreateZ3Solver();
mutable SMTSolverRef Solver = CreateZ3Solver();
public:
SMTConstraintManager(clang::ento::SubEngine *SE, clang::ento::SValBuilder &SB)
@ -44,8 +44,7 @@ public:
QualType RetTy;
bool hasComparison;
llvm::SMTExprRef Exp =
SMTConv::getExpr(Solver, Ctx, Sym, &RetTy, &hasComparison);
SMTExprRef Exp = SMTConv::getExpr(Solver, Ctx, Sym, &RetTy, &hasComparison);
// Create zero comparison for implicit boolean cast, with reversed
// assumption
@ -81,12 +80,12 @@ public:
QualType RetTy;
// The expression may be casted, so we cannot call getZ3DataExpr() directly
llvm::SMTExprRef VarExp = SMTConv::getExpr(Solver, Ctx, Sym, &RetTy);
llvm::SMTExprRef Exp =
SMTExprRef VarExp = SMTConv::getExpr(Solver, Ctx, Sym, &RetTy);
SMTExprRef Exp =
SMTConv::getZeroExpr(Solver, Ctx, VarExp, RetTy, /*Assumption=*/true);
// Negate the constraint
llvm::SMTExprRef NotExp =
SMTExprRef NotExp =
SMTConv::getZeroExpr(Solver, Ctx, VarExp, RetTy, /*Assumption=*/false);
ConditionTruthVal isSat = checkModel(State, Sym, Exp);
@ -119,7 +118,7 @@ public:
// this method tries to get the interpretation (the actual value) from
// the solver, which is currently not cached.
llvm::SMTExprRef Exp =
SMTExprRef Exp =
SMTConv::fromData(Solver, SD->getSymbolID(), Ty, Ctx.getTypeSize(Ty));
Solver->reset();
@ -135,7 +134,7 @@ public:
return nullptr;
// A value has been obtained, check if it is the only value
llvm::SMTExprRef NotExp = SMTConv::fromBinOp(
SMTExprRef NotExp = SMTConv::fromBinOp(
Solver, Exp, BO_NE,
Ty->isBooleanType() ? Solver->mkBoolean(Value.getBoolValue())
: Solver->mkBitvector(Value, Value.getBitWidth()),
@ -273,7 +272,7 @@ public:
protected:
// Check whether a new model is satisfiable, and update the program state.
virtual ProgramStateRef assumeExpr(ProgramStateRef State, SymbolRef Sym,
const llvm::SMTExprRef &Exp) {
const 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));
@ -290,9 +289,9 @@ protected:
// Construct the logical AND of all the constraints
if (I != IE) {
std::vector<llvm::SMTExprRef> ASTs;
std::vector<SMTExprRef> ASTs;
llvm::SMTExprRef Constraint = I++->second;
SMTExprRef Constraint = I++->second;
while (I != IE) {
Constraint = Solver->mkAnd(Constraint, I++->second);
}
@ -303,7 +302,7 @@ protected:
// Generate and check a Z3 model, using the given constraint.
ConditionTruthVal checkModel(ProgramStateRef State, SymbolRef Sym,
const llvm::SMTExprRef &Exp) const {
const SMTExprRef &Exp) const {
ProgramStateRef NewState =
State->add<ConstraintSMT>(std::make_pair(Sym, Exp));

227
clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h
View File

@ -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 @@ namespace ento {
class SMTConv {
public:
// Returns an appropriate sort, given a QualType and it's bit width.
static inline llvm::SMTSortRef mkSort(llvm::SMTSolverRef &Solver,
const QualType &Ty, unsigned BitWidth) {
static inline SMTSortRef mkSort(SMTSolverRef &Solver, const QualType &Ty,
unsigned BitWidth) {
if (Ty->isBooleanType())
return Solver->getBoolSort();
@ -35,10 +35,10 @@ public:
return Solver->getBitvectorSort(BitWidth);
}
/// Constructs an SMTSolverRef from an unary operator.
static inline llvm::SMTExprRef fromUnOp(llvm::SMTSolverRef &Solver,
const UnaryOperator::Opcode Op,
const llvm::SMTExprRef &Exp) {
/// Constructs an SMTExprRef from an unary operator.
static inline SMTExprRef fromUnOp(SMTSolverRef &Solver,
const UnaryOperator::Opcode Op,
const SMTExprRef &Exp) {
switch (Op) {
case UO_Minus:
return Solver->mkBVNeg(Exp);
@ -54,10 +54,10 @@ public:
llvm_unreachable("Unimplemented opcode");
}
/// 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) {
/// Constructs an SMTExprRef from a floating-point unary operator.
static inline SMTExprRef fromFloatUnOp(SMTSolverRef &Solver,
const UnaryOperator::Opcode Op,
const SMTExprRef &Exp) {
switch (Op) {
case UO_Minus:
return Solver->mkFPNeg(Exp);
@ -70,28 +70,27 @@ public:
llvm_unreachable("Unimplemented opcode");
}
/// 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) {
/// Construct an SMTExprRef from a n-ary binary operator.
static inline SMTExprRef fromNBinOp(SMTSolverRef &Solver,
const BinaryOperator::Opcode Op,
const std::vector<SMTExprRef> &ASTs) {
assert(!ASTs.empty());
if (Op != BO_LAnd && Op != BO_LOr)
llvm_unreachable("Unimplemented opcode");
llvm::SMTExprRef res = ASTs.front();
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 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) {
/// 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) {
assert(*Solver->getSort(LHS) == *Solver->getSort(RHS) &&
"AST's must have the same sort!");
@ -163,10 +162,9 @@ public:
llvm_unreachable("Unimplemented opcode");
}
/// Construct an SMTSolverRef from a special floating-point binary
/// operator.
static inline llvm::SMTExprRef
fromFloatSpecialBinOp(llvm::SMTSolverRef &Solver, const llvm::SMTExprRef &LHS,
/// Construct an SMTExprRef from a special floating-point binary operator.
static inline SMTExprRef
fromFloatSpecialBinOp(SMTSolverRef &Solver, const SMTExprRef &LHS,
const BinaryOperator::Opcode Op,
const llvm::APFloat::fltCategory &RHS) {
switch (Op) {
@ -197,11 +195,11 @@ public:
llvm_unreachable("Unimplemented opcode");
}
/// 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) {
/// 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) {
assert(*Solver->getSort(LHS) == *Solver->getSort(RHS) &&
"AST's must have the same sort!");
@ -255,13 +253,11 @@ public:
llvm_unreachable("Unimplemented opcode");
}
/// 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) {
/// 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) {
if ((FromTy->isIntegralOrEnumerationType() &&
ToTy->isIntegralOrEnumerationType()) ||
(FromTy->isAnyPointerType() ^ ToTy->isAnyPointerType()) ||
@ -295,7 +291,7 @@ public:
}
if (FromTy->isIntegralOrEnumerationType() && ToTy->isRealFloatingType()) {
llvm::SMTSortRef Sort = Solver->getFloatSort(ToBitWidth);
SMTSortRef Sort = Solver->getFloatSort(ToBitWidth);
return FromTy->isSignedIntegerOrEnumerationType()
? Solver->mkSBVtoFP(Exp, Sort)
: Solver->mkUBVtoFP(Exp, Sort);
@ -310,7 +306,7 @@ public:
}
// Callback function for doCast parameter on APSInt type.
static inline llvm::APSInt castAPSInt(llvm::SMTSolverRef &Solver,
static inline llvm::APSInt castAPSInt(SMTSolverRef &Solver,
const llvm::APSInt &V, QualType ToTy,
uint64_t ToWidth, QualType FromTy,
uint64_t FromWidth) {
@ -318,32 +314,30 @@ public:
return TargetType.convert(V);
}
/// Construct an SMTSolverRef from a SymbolData.
static inline llvm::SMTExprRef fromData(llvm::SMTSolverRef &Solver,
const SymbolID ID, const QualType &Ty,
uint64_t BitWidth) {
/// Construct an SMTExprRef from a SymbolData.
static inline SMTExprRef fromData(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 SMTSolverRef from SymbolCast data.
static inline llvm::SMTExprRef getCastExpr(llvm::SMTSolverRef &Solver,
ASTContext &Ctx,
const llvm::SMTExprRef &Exp,
QualType FromTy, QualType ToTy) {
// Wrapper to generate SMTExprRef from SymbolCast data.
static inline SMTExprRef getCastExpr(SMTSolverRef &Solver, ASTContext &Ctx,
const SMTExprRef &Exp, QualType FromTy,
QualType ToTy) {
return fromCast(Solver, Exp, ToTy, Ctx.getTypeSize(ToTy), FromTy,
Ctx.getTypeSize(FromTy));
}
// 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;
// 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;
doTypeConversion(Solver, Ctx, NewLHS, NewRHS, LTy, RTy);
// Update the return type parameter if the output type has changed.
@ -371,40 +365,36 @@ public:
LTy->isSignedIntegerOrEnumerationType());
}
// 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) {
// 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) {
QualType LTy, RTy;
BinaryOperator::Opcode Op = BSE->getOpcode();
if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(BSE)) {
llvm::SMTExprRef LHS =
SMTExprRef LHS =
getSymExpr(Solver, Ctx, SIE->getLHS(), &LTy, hasComparison);
llvm::APSInt NewRInt;
std::tie(NewRInt, RTy) = fixAPSInt(Ctx, SIE->getRHS());
llvm::SMTExprRef RHS =
Solver->mkBitvector(NewRInt, NewRInt.getBitWidth());
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());
llvm::SMTExprRef LHS =
Solver->mkBitvector(NewLInt, NewLInt.getBitWidth());
llvm::SMTExprRef RHS =
SMTExprRef LHS = Solver->mkBitvector(NewLInt, NewLInt.getBitWidth());
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)) {
llvm::SMTExprRef LHS =
SMTExprRef LHS =
getSymExpr(Solver, Ctx, SSM->getLHS(), &LTy, hasComparison);
llvm::SMTExprRef RHS =
SMTExprRef RHS =
getSymExpr(Solver, Ctx, SSM->getRHS(), &RTy, hasComparison);
return getBinExpr(Solver, Ctx, LHS, LTy, Op, RHS, RTy, RetTy);
}
@ -414,10 +404,9 @@ public:
// Recursive implementation to unpack and generate symbolic expression.
// Sets the hasComparison and RetTy parameters. See getExpr().
static inline llvm::SMTExprRef getSymExpr(llvm::SMTSolverRef &Solver,
ASTContext &Ctx, SymbolRef Sym,
QualType *RetTy,
bool *hasComparison) {
static inline SMTExprRef getSymExpr(SMTSolverRef &Solver, ASTContext &Ctx,
SymbolRef Sym, QualType *RetTy,
bool *hasComparison) {
if (const SymbolData *SD = dyn_cast<SymbolData>(Sym)) {
if (RetTy)
*RetTy = Sym->getType();
@ -431,7 +420,7 @@ public:
*RetTy = Sym->getType();
QualType FromTy;
llvm::SMTExprRef Exp =
SMTExprRef Exp =
getSymExpr(Solver, Ctx, SC->getOperand(), &FromTy, hasComparison);
// Casting an expression with a comparison invalidates it. Note that this
@ -443,8 +432,7 @@ public:
}
if (const BinarySymExpr *BSE = dyn_cast<BinarySymExpr>(Sym)) {
llvm::SMTExprRef Exp =
getSymBinExpr(Solver, Ctx, BSE, hasComparison, RetTy);
SMTExprRef Exp = getSymBinExpr(Solver, Ctx, BSE, hasComparison, RetTy);
// Set the hasComparison parameter, in post-order traversal order.
if (hasComparison)
*hasComparison = BinaryOperator::isComparisonOp(BSE->getOpcode());
@ -454,14 +442,13 @@ public:
llvm_unreachable("Unsupported SymbolRef type!");
}
// Generate an SMTSolverRef that represents the given symbolic expression.
// Generate an SMTExprRef 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 llvm::SMTExprRef getExpr(llvm::SMTSolverRef &Solver,
ASTContext &Ctx, SymbolRef Sym,
QualType *RetTy = nullptr,
bool *hasComparison = nullptr) {
static inline SMTExprRef getExpr(SMTSolverRef &Solver, ASTContext &Ctx,
SymbolRef Sym, QualType *RetTy = nullptr,
bool *hasComparison = nullptr) {
if (hasComparison) {
*hasComparison = false;
}
@ -469,11 +456,11 @@ public:
return getSymExpr(Solver, Ctx, Sym, RetTy, hasComparison);
}
// 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) {
// Generate an SMTExprRef that compares the expression to zero.
static inline SMTExprRef getZeroExpr(SMTSolverRef &Solver, ASTContext &Ctx,
const SMTExprRef &Exp, QualType Ty,
bool Assumption) {
if (Ty->isRealFloatingType()) {
llvm::APFloat Zero =
llvm::APFloat::getZero(Ctx.getFloatTypeSemantics(Ty));
@ -498,21 +485,21 @@ public:
llvm_unreachable("Unsupported type for zero value!");
}
// 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) {
// 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) {
// Convert lower bound
QualType FromTy;
llvm::APSInt NewFromInt;
std::tie(NewFromInt, FromTy) = fixAPSInt(Ctx, From);
llvm::SMTExprRef FromExp =
SMTExprRef FromExp =
Solver->mkBitvector(NewFromInt, NewFromInt.getBitWidth());
// Convert symbol
QualType SymTy;
llvm::SMTExprRef Exp = getExpr(Solver, Ctx, Sym, &SymTy);
SMTExprRef Exp = getExpr(Solver, Ctx, Sym, &SymTy);
// Construct single (in)equality
if (From == To)
@ -522,17 +509,16 @@ public:
QualType ToTy;
llvm::APSInt NewToInt;
std::tie(NewToInt, ToTy) = fixAPSInt(Ctx, To);
llvm::SMTExprRef ToExp =
Solver->mkBitvector(NewToInt, NewToInt.getBitWidth());
SMTExprRef ToExp = Solver->mkBitvector(NewToInt, NewToInt.getBitWidth());
assert(FromTy == ToTy && "Range values have different types!");
// Construct two (in)equalities, and a logical and/or
llvm::SMTExprRef LHS =
SMTExprRef LHS =
getBinExpr(Solver, Ctx, Exp, SymTy, InRange ? BO_GE : BO_LT, FromExp,
FromTy, /*RetTy=*/nullptr);
llvm::SMTExprRef RHS = getBinExpr(Solver, Ctx, Exp, SymTy,
InRange ? BO_LE : BO_GT, ToExp, ToTy,
/*RetTy=*/nullptr);
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());
@ -564,24 +550,23 @@ public:
// 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(llvm::SMTSolverRef &Solver,
ASTContext &Ctx, llvm::SMTExprRef &LHS,
llvm::SMTExprRef &RHS, QualType &LTy,
QualType &RTy) {
static inline void doTypeConversion(SMTSolverRef &Solver, ASTContext &Ctx,
SMTExprRef &LHS, SMTExprRef &RHS,
QualType &LTy, 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<llvm::SMTExprRef, &fromCast>(
Solver, Ctx, LHS, LTy, RHS, RTy);
SMTConv::doIntTypeConversion<SMTExprRef, &fromCast>(Solver, Ctx, LHS, LTy,
RHS, RTy);
return;
}
if (LTy->isRealFloatingType() || RTy->isRealFloatingType()) {
SMTConv::doFloatTypeConversion<llvm::SMTExprRef, &fromCast>(
Solver, Ctx, LHS, LTy, RHS, RTy);
SMTConv::doFloatTypeConversion<SMTExprRef, &fromCast>(Solver, Ctx, LHS,
LTy, RHS, RTy);
return;
}
@ -639,11 +624,12 @@ public:
// Perform implicit integer type conversion.
// May modify all input parameters.
// TODO: Refactor to use Sema::handleIntegerConversion()
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 &LTy,
T &RHS, QualType &RTy) {
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 &LTy, T &RHS,
QualType &RTy) {
uint64_t LBitWidth = Ctx.getTypeSize(LTy);
uint64_t RBitWidth = Ctx.getTypeSize(RTy);
@ -721,11 +707,12 @@ public:
// Perform implicit floating-point type conversion.
// May modify all input parameters.
// TODO: Refactor to use Sema::handleFloatConversion()
template <typename T, T (*doCast)(llvm::SMTSolverRef &Solver, const T &,
QualType, uint64_t, QualType, uint64_t)>
template <typename T, T (*doCast)(SMTSolverRef &Solver, const T &, QualType,
uint64_t, QualType, uint64_t)>
static inline void
doFloatTypeConversion(llvm::SMTSolverRef &Solver, ASTContext &Ctx, T &LHS,
doFloatTypeConversion(SMTSolverRef &Solver, ASTContext &Ctx, T &LHS,
QualType &LTy, T &RHS, QualType &RTy) {
uint64_t LBitWidth = Ctx.getTypeSize(LTy);
uint64_t RBitWidth = Ctx.getTypeSize(RTy);
@ -762,4 +749,4 @@ public:
} // namespace ento
} // namespace clang
#endif
#endif

4
clang/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp
View File

@ -2411,7 +2411,7 @@ void FalsePositiveRefutationBRVisitor::finalizeVisitor(
VisitNode(EndPathNode, BRC, BR);
// Create a refutation manager
llvm::SMTSolverRef RefutationSolver = llvm::CreateZ3Solver();
SMTSolverRef RefutationSolver = CreateZ3Solver();
ASTContext &Ctx = BRC.getASTContext();
// Add constraints to the solver
@ -2419,7 +2419,7 @@ void FalsePositiveRefutationBRVisitor::finalizeVisitor(
const SymbolRef Sym = I.first;
auto RangeIt = I.second.begin();
llvm::SMTExprRef Constraints = SMTConv::getRangeExpr(
SMTExprRef Constraints = SMTConv::getRangeExpr(
RefutationSolver, Ctx, Sym, RangeIt->From(), RangeIt->To(),
/*InRange=*/true);
while ((++RangeIt) != I.second.end()) {

16
clang/lib/StaticAnalyzer/Core/CMakeLists.txt
View File

@ -1,5 +1,12 @@
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
@ -39,7 +46,6 @@ add_clang_library(clangStaticAnalyzerCore
SarifDiagnostics.cpp
SimpleConstraintManager.cpp
SimpleSValBuilder.cpp
SMTConstraintManager.cpp
Store.cpp
SubEngine.cpp
SValBuilder.cpp
@ -47,6 +53,7 @@ add_clang_library(clangStaticAnalyzerCore
SymbolManager.cpp
TaintManager.cpp
WorkList.cpp
Z3ConstraintManager.cpp
LINK_LIBS
clangAST
@ -56,5 +63,12 @@ add_clang_library(clangStaticAnalyzerCore
clangCrossTU
clangLex
clangRewrite
${Z3_LINK_FILES}
)
if(CLANG_ANALYZER_WITH_Z3)
target_include_directories(clangStaticAnalyzerCore SYSTEM
PRIVATE
${Z3_INCLUDE_DIR}
)
endif()

18
clang/lib/StaticAnalyzer/Core/SMTConstraintManager.cpp
View File

@ -1,18 +0,0 @@
//== 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());
}

33
llvm/lib/Support/Z3Solver.cpp → clang/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
View File

@ -1,4 +1,4 @@
//== Z3Solver.cpp -----------------------------------------------*- C++ -*--==//
//== Z3ConstraintManager.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,14 +6,18 @@
//
//===----------------------------------------------------------------------===//
#include "llvm/ADT/Twine.h"
#include "llvm/Config/config.h"
#include "llvm/Support/SMTAPI.h"
#include <set>
#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"
using namespace llvm;
#include "clang/Config/config.h"
#if LLVM_WITH_Z3
using namespace clang;
using namespace ento;
#if CLANG_ANALYZER_WITH_Z3
#include <z3.h>
@ -814,19 +818,18 @@ public:
#endif
llvm::SMTSolverRef llvm::CreateZ3Solver() {
#if LLVM_WITH_Z3
SMTSolverRef clang::ento::CreateZ3Solver() {
#if CLANG_ANALYZER_WITH_Z3
return llvm::make_unique<Z3Solver>();
#else
llvm::report_fatal_error("Clang was not compiled with Z3 support, rebuild "
"with -DLLVM_ENABLE_Z3_SOLVER=ON",
"with -DCLANG_ANALYZER_ENABLE_Z3_SOLVER=ON",
false);
return nullptr;
#endif
}
LLVM_DUMP_METHOD void SMTSort::dump() const { print(llvm::errs()); }
LLVM_DUMP_METHOD void SMTExpr::dump() const { print(llvm::errs()); }
LLVM_DUMP_METHOD void SMTSolver::dump() const { print(llvm::errs()); }
std::unique_ptr<ConstraintManager>
ento::CreateZ3ConstraintManager(ProgramStateManager &StMgr, SubEngine *Eng) {
return llvm::make_unique<SMTConstraintManager>(Eng, StMgr.getSValBuilder());
}

2
clang/test/CMakeLists.txt
View File

@ -144,7 +144,7 @@ if (CLANG_ENABLE_STATIC_ANALYZER)
set_target_properties(check-clang-analyzer PROPERTIES FOLDER "Clang tests")
if (LLVM_WITH_Z3)
if (CLANG_ANALYZER_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}

2
clang/test/lit.site.cfg.py.in
View File

@ -20,7 +20,7 @@ config.have_zlib = @HAVE_LIBZ@
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 = "@LLVM_WITH_Z3@"
config.clang_staticanalyzer_z3 = "@CLANG_ANALYZER_WITH_Z3@"
config.clang_examples = @CLANG_BUILD_EXAMPLES@
config.enable_shared = @ENABLE_SHARED@
config.enable_backtrace = @ENABLE_BACKTRACES@

26
llvm/CMakeLists.txt
View File

@ -383,32 +383,6 @@ option(LLVM_ENABLE_THREADS "Use threads if available." ON)
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()

2
llvm/cmake/modules/LLVMConfig.cmake.in
View File

@ -44,8 +44,6 @@ set(LLVM_ENABLE_ZLIB @LLVM_ENABLE_ZLIB@)
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@)

3
llvm/include/llvm/Config/config.h.cmake
View File

@ -347,9 +347,6 @@
/* 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}"

17
llvm/lib/Support/CMakeLists.txt
View File

@ -44,13 +44,6 @@ if (MSVC)
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
@ -158,7 +151,6 @@ add_llvm_library(LLVMSupport
regfree.c
regstrlcpy.c
xxhash.cpp
Z3Solver.cpp
# System
Atomic.cpp
@ -184,14 +176,7 @@ add_llvm_library(LLVMSupport
${LLVM_MAIN_INCLUDE_DIR}/llvm/ADT
${LLVM_MAIN_INCLUDE_DIR}/llvm/Support
${Backtrace_INCLUDE_DIRS}
LINK_LIBS ${system_libs} ${delayload_flags} ${Z3_LINK_FILES}
LINK_LIBS ${system_libs} ${delayload_flags}
)
set_property(TARGET LLVMSupport PROPERTY LLVM_SYSTEM_LIBS "${system_libs}")
if(LLVM_WITH_Z3)
target_include_directories(LLVMSupport SYSTEM
PRIVATE
${Z3_INCLUDE_DIR}
)
endif()