FStarLang/karamel

Build fails on native Apple M1 + macOS toolchain

beurdouche opened this issue · 3 comments

beurdouche commented

I've been attempting to build Kremlin on an M1.

  • F* branch fangyi-zhou-ppxlib
  • Kremlin based branch wasm-1.1 on top of which master (4ccb2de) has been merged
clang --version
Apple clang version 12.0.0 (clang-1200.0.32.29)
Target: arm64-apple-darwin20.3.0
Thread model: posix
InstalledDir: /Applications/Xcode.app/Contents/Developer/Toolchains/XcodeDefault.xctoolchain/usr/bin

I can confirm that this works on x86_64 but when running gmake on M1, I get the following errors:

⚙ KreMLin auto-detecting tools. Here's what we found:
readlink is: greadlink
KreMLin called via: ../krml
KreMLin home is: /opt/kremlin
⚙ KreMLin will drive F*. Here's what we found:
read FSTAR_HOME via the environment
fstar is on branch fangyi-zhou-ppxlib
fstar is: /opt/fstar/bin/fstar.exe /opt/kremlin/runtime/WasmSupport.fst /opt/fstar/ulib/FStar.UInt128.fst --trace_error --cache_checked_modules --expose_interfaces --include /opt/kremlin/kremlib --include /opt/kremlin/include
✔ [PrettyPrinting] ⏱️ 5ms
KreMLin: wrote out .c files for WasmSupport, FStar_ModifiesGen, FStar_VConfig, FStar_Order
KreMLin: wrote out .h files for Prims, FStar_BitVector, FStar_UInt, FStar_UInt_8_16_32_64, LowStar_Endianness, C_Failure, FStar_String, LowStar_Printf, FStar_HyperStack_IO, TestLib, FStar_Bytes, C_String, FStar_Char, C, FStar_IO, FStar_Float, FStar_Monotonic_HyperStack, C_Loops, WasmSupport, FStar_Int_Cast, FStar_Int, FStar_Int8, FStar_Int32, FStar_Int64, FStar_All, FStar_Monotonic_Heap, FStar_ST, FStar_Kremlin_Endianness, FStar_ModifiesGen, FStar_Date, FStar_VConfig, FStar_Order, FStar_HyperStack_All, FStar_HyperStack_ST, FStar_Monotonic_HyperHeap, FStar_Int16, FStar_Math_Lib, FStar_Mul, FStar_Pervasives
cp c/*.c c/*.h dist/generic/
gmake -C dist/generic -f Makefile.basic
gmake[2]: Entering directory '/opt/kremlin/kremlib/dist/generic'
clang: error: the clang compiler does not support '-march=native'

After removing -march=native from ./kremlib/Makefile the build fails with:

gmake -C kremlib
gmake[1]: Entering directory '/opt/kremlin/kremlib'
/opt/fstar/bin/fstar.exe --record_hints --use_hints --odir .extract --warn_error @332 --cache_checked_modules --cache_dir obj --hint_dir hints --include ../runtime --cmi --already_cached 'Prims FStar -FStar.Kremlin.Endianness LowStar -LowStar.Lib'  --dep full C.Endianness.fst C.Failure.fst C.Loops.fst C.String.fst C.fst FStar.Kremlin.Endianness.fst LowStar.Lib.AssocList.fst LowStar.Lib.LinkedList.fst LowStar.Lib.LinkedList2.fst Spec.Loops.fst C.String.fsti LowStar.Lib.AssocList.fsti TestLib.fsti ../runtime/WasmSupport.fst FStar.UInt128.fst FStar.Date.fsti FStar.HyperStack.IO.fst FStar.IO.fst FStar.Int.Cast.Full.fst FStar.Bytes.fsti FStar.Dyn.fsti LowStar.Printf.fst LowStar.Endianness.fst > .depend
gmake -C dist/generic -f Makefile.basic
gmake[2]: Entering directory '/opt/kremlin/kremlib/dist/generic'
cc -O3 -I. -I /opt/kremlin/include -I /opt/kremlin/kremlib/dist/minimal -Wall -Wextra -Werror -std=c11 -Wno-unused-variable -Wno-unknown-warning-option -Wno-unused-but-set-variable -Wno-unused-parameter -Wno-infinite-recursion -g -fwrapv -D_BSD_SOURCE -D_DEFAULT_SOURCE -fPIC    -c -o testlib.o testlib.c
testlib.c:9:34: error: invalid output constraint '=a' in asm
  __asm__ __volatile__("rdtsc" : "=a"(lo), "=d"(hi));
                                 ^
testlib.c:16:116: error: unknown register name '%rax' in asm
  __asm__ __volatile__ ("CPUID\n\t"  "RDTSC\n\t"  "mov %%edx, %0\n\t"  "mov %%eax, %1\n\t": "=r" (hi), "=r" (lo):: "%rax", "%rbx", "%rcx", "%rdx");
                                                                                                                   ^
testlib.c:23:121: error: unknown register name '%rax' in asm
  __asm__ __volatile__ ("RDTSCP\n\t"  "mov %%edx, %0\n\t"  "mov %%eax, %1\n\t"  "CPUID\n\t": "=r" (hi), "=r" (lo)::     "%rax", "%rbx", "%rcx"...
                                                                                                                        ^
3 errors generated.
msprotz commented

Thanks for testing. We can probably ditch the -march=native and just rely on -O2 or whatever makes sense. It's not like there's any performance-critical code in kremlib anyhow.

For the second error, it's the cpu cycles counting routines that are x64-only. Do you know how to do this on ARM? (I don't.) it could be helpful to then start having multiple implementations of those via #ifdefs.

landonf commented

For the second error, it's the cpu cycles counting routines that are x64-only. Do you know how to do this on ARM? (I don't.) it could be helpful to then start having multiple implementations of those via #ifdefs

Clang supports __builtin_readcyclecounter, but (at least on ARM), userspace may not have adequate run-time privilege and you might see the generated code raise SIGILL.

For Apple systems, I'd recommend using mach_absolute_time(), which relies on the "comm page" to select the best available counter source at runtime. If you want nanoseconds instead of "cycles", you can use clock_gettime_nsec_np(CLOCK_UPTIME_RAW), which is just mach_absolute_time() + mach_timebase_info()

For other systems, https://github.com/google/benchmark/blob/master/src/cycleclock.h is a pretty comprehensive source of what's available.

protz commented

It looks like I fixed this here: 7db5eb6

TestLib is deprecated and no one uses this so I'm actually contemplating just ditching it.

@landonf: your comments are helpful and would be best integrated into https://github.com/project-everest/hacl-star/blob/master/tests/test_helpers.h#L84