On Wed, Aug 07, 2019 at 05:17:14PM +0000, Brooks Davis wrote:
> On Tue, Aug 06, 2019 at 09:22:52PM -0700, Mark Millard wrote:
> > [I found something known to be missing in the
> > in at least some versions of
> > llvm/cmake/modules/CrossCompile.cmake that messes
> > up the overall handling of LLVM_ENABLE_Z3_SOLVER .]
> >
> > On 2019-Aug-6, at 20:23, Mark Millard <marklmi at yahoo.com> wrote:
> >
> >
> >
> > > On 2019-Aug-6, at 19:08, Brooks Davis <brooks at freebsd.org> wrote:
> > >
> > >> On Tue, Aug 06, 2019 at 05:59:21PM -0700, Mark Millard wrote:
> > >>>
> > >>>
> > >>> On 2019-Aug-6, at 09:55, Brooks Davis <brooks at freebsd.org> wrote:
> > >>>
> > >>>> I'd prefer to disable this dependency. There's a knob that worked in
> > >>>> the 8.0 timeframe, but the lit build now autodetects z3 when it is
> > >>>> present and I've failed to find a knob to disable it. For now, the
> > >>>> easy
> > >>>> workaround is probably to disable options LIT. We could make that the
> > >>>> default on non-LLVM platforms is that makes sense.
> > >>>>
> > >>>> -- Brooks
> > >>>
> > >>> Okay.
> > >>>
> > >>> poudriere-devel automatically built math/z3 because
> > >>> I'd indicated to build devel/llvm90 . math/z3 was not
> > >>> previously built: I've never had other use of it. So
> > >>> my context was not one of an implicit autodetect.
> > >>
> > >> The dependency is there because if z3 is installed then the package
> > >> that is built depends on z3. Thus I had not choice but to add a z3
> > >> dependency until I find a way to turn it off. You can either help find
> > >> a way to disable z3 detection in the cmake infrastructure or turn off
> > >> LIT. I don't have any use for reports on the effects of commenting out
> > >> the DEPENDS line. I know what that does.
> > >
> > >
> > > I hope this helps. (I'm not a cmake expert.)
> > >
> > > llvm-9.0.0rc1.src/lib/Support/Z3Solver.cpp does:
> > >
> > > #if LLVM_WITH_Z3
> > >
> > > #include <z3.h>
> > >
> > > namespace {
> > > . . .
> > > } // end anonymous namespace
> > >
> > > #endif
> > >
> > > llvm::SMTSolverRef llvm::CreateZ3Solver() {
> > > #if LLVM_WITH_Z3
> > > return llvm::make_unique<Z3Solver>();
> > > #else
> > > llvm::report_fatal_error("LLVM was not compiled with Z3 support, rebuild
> > > "
> > > "with -DLLVM_ENABLE_Z3_SOLVER=ON",
> > > false);
> > > return nullptr;
> > > #endif
> > > }
> > >
> > > (There are other places LLVM_WITH_Z3 is used but the
> > > above is suggestive.)
> > >
> > > Working backwards finds that:
> > >
> > > /wrkdirs/usr/ports/devel/llvm90/work/llvm-9.0.0rc1.src/CMakeLists.txt
> > >
> > > shows LLVM_WITH_Z3 being conditionally set to 1 via . . .
> > >
> > > set(LLVM_Z3_INSTALL_DIR "" CACHE STRING "Install directory of the Z3
> > > solver.")
> > >
> > > find_package(Z3 4.7.1)
> > >
> > > if (LLVM_Z3_INSTALL_DIR)
> > > if (NOT Z3_FOUND)
> > > message(FATAL_ERROR "Z3 >= 4.7.1 has not been found in
> > > LLVM_Z3_INSTALL_DIR: ${LLVM_Z3_INSTALL_DIR}.")
> > > endif()
> > > endif()
> > >
> > > set(LLVM_ENABLE_Z3_SOLVER_DEFAULT "${Z3_FOUND}")
> > >
> > > option(LLVM_ENABLE_Z3_SOLVER
> > > "Enable Support for the Z3 constraint solver in LLVM."
> > > ${LLVM_ENABLE_Z3_SOLVER_DEFAULT}
> > > )
> > >
> > > if (LLVM_ENABLE_Z3_SOLVER)
> > > if (NOT Z3_FOUND)
> > > message(FATAL_ERROR "LLVM_ENABLE_Z3_SOLVER cannot be enabled when Z3
> > > is not available.")
> > > endif()
> > >
> > > set(LLVM_WITH_Z3 1)
> > > endif()
> > >
> > > if( LLVM_TARGETS_TO_BUILD STREQUAL "all" )
> > > set( LLVM_TARGETS_TO_BUILD ${LLVM_ALL_TARGETS} )
> > > endif()
> > >
> > >
> > > If I read that correctly, LLVM_ENABLE_Z3_SOLVER set directly
> > > appears to override the default (that tracks if z3 was found).
> >
> > I saw a reference to:
> >
> > diff --git a/llvm/cmake/modules/CrossCompile.cmake
> > b/llvm/cmake/modules/CrossCompile.cmake
> > index bc3b210f018..0c30b88f80f 100644
> > --- a/llvm/cmake/modules/CrossCompile.cmake
> > +++ b/llvm/cmake/modules/CrossCompile.cmake
> > @@ -53,6 +53,7 @@ function(llvm_create_cross_target_internal target_name
> > toolchain buildtype)
> > -DLLVM_DEFAULT_TARGET_TRIPLE="${TARGET_TRIPLE}"
> > -DLLVM_TARGET_ARCH="${LLVM_TARGET_ARCH}"
> >
> > -DLLVM_TEMPORARILY_ALLOW_OLD_TOOLCHAIN="${LLVM_TEMPORARILY_ALLOW_OLD_TOOLCHAIN}"
> > + -DLLVM_ENABLE_Z3_SOLVER="${LLVM_ENABLE_Z3_SOLVER}"
> > ${build_type_flags} ${linker_flag} ${external_clang_dir}
> > WORKING_DIRECTORY ${LLVM_${target_name}_BUILD}
> > DEPENDS CREATE_LLVM_${target_name}
> >
> > in https://reviews.llvm.org/D54978 on Feb 12 2019, 5:41 PM
> > and it had the comment:
> >
> > QUOTE
> > Independent of the rest of the discussion, this patch should be part of the
> > reland, to make sure that explicitly turning off Z3 works reliably. Thanks
> > for coming up with that, and thanks everyone for the good discussion here :)
> > END QUOTE
> >
> > This apparently fixes a sub-cmake not respecting the
> > LLVM_ENABLE_Z3_SOLVER setting in the parent cmake.
> > (The overall review earlier describes the sub-cmake
> > not doing the right thing.)
>
> Thanks for digging this up. Unfortunately, this doesn't seem to have
> solved the problem. With this patch applied I still get this if I have
> z3 installed on the system and no LIB_DEPENDS line:
>
> Error: /usr/local/bin/FileCheck90 is linked to /usr/local/lib/libz3.so.0
> from math/z3 but it is not declared as a dependency
> Warning: you need LIB_DEPENDS+=libz3.so:math/z3
>
> I've generally observed that the portions of the system that cover lit
> (which includes FileCheck) aren't very well behaved.I've filed https://bugs.llvm.org/show_bug.cgi?id=42921 upstream, hopefully someone who understand this part of the cmake system will help us out. -- Brooks
signature.asc
Description: PGP signature
