Behavior differs from x86-64 binary

[mkarup]

I have some C code generated through the CertiCoq project and the behavior (printed result) of running the Wasm module via the generated js scaffolding (w/ node v.20.12.2) differs from the output of running the x86-64 binary (compiled w/ clang v.17.0.6).

The code is supposed to prettyprint a functional list of booleans (result of the Coq expression List.app (List.repeat true 500) (List.repeat false 300) in s-expression form.

I have attached a zip with the C files needed for running the emcc command:
demo1.zip

Output of running the x86-64 binary:

Time taken 0.000104 seconds 0.104000 milliseconds
(cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons true (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false (cons false nil))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))

Output of running the Wasm module through node via the generated js scaffolding:

Time taken 0.017000 seconds 17.000000 milliseconds
nil

If I add the -O1 optimization flag, the correct result is printed.

Emscripten version:

emcc (Emscripten gcc/clang-like replacement + linker emulating GNU ld) 3.1.58 (a41843e0860e52c948c1fce20307933c6631c800)
clang version 19.0.0git (https:/github.com/llvm/llvm-project 0a8cd1ed1f4f35905df318015b0dbcb69d81d7c2)
Target: wasm32-unknown-emscripten
Thread model: posix

Full command:

emcc -v -O0 -o demo1-opt_O0.js -w -Wno-everything -I./ demo1_main_wasm.c gc_stack.c CertiCoq.Benchmarks.tests.demo1.c glue_demo1.c -sALLOW_MEMORY_GROWTH=1 -sSTACK_SIZE=1000000 --profiling

Output:

 /home/martin/code/emsdk/upstream/bin/clang -target wasm32-unknown-emscripten -fignore-exceptions -fvisibility=default -mllvm -combiner-global-alias-analysis=false -mllvm -enable-emscripten-sjlj -mllvm -disable-lsr --sysroot=/home/martin/code/emsdk/upstream/emscripten/cache/sysroot -DEMSCRIPTEN -Werror=implicit-function-declaration -Xclang -iwithsysroot/include/fakesdl -Xclang -iwithsysroot/include/compat -v -O0 -w -Wno-everything -I./ demo1_main_wasm.c -c -o /tmp/emscripten_temp_v2coerxi/demo1_main_wasm_0.o
clang version 19.0.0git (https:/github.com/llvm/llvm-project 0a8cd1ed1f4f35905df318015b0dbcb69d81d7c2)
Target: wasm32-unknown-emscripten
Thread model: posix
InstalledDir: /home/martin/code/emsdk/upstream/bin
 (in-process)
 "/home/martin/code/emsdk/upstream/bin/clang-19" -cc1 -triple wasm32-unknown-emscripten -emit-obj -mrelax-all -disable-free -clear-ast-before-backend -disable-llvm-verifier -discard-value-names -main-file-name demo1_main_wasm.c -mrelocation-model static -mframe-pointer=none -ffp-contract=on -fno-rounding-math -mconstructor-aliases -target-cpu generic -debugger-tuning=gdb -fdebug-compilation-dir=/home/martin/Documents -v -fcoverage-compilation-dir=/home/martin/Documents -resource-dir /home/martin/code/emsdk/upstream/lib/clang/19 -D EMSCRIPTEN -I ./ -isysroot /home/martin/code/emsdk/upstream/emscripten/cache/sysroot -internal-isystem /home/martin/code/emsdk/upstream/lib/clang/19/include -internal-isystem /home/martin/code/emsdk/upstream/emscripten/cache/sysroot/include/wasm32-emscripten -internal-isystem /home/martin/code/emsdk/upstream/emscripten/cache/sysroot/include -O0 -Werror=implicit-function-declaration -Wno-everything -w -ferror-limit 19 -fvisibility=default -fgnuc-version=4.2.1 -fskip-odr-check-in-gmf -fignore-exceptions -fcolor-diagnostics -iwithsysroot/include/fakesdl -iwithsysroot/include/compat -mllvm -combiner-global-alias-analysis=false -mllvm -enable-emscripten-sjlj -mllvm -disable-lsr -o /tmp/emscripten_temp_v2coerxi/demo1_main_wasm_0.o -x c demo1_main_wasm.c
clang -cc1 version 19.0.0git based upon LLVM 19.0.0git default target x86_64-unknown-linux-gnu
ignoring nonexistent directory "/home/martin/code/emsdk/upstream/emscripten/cache/sysroot/include/wasm32-emscripten"
#include "..." search starts here:
#include <...> search starts here:
 .
 /home/martin/code/emsdk/upstream/emscripten/cache/sysroot/include/fakesdl
 /home/martin/code/emsdk/upstream/emscripten/cache/sysroot/include/compat
 /home/martin/code/emsdk/upstream/lib/clang/19/include
 /home/martin/code/emsdk/upstream/emscripten/cache/sysroot/include
End of search list.
 /home/martin/code/emsdk/upstream/bin/clang -target wasm32-unknown-emscripten -fignore-exceptions -fvisibility=default -mllvm -combiner-global-alias-analysis=false -mllvm -enable-emscripten-sjlj -mllvm -disable-lsr --sysroot=/home/martin/code/emsdk/upstream/emscripten/cache/sysroot -DEMSCRIPTEN -Werror=implicit-function-declaration -Xclang -iwithsysroot/include/fakesdl -Xclang -iwithsysroot/include/compat -v -O0 -w -Wno-everything -I./ gc_stack.c -c -o /tmp/emscripten_temp_v2coerxi/gc_stack_1.o
clang version 19.0.0git (https:/github.com/llvm/llvm-project 0a8cd1ed1f4f35905df318015b0dbcb69d81d7c2)
Target: wasm32-unknown-emscripten
Thread model: posix
InstalledDir: /home/martin/code/emsdk/upstream/bin
 (in-process)
 "/home/martin/code/emsdk/upstream/bin/clang-19" -cc1 -triple wasm32-unknown-emscripten -emit-obj -mrelax-all -disable-free -clear-ast-before-backend -disable-llvm-verifier -discard-value-names -main-file-name gc_stack.c -mrelocation-model static -mframe-pointer=none -ffp-contract=on -fno-rounding-math -mconstructor-aliases -target-cpu generic -debugger-tuning=gdb -fdebug-compilation-dir=/home/martin/Documents -v -fcoverage-compilation-dir=/home/martin/Documents -resource-dir /home/martin/code/emsdk/upstream/lib/clang/19 -D EMSCRIPTEN -I ./ -isysroot /home/martin/code/emsdk/upstream/emscripten/cache/sysroot -internal-isystem /home/martin/code/emsdk/upstream/lib/clang/19/include -internal-isystem /home/martin/code/emsdk/upstream/emscripten/cache/sysroot/include/wasm32-emscripten -internal-isystem /home/martin/code/emsdk/upstream/emscripten/cache/sysroot/include -O0 -Werror=implicit-function-declaration -Wno-everything -w -ferror-limit 19 -fvisibility=default -fgnuc-version=4.2.1 -fskip-odr-check-in-gmf -fignore-exceptions -fcolor-diagnostics -iwithsysroot/include/fakesdl -iwithsysroot/include/compat -mllvm -combiner-global-alias-analysis=false -mllvm -enable-emscripten-sjlj -mllvm -disable-lsr -o /tmp/emscripten_temp_v2coerxi/gc_stack_1.o -x c gc_stack.c
clang -cc1 version 19.0.0git based upon LLVM 19.0.0git default target x86_64-unknown-linux-gnu
ignoring nonexistent directory "/home/martin/code/emsdk/upstream/emscripten/cache/sysroot/include/wasm32-emscripten"
#include "..." search starts here:
#include <...> search starts here:
 .
 /home/martin/code/emsdk/upstream/emscripten/cache/sysroot/include/fakesdl
 /home/martin/code/emsdk/upstream/emscripten/cache/sysroot/include/compat
 /home/martin/code/emsdk/upstream/lib/clang/19/include
 /home/martin/code/emsdk/upstream/emscripten/cache/sysroot/include
End of search list.
 /home/martin/code/emsdk/upstream/bin/clang -target wasm32-unknown-emscripten -fignore-exceptions -fvisibility=default -mllvm -combiner-global-alias-analysis=false -mllvm -enable-emscripten-sjlj -mllvm -disable-lsr --sysroot=/home/martin/code/emsdk/upstream/emscripten/cache/sysroot -DEMSCRIPTEN -Werror=implicit-function-declaration -Xclang -iwithsysroot/include/fakesdl -Xclang -iwithsysroot/include/compat -v -O0 -w -Wno-everything -I./ CertiCoq.Benchmarks.tests.demo1.c -c -o /tmp/emscripten_temp_v2coerxi/CertiCoq.Benchmarks.tests.demo1_2.o
clang version 19.0.0git (https:/github.com/llvm/llvm-project 0a8cd1ed1f4f35905df318015b0dbcb69d81d7c2)
Target: wasm32-unknown-emscripten
Thread model: posix
InstalledDir: /home/martin/code/emsdk/upstream/bin
 (in-process)
 "/home/martin/code/emsdk/upstream/bin/clang-19" -cc1 -triple wasm32-unknown-emscripten -emit-obj -mrelax-all -disable-free -clear-ast-before-backend -disable-llvm-verifier -discard-value-names -main-file-name CertiCoq.Benchmarks.tests.demo1.c -mrelocation-model static -mframe-pointer=none -ffp-contract=on -fno-rounding-math -mconstructor-aliases -target-cpu generic -debugger-tuning=gdb -fdebug-compilation-dir=/home/martin/Documents -v -fcoverage-compilation-dir=/home/martin/Documents -resource-dir /home/martin/code/emsdk/upstream/lib/clang/19 -D EMSCRIPTEN -I ./ -isysroot /home/martin/code/emsdk/upstream/emscripten/cache/sysroot -internal-isystem /home/martin/code/emsdk/upstream/lib/clang/19/include -internal-isystem /home/martin/code/emsdk/upstream/emscripten/cache/sysroot/include/wasm32-emscripten -internal-isystem /home/martin/code/emsdk/upstream/emscripten/cache/sysroot/include -O0 -Werror=implicit-function-declaration -Wno-everything -w -ferror-limit 19 -fvisibility=default -fgnuc-version=4.2.1 -fskip-odr-check-in-gmf -fignore-exceptions -fcolor-diagnostics -iwithsysroot/include/fakesdl -iwithsysroot/include/compat -mllvm -combiner-global-alias-analysis=false -mllvm -enable-emscripten-sjlj -mllvm -disable-lsr -o /tmp/emscripten_temp_v2coerxi/CertiCoq.Benchmarks.tests.demo1_2.o -x c CertiCoq.Benchmarks.tests.demo1.c
clang -cc1 version 19.0.0git based upon LLVM 19.0.0git default target x86_64-unknown-linux-gnu
ignoring nonexistent directory "/home/martin/code/emsdk/upstream/emscripten/cache/sysroot/include/wasm32-emscripten"
#include "..." search starts here:
#include <...> search starts here:
 .
 /home/martin/code/emsdk/upstream/emscripten/cache/sysroot/include/fakesdl
 /home/martin/code/emsdk/upstream/emscripten/cache/sysroot/include/compat
 /home/martin/code/emsdk/upstream/lib/clang/19/include
 /home/martin/code/emsdk/upstream/emscripten/cache/sysroot/include
End of search list.
 /home/martin/code/emsdk/upstream/bin/clang -target wasm32-unknown-emscripten -fignore-exceptions -fvisibility=default -mllvm -combiner-global-alias-analysis=false -mllvm -enable-emscripten-sjlj -mllvm -disable-lsr --sysroot=/home/martin/code/emsdk/upstream/emscripten/cache/sysroot -DEMSCRIPTEN -Werror=implicit-function-declaration -Xclang -iwithsysroot/include/fakesdl -Xclang -iwithsysroot/include/compat -v -O0 -w -Wno-everything -I./ glue_demo1.c -c -o /tmp/emscripten_temp_v2coerxi/glue_demo1_3.o
clang version 19.0.0git (https:/github.com/llvm/llvm-project 0a8cd1ed1f4f35905df318015b0dbcb69d81d7c2)
Target: wasm32-unknown-emscripten
Thread model: posix
InstalledDir: /home/martin/code/emsdk/upstream/bin
 (in-process)
 "/home/martin/code/emsdk/upstream/bin/clang-19" -cc1 -triple wasm32-unknown-emscripten -emit-obj -mrelax-all -disable-free -clear-ast-before-backend -disable-llvm-verifier -discard-value-names -main-file-name glue_demo1.c -mrelocation-model static -mframe-pointer=none -ffp-contract=on -fno-rounding-math -mconstructor-aliases -target-cpu generic -debugger-tuning=gdb -fdebug-compilation-dir=/home/martin/Documents -v -fcoverage-compilation-dir=/home/martin/Documents -resource-dir /home/martin/code/emsdk/upstream/lib/clang/19 -D EMSCRIPTEN -I ./ -isysroot /home/martin/code/emsdk/upstream/emscripten/cache/sysroot -internal-isystem /home/martin/code/emsdk/upstream/lib/clang/19/include -internal-isystem /home/martin/code/emsdk/upstream/emscripten/cache/sysroot/include/wasm32-emscripten -internal-isystem /home/martin/code/emsdk/upstream/emscripten/cache/sysroot/include -O0 -Werror=implicit-function-declaration -Wno-everything -w -ferror-limit 19 -fvisibility=default -fgnuc-version=4.2.1 -fskip-odr-check-in-gmf -fignore-exceptions -fcolor-diagnostics -iwithsysroot/include/fakesdl -iwithsysroot/include/compat -mllvm -combiner-global-alias-analysis=false -mllvm -enable-emscripten-sjlj -mllvm -disable-lsr -o /tmp/emscripten_temp_v2coerxi/glue_demo1_3.o -x c glue_demo1.c
clang -cc1 version 19.0.0git based upon LLVM 19.0.0git default target x86_64-unknown-linux-gnu
ignoring nonexistent directory "/home/martin/code/emsdk/upstream/emscripten/cache/sysroot/include/wasm32-emscripten"
#include "..." search starts here:
#include <...> search starts here:
 .
 /home/martin/code/emsdk/upstream/emscripten/cache/sysroot/include/fakesdl
 /home/martin/code/emsdk/upstream/emscripten/cache/sysroot/include/compat
 /home/martin/code/emsdk/upstream/lib/clang/19/include
 /home/martin/code/emsdk/upstream/emscripten/cache/sysroot/include
End of search list.
 /home/martin/code/emsdk/upstream/bin/clang --version
 /home/martin/code/emsdk/upstream/bin/wasm-ld -o demo1-opt_O0.wasm -L/home/martin/code/emsdk/upstream/emscripten/cache/sysroot/lib/wasm32-emscripten /tmp/emscripten_temp_v2coerxi/demo1_main_wasm_0.o /tmp/emscripten_temp_v2coerxi/gc_stack_1.o /tmp/emscripten_temp_v2coerxi/CertiCoq.Benchmarks.tests.demo1_2.o /tmp/emscripten_temp_v2coerxi/glue_demo1_3.o -lGL-getprocaddr -lal -lhtml5 -lstubs-debug -lnoexit -lc-debug -ldlmalloc -lcompiler_rt -lc++-noexcept -lc++abi-debug-noexcept -lsockets -mllvm -combiner-global-alias-analysis=false -mllvm -enable-emscripten-sjlj -mllvm -disable-lsr /tmp/tmp5vro1s1tlibemscripten_js_symbols.so --export=emscripten_stack_get_end --export=emscripten_stack_get_free --export=emscripten_stack_get_base --export=emscripten_stack_get_current --export=emscripten_stack_init --export=_emscripten_stack_alloc --export=__get_temp_ret --export=__set_temp_ret --export=__wasm_call_ctors --export=_emscripten_stack_restore --export-if-defined=__start_em_asm --export-if-defined=__stop_em_asm --export-if-defined=__start_em_lib_deps --export-if-defined=__stop_em_lib_deps --export-if-defined=__start_em_js --export-if-defined=__stop_em_js --export-if-defined=main --export-if-defined=__main_argc_argv --export-if-defined=fflush --export-table -z stack-size=1000000 --max-memory=2147483648 --initial-heap=16777216 --no-entry --stack-first --table-base=1
 /home/martin/code/emsdk/upstream/bin/llvm-objcopy demo1-opt_O0.wasm demo1-opt_O0.wasm --remove-section=.debug* --remove-section=producers
 /home/martin/code/emsdk/upstream/bin/wasm-emscripten-finalize -g --dyncalls-i64 --pass-arg=legalize-js-interface-exported-helpers demo1-opt_O0.wasm -o demo1-opt_O0.wasm --detect-features
 /home/martin/code/emsdk/node/16.20.0_64bit/bin/node /home/martin/code/emsdk/upstream/emscripten/src/compiler.mjs /tmp/tmp0i304x6q.json

[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.