NoQ added a comment.
In https://reviews.llvm.org/D31886#724796, @xazax.hun wrote:
> maybe we want to skip this kind of simplification in case of Z3?
Hmm, that depends on how would we want to use it eventually.
- If Z3 acts all alone and fires only over actual bug reports, then yeah, it
turns this simplification procedure into a dry-run no-op. However, the much
bigger performance problem would be the increased path explosion from not
removing infeasible paths early on.
- If we try to filter out infeasible paths continuously, either by employing
RangeConstraintManager as a filter, or by employing Z3 as a filter, then Z3
would anyway benefit from simpler symbolic expressions. In the worst case
("that's what Z3 would have done itself anyway), we'd, i guess, have little
effect on quality *or* performance
Generally, i've a feeling that simplifying SVals is a safe thing to do.
https://reviews.llvm.org/D31886
_______________________________________________
cfe-commits mailing list
cfe-commits@lists.llvm.org
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
