Extend STP_STUB and YICES_STUB flag #600
Conversation
The new build flag STP_USE_LIB can be set to choose the STP library to be used. Options are '', 'included', 'system', 'disable', and an absolute path starting with '/'. The empty string defaults to the same behavior as 'included' which builds STP from the provided source. 'disable' has the same effect as STP_STUB=1, i.e. disabling STP at runtime. 'system' tries to find the system library (currently only in /usr/lib) and then copies it for building. An absolute path starting with '/' can be provided and must point to the directory in which the desired STP library is located. Otherwise the same as 'system'. The options for precompiled STP libraries essentially do the same things as STP_STUB, except they copies the library instead of compiling the stub. For compatibility reasons within the Makefiles, the library is linked to under the soname libstp.so.1 eventhough technically it should be libstp.so.2.3 (for the newest versions), but STP is backwards-compatible enough that this does not cause issues. Enabling the flag reduced the build time by up to 25% (the time to compile STP from source), while `make TEST_BSC_OPTIONS="-sat-stp" smoke` saw no reductions, both compared to the provided source and Yices.
Defining STP_STUB now creates an error with a hint to use STP_USE_LIB=disable. The new way is more readable and clearer in intent. Since STP_STUB had a bug that made it effectively unusable for 3 years, replacing the option likely affects few users while those that worked around the bug have to change things anyway. This change also enabled some minor refactoring work for better readability.
On MacOS, libraries have a different suffix and the filesystem is structured differently. This commit adds the relevant bits and pieces for the option STP_USE_LIB to work on MacOS in principle. Also fixes the issue with STP_STUB (which is used with STP_USE_LIB=disable), where the wrong library file is copied, resulting in a linking error down the line.
On Linux, use find in /usr/lib to find the correct library. Only consider the first result; all results should point to the same source anyway. The results are also cleaned to ensure reliable behavior (the library name must only contain alphanumerics + colon) Improve cleaning of user input when a path is passed in
The logic for STP_USE_LIB has been indented to improve the readability and make the different cases more obvious. Also, minor fixes. `find` ends with NUL byte, so replace that with newline. The BSC linker needs at least a symlink named libstp.so The SNAME is completely independent from the library name, so just choose a fitting one
The SNAME is exported in the general stp Makefile. The symbolic link is created there too. Remove both actions from the special case as they are handled in the general case.
|
Previous attempts to change the library loading behavior of STP and YICES are listed in this comment. Ultimately, something like SBV is the best solution, but there is no ETA and I'm not too familar with Haskell, so waiting for that is hardly an option. This PR extends the CLI options at build time to enable usage of the system library for STP, or even a custom library. The changes are limited to the respective Makefiles and INSTALL.md (the latter for obvious reasons). This is done to hopefully quickly merge the changes after the next release. |
|
Taken from this comment by @quark17:
When specifying
Given that this is about a build time option, I don't think that changing the library later is a use case that has to be supported. Indeed, changing the name, or even creating a symlink, isn't terribly difficult. Other proposals
Yeah, I know about these discussions, and also know about the great summary I mentioned in the previous comment. But as stated elsewhere, all of that takes even more time and does things that aren't necessary at this point. So the question is
To reply to this point more specifically: This question relies on the assumption that the effort needed for the big proposals is of the same kind (just more of it) as the one needed for this PR. But they are completely different on a technical level, sufficiently different that I don't consider myself able of implementing them. In part, this misunderstanding may have been caused by my usage of "overhaul", as this PR is really just a minor refactor + feature addition. Doesn't alleviate the need for testing, but certainly not the grand vision that the other proposals are. |
|
All good. And thank you for your effort and input on this! For some background: Yices and STP were added back when BSC was a proprietary tool. Yices was not open source either at the time, but people could download the pre-compiled library for individual use. The Bluespec company didn't have the right to distribute the library. Instead, BSC was shipped with a Yices stub, and users who wanted to use Yices could download the real library and move the stub aside. So stubbing was introduced exactly for the reason of allowing people to change the library used by their installation of BSC. When BSC went open on GitHub, there were concerns about compiling/including STP. The STP stub was introduced, probably as a simple way to satisfy those concerns at the time. I can't recall if there was a conscious choice to go with a stub (vs just removing STP out of the build with macros). Because, thinking about it now, the only reason to have a stub is because you want to change that choice later. On the other github issue, you mentioned in a comment about it being a build option. If not using STP is a build-time option, then we don't need a stub: the BSC executable could just be built to know that STP is not available and to not go looking for a library at all. |
|
I see. Up to now, the *_STUB options were only mentioned in the context of disabling, but it makes sense that there were other motivations behind them. I can implement another option |
Using STP_USE_LIB=placeholder means that the stub is compiled with a generic name and copied to the installation, but is supposed to be replaced at a later date. To make the intentions clear, the library is renamed to *_placeholder with a symlink created with the original name pointing to the library.
This commit series renames STP_STUB to STP_USE_LIB and extends it to accept config values instead of being a simple boolean flag. The old behavior of STP_STUB=1 is realized with STP_USE_LIB=disable
Two new options are added to the flag,
systemandarbitrary absolute path. The first option searches the standard locations to find the system installed version of STP, while the latter takes a path to a user-defined library providing STP.YICES_STUB will be refactored in a similar manner to ensure consistency between the two flags.