WIP: Z3builder

[rsas]

This is my WIP pull request to replace KLEEBuilder with Z3 library for building SMT-LIB v2 expressions (enabled per default at the moment). Some tests are still failing requiring some investigation why. Also, after the integration of Alive backend, I cannot build it anymore, because cmake is complaining.

[googlebot]

We found a Contributor License Agreement for you (the sender of this pull request), but were unable to find agreements for all the commit author(s) or Co-authors. If you authored these, maybe you used a different email address in the git commits than was used to sign the CLA (login here to double check)? If these were authored by someone else, then they will need to sign a CLA as well, and confirm that they're okay with these being contributed to Google.
In order to pass this check, please resolve this problem and have the pull request author add another comment and the bot will run again. If the bot doesn't comment, it means it doesn't think anything has changed.

[manasij7479]

Thanks, I'll take a look at the cmake issue.

[regehr]

Raimondas, can you elaborate about the build issues? Did you do a full build_deps.sh?

[rsas]

cmake of Alive fails to find z3 (which is not built at the time), there was no issue before the integration of Alive.

[regehr]

please paste the actual output

[rsas]

$ ./build_deps.sh 
Cloning into 'third_party/alive2/alive2'...
remote: Enumerating objects: 6, done.
remote: Counting objects: 100% (6/6), done.
remote: Compressing objects: 100% (6/6), done.
remote: Total 825 (delta 0), reused 2 (delta 0), pack-reused 819
Receiving objects: 100% (825/825), 212.16 KiB | 588.00 KiB/s, done.
Resolving deltas: 100% (548/548), done.
-- The C compiler identification is AppleClang 10.0.0.10001145
-- The CXX compiler identification is AppleClang 10.0.0.10001145
-- Check for working C compiler: /Applications/Xcode.app/Contents/Developer/Toolchains/XcodeDefault.xctoolchain/usr/bin/cc
-- Check for working C compiler: /Applications/Xcode.app/Contents/Developer/Toolchains/XcodeDefault.xctoolchain/usr/bin/cc -- works
-- Detecting C compiler ABI info
-- Detecting C compiler ABI info - done
-- Detecting C compile features
-- Detecting C compile features - done
-- Check for working CXX compiler: /Applications/Xcode.app/Contents/Developer/Toolchains/XcodeDefault.xctoolchain/usr/bin/c++
-- Check for working CXX compiler: /Applications/Xcode.app/Contents/Developer/Toolchains/XcodeDefault.xctoolchain/usr/bin/c++ -- works
-- Detecting CXX compiler ABI info
-- Detecting CXX compiler ABI info - done
-- Detecting CXX compile features
-- Detecting CXX compile features - done
-- Build type: Release
-- Z3: Z3_INCLUDE_DIR-NOTFOUND /usr/local/lib/libz3.dylib
CMake Error at cmake/FindZ3.cmake:23 (message):
  Z3 required version: 4.8.1 (installed: 0.0.0)
Call Stack (most recent call first):
  CMakeLists.txt:33 (find_package)


-- Configuring incomplete, errors occurred!
See also "/Users/rsas/work/souper-rsas/third_party/alive2/build/CMakeFiles/CMakeOutput.log".

[regehr]

whose z3 build are you using?
we had trouble using a binary from the z3 people and had to install it ourselves

[regehr]

I mean build it ourselves

if this seems like much of a problem we'll just add z3 to build_deps.sh

[rsas]

My pull request builds own z3, see build_deps.sh and CMakeLists.txt. After Alive integration, it doesn't build anymore.

[regehr]

hmm...
how about we get souper to build z3 and make alive2 happy with that, and then it should be straightforward for you to use that z3?

[manasij7479]

That should work. Might require some cmake hacking for alive.

[rsas]

@regehr your patch works for compiling, thank you. Now, is there a trick how to pass the LD_LIBRARY_PATH to llvm-lit? It is a Python tool, thus, we would need to append sys.path somehow.

[regehr]

what kind of tests need a different LD_LIBRARY_PATH?
lit discards environment variables before running tests but I think LD_LIBRARY_PATH is honored normally

[rsas]

We need somehow to pass the path to the libz3.dylib in lit:

********************
FAIL: Souper :: Unit/parser_tests.ll (461 of 462)
******************** TEST 'Souper :: Unit/parser_tests.ll' FAILED ********************
Script:
--
: 'RUN: at line 1';   /Users/rsas/work/souper-rsas/build-Release/parser_tests
--
Exit Code: 134

Command Output (stderr):
--
dyld: Library not loaded: libz3.dylib
  Referenced from: /Users/rsas/work/souper-rsas/third_party/alive2/build/libalive2.dylib
  Reason: image not found
/Users/rsas/work/souper-rsas/build-Release/test/Unit/Output/parser_tests.ll.script: line 1: 86900 Abort trap: 6           /Users/rsas/work/souper-rsas/build-Release/parser_tests

--

[regehr]

hmm, weird, this test passes for me. Iet me look into it.

[regehr]

hmm, we should not have to mess with library paths
we're giving alive2 a hard-coded path to the z3 library in build_deps.sh like this:
-DZ3_LIBRARIES=$z3_installdir/lib/libz3$shlib_extension
@rsas can you verify that this is resolving to the correct path and that the z3 library in fact exists at the referenced location on your machine?

[rsas]

It looks like on Darwin the path is not taken as a hard-coded one:

$ otool -L libalive2.dylib 
libalive2.dylib:
	@rpath/libalive2.dylib (compatibility version 0.0.0, current version 0.0.0)
	libz3.dylib (compatibility version 0.0.0, current version 0.0.0)
	/usr/lib/libc++.1.dylib (compatibility version 1.0.0, current version 400.9.4)
	/usr/lib/libSystem.B.dylib (compatibility version 1.0.0, current version 1252.200.5)

z3 lib exists:

$ ll third_party/z3-install/lib/libz3.dylib 
-rwxr-xr-x  1 rsas  staff  20917952 Feb  3 14:20 third_party/z3-install/lib/libz3.dylib

Does someone have a Mac to reproduce my issues?

[regehr]

yes I can try, do I just build your branch?

[rsas]

Yes, the 'z3builder' branch. Thank you.

[regehr]

@rsas please remove the part of build_deps (at the bottom) that builds z3, since we're building it earlier

[regehr]

also can you merge in the latest souper master? this will pull a change that refers uses a specific alive version, as opposed to using Manasij's head, which no longer works against your version here

[regehr]

I'm trying these changes myself, will post an update later, my Mac is slow at building everything

[regehr]

well, now I'm getting this when trying to link parser_tests

  "llvm::EnableABIBreakingChecks", referenced from:
      llvm::VerifyEnableABIBreakingChecks in ParserTests.cpp.o
      llvm::VerifyEnableABIBreakingChecks in libsouperParser.a(Parser.cpp.o)
      llvm::VerifyEnableABIBreakingChecks in libsouperInst.a(Inst.cpp.o)
      llvm::VerifyEnableABIBreakingChecks in libgtest_main.a(TestMain.cpp.o)
ld: symbol(s) not found for architecture x86_64
clang-7: error: linker command failed with exit code 1 (use -v to see invocation)
ninja: build stopped: subcommand failed.
Johns-MacBook-Pro:build johnregehr$ 

[rsas]

Let's move the discussion to #441.