contrib/llvm/tools/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h

   1 //== SMTConstraintManager.h -------------------------------------*- C++ -*--==//
   2 //
   3 //                     The LLVM Compiler Infrastructure
   4 //
   5 // This file is distributed under the University of Illinois Open Source
   6 // License. See LICENSE.TXT for details.
   7 //
   8 //===----------------------------------------------------------------------===//
   9 //
  10 //  This file defines a SMT generic API, which will be the base class for
  11 //  every SMT solver specific class.
  12 //
  13 //===----------------------------------------------------------------------===//
  14
  15 #ifndef LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTCONSTRAINTMANAGER_H
  16 #define LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTCONSTRAINTMANAGER_H
  17
  18 #include "clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h"
  19 #include "clang/StaticAnalyzer/Core/PathSensitive/SMTSolver.h"
  20
  21 namespace clang {
  22 namespace ento {
  23
  24 class SMTConstraintManager : public clang::ento::SimpleConstraintManager {
  25   SMTSolverRef &Solver;
  26
  27 public:
  28   SMTConstraintManager(clang::ento::SubEngine *SE, clang::ento::SValBuilder &SB,
  29                        SMTSolverRef &S)
  30       : SimpleConstraintManager(SE, SB), Solver(S) {}
  31   virtual ~SMTConstraintManager() = default;
  32
  33   //===------------------------------------------------------------------===//
  34   // Implementation for interface from SimpleConstraintManager.
  35   //===------------------------------------------------------------------===//
  36
  37   ProgramStateRef assumeSym(ProgramStateRef state, SymbolRef Sym,
  38                             bool Assumption) override;
  39
  40   ProgramStateRef assumeSymInclusiveRange(ProgramStateRef State, SymbolRef Sym,
  41                                           const llvm::APSInt &From,
  42                                           const llvm::APSInt &To,
  43                                           bool InRange) override;
  44
  45   ProgramStateRef assumeSymUnsupported(ProgramStateRef State, SymbolRef Sym,
  46                                        bool Assumption) override;
  47
  48   //===------------------------------------------------------------------===//
  49   // Implementation for interface from ConstraintManager.
  50   //===------------------------------------------------------------------===//
  51
  52   ConditionTruthVal checkNull(ProgramStateRef State, SymbolRef Sym) override;
  53
  54   const llvm::APSInt *getSymVal(ProgramStateRef State,
  55                                 SymbolRef Sym) const override;
  56
  57   /// Dumps SMT formula
  58   LLVM_DUMP_METHOD void dump() const { Solver->dump(); }
  59
  60 protected:
  61   // Check whether a new model is satisfiable, and update the program state.
  62   virtual ProgramStateRef assumeExpr(ProgramStateRef State, SymbolRef Sym,
  63                                      const SMTExprRef &Exp) = 0;
  64
  65   /// Given a program state, construct the logical conjunction and add it to
  66   /// the solver
  67   virtual void addStateConstraints(ProgramStateRef State) const = 0;
  68
  69   // Generate and check a Z3 model, using the given constraint.
  70   ConditionTruthVal checkModel(ProgramStateRef State,
  71                                const SMTExprRef &Exp) const;
  72 }; // end class SMTConstraintManager
  73
  74 } // namespace ento
  75 } // namespace clang
  76
  77 #endif