r333899 - Created a tiny SMT interface and make Z3ConstraintManager implement it
Mikhail R. Gadelha via cfe-commits
cfe-commits at lists.llvm.org
Mon Jun 4 07:25:58 PDT 2018
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.
//===------------------------------------------------------------------===//
More information about the cfe-commits
mailing list