Merge remote-tracking branch 'origin/mppa-refactor-reviewed' into mppa-refactor

Conflicts:
	mppa_k1c/Asmblock.v
	mppa_k1c/Asmblockdeps.v
	mppa_k1c/PostpassSchedulingproof.v
	mppa_k1c/lib/Asmblockgenproof0.v

1 files changed, 222 insertions, 128 deletions

diff --git a/mppa_k1c/Asmblock.v b/mppa_k1c/Asmblock.v
index c7528272..ed145f21 100644
--- a/mppa_k1c/Asmblock.v
+++ b/mppa_k1c/Asmblock.v
@@ -33,6 +33,227 @@ Require Import Conventions.
 Require Import Errors.
 Require Export Asmvliw.
 
+
+(** * Auxiliary utilies on basic blocks *)
+
+(** ** A unified view of Kalray instructions *)
+
+Inductive instruction : Type :=
+  | PBasic    (i: basic)
+  | PControl  (i: control)
+.
+
+Coercion PBasic:    basic >-> instruction.
+Coercion PControl:  control >-> instruction.
+
+Definition code := list instruction.
+Definition bcode := list basic.
+
+Fixpoint basics_to_code (l: list basic) :=
+  match l with
+  | nil => nil
+  | bi::l => (PBasic bi)::(basics_to_code l)
+  end.
+
+Fixpoint code_to_basics (c: code) :=
+  match c with
+  | (PBasic i)::c =>
+    match code_to_basics c with
+    | None => None
+    | Some l => Some (i::l)
+    end
+  | _::c => None
+  | nil => Some nil
+  end.
+
+Lemma code_to_basics_id: forall c, code_to_basics (basics_to_code c) = Some c.
+Proof.
+  intros. induction c as [|i c]; simpl; auto.
+  rewrite IHc. auto.
+Qed.
+
+Lemma code_to_basics_dist:
+  forall c c' l l',
+  code_to_basics c = Some l ->
+  code_to_basics c' = Some l' ->
+  code_to_basics (c ++ c') = Some (l ++ l').
+Proof.
+  induction c as [|i c]; simpl; auto.
+  - intros. inv H. simpl. auto.
+  - intros. destruct i; try discriminate. destruct (code_to_basics c) eqn:CTB; try discriminate.
+    inv H. erewrite IHc; eauto. auto.
+Qed.
+
+(** 
+  Asmblockgen will have to translate a Mach control into a list of instructions of the form
+   i1 :: i2 :: i3 :: ctl :: nil ; where i1..i3 are basic instructions, ctl is a control instruction
+  These functions provide way to extract the basic / control instructions
+*)
+
+Fixpoint extract_basic (c: code) :=
+  match c with
+  | nil => nil
+  | PBasic i :: c => i :: (extract_basic c)
+  | PControl i :: c => nil
+  end.
+
+Fixpoint extract_ctl (c: code) :=
+  match c with
+  | nil => None
+  | PBasic i :: c => extract_ctl c
+  | PControl i :: nil => Some i
+  | PControl i :: _ => None (* if the first found control instruction isn't the last *)
+  end.
+
+(** ** Wellformness of basic blocks *)
+
+Ltac exploreInst :=
+  repeat match goal with
+  | [ H : match ?var with | _ => _ end = _ |- _ ] => destruct var
+  | [ H : OK _ = OK _ |- _ ] => monadInv H
+  | [ |- context[if ?b then _ else _] ] => destruct b
+  | [ |- context[match ?m with | _ => _ end] ] => destruct m
+  | [ |- context[match ?m as _ return _ with | _ => _ end]] => destruct m
+  | [ H : bind _ _ = OK _ |- _ ] => monadInv H
+  | [ H : Error _ = OK _ |- _ ] => inversion H
+  end.
+
+Definition non_empty_bblock (body: list basic) (exit: option control): Prop
+ := body <> nil \/ exit <> None.
+
+Lemma non_empty_bblock_refl:
+  forall body exit,
+  non_empty_bblock body exit <->
+  Is_true (non_empty_bblockb body exit).
+Proof.
+  intros. split.
+  - destruct body; destruct exit.
+    all: simpl; auto. intros. inversion H; contradiction.
+  - destruct body; destruct exit.
+    all: simpl; auto.
+    all: intros; try (right; discriminate); try (left; discriminate).
+    contradiction.
+Qed.
+
+Definition builtin_alone (body: list basic) (exit: option control) := forall ef args res,
+  exit = Some (PExpand (Pbuiltin ef args res)) -> body = nil.
+
+
+Lemma builtin_alone_refl:
+  forall body exit,
+  builtin_alone body exit <-> Is_true (builtin_aloneb body exit).
+Proof.
+  intros. split.
+  - destruct body; destruct exit.
+    all: simpl; auto.
+    all: exploreInst; simpl; auto.
+    unfold builtin_alone. intros. assert (Some (Pbuiltin e l b0) = Some (Pbuiltin e l b0)); auto.
+    assert (b :: body = nil). eapply H; eauto. discriminate.
+  - destruct body; destruct exit.
+    all: simpl; auto; try constructor.
+    + exploreInst; try discriminate.
+        simpl. contradiction.
+    + intros. discriminate.
+Qed.
+
+Definition wf_bblock (body: list basic) (exit: option control) :=
+  non_empty_bblock body exit /\ builtin_alone body exit.
+
+Lemma wf_bblock_refl:
+  forall body exit,
+  wf_bblock body exit <-> Is_true (wf_bblockb body exit).
+Proof.
+  intros. split.
+  - intros. inv H. apply non_empty_bblock_refl in H0. apply builtin_alone_refl in H1.
+    apply andb_prop_intro. auto.
+  - intros. apply andb_prop_elim in H. inv H.
+    apply non_empty_bblock_refl in H0. apply builtin_alone_refl in H1.
+    unfold wf_bblock. split; auto.
+Qed.
+
+Ltac bblock_auto_correct := (apply non_empty_bblock_refl; try discriminate; try (left; discriminate); try (right; discriminate)).
+(* Local Obligation Tactic := bblock_auto_correct. *)
+
+Lemma Istrue_proof_irrelevant (b: bool): forall (p1 p2:Is_true b), p1=p2.
+Proof.
+  destruct b; simpl; auto.
+  - destruct p1, p2; auto.
+  - destruct p1.
+Qed.
+
+Lemma bblock_equality bb1 bb2: header bb1=header bb2 -> body bb1 = body bb2 -> exit bb1 = exit bb2 -> bb1 = bb2.
+Proof.
+  destruct bb1 as [h1 b1 e1 c1], bb2 as [h2 b2 e2 c2]; simpl.
+  intros; subst.
+  rewrite (Istrue_proof_irrelevant _ c1 c2).
+  auto.
+Qed.
+
+Program Definition bblock_single_inst (i: instruction) :=
+  match i with
+  | PBasic b => {| header:=nil; body:=(b::nil); exit:=None |}
+  | PControl ctl => {| header:=nil; body:=nil; exit:=(Some ctl) |}
+  end.
+Next Obligation.
+  apply wf_bblock_refl. constructor.
+    right. discriminate.
+    constructor.
+Qed.
+
+Lemma length_nonil {A: Type} : forall l:(list A), l <> nil -> (length l > 0)%nat.
+Proof.
+  intros. destruct l; try (contradict H; auto; fail).
+  simpl. omega.
+Qed.
+
+Lemma to_nat_pos : forall z:Z, (Z.to_nat z > 0)%nat -> z > 0.
+Proof.
+  intros. destruct z; auto.
+  - contradict H. simpl. apply gt_irrefl.
+  - apply Zgt_pos_0.
+  - contradict H. simpl. apply gt_irrefl.
+Qed.
+
+Lemma size_positive (b:bblock): size b > 0.
+Proof.
+  unfold size. destruct b as [hd bdy ex cor]. simpl.
+  destruct ex; destruct bdy; try (apply to_nat_pos; rewrite Nat2Z.id; simpl; omega).
+  inversion cor; contradict H; simpl; auto.
+Qed.
+
+
+Program Definition no_header (bb : bblock) := {| header := nil; body := body bb; exit := exit bb |}.
+Next Obligation.
+  destruct bb; simpl. assumption.
+Defined.
+
+Lemma no_header_size:
+  forall bb, size (no_header bb) = size bb.
+Proof.
+  intros. destruct bb as [hd bdy ex COR]. unfold no_header. simpl. reflexivity.
+Qed.
+
+Program Definition stick_header (h : list label) (bb : bblock) := {| header := h; body := body bb; exit := exit bb |}.
+Next Obligation.
+  destruct bb; simpl. assumption.
+Defined.
+
+Lemma stick_header_size:
+  forall h bb, size (stick_header h bb) = size bb.
+Proof.
+  intros. destruct bb. unfold stick_header. simpl. reflexivity.
+Qed.
+
+Lemma stick_header_no_header:
+  forall bb, stick_header (header bb) (no_header bb) = bb.
+Proof.
+  intros. destruct bb as [hd bdy ex COR]. simpl. unfold no_header; unfold stick_header; simpl. reflexivity.
+Qed.
+
+
+
+
+(** * Sequential Semantics of basic blocks *)
 Section RELSEM.
 
 (** Execution of arith instructions *)
@@ -102,10 +323,7 @@ Definition exec_bblock (f: function) (b: bblock) (rs0: regset) (m: mem) : outcom
   end.
 
 
-(** TODO
- * For now, we consider a builtin is alone in a basic block.
- * Perhaps there is a way to avoid that ?
- *)
+(** Execution of the instruction at [rs PC]. *)
 
 Inductive step: state -> trace -> state -> Prop :=
   | exec_step_internal:
@@ -147,68 +365,6 @@ End RELSEM.
 Definition semantics (p: program) :=
   Semantics step (initial_state p) final_state (Genv.globalenv p).
 
-(* Useless
-
-Remark extcall_arguments_determ:
-  forall rs m sg args1 args2,
-  extcall_arguments rs m sg args1 -> extcall_arguments rs m sg args2 -> args1 = args2.
-Proof.
-  intros until m.
-  assert (A: forall l v1 v2,
-             extcall_arg rs m l v1 -> extcall_arg rs m l v2 -> v1 = v2).
-  { intros. inv H; inv H0; congruence. }
-  assert (B: forall p v1 v2,
-             extcall_arg_pair rs m p v1 -> extcall_arg_pair rs m p v2 -> v1 = v2).
-  { intros. inv H; inv H0. 
-    eapply A; eauto.
-    f_equal; eapply A; eauto. }
-  assert (C: forall ll vl1, list_forall2 (extcall_arg_pair rs m) ll vl1 ->
-             forall vl2, list_forall2 (extcall_arg_pair rs m) ll vl2 -> vl1 = vl2).
-  {
-    induction 1; intros vl2 EA; inv EA.
-    auto.
-    f_equal; eauto. }
-  intros. eapply C; eauto.
-Qed.
-
-Lemma semantics_determinate: forall p, determinate (semantics p).
-Proof.
-Ltac Equalities :=
-  match goal with
-  | [ H1: ?a = ?b, H2: ?a = ?c |- _ ] =>
-      rewrite H1 in H2; inv H2; Equalities
-  | _ => idtac
-  end.
-  intros; constructor; simpl; intros.
-- (* determ *)
-  inv H; inv H0; Equalities.
-  + split. constructor. auto.
-  + unfold exec_bblock in H4. destruct (exec_body _ _ _ _); try discriminate.
-    rewrite H9 in H4. discriminate.
-  + unfold exec_bblock in H13. destruct (exec_body _ _ _ _); try discriminate.
-    rewrite H4 in H13. discriminate.
-  + assert (vargs0 = vargs) by (eapply eval_builtin_args_determ; eauto). subst vargs0.
-    exploit external_call_determ. eexact H6. eexact H13. intros [A B].
-    split. auto. intros. destruct B; auto. subst. auto.
-  + assert (args0 = args) by (eapply extcall_arguments_determ; eauto). subst args0.
-    exploit external_call_determ. eexact H3. eexact H8. intros [A B].
-    split. auto. intros. destruct B; auto. subst. auto.
-- (* trace length *)
-  red; intros. inv H; simpl.
-  omega.
-  eapply external_call_trace_length; eauto.
-  eapply external_call_trace_length; eauto.
-- (* initial states *)
-  inv H; inv H0. f_equal. congruence.
-- (* final no step *)
-  assert (NOTNULL: forall b ofs, Vnullptr <> Vptr b ofs).
-  { intros; unfold Vnullptr; destruct Archi.ptr64; congruence. }
-  inv H. unfold Vzero in H0. red; intros; red; intros.
-  inv H; rewrite H0 in *; eelim NOTNULL; eauto.
-- (* final states *)
-  inv H; inv H0. congruence.
-Qed.
-*)
 
 Definition data_preg (r: preg) : bool :=
   match r with
@@ -219,65 +375,3 @@ Definition data_preg (r: preg) : bool :=
   | PC     => false
   end.
 
-(** Determinacy of the [Asm] semantics. *)
-
-(* Useless.
-
-Remark extcall_arguments_determ:
-  forall rs m sg args1 args2,
-  extcall_arguments rs m sg args1 -> extcall_arguments rs m sg args2 -> args1 = args2.
-Proof.
-  intros until m.
-  assert (A: forall l v1 v2,
-             extcall_arg rs m l v1 -> extcall_arg rs m l v2 -> v1 = v2).
-  { intros. inv H; inv H0; congruence. }
-  assert (B: forall p v1 v2,
-             extcall_arg_pair rs m p v1 -> extcall_arg_pair rs m p v2 -> v1 = v2).
-  { intros. inv H; inv H0. 
-    eapply A; eauto.
-    f_equal; eapply A; eauto. }
-  assert (C: forall ll vl1, list_forall2 (extcall_arg_pair rs m) ll vl1 ->
-             forall vl2, list_forall2 (extcall_arg_pair rs m) ll vl2 -> vl1 = vl2).
-  {
-    induction 1; intros vl2 EA; inv EA.
-    auto.
-    f_equal; eauto. }
-  intros. eapply C; eauto.
-Qed.
-
-Lemma semantics_determinate: forall p, determinate (semantics p).
-Proof.
-Ltac Equalities :=
-  match goal with
-  | [ H1: ?a = ?b, H2: ?a = ?c |- _ ] =>
-      rewrite H1 in H2; inv H2; Equalities
-  | _ => idtac
-  end.
-  intros; constructor; simpl; intros.
-- (* determ *)
-  inv H; inv H0; Equalities.
-  split. constructor. auto.
-  discriminate.
-  discriminate.
-  assert (vargs0 = vargs) by (eapply eval_builtin_args_determ; eauto). subst vargs0.
-  exploit external_call_determ. eexact H5. eexact H11. intros [A B].
-  split. auto. intros. destruct B; auto. subst. auto.
-  assert (args0 = args) by (eapply extcall_arguments_determ; eauto). subst args0.
-  exploit external_call_determ. eexact H3. eexact H8. intros [A B].
-  split. auto. intros. destruct B; auto. subst. auto.
-- (* trace length *)
-  red; intros. inv H; simpl.
-  omega.
-  eapply external_call_trace_length; eauto.
-  eapply external_call_trace_length; eauto.
-- (* initial states *)
-  inv H; inv H0. f_equal. congruence.
-- (* final no step *)
-  assert (NOTNULL: forall b ofs, Vnullptr <> Vptr b ofs).
-  { intros; unfold Vnullptr; destruct Archi.ptr64; congruence. }
-  inv H. unfold Vzero in H0. red; intros; red; intros.
-  inv H; rewrite H0 in *; eelim NOTNULL; eauto.
-- (* final states *)
-  inv H; inv H0. congruence.
-Qed.
-*)