[analyzer] Why use `checkPostCall()` to model the function semantics in `StdLibraryFunctionsChecker.cpp`?

Hi all,

StdLibraryFunctionsChecker.cpp is a very useful and great tool to improve the modeling of library function. But I can’t figure out why use checkPostCall() to model the function samantic.

What puzzles me is the order of API calls. For example, if we want to make some checks on getline() in CheckerA, and use checkPostCall() to collect information or set ProgramState, the checkPostCall() of CheckerA is likely to be behind the checkPostCall() of StdLibraryFunctionsChecker.cpp. At this point, CheckerA does not use the model information of getline() in StdLibraryFunctionsChecker.cpp. So what is the original intention of using checkPostCall() to play the key role in modeling?

And I want to know what plans community have for StdLibraryFunctionsChecker.cpp in the future, for example, extend it to handle more complex library functions?

Thanks in advance!

Henry Wong
Qihoo 360 Codesafe Team

StdLibraryFunctionsChecker uses evalCall for most calls it models. It uses checkPostCall only for few functions for which it models so little about the function that it’s unlikely to ever be a problem for other checkers that may eventually want to model the function exactly. The checker’s original intent was to cut away infeasible paths in the program, eg. preventing analysis of paths on which getline() is assumed to return -2. It is indeed a problem that other checkers are not able to reliably access this information immediately in their own checkPostCall, but currently there are no checkers that are actively relying on that. There are also discussions about introducing a system of dependencies between checkers so that dependent checkers automatically turned on checkers on which they depend and have their callbacks fire in a specific order, which could probably be already hacked up by writing weird registerChecker() functions that register dependencies first.

There are currently at least 4 different ways the analyzer can model a function:

  1. Conservative evaluation (normal analyzer behavior when body of the function is unavailable).
  2. Inlining (model the function precisely by jumping into it and proceeding with normal analysis inside it).
    (1. and 2. will be collectively referred to as “default evaluation”.)
  3. Body farm (provide a simplified synthetic AST for the function body and then inline it).
  4. evalCall() in checker (let a checker manipulate the program state manually to model arbitrary effects of the function).

Additionally, any checker may influence the analysis at almost any point, which should be used carefully. For instance, splitting the path or cutting away a path that seems infeasible is fine (as long as it is the desired behavior), replacing a value of an expression with a different value is bad.

When body farms were introduced, they seemed to be a great way of modeling library functions, and they are fairly effective for the few functions they were used for. But later a lot of functions turned out to be problematic to model that way - either because their simplified AST is too complicated to synthesize correctly (eg. std::call_once turned out to be extremely painful because we had to write down AST for template instantiations manually node-by-node without being able to rely on the compiler to help us with that) or because a good synthetic AST will not be understood by the analyzer anyway. StdLibraryFunctionsChecker is modeling some functions that fall to the latter category. You should be able to find further explanation of why they are hard to body-farm in the checker’s comments.

The difference between evalCall and checkPostCall is that evalCall overrides the default evaluation. If a checker does evalCall(), the function will never be inlined or invalidate potentially accessible memory. The checker will also need to come up with a good representation of the return value and will have a chance to specify it. If two different checkers try to evalCall() the same call, the analyzer will defensively crash.

StdLibraryFunctionsChecker uses evalCall for modeling calls that it can model exactly.

It also uses checkPostCall for stuff that it can’t model exactly, but for the lack of better modeling it can still model a few things that are safe to model in post-call, in addition to the effects of default evaluation. For example, it doesn’t model the string (or even the length of the string) produced by getline() but it does know that this function never returns -2, so it cuts away the respective paths. If getline() is inlined or a different checker models it in evalCall or even in checkPostCall, StdLibraryFunctionsChecker will still work correctly, because, well, whatever the other modeling does, it shouldn’t make getline() return -2. It might happen that another checker substitutes the return value in PostCall leading to a race, but that’s the exact reason why substituting expression values after the expression is evaluated is a bad idea anywhere in the analyzer.

StdLibraryFunctionsChecker uses a custom system of function summaries which is relatively extensible but not super flexible. It should probably not used for modeling everything. In fact, i doubt it’d be easy to extend it to reliably model anything but range constraints. Side effects like “this function writes its 1st argument to memory pointed to by its 2nd argument” are already pretty unpleasant to summarize declaratively; add a couple of levels of pointer indirection and it’d be a nightmare.

So, adding more functions and side effect variants similar to what’s already there is welcome. I’m moderately curious about how far this summary system can be pushed, but reliability comes first. Trying to model every function this way is not a great idea.

+cfe-dev You won’t be able to move that logic because not all functions should be modeled via evalCall(). You may duplicate the logic in evalCall() so that state split happened earlier for functions that are modeled with evalCall(), but i’m still interested in seeing a motivation for such change. There’s only one correct way to make a state split, and such state split is pretty much idempotent.