================ @@ -133,12 +195,19 @@ computeOffset(ProgramStateRef State, SValBuilder &SVB, SVal Location) { return std::nullopt; } -// TODO: once the constraint manager is smart enough to handle non simplified -// symbolic expressions remove this function. Note that this can not be used in -// the constraint manager as is, since this does not handle overflows. It is -// safe to assume, however, that memory offsets will not overflow. -// NOTE: callers of this function need to be aware of the effects of overflows -// and signed<->unsigned conversions! +// NOTE: This function is the "heart" of this checker. It simplifies +// inequalities with transformations that are valid (and very elementary) in +// pure mathematics, but become invalid if we use them in C++ number model +// where the calculations may overflow. +// Due to the overflow issues I think it's impossible (or at least not +// practical) to integrate this kind of simplification into the resolution of +// arbitrary inequalities (i.e. the code of `evalBinOp`); but this function +// produces valid results if the arguments are memory offsets which are known +// to be << SIZE_MAX. +// TODO: This algorithm should be moved to a central location where it's +// available for other checkers that need to compare memory offsets. +// NOTE: When using the results of this function, don't forget that `evalBinOp` +// uses the evaluation rules of C++, so e.g. `(size_t)123 < -1`! ---------------- NagyDonat wrote:
I'll clarify this note. https://github.com/llvm/llvm-project/pull/78315 _______________________________________________ cfe-commits mailing list cfe-commits@lists.llvm.org https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits