Roadmap of modeling symbolic cast operations

Clang Frontend Static Analyzer
1

There are many false positives because of the lack of modeling explicit or
implicit cast operations. Currently, we are in the middle of a transition to
support cast operations.

In the static analyzer, we associate a symbol for any symbolic expression.
A symbol is represented by the class hierarchy with the base class SymExpr,
this is somewhat similar to the AST. For example, a binary operator is
represented as a SymSymExpr that holds a pointer to both the LHS and the RHS.
In order to model a cast operation,

  • we have to emit a SymbolCast into the symbol tree (1)
  • the analyzer engine together with the underlying constraint solver must
    process the SymbolCast nodes of the symbol tree (2).

Since Denys’ initial patch, we can emit the symbolic cast operations into the
symbol tree. This supposed to fulfill point (1), but we emit the SymbolCast
only if the support-symbolic-integer-casts option is set to true and that
is false now by default. Our goal is to set this option to true by default.
If we do that now, then there are 27 lit test cases that fail. There are
trivial failures, e.g. the dump of an SVal has changed, or we have to provide
an overload of the clang_analyzer_* debug functions. I am proposing to have
two RUN lines for the failing lit tests, one for the legacy behavior and one
for the new behavior. I.e. one for support-symbolic-integer-casts=false and one
for support-symbolic-integer-casts=true. There might be differences in the
evaluation of clang_analyzer_eval calls. We should document the reasons of
these differences and we should add a FIXME if needed about hints for the
solution. Probably, most of these will be fixed only once point (2) is
addressed in ⚙ D103096 [analyzer] Implement cast for ranges of symbolic integers.

At some point in the future, we may consider the support so stable that we
could remove the mentioned option. That would be the time to remove the legacy
RUN lines with support-symbolic-integer-casts=false.

I am about to start this process and create new patches for the failing lit tests
with the mentioned duplicated RUN lines.

2

@ASDenysPetrov, @vbridgers, @NoQ, @steakhal FYI

3

Forgot to mention an other really important motivation: Z3 refutation often crashes because of the lack of handling of casts.

4

There are
trivial failures, e.g. the dump of an SVal has changed, or we have to provide
an overload of the clang_analyzer_* debug functions.

Could you please annotate it with an example?

Btw the RFC looks good to me, but we’ve talked about this downstream a couple times.

5

Sure. Here they are:

6

I’m somewhat worried that a lot of new warnings found due to improved precision will be hard to understand, and a lot of new paths may be infeasible in practice. I.e., if the programmer puts a string size into an int variable, we can totally explore the path where the size is truncated this way, but:

  • Do we really know that this specific string can really be that long? How often can it be that long? Does the programmer care about that?
  • If we actually know that this specific string can be that long, do we have a way to explain to the user that the truncation occurs on the current path and what are the consequences?

So I’m curious if you have plans to address these problems, eg. make more bug visitors / path notes to explain what’s going on and possibly suppress bug reports that rely on eg. different casts assumed in different directions (which may be technically possible but unlikely in practice)?

7

I see your point. However, currently we face the exact same issue, but reversed. Consider e.g.

static_assert(sizeof(short) == 2, "");
static_assert(sizeof(long) == 8, "");
void test(short k) {
  ++k;
  assert(k == 1);
  (long)k << 16; // FP warning
}

where we cannot explain how can the result of the left-shift be unrepresentable as long.

Yeah it is a good idea. But, I guess, this should be an orthogonal improvement from the cast modeling. See the example above, where we already fail to explain a value range.
Also, I am wondering maybe we should approach this from a more general viewpoint. Ideally, we should emit a note if an (interesting) SVal is getting constrained, i.e when the associated RangeSet (or a binding in the store) changes. We do emit a note already for all SVals if they are constrained in a condition. Perhaps we could extend this to interesting values that had been casted.

8

Yeah, I totally understand the motivation, what I’m trying to say is, last time I tried this, there were a lot more false positives / unactionable warnings introduced than fixed. Some of that was due to constraint solver unable to handle the increased amount of symbols but some were just that - unlikely scenarios that were also poorly explained.

So I’m trying to avoid making things worse on average, because users don’t care whether the issues are orthogonal or not (I absolutely agree they are), they see unactionable warnings => they become frustrated.

Ideally, we should emit a note if an (interesting) SVal is getting constrained, i.e when the associated RangeSet (or a binding in the store) changes.

Yeah, totally, we should at the very least emit a note when constrains become sufficient to conclude that the bug has occured, for any reason. Then, separately, we could add more notes to explain individual constraints that contributed to non-buggy state being unsatisfiable; we could put unprunable notes at the moments when these constraints were introduced.

9

Okay, sounds good. I’ll try to find some time (or someone) to look into this.