Behavior differs from x86-64 binary about emscripten

[sbc100]

If possible, I think think would be a lot more actionable if you could narrow this down. In doing so you could also reveal more about the divergence.

[mkarup]

Sorry for the late, late reply.
It seems to happen when trying to pretty print anything that is an in-memory data structure (using pointers) (which is basically what CertiCoq translates a Coq inductive data types like list to).

If I compile with emcc and add -fsanitize=undefined and -sSAFE_HEAP I get

load of misaligned address 0x00046ea4 for type 'unsigned long long', which requires 8 byte alignment
0x000471e4: note: pointer points here
  b4 71 04 00 d4 71 04 00  00 08 00 00 a4 71 04 00  e0 71 04 00 00 00 00 00  00 00 00 00 00 00 00 00
              ^ 
Aborted(alignment fault)

The load happens in this function:

unsigned long long get_boxed_ordinal(value $v)
{
  return (unsigned long long) *((unsigned long long *) $v + -1LL) & 255LL;
}

value is typedef'd as int64_t.

Compiling the C code with clang also with -fsanitize=undefined (and no optimizations) and running it doesn't give me an error.

If I add -O1 when compiling with emcc, along with -fsanitize=undefined and -sSAFE_HEAP I still get the error about the misaligned load from the sanitizer, but it doesn't abort and it pretty prints correctly.

[sbc100]

Unaligned accesses are allowed in Wasm, so you can use -sSAFE_HEAP=2 to ignore the alignment fault.