<html>
<head>
<base href="https://bugs.llvm.org/">
</head>
<body><table border="1" cellspacing="0" cellpadding="8">
<tr>
<th>Bug ID</th>
<td><a class="bz_bug_link
bz_status_NEW "
title="NEW - RangeConstraintManager infeasible execution path due to EquivalenceClasses"
href="https://bugs.llvm.org/show_bug.cgi?id=49490">49490</a>
</td>
</tr>
<tr>
<th>Summary</th>
<td>RangeConstraintManager infeasible execution path due to EquivalenceClasses
</td>
</tr>
<tr>
<th>Product</th>
<td>clang
</td>
</tr>
<tr>
<th>Version</th>
<td>trunk
</td>
</tr>
<tr>
<th>Hardware</th>
<td>PC
</td>
</tr>
<tr>
<th>OS</th>
<td>All
</td>
</tr>
<tr>
<th>Status</th>
<td>NEW
</td>
</tr>
<tr>
<th>Severity</th>
<td>enhancement
</td>
</tr>
<tr>
<th>Priority</th>
<td>P
</td>
</tr>
<tr>
<th>Component</th>
<td>Static Analyzer
</td>
</tr>
<tr>
<th>Assignee</th>
<td>dcoughlin@apple.com
</td>
</tr>
<tr>
<th>Reporter</th>
<td>balazs.benics@sigmatechnology.se
</td>
</tr>
<tr>
<th>CC</th>
<td>dcoughlin@apple.com, llvm-bugs@lists.llvm.org
</td>
</tr></table>
<p>
<div>
<pre>Created <span class=""><a href="attachment.cgi?id=24605" name="attach_24605" title="reproducer">attachment 24605</a> <a href="attachment.cgi?id=24605&action=edit" title="reproducer">[details]</a></span>
reproducer
RangeConstraintManager::setConstraint produces a State, where an empty RangeSet
is associated with an EquivalenceClass.
AFAIK that should never happen.
Originally, the Z3 crosscheck visitor crashed on this when it tried to
serialize the range set of a symbol.
Then I realized that this is connected to the `RangeConstraintManager`,
constructing an infeasible execution path.
I attach the trimmed exploded graph segment, where the first state appears with
the empty range-set.
You can add the required assertions to diagnose it by applying the attached
`add-sanity-check-assertions.patch` patch file on top of
b9f169fb7dcd09721a4487801873a61a1e20da7e (current trunk).
It will check if the State returned by `RangeConstraintManager::setConstraint`
has no empty range sets associated with any EquivalenceClasses.
Then run the analysis on the attached code:
./bin/clang --analyze -Xclang -analyzer-display-progress -Xclang
-analyze-function="bar()" -Xclang
-analyzer-checker=core,alpha.security.ArrayBound MemorySSA-preprocessed.cpp
I would fix this myself, but I'm quite busy right now.</pre>
</div>
</p>
<hr>
<span>You are receiving this mail because:</span>
<ul>
<li>You are on the CC list for the bug.</li>
</ul>
</body>
</html>