cmake: build correctly with globally installed z3

[gerion0]

I have no clue of cmake but this seems to enable building against a globally installed z3 (like per a distribution package).

[yuleisui]

We plan to remove cudd in the near future and Z3 will be part of SVF's third-party lib later.

1ac1476

I found the issue for missing z3 due to an extra SVF_Z3 macro. I have just removed it. This should solve the problem. However, your patch seems to solve the same problem that build.sh does. Please let me whether the current upstream works or if you want to change anything in CMakelist.txt to make it more robust.

[yuleisui]

We plan to remove cudd in the near future and Z3 will be part of SVF's third-party lib later.

I found the issue for missing z3 due to an extra SVF_Z3 macro. I have just removed it. This should solve the problem. However, your patch seems to solve the same problem that build.sh does. Please let me whether the current upstream works or if you want to change anything in CMakelist.txt to make it more robust.

[gerion0]

Sorry, I don't get, what you mean. In the current master, z3 is already a hard dependency, because of:

add_llvm_library(Svf STATIC ${SOURCES} LINK_LIBS Cudd ${Z3_DIR}/bin/libz3.a)

(Source)

However, this line forced z3 to be

• statically linked
• laying in a directory bin/

This forces z3 to be exactly the z3 that is downloaded with build.sh. But this is not always the case. The Debian package for example has z3 as /usr/lib/x86_64-linux-gnu/libz3.so.4 (Source). CMake can access this package (and the correct build flags) via pkgconfig. My patch enables both, the current building via an externally downloaded z3 (as it is done in build.sh) and a building against a globally installed z3 that is found via pkgconfig.

Enabling the build only with build.sh does not serve my needs. I'm embedding SVF as meson subproject that calles cmake directly.

With my patch it should be enough to execute this (on a Debian/Ubuntu) to successfully compile SVF:

$ sudo apt install libz3-dev llvm-11-dev
$ mkdir build && cd build
$ cmake -G "Ninja" -DLLVM_DIR="/usr/lib/llvm-11" ..
$ ninja

[yuleisui]

I see. However, for my build on mac os, there is a compilation error (z3++.h not found) if we do not include Z3_DIR here: https://github.com/SVF-tools/SVF/pull/502/files#diff-1e7de1ae2d059d21e1dd75d5812d5a34b0222cef273b7c3a2af62eb747f9d20aL56.

BTW: what do you want to do here: https://github.com/SVF-tools/SVF/pull/502/files#diff-1e7de1ae2d059d21e1dd75d5812d5a34b0222cef273b7c3a2af62eb747f9d20aR55?

[yuleisui]

I see. However, for my build on mac os, there is a compilation error (z3++.h not found) if we do not include Z3_DIR here: https://github.com/SVF-tools/SVF/pull/502/files#diff-1e7de1ae2d059d21e1dd75d5812d5a34b0222cef273b7c3a2af62eb747f9d20aL56.

BTW: what do you want to do here: https://github.com/SVF-tools/SVF/pull/502/files#diff-1e7de1ae2d059d21e1dd75d5812d5a34b0222cef273b7c3a2af62eb747f9d20aR55?

my build command:

./build.sh

[yuleisui]

I think we need to include ${Z3_INSTALLS} here.

[gerion0]

This should be fixed.

[gerion0]

BTW: what do you want to do here: https://github.com/SVF-tools/SVF/pull/502/files#diff-1e7de1ae2d059d21e1dd75d5812d5a34b0222cef273b7c3a2af62eb747f9d20aR55?

This resolves a relative path to the build directory for Z3_DIR in an absolute path. If I remember correctly, the linker had problems with relative paths.