Bug 238284
| Summary: | math/z3: compile warnings on non-x86 systems | ||||||
|---|---|---|---|---|---|---|---|
| Product: | Ports & Packages | Reporter: | John F. Carr <jfc> | ||||
| Component: | Individual Port(s) | Assignee: | Gleb Popov <arrowd> | ||||
| Status: | Closed FIXED | ||||||
| Severity: | Affects Only Me | CC: | linimon, nbjorner | ||||
| Priority: | --- | Flags: | bugzilla:
maintainer-feedback?
(arrowd) |
||||
| Version: | Latest | ||||||
| Hardware: | arm64 | ||||||
| OS: | Any | ||||||
| Attachments: |
|
||||||
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 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 (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? 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.
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?
Is this PR still relevant? All mentioned issue seem to be fixed upstream. |
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.