[cfe-dev] Buildling with/without AddressSanitizer causes divergent execution behaviour

[Dan Liew via cfe-dev]

Hi,

Well I dug into Z3's codebase a little more and figured out what the
problem was. If you're curious see [1].

What worries me more is that prior to a heap-use-after-free being
reported there an out of bounds write occurs but ASan doesn't catch it
which seems like a bug to me. Note I'm using Clang 3.7.1

Here's how to reproduce (you need to build this on Linux on a x86_64 machine)

```
git clone -b asan_miss_out_of_bounds https://github.com/delcypher/z3-1.git src
cd src
CXX=clang++ CC=clang CXXFLAGS="-fno-omit-frame-pointer
-fsanitize=address" LDFLAGS="-fsanitize=address" python
scripts/mk_make.py --build build_clang_asan --noomp --debug
cd build_clang_asan
make -j4
make c_example
LD_LIBRARY_PATH=`pwd` ./c_example
```

You should see output like

```
...
About to do out of bounds access!
Did out of bounds access! If doing an ASan build do I get printed?
=================================================================
==12965==ERROR: AddressSanitizer: heap-use-after-free on address
0x60400005fe54 at pc 0x7f228dcad7a9 bp 0x7ffda15af250 sp
0x7ffda15af248
...
```

In this version of Z3 I've added (see [2]) some printf statements that
print a message just before doing an out of bounds write (``About to
do out of bounds access!``) and then prints a message after doing it
(``Did out of bounds access! If doing an ASan build do I get
printed?``). If ASan were to catch the out of bounds access I would
not expect the second message to be printed. However the second
message gets printed and program continues running and later hits a
heap-use-after-free.

This seems like a bug to me. Thoughts?


[1] https://github.com/Z3Prover/z3/issues/436#issuecomment-184713859
[2] https://github.com/delcypher/z3-1/commit/cc60cd483039af78604401abac703d9a903f74b6

Thanks,
Dan.