NagyDonat wrote:
> [...] we should strive to handle comparison evaluation more uniformly and
> preferably behind the API barrier of the constraint manager.
Actually this commit is a step towards the opposite direction -- it adds some
tricky workaround logic to one particular checker (and not the constraint
manager). Eventually it would be good to move this bounds checking into the
constraint manager (or a related, but separate library file) -- but it's very
hard to be clear, elegant and general in this area.
The main issue is that:
- due to the automatic conversion there is is a subtle difference between the
C/C++ `operator<` and the mathematical _"less than"_,
- so it is not entirely correct to use `evalBinOpNN` to represent and check the
preconditions of memory access,
- but we _want_ to use the same symbolic expression to represent the
comparisons expressed in the code (e.g. in an `if (idx < arraySize) {...}`
branch) and the logical preconditions (that a given value must be in bounds)
- ...because otherwise a constraint coming from the conditional expression
couldn't be used to prove the precondition.
This is why I _need_ to use this hacky "early return for the trivial cases,
then use `evalBinOpNN` in the common case" strategy.
https://github.com/llvm/llvm-project/pull/81034
_______________________________________________
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
