Core/PathSensitive/SimpleConstraintManager.h

0001 //== SimpleConstraintManager.h ----------------------------------*- C++ -*--==//
0002 //
0003 // Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
0004 // See https://llvm.org/LICENSE.txt for license information.
0005 // SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
0006 //
0007 //===----------------------------------------------------------------------===//
0008 //
0009 //  Simplified constraint manager backend.
0010 //
0011 //===----------------------------------------------------------------------===//
0012
0013 #ifndef LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SIMPLECONSTRAINTMANAGER_H
0014 #define LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SIMPLECONSTRAINTMANAGER_H
0015
0016 #include "clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h"
0017 #include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h"
0018
0019 namespace clang {
0020
0021 namespace ento {
0022
0023 class SimpleConstraintManager : public ConstraintManager {
0024   ExprEngine *EE;
0025   SValBuilder &SVB;
0026
0027 public:
0028   SimpleConstraintManager(ExprEngine *exprengine, SValBuilder &SB)
0029       : EE(exprengine), SVB(SB) {}
0030
0031   ~SimpleConstraintManager() override;
0032
0033   //===------------------------------------------------------------------===//
0034   // Implementation for interface from ConstraintManager.
0035   //===------------------------------------------------------------------===//
0036
0037 protected:
0038   //===------------------------------------------------------------------===//
0039   // Interface that subclasses must implement.
0040   //===------------------------------------------------------------------===//
0041
0042   /// Given a symbolic expression that can be reasoned about, assume that it is
0043   /// true/false and generate the new program state.
0044   virtual ProgramStateRef assumeSym(ProgramStateRef State, SymbolRef Sym,
0045                                     bool Assumption) = 0;
0046
0047   /// Given a symbolic expression within the range [From, To], assume that it is
0048   /// true/false and generate the new program state.
0049   /// This function is used to handle case ranges produced by a language
0050   /// extension for switch case statements.
0051   virtual ProgramStateRef assumeSymInclusiveRange(ProgramStateRef State,
0052                                                   SymbolRef Sym,
0053                                                   const llvm::APSInt &From,
0054                                                   const llvm::APSInt &To,
0055                                                   bool InRange) = 0;
0056
0057   /// Given a symbolic expression that cannot be reasoned about, assume that
0058   /// it is zero/nonzero and add it directly to the solver state.
0059   virtual ProgramStateRef assumeSymUnsupported(ProgramStateRef State,
0060                                                SymbolRef Sym,
0061                                                bool Assumption) = 0;
0062
0063   //===------------------------------------------------------------------===//
0064   // Internal implementation.
0065   //===------------------------------------------------------------------===//
0066
0067   /// Ensures that the DefinedSVal conditional is expressed as a NonLoc by
0068   /// creating boolean casts to handle Loc's.
0069   ProgramStateRef assumeInternal(ProgramStateRef State, DefinedSVal Cond,
0070                                  bool Assumption) override;
0071
0072   ProgramStateRef assumeInclusiveRangeInternal(ProgramStateRef State,
0073                                                NonLoc Value,
0074                                                const llvm::APSInt &From,
0075                                                const llvm::APSInt &To,
0076                                                bool InRange) override;
0077
0078   SValBuilder &getSValBuilder() const { return SVB; }
0079   BasicValueFactory &getBasicVals() const { return SVB.getBasicValueFactory(); }
0080   SymbolManager &getSymbolManager() const { return SVB.getSymbolManager(); }
0081
0082 private:
0083   ProgramStateRef assume(ProgramStateRef State, NonLoc Cond, bool Assumption);
0084
0085   ProgramStateRef assumeAux(ProgramStateRef State, NonLoc Cond,
0086                             bool Assumption);
0087 };
0088
0089 } // end namespace ento
0090
0091 } // end namespace clang
0092
0093 #endif