@@ -2776,10 +2776,12 @@ assumeCondition(const Stmt *Condition, ExplodedNode *N) {
2776
2776
return State->assume (V);
2777
2777
}
2778
2778
2779
- void ExprEngine::processBranch (
2780
- const Stmt *Condition, NodeBuilderContext &BldCtx, ExplodedNode *Pred,
2781
- ExplodedNodeSet &Dst, const CFGBlock *DstT, const CFGBlock *DstF,
2782
- std::optional<unsigned > IterationsCompletedInLoop) {
2779
+ void ExprEngine::processBranch (const Stmt *Condition,
2780
+ NodeBuilderContext& BldCtx,
2781
+ ExplodedNode *Pred,
2782
+ ExplodedNodeSet &Dst,
2783
+ const CFGBlock *DstT,
2784
+ const CFGBlock *DstF) {
2783
2785
assert ((!Condition || !isa<CXXBindTemporaryExpr>(Condition)) &&
2784
2786
" CXXBindTemporaryExprs are handled by processBindTemporary." );
2785
2787
const LocationContext *LCtx = Pred->getLocationContext ();
@@ -2822,63 +2824,11 @@ void ExprEngine::processBranch(
2822
2824
if (StTrue && StFalse)
2823
2825
assert (!isa<ObjCForCollectionStmt>(Condition));
2824
2826
2825
- // We want to ensure consistent behavior between `eagerly-assume=false`,
2826
- // when the state split is always performed by the `assumeCondition()`
2827
- // call within this function and `eagerly-assume=true` (the default), when
2828
- // some conditions (comparison operators, unary negation) can trigger a
2829
- // state split before this callback. There are some contrived corner cases
2830
- // that behave differently with and without `eagerly-assume`, but I don't
2831
- // know about an example that could plausibly appear in "real" code.
2832
- bool BothFeasible =
2833
- (StTrue && StFalse) ||
2834
- didEagerlyAssumeBifurcateAt (PrevState, dyn_cast<Expr>(Condition));
2835
-
2836
- if (StTrue) {
2837
- // In a loop, if both branches are feasible (i.e. the analyzer doesn't
2838
- // understand the loop condition) and two iterations have already been
2839
- // completed, then don't assume a third iteration because it is a
2840
- // redundant execution path (unlikely to be different from earlier loop
2841
- // exits) and can cause false positives if e.g. the loop iterates over a
2842
- // two-element structure with an opaque condition.
2843
- //
2844
- // The iteration count "2" is hardcoded because it's the natural limit:
2845
- // * the fact that the programmer wrote a loop (and not just an `if`)
2846
- // implies that they thought that the loop body might be executed twice;
2847
- // * however, there are situations where the programmer knows that there
2848
- // are at most two iterations but writes a loop that appears to be
2849
- // generic, because there is no special syntax for "loop with at most
2850
- // two iterations". (This pattern is common in FFMPEG and appears in
2851
- // many other projects as well.)
2852
- bool CompletedTwoIterations = IterationsCompletedInLoop.value_or (0 ) >= 2 ;
2853
- bool SkipTrueBranch = BothFeasible && CompletedTwoIterations;
2854
-
2855
- // FIXME: This "don't assume third iteration" heuristic partially
2856
- // conflicts with the widen-loop analysis option (which is off by
2857
- // default). If we intend to support and stabilize the loop widening,
2858
- // we must ensure that it 'plays nicely' with this logic.
2859
- if (!SkipTrueBranch || AMgr.options .ShouldWidenLoops )
2860
- Builder.generateNode (StTrue, true , PredN);
2861
- }
2862
-
2863
- if (StFalse) {
2864
- // In a loop, if both branches are feasible (i.e. the analyzer doesn't
2865
- // understand the loop condition), we are before the first iteration and
2866
- // the analyzer option `assume-at-least-one-iteration` is set to `true`,
2867
- // then avoid creating the execution path where the loop is skipped.
2868
- //
2869
- // In some situations this "loop is skipped" execution path is an
2870
- // important corner case that may evade the notice of the developer and
2871
- // hide significant bugs -- however, there are also many situations where
2872
- // it's guaranteed that at least one iteration will happen (e.g. some
2873
- // data structure is always nonempty), but the analyzer cannot realize
2874
- // this and will produce false positives when it assumes that the loop is
2875
- // skipped.
2876
- bool BeforeFirstIteration = IterationsCompletedInLoop == std::optional{0 };
2877
- bool SkipFalseBranch = BothFeasible && BeforeFirstIteration &&
2878
- AMgr.options .ShouldAssumeAtLeastOneIteration ;
2879
- if (!SkipFalseBranch)
2880
- Builder.generateNode (StFalse, false , PredN);
2881
- }
2827
+ if (StTrue)
2828
+ Builder.generateNode (StTrue, true , PredN);
2829
+
2830
+ if (StFalse)
2831
+ Builder.generateNode (StFalse, false , PredN);
2882
2832
}
2883
2833
currBldrCtx = nullptr ;
2884
2834
}
@@ -3819,12 +3769,6 @@ ExprEngine::getEagerlyAssumeBifurcationTags() {
3819
3769
return std::make_pair (&TrueTag, &FalseTag);
3820
3770
}
3821
3771
3822
- // / If the last EagerlyAssume attempt was successful (i.e. the true and false
3823
- // / cases were both feasible), this state trait stores the expression where it
3824
- // / happened; otherwise this holds nullptr.
3825
- REGISTER_TRAIT_WITH_PROGRAMSTATE (LastEagerlyAssumeExprIfSuccessful,
3826
- const Expr *)
3827
-
3828
3772
void ExprEngine::evalEagerlyAssumeBifurcation (ExplodedNodeSet &Dst,
3829
3773
ExplodedNodeSet &Src,
3830
3774
const Expr *Ex) {
@@ -3840,19 +3784,13 @@ void ExprEngine::evalEagerlyAssumeBifurcation(ExplodedNodeSet &Dst,
3840
3784
}
3841
3785
3842
3786
ProgramStateRef State = Pred->getState ();
3843
- State = State->set <LastEagerlyAssumeExprIfSuccessful>(nullptr );
3844
3787
SVal V = State->getSVal (Ex, Pred->getLocationContext ());
3845
3788
std::optional<nonloc::SymbolVal> SEV = V.getAs <nonloc::SymbolVal>();
3846
3789
if (SEV && SEV->isExpression ()) {
3847
3790
const auto &[TrueTag, FalseTag] = getEagerlyAssumeBifurcationTags ();
3848
3791
3849
3792
auto [StateTrue, StateFalse] = State->assume (*SEV);
3850
3793
3851
- if (StateTrue && StateFalse) {
3852
- StateTrue = StateTrue->set <LastEagerlyAssumeExprIfSuccessful>(Ex);
3853
- StateFalse = StateFalse->set <LastEagerlyAssumeExprIfSuccessful>(Ex);
3854
- }
3855
-
3856
3794
// First assume that the condition is true.
3857
3795
if (StateTrue) {
3858
3796
SVal Val = svalBuilder.makeIntVal (1U , Ex->getType ());
@@ -3870,11 +3808,6 @@ void ExprEngine::evalEagerlyAssumeBifurcation(ExplodedNodeSet &Dst,
3870
3808
}
3871
3809
}
3872
3810
3873
- bool ExprEngine::didEagerlyAssumeBifurcateAt (ProgramStateRef State,
3874
- const Expr *Ex) const {
3875
- return Ex && State->get <LastEagerlyAssumeExprIfSuccessful>() == Ex;
3876
- }
3877
-
3878
3811
void ExprEngine::VisitGCCAsmStmt (const GCCAsmStmt *A, ExplodedNode *Pred,
3879
3812
ExplodedNodeSet &Dst) {
3880
3813
StmtNodeBuilder Bldr (Pred, Dst, *currBldrCtx);
0 commit comments