clang  6.0.0svn
SimpleConstraintManager.cpp
Go to the documentation of this file.
1 //== SimpleConstraintManager.cpp --------------------------------*- C++ -*--==//
2 //
3 // The LLVM Compiler Infrastructure
4 //
5 // This file is distributed under the University of Illinois Open Source
6 // License. See LICENSE.TXT for details.
7 //
8 //===----------------------------------------------------------------------===//
9 //
10 // This file defines SimpleConstraintManager, a class that provides a
11 // simplified constraint manager interface, compared to ConstraintManager.
12 //
13 //===----------------------------------------------------------------------===//
14 
19 
20 namespace clang {
21 
22 namespace ento {
23 
25 
27  DefinedSVal Cond,
28  bool Assumption) {
29  // If we have a Loc value, cast it to a bool NonLoc first.
30  if (Optional<Loc> LV = Cond.getAs<Loc>()) {
31  SValBuilder &SVB = State->getStateManager().getSValBuilder();
32  QualType T;
33  const MemRegion *MR = LV->getAsRegion();
34  if (const TypedRegion *TR = dyn_cast_or_null<TypedRegion>(MR))
35  T = TR->getLocationType();
36  else
37  T = SVB.getContext().VoidPtrTy;
38 
39  Cond = SVB.evalCast(*LV, SVB.getContext().BoolTy, T).castAs<DefinedSVal>();
40  }
41 
42  return assume(State, Cond.castAs<NonLoc>(), Assumption);
43 }
44 
46  NonLoc Cond, bool Assumption) {
47  State = assumeAux(State, Cond, Assumption);
48  if (NotifyAssumeClients && SU)
49  return SU->processAssume(State, Cond, Assumption);
50  return State;
51 }
52 
53 ProgramStateRef SimpleConstraintManager::assumeAux(ProgramStateRef State,
54  NonLoc Cond,
55  bool Assumption) {
56 
57  // We cannot reason about SymSymExprs, and can only reason about some
58  // SymIntExprs.
59  if (!canReasonAbout(Cond)) {
60  // Just add the constraint to the expression without trying to simplify.
61  SymbolRef Sym = Cond.getAsSymExpr();
62  assert(Sym);
63  return assumeSymUnsupported(State, Sym, Assumption);
64  }
65 
66  switch (Cond.getSubKind()) {
67  default:
68  llvm_unreachable("'Assume' not implemented for this NonLoc");
69 
70  case nonloc::SymbolValKind: {
72  SymbolRef Sym = SV.getSymbol();
73  assert(Sym);
74  return assumeSym(State, Sym, Assumption);
75  }
76 
77  case nonloc::ConcreteIntKind: {
78  bool b = Cond.castAs<nonloc::ConcreteInt>().getValue() != 0;
79  bool isFeasible = b ? Assumption : !Assumption;
80  return isFeasible ? State : nullptr;
81  }
82 
83  case nonloc::PointerToMemberKind: {
84  bool IsNull = !Cond.castAs<nonloc::PointerToMember>().isNullMemberPointer();
85  bool IsFeasible = IsNull ? Assumption : !Assumption;
86  return IsFeasible ? State : nullptr;
87  }
88 
89  case nonloc::LocAsIntegerKind:
90  return assume(State, Cond.castAs<nonloc::LocAsInteger>().getLoc(),
91  Assumption);
92  } // end switch
93 }
94 
96  ProgramStateRef State, NonLoc Value, const llvm::APSInt &From,
97  const llvm::APSInt &To, bool InRange) {
98 
99  assert(From.isUnsigned() == To.isUnsigned() &&
100  From.getBitWidth() == To.getBitWidth() &&
101  "Values should have same types!");
102 
103  if (!canReasonAbout(Value)) {
104  // Just add the constraint to the expression without trying to simplify.
105  SymbolRef Sym = Value.getAsSymExpr();
106  assert(Sym);
107  return assumeSymInclusiveRange(State, Sym, From, To, InRange);
108  }
109 
110  switch (Value.getSubKind()) {
111  default:
112  llvm_unreachable("'assumeInclusiveRange' is not implemented"
113  "for this NonLoc");
114 
115  case nonloc::LocAsIntegerKind:
116  case nonloc::SymbolValKind: {
117  if (SymbolRef Sym = Value.getAsSymbol())
118  return assumeSymInclusiveRange(State, Sym, From, To, InRange);
119  return State;
120  } // end switch
121 
122  case nonloc::ConcreteIntKind: {
123  const llvm::APSInt &IntVal = Value.castAs<nonloc::ConcreteInt>().getValue();
124  bool IsInRange = IntVal >= From && IntVal <= To;
125  bool isFeasible = (IsInRange == InRange);
126  return isFeasible ? State : nullptr;
127  }
128  } // end switch
129 }
130 
131 } // end of namespace ento
132 
133 } // end of namespace clang
CanQualType VoidPtrTy
Definition: ASTContext.h:1012
A (possibly-)qualified type.
Definition: Type.h:653
MemRegion - The root abstract class for all memory regions.
Definition: MemRegion.h:79
virtual ProgramStateRef assumeSymUnsupported(ProgramStateRef State, SymbolRef Sym, bool Assumption)=0
Given a symbolic expression that cannot be reasoned about, assume that it is zero/nonzero and add it ...
SVal evalCast(SVal val, QualType castTy, QualType originalType)
Value representing integer constant.
Definition: SVals.h:353
Symbolic value.
Definition: SymExpr.h:29
Value representing pointer-to-member.
Definition: SVals.h:487
LineState State
bool NotifyAssumeClients
A flag to indicate that clients should be notified of assumptions.
SymbolRef getAsSymbol(bool IncludeBaseRegions=false) const
If this SVal wraps a symbol return that SymbolRef.
Definition: SVals.cpp:116
ProgramStateRef assumeInclusiveRange(ProgramStateRef State, NonLoc Value, const llvm::APSInt &From, const llvm::APSInt &To, bool InRange) override
virtual ProgramStateRef assumeSym(ProgramStateRef State, SymbolRef Sym, bool Assumption)=0
Given a symbolic expression that can be reasoned about, assume that it is true/false and generate the...
unsigned getSubKind() const
Definition: SVals.h:108
const FunctionProtoType * T
virtual ProgramStateRef processAssume(ProgramStateRef state, SVal cond, bool assumption)=0
Called by ConstraintManager.
static SVal getValue(SVal val, SValBuilder &svalBuilder)
Optional< T > getAs() const
Convert to the specified SVal type, returning None if this SVal is not of the desired type...
Definition: SVals.h:100
ProgramStateRef assume(ProgramStateRef State, DefinedSVal Cond, bool Assumption) override
Ensures that the DefinedSVal conditional is expressed as a NonLoc by creating boolean casts to handle...
virtual ProgramStateRef assumeSymInclusiveRange(ProgramStateRef State, SymbolRef Sym, const llvm::APSInt &From, const llvm::APSInt &To, bool InRange)=0
Given a symbolic expression within the range [From, To], assume that it is true/false and generate th...
ASTContext & getContext()
Definition: SValBuilder.h:131
virtual bool canReasonAbout(SVal X) const =0
canReasonAbout - Not all ConstraintManagers can accurately reason about all SVal values.
Dataflow Directional Tag Classes.
Represents symbolic expression.
Definition: SVals.h:327
T castAs() const
Convert to the specified SVal type, asserting that this SVal is of the desired type.
Definition: SVals.h:92
SymbolRef getSymbol() const
Definition: SVals.h:332
const SymExpr * getAsSymExpr() const
Definition: SVals.cpp:133
CanQualType BoolTy
Definition: ASTContext.h:997
TypedRegion - An abstract class representing regions that are typed.
Definition: MemRegion.h:487