<div dir="ltr"><div><div>Hi!<br><br></div>This is an excellent point and it is not easy to solve. One of the reason why your original idea is hard to implement is the following. Let's look at the code snippet below:<br></div><div><span style="font-family:courier new,monospace">void f(int *p, int *q) {<br></span></div><div><span style="font-family:courier new,monospace"> int *p2 = p + 2;<br></span></div><div><span style="font-family:courier new,monospace"> if (p == q) {<br></span></div><div><span style="font-family:courier new,monospace"> // Here we learned something new about p2 as well.<br></span></div><div><span style="font-family:courier new,monospace"> // So we might need to update all the symbolic expressions and bindings, not just p.<br></span></div><div><span style="font-family:courier new,monospace"> }<br></span></div><div><span style="font-family:courier new,monospace">}<br></span><br></div><div>I think your second idea should work well, but I have no idea about the performance implications. As a starting point we could implement your second solution and do some benchmarks both performance wise and looking at the results from some open source projects to see what happens to the false positive rate.<br><br></div><div>Out of curiosity, do we have the same problems with invalidations?<br><br></div><div>I am sure Artem will have some more to add but as far as I know he is busy with WWDC this week. <br></div><div><br></div><div>Regards,<br></div><div>Gabor<br></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Tue, 4 Jun 2019 at 14:53, Ádám Balogh via cfe-dev <<a href="mailto:cfe-dev@lists.llvm.org">cfe-dev@lists.llvm.org</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">
<div lang="EN-US">
<div class="gmail-m_8770444531635733315WordSection1">
<p class="MsoNormal">Hello,<u></u><u></u></p>
<p class="MsoNormal"><u></u> <u></u></p>
<p class="MsoNormal">This is not the first time that we are facing the following problem.<u></u><u></u></p>
<p class="MsoNormal"><u></u> <u></u></p>
<p class="MsoNormal">Given a code that clears all non-sentinel elements from a circular double-linked list with sentinel element:<u></u><u></u></p>
<p class="MsoNormal"><u></u> <u></u></p>
<p class="MsoNormal">typedef struct ListNode {<u></u><u></u></p>
<p class="MsoNormal"> struct ListNode *next;<u></u><u></u></p>
<p class="MsoNormal"> struct ListNode *prev;<u></u><u></u></p>
<p class="MsoNormal"> void *data;<u></u><u></u></p>
<p class="MsoNormal">} ListNode;<u></u><u></u></p>
<p class="MsoNormal"><u></u> <u></u></p>
<p class="MsoNormal">void ListClear(ListNode *list) {<u></u><u></u></p>
<p class="MsoNormal"> while (list->next != list) {<u></u><u></u></p>
<p class="MsoNormal"> ListNode *node = list->next;<u></u><u></u></p>
<p class="MsoNormal"><u></u> <u></u></p>
<p class="MsoNormal"> node->next->prev = node->prev;<u></u><u></u></p>
<p class="MsoNormal"> node->prev->next = node->next;<u></u><u></u></p>
<p class="MsoNormal"><u></u> <u></u></p>
<p class="MsoNormal"> node->next = NULL;<u></u><u></u></p>
<p class="MsoNormal"> node->prev = NULL;<u></u><u></u></p>
<p class="MsoNormal"><u></u> <u></u></p>
<p class="MsoNormal"> free(node);<u></u><u></u></p>
<p class="MsoNormal"> }<u></u><u></u></p>
<p class="MsoNormal">}<u></u><u></u></p>
<p class="MsoNormal"><u></u> <u></u></p>
<p class="MsoNormal">unix.Malloc Use after free is reported in the second iteration of the loop for `node`.<u></u><u></u></p>
<p class="MsoNormal"><u></u> <u></u></p>
<p class="MsoNormal">This is not necessarily a false positive if analyzed top level. The function that clears the nodes of the list implicitly assumes that it is a consistent circular double-linked list with a sentinel node. However this invariant is not ensured
anywhere inside the function. It is thus not known that the `prev` pointer of the first non-sentinel node points back to the sentinel node, neither is it known that applying a `prev` and a `next` after each other in any order leads back to the original node.
Without these invariants the analyzer cannot know that after unlinking and freeing the first non-sentinel element and then taking again the first non-sentinel element is not equal to the original sentinel element. So it assumes that they are equal and used
again after freeing its memory space. Thus from the perspective of the standalone function it can be a use-after-free situation.<u></u><u></u></p>
<p class="MsoNormal"><u></u> <u></u></p>
<p class="MsoNormal">So I fixed the function by inserting assertions to ensure the invariant:<u></u><u></u></p>
<p class="MsoNormal"><u></u> <u></u></p>
<p class="MsoNormal">void ListClear(ListNode *list) {<u></u><u></u></p>
<p class="MsoNormal"> while (list->next != list) {<u></u><u></u></p>
<p class="MsoNormal"> ListNode *node = list->next;<u></u><u></u></p>
<p class="MsoNormal"><u></u> <u></u></p>
<p class="MsoNormal"> assert(node->prev == list);<u></u><u></u></p>
<p class="MsoNormal"> assert(node->next->prev == node);<u></u><u></u></p>
<p class="MsoNormal"> assert(node->prev->next == node);<u></u><u></u></p>
<p class="MsoNormal"><u></u> <u></u></p>
<p class="MsoNormal"> node->next->prev = node->prev;<u></u><u></u></p>
<p class="MsoNormal"> node->prev->next = node->next;<u></u><u></u></p>
<p class="MsoNormal"><u></u> <u></u></p>
<p class="MsoNormal"> node->next = NULL;<u></u><u></u></p>
<p class="MsoNormal"> node->prev = NULL;<u></u><u></u></p>
<p class="MsoNormal"><u></u> <u></u></p>
<p class="MsoNormal"> free(node);<u></u><u></u></p>
<p class="MsoNormal"> }<u></u><u></u></p>
<p class="MsoNormal">}<u></u><u></u></p>
<p class="MsoNormal"><u></u> <u></u></p>
<p class="MsoNormal">However, it did not help because the analyzer cannot handle equality of pointers correctly. If we have an assumption that two pointers are equal the analyzer still creates two symbolic regions and records a constraint that the symbols of
the symbolic regions are equal. Later this constraint can be used for deciding whether they are equal or not but it does not handle them as the same region. So if we change the pointer `node->prev->next` to `node->next` then `node->prev->next` is changed but
`list->next` not even if we assumed that they are the same. That is the reason the analyzer takes the freed region again in the next iteration of the loop and reports an error.<u></u><u></u></p>
<p class="MsoNormal"><u></u> <u></u></p>
<p class="MsoNormal">A strange thing is that the constraint manager rearranges the comparison of the two symbols (of the symbolic regions) to a difference without `aggressive-binary-operation-simplification` disabled. (It should not do it even if this option
is enabled since the ranges of symbolic values are not constrained to `MAX/4` of the type.)<u></u><u></u></p>
<p class="MsoNormal"><u></u> <u></u></p>
<p class="MsoNormal">The question is how to fix this. I think that if two pointers are the same, then they must point to exactly the same memory region which means exactly the same symbol if it is a symbolic region. Thus instead of assigning `$reg2` to `node->prev`
and recording whether the range of `$reg2-$reg0` is `[0..0]` the analyzer should assign `$reg0` to `node->prev` which is the region of `list`. Similarly, `node->next->prev` should not become `$reg7` where the range of `$reg7-$reg1` is `[0..0]` and `node->prev->next
` should not become `$reg11` where the range of `$reg11-$reg1` is `[0..0]` but both should become `$reg1`. This way when we unlink `node` `node->next->prev` becomes `reg0` (thus the region of `list`) and `node->prev->next` e.g. `$reg2`. This way in the next
iteration `node->next` is `$reg2` instead of the freed `$reg1` so the false warning goes away. Of course I know this is not easy to implement. If both pointers already have regions assigned then which one to chose and how to replace the other one?<u></u><u></u></p>
<p class="MsoNormal"><u></u> <u></u></p>
<p class="MsoNormal">Another solution could be iterating all the existing regions upon bindings and do the same binding to the regions equal to the affected region. (I hope I managed to express myself clearly enough here.)<u></u><u></u></p>
<p class="MsoNormal"><u></u> <u></u></p>
<p class="MsoNormal">This is an old weakness of the Analyzer which should be solved eventually because it causes false positives. A new constraint manager does not help because the problem is not there.<u></u><u></u></p>
<p class="MsoNormal"><u></u> <u></u></p>
<p class="MsoNormal">Any ideas?<u></u><u></u></p>
<p class="MsoNormal"><u></u> <u></u></p>
<p class="MsoNormal">Regards,<u></u><u></u></p>
<p class="MsoNormal"><u></u> <u></u></p>
<p class="MsoNormal"><span lang="HU">Ádám<u></u><u></u></span></p>
<p class="MsoNormal"><span lang="HU"><u></u> <u></u></span></p>
<p class="MsoNormal"><u></u> <u></u></p>
<p class="MsoNormal"><u></u> <u></u></p>
</div>
</div>
_______________________________________________<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>
</blockquote></div>