relecture sylvain

avec TODOs pour refactoring #90

1 files changed, 244 insertions, 168 deletions

diff --git a/mppa_k1c/Asmblock.v b/mppa_k1c/Asmblock.v
index 3bcb321d..0f65b1d0 100644
--- a/mppa_k1c/Asmblock.v
+++ b/mppa_k1c/Asmblock.v
@@ -33,13 +33,234 @@ 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 *)
 
 Variable ge: genv.
 
-
+(* TODO: delete this or define it as [parexec_arith_instr ge ai rs rs] *)
 Definition exec_arith_instr (ai: ar_instruction) (rs: regset): regset :=
   match ai with
   | PArithR n d => rs#d <- (arith_eval_r ge n)
@@ -68,7 +289,7 @@ Definition exec_arith_instr (ai: ar_instruction) (rs: regset): regset :=
 
 (** Auxiliaries for memory accesses *)
 
-
+(* TODO: delete this or define it as [parexec_load_offset ge chunk rs rs m m d a ofs] *)
 Definition exec_load_offset (chunk: memory_chunk) (rs: regset) (m: mem) (d a: ireg) (ofs: offset) :=
   match (eval_offset ge ofs) with
   | OK ptr => match Mem.loadv chunk m (Val.offset_ptr (rs a) ptr) with
@@ -78,12 +299,14 @@ Definition exec_load_offset (chunk: memory_chunk) (rs: regset) (m: mem) (d a: ir
   | _ => Stuck
   end.
 
+(* TODO: delete this or define it as [parexec_load_reg ge chunk rs rs m m d a ro] *)
 Definition exec_load_reg (chunk: memory_chunk) (rs: regset) (m: mem) (d a ro: ireg) :=
   match Mem.loadv chunk m (Val.addl (rs a) (rs ro)) with
   | None => Stuck
   | Some v => Next (rs#d <- v) m
   end.
 
+(* TODO: delete this as define it as ... *)
 Definition exec_store_offset (chunk: memory_chunk) (rs: regset) (m: mem) (s a: ireg) (ofs: offset) :=
   match (eval_offset ge ofs) with
   | OK ptr => match Mem.storev chunk m (Val.offset_ptr (rs a) ptr) (rs s) with
@@ -93,6 +316,7 @@ Definition exec_store_offset (chunk: memory_chunk) (rs: regset) (m: mem) (s a: i
   | _ => Stuck
   end.
 
+(* TODO: delete this as define it as ... *)
 Definition exec_store_reg (chunk: memory_chunk) (rs: regset) (m: mem) (s a ro: ireg) :=
   match Mem.storev chunk m (Val.addl (rs a) (rs ro)) (rs s) with
   | None => Stuck
@@ -103,6 +327,7 @@ Definition exec_store_reg (chunk: memory_chunk) (rs: regset) (m: mem) (s a ro: i
 
 (** * basic instructions *)
 
+(* TODO: define this [parexec_basic_instr ge bi rs rs m m] *)
 Definition exec_basic_instr (bi: basic) (rs: regset) (m: mem) : outcome :=
   match bi with
   | PArith ai => Next (exec_arith_instr ai rs) m
@@ -157,12 +382,9 @@ Fixpoint exec_body (body: list basic) (rs: regset) (m: mem): outcome :=
      end
   end.
 
+(** * control-flow instructions *)
 
-
-(** Position corresponding to a label *)
-
-
-
+(* TODO: delete this or define it as [par_goto_label ge f lbl rs rs m] *)
 Definition goto_label (f: function) (lbl: label) (rs: regset) (m: mem) : outcome :=
   match label_pos lbl 0 (fn_blocks f) with
   | None => Stuck
@@ -173,11 +395,7 @@ Definition goto_label (f: function) (lbl: label) (rs: regset) (m: mem) : outcome
       end
   end.
 
-(** Evaluating a branch 
-
-Warning: in m PC is assumed to be already pointing on the next instruction !
-
-*)
+(* TODO: delete this or define it as [par_eval_branch ge f l rs rs m res] *)
 Definition eval_branch (f: function) (l: label) (rs: regset) (m: mem) (res: option bool) : outcome :=
   match res with
     | Some true  => goto_label f l rs m
@@ -185,23 +403,7 @@ Definition eval_branch (f: function) (l: label) (rs: regset) (m: mem) (res: opti
     | None => Stuck
   end.
 
-
-(** Execution of a single control-flow instruction [i] in initial state [rs] and
-    [m].  Return updated state.
-
-    As above: PC is assumed to be incremented on the next block before the control-flow instruction
-
-    For instructions that correspond tobuiltin
-    actual RISC-V instructions, the cases are straightforward
-    transliterations of the informal descriptions given in the RISC-V
-    user-mode specification.  For pseudo-instructions, refer to the
-    informal descriptions given above.
-
-    Note that we set to [Vundef] the registers used as temporaries by
-    the expansions of the pseudo-instructions, so that the RISC-V code
-    we generate cannot use those registers to hold values that must
-    survive the execution of the pseudo-instruction. *)
-
+(* TODO: delete this or define it as [parexec_control ge f oc rs rs m] *)
 Definition exec_control (f: function) (oc: option control) (rs: regset) (m: mem) : outcome :=
   match oc with
   | Some ic =>
@@ -252,32 +454,30 @@ Definition exec_control (f: function) (oc: option control) (rs: regset) (m: mem)
   | None => Next rs m
 end.
 
+(* TODO: change [exec_bblock] for a definition like this one: 
+
+Definition exec_exit (f: function) ext size_b (rs: regset) (m: mem) 
+  := parexec_exit ge f ext size_b rs rs m.
+
 Definition exec_bblock (f: function) (b: bblock) (rs0: regset) (m: mem) : outcome :=
   match exec_body (body b) rs0 m with
-  | Next rs' m' =>
-    let rs1 := nextblock b rs' in exec_control f (exit b) rs1 m'
+  | Next rs' m' => exec_exit f (exit b) (Ptrofs.repr (size b)) rs' m'
   | Stuck => Stuck
   end.
 
-(** Translation of the LTL/Linear/Mach view of machine registers to
-  the RISC-V view.  Note that no LTL register maps to [X31].  This
-  register is reserved as temporary, to be used by the generated RV32G
-  code.  *)
-
-
-
-
+*)
 
+Definition exec_bblock (f: function) (b: bblock) (rs0: regset) (m: mem) : outcome :=
+  match exec_body (body b) rs0 m with
+  | Next rs' m' =>
+    let rs1 := nextblock b rs' in exec_control f (exit b) rs1 m'
+  | Stuck => Stuck
+  end.
 
 
 (** Execution of the instruction at [rs PC]. *)
 
 
-(** TODO
- * For now, we consider a builtin is alone in a basic block.
- * Perhaps there is a way to avoid that ?
- *)
-
 Inductive step: state -> trace -> state -> Prop :=
   | exec_step_internal:
       forall b ofs f bi rs m rs' m',
@@ -318,68 +518,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
@@ -390,65 +528,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.
-*)