Merge pull request #823 from CakeML/arm64-apple

Adapt arm8 backend for Apple platforms
CakeML · Mar 30, 2021 · d97d412 · d97d412
2 parents 2b84c94 + e469527
commit d97d412
Show file tree

Hide file tree

Showing 5 changed files with 34 additions and 14 deletions.
diff --git a/compiler/backend/arm8/arm8_configScript.sml b/compiler/backend/arm8/arm8_configScript.sml
@@ -7,19 +7,23 @@ 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
-     (* Next one is for well-formedness only *)
+     insert 18 4 o
+     insert 25 29 o
+     insert 26 25 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/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";

diff --git 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

diff --git 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

diff --git 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 =