8e6b6c0c2f
Canonicalizing these two forms allows us to better model containers like std::vector, which use "m_start != m_finish" to implement empty() but "m_finish - m_start" to implement size(). The analyzer should have a consistent interpretation of these two symbolic expressions, even though it's not properly reasoning about either one yet. The other unfortunate thing is that while the size() expression will only ever be written "m_finish - m_start", the comparison may be written "m_finish == m_start" or "m_start == m_finish". Right now the analyzer does not attempt to canonicalize those two expressions, since it doesn't know which length expression to pick. Doing this correctly will probably require implementing unary minus as a new SymExpr kind (<rdar://problem/12351075>). For now, the analyzer inverts the order of arguments in the comparison to build the subtraction, on the assumption that "begin() != end()" is written more often than "end() != begin()". This is purely speculation. <rdar://problem/13239003> llvm-svn: 177801
107 lines
4.2 KiB
C++
107 lines
4.2 KiB
C++
//== SimpleConstraintManager.h ----------------------------------*- C++ -*--==//
|
|
//
|
|
// The LLVM Compiler Infrastructure
|
|
//
|
|
// This file is distributed under the University of Illinois Open Source
|
|
// License. See LICENSE.TXT for details.
|
|
//
|
|
//===----------------------------------------------------------------------===//
|
|
//
|
|
// Code shared between BasicConstraintManager and RangeConstraintManager.
|
|
//
|
|
//===----------------------------------------------------------------------===//
|
|
|
|
#ifndef LLVM_CLANG_GR_SIMPLE_CONSTRAINT_MANAGER_H
|
|
#define LLVM_CLANG_GR_SIMPLE_CONSTRAINT_MANAGER_H
|
|
|
|
#include "clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h"
|
|
#include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h"
|
|
|
|
namespace clang {
|
|
|
|
namespace ento {
|
|
|
|
class SimpleConstraintManager : public ConstraintManager {
|
|
SubEngine *SU;
|
|
SValBuilder &SVB;
|
|
public:
|
|
SimpleConstraintManager(SubEngine *subengine, SValBuilder &SB)
|
|
: SU(subengine), SVB(SB) {}
|
|
virtual ~SimpleConstraintManager();
|
|
|
|
//===------------------------------------------------------------------===//
|
|
// Common implementation for the interface provided by ConstraintManager.
|
|
//===------------------------------------------------------------------===//
|
|
|
|
ProgramStateRef assume(ProgramStateRef state, DefinedSVal Cond,
|
|
bool Assumption);
|
|
|
|
ProgramStateRef assume(ProgramStateRef state, Loc Cond, bool Assumption);
|
|
|
|
ProgramStateRef assume(ProgramStateRef state, NonLoc Cond, bool Assumption);
|
|
|
|
ProgramStateRef assumeSymRel(ProgramStateRef state,
|
|
const SymExpr *LHS,
|
|
BinaryOperator::Opcode op,
|
|
const llvm::APSInt& Int);
|
|
|
|
protected:
|
|
|
|
//===------------------------------------------------------------------===//
|
|
// Interface that subclasses must implement.
|
|
//===------------------------------------------------------------------===//
|
|
|
|
// Each of these is of the form "$sym+Adj <> V", where "<>" is the comparison
|
|
// operation for the method being invoked.
|
|
virtual ProgramStateRef assumeSymNE(ProgramStateRef state, SymbolRef sym,
|
|
const llvm::APSInt& V,
|
|
const llvm::APSInt& Adjustment) = 0;
|
|
|
|
virtual ProgramStateRef assumeSymEQ(ProgramStateRef state, SymbolRef sym,
|
|
const llvm::APSInt& V,
|
|
const llvm::APSInt& Adjustment) = 0;
|
|
|
|
virtual ProgramStateRef assumeSymLT(ProgramStateRef state, SymbolRef sym,
|
|
const llvm::APSInt& V,
|
|
const llvm::APSInt& Adjustment) = 0;
|
|
|
|
virtual ProgramStateRef assumeSymGT(ProgramStateRef state, SymbolRef sym,
|
|
const llvm::APSInt& V,
|
|
const llvm::APSInt& Adjustment) = 0;
|
|
|
|
virtual ProgramStateRef assumeSymLE(ProgramStateRef state, SymbolRef sym,
|
|
const llvm::APSInt& V,
|
|
const llvm::APSInt& Adjustment) = 0;
|
|
|
|
virtual ProgramStateRef assumeSymGE(ProgramStateRef state, SymbolRef sym,
|
|
const llvm::APSInt& V,
|
|
const llvm::APSInt& Adjustment) = 0;
|
|
|
|
//===------------------------------------------------------------------===//
|
|
// Internal implementation.
|
|
//===------------------------------------------------------------------===//
|
|
|
|
BasicValueFactory &getBasicVals() const { return SVB.getBasicValueFactory(); }
|
|
SymbolManager &getSymbolManager() const { return SVB.getSymbolManager(); }
|
|
|
|
bool canReasonAbout(SVal X) const;
|
|
|
|
ProgramStateRef assumeAux(ProgramStateRef state,
|
|
Loc Cond,
|
|
bool Assumption);
|
|
|
|
ProgramStateRef assumeAux(ProgramStateRef state,
|
|
NonLoc Cond,
|
|
bool Assumption);
|
|
|
|
ProgramStateRef assumeAuxForSymbol(ProgramStateRef State,
|
|
SymbolRef Sym,
|
|
bool Assumption);
|
|
};
|
|
|
|
} // end GR namespace
|
|
|
|
} // end clang namespace
|
|
|
|
#endif
|