Public bug reported:

[ Description ]

* This bug was found on Ubuntu 26.04 LTS for llvm-toolchain-18

* 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@

* 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


[ 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.


[ 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.

** Affects: llvm-toolchain-18 (Ubuntu)
     Importance: Undecided
     Assignee: Ryan Carlson (ryancarlson12)
         Status: New

-- 
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

Reply via email to