NoQ added a comment. With Z3 //constraint// manager you absolutely want your constraints to be as precise as possible. The only reason we don't add these casts is because it confuses the constraint manager a lot. With a better constraint manager we would have spared ourselves a lot of suffering in this area.
With Z3 //refutation// manager - probably same but not sure, experimental data needed. Z3 occasionally refuting correct reports is not that big of a deal; the overall picture is still much better than without refutation due to sheer numbers of eliminated false positives. Improved cast modeling will also allow it to occasionally eliminate more false positives because it's now being fed correct formulas. However most of the decisions *during* the path are still made with RangeConstraintManager, which includes deciding whether to make a state split. RangeConstraintManager fails to solve constraints => double up the remaining analysis time. Exponentially with respect to the amount of constraints it couldn't solve. We'll have to weigh that performance cost against the improved quality. > We might be able to do that by extending the Equivalence class of the > constraint map with the notion of casts of... In my previous life i once did an experiment with RangeConstraintManager in which i added truncating cast symbols but not widening cast symbols. I believe it worked fairly well but i'm not sure, i was too young to properly assess the situation. So i believe something like this might actually work but there's still a high risk of failure (behaving overall worse than before) and it won't solve the entirety of the problem anyway (for instance, it won't help us solve https://bugs.llvm.org/show_bug.cgi?id=44114 by making our SVals type-correct so that extents didn't have to be stored separately - and that's currently one of the main sources of false positives we have). Repository: rG LLVM Github Monorepo CHANGES SINCE LAST ACTION https://reviews.llvm.org/D85528/new/ https://reviews.llvm.org/D85528 _______________________________________________ cfe-commits mailing list cfe-commits@lists.llvm.org https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
