Merge branch 'master' of https://github.com/AbsInt/CompCert into mppa-work-upstream-merge

4 files changed, 26 insertions, 5 deletions

diff --git a/aarch64/Asmexpand.ml b/aarch64/Asmexpand.ml
index ab155e9c..55922e9e 100644
--- a/aarch64/Asmexpand.ml
+++ b/aarch64/Asmexpand.ml
@@ -408,13 +408,28 @@ let expand_instruction instr =
   | _ ->
      emit instr
 
-let int_reg_to_dwarf r = 0              (* TODO *)
-
-let float_reg_to_dwarf r = 0            (* TODO *)
+let int_reg_to_dwarf = function
+  | X0 -> 0 | X1 -> 1 | X2 -> 2 | X3 -> 3 | X4 -> 4
+  | X5 -> 5 | X6 -> 6 | X7 -> 7 | X8 -> 8 | X9 -> 9
+  | X10 -> 10 | X11 -> 11 | X12 -> 12 | X13 -> 13 | X14 -> 14
+  | X15 -> 15 | X16 -> 16 | X17 -> 17 | X18 -> 18 | X19 -> 19
+  | X20 -> 20 | X21 -> 21 | X22 -> 22 | X23 -> 23 | X24 -> 24
+  | X25 -> 25 | X26 -> 26 | X27 -> 27 | X28 -> 28 | X29 -> 29
+  | X30 -> 30
+
+let float_reg_to_dwarf = function
+  | D0 -> 64 | D1 -> 65 | D2 -> 66 | D3 -> 67 | D4 -> 68
+  | D5 -> 69 | D6 -> 70 | D7 -> 71 | D8 -> 72 | D9 -> 73
+  | D10 -> 74 | D11 -> 75 | D12 -> 76 | D13 -> 77 | D14 -> 78
+  | D15 -> 79 | D16 -> 80 | D17 -> 81 | D18 -> 82 | D19 -> 83
+  | D20 -> 84 | D21 -> 85 | D22 -> 86 | D23 -> 87 | D24 -> 88
+  | D25 -> 89 | D26 -> 90 | D27 -> 91 | D28 -> 92 | D29 -> 93
+  | D30 -> 94 | D31 -> 95
 
 let preg_to_dwarf = function
    | IR r -> int_reg_to_dwarf r
    | FR r -> float_reg_to_dwarf r
+   | SP -> 31
    | _ -> assert false
 
 let expand_function id fn =
diff --git a/aarch64/Asmgen.v b/aarch64/Asmgen.v
index c7332329..0c72c7cc 100644
--- a/aarch64/Asmgen.v
+++ b/aarch64/Asmgen.v
@@ -20,6 +20,11 @@ Local Open Scope string_scope.
 Local Open Scope list_scope.
 Local Open Scope error_monad_scope.
 
+(** Alignment check for symbols *)
+
+Parameter symbol_is_aligned : ident -> Z -> bool.
+(** [symbol_is_aligned id sz] checks whether the symbol [id] is [sz] aligned *)
+
 (** Extracting integer or float registers. *)
 
 Definition ireg_of (r: mreg) : res ireg :=
@@ -942,7 +947,7 @@ Definition transl_addressing (sz: Z) (addr: Op.addressing) (args: list mreg)
                            (insn (ADimm X16 Int64.zero) :: k))
   | Aglobal id ofs, nil =>
       assertion (negb (Archi.pic_code tt));
-      if Ptrofs.eq (Ptrofs.modu ofs (Ptrofs.repr sz)) Ptrofs.zero
+      if Ptrofs.eq (Ptrofs.modu ofs (Ptrofs.repr sz)) Ptrofs.zero && symbol_is_aligned id sz
       then OK (Padrp X16 id ofs :: insn (ADadr X16 id ofs) :: k)
       else OK (loadsymbol X16 id ofs (insn (ADimm X16 Int64.zero) :: k))
   | Ainstack ofs, nil =>
diff --git a/aarch64/Asmgenproof1.v b/aarch64/Asmgenproof1.v
index 245eeb62..b622a0bb 100644
--- a/aarch64/Asmgenproof1.v
+++ b/aarch64/Asmgenproof1.v
@@ -1592,7 +1592,7 @@ Proof.
   simpl; rewrite Int64.add_zero; auto.
   intros. apply C; eauto with asmgen.
 - (* Aglobal *)
-  destruct (Ptrofs.eq (Ptrofs.modu ofs (Ptrofs.repr sz)) Ptrofs.zero); inv TR.
+  destruct (Ptrofs.eq (Ptrofs.modu ofs (Ptrofs.repr sz)) Ptrofs.zero && symbol_is_aligned id sz); inv TR.
 + econstructor; econstructor; split.
   apply exec_straight_opt_intro. apply exec_straight_one. simpl; eauto. auto.
   split. simpl. Simpl. rewrite symbol_high_low. simpl in EV. congruence.
diff --git a/aarch64/extractionMachdep.v b/aarch64/extractionMachdep.v
index a447d12f..e82056e2 100644
--- a/aarch64/extractionMachdep.v
+++ b/aarch64/extractionMachdep.v
@@ -21,3 +21,4 @@ Extract Constant Archi.pic_code => "fun () -> false".  (* for the time being *)
 (* Asm *)
 Extract Constant Asm.symbol_low => "fun _ _ _ -> assert false".
 Extract Constant Asm.symbol_high => "fun _ _ _ -> assert false".
+Extract Constant Asmgen.symbol_is_aligned => "C2C.atom_is_aligned".