1 | //===- ConstraintManager.cpp - Constraints on symbolic values. ------------===// |
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 defined the interface to manage constraints on symbolic values. |
10 | // |
11 | //===----------------------------------------------------------------------===// |
12 | |
13 | #include "clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h" |
14 | #include "clang/AST/Type.h" |
15 | #include "clang/StaticAnalyzer/Core/PathSensitive/MemRegion.h" |
16 | #include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h" |
17 | #include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState_Fwd.h" |
18 | #include "clang/StaticAnalyzer/Core/PathSensitive/SVals.h" |
19 | #include "llvm/ADT/ScopeExit.h" |
20 | |
21 | using namespace clang; |
22 | using namespace ento; |
23 | |
24 | ConstraintManager::~ConstraintManager() = default; |
25 | |
26 | static DefinedSVal getLocFromSymbol(const ProgramStateRef &State, |
27 | SymbolRef Sym) { |
28 | const MemRegion *R = |
29 | State->getStateManager().getRegionManager().getSymbolicRegion(Sym); |
30 | return loc::MemRegionVal(R); |
31 | } |
32 | |
33 | ConditionTruthVal ConstraintManager::checkNull(ProgramStateRef State, |
34 | SymbolRef Sym) { |
35 | QualType Ty = Sym->getType(); |
36 | DefinedSVal V = Loc::isLocType(T: Ty) ? getLocFromSymbol(State, Sym) |
37 | : nonloc::SymbolVal(Sym); |
38 | const ProgramStatePair &P = assumeDual(State, Cond: V); |
39 | if (P.first && !P.second) |
40 | return ConditionTruthVal(false); |
41 | if (!P.first && P.second) |
42 | return ConditionTruthVal(true); |
43 | return {}; |
44 | } |
45 | |
46 | template <typename AssumeFunction> |
47 | ConstraintManager::ProgramStatePair |
48 | ConstraintManager::assumeDualImpl(ProgramStateRef &State, |
49 | AssumeFunction &Assume) { |
50 | if (LLVM_UNLIKELY(State->isPosteriorlyOverconstrained())) |
51 | return {State, State}; |
52 | |
53 | // Assume functions might recurse (see `reAssume` or `tryRearrange`). During |
54 | // the recursion the State might not change anymore, that means we reached a |
55 | // fixpoint. |
56 | // We avoid infinite recursion of assume calls by checking already visited |
57 | // States on the stack of assume function calls. |
58 | const ProgramState *RawSt = State.get(); |
59 | if (LLVM_UNLIKELY(AssumeStack.contains(RawSt))) |
60 | return {State, State}; |
61 | AssumeStack.push(S: RawSt); |
62 | auto AssumeStackBuilder = |
63 | llvm::make_scope_exit([this]() { AssumeStack.pop(); }); |
64 | |
65 | ProgramStateRef StTrue = Assume(true); |
66 | |
67 | if (!StTrue) { |
68 | ProgramStateRef StFalse = Assume(false); |
69 | if (LLVM_UNLIKELY(!StFalse)) { // both infeasible |
70 | ProgramStateRef StInfeasible = State->cloneAsPosteriorlyOverconstrained(); |
71 | assert(StInfeasible->isPosteriorlyOverconstrained()); |
72 | // Checkers might rely on the API contract that both returned states |
73 | // cannot be null. Thus, we return StInfeasible for both branches because |
74 | // it might happen that a Checker uncoditionally uses one of them if the |
75 | // other is a nullptr. This may also happen with the non-dual and |
76 | // adjacent `assume(true)` and `assume(false)` calls. By implementing |
77 | // assume in therms of assumeDual, we can keep our API contract there as |
78 | // well. |
79 | return ProgramStatePair(StInfeasible, StInfeasible); |
80 | } |
81 | return ProgramStatePair(nullptr, StFalse); |
82 | } |
83 | |
84 | ProgramStateRef StFalse = Assume(false); |
85 | if (!StFalse) { |
86 | return ProgramStatePair(StTrue, nullptr); |
87 | } |
88 | |
89 | return ProgramStatePair(StTrue, StFalse); |
90 | } |
91 | |
92 | ConstraintManager::ProgramStatePair |
93 | ConstraintManager::assumeDual(ProgramStateRef State, DefinedSVal Cond) { |
94 | auto AssumeFun = [&, Cond](bool Assumption) { |
95 | return assumeInternal(state: State, Cond, Assumption); |
96 | }; |
97 | return assumeDualImpl(State, Assume&: AssumeFun); |
98 | } |
99 | |
100 | ConstraintManager::ProgramStatePair |
101 | ConstraintManager::assumeInclusiveRangeDual(ProgramStateRef State, NonLoc Value, |
102 | const llvm::APSInt &From, |
103 | const llvm::APSInt &To) { |
104 | auto AssumeFun = [&](bool Assumption) { |
105 | return assumeInclusiveRangeInternal(State, Value, From, To, InBound: Assumption); |
106 | }; |
107 | return assumeDualImpl(State, Assume&: AssumeFun); |
108 | } |
109 | |
110 | ProgramStateRef ConstraintManager::assume(ProgramStateRef State, |
111 | DefinedSVal Cond, bool Assumption) { |
112 | ConstraintManager::ProgramStatePair R = assumeDual(State, Cond); |
113 | return Assumption ? R.first : R.second; |
114 | } |
115 | |
116 | ProgramStateRef |
117 | ConstraintManager::assumeInclusiveRange(ProgramStateRef State, NonLoc Value, |
118 | const llvm::APSInt &From, |
119 | const llvm::APSInt &To, bool InBound) { |
120 | ConstraintManager::ProgramStatePair R = |
121 | assumeInclusiveRangeDual(State, Value, From, To); |
122 | return InBound ? R.first : R.second; |
123 | } |
124 | |