#include <stdio.h>
#include <stdint.h>
const char __attribute__((section(".text"))) vrot8[] = "WXfPPfXX\xc3";
int main() {
	uint64_t __attribute__((sysv_abi)) (*rotator)(uint64_t) = vrot8;
	uint64_t x = 0x123456789abcdef;
	printf("rot(%lx) = %lx\n", x, rotator(x));
	return 0;
}