<div dir="ltr"><div>Hi,</div><div><br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div>
the existing range based constraint manager only produces constraints for certain symbols

</div></blockquote><div>You are right, our constraint manager has its limitations.</div><div><br></div><div>Right now, it can not deal with symbol comparisons like `$1 < $2` even if both `$1` and `$2` are well-constrained symbols.</div><div>Although I recently made a patch implementing such: <a href="https://reviews.llvm.org/D77792">D77792</a><br></div><div><br></div><div>There is already a huge complexity behind the range based constraint manager and we should not bloat it even further.</div><div>Probably a complete redesign would help, but there is no free lunch. You can not have both accuracy and speed.</div><div><br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div>
... generating range constraints for some C programs, in the hopes of finding potential UB for bitshift operatio</div></blockquote><div>For precise constraint modeling, you should use the Z3 based constraint manager instead of the default ranged based one.<br>You can enable that with the `-analyzer-config -analyzer-constraints=z3` flags.<br></div><div>Note that, it will introduce a <b>significant </b>runtime overhead.<br></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">Christoph Steefel via cfe-dev <<a href="mailto:cfe-dev@lists.llvm.org">cfe-dev@lists.llvm.org</a>> ezt írta (időpont: 2020. ápr. 18., Szo, 23:57):<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div dir="ltr"><div>Hello all,</div><div><br></div><div>I have been looking into generating range constraints for some C programs, in the hopes of finding potential UB for bitshift operations. However, it seems that the existing range based constraint manager only produces constraints for certain symbols. For other symbols, such as those generated by arithmetic on a range bounded symbol, I found myself needing to calculate the new range constraint myself. Is this a reasonable path forwards, or is there some existing code that does something  similar to this already?</div><div><br></div><div>I have been looking at the RangedConstraintManager, and using it's RangeSet implementation,  but I also haven't  found where the RangeSet is actually used.</div><div><br></div><div>Any help would be appreciated.</div><div><br></div><div>Best,</div><div>Christoph<br></div></div>
_______________________________________________<br>
cfe-dev mailing list<br>
<a href="mailto:cfe-dev@lists.llvm.org" target="_blank">cfe-dev@lists.llvm.org</a><br>
<a href="https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev" rel="noreferrer" target="_blank">https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev</a><br>
</blockquote></div>