=?utf-8?q?Donát?= Nagy <donat.n...@ericsson.com>
Message-ID:
In-Reply-To: <llvm.org/llvm/llvm-project/pull/109...@github.com>
================
@@ -2808,27 +2825,63 @@ void ExprEngine::processBranch(const Stmt *Condition,
std::tie(StTrue, StFalse) = *KnownCondValueAssumption;
else {
assert(!isa<ObjCForCollectionStmt>(Condition));
+ // TODO: instead of this shortcut perhaps it would be better to "rejoin"
+ // the common execution path with
+ // StTrue = StFalse = PrevState;
builder.generateNode(PrevState, true, PredN);
builder.generateNode(PrevState, false, PredN);
continue;
}
if (StTrue && StFalse)
assert(!isa<ObjCForCollectionStmt>(Condition));
+ const Expr *EagerlyAssumeExpr =
+ PrevState->get<LastEagerlyAssumeAssumptionAt>();
+ const Expr *ConditionExpr = dyn_cast<Expr>(Condition);
+ if (ConditionExpr)
+ ConditionExpr = ConditionExpr->IgnoreParenCasts();
+ bool DidEagerlyAssume = EagerlyAssumeExpr == ConditionExpr;
+ bool BothFeasible = (DidEagerlyAssume || (StTrue && StFalse)) &&
+ builder.isFeasible(true) && builder.isFeasible(false);
+
// Process the true branch.
if (builder.isFeasible(true)) {
- if (StTrue)
+ if (StTrue) {
+ if (BothFeasible && IterationsFinishedInLoop &&
+ *IterationsFinishedInLoop >= 2) {
+ // When programmers write a loop, they imply that at least two
+ // iterations are possible (otherwise they would just write an `if`),
+ // but the third iteration is not implied: there are situations where
+ // the programmer knows that there won't be a third iteration (e.g.
+ // they iterate over a structure that has <= 2 elements) but this is
+ // not marked in the source code.
+ // Checkers may use this heuristic mark to discard results found on
+ // branches that contain this "weak" assumption.
+ StTrue = recordWeakLoopAssumption(StTrue);
+ }
builder.generateNode(StTrue, true, PredN);
- else
+ } else {
builder.markInfeasible(true);
+ }
}
// Process the false branch.
if (builder.isFeasible(false)) {
- if (StFalse)
+ if (StFalse) {
+ if (BothFeasible && IterationsFinishedInLoop &&
+ *IterationsFinishedInLoop == 0) {
----------------
isuckatcs wrote:
```suggestion
if (BothFeasible && IterationsFinishedInLoop.value_or(1) == 0) {
```
https://github.com/llvm/llvm-project/pull/109804
_______________________________________________
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
