From c11b19619e82377be9c43e926d66086124637044 Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavierleroy@users.noreply.github.com>
Date: Mon, 2 Mar 2020 18:59:02 +0100
Subject: Update the RISC-V calling conventions, continued (#227)

Double FP arguments passed on stack were incorrectly aligned:
they must be 8-aligned but were 4-aligned only.

This was due to the use of `Location.typealign`, which is the minimal
hardware-supported alignment for a given type, namely 1 word for type Tfloat.
To get the correct alignments, `Location.typesize` must be used instead.
---
 riscV/Conventions1.v | 17 ++++++++++-------
 1 file changed, 10 insertions(+), 7 deletions(-)

(limited to 'riscV/Conventions1.v')

diff --git a/riscV/Conventions1.v b/riscV/Conventions1.v
index 7f8048f6..17326139 100644
--- a/riscV/Conventions1.v
+++ b/riscV/Conventions1.v
@@ -210,7 +210,7 @@ Definition int_arg (ri rf ofs: Z) (ty: typ)
   | Some r =>
       One(R r) :: rec (ri + 1) rf ofs
   | None   =>
-      let ofs := align ofs (typealign ty) in
+      let ofs := align ofs (typesize ty) in
       One(S Outgoing ofs ty)
       :: rec ri rf (ofs + (if Archi.ptr64 then 2 else typesize ty))
   end.
@@ -228,13 +228,13 @@ Definition float_arg (va: bool) (ri rf ofs: Z) (ty: typ)
             One (R r) :: rec ri' (rf + 1) ofs
         else
             (* we are out of integer registers, pass argument on stack *)
-            let ofs := align ofs (typealign ty) in
+            let ofs := align ofs (typesize ty) in
             One(S Outgoing ofs ty)
             :: rec ri' rf (ofs + (if Archi.ptr64 then 2 else typesize ty)))
       else
         One (R r) :: rec ri (rf + 1) ofs
   | None   =>
-      let ofs := align ofs (typealign ty) in
+      let ofs := align ofs (typesize ty) in
       One(S Outgoing ofs ty)
       :: rec ri rf (ofs + (if Archi.ptr64 then 2 else typesize ty))
   end.
@@ -306,10 +306,13 @@ Proof.
   { decide_goal. }
   assert (CSF: forall r, In r float_param_regs -> is_callee_save r = false).
   { decide_goal. }
-  assert (AL: forall ofs ty, ofs >= 0 -> align ofs (typealign ty) >= 0).
+  assert (AL: forall ofs ty, ofs >= 0 -> align ofs (typesize ty) >= 0).
   { intros. 
-    assert (ofs <= align ofs (typealign ty)) by (apply align_le; apply typealign_pos).
+    assert (ofs <= align ofs (typesize ty)) by (apply align_le; apply typesize_pos).
     omega. }
+  assert (ALD: forall ofs ty, ofs >= 0 -> (typealign ty | align ofs (typesize ty))).
+  { intros. eapply Z.divide_trans. apply typealign_typesize.
+    apply align_divides. apply typesize_pos. }
   assert (SK: (if Archi.ptr64 then 2 else 1) > 0).
   { destruct Archi.ptr64; omega. }
   assert (SKK: forall ty, (if Archi.ptr64 then 2 else typesize ty) > 0).
@@ -332,12 +335,12 @@ Proof.
     destruct va; [destruct (zle ri' 8)|idtac]; destruct H.
     + subst p; simpl. apply CSF. eapply list_nth_z_in; eauto.
     + eapply OF; eauto.
-    + subst p; repeat split; auto using align_divides, typealign_pos.
+    + subst p; repeat split; auto.
     + eapply OF; [idtac|eauto]. generalize (AL ofs ty OO) (SKK ty); omega.
     + subst p; simpl. apply CSF. eapply list_nth_z_in; eauto.
     + eapply OF; eauto.
   - destruct H.
-    + subst p; repeat split; auto using align_divides, typealign_pos.
+    + subst p; repeat split; auto.
     + eapply OF; [idtac|eauto]. generalize (AL ofs ty OO) (SKK ty); omega.
   }
   assert (C: forall va ri rf ofs f,
-- 
cgit