clang  9.0.0svn
SMTConstraintManager.h
Go to the documentation of this file.
1 //== SMTConstraintManager.h -------------------------------------*- C++ -*--==//
2 //
3 // Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
4 // See https://llvm.org/LICENSE.txt for license information.
5 // SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
6 //
7 //===----------------------------------------------------------------------===//
8 //
9 // This file defines a SMT generic API, which will be the base class for
10 // every SMT solver specific class.
11 //
12 //===----------------------------------------------------------------------===//
13 
14 #ifndef LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTCONSTRAINTMANAGER_H
15 #define LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTCONSTRAINTMANAGER_H
16 
19 
20 typedef llvm::ImmutableSet<
21  std::pair<clang::ento::SymbolRef, const clang::ento::SMTExpr *>>
24 
25 namespace clang {
26 namespace ento {
27 
29  mutable SMTSolverRef Solver = CreateZ3Solver();
30 
31 public:
33  : SimpleConstraintManager(SE, SB) {}
34  virtual ~SMTConstraintManager() = default;
35 
36  //===------------------------------------------------------------------===//
37  // Implementation for interface from SimpleConstraintManager.
38  //===------------------------------------------------------------------===//
39 
41  bool Assumption) override {
43 
44  QualType RetTy;
45  bool hasComparison;
46 
47  SMTExprRef Exp = SMTConv::getExpr(Solver, Ctx, Sym, &RetTy, &hasComparison);
48 
49  // Create zero comparison for implicit boolean cast, with reversed
50  // assumption
51  if (!hasComparison && !RetTy->isBooleanType())
52  return assumeExpr(
53  State, Sym,
54  SMTConv::getZeroExpr(Solver, Ctx, Exp, RetTy, !Assumption));
55 
56  return assumeExpr(State, Sym, Assumption ? Exp : Solver->mkNot(Exp));
57  }
58 
60  const llvm::APSInt &From,
61  const llvm::APSInt &To,
62  bool InRange) override {
64  return assumeExpr(
65  State, Sym, SMTConv::getRangeExpr(Solver, Ctx, Sym, From, To, InRange));
66  }
67 
69  bool Assumption) override {
70  // Skip anything that is unsupported
71  return State;
72  }
73 
74  //===------------------------------------------------------------------===//
75  // Implementation for interface from ConstraintManager.
76  //===------------------------------------------------------------------===//
77 
80 
81  QualType RetTy;
82  // The expression may be casted, so we cannot call getZ3DataExpr() directly
83  SMTExprRef VarExp = SMTConv::getExpr(Solver, Ctx, Sym, &RetTy);
84  SMTExprRef Exp =
85  SMTConv::getZeroExpr(Solver, Ctx, VarExp, RetTy, /*Assumption=*/true);
86 
87  // Negate the constraint
88  SMTExprRef NotExp =
89  SMTConv::getZeroExpr(Solver, Ctx, VarExp, RetTy, /*Assumption=*/false);
90 
91  ConditionTruthVal isSat = checkModel(State, Sym, Exp);
92  ConditionTruthVal isNotSat = checkModel(State, Sym, NotExp);
93 
94  // Zero is the only possible solution
95  if (isSat.isConstrainedTrue() && isNotSat.isConstrainedFalse())
96  return true;
97 
98  // Zero is not a solution
99  if (isSat.isConstrainedFalse() && isNotSat.isConstrainedTrue())
100  return false;
101 
102  // Zero may be a solution
103  return ConditionTruthVal();
104  }
105 
106  const llvm::APSInt *getSymVal(ProgramStateRef State,
107  SymbolRef Sym) const override {
109  ASTContext &Ctx = BVF.getContext();
110 
111  if (const SymbolData *SD = dyn_cast<SymbolData>(Sym)) {
112  QualType Ty = Sym->getType();
113  assert(!Ty->isRealFloatingType());
114  llvm::APSInt Value(Ctx.getTypeSize(Ty),
116 
117  // TODO: this should call checkModel so we can use the cache, however,
118  // this method tries to get the interpretation (the actual value) from
119  // the solver, which is currently not cached.
120 
121  SMTExprRef Exp =
122  SMTConv::fromData(Solver, SD->getSymbolID(), Ty, Ctx.getTypeSize(Ty));
123 
124  Solver->reset();
125  addStateConstraints(State);
126 
127  // Constraints are unsatisfiable
128  Optional<bool> isSat = Solver->check();
129  if (!isSat.hasValue() || !isSat.getValue())
130  return nullptr;
131 
132  // Model does not assign interpretation
133  if (!Solver->getInterpretation(Exp, Value))
134  return nullptr;
135 
136  // A value has been obtained, check if it is the only value
138  Solver, Exp, BO_NE,
139  Ty->isBooleanType() ? Solver->mkBoolean(Value.getBoolValue())
140  : Solver->mkBitvector(Value, Value.getBitWidth()),
141  /*isSigned=*/false);
142 
143  Solver->addConstraint(NotExp);
144 
145  Optional<bool> isNotSat = Solver->check();
146  if (!isSat.hasValue() || isNotSat.getValue())
147  return nullptr;
148 
149  // This is the only solution, store it
150  return &BVF.getValue(Value);
151  }
152 
153  if (const SymbolCast *SC = dyn_cast<SymbolCast>(Sym)) {
154  SymbolRef CastSym = SC->getOperand();
155  QualType CastTy = SC->getType();
156  // Skip the void type
157  if (CastTy->isVoidType())
158  return nullptr;
159 
160  const llvm::APSInt *Value;
161  if (!(Value = getSymVal(State, CastSym)))
162  return nullptr;
163  return &BVF.Convert(SC->getType(), *Value);
164  }
165 
166  if (const BinarySymExpr *BSE = dyn_cast<BinarySymExpr>(Sym)) {
167  const llvm::APSInt *LHS, *RHS;
168  if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(BSE)) {
169  LHS = getSymVal(State, SIE->getLHS());
170  RHS = &SIE->getRHS();
171  } else if (const IntSymExpr *ISE = dyn_cast<IntSymExpr>(BSE)) {
172  LHS = &ISE->getLHS();
173  RHS = getSymVal(State, ISE->getRHS());
174  } else if (const SymSymExpr *SSM = dyn_cast<SymSymExpr>(BSE)) {
175  // Early termination to avoid expensive call
176  LHS = getSymVal(State, SSM->getLHS());
177  RHS = LHS ? getSymVal(State, SSM->getRHS()) : nullptr;
178  } else {
179  llvm_unreachable("Unsupported binary expression to get symbol value!");
180  }
181 
182  if (!LHS || !RHS)
183  return nullptr;
184 
185  llvm::APSInt ConvertedLHS, ConvertedRHS;
186  QualType LTy, RTy;
187  std::tie(ConvertedLHS, LTy) = SMTConv::fixAPSInt(Ctx, *LHS);
188  std::tie(ConvertedRHS, RTy) = SMTConv::fixAPSInt(Ctx, *RHS);
189  SMTConv::doIntTypeConversion<llvm::APSInt, &SMTConv::castAPSInt>(
190  Solver, Ctx, ConvertedLHS, LTy, ConvertedRHS, RTy);
191  return BVF.evalAPSInt(BSE->getOpcode(), ConvertedLHS, ConvertedRHS);
192  }
193 
194  llvm_unreachable("Unsupported expression to get symbol value!");
195  }
196 
198  SymbolReaper &SymReaper) override {
199  auto CZ = State->get<ConstraintSMT>();
200  auto &CZFactory = State->get_context<ConstraintSMT>();
201 
202  for (auto I = CZ.begin(), E = CZ.end(); I != E; ++I) {
203  if (SymReaper.isDead(I->first))
204  CZ = CZFactory.remove(CZ, *I);
205  }
206 
207  return State->set<ConstraintSMT>(CZ);
208  }
209 
210  void print(ProgramStateRef St, raw_ostream &OS, const char *nl,
211  const char *sep) override {
212 
213  auto CZ = St->get<ConstraintSMT>();
214 
215  OS << nl << sep << "Constraints:";
216  for (auto I = CZ.begin(), E = CZ.end(); I != E; ++I) {
217  OS << nl << ' ' << I->first << " : ";
218  I->second->print(OS);
219  }
220  OS << nl;
221  }
222 
223  bool canReasonAbout(SVal X) const override {
225 
227  if (!SymVal)
228  return true;
229 
230  const SymExpr *Sym = SymVal->getSymbol();
231  QualType Ty = Sym->getType();
232 
233  // Complex types are not modeled
234  if (Ty->isComplexType() || Ty->isComplexIntegerType())
235  return false;
236 
237  // Non-IEEE 754 floating-point types are not modeled
238  if ((Ty->isSpecificBuiltinType(BuiltinType::LongDouble) &&
239  (&TI.getLongDoubleFormat() == &llvm::APFloat::x87DoubleExtended() ||
240  &TI.getLongDoubleFormat() == &llvm::APFloat::PPCDoubleDouble())))
241  return false;
242 
243  if (Ty->isRealFloatingType())
244  return Solver->isFPSupported();
245 
246  if (isa<SymbolData>(Sym))
247  return true;
248 
249  SValBuilder &SVB = getSValBuilder();
250 
251  if (const SymbolCast *SC = dyn_cast<SymbolCast>(Sym))
252  return canReasonAbout(SVB.makeSymbolVal(SC->getOperand()));
253 
254  if (const BinarySymExpr *BSE = dyn_cast<BinarySymExpr>(Sym)) {
255  if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(BSE))
256  return canReasonAbout(SVB.makeSymbolVal(SIE->getLHS()));
257 
258  if (const IntSymExpr *ISE = dyn_cast<IntSymExpr>(BSE))
259  return canReasonAbout(SVB.makeSymbolVal(ISE->getRHS()));
260 
261  if (const SymSymExpr *SSE = dyn_cast<SymSymExpr>(BSE))
262  return canReasonAbout(SVB.makeSymbolVal(SSE->getLHS())) &&
263  canReasonAbout(SVB.makeSymbolVal(SSE->getRHS()));
264  }
265 
266  llvm_unreachable("Unsupported expression to reason about!");
267  }
268 
269  /// Dumps SMT formula
270  LLVM_DUMP_METHOD void dump() const { Solver->dump(); }
271 
272 protected:
273  // Check whether a new model is satisfiable, and update the program state.
275  const SMTExprRef &Exp) {
276  // Check the model, avoid simplifying AST to save time
277  if (checkModel(State, Sym, Exp).isConstrainedTrue())
278  return State->add<ConstraintSMT>(std::make_pair(Sym, Exp));
279 
280  return nullptr;
281  }
282 
283  /// Given a program state, construct the logical conjunction and add it to
284  /// the solver
286  // TODO: Don't add all the constraints, only the relevant ones
287  auto CZ = State->get<ConstraintSMT>();
288  auto I = CZ.begin(), IE = CZ.end();
289 
290  // Construct the logical AND of all the constraints
291  if (I != IE) {
292  std::vector<SMTExprRef> ASTs;
293 
294  SMTExprRef Constraint = I++->second;
295  while (I != IE) {
296  Constraint = Solver->mkAnd(Constraint, I++->second);
297  }
298 
299  Solver->addConstraint(Constraint);
300  }
301  }
302 
303  // Generate and check a Z3 model, using the given constraint.
305  const SMTExprRef &Exp) const {
306  ProgramStateRef NewState =
307  State->add<ConstraintSMT>(std::make_pair(Sym, Exp));
308 
309  llvm::FoldingSetNodeID ID;
310  NewState->get<ConstraintSMT>().Profile(ID);
311 
312  unsigned hash = ID.ComputeHash();
313  auto I = Cached.find(hash);
314  if (I != Cached.end())
315  return I->second;
316 
317  Solver->reset();
318  addStateConstraints(NewState);
319 
320  Optional<bool> res = Solver->check();
321  if (!res.hasValue())
322  Cached[hash] = ConditionTruthVal();
323  else
324  Cached[hash] = ConditionTruthVal(res.getValue());
325 
326  return Cached[hash];
327  }
328 
329  // Cache the result of an SMT query (true, false, unknown). The key is the
330  // hash of the constraints in a state
331  mutable llvm::DenseMap<unsigned, ConditionTruthVal> Cached;
332 }; // end class SMTConstraintManager
333 
334 } // namespace ento
335 } // namespace clang
336 
337 #endif
bool isConstrainedFalse() const
Return true if the constraint is perfectly constrained to &#39;false&#39;.
ConditionTruthVal checkModel(ProgramStateRef State, SymbolRef Sym, const SMTExprRef &Exp) const
A (possibly-)qualified type.
Definition: Type.h:634
SMTConstraintManager(clang::ento::SubEngine *SE, clang::ento::SValBuilder &SB)
bool isDead(SymbolRef sym)
Returns whether or not a symbol has been confirmed dead.
static SMTExprRef getRangeExpr(SMTSolverRef &Solver, ASTContext &Ctx, SymbolRef Sym, const llvm::APSInt &From, const llvm::APSInt &To, bool InRange)
Definition: SMTConv.h:490
bool isRealFloatingType() const
Floating point categories.
Definition: Type.cpp:1959
static SMTExprRef getZeroExpr(SMTSolverRef &Solver, ASTContext &Ctx, const SMTExprRef &Exp, QualType Ty, bool Assumption)
Definition: SMTConv.h:460
static SMTExprRef getExpr(SMTSolverRef &Solver, ASTContext &Ctx, SymbolRef Sym, QualType *RetTy=nullptr, bool *hasComparison=nullptr)
Definition: SMTConv.h:449
const TargetInfo & getTargetInfo() const
Definition: ASTContext.h:689
ProgramStateRef assumeSymInclusiveRange(ProgramStateRef State, SymbolRef Sym, const llvm::APSInt &From, const llvm::APSInt &To, bool InRange) override
Given a symbolic expression within the range [From, To], assume that it is true/false and generate th...
Generic base class for SMT exprs.
Definition: SMTAPI.h:99
Symbolic value.
Definition: SymExpr.h:29
static std::pair< llvm::APSInt, QualType > fixAPSInt(ASTContext &Ctx, const llvm::APSInt &Int)
Definition: SMTConv.h:536
SVal makeSymbolVal(SymbolRef Sym)
Make an SVal that represents the given symbol.
Definition: SValBuilder.h:372
Holds long-lived AST nodes (such as types and decls) that can be referred to throughout the semantic ...
Definition: ASTContext.h:154
static SMTExprRef fromData(SMTSolverRef &Solver, const SymbolID ID, const QualType &Ty, uint64_t BitWidth)
Construct an SMTExprRef from a SymbolData.
Definition: SMTConv.h:318
LineState State
bool isSpecificBuiltinType(unsigned K) const
Test for a particular builtin type.
Definition: Type.h:6520
const llvm::APSInt & Convert(const llvm::APSInt &To, const llvm::APSInt &From)
Convert - Create a new persistent APSInt with the same value as &#39;From&#39; but with the bitwidth and sign...
Represents a symbolic expression like &#39;x&#39; + 3.
virtual QualType getType() const =0
bool isConstrainedTrue() const
Return true if the constraint is perfectly constrained to &#39;true&#39;.
bool isComplexType() const
isComplexType() does not include complex integers (a GCC extension).
Definition: Type.cpp:481
const llvm::fltSemantics & getLongDoubleFormat() const
Definition: TargetInfo.h:588
Exposes information about the current target.
Definition: TargetInfo.h:161
BasicValueFactory & getBasicVals() const
virtual ProgramStateRef assumeExpr(ProgramStateRef State, SymbolRef Sym, const SMTExprRef &Exp)
ProgramStateRef removeDeadBindings(ProgramStateRef State, SymbolReaper &SymReaper) override
Scan all symbols referenced by the constraints.
Represents a cast expression.
virtual ~SMTConstraintManager()=default
Optional< T > getAs() const
Convert to the specified SVal type, returning None if this SVal is not of the desired type...
Definition: SVals.h:111
#define REGISTER_TRAIT_WITH_PROGRAMSTATE(Name, Type)
Declares a program state trait for type Type called Name, and introduce a type named NameTy...
bool canReasonAbout(SVal X) const override
canReasonAbout - Not all ConstraintManagers can accurately reason about all SVal values.
SVal - This represents a symbolic expression, which can be either an L-value or an R-value...
Definition: SVals.h:75
bool isSignedIntegerOrEnumerationType() const
Determines whether this is an integer type that is signed or an enumeration types whose underlying ty...
Definition: Type.cpp:1882
Represents a symbolic expression like 3 - &#39;x&#39;.
A class responsible for cleaning up unused symbols.
const llvm::APSInt * evalAPSInt(BinaryOperator::Opcode Op, const llvm::APSInt &V1, const llvm::APSInt &V2)
SMTSolverRef CreateZ3Solver()
Convenience method to create and Z3Solver object.
static SMTExprRef fromBinOp(SMTSolverRef &Solver, const SMTExprRef &LHS, const BinaryOperator::Opcode Op, const SMTExprRef &RHS, bool isSigned)
Construct an SMTExprRef from a binary operator.
Definition: SMTConv.h:90
ProgramStateRef assumeSymUnsupported(ProgramStateRef State, SymbolRef Sym, bool Assumption) override
Given a symbolic expression that cannot be reasoned about, assume that it is zero/nonzero and add it ...
Dataflow Directional Tag Classes.
Represents a symbolic expression involving a binary operator.
LLVM_DUMP_METHOD void dump() const
Dumps SMT formula.
bool isBooleanType() const
Definition: Type.h:6670
Represents symbolic expression that isn&#39;t a location.
Definition: SVals.h:346
std::shared_ptr< SMTSolver > SMTSolverRef
Shared pointer for SMTSolvers.
Definition: SMTAPI.h:397
Indicates that the tracking object is a descendant of a referenced-counted OSObject, used in the Darwin kernel.
ProgramStateRef assumeSym(ProgramStateRef State, SymbolRef Sym, bool Assumption) override
Given a symbolic expression that can be reasoned about, assume that it is true/false and generate the...
uint64_t getTypeSize(QualType T) const
Return the size of the specified (complete) type T, in bits.
Definition: ASTContext.h:2072
const llvm::APSInt * getSymVal(ProgramStateRef State, SymbolRef Sym) const override
If a symbol is perfectly constrained to a constant, attempt to return the concrete value...
X
Add a minimal nested name specifier fixit hint to allow lookup of a tag name from an outer enclosing ...
Definition: SemaDecl.cpp:13978
llvm::DenseMap< unsigned, ConditionTruthVal > Cached
bool isVoidType() const
Definition: Type.h:6553
virtual void addStateConstraints(ProgramStateRef State) const
Given a program state, construct the logical conjunction and add it to the solver.
bool isComplexIntegerType() const
Definition: Type.cpp:487
ConditionTruthVal checkNull(ProgramStateRef State, SymbolRef Sym) override
Returns whether or not a symbol is known to be null ("true"), known to be non-null ("false")...
void print(ProgramStateRef St, raw_ostream &OS, const char *nl, const char *sep) override
llvm::ImmutableSet< std::pair< clang::ento::SymbolRef, const clang::ento::SMTExpr * > > ConstraintSMTType
Represents a symbolic expression like &#39;x&#39; + &#39;y&#39;.
A symbol representing data which can be stored in a memory location (region).
Definition: SymExpr.h:116