runtimeverification / llvm-backend

KORE to llvm translation
BSD 3-Clause "New" or "Revised" License
36 stars 23 forks source link

Suboptimal type for kore_definition_syntax? #1115

Closed 0cjs closed 3 months ago

0cjs commented 3 months ago

In binds/c/lib.cpp, we have the following definitions:

/*
 * These symbols may not have been compiled into the library (if
 * `--embed-kprint` was not passed), and so we need to give them a weak default
 * definition. If the embed flag was passed, the value of these symbols will be
 * given by the embedded data.
 */
 char kore_definition_syntax __attribute__((weak)) = -1;
 char kore_definition_macros __attribute__((weak)) = -1;

Note that there's no indication of whether these are signed or unsigned.

However, later in the file we have:

if (kore_definition_macros_len == -1 || kore_definition_macros == -1
    || kore_definition_syntax_len == -1 || kore_definition_syntax == -1) {

These comparisons with -1 of course work only with signed chars, but on Linux aarch64 and Darwin arm64 platforms the default type of char is unsigned for clang (and perhaps the ABI). This produces (fortunately) an error due to the -Wall.

There appear to be no warnings we can turn on that will indicate that such non-portable code is being used. (We get a tautological-constant-out-of-range-compare only when compiling on aarch64/arm64 platforms.)

It looks as if this type is one we define internally, so perhaps this document might provide some guidance on a better type to choose?

(BTW, this makes the program uncompilable on Apple Silicon CPUs for both MacOS and Linux.)

0cjs commented 3 months ago

Appears to be fixed by #1116.