From: Ted Kremenek Date: Thu, 14 Feb 2008 22:13:12 +0000 (+0000) Subject: Partitioned definition/implementation of GRExperEngine into .h and .cpp. X-Git-Url: https://granicus.if.org/sourcecode?a=commitdiff_plain;h=77349cb20bfd7069d081f84c91975bfa8ef60a32;p=clang Partitioned definition/implementation of GRExperEngine into .h and .cpp. Still some cleanup to do, but this initial checkin compiles and runs correctly. git-svn-id: https://llvm.org/svn/llvm-project/cfe/trunk@47135 91177308-0d34-0410-b5e6-96231b3b80d8 --- diff --git a/Analysis/GRExprEngine.cpp b/Analysis/GRExprEngine.cpp index 73ae7286eb..ce504c10b0 100644 --- a/Analysis/GRExprEngine.cpp +++ b/Analysis/GRExprEngine.cpp @@ -1,4 +1,4 @@ -//===-- GRExprEngine.cpp - Simple, Path-Sens. Constant Prop. -----*- C++ -*-==// +//=-- GRExprEngine.cpp - Path-Sensitive Expression-Level Dataflow ---*- C++ -*-= // // The LLVM Compiler Infrastructure // @@ -7,345 +7,13 @@ // //===----------------------------------------------------------------------===// // -// Constant Propagation via Graph Reachability +// This file defines a meta-engine for path-sensitive dataflow analysis that +// is built on GREngine, but provides the boilerplate to execute transfer +// functions and build the ExplodedGraph at the expression level. // -// This files defines a simple analysis that performs path-sensitive -// constant propagation within a function. An example use of this analysis -// is to perform simple checks for NULL dereferences. -// -//===----------------------------------------------------------------------===// - -#include "ValueState.h" - -#include "clang/Analysis/PathSensitive/GRCoreEngine.h" -#include "clang/Analysis/PathSensitive/GRTransferFuncs.h" -#include "GRSimpleVals.h" - -#include "clang/AST/Expr.h" -#include "clang/AST/ASTContext.h" -#include "clang/Analysis/Analyses/LiveVariables.h" -#include "clang/Basic/Diagnostic.h" - -#include "llvm/Support/Casting.h" -#include "llvm/Support/DataTypes.h" -#include "llvm/ADT/APSInt.h" -#include "llvm/ADT/FoldingSet.h" -#include "llvm/ADT/ImmutableMap.h" -#include "llvm/ADT/SmallVector.h" -#include "llvm/ADT/SmallPtrSet.h" -#include "llvm/Support/Allocator.h" -#include "llvm/Support/Compiler.h" -#include "llvm/Support/Streams.h" - -#include - -#ifndef NDEBUG -#include "llvm/Support/GraphWriter.h" -#include -#endif - -using namespace clang; -using llvm::dyn_cast; -using llvm::cast; -using llvm::APSInt; - //===----------------------------------------------------------------------===// -// The Checker. -// -// FIXME: This checker logic should be eventually broken into two components. -// The first is the "meta"-level checking logic; the code that -// does the Stmt visitation, fetching values from the map, etc. -// The second part does the actual state manipulation. This way we -// get more of a separate of concerns of these two pieces, with the -// latter potentially being refactored back into the main checking -// logic. -//===----------------------------------------------------------------------===// - -namespace { - -class VISIBILITY_HIDDEN GRExprEngine { - -public: - typedef ValueStateManager::StateTy StateTy; - typedef ExplodedGraph GraphTy; - typedef GraphTy::NodeTy NodeTy; - - // Builders. - typedef GRStmtNodeBuilder StmtNodeBuilder; - typedef GRBranchNodeBuilder BranchNodeBuilder; - typedef GRIndirectGotoNodeBuilder IndirectGotoNodeBuilder; - typedef GRSwitchNodeBuilder SwitchNodeBuilder; - - class NodeSet { - typedef llvm::SmallVector ImplTy; - ImplTy Impl; - public: - - NodeSet() {} - NodeSet(NodeTy* N) { assert (N && !N->isSink()); Impl.push_back(N); } - - void Add(NodeTy* N) { if (N && !N->isSink()) Impl.push_back(N); } - - typedef ImplTy::iterator iterator; - typedef ImplTy::const_iterator const_iterator; - - unsigned size() const { return Impl.size(); } - bool empty() const { return Impl.empty(); } - - iterator begin() { return Impl.begin(); } - iterator end() { return Impl.end(); } - - const_iterator begin() const { return Impl.begin(); } - const_iterator end() const { return Impl.end(); } - }; - -protected: - /// G - the simulation graph. - GraphTy& G; - - /// Liveness - live-variables information the ValueDecl* and block-level - /// Expr* in the CFG. Used to prune out dead state. - LiveVariables Liveness; - - /// Builder - The current GRStmtNodeBuilder which is used when building the - /// nodes for a given statement. - StmtNodeBuilder* Builder; - - /// StateMgr - Object that manages the data for all created states. - ValueStateManager StateMgr; - - /// ValueMgr - Object that manages the data for all created RValues. - ValueManager& ValMgr; - - /// TF - Object that represents a bundle of transfer functions - /// for manipulating and creating RValues. - GRTransferFuncs& TF; - - /// SymMgr - Object that manages the symbol information. - SymbolManager& SymMgr; - - /// StmtEntryNode - The immediate predecessor node. - NodeTy* StmtEntryNode; - - /// CurrentStmt - The current block-level statement. - Stmt* CurrentStmt; - - /// UninitBranches - Nodes in the ExplodedGraph that result from - /// taking a branch based on an uninitialized value. - typedef llvm::SmallPtrSet UninitBranchesTy; - UninitBranchesTy UninitBranches; - - /// ImplicitNullDeref - Nodes in the ExplodedGraph that result from - /// taking a dereference on a symbolic pointer that may be NULL. - typedef llvm::SmallPtrSet NullDerefTy; - NullDerefTy ImplicitNullDeref; - NullDerefTy ExplicitNullDeref; - - - bool StateCleaned; - -public: - GRExprEngine(GraphTy& g) : - G(g), Liveness(G.getCFG(), G.getFunctionDecl()), - Builder(NULL), - StateMgr(G.getContext(), G.getAllocator()), - ValMgr(StateMgr.getValueManager()), - TF(*(new GRSimpleVals())), // FIXME. - SymMgr(StateMgr.getSymbolManager()), - StmtEntryNode(NULL), CurrentStmt(NULL) { - - // Compute liveness information. - Liveness.runOnCFG(G.getCFG()); - Liveness.runOnAllBlocks(G.getCFG(), NULL, true); - } - - /// getContext - Return the ASTContext associated with this analysis. - ASTContext& getContext() const { return G.getContext(); } - - /// getCFG - Returns the CFG associated with this analysis. - CFG& getCFG() { return G.getCFG(); } - - /// getInitialState - Return the initial state used for the root vertex - /// in the ExplodedGraph. - StateTy getInitialState() { - StateTy St = StateMgr.getInitialState(); - - // Iterate the parameters. - FunctionDecl& F = G.getFunctionDecl(); - - for (FunctionDecl::param_iterator I=F.param_begin(), E=F.param_end(); - I!=E; ++I) - St = SetValue(St, lval::DeclVal(*I), RValue::GetSymbolValue(SymMgr, *I)); - - return St; - } - - bool isUninitControlFlow(const NodeTy* N) const { - return N->isSink() && UninitBranches.count(const_cast(N)) != 0; - } - - bool isImplicitNullDeref(const NodeTy* N) const { - return N->isSink() && ImplicitNullDeref.count(const_cast(N)) != 0; - } - - bool isExplicitNullDeref(const NodeTy* N) const { - return N->isSink() && ExplicitNullDeref.count(const_cast(N)) != 0; - } - - typedef NullDerefTy::iterator null_iterator; - null_iterator null_begin() { return ExplicitNullDeref.begin(); } - null_iterator null_end() { return ExplicitNullDeref.end(); } - - /// ProcessStmt - Called by GRCoreEngine. Used to generate new successor - /// nodes by processing the 'effects' of a block-level statement. - void ProcessStmt(Stmt* S, StmtNodeBuilder& builder); - - /// ProcessBranch - Called by GRCoreEngine. Used to generate successor - /// nodes by processing the 'effects' of a branch condition. - void ProcessBranch(Expr* Condition, Stmt* Term, BranchNodeBuilder& builder); - - /// ProcessIndirectGoto - Called by GRCoreEngine. Used to generate successor - /// nodes by processing the 'effects' of a computed goto jump. - void ProcessIndirectGoto(IndirectGotoNodeBuilder& builder); - - /// ProcessSwitch - Called by GRCoreEngine. Used to generate successor - /// nodes by processing the 'effects' of a switch statement. - void ProcessSwitch(SwitchNodeBuilder& builder); - - /// RemoveDeadBindings - Return a new state that is the same as 'St' except - /// that all subexpression mappings are removed and that any - /// block-level expressions that are not live at 'S' also have their - /// mappings removed. - inline StateTy RemoveDeadBindings(Stmt* S, StateTy St) { - return StateMgr.RemoveDeadBindings(St, S, Liveness); - } - - StateTy SetValue(StateTy St, Expr* S, const RValue& V); - - StateTy SetValue(StateTy St, const Expr* S, const RValue& V) { - return SetValue(St, const_cast(S), V); - } - - /// SetValue - This version of SetValue is used to batch process a set - /// of different possible RValues and return a set of different states. - const StateTy::BufferTy& SetValue(StateTy St, Expr* S, - const RValue::BufferTy& V, - StateTy::BufferTy& RetBuf); - - StateTy SetValue(StateTy St, const LValue& LV, const RValue& V); - - inline RValue GetValue(const StateTy& St, Expr* S) { - return StateMgr.GetValue(St, S); - } - - inline RValue GetValue(const StateTy& St, Expr* S, bool& hasVal) { - return StateMgr.GetValue(St, S, &hasVal); - } - - inline RValue GetValue(const StateTy& St, const Expr* S) { - return GetValue(St, const_cast(S)); - } - - inline RValue GetValue(const StateTy& St, const LValue& LV, - QualType* T = NULL) { - - return StateMgr.GetValue(St, LV, T); - } - - inline LValue GetLValue(const StateTy& St, Expr* S) { - return StateMgr.GetLValue(St, S); - } - - inline NonLValue GetRValueConstant(uint64_t X, Expr* E) { - return NonLValue::GetValue(ValMgr, X, E->getType(), E->getLocStart()); - } - - /// Assume - Create new state by assuming that a given expression - /// is true or false. - inline StateTy Assume(StateTy St, RValue Cond, bool Assumption, - bool& isFeasible) { - if (isa(Cond)) - return Assume(St, cast(Cond), Assumption, isFeasible); - else - return Assume(St, cast(Cond), Assumption, isFeasible); - } - - StateTy Assume(StateTy St, LValue Cond, bool Assumption, bool& isFeasible); - StateTy Assume(StateTy St, NonLValue Cond, bool Assumption, bool& isFeasible); - - StateTy AssumeSymNE(StateTy St, SymbolID sym, const llvm::APSInt& V, - bool& isFeasible); - - StateTy AssumeSymEQ(StateTy St, SymbolID sym, const llvm::APSInt& V, - bool& isFeasible); - - StateTy AssumeSymInt(StateTy St, bool Assumption, const SymIntConstraint& C, - bool& isFeasible); - - NodeTy* Nodify(NodeSet& Dst, Stmt* S, NodeTy* Pred, StateTy St); - - /// Nodify - This version of Nodify is used to batch process a set of states. - /// The states are not guaranteed to be unique. - void Nodify(NodeSet& Dst, Stmt* S, NodeTy* Pred, const StateTy::BufferTy& SB); - - /// Visit - Transfer function logic for all statements. Dispatches to - /// other functions that handle specific kinds of statements. - void Visit(Stmt* S, NodeTy* Pred, NodeSet& Dst); - - /// VisitBinaryOperator - Transfer function logic for binary operators. - void VisitBinaryOperator(BinaryOperator* B, NodeTy* Pred, NodeSet& Dst); - - void VisitAssignmentLHS(Expr* E, NodeTy* Pred, NodeSet& Dst); - - /// VisitCast - Transfer function logic for all casts (implicit and explicit). - void VisitCast(Expr* CastE, Expr* E, NodeTy* Pred, NodeSet& Dst); - - /// VisitDeclRefExpr - Transfer function logic for DeclRefExprs. - void VisitDeclRefExpr(DeclRefExpr* DR, NodeTy* Pred, NodeSet& Dst); - - /// VisitDeclStmt - Transfer function logic for DeclStmts. - void VisitDeclStmt(DeclStmt* DS, NodeTy* Pred, NodeSet& Dst); - - /// VisitGuardedExpr - Transfer function logic for ?, __builtin_choose - void VisitGuardedExpr(Expr* S, Expr* LHS, Expr* RHS, - NodeTy* Pred, NodeSet& Dst); - - /// VisitLogicalExpr - Transfer function logic for '&&', '||' - void VisitLogicalExpr(BinaryOperator* B, NodeTy* Pred, NodeSet& Dst); - - /// VisitSizeOfAlignOfTypeExpr - Transfer function for sizeof(type). - void VisitSizeOfAlignOfTypeExpr(SizeOfAlignOfTypeExpr* S, NodeTy* Pred, - NodeSet& Dst); - - /// VisitUnaryOperator - Transfer function logic for unary operators. - void VisitUnaryOperator(UnaryOperator* B, NodeTy* Pred, NodeSet& Dst); - - - inline RValue EvalCast(ValueManager& ValMgr, RValue R, Expr* CastExpr) { - return TF.EvalCast(ValMgr, R, CastExpr); - } - - inline NonLValue EvalMinus(ValueManager& ValMgr, UnaryOperator* U, - NonLValue X) { - return TF.EvalMinus(ValMgr, U, X); - } - - inline NonLValue EvalComplement(ValueManager& ValMgr, NonLValue X) { - return TF.EvalComplement(ValMgr, X); - } - - inline NonLValue EvalBinaryOp(ValueManager& ValMgr, BinaryOperator::Opcode Op, - NonLValue LHS, NonLValue RHS) { - return TF.EvalBinaryOp(ValMgr, Op, LHS, RHS); - } - - inline RValue EvalBinaryOp(ValueManager& ValMgr, BinaryOperator::Opcode Op, - LValue LHS, LValue RHS) { - return TF.EvalBinaryOp(ValMgr, Op, LHS, RHS); - } -}; -} // end anonymous namespace +#include "clang/Analysis/PathSensitive/GRExprEngine.h" GRExprEngine::StateTy GRExprEngine::SetValue(StateTy St, Expr* S, const RValue& V) { @@ -1542,6 +1210,8 @@ void RunGRConstants(CFG& cfg, FunctionDecl& FD, ASTContext& Ctx, GRCoreEngine Engine(cfg, FD, Ctx); GRExprEngine* CheckerState = &Engine.getCheckerState(); + GRSimpleVals GRSV; + CheckerState->setTransferFunctions(GRSV); // Execute the worklist algorithm. Engine.ExecuteWorkList(); diff --git a/include/clang/Analysis/PathSensitive/GRExprEngine.h b/include/clang/Analysis/PathSensitive/GRExprEngine.h new file mode 100644 index 0000000000..1259af691d --- /dev/null +++ b/include/clang/Analysis/PathSensitive/GRExprEngine.h @@ -0,0 +1,338 @@ +//===-- GRExprEngine.cpp - Simple, Path-Sens. Constant Prop. -----*- C++ -*-==// +// +// The LLVM Compiler Infrastructure +// +// This file is distributed under the University of Illinois Open Source +// License. See LICENSE.TXT for details. +// +//===----------------------------------------------------------------------===// +// +// Constant Propagation via Graph Reachability +// +// This files defines +// +// +//===----------------------------------------------------------------------===// + +#include "ValueState.h" + +#include "clang/Analysis/PathSensitive/GRCoreEngine.h" +#include "clang/Analysis/PathSensitive/GRTransferFuncs.h" +#include "GRSimpleVals.h" + +#include "clang/AST/Expr.h" +#include "clang/AST/ASTContext.h" +#include "clang/Analysis/Analyses/LiveVariables.h" +#include "clang/Basic/Diagnostic.h" + +#include "llvm/Support/Casting.h" +#include "llvm/Support/DataTypes.h" +#include "llvm/ADT/APSInt.h" +#include "llvm/ADT/FoldingSet.h" +#include "llvm/ADT/ImmutableMap.h" +#include "llvm/ADT/SmallVector.h" +#include "llvm/ADT/SmallPtrSet.h" +#include "llvm/Support/Allocator.h" +#include "llvm/Support/Compiler.h" +#include "llvm/Support/Streams.h" + +#include + +#ifndef NDEBUG +#include "llvm/Support/GraphWriter.h" +#include +#endif + +using namespace clang; +using llvm::dyn_cast; +using llvm::cast; +using llvm::APSInt; + +namespace { + + class VISIBILITY_HIDDEN GRExprEngine { + + public: + typedef ValueStateManager::StateTy StateTy; + typedef ExplodedGraph GraphTy; + typedef GraphTy::NodeTy NodeTy; + + // Builders. + typedef GRStmtNodeBuilder StmtNodeBuilder; + typedef GRBranchNodeBuilder BranchNodeBuilder; + typedef GRIndirectGotoNodeBuilder IndirectGotoNodeBuilder; + typedef GRSwitchNodeBuilder SwitchNodeBuilder; + + class NodeSet { + typedef llvm::SmallVector ImplTy; + ImplTy Impl; + public: + + NodeSet() {} + NodeSet(NodeTy* N) { assert (N && !N->isSink()); Impl.push_back(N); } + + void Add(NodeTy* N) { if (N && !N->isSink()) Impl.push_back(N); } + + typedef ImplTy::iterator iterator; + typedef ImplTy::const_iterator const_iterator; + + unsigned size() const { return Impl.size(); } + bool empty() const { return Impl.empty(); } + + iterator begin() { return Impl.begin(); } + iterator end() { return Impl.end(); } + + const_iterator begin() const { return Impl.begin(); } + const_iterator end() const { return Impl.end(); } + }; + + protected: + /// G - the simulation graph. + GraphTy& G; + + /// Liveness - live-variables information the ValueDecl* and block-level + /// Expr* in the CFG. Used to prune out dead state. + LiveVariables Liveness; + + /// Builder - The current GRStmtNodeBuilder which is used when building the + /// nodes for a given statement. + StmtNodeBuilder* Builder; + + /// StateMgr - Object that manages the data for all created states. + ValueStateManager StateMgr; + + /// ValueMgr - Object that manages the data for all created RValues. + ValueManager& ValMgr; + + /// TF - Object that represents a bundle of transfer functions + /// for manipulating and creating RValues. + GRTransferFuncs* TF; + + /// SymMgr - Object that manages the symbol information. + SymbolManager& SymMgr; + + /// StmtEntryNode - The immediate predecessor node. + NodeTy* StmtEntryNode; + + /// CurrentStmt - The current block-level statement. + Stmt* CurrentStmt; + + /// UninitBranches - Nodes in the ExplodedGraph that result from + /// taking a branch based on an uninitialized value. + typedef llvm::SmallPtrSet UninitBranchesTy; + UninitBranchesTy UninitBranches; + + /// ImplicitNullDeref - Nodes in the ExplodedGraph that result from + /// taking a dereference on a symbolic pointer that may be NULL. + typedef llvm::SmallPtrSet NullDerefTy; + NullDerefTy ImplicitNullDeref; + NullDerefTy ExplicitNullDeref; + + + bool StateCleaned; + + public: + GRExprEngine(GraphTy& g) : + G(g), Liveness(G.getCFG(), G.getFunctionDecl()), + Builder(NULL), + StateMgr(G.getContext(), G.getAllocator()), + ValMgr(StateMgr.getValueManager()), + TF(NULL), // FIXME. + SymMgr(StateMgr.getSymbolManager()), + StmtEntryNode(NULL), CurrentStmt(NULL) { + + // Compute liveness information. + Liveness.runOnCFG(G.getCFG()); + Liveness.runOnAllBlocks(G.getCFG(), NULL, true); + } + + /// getContext - Return the ASTContext associated with this analysis. + ASTContext& getContext() const { return G.getContext(); } + + /// getCFG - Returns the CFG associated with this analysis. + CFG& getCFG() { return G.getCFG(); } + + /// setTransferFunctions + void setTransferFunctions(GRTransferFuncs* tf) { TF = tf; } + void setTransferFunctions(GRTransferFuncs& tf) { TF = &tf; } + + /// getInitialState - Return the initial state used for the root vertex + /// in the ExplodedGraph. + StateTy getInitialState() { + StateTy St = StateMgr.getInitialState(); + + // Iterate the parameters. + FunctionDecl& F = G.getFunctionDecl(); + + for (FunctionDecl::param_iterator I=F.param_begin(), E=F.param_end(); + I!=E; ++I) + St = SetValue(St, lval::DeclVal(*I), RValue::GetSymbolValue(SymMgr, *I)); + + return St; + } + + bool isUninitControlFlow(const NodeTy* N) const { + return N->isSink() && UninitBranches.count(const_cast(N)) != 0; + } + + bool isImplicitNullDeref(const NodeTy* N) const { + return N->isSink() && ImplicitNullDeref.count(const_cast(N)) != 0; + } + + bool isExplicitNullDeref(const NodeTy* N) const { + return N->isSink() && ExplicitNullDeref.count(const_cast(N)) != 0; + } + + typedef NullDerefTy::iterator null_iterator; + null_iterator null_begin() { return ExplicitNullDeref.begin(); } + null_iterator null_end() { return ExplicitNullDeref.end(); } + + /// ProcessStmt - Called by GRCoreEngine. Used to generate new successor + /// nodes by processing the 'effects' of a block-level statement. + void ProcessStmt(Stmt* S, StmtNodeBuilder& builder); + + /// ProcessBranch - Called by GRCoreEngine. Used to generate successor + /// nodes by processing the 'effects' of a branch condition. + void ProcessBranch(Expr* Condition, Stmt* Term, BranchNodeBuilder& builder); + + /// ProcessIndirectGoto - Called by GRCoreEngine. Used to generate successor + /// nodes by processing the 'effects' of a computed goto jump. + void ProcessIndirectGoto(IndirectGotoNodeBuilder& builder); + + /// ProcessSwitch - Called by GRCoreEngine. Used to generate successor + /// nodes by processing the 'effects' of a switch statement. + void ProcessSwitch(SwitchNodeBuilder& builder); + + /// RemoveDeadBindings - Return a new state that is the same as 'St' except + /// that all subexpression mappings are removed and that any + /// block-level expressions that are not live at 'S' also have their + /// mappings removed. + inline StateTy RemoveDeadBindings(Stmt* S, StateTy St) { + return StateMgr.RemoveDeadBindings(St, S, Liveness); + } + + StateTy SetValue(StateTy St, Expr* S, const RValue& V); + + StateTy SetValue(StateTy St, const Expr* S, const RValue& V) { + return SetValue(St, const_cast(S), V); + } + + /// SetValue - This version of SetValue is used to batch process a set + /// of different possible RValues and return a set of different states. + const StateTy::BufferTy& SetValue(StateTy St, Expr* S, + const RValue::BufferTy& V, + StateTy::BufferTy& RetBuf); + + StateTy SetValue(StateTy St, const LValue& LV, const RValue& V); + + inline RValue GetValue(const StateTy& St, Expr* S) { + return StateMgr.GetValue(St, S); + } + + inline RValue GetValue(const StateTy& St, Expr* S, bool& hasVal) { + return StateMgr.GetValue(St, S, &hasVal); + } + + inline RValue GetValue(const StateTy& St, const Expr* S) { + return GetValue(St, const_cast(S)); + } + + inline RValue GetValue(const StateTy& St, const LValue& LV, + QualType* T = NULL) { + + return StateMgr.GetValue(St, LV, T); + } + + inline LValue GetLValue(const StateTy& St, Expr* S) { + return StateMgr.GetLValue(St, S); + } + + inline NonLValue GetRValueConstant(uint64_t X, Expr* E) { + return NonLValue::GetValue(ValMgr, X, E->getType(), E->getLocStart()); + } + + /// Assume - Create new state by assuming that a given expression + /// is true or false. + inline StateTy Assume(StateTy St, RValue Cond, bool Assumption, + bool& isFeasible) { + if (isa(Cond)) + return Assume(St, cast(Cond), Assumption, isFeasible); + else + return Assume(St, cast(Cond), Assumption, isFeasible); + } + + StateTy Assume(StateTy St, LValue Cond, bool Assumption, bool& isFeasible); + StateTy Assume(StateTy St, NonLValue Cond, bool Assumption, bool& isFeasible); + + StateTy AssumeSymNE(StateTy St, SymbolID sym, const llvm::APSInt& V, + bool& isFeasible); + + StateTy AssumeSymEQ(StateTy St, SymbolID sym, const llvm::APSInt& V, + bool& isFeasible); + + StateTy AssumeSymInt(StateTy St, bool Assumption, const SymIntConstraint& C, + bool& isFeasible); + + NodeTy* Nodify(NodeSet& Dst, Stmt* S, NodeTy* Pred, StateTy St); + + /// Nodify - This version of Nodify is used to batch process a set of states. + /// The states are not guaranteed to be unique. + void Nodify(NodeSet& Dst, Stmt* S, NodeTy* Pred, const StateTy::BufferTy& SB); + + /// Visit - Transfer function logic for all statements. Dispatches to + /// other functions that handle specific kinds of statements. + void Visit(Stmt* S, NodeTy* Pred, NodeSet& Dst); + + /// VisitBinaryOperator - Transfer function logic for binary operators. + void VisitBinaryOperator(BinaryOperator* B, NodeTy* Pred, NodeSet& Dst); + + void VisitAssignmentLHS(Expr* E, NodeTy* Pred, NodeSet& Dst); + + /// VisitCast - Transfer function logic for all casts (implicit and explicit). + void VisitCast(Expr* CastE, Expr* E, NodeTy* Pred, NodeSet& Dst); + + /// VisitDeclRefExpr - Transfer function logic for DeclRefExprs. + void VisitDeclRefExpr(DeclRefExpr* DR, NodeTy* Pred, NodeSet& Dst); + + /// VisitDeclStmt - Transfer function logic for DeclStmts. + void VisitDeclStmt(DeclStmt* DS, NodeTy* Pred, NodeSet& Dst); + + /// VisitGuardedExpr - Transfer function logic for ?, __builtin_choose + void VisitGuardedExpr(Expr* S, Expr* LHS, Expr* RHS, + NodeTy* Pred, NodeSet& Dst); + + /// VisitLogicalExpr - Transfer function logic for '&&', '||' + void VisitLogicalExpr(BinaryOperator* B, NodeTy* Pred, NodeSet& Dst); + + /// VisitSizeOfAlignOfTypeExpr - Transfer function for sizeof(type). + void VisitSizeOfAlignOfTypeExpr(SizeOfAlignOfTypeExpr* S, NodeTy* Pred, + NodeSet& Dst); + + /// VisitUnaryOperator - Transfer function logic for unary operators. + void VisitUnaryOperator(UnaryOperator* B, NodeTy* Pred, NodeSet& Dst); + + + inline RValue EvalCast(ValueManager& ValMgr, RValue R, Expr* CastExpr) { + return TF->EvalCast(ValMgr, R, CastExpr); + } + + inline NonLValue EvalMinus(ValueManager& ValMgr, UnaryOperator* U, + NonLValue X) { + return TF->EvalMinus(ValMgr, U, X); + } + + inline NonLValue EvalComplement(ValueManager& ValMgr, NonLValue X) { + return TF->EvalComplement(ValMgr, X); + } + + inline NonLValue EvalBinaryOp(ValueManager& ValMgr, BinaryOperator::Opcode Op, + NonLValue LHS, NonLValue RHS) { + return TF->EvalBinaryOp(ValMgr, Op, LHS, RHS); + } + + inline RValue EvalBinaryOp(ValueManager& ValMgr, BinaryOperator::Opcode Op, + LValue LHS, LValue RHS) { + return TF->EvalBinaryOp(ValMgr, Op, LHS, RHS); + } + }; +} // end anonymous namespace \ No newline at end of file