Use rpath to find libstp.so

[trixirt]

bsc depends on its wrapper to set the LD_LIBRARY_PATH to
it's private version of libstp.so. Link with an rpath
to this library and bsc can be run without the wrapper.

Signed-off-by: Tom Rix [email protected]

[quark17]

Thank you for contributing this. However, I believe that it is already covered by PR #163. That PR addresses a few issues that are not addressed here: the Makefile needs to also work for macOS, and the Yices library also needs to be found.

That PR hasn't been merged because it seemed like a better approach would be for the BSC executable to load the library with dlopen from a known location (rather than linking at runtime, and without hardcoding the BLUESPECDIR in an additional location). No one has written that code yet, though. But I will add it to the wishlist for the next release.

It's worth noting that the wrapper is still needed, to set BLUESPECDIR.

[trixirt]

yices is in the same dir as stp and has stp as its dependency so the single rpath should work, though duplicating it would be fine too.
dlopen usually defers link errors to runtime when that happens to a user, they are normally stuck.
The BUILDSPECDIR is still need.

[quark17]

BSC uses a SAT/SMT solver for a number of purposes. Yices and STP are two separate implementations that the user can choose from, by providing the flags -sat-yices or -sat-stp on the command line. (Yices is the default if no flags are provided.)

The very first thing that BSC does when executed is to check the flags. During that, it checks which solver has been selected; and then it checks to see whether the linked library is of the right version. (Note that this repo supports building a stub in place of either STP or Yices; if, for some reason, you can't build that on your system, or don't want to. So BSC also needs to check that the library is not a stub!) For Yices, there is a function in its API that returns the version number. If the user has selected Yices, but the version does not match the expected version, then BSC warns the user and attempts to use STP instead. STP does not have a version function in its API; but we still want to check that it is a not a stub, so we look for a non-NULL pointer returned by the init function.

There have been several proposed improvements to this situation:

• Don't offer a choice of solver. Instead, remove STP and just use Yices. In that case, we could even statically link with Yices, perhaps. (See PR Remove STP support #31)
• Unvendor STP and Yices (see issues Unvendor yices2  #50 and Unvendor stp #51). Then, it would be the user's responsibility to have the right version installed, and in the linker's search path
• Have BSC use a standardized API (such as SMT-lib), to which any solver (that supports the format) can be plugged in (see issue Investigate smtlib for bsc constraint solving #117)
• Use dlopen (discussed on PR Load SAT libs from dir relative to exe using linker flags #163). The BSC repo would not need to support building stubs in this case, because that could be implemented by just not having a library of the given name in the SAT directory, as BSC would check for that first before attempting to call dlopen.

Unvendoring Yices/STP and using a standardized API (SMT-lib) might be my preferred choice. Although it could make BSC a little harder to install, because users would have to install an SMT solver first, and there are not convenient packages for those.

Applying an RPATH in the meantime is fine with me. But there are still two problems that would need to be addressed: (1) Your change doesn't work for macOS; you'll need an if-else in the Makefile to use a different syntax for mac. Your change doesn't remove the LD_LIBRARY_PATH from the wrapper, so the CI won't be testing it. (2) The relative location of BLUESPECDIR to the binaries (../lib/) should not be hardcoded in more than one place, if we can avoid it. It's worth noting that, with the current installation of BSC, someone can move the BLUESPECDIR to wherever they want and just change the wrapper file; with RPATH, they would also now need to change the RPATH in the binaries. (Probably not a big deal, but it'd be worth noting the new requirement in the build documentation.)