From 2130053d398ecbbb62d3a20afb55483940191e8d Mon Sep 17 00:00:00 2001 From: Oskar Abrahamsson Date: Sun, 28 Mar 2021 14:39:38 +0200 Subject: [PATCH 1/5] Avoid register r18 on the Arm8 backend According to the Arm 64-bit Procedure Call Standard [1], register r18 is platform specific and should be avoided in platform-independent code. On Apple Arm64 platforms this register can't be used [2]. [1] https://developer.arm.com/documentation/ihi0055/d/ [2] https://developer.apple.com/documentation/xcode/writing_arm64_code_for_apple_platforms --- compiler/backend/arm8/arm8_configScript.sml | 5 ++++- compiler/encoders/arm8/arm8_targetScript.sml | 3 ++- 2 files changed, 6 insertions(+), 2 deletions(-) diff --git a/compiler/backend/arm8/arm8_configScript.sml b/compiler/backend/arm8/arm8_configScript.sml index f455cf9bfc..e904c9e6c4 100644 --- a/compiler/backend/arm8/arm8_configScript.sml +++ b/compiler/backend/arm8/arm8_configScript.sml @@ -8,6 +8,7 @@ val _ = new_theory"arm8_config"; val arm8_names_def = Define ` arm8_names = (* source can use 30 regs (0-29), + target's r18 should be avoided (platform reserved), target's r26 must be avoided (extra encoding register), target's r31 must be avoided (stack pointer), source 0 must represent r30 (link register), @@ -19,7 +20,9 @@ val arm8_names_def = Define ` insert 3 2 o insert 4 3 o insert 26 4 o - (* Next one is for well-formedness only *) + insert 18 5 o + (* Next ones are for well-formedness only *) + insert 29 18 o insert 30 26) LN:num num_map` val arm8_names_def = save_thm("arm8_names_def[compute]", diff --git a/compiler/encoders/arm8/arm8_targetScript.sml b/compiler/encoders/arm8/arm8_targetScript.sml index b646b0d275..00dfb6390c 100644 --- a/compiler/encoders/arm8/arm8_targetScript.sml +++ b/compiler/encoders/arm8/arm8_targetScript.sml @@ -269,7 +269,8 @@ val arm8_config_def = Define` ; encode := arm8_enc ; reg_count := 32 ; fp_reg_count := 0 - ; avoid_regs := [26; 31] + (* register x18 is reserved on some platforms, e.g., Apple platforms *) + ; avoid_regs := [18; 26; 31] ; link_reg := SOME 30 ; two_reg_arith := F ; big_endian := F From fa107de335b8d1dca60e6f2d122839c1a7c479f9 Mon Sep 17 00:00:00 2001 From: Oskar Abrahamsson Date: Sun, 28 Mar 2021 21:09:20 +0200 Subject: [PATCH 2/5] Adapt arm8 export to use relative addressing Absolute addressing is not supported on for example Apple arm64. Tested on both Apple arm64 and 64-bit ARM Ubuntu under qemu. --- compiler/backend/arm8/export_arm8Script.sml | 23 ++++++++++++++++----- 1 file changed, 18 insertions(+), 5 deletions(-) diff --git a/compiler/backend/arm8/export_arm8Script.sml b/compiler/backend/arm8/export_arm8Script.sml index 5e5c911050..812564446a 100644 --- a/compiler/backend/arm8/export_arm8Script.sml +++ b/compiler/backend/arm8/export_arm8Script.sml @@ -27,16 +27,29 @@ val startup = " .globl cdecl(cml_heap)"; " .globl cdecl(cml_stack)"; " .globl cdecl(cml_stackend)"; + "#ifndef __APPLE__"; " .type cml_main, function"; + "#endif"; + ""; + ".macro _ldrel reg sym"; + "#ifdef __APPLE__"; + "adrp \\reg, \\sym@PAGE"; + "add \\reg, \\reg, \\sym@PAGEOFF"; + "#else"; + "adrp \\reg, \\sym"; + "add \\reg, \\reg, :lo12:\\sym"; + "#endif"; + ".endm"; + ""; "cdecl(cml_main):"; - " ldr x0,=cake_main /* arg1: entry address */"; - " ldr x1,=cdecl(cml_heap) /* arg2: first address of heap */"; + " _ldrel x0, cake_main /* arg1: entry address */"; + " _ldrel x1, cdecl(cml_heap) /* arg2: first address of heap */"; " ldr x1,[x1]"; - " ldr x2,=cake_bitmaps"; + " _ldrel x2, cake_bitmaps"; " str x2,[x1] /* store bitmap pointer */"; - " ldr x2,=cdecl(cml_stack) /* arg3: first address of stack */"; + " _ldrel x2, cdecl(cml_stack) /* arg3: first address of stack */"; " ldr x2,[x2]"; - " ldr x3,=cdecl(cml_stackend) /* arg4: first address past the stack */"; + " _ldrel x3, cdecl(cml_stackend) /* arg4: first address past the stack */"; " ldr x3,[x3]"; " b cake_main"; " .ltorg"; From efee455718f36f4dd0ab128bf263ea2110d0cc7e Mon Sep 17 00:00:00 2001 From: Oskar Abrahamsson Date: Mon, 29 Mar 2021 10:44:19 +0200 Subject: [PATCH 3/5] Fix arm8_targetProof --- compiler/encoders/arm8/proofs/arm8_targetProofScript.sml | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/compiler/encoders/arm8/proofs/arm8_targetProofScript.sml b/compiler/encoders/arm8/proofs/arm8_targetProofScript.sml index ed53f99799..c8c0ec585e 100644 --- a/compiler/encoders/arm8/proofs/arm8_targetProofScript.sml +++ b/compiler/encoders/arm8/proofs/arm8_targetProofScript.sml @@ -155,8 +155,8 @@ val lem13 = Q.prove( val lem14 = Q.prove( `!s state c: word64 n. - target_state_rel arm8_target s state /\ n <> 26 /\ n <> 31 /\ n < 32 /\ - aligned 3 (c + s.regs n) ==> aligned 3 (c + state.REG (n2w n))`, + target_state_rel arm8_target s state /\ n <> 18 /\ n <> 26 /\ n <> 31 /\ + n < 32 /\ aligned 3 (c + s.regs n) ==> aligned 3 (c + state.REG (n2w n))`, rw [asmPropsTheory.target_state_rel_def, arm8_target_def, arm8_config_def] ) @@ -747,7 +747,9 @@ fun state_tac thms = fs ([asmPropsTheory.sym_target_state_rel, arm8_target_def, arm8_config, asmPropsTheory.all_pcs, arm8_ok_def, lem30, set_sepTheory.fun2set_eq] @ thms) - \\ rw [combinTheory.APPLY_UPDATE_THM, alignmentTheory.aligned_numeric] + \\ rewrite_tac [combinTheory.APPLY_UPDATE_THM, alignmentTheory.aligned_numeric] + \\ fs [] + \\ rw [] \\ rfs [] val shift_cases_tac = From f1e0d51410699ed7d0e73ee9abd5eefad1d272bd Mon Sep 17 00:00:00 2001 From: Oskar Abrahamsson Date: Mon, 29 Mar 2021 11:51:09 +0200 Subject: [PATCH 4/5] Update arm8_config and proof Use Yong-Kiam's suggested mapping (which is actually a permutation) and add a few more registers to the callee-saved regs. --- compiler/backend/arm8/arm8_configScript.sml | 10 ++++++---- .../backend/arm8/proofs/arm8_configProofScript.sml | 2 +- 2 files changed, 7 insertions(+), 5 deletions(-) diff --git a/compiler/backend/arm8/arm8_configScript.sml b/compiler/backend/arm8/arm8_configScript.sml index e904c9e6c4..2e0a62b262 100644 --- a/compiler/backend/arm8/arm8_configScript.sml +++ b/compiler/backend/arm8/arm8_configScript.sml @@ -7,20 +7,22 @@ val _ = new_theory"arm8_config"; val arm8_names_def = Define ` arm8_names = - (* source can use 30 regs (0-29), + (* source can use 29 regs (0-28), target's r18 should be avoided (platform reserved), target's r26 must be avoided (extra encoding register), target's r31 must be avoided (stack pointer), source 0 must represent r30 (link register), source 1-4 must be r0-r3 (1st 4 args), - top three (28-30) must be callee-saved (in r19-r29) *) + top three (26-28) must be callee-saved (in r19-r28) *) (insert 0 30 o insert 1 0 o insert 2 1 o insert 3 2 o insert 4 3 o - insert 26 4 o - insert 18 5 o + insert 18 4 o + insert 25 29 o + insert 26 25 o + (*insert 26 29 o*) (* Next ones are for well-formedness only *) insert 29 18 o insert 30 26) LN:num num_map` diff --git a/compiler/backend/arm8/proofs/arm8_configProofScript.sml b/compiler/backend/arm8/proofs/arm8_configProofScript.sml index a3806bc55a..0a9af9d674 100644 --- a/compiler/backend/arm8/proofs/arm8_configProofScript.sml +++ b/compiler/backend/arm8/proofs/arm8_configProofScript.sml @@ -15,7 +15,7 @@ val is_arm8_machine_config_def = Define` mc.ptr_reg = 0 ∧ mc.len2_reg =3 ∧ mc.ptr2_reg = 2 ∧ - mc.callee_saved_regs = [27;28;29]`; + mc.callee_saved_regs = [19;20;21;22;23;24;25;26;27;28]`; val names_tac = simp[tlookup_bij_iff] \\ EVAL_TAC From e4695275e4d5b97462460088478cf7d14f19092f Mon Sep 17 00:00:00 2001 From: Oskar Abrahamsson Date: Mon, 29 Mar 2021 12:43:06 +0200 Subject: [PATCH 5/5] Remove commented-out junk --- compiler/backend/arm8/arm8_configScript.sml | 1 - 1 file changed, 1 deletion(-) diff --git a/compiler/backend/arm8/arm8_configScript.sml b/compiler/backend/arm8/arm8_configScript.sml index 2e0a62b262..ca01dc54c9 100644 --- a/compiler/backend/arm8/arm8_configScript.sml +++ b/compiler/backend/arm8/arm8_configScript.sml @@ -22,7 +22,6 @@ val arm8_names_def = Define ` insert 18 4 o insert 25 29 o insert 26 25 o - (*insert 26 29 o*) (* Next ones are for well-formedness only *) insert 29 18 o insert 30 26) LN:num num_map`