NoQ added a comment.
In https://reviews.llvm.org/D32642#787913, @baloghadamsoftware wrote:
> I tried `SValBuilder::evalBinOp()` first but it did not help too much. It
> could decide only if I compared the same conjured symbols or different ones,
> but nothing more. It always gave me `UnknownVal`. Even if comparing ${conj_X}
> == ${conj_X} + n where n was a concrete integer. So I have to compare the
> symbol part and the concrete integer part separately.
In any case, it's not right to have two `SValBuilder`s. Your code simplifies
symbolic expressions of numeric types, `SValBuilder` does the same thing,
there's no need to duplicate. It would be much better to move the functionality
you need (and already have implemented) directly to `SValBuilder`.
I'm sure that simplification `(($x + N) + M) ~> ($x + (M + N))` is already
working in `SValBuilder`. I think it's totally worth it to add `(($x + M) ==
($x + N)) ~> (M == N)` and `(($x + M) - ($x + N)) ~> M - N` into `SValBuilder`
in case it's not already there, because the whole analyzer would immediately
benefit from that, not just your checker.
Generally, i totally encourage you to modify the analyzer's core to fit your
purposes, even if to reduce code duplication. It's not worth it to teach the
core constraint manager how to work with user-defined types such as iterators,
but it's definitely worth it to teach `SValBuilder` how to handle numeric-type
symbols better.
In https://reviews.llvm.org/D32642#787913, @baloghadamsoftware wrote:
> If Z3 constraint solver is accepted and will be the default constraint
> manager, then I can somewhat simplify my code. That patch is under review for
> long and I am not sure whether it will be the default ever.
I don't expect Z3 to be on by default soon, however i'm only pointing to the
changes in the mainline `SValBuilder` in that patch. Z3 doesn't replace
`SValBuilder`, it only replaces the constraint manager. However, `SValBuilder`
needs to provide accurate `SVal`s to Z3, which means that a lot of
`UnknownVal`s need to go away. We're discussing if they should go away
completely even if Z3 isn't on.
In https://reviews.llvm.org/D32642#787913, @baloghadamsoftware wrote:
> Waiting is not an option for us since we are a bit delayed with this checker.
> I have to bring them out of alpha until the end of the year.
While moving things out of alpha is pretty much the primary goal of any work we
do, sacrificing quality defeats that purpose. We can only afford to enable
things by default when we know they're ready. This checker is research-heavy
and as such hard to plan. We need to understand the decisions and trade-offs
that you made.
https://reviews.llvm.org/D32642
_______________________________________________
cfe-commits mailing list
cfe-commits@lists.llvm.org
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
