** Description changed:
[ Description ]
- * This bug was found on Ubuntu 26.04 LTS for llvm-toolchain-18
+ * This bug is present for llvm-toolchains 18-22 on stonking and resolute
* Autopkgtest trigger z3/4.13.3-1build1 consistently fails for Resolute
on AMD64 and ARM64 with error message
639s # (in test file debian/qualify-clang.sh, line 1815)
639s # `assert_success "Static analysis with Z3 constraints failed"' failed
639s #
639s # -- command failed --
639s # status : 1
639s # output (2 lines):
639s # error: 'expected-error' diagnostics seen but not expected:
639s # (frontend): analyzer constraint manager 'z3' is only available if
LLVM was built with -DLLVM_ENABLE_Z3_SOLVER=ON
639s # --
https://autopkgtest.ubuntu.com/packages/llvm-toolchain-18/resolute/amd64/20251108_180943_0c890@
https://autopkgtest.ubuntu.com/packages/llvm-toolchain-18/resolute/arm64/20251108_204444_3c296@
(Note that this is classified as tmpfail for ARM64)
* This fails because DLLVM_ENABLE_Z3_SOLVER is always set to OFF for
Ubuntu builds:
Z3_FLAG = -DLLVM_ENABLE_Z3_SOLVER=OFF
ifeq ($(shell dpkg --compare-versions $(shell dpkg-query -W -f '${Version}'
libz3-dev) gt 4.7.0; echo $$?),0)
# no ocaml support in main for Ubuntu
ifneq ($(shell dpkg-vendor --derives-from Ubuntu && echo yes),yes)
Z3_FLAG = -DLLVM_ENABLE_Z3_SOLVER=ON
endif
endif
* It is believed that the ifneq clause was included to avoid adding z3
(which lives in universe) as a runtime dependency to llvm-toolchain-18
when it was in main. llvm-toolchain-18 has since been demoted to
universe, so this clause is no longer needed and Z3_FLAG can be set to
ON for Ubuntu builds.
The fix looks like replacing the code above with the following code in
debian/rules:
Z3_FLAG = -DLLVM_ENABLE_Z3_SOLVER=OFF
ifeq ($(shell dpkg --compare-versions $(shell dpkg-query -W -f '${Version}'
libz3-dev) gt 4.7.0; echo $$?),0)
Z3_FLAG = -DLLVM_ENABLE_Z3_SOLVER=ON
endif
+
+ Please note that for the default version of llvm-toolchains, z3 solver
+ should not be enabled because we must ensure that the default llvm (in
+ main) does not depend on z3 (in universe).
+
[ Impact ]
* This fix will allow z3 to be enabled as a runtime dependency for llvm-
toolchain-18 which will cause the z3/4.13.3-1build1 autopkgtest to pass.
[ Test Plan ]
* This bug can be reproduced, and the fix tested, by following these
steps
$ git ubuntu clone llvm-toolchain-18
$ git cd llvm-toolchain-18
$ git checkout --track pkg/ubuntu/resolute
$ git ubuntu export-orig
$ dpkg-buildpackage -S -nc -sa
Next, build the package locally with sbuild using -d resolute, or in a ppa,
and triggering autopkgtests against all-proposed for at least AMD64 and ARM64.
The autopkgtests should fail and yield an error message like this:
639s # (in test file debian/qualify-clang.sh, line 1815)
639s # `assert_success "Static analysis with Z3 constraints failed"' failed
639s #
639s # -- command failed --
639s # status : 1
639s # output (2 lines):
639s # error: 'expected-error' diagnostics seen but not expected:
639s # (frontend): analyzer constraint manager 'z3' is only available if
LLVM was built with -DLLVM_ENABLE_Z3_SOLVER=ON
639s # --
To test the fix, change this code in debian/rules:
Z3_FLAG = -DLLVM_ENABLE_Z3_SOLVER=OFF
ifeq ($(shell dpkg --compare-versions $(shell dpkg-query -W -f '${Version}'
libz3-dev) gt 4.7.0; echo $$?),0)
# no ocaml support in main for Ubuntu
ifneq ($(shell dpkg-vendor --derives-from Ubuntu && echo yes),yes)
Z3_FLAG = -DLLVM_ENABLE_Z3_SOLVER=ON
endif
endif
To:
Z3_FLAG = -DLLVM_ENABLE_Z3_SOLVER=OFF
ifeq ($(shell dpkg --compare-versions $(shell dpkg-query -W -f '${Version}'
libz3-dev) gt 4.7.0; echo $$?),0)
Z3_FLAG = -DLLVM_ENABLE_Z3_SOLVER=ON
endif
Rebuild and retrigger autopkgtests and the error message should not be
present.
[ Where problems could occur ]
* If a custom build environment lacks libz3-dev during debian/rules
evaluation, the dpkg-query version check will evaluate to false, falling
back to -DLLVM_ENABLE_Z3_SOLVER=OFF and causing the "`assert_success
"Static analysis with Z3 constraints failed"' failed" error to occur.
However, because libz3-dev is strictly declared in debian/control Build-
Depends, standard build environments (sbuild/Launchpad) should always
have the package installed.
+ * We must ensure that z3 solver is not enabled for the default version
+ of llvm-toolchains
+
[ Other Info ]
This was encountered while testing a patch for LP #2146915
(https://bugs.launchpad.net/ubuntu/+source/llvm-
toolchain-18/+bug/2146915).
It is intended to bundle the fix for that bug (and related FTBFS issues
with LLVM 17, 19, and 20) and this fix into one SRU to Resolute.
** Also affects: llvm-toolchain-19 (Ubuntu)
Importance: Undecided
Status: New
** Also affects: llvm-toolchain-20 (Ubuntu)
Importance: Undecided
Status: New
** Also affects: llvm-toolchain-21 (Ubuntu)
Importance: Undecided
Status: New
** Also affects: llvm-toolchain-22 (Ubuntu)
Importance: Undecided
Status: New
** Also affects: llvm-toolchain-18 (Ubuntu Stonking)
Importance: Low
Assignee: Ryan Carlson (ryancarlson12)
Status: In Progress
** Also affects: llvm-toolchain-19 (Ubuntu Stonking)
Importance: Undecided
Status: New
** Also affects: llvm-toolchain-20 (Ubuntu Stonking)
Importance: Undecided
Status: New
** Also affects: llvm-toolchain-21 (Ubuntu Stonking)
Importance: Undecided
Status: New
** Also affects: llvm-toolchain-22 (Ubuntu Stonking)
Importance: Undecided
Status: New
** Changed in: llvm-toolchain-19 (Ubuntu Resolute)
Assignee: (unassigned) => Ryan Carlson (ryancarlson12)
** Changed in: llvm-toolchain-19 (Ubuntu Stonking)
Assignee: (unassigned) => Ryan Carlson (ryancarlson12)
** Changed in: llvm-toolchain-20 (Ubuntu Resolute)
Assignee: (unassigned) => Ryan Carlson (ryancarlson12)
** Changed in: llvm-toolchain-20 (Ubuntu Stonking)
Assignee: (unassigned) => Ryan Carlson (ryancarlson12)
** Changed in: llvm-toolchain-21 (Ubuntu Resolute)
Assignee: (unassigned) => Ryan Carlson (ryancarlson12)
** Changed in: llvm-toolchain-21 (Ubuntu Stonking)
Assignee: (unassigned) => Ryan Carlson (ryancarlson12)
** Changed in: llvm-toolchain-22 (Ubuntu Resolute)
Assignee: (unassigned) => Ryan Carlson (ryancarlson12)
** Changed in: llvm-toolchain-22 (Ubuntu Stonking)
Assignee: (unassigned) => Ryan Carlson (ryancarlson12)
--
You received this bug notification because you are a member of Ubuntu
Bugs, which is subscribed to Ubuntu.
https://bugs.launchpad.net/bugs/2167986
Title:
qualify-clang.sh fails during autopkgtest: Z3 static analysis test
fails because Z3_FLAG is disabled for Ubuntu builds
To manage notifications about this bug go to:
https://bugs.launchpad.net/ubuntu/+source/llvm-toolchain-18/+bug/2167986/+subscriptions
--
ubuntu-bugs mailing list
[email protected]
https://lists.ubuntu.com/mailman/listinfo/ubuntu-bugs
