Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Extend STP_STUB and YICES_STUB flag #600

Draft
wants to merge 8 commits into
base: main
Choose a base branch
from
Draft

Commits on Aug 13, 2023

  1. Introduce STP_USE_LIB flag

    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.
    Vekhir committed Aug 13, 2023
    Configuration menu
    Copy the full SHA
    d81def4 View commit details
    Browse the repository at this point in the history
  2. Prohibit STP_STUB in favor of STP_USE_LIB=disable

    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.
    Vekhir committed Aug 13, 2023
    Configuration menu
    Copy the full SHA
    d3b34e3 View commit details
    Browse the repository at this point in the history
  3. Add MacOS support to STP_USE_LIB

    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.
    Vekhir committed Aug 13, 2023
    Configuration menu
    Copy the full SHA
    0feb6b8 View commit details
    Browse the repository at this point in the history
  4. Generalize search for STP system library

    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
    Vekhir committed Aug 13, 2023
    Configuration menu
    Copy the full SHA
    a4536b8 View commit details
    Browse the repository at this point in the history
  5. Improve readability in stp/Makefile

    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
    Vekhir committed Aug 13, 2023
    Configuration menu
    Copy the full SHA
    fcb8e05 View commit details
    Browse the repository at this point in the history
  6. Clean up STP src

    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.
    Vekhir committed Aug 13, 2023
    Configuration menu
    Copy the full SHA
    4866ecf View commit details
    Browse the repository at this point in the history
  7. Minor fixes for STP handling

    Vekhir committed Aug 13, 2023
    Configuration menu
    Copy the full SHA
    cf03829 View commit details
    Browse the repository at this point in the history

Commits on Aug 16, 2023

  1. Introduce placeholder option to STP

    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.
    Vekhir committed Aug 16, 2023
    Configuration menu
    Copy the full SHA
    aed005b View commit details
    Browse the repository at this point in the history