Bug 238284 - math/z3: compile warnings on non-x86 systems
Summary: math/z3: compile warnings on non-x86 systems
Status: Open
Alias: None
Product: Ports & Packages
Classification: Unclassified
Component: Individual Port(s) (show other bugs)
Version: Latest
Hardware: arm64 Any
: --- Affects Only Me
Assignee: Gleb Popov
URL:
Keywords:
Depends on:
Blocks:
 
Reported: 2019-06-01 23:06 UTC by John F. Carr
Modified: 2019-07-18 09:14 UTC (History)
2 users (show)

See Also:
bugzilla: maintainer-feedback? (arrowd)


Attachments
Eliminate compile warnings on ARM64 (7.49 KB, patch)
2019-06-03 08:14 UTC, John F. Carr
no flags Details | Diff

Note You need to log in before you can comment on or make changes to this bug.
Description John F. Carr 2019-06-01 23:06:25 UTC
Building math/z3 on arm64 generates a lot of warnings, some of which are real bugs.  z3 is required by llvm-devel.

src/util/statistics.cpp
c++: warning: argument unused during compilation: '-msse' [-Wunused-command-line-argument]
c++: warning: argument unused during compilation: '-msse2' [-Wunused-command-line-argument]

The above is repeated for every file.  My ARM CPU does not have SSE or SSE2.  I suspect the culprit is scripts/mk_util.py function test_fpmath, which requests SSE flags unless they make the compiler return a non-zero exit code.

--- api/z3_replayer.o ---
../src/api/z3_replayer.cpp:172:19: warning: result of comparison of constant -1 with expression of type 'char' is always false [-Wtautological-constant-out-of-range-compare]
            if (c == EOF) {
                ~ ^  ~~~
../src/api/z3_replayer.cpp:417:19: warning: result of comparison of constant -1 with expression of type 'char' is always false [-Wtautological-constant-out-of-range-compare]
            if (c == EOF)
                ~ ^  ~~~

--- parsers/util/scanner.o ---
../src/parsers/util/scanner.cpp:65:35: warning: result of comparison of constant -1 with expression of type 'char' is always false [-Wtautological-constant-out-of-range-compare]
        if (delimiter == ch || -1 == ch) {
                               ~~ ^  ~~
../src/parsers/util/scanner.cpp:76:16: warning: result of comparison of constant -1 with expression of type 'char' is always false [-Wtautological-constant-out-of-range-compare]
        if (ch == EOF) {
            ~~ ^  ~~~
../src/parsers/util/scanner.cpp:191:24: warning: result of comparison of constant -1 with expression of type 'char' is always false [-Wtautological-constant-out-of-range-compare]
                if (ch == EOF) {
                    ~~ ^  ~~~
../src/parsers/util/scanner.cpp:249:35: warning: result of comparison of constant -1 with expression of type 'char' is always false [-Wtautological-constant-out-of-range-compare]
        if (ch == delimiter || ch == EOF) {
                               ~~ ^  ~~~
4 warnings generated.

../src/smt/mam.cpp:97:36: warning: result of comparison of constant -1 with expression of type 'char' is always false [-Wtautological-constant-out-of-range-compare]
            if (m_lbl2hash[lbl_id] == -1) {
                ~~~~~~~~~~~~~~~~~~ ^  ~~
../src/smt/mam.cpp:108:35: warning: result of comparison of constant -1 with expression of type 'const char' is always true [-Wtautological-constant-out-of-range-compare]
                if (m_lbl2hash[i] != -1) {
                    ~~~~~~~~~~~~~ ^  ~~

These say the programmer never imagined that type char could be unsigned.
Comment 1 Kubilay Kocak freebsd_committer freebsd_triage 2019-06-02 03:29:41 UTC
Thank you for your report John

These kinds of issues are great candidates to report upstream as a first step, which appears quite receptive to fixing these issues [1].

Could you open an issue upstream [2] to have this resolved?


[1] https://github.com/Z3Prover/z3/issues/1130#issuecomment-312948353
[2] https://github.com/Z3Prover/z3/issues
Comment 2 Nikolaj Bjorner 2019-06-02 23:05:42 UTC
The current build CI pipelines that we use don't give me a way to easily validate fixes to this, but I have pushed what is hopefully fixes to the EOF errors.

Regarding the sse warnings, I would appreciate help. The utility test_fpmath in scripts/mk_util.py under the Z3 sources is almost for sure the culprit. So I believe the approach to fix this is by adapting this test. 
Note that there are two alternative ways of building Z3: (1) using the python based build system by running scripts/mk_make.py, or (2) using cmake based system. For the CMake based system the configuration of sse is under the root directory in CMakeLists.txt. The CMake based build system is in many ways nicer than the legacy python based system, but I am unable to fully deprecate the legacy system at this point. The sse relevant code is:

https://github.com/Z3Prover/z3/blob/master/scripts/mk_util.py#L294

and for cmake:

https://github.com/Z3Prover/z3/blob/master/CMakeLists.txt#L329
Comment 3 Gleb Popov freebsd_committer 2019-06-03 07:32:51 UTC
(In reply to Nikolaj Bjorner from comment #2)

> The current build CI pipelines that we use don't give me a way to easily validate fixes to this, but I have pushed what is hopefully fixes to the EOF errors.

Whoa, it is unexpected to meet upstream devs here. Thanks for feedback&fixes.

(In reply to John F. Carr from comment #0)

Do you want me to pull these patches into FreeBSD port, or we can just wait for the next Z3 release?
Comment 4 John F. Carr 2019-06-03 08:14:37 UTC
Created attachment 204797 [details]
Eliminate compile warnings on ARM64

This is an updated diff (including the existing ports diff) to eliminate the compile warnings.  I sent it upstream already.  I only tested it on ARM64.

In general the assumption that char is signed has the potential to lead to infinite loops because EOF is never recognized.  I don't know if it does in z3 in particular -- if character 255 is invalid for some reason the consequence is an incorrect error instead of an infinite loop.
Comment 5 Gleb Popov freebsd_committer 2019-07-18 09:14:39 UTC
I see parts of this patch are applied upstream, but some changes are left out. For instance, this hunk:

-- src/parsers/util/scanner.h	2018-12-20 13:32:36.000000000 -0500
+++ src/parsers/util/scanner.h	2019-06-02 19:19:59.921462000 -0400
@@ -71,13 +71,13 @@ 
     buffer<char>       m_buffer;
     unsigned           m_bpos;
     unsigned           m_bend;
-    char               m_last_char;
+    int                m_last_char;
     bool               m_is_interactive;
     bool               m_smt2;
     bool               m_bv_token;
 
-    char read_char();
-    token read_symbol(char ch);
+    int read_char();
+    token read_symbol(int ch);

@Nikolaj Bjorner, did you skip it deliberately?