[PATCH] D103096: [analyzer] Implement cast for ranges of symbolic integers.

Fri Jun 4 00:51:12 PDT 2021

steakhal added a comment.

There is so much fancy stuff going on upstream. Awesome to see.
I'm trying to catch up ASAP, I'm finally done with my master's thesis.

In D103096#2798238 <https://reviews.llvm.org/D103096#2798238>, @NoQ wrote:

> Additionally, presence of cast symbols is extremely valuable for z3 runs in which our concerns for increased complexity are eliminated.

You are probably referring to D85528 <https://reviews.llvm.org/D85528>. (Without that patch, Z3 refutation crashes all over the place due to the //not// modeled widening/narrowing casts.)

>>> But this still requires //massive// testing, a lot more than a typical constraint solver patch; extraordinary claims require extraordinary evidence.
>>
>> What kind of tests do you think we need?
>
> Test on a lot of real-world code. Like, seriously, *A LOT* of real-world code. Say, 20x the amount of code we have in docker and csa-testbench, from a large variety of projects. Investigate newly appeared reports carefully to understand the impact. I'll be happy to help with this at some point.

The CSA-testbench is capable of using the Conan package manager.
By cloning the https://github.com/conan-io/conan-center-index you can get a bunch of Conan package recipes, with tests actually using the given library.
Running their tests would ensure that header-only libraries get analyzed as well as //normal// libraries. However, frequently used packages would be analyzed over and over again, similarly to how headers suffer from this.

We planned to make use of this in the future to make CTU analysis and Z3 refutation more and more robust.
As soon as we have the infrastructure and scale, we plan to enable a small set of contributors of initiating such measurements, but don't expect it in the close future.

Repository:
  rG LLVM Github Monorepo

CHANGES SINCE LAST ACTION
  https://reviews.llvm.org/D103096/new/

https://reviews.llvm.org/D103096