<div dir="ltr"><div>Oh, I see. Unfortunate :|<br>You probably remember our previous conversation (<a href="http://lists.llvm.org/pipermail/cfe-dev/2020-March/064881.html" target="_blank">[analyzer] Constrain the size of unknown memory</a>) where you proposed to use assert with the `<span style="font-family:monospace">clang_analyzer_getExtent</span>` to make constraints on the size of the allocated memory region.</div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div><pre>ANALYZER_ASSERT(ANALYZER_EXTENT(buff) == size);</pre></div></blockquote><div><br></div><div><br></div><div>According to the Bugzilla tickets you linked, this is the limitation of our constraint solver.<br></div><div>Even though the constraint solver has its limitations, we are not planning to improve it, since that would be like a reimplementation of a SAT solver.<br></div><div>But we won't use Z3 as a constraint solver either, because that would be really really slow. (AFAIK Z3 is only used for refutation if enabled)<br><br></div><div>It seems to be a dead-end to me, regarding that without Z3 like solver we are not strong enough, and with it unbelievably slow.<br></div>If a general solution would be too complex, should we consider handling only the easy cases as I mentioned?<br><div><br></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">Artem Dergachev <<a href="mailto:noqnoqneo@gmail.com" target="_blank">noqnoqneo@gmail.com</a>> ezt írta (időpont: 2020. márc. 25., Sze, 16:25):<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">Basically <a href="https://bugs.llvm.org/show_bug.cgi?id=40145" rel="noreferrer" target="_blank">https://bugs.llvm.org/show_bug.cgi?id=40145</a>.<br>
<br>
On 3/25/20 4:20 PM, Balázs Benics via cfe-dev wrote:<br>
> Why cannot prove analyzer that only the true case is feasible for the <br>
> following example?<br>
> ```<br>
> ProgramStateRef StInBound  = state->assumeInBound(Idx, Size, true);<br>
> ProgramStateRef StOutBound = state->assumeInBound(Idx, Size, false);<br>
> ```<br>
><br>
> Given that we know:<br>
> SVals:<br>
>   Idx.dump():  (conj_$8{int, LC1, S2294, #1}) - 1U<br>
>   Size.dump(): extent_$5{SymRegion{reg_$4<char * dst>}}<br>
><br>
> Range constraints according to the exploded graph nodes:<br>
> extent_$5{SymRegion{reg_$4<char * dst>}}  {[10,18446...]}<br>
>   conj_$8{int, LC1, S2294, #1}              {[1,9]}<br>
><br>
> Does the `Idx < Size` hold for all possible values of `Idx` and `Size`?<br>
> IMO yes, since [0-8] < [10,18446...], but the analyzer returns <br>
> _non-null_ states for both of the `assumeInBound` calls, but why?<br>
><br>
> Balazs<br>
><br>
> _______________________________________________<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>
<br>
</blockquote></div>