<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
</head>
<body>
<br>
<br>
<div class="moz-cite-prefix">On 7/6/20 8:53 AM, Balázs Benics via
cfe-dev wrote:<br>
</div>
<blockquote type="cite"
cite="mid:CAF2=K3Um7e=QsfLcv3-1UgOjEhv24jx3DREsyzQd6ryhK6RTig@mail.gmail.com">
<meta http-equiv="content-type" content="text/html; charset=UTF-8">
<div dir="ltr">Is it reasonable to assume in the analyzer that a
symbol representing the extent<br>
of an analyzed memory region can not be greater then
size_t_max/2?<br>
</div>
</blockquote>
<br>
I think it's pretty reasonable. Otherwise ssize_t won't work. In
fact, neither can it be equal to SIZE_MAX/2, for the same reason.
The actual limits are probably smaller, e.g. Clang won't let you
declare a fixed-length array larger than a certain size that's much
smaller than SIZE_MAX/2 (even if you are willing to find a computer
that has that much RAM).<br>
<br>
<blockquote type="cite"
cite="mid:CAF2=K3Um7e=QsfLcv3-1UgOjEhv24jx3DREsyzQd6ryhK6RTig@mail.gmail.com">
<div dir="ltr">If so, why does the constraint manager not know
about this fact?<br>
</div>
</blockquote>
<br>
It's not up to the constraint manager to decide whether or not a
specific symbol represents an extent. SymbolExtent obviously does
represent an extent, so i guess it'll be reasonable to hardcode
that. The opposite is not true though; say, the extent of heap-based
symbolic region allocated by `malloc(x)` is the completely arbitrary
symbol `$x` (it can even be a concrete value).<br>
<br>
So instead of making the constraint manager make such guesses i'd
much rather have the entities responsible for allocation
(MallocChecker, ExprEngine for operator new/new[] and VLAs, etc.)
*actively* tell the constraint manager that these symbols may only
have limited range (it doesn't need to know that this is because of
them being an extent of something, it only needs the raw facts) by
explicitly adding the respective constraints via assume().
IteratorChecker already does that for iterator position / difference
symbols and i think that's the right thing to do. Now it's entirely
up to the constraint solver to take these hints into account.<br>
<br>
<blockquote type="cite"
cite="mid:CAF2=K3Um7e=QsfLcv3-1UgOjEhv24jx3DREsyzQd6ryhK6RTig@mail.gmail.com">
<div dir="ltr">If not, why does the `ProgramState::assumeInBound`
still heavily exploit this<br>
fact in its implementation?<br>
<br>
Without deciding this Z3 refutation will not be able to filter
as many false<br>
positives as it potentially could.<br>
<br>
Regards,<br>
Balazs</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>