CoqToLeanAsm: x86 Macro Assembler in Lean 4

2.5. Calling Convention Abstraction (Paper Section 4.2)

The paper abstracts over x86 calling conventions (cdecl, stdcall, fastcall) with a single callconv function that generates both caller and callee code:

let (call, def) := callconv cc (mkFunSig 3 true) in
def (fun arg1 arg2 arg3 =>
  MOV EAX, arg1;;
  ADD EAX, arg2;;
  ADD EAX, arg3);;
call MyFunc 2 3 4

The same source expands differently for each convention:

  • cdecl: Caller cleans stack (ADD ESP, 12 after call)

  • stdcall: Callee cleans stack (RET 12)

  • fastcall: First two args in ECX, EDX