1 //== SMTConstraintManager.h -------------------------------------*- C++ -*--==//
3 // The LLVM Compiler Infrastructure
5 // This file is distributed under the University of Illinois Open Source
6 // License. See LICENSE.TXT for details.
8 //===----------------------------------------------------------------------===//
10 // This file defines a SMT generic API, which will be the base class for
11 // every SMT solver specific class.
13 //===----------------------------------------------------------------------===//
15 #ifndef LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTCONSTRAINTMANAGER_H
16 #define LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTCONSTRAINTMANAGER_H
18 #include "clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h"
19 #include "clang/StaticAnalyzer/Core/PathSensitive/SMTSolver.h"
24 class SMTConstraintManager : public clang::ento::SimpleConstraintManager {
28 SMTConstraintManager(clang::ento::SubEngine *SE, clang::ento::SValBuilder &SB,
30 : SimpleConstraintManager(SE, SB), Solver(S) {}
31 virtual ~SMTConstraintManager() = default;
33 //===------------------------------------------------------------------===//
34 // Implementation for interface from SimpleConstraintManager.
35 //===------------------------------------------------------------------===//
37 ProgramStateRef assumeSym(ProgramStateRef state, SymbolRef Sym,
38 bool Assumption) override;
40 ProgramStateRef assumeSymInclusiveRange(ProgramStateRef State, SymbolRef Sym,
41 const llvm::APSInt &From,
42 const llvm::APSInt &To,
43 bool InRange) override;
45 ProgramStateRef assumeSymUnsupported(ProgramStateRef State, SymbolRef Sym,
46 bool Assumption) override;
48 //===------------------------------------------------------------------===//
49 // Implementation for interface from ConstraintManager.
50 //===------------------------------------------------------------------===//
52 ConditionTruthVal checkNull(ProgramStateRef State, SymbolRef Sym) override;
54 const llvm::APSInt *getSymVal(ProgramStateRef State,
55 SymbolRef Sym) const override;
58 LLVM_DUMP_METHOD void dump() const { Solver->dump(); }
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;
65 /// Given a program state, construct the logical conjunction and add it to
67 virtual void addStateConstraints(ProgramStateRef State) const = 0;
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