balazske added a comment. In D72705#1859157 <https://reviews.llvm.org/D72705#1859157>, @Szelethus wrote:
> In D72705#1838324 <https://reviews.llvm.org/D72705#1838324>, @balazske wrote: > > > I am still unsure about how this checker works if the function to check is > > "modeled" or evaluated by another checker. Then the function may have > > already a constrained value at the PostCall event (for example if a > > `malloc` fails) and the basic idea of this checker that the constraints on > > the return value indicate the checks that the program makes does not work. > > So it may be better to check for the initial constraint somehow and if > > found ignore that function. Or create a new state where the function call's > > value is not constrained. > > > Under evaluation, you mean `evalCall()`? Could you please detail what your > worry is, and what the essence of the current solution is? This comment applies to a previous solution for the problem. In that case the checker worked by testing the constraints that are put on the "return value". The "return value" is the `SymbolRef` that comes from the function call return value. The main idea was that initially this value is unconstrained, then the conditions in the evaluated code generate constraints for it. By checking these constraints it is possible to reason about the conditions that were applied in the code to the value. And find out if a specific condition was applied, the one that means that the value was checked for error code. int X = f(); // X is not constrained if (X) { // X is constrained to non-zero } else { // X is constrained to zero } The constraints accumulate during an execution path and at a time the required state is reached (or not). In this example code we know at the end that `X` was checked for "nullness" (it can be either only zero or anything except zero). This was the first idea but does not work always correct and requires too exact error checking in the evaluated code. In a next solution the searched constraint was only that the return value should be constrained to outside of the error return range. Basically a single execution path with this condition was searched. (In the simple code above, search for one execution path where `X` is for sure not zero at the end.) This solution has problems too. So the whole way of this constraint-based search was abandoned. The comment is about if initially the symbol for called function (`f` in the code above) is constrained. For example a postCall put constraints on it if it is known that the returned value is always non-negative. Or more worse, an error path is generated when the return value is exactly the error return code. In the mentioned case if the `f` function is modeled and a path is added where it has return value zero the checker will "think" that there was an `if (X == 0)` condition in the code. Repository: rG LLVM Github Monorepo CHANGES SINCE LAST ACTION https://reviews.llvm.org/D72705/new/ https://reviews.llvm.org/D72705 _______________________________________________ cfe-commits mailing list cfe-commits@lists.llvm.org https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
