//== RangedConstraintManager.h ----------------------------------*- C++ -*--==//

//

// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.

// See https://llvm.org/LICENSE.txt for license information.

// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception

//

//===----------------------------------------------------------------------===//

//

//  Ranged constraint manager, built on SimpleConstraintManager.

//

//===----------------------------------------------------------------------===//

#ifndef LLVM_CLANG_LIB_STATICANALYZER_CORE_RANGEDCONSTRAINTMANAGER_H

#define LLVM_CLANG_LIB_STATICANALYZER_CORE_RANGEDCONSTRAINTMANAGER_H

#include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h"

#include "clang/StaticAnalyzer/Core/PathSensitive/ProgramStateTrait.h"

#include "clang/StaticAnalyzer/Core/PathSensitive/SimpleConstraintManager.h"

namespace clang {

namespace ento {

/// A Range represents the closed range [from, to].  The caller must

/// guarantee that from <= to.  Note that Range is immutable, so as not

/// to subvert RangeSet's immutability.

class Range : public std::pair<const llvm::APSInt *, const llvm::APSInt *> {

public:

  Range(const llvm::APSInt &from, const llvm::APSInt &to)

      : std::pair<const llvm::APSInt *, const llvm::APSInt *>(&from, &to) {

    assert(from <= to);

  }

  bool Includes(const llvm::APSInt &v) const {

    return *first <= v && 
v <= *second416k
;

  }

  const llvm::APSInt &From() const { return *first; }

  const llvm::APSInt &To() const { return *second; }

  const llvm::APSInt *getConcreteValue() const {

    return &From() == &To() ? 
&From()16.3k
 : 
nullptr46.3k
;

  }

  void Profile(llvm::FoldingSetNodeID &ID) const {

    ID.AddPointer(&From());

    ID.AddPointer(&To());

  }

};

class RangeTrait : public llvm::ImutContainerInfo<Range> {

public:

  // When comparing if one Range is less than another, we should compare

  // the actual APSInt values instead of their pointers.  This keeps the order

  // consistent (instead of comparing by pointer values) and can potentially

  // be used to speed up some of the operations in RangeSet.

  static inline bool isLess(key_type_ref lhs, key_type_ref rhs) {

    return *lhs.first < *rhs.first ||

           
(29.4k
!(*rhs.first < *lhs.first)29.4k
 && 
*lhs.second < *rhs.second0
);

  }

};

/// RangeSet contains a set of ranges. If the set is empty, then

///  there the value of a symbol is overly constrained and there are no

///  possible values for that symbol.

class RangeSet {

  typedef llvm::ImmutableSet<Range, RangeTrait> PrimRangeSet;

  PrimRangeSet ranges; // no need to make const, since it is an

                       // ImmutableSet - this allows default operator=

                       // to work.

public:

  typedef PrimRangeSet::Factory Factory;

  typedef PrimRangeSet::iterator iterator;

  RangeSet(PrimRangeSet RS) : ranges(RS) {}

  /// Create a new set with all ranges of this set and RS.

  /// Possible intersections are not checked here.

  RangeSet addRange(Factory &F, const RangeSet &RS) {

    PrimRangeSet Ranges(RS.ranges);

    for (const auto &range : ranges)

      Ranges = F.add(Ranges, range);

    return RangeSet(Ranges);

  }

  iterator begin() const { return ranges.begin(); }

  iterator end() const { return ranges.end(); }

  bool isEmpty() const { return ranges.isEmpty(); }

  /// Construct a new RangeSet representing '{ [from, to] }'.

  RangeSet(Factory &F, const llvm::APSInt &from, const llvm::APSInt &to)

      : ranges(F.add(F.getEmptySet(), Range(from, to))) {}

  /// Profile - Generates a hash profile of this RangeSet for use

  ///  by FoldingSet.

  void Profile(llvm::FoldingSetNodeID &ID) const { ranges.Profile(ID); }

  /// getConcreteValue - If a symbol is contrained to equal a specific integer

  ///  constant then this method returns that value.  Otherwise, it returns

  ///  NULL.

  const llvm::APSInt *getConcreteValue() const {

    return ranges.isSingleton() ? 
ranges.begin()->getConcreteValue()62.7k
 : 
nullptr3.72k
;

  }

private:

  void IntersectInRange(BasicValueFactory &BV, Factory &F,

                        const llvm::APSInt &Lower, const llvm::APSInt &Upper,

                        PrimRangeSet &newRanges, PrimRangeSet::iterator &i,

                        PrimRangeSet::iterator &e) const;

  const llvm::APSInt &getMinValue() const;

  bool pin(llvm::APSInt &Lower, llvm::APSInt &Upper) const;

public:

  RangeSet Intersect(BasicValueFactory &BV, Factory &F, llvm::APSInt Lower,

                     llvm::APSInt Upper) const;

  RangeSet Intersect(BasicValueFactory &BV, Factory &F,

                     const RangeSet &Other) const;

  RangeSet Negate(BasicValueFactory &BV, Factory &F) const;

  void print(raw_ostream &os) const;

  bool operator==(const RangeSet &other) const {

    return ranges == other.ranges;

  }

};

class ConstraintRange {};

using ConstraintRangeTy = llvm::ImmutableMap<SymbolRef, RangeSet>;

template <>

struct ProgramStateTrait<ConstraintRange>

  : public ProgramStatePartialTrait<ConstraintRangeTy> {

  static void *GDMIndex();

};

class RangedConstraintManager : public SimpleConstraintManager {

public:

  RangedConstraintManager(SubEngine *SE, SValBuilder &SB)

      : SimpleConstraintManager(SE, SB) {}

  ~RangedConstraintManager() override;

  //===------------------------------------------------------------------===//

  // Implementation for interface from SimpleConstraintManager.

  //===------------------------------------------------------------------===//

  ProgramStateRef assumeSym(ProgramStateRef State, SymbolRef Sym,

                            bool Assumption) override;

  ProgramStateRef assumeSymInclusiveRange(ProgramStateRef State, SymbolRef Sym,

                                          const llvm::APSInt &From,

                                          const llvm::APSInt &To,

                                          bool InRange) override;

  ProgramStateRef assumeSymUnsupported(ProgramStateRef State, SymbolRef Sym,

                                       bool Assumption) override;

protected:

  /// Assume a constraint between a symbolic expression and a concrete integer.

  virtual ProgramStateRef assumeSymRel(ProgramStateRef State, SymbolRef Sym,

                               BinaryOperator::Opcode op,

                               const llvm::APSInt &Int);

  //===------------------------------------------------------------------===//

  // Interface that subclasses must implement.

  //===------------------------------------------------------------------===//

  // Each of these is of the form "$Sym+Adj <> V", where "<>" is the comparison

  // operation for the method being invoked.

  virtual ProgramStateRef assumeSymNE(ProgramStateRef State, SymbolRef Sym,

                                      const llvm::APSInt &V,

                                      const llvm::APSInt &Adjustment) = 0;

  virtual ProgramStateRef assumeSymEQ(ProgramStateRef State, SymbolRef Sym,

                                      const llvm::APSInt &V,

                                      const llvm::APSInt &Adjustment) = 0;

  virtual ProgramStateRef assumeSymLT(ProgramStateRef State, SymbolRef Sym,

                                      const llvm::APSInt &V,

                                      const llvm::APSInt &Adjustment) = 0;

  virtual ProgramStateRef assumeSymGT(ProgramStateRef State, SymbolRef Sym,

                                      const llvm::APSInt &V,

                                      const llvm::APSInt &Adjustment) = 0;

  virtual ProgramStateRef assumeSymLE(ProgramStateRef State, SymbolRef Sym,

                                      const llvm::APSInt &V,

                                      const llvm::APSInt &Adjustment) = 0;

  virtual ProgramStateRef assumeSymGE(ProgramStateRef State, SymbolRef Sym,

                                      const llvm::APSInt &V,

                                      const llvm::APSInt &Adjustment) = 0;

  virtual ProgramStateRef assumeSymWithinInclusiveRange(

      ProgramStateRef State, SymbolRef Sym, const llvm::APSInt &From,

      const llvm::APSInt &To, const llvm::APSInt &Adjustment) = 0;

  virtual ProgramStateRef assumeSymOutsideInclusiveRange(

      ProgramStateRef State, SymbolRef Sym, const llvm::APSInt &From,

      const llvm::APSInt &To, const llvm::APSInt &Adjustment) = 0;

  //===------------------------------------------------------------------===//

  // Internal implementation.

  //===------------------------------------------------------------------===//

private:

  static void computeAdjustment(SymbolRef &Sym, llvm::APSInt &Adjustment);

};

} // end GR namespace

} // end clang namespace

#endif