Adding a predicate that a builtin must be alone in its basicblock

3 files changed, 168 insertions, 88 deletions

diff --git a/mppa_k1c/Asmblock.v b/mppa_k1c/Asmblock.v
index 5d60af6b..14ceb082 100644
--- a/mppa_k1c/Asmblock.v
+++ b/mppa_k1c/Asmblock.v
@@ -30,6 +30,7 @@ Require Import Smallstep.
 Require Import Locations.
 Require Stacklayout.
 Require Import Conventions.
+Require Import Errors.
 
 (** * Abstract syntax *)
 
@@ -384,6 +385,17 @@ Coercion PCtlFlow:  cf_instruction >-> control.
 
 (** * Definition of a bblock *)
 
+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.
 
@@ -415,12 +427,54 @@ Proof.
     contradiction.
 Qed.
 
-(* Definition builtin_alone (body: list basic) (exit: option control) := forall ef args res,
+Definition builtin_alone (body: list basic) (exit: option control) := forall ef args res,
   exit = Some (PExpand (Pbuiltin ef args res)) -> body = nil.
- *)
 
-(* Definition wf_bblock (header: list label) (body: list basic) (exit: option control) :=
-  non_empty_bblock body exit (* /\ builtin_alone body exit *). *)
+Definition builtin_aloneb (body: list basic) (exit: option control) :=
+  match exit with
+  | Some (PExpand (Pbuiltin _ _ _)) =>
+    match body with
+    | nil => true
+    | _ => false
+    end
+  | _ => true
+  end.
+
+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.
+        simpl. contradiction.
+        discriminate.
+    + intros. discriminate.
+Qed.
+
+Definition wf_bblockb (body: list basic) (exit: option control) :=
+  (non_empty_bblockb body exit) && (builtin_aloneb body exit).
+
+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.
 
 (** A bblock is well-formed if he contains at least one instruction,
     and if there is a builtin then it must be alone in this bblock. *)
@@ -429,7 +483,7 @@ Record bblock := mk_bblock {
   header: list label;
   body: list basic;
   exit: option control;
-  correct: Is_true (non_empty_bblockb body exit)
+  correct: Is_true (wf_bblockb body exit)
 }.
 
 Ltac bblock_auto_correct := (apply non_empty_bblock_refl; try discriminate; try (left; discriminate); try (right; discriminate)).
@@ -582,8 +636,14 @@ Program Definition bblock_single_inst (i: instruction) :=
   | 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.
 
-Program Definition bblock_basic_ctl (c: list basic) (i: option control) :=
+(** This definition is not used anymore *)
+(* Program Definition bblock_basic_ctl (c: list basic) (i: option control) :=
   match i with
   | Some i => {| header:=nil; body:=c; exit:=Some i |}
   | None =>
@@ -596,7 +656,7 @@ Next Obligation.
   bblock_auto_correct.
 Qed. Next Obligation.
   bblock_auto_correct.
-Qed.
+Qed. *)
 
 
 (** * Operational semantics *)
@@ -1310,75 +1370,75 @@ Ltac Equalities :=
   inv H; inv H0. congruence.
 Qed.
 
-Definition data_preg (r: preg) : bool :=

-  match r with

-  | RA  => false

-  | IR GPRA => false

-  | IR RTMP => false

-  | IR _   => true

-  | FR _   => true

-  | PC     => false

-  end.

-

-(** Determinacy of the [Asm] semantics. *)

-

-(* TODO.

-

-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.

-*)

+Definition data_preg (r: preg) : bool :=
+  match r with
+  | RA  => false
+  | IR GPRA => false
+  | IR RTMP => false
+  | IR _   => true
+  | FR _   => true
+  | PC     => false
+  end.
+
+(** Determinacy of the [Asm] semantics. *)
+
+(* TODO.
+
+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.
+*)
diff --git a/mppa_k1c/Asmblockgen.v b/mppa_k1c/Asmblockgen.v
index 0d1dd49c..e32748f8 100644
--- a/mppa_k1c/Asmblockgen.v
+++ b/mppa_k1c/Asmblockgen.v
@@ -891,9 +891,13 @@ Program Definition gen_bblocks (hd: list label) (c: list basic) (ctl: list instr
   end
 .
 Next Obligation.
-  bblock_auto_correct. intros. constructor. apply not_eq_sym. auto.
+  apply wf_bblock_refl. constructor.
+    left. auto.
+    discriminate.
 Qed. Next Obligation.
-  bblock_auto_correct.
+  apply wf_bblock_refl. constructor.
+    right. discriminate.
+    discriminate.
 Qed.
 
 Definition transl_block (f: Machblock.function) (fb: Machblock.bblock) (ep: bool) : res (list bblock) :=
diff --git a/mppa_k1c/PostpassSchedulingproof.v b/mppa_k1c/PostpassSchedulingproof.v
index 73a44058..2b09bb01 100644
--- a/mppa_k1c/PostpassSchedulingproof.v
+++ b/mppa_k1c/PostpassSchedulingproof.v
@@ -41,22 +41,38 @@ Proof.
   - discriminate.

 Qed.

 

+Lemma app_nonil2 {A: Type} : forall (l': list A) l, l' <> nil -> l ++ l' <> nil.

+Proof.

+  induction l'; try contradiction.

+  intros. cutrewrite (l ++ a :: l' = (l ++ a :: nil) ++ l'). apply app_nonil.

+Admitted.

+

 Program Definition concat2 (bb bb': bblock) : res bblock :=

   match (exit bb) with

   | None => 

       match (header bb') with

-      | nil => OK {| header := header bb; body := body bb ++ body bb'; exit := exit bb' |}

+      | nil => 

+          match (exit bb') with 

+          | Some (PExpand (Pbuiltin _ _ _)) => Error (msg "PostpassSchedulingproof.concat2: builtin not alone")

+          | _ => OK {| header := header bb; body := body bb ++ body bb'; exit := exit bb' |}

+          end

       | _ => Error (msg "PostpassSchedulingproof.concat2")

       end

   | _ => Error (msg "PostpassSchedulingproof.concat2")

   end.

 Next Obligation.

-  apply non_empty_bblock_refl.

-  destruct bb as [hd bdy ex COR]; destruct bb' as [hd' bdy' ex' COR']. simpl in *.

-  apply non_empty_bblock_refl in COR. apply non_empty_bblock_refl in COR'.

-  inv COR.

-  - left. apply app_nonil. auto.

-  - contradiction.

+  apply wf_bblock_refl. constructor.

+  - destruct bb' as [hd' bdy' ex' WF']. destruct bb as [hd bdy ex WF]. simpl in *.

+    apply wf_bblock_refl in WF'. apply wf_bblock_refl in WF.

+    inversion_clear WF'. inversion_clear WF. clear H1 H3.

+    inversion H2; inversion H0.

+    + left. apply app_nonil. auto.

+    + right. auto.

+    + left. apply app_nonil2. auto.

+    + right. auto.

+  - unfold builtin_alone. intros. rewrite H0 in H.

+    assert (Some (PExpand (Pbuiltin ef args res)) <> Some (PExpand (Pbuiltin ef args res))).

+    apply (H ef args res). contradict H1. auto.

 Qed.

 

 Fixpoint concat_all (lbb: list bblock) : res bblock :=