vinay-deshmukh wrote:
> I was thinking about the case, and I think it's okay to have state-splits in
> the subexpressions coming from an assume expression - given that the assume
> expression has no side effects. This way we should have 2 paths after the
> assume expression (but still before the first if statement).
>
> 1. where `a > 10` is true
> 2. where `a > 10` is false, aka. `a <= 10`.
>
> This is I think the current behavior of your proposed implementation. Could
> you demonstrate it in tests?
>
> Something like this should prove it:
>
> ```c++
> int ternary_in_assume(int a, int b) {
> [[assume(a > 10 ? b == 4 : b == 10)]];
> clang_analyzer_value(a); // we should have 2 dumps here.
> clang_analyzer_dump(b); // This should be either 4 or 10.
> if (a > 20) {
> clang_analyzer_dump(b + 100); // expecting 104
> return;
> }
> if (a > 10) {
> clang_analyzer_dump(b + 200); // expecting 204
> return;
> }
> clang_analyzer_dump(b + 300); // expecting 310
> }
> ```
Summary for the latest commit:
In the current implementation, when we run `clang_analyzer_dump`, it prints
the actual constrained values (i.e. `b == 4` or `b == 10`), but it will
**also** print `reg_$2<int b>`. As far as I can tell, this is exactly how it
works for the `__builtin_assume` as well, except the difference is that when
`core.BuiltinChecker` is run, it will eliminate the `ExplodedNode`(s) where the
expression is false / "unconstrained".
To pass the tests for now, I've added a `FIXME` that also "expects" the
symbolic print as follows so `lit` tests "pass" :
```c++
clang_analyzer_dump(b + 100); // expected-warning{{104}} FIXME:
expected-warning{{(reg_$2<int b>) + 100}}
```
As far as I know, to eliminate the warning emitted corresponding to the FIXME
comment, we need to implement a new Checker for attributes; we can do this in a
second PR to avoid scope creep for this issue/PR.
P.S. I needed to add a check to `ExprEngine::VisitGuardedExpr` to "continue" if
the ProgramPoint is a `StmtPoint`, because without it, the `getAs<BlockEdge>`
runs into undefined behavior. Added an `assert` for that as well to be careful
in the future.
https://github.com/llvm/llvm-project/blob/eabbef2be6a4f956171a21632d8cf07b4a48e162/clang/lib/StaticAnalyzer/Core/ExprEngineC.cpp#L799-L810
now working on getting the tests to pass locally, might need some more minor
fixes.
https://github.com/llvm/llvm-project/pull/116462
_______________________________________________
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
