diff mbox series

[bug#56107] : Update z3 to 4.8.17 and use cmake to build the package.

Message ID 86fsjyv3bc.fsf@163.com
State New
Headers show
Series [bug#56107] : Update z3 to 4.8.17 and use cmake to build the package. | expand

Checks

Context Check Description
cbaines/applying patch fail View Laminar job
cbaines/issue success View issue

Commit Message

Zhu Zihao June 21, 2022, 8:16 a.m. UTC
Thanks, patches updated.

Comments

Ludovic Courtès July 2, 2022, 11:40 p.m. UTC | #1
Hi!

The series LGTM, but unfortunately the upgrade breaks one dependent,
‘solidity’:

--8<---------------cut here---------------start------------->8---
--- SKIPPING ALL SEMANTICS TESTS ---

Running 4839 test cases...

0%   10   20   30   40   50   60   70   80   90   100%
|----|----|----|----|----|----|----|----|----|----|
*********************************************/solidity/test/boostTest.cpp(114): error: in "smtCheckerTests/loops/while_loop_array_assignment_storage_storage": Test expectation mismatch.
Expected result:
  Warning 6328: (290-309): CHC: Assertion violation happens here.
  Warning 6328: (313-332): CHC: Assertion violation happens here.
Obtained result:
  Warning 6328: (290-309): CHC: Assertion violation happens here.
  Warning 6328: (313-332): CHC: Assertion violation happens here.
  Warning 4661: (266-286): BMC: Assertion violation happens here.

/solidity/test/boostTest.cpp(114): error: in "smtCheckerTests/loops/for_1_false_positive": Test expectation mismatch.
Expected result:
  Warning 2661: (176-181): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.
Obtained result:
  Warning 2661: (176-181): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.
  Warning 4661: (296-309): BMC: Assertion violation happens here.

*/solidity/test/boostTest.cpp(114): error: in "smtCheckerTests/crypto/crypto_functions_compare_hashes": Test expectation mismatch.
Expected result:
  Warning 6328: (183-197): CHC: Assertion violation happens here.
  Warning 6328: (201-215): CHC: Assertion violation happens here.
  Warning 6328: (219-233): CHC: Assertion violation happens here.
Obtained result:
  Warning 1218: (183-197): CHC: Error trying to invoke SMT solver.
  Warning 1218: (201-215): CHC: Error trying to invoke SMT solver.
  Warning 1218: (219-233): CHC: Error trying to invoke SMT solver.
  Warning 4661: (183-197): BMC: Assertion violation happens here.
  Warning 4661: (201-215): BMC: Assertion violation happens here.
  Warning 4661: (219-233): BMC: Assertion violation happens here.

/solidity/test/boostTest.cpp(114): error: in "smtCheckerTests/crypto/crypto_functions_not_same": Test expectation mismatch.
Expected result:
  Warning 6328: (229-243): CHC: Assertion violation happens here.
Obtained result:
  Warning 1218: (229-243): CHC: Error trying to invoke SMT solver.
  Warning 4661: (229-243): BMC: Assertion violation happens here.
  Warning 4661: (229-243): BMC: Assertion violation happens here.

**/solidity/test/boostTest.cpp(114): error: in "smtCheckerTests/operators/compound_bitwise_or_uint_2": Test expectation mismatch.
Expected result:
  Warning 7812: (173-192): BMC: Assertion violation might happen here.
Obtained result:
  Warning 6328: (173-192): CHC: Assertion violation happens here.

*/solidity/test/boostTest.cpp(114): error: in "smtCheckerTests/operators/slice_default_start": Test expectation mismatch.
Expected result:
  Warning 6328: (193-225): CHC: Assertion violation happens here.
  Warning 4661: (157-189): BMC: Assertion violation happens here.
Obtained result:
  Warning 4661: (157-189): BMC: Assertion violation happens here.
  Warning 4661: (193-225): BMC: Assertion violation happens here.

**

*** 6 failures are detected in the test module "SolidityTests"
error: in phase 'check': uncaught exception:
%exception #<&invoke-error program: "./scripts/tests.sh" arguments: () exit-status: 1 term-signal: #f stop-signal: #f> 
phase `check' failed after 656.5 seconds
command "./scripts/tests.sh" failed with status 1
builder for `/gnu/store/g69say6c7vqvk15p8jark6l3m4k6z7bg-solidity-0.7.4.drv' failed with exit code 1
build of /gnu/store/g69say6c7vqvk15p8jark6l3m4k6z7bg-solidity-0.7.4.drv failed
--8<---------------cut here---------------end--------------->8---

Thoughts?

Ludo’.
diff mbox series

Patch

From e1df674d84fe5a26a343a2ea68ea961d045dffe8 Mon Sep 17 00:00:00 2001
From: Zhu Zihao <all_but_last@163.com>
Date: Mon, 20 Jun 2022 20:17:54 +0800
Subject: [PATCH 3/3] gnu: z3: Prefer CMake to build the package.

Z3 developer recommends to use CMake to build Z3 except the OCaml bindings.
Use CMake also enable us to cross compile z3.

* gnu/packages/maths.scm (z3)[build-system]: Use cmake-build-system.
[arguments]<#:configure-flags>: Add flags for CMake.
<#:phases>: Remove stale phase 'fix-compatability'.
In phase 'check', build the z3 test binary and don't test when cross
compiling.
Add phase 'compile-python-modules' phase to generate python bytecode cache for
z3 python binding.
Add phase 'fix-z3-library-path' to help z3 pythong binding to find the z3
shared library.

(ocaml-z3)[build-system]: Override the inherited value with 'gnu-build-system'.
---
 gnu/packages/maths.scm | 64 ++++++++++++++++++++----------------------
 1 file changed, 31 insertions(+), 33 deletions(-)

diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm
index 2f1f731890..a73dfdb809 100644
--- a/gnu/packages/maths.scm
+++ b/gnu/packages/maths.scm
@@ -5827,8 +5827,8 @@  (define-public z3
               (file-name (git-file-name name version))
               (sha256
                (base32
-    (build-system gnu-build-system)
                 "1vvb09q7w7zd29qc4qjysrrhyylszm1wf6azkff004ixwn026b05"))))
+    (build-system cmake-build-system)
     (arguments
      (list
       #:imported-modules `((guix build python-build-system)
@@ -5836,43 +5836,40 @@  (define-public z3
       #:modules '((guix build cmake-build-system)
                   (guix build utils)
                   ((guix build python-build-system) #:select (site-packages)))
+      #:configure-flags
+      #~(list "-DZ3_BUILD_PYTHON_BINDINGS=ON"
+              "-DZ3_LINK_TIME_OPTIMIZATION=ON"
+              (string-append
+               "-DCMAKE_INSTALL_PYTHON_PKG_DIR="
+               #$output "/lib/python"
+               #$(version-major+minor (package-version python-wrapper))
+               "/site-packages"))
       #:phases
       #~(modify-phases %standard-phases
-          (add-after 'unpack 'enable-bytecode-determinism
+          (replace 'check
+            (lambda* (#:key parallel-build? tests? #:allow-other-keys)
+              (when tests?
+                (invoke "make" "test-z3"
+                        (format #f "-j~a"
+                                (if parallel-build?
+                                    (parallel-job-count)
+                                    1)))
+                (invoke "./test-z3" "/a"))))
+          (add-after 'install 'compile-python-modules
             (lambda _
               (setenv "PYTHONHASHSEED" "0")
-              #t))
-          (add-after 'unpack 'fix-compatability
-            ;; Versions after 4.8.3 have immintrin.h IFDEFed for Windows only.
-            (lambda _
-              (substitute* "src/util/mpz.cpp"
-                (("#include <immintrin.h>") ""))
-              #t))
-          (add-before 'configure 'bootstrap
-            (lambda _
-              (invoke "python" "scripts/mk_make.py")))
-          ;; work around gnu-build-system's setting --enable-fast-install
-          ;; (z3's `configure' is a wrapper around the above python file,
-          ;; which fails when passed --enable-fast-install)
-          (replace 'configure
+
+              (invoke "python" "-m" "compileall"
+                      "--invalidation-mode=unchecked-hash"
+                      #$output)))
+          ;; This step is missing in the CMake build system, do it here.
+          (add-after 'compile-python-modules 'fix-z3-library-path
             (lambda* (#:key inputs outputs #:allow-other-keys)
-              (invoke "./configure"
-                      "--python"
-                      (string-append "--prefix=" (assoc-ref outputs "out"))
-                      (string-append "--pypkgdir=" (site-packages inputs outputs)))))
-          (add-after 'configure 'change-directory
-            (lambda _
-              (chdir "build")
-              #t))
-          (add-before 'check 'make-test-z3
-            (lambda _
-              ;; Build the test suite executable.
-              (invoke "make" "test-z3" "-j"
-                      (number->string (parallel-job-count)))))
-          (replace 'check
-            (lambda _
-              ;; Run all the tests that don't require arguments.
-              (invoke "./test-z3" "/a"))))))
+              (let* ((dest (string-append (site-packages inputs outputs)
+                                          "/z3/lib/libz3.so"))
+                     (z3-lib (string-append #$output "/lib/libz3.so")))
+                (mkdir-p (dirname dest))
+                (symlink z3-lib dest)))))))
     (native-inputs
      (list which python-wrapper))
     (synopsis "Theorem prover")
@@ -5884,6 +5881,7 @@  (define-public ocaml-z3
   (package
     (inherit z3)
     (name "ocaml-z3")
+    (build-system gnu-build-system)
     (arguments
      `(#:imported-modules ((guix build python-build-system)
                            ,@%gnu-build-system-modules)
-- 
2.36.1