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 
20 
21 typedef llvm::ImmutableSet<
22  std::pair<clang::ento::SymbolRef, const llvm::SMTExpr *>>
25 
26 namespace clang {
27 namespace ento {
28 
30  mutable llvm::SMTSolverRef Solver = llvm::CreateZ3Solver();
31 
32 public:
34  : SimpleConstraintManager(SE, SB) {}
35  virtual ~SMTConstraintManager() = default;
36 
37  //===------------------------------------------------------------------===//
38  // Implementation for interface from SimpleConstraintManager.
39  //===------------------------------------------------------------------===//
40 
42  bool Assumption) override {
44 
45  QualType RetTy;
46  bool hasComparison;
47 
48  llvm::SMTExprRef Exp =
49  SMTConv::getExpr(Solver, Ctx, Sym, &RetTy, &hasComparison);
50 
51  // Create zero comparison for implicit boolean cast, with reversed
52  // assumption
53  if (!hasComparison && !RetTy->isBooleanType())
54  return assumeExpr(
55  State, Sym,
56  SMTConv::getZeroExpr(Solver, Ctx, Exp, RetTy, !Assumption));
57 
58  return assumeExpr(State, Sym, Assumption ? Exp : Solver->mkNot(Exp));
59  }
60 
62  const llvm::APSInt &From,
63  const llvm::APSInt &To,
64  bool InRange) override {
66  return assumeExpr(
67  State, Sym, SMTConv::getRangeExpr(Solver, Ctx, Sym, From, To, InRange));
68  }
69 
71  bool Assumption) override {
72  // Skip anything that is unsupported
73  return State;
74  }
75 
76  //===------------------------------------------------------------------===//
77  // Implementation for interface from ConstraintManager.
78  //===------------------------------------------------------------------===//
79 
82 
83  QualType RetTy;
84  // The expression may be casted, so we cannot call getZ3DataExpr() directly
85  llvm::SMTExprRef VarExp = SMTConv::getExpr(Solver, Ctx, Sym, &RetTy);
86  llvm::SMTExprRef Exp =
87  SMTConv::getZeroExpr(Solver, Ctx, VarExp, RetTy, /*Assumption=*/true);
88 
89  // Negate the constraint
90  llvm::SMTExprRef NotExp =
91  SMTConv::getZeroExpr(Solver, Ctx, VarExp, RetTy, /*Assumption=*/false);
92 
93  ConditionTruthVal isSat = checkModel(State, Sym, Exp);
94  ConditionTruthVal isNotSat = checkModel(State, Sym, NotExp);
95 
96  // Zero is the only possible solution
97  if (isSat.isConstrainedTrue() && isNotSat.isConstrainedFalse())
98  return true;
99 
100  // Zero is not a solution
101  if (isSat.isConstrainedFalse() && isNotSat.isConstrainedTrue())
102  return false;
103 
104  // Zero may be a solution
105  return ConditionTruthVal();
106  }
107 
108  const llvm::APSInt *getSymVal(ProgramStateRef State,
109  SymbolRef Sym) const override {
111  ASTContext &Ctx = BVF.getContext();
112 
113  if (const SymbolData *SD = dyn_cast<SymbolData>(Sym)) {
114  QualType Ty = Sym->getType();
115  assert(!Ty->isRealFloatingType());
116  llvm::APSInt Value(Ctx.getTypeSize(Ty),
118 
119  // TODO: this should call checkModel so we can use the cache, however,
120  // this method tries to get the interpretation (the actual value) from
121  // the solver, which is currently not cached.
122 
123  llvm::SMTExprRef Exp =
124  SMTConv::fromData(Solver, SD->getSymbolID(), Ty, Ctx.getTypeSize(Ty));
125 
126  Solver->reset();
127  addStateConstraints(State);
128 
129  // Constraints are unsatisfiable
130  Optional<bool> isSat = Solver->check();
131  if (!isSat.hasValue() || !isSat.getValue())
132  return nullptr;
133 
134  // Model does not assign interpretation
135  if (!Solver->getInterpretation(Exp, Value))
136  return nullptr;
137 
138  // A value has been obtained, check if it is the only value
139  llvm::SMTExprRef NotExp = SMTConv::fromBinOp(
140  Solver, Exp, BO_NE,
141  Ty->isBooleanType() ? Solver->mkBoolean(Value.getBoolValue())
142  : Solver->mkBitvector(Value, Value.getBitWidth()),
143  /*isSigned=*/false);
144 
145  Solver->addConstraint(NotExp);
146 
147  Optional<bool> isNotSat = Solver->check();
148  if (!isSat.hasValue() || isNotSat.getValue())
149  return nullptr;
150 
151  // This is the only solution, store it
152  return &BVF.getValue(Value);
153  }
154 
155  if (const SymbolCast *SC = dyn_cast<SymbolCast>(Sym)) {
156  SymbolRef CastSym = SC->getOperand();
157  QualType CastTy = SC->getType();
158  // Skip the void type
159  if (CastTy->isVoidType())
160  return nullptr;
161 
162  const llvm::APSInt *Value;
163  if (!(Value = getSymVal(State, CastSym)))
164  return nullptr;
165  return &BVF.Convert(SC->getType(), *Value);
166  }
167 
168  if (const BinarySymExpr *BSE = dyn_cast<BinarySymExpr>(Sym)) {
169  const llvm::APSInt *LHS, *RHS;
170  if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(BSE)) {
171  LHS = getSymVal(State, SIE->getLHS());
172  RHS = &SIE->getRHS();
173  } else if (const IntSymExpr *ISE = dyn_cast<IntSymExpr>(BSE)) {
174  LHS = &ISE->getLHS();
175  RHS = getSymVal(State, ISE->getRHS());
176  } else if (const SymSymExpr *SSM = dyn_cast<SymSymExpr>(BSE)) {
177  // Early termination to avoid expensive call
178  LHS = getSymVal(State, SSM->getLHS());
179  RHS = LHS ? getSymVal(State, SSM->getRHS()) : nullptr;
180  } else {
181  llvm_unreachable("Unsupported binary expression to get symbol value!");
182  }
183 
184  if (!LHS || !RHS)
185  return nullptr;
186 
187  llvm::APSInt ConvertedLHS, ConvertedRHS;
188  QualType LTy, RTy;
189  std::tie(ConvertedLHS, LTy) = SMTConv::fixAPSInt(Ctx, *LHS);
190  std::tie(ConvertedRHS, RTy) = SMTConv::fixAPSInt(Ctx, *RHS);
191  SMTConv::doIntTypeConversion<llvm::APSInt, &SMTConv::castAPSInt>(
192  Solver, Ctx, ConvertedLHS, LTy, ConvertedRHS, RTy);
193  return BVF.evalAPSInt(BSE->getOpcode(), ConvertedLHS, ConvertedRHS);
194  }
195 
196  llvm_unreachable("Unsupported expression to get symbol value!");
197  }
198 
200  SymbolReaper &SymReaper) override {
201  auto CZ = State->get<ConstraintSMT>();
202  auto &CZFactory = State->get_context<ConstraintSMT>();
203 
204  for (auto I = CZ.begin(), E = CZ.end(); I != E; ++I) {
205  if (SymReaper.isDead(I->first))
206  CZ = CZFactory.remove(CZ, *I);
207  }
208 
209  return State->set<ConstraintSMT>(CZ);
210  }
211 
212  void printJson(raw_ostream &Out, ProgramStateRef State, const char *NL = "\n",
213  unsigned int Space = 0, bool IsDot = false) const override {
214  ConstraintSMTType Constraints = State->get<ConstraintSMT>();
215 
216  Indent(Out, Space, IsDot) << "\"constraints\": ";
217  if (Constraints.isEmpty()) {
218  Out << "null," << NL;
219  return;
220  }
221 
222  ++Space;
223  Out << '[' << NL;
224  for (ConstraintSMTType::iterator I = Constraints.begin();
225  I != Constraints.end(); ++I) {
226  Indent(Out, Space, IsDot)
227  << "{ \"symbol\": \"" << I->first << "\", \"range\": \"";
228  I->second->print(Out);
229  Out << "\" }";
230 
231  if (std::next(I) != Constraints.end())
232  Out << ',';
233  Out << NL;
234  }
235 
236  --Space;
237  Indent(Out, Space, IsDot) << "],";
238  }
239 
241  ProgramStateRef S2) const override {
242  return S1->get<ConstraintSMT>() == S2->get<ConstraintSMT>();
243  }
244 
245  bool canReasonAbout(SVal X) const override {
247 
249  if (!SymVal)
250  return true;
251 
252  const SymExpr *Sym = SymVal->getSymbol();
253  QualType Ty = Sym->getType();
254 
255  // Complex types are not modeled
256  if (Ty->isComplexType() || Ty->isComplexIntegerType())
257  return false;
258 
259  // Non-IEEE 754 floating-point types are not modeled
260  if ((Ty->isSpecificBuiltinType(BuiltinType::LongDouble) &&
261  (&TI.getLongDoubleFormat() == &llvm::APFloat::x87DoubleExtended() ||
262  &TI.getLongDoubleFormat() == &llvm::APFloat::PPCDoubleDouble())))
263  return false;
264 
265  if (Ty->isRealFloatingType())
266  return Solver->isFPSupported();
267 
268  if (isa<SymbolData>(Sym))
269  return true;
270 
271  SValBuilder &SVB = getSValBuilder();
272 
273  if (const SymbolCast *SC = dyn_cast<SymbolCast>(Sym))
274  return canReasonAbout(SVB.makeSymbolVal(SC->getOperand()));
275 
276  if (const BinarySymExpr *BSE = dyn_cast<BinarySymExpr>(Sym)) {
277  if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(BSE))
278  return canReasonAbout(SVB.makeSymbolVal(SIE->getLHS()));
279 
280  if (const IntSymExpr *ISE = dyn_cast<IntSymExpr>(BSE))
281  return canReasonAbout(SVB.makeSymbolVal(ISE->getRHS()));
282 
283  if (const SymSymExpr *SSE = dyn_cast<SymSymExpr>(BSE))
284  return canReasonAbout(SVB.makeSymbolVal(SSE->getLHS())) &&
285  canReasonAbout(SVB.makeSymbolVal(SSE->getRHS()));
286  }
287 
288  llvm_unreachable("Unsupported expression to reason about!");
289  }
290 
291  /// Dumps SMT formula
292  LLVM_DUMP_METHOD void dump() const { Solver->dump(); }
293 
294 protected:
295  // Check whether a new model is satisfiable, and update the program state.
297  const llvm::SMTExprRef &Exp) {
298  // Check the model, avoid simplifying AST to save time
299  if (checkModel(State, Sym, Exp).isConstrainedTrue())
300  return State->add<ConstraintSMT>(std::make_pair(Sym, Exp));
301 
302  return nullptr;
303  }
304 
305  /// Given a program state, construct the logical conjunction and add it to
306  /// the solver
308  // TODO: Don't add all the constraints, only the relevant ones
309  auto CZ = State->get<ConstraintSMT>();
310  auto I = CZ.begin(), IE = CZ.end();
311 
312  // Construct the logical AND of all the constraints
313  if (I != IE) {
314  std::vector<llvm::SMTExprRef> ASTs;
315 
316  llvm::SMTExprRef Constraint = I++->second;
317  while (I != IE) {
318  Constraint = Solver->mkAnd(Constraint, I++->second);
319  }
320 
321  Solver->addConstraint(Constraint);
322  }
323  }
324 
325  // Generate and check a Z3 model, using the given constraint.
327  const llvm::SMTExprRef &Exp) const {
328  ProgramStateRef NewState =
329  State->add<ConstraintSMT>(std::make_pair(Sym, Exp));
330 
331  llvm::FoldingSetNodeID ID;
332  NewState->get<ConstraintSMT>().Profile(ID);
333 
334  unsigned hash = ID.ComputeHash();
335  auto I = Cached.find(hash);
336  if (I != Cached.end())
337  return I->second;
338 
339  Solver->reset();
340  addStateConstraints(NewState);
341 
342  Optional<bool> res = Solver->check();
343  if (!res.hasValue())
344  Cached[hash] = ConditionTruthVal();
345  else
346  Cached[hash] = ConditionTruthVal(res.getValue());
347 
348  return Cached[hash];
349  }
350 
351  // Cache the result of an SMT query (true, false, unknown). The key is the
352  // hash of the constraints in a state
353  mutable llvm::DenseMap<unsigned, ConditionTruthVal> Cached;
354 }; // end class SMTConstraintManager
355 
356 } // namespace ento
357 } // namespace clang
358 
359 #endif
bool isConstrainedFalse() const
Return true if the constraint is perfectly constrained to &#39;false&#39;.
A (possibly-)qualified type.
Definition: Type.h:643
SMTConstraintManager(clang::ento::SubEngine *SE, clang::ento::SValBuilder &SB)
bool isDead(SymbolRef sym)
Returns whether or not a symbol has been confirmed dead.
bool isRealFloatingType() const
Floating point categories.
Definition: Type.cpp:1968
const TargetInfo & getTargetInfo() const
Definition: ASTContext.h:693
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...
llvm::ImmutableSet< std::pair< clang::ento::SymbolRef, const llvm::SMTExpr * > > ConstraintSMTType
Symbolic value.
Definition: SymExpr.h:29
static std::pair< llvm::APSInt, QualType > fixAPSInt(ASTContext &Ctx, const llvm::APSInt &Int)
Definition: SMTConv.h:550
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
LineState State
bool isSpecificBuiltinType(unsigned K) const
Test for a particular builtin type.
Definition: Type.h:6577
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...
void printJson(raw_ostream &Out, ProgramStateRef State, const char *NL="\, unsigned int Space=0, bool IsDot=false) const override
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;.
virtual ProgramStateRef assumeExpr(ProgramStateRef State, SymbolRef Sym, const llvm::SMTExprRef &Exp)
bool isComplexType() const
isComplexType() does not include complex integers (a GCC extension).
Definition: Type.cpp:481
const llvm::fltSemantics & getLongDoubleFormat() const
Definition: TargetInfo.h:590
Exposes information about the current target.
Definition: TargetInfo.h:161
BasicValueFactory & getBasicVals() const
ProgramStateRef removeDeadBindings(ProgramStateRef State, SymbolReaper &SymReaper) override
Scan all symbols referenced by the constraints.
static llvm::SMTExprRef getZeroExpr(llvm::SMTSolverRef &Solver, ASTContext &Ctx, const llvm::SMTExprRef &Exp, QualType Ty, bool Assumption)
Definition: SMTConv.h:473
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...
static llvm::SMTExprRef getExpr(llvm::SMTSolverRef &Solver, ASTContext &Ctx, SymbolRef Sym, QualType *RetTy=nullptr, bool *hasComparison=nullptr)
Definition: SMTConv.h:461
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:1891
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)
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.
static llvm::SMTExprRef fromBinOp(llvm::SMTSolverRef &Solver, const llvm::SMTExprRef &LHS, const BinaryOperator::Opcode Op, const llvm::SMTExprRef &RHS, bool isSigned)
Construct an SMTSolverRef from a binary operator.
Definition: SMTConv.h:90
bool isBooleanType() const
Definition: Type.h:6727
Represents symbolic expression that isn&#39;t a location.
Definition: SVals.h:349
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:2079
ConditionTruthVal checkModel(ProgramStateRef State, SymbolRef Sym, const llvm::SMTExprRef &Exp) const
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...
static llvm::SMTExprRef fromData(llvm::SMTSolverRef &Solver, const SymbolID ID, const QualType &Ty, uint64_t BitWidth)
Construct an SMTSolverRef from a SymbolData.
Definition: SMTConv.h:322
X
Add a minimal nested name specifier fixit hint to allow lookup of a tag name from an outer enclosing ...
Definition: SemaDecl.cpp:14125
llvm::DenseMap< unsigned, ConditionTruthVal > Cached
bool isVoidType() const
Definition: Type.h:6610
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
raw_ostream & Indent(raw_ostream &Out, const unsigned int Space, bool IsDot)
Definition: JsonSupport.h:19
bool haveEqualConstraints(ProgramStateRef S1, ProgramStateRef S2) const override
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")...
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
static llvm::SMTExprRef getRangeExpr(llvm::SMTSolverRef &Solver, ASTContext &Ctx, SymbolRef Sym, const llvm::APSInt &From, const llvm::APSInt &To, bool InRange)
Definition: SMTConv.h:504
res[0]
Definition: emmintrin.h:1141