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(Ty) ? getLocFromSymbol(State, Sym) |

37 | : nonloc::SymbolVal(Sym); |

38 | const ProgramStatePair &P = assumeDual(State, 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(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 = [&](bool Assumption) { |

95 | return assumeInternal(State, Cond, Assumption); |

96 | }; |

97 | return assumeDualImpl(State, 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, Assumption); |

106 | }; |

107 | return assumeDualImpl(State, 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 |