================
@@ -1224,16 +1224,33 @@ void ExprEngine::VisitLambdaExpr(const LambdaExpr *LE,
ExplodedNode *Pred,
void ExprEngine::VisitAttributedStmt(const AttributedStmt *A,
ExplodedNode *Pred, ExplodedNodeSet &Dst)
{
+ const LocationContext *LCtx = Pred->getLocationContext();
ExplodedNodeSet CheckerPreStmt;
getCheckerManager().runCheckersForPreStmt(CheckerPreStmt, Pred, A, *this);
ExplodedNodeSet EvalSet;
- NodeBuilder Bldr(CheckerPreStmt, EvalSet, *currBldrCtx);
- for (const auto *Attr : getSpecificAttrs<CXXAssumeAttr>(A->getAttrs())) {
- for (ExplodedNode *N : CheckerPreStmt) {
- Visit(Attr->getAssumption()->IgnoreParens(), N, EvalSet);
+ for (ExplodedNode *N : CheckerPreStmt) {
+ ProgramStateRef State = N->getState();
+ for (const auto *Attr : getSpecificAttrs<CXXAssumeAttr>(A->getAttrs())) {
+ SVal AssumedVal = State->getSVal(Attr->getAssumption(), LCtx);
+ if (auto ValidAssumedVal = AssumedVal.getAs<DefinedOrUnknownSVal>()) {
+ State = State->assume(*ValidAssumedVal, true);
+ } else {
+ // The assumption expression has evaluated to UndefinedVal.
----------------
NagyDonat wrote:
> If I understand this correctly, in the past if the assume-expr was Undef, we
> just continued.
> (This is proven by the fact that we report
> [here](https://godbolt.org/z/WYrx5fd3r).)
> After this patch, we would no longer get this actually TP report, right?
Yes, in the past the value of the assume-expr was ignored by the analyzer [1],
so we just continued even if it was undef. After this patch we would no longer
get the true positive report that you linked.
> We could have 2 options here:
>
> * Have a checker that would report that the assume expr is Undef in a
> `runCheckersForPreStmt` handler, or
>
> * Skip adding the `assume true` constraint to the apparently `undef`
> assume expr.
>
>
> The latter would make sure that it behaves as if we didn't take the
> assumption into account - as if it was completely ignored. Implementations
> are allowed to ignore them.
>
> IMO approach (1) is better, and isn't that when iterating the
> `CheckerPreStmt` it would skip sink nodes?
`ExplodedNodeSet` instances (e.g. `CheckerPreStmt`) have an invariant that they
never contain sink nodes (trying to insert a sink into an exploded node set has
no effect).
> Thus would naturally imply that the assumption expr can't be Undef here?
> (assuming that the imaginary core checker reporting undef assumptions is
> enabled)?
Yes, if the imaginary undef assumption checker is enabled, the assumption expr
can't be Undef here.
I agree that (1) would be the best behavior, but I don't want to squeeze
creating a new checker into this patch. In this patch I would like to implement
some simple behavior (either sinking or skipping the undef assumption expr) and
then a follow-up commit can implement that simple core checker. (I probably
won't have time for that in the foreseeable future.)
-----
[1] There was a test where code after `[[assume(false)]];` was not reachable;
but I don't exactly why did this work. I suspect that this literal false may
have been recognized by the CFG generation logic, because I didn't see any code
in the analyzer that can see any difference between e.g. `assume(true)` and
`assume(false)`.
https://github.com/llvm/llvm-project/pull/198618
_______________________________________________
cfe-commits mailing list
[email protected]
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
