Details | Last modification | View Log | RSS feed
| Rev | Author | Line No. | Line |
|---|---|---|---|
| 14 | pmbaty | 1 | //== RangedConstraintManager.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 | // Ranged constraint manager, built on SimpleConstraintManager. |
||
| 10 | // |
||
| 11 | //===----------------------------------------------------------------------===// |
||
| 12 | |||
| 13 | #ifndef LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_RANGEDCONSTRAINTMANAGER_H |
||
| 14 | #define LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_RANGEDCONSTRAINTMANAGER_H |
||
| 15 | |||
| 16 | #include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h" |
||
| 17 | #include "clang/StaticAnalyzer/Core/PathSensitive/ProgramStateTrait.h" |
||
| 18 | #include "clang/StaticAnalyzer/Core/PathSensitive/SimpleConstraintManager.h" |
||
| 19 | #include "llvm/ADT/APSInt.h" |
||
| 20 | #include "llvm/Support/Allocator.h" |
||
| 21 | |||
| 22 | namespace clang { |
||
| 23 | |||
| 24 | namespace ento { |
||
| 25 | |||
| 26 | /// A Range represents the closed range [from, to]. The caller must |
||
| 27 | /// guarantee that from <= to. Note that Range is immutable, so as not |
||
| 28 | /// to subvert RangeSet's immutability. |
||
| 29 | class Range { |
||
| 30 | public: |
||
| 31 | Range(const llvm::APSInt &From, const llvm::APSInt &To) : Impl(&From, &To) { |
||
| 32 | assert(From <= To); |
||
| 33 | } |
||
| 34 | |||
| 35 | Range(const llvm::APSInt &Point) : Range(Point, Point) {} |
||
| 36 | |||
| 37 | bool Includes(const llvm::APSInt &Point) const { |
||
| 38 | return From() <= Point && Point <= To(); |
||
| 39 | } |
||
| 40 | const llvm::APSInt &From() const { return *Impl.first; } |
||
| 41 | const llvm::APSInt &To() const { return *Impl.second; } |
||
| 42 | const llvm::APSInt *getConcreteValue() const { |
||
| 43 | return &From() == &To() ? &From() : nullptr; |
||
| 44 | } |
||
| 45 | |||
| 46 | void Profile(llvm::FoldingSetNodeID &ID) const { |
||
| 47 | ID.AddPointer(&From()); |
||
| 48 | ID.AddPointer(&To()); |
||
| 49 | } |
||
| 50 | void dump(raw_ostream &OS) const; |
||
| 51 | void dump() const; |
||
| 52 | |||
| 53 | // In order to keep non-overlapping ranges sorted, we can compare only From |
||
| 54 | // points. |
||
| 55 | bool operator<(const Range &RHS) const { return From() < RHS.From(); } |
||
| 56 | |||
| 57 | bool operator==(const Range &RHS) const { return Impl == RHS.Impl; } |
||
| 58 | bool operator!=(const Range &RHS) const { return !operator==(RHS); } |
||
| 59 | |||
| 60 | private: |
||
| 61 | std::pair<const llvm::APSInt *, const llvm::APSInt *> Impl; |
||
| 62 | }; |
||
| 63 | |||
| 64 | /// @class RangeSet is a persistent set of non-overlapping ranges. |
||
| 65 | /// |
||
| 66 | /// New RangeSet objects can be ONLY produced by RangeSet::Factory object, which |
||
| 67 | /// also supports the most common operations performed on range sets. |
||
| 68 | /// |
||
| 69 | /// Empty set corresponds to an overly constrained symbol meaning that there |
||
| 70 | /// are no possible values for that symbol. |
||
| 71 | class RangeSet { |
||
| 72 | public: |
||
| 73 | class Factory; |
||
| 74 | |||
| 75 | private: |
||
| 76 | // We use llvm::SmallVector as the underlying container for the following |
||
| 77 | // reasons: |
||
| 78 | // |
||
| 79 | // * Range sets are usually very simple, 1 or 2 ranges. |
||
| 80 | // That's why llvm::ImmutableSet is not perfect. |
||
| 81 | // |
||
| 82 | // * Ranges in sets are NOT overlapping, so it is natural to keep them |
||
| 83 | // sorted for efficient operations and queries. For this reason, |
||
| 84 | // llvm::SmallSet doesn't fit the requirements, it is not sorted when it |
||
| 85 | // is a vector. |
||
| 86 | // |
||
| 87 | // * Range set operations usually a bit harder than add/remove a range. |
||
| 88 | // Complex operations might do many of those for just one range set. |
||
| 89 | // Formerly it used to be llvm::ImmutableSet, which is inefficient for our |
||
| 90 | // purposes as we want to make these operations BOTH immutable AND |
||
| 91 | // efficient. |
||
| 92 | // |
||
| 93 | // * Iteration over ranges is widespread and a more cache-friendly |
||
| 94 | // structure is preferred. |
||
| 95 | using ImplType = llvm::SmallVector<Range, 4>; |
||
| 96 | |||
| 97 | struct ContainerType : public ImplType, public llvm::FoldingSetNode { |
||
| 98 | void Profile(llvm::FoldingSetNodeID &ID) const { |
||
| 99 | for (const Range &It : *this) { |
||
| 100 | It.Profile(ID); |
||
| 101 | } |
||
| 102 | } |
||
| 103 | }; |
||
| 104 | // This is a non-owning pointer to an actual container. |
||
| 105 | // The memory is fully managed by the factory and is alive as long as the |
||
| 106 | // factory itself is alive. |
||
| 107 | // It is a pointer as opposed to a reference, so we can easily reassign |
||
| 108 | // RangeSet objects. |
||
| 109 | using UnderlyingType = const ContainerType *; |
||
| 110 | UnderlyingType Impl; |
||
| 111 | |||
| 112 | public: |
||
| 113 | using const_iterator = ImplType::const_iterator; |
||
| 114 | |||
| 115 | const_iterator begin() const { return Impl->begin(); } |
||
| 116 | const_iterator end() const { return Impl->end(); } |
||
| 117 | size_t size() const { return Impl->size(); } |
||
| 118 | |||
| 119 | bool isEmpty() const { return Impl->empty(); } |
||
| 120 | |||
| 121 | class Factory { |
||
| 122 | public: |
||
| 123 | Factory(BasicValueFactory &BV) : ValueFactory(BV) {} |
||
| 124 | |||
| 125 | /// Create a new set with all ranges from both LHS and RHS. |
||
| 126 | /// Possible intersections are not checked here. |
||
| 127 | /// |
||
| 128 | /// Complexity: O(N + M) |
||
| 129 | /// where N = size(LHS), M = size(RHS) |
||
| 130 | RangeSet add(RangeSet LHS, RangeSet RHS); |
||
| 131 | /// Create a new set with all ranges from the original set plus the new one. |
||
| 132 | /// Possible intersections are not checked here. |
||
| 133 | /// |
||
| 134 | /// Complexity: O(N) |
||
| 135 | /// where N = size(Original) |
||
| 136 | RangeSet add(RangeSet Original, Range Element); |
||
| 137 | /// Create a new set with all ranges from the original set plus the point. |
||
| 138 | /// Possible intersections are not checked here. |
||
| 139 | /// |
||
| 140 | /// Complexity: O(N) |
||
| 141 | /// where N = size(Original) |
||
| 142 | RangeSet add(RangeSet Original, const llvm::APSInt &Point); |
||
| 143 | /// Create a new set which is a union of two given ranges. |
||
| 144 | /// Possible intersections are not checked here. |
||
| 145 | /// |
||
| 146 | /// Complexity: O(N + M) |
||
| 147 | /// where N = size(LHS), M = size(RHS) |
||
| 148 | RangeSet unite(RangeSet LHS, RangeSet RHS); |
||
| 149 | /// Create a new set by uniting given range set with the given range. |
||
| 150 | /// All intersections and adjacent ranges are handled here. |
||
| 151 | /// |
||
| 152 | /// Complexity: O(N) |
||
| 153 | /// where N = size(Original) |
||
| 154 | RangeSet unite(RangeSet Original, Range Element); |
||
| 155 | /// Create a new set by uniting given range set with the given point. |
||
| 156 | /// All intersections and adjacent ranges are handled here. |
||
| 157 | /// |
||
| 158 | /// Complexity: O(N) |
||
| 159 | /// where N = size(Original) |
||
| 160 | RangeSet unite(RangeSet Original, llvm::APSInt Point); |
||
| 161 | /// Create a new set by uniting given range set with the given range |
||
| 162 | /// between points. All intersections and adjacent ranges are handled here. |
||
| 163 | /// |
||
| 164 | /// Complexity: O(N) |
||
| 165 | /// where N = size(Original) |
||
| 166 | RangeSet unite(RangeSet Original, llvm::APSInt From, llvm::APSInt To); |
||
| 167 | |||
| 168 | RangeSet getEmptySet() { return &EmptySet; } |
||
| 169 | |||
| 170 | /// Create a new set with just one range. |
||
| 171 | /// @{ |
||
| 172 | RangeSet getRangeSet(Range Origin); |
||
| 173 | RangeSet getRangeSet(const llvm::APSInt &From, const llvm::APSInt &To) { |
||
| 174 | return getRangeSet(Range(From, To)); |
||
| 175 | } |
||
| 176 | RangeSet getRangeSet(const llvm::APSInt &Origin) { |
||
| 177 | return getRangeSet(Origin, Origin); |
||
| 178 | } |
||
| 179 | /// @} |
||
| 180 | |||
| 181 | /// Intersect the given range sets. |
||
| 182 | /// |
||
| 183 | /// Complexity: O(N + M) |
||
| 184 | /// where N = size(LHS), M = size(RHS) |
||
| 185 | RangeSet intersect(RangeSet LHS, RangeSet RHS); |
||
| 186 | /// Intersect the given set with the closed range [Lower, Upper]. |
||
| 187 | /// |
||
| 188 | /// Unlike the Range type, this range uses modular arithmetic, corresponding |
||
| 189 | /// to the common treatment of C integer overflow. Thus, if the Lower bound |
||
| 190 | /// is greater than the Upper bound, the range is taken to wrap around. This |
||
| 191 | /// is equivalent to taking the intersection with the two ranges [Min, |
||
| 192 | /// Upper] and [Lower, Max], or, alternatively, /removing/ all integers |
||
| 193 | /// between Upper and Lower. |
||
| 194 | /// |
||
| 195 | /// Complexity: O(N) |
||
| 196 | /// where N = size(What) |
||
| 197 | RangeSet intersect(RangeSet What, llvm::APSInt Lower, llvm::APSInt Upper); |
||
| 198 | /// Intersect the given range with the given point. |
||
| 199 | /// |
||
| 200 | /// The result can be either an empty set or a set containing the given |
||
| 201 | /// point depending on whether the point is in the range set. |
||
| 202 | /// |
||
| 203 | /// Complexity: O(logN) |
||
| 204 | /// where N = size(What) |
||
| 205 | RangeSet intersect(RangeSet What, llvm::APSInt Point); |
||
| 206 | |||
| 207 | /// Delete the given point from the range set. |
||
| 208 | /// |
||
| 209 | /// Complexity: O(N) |
||
| 210 | /// where N = size(From) |
||
| 211 | RangeSet deletePoint(RangeSet From, const llvm::APSInt &Point); |
||
| 212 | /// Negate the given range set. |
||
| 213 | /// |
||
| 214 | /// Turn all [A, B] ranges to [-B, -A], when "-" is a C-like unary minus |
||
| 215 | /// operation under the values of the type. |
||
| 216 | /// |
||
| 217 | /// We also handle MIN because applying unary minus to MIN does not change |
||
| 218 | /// it. |
||
| 219 | /// Example 1: |
||
| 220 | /// char x = -128; // -128 is a MIN value in a range of 'char' |
||
| 221 | /// char y = -x; // y: -128 |
||
| 222 | /// |
||
| 223 | /// Example 2: |
||
| 224 | /// unsigned char x = 0; // 0 is a MIN value in a range of 'unsigned char' |
||
| 225 | /// unsigned char y = -x; // y: 0 |
||
| 226 | /// |
||
| 227 | /// And it makes us to separate the range |
||
| 228 | /// like [MIN, N] to [MIN, MIN] U [-N, MAX]. |
||
| 229 | /// For instance, whole range is {-128..127} and subrange is [-128,-126], |
||
| 230 | /// thus [-128,-127,-126,...] negates to [-128,...,126,127]. |
||
| 231 | /// |
||
| 232 | /// Negate restores disrupted ranges on bounds, |
||
| 233 | /// e.g. [MIN, B] => [MIN, MIN] U [-B, MAX] => [MIN, B]. |
||
| 234 | /// |
||
| 235 | /// Negate is a self-inverse function, i.e. negate(negate(R)) == R. |
||
| 236 | /// |
||
| 237 | /// Complexity: O(N) |
||
| 238 | /// where N = size(What) |
||
| 239 | RangeSet negate(RangeSet What); |
||
| 240 | /// Performs promotions, truncations and conversions of the given set. |
||
| 241 | /// |
||
| 242 | /// This function is optimized for each of the six cast cases: |
||
| 243 | /// - noop |
||
| 244 | /// - conversion |
||
| 245 | /// - truncation |
||
| 246 | /// - truncation-conversion |
||
| 247 | /// - promotion |
||
| 248 | /// - promotion-conversion |
||
| 249 | /// |
||
| 250 | /// NOTE: This function is NOT self-inverse for truncations, because of |
||
| 251 | /// the higher bits loss: |
||
| 252 | /// - castTo(castTo(OrigRangeOfInt, char), int) != OrigRangeOfInt. |
||
| 253 | /// - castTo(castTo(OrigRangeOfChar, int), char) == OrigRangeOfChar. |
||
| 254 | /// But it is self-inverse for all the rest casts. |
||
| 255 | /// |
||
| 256 | /// Complexity: |
||
| 257 | /// - Noop O(1); |
||
| 258 | /// - Truncation O(N^2); |
||
| 259 | /// - Another case O(N); |
||
| 260 | /// where N = size(What) |
||
| 261 | RangeSet castTo(RangeSet What, APSIntType Ty); |
||
| 262 | RangeSet castTo(RangeSet What, QualType T); |
||
| 263 | |||
| 264 | /// Return associated value factory. |
||
| 265 | BasicValueFactory &getValueFactory() const { return ValueFactory; } |
||
| 266 | |||
| 267 | private: |
||
| 268 | /// Return a persistent version of the given container. |
||
| 269 | RangeSet makePersistent(ContainerType &&From); |
||
| 270 | /// Construct a new persistent version of the given container. |
||
| 271 | ContainerType *construct(ContainerType &&From); |
||
| 272 | |||
| 273 | RangeSet intersect(const ContainerType &LHS, const ContainerType &RHS); |
||
| 274 | /// NOTE: This function relies on the fact that all values in the |
||
| 275 | /// containers are persistent (created via BasicValueFactory::getValue). |
||
| 276 | ContainerType unite(const ContainerType &LHS, const ContainerType &RHS); |
||
| 277 | |||
| 278 | /// This is a helper function for `castTo` method. Implies not to be used |
||
| 279 | /// separately. |
||
| 280 | /// Performs a truncation case of a cast operation. |
||
| 281 | ContainerType truncateTo(RangeSet What, APSIntType Ty); |
||
| 282 | |||
| 283 | /// This is a helper function for `castTo` method. Implies not to be used |
||
| 284 | /// separately. |
||
| 285 | /// Performs a conversion case and a promotion-conversion case for signeds |
||
| 286 | /// of a cast operation. |
||
| 287 | ContainerType convertTo(RangeSet What, APSIntType Ty); |
||
| 288 | |||
| 289 | /// This is a helper function for `castTo` method. Implies not to be used |
||
| 290 | /// separately. |
||
| 291 | /// Performs a promotion for unsigneds only. |
||
| 292 | ContainerType promoteTo(RangeSet What, APSIntType Ty); |
||
| 293 | |||
| 294 | // Many operations include producing new APSInt values and that's why |
||
| 295 | // we need this factory. |
||
| 296 | BasicValueFactory &ValueFactory; |
||
| 297 | // Allocator for all the created containers. |
||
| 298 | // Containers might own their own memory and that's why it is specific |
||
| 299 | // for the type, so it calls container destructors upon deletion. |
||
| 300 | llvm::SpecificBumpPtrAllocator<ContainerType> Arena; |
||
| 301 | // Usually we deal with the same ranges and range sets over and over. |
||
| 302 | // Here we track all created containers and try not to repeat ourselves. |
||
| 303 | llvm::FoldingSet<ContainerType> Cache; |
||
| 304 | static ContainerType EmptySet; |
||
| 305 | }; |
||
| 306 | |||
| 307 | RangeSet(const RangeSet &) = default; |
||
| 308 | RangeSet &operator=(const RangeSet &) = default; |
||
| 309 | RangeSet(RangeSet &&) = default; |
||
| 310 | RangeSet &operator=(RangeSet &&) = default; |
||
| 311 | ~RangeSet() = default; |
||
| 312 | |||
| 313 | /// Construct a new RangeSet representing '{ [From, To] }'. |
||
| 314 | RangeSet(Factory &F, const llvm::APSInt &From, const llvm::APSInt &To) |
||
| 315 | : RangeSet(F.getRangeSet(From, To)) {} |
||
| 316 | |||
| 317 | /// Construct a new RangeSet representing the given point as a range. |
||
| 318 | RangeSet(Factory &F, const llvm::APSInt &Point) |
||
| 319 | : RangeSet(F.getRangeSet(Point)) {} |
||
| 320 | |||
| 321 | static void Profile(llvm::FoldingSetNodeID &ID, const RangeSet &RS) { |
||
| 322 | ID.AddPointer(RS.Impl); |
||
| 323 | } |
||
| 324 | |||
| 325 | /// Profile - Generates a hash profile of this RangeSet for use |
||
| 326 | /// by FoldingSet. |
||
| 327 | void Profile(llvm::FoldingSetNodeID &ID) const { Profile(ID, *this); } |
||
| 328 | |||
| 329 | /// getConcreteValue - If a symbol is constrained to equal a specific integer |
||
| 330 | /// constant then this method returns that value. Otherwise, it returns |
||
| 331 | /// NULL. |
||
| 332 | const llvm::APSInt *getConcreteValue() const { |
||
| 333 | return Impl->size() == 1 ? begin()->getConcreteValue() : nullptr; |
||
| 334 | } |
||
| 335 | |||
| 336 | /// Get the minimal value covered by the ranges in the set. |
||
| 337 | /// |
||
| 338 | /// Complexity: O(1) |
||
| 339 | const llvm::APSInt &getMinValue() const; |
||
| 340 | /// Get the maximal value covered by the ranges in the set. |
||
| 341 | /// |
||
| 342 | /// Complexity: O(1) |
||
| 343 | const llvm::APSInt &getMaxValue() const; |
||
| 344 | |||
| 345 | bool isUnsigned() const; |
||
| 346 | uint32_t getBitWidth() const; |
||
| 347 | APSIntType getAPSIntType() const; |
||
| 348 | |||
| 349 | /// Test whether the given point is contained by any of the ranges. |
||
| 350 | /// |
||
| 351 | /// Complexity: O(logN) |
||
| 352 | /// where N = size(this) |
||
| 353 | bool contains(llvm::APSInt Point) const { return containsImpl(Point); } |
||
| 354 | |||
| 355 | bool containsZero() const { |
||
| 356 | APSIntType T{getMinValue()}; |
||
| 357 | return contains(T.getZeroValue()); |
||
| 358 | } |
||
| 359 | |||
| 360 | /// Test if the range is the [0,0] range. |
||
| 361 | /// |
||
| 362 | /// Complexity: O(1) |
||
| 363 | bool encodesFalseRange() const { |
||
| 364 | const llvm::APSInt *Constant = getConcreteValue(); |
||
| 365 | return Constant && Constant->isZero(); |
||
| 366 | } |
||
| 367 | |||
| 368 | /// Test if the range doesn't contain zero. |
||
| 369 | /// |
||
| 370 | /// Complexity: O(logN) |
||
| 371 | /// where N = size(this) |
||
| 372 | bool encodesTrueRange() const { return !containsZero(); } |
||
| 373 | |||
| 374 | void dump(raw_ostream &OS) const; |
||
| 375 | void dump() const; |
||
| 376 | |||
| 377 | bool operator==(const RangeSet &Other) const { return *Impl == *Other.Impl; } |
||
| 378 | bool operator!=(const RangeSet &Other) const { return !(*this == Other); } |
||
| 379 | |||
| 380 | private: |
||
| 381 | /* implicit */ RangeSet(ContainerType *RawContainer) : Impl(RawContainer) {} |
||
| 382 | /* implicit */ RangeSet(UnderlyingType Ptr) : Impl(Ptr) {} |
||
| 383 | |||
| 384 | /// Pin given points to the type represented by the current range set. |
||
| 385 | /// |
||
| 386 | /// This makes parameter points to be in-out parameters. |
||
| 387 | /// In order to maintain consistent types across all of the ranges in the set |
||
| 388 | /// and to keep all the operations to compare ONLY points of the same type, we |
||
| 389 | /// need to pin every point before any operation. |
||
| 390 | /// |
||
| 391 | /// @Returns true if the given points can be converted to the target type |
||
| 392 | /// without changing the values (i.e. trivially) and false otherwise. |
||
| 393 | /// @{ |
||
| 394 | bool pin(llvm::APSInt &Lower, llvm::APSInt &Upper) const; |
||
| 395 | bool pin(llvm::APSInt &Point) const; |
||
| 396 | /// @} |
||
| 397 | |||
| 398 | // This version of this function modifies its arguments (pins it). |
||
| 399 | bool containsImpl(llvm::APSInt &Point) const; |
||
| 400 | |||
| 401 | friend class Factory; |
||
| 402 | }; |
||
| 403 | |||
| 404 | using ConstraintMap = llvm::ImmutableMap<SymbolRef, RangeSet>; |
||
| 405 | ConstraintMap getConstraintMap(ProgramStateRef State); |
||
| 406 | |||
| 407 | class RangedConstraintManager : public SimpleConstraintManager { |
||
| 408 | public: |
||
| 409 | RangedConstraintManager(ExprEngine *EE, SValBuilder &SB) |
||
| 410 | : SimpleConstraintManager(EE, SB) {} |
||
| 411 | |||
| 412 | ~RangedConstraintManager() override; |
||
| 413 | |||
| 414 | //===------------------------------------------------------------------===// |
||
| 415 | // Implementation for interface from SimpleConstraintManager. |
||
| 416 | //===------------------------------------------------------------------===// |
||
| 417 | |||
| 418 | ProgramStateRef assumeSym(ProgramStateRef State, SymbolRef Sym, |
||
| 419 | bool Assumption) override; |
||
| 420 | |||
| 421 | ProgramStateRef assumeSymInclusiveRange(ProgramStateRef State, SymbolRef Sym, |
||
| 422 | const llvm::APSInt &From, |
||
| 423 | const llvm::APSInt &To, |
||
| 424 | bool InRange) override; |
||
| 425 | |||
| 426 | ProgramStateRef assumeSymUnsupported(ProgramStateRef State, SymbolRef Sym, |
||
| 427 | bool Assumption) override; |
||
| 428 | |||
| 429 | protected: |
||
| 430 | /// Assume a constraint between a symbolic expression and a concrete integer. |
||
| 431 | virtual ProgramStateRef assumeSymRel(ProgramStateRef State, SymbolRef Sym, |
||
| 432 | BinaryOperator::Opcode op, |
||
| 433 | const llvm::APSInt &Int); |
||
| 434 | |||
| 435 | //===------------------------------------------------------------------===// |
||
| 436 | // Interface that subclasses must implement. |
||
| 437 | //===------------------------------------------------------------------===// |
||
| 438 | |||
| 439 | // Each of these is of the form "$Sym+Adj <> V", where "<>" is the comparison |
||
| 440 | // operation for the method being invoked. |
||
| 441 | |||
| 442 | virtual ProgramStateRef assumeSymNE(ProgramStateRef State, SymbolRef Sym, |
||
| 443 | const llvm::APSInt &V, |
||
| 444 | const llvm::APSInt &Adjustment) = 0; |
||
| 445 | |||
| 446 | virtual ProgramStateRef assumeSymEQ(ProgramStateRef State, SymbolRef Sym, |
||
| 447 | const llvm::APSInt &V, |
||
| 448 | const llvm::APSInt &Adjustment) = 0; |
||
| 449 | |||
| 450 | virtual ProgramStateRef assumeSymLT(ProgramStateRef State, SymbolRef Sym, |
||
| 451 | const llvm::APSInt &V, |
||
| 452 | const llvm::APSInt &Adjustment) = 0; |
||
| 453 | |||
| 454 | virtual ProgramStateRef assumeSymGT(ProgramStateRef State, SymbolRef Sym, |
||
| 455 | const llvm::APSInt &V, |
||
| 456 | const llvm::APSInt &Adjustment) = 0; |
||
| 457 | |||
| 458 | virtual ProgramStateRef assumeSymLE(ProgramStateRef State, SymbolRef Sym, |
||
| 459 | const llvm::APSInt &V, |
||
| 460 | const llvm::APSInt &Adjustment) = 0; |
||
| 461 | |||
| 462 | virtual ProgramStateRef assumeSymGE(ProgramStateRef State, SymbolRef Sym, |
||
| 463 | const llvm::APSInt &V, |
||
| 464 | const llvm::APSInt &Adjustment) = 0; |
||
| 465 | |||
| 466 | virtual ProgramStateRef assumeSymWithinInclusiveRange( |
||
| 467 | ProgramStateRef State, SymbolRef Sym, const llvm::APSInt &From, |
||
| 468 | const llvm::APSInt &To, const llvm::APSInt &Adjustment) = 0; |
||
| 469 | |||
| 470 | virtual ProgramStateRef assumeSymOutsideInclusiveRange( |
||
| 471 | ProgramStateRef State, SymbolRef Sym, const llvm::APSInt &From, |
||
| 472 | const llvm::APSInt &To, const llvm::APSInt &Adjustment) = 0; |
||
| 473 | |||
| 474 | //===------------------------------------------------------------------===// |
||
| 475 | // Internal implementation. |
||
| 476 | //===------------------------------------------------------------------===// |
||
| 477 | private: |
||
| 478 | static void computeAdjustment(SymbolRef &Sym, llvm::APSInt &Adjustment); |
||
| 479 | }; |
||
| 480 | |||
| 481 | /// Try to simplify a given symbolic expression based on the constraints in |
||
| 482 | /// State. This is needed because the Environment bindings are not getting |
||
| 483 | /// updated when a new constraint is added to the State. If the symbol is |
||
| 484 | /// simplified to a non-symbol (e.g. to a constant) then the original symbol |
||
| 485 | /// is returned. We use this function in the family of assumeSymNE/EQ/LT/../GE |
||
| 486 | /// functions where we can work only with symbols. Use the other function |
||
| 487 | /// (simplifyToSVal) if you are interested in a simplification that may yield |
||
| 488 | /// a concrete constant value. |
||
| 489 | SymbolRef simplify(ProgramStateRef State, SymbolRef Sym); |
||
| 490 | |||
| 491 | /// Try to simplify a given symbolic expression's associated `SVal` based on the |
||
| 492 | /// constraints in State. This is very similar to `simplify`, but this function |
||
| 493 | /// always returns the simplified SVal. The simplified SVal might be a single |
||
| 494 | /// constant (i.e. `ConcreteInt`). |
||
| 495 | SVal simplifyToSVal(ProgramStateRef State, SymbolRef Sym); |
||
| 496 | |||
| 497 | } // namespace ento |
||
| 498 | } // namespace clang |
||
| 499 | |||
| 500 | REGISTER_FACTORY_WITH_PROGRAMSTATE(ConstraintMap) |
||
| 501 | |||
| 502 | #endif |