<html><head><meta http-equiv="Content-Type" content="text/html; charset=utf-8"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class=""><blockquote type="cite" class=""><div class="">...only base regions and raw offsets are truly material.</div></blockquote><div class=""><br class=""></div>I strongly agree with this statement and believe that the analysis should operate <b class="">only</b> in these terms. However, for a better experience of us (the analyzer developers), I would still leave ElementRegion or FieldRegion as a very thin layer over base + offset for debugging purposes.<br class=""><div><br class=""><blockquote type="cite" class=""><div class="">On 28 Jul 2020, at 22:38, Artem Dergachev via cfe-dev <<a href="mailto:cfe-dev@lists.llvm.org" class="">cfe-dev@lists.llvm.org</a>> wrote:</div><br class="Apple-interchange-newline"><div class="">
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8" class="">
<div class="">
Yes, we should totally handle this case. I'll take a look at the
patch.<br class="">
<br class="">
The bigger picture here is that ElementRegion is on its own a fairly
annoying fundamental bug in our region hierarchy
(<a class="moz-txt-link-freetext" href="https://bugs.llvm.org/show_bug.cgi?id=43364">https://bugs.llvm.org/show_bug.cgi?id=43364</a>). I ultimately prefer
to solve this by eliminating ElementRegion, FieldRegion, etc.,
entirely; only base regions and raw offsets are truly material.<br class="">
<br class="">
<div class="moz-cite-prefix">On 7/28/20 3:47 AM, Balázs Benics via
cfe-dev wrote:<br class="">
</div>
<blockquote type="cite" cite="mid:CAF2=K3UmEZgwcqgrqoLZEnHGFhYTuu0m0X1fv1KM-zXTSF_TNQ@mail.gmail.com" class="">
<meta http-equiv="content-type" content="text/html; charset=UTF-8" class="">
<div dir="ltr" class="">
<div class=""><p class="">Currently, if the analyzer evaluates an expression like <tt class="gmail-remarkup-monospaced">to - from</tt>, it only
computes reasonable answer if both are representing
ElementRegions.</p><p class="">Formally, <strong class="">for all</strong> memory region <tt class="gmail-remarkup-monospaced">X</tt> and <strong class="">for
all</strong> SVal offset <tt class="gmail-remarkup-monospaced">Y</tt>:<br class="">
<tt class="gmail-remarkup-monospaced">&Element{SymRegion{X},Y,char}
- &SymRegion{X}</tt> => <tt class="gmail-remarkup-monospaced">Y</tt><br class="">
The same for the symmetric version, but returning <tt class="gmail-remarkup-monospaced">-Y</tt> instead.</p><p class="">I'm curious why don't we handle the case, when only one of
the operands is an <tt class="gmail-remarkup-monospaced">ElementRegion</tt>
and the other is a plain <tt class="gmail-remarkup-monospaced">SymbolicRegion</tt>.<br class="">
IMO if the super memory region of the ElementRegion is the
same as the SymbolicRegion then we can still return a
reasonable answer.</p><p class="">In this patch, I suppose an extension to resolve this in <a href="https://reviews.llvm.org/D84736" moz-do-not-send="true" class="">https://reviews.llvm.org/D84736</a></p><p class="">Unfortunately, Phabricator patches require passing the
tests to start a discussion recently.</p><p class="">Analyzer devs, could you share your opinion on this?</p><p class="">Balazs.<br class="">
</p>
</div>
<div class=""><br class="">
</div>
<div class=""><br class="">
</div>
<div class=""><br class="">
</div>
</div>
<br class="">
<fieldset class="mimeAttachmentHeader"></fieldset>
<pre class="moz-quote-pre" wrap="">_______________________________________________
cfe-dev mailing list
<a class="moz-txt-link-abbreviated" href="mailto:cfe-dev@lists.llvm.org">cfe-dev@lists.llvm.org</a>
<a class="moz-txt-link-freetext" href="https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev">https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev</a>
</pre>
</blockquote>
<br class="">
</div>
_______________________________________________<br class="">cfe-dev mailing list<br class=""><a href="mailto:cfe-dev@lists.llvm.org" class="">cfe-dev@lists.llvm.org</a><br class="">https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev<br class=""></div></blockquote></div><br class=""></body></html>