<div dir="ltr">Hi Dan, <br><div class="gmail_extra"><br><div class="gmail_quote">On Tue, Feb 9, 2016 at 10:57 AM, Dan Liew <span dir="ltr"><<a href="mailto:dan@su-root.co.uk" target="_blank">dan@su-root.co.uk</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">Hi,<br>
<br>
# TL;DR<br>
<br>
I've been building an application with and without the address<br>
sanitizer (with gcc 5.3 and clang 3.7.1) and I've observed that the<br>
application's behaviour changes (assertion hit/ not hit). I'm<br>
wondering if this could be a bug in address sanitizer or if the<br>
application I'm running is just buggy (e.g. doing bad things like<br>
relying on memory layout, etc.). I'm also observing ASan reporting a<br>
heap-use-after-free which Valgrind is not reporting, which makes me<br>
wonder if it is a false positive.<br></blockquote><div><br></div><div>Let us start from this heap-use-after-free report. The one in <a href="https://github.com/Z3Prover/z3/issues/436">https://github.com/Z3Prover/z3/issues/436</a> looks legitimate. </div><div>Unless the application does something extremely weird and tricky, heap-use-after-free reports are usually true positives. </div><div><br></div><div>Can you somehow verify that this heap-use-after-free is happening? </div>E.g. print all the pointer values coming from memory::allocate, coming into memory::deallocate, and coming into sat::clause::operator[]</div><div class="gmail_quote"><br></div><div class="gmail_quote">If curious, check what size of quarantine is required to catch this bug (ASAN_OPTIONS=quarantine_size_mb=N, default=256)</div><div class="gmail_quote">Valgrind may have smaller default quarantine and thus misses this bug. <br><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">
<br>
Any hints on how I might determine this? Building with UBSan doesn't<br>
turn up anything.<br></blockquote><div><br></div><div>Does the application have threads? (If yes, did you run with TSan?)</div><div>Is it valgrind-clean? </div><div>Did you try msan? </div><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">
<br>
# Longer version (if you are interested in the specific details)<br>
<br>
The application of interest is the Z3 constraint solver [1].<br></blockquote><div><br></div><div>Yay! </div><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">
<br>
Much of what I'm going to say is covered in [2] which is a bug report<br>
I opened (including a heap-use-after-free AddressSanitizer finds, I'm<br>
not sure if this a false positive or not) but here are the basics of<br>
what I found.<br>
<br>
Build Z3 as follows<br>
<br>
```<br>
git clone <a href="https://github.com/Z3Prover/z3.git" rel="noreferrer" target="_blank">https://github.com/Z3Prover/z3.git</a><br>
cd z3<br>
<br>
# Now apply the attached patch.<br>
# Basically this makes it so that in ``examples/c/test_capi.c``<br>
# the main() function only calls two functions.<br>
# Note if you build without the patch when running ``c_example``<br>
program AddressSanitizer<br>
# reports a heap-use-after-free. I'm not sure if this a false positive<br>
or not. Valgrind doesn't<br>
# seem to think there's a problem.<br>
<br>
# Build with ASan, Assertion will be hit when running the example<br>
CXX=clang++ CC=clang CXXFLAGS="-fno-omit-frame-pointer<br>
-fsanitize=address" LDFLAGS="-fsanitize=address" python<br>
scripts/mk_make.py --debug --noomp --build build_asan<br>
cd build_asan<br>
make<br>
make c_examples<br>
LD_LIBRARY_PATH=`pwd` ./c_example<br>
...<br>
ASSERTION VIOLATION<br>
File: ../src/sat/sat_clause.h<br>
Line: 59<br>
<br>
# Now build without ASan<br>
cd ../<br>
CXX=clang++ CC=clang python scripts/mk_make.py --debug --noomp --build<br>
build_noasan<br>
cd build_noasan<br>
make<br>
make c_example<br>
LD_LIBRARY_PATH=`pwd` ./c_example<br>
<br>
# No assertion is hit<br>
```<br>
<br>
Any insights/suggestions on how I could debug what I'm seeing further<br>
would be appreciated.<br>
<br>
[1] <a href="https://github.com/z3prover/z3" rel="noreferrer" target="_blank">https://github.com/z3prover/z3</a><br>
[2] <a href="https://github.com/Z3Prover/z3/issues/436" rel="noreferrer" target="_blank">https://github.com/Z3Prover/z3/issues/436</a><br>
<br>
Thanks,<br>
Dan.<br>
</blockquote></div><br></div></div>