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

1 files changed, 17 insertions, 6 deletions

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: