From e6a40c34f710f751ac7e0edac48a9abf07f03315 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?C=C3=B4me=20LE=20BRETON?= Date: Tue, 7 Jul 2026 15:22:53 +0200 Subject: [PATCH 01/58] Add ARMv8-A (AArch64) backend (functional milestone) New architecture `-arch armv8a` targeting A64, modeled at the full 64-bit register width (reg_size = U64, X registers only). Coq: - armv8a_decl.v: registers R0..R30/RZR/RSP printed x0..x30/xzr/sp, NZCV flags, 14 condition codes, AAPCS64 calling convention, register shifts (0..63). - armv8a_instr_decl.v: 76 mnemonics with full semantics; each carries its ARM ARM (DDI 0487 M.a) documentation block (C6.2 section, page, summary, syntax and Operation pseudocode). Flag-setting forms are separate mnemonics (ADDS, ...); conditional selection (CSEL family) takes the condition as a first-class operand; loads/stores rely on the framework for the memory access and only extend values; MOVZ/MOVN/MOVK model wide immediate moves. - armv8a.v: NZCV condition evaluation and asm instance. - armv8a_extra.v: swap, add_large_imm and smart_li pseudo-instructions (smart_li expands to MOVZ/MOVK sequences; A64 has no conditional execution so there is no conditional variant). - armv8a_lowering.v (new): lowering pass; conditions via CMP/TST and NZCV, word conditional expressions via CSEL, large ADD/SUB immediates via add_large_imm, shifted-operand fusion. - armv8a_params_core.v, armv8a_params.v, armv8a_stack_zeroization.v: compiler passes parameters at U64. - arch_decl.v: new CAimmC_armv8a_shift_amount and CAimmC_armv8a_0_16_32_48 immediate checkers (other architectures reject them). OCaml: - pp_arm_v8a.ml: GNU/ELF AArch64 printer; W-register forms for narrow loads/stores, extensions and 32-bit multiplies; ADRP/ADD :lo12: for global addresses; b.cc branches and ret-based returns. - coreArchFactory retargeted to Armv8a_* modules; callstyle returns via X30. Docs: compiler/doc/armv8a_isa_docs.json machine-readable extraction of the ARM ARM instruction documentation (recording the PDF edition and hash of the source document). Tests: 14 test programs under tests/success/armv8a, wired as the `armv8a` check category (compiled, assembled with llvm-mc --triple=aarch64 and linked with ld.lld). Correctness proofs are deferred; every semantics function is total and the extraction cone contains no admitted statement. --- compiler/Makefile | 1 + compiler/config/tests.config | 5 + compiler/doc/armv8a_isa_docs.json | 1490 ++++++++ compiler/safetylib/safetyMain.ml | 8 + compiler/scripts/check | 3 + compiler/src/armv8a_arch_full.ml | 72 + compiler/src/coreArchFactory.ml | 5 + compiler/src/coreArchFactory.mli | 9 + compiler/src/glob_options.ml | 3 +- compiler/src/pp_arm_v8a.ml | 247 ++ compiler/src/pp_arm_v8a.mli | 4 + compiler/src/sct_checker_forward.ml | 1 + compiler/src/toEC.ml | 2 + compiler/src/utils.ml | 2 + compiler/src/utils.mli | 1 + compiler/tests/success/armv8a/add.jazz | 21 + compiler/tests/success/armv8a/addcarry.jazz | 9 + compiler/tests/success/armv8a/and.jazz | 10 + compiler/tests/success/armv8a/call.jazz | 20 + compiler/tests/success/armv8a/csel.jazz | 24 + compiler/tests/success/armv8a/div.jazz | 8 + compiler/tests/success/armv8a/intrinsics.jazz | 49 + compiler/tests/success/armv8a/ldst.jazz | 28 + compiler/tests/success/armv8a/loop.jazz | 18 + compiler/tests/success/armv8a/mul.jazz | 16 + compiler/tests/success/armv8a/or.jazz | 12 + compiler/tests/success/armv8a/shift.jazz | 15 + compiler/tests/success/armv8a/sub.jazz | 12 + compiler/tests/success/armv8a/swap.jazz | 9 + eclib/JModel_armv8a.ec | 214 ++ proofs/_CoqProject | 9 + proofs/arch/arch_decl.v | 2 + proofs/arch/asm_gen.v | 2 + proofs/compiler/arm_decl.v | 1 + proofs/compiler/armv8a.v | 64 + proofs/compiler/armv8a_decl.v | 326 ++ proofs/compiler/armv8a_extra.v | 205 ++ proofs/compiler/armv8a_instr_decl.v | 3262 +++++++++++++++++ proofs/compiler/armv8a_lowering.v | 483 +++ proofs/compiler/armv8a_params.v | 349 ++ proofs/compiler/armv8a_params_core.v | 146 + proofs/compiler/armv8a_stack_zeroization.v | 167 + proofs/compiler/jasmin_compiler.v | 1 + proofs/compiler/riscv_decl.v | 3 +- proofs/compiler/x86_decl.v | 1 + proofs/lang/extraction.v | 7 + tests/success/armv8a/add.jazz | 21 + 47 files changed, 7365 insertions(+), 2 deletions(-) create mode 100644 compiler/doc/armv8a_isa_docs.json create mode 100644 compiler/src/armv8a_arch_full.ml create mode 100644 compiler/src/pp_arm_v8a.ml create mode 100644 compiler/src/pp_arm_v8a.mli create mode 100644 compiler/tests/success/armv8a/add.jazz create mode 100644 compiler/tests/success/armv8a/addcarry.jazz create mode 100644 compiler/tests/success/armv8a/and.jazz create mode 100644 compiler/tests/success/armv8a/call.jazz create mode 100644 compiler/tests/success/armv8a/csel.jazz create mode 100644 compiler/tests/success/armv8a/div.jazz create mode 100644 compiler/tests/success/armv8a/intrinsics.jazz create mode 100644 compiler/tests/success/armv8a/ldst.jazz create mode 100644 compiler/tests/success/armv8a/loop.jazz create mode 100644 compiler/tests/success/armv8a/mul.jazz create mode 100644 compiler/tests/success/armv8a/or.jazz create mode 100644 compiler/tests/success/armv8a/shift.jazz create mode 100644 compiler/tests/success/armv8a/sub.jazz create mode 100644 compiler/tests/success/armv8a/swap.jazz create mode 100644 eclib/JModel_armv8a.ec create mode 100644 proofs/compiler/armv8a.v create mode 100644 proofs/compiler/armv8a_decl.v create mode 100644 proofs/compiler/armv8a_extra.v create mode 100644 proofs/compiler/armv8a_instr_decl.v create mode 100644 proofs/compiler/armv8a_lowering.v create mode 100644 proofs/compiler/armv8a_params.v create mode 100644 proofs/compiler/armv8a_params_core.v create mode 100644 proofs/compiler/armv8a_stack_zeroization.v create mode 100644 tests/success/armv8a/add.jazz diff --git a/compiler/Makefile b/compiler/Makefile index a6ade6c988..38a1e1a7d1 100644 --- a/compiler/Makefile +++ b/compiler/Makefile @@ -17,6 +17,7 @@ CHECKCATS ?= \ arm-m4-stack-zero-unrolled \ risc-v-stack-zero-loop \ risc-v-stack-zero-unrolled \ + armv8a \ CCT CCT-DOIT SCT # -------------------------------------------------------------------- diff --git a/compiler/config/tests.config b/compiler/config/tests.config index 052ec95372..7cdd7631c1 100644 --- a/compiler/config/tests.config +++ b/compiler/config/tests.config @@ -54,6 +54,11 @@ bin = ./scripts/check args = -arch riscv okdirs = examples/**/risc-v tests/success/**/risc-v tests/success/**/common +[test-armv8a] +bin = ./scripts/check +args = -arch armv8a +okdirs = tests/success/**/armv8a + [test-risc-v-extraction] bin = ./scripts/extract-and-check args = riscv diff --git a/compiler/doc/armv8a_isa_docs.json b/compiler/doc/armv8a_isa_docs.json new file mode 100644 index 0000000000..5003561d04 --- /dev/null +++ b/compiler/doc/armv8a_isa_docs.json @@ -0,0 +1,1490 @@ +{ + "pdf": { + "file": "DDI0487_M.a.a_a-profile_architecture_reference_manual.pdf", + "edition": "DDI0487 M.a", + "sha256": "c07b1302a3db0c6bc0490808c771d66684ddd5adfb2ef64fd23e6beeb7b22e48" + }, + "mnemonics": { + "ADD": [ + { + "c62_id": "C6.2.5", + "title": "ADD (immediate)", + "page": 1796, + "page_end": 1797, + "summary": "Add immediate value\n\nThis instruction adds a register value and an optionally-shifted immediate value, and writes the result to the destination register.\n\nThis instruction is used by the alias MOV (to/from SP).", + "syntax": [ + "ADD , , #{, }", + "ADD , , #{, }" + ], + "operation_asl": "constant bits(datasize) operand1 = if n == 31 then SP[datasize] else X[n, datasize];\nconstant bits(datasize) operand2 = ZeroExtend(imm, datasize);\nbits(datasize) result;\n(result, -) = AddWithCarry(operand1, operand2, '0');\nif d == 31 then\n SP[64] = ZeroExtend(result, 64);\nelse\n X[d, datasize] = result;" + }, + { + "c62_id": "C6.2.6", + "title": "ADD (shifted register)", + "page": 1798, + "page_end": 1799, + "summary": "Add optionally-shifted register\n\nThis instruction adds a register value and an optionally-shifted register value, and writes the result to the destination register.", + "syntax": [ + "ADD , , {, #}", + "ADD , , {, #}" + ], + "operation_asl": "constant bits(datasize) operand1 = X[n, datasize];\nconstant bits(datasize) operand2 = ShiftReg(m, shift_type, shift_amount, datasize);\nbits(datasize) result;\n(result, -) = AddWithCarry(operand1, operand2, '0');\nX[d, datasize] = result;" + }, + { + "c62_id": "C6.2.4", + "title": "ADD (extended register)", + "page": 1793, + "page_end": 1795, + "summary": "Add extended and scaled register\n\nThis instruction adds a register value and a sign or zero-extended register value, followed by an optional left shift amount, and writes the result to the destination register. The argument that is extended from the register can be a byte, halfword, word, or doubleword.", + "syntax": [ + "ADD , , {, {#}}", + "ADD , , {, {#}}" + ], + "operation_asl": "constant bits(datasize) operand1 = if n == 31 then SP[datasize] else X[n, datasize];\nconstant bits(datasize) operand2 = ExtendReg(m, extend_type, shift, datasize);\nbits(datasize) result;\n(result, -) = AddWithCarry(operand1, operand2, '0');\nif d == 31 then\n SP[64] = ZeroExtend(result, 64);\nelse\n X[d, datasize] = result;" + } + ], + "ADDS": [ + { + "c62_id": "C6.2.10", + "title": "ADDS (immediate)", + "page": 1805, + "page_end": 1806, + "summary": "Add immediate value, setting flags\n\nThis instruction adds a register value and an optionally-shifted immediate value, and writes the result to the destination register. It updates the condition flags based on the result.\n\nThis instruction is used by the alias CMN (immediate).", + "syntax": [ + "ADDS , , #{, }", + "ADDS , , #{, }" + ], + "operation_asl": "constant bits(datasize) operand1 = if n == 31 then SP[datasize] else X[n, datasize];\nconstant bits(datasize) operand2 = ZeroExtend(imm, datasize);\nbits(datasize) result;\nbits(4) nzcv;\n(result, nzcv) = AddWithCarry(operand1, operand2, '0');\nX[d, datasize] = result;\nPSTATE. = nzcv;" + }, + { + "c62_id": "C6.2.11", + "title": "ADDS (shifted register)", + "page": 1807, + "page_end": 1808, + "summary": "Add optionally-shifted register, setting flags\n\nThis instruction adds a register value and an optionally-shifted register value, and writes the result to the destination register. It updates the condition flags based on the result.\n\nThis instruction is used by the alias CMN (shifted register).", + "syntax": [ + "ADDS , , {, #}", + "ADDS , , {, #}" + ], + "operation_asl": "constant bits(datasize) operand1 = X[n, datasize];\nconstant bits(datasize) operand2 = ShiftReg(m, shift_type, shift_amount, datasize);\nbits(datasize) result;\nbits(4) nzcv;\n(result, nzcv) = AddWithCarry(operand1, operand2, '0');\nX[d, datasize] = result;\nPSTATE. = nzcv;" + } + ], + "ADC": [ + { + "c62_id": "C6.2.2", + "title": "ADC", + "page": 1789, + "page_end": 1790, + "summary": "Add with carry\n\nThis instruction adds two register values and the Carry flag value, and writes the result to the destination register.", + "syntax": [ + "ADC , , ", + "ADC , , " + ], + "operation_asl": "constant bits(datasize) operand1 = X[n, datasize];\nconstant bits(datasize) operand2 = X[m, datasize];\nbits(datasize) result;\n(result, -) = AddWithCarry(operand1, operand2, PSTATE.C);\nX[d, datasize] = result;" + } + ], + "ADCS": [ + { + "c62_id": "C6.2.3", + "title": "ADCS", + "page": 1791, + "page_end": 1792, + "summary": "Add with carry, setting flags\n\nThis instruction adds two register values and the Carry flag value, and writes the result to the destination register. It updates the condition flags based on the result.", + "syntax": [ + "ADCS , , ", + "ADCS , , " + ], + "operation_asl": "constant bits(datasize) operand1 = X[n, datasize];\nconstant bits(datasize) operand2 = X[m, datasize];\nbits(datasize) result;\nbits(4) nzcv;\n(result, nzcv) = AddWithCarry(operand1, operand2, PSTATE.C);\nX[d, datasize] = result;\nPSTATE. = nzcv;" + } + ], + "SUB": [ + { + "c62_id": "C6.2.456", + "title": "SUB (immediate)", + "page": 2783, + "page_end": 2784, + "summary": "Subtract immediate value\n\nThis instruction subtracts an optionally-shifted immediate value from a register value, and writes the result to the destination register.", + "syntax": [ + "SUB , , #{, }", + "SUB , , #{, }" + ], + "operation_asl": "constant bits(datasize) operand1 = if n == 31 then SP[datasize] else X[n, datasize];\nconstant bits(datasize) operand2 = ZeroExtend(imm, datasize);\nbits(datasize) result;\n(result, -) = AddWithCarry(operand1, NOT(operand2), '1');\nif d == 31 then\n SP[64] = ZeroExtend(result, 64);\nelse\n X[d, datasize] = result;" + }, + { + "c62_id": "C6.2.457", + "title": "SUB (shifted register)", + "page": 2785, + "page_end": 2786, + "summary": "Subtract optionally-shifted register\n\nThis instruction subtracts an optionally-shifted register value from a register value, and writes the result to the destination register.\n\nThis instruction is used by the alias NEG (shifted register).", + "syntax": [ + "SUB , , {, #}", + "SUB , , {, #}" + ], + "operation_asl": "constant bits(datasize) operand1 = X[n, datasize];\nconstant bits(datasize) operand2 = NOT(ShiftReg(m, shift_type, shift_amount, datasize));\nbits(datasize) result;\n(result, -) = AddWithCarry(operand1, operand2, '1');\nX[d, datasize] = result;" + }, + { + "c62_id": "C6.2.455", + "title": "SUB (extended register)", + "page": 2780, + "page_end": 2782, + "summary": "Subtract extended and scaled register\n\nThis instruction subtracts a sign or zero-extended register value, followed by an optional left shift amount, from a register value, and writes the result to the destination register. The argument that is extended from the register can be a byte, halfword, word, or doubleword.", + "syntax": [ + "SUB , , {, {#}}", + "SUB , , {, {#}}" + ], + "operation_asl": "constant bits(datasize) operand1 = if n == 31 then SP[datasize] else X[n, datasize];\nconstant bits(datasize) operand2 = NOT(ExtendReg(m, extend_type, shift, datasize));\nbits(datasize) result;\n(result, -) = AddWithCarry(operand1, operand2, '1');\nif d == 31 then\n SP[64] = ZeroExtend(result, 64);\nelse\n X[d, datasize] = result;" + } + ], + "SUBS": [ + { + "c62_id": "C6.2.463", + "title": "SUBS (immediate)", + "page": 2795, + "page_end": 2796, + "summary": "Subtract immediate value, setting flags\n\nThis instruction subtracts an optionally-shifted immediate value from a register value, and writes the result to the destination register. It updates the condition flags based on the result.\n\nThis instruction is used by the alias CMP (immediate).", + "syntax": [ + "SUBS , , #{, }", + "SUBS , , #{, }" + ], + "operation_asl": "constant bits(datasize) operand1 = if n == 31 then SP[datasize] else X[n, datasize];\nconstant bits(datasize) operand2 = ZeroExtend(imm, datasize);\nbits(datasize) result;\nbits(4) nzcv;\n(result, nzcv) = AddWithCarry(operand1, NOT(operand2), '1');\nX[d, datasize] = result;\nPSTATE. = nzcv;" + }, + { + "c62_id": "C6.2.464", + "title": "SUBS (shifted register)", + "page": 2797, + "page_end": 2798, + "summary": "Subtract optionally-shifted register, setting flags\n\nThis instruction subtracts an optionally-shifted register value from a register value, and writes the result to the destination register. It updates the condition flags based on the result.\n\nThis instruction is used by the aliases CMP (shifted register) and NEGS.", + "syntax": [ + "SUBS , , {, #}", + "SUBS , , {, #}" + ], + "operation_asl": "constant bits(datasize) operand1 = X[n, datasize];\nconstant bits(datasize) operand2 = NOT(ShiftReg(m, shift_type, shift_amount, datasize));\nbits(datasize) result;\nbits(4) nzcv;\n(result, nzcv) = AddWithCarry(operand1, operand2, '1');\nX[d, datasize] = result;\nPSTATE. = nzcv;" + } + ], + "SBC": [ + { + "c62_id": "C6.2.351", + "title": "SBC", + "page": 2548, + "page_end": 2549, + "summary": "Subtract with carry\n\nThis instruction subtracts a register value and the value of NOT (Carry flag) from a register value, and writes the result to the destination register.\n\nThis instruction is used by the alias NGC.", + "syntax": [ + "SBC , , ", + "SBC , , " + ], + "operation_asl": "constant bits(datasize) operand1 = X[n, datasize];\nconstant bits(datasize) operand2 = NOT(X[m, datasize]);\nbits(datasize) result;\n(result, -) = AddWithCarry(operand1, operand2, PSTATE.C);\nX[d, datasize] = result;" + } + ], + "SBCS": [ + { + "c62_id": "C6.2.352", + "title": "SBCS", + "page": 2550, + "page_end": 2551, + "summary": "Subtract with carry, setting flags\n\nThis instruction subtracts a register value and the value of NOT (Carry flag) from a register value, and writes the result to the destination register. It updates the condition flags based on the result.\n\nThis instruction is used by the alias NGCS.", + "syntax": [ + "SBCS , , ", + "SBCS , , " + ], + "operation_asl": "constant bits(datasize) operand1 = X[n, datasize];\nconstant bits(datasize) operand2 = NOT(X[m, datasize]);\nbits(datasize) result;\nbits(4) nzcv;\n(result, nzcv) = AddWithCarry(operand1, operand2, PSTATE.C);\nX[d, datasize] = result;\nPSTATE. = nzcv;" + } + ], + "MUL": [ + { + "c62_id": "C6.2.292", + "title": "MUL", + "page": 2436, + "page_end": 2437, + "summary": "Multiply\n\nThis instruction multiplies two register values and writes the result to the destination register.\n\nThis is an alias of MADD. This means:\n\n• The encodings in this description are named to match the encodings of MADD. • The description of MADD gives the operational pseudocode, any CONSTRAINED UNPREDICTABLE behavior, and any operational information for this instruction.", + "syntax": [ + "MUL , , == MADD , , , WZR", + "MUL , , == MADD , , , XZR" + ], + "operation_asl": "The description of MADD gives the operational pseudocode for this instruction.", + "note": "MUL is an alias of MADD with Ra = ZR (see the MADD entry for the operational pseudocode)." + } + ], + "MADD": [ + { + "c62_id": "C6.2.274", + "title": "MADD", + "page": 2401, + "page_end": 2402, + "summary": "Multiply-add\n\nThis instruction multiplies two register values, adds a third register value, and writes the result to the destination register.\n\nThis instruction is used by the alias MUL.", + "syntax": [ + "MADD , , , ", + "MADD , , , " + ], + "operation_asl": "constant bits(datasize) operand1 = X[n, datasize];\nconstant bits(datasize) operand2 = X[m, datasize];\nconstant bits(datasize) operand3 = X[a, datasize];\nconstant integer result = UInt(operand3) + (UInt(operand1) * UInt(operand2));\nX[d, datasize] = result;" + } + ], + "MSUB": [ + { + "c62_id": "C6.2.290", + "title": "MSUB", + "page": 2432, + "page_end": 2433, + "summary": "Multiply-subtract\n\nThis instruction multiplies two register values, subtracts the product from a third register value, and writes the result to the destination register.\n\nThis instruction is used by the alias MNEG.", + "syntax": [ + "MSUB , , , ", + "MSUB , , , " + ], + "operation_asl": "constant bits(datasize) operand1 = X[n, datasize];\nconstant bits(datasize) operand2 = X[m, datasize];\nconstant bits(datasize) operand3 = X[a, datasize];\nconstant integer result = UInt(operand3) - (UInt(operand1) * UInt(operand2));\nX[d, datasize] = result;" + } + ], + "NEG": [ + { + "c62_id": "C6.2.294", + "title": "NEG (shifted register)", + "page": 2440, + "page_end": 2441, + "summary": "Negate (shifted register)\n\nThis instruction negates an optionally-shifted register value, and writes the result to the destination register.\n\nThis is an alias of SUB (shifted register). This means:\n\n• The encodings in this description are named to match the encodings of SUB (shifted register). • The description of SUB (shifted register) gives the operational pseudocode, any CONSTRAINED UNPREDICTABLE behavior, and any operational information for this instruction.", + "syntax": [ + "NEG , {, #} == SUB , WZR, {, #}", + "NEG , {, #} == SUB , XZR, {, #}" + ], + "operation_asl": "The description of SUB (shifted register) gives the operational pseudocode for this instruction.", + "note": "NEG is an alias of SUB (shifted register) with Rn = ZR; the SUB entry carries the operational pseudocode." + }, + { + "c62_id": "C6.2.457", + "title": "SUB (shifted register)", + "page": 2785, + "page_end": 2786, + "summary": "Subtract optionally-shifted register\n\nThis instruction subtracts an optionally-shifted register value from a register value, and writes the result to the destination register.\n\nThis instruction is used by the alias NEG (shifted register).", + "syntax": [ + "SUB , , {, #}", + "SUB , , {, #}" + ], + "operation_asl": "constant bits(datasize) operand1 = X[n, datasize];\nconstant bits(datasize) operand2 = NOT(ShiftReg(m, shift_type, shift_amount, datasize));\nbits(datasize) result;\n(result, -) = AddWithCarry(operand1, operand2, '1');\nX[d, datasize] = result;", + "note": "NEG is an alias of SUB (shifted register) with Rn = ZR; the SUB entry carries the operational pseudocode." + } + ], + "SDIV": [ + { + "c62_id": "C6.2.356", + "title": "SDIV", + "page": 2558, + "page_end": 2559, + "summary": "Signed divide\n\nThis instruction divides the first signed source register value by the second signed source register value, and writes the result to the destination register. Dividing by zero writes the value zero to the destination register. The condition flags are not affected.", + "syntax": [ + "SDIV , , ", + "SDIV , , " + ], + "operation_asl": "constant bits(datasize) operand1 = X[n, datasize];\nconstant bits(datasize) operand2 = X[m, datasize];\nconstant integer dividend = SInt(operand1);\nconstant integer divisor = SInt(operand2);\ninteger result;\nif divisor == 0 then\n result = 0;\nelsif (dividend < 0) == (divisor < 0) then\n result = Abs(dividend) DIV Abs(divisor); // same signs - positive result\nelse\n result = -(Abs(dividend) DIV Abs(divisor)); // different signs - negative result\nX[d, datasize] = result;" + } + ], + "UDIV": [ + { + "c62_id": "C6.2.489", + "title": "UDIV", + "page": 2846, + "page_end": 2847, + "summary": "Unsigned divide\n\nThis instruction divides the first unsigned source register value by the second unsigned source register value, and writes the result to the destination register. Dividing by zero writes the value zero to the destination register. The condition flags are not affected.", + "syntax": [ + "UDIV , , ", + "UDIV , , " + ], + "operation_asl": "constant bits(datasize) operand1 = X[n, datasize];\nconstant bits(datasize) operand2 = X[m, datasize];\nconstant integer dividend = UInt(operand1);\nconstant integer divisor = UInt(operand2);\ninteger result;\nif divisor == 0 then\n result = 0;\nelse\n result = dividend DIV divisor;\nX[d, datasize] = result;" + } + ], + "UMULL": [ + { + "c62_id": "C6.2.498", + "title": "UMULL", + "page": 2862, + "page_end": 2862, + "summary": "Unsigned multiply long\n\nThis instruction multiplies two 32-bit register values, and writes the result to the 64-bit destination register.\n\nThis is an alias of UMADDL. This means:\n\n• The encodings in this description are named to match the encodings of UMADDL. • The description of UMADDL gives the operational pseudocode, any CONSTRAINED UNPREDICTABLE behavior, and any operational information for this instruction.", + "syntax": [ + "UMULL , , == UMADDL , , , XZR" + ], + "operation_asl": "The description of UMADDL gives the operational pseudocode for this instruction.", + "note": "UMULL is an alias of UMADDL with Ra = XZR." + } + ], + "SMULL": [ + { + "c62_id": "C6.2.379", + "title": "SMULL", + "page": 2616, + "page_end": 2616, + "summary": "Signed multiply long\n\nThis instruction multiplies two 32-bit register values, and writes the result to the 64-bit destination register.\n\nThis is an alias of SMADDL. This means:\n\n• The encodings in this description are named to match the encodings of SMADDL. • The description of SMADDL gives the operational pseudocode, any CONSTRAINED UNPREDICTABLE behavior, and any operational information for this instruction.", + "syntax": [ + "SMULL , , == SMADDL , , , XZR" + ], + "operation_asl": "The description of SMADDL gives the operational pseudocode for this instruction.", + "note": "SMULL is an alias of SMADDL with Ra = XZR." + } + ], + "UMADDL": [ + { + "c62_id": "C6.2.490", + "title": "UMADDL", + "page": 2848, + "page_end": 2849, + "summary": "Unsigned multiply-add long\n\nThis instruction multiplies two 32-bit register values, adds a 64-bit register value, and writes the result to the 64-bit destination register.\n\nThis instruction is used by the alias UMULL.", + "syntax": [ + "UMADDL , , , " + ], + "operation_asl": "constant bits(32) operand1 = X[n, 32];\nconstant bits(32) operand2 = X[m, 32];\nconstant bits(64) operand3 = X[a, 64];\nconstant integer result = UInt(operand3) + (UInt(operand1) * UInt(operand2));\nX[d, 64] = result<63:0>;" + } + ], + "SMADDL": [ + { + "c62_id": "C6.2.368", + "title": "SMADDL", + "page": 2599, + "page_end": 2600, + "summary": "Signed multiply-add long\n\nThis instruction multiplies two 32-bit register values, adds a 64-bit register value, and writes the result to the 64-bit destination register.\n\nThis instruction is used by the alias SMULL.", + "syntax": [ + "SMADDL , , , " + ], + "operation_asl": "constant bits(32) operand1 = X[n, 32];\nconstant bits(32) operand2 = X[m, 32];\nconstant bits(64) operand3 = X[a, 64];\nconstant integer result = SInt(operand3) + (SInt(operand1) * SInt(operand2));\nX[d, 64] = result<63:0>;" + } + ], + "UMULH": [ + { + "c62_id": "C6.2.497", + "title": "UMULH", + "page": 2861, + "page_end": 2861, + "summary": "Unsigned multiply high\n\nThis instruction multiplies two 64-bit register values, and writes bits[127:64] of the 128-bit result to the 64-bit destination register.", + "syntax": [ + "UMULH , , " + ], + "operation_asl": "constant bits(64) operand1 = X[n, 64];\nconstant bits(64) operand2 = X[m, 64];\nconstant integer result = UInt(operand1) * UInt(operand2);\nX[d, 64] = result<127:64>;" + } + ], + "SMULH": [ + { + "c62_id": "C6.2.378", + "title": "SMULH", + "page": 2615, + "page_end": 2615, + "summary": "Signed multiply high\n\nThis instruction multiplies two 64-bit register values, and writes bits[127:64] of the 128-bit result to the 64-bit destination register.", + "syntax": [ + "SMULH , , " + ], + "operation_asl": "constant bits(64) operand1 = X[n, 64];\nconstant bits(64) operand2 = X[m, 64];\nconstant integer result = SInt(operand1) * SInt(operand2);\nX[d, 64] = result<127:64>;" + } + ], + "AND": [ + { + "c62_id": "C6.2.14", + "title": "AND (immediate)", + "page": 1811, + "page_end": 1812, + "summary": "Bitwise AND (immediate)\n\nThis instruction performs a bitwise AND of a register value and an immediate value, and writes the result to the destination register.", + "syntax": [ + "AND , , #", + "AND , , #" + ], + "operation_asl": "constant bits(datasize) operand1 = X[n, datasize];\nconstant bits(datasize) operand2 = imm;\nconstant bits(datasize) result = operand1 AND operand2;\nif d == 31 then\n SP[64] = ZeroExtend(result, 64);\nelse\n X[d, datasize] = result;" + }, + { + "c62_id": "C6.2.15", + "title": "AND (shifted register)", + "page": 1813, + "page_end": 1814, + "summary": "Bitwise AND (shifted register)\n\nThis instruction performs a bitwise AND of a register value and an optionally-shifted register value, and writes the result to the destination register.", + "syntax": [ + "AND , , {, #}", + "AND , , {, #}" + ], + "operation_asl": "constant bits(datasize) operand1 = X[n, datasize];\nconstant bits(datasize) operand2 = ShiftReg(m, shift_type, shift_amount, datasize);\nX[d, datasize] = operand1 AND operand2;" + } + ], + "ANDS": [ + { + "c62_id": "C6.2.16", + "title": "ANDS (immediate)", + "page": 1815, + "page_end": 1816, + "summary": "Bitwise AND (immediate), setting flags\n\nThis instruction performs a bitwise AND of a register value and an immediate value, and writes the result to the destination register. It updates the condition flags based on the result.\n\nThis instruction is used by the alias TST (immediate).", + "syntax": [ + "ANDS , , #", + "ANDS , , #" + ], + "operation_asl": "constant bits(datasize) operand1 = X[n, datasize];\nconstant bits(datasize) operand2 = imm;\nconstant bits(datasize) result = operand1 AND operand2;\nX[d, datasize] = result;\nPSTATE. = result:IsZeroBit(result):'00';" + }, + { + "c62_id": "C6.2.17", + "title": "ANDS (shifted register)", + "page": 1817, + "page_end": 1818, + "summary": "Bitwise AND (shifted register), setting flags\n\nThis instruction performs a bitwise AND of a register value and an optionally-shifted register value, and writes the result to the destination register. It updates the condition flags based on the result.\n\nThis instruction is used by the alias TST (shifted register).", + "syntax": [ + "ANDS , , {, #}", + "ANDS , , {, #}" + ], + "operation_asl": "constant bits(datasize) operand1 = X[n, datasize];\nconstant bits(datasize) operand2 = ShiftReg(m, shift_type, shift_amount, datasize);\nconstant bits(datasize) result = operand1 AND operand2;\nX[d, datasize] = result;\nPSTATE. = result:IsZeroBit(result):'00';" + } + ], + "BIC": [ + { + "c62_id": "C6.2.41", + "title": "BIC (shifted register)", + "page": 1856, + "page_end": 1857, + "summary": "Bitwise bit clear (shifted register)\n\nThis instruction performs a bitwise AND of a register value and the complement of an optionally-shifted register value, and writes the result to the destination register.", + "syntax": [ + "BIC , , {, #}", + "BIC , , {, #}" + ], + "operation_asl": "constant bits(datasize) operand1 = X[n, datasize];\nconstant bits(datasize) operand2 = ShiftReg(m, shift_type, shift_amount, datasize);\nX[d, datasize] = operand1 AND NOT(operand2);" + } + ], + "BICS": [ + { + "c62_id": "C6.2.42", + "title": "BICS (shifted register)", + "page": 1858, + "page_end": 1859, + "summary": "Bitwise bit clear (shifted register), setting flags\n\nThis instruction performs a bitwise AND of a register value and the complement of an optionally-shifted register value, and writes the result to the destination register. It updates the condition flags based on the result.", + "syntax": [ + "BICS , , {, #}", + "BICS , , {, #}" + ], + "operation_asl": "constant bits(datasize) operand1 = X[n, datasize];\nconstant bits(datasize) operand2 = ShiftReg(m, shift_type, shift_amount, datasize);\nconstant bits(datasize) result = operand1 AND NOT(operand2);\nX[d, datasize] = result;\nPSTATE. = result:IsZeroBit(result):'00';" + } + ], + "ORR": [ + { + "c62_id": "C6.2.300", + "title": "ORR (immediate)", + "page": 2451, + "page_end": 2452, + "summary": "Bitwise OR (immediate)\n\nThis instruction performs a bitwise (inclusive) OR of a register value and an immediate value, and writes the result to the destination register.\n\nThis instruction is used by the alias MOV (bitmask immediate).", + "syntax": [ + "ORR , , #", + "ORR , , #" + ], + "operation_asl": "constant bits(datasize) operand1 = X[n, datasize];\nconstant bits(datasize) operand2 = imm;\nconstant bits(datasize) result = operand1 OR operand2;\nif d == 31 then\n SP[64] = ZeroExtend(result, 64);\nelse\n X[d, datasize] = result;" + }, + { + "c62_id": "C6.2.301", + "title": "ORR (shifted register)", + "page": 2453, + "page_end": 2454, + "summary": "Bitwise OR (shifted register)\n\nThis instruction performs a bitwise (inclusive) OR of a register value and an optionally-shifted register value, and writes the result to the destination register.\n\nThis instruction is used by the alias MOV (register).", + "syntax": [ + "ORR , , {, #}", + "ORR , , {, #}" + ], + "operation_asl": "constant bits(datasize) operand1 = X[n, datasize];\nconstant bits(datasize) operand2 = ShiftReg(m, shift_type, shift_amount, datasize);\nX[d, datasize] = operand1 OR operand2;" + } + ], + "EOR": [ + { + "c62_id": "C6.2.155", + "title": "EOR (immediate)", + "page": 2167, + "page_end": 2168, + "summary": "Bitwise exclusive-OR (immediate)\n\nThis instruction performs a bitwise exclusive-OR of a register value and an immediate value, and writes the result to the destination register.", + "syntax": [ + "EOR , , #", + "EOR , , #" + ], + "operation_asl": "constant bits(datasize) operand1 = X[n, datasize];\nconstant bits(datasize) operand2 = imm;\nconstant bits(datasize) result = operand1 EOR operand2;\nif d == 31 then\n SP[64] = ZeroExtend(result, 64);\nelse\n X[d, datasize] = result;" + }, + { + "c62_id": "C6.2.156", + "title": "EOR (shifted register)", + "page": 2169, + "page_end": 2170, + "summary": "Bitwise exclusive-OR (shifted register)\n\nThis instruction performs a bitwise exclusive-OR of a register value and an optionally-shifted register value, and writes the result to the destination register.", + "syntax": [ + "EOR , , {, #}", + "EOR , , {, #}" + ], + "operation_asl": "constant bits(datasize) operand1 = X[n, datasize];\nconstant bits(datasize) operand2 = ShiftReg(m, shift_type, shift_amount, datasize);\nX[d, datasize] = operand1 EOR operand2;" + } + ], + "MVN": [ + { + "c62_id": "C6.2.293", + "title": "MVN", + "page": 2438, + "page_end": 2439, + "summary": "Bitwise NOT\n\nThis instruction writes the bitwise inverse of a register value to the destination register.\n\nThis is an alias of ORN (shifted register). This means:\n\n• The encodings in this description are named to match the encodings of ORN (shifted register). • The description of ORN (shifted register) gives the operational pseudocode, any CONSTRAINED UNPREDICTABLE behavior, and any operational information for this instruction.", + "syntax": [ + "MVN , {, #} == ORN , WZR, {, #}", + "MVN , {, #} == ORN , XZR, {, #}" + ], + "operation_asl": "The description of ORN (shifted register) gives the operational pseudocode for this instruction." + } + ], + "ASR": [ + { + "c62_id": "C6.2.19", + "title": "ASR (register)", + "page": 1820, + "page_end": 1821, + "summary": "Arithmetic shift right (register)\n\nThis instruction shifts a register value right by a variable number of bits, shifting in copies of its sign bit, and writes the result to the destination register. The value of the second source register modulo the register size in bits gives the number of bits by which the first source register is right-shifted.\n\nThis is an alias of ASRV. This means:\n\n• The encodings in this description are named to match the encodings of ASRV. • The description of ASRV gives the operational pseudocode, any CONSTRAINED UNPREDICTABLE behavior, and any operational information for this instruction.", + "syntax": [ + "ASR , , == ASRV , , ", + "ASR , , == ASRV , , " + ], + "operation_asl": "The description of ASRV gives the operational pseudocode for this instruction." + }, + { + "c62_id": "C6.2.20", + "title": "ASR (immediate)", + "page": 1822, + "page_end": 1823, + "summary": "Arithmetic shift right (immediate)\n\nThis instruction shifts a register value right by an immediate number of bits, shifting in copies of the sign bit in the upper bits and zeros in the lower bits, and writes the result to the destination register.\n\nThis is an alias of SBFM. This means:\n\n• The encodings in this description are named to match the encodings of SBFM. • The description of SBFM gives the operational pseudocode, any CONSTRAINED UNPREDICTABLE behavior, and any operational information for this instruction.", + "syntax": [ + "ASR , , # == SBFM , , #, #31", + "ASR , , # == SBFM , , #, #63" + ], + "operation_asl": "The description of SBFM gives the operational pseudocode for this instruction." + } + ], + "ASRV": [ + { + "c62_id": "C6.2.21", + "title": "ASRV", + "page": 1824, + "page_end": 1825, + "summary": "Arithmetic shift right variable\n\nThis instruction shifts a register value right by a variable number of bits, shifting in copies of its sign bit, and writes the result to the destination register. The value of the second source register modulo the register size in bits gives the number of bits by which the first source register is right-shifted.\n\nThis instruction is used by the alias ASR (register).", + "syntax": [ + "ASRV , , ", + "ASRV , , " + ], + "operation_asl": "constant bits(datasize) operand2 = X[m, datasize];\nX[d, datasize] = ShiftReg(n, shift_type, UInt(operand2) MOD datasize, datasize);" + } + ], + "LSL": [ + { + "c62_id": "C6.2.268", + "title": "LSL (register)", + "page": 2389, + "page_end": 2390, + "summary": "Logical shift left (register)\n\nThis instruction shifts a register value left by a variable number of bits, shifting in zeros, and writes the result to the destination register. The value of the second source register modulo the register size in bits gives the number of bits by which the first source register is left-shifted.\n\nThis is an alias of LSLV. This means:\n\n• The encodings in this description are named to match the encodings of LSLV. • The description of LSLV gives the operational pseudocode, any CONSTRAINED UNPREDICTABLE behavior, and any operational information for this instruction.", + "syntax": [ + "LSL , , == LSLV , , ", + "LSL , , == LSLV , , " + ], + "operation_asl": "The description of LSLV gives the operational pseudocode for this instruction." + }, + { + "c62_id": "C6.2.269", + "title": "LSL (immediate)", + "page": 2391, + "page_end": 2392, + "summary": "Logical shift left (immediate)\n\nThis instruction shifts a register value left by an immediate number of bits, shifting in zeros, and writes the result to the destination register.\n\nThis is an alias of UBFM. This means:\n\n• The encodings in this description are named to match the encodings of UBFM. • The description of UBFM gives the operational pseudocode, any CONSTRAINED UNPREDICTABLE behavior, and any operational information for this instruction.", + "syntax": [ + "LSL , , # == UBFM , , #(- MOD 32), #(31-)", + "LSL , , # == UBFM , , #(- MOD 64), #(63-)" + ], + "operation_asl": "The description of UBFM gives the operational pseudocode for this instruction." + } + ], + "LSLV": [ + { + "c62_id": "C6.2.270", + "title": "LSLV", + "page": 2393, + "page_end": 2394, + "summary": "Logical shift left variable\n\nThis instruction shifts a register value left by a variable number of bits, shifting in zeros, and writes the result to the destination register. The value of the second source register modulo the register size in bits gives the number of bits by which the first source register is left-shifted.\n\nThis instruction is used by the alias LSL (register).", + "syntax": [ + "LSLV , , ", + "LSLV , , " + ], + "operation_asl": "constant bits(datasize) operand2 = X[m, datasize];\nX[d, datasize] = ShiftReg(n, shift_type, UInt(operand2) MOD datasize, datasize);" + } + ], + "LSR": [ + { + "c62_id": "C6.2.271", + "title": "LSR (register)", + "page": 2395, + "page_end": 2396, + "summary": "Logical shift right (register)\n\nThis instruction shifts a register value right by a variable number of bits, shifting in zeros, and writes the result to the destination register. The value of the second source register modulo the register size in bits gives the number of bits by which the first source register is right-shifted.\n\nThis is an alias of LSRV. This means:\n\n• The encodings in this description are named to match the encodings of LSRV. • The description of LSRV gives the operational pseudocode, any CONSTRAINED UNPREDICTABLE behavior, and any operational information for this instruction.", + "syntax": [ + "LSR , , == LSRV , , ", + "LSR , , == LSRV , , " + ], + "operation_asl": "The description of LSRV gives the operational pseudocode for this instruction." + }, + { + "c62_id": "C6.2.272", + "title": "LSR (immediate)", + "page": 2397, + "page_end": 2398, + "summary": "Logical shift right (immediate)\n\nThis instruction shifts a register value right by an immediate number of bits, shifting in zeros, and writes the result to the destination register.\n\nThis is an alias of UBFM. This means:\n\n• The encodings in this description are named to match the encodings of UBFM. • The description of UBFM gives the operational pseudocode, any CONSTRAINED UNPREDICTABLE behavior, and any operational information for this instruction.", + "syntax": [ + "LSR , , # == UBFM , , #, #31", + "LSR , , # == UBFM , , #, #63" + ], + "operation_asl": "The description of UBFM gives the operational pseudocode for this instruction." + } + ], + "LSRV": [ + { + "c62_id": "C6.2.273", + "title": "LSRV", + "page": 2399, + "page_end": 2400, + "summary": "Logical shift right variable\n\nThis instruction shifts a register value right by a variable number of bits, shifting in zeros, and writes the result to the destination register. The value of the second source register modulo the register size in bits gives the number of bits by which the first source register is right-shifted.\n\nThis instruction is used by the alias LSR (register).", + "syntax": [ + "LSRV , , ", + "LSRV , , " + ], + "operation_asl": "constant bits(datasize) operand2 = X[m, datasize];\nX[d, datasize] = ShiftReg(n, shift_type, UInt(operand2) MOD datasize, datasize);" + } + ], + "ROR": [ + { + "c62_id": "C6.2.346", + "title": "ROR (immediate)", + "page": 2539, + "page_end": 2540, + "summary": "Rotate right (immediate)\n\nThis instruction provides the value of the contents of a register rotated by a variable number of bits. The bits that are rotated off the right end are inserted into the vacated bit positions on the left.\n\nThis is an alias of EXTR. This means:\n\n• The encodings in this description are named to match the encodings of EXTR. • The description of EXTR gives the operational pseudocode, any CONSTRAINED UNPREDICTABLE behavior, and any operational information for this instruction.", + "syntax": [ + "ROR , , # == EXTR , , , #", + "ROR , , # == EXTR , , , #" + ], + "operation_asl": "The description of EXTR gives the operational pseudocode for this instruction." + }, + { + "c62_id": "C6.2.347", + "title": "ROR (register)", + "page": 2541, + "page_end": 2542, + "summary": "Rotate right (register)\n\nThis instruction provides the value of the contents of a register rotated by a variable number of bits. The bits that are rotated off the right end are inserted into the vacated bit positions on the left. The value of the second source register modulo the register size in bits gives the number of bits by which the first source register is right-shifted.\n\nThis is an alias of RORV. This means:\n\n• The encodings in this description are named to match the encodings of RORV. • The description of RORV gives the operational pseudocode, any CONSTRAINED UNPREDICTABLE behavior, and any operational information for this instruction.", + "syntax": [ + "ROR , , == RORV , , ", + "ROR , , == RORV , , " + ], + "operation_asl": "The description of RORV gives the operational pseudocode for this instruction." + } + ], + "RORV": [ + { + "c62_id": "C6.2.348", + "title": "RORV", + "page": 2543, + "page_end": 2544, + "summary": "Rotate right variable\n\nThis instruction provides the value of the contents of a register rotated by a variable number of bits. The bits that are rotated off the right end are inserted into the vacated bit positions on the left. The value of the second source register modulo the register size in bits gives the number of bits by which the first source register is right-shifted.\n\nThis instruction is used by the alias ROR (register).", + "syntax": [ + "RORV , , ", + "RORV , , " + ], + "operation_asl": "constant bits(datasize) operand2 = X[m, datasize];\nX[d, datasize] = ShiftReg(n, shift_type, UInt(operand2) MOD datasize, datasize);" + } + ], + "BFXIL": [ + { + "c62_id": "C6.2.40", + "title": "BFXIL", + "page": 1854, + "page_end": 1855, + "summary": "Bitfield extract and insert at low end\n\nThis instruction copies a bitfield of bits starting from bit position in the source register to the least significant bits of the destination register, leaving the other destination bits unchanged.\n\nThis is an alias of BFM. This means:\n\n• The encodings in this description are named to match the encodings of BFM. • The description of BFM gives the operational pseudocode, any CONSTRAINED UNPREDICTABLE behavior, and any operational information for this instruction.", + "syntax": [ + "BFXIL , , #, # == BFM , , #, #(+-1)", + "BFXIL , , #, # == BFM , , #, #(+-1)" + ], + "operation_asl": "The description of BFM gives the operational pseudocode for this instruction." + }, + { + "c62_id": "C6.2.39", + "title": "BFM", + "page": 1852, + "page_end": 1853, + "summary": "Bitfield move\n\nThis instruction is usually accessed via one of its aliases, which are always preferred for disassembly.\n\nIf is greater than or equal to , this copies a bitfield of (-+1) bits starting from bit position in the source register to the least significant bits of the destination register.\n\nIf is less than , this copies a bitfield of (+1) bits from the least significant bits of the source register to bit position (regsize-) of the destination register, where regsize is the destination register size of 32 or 64 bits.\n\nIn both cases, the other bits of the destination register remain unchanged.\n\nThis instruction is used by the aliases BFC, BFI, and BFXIL.", + "syntax": [ + "BFM , , #, #", + "BFM , , #, #" + ], + "operation_asl": "constant bits(datasize) dst = X[d, datasize];\nconstant bits(datasize) src = X[n, datasize];\n// Perform bitfield move on low bits\nconstant bits(datasize) bot = (dst AND NOT(wmask)) OR (ROR(src, r) AND wmask);\n// Combine extension bits and result bits\nX[d, datasize] = (dst AND NOT(tmask)) OR (bot AND tmask);" + } + ], + "SBFX": [ + { + "c62_id": "C6.2.355", + "title": "SBFX", + "page": 2556, + "page_end": 2557, + "summary": "Signed bitfield extract\n\nThis instruction copies a bitfield of bits starting from bit position in the source register to the least significant bits of the destination register, and sets destination bits above the bitfield to a copy of the most significant bit of the bitfield.\n\nThis is an alias of SBFM. This means:\n\n• The encodings in this description are named to match the encodings of SBFM. • The description of SBFM gives the operational pseudocode, any CONSTRAINED UNPREDICTABLE behavior, and any operational information for this instruction.", + "syntax": [ + "SBFX , , #, # == SBFM , , #, #(+-1)", + "SBFX , , #, # == SBFM , , #, #(+-1)" + ], + "operation_asl": "The description of SBFM gives the operational pseudocode for this instruction." + }, + { + "c62_id": "C6.2.354", + "title": "SBFM", + "page": 2554, + "page_end": 2555, + "summary": "Signed bitfield move\n\nThis instruction is usually accessed via one of its aliases, which are always preferred for disassembly.\n\nIf is greater than or equal to , this copies a bitfield of (-+1) bits starting from bit position in the source register to the least significant bits of the destination register.\n\nIf is less than , this copies a bitfield of (+1) bits from the least significant bits of the source register to bit position (regsize-) of the destination register, where regsize is the destination register size of 32 or 64 bits.\n\nIn both cases, the destination bits below the bitfield are set to zero, and the bits above the bitfield are set to a copy of the most significant bit of the bitfield.\n\nThis instruction is used by the aliases ASR (immediate), SBFIZ, SBFX, SXTB, SXTH, and SXTW.", + "syntax": [ + "SBFM , , #, #", + "SBFM , , #, #" + ], + "operation_asl": "constant bits(datasize) src = X[n, datasize];\n// Perform bitfield move on low bits\nconstant bits(datasize) bot = ROR(src, r) AND wmask;\nconstant bits(datasize) top = Replicate(src, datasize);\n// Combine extension bits and result bits\nX[d, datasize] = (top AND NOT(tmask)) OR (bot AND tmask);" + } + ], + "UBFX": [ + { + "c62_id": "C6.2.487", + "title": "UBFX", + "page": 2843, + "page_end": 2844, + "summary": "Unsigned bitfield extract\n\nThis instruction copies a bitfield of bits starting from bit position in the source register to the least significant bits of the destination register, and sets destination bits above the bitfield to zero.\n\nThis is an alias of UBFM. This means:\n\n• The encodings in this description are named to match the encodings of UBFM. • The description of UBFM gives the operational pseudocode, any CONSTRAINED UNPREDICTABLE behavior, and any operational information for this instruction.", + "syntax": [ + "UBFX , , #, # == UBFM , , #, #(+-1)", + "UBFX , , #, # == UBFM , , #, #(+-1)" + ], + "operation_asl": "The description of UBFM gives the operational pseudocode for this instruction." + }, + { + "c62_id": "C6.2.486", + "title": "UBFM", + "page": 2841, + "page_end": 2842, + "summary": "Unsigned bitfield move\n\nThis instruction is usually accessed via one of its aliases, which are always preferred for disassembly.\n\nIf is greater than or equal to , this copies a bitfield of (-+1) bits starting from bit position in the source register to the least significant bits of the destination register.\n\nIf is less than , this copies a bitfield of (+1) bits from the least significant bits of the source register to bit position (regsize-) of the destination register, where regsize is the destination register size of 32 or 64 bits.\n\nIn both cases, the destination bits below and above the bitfield are set to zero.\n\nThis instruction is used by the aliases LSL (immediate), LSR (immediate), UBFIZ, UBFX, UXTB, and UXTH.", + "syntax": [ + "UBFM , , #, #", + "UBFM , , #, #" + ], + "operation_asl": "constant bits(datasize) src = X[n, datasize];\n// Perform bitfield move on low bits\nconstant bits(datasize) bot = ROR(src, r) AND wmask;\n// Combine extension bits and result bits\nX[d, datasize] = bot AND tmask;" + } + ], + "BFC": [ + { + "c62_id": "C6.2.37", + "title": "BFC", + "page": 1848, + "page_end": 1849, + "summary": "Bitfield clear\n\nThis instruction sets a bitfield of bits at bit position of the destination register to zero, leaving the other destination bits unchanged.\n\nThis is an alias of BFM. This means:\n\n• The encodings in this description are named to match the encodings of BFM. • The description of BFM gives the operational pseudocode, any CONSTRAINED UNPREDICTABLE behavior, and any operational information for this instruction.", + "syntax": [ + "BFC , #, # == BFM , WZR, #(- MOD 32), #(-1)", + "BFC , #, # == BFM , XZR, #(- MOD 64), #(-1)" + ], + "operation_asl": "The description of BFM gives the operational pseudocode for this instruction." + }, + { + "c62_id": "C6.2.39", + "title": "BFM", + "page": 1852, + "page_end": 1853, + "summary": "Bitfield move\n\nThis instruction is usually accessed via one of its aliases, which are always preferred for disassembly.\n\nIf is greater than or equal to , this copies a bitfield of (-+1) bits starting from bit position in the source register to the least significant bits of the destination register.\n\nIf is less than , this copies a bitfield of (+1) bits from the least significant bits of the source register to bit position (regsize-) of the destination register, where regsize is the destination register size of 32 or 64 bits.\n\nIn both cases, the other bits of the destination register remain unchanged.\n\nThis instruction is used by the aliases BFC, BFI, and BFXIL.", + "syntax": [ + "BFM , , #, #", + "BFM , , #, #" + ], + "operation_asl": "constant bits(datasize) dst = X[d, datasize];\nconstant bits(datasize) src = X[n, datasize];\n// Perform bitfield move on low bits\nconstant bits(datasize) bot = (dst AND NOT(wmask)) OR (ROR(src, r) AND wmask);\n// Combine extension bits and result bits\nX[d, datasize] = (dst AND NOT(tmask)) OR (bot AND tmask);" + } + ], + "BFI": [ + { + "c62_id": "C6.2.38", + "title": "BFI", + "page": 1850, + "page_end": 1851, + "summary": "Bitfield insert\n\nThis instruction copies a bitfield of bits from the least significant bits of the source register to bit position of the destination register, leaving the other destination bits unchanged.\n\nThis is an alias of BFM. This means:\n\n• The encodings in this description are named to match the encodings of BFM. • The description of BFM gives the operational pseudocode, any CONSTRAINED UNPREDICTABLE behavior, and any operational information for this instruction.", + "syntax": [ + "BFI , , #, # == BFM , , #(- MOD 32), #(-1)", + "BFI , , #, # == BFM , , #(- MOD 64), #(-1)" + ], + "operation_asl": "The description of BFM gives the operational pseudocode for this instruction." + }, + { + "c62_id": "C6.2.39", + "title": "BFM", + "page": 1852, + "page_end": 1853, + "summary": "Bitfield move\n\nThis instruction is usually accessed via one of its aliases, which are always preferred for disassembly.\n\nIf is greater than or equal to , this copies a bitfield of (-+1) bits starting from bit position in the source register to the least significant bits of the destination register.\n\nIf is less than , this copies a bitfield of (+1) bits from the least significant bits of the source register to bit position (regsize-) of the destination register, where regsize is the destination register size of 32 or 64 bits.\n\nIn both cases, the other bits of the destination register remain unchanged.\n\nThis instruction is used by the aliases BFC, BFI, and BFXIL.", + "syntax": [ + "BFM , , #, #", + "BFM , , #, #" + ], + "operation_asl": "constant bits(datasize) dst = X[d, datasize];\nconstant bits(datasize) src = X[n, datasize];\n// Perform bitfield move on low bits\nconstant bits(datasize) bot = (dst AND NOT(wmask)) OR (ROR(src, r) AND wmask);\n// Combine extension bits and result bits\nX[d, datasize] = (dst AND NOT(tmask)) OR (bot AND tmask);" + } + ], + "EXTR": [ + { + "c62_id": "C6.2.160", + "title": "EXTR", + "page": 2174, + "page_end": 2175, + "summary": "Extract register\n\nThis instruction extracts a register from a pair of registers.\n\nThis instruction is used by the alias ROR (immediate).", + "syntax": [ + "EXTR , , , #", + "EXTR , , , #" + ], + "operation_asl": "bits(datasize) result;\nconstant bits(datasize) operand1 = X[n, datasize];\nconstant bits(datasize) operand2 = X[m, datasize];\nconstant bits(2*datasize) concat = operand1:operand2;\nresult = concat<(lsb+datasize)-1:lsb>;\nX[d, datasize] = result;" + } + ], + "MOV": [ + { + "c62_id": "C6.2.281", + "title": "MOV (register)", + "page": 2413, + "page_end": 2414, + "summary": "Move register value\n\nThis instruction copies the value in a source register to the destination register.\n\nThis is an alias of ORR (shifted register). This means:\n\n• The encodings in this description are named to match the encodings of ORR (shifted register). • The description of ORR (shifted register) gives the operational pseudocode, any CONSTRAINED UNPREDICTABLE behavior, and any operational information for this instruction.", + "syntax": [ + "MOV , == ORR , WZR, ", + "MOV , == ORR , XZR, " + ], + "operation_asl": "The description of ORR (shifted register) gives the operational pseudocode for this instruction." + }, + { + "c62_id": "C6.2.277", + "title": "MOV (to/from SP)", + "page": 2407, + "page_end": 2408, + "summary": "Move register value to or from SP\n\nThis instruction copies the value of a register to or from the stack pointer.\n\nThis is an alias of ADD (immediate). This means:\n\n• The encodings in this description are named to match the encodings of ADD (immediate). • The description of ADD (immediate) gives the operational pseudocode, any CONSTRAINED UNPREDICTABLE behavior, and any operational information for this instruction.", + "syntax": [ + "MOV , == ADD , , #0", + "MOV , == ADD , , #0" + ], + "operation_asl": "The description of ADD (immediate) gives the operational pseudocode for this instruction." + } + ], + "MOVN": [ + { + "c62_id": "C6.2.283", + "title": "MOVN", + "page": 2416, + "page_end": 2417, + "summary": "Move wide with NOT\n\nThis instruction moves the inverse of an optionally-shifted 16-bit immediate value to a register.\n\nThis instruction is used by the alias MOV (inverted wide immediate).", + "syntax": [ + "MOVN , #{, LSL #}", + "MOVN , #{, LSL #}" + ], + "operation_asl": "bits(datasize) result = Zeros(datasize);\nresult = imm;\nX[d, datasize] = NOT(result);" + } + ], + "MOVZ": [ + { + "c62_id": "C6.2.284", + "title": "MOVZ", + "page": 2418, + "page_end": 2419, + "summary": "Move wide with zero\n\nThis instruction moves an optionally-shifted 16-bit immediate value to a register.\n\nThis instruction is used by the alias MOV (wide immediate).", + "syntax": [ + "MOVZ , #{, LSL #}", + "MOVZ , #{, LSL #}" + ], + "operation_asl": "bits(datasize) result = Zeros(datasize);\nresult = imm;\nX[d, datasize] = result;" + } + ], + "MOVK": [ + { + "c62_id": "C6.2.282", + "title": "MOVK", + "page": 2415, + "page_end": 2415, + "summary": "Move wide with keep\n\nThis instruction moves an optionally-shifted 16-bit immediate value into a register, keeping other bits unchanged.", + "syntax": [ + "MOVK , #{, LSL #}", + "MOVK , #{, LSL #}" + ], + "operation_asl": "bits(datasize) result = X[d, datasize];\nresult = imm;\nX[d, datasize] = result;" + } + ], + "ADR": [ + { + "c62_id": "C6.2.12", + "title": "ADR", + "page": 1809, + "page_end": 1809, + "summary": "Form PC-relative address\n\nThis instruction adds an immediate value to the PC value to form a PC-relative address, and writes the result to the destination register.", + "syntax": [ + "ADR ,