[clang] [clang-tools-extra] [analyzer][clang-tidy][NFC] Clean up eagerly-assume handling (PR #112209)
via cfe-commits
cfe-commits at lists.llvm.org
Tue Oct 15 05:57:30 PDT 2024
=?utf-8?q?Donát?= Nagy <donat.nagy at ericsson.com>,
=?utf-8?q?Donát?= Nagy <donat.nagy at ericsson.com>,
=?utf-8?q?Donát?= Nagy <donat.nagy at ericsson.com>,
=?utf-8?q?Donát?= Nagy <donat.nagy at ericsson.com>
Message-ID:
In-Reply-To: <llvm.org/llvm/llvm-project/pull/112209 at github.com>
================
@@ -3767,28 +3764,26 @@ void ExprEngine::evalEagerlyAssumeBinOpBifurcation(ExplodedNodeSet &Dst,
continue;
}
- ProgramStateRef state = Pred->getState();
- SVal V = state->getSVal(Ex, Pred->getLocationContext());
+ ProgramStateRef State = Pred->getState();
+ SVal V = State->getSVal(Ex, Pred->getLocationContext());
std::optional<nonloc::SymbolVal> SEV = V.getAs<nonloc::SymbolVal>();
if (SEV && SEV->isExpression()) {
- const std::pair<const ProgramPointTag *, const ProgramPointTag*> &tags =
- geteagerlyAssumeBinOpBifurcationTags();
+ auto [TrueTag, FalseTag] = getEagerlyAssumeBifurcationTags();
- ProgramStateRef StateTrue, StateFalse;
- std::tie(StateTrue, StateFalse) = state->assume(*SEV);
+ auto [StateTrue, StateFalse] = State->assume(*SEV);
// First assume that the condition is true.
if (StateTrue) {
SVal Val = svalBuilder.makeIntVal(1U, Ex->getType());
StateTrue = StateTrue->BindExpr(Ex, Pred->getLocationContext(), Val);
- Bldr.generateNode(Ex, Pred, StateTrue, tags.first);
+ Bldr.generateNode(Ex, Pred, StateTrue, TrueTag);
}
// Next, assume that the condition is false.
if (StateFalse) {
SVal Val = svalBuilder.makeIntVal(0U, Ex->getType());
StateFalse = StateFalse->BindExpr(Ex, Pred->getLocationContext(), Val);
- Bldr.generateNode(Ex, Pred, StateFalse, tags.second);
+ Bldr.generateNode(Ex, Pred, StateFalse, FalseTag);
----------------
isuckatcs wrote:
I don't think that passing the tag here is an issue. The process for creating the node is "eager assumption" and in this case it only creates one branch.
The tags in the egraph tell the user how the analyzer reached the conclusion to create that node and they are also useful for serving logging/debugging purposes. For example if the egraph is wrong at the node with this tag, you immediately know where the issue is. If there is no tag and the analyzer only creates one branch, it might be difficult to figure out where the node was created.
The only issue might be the wording, which says "Eagerly Assume" even though the analyzer _knows_ the value of the condition, but once again the creation of the node is the result of "eager assumption", so I guess it's fine to leave it like this.
https://github.com/llvm/llvm-project/pull/112209
More information about the cfe-commits
mailing list