Tentative first fix for offsets of ld/std.

The offsets immediates used in the ld and std instructions must be a
multiple of the word size. This commit changes the two functions which
are used when generating load/stores in Asmgen, accessind and
transl_memory_access.

For accessind one only needs an additional check that the offset is a
multiple of the word size for the case that the high part of the offset
is zero, since otherwise the immediate is loaded into a register anyway.

The transl_memory_access function needs some slightly more complex
adoption. For all variants that do not construct the address in a
register before hand we must check that the offsets are multiples of the
word size and additionally if a symbol is used that the alignment of the
symbol is also a multiple of the word size. Therefore a new parameter is
introduced that allows checking the alignment.

In order to reduce the code duplication for the proofs these two
functions get an additional parameter in order to indicate wether the
offset needs to be a multiple of the word size or not.
Bug 30983

5 files changed, 259 insertions, 152 deletions

diff --git a/powerpc/Asm.v b/powerpc/Asm.v
index 93bc31b8..6b1f2232 100644
--- a/powerpc/Asm.v
+++ b/powerpc/Asm.v
@@ -538,6 +538,8 @@ Axiom small_data_area_addressing:
 
 Parameter symbol_is_rel_data: ident -> ptrofs -> bool.
 
+Parameter symbol_is_aligned: ident -> Z -> bool.
+
 (** Armed with the [low_half] and [high_half] functions,
   we can define the evaluation of a symbolic constant.
   Note that for [const_high], integer constants
diff --git a/powerpc/Asmgen.v b/powerpc/Asmgen.v
index 1dca4ba4..0a75ad58 100644
--- a/powerpc/Asmgen.v
+++ b/powerpc/Asmgen.v
@@ -190,36 +190,38 @@ Definition rolm64 (r1 r2: ireg) (amount: int) (mask: int64) (k: code) :=
 
 (** Accessing slots in the stack frame.  *)
 
+(* For 64 bit load and store the offset needs to be a multiple of word size *)
 Definition accessind {A: Type}
        (instr1: A -> constant -> ireg -> instruction)
        (instr2: A -> ireg -> ireg -> instruction)
+       (unaligned : bool)
        (base: ireg) (ofs: ptrofs) (r: A) (k: code) :=
   let ofs := Ptrofs.to_int ofs in
-  if Int.eq (high_s ofs) Int.zero
+  if Int.eq (high_s ofs) Int.zero && (unaligned || (Int.eq (Int.mods ofs (Int.repr 4)) Int.zero))
   then instr1 r (Cint ofs) base :: k
   else loadimm GPR0 ofs (instr2 r base GPR0 :: k).
 
 Definition loadind (base: ireg) (ofs: ptrofs) (ty: typ) (dst: mreg) (k: code) :=
   match ty, preg_of dst with
-  | Tint, IR r => OK(accessind Plwz Plwzx base ofs r k)
-  | Tany32, IR r => OK(accessind Plwz_a Plwzx_a base ofs r k)
-  | Tsingle, FR r => OK(accessind Plfs Plfsx base ofs r k)
-  | Tlong, IR r => OK(accessind Pld Pldx base ofs r k)
-  | Tfloat, FR r => OK(accessind Plfd Plfdx base ofs r k)
-  | Tany64, IR r => OK(accessind Pld_a Pldx_a base ofs r k)
-  | Tany64, FR r => OK(accessind Plfd_a Plfdx_a base ofs r k)
+  | Tint, IR r => OK(accessind Plwz Plwzx true base ofs r k)
+  | Tany32, IR r => OK(accessind Plwz_a Plwzx_a true base ofs r k)
+  | Tsingle, FR r => OK(accessind Plfs Plfsx true base ofs r k)
+  | Tlong, IR r => OK(accessind Pld Pldx false base ofs r k)
+  | Tfloat, FR r => OK(accessind Plfd Plfdx  true base ofs r k)
+  | Tany64, IR r => OK(accessind Pld_a Pldx_a false base ofs r k)
+  | Tany64, FR r => OK(accessind Plfd_a Plfdx_a true base ofs r k)
   | _, _ => Error (msg "Asmgen.loadind")
   end.
 
 Definition storeind (src: mreg) (base: ireg) (ofs: ptrofs) (ty: typ) (k: code) :=
   match ty, preg_of src with
-  | Tint, IR r => OK(accessind Pstw Pstwx base ofs r k)
-  | Tany32, IR r => OK(accessind Pstw_a Pstwx_a base ofs r k)
-  | Tsingle, FR r => OK(accessind Pstfs Pstfsx base ofs r k)
-  | Tlong, IR r => OK(accessind Pstd Pstdx base ofs r k)
-  | Tfloat, FR r => OK(accessind Pstfd Pstfdx base ofs r k)
-  | Tany64, IR r => OK(accessind Pstd_a Pstdx_a base ofs r k)
-  | Tany64, FR r => OK(accessind Pstfd_a Pstfdx_a base ofs r k)
+  | Tint, IR r => OK(accessind Pstw Pstwx true base ofs r k)
+  | Tany32, IR r => OK(accessind Pstw_a Pstwx_a true base ofs r k)
+  | Tsingle, FR r => OK(accessind Pstfs Pstfsx true base ofs r k)
+  | Tlong, IR r => OK(accessind Pstd Pstdx false base ofs r k)
+  | Tfloat, FR r => OK(accessind Pstfd Pstfdx true base ofs r k)
+  | Tany64, IR r => OK(accessind Pstd_a Pstdx_a false base ofs r k)
+  | Tany64, FR r => OK(accessind Pstfd_a Pstfdx_a true base ofs r k)
   | _, _ => Error (msg "Asmgen.storeind")
   end.
 
@@ -724,32 +726,48 @@ Definition transl_op
 Definition int_temp_for (r: mreg) :=
   if mreg_eq r R12 then GPR11 else GPR12.
 
+Definition symbol_ofs_word_aligned symb ofs :=
+  let ofs := Ptrofs.to_int ofs in
+  symbol_is_aligned symb 4 && (Int.eq (Int.mods ofs (Int.repr 4)) Int.zero).
+
 Definition transl_memory_access
      (mk1: constant -> ireg -> instruction)
      (mk2: ireg -> ireg -> instruction)
+     (unaligned : bool)
      (addr: addressing) (args: list mreg)
      (temp: ireg) (k: code) :=
   match addr, args with
   | Aindexed ofs, a1 :: nil =>
       do r1 <- ireg_of a1;
-      OK (if Int.eq (high_s ofs) Int.zero then
-           mk1 (Cint ofs) r1 :: k
-         else
-           Paddis temp r1 (Cint (high_s ofs)) ::
-           mk1 (Cint (low_s ofs)) temp :: k)
+      OK (if unaligned || Int.eq (Int.mods ofs (Int.repr 4)) Int.zero then
+            if Int.eq (high_s ofs) Int.zero then
+               mk1 (Cint ofs) r1 :: k
+             else
+               Paddis temp r1 (Cint (high_s ofs)) ::
+               mk1 (Cint (low_s ofs)) temp :: k
+          else
+            (loadimm GPR0 ofs (mk2 r1 GPR0 :: k)))
   | Aindexed2, a1 :: a2 :: nil =>
       do r1 <- ireg_of a1; do r2 <- ireg_of a2;
       OK (mk2 r1 r2 :: k)
   | Aglobal symb ofs, nil =>
-      OK (if symbol_is_small_data symb ofs then
-           mk1 (Csymbol_sda symb ofs) GPR0 :: k
+       OK (if symbol_is_small_data symb ofs then
+             if unaligned || symbol_ofs_word_aligned symb ofs then
+               mk1 (Csymbol_sda symb ofs) GPR0 :: k
+             else
+               Paddi temp GPR0 (Csymbol_sda symb ofs) ::
+               mk1 (Cint Int.zero) temp :: k
          else if symbol_is_rel_data symb ofs then
            Paddis temp GPR0 (Csymbol_rel_high symb ofs) ::
            Paddi temp temp (Csymbol_rel_low symb ofs) ::
            mk1 (Cint Int.zero) temp :: k
+         else if  unaligned || symbol_ofs_word_aligned symb ofs then
+           Paddis temp GPR0 (Csymbol_high symb ofs) ::
+           mk1 (Csymbol_low symb ofs) temp :: k
          else
            Paddis temp GPR0 (Csymbol_high symb ofs) ::
-           mk1 (Csymbol_low symb ofs) temp :: k)
+           Paddi temp temp (Csymbol_low symb ofs) ::
+           mk1 (Cint Int.zero) temp :: k)
   | Abased symb ofs, a1 :: nil =>
       do r1 <- ireg_of a1;
       OK (if symbol_is_small_data symb ofs then
@@ -760,16 +778,24 @@ Definition transl_memory_access
             Paddis temp GPR0 (Csymbol_rel_high symb ofs) ::
             Paddi temp temp (Csymbol_rel_low symb ofs) ::
             mk2 temp GPR0 :: k
-          else
+          else if  unaligned || symbol_ofs_word_aligned symb ofs then
             Paddis temp r1 (Csymbol_high symb ofs) ::
-            mk1 (Csymbol_low symb ofs) temp :: k)
+            mk1 (Csymbol_low symb ofs) temp :: k
+          else
+            Pmr GPR0 r1 ::
+            Paddis temp GPR0 (Csymbol_high symb ofs) ::
+            Paddi temp temp (Csymbol_low symb ofs) ::
+            mk2 temp GPR0 :: k)
   | Ainstack ofs, nil =>
       let ofs := Ptrofs.to_int ofs in
-      OK (if Int.eq (high_s ofs) Int.zero then
-           mk1 (Cint ofs) GPR1 :: k
-         else
-           Paddis temp GPR1 (Cint (high_s ofs)) ::
-           mk1 (Cint (low_s ofs)) temp :: k)
+      OK (if  unaligned || Int.eq (Int.mods ofs (Int.repr 4)) Int.zero then
+            if Int.eq (high_s ofs) Int.zero then
+              mk1 (Cint ofs) GPR1 :: k
+            else
+              Paddis temp GPR1 (Cint (high_s ofs)) ::
+              mk1 (Cint (low_s ofs)) temp :: k
+          else
+             addimm temp GPR1 ofs (mk1 (Cint Int.zero) temp :: k))
   | _, _ =>
       Error(msg "Asmgen.transl_memory_access")
   end.
@@ -779,28 +805,28 @@ Definition transl_load (chunk: memory_chunk) (addr: addressing)
   match chunk with
   | Mint8signed =>
       do r <- ireg_of dst;
-      transl_memory_access (Plbz r) (Plbzx r) addr args GPR12 (Pextsb r r :: k)
+      transl_memory_access (Plbz r) (Plbzx r) true addr args GPR12 (Pextsb r r :: k)
   | Mint8unsigned =>
       do r <- ireg_of dst;
-      transl_memory_access (Plbz r) (Plbzx r) addr args GPR12 k
+      transl_memory_access (Plbz r) (Plbzx r) true addr args GPR12 k
   | Mint16signed =>
       do r <- ireg_of dst;
-      transl_memory_access (Plha r) (Plhax r) addr args GPR12 k
+      transl_memory_access (Plha r) (Plhax r) true addr args GPR12 k
   | Mint16unsigned =>
       do r <- ireg_of dst;
-      transl_memory_access (Plhz r) (Plhzx r) addr args GPR12 k
+      transl_memory_access (Plhz r) (Plhzx r) true addr args GPR12 k
   | Mint32 =>
       do r <- ireg_of dst;
-      transl_memory_access (Plwz r) (Plwzx r) addr args GPR12 k
+      transl_memory_access (Plwz r) (Plwzx r) true addr args GPR12 k
   | Mint64 =>
       do r <- ireg_of dst;
-      transl_memory_access (Pld r) (Pldx r) addr args GPR12 k
+      transl_memory_access (Pld r) (Pldx r) false addr args GPR12 k
   | Mfloat32 =>
       do r <- freg_of dst;
-      transl_memory_access (Plfs r) (Plfsx r) addr args GPR12 k
+      transl_memory_access (Plfs r) (Plfsx r) true addr args GPR12 k
   | Mfloat64 =>
       do r <- freg_of dst;
-      transl_memory_access (Plfd r) (Plfdx r) addr args GPR12 k
+      transl_memory_access (Plfd r) (Plfdx r) true addr args GPR12 k
   | _ =>
       Error (msg "Asmgen.transl_load")
   end.
@@ -811,22 +837,22 @@ Definition transl_store (chunk: memory_chunk) (addr: addressing)
   match chunk with
   | Mint8signed | Mint8unsigned =>
       do r <- ireg_of src;
-      transl_memory_access (Pstb r) (Pstbx r) addr args temp k
+      transl_memory_access (Pstb r) (Pstbx r) true addr args temp k
   | Mint16signed | Mint16unsigned =>
       do r <- ireg_of src;
-      transl_memory_access (Psth r) (Psthx r) addr args temp k
+      transl_memory_access (Psth r) (Psthx r) true addr args temp k
   | Mint32  =>
       do r <- ireg_of src;
-      transl_memory_access (Pstw r) (Pstwx r) addr args temp k
+      transl_memory_access (Pstw r) (Pstwx r) true addr args temp k
   | Mint64  =>
       do r <- ireg_of src;
-      transl_memory_access (Pstd r) (Pstdx r) addr args temp k
+      transl_memory_access (Pstd r) (Pstdx r) false addr args temp k
   | Mfloat32 =>
       do r <- freg_of src;
-      transl_memory_access (Pstfs r) (Pstfsx r) addr args temp k
+      transl_memory_access (Pstfs r) (Pstfsx r) true addr args temp k
   | Mfloat64 =>
       do r <- freg_of src;
-      transl_memory_access (Pstfd r) (Pstfdx r) addr args temp k
+      transl_memory_access (Pstfd r) (Pstfdx r) true addr args temp k
   | _ =>
       Error (msg "Asmgen.transl_store")
   end.
diff --git a/powerpc/Asmgenproof.v b/powerpc/Asmgenproof.v
index 23071756..2730e3d6 100644
--- a/powerpc/Asmgenproof.v
+++ b/powerpc/Asmgenproof.v
@@ -205,10 +205,13 @@ Remark loadind_label:
   forall base ofs ty dst k c,
   loadind base ofs ty dst k = OK c -> tail_nolabel k c.
 Proof.
-  unfold loadind, accessind; intros. set (ofs' := Ptrofs.to_int ofs) in *.
+  unfold loadind, accessind ; intros.
+  set (ofs' := Ptrofs.to_int ofs) in *.
+  set (ofs_mod := Int.eq (Int.mods ofs' (Int.repr 4)) Int.zero) in *.
   destruct ty; try discriminate;
   destruct (preg_of dst); try discriminate;
   destruct (Int.eq (high_s ofs') Int.zero);
+  destruct ofs_mod;
   TailNoLabel; eapply tail_nolabel_trans; TailNoLabel.
 Qed.
 
@@ -216,10 +219,13 @@ Remark storeind_label:
   forall base ofs ty src k c,
   storeind src base ofs ty k = OK c -> tail_nolabel k c.
 Proof.
-  unfold storeind, accessind; intros. set (ofs' := Ptrofs.to_int ofs) in *.
+  unfold storeind, accessind;
+  intros. set (ofs' := Ptrofs.to_int ofs) in *.
+  set (ofs_mod := Int.eq (Int.mods ofs' (Int.repr 4)) Int.zero) in *.
   destruct ty; try discriminate;
   destruct (preg_of src); try discriminate;
   destruct (Int.eq (high_s ofs') Int.zero);
+  destruct ofs_mod;
   TailNoLabel; eapply tail_nolabel_trans; TailNoLabel.
 Qed.
 
@@ -298,17 +304,22 @@ Qed.
 
 Remark transl_memory_access_label:
   forall (mk1: constant -> ireg -> instruction) (mk2: ireg -> ireg -> instruction)
-         addr args temp k c,
-  transl_memory_access mk1 mk2 addr args temp k = OK c ->
+         unaligned addr args temp k c,
+  transl_memory_access mk1 mk2 unaligned addr args temp k = OK c ->
   (forall c r, nolabel (mk1 c r)) ->
   (forall r1 r2, nolabel (mk2 r1 r2)) ->
   tail_nolabel k c.
 Proof.
   unfold transl_memory_access; intros; destruct addr; TailNoLabel.
-  destruct (Int.eq (high_s i) Int.zero); TailNoLabel.
-  destruct (symbol_is_small_data i i0). TailNoLabel. destruct (symbol_is_rel_data i i0); TailNoLabel.
+  destruct (unaligned || Int.eq (Int.mods i (Int.repr 4)) Int.zero). destruct (Int.eq (high_s i) Int.zero); TailNoLabel.
+  eapply tail_nolabel_trans. apply loadimm_label. TailNoLabel.
+  destruct (symbol_is_small_data i i0). destruct (unaligned || symbol_ofs_word_aligned i i0); TailNoLabel. destruct (symbol_is_rel_data i i0); TailNoLabel.
+  destruct (unaligned || symbol_ofs_word_aligned i i0); TailNoLabel.
   destruct (symbol_is_small_data i i0). TailNoLabel. destruct (symbol_is_rel_data i i0); TailNoLabel.
+  destruct (unaligned || symbol_ofs_word_aligned i i0); TailNoLabel.
+  destruct (unaligned || Int.eq (Int.mods (Ptrofs.to_int i) (Int.repr 4)) Int.zero).
   destruct (Int.eq (high_s (Ptrofs.to_int i)) Int.zero); TailNoLabel.
+  eapply tail_nolabel_trans. eapply addimm_label. TailNoLabel.
 Qed.
 
 Remark transl_epilogue_label:
diff --git a/powerpc/Asmgenproof1.v b/powerpc/Asmgenproof1.v
index 89514d62..7268b407 100644
--- a/powerpc/Asmgenproof1.v
+++ b/powerpc/Asmgenproof1.v
@@ -805,6 +805,7 @@ Lemma accessind_load_correct:
   forall (A: Type) (inj: A -> preg)
        (instr1: A -> constant -> ireg -> instruction)
        (instr2: A -> ireg -> ireg -> instruction)
+       (unaligned: bool)
        (base: ireg) ofs rx chunk v (rs: regset) m k,
   (forall rs m r1 cst r2,
    exec_instr ge fn (instr1 r1 cst r2) rs m = load1 ge chunk (inj r1) cst r2 rs m) ->
@@ -813,14 +814,15 @@ Lemma accessind_load_correct:
   Mem.loadv chunk m (Val.offset_ptr rs#base ofs) = Some v ->
   base <> GPR0 -> inj rx <> PC ->
   exists rs',
-     exec_straight ge fn (accessind instr1 instr2 base ofs rx k) rs m k rs' m
+     exec_straight ge fn (accessind instr1 instr2 unaligned base ofs rx k) rs m k rs' m
   /\ rs'#(inj rx) = v
   /\ forall r, r <> PC -> r <> inj rx -> r <> GPR0 -> rs'#r = rs#r.
 Proof.
   intros. unfold accessind. set (ofs' := Ptrofs.to_int ofs) in *.
+  set (ofs_mod := unaligned || Int.eq (Int.mods ofs' (Int.repr 4)) Int.zero) in *.
   assert (LD: Mem.loadv chunk m (Val.add (rs base) (Vint ofs')) = Some v)
   by (apply loadv_offset_ptr; auto).
-  destruct (Int.eq (high_s ofs') Int.zero).
+  destruct (Int.eq (high_s ofs') Int.zero && ofs_mod).
 - econstructor; split. apply exec_straight_one.
   rewrite H. unfold load1. rewrite gpr_or_zero_not_zero by auto. simpl.
   rewrite LD. eauto. unfold nextinstr. repeat Simplif.
@@ -862,6 +864,7 @@ Lemma accessind_store_correct:
   forall (A: Type) (inj: A -> preg)
        (instr1: A -> constant -> ireg -> instruction)
        (instr2: A -> ireg -> ireg -> instruction)
+       (unaligned: bool)
        (base: ireg) ofs rx chunk (rs: regset) m m' k,
   (forall rs m r1 cst r2,
    exec_instr ge fn (instr1 r1 cst r2) rs m = store1 ge chunk (inj r1) cst r2 rs m) ->
@@ -870,13 +873,14 @@ Lemma accessind_store_correct:
   Mem.storev chunk m (Val.offset_ptr rs#base ofs) (rs (inj rx)) = Some m' ->
   base <> GPR0 -> inj rx <> PC -> inj rx <> GPR0 ->
   exists rs',
-     exec_straight ge fn (accessind instr1 instr2 base ofs rx k) rs m k rs' m'
+     exec_straight ge fn (accessind instr1 instr2 unaligned base ofs rx k) rs m k rs' m'
   /\ forall r, r <> PC -> r <> GPR0 -> rs'#r = rs#r.
 Proof.
   intros. unfold accessind. set (ofs' := Ptrofs.to_int ofs) in *.
+  set (ofs_mod := unaligned || Int.eq (Int.mods ofs' (Int.repr 4)) Int.zero) in *.
   assert (ST: Mem.storev chunk m (Val.add (rs base) (Vint ofs')) (rs (inj rx)) = Some m')
   by (apply storev_offset_ptr; auto).
-  destruct (Int.eq (high_s ofs') Int.zero).
+  destruct (Int.eq (high_s ofs') Int.zero && ofs_mod).
 - econstructor; split. apply exec_straight_one.
   rewrite H. unfold store1. rewrite gpr_or_zero_not_zero by auto. simpl.
   rewrite ST. eauto. unfold nextinstr. repeat Simplif.
@@ -1540,8 +1544,8 @@ Qed.
 (** Translation of memory accesses *)
 
 Lemma transl_memory_access_correct:
-  forall (P: regset -> Prop) mk1 mk2 addr args temp k c (rs: regset) a m m',
-  transl_memory_access mk1 mk2 addr args temp k = OK c ->
+  forall (P: regset -> Prop) mk1 mk2 unaligned addr args temp k c (rs: regset) a m m',
+  transl_memory_access mk1 mk2 unaligned addr args temp k = OK c ->
   eval_addressing ge (rs#GPR1) addr (map rs (map preg_of args)) = Some a ->
   temp <> GPR0 ->
   (forall cst (r1: ireg) (rs1: regset) k,
@@ -1559,111 +1563,174 @@ Lemma transl_memory_access_correct:
 Proof.
   intros until m'; intros TR ADDR TEMP MK1 MK2.
   unfold transl_memory_access in TR; destruct addr; ArgsInv; simpl in ADDR; inv ADDR.
-  (* Aindexed *)
-  case (Int.eq (high_s i) Int.zero).
-  (* Aindexed short *)
-  apply MK1. rewrite gpr_or_zero_not_zero; eauto with asmgen. auto.
-  (* Aindexed long *)
-  set (rs1 := nextinstr (rs#temp <- (Val.add (rs x) (Vint (Int.shl (high_s i) (Int.repr 16)))))).
-  exploit (MK1 (Cint (low_s i)) temp rs1 k).
-    simpl. rewrite gpr_or_zero_not_zero; eauto with asmgen.
-    unfold rs1; Simpl. rewrite Val.add_assoc.
-Transparent Val.add.
-    simpl. rewrite low_high_s. auto.
-    intros; unfold rs1; Simpl.
-  intros [rs' [EX' AG']].
-  exists rs'. split. apply exec_straight_step with rs1 m.
-  simpl. rewrite gpr_or_zero_not_zero; eauto with asmgen. auto.
-  auto. auto.
-  (* Aindexed2 *)
-  apply MK2. rewrite gpr_or_zero_not_zero; eauto with asmgen. auto.
-  (* Aglobal *)
-  destruct (symbol_is_small_data i i0) eqn:SISD; [ | destruct (symbol_is_rel_data i i0) ]; inv TR.
-  (* Aglobal from small data *)
-  apply MK1. unfold const_low. rewrite small_data_area_addressing by auto.
-  rewrite add_zero_symbol_address. auto.
-  auto.
-  (* Aglobal from relative data *)
-  set (rs1 := nextinstr (rs#temp <- (Val.add Vzero (high_half ge i i0)))).
-  set (rs2 := nextinstr (rs1#temp <- (Genv.symbol_address ge i i0))).
-  exploit (MK1 (Cint Int.zero) temp rs2).
-    simpl. rewrite gpr_or_zero_not_zero by eauto with asmgen.
-    unfold rs2. Simpl. rewrite Val.add_commut. rewrite add_zero_symbol_address. auto.
-    intros; unfold rs2, rs1; Simpl.
-  intros [rs' [EX' AG']].
-  exists rs'; split. apply exec_straight_step with rs1 m; auto.
-  apply exec_straight_step with rs2 m; auto. simpl. unfold rs2.
-  rewrite gpr_or_zero_not_zero by eauto with asmgen. f_equal. f_equal. f_equal.
-  unfold rs1; Simpl. apply low_high_half_zero.
-  eexact EX'. auto.
-  (* Aglobal from absolute data *)
-  set (rs1 := nextinstr (rs#temp <- (Val.add Vzero (high_half ge i i0)))).
-  exploit (MK1 (Csymbol_low i i0) temp rs1).
-    simpl. rewrite gpr_or_zero_not_zero by eauto with asmgen.
-    unfold rs1. Simpl. rewrite low_high_half_zero. auto.
-    intros; unfold rs1; Simpl.
-  intros [rs' [EX' AG']].
-  exists rs'; split. apply exec_straight_step with rs1 m; auto.
-  eexact EX'. auto.
-  (* Abased *)
+  - (* Aindexed *)
+    destruct (unaligned || Int.eq (Int.mods i (Int.repr 4)) Int.zero); [destruct (Int.eq (high_s i) Int.zero) |].
+    + (* Aindexed 4 aligned short *)
+      apply MK1. rewrite gpr_or_zero_not_zero; eauto with asmgen. auto.
+    (* Aindexed 4 aligned long *)
+    + set (rs1 := nextinstr (rs#temp <- (Val.add (rs x) (Vint (Int.shl (high_s i) (Int.repr 16)))))).
+      exploit (MK1 (Cint (low_s i)) temp rs1 k).
+      simpl. rewrite gpr_or_zero_not_zero; eauto with asmgen.
+      unfold rs1; Simpl. rewrite Val.add_assoc.
+      Transparent Val.add.
+      simpl. rewrite low_high_s. auto.
+      intros; unfold rs1; Simpl.
+      intros [rs' [EX' AG']].
+      exists rs'. split. apply exec_straight_step with rs1 m.
+      simpl. rewrite gpr_or_zero_not_zero; eauto with asmgen. auto.
+      auto. auto.
+    + (* Aindexed non 4 aligned *)
+      exploit (loadimm_correct GPR0 i (mk2 x GPR0 :: k) rs).
+      intros (rs' & A & B & C).
+      exploit (MK2 x GPR0 rs').
+      rewrite gpr_or_zero_not_zero; eauto with asmgen.
+      rewrite B. rewrite C; eauto with asmgen. auto.
+      intros.  destruct H as [rs'' [A1 B1]]. exists rs''.
+      split. eapply exec_straight_trans. exact A. exact A1. auto.
+  - (* Aindexed2 *)
+    apply MK2. rewrite gpr_or_zero_not_zero; eauto with asmgen. auto.
+  - (* Aglobal *)
+    destruct (symbol_is_small_data i i0) eqn:SISD; [ | destruct (symbol_is_rel_data i i0) ]; inv TR.
+    + (* Aglobal from small data 4 aligned *)
+      case (unaligned || symbol_ofs_word_aligned i i0).
+      apply MK1. unfold const_low. rewrite small_data_area_addressing by auto.
+      rewrite add_zero_symbol_address. auto. auto.
+      (* Aglobal from small data not aligned *)
+      set (rs1 := nextinstr (rs#temp <- (Val.add (gpr_or_zero rs GPR0) (const_low ge (Csymbol_sda i i0))))).
+      exploit (MK1 (Cint Int.zero) temp rs1). rewrite gpr_or_zero_not_zero; auto.
+      unfold const_low. unfold rs1. Simpl.
+      rewrite gpr_or_zero_zero. unfold const_low.
+      rewrite small_data_area_addressing by auto.
+      rewrite add_zero_symbol_address. rewrite Val.add_commut.
+      rewrite add_zero_symbol_address. auto.
+      intros. unfold rs1. Simpl.
+      intros. destruct H as [rs2 [A B]].
+      exists rs2. split. eapply exec_straight_step. reflexivity.
+      reflexivity. eexact A. apply B.
+    + (* relative data *)
+        set (rs1 := nextinstr (rs#temp <- (Val.add Vzero (high_half ge i i0)))).
+        set (rs2 := nextinstr (rs1#temp <- (Genv.symbol_address ge i i0))).
+        exploit (MK1 (Cint Int.zero) temp rs2).
+        simpl. rewrite gpr_or_zero_not_zero by eauto with asmgen.
+        unfold rs2. Simpl. rewrite Val.add_commut. rewrite add_zero_symbol_address. auto.
+        intros; unfold rs2, rs1; Simpl.
+        intros [rs' [EX' AG']].
+        exists rs'; split. apply exec_straight_step with rs1 m; auto.
+        apply exec_straight_step with rs2 m; auto. simpl. unfold rs2.
+        rewrite gpr_or_zero_not_zero by eauto with asmgen. f_equal. f_equal. f_equal.
+        unfold rs1; Simpl. apply low_high_half_zero.
+        eexact EX'. auto.
+    + (* Aglobal from absolute data *)
+      destruct (unaligned || symbol_ofs_word_aligned i i0).
+      (* Aglobal 4 aligned *)
+      set (rs1 := nextinstr (rs#temp <- (Val.add Vzero (high_half ge i i0)))).
+      exploit (MK1 (Csymbol_low i i0) temp rs1).
+      simpl. rewrite gpr_or_zero_not_zero by eauto with asmgen.
+      unfold rs1. Simpl. rewrite low_high_half_zero. auto.
+      intros; unfold rs1; Simpl.
+      intros [rs' [EX' AG']].
+      exists rs'; split. apply exec_straight_step with rs1 m; auto.
+      eexact EX'. auto.
+      (* Aglobal non aligned *)
+      set (rs1 := nextinstr (rs#temp <- (Val.add Vzero (high_half ge i i0)))).
+      set (rs2 := nextinstr (rs1#temp <- (Genv.symbol_address ge i i0))).
+      exploit (MK1 (Cint Int.zero) temp rs2).
+      simpl. rewrite gpr_or_zero_not_zero by eauto with asmgen.
+      unfold rs2. Simpl. rewrite Val.add_commut. rewrite add_zero_symbol_address.
+      auto. intros; unfold rs2, rs1; Simpl.
+      intros [rs' [EX' AG']].
+      exists rs'; split. apply exec_straight_step with rs1 m; auto.
+      apply exec_straight_step with rs2 m; auto. simpl. unfold rs2.
+      rewrite gpr_or_zero_not_zero; auto. f_equal. f_equal. f_equal.
+      unfold rs1; Simpl. apply low_high_half_zero. eexact EX'. auto.
+  -(* Abased *)
   destruct (symbol_is_small_data i i0) eqn:SISD; [ | destruct (symbol_is_rel_data i i0) ].
-  (* Abased from small data *)
-  set (rs1 := nextinstr (rs#GPR0 <- (Genv.symbol_address ge i i0))).
-  exploit (MK2 x GPR0 rs1 k).
+  + (* Abased from small data *)
+    set (rs1 := nextinstr (rs#GPR0 <- (Genv.symbol_address ge i i0))).
+    exploit (MK2 x GPR0 rs1 k).
     simpl. rewrite gpr_or_zero_not_zero by eauto with asmgen.
     unfold rs1; Simpl. rewrite Val.add_commut. auto.
     intros. unfold rs1; Simpl.
-  intros [rs' [EX' AG']].
-  exists rs'; split. apply exec_straight_step with rs1 m.
-  unfold exec_instr. rewrite gpr_or_zero_zero. f_equal. unfold rs1. f_equal. f_equal.
-  unfold const_low. rewrite small_data_area_addressing; auto.
-  apply add_zero_symbol_address.
-  reflexivity.
-  assumption. assumption.
-  (* Abased from relative data *)
-  set (rs1 := nextinstr (rs#GPR0 <- (rs#x))).
-  set (rs2 := nextinstr (rs1#temp <- (Val.add Vzero (high_half ge i i0)))).
-  set (rs3 := nextinstr (rs2#temp <- (Genv.symbol_address ge i i0))).
-  exploit (MK2 temp GPR0 rs3).
+    intros [rs' [EX' AG']].
+    exists rs'; split. apply exec_straight_step with rs1 m.
+    unfold exec_instr. rewrite gpr_or_zero_zero. f_equal. unfold rs1. f_equal. f_equal.
+    unfold const_low. rewrite small_data_area_addressing; auto.
+    apply add_zero_symbol_address.
+    reflexivity.
+    assumption. assumption.
+  + (* Abased from relative data *)
+    set (rs1 := nextinstr (rs#GPR0 <- (rs#x))).
+    set (rs2 := nextinstr (rs1#temp <- (Val.add Vzero (high_half ge i i0)))).
+    set (rs3 := nextinstr (rs2#temp <- (Genv.symbol_address ge i i0))).
+    exploit (MK2 temp GPR0 rs3).
     rewrite gpr_or_zero_not_zero by eauto with asmgen.
     f_equal. unfold rs3; Simpl. unfold rs3, rs2, rs1; Simpl.
     intros. unfold rs3, rs2, rs1; Simpl.
-  intros [rs' [EX' AG']].
-  exists rs'. split. eapply exec_straight_trans with (rs2 := rs3) (m2 := m).
-  apply exec_straight_three with rs1 m rs2 m; auto.
-  simpl. unfold rs3. f_equal. f_equal. f_equal. rewrite gpr_or_zero_not_zero by auto.
-  unfold rs2; Simpl. apply low_high_half_zero.
-  eexact EX'. auto.
-  (* Abased absolute *)
-  set (rs1 := nextinstr (rs#temp <- (Val.add (rs x) (high_half ge i i0)))).
-  exploit (MK1 (Csymbol_low i i0) temp rs1 k).
+    intros [rs' [EX' AG']].
+    exists rs'. split. eapply exec_straight_trans with (rs2 := rs3) (m2 := m).
+    apply exec_straight_three with rs1 m rs2 m; auto.
+    simpl. unfold rs3. f_equal. f_equal. f_equal. rewrite gpr_or_zero_not_zero by auto.
+    unfold rs2; Simpl. apply low_high_half_zero.
+    eexact EX'. auto.
+  + (* Abased absolute *)
+    destruct (unaligned || symbol_ofs_word_aligned i i0).
+    (* Abased absolute 4 aligned *)
+    set (rs1 := nextinstr (rs#temp <- (Val.add (rs x) (high_half ge i i0)))).
+    exploit (MK1 (Csymbol_low i i0) temp rs1 k).
     simpl. rewrite gpr_or_zero_not_zero; eauto with asmgen.
     unfold rs1. Simpl.
     rewrite Val.add_assoc. rewrite low_high_half. rewrite Val.add_commut. auto.
     intros; unfold rs1; Simpl.
-  intros [rs' [EX' AG']].
-  exists rs'. split. apply exec_straight_step with rs1 m.
-  unfold exec_instr. rewrite gpr_or_zero_not_zero; eauto with asmgen. auto.
-  assumption. assumption.
-  (* Ainstack *)
-  set (ofs := Ptrofs.to_int i) in *.
-  assert (L: Val.lessdef (Val.offset_ptr (rs GPR1) i) (Val.add (rs GPR1) (Vint ofs))).
-  { destruct (rs GPR1); simpl; auto. unfold ofs; rewrite Ptrofs.of_int_to_int; auto. }
-  destruct (Int.eq (high_s ofs) Int.zero); inv TR.
-  apply MK1. simpl. rewrite gpr_or_zero_not_zero; eauto with asmgen. auto.
-  set (rs1 := nextinstr (rs#temp <- (Val.add rs#GPR1 (Vint (Int.shl (high_s ofs) (Int.repr 16)))))).
-  exploit (MK1 (Cint (low_s ofs)) temp rs1 k).
-    simpl. rewrite gpr_or_zero_not_zero; auto.
-    unfold rs1. rewrite nextinstr_inv. rewrite Pregmap.gss.
-    rewrite Val.add_assoc. simpl. rewrite low_high_s. auto.
-    congruence.
-    intros. unfold rs1. rewrite nextinstr_inv; auto. apply Pregmap.gso; auto.
-  intros [rs' [EX' AG']].
-  exists rs'. split. apply exec_straight_step with rs1 m.
-  unfold exec_instr. rewrite gpr_or_zero_not_zero; eauto with asmgen. auto.
-  assumption. assumption.
+    intros [rs' [EX' AG']].
+    exists rs'. split. apply exec_straight_step with rs1 m.
+    unfold exec_instr. rewrite gpr_or_zero_not_zero; eauto with asmgen. auto.
+    assumption. assumption.
+    (* Abased absolute non aligned *)
+    set (rs1 := nextinstr (rs#GPR0 <- (rs#x))).
+    set (rs2 := nextinstr (rs1#temp <- (Val.add Vzero (high_half ge i i0)))).
+    set (rs3 := nextinstr (rs2#temp <- (Genv.symbol_address ge i i0))).
+    exploit (MK2 temp GPR0 rs3).
+    rewrite gpr_or_zero_not_zero by eauto with asmgen.
+    f_equal. unfold rs3; Simpl. unfold rs3, rs2, rs1; Simpl.
+    intros. unfold rs3, rs2, rs1; Simpl.
+    intros [rs' [EX' AG']].
+    exists rs'. split. eapply exec_straight_trans with (rs2 := rs3) (m2 := m).
+    apply exec_straight_three with rs1 m rs2 m; auto.
+    simpl. unfold rs3. f_equal. f_equal. f_equal. rewrite gpr_or_zero_not_zero by auto.
+    unfold rs2; Simpl. apply low_high_half_zero.
+    eexact EX'. auto.
+  - (* Ainstack *)
+    set (ofs := Ptrofs.to_int i) in *.
+    assert (L: Val.lessdef (Val.offset_ptr (rs GPR1) i) (Val.add (rs GPR1) (Vint ofs))).
+    { destruct (rs GPR1); simpl; auto. unfold ofs; rewrite Ptrofs.of_int_to_int; auto. }
+    destruct (unaligned || Int.eq (Int.mods ofs (Int.repr 4)) Int.zero); [destruct (Int.eq (high_s ofs) Int.zero)|]; inv TR.
+    + (* Ainstack short *)
+      apply MK1. simpl. rewrite gpr_or_zero_not_zero; eauto with asmgen. auto.
+    + (* Ainstack non short *)
+      set (rs1 := nextinstr (rs#temp <- (Val.add rs#GPR1 (Vint (Int.shl (high_s ofs) (Int.repr 16)))))).
+      exploit (MK1 (Cint (low_s ofs)) temp rs1 k).
+      simpl. rewrite gpr_or_zero_not_zero; auto.
+      unfold rs1. rewrite nextinstr_inv. rewrite Pregmap.gss.
+      rewrite Val.add_assoc. simpl. rewrite low_high_s. auto.
+      congruence.
+      intros. unfold rs1. rewrite nextinstr_inv; auto. apply Pregmap.gso; auto.
+      intros [rs' [EX' AG']].
+      exists rs'. split. apply exec_straight_step with rs1 m.
+      unfold exec_instr. rewrite gpr_or_zero_not_zero; eauto with asmgen. auto.
+      assumption. assumption.
+    + (* Ainstack non aligned *)
+      exploit (addimm_correct temp GPR1 ofs  (mk1 (Cint Int.zero) temp :: k) rs); eauto with asmgen.
+      intros [rs1 [A [B C]]].
+      exploit (MK1 (Cint Int.zero) temp rs1 k).
+      rewrite gpr_or_zero_not_zero; auto. rewrite B. simpl.
+      destruct (rs GPR1); auto.  simpl. rewrite Ptrofs.add_zero.
+      unfold ofs. rewrite Ptrofs.of_int_to_int. auto. auto.
+      intros. rewrite C; auto. intros [rs2 [EX' AG']].
+      exists rs2. split; auto.
+      eapply exec_straight_trans. eexact A. assumption.
 Qed.
 
+
 (** Translation of loads *)
 
 Lemma transl_load_correct:
@@ -1679,8 +1746,8 @@ Proof.
   intros.
   assert (LD: forall v, Val.lessdef a v -> v = a).
   { intros. inv H2; auto. discriminate H1. }
-  assert (BASE: forall mk1 mk2 k' chunk' v',
-  transl_memory_access mk1 mk2 addr args GPR12 k' = OK c ->
+  assert (BASE: forall mk1 mk2 unaligned k' chunk' v',
+  transl_memory_access mk1 mk2 unaligned addr args GPR12 k' = OK c ->
   Mem.loadv chunk' m a = Some v' ->
   (forall cst (r1: ireg) (rs1: regset),
     exec_instr ge fn (mk1 cst r1) rs1 m =
@@ -1758,8 +1825,8 @@ Local Transparent destroyed_by_store.
     subst src; simpl; congruence.
     change (IR GPR12) with (preg_of R12). red; intros; elim n.
     eapply preg_of_injective; eauto.
-  assert (BASE: forall mk1 mk2 chunk',
-  transl_memory_access mk1 mk2 addr args (int_temp_for src) k = OK c ->
+  assert (BASE: forall mk1 mk2 unaligned chunk',
+  transl_memory_access mk1 mk2 unaligned addr args (int_temp_for src) k = OK c ->
   Mem.storev chunk' m a (rs (preg_of src)) = Some m' ->
   (forall cst (r1: ireg) (rs1: regset),
     exec_instr ge fn (mk1 cst r1) rs1 m =
diff --git a/powerpc/extractionMachdep.v b/powerpc/extractionMachdep.v
index a3e945bf..5193e453 100644
--- a/powerpc/extractionMachdep.v
+++ b/powerpc/extractionMachdep.v
@@ -21,6 +21,7 @@ Extract Constant Asm.high_half => "fun _ _ _ -> assert false".
 Extract Constant Asm.symbol_is_small_data => "C2C.atom_is_small_data".
 Extract Constant Asm.small_data_area_offset => "fun _ _ _ -> assert false".
 Extract Constant Asm.symbol_is_rel_data => "C2C.atom_is_rel_data".
+Extract Constant Asm.symbol_is_aligned => "C2C.atom_is_aligned".
 
 (* Suppression of stupidly big equality functions *)
 Extract Constant Asm.ireg_eq => "fun (x: ireg) (y: ireg) -> x = y".