| 1 | //===- BoundsChecking.cpp - Bounds checking related APIs --------*- 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 implements 'checkBounds', a function that compares memory offsets |
| 10 | // (that may be symbolic) and uses heuristical workarounds to provide more |
| 11 | // accurate results than the 'naive' evalBinOp calls. |
| 12 | // |
| 13 | //===----------------------------------------------------------------------===// |
| 14 | |
| 15 | #include "clang/StaticAnalyzer/Checkers/BoundsChecking.h" |
| 16 | |
| 17 | using namespace clang; |
| 18 | using namespace ento; |
| 19 | |
| 20 | // NOTE: This function is the "heart" of this algorithm. It simplifies |
| 21 | // inequalities with transformations that are valid (and very elementary) in |
| 22 | // pure mathematics, but become invalid if we use them in C++ number model |
| 23 | // where the calculations may overflow. |
| 24 | // Due to the overflow issues I think it's impossible (or at least not |
| 25 | // practical) to integrate this kind of simplification into the resolution of |
| 26 | // arbitrary inequalities (i.e. the code of `evalBinOp`); but this function |
| 27 | // produces valid results when the calculations are handling memory offsets |
| 28 | // and every value is well below SIZE_MAX. |
| 29 | // NOTE: the simplification preserves the order of the two operands in a |
| 30 | // mathematical sense, but it may change the result produced by a C++ |
| 31 | // comparison operator (and the automatic type conversions). |
| 32 | // For example, consider a comparison "X+1 < 0", where the LHS is stored as a |
| 33 | // size_t and the RHS is stored in an int. (As size_t is unsigned, this |
| 34 | // comparison is false for all values of "X".) However, the simplification may |
| 35 | // turn it into "X < -1", which is still always false in a mathematical sense, |
| 36 | // but can produce a true result when evaluated by `evalBinOp` (which follows |
| 37 | // the rules of C++ and casts -1 to SIZE_MAX). |
| 38 | static std::pair<NonLoc, nonloc::ConcreteInt> |
| 39 | getSimplifiedOffsets(NonLoc Offset, nonloc::ConcreteInt Extent, |
| 40 | SValBuilder &SVB) { |
| 41 | const llvm::APSInt &ExtentVal = Extent.getValue(); |
| 42 | std::optional<nonloc::SymbolVal> SymVal = Offset.getAs<nonloc::SymbolVal>(); |
| 43 | if (SymVal && SymVal->isExpression()) { |
| 44 | if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(Val: SymVal->getSymbol())) { |
| 45 | llvm::APSInt Num = APSIntType(ExtentVal).convert(Value: SIE->getRHS()); |
| 46 | switch (SIE->getOpcode()) { |
| 47 | case BO_Mul: |
| 48 | // The Num should never be 0 here, because multiplication by zero |
| 49 | // is simplified by the engine. |
| 50 | if ((ExtentVal % Num) != 0) |
| 51 | return std::pair<NonLoc, nonloc::ConcreteInt>(Offset, Extent); |
| 52 | else |
| 53 | return getSimplifiedOffsets(Offset: nonloc::SymbolVal(SIE->getLHS()), |
| 54 | Extent: SVB.makeIntVal(integer: ExtentVal / Num), SVB); |
| 55 | case BO_Add: |
| 56 | return getSimplifiedOffsets(Offset: nonloc::SymbolVal(SIE->getLHS()), |
| 57 | Extent: SVB.makeIntVal(integer: ExtentVal - Num), SVB); |
| 58 | default: |
| 59 | break; |
| 60 | } |
| 61 | } |
| 62 | } |
| 63 | |
| 64 | return std::pair<NonLoc, nonloc::ConcreteInt>(Offset, Extent); |
| 65 | } |
| 66 | |
| 67 | static bool isNegative(SValBuilder &SVB, ProgramStateRef State, NonLoc Value) { |
| 68 | const llvm::APSInt *MaxV = SVB.getMaxValue(state: State, val: Value); |
| 69 | return MaxV && MaxV->isNegative(); |
| 70 | } |
| 71 | |
| 72 | static bool isUnsigned(SValBuilder &SVB, NonLoc Value) { |
| 73 | QualType T = Value.getType(SVB.getContext()); |
| 74 | return T->isUnsignedIntegerType(); |
| 75 | } |
| 76 | |
| 77 | std::pair<ProgramStateRef, ProgramStateRef> |
| 78 | bounds::compareValueToThreshold(ProgramStateRef State, SValBuilder &SVB, |
| 79 | NonLoc Value, NonLoc Threshold, |
| 80 | Comparison CmpKind) { |
| 81 | if (auto ConcreteThreshold = Threshold.getAs<nonloc::ConcreteInt>()) { |
| 82 | std::tie(args&: Value, args&: Threshold) = |
| 83 | getSimplifiedOffsets(Offset: Value, Extent: *ConcreteThreshold, SVB); |
| 84 | } |
| 85 | |
| 86 | // We want to perform a _mathematical_ comparison between the numbers `Value` |
| 87 | // and `Threshold`; but `evalBinOpNN` evaluates a C/C++ operator that may |
| 88 | // perform automatic conversions. For example the number -1 is less than the |
| 89 | // number 1000, but -1 < `1000ull` will evaluate to `false` because the `int` |
| 90 | // -1 is converted to ULONGLONG_MAX. |
| 91 | // To avoid automatic conversions, we evaluate the "obvious" cases without |
| 92 | // calling `evalBinOpNN`: |
| 93 | if (isNegative(SVB, State, Value) && isUnsigned(SVB, Value: Threshold)) { |
| 94 | if (CmpKind == Comparison::EQ) { |
| 95 | // negative == unsigned is always false |
| 96 | return {nullptr, State}; |
| 97 | } |
| 98 | // negative < unsigned and negative <= unsigned are always true |
| 99 | return {State, nullptr}; |
| 100 | } |
| 101 | if (isUnsigned(SVB, Value) && isNegative(SVB, State, Value: Threshold)) { |
| 102 | // unsigned == negative, unsigned < negative and unsigned <= negative are |
| 103 | // all always false |
| 104 | return {nullptr, State}; |
| 105 | } |
| 106 | // FIXME: These special cases are sufficient for handling real-world |
| 107 | // comparisons, but in theory there could be contrived situations where |
| 108 | // automatic conversion of a symbolic value (which can be negative and can be |
| 109 | // positive) leads to incorrect results. |
| 110 | // NOTE: We NEED to use the `evalBinOpNN` call in the "common" case, because |
| 111 | // we want to ensure that assumptions coming from this precondition and |
| 112 | // assumptions coming from regular C/C++ operator calls are represented by |
| 113 | // constraints on the same symbolic expression. A solution that would |
| 114 | // evaluate these "mathematical" comparisons through a separate pathway would |
| 115 | // be a step backwards in this sense. |
| 116 | |
| 117 | const BinaryOperatorKind OpKind = asOpcode(C: CmpKind); |
| 118 | auto BelowThreshold = |
| 119 | SVB.evalBinOpNN(state: State, op: OpKind, lhs: Value, rhs: Threshold, resultTy: SVB.getConditionType()) |
| 120 | .getAs<NonLoc>(); |
| 121 | |
| 122 | if (BelowThreshold) |
| 123 | return State->assume(Cond: *BelowThreshold); |
| 124 | |
| 125 | return {nullptr, nullptr}; |
| 126 | } |
| 127 | |
| 128 | bounds::CheckResult bounds::checkBounds(ProgramStateRef State, SValBuilder &SVB, |
| 129 | NonLoc Offset, |
| 130 | std::optional<NonLoc> Extent, |
| 131 | bounds::CheckFlags Flags) { |
| 132 | |
| 133 | bounds::CheckResult Res(Offset); |
| 134 | |
| 135 | // CHECK LOWER BOUND |
| 136 | if (Flags.CheckUnderflow) { |
| 137 | auto [PrecedesLowerBound, WithinLowerBound] = compareValueToThreshold( |
| 138 | State, SVB, Value: Offset, Threshold: SVB.makeZeroArrayIndex(), CmpKind: Comparison::LT); |
| 139 | |
| 140 | if (PrecedesLowerBound) { |
| 141 | // The analyzer thinks that the offset may be invalid (negative)... |
| 142 | if (Flags.OffsetObviouslyNonnegative) { |
| 143 | // ...but the offset is obviously non-negative (clear array subscript |
| 144 | // with an unsigned index), so we're in a buggy situation. |
| 145 | |
| 146 | // TODO: Currently the analyzer ignores many casts (e.g. signed -> |
| 147 | // unsigned casts), so it can easily reach states where it will load a |
| 148 | // signed (and negative) value from an unsigned variable. This sanity |
| 149 | // check is a duct tape "solution" that silences most of the ugly false |
| 150 | // positives that are caused by this buggy behavior. Note that this is |
| 151 | // not a complete solution: this cannot silence reports where pointer |
| 152 | // arithmetic complicates the picture and cannot ensure modeling of the |
| 153 | // "unsigned index is positive with highest bit set" cases which are |
| 154 | // "usurped" by the nonsense "unsigned index is negative" case. |
| 155 | // For more information about this topic, see the umbrella ticket |
| 156 | // https://github.com/llvm/llvm-project/issues/39492 |
| 157 | // TODO: Remove this hack once 'SymbolCast's are modeled properly. |
| 158 | |
| 159 | if (!WithinLowerBound) { |
| 160 | // The state is completely nonsense -- let's just sink it! |
| 161 | Res.IsCorruptedState = true; |
| 162 | return Res; |
| 163 | } |
| 164 | // Otherwise continue on the 'WithinLowerBound' branch where the |
| 165 | // unsigned index _is_ non-negative. Don't mention this assumption as a |
| 166 | // note tag, because it would just confuse the users! |
| 167 | } else { |
| 168 | Res.MayUnderflow = true; |
| 169 | |
| 170 | if (!WithinLowerBound) { |
| 171 | // ...and it cannot be valid (>= 0), so report an error. |
| 172 | return Res; |
| 173 | } |
| 174 | } |
| 175 | } |
| 176 | |
| 177 | // Actually update the state. The "if" only fails in the extremely unlikely |
| 178 | // case when compareValueToThreshold returns {nullptr, nullptr} because |
| 179 | // evalBinOpNN fails to evaluate the less-than operator. |
| 180 | if (WithinLowerBound) |
| 181 | State = WithinLowerBound; |
| 182 | } |
| 183 | |
| 184 | // CHECK UPPER BOUND |
| 185 | if (Extent) { |
| 186 | Comparison CK = Flags.AlsoAcceptEquality ? Comparison::LE : Comparison::LT; |
| 187 | auto [WithinUpperBound, ExceedsUpperBound] = |
| 188 | compareValueToThreshold(State, SVB, Value: Offset, Threshold: *Extent, /*CmpKind=*/CK); |
| 189 | |
| 190 | if (ExceedsUpperBound) { |
| 191 | // The offset may be invalid (>= Size)... |
| 192 | Res.ExtentIfMayOverflow = Extent; |
| 193 | |
| 194 | if (!WithinUpperBound) { |
| 195 | // ...and it cannot be within bounds. |
| 196 | return Res; |
| 197 | } |
| 198 | } |
| 199 | if (WithinUpperBound) |
| 200 | State = WithinUpperBound; |
| 201 | } |
| 202 | |
| 203 | Res.InBoundsState = State; |
| 204 | return Res; |
| 205 | } |
| 206 | |