Witness edge scope makes name resolving ambiguous

[JanSvejda]

extern void __VERIFIER_error();

static float one(float *foo){
    return *foo;
}

static float two(float *foo){
    return *foo;
}

float x = 0;

void step() {
    x = one(0);
}

int main(void) {
    while (1) {
        step();
        if (x == 0) {
            __VERIFIER_error();
        }
    }
    return 0;
}

CBMC version: 5.8, also tested on 5.11 with same results
Operating system: Ubuntu 18.04
Exact command line resulting in the issue: cbmc --32 --graphml-witness witness.graphml --unwindset main.0:1 --unwinding-assertions main.c
What behaviour did you expect: The scope of assumption "foo = ((float *)NULL);" in the witness should be 'one'.
What happened instead: Scope is 'step'. Assignment to parameter 'foo' is thus ambiguous, since there are two possibilities - either parameter of function 'one' or 'two'.

This behaviour produces 'unknown expression' warnings when I try to validate the witness with CPAChecker and also causes CPAChecker to ignore any of these assumptions in its validation procedure.

I think it might be a cause of why CBMC and CPAChecker disagree on results of verifications in a casy study I am doing where the witnesses from CBMC are validated with CPAChecker. I could have a look at fixing this myself if you would like, though if you pointed me in the right direction it would be much appreciated. I am not very familiar with CBMC sources.

On a slightly different note, the witnesses also contain symbols like NULL, NAN and INFINITY, which have to be replaced for CPAChecker to not give 'unkwnon expression' warnings. In C these are actually macros and not part of the language itself. I was wondering if this behaviour was deliberate.

Here is the source code and the output witness:
source_and_witness.zip

[tautschnig]

Thank you very much for this report! I'm afraid CBMC's GraphML output is in a rather messy state and certainly needs fixing. Your example may help us sort this out! There is #2001, a variation of which has again been used in SV-COMP'19 (see #3486) for some fixes, which might include the NULL/NAN/INFINITY bits. But it does need a lot of cleanup, and possibly also further fixes.

[tautschnig]

I have now included a fix for the scope problem in #2001. That PR also addresses problems with NULL. For NAN and INFINITY, however, I am wondering what could even be done: the GraphML witness specification forbids function calls in assumptions, but that's what NAN (__builtin_nanf("")) and INFINITY (__builtin_inff()) would expand to!?

[JanSvejda]

Wonderful, thank you very much for fixing the scope issue! Glad I could help.
About NULLs etc: when I was validating other witnesses, I changed all occurences of NULL to 0, NAN to 0.0/0.0 and INFINITY to 1.0/0.0, but these are rather hacky approaches and may not even be semantically correct.

[tautschnig]

Thanks @JanSvejda! @martin-cs Would you have some suggestions or comments on @JanSvejda's ideas for representing NAN and INFINITY?

[martin-cs]

@JanSvejda @tautschnig : they are indeed correct. I would suggest that you use names rather than expressions because, strictly speaking, the expressions trigger floating-point exceptions. IEEE-754 doesn't give specific names for these, nor does ISO 9899 because the link between float and double is optional so things like NaN and Inf are not guaranteed to exist.

[tautschnig]

Thanks @JanSvejda @martin-cs! I have added code to #2001 to generate output without those macros for GraphML (or in general when using the "clean" configuration of expr2ct).