#include <stdio.h>
#include <stdint.h>
char *__attribute__((section(".text"))) rot = "fhUUfhUUfhUUfhUUTZWXPPH+\"H+\"H+\"XH+\"H+\"H+\"H+\"H+\"H+\"H+\"H+\"H+\"H+\"H+\"H+\"H+\"H+\"H+\"H+\"H+\"H+\"H+\"H+\"H+\"Z\xc3";
int main() {
    uint64_t __attribute__((sysv_abi)) (* rotator)(uint64_t) = (void *)rot;
    uint64_t x = 0x123456789abcdef;
    printf("rot(%lx) = %lx\n", x, rotator(x));
    return 0;
}