Merge remote-tracking branch 'origin/mppa-work' into mppa-thread

6 files changed, 203 insertions, 132 deletions

diff --git a/powerpc/Archi.v b/powerpc/Archi.v
index ab348c14..10f38391 100644
--- a/powerpc/Archi.v
+++ b/powerpc/Archi.v
@@ -30,6 +30,10 @@ Definition align_float64 := 8%Z.
 (** Can we use the 64-bit extensions to the PowerPC architecture? *)
 Parameter ppc64 : bool.
 
+(** Should single-precision FP arguments passed on stack be passed 
+    as singles or use double FP format. *)
+Parameter single_passed_as_single : bool.
+
 Definition splitlong := negb ppc64.
 
 Lemma splitlong_ptr32: splitlong = true -> ptr64 = false.
diff --git a/powerpc/CSE2deps.v b/powerpc/CSE2deps.v
new file mode 100644
index 00000000..9db51bbb
--- /dev/null
+++ b/powerpc/CSE2deps.v
@@ -0,0 +1,20 @@
+Require Import BoolEqual Coqlib.
+Require Import AST Integers Floats.
+Require Import Values Memory Globalenvs Events.
+Require Import Op.
+
+
+Definition can_swap_accesses_ofs ofsr chunkr ofsw chunkw :=
+     (0 <=? ofsw) && (ofsw <=? (Ptrofs.modulus - largest_size_chunk))
+  && (0 <=? ofsr) && (ofsr <=? (Ptrofs.modulus - largest_size_chunk))
+  && ((ofsw + size_chunk chunkw <=? ofsr) ||
+      (ofsr + size_chunk chunkr <=? ofsw)).
+
+Definition may_overlap chunk addr args chunk' addr' args' :=
+  match addr, addr', args, args' with
+  | (Aindexed ofs), (Aindexed ofs'),
+    (base :: nil), (base' :: nil) =>
+    if peq base base'
+    then negb (can_swap_accesses_ofs (Int.unsigned ofs') chunk' (Int.unsigned ofs) chunk)
+    else true  | _, _, _, _ => true
+  end.
diff --git a/powerpc/CSE2depsproof.v b/powerpc/CSE2depsproof.v
new file mode 100644
index 00000000..fdded9b6
--- /dev/null
+++ b/powerpc/CSE2depsproof.v
@@ -0,0 +1,135 @@
+Require Import Coqlib Maps Errors Integers Floats Lattice Kildall.
+Require Import AST Linking.
+Require Import Memory Registers Op RTL Maps.
+
+Require Import Globalenvs Values.
+Require Import Linking Values Memory Globalenvs Events Smallstep.
+Require Import Registers Op RTL.
+Require Import CSE2 CSE2deps.
+Require Import Lia.
+
+Lemma ptrofs_size :
+  Ptrofs.wordsize = if Archi.ptr64 then 64%nat else 32%nat.
+Proof.
+  unfold Ptrofs.wordsize.
+  unfold Wordsize_Ptrofs.wordsize.
+  trivial.
+Qed.
+
+Lemma ptrofs_modulus :
+  Ptrofs.modulus = if Archi.ptr64 then 18446744073709551616 else 4294967296.
+Proof.
+  unfold Ptrofs.modulus.
+  rewrite ptrofs_size.
+  destruct Archi.ptr64; reflexivity.
+Qed.
+
+Lemma ptrofs_max_unsigned :
+  Ptrofs.max_unsigned = if Archi.ptr64 then 18446744073709551615 else 4294967295.
+Proof.
+  unfold Ptrofs.max_unsigned.
+  rewrite ptrofs_modulus.
+  destruct Archi.ptr64; reflexivity.
+Qed.
+
+Section SOUNDNESS.
+  Variable F V : Type.
+  Variable genv: Genv.t F V.
+  Variable sp : val.
+
+Section MEMORY_WRITE.
+  Variable m m2 : mem.
+  Variable chunkw chunkr : memory_chunk.
+  Variable base : val.
+  
+  Variable addrw addrr valw : val.
+  Hypothesis STORE : Mem.storev chunkw m addrw valw = Some m2.
+
+  Section INDEXED_AWAY.
+  Variable ofsw ofsr : int.
+  Hypothesis ADDRW : eval_addressing genv sp
+                       (Aindexed ofsw) (base :: nil) = Some addrw. 
+  Hypothesis ADDRR : eval_addressing genv sp
+                       (Aindexed ofsr) (base :: nil) = Some addrr.
+
+  Lemma load_store_away1 :
+    forall RANGEW : 0 <= Int.unsigned ofsw <= Ptrofs.modulus - largest_size_chunk,
+    forall RANGER : 0 <= Int.unsigned ofsr <= Ptrofs.modulus - largest_size_chunk,
+    forall SWAPPABLE :    Int.unsigned ofsw + size_chunk chunkw <= Int.unsigned ofsr
+                       \/ Int.unsigned ofsr + size_chunk chunkr <= Int.unsigned ofsw,
+    Mem.loadv chunkr m2 addrr = Mem.loadv chunkr m addrr.
+  Proof.
+    intros.
+    
+    pose proof (max_size_chunk chunkr) as size_chunkr_bounded.
+    pose proof (max_size_chunk chunkw) as size_chunkw_bounded.
+    unfold largest_size_chunk in *.
+
+    rewrite ptrofs_modulus in *.
+    simpl in *.
+    inv ADDRR.
+    inv ADDRW.
+    destruct base; try discriminate.
+    eapply Mem.load_store_other with (chunk := chunkw) (v := valw) (b := b).
+    exact STORE.
+    right.
+
+    all: try (destruct (Ptrofs.unsigned_add_either i (Ptrofs.of_int ofsr)) as [OFSR | OFSR];
+              rewrite OFSR).
+    all: try (destruct (Ptrofs.unsigned_add_either i (Ptrofs.of_int ofsw)) as [OFSW | OFSW];
+              rewrite OFSW).
+    all: unfold Ptrofs.of_int.
+
+    all: repeat rewrite Ptrofs.unsigned_repr by (unfold Ptrofs.max_unsigned; rewrite ptrofs_modulus; destruct Archi.ptr64; lia).
+    all: repeat rewrite ptrofs_modulus.
+    all: destruct Archi.ptr64; intuition lia.
+  Qed.
+  
+  Theorem load_store_away :
+    can_swap_accesses_ofs (Int.unsigned ofsr) chunkr (Int.unsigned ofsw) chunkw = true ->
+    Mem.loadv chunkr m2 addrr = Mem.loadv chunkr m addrr.
+  Proof.
+    intro SWAP.
+    unfold can_swap_accesses_ofs in SWAP.
+    repeat rewrite andb_true_iff in SWAP.
+    repeat rewrite orb_true_iff in SWAP.
+    repeat rewrite Z.leb_le in SWAP.
+    apply load_store_away1.
+    all: tauto.
+  Qed.
+  End INDEXED_AWAY.
+End MEMORY_WRITE.
+End SOUNDNESS.
+
+
+Section SOUNDNESS.
+  Variable F V : Type.
+  Variable genv: Genv.t F V.
+  Variable sp : val.
+
+Lemma may_overlap_sound:
+  forall m m' : mem,
+  forall chunk addr args chunk' addr' args' v a a' rs,
+    (eval_addressing genv sp addr (rs ## args)) = Some a ->
+    (eval_addressing genv sp addr' (rs ## args')) = Some a' ->
+    (may_overlap chunk addr args chunk' addr' args') = false ->
+    (Mem.storev chunk m a v) = Some m' ->
+    (Mem.loadv chunk' m' a') = (Mem.loadv chunk' m  a').
+Proof.
+  intros until rs.
+  intros ADDR ADDR' OVERLAP STORE.
+  destruct addr; destruct addr'; try discriminate.
+  { (* Aindexed / Aindexed *)
+  destruct args as [ | base [ | ]]. 1,3: discriminate.
+  destruct args' as [ | base' [ | ]]. 1,3: discriminate.
+  simpl in OVERLAP.
+  destruct (peq base base'). 2: discriminate.
+  subst base'.
+  destruct (can_swap_accesses_ofs (Int.unsigned i0) chunk' (Int.unsigned i) chunk) eqn:SWAP.
+  2: discriminate.
+  simpl in *.
+  eapply load_store_away with (F:=F) (V:=V) (genv:=genv) (sp:=sp); eassumption.
+  }
+Qed.
+
+End SOUNDNESS.
diff --git a/powerpc/Conventions1.v b/powerpc/Conventions1.v
index 25d9c081..5c9cbd4f 100644
--- a/powerpc/Conventions1.v
+++ b/powerpc/Conventions1.v
@@ -208,7 +208,16 @@ Fixpoint loc_arguments_rec
       | Some ireg =>
           One (R ireg) :: loc_arguments_rec tys (ir + 1) fr ofs
       end
-  | (Tfloat | Tsingle | Tany64) as ty :: tys =>
+  | Tsingle as ty :: tys =>
+      match list_nth_z float_param_regs fr with
+      | None =>
+          let ty := if Archi.single_passed_as_single then Tsingle else Tany64 in
+          let ofs := align ofs (typesize ty) in
+          One (S Outgoing ofs ty) :: loc_arguments_rec tys ir fr (ofs + (typesize ty))
+      | Some freg =>
+          One (R freg) :: loc_arguments_rec tys ir (fr + 1) ofs
+      end
+  | (Tfloat | Tany64) as ty :: tys =>
       match list_nth_z float_param_regs fr with
       | None =>
           let ofs := align ofs 2 in
@@ -236,33 +245,6 @@ Fixpoint loc_arguments_rec
 Definition loc_arguments (s: signature) : list (rpair loc) :=
   loc_arguments_rec s.(sig_args) 0 0 0.
 
-(** [size_arguments s] returns the number of [Outgoing] slots used
-  to call a function with signature [s]. *)
-
-Fixpoint size_arguments_rec (tyl: list typ) (ir fr ofs: Z) {struct tyl} : Z :=
-  match tyl with
-  | nil => ofs
-  | (Tint | Tany32) :: tys =>
-      match list_nth_z int_param_regs ir with
-      | None => size_arguments_rec tys ir fr (ofs + 1)
-      | Some ireg => size_arguments_rec tys (ir + 1) fr ofs
-      end
-  | (Tfloat | Tsingle | Tany64) :: tys =>
-      match list_nth_z float_param_regs fr with
-      | None => size_arguments_rec tys ir fr (align ofs 2 + 2)
-      | Some freg => size_arguments_rec tys ir (fr + 1) ofs
-      end
-  | Tlong :: tys =>
-      let ir := align ir 2 in
-      match list_nth_z int_param_regs ir, list_nth_z int_param_regs (ir + 1) with
-      | Some r1, Some r2 => size_arguments_rec tys (ir + 2) fr ofs
-      | _, _ => size_arguments_rec tys ir fr (align ofs 2 + 2)
-      end
-  end.
-
-Definition size_arguments (s: signature) : Z :=
-  size_arguments_rec s.(sig_args) 0 0 0.
-
 (** Argument locations are either caller-save registers or [Outgoing]
   stack slots at nonnegative offsets. *)
 
@@ -322,12 +304,14 @@ Opaque list_nth_z.
   apply align_divides; omega. apply Z.divide_1_l. apply Z.divide_1_l.
   eapply Y; eauto. omega.
 - (* single *)
+  assert (ofs <= align ofs 1) by (apply align_le; omega).
   assert (ofs <= align ofs 2) by (apply align_le; omega).
   destruct (list_nth_z float_param_regs fr) as [r|] eqn:E; destruct H.
   subst. right. eapply list_nth_z_in; eauto.
   eapply IHtyl; eauto.
-  subst. split. omega. apply Z.divide_1_l.
-  eapply Y; eauto. omega.
+  subst. split. destruct Archi.single_passed_as_single; simpl; omega.
+  destruct Archi.single_passed_as_single; simpl; apply Z.divide_1_l.
+  eapply Y; eauto. destruct Archi.single_passed_as_single; simpl; omega.
 - (* any32 *)
   destruct (list_nth_z int_param_regs ir) as [r|] eqn:E; destruct H.
   subst. left. eapply list_nth_z_in; eauto.
@@ -359,105 +343,6 @@ Qed.
 
 Hint Resolve loc_arguments_acceptable: locs.
 
-(** The offsets of [Outgoing] arguments are below [size_arguments s]. *)
-
-Remark size_arguments_rec_above:
-  forall tyl ir fr ofs0,
-  ofs0 <= size_arguments_rec tyl ir fr ofs0.
-Proof.
-  induction tyl; simpl; intros.
-  omega.
-  destruct a.
-  destruct (list_nth_z int_param_regs ir); eauto. apply Z.le_trans with (ofs0 + 1); auto; omega.
-  destruct (list_nth_z float_param_regs fr); eauto.
-  apply Z.le_trans with (align ofs0 2). apply align_le; omega.
-  apply Z.le_trans with (align ofs0 2 + 2); auto; omega.
-  set (ir' := align ir 2).
-  destruct (list_nth_z int_param_regs ir'); eauto.
-  destruct (list_nth_z int_param_regs (ir' + 1)); eauto.
-  apply Z.le_trans with (align ofs0 2). apply align_le; omega.
-  apply Z.le_trans with (align ofs0 2 + 2); auto; omega.
-  apply Z.le_trans with (align ofs0 2). apply align_le; omega.
-  apply Z.le_trans with (align ofs0 2 + 2); auto; omega.
-  destruct (list_nth_z float_param_regs fr); eauto.
-  apply Z.le_trans with (align ofs0 2). apply align_le; omega.
-  apply Z.le_trans with (align ofs0 2 + 2); auto; omega.
-  destruct (list_nth_z int_param_regs ir); eauto. apply Z.le_trans with (ofs0 + 1); auto; omega.
-  destruct (list_nth_z float_param_regs fr); eauto.
-  apply Z.le_trans with (align ofs0 2). apply align_le; omega.
-  apply Z.le_trans with (align ofs0 2 + 2); auto; omega.
-Qed.
-
-Lemma size_arguments_above:
-  forall s, size_arguments s >= 0.
-Proof.
-  intros; unfold size_arguments. apply Z.le_ge.
-  apply size_arguments_rec_above.
-Qed.
-
-Lemma loc_arguments_bounded:
-  forall (s: signature) (ofs: Z) (ty: typ),
-  In (S Outgoing ofs ty) (regs_of_rpairs (loc_arguments s)) ->
-  ofs + typesize ty <= size_arguments s.
-Proof.
-  intros.
-  assert (forall tyl ir fr ofs0,
-    In (S Outgoing ofs ty) (regs_of_rpairs (loc_arguments_rec tyl ir fr ofs0)) ->
-    ofs + typesize ty <= size_arguments_rec tyl ir fr ofs0).
-{
-  induction tyl; simpl; intros.
-  elim H0.
-  destruct a.
-- (* int *)
-  destruct (list_nth_z int_param_regs ir); destruct H0.
-  congruence.
-  eauto.
-  inv H0. apply size_arguments_rec_above.
-  eauto.
-- (* float *)
-  destruct (list_nth_z float_param_regs fr); destruct H0.
-  congruence.
-  eauto.
-  inv H0. apply size_arguments_rec_above. eauto.
-- (* long *)
-  set (ir' := align ir 2) in *.
-  assert (DFL:
-    In (S Outgoing ofs ty) (regs_of_rpairs
-                             ((if Archi.ptr64
-                               then One (S Outgoing (align ofs0 2) Tlong)
-                               else Twolong (S Outgoing (align ofs0 2) Tint)
-                                            (S Outgoing (align ofs0 2 + 1) Tint))
-                          :: loc_arguments_rec tyl ir' fr (align ofs0 2 + 2))) ->
-    ofs + typesize ty <= size_arguments_rec tyl ir' fr (align ofs0 2 + 2)).
-  { destruct Archi.ptr64; intros IN.
-  - destruct IN. inv H1. apply size_arguments_rec_above. auto.
-  - destruct IN. inv H1. transitivity (align ofs0 2 + 2). simpl; omega. apply size_arguments_rec_above.
-    destruct H1. inv H1. transitivity (align ofs0 2 + 2). simpl; omega. apply size_arguments_rec_above.
-    auto. }
-  destruct (list_nth_z int_param_regs ir'); auto.
-  destruct (list_nth_z int_param_regs (ir' + 1)); auto.
-  destruct H0. congruence. destruct H0. congruence. eauto.
-- (* single *)
-  destruct (list_nth_z float_param_regs fr); destruct H0.
-  congruence.
-  eauto.
-  inv H0. transitivity (align ofs0 2 + 2). simpl; omega. apply size_arguments_rec_above.
-  eauto.
-- (* any32 *)
-  destruct (list_nth_z int_param_regs ir); destruct H0.
-  congruence.
-  eauto.
-  inv H0. apply size_arguments_rec_above.
-  eauto.
-- (* any64 *)
-  destruct (list_nth_z float_param_regs fr); destruct H0.
-  congruence.
-  eauto.
-  inv H0. apply size_arguments_rec_above. eauto.
-  }
-  eauto.
-Qed.
-
 Lemma loc_arguments_main:
   loc_arguments signature_main = nil.
 Proof.
diff --git a/powerpc/DuplicateOpcodeHeuristic.ml b/powerpc/DuplicateOpcodeHeuristic.ml
index 85505245..33be79e8 100644
--- a/powerpc/DuplicateOpcodeHeuristic.ml
+++ b/powerpc/DuplicateOpcodeHeuristic.ml
@@ -1,3 +1,27 @@
-exception HeuristicSucceeded
-        
-let opcode_heuristic code cond ifso ifnot preferred = ()
+(* open Camlcoq *)
+open Op
+open Integers
+
+let opcode_heuristic code cond ifso ifnot is_loop_header =
+  match cond with
+  | Ccompimm (c, n) | Ccompuimm (c, n) -> if n == Integers.Int.zero then (match c with
+      | Clt | Cle -> Some false
+      | Cgt | Cge -> Some true
+      | _ -> None
+      ) else None
+  | Ccomplimm (c, n) | Ccompluimm (c, n) -> if n == Integers.Int64.zero then (match c with
+      | Clt | Cle -> Some false
+      | Cgt | Cge -> Some true
+      | _ -> None
+      ) else None
+  | Ccompf c -> (match c with
+      | Ceq -> Some false
+      | Cne -> Some true
+      | _ -> None
+      )
+  | Cnotcompf c -> (match c with
+      | Ceq -> Some true
+      | Cne -> Some false
+      | _ -> None
+      )
+  | _ -> None
diff --git a/powerpc/extractionMachdep.v b/powerpc/extractionMachdep.v
index 7482435f..a3e945bf 100644
--- a/powerpc/extractionMachdep.v
+++ b/powerpc/extractionMachdep.v
@@ -34,3 +34,6 @@ Extract Constant Archi.ppc64 =>
    | ""e5500"" -> true
    | _ -> false
    end".
+
+(* Choice of passing of single *)
+Extract Constant Archi.single_passed_as_single => "Configuration.gnu_toolchain".