123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230(* Assembly printer for ARMv8-A (AArch64).
GNU assembler (ELF) syntax. General-purpose registers are printed in
their 64-bit X form except for the instruction operands that require the
32-bit W form (narrow loads and stores, 32-bit multiplies, zero
extensions). Immediate values are printed as nonnegative integers. *)openArch_declopenUtilsopenPrintASMopenAsm_utils(* Architecture imports*)openArm_commonopenArmv8a_declopenArmv8a_instr_declletarch=armv8a_declletimm_pre="#"(* We support the following AArch64 memory accesses.
Offset addressing:
- A base register and an immediate offset (displacement):
[<reg>, #<imm>].
- A base register and a register offset: [<reg>, <reg>].
- A base register and a scaled register offset:
[<reg>, <reg>, LSL #<imm>].
*)letpp_reg_address_auxbasedispoffscal=match(disp,off,scal)with|None,None,None->Format.asprintf"[%s]"base|Somedisp,None,None->Format.asprintf"[%s, %s%s]"baseimm_predisp|None,Someoff,None->Format.asprintf"[%s, %s]"baseoff|None,Someoff,Somescal->Format.asprintf"[%s, %s, lsl %s%s]"baseoffimm_prescal|_,_,_->hierror~loc:Lnone~kind:"assembly printing"~internal:true"the address computation is too complex: an intermediate variable might be needed"letpp_imm=pp_immimm_preletpp_register=pp_registerarch(* The 32-bit (W) view of a general-purpose register. *)letpp_wregisterr=matchpp_registerrwith|"xzr"->"wzr"|"sp"->"wsp"|s->"w"^String.subs1(String.lengths-1)letpp_reg_addressaddr=letaddr=parse_reg_addressarchaddrinpp_reg_address_auxaddr.baseaddr.displacementaddr.offsetaddr.scaleletpp_condt=hash_to_stringstring_of_condt(* A64 has no conditional execution: a condition is always a proper operand
(CSEL, CSET, ...), declared last in the argument list, so it is printed
in place like any other operand. *)letpp_asm_arg?(wform=false)(arg:(register,Arch_utils.empty,Arch_utils.empty,rflag,condt)asm_arg)=matchargwith|Condtct->pp_condtct|Imm(ws,w)->pp_imm(Conv.z_unsigned_of_wordwsw)|Regr->ifwformthenpp_wregisterrelsepp_registerr|Regx_->.|Addr(Aregra)->pp_reg_addressra|Addr(Aripr)->pp_rip_addressr|XReg_->.(* -------------------------------------------------------------------- *)letpp_shift_kind=hash_to_stringstring_of_shift_kind(* Append the optional shift to the last (immediate) operand:
[..., <shift> #<amount>]. *)letpp_shift(ARMv8A_op(_,opts))args=matchhas_shiftoptswith|None->args|Somesk->letsh=pp_shift_kindskinList.modify_last(Format.asprintf"%s %s"sh)args(* The last operand of MOVZ/MOVN/MOVK is the halfword shift: print it as
[LSL #<sh>], dropping it when it is zero. *)letpp_mov_wide_shiftargs=matchList.revargswith|"#0"::rest->List.revrest|sh::rest->List.rev(Format.asprintf"lsl %s"sh::rest)|[]->[]letpp_mnemonic(ARMv8A_op(mn,_)asop)=letid=instr_descArmv8a_decl.armv8a_declArmv8a_instr_decl.armv8a_op_decl(None,op)inletpp=id.id_pp_asm[]inmatchmnwith|UXTW->"mov"(* [UXTW] is written [MOV <Wd>, <Wn>]. *)|_->String.lowercase_asciipp.pp_aop_name(* Split an [ADR] instruction to a global symbol into an [ADRP]/[ADD]
pair using :lo12: relocations. *)letpp_ADRargs=matchargswith|dst::addr::_->[Instr("adrp",[dst;addr]);Instr("add",[dst;dst;":lo12:"^addr])]|_->assertfalsemoduleArmv8aTarget:AsmTargetBuilder.AsmTargetwithtypereg=Armv8a_decl.registerandtyperegx=Arch_utils.emptyandtypexreg=Arch_utils.emptyandtyperflag=Arm_common.rflagandtypecond=Arm_common.condtandtypeasm_op=armv8a_asm_op=structtypereg=Armv8a_decl.registertyperegx=Arch_utils.emptytypexreg=Arch_utils.emptytyperflag=Arm_common.rflagtypecond=Arm_common.condttypeasm_op=armv8a_asm_opletheaders=[]letdata_segment_header=[Instr(".p2align",["5"]);Labelglobal_datas_label](* A64 instructions must be 4-byte aligned. *)letfunction_directives=[Instr(".p2align",["2"])](* The return address (X30) is saved on the stack around the body of
export functions; SP must stay 16-byte aligned. *)letfunction_header=[Instr("str",["x30";"[sp, #-16]!"])]letfunction_tail=[Instr("ldr",["x30";"[sp], #16"]);Instr("ret",[])]letpp_instr_rfni=matchiwith|ALIGN->(* A64 instructions are fixed-width: code is always 4-byte
aligned, there is nothing to emit. *)[]|LABEL(_,lbl)->[Label(string_of_labelfnlbl)]|STORELABEL(dst,lbl)->[Instr("adr",[pp_registerdst;string_of_labelfnlbl])]|JMPlbl->[Instr("b",[pp_remote_labellbl])]|JMPIarg->beginmatchargwith|RegR30->[Instr("ret",[])]|Regr->[Instr("br",[pp_registerr])]|_->hierror~loc:Lnone~kind:"assembly printing""unsupported indirect jump argument"end|Jcc(lbl,ct)->letiname=Format.asprintf"b.%s"(pp_condtct)in[Instr(iname,[string_of_labelfnlbl])]|JAL(R30,lbl)->[Instr("bl",[pp_remote_labellbl])]|CALL_|JAL_->assertfalse|POPPC->[Instr("ldr",["x30";"[sp], #16"]);Instr("ret",[])]|SysCallop->[Instr("bl",[pp_syscallop])]|Declassify_val(lty,a)->declassify_val(fun_ltya->pp_asm_arga)ltya|Declassify_mem(len,a)->declassify_memarchlena|AsmOp(op,args)->let(ARMv8A_op(mn,_))=opinletid=instr_descArmv8a_decl.armv8a_declArmv8a_instr_decl.armv8a_op_decl(None,op)inletpp=id.id_pp_asmargsinmatchop,argswith|ARMv8A_op(ADR,_),_::Addr(Arip_)::_->letargs=List.map(fun(_,a)->pp_asm_arga)pp.pp_aop_argsinpp_ADRargs|_,_->letname=pp_mnemonicopin(* Registers are printed in the W form when the instruction
declaration pairs them with a width of at most [U32]. *)letpargs=List.map(fun(sz,a)->pp_asm_arg~wform:(Wsize.size_8_32sz)a)pp.pp_aop_argsinletpargs=matchmnwith|MOVZ|MOVN|MOVK->pp_mov_wide_shiftpargs|_->pp_shiftoppargsin[Instr(name,pargs)]endmoduleArmv8aBuilder=AsmTargetBuilder.Make(Armv8aTarget)letprint_progfmtprog=PrintASM.pp_asmfmt(Armv8aBuilder.asm_of_progprog)