Lemma for bisimu with potential builtins, alloc and constant

1 files changed, 132 insertions, 65 deletions

diff --git a/aarch64/Asmblockdeps.v b/aarch64/Asmblockdeps.v
index 31ce8065..3c5cc9dd 100644
--- a/aarch64/Asmblockdeps.v
+++ b/aarch64/Asmblockdeps.v
@@ -36,6 +36,7 @@ Require Import Coqlib.
 Require Import ImpSimuTest.
 Require Import Axioms.
 Require Import Permutation.
+Require Import Events.
 
 Require Import Lia.
 
@@ -121,12 +122,19 @@ Inductive load_op :=
   | OloadU (ld: load_rd_a) (a: addressing)
 .
 
+Inductive allocf_op :=
+  | OAllocf_SP (sz: Z) (linkofs: ptrofs)
+  | OAllocf_Mem (sz: Z) (linkofs: ptrofs)
+.
+
 Inductive op_wrap :=
   (* arithmetic operation *)
   | Arith (op: arith_op)
   | Load (ld: load_op)
   | Store (st: store_op)
+  | Allocframe (al: allocf_op)
   | Control (co: control_op)
+  | Constant (v: val)
 .
 
 Definition op:=op_wrap.
@@ -335,9 +343,9 @@ Definition arith_op_eval (op: arith_op) (l: list value) :=
   | _, _ => None
   end.
 
-Definition call_ll_storev (n: store_rs_a) (m: mem) (v: option val) (vs: val) :=
+Definition call_ll_storev (c: memory_chunk) (m: mem) (v: option val) (vs: val) :=
   match v with
-  | Some va => match Mem.storev (chunk_store_rs_a n) m va vs with
+  | Some va => match Mem.storev c m va vs with
                | Some m' => Some (Memstate m')
                | None => None
                end
@@ -351,7 +359,7 @@ Definition exec_store1 (n: store_rs_a) (m: mem) (a: addressing) (vr vs: val) :=
     | ADadr _ id ofs => Some (Val.addl vs (symbol_low Ge.(_lk) id ofs))
     | _ => None
     end in
-  call_ll_storev n m v vr.
+  call_ll_storev (chunk_store_rs_a n) m v vr.
 
 Definition exec_store2 (n: store_rs_a) (m: mem) (a: addressing) (vr vs1 vs2: val) :=
   let v :=
@@ -362,10 +370,10 @@ Definition exec_store2 (n: store_rs_a) (m: mem) (a: addressing) (vr vs1 vs2: val
     | ADuxt _ _ n => Some (Val.addl vs1 (Val.shll (Val.longofintu vs2) (Vint n)))
     | _ => None
     end in
-  call_ll_storev n m v vr.
+  call_ll_storev (chunk_store_rs_a n) m v vr.
   
 Definition exec_storeU (n: store_rs_a) (m: mem) (a: addressing) (vr: val) :=
-  call_ll_storev n m None vr.
+  call_ll_storev (chunk_store_rs_a n) m None vr.
 
 Definition goto_label_deps (f: function) (lbl: label) (vpc: val) :=
   match label_pos lbl 0 (fn_blocks f) with
@@ -393,10 +401,10 @@ Definition store_eval (o: store_op) (l: list value) :=
   | _, _ => None
   end.
 
-Definition call_ll_loadv (n: load_rd_a) (m: mem) (v: option val) :=
+Definition call_ll_loadv (c: memory_chunk) (transf: val -> val) (m: mem) (v: option val) :=
   match v with
-  | Some va => match Mem.loadv (chunk_load_rd_a n) m va with
-               | Some v' => Some (Val ((interp_load_rd_a n) v'))
+  | Some va => match Mem.loadv c m va with
+               | Some v' => Some (Val (transf v'))
                | None => None
                end
   | None => None (* should never occurs *)
@@ -409,7 +417,7 @@ Definition exec_load1 (n: load_rd_a) (m: mem) (a: addressing) (vl: val) :=
     | ADadr _ id ofs => Some (Val.addl vl (symbol_low Ge.(_lk) id ofs))
     | _ => None
     end in
-  call_ll_loadv n m v.
+  call_ll_loadv (chunk_load_rd_a n) (interp_load_rd_a n) m v.
 
 Definition exec_load2 (n: load_rd_a) (m: mem) (a: addressing) (vl1 vl2: val) :=
   let v :=
@@ -420,10 +428,10 @@ Definition exec_load2 (n: load_rd_a) (m: mem) (a: addressing) (vl1 vl2: val) :=
     | ADuxt _ _ n => Some (Val.addl vl1 (Val.shll (Val.longofintu vl2) (Vint n)))
     | _ => None
     end in
-  call_ll_loadv n m v.
+  call_ll_loadv (chunk_load_rd_a n) (interp_load_rd_a n) m v.
   
 Definition exec_loadU (n: load_rd_a) (m: mem) (a: addressing) :=
-  call_ll_loadv n m None.
+  call_ll_loadv (chunk_load_rd_a n) (interp_load_rd_a n) m None.
 
 Definition load_eval (o: load_op) (l: list value) :=
   match o, l with
@@ -433,12 +441,31 @@ Definition load_eval (o: load_op) (l: list value) :=
   | _, _ => None
   end.
 
+Definition eval_allocf (o: allocf_op) (l: list value) :=
+  match o, l with
+  | OAllocf_Mem sz linkofs, [Val spv; Memstate m] =>
+      let (m1, stk) := Mem.alloc m 0 sz in
+      let sp := (Vptr stk Ptrofs.zero) in
+      call_ll_storev Mint64 m1 (Some (Val.offset_ptr sp linkofs)) spv
+  | OAllocf_SP sz linkofs, [Val spv; Memstate m] =>
+      let (m1, stk) := Mem.alloc m 0 sz in
+      let sp := (Vptr stk Ptrofs.zero) in
+      match call_ll_storev Mint64 m1 (Some (Val.offset_ptr sp linkofs)) spv with
+      | None => None
+      | Some ms => Some (Val sp)
+      end
+  | _, _ => None
+  end.
+
 Definition op_eval (op: op) (l:list value) :=
   match op, l with
   | Arith op, l => arith_op_eval op l
   | Load o, l => load_eval o l
   | Store o, l => store_eval o l
+  | Allocframe o, l => eval_allocf o l
   | Control o, l => control_eval o l
+  | Constant v, [] => Some (Val v)
+  | _, _ => None
   end.
 
 Definition vz_eq (vz1 vz2: val) : ?? bool :=
@@ -685,6 +712,9 @@ Qed.
 Hint Resolve load_op_eq_correct: wlp.
 Opaque load_op_eq_correct.
 
+(*Definition allocf_op_eq (al1 al2: allocf_op): ?? bool :=*)
+  
+
 Definition op_eq (o1 o2: op): ?? bool :=
   match o1 with
   | Arith i1 =>
@@ -695,6 +725,9 @@ Definition op_eq (o1 o2: op): ?? bool :=
       match o2 with Load i2 => load_op_eq i1 i2 | _ => RET false end
   | Store i1 =>
       match o2 with Store i2 => store_op_eq i1 i2 | _ => RET false end
+  | Constant c1 =>
+    match o2 with Constant c2 => phys_eq c1 c2 | _ => RET false end
+  | _ => RET false
   end.
 
 Lemma op_eq_correct o1 o2: 
@@ -987,6 +1020,12 @@ Definition trans_basic (b: basic) : inst :=
       let lr := eval_addressing_rlocs_ld ld a in [(#r, lr)]
   | PStore st r a => 
       let lr := eval_addressing_rlocs_st st r a in [(pmem, lr)]
+  (*| Pallocframe sz linkofs =>*)
+      (*[(#X29, PReg(#SP));*)
+       (*(#SP, Op (OAllocf_SP sz linkofs) (PReg (#SP) @ PReg pmem @ Enil));*)
+       (*(#X16, Op (Constant Vundef) Enil);*)
+       (*(pmem, Op (OAllocf_Mem ))]*)
+
   | _ => []
   (*| PLoadRRO trap n d a ofs => [(#d, Op (Load (OLoadRRO n trap ofs)) (PReg (#a) @ PReg pmem @ Enil))]*)
   (*| PLoadRRR trap n d a ro =>  [(#d, Op (Load (OLoadRRR n trap)) (PReg (#a) @ PReg (#ro) @ PReg pmem @ Enil))]*)
@@ -1900,30 +1939,30 @@ Proof.
   - intros X; erewrite run_app_None; eauto.
 Qed.*)
 
-Theorem bisimu_bblock rsr mr sr bdy1 bdy2 ex sz:
-  match_states (State rsr mr) sr ->
-  match_outcome 
-   match bbstep Ge.(_lk) Ge.(_genv) Ge.(_fn) ex (Ptrofs.repr sz) bdy1 rsr mr with
-   | Some (State rs' m') => exec_body Ge.(_lk) Ge.(_genv) bdy2 rs' m'
-   | Stuck => Stuck
-   end
-   (run Ge ((trans_block_aux bdy1 sz (Some (PCtlFlow (ex))))++(trans_body bdy2)) sr).
-Proof.
-  intros.
-  exploit (bisimu rsr mr sr bdy1 ex sz); eauto.
-  destruct (bbstep _ _ _ _ _ _); simpl.
-  - intros (s' & X1 & X2).
-    erewrite run_app_Some; eauto. destruct s.
-    eapply bisimu_body; eauto.
-  - intros; erewrite run_app_None; eauto.
-Qed.
+(*Theorem bisimu_bblock rsr mr sr bdy1 bdy2 ex sz:*)
+  (*match_states (State rsr mr) sr ->*)
+  (*match_outcome *)
+   (*match bbstep Ge.(_lk) Ge.(_genv) Ge.(_fn) ex (Ptrofs.repr sz) bdy1 rsr mr with*)
+   (*| Some (State rs' m') => exec_body Ge.(_lk) Ge.(_genv) bdy2 rs' m'*)
+   (*| Stuck => Stuck*)
+   (*end*)
+   (*(run Ge ((trans_block_aux bdy1 sz (Some (PCtlFlow (ex))))++(trans_body bdy2)) sr).*)
+(*Proof.*)
+  (*intros.*)
+  (*exploit (bisimu rsr mr sr bdy1 ex sz); eauto.*)
+  (*destruct (bbstep _ _ _ _ _ _); simpl.*)
+  (*- intros (s' & X1 & X2).*)
+    (*erewrite run_app_Some; eauto. destruct s.*)
+    (*eapply bisimu_body; eauto.*)
+  (*- intros; erewrite run_app_None; eauto.*)
+(*Qed.*)
 
-Lemma trans_body_perserves_permutation bdy1 bdy2:
-  Permutation bdy1 bdy2 ->
-  Permutation (trans_body bdy1) (trans_body bdy2).
-Proof.
-  induction 1; simpl; econstructor; eauto.
-Qed.
+(*Lemma trans_body_perserves_permutation bdy1 bdy2:*)
+  (*Permutation bdy1 bdy2 ->*)
+  (*Permutation (trans_body bdy1) (trans_body bdy2).*)
+(*Proof.*)
+  (*induction 1; simpl; econstructor; eauto.*)
+(*Qed.*)
 
 Lemma trans_body_app bdy1: forall bdy2,
    trans_body (bdy1++bdy2) = (trans_body bdy1) ++ (trans_body bdy2).
@@ -1931,19 +1970,19 @@ Proof.
   induction bdy1; simpl; congruence.
 Qed.
 
-Theorem trans_block_perserves_permutation bdy1 bdy2 b:
-  Permutation (bdy1 ++ bdy2) (body b) ->
-  Permutation (trans_block b) ((trans_block_aux bdy1 (size b) (exit b))++(trans_body bdy2)).
-Proof.
-  intro H; unfold trans_block, trans_block_aux.
-  eapply perm_trans.
-  - eapply Permutation_app_tail. 
-    apply trans_body_perserves_permutation.
-    apply Permutation_sym; eapply H.
-  - rewrite trans_body_app. rewrite <-! app_assoc.
-    apply Permutation_app_head.
-    apply Permutation_app_comm.
-Qed.
+(*Theorem trans_block_perserves_permutation bdy1 bdy2 b:*)
+  (*Permutation (bdy1 ++ bdy2) (body b) ->*)
+  (*Permutation (trans_block b) ((trans_block_aux bdy1 (size b) (exit b))++(trans_body bdy2)).*)
+(*Proof.*)
+  (*intro H; unfold trans_block, trans_block_aux.*)
+  (*eapply perm_trans.*)
+  (*- eapply Permutation_app_tail. *)
+    (*apply trans_body_perserves_permutation.*)
+    (*apply Permutation_sym; eapply H.*)
+  (*- rewrite trans_body_app. rewrite <-! app_assoc.*)
+    (*apply Permutation_app_head.*)
+    (*apply Permutation_app_comm.*)
+(*Qed.*)
 
 (*Theorem bisimu_par rs1 m1 s1' b ge fn o2:*)
     (*Ge = Genv ge fn ->*)
@@ -1997,22 +2036,44 @@ Qed.
   (*apply (bisimu_par_control (exit b) (size b) (Val.offset_ptr (rs PC) (Ptrofs.repr (size b))) ge fn rs rs m m s s); auto.*)
 (*Qed.*)
 
-(*Theorem bisimu rs m b ge fn s:*)
-    (*Ge = Genv ge fn ->*)
-    (*match_states (State rs m) s -> *)
-    (*match_outcome (exec_bblock ge fn b rs m) (exec Ge (trans_block b) s).*)
-(*Proof.*)
-  (*intros GENV MS. unfold exec_bblock.*)
-  (*exploit (bisimu_body (body b) ge fn rs m s); eauto.*)
-  (*unfold exec, trans_block; simpl.*)
-  (*destruct (exec_body _ _ _ _); simpl.*)
-  (*- intros (s' & X1 & X2).*)
-    (*erewrite run_app_Some; eauto.*)
-    (*exploit (bisimu_exit ge fn b rs0 m0 s'); eauto.*)
-    (*subst Ge; simpl. destruct X2 as (Y1 & Y2). erewrite Y2; simpl.*)
-    (*destruct (inst_run _ _ _); simpl; auto.*)
-  (*- intros X; erewrite run_app_None; eauto.*)
-(*Qed.*)
+Lemma bbstep_is_exec_bblock: forall bb (cfi: cf_instruction) size_bb bdy rs m rs' m' t,
+  (body bb) = bdy ->
+  (exit bb) = Some (PCtlFlow cfi) ->
+  Ptrofs.repr (size bb) = size_bb ->
+  exec_bblock Ge.(_lk) Ge.(_genv) Ge.(_fn) bb rs m t rs' m'
+  <-> (bbstep Ge.(_lk) Ge.(_genv) Ge.(_fn) (cfi) size_bb bdy rs m = Next rs' m' /\ t = E0).
+Proof.
+  intros.
+Admitted.
+
+(* TODO This is the lemma we should use if we want to modelize
+builtins in our scheduling process.
+If we do not modelize builtins, we could use a simpler definition (trace E0) *)
+(*
+Theorem bisimu' rs m rs' m' bb s:
+    match_states (State rs m) s -> 
+    (exists t, exec_bblock Ge.(_lk) Ge.(_genv) Ge.(_fn) bb rs m t rs' m')
+    <-> (exists s', (exec Ge (trans_block bb) s) = Some s' /\ match_states (State rs' m') s').
+Proof.
+  intros MS.
+  destruct (exit bb) eqn:EQEXIT.
+  destruct c eqn:EQC.
+  - split.
+    + intros (t & H).
+  rewrite bbstep_is_exec_bblock in H; eauto.
+  eexists; split. destruct H as [H0 H1].
+  generalize (bisimu )
+  unfold exec_bblock.
+  exploit (bisimu_body (body b) ge fn rs m s); eauto.
+  unfold exec, trans_block; simpl.
+  destruct (exec_body _ _ _ _); simpl.
+  - intros (s' & X1 & X2).
+    erewrite run_app_Some; eauto.
+    exploit (bisimu_exit ge fn b rs0 m0 s'); eauto.
+    subst Ge; simpl. destruct X2 as (Y1 & Y2). erewrite Y2; simpl.
+    destruct (inst_run _ _ _); simpl; auto.
+  - intros X; erewrite run_app_None; eauto.
+Qed.*)
 
 Theorem trans_state_match: forall S, match_states S (trans_state S).
 Proof.
@@ -2428,17 +2489,23 @@ Definition string_of_control (op: control_op) : pstring :=
   (*| OIncremPC _ => "OIncremPC"*)
   end.
 
+Definition string_of_allocf (op: allocf_op) : pstring :=
+  match op with
+  | OAllocf_SP _ _ => "OAllocf_SP"
+  | OAllocf_Mem _ _ => "OAllocf_Mem"
+  end.
+
 Definition string_of_op (op: P.op): ?? pstring := 
   match op with
   | Arith op => RET (string_of_arith op)
   | Load op => RET (string_of_load op)
   | Store op => RET (string_of_store op)
   | Control op => RET (string_of_control op)
-  (*| Allocframe _ _ => RET (Str "Allocframe")*)
+  | Allocframe op => RET (string_of_allocf op)
   (*| Allocframe2 _ _ => RET (Str "Allocframe2")*)
   (*| Freeframe _ _ => RET (Str "Freeframe")*)
   (*| Freeframe2 _ _ => RET (Str "Freeframe2")*)
-  (*| Constant _ => RET (Str "Constant")*)
+  | Constant _ => RET (Str "Constant")
   (*| Fail => RET (Str "Fail")*)
   end.
 End SECT_BBLOCK_EQUIV.