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

5 files changed, 305 insertions, 149 deletions

diff --git a/x86/Asmexpand.ml b/x86/Asmexpand.ml
index c82d406e..b8353046 100644
--- a/x86/Asmexpand.ml
+++ b/x86/Asmexpand.ml
@@ -251,7 +251,7 @@ let expand_builtin_va_start_32 r =
     invalid_arg "Fatal error: va_start used in non-vararg function";
   let ofs =
     Int32.(add (add !PrintAsmaux.current_function_stacksize 4l)
-               (mul 4l (Z.to_int32 (Conventions1.size_arguments
+               (mul 4l (Z.to_int32 (Conventions.size_arguments
                                       (get_current_function_sig ()))))) in
   emit (Pleal (RAX, linear_addr RSP (Z.of_uint32 ofs)));
   emit (Pmovl_mr (linear_addr r _0z, RAX))
diff --git a/x86/CSE2deps.v b/x86/CSE2deps.v
new file mode 100644
index 00000000..f4d9e254
--- /dev/null
+++ b/x86/CSE2deps.v
@@ -0,0 +1,24 @@
+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 ofs' chunk' ofs chunk)
+    else true
+  | (Aglobal symb ofs), (Aglobal symb' ofs'), nil, nil =>
+    if peq symb symb'
+    then negb (can_swap_accesses_ofs (Ptrofs.unsigned ofs') chunk' (Ptrofs.unsigned ofs) chunk)
+    else false
+  | _, _, _, _ => true
+  end.
diff --git a/x86/CSE2depsproof.v b/x86/CSE2depsproof.v
new file mode 100644
index 00000000..1e913254
--- /dev/null
+++ b/x86/CSE2depsproof.v
@@ -0,0 +1,253 @@
+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.
+
+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 : Z.
+  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 <= ofsw <= Ptrofs.modulus - largest_size_chunk,
+    forall RANGER : 0 <= ofsr <= Ptrofs.modulus - largest_size_chunk,
+    forall SWAPPABLE :    ofsw + size_chunk chunkw <= ofsr
+                       \/ ofsr + size_chunk chunkr <= 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.
+    try change (Ptrofs.modulus - largest_size_chunk) with 4294967288 in *.
+    try change (Ptrofs.modulus - largest_size_chunk) with 18446744073709551608 in *.
+    destruct addrr ; simpl in * ; trivial.
+    unfold eval_addressing, eval_addressing32, eval_addressing64 in *.
+    destruct Archi.ptr64 eqn:PTR64; destruct base; simpl in *; try discriminate.
+    rewrite PTR64 in *.
+    
+    inv ADDRR.
+    inv ADDRW.
+    eapply Mem.load_store_other with (chunk := chunkw) (v := valw) (b := b).
+    exact STORE.
+    right.
+ 
+    all: try (destruct (Ptrofs.unsigned_add_either i0
+                (Ptrofs.of_int (Int.repr ofsr))) as [OFSR | OFSR];
+              rewrite OFSR).
+    all: try (destruct (Ptrofs.unsigned_add_either i0
+                (Ptrofs.of_int64 (Int64.repr ofsr))) as [OFSR | OFSR];
+              rewrite OFSR).
+    all: try (destruct (Ptrofs.unsigned_add_either i0
+                (Ptrofs.of_int (Int.repr ofsw))) as [OFSW | OFSW];
+              rewrite OFSW).
+    all: try (destruct (Ptrofs.unsigned_add_either i0
+                (Ptrofs.of_int64 (Int64.repr ofsw))) as [OFSW | OFSW];
+              rewrite OFSW).
+    
+    all: unfold Ptrofs.of_int64.
+    all: unfold Ptrofs.of_int.
+   
+
+    all: repeat rewrite Int.unsigned_repr by (change Int.max_unsigned with 4294967295; lia).
+    all: repeat rewrite Ptrofs.unsigned_repr by (change Ptrofs.max_unsigned with 4294967295; lia).
+    all: repeat rewrite Int64.unsigned_repr by (change Int64.max_unsigned with 18446744073709551615; lia).
+    all: repeat rewrite Ptrofs.unsigned_repr by (change Ptrofs.max_unsigned with 18446744073709551615; lia).
+
+    all: try change Ptrofs.modulus with 4294967296.
+    all: try change Ptrofs.modulus with 18446744073709551616.
+   
+    all: intuition lia.
+  Qed.
+  
+  Theorem load_store_away :
+    can_swap_accesses_ofs ofsr chunkr 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.
+
+  Section DIFFERENT_GLOBALS.
+    Variable ofsw ofsr : ptrofs.
+    Hypothesis symw symr : ident.
+    Hypothesis ADDRW : eval_addressing genv sp
+                                       (Aglobal symw ofsw) nil = Some addrw. 
+    Hypothesis ADDRR : eval_addressing genv sp
+                                       (Aglobal symr ofsr) nil = Some addrr.
+
+    Lemma ptr64_cases:
+      forall {T : Type},
+      forall b : bool,
+      forall x y : T,
+        (if b then (if b then x else y) else (if b then y else x)) = x.
+    Proof.
+      destruct b; reflexivity.
+    Qed.
+
+    (* not needed
+    Lemma bool_cases_same:
+      forall {T : Type},
+      forall b : bool,
+      forall x : T,
+        (if b then x else x) = x.
+    Proof.
+      destruct b; reflexivity.
+    Qed.
+     *)
+
+    Lemma load_store_diff_globals :
+      symw <> symr ->
+      Mem.loadv chunkr m2 addrr = Mem.loadv chunkr m addrr.
+    Proof.
+      intros.
+      unfold eval_addressing in *.
+      simpl in *.
+      rewrite ptr64_cases in ADDRR.
+      rewrite ptr64_cases in ADDRW.
+      unfold Genv.symbol_address in *.
+      unfold Genv.find_symbol in *.
+      destruct ((Genv.genv_symb genv) ! symw) as [bw |] eqn:SYMW; inv ADDRW.
+      2: simpl in STORE; discriminate.
+      destruct ((Genv.genv_symb genv) ! symr) as [br |] eqn:SYMR; inv ADDRR.
+      2: reflexivity.
+      assert (br <> bw).
+      {
+        intro EQ.
+        subst br.
+        assert (symr = symw).
+        {
+          eapply Genv.genv_vars_inj; eauto.
+        }
+        congruence.
+      }
+      eapply Mem.load_store_other with (chunk := chunkw) (v := valw) (b := bw).
+      - exact STORE.
+      - left. assumption.
+    Qed.
+  End DIFFERENT_GLOBALS.
+
+  Section SAME_GLOBALS.
+    Variable ofsw ofsr : ptrofs.
+    Hypothesis sym : ident.
+    Hypothesis ADDRW : eval_addressing genv sp
+                                       (Aglobal sym ofsw) nil = Some addrw. 
+    Hypothesis ADDRR : eval_addressing genv sp
+                                       (Aglobal sym ofsr) nil = Some addrr.
+    
+  Lemma load_store_glob_away1 :
+    forall RANGEW : 0 <= (Ptrofs.unsigned ofsw) <= Ptrofs.modulus - largest_size_chunk,
+    forall RANGER : 0 <= (Ptrofs.unsigned ofsr) <= Ptrofs.modulus - largest_size_chunk,
+    forall SWAPPABLE : (Ptrofs.unsigned ofsw) + size_chunk chunkw <= (Ptrofs.unsigned ofsr)
+                    \/ (Ptrofs.unsigned ofsr) + size_chunk chunkr <= (Ptrofs.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 size_chunkr_bounded, size_chunkw_bounded.
+    try change (Ptrofs.modulus - largest_size_chunk) with 4294967288 in *.
+    try change (Ptrofs.modulus - largest_size_chunk) with 18446744073709551608 in *.
+    unfold eval_addressing, eval_addressing32, eval_addressing64 in *.
+
+    rewrite ptr64_cases in ADDRR.
+    rewrite ptr64_cases in ADDRW.
+    unfold Genv.symbol_address in *.
+    inv ADDRR.
+    inv ADDRW.
+    destruct (Genv.find_symbol genv sym).
+    2: discriminate.
+    
+    eapply Mem.load_store_other with (chunk := chunkw) (v := valw) (b := b).
+    exact STORE.
+    right.
+    tauto.
+  Qed.
+
+  Lemma load_store_glob_away :
+    (can_swap_accesses_ofs (Ptrofs.unsigned ofsr) chunkr (Ptrofs.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_glob_away1.
+    all: tauto.
+  Qed.
+  End SAME_GLOBALS.
+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 z0 chunk' z chunk) eqn:SWAP.
+  2: discriminate.
+  simpl in *.
+  eapply load_store_away; eassumption.
+  }
+  { (* Aglobal / Aglobal *)
+    destruct args. 2: discriminate.
+    destruct args'. 2: discriminate.
+    simpl in *.
+    destruct (peq i i1).
+    {
+      subst i1.
+      rewrite negb_false_iff in OVERLAP.
+      eapply load_store_glob_away; eassumption.
+    }
+    eapply load_store_diff_globals; eassumption.
+  }
+Qed.
+
+End SOUNDNESS.
diff --git a/x86/Conventions1.v b/x86/Conventions1.v
index ab4c4b13..d9f5b8fa 100644
--- a/x86/Conventions1.v
+++ b/x86/Conventions1.v
@@ -221,36 +221,6 @@ Definition loc_arguments (s: signature) : list (rpair loc) :=
   then loc_arguments_64 s.(sig_args) 0 0 0
   else loc_arguments_32 s.(sig_args) 0.
 
-(** [size_arguments s] returns the number of [Outgoing] slots used
-  to call a function with signature [s]. *)
-
-Fixpoint size_arguments_32
-    (tyl: list typ) (ofs: Z) {struct tyl} : Z :=
-  match tyl with
-  | nil => ofs
-  | ty :: tys => size_arguments_32 tys (ofs + typesize ty)
-  end.
-
-Fixpoint size_arguments_64 (tyl: list typ) (ir fr ofs: Z) {struct tyl} : Z :=
-  match tyl with
-  | nil => ofs
-  | (Tint | Tlong | Tany32 | Tany64) :: tys =>
-      match list_nth_z int_param_regs ir with
-      | None => size_arguments_64 tys ir fr (ofs + 2)
-      | Some ireg => size_arguments_64 tys (ir + 1) fr ofs
-      end
-  | (Tfloat | Tsingle) :: tys =>
-      match list_nth_z float_param_regs fr with
-      | None => size_arguments_64 tys ir fr (ofs + 2)
-      | Some freg => size_arguments_64 tys ir (fr + 1) ofs
-      end
-  end.
-
-Definition size_arguments (s: signature) : Z :=
-  if Archi.ptr64
-  then size_arguments_64 s.(sig_args) 0 0 0
-  else size_arguments_32 s.(sig_args) 0.
-
 (** Argument locations are either caller-save registers or [Outgoing]
   stack slots at nonnegative offsets. *)
 
@@ -352,121 +322,6 @@ Qed.
 
 Hint Resolve loc_arguments_acceptable: locs.
 
-(** The offsets of [Outgoing] arguments are below [size_arguments s]. *)
-
-Remark size_arguments_32_above:
-  forall tyl ofs0, ofs0 <= size_arguments_32 tyl ofs0.
-Proof.
-  induction tyl; simpl; intros.
-  omega.
-  apply Z.le_trans with (ofs0 + typesize a); auto.
-  generalize (typesize_pos a); omega.
-Qed.
-
-Remark size_arguments_64_above:
-  forall tyl ir fr ofs0,
-  ofs0 <= size_arguments_64 tyl ir fr ofs0.
-Proof.
-  induction tyl; simpl; intros.
-  omega.
-  assert (A: ofs0 <=
-    match list_nth_z int_param_regs ir with
-    | Some _ => size_arguments_64 tyl (ir + 1) fr ofs0
-    | None => size_arguments_64 tyl ir fr (ofs0 + 2)
-    end).
-  { destruct (list_nth_z int_param_regs ir); eauto.
-    apply Z.le_trans with (ofs0 + 2); auto. omega. }
-  assert (B: ofs0 <=
-    match list_nth_z float_param_regs fr with
-    | Some _ => size_arguments_64 tyl ir (fr + 1) ofs0
-    | None => size_arguments_64 tyl ir fr (ofs0 + 2)
-    end).
-  { destruct (list_nth_z float_param_regs fr); eauto.
-    apply Z.le_trans with (ofs0 + 2); auto. omega. }
-  destruct a; auto.
-Qed.
-
-Lemma size_arguments_above:
-  forall s, size_arguments s >= 0.
-Proof.
-  intros; unfold size_arguments. apply Z.le_ge.
-  destruct Archi.ptr64; [apply size_arguments_64_above|apply size_arguments_32_above].
-Qed.
-
-Lemma loc_arguments_32_bounded:
-  forall ofs ty tyl ofs0,
-  In (S Outgoing ofs ty) (regs_of_rpairs (loc_arguments_32 tyl ofs0)) ->
-  ofs + typesize ty <= size_arguments_32 tyl ofs0.
-Proof.
-  induction tyl as [ | t l]; simpl; intros x IN.
-- contradiction.
-- rewrite in_app_iff in IN; destruct IN as [IN|IN].
-+ apply Z.le_trans with (x + typesize t); [|apply size_arguments_32_above].
-  Ltac decomp :=
-  match goal with
-  | [ H: _ \/ _ |- _ ] => destruct H; decomp
-  | [ H: S _ _ _ = S _ _ _ |- _ ] => inv H
-  | [ H: False |- _ ] => contradiction
-  end.
-  destruct t; simpl in IN; decomp; simpl; omega.
-+ apply IHl; auto.
-Qed.
-
-Lemma loc_arguments_64_bounded:
-  forall ofs ty tyl ir fr ofs0,
-  In (S Outgoing ofs ty) (regs_of_rpairs (loc_arguments_64 tyl ir fr ofs0)) ->
-  ofs + typesize ty <= size_arguments_64 tyl ir fr ofs0.
-Proof.
-  induction tyl; simpl; intros.
-  contradiction.
-  assert (T: forall ty0, typesize ty0 <= 2).
-  { destruct ty0; simpl; omega. }
-  assert (A: forall ty0,
-             In (S Outgoing ofs ty) (regs_of_rpairs
-              match list_nth_z int_param_regs ir with
-              | Some ireg =>
-                  One (R ireg) :: loc_arguments_64 tyl (ir + 1) fr ofs0
-              | None => One (S Outgoing ofs0 ty0) :: loc_arguments_64 tyl ir fr (ofs0 + 2)
-              end) ->
-             ofs + typesize ty <=
-             match list_nth_z int_param_regs ir with
-             | Some _ => size_arguments_64 tyl (ir + 1) fr ofs0
-             | None => size_arguments_64 tyl ir fr (ofs0 + 2)
-             end).
-  { intros. destruct (list_nth_z int_param_regs ir); simpl in H0; destruct H0.
-  - discriminate.
-  - eapply IHtyl; eauto.
-  - inv H0. apply Z.le_trans with (ofs + 2). specialize (T ty). omega. apply size_arguments_64_above.
-  - eapply IHtyl; eauto. }
-  assert (B: forall ty0,
-             In (S Outgoing ofs ty) (regs_of_rpairs
-              match list_nth_z float_param_regs fr with
-              | Some ireg =>
-                  One (R ireg) :: loc_arguments_64 tyl ir (fr + 1) ofs0
-              | None => One (S Outgoing ofs0 ty0) :: loc_arguments_64 tyl ir fr (ofs0 + 2)
-              end) ->
-             ofs + typesize ty <=
-             match list_nth_z float_param_regs fr with
-             | Some _ => size_arguments_64 tyl ir (fr + 1) ofs0
-             | None => size_arguments_64 tyl ir fr (ofs0 + 2)
-             end).
-  { intros. destruct (list_nth_z float_param_regs fr); simpl in H0; destruct H0.
-  - discriminate.
-  - eapply IHtyl; eauto.
-  - inv H0. apply Z.le_trans with (ofs + 2). specialize (T ty). omega. apply size_arguments_64_above.
-  - eapply IHtyl; eauto. }
-  destruct a; eauto.
-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.
-  unfold loc_arguments, size_arguments; intros.
-  destruct Archi.ptr64; eauto using loc_arguments_32_bounded, loc_arguments_64_bounded.
-Qed.
-
 Lemma loc_arguments_main:
   loc_arguments signature_main = nil.
 Proof.
diff --git a/x86/DuplicateOpcodeHeuristic.ml b/x86/DuplicateOpcodeHeuristic.ml
index 85505245..2ec314c1 100644
--- a/x86/DuplicateOpcodeHeuristic.ml
+++ b/x86/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 | Ccompfs c -> (match c with
+      | Ceq -> Some false
+      | Cne -> Some true
+      | _ -> None
+      )
+  | Cnotcompf c | Cnotcompfs c -> (match c with
+      | Ceq -> Some true
+      | Cne -> Some false
+      | _ -> None
+      )
+  | _ -> None