#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"
};
}
+typedef ValueMapTy StateTy;
+
//===----------------------------------------------------------------------===//
// 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 {
public:
NodeSet() {}
- NodeSet(NodeTy* N) { assert (N && !N->isInfeasible()); Impl.push_back(N); }
+ NodeSet(NodeTy* N) { assert (N && !N->isSink()); Impl.push_back(N); }
- void Add(NodeTy* N) { if (N && !N->isInfeasible()) 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;
/// 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<NodeTy*,5> UninitBranchesTy;
+ UninitBranchesTy UninitBranches;
+
bool StateCleaned;
ASTContext& getContext() const { return G.getContext(); }
RValue GetValue(const StateTy& St, const LValue& LV);
LValue GetLValue(const StateTy& St, Stmt* S);
+
+ /// 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<LValue>(Cond))
+ return Assume(St, cast<LValue>(Cond), Assumption, isFeasible);
+ else
+ return Assume(St, cast<NonLValue>(Cond), Assumption, isFeasible);
+ }
+
+ StateTy Assume(StateTy St, LValue Cond, bool Assumption, bool& isFeasible);
+ StateTy Assume(StateTy St, NonLValue Cond, bool Assumption, bool& isFeasible);
void Nodify(NodeSet& Dst, Stmt* S, NodeTy* Pred, StateTy St);
void GRConstants::ProcessBranch(Stmt* Condition, Stmt* Term,
BranchNodeBuilder& builder) {
+
+ StateTy PrevState = builder.getState();
+
+ // Remove old bindings for subexpressions.
+ for (StateTy::iterator I=PrevState.begin(), E=PrevState.end(); I!=E; ++I)
+ if (I.getKey().isSubExpr())
+ PrevState = StateMgr.Remove(PrevState, I.getKey());
+
+ RValue V = GetValue(PrevState, Condition);
+
+ switch (V.getBaseKind()) {
+ default:
+ break;
+
+ case RValue::InvalidKind:
+ builder.generateNode(PrevState, true);
+ builder.generateNode(PrevState, false);
+ return;
+
+ case RValue::UninitializedKind: {
+ NodeTy* N = builder.generateNode(PrevState, true);
+
+ if (N) {
+ N->markAsSink();
+ UninitBranches.insert(N);
+ }
+
+ builder.markInfeasible(false);
+ return;
+ }
+ }
+
+ // Process the true branch.
+ bool isFeasible = true;
+ StateTy St = Assume(PrevState, V, true, isFeasible);
+
+ if (isFeasible) builder.generateNode(St, true);
+ else {
+ builder.markInfeasible(true);
+ isFeasible = true;
+ }
+ // Process the false branch.
+ St = Assume(PrevState, V, false, isFeasible);
+ if (isFeasible) builder.generateNode(St, false);
+ else builder.markInfeasible(false);
+
}
void GRConstants::ProcessStmt(Stmt* S, StmtNodeBuilder& builder) {
}
}
+//===----------------------------------------------------------------------===//
+// "Assume" logic.
+//===----------------------------------------------------------------------===//
+
+StateTy GRConstants::Assume(StateTy St, LValue Cond, bool Assumption,
+ bool& isFeasible) {
+ return St;
+}
+
+StateTy GRConstants::Assume(StateTy St, NonLValue Cond, bool Assumption,
+ bool& isFeasible) {
+
+ switch (Cond.getSubKind()) {
+ default:
+ assert (false && "'Assume' not implemented for this NonLValue.");
+ return St;
+
+ case ConcreteIntKind: {
+ bool b = cast<ConcreteInt>(Cond).getValue() != 0;
+ isFeasible = b ? Assumption : !Assumption;
+ return St;
+ }
+ }
+}
+
+
//===----------------------------------------------------------------------===//
// Driver.
//===----------------------------------------------------------------------===//
const BlockEdge& E = cast<BlockEdge>(Loc);
Out << "Edge: (B" << E.getSrc()->getBlockID() << ", B"
<< E.getDst()->getBlockID() << ')';
+
+ if (Stmt* T = E.getSrc()->getTerminator()) {
+ Out << "\\|Terminator: ";
+ E.getSrc()->printTerminator(Out);
+
+ if (isa<SwitchStmt>(T)) {
+ // FIXME
+ }
+ else {
+ Out << "\\lCondition: ";
+ if (*E.getSrc()->succ_begin() == E.getDst())
+ Out << "true";
+ else
+ Out << "false";
+ }
+
+ Out << "\\l";
+ }
}
}
friend class GRBranchNodeBuilderImpl;
class NodeGroup {
- enum { Size1 = 0x0, SizeOther = 0x1, Infeasible = 0x2, Flags = 0x3 };
+ enum { Size1 = 0x0, SizeOther = 0x1, AuxFlag = 0x2, Mask = 0x3 };
uintptr_t P;
unsigned getKind() const {
- return P & Flags;
+ return P & Mask;
}
void* getPtr() const {
- return reinterpret_cast<void*>(P & ~Flags);
+ return reinterpret_cast<void*>(P & ~Mask);
}
ExplodedNodeImpl* getNode() const {
void addNode(ExplodedNodeImpl* N);
- void setInfeasibleFlag() {
- P |= Infeasible;
+ void setFlag() {
+ P |= AuxFlag;
}
- bool getInfeasibleFlag() const {
- return P & Infeasible ? true : false;
+ bool getFlag() const {
+ return P & AuxFlag ? true : false;
}
- };
-
+ };
/// Location - The program location (within a function body) associated
/// with this node.
/// addPredeccessor - Adds a predecessor to the current node, and
/// in tandem add this node as a successor of the other node.
void addPredecessor(ExplodedNodeImpl* V) {
- assert (!V->isInfeasible());
+ assert (!V->isSink());
Preds.addNode(V);
V->Succs.addNode(this);
}
bool succ_empty() const { return Succs.empty(); }
bool pred_empty() const { return Preds.size(); }
- bool isInfeasible() const { return Preds.getInfeasibleFlag(); }
- void setInfeasible() { Preds.setInfeasibleFlag(); }
+ bool isSink() const { return Preds.getFlag(); }
+ void markAsSink() { Preds.setFlag(); }
};
const ExplodedGraphImpl& getGraph() const { return *Eng.G; }
inline ExplodedNodeImpl* getLastNode() {
- return LastNode ? (LastNode->isInfeasible() ? NULL : LastNode) : NULL;
+ return LastNode ? (LastNode->isSink() ? NULL : LastNode) : NULL;
}
ExplodedNodeImpl* generateNodeImpl(Stmt* S, void* State,
~GRBranchNodeBuilderImpl();
+ ExplodedNodeImpl* getPredecessor() const { return Pred; }
const ExplodedGraphImpl& getGraph() const { return *Eng.G; }
- void generateNodeImpl(void* State, bool branch);
+ ExplodedNodeImpl* generateNodeImpl(void* State, bool branch);
void markInfeasible(bool branch) {
if (branch) GeneratedTrue = true;
const GraphTy& getGraph() const {
return static_cast<const GraphTy&>(NB.getGraph());
}
+
+ NodeTy* getPredecessor() const {
+ return static_cast<NodeTy*>(NB.getPredecessor());
+ }
+
+ StateTy getState() const {
+ return getPredecessor()->getState();
+ }
- inline void generateNode(StateTy State, bool branch) {
+ inline NodeTy* generateNode(StateTy State, bool branch) {
void *state = GRTrait<StateTy>::toPtr(State);
- NB.generateNodeImpl(state, branch);
+ return static_cast<NodeTy*>(NB.generateNodeImpl(state, branch));
}
inline void markInfeasible(bool branch) {