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; 2678114a58f8cf5e9b948e82448b2f0904f5b6c19eJordan Rose SValBuilder &SVB; 274502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenekpublic: 2878114a58f8cf5e9b948e82448b2f0904f5b6c19eJordan Rose SimpleConstraintManager(SubEngine *subengine, SValBuilder &SB) 2978114a58f8cf5e9b948e82448b2f0904f5b6c19eJordan Rose : SU(subengine), SVB(SB) {} 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, 37651f13cea278ec967336033dd032faef0e9fc2ecStephen Hines bool Assumption) override; 38f1b8227d758721075e3a84a85e66cb7173334b13Ted Kremenek 398bef8238181a30e52dea380789a7e2d760eac532Ted Kremenek ProgramStateRef assume(ProgramStateRef state, NonLoc Cond, bool Assumption); 404502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 418bef8238181a30e52dea380789a7e2d760eac532Ted Kremenek ProgramStateRef assumeSymRel(ProgramStateRef state, 42ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose const SymExpr *LHS, 43ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose BinaryOperator::Opcode op, 44ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose const llvm::APSInt& Int); 451eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 46a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenekprotected: 471eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 48a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek //===------------------------------------------------------------------===// 49a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek // Interface that subclasses must implement. 50a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek //===------------------------------------------------------------------===// 511eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 52ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose // Each of these is of the form "$sym+Adj <> V", where "<>" is the comparison 53ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose // operation for the method being invoked. 548bef8238181a30e52dea380789a7e2d760eac532Ted Kremenek virtual ProgramStateRef assumeSymNE(ProgramStateRef state, SymbolRef sym, 55ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose const llvm::APSInt& V, 56ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose const llvm::APSInt& Adjustment) = 0; 574502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 588bef8238181a30e52dea380789a7e2d760eac532Ted Kremenek virtual ProgramStateRef assumeSymEQ(ProgramStateRef state, SymbolRef sym, 59ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose const llvm::APSInt& V, 60ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose const llvm::APSInt& Adjustment) = 0; 614502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 628bef8238181a30e52dea380789a7e2d760eac532Ted Kremenek virtual ProgramStateRef assumeSymLT(ProgramStateRef state, SymbolRef sym, 63ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose const llvm::APSInt& V, 64ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose const llvm::APSInt& Adjustment) = 0; 654502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 668bef8238181a30e52dea380789a7e2d760eac532Ted Kremenek virtual ProgramStateRef assumeSymGT(ProgramStateRef state, SymbolRef sym, 67ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose const llvm::APSInt& V, 68ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose const llvm::APSInt& Adjustment) = 0; 694502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 708bef8238181a30e52dea380789a7e2d760eac532Ted Kremenek virtual ProgramStateRef assumeSymLE(ProgramStateRef state, SymbolRef sym, 71ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose const llvm::APSInt& V, 72ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose const llvm::APSInt& Adjustment) = 0; 734502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 748bef8238181a30e52dea380789a7e2d760eac532Ted Kremenek virtual ProgramStateRef assumeSymGE(ProgramStateRef state, SymbolRef sym, 75ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose const llvm::APSInt& V, 76ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose const llvm::APSInt& Adjustment) = 0; 771eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 78a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek //===------------------------------------------------------------------===// 79a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek // Internal implementation. 80a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek //===------------------------------------------------------------------===// 811eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 8278114a58f8cf5e9b948e82448b2f0904f5b6c19eJordan Rose BasicValueFactory &getBasicVals() const { return SVB.getBasicValueFactory(); } 8378114a58f8cf5e9b948e82448b2f0904f5b6c19eJordan Rose SymbolManager &getSymbolManager() const { return SVB.getSymbolManager(); } 841d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose 85651f13cea278ec967336033dd032faef0e9fc2ecStephen Hines bool canReasonAbout(SVal X) const override; 86eca4e6e58170129cbdf105b2cfdb9ac2be61858eAnna Zaks 878bef8238181a30e52dea380789a7e2d760eac532Ted Kremenek ProgramStateRef assumeAux(ProgramStateRef state, 883cdf584e068056540769dab56cad333e95a89750Anna Zaks NonLoc Cond, 893cdf584e068056540769dab56cad333e95a89750Anna Zaks bool Assumption); 903cdf584e068056540769dab56cad333e95a89750Anna Zaks 918bef8238181a30e52dea380789a7e2d760eac532Ted Kremenek ProgramStateRef assumeAuxForSymbol(ProgramStateRef State, 923cdf584e068056540769dab56cad333e95a89750Anna Zaks SymbolRef Sym, 933cdf584e068056540769dab56cad333e95a89750Anna Zaks bool Assumption); 944502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek}; 954502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 965a4f98ff943e6a501b0fe47ade007c9bbf96cb88Argyrios Kyrtzidis} // end GR namespace 975a4f98ff943e6a501b0fe47ade007c9bbf96cb88Argyrios Kyrtzidis 985a4f98ff943e6a501b0fe47ade007c9bbf96cb88Argyrios Kyrtzidis} // end clang namespace 994502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 100669c0e13d3ab342f9b074a8c3eeeb887cf54b52fTed Kremenek#endif 101