Bug: Memcpy with #memory_int and #memory_real present

[jankoerner]

Basic Info

• Commit: 0f2a44d (currently dev)
• Input file:

int main() { 
    int* i = (int*) malloc(sizeof(int));
    *i = 42;
    
    int* i2 = (int*) malloc(sizeof(int));
    memcpy(i2, i, sizeof(int));
    assert(*i2 == 42);

    float* f1 = (float*) malloc(sizeof(float));
    *f1 = 44.0;
    
    return 0;
}

• Settings: settings.txt
• Toolchain: toolchain.txt
• Logs: violation-log.txt, holds-log.txt

Description

Given the following program, I would assume that both asserts hold, however Ultimate reports that assert(i2 == 42) can be violated.

What's interesting is the fact, that Ultimate reports that this assert(*i2 == 42) holds, if the malloc of the floating point is removed.
I assume that this problem might be related to the fact, that the floating point allocation introduces the #memory_real map into the Boogie code, which then leads to #Ultimate.C_memcpy writing to #memory_int and #memory_real.

[maul-esel]

Thank you @jankoerner for reporting this issue.

Your suspicion seems to be correct. Although it gets even a bit funnier: I just ran the verification on your program 15 times, and in 9 cases, a counterexample was found, but in the other 6 cases, the program was declared to be correct. 🙃

---

It seems our implementation of C_memcpy is quite incorrect:

implementation #Ultimate.C_memcpy(dest : $Pointer$, src : $Pointer$, size : int) returns (#res : $Pointer$){
    var #t~loopctr6 : int;

    #t~loopctr6 := 0;
    while (#t~loopctr6 % 18446744073709551616 < size % 18446744073709551616)
    {
        call write~unchecked~int(#memory_int[{ base: src!base, offset: src!offset + #t~loopctr6 }], { base: dest!base, offset: dest!offset + #t~loopctr6 }, 4);
        call write~unchecked~real(#memory_real[{ base: src!base, offset: src!offset + #t~loopctr6 }], { base: dest!base, offset: dest!offset + #t~loopctr6 }, 4);
        #t~loopctr6 := 1 + #t~loopctr6;
    }
}

procedure write~unchecked~real(#value : real, #ptr : $Pointer$, #sizeOfWrittenType : int) returns ();
ensures #memory_real == old(#memory_real)[#ptr := #value] && #memory_int == old(#memory_int)[#ptr := #memory_int[#ptr]];
modifies #memory_real, #memory_int;

procedure write~unchecked~int(#value : int, #ptr : $Pointer$, #sizeOfWrittenType : int) returns ();
ensures #memory_real == old(#memory_real)[#ptr := #memory_real[#ptr]] && #memory_int == old(#memory_int)[#ptr := #value];
modifies #memory_real, #memory_int;

This first reads the source value from #memory_int and copies it to the destination position in #memory_int, while nondeterministically changing the destination position in #memory_real. Then it reads the source value from #memory_real and copies it to the destination position in #memory_real, while nondeterministically changing the destination position in #memory_int.

The latter nondeterministic change leads to the loss of the correct value (which had just been copied there).

---

I suspect the fact that the verdict is sometimes correct and sometimes wrong is due to a nondeterminism-bug in Ultimate that changes the order in which the two memory arrays are updated.

---

The solution should be a C_memcpy implementation that avoids these nondeterministic updates.