Missing reference to Z3_mk_re_diff, but only on linux and only when testing code coverage

[daemontus]

Hi!

I have an interesting issue...

Since version 0.13.0, I can't compile any crate using z3 when testing code coverage using tarpaulin on linux.

Symptoms:

• The error I'm getting is "missing symbols" Z3_mk_re_diff, Z3_mk_re_allchar and Z3_mk_re_power (AFAIK, I'm not actually using these functions in my code).
• I'm using setup-z3 in my CI, so the version is fixed to 4.13.3.
• "Normal" test runs work ok on any operating system (see here and also here).
• Test runs using tarpaulin on macOS work ok (see here).
• Test runs using tarpaulin on linux fail (see here).

Could it be possible that these symbols are no longer present in Z3, but are still included in z3-sys? (and macOS is for some reason correctly recognizing that they are unused) Or do you have any other suggestions or experience with this stuff?

[toolCHAINZ]

Hmm that is very puzzling. I looked through the usage of those symbols and the z3.rs high level API does use them in the RegExp type.

On the z3 side, it looks like those symbols are pretty old (introduced in z3 4.8) and have been untouched all the way through z3 4.15.

So they should be present in z3 4.13.

I can't think what could be happening that would enable the linker to apparently find the z3 library but not find only those symbols.

Looks like high level support for these APIs was added in #275 by @Pat-Lafon , perhaps he might have some idea? The low level binding was already present in z3rs 0.12.1.

[toolCHAINZ]

I'd be curious if this still happens if you build z3rs with the gh-release enabled. Note that if you're doing it in CI you might be rate limited by GitHub (when the build tries to download the GitHub release) if you don't have a read-only GitHub API token accessible from the action.

[daemontus]

Thank you for the suggestions! I will definitely try to enable gh-release and see what happens.

Also, I was trying to reproduce the issues on a standalone Debian machine and my experience was again... weird.

First, I was testing with z3 4.8, as that is what was available for that version of Debian through apt. Here, I got the same "unknown symbols" error, even though as you said, they should be already there in this version. But then I upgraded manually to 4.13 and the tests actually ran fine. That still does not explain why it only happens when building for tarpaulin or why it happens in my CI jobs where 4.13 should be the default version though. So it might be a combination of things... I'll keep digging :)

[toolCHAINZ]

Oh actually that might explain it! What if z3 4.8 is installed in the CI runner, but it's a version before the point release that added those APIs?

Perhaps both 4.8 (from apt) and 4.13 are present but it's trying to link against 4.8?

I'm not sure why the link paths would be differing depending on whether it's a coverage job though.

We did so a little playing around with some of the link options in 0.13.x. It might be interesting to try it locked to exactly 0.13.0 and see if that works. If it does, that might narrow down if it was a link flag change we made.

[Pat-Lafon]

Yeah, that is my only thought. So I think the ubuntu runner comes with 4.8.12(https://packages.ubuntu.com/noble/libz3-4) which was cut on July 13, 2021. The Z3_mk_re_diff wouldn't be introduced until December 20th of that year Z3Prover/z3@7a60705

One quick thing to try is if you can set Z3_LIBRARY_PATH_OVERRIDE to the location that setup-z3 has it in, this would try to force the write version of z3 if you have two locally. I'm not sure if tarpaulin is setting an environment or anything that is messing with the binary resolution.

I was trying to look to see if the the object file being linked in for z3 is somehow listed in the log output but I don't think so.

[daemontus]

Awesome, thank you! That indeed sounds like a very plausible explanation. I'm traveling this weekend, so I'm not sure when I'll be able to test it. But I'll try to report back with more information as soon as I can.

[daemontus]

Well, greetings from the SMT workshop in Glasgow!

I ran some additional tests, and it seems that the explanation is correct :)

(1) Ubuntu runners come pre-installed with a version of Z3 that is not compatible with z3.rs > = 0.13.0.
(2) The setup-z3 github action seems to be correctly installing a new version of Z3 and adding it to LIBRARY_PATH and LD_LIBRARY_PATH (that's why the normal test runs work ok); Also, in a strange twist of faith, it turns out it was me who added this feature (the library paths) to the github action and forgot about it.
(3) For reasons unbeknownst to men, when building with tarpaulin, the linker insists on using the older version of the library, even though it can access the newer version as well (since it can find it once the older version is removed).

So, at this point, the most straightforward workaround is to either (a) explicitly install newer Z3 as a .deb package (instead of using setup-z3), which auto-removes the older version (b) install newer version of Z3 using setup-z3, and then remove the old version which is now obsolete. With both options, my CI builds now work as expected.

However, ideally, I would still like to fix the issue "more universally" if possible. Unfortunately, my knowledge of the build process for rust libraries that interface with C is not amazing. Do you think this is more likely to be an issue in setup-Z3 (i.e. something else other than LIBRARY_PATH and LD_LIBRARY_PATH needs to be set), or an issue with tarpaulin (some non-standard handling of linker options which prioritizes the older version of the library). Or is this something that simply is not possible to resolve deterministically? (i.e. unless the older version of the library is removed, the problem can come up randomly in various configurations)

[toolCHAINZ]

Glad to hear it is fixed!

As @Pat-Lafon suggested you could try using the Z3_LIBRARY_PATH_OVERRIDE (from #377 in 0.13.3), which was added for this type of situation (e.g. something is messing with link flags but you want to force it to use the right one).

As for a more universal fix, I'm not sure where the root cause is here; I'm inclined to blame tarpaulin, since it only happens with tarpaulin builds and only on x86.

Thankfully, this is a problem that should "solve itself" within a year when the next Ubuntu LTS comes out and bumps the version of z3 in apt.

I do wonder if this library should be more explicit about z3 version:

Maybe we could have some features like:

[features]
z3_4_8_12 = []
z3_4_9_0 = ["z3_4_8_12"]
z3_4_10_0 = ["z3_4_9_0"]
# etc, etc, etc

And then gate high-level APIs with the Z3 version they were added in.

[daemontus]

I see!

Z3_LIBRARY_PATH_OVERRIDE is also a good solution, but I'll have to check if setup-z3 sets some environment variable that can be actually used to get the location of the Z3 installation (other than trying to parse it from PATH or something).

Anyway, on my part, feel free to close this issue as resolved. If you want to keep it open until the new Ubuntu LTS version comes out (or simply as documentation for anyone that might have the same issue), that's of course also fine with me as well :)

[toolCHAINZ]

Oh I guess I should also say, gh-release side-steps all of this by just downloading the latest release and linking against that, so it all gets managed by cargo. The release is downloaded into the target directory so if you cache that in the action, you can even avoid the repeated downloads.

[toolCHAINZ]

I'll close this and convert into a discussion I think, since the default build works