``shell``, ``libz3`` and ``test-z3`` should use the same generated ``.cpp`` files

[delcypher]

As mentioned in #491

The build system seems to generate three separate copies of

• gparams_register_modules.cpp
• install_tactic.cpp
• mem_initializer.cpp

for the shell (i.e the z3 executable), api_dll and test (i.e. test-z3 executable) components.

Right now all these generated .cpp files are the same so there is no divergence in behaviour but it could lead to weird problems later on, it's also a little bit confusing.

The particular situation I was thinking of was having the z3 executable link against the libz3 shared library.

Out of curiosity I tried seeing what would happen if I removed -fvisibility=hidden and linked the z3 executable against of libz3.so on Linux. To my surprise this actually worked. I was expecting the linker to complain about multiple definitions of the same symbol (e.g. install_tactics(...)) but GNU ld doesn't seem to care.

When running the application it seems that the dynamic linker (ld-linux.so) searches the application first before considering shared libraries. So when z3 is executed install_tactics(...) from the shell component rather than libz3.so gets used. I wasn't expecting this.

I stumbled across this blog post which illustrates what I'm seeing.

As mentioned above because the generated .cpp files are all identical there isn't a problem right now (i.e. calling install_tactics(...) in the shell or api_dll component makes no difference) but I think it would be nice to fix this.

Here's my suggested fix:

1. Introduce a new component all_init (sorry, I need a better name) and have the three generated .cpp files emitted there only (i.e. the shell, api_dll and test no longer have their own versions of these files). When generating files the component directories to scan over all would be all other component directories (apart from executable and library components).
2. Make the shell, api_dll and test components depend on the all_init component so that they all share the implementation of install_tactics(...) and the other functions.

To me this fix seems like the right approach because

• It follows the existing notion of components and their dependencies that already exists in both the Python and CMake build systems. That should make the change fairly simple to implement in both build systems.
• It doesn't prevent the possibility in the future of introducing another executable or library (e.g. z3-embedded) that only uses a subset of Z3's components. For this fictional z3-embedded executable/library it would not have all_init as a dependency and it would generate it's own .cpp files based on the components it actually uses.

If this seems sensible enough I'd be happy to implement this (although I'd like to base my work on top of #498 so I'd start work after that's merged into the mainline).

[delcypher]

Well I had a go at writing a proof of concept ( https://github.com/delcypher/z3-1/commit/503b954cf932e8be794ee2e28ceb8a8c3b7c107d ).

I'm not very satisfied with it. A problem I had not realised is that the proposed all_init library is circularly dependent (e.g. util depends on all_init, but all_init depends on util). This means that all_init.a would need to be put multiple times on the linking command line for linking to succeed. In the end I ended up treating the all_init component specially and putting it's object files on the linking command line instead to avoid this problem. There seems to be some precedence for this as the DLLComponent has special code for the reexports that emits the object files on the linking command line. However this does not feel very elegant to me.

The CMake build does not have this problem because components are not built into static libraries.

So the proof of concept ends up making the CMake build system simpler but complicates the Python build system. It also kind of breaks the behaviour of "components" because all_init is circularly dependent but all other components are not. Therefore I don't think this is the right approach.

@wintersteiger @NikolajBjorner Do you have any thoughts on what the right approach might be?

[NikolajBjorner]

BTW, I noticed that default build under nmake defines Z3DEBUG but not _TRACE. The previous behavior is to enable TRACE in debug builds.

[NikolajBjorner]

Another note: I am currently unable to complete the nmake build on windows:

['C:/cmake/z3/src/api', 'api_ast_map.h'] Traceback (most recent call last): File "C:/cmake/z3/scripts/mk_gparams_register_modules_cpp.py", line 38, in sys.exit(main(sys.argv[1:])) File "C:/cmake/z3/scripts/mk_gparams_register_modules_cpp.py", line 32, in main pargs.destination_dir File "C:\cmake\z3\scripts\mk_genfile_common.py", line 233, in mk_gparams_register_modules_internal for h_file in sorted_headers_by_component(h_files_full_path): File "C:\cmake\z3\scripts\mk_genfile_common.py", line 74, in sorted_headers_by_component sorted_headers = sorted(l, key=get_key) File "C:\cmake\z3\scripts\mk_genfile_common.py", line 61, in get_key assert 'src' in stripped_path.split(os.path.sep) AssertionError

[delcypher]

@NikolajBjorner Is this using NMake with the Python build system or using the CMake build system to generate an NMake Makefile?

[delcypher]

@NikolajBjorner Nevermind I've inferred from the stacktrace that this is the CMake build. I'll take a look. I don't use NMake generator with CMake. I use Ninja (so much faster) or VisualStudio under Windows

[NikolajBjorner]

I have a local fix which is to add a disjunction to the assert. The rest of the code seems ok

[delcypher]

It looks like using os.path.sep does not work in this case because NMake may be using / rather than \. The other generators (i.e Ninja and Visual Studio) don't seem to have this problem.

[delcypher]

@NikolajBjorner Looks like you fixed the assertion in 67dc5ce2b5f2b29defb43c47286604008535e1a2 . Thanks for doing that.

[levnach]

@delcypher Suppose we want relative paths in the includes. How can we instrument cmake to make sure that the include path includes src? Something like:

      list(APPEND Z3_COMPONENT_EXTRA_INCLUDE_DIRS "src")

(which does not work) ?

[delcypher]

@levnach Please don't hijack unrelated issues with your questions. Please open a new issue and I'll try my best to answer.