OLD | NEW |
1 //=-- ExprEngine.cpp - Path-Sensitive Expression-Level Dataflow ---*- C++ -*-= | 1 //=-- ExprEngine.cpp - Path-Sensitive Expression-Level Dataflow ---*- C++ -*-= |
2 // | 2 // |
3 // The LLVM Compiler Infrastructure | 3 // The LLVM Compiler Infrastructure |
4 // | 4 // |
5 // This file is distributed under the University of Illinois Open Source | 5 // This file is distributed under the University of Illinois Open Source |
6 // License. See LICENSE.TXT for details. | 6 // License. See LICENSE.TXT for details. |
7 // | 7 // |
8 //===----------------------------------------------------------------------===// | 8 //===----------------------------------------------------------------------===// |
9 // | 9 // |
10 // This file defines a meta-engine for path-sensitive dataflow analysis that | 10 // This file defines a meta-engine for path-sensitive dataflow analysis that |
(...skipping 2262 matching lines...) Expand 10 before | Expand all | Expand 10 after Loading... |
2273 // Handle the case where the container has no elements. | 2273 // Handle the case where the container has no elements. |
2274 SVal FalseV = svalBuilder.makeTruthVal(0); | 2274 SVal FalseV = svalBuilder.makeTruthVal(0); |
2275 const GRState *noElems = state->BindExpr(S, FalseV); | 2275 const GRState *noElems = state->BindExpr(S, FalseV); |
2276 | 2276 |
2277 if (loc::MemRegionVal* MV = dyn_cast<loc::MemRegionVal>(&ElementV)) | 2277 if (loc::MemRegionVal* MV = dyn_cast<loc::MemRegionVal>(&ElementV)) |
2278 if (const TypedRegion* R = dyn_cast<TypedRegion>(MV->getRegion())) { | 2278 if (const TypedRegion* R = dyn_cast<TypedRegion>(MV->getRegion())) { |
2279 // FIXME: The proper thing to do is to really iterate over the | 2279 // FIXME: The proper thing to do is to really iterate over the |
2280 // container. We will do this with dispatch logic to the store. | 2280 // container. We will do this with dispatch logic to the store. |
2281 // For now, just 'conjure' up a symbolic value. | 2281 // For now, just 'conjure' up a symbolic value. |
2282 QualType T = R->getValueType(); | 2282 QualType T = R->getValueType(); |
2283 assert(Loc::IsLocType(T)); | 2283 assert(Loc::isLocType(T)); |
2284 unsigned Count = Builder->getCurrentBlockCount(); | 2284 unsigned Count = Builder->getCurrentBlockCount(); |
2285 SymbolRef Sym = SymMgr.getConjuredSymbol(elem, T, Count); | 2285 SymbolRef Sym = SymMgr.getConjuredSymbol(elem, T, Count); |
2286 SVal V = svalBuilder.makeLoc(Sym); | 2286 SVal V = svalBuilder.makeLoc(Sym); |
2287 hasElems = hasElems->bindLoc(ElementV, V); | 2287 hasElems = hasElems->bindLoc(ElementV, V); |
2288 | 2288 |
2289 // Bind the location to 'nil' on the false branch. | 2289 // Bind the location to 'nil' on the false branch. |
2290 SVal nilV = svalBuilder.makeIntVal(0, T); | 2290 SVal nilV = svalBuilder.makeIntVal(0, T); |
2291 noElems = noElems->bindLoc(ElementV, nilV); | 2291 noElems = noElems->bindLoc(ElementV, nilV); |
2292 } | 2292 } |
2293 | 2293 |
(...skipping 497 matching lines...) Expand 10 before | Expand all | Expand 10 after Loading... |
2791 else { | 2791 else { |
2792 // Still some initializer values to go. Push them onto the worklist. | 2792 // Still some initializer values to go. Push them onto the worklist. |
2793 WorkList.push_back(InitListWLItem(*NI, NewVals, NewItr)); | 2793 WorkList.push_back(InitListWLItem(*NI, NewVals, NewItr)); |
2794 } | 2794 } |
2795 } | 2795 } |
2796 } | 2796 } |
2797 | 2797 |
2798 return; | 2798 return; |
2799 } | 2799 } |
2800 | 2800 |
2801 if (Loc::IsLocType(T) || T->isIntegerType()) { | 2801 if (Loc::isLocType(T) || T->isIntegerType()) { |
2802 assert (E->getNumInits() == 1); | 2802 assert (E->getNumInits() == 1); |
2803 ExplodedNodeSet Tmp; | 2803 ExplodedNodeSet Tmp; |
2804 const Expr* Init = E->getInit(0); | 2804 const Expr* Init = E->getInit(0); |
2805 Visit(Init, Pred, Tmp); | 2805 Visit(Init, Pred, Tmp); |
2806 for (ExplodedNodeSet::iterator I=Tmp.begin(), EI=Tmp.end(); I != EI; ++I) { | 2806 for (ExplodedNodeSet::iterator I=Tmp.begin(), EI=Tmp.end(); I != EI; ++I) { |
2807 state = GetState(*I); | 2807 state = GetState(*I); |
2808 MakeNode(Dst, E, *I, state->BindExpr(E, state->getSVal(Init))); | 2808 MakeNode(Dst, E, *I, state->BindExpr(E, state->getSVal(Init))); |
2809 } | 2809 } |
2810 return; | 2810 return; |
2811 } | 2811 } |
(...skipping 284 matching lines...) Expand 10 before | Expand all | Expand 10 after Loading... |
3096 // Conjure a new symbol if necessary to recover precision. | 3096 // Conjure a new symbol if necessary to recover precision. |
3097 if (Result.isUnknown() || !getConstraintManager().canReasonAbout(Result)){ | 3097 if (Result.isUnknown() || !getConstraintManager().canReasonAbout(Result)){ |
3098 DefinedOrUnknownSVal SymVal = | 3098 DefinedOrUnknownSVal SymVal = |
3099 svalBuilder.getConjuredSymbolVal(NULL, Ex, | 3099 svalBuilder.getConjuredSymbolVal(NULL, Ex, |
3100 Builder->getCurrentBlockCount()); | 3100 Builder->getCurrentBlockCount()); |
3101 Result = SymVal; | 3101 Result = SymVal; |
3102 | 3102 |
3103 // If the value is a location, ++/-- should always preserve | 3103 // If the value is a location, ++/-- should always preserve |
3104 // non-nullness. Check if the original value was non-null, and if so | 3104 // non-nullness. Check if the original value was non-null, and if so |
3105 // propagate that constraint. | 3105 // propagate that constraint. |
3106 if (Loc::IsLocType(U->getType())) { | 3106 if (Loc::isLocType(U->getType())) { |
3107 DefinedOrUnknownSVal Constraint = | 3107 DefinedOrUnknownSVal Constraint = |
3108 svalBuilder.evalEQ(state, V2,svalBuilder.makeZeroVal(U->getType())); | 3108 svalBuilder.evalEQ(state, V2,svalBuilder.makeZeroVal(U->getType())); |
3109 | 3109 |
3110 if (!state->assume(Constraint, true)) { | 3110 if (!state->assume(Constraint, true)) { |
3111 // It isn't feasible for the original value to be null. | 3111 // It isn't feasible for the original value to be null. |
3112 // Propagate this constraint. | 3112 // Propagate this constraint. |
3113 Constraint = svalBuilder.evalEQ(state, SymVal, | 3113 Constraint = svalBuilder.evalEQ(state, SymVal, |
3114 svalBuilder.makeZeroVal(U->getType())); | 3114 svalBuilder.makeZeroVal(U->getType())); |
3115 | 3115 |
3116 | 3116 |
(...skipping 526 matching lines...) Expand 10 before | Expand all | Expand 10 after Loading... |
3643 | 3643 |
3644 if (!TrimmedG.get()) | 3644 if (!TrimmedG.get()) |
3645 llvm::errs() << "warning: Trimmed ExplodedGraph is empty.\n"; | 3645 llvm::errs() << "warning: Trimmed ExplodedGraph is empty.\n"; |
3646 else | 3646 else |
3647 llvm::ViewGraph(*TrimmedG->roots_begin(), "TrimmedExprEngine"); | 3647 llvm::ViewGraph(*TrimmedG->roots_begin(), "TrimmedExprEngine"); |
3648 | 3648 |
3649 GraphPrintCheckerState = NULL; | 3649 GraphPrintCheckerState = NULL; |
3650 GraphPrintSourceManager = NULL; | 3650 GraphPrintSourceManager = NULL; |
3651 #endif | 3651 #endif |
3652 } | 3652 } |
OLD | NEW |