dioscc and divine cc explicitly undefine the __x86_64__ macro

[Lukáš Zaoral]

Hello, the following code is preprocessed differently than with other compilers (e.g. divcc (fixed in #76), clang, ...) when using dioscc or divine cc, therefore, Divine 4.3.6 gives a wrong verification result.

#include <stdio.h>

int main(void) {
    puts("Expecting a NULL pointer dereference...");
#ifdef __x86_64__
    int* a = NULL; 
    return *a;
#else
    puts("... and nothing happened.");
#endif
}

The __x68_64__ and __x86_64 macros are explicitly undefined in the "divine/rt/dios-cc.cpp" file. If this is an expected behaviour, could you please provide the reason for such decision? Thank you.

[mornfall]

We have discussed this in IRC, but the gist is: DiOS running on DiVM is not x86-64 and therefore should not set this macro. Checking architecture-specific code will need special precautions in either case: it is correct and expected that code uses this and related macros to guard inline assembly and other CPU-specific code which we can't correctly execute anyway (at least for the time being).

[Kamil Dudka]

"DiOS running on DiVM" is an implementation detail of Divine. As long as Divine is a tool that does formal verification of software, the tool has to over-approximate everything that cannot be modeled precisely enough. Otherwise it is unclear what Divine's answer CORRECT actually means for the user. One would expect that a correct program does not crash immediately after start, for example.

[Vladimír Štill]

Well, this is partly a problem of specification… if we disregard implementation details which are mostly not relevant to verification results, DIVINE is running the code as on a 64bit platform, not specifically x86-64. For this reason, the __x86_64__ macro is not set. Also, we do not support inline assembly, which is expected to work if __x86_64__ is defined. Similarry for code which assumes particular stack layout (e.g., varag implementation).

Most well-written programs which require platform-specific code should have some sort of catchall implementation or fail to compile when no platform-specific code is available (for example libc++ does that). Of course, this could mean DIVINE is analysing a different code than would run if compiled on the given platform.

Overall, I don't think this has a nice solution unless we can fully support x86-64 specifics, which would be a lot of hard work. As a work-around, if you know that no x86-64 specifics are used but the macro is only used to guard code intended for 64bit platforms, you can define the __x86_64__ macro manually in dioscc. Of course, if there is any inline assembly or code which assumes it really runs on x86-64, it will not work.

[Kamil Dudka]

My concern is not inline assembly or low-level access to stack layout. The most critical problem with this bug is that the __x86_64__ macro is used by <bits/wordsize.h>, which is commonly used by system header files of multilib-ready libraries. Lack of the __x86_64__ macro definition will cause Divine to run formal verification against different set of header files than the ones that are used for production builds. You should have a look at how multilib is implemented in Linux distros, e.g.:

​https://src.fedoraproject.org/rpms/multilib-rpm-config

I see no value in formal verification of code that is qualitatively different from what is being run in production. Please consider reopening this bug.

[mornfall]

I think there's a fundamental misunderstanding what DiOS is and how it works. DiOS provides its own headers: how macros like __x86_64__ are used in system headers has no effect on 'divine cc' or 'dioscc'. If you want to use system headers, you want to use 'divcc' instead. Both approaches have their downsides.

[Kamil Dudka]

The problem is that Red Hat needs formal verification tool that inputs source code from packages of a Linux distribution and that compiles (and understands) the code in the same way as the system compiler. I understand that dioscc cannot be used for this task. But divcc did not work for us either. That is why Lukáš spent non-trivial amount of time to make it work with dioscc.