Silent transformation of __CPROVER_{r,w,rw}_ok causing surprising behaviour

[tautschnig]

Posting an analysis by @nwetzler, @jimgrundy and @remi-delmas-3000 The attached a gzipped tarball contains a single C file and a script to demonstrate the problem.

The following function takes a single pointer and asserts that it is read/write okay:

void foo (char* x) {
    __CPROVER_assert(__CPROVER_rw_ok(x, 1), "");
    return;
}

We can compile this to goto (to create a.out) and then run goto-instrument on the resulting binary to create a new binary (which is b.out). Off the bat, you’ll notice that the size of these two binaries is different. However, if you show-goto-functions or program-only (for the SSA) and compare the two, they will be identical.

But if you now enable pointer-check and pointer-primitive-check, you’ll see that they produce different show-goto-functions and program-only output. Furthermore, we think the assertions produced by the checks are even semantically different between the two, which seems like a bug in CBMC.

83c83
<         ASSERT pointer_object(NULL) = pointer_object(foo::x) ∨ ¬(is_invalid_pointer(foo::x)) // pointer invalid in RW_OK(x, (unsigned long int)1)
---
>         ASSERT (¬(pointer_object(foo::x) = pointer_object(NULL)) ∧ ¬(is_invalid_pointer(foo::x)) ∧ ¬(pointer_object(foo::x) = pointer_object(__CPROVER_deallocated)) ∧ ¬(pointer_object(foo::x) = pointer_object(__CPROVER_dead_object)) ∧ pointer_offset(foo::x) ≥ 0) ⇒ (pointer_object(NULL) = pointer_object(foo::x) ∨ ¬(is_invalid_pointer(foo::x))) // pointer invalid in OBJECT_SIZE(x)

Several issues appear to arise:

1. There isn't actually a way to just dump the contents of a GOTO binary for goto-instrument will always call into instrumentation steps.
2. Just like you cannot just dump a GOTO binary, running goto-instrument a.out b.out will perform transformations despite no such transformation being requested.
3. A particular example of such a transformation (maybe the only one, maybe there are others) is the expansion of __CPROVER_{r,w,rw}_ok that goto_check_ct does (irrespective of whether a property instrumentation was requested).
4. goto_check_ct is not idempotent: doing one round of goto_check_ct followed by another with --pointer-primitive-check enabled is not the same as doing just one round of goto_check_ct with --pointer-primitive-check enabled.

[jimgrundy]

There is some urgency to this one as it looks like the extra complication introduced into the assertion is part of a performance problem we are seeing (in a more complex example, of course). Removing this complication is important.

[remi-delmas-3000]

the related issue is decribed here : #7378

[tautschnig]

I started to work on the issues noticed in here (as well as in #7378). #7395 should be part of the puzzle (once complete). I am still trying to figure out, however, what is really causing this performance problem (the issues listed in this ticket are to be addressed, but don't necessarily explain why performance should be so much worse).

[jimgrundy]

Can we get a status update?