From 3a43d16d95f8f64f78eadd0efe986cc96c396f4e Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Fri, 13 Nov 2020 17:02:17 +0100 Subject: Lemma for bisimu with potential builtins, alloc and constant --- aarch64/Asmblockdeps.v | 197 +++++++++++++++++++++++++++++++++---------------- 1 file changed, 132 insertions(+), 65 deletions(-) (limited to 'aarch64/Asmblockdeps.v') 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. -- cgit