add install tip for bitwuzla

[syheliel]

Triton will fail to compile if bitwuzla isn't using --share in configuration

[SweetVishnya]

This sounds wrong. We successfully link everything statically.

[syheliel]

There is an error if I drop the --shared arg. Actually that's what CI does: https://github.com/JonathanSalwan/Triton/blob/master/.github/workflows/linux.yml

[SweetVishnya]

Have you tried to specify paths to Bitwuzla libs and includes?

[syheliel]

I'm sure that It's not a lib missing problem. The problem is like this #1042 but occur in libbitwuzla.a. Anyway, I'm trying to reproduce the problem through CI.

[SweetVishnya]

Can you build Bitwuzla with -fPIC?

[SweetVishnya]

This is how we build Bitwuzla in Sydr:

    if(${CMAKE_BUILD_TYPE} MATCHES "Debug")
      set(GMP_COMPILER_FLAGS CFLAGS=-g CXXFLAGS=-g)
      set(GMP_OPTIONS --enable-assert --enable-alloca=debug --disable-assembly)
      set(BITWUZLA_BUILD_TYPE debug)
    else()
      set(BITWUZLA_BUILD_TYPE production)
    endif()

    # Build GMP
    ExternalProject_Add(gmp
      URL ${GMP_SOURCE_DIR}
      URL_HASH SHA256=bb7ede21073992ba41a8f42f74788eaade9c2fa863de7b4cfa3d798ad58a013c
      PREFIX ${GMP_DIR}-build
      INSTALL_DIR ${GMP_DIR}
      CONFIGURE_COMMAND CC=${CMAKE_C_COMPILER} CXX=${CMAKE_CXX_COMPILER} ${GMP_COMPILER_FLAGS}
                        ../gmp/configure --prefix=${GMP_DIR} --enable-cxx --disable-shared ${GMP_OPTIONS}
      BUILD_ALWAYS OFF
    )

    # Build CaDiCaL
    ExternalProject_Add(cadical
      SOURCE_DIR ${CADICAL_SOURCE_DIR}
      PREFIX ${CADICAL_DIR}-build
      INSTALL_DIR ${CADICAL_DIR}
      CONFIGURE_COMMAND cp -r ${CADICAL_SOURCE_DIR} . && cd cadical &&
                        CC=${CMAKE_C_COMPILER} CXX=${CMAKE_CXX_COMPILER} CXXFLAGS=-fPIC ./configure
      BUILD_COMMAND cd cadical && make -j
      INSTALL_COMMAND mkdir -p ${CADICAL_DIR}/lib && cp cadical/build/libcadical.a ${CADICAL_DIR}/lib &&
                      mkdir -p ${CADICAL_DIR}/include && cp cadical/src/ccadical.h ${CADICAL_DIR}/include
      BUILD_ALWAYS OFF
    )

    # Build Btor2tools
    ExternalProject_Add(btor2tools
      SOURCE_DIR ${BTOR_SOURCE_DIR}
      PREFIX ${BTOR_DIR}-build
      INSTALL_DIR ${BTOR_DIR}
      CMAKE_ARGS -DCMAKE_CXX_COMPILER=${CMAKE_CXX_COMPILER}
                 -DCMAKE_C_COMPILER=${CMAKE_C_COMPILER}
                 -DCMAKE_CXX_FLAGS=-D__STDC_FORMAT_MACROS
                 -DCMAKE_BUILD_TYPE=${CMAKE_BUILD_TYPE}
                 -DCMAKE_POSITION_INDEPENDENT_CODE=ON
                 -DBUILD_SHARED_LIBS=OFF
                 -DCMAKE_INSTALL_PREFIX=${BTOR_DIR}
                 -DCMAKE_INSTALL_LIBDIR=lib
      BUILD_ALWAYS OFF
    )

    # Build Bitwuzla
    ExternalProject_Add(bitwuzla
      SOURCE_DIR ${BITWUZLA_SOURCE_DIR}
      PREFIX ${BITWUZLA_DIR}-build
      INSTALL_DIR ${BITWUZLA_DIR}
      CONFIGURE_COMMAND cp -r ${BITWUZLA_SOURCE_DIR} . && cd bitwuzla &&
                        CC=${CMAKE_C_COMPILER} CXX=${CMAKE_CXX_COMPILER} ./configure.sh ${BITWUZLA_BUILD_TYPE}
                            --prefix ${BITWUZLA_DIR}
                            --path ${GMP_DIR} --path ${BTOR_DIR} --path ${CADICAL_DIR}
                            --only-cadical --no-symfpu --no-testing
      BUILD_COMMAND make install -j -C bitwuzla/build
      INSTALL_COMMAND ""
      BUILD_ALWAYS OFF
      DEPENDS gmp cadical btor2tools
    )
  endif()

[syheliel]

Seems that sydr doesn't require --shared or -fPIC. But I have confirmed the problem in CI by removing --shared arg in linux.yml. see https://github.com/syheliel/Triton/actions/runs/3367955710/jobs/5585960627

[SweetVishnya]

Sydr uses Triton inside. The problem in CI is that you should specify -fPIC.

[JonathanSalwan]

Hey guys,

Yes I agree with @SweetVishnya, it's the user responsibility to compile its dependencies either on shared or static. It's totally possible to compile Bitwuzla statically, but as @SweetVishnya said, you have to define the code as position independent (-fPIC). Then, you can define the BITWUZLA_LIBRARIES variable to use the Bitwuzla archive when compiling Triton.