<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
</head>
<body>
Yes, we should totally handle this case. I'll take a look at the
patch.<br>
<br>
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>
<br>
<div class="moz-cite-prefix">On 7/28/20 3:47 AM, Balázs Benics via
cfe-dev wrote:<br>
</div>
<blockquote type="cite"
cite="mid:CAF2=K3UmEZgwcqgrqoLZEnHGFhYTuu0m0X1fv1KM-zXTSF_TNQ@mail.gmail.com">
<meta http-equiv="content-type" content="text/html; charset=UTF-8">
<div dir="ltr">
<div>
<p>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>Formally, <strong>for all</strong> memory region <tt
class="gmail-remarkup-monospaced">X</tt> and <strong>for
all</strong> SVal offset <tt
class="gmail-remarkup-monospaced">Y</tt>:<br>
<tt class="gmail-remarkup-monospaced">&Element{SymRegion{X},Y,char}
- &SymRegion{X}</tt> => <tt
class="gmail-remarkup-monospaced">Y</tt><br>
The same for the symmetric version, but returning <tt
class="gmail-remarkup-monospaced">-Y</tt> instead.</p>
<p>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>
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>In this patch, I suppose an extension to resolve this in <a
href="https://reviews.llvm.org/D84736"
moz-do-not-send="true">https://reviews.llvm.org/D84736</a></p>
<p>Unfortunately, Phabricator patches require passing the
tests to start a discussion recently.</p>
<p>Analyzer devs, could you share your opinion on this?</p>
<p>Balazs.<br>
</p>
</div>
<div><br>
</div>
<div><br>
</div>
<div><br>
</div>
</div>
<br>
<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>
</body>
</html>