14502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek//== SimpleConstraintManager.h ----------------------------------*- C++ -*--==//
24502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek//
34502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek//                     The LLVM Compiler Infrastructure
44502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek//
54502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek// This file is distributed under the University of Illinois Open Source
64502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek// License. See LICENSE.TXT for details.
74502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek//
84502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek//===----------------------------------------------------------------------===//
94502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek//
104502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek//  Code shared between BasicConstraintManager and RangeConstraintManager.
114502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek//
124502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek//===----------------------------------------------------------------------===//
134502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek
145a4f98ff943e6a501b0fe47ade007c9bbf96cb88Argyrios Kyrtzidis#ifndef LLVM_CLANG_GR_SIMPLE_CONSTRAINT_MANAGER_H
155a4f98ff943e6a501b0fe47ade007c9bbf96cb88Argyrios Kyrtzidis#define LLVM_CLANG_GR_SIMPLE_CONSTRAINT_MANAGER_H
164502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek
179b663716449b618ba0390b1dbebc54fa8e971124Ted Kremenek#include "clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h"
1818c66fdc3c4008d335885695fe36fb5353c5f672Ted Kremenek#include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h"
194502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek
204502195fecf399fdbbb9ee2393ad08148c394179Ted Kremeneknamespace clang {
214502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek
229ef6537a894c33003359b1f9b9676e9178e028b7Ted Kremeneknamespace ento {
235a4f98ff943e6a501b0fe47ade007c9bbf96cb88Argyrios Kyrtzidis
244502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenekclass SimpleConstraintManager : public ConstraintManager {
25ca5d78d0bc3010164f2f9682967d64d7e305a167Jordan Rose  SubEngine *SU;
261d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose  BasicValueFactory &BVF;
274502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenekpublic:
28ca5d78d0bc3010164f2f9682967d64d7e305a167Jordan Rose  SimpleConstraintManager(SubEngine *subengine, BasicValueFactory &BV)
291d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose    : SU(subengine), BVF(BV) {}
301eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump  virtual ~SimpleConstraintManager();
311eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
32a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek  //===------------------------------------------------------------------===//
33a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek  // Common implementation for the interface provided by ConstraintManager.
34a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek  //===------------------------------------------------------------------===//
35f1b8227d758721075e3a84a85e66cb7173334b13Ted Kremenek
368bef8238181a30e52dea380789a7e2d760eac532Ted Kremenek  ProgramStateRef assume(ProgramStateRef state, DefinedSVal Cond,
375b9bd2137ebef350af803c634e3fdf5d74678100Ted Kremenek                        bool Assumption);
38f1b8227d758721075e3a84a85e66cb7173334b13Ted Kremenek
398bef8238181a30e52dea380789a7e2d760eac532Ted Kremenek  ProgramStateRef assume(ProgramStateRef state, Loc Cond, bool Assumption);
404502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek
418bef8238181a30e52dea380789a7e2d760eac532Ted Kremenek  ProgramStateRef assume(ProgramStateRef state, NonLoc Cond, bool Assumption);
424502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek
438bef8238181a30e52dea380789a7e2d760eac532Ted Kremenek  ProgramStateRef assumeSymRel(ProgramStateRef state,
44ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose                              const SymExpr *LHS,
45ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose                              BinaryOperator::Opcode op,
46ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose                              const llvm::APSInt& Int);
471eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
48a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenekprotected:
491eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
50a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek  //===------------------------------------------------------------------===//
51a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek  // Interface that subclasses must implement.
52a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek  //===------------------------------------------------------------------===//
531eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
54ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose  // Each of these is of the form "$sym+Adj <> V", where "<>" is the comparison
55ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose  // operation for the method being invoked.
568bef8238181a30e52dea380789a7e2d760eac532Ted Kremenek  virtual ProgramStateRef assumeSymNE(ProgramStateRef state, SymbolRef sym,
57ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose                                     const llvm::APSInt& V,
58ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose                                     const llvm::APSInt& Adjustment) = 0;
594502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek
608bef8238181a30e52dea380789a7e2d760eac532Ted Kremenek  virtual ProgramStateRef assumeSymEQ(ProgramStateRef state, SymbolRef sym,
61ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose                                     const llvm::APSInt& V,
62ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose                                     const llvm::APSInt& Adjustment) = 0;
634502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek
648bef8238181a30e52dea380789a7e2d760eac532Ted Kremenek  virtual ProgramStateRef assumeSymLT(ProgramStateRef state, SymbolRef sym,
65ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose                                     const llvm::APSInt& V,
66ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose                                     const llvm::APSInt& Adjustment) = 0;
674502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek
688bef8238181a30e52dea380789a7e2d760eac532Ted Kremenek  virtual ProgramStateRef assumeSymGT(ProgramStateRef state, SymbolRef sym,
69ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose                                     const llvm::APSInt& V,
70ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose                                     const llvm::APSInt& Adjustment) = 0;
714502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek
728bef8238181a30e52dea380789a7e2d760eac532Ted Kremenek  virtual ProgramStateRef assumeSymLE(ProgramStateRef state, SymbolRef sym,
73ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose                                     const llvm::APSInt& V,
74ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose                                     const llvm::APSInt& Adjustment) = 0;
754502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek
768bef8238181a30e52dea380789a7e2d760eac532Ted Kremenek  virtual ProgramStateRef assumeSymGE(ProgramStateRef state, SymbolRef sym,
77ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose                                     const llvm::APSInt& V,
78ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose                                     const llvm::APSInt& Adjustment) = 0;
791eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
80a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek  //===------------------------------------------------------------------===//
81a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek  // Internal implementation.
82a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek  //===------------------------------------------------------------------===//
831eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
841d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose  BasicValueFactory &getBasicVals() const { return BVF; }
851d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose
86eca4e6e58170129cbdf105b2cfdb9ac2be61858eAnna Zaks  bool canReasonAbout(SVal X) const;
87eca4e6e58170129cbdf105b2cfdb9ac2be61858eAnna Zaks
888bef8238181a30e52dea380789a7e2d760eac532Ted Kremenek  ProgramStateRef assumeAux(ProgramStateRef state,
893cdf584e068056540769dab56cad333e95a89750Anna Zaks                                Loc Cond,
903cdf584e068056540769dab56cad333e95a89750Anna Zaks                                bool Assumption);
911eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
928bef8238181a30e52dea380789a7e2d760eac532Ted Kremenek  ProgramStateRef assumeAux(ProgramStateRef state,
933cdf584e068056540769dab56cad333e95a89750Anna Zaks                                NonLoc Cond,
943cdf584e068056540769dab56cad333e95a89750Anna Zaks                                bool Assumption);
953cdf584e068056540769dab56cad333e95a89750Anna Zaks
968bef8238181a30e52dea380789a7e2d760eac532Ted Kremenek  ProgramStateRef assumeAuxForSymbol(ProgramStateRef State,
973cdf584e068056540769dab56cad333e95a89750Anna Zaks                                         SymbolRef Sym,
983cdf584e068056540769dab56cad333e95a89750Anna Zaks                                         bool Assumption);
994502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek};
1004502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek
1015a4f98ff943e6a501b0fe47ade007c9bbf96cb88Argyrios Kyrtzidis} // end GR namespace
1025a4f98ff943e6a501b0fe47ade007c9bbf96cb88Argyrios Kyrtzidis
1035a4f98ff943e6a501b0fe47ade007c9bbf96cb88Argyrios Kyrtzidis} // end clang namespace
1044502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek
105669c0e13d3ab342f9b074a8c3eeeb887cf54b52fTed Kremenek#endif
106