<div dir="ltr"><br><div class="gmail_extra"><br><div class="gmail_quote">On Thu, Feb 11, 2016 at 9:08 AM, Reid Kleckner <span dir="ltr"><<a href="mailto:rnk@google.com" target="_blank">rnk@google.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-color:rgb(204,204,204);border-left-style:solid;padding-left:1ex"><div dir="ltr"><div class="gmail_extra"><div class="gmail_quote"><span class="">On Thu, Feb 11, 2016 at 5:53 AM, Dan Liew via cfe-dev <span dir="ltr"><<a href="mailto:cfe-dev@lists.llvm.org" target="_blank">cfe-dev@lists.llvm.org</a>></span> wrote:<blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-color:rgb(204,204,204);border-left-style:solid;padding-left:1ex"><span>
> Can you somehow verify that this heap-use-after-free is happening?<br>
> E.g. print all the pointer values coming from memory::allocate, coming into<br>
> memory::deallocate, and coming into sat::clause::operator[]<br>
><br>
> If curious, check what size of quarantine is required to catch this bug<br>
> (ASAN_OPTIONS=quarantine_size_mb=N, default=256)<br>
> Valgrind may have smaller default quarantine and thus misses this bug.<br>
<br>
</span>I was lazy and just told valgrind to execute the program (built by gcc<br>
without ASan) with the largest quarantine it supported.<br></blockquote><div><br></div></span><div>There are some differences between Clang and GCC, such as left-to-right vs right-to-left argument evaluation. This usually bites people who are moving unique_ptr or vector and accessing it in the same expression. Given the stack traces, I suspect that different orderings of refcount operations is what's happening here. I would suggest building Z3 with Clang without ASan and running valgrind on that.</div><span class=""><div> </div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-color:rgb(204,204,204);border-left-style:solid;padding-left:1ex">> Did you try msan?<br>
<br>
I just have and it immediately reported a problem. I took a closer<br>
look and it looks like a false positive to me.<br></blockquote></span><div>...</div><div><br></div><div>This is because your STL was not compiled with MSan. The std::ofstream constructor is provided by libstdc++, the writes are not instrumented, and MSan never sees the initialization. Unfortunately, MSan is not very useful unless you recompile your *entire* application minus glibc with msan. =/</div><div><br></div><div>It is possible to build an MSan-ified libc++ and use it if you want to keep trying, but it's involved.<br></div></div></div></div></blockquote><div>Exact steps: </div><div><a href="https://github.com/google/sanitizers/wiki/MemorySanitizerLibcxxHowTo">https://github.com/google/sanitizers/wiki/MemorySanitizerLibcxxHowTo</a> </div></div><br></div></div>