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

_______________________________________________
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

Reply via email to