=?utf-8?q?Donát?= Nagy <[email protected]>,
=?utf-8?q?Donát?= Nagy <[email protected]>,
=?utf-8?q?Donát?= Nagy <[email protected]>,
=?utf-8?q?Donát?= Nagy <[email protected]>
Message-ID:
In-Reply-To: <llvm.org/llvm/llvm-project/pull/[email protected]>
================
@@ -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
_______________________________________________
cfe-commits mailing list
[email protected]
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
