Author: mramalho Date: Mon Jun 4 07:25:58 2018 New Revision: 333899 URL: http://llvm.org/viewvc/llvm-project?rev=333899&view=rev Log: Created a tiny SMT interface and make Z3ConstraintManager implement it
Summary: This patch implements a simple SMTConstraintManager API, and requires the implementation of two methods for now: `addRangeConstraints` and `isModelFeasible`. Update Z3ConstraintManager to inherit it and implement required methods. I also moved the method to dump the SMT formula from D45517 to this patch. This patch was created based on the reviews from D47640. Reviewers: george.karpenkov, NoQ, ddcc, dcoughlin Reviewed By: george.karpenkov Differential Revision: https://reviews.llvm.org/D47689 Added: cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h Modified: cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp Added: cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h?rev=333899&view=auto ============================================================================== --- cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h (added) +++ cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h Mon Jun 4 07:25:58 2018 @@ -0,0 +1,43 @@ +//== SMTConstraintManager.h -------------------------------------*- C++ -*--==// +// +// The LLVM Compiler Infrastructure +// +// This file is distributed under the University of Illinois Open Source +// License. See LICENSE.TXT for details. +// +//===----------------------------------------------------------------------===// +// +// This file defines a SMT generic API, which will be the base class for +// every SMT solver specific class. +// +//===----------------------------------------------------------------------===// + +#ifndef LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTCONSTRAINTMANAGER_H +#define LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTCONSTRAINTMANAGER_H + +#include "clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h" + +namespace clang { +namespace ento { + +class SMTConstraintManager : public clang::ento::SimpleConstraintManager { + +public: + SMTConstraintManager(clang::ento::SubEngine *SE, clang::ento::SValBuilder &SB) + : SimpleConstraintManager(SE, SB) {} + virtual ~SMTConstraintManager() = default; + + /// Converts the ranged constraints of a set of symbols to SMT + /// + /// \param CR The set of constraints. + virtual void addRangeConstraints(clang::ento::ConstraintRangeTy CR) = 0; + + /// Checks if the added constraints are satisfiable + virtual clang::ento::ConditionTruthVal isModelFeasible() = 0; + +}; // end class SMTConstraintManager + +} // namespace ento +} // namespace clang + +#endif Modified: cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp?rev=333899&r1=333898&r2=333899&view=diff ============================================================================== --- cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp (original) +++ cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp Mon Jun 4 07:25:58 2018 @@ -10,7 +10,7 @@ #include "clang/Basic/TargetInfo.h" #include "clang/StaticAnalyzer/Core/PathSensitive/ExprEngine.h" #include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h" -#include "clang/StaticAnalyzer/Core/PathSensitive/SimpleConstraintManager.h" +#include "clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h" #include "clang/Config/config.h" @@ -880,6 +880,12 @@ public: /// Reset the solver and remove all constraints. void reset() { Z3_solver_reset(Z3Context::ZC, Solver); } + + void print(raw_ostream &OS) const { + OS << Z3_solver_to_string(Z3Context::ZC, Solver); + } + + LLVM_DUMP_METHOD void dump() const { print(llvm::errs()); } }; // end class Z3Solver void Z3ErrorHandler(Z3_context Context, Z3_error_code Error) { @@ -887,16 +893,23 @@ void Z3ErrorHandler(Z3_context Context, llvm::Twine(Z3_get_error_msg_ex(Context, Error))); } -class Z3ConstraintManager : public SimpleConstraintManager { +class Z3ConstraintManager : public SMTConstraintManager { Z3Context Context; mutable Z3Solver Solver; public: Z3ConstraintManager(SubEngine *SE, SValBuilder &SB) - : SimpleConstraintManager(SE, SB), + : SMTConstraintManager(SE, SB), Solver(Z3_mk_simple_solver(Z3Context::ZC)) { Z3_set_error_handler(Z3Context::ZC, Z3ErrorHandler); } + //===------------------------------------------------------------------===// + // Implementation for Refutation. + //===------------------------------------------------------------------===// + + void addRangeConstraints(clang::ento::ConstraintRangeTy CR) override; + + ConditionTruthVal isModelFeasible() override; //===------------------------------------------------------------------===// // Implementation for interface from ConstraintManager. @@ -1242,6 +1255,48 @@ Z3ConstraintManager::removeDeadBindings( return State->set<ConstraintZ3>(CZ); } +void Z3ConstraintManager::addRangeConstraints(ConstraintRangeTy CR) { + for (const auto &I : CR) { + SymbolRef Sym = I.first; + + Z3Expr Constraints = Z3Expr::fromBoolean(false); + + for (const auto &Range : I.second) { + const llvm::APSInt &From = Range.From(); + const llvm::APSInt &To = Range.To(); + + QualType FromTy; + llvm::APSInt NewFromInt; + std::tie(NewFromInt, FromTy) = fixAPSInt(From); + Z3Expr FromExp = Z3Expr::fromAPSInt(NewFromInt); + QualType SymTy; + Z3Expr Exp = getZ3Expr(Sym, &SymTy); + bool IsSignedTy = SymTy->isSignedIntegerOrEnumerationType(); + QualType ToTy; + llvm::APSInt NewToInt; + std::tie(NewToInt, ToTy) = fixAPSInt(To); + Z3Expr ToExp = Z3Expr::fromAPSInt(NewToInt); + assert(FromTy == ToTy && "Range values have different types!"); + + Z3Expr LHS = + getZ3BinExpr(Exp, SymTy, BO_GE, FromExp, FromTy, /*RetTy=*/nullptr); + Z3Expr RHS = + getZ3BinExpr(Exp, SymTy, BO_LE, ToExp, FromTy, /*RetTy=*/nullptr); + Z3Expr SymRange = Z3Expr::fromBinOp(LHS, BO_LAnd, RHS, IsSignedTy); + Constraints = + Z3Expr::fromBinOp(Constraints, BO_LOr, SymRange, IsSignedTy); + } + Solver.addConstraint(Constraints); + } +} + +clang::ento::ConditionTruthVal Z3ConstraintManager::isModelFeasible() { + if (Solver.check() == Z3_L_FALSE) + return false; + + return ConditionTruthVal(); +} + //===------------------------------------------------------------------===// // Internal implementation. //===------------------------------------------------------------------===// _______________________________________________ cfe-commits mailing list cfe-commits@lists.llvm.org http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
