Missing stdcall annotations on Vale extern declarations

[msprotz]

Describe the bug

The source contains numerous precise C calling-convention annotations:

jonathan@absinthe:~/Code/everest/hacl-star (protz_sha2) $ git grep CCConv
vale/code/arch/x64/interop/Vale.Stdcalls.X64.Aes.fsti:[@ (CCConv "stdcall") ]
vale/code/arch/x64/interop/Vale.Stdcalls.X64.Aes.fsti:[@ (CCConv "stdcall") ]
vale/code/arch/x64/interop/Vale.Stdcalls.X64.AesHash.fst:[@ (CCConv "stdcall") ]
vale/code/arch/x64/interop/Vale.Stdcalls.X64.AesHash.fst:[@ (CCConv "stdcall") ]
vale/code/arch/x64/interop/Vale.Stdcalls.X64.Cpuid.fsti:[@ (CCConv "stdcall") ]
vale/code/arch/x64/interop/Vale.Stdcalls.X64.Cpuid.fsti:[@ (CCConv "stdcall") ]
vale/code/arch/x64/interop/Vale.Stdcalls.X64.Cpuid.fsti:[@ (CCConv "stdcall") ]
vale/code/arch/x64/interop/Vale.Stdcalls.X64.Cpuid.fsti:[@ (CCConv "stdcall") ]
vale/code/arch/x64/interop/Vale.Stdcalls.X64.Cpuid.fsti:[@ (CCConv "stdcall") ]
vale/code/arch/x64/interop/Vale.Stdcalls.X64.Cpuid.fsti:[@ (CCConv "stdcall") ]
vale/code/arch/x64/interop/Vale.Stdcalls.X64.Cpuid.fsti:[@ (CCConv "stdcall") ]
vale/code/arch/x64/interop/Vale.Stdcalls.X64.Cpuid.fsti:[@ (CCConv "stdcall") ]
vale/code/arch/x64/interop/Vale.Stdcalls.X64.Cpuid.fsti:[@ (CCConv "stdcall") ]
vale/code/arch/x64/interop/Vale.Stdcalls.X64.Cpuid.fsti:[@ (CCConv "stdcall") ]
vale/code/arch/x64/interop/Vale.Stdcalls.X64.Cpuid.fsti:[@ (CCConv "stdcall") ]
vale/code/arch/x64/interop/Vale.Stdcalls.X64.Cpuid.fsti:[@ (CCConv "stdcall") ]
vale/code/arch/x64/interop/Vale.Stdcalls.X64.Fadd.fsti:[@ (CCConv "stdcall") ]
vale/code/arch/x64/interop/Vale.Stdcalls.X64.Fadd.fsti:[@ (CCConv "stdcall") ]
vale/code/arch/x64/interop/Vale.Stdcalls.X64.Fmul.fsti:[@ (CCConv "stdcall") ]
vale/code/arch/x64/interop/Vale.Stdcalls.X64.Fmul.fsti:[@ (CCConv "stdcall") ]
vale/code/arch/x64/interop/Vale.Stdcalls.X64.Fmul.fsti:[@ (CCConv "stdcall") ]
vale/code/arch/x64/interop/Vale.Stdcalls.X64.Fsqr.fsti:[@ (CCConv "stdcall") ]
vale/code/arch/x64/interop/Vale.Stdcalls.X64.Fsqr.fsti:[@ (CCConv "stdcall") ]
vale/code/arch/x64/interop/Vale.Stdcalls.X64.Fsub.fsti:[@ (CCConv "stdcall") ]
vale/code/arch/x64/interop/Vale.Stdcalls.X64.Fswap.fsti:[@ (CCConv "stdcall") ]
vale/code/arch/x64/interop/Vale.Stdcalls.X64.GCM_IV.fst:[@ (CCConv "stdcall") ]
vale/code/arch/x64/interop/Vale.Stdcalls.X64.GCMdecryptOpt.fst:[@ (CCConv "stdcall") ]
vale/code/arch/x64/interop/Vale.Stdcalls.X64.GCMdecryptOpt.fst:[@ (CCConv "stdcall") ]
vale/code/arch/x64/interop/Vale.Stdcalls.X64.GCMencryptOpt.fst:[@ (CCConv "stdcall") ]
vale/code/arch/x64/interop/Vale.Stdcalls.X64.GCMencryptOpt.fst:[@ (CCConv "stdcall") ]
vale/code/arch/x64/interop/Vale.Stdcalls.X64.GCTR.fst:[@ (CCConv "stdcall") ]
vale/code/arch/x64/interop/Vale.Stdcalls.X64.GCTR.fst:[@ (CCConv "stdcall") ]
vale/code/arch/x64/interop/Vale.Stdcalls.X64.Poly.fsti:[@ (CCConv "stdcall") ]
vale/code/arch/x64/interop/Vale.Stdcalls.X64.Sha.fsti:[@ (CCConv "stdcall") ]

but it seems like krml does nothing with them: there are no keywords stdcall in internal/Vale.h

Expected behavior

krml should probably emit stdcall

@franziskuskiefer do you know if this is a problem on Windows? I'm not sure how it worked so far... is stdcall the default convention?

[msprotz]

Note: I found this bug while spending an afternoon going down the rabbit hole of header inclusion in krml. Following my most recent changes, callconv.h should only be used from within Vale.h, possibly by passing -add-include 'Vale.h:"krml/internal/callconv.h"' to krml

[franziskuskiefer]

I haven't seen any issue with calling conventions on Windows. The .asm work fine with msvc and the .S with clang-cl. I didn't check the assembly though.

[msprotz]

ok, because the Vale assembly code definitely expects stdcall, so I'm just curious how this is even working out -- the default is cdecl I think on Windows... isn't there some issue related to stack cleanup?