draft of the exec_bblock Asmblockdeps proof

1 files changed, 116 insertions, 29 deletions

diff --git a/aarch64/Asmblockdeps.v b/aarch64/Asmblockdeps.v
index 0427d1c4..1bccb5dd 100644
--- a/aarch64/Asmblockdeps.v
+++ b/aarch64/Asmblockdeps.v
@@ -199,6 +199,7 @@ Inductive op_wrap :=
 Definition op:=op_wrap.
 
 Coercion Arith: arith_op >-> op_wrap.
+Coercion Control: control_op >-> op_wrap.
 
 Definition v_compare_int (v1 v2: val) : CRflags :=
   {| _CN := (Val.negative (Val.sub v1 v2));
@@ -1056,7 +1057,7 @@ Definition trans_control (ctl: control) : inst :=
                     (#PC, Op (Control (Obtbl tbl)) (PReg(#r) @ PReg(#PC) @ Enil));
                     (#X16, Op (Constant Vundef) Enil);
                     (#X17, Op (Constant Vundef) Enil)]
-  | Pbuiltin ef args res => []
+  | Pbuiltin ef args res => [(# PC, Op (Control OError) Enil)]
   end.
 
 Definition trans_exit (ex: option control) : L.inst :=
@@ -1936,24 +1937,51 @@ Qed.
 
 Theorem bisimu_exit ex sz rsr mr sr:
   match_states (State rsr mr) sr ->
-  match_outcome (estep Ge.(_genv) Ge.(_fn) ex (Ptrofs.repr sz) rsr mr) (inst_run Ge (trans_pcincr sz (trans_exit (Some (PCtlFlow ex)))) sr sr).
+  match_outcome (estep Ge.(_genv) Ge.(_fn) ex (Ptrofs.repr sz) rsr mr) (inst_run Ge (trans_pcincr sz (trans_exit ex)) sr sr).
 Proof.
-  intros; unfold estep.
-  exploit (bisimu_control ex sz rsr mr sr); eauto.
+  intros MS; unfold estep.
+  destruct ex.
+  - destruct c.
+    + exploit (bisimu_control i sz rsr mr sr); eauto.
+    + simpl; inv MS. unfold control_eval; destruct Ge.
+      replace_pc; rewrite H0. reflexivity.
+  - simpl. inv MS. eexists; split; [| split].
+    + unfold control_eval; destruct Ge.
+      replace_pc; rewrite (H0 PC); eauto.
+    + rewrite assign_diff; auto.
+    + intros rr. unfold incrPC. destruct (PregEq.eq rr PC); subst.
+      * rewrite sr_gss, Pregmap.gss. reflexivity.
+      * rewrite assign_diff, Pregmap.gso; try rewrite H0; try rewrite ppos_discr; auto.
 Qed.
 
 Definition trans_block_aux bdy sz ex := (trans_body bdy) ++ (trans_pcincr sz (trans_exit ex) :: nil).
 
-Theorem bisimu rsr mr sr bdy ex sz:
+(*Theorem bisimu rsr mr sr bdy ex sz:*)
+  (*match_states (State rsr mr) sr ->*)
+  (*match_outcome (bbstep Ge.(_lk) Ge.(_genv) Ge.(_fn) ex (Ptrofs.repr sz) bdy rsr mr) (run Ge (trans_block_aux bdy sz (Some (PCtlFlow ex))) sr).*)
+(*Proof.*)
+  (*intros MS. unfold bbstep, trans_block_aux.*)
+  (*exploit (bisimu_body bdy rsr mr sr); eauto.*)
+  (*destruct (exec_body _ _ _ _ _); simpl.*)
+  (*- unfold match_states in *. intros (s' & X1 & X2). destruct s.*)
+    (*erewrite run_app_Some; eauto.*)
+    (*exploit (bisimu_exit ex sz _rs _m s'); eauto.*)
+    (*destruct Ge; simpl. destruct MS as (Y1 & Y2). destruct X2 as (X2 & X3).*)
+    (*replace_pc. erewrite !X3; simpl.*)
+    (*destruct (inst_run _ _ _ _); simpl; auto.*)
+  (*- intros X; erewrite run_app_None; eauto.*)
+(*Qed.*)
+
+Theorem bisimu rsr mr sr bb:
   match_states (State rsr mr) sr ->
-  match_outcome (bbstep Ge.(_lk) Ge.(_genv) Ge.(_fn) ex (Ptrofs.repr sz) bdy rsr mr) (run Ge (trans_block_aux bdy sz (Some (PCtlFlow ex))) sr).
+  match_outcome (bbstep Ge.(_lk) Ge.(_genv) Ge.(_fn) bb rsr mr) (exec Ge (trans_block bb) sr).
 Proof.
-  intros MS. unfold bbstep, trans_block_aux.
-  exploit (bisimu_body bdy rsr mr sr); eauto.
+  intros MS. unfold bbstep, trans_block.
+  exploit (bisimu_body (body bb) rsr mr sr); eauto.
   destruct (exec_body _ _ _ _ _); simpl.
   - unfold match_states in *. intros (s' & X1 & X2). destruct s.
     erewrite run_app_Some; eauto.
-    exploit (bisimu_exit ex sz _rs _m s'); eauto.
+    exploit (bisimu_exit (exit bb) (size bb) _rs _m s'); eauto.
     destruct Ge; simpl. destruct MS as (Y1 & Y2). destruct X2 as (X2 & X3).
     replace_pc. erewrite !X3; simpl.
     destruct (inst_run _ _ _ _); simpl; auto.
@@ -2158,29 +2186,88 @@ Variable Ge: genv.
 
 Local Hint Resolve trans_state_match: core.
 
+(* TODO remove ? *)
+Definition exit_cfi bb : option cf_instruction :=
+  match exit bb with
+  | Some (Pbuiltin _ _ _) => None
+  | Some (PCtlFlow c) => Some c
+  | None => None
+  end.
+
+Lemma bblock_simu_reduce_aux:
+  forall p1 p2,
+  L.bblock_simu Ge (trans_block p1) (trans_block p2) ->
+  Asmblockprops.bblock_simu_aux Ge.(_lk) Ge.(_genv) Ge.(_fn) p1 p2.
+Proof.
+  intros p1 p2 H0 rs m EBB.
+  generalize (H0 (trans_state (State rs m))); clear H0.
+  intro H0.
+  exploit (bisimu Ge rs m (trans_state (State rs m)) p1); eauto.
+  exploit (bisimu Ge rs m (trans_state (State rs m)) p2); eauto.
+  destruct (bbstep Ge.(_lk) Ge.(_genv) Ge.(_fn) p1 rs m); try (unfold Stuck in EBB; congruence).
+  intros H1 (s2' & exp2 & MS'). unfold exec in exp2, H1. rewrite exp2 in H0.
+  destruct H0 as (m2' & H0 & H2). discriminate. rewrite H0 in H1.
+  destruct (bbstep Ge.(_lk) Ge.(_genv) Ge.(_fn) p2 rs m); simpl in H1.
+  * unfold match_states in H1, MS'. destruct s, s0.
+    destruct H1 as (s' & H1 & H3 & H4). inv H1. inv MS'.
+    replace (_rs0) with (_rs).
+    - replace (_m0) with (_m); auto. congruence.
+    - apply functional_extensionality. intros r.
+      generalize (H1 r). intros Hr. congruence.
+  * discriminate.
+Qed.
+
 Lemma bblock_simu_reduce:
   forall p1 p2,
   L.bblock_simu Ge (trans_block p1) (trans_block p2) ->
   (has_builtin p1 = true -> exit p1 = exit p2) ->
   Asmblockprops.bblock_simu Ge.(_lk) Ge.(_genv) Ge.(_fn) p1 p2.
 Proof.
-  unfold bblock_simu. intros p1 p2 H BLT rs m rs' m' t EBB.
-  generalize (H (trans_state (State rs m))); clear H.
-  intro H. (* TODO How to define this correctly ?
-  exploit (bisimu rs m (body p1) (trans_state (State rs m))); eauto.
-  exploit (bisimu Ge rs m p2 ge fn (trans_state (State rs m))); eauto.
-  destruct (exec_bblock ge fn p1 rs m); try congruence.
-  intros H3 (s2' & exp2 & MS'). unfold exec in exp2, H3. rewrite exp2 in H2.
-  destruct H2 as (m2' & H2 & H4). discriminate. rewrite H2 in H3.
-  destruct (exec_bblock ge fn p2 rs m); simpl in H3.
-  * destruct H3 as (s' & H3 & H5 & H6). inv H3. inv MS'.
-    cutrewrite (rs0=rs1).
-    - cutrewrite (m0=m1); auto. congruence.
+  unfold bblock_simu. intros p1 p2 H0 BLT rs m EBB.
+  unfold exec_bblock.
+  generalize (H0 (trans_state (State rs m))); clear H0.
+  intros H0 m' t0 (rs1 & m1 & H1 & H2).
+  exploit (bisimu Ge rs m (trans_state (State rs m)) p1); eauto.
+  exploit (bisimu Ge rs m (trans_state (State rs m)) p2); eauto.
+  unfold bbstep, estep.
+  rewrite H1; simpl.
+  unfold has_builtin in BLT.
+  destruct (exit p1) eqn:EQEX1. destruct c.
+  - inversion H2; subst.
+    destruct (exec_body _ _ (body p2) _ _) as [[rs2 m2]|] eqn:EQBDY2; try congruence.
+    unfold trans_block, exec in *.
+    exploit (bisimu_body); eauto. erewrite H1. simpl.
+    (*destruct (exec_body _ _ (body p2) _ _) eqn:EQBDY1.*)
+  destruct (bbstep Ge.(_lk) Ge.(_genv) Ge.(_fn) p1 rs m); try (unfold Stuck in EBB; congruence).
+  intros H1 (s2' & exp2 & MS'). unfold exec in exp2, H1. rewrite exp2 in H0.
+  destruct H0 as (m2' & H0 & H2). discriminate. rewrite H0 in H1.
+  destruct (bbstep Ge.(_lk) Ge.(_genv) Ge.(_fn) p2 rs m); simpl in H1.
+  * unfold match_states in H1, MS'. destruct s, s0.
+    destruct H1 as (s' & H1 & H3 & H4). inv H1. inv MS'.
+    replace (_rs0) with (_rs).
+    - replace (_m0) with (_m); auto. congruence.
     - apply functional_extensionality. intros r.
-      generalize (H0 r). intros Hr. congruence.
+      generalize (H1 r). intros Hr. congruence.
   * discriminate.
-Qed.*)
-Admitted.
+
+
+  (*generalize (bblock_simu_reduce_aux p1 p2 H0).*)
+  (*unfold bblock_simu_aux. clear H0.*)
+  (*unfold exec_bblock, bbstep. intros H0 m' t0 (rs1 & m1 & H1 & H2).*)
+  (*generalize (H0 rs m); clear H0. rewrite H1. simpl. unfold estep.*)
+  (*inversion H2.*)
+  (*- intros H6. exploit (H6); try discriminate; clear H6.*)
+    (*destruct (exec_body _ _ (body p2) _ _) as [[rs2 m2]|]; try discriminate.*)
+    (*intros H6. eexists; eexists; split; try reflexivity.*)
+    (*destruct (exit p2) eqn:EQOC.*)
+    (*destruct (c).*)
+    (*+  econstructor; eauto.*)
+    (*+*)
+  (*generalize (H0 (trans_state (State rs m))); clear H0.*)
+  (*intro H0.*)
+
+  (*exploit (*)
+(*Qed.*)
 
 (** Used for debug traces *)
 
@@ -2550,17 +2637,17 @@ End SECT_BBLOCK_EQUIV.
 (** REWRITE RULES *)
 
 Definition is_constant (o: op): bool :=
-  match o with (* TODO *)
-  | OArithP _ | OArithRR0_XZR _ _ | Ofmovi_XZR _ => true
+  match o with
+  | OArithP _ | OArithRR0_XZR _ _ | Ofmovi_XZR _ | Loadsymbol _ | Constant _ | Obl _ | Obs _ => true
   | _ => false
   end.
 
 Lemma is_constant_correct ge o: is_constant o = true -> op_eval ge o [] <> None.
 Proof.
   destruct o; simpl in * |- *; try congruence.
-  destruct op0; simpl in * |- *; try congruence;
-  destruct n; simpl in * |- *; try congruence;
-  unfold arith_eval; destruct ge; simpl in * |- *; try congruence.
+  destruct op0; simpl in * |- *; try congruence.
+  destruct co; simpl in * |- *; try congruence;
+  unfold control_eval; destruct ge; simpl in * |- *; try congruence.
 Qed.
 
 Definition main_reduce (t: Terms.term):= RET (Terms.nofail is_constant t).