relecture

2 files changed, 148 insertions, 27 deletions

diff --git a/mppa_k1c/Asmblock.v b/mppa_k1c/Asmblock.v
index ba14c451..4f825bf5 100644
--- a/mppa_k1c/Asmblock.v
+++ b/mppa_k1c/Asmblock.v
@@ -576,7 +576,6 @@ Fixpoint set_res (res: builtin_res preg) (v: val) (rs: regset) : regset :=
 
 Section RELSEM.
 
-Variable ge: genv.
 
 (** The semantics is purely small-step and defined as a function
   from the current state (a register set + a memory state)
@@ -713,6 +712,9 @@ FIXME: replace parameter "m" by a function corresponding to the resul of "(Mem.v
 
 *)
 
+Variable ge: genv.
+
+
 Definition exec_arith_instr (ai: ar_instruction) (rs: bregset) (m: mem) : bregset :=
   match ai with
   | PArithR n d =>
diff --git a/mppa_k1c/Asmbundle.v b/mppa_k1c/Asmbundle.v
index 14a2ea7e..b5f92c2a 100644
--- a/mppa_k1c/Asmbundle.v
+++ b/mppa_k1c/Asmbundle.v
@@ -14,6 +14,19 @@ Require Import Conventions.
 Require Export Asmblock.
 Require Import ListSet.
 
+
+Fixpoint notIn {A} (x: A) (l:list A): Prop :=
+  match l with
+  | nil => True
+  | a::l' => x <> a /\ notIn x l'
+  end.
+
+Lemma notIn_rewrite A (r:A) l: (~List.In r l) <-> notIn r l.
+Proof.
+  induction l; simpl; intuition.
+Qed.
+
+
 Section RELSEM.
 
 Variable ge: genv.
@@ -44,6 +57,71 @@ Proof.
   - unfold all_bregs. repeat (apply in_app_iff; right). simpl. left; auto.
 Qed.
 
+Definition writeregs (i: instruction): list breg :=
+  match i with
+  (* Control instructions *)
+  | Pset rd rs => rd::nil
+  | Pget rd rs => IR rd::nil
+  | Pcall s => RA::nil
+  (* Load *)
+  | PLoadRRO i rd ra o => IR rd::nil
+  (* Arith *)
+  | PArithR i rd => IR rd::nil
+  | PArithRR i rd rs => IR rd::nil
+  | PArithRI32 i rd imm => IR rd::nil
+  | PArithRI64 i rd imm => IR rd::nil
+  | PArithRRR i rd rs1 rs2 => IR rd::nil
+  | PArithRRI32 i rd rs imm => IR rd::nil
+  | PArithRRI64 i rd rs imm => IR rd::nil
+  (* Alloc and freeframe *)
+  | Pallocframe _ _ => IR FP::IR GPR31::IR SP :: nil
+  | Pfreeframe _ _ => IR GPR31::IR SP :: nil
+  (* builtins : only implemented in OCaml, we know nothing about them *)
+  | Pbuiltin _ _ _ => all_bregs
+  (* Instructions that do not write *)
+  | Pnop | Pret | Pgoto _ | Pj_l _ | Pcb _ _ _ | Pcbu _ _ _ | PStoreRRO _ _ _ _ => nil
+  end.
+
+Lemma update_PC_breg (rs: regset) v (r: breg):
+  (rs#PC <-- v) r = rs r.
+Proof.
+ rewrite Pregmap.gso; congruence.
+Qed.
+
+Lemma update_pregs_diff (rs:regset) rd x r: r <> rd -> update_pregs rs (rs # rd <- x) r = rs r.
+Proof.
+  unfold update_pregs. intro H. rewrite Bregmap.gso; congruence.
+Qed.
+ 
+Hint Rewrite update_PC_breg update_pregs_diff: regset_rw.
+
+Fact writeregs_correct f i rs m rs' m' r: 
+    ~(List.In r (writeregs i)) -> 
+    (exec_bblock ge f (bblock_single_inst i) rs m) = Next rs' m' ->
+    rs' r = rs r.
+Proof.
+  rewrite notIn_rewrite.
+  unfold exec_bblock, nextblock, size; destruct i; simpl.
+  destruct i; simpl.
+  destruct i; simpl; try ( 
+    destruct i; simpl; intro H; decompose [and] H; clear H;
+    intros H; inversion_clear H;
+    autorewrite with regset_rw; auto; fail).
+  - (* LOAD *) destruct i; simpl. 
+  destruct i; simpl; unfold exec_load; 
+  destruct (Mem.loadv _ _ _); try discriminate;
+  intro H; decompose [and] H; clear H;
+  intros H; inversion_clear H;
+  autorewrite with regset_rw; auto.
+  - (* STORE *) destruct i; simpl. 
+  destruct i; simpl; unfold exec_store;
+  destruct (Mem.storev _ _ _ _); try discriminate;
+  intro H; clear H;
+  intros H; inversion_clear H;
+  autorewrite with regset_rw; auto.
+  - (* ALLOCFRAME *)
+Admitted.
+
 Definition readregs (i: instruction) : list breg :=
   match i with
   (* Control instructions *)
@@ -60,37 +138,67 @@ Definition readregs (i: instruction) : list breg :=
   | PArithRRR i rd rs1 rs2 => IR rs1 :: IR rs2 :: nil
   | PArithRRI32 i rd rs imm => IR rs :: nil
   | PArithRRI64 i rd rs imm => IR rs :: nil
-  (* Alloc and freeframe and builtins : implemented in OCaml, we know nothing about them *)
-  | Pallocframe _ _ | Pfreeframe _ _ | Pbuiltin _ _ _ => all_bregs
+  (* Alloc and freeframe (from the semantics) *) 
+  | Pallocframe _ _ | Pfreeframe _ _ => IR SP :: nil
+  (* builtins : only implemented in OCaml, we know nothing about them *)
+  | Pbuiltin _ _ _ => all_bregs
   (* Instructions that do not read *)
   | Pnop | Pcall _ | Pgoto _ | Pj_l _ | PArithR _ _ | PArithRI32 _ _ _ | PArithRI64 _ _ _ => nil
   end.
 
-Definition writeregs (i: instruction): list breg :=
-  match i with
-  (* Control instructions *)
-  | Pset rd rs => rd::nil
-  | Pget rd rs => IR rd::nil
-  | Pcall s => RA::nil
-  (* Load *)
-  | PLoadRRO i rd ra o => IR rd::nil
-  (* Arith *)
-  | PArithR i rd => IR rd::nil
-  | PArithRR i rd rs => IR rd::nil
-  | PArithRI32 i rd imm => IR rd::nil
-  | PArithRI64 i rd imm => IR rd::nil
-  | PArithRRR i rd rs1 rs2 => IR rd::nil
-  | PArithRRI32 i rd rs imm => IR rd::nil
-  | PArithRRI64 i rd rs imm => IR rd::nil
-  (* Alloc and freeframe *)
-  | Pallocframe _ _ | Pfreeframe _ _ | Pbuiltin _ _ _ => all_bregs
-  (* Instructions that do not write *)
-  | Pnop | Pret | Pgoto _ | Pj_l _ | Pcb _ _ _ | Pcbu _ _ _ | PStoreRRO _ _ _ _ => nil
+Axiom TODO: False.
+
+Definition outcome_equiv (r: breg) v (o1 o2: outcome (rgset:=regset))  :=
+  match o1 with
+  | Next rs1 m1 => exists rs2, exists m2, o2=Next rs2 m2 /\ (forall r, (rs1#r <-- v) r = rs2 r) /\ (forall chunk p, Mem.loadv chunk m1 p = Mem.loadv chunk m2 p)
+  | Stuck => o2 = Stuck
   end.
 
-(* Definition disjoint {A: Type} (l l':list A) : Prop := forall r, In r l -> In r l' -> False. *)
+Fact useregs_correct f i rs m r v: 
+  ~(List.In r ((readregs i)++(writeregs i))) -> 
+    outcome_equiv r v
+                  (exec_bblock ge f (bblock_single_inst i) rs m) 
+                  (exec_bblock ge f (bblock_single_inst i) (rs#r <-- v) m).
+Proof.
+  rewrite notIn_rewrite.
+  unfold exec_bblock, nextblock, size; destruct i; simpl.
+  + destruct i; simpl.
+   - destruct i; simpl.
+     * intro H; decompose [and] H; clear H. (* H useless *)
+       elim TODO.
+     * intro H; decompose [and] H; clear H.
+       destruct i; simpl.
+       simpl; eexists; eexists; constructor 1; eauto. 
+       intuition. 
+       destruct r0.
+       rewrite! update_PC_breg.
+    (* TODO: lemma on  rs # _ <-- _ *)
+Abort.
+
+(* alternative definition of disjoint *)
+Definition disjoint_x {A: Type} (l l':list A) : Prop := forall r, In r l -> ~In r l'. (* TODO: use notIn instead ? *)
+
+Example disjoint_x_ex1: disjoint_x (4::2::1::nil) (3::5::7::nil).
+Proof.
+  unfold disjoint_x; simpl. intuition.
+Qed.
+
+Lemma disjoint_x_nilr : forall A (l:list A), disjoint_x l nil.
+Proof.
+  unfold disjoint_x; simpl. intuition.
+Qed.
+
+Lemma disjoint_x_consl : forall A l l' (e:A), disjoint_x l l' -> (~ In e l') -> disjoint_x (e::l) l'.
+Proof.
+  unfold disjoint_x; simpl. intuition (subst; eauto).
+Qed.
+
+(* Inductive definition of disjoint, easier to reason with 
+
+Sylvain: I am not sure. Actually, from the above definition, we can still prove the following "constructors" as lemma if needed
+ (cf. example above).
+*)
 
-(* Inductive definition of disjoint, easier to reason with *)
 Inductive disjoint {A: Type} : list A -> list A -> Prop :=
   | disjoint_nilr : forall l, disjoint l nil
   | disjoint_nill : forall l, disjoint nil l
@@ -106,15 +214,26 @@ Proof.
 Qed.
 
 Inductive depfree : list breg -> list breg -> list instruction -> Prop :=
-  | depfree_nil : forall lw lr, depfree lw lr nil
+  | depfree_nil : forall lr lw, depfree lr lw nil
   | depfree_cons : forall i lri lwi lw lr l,
                     lri = readregs i -> lwi = writeregs i ->
                     disjoint lwi lw -> (* Checking for WAW *)
-                    disjoint lwi lr -> (* Checking for RAW *)
+                    disjoint lri lw -> (* Checking for RAW *)
                     depfree (lr++lri) (lw++lwi) l ->
                     depfree lr lw (i::l)
   .
 
+(* une version alternative *)
+Inductive depfreex : list breg -> list instruction -> Prop :=
+  | depfreex_nil : forall lw, depfreex lw nil
+  | depfreex_cons : forall i lri lwi lw l,
+                    lri = readregs i -> lwi = writeregs i ->
+                    disjoint (lri++lwi) lw -> (* Checking for WAW + RAW *)
+                    depfreex (lw++lwi) l ->
+                    depfreex lw (i::l)
+  .
+
+
 (* FIXME: STUB *)
 Definition is_bundle (b:bblock):=True.