Miscompilation after inexact pointer-equality check leads to dereference of incorrect capability

[martin-fink]

On CHERI RISC-V and Morello, the compiler performs an address-only capability equality check (p == q) and then treats the two capabilities p and q as interchangeable. This is incorrect under CHERI semantics with inexact equality checks: it should not imply that capabilities are substitutable. As a result, the compiler may dereference a capability with an invalid tag even though the source code dereferences a valid one. Example (Compiler Explorer link):

#include <stdint.h>
#include <stdio.h>
#include <stdlib.h>
#include <cheriintrin.h>

int main() {
    uint64_t *buf = (uint64_t *)aligned_alloc(64, 128);
    if (!buf) { perror("alloc"); return 1; }

    for (size_t i = 0; i < (128 / 8); i++) buf[i] = (uint64_t)i;

    const uint64_t *p = buf;
    const uint64_t *q = p;

    // p and q differ only in their tag
    p = cheri_tag_clear(p);

    // force compiler to treat p and q as unknown after this
    __asm__ volatile("" : "+C"(p), "+C"(q) : : "memory");

    uint64_t result = 0;
    if (p == q) {
        // this should succeed, since we access `q`. only `p` has a cleared tag bit.
        result = q[0];
    }

    printf("out=%llu\n", (unsigned long long)result);

    free(buf);
    return 0;
}

Expected behavior

• p == q evaluates to true
• q[0] succeeds, since q has a valid tag bit

Actual behavior

• p == q evaluates to true
• q[0] segfaults with optimizations on, succeeds with optimizations off.

Here is the generated code on Morello and RISCV:

        clrtag  c0, c19    # clear the tag in c0
        stp     q2, q3, [c19, #96]
        cmp     x0, x1
        b.eq    .LBB0_3
        mov     x8, xzr
        b       .LBB0_4
.LBB0_3:
        ldr     x8, [c0]   # use c0 (tag cleared) to load

        ccleartag       ca0, cs0  # clear tag
        cmove   ca2, cs0
        li      a1, 0
        bne     a0, a2, .LBB0_3
        ld      a1, 0(ca0)        # use ca0 (tag cleared) to load