diff options
Diffstat (limited to 'mppa_k1c/abstractbb/DepExampleEqTest.v')
| -rw-r--r-- | mppa_k1c/abstractbb/DepExampleEqTest.v | 334 |
1 files changed, 0 insertions, 334 deletions
diff --git a/mppa_k1c/abstractbb/DepExampleEqTest.v b/mppa_k1c/abstractbb/DepExampleEqTest.v deleted file mode 100644 index a633ee07..00000000 --- a/mppa_k1c/abstractbb/DepExampleEqTest.v +++ /dev/null @@ -1,334 +0,0 @@ -(** Implementation of the example illustrating how to use ImpDep. *) - -Require Export DepExample. -Require Export Impure.ImpIO. -Export Notations. - -Require Import ImpDep. - -Open Scope impure. - -Module P<: ImpParam. - -Module R := Pos. - -Definition genv := unit. - -Section IMP. - -Inductive value_wrap := - | Std (v:value) (* value = DepExample.value *) - | Mem (m:mem) - . - -Inductive op_wrap := - (* constants *) - | Imm (i:Z) - (* arithmetic operation *) - | ARITH (op: arith_op) - | LOAD - | STORE - . - -Definition op_eval (ge: genv) (op: op_wrap) (l:list value_wrap): option value_wrap := - match op, l with - | Imm i, [] => Some (Std i) - | ARITH op, [Std v1; Std v2] => Some (Std (arith_op_eval op v1 v2)) - | LOAD, [Mem m; Std base; Std offset] => - match (Z.add base offset) with - | Zpos srce => Some (Std (m srce)) - | _ => None - end - | STORE, [Mem m; Std srce; Std base; Std offset] => - match (Z.add base offset) with - | Zpos dest => Some (Mem (assign m dest srce)) - | _ => None - end - | _, _ => None - end. - - -Definition value:=value_wrap. -Definition op:=op_wrap. - -Definition op_eq (o1 o2: op_wrap): ?? bool := - match o1, o2 with - | Imm i1, Imm i2 => phys_eq i1 i2 - | ARITH o1, ARITH o2 => phys_eq o1 o2 - | LOAD, LOAD => RET true - | STORE, STORE => RET true - | _, _ => RET false - end. - -Lemma op_eq_correct o1 o2: - WHEN op_eq o1 o2 ~> b THEN b=true -> o1 = o2. -Proof. - destruct o1, o2; wlp_simplify; congruence. -Qed. - -End IMP. -End P. - - -Module L <: ISeqLanguage with Module LP:=P. - -Module LP:=P. - -Include MkSeqLanguage P. - -End L. - - -Module IDT := ImpDepTree L ImpPosDict. - -Section SECT. -Variable ge: P.genv. - -(** Compilation from DepExample to L *) - -Definition the_mem: P.R.t := 1. -Definition reg_map (r: reg): P.R.t := Pos.succ r. - -Coercion L.Name: P.R.t >-> L.exp. - -Definition comp_op (o:operand): L.exp := - match o with - | Imm i => L.Op (P.Imm i) L.Enil - | Reg r => reg_map r - end. - -Definition comp_inst (i: inst): L.macro := - match i with - | MOVE dest src => - [ (reg_map dest, (comp_op src)) ] - | ARITH dest op src1 src2 => - [ (reg_map dest, L.Op (P.ARITH op) (L.Econs (comp_op src1) (L.Econs (comp_op src2) L.Enil))) ] - | LOAD dest base offset => - [ (reg_map dest, L.Op P.LOAD (L.Econs the_mem (L.Econs (reg_map base) (L.Econs (comp_op offset) L.Enil)))) ] - | STORE srce base offset => - [ (the_mem, L.Op P.STORE (L.Econs the_mem (L.Econs (reg_map srce) (L.Econs (reg_map base) (L.Econs (comp_op offset) L.Enil))))) ] - | MEMSWAP x base offset => - [ (reg_map x, L.Op P.LOAD (L.Econs the_mem (L.Econs (reg_map base) (L.Econs (comp_op offset) L.Enil)))); - (the_mem, L.Old (L.Op P.STORE (L.Econs the_mem (L.Econs (reg_map x) (L.Econs (reg_map base) (L.Econs (comp_op offset) L.Enil)))))) ] - end. - -Fixpoint comp_bblock (p: bblock): L.bblock := - match p with - | nil => nil - | i::p' => (comp_inst i)::(comp_bblock p') - end. - -(** Correctness proof of the compiler *) - -Lemma the_mem_separation: forall r, reg_map r <> the_mem. -Proof. - intros r; apply Pos.succ_not_1. -Qed. - -Lemma reg_map_separation: forall r1 r2, r1 <> r2 -> reg_map r1 <> reg_map r2. -Proof. - unfold reg_map; intros r1 r2 H1 H2; lapply (Pos.succ_inj r1 r2); auto. -Qed. - -Local Hint Resolve the_mem_separation reg_map_separation. - -Definition match_state (s: state) (m:L.mem): Prop := - m the_mem = P.Mem (sm s) /\ forall r, m (reg_map r) = P.Std (rm s r). - -Definition trans_state (s: state): L.mem := - fun x => - if Pos.eq_dec x the_mem - then P.Mem (sm s) - else P.Std (rm s (Pos.pred x)). - -Lemma match_trans_state (s:state): match_state s (trans_state s). -Proof. - unfold trans_state; constructor 1. - - destruct (Pos.eq_dec the_mem the_mem); try congruence. - - intros r; destruct (Pos.eq_dec (reg_map r) the_mem). - * generalize the_mem_separation; subst; congruence. - * unfold reg_map; rewrite Pos.pred_succ. auto. -Qed. - -Definition match_option_state (os: option state) (om:option L.mem): Prop := - match os with - | Some s => exists m, om = Some m /\ match_state s m - | None => om = None - end. - -Lemma comp_op_correct o s m old: match_state s m -> L.exp_eval ge (comp_op o) m old = Some (P.Std (operand_eval o (rm s))). -Proof. - destruct 1 as [H1 H2]; destruct o; simpl; auto. - rewrite H2; auto. -Qed. - -Lemma comp_bblock_correct_aux p: forall s m, match_state s m -> match_option_state (sem_bblock p s) (L.run ge (comp_bblock p) m). -Proof. - induction p as [| i p IHp]; simpl; eauto. - intros s m H; destruct i; simpl; erewrite !comp_op_correct; eauto; simpl. - - (* MOVE *) - apply IHp. - destruct H as [H1 H2]; constructor 1; simpl. - + rewrite L.assign_diff; auto. - + unfold assign; intros r; destruct (Pos.eq_dec dest r). - * subst; rewrite L.assign_eq; auto. - * rewrite L.assign_diff; auto. - - (* ARITH *) - apply IHp. - destruct H as [H1 H2]; constructor 1; simpl. - + rewrite L.assign_diff; auto. - + unfold assign; intros r; destruct (Pos.eq_dec dest r). - * subst; rewrite L.assign_eq; auto. - * rewrite L.assign_diff; auto. - - (* LOAD *) - destruct H as [H1 H2]. - rewrite H1, H2; simpl. - unfold get_addr. - destruct (rm s base + operand_eval offset (rm s))%Z; simpl; auto. - apply IHp. - constructor 1; simpl. - + rewrite L.assign_diff; auto. - + unfold assign; intros r; destruct (Pos.eq_dec dest r). - * subst; rewrite L.assign_eq; auto. - * rewrite L.assign_diff; auto. - - (* STORE *) - destruct H as [H1 H2]. - rewrite H1, !H2; simpl. - unfold get_addr. - destruct (rm s base + operand_eval offset (rm s))%Z; simpl; auto. - apply IHp. - constructor 1; simpl; auto. - + intros r; rewrite L.assign_diff; auto. - - (* MEMSWAP *) - destruct H as [H1 H2]. - rewrite H1, !H2; simpl. - unfold get_addr. - destruct (rm s base + operand_eval offset (rm s))%Z; simpl; auto. - apply IHp. - constructor 1; simpl; auto. - intros r0; rewrite L.assign_diff; auto. - unfold assign; destruct (Pos.eq_dec r r0). - * subst; rewrite L.assign_eq; auto. - * rewrite L.assign_diff; auto. -Qed. - -Lemma comp_bblock_correct p s: match_option_state (sem_bblock p s) (L.run ge (comp_bblock p) (trans_state s)). -Proof. - eapply comp_bblock_correct_aux. apply match_trans_state. -Qed. - -Lemma state_equiv_from_match (s1 s2: state) (m: L.mem) : - (match_state s1 m) -> (match_state s2 m) -> (state_equiv s1 s2). -Proof. - unfold state_equiv, match_state. intuition. - - congruence. - - assert (P.Std (rm s1 x) = P.Std (rm s2 x)); congruence. -Qed. - -Definition match_option_stateX (om:option L.mem) (os:option state): Prop := - match om with - | Some m => exists s, os = Some s /\ match_state s m - | None => os = None - end. - -Local Hint Resolve state_equiv_from_match. - -Lemma res_equiv_from_match (os1 os2: option state) (om: option L.mem): - (match_option_state os1 om) -> (match_option_stateX om os2) -> (res_equiv os1 os2). -Proof. - destruct os1 as [s1|]; simpl. - - intros [m [H1 H2]]; subst; simpl. - intros [s2 [H3 H4]]; subst; simpl. - eapply ex_intro; intuition eauto. - - intro; subst; simpl; auto. -Qed. - - -Lemma match_option_state_intro_X om os: match_option_state os om -> match_option_stateX om os. -Proof. - destruct os as [s | ]; simpl. - - intros [m [H1 H2]]. subst; simpl. eapply ex_intro; intuition eauto. - - intros; subst; simpl; auto. -Qed. - - -Lemma match_from_res_eq om1 om2 os: - L.res_eq om2 om1 -> match_option_stateX om1 os -> match_option_stateX om2 os. -Proof. - destruct om2 as [m2 | ]; simpl. - - intros [m [H1 H2]]. subst; simpl. - intros [s [H3 H4]]; subst; simpl. - eapply ex_intro; intuition eauto. - unfold match_state in * |- *. - intuition (rewrite H2; auto). - - intros; subst; simpl; auto. -Qed. - -Lemma bblock_equiv_reduce p1 p2: L.bblock_equiv ge (comp_bblock p1) (comp_bblock p2) -> bblock_equiv p1 p2. -Proof. - unfold L.bblock_equiv, bblock_equiv. - intros; eapply res_equiv_from_match. - apply comp_bblock_correct. - eapply match_from_res_eq. eauto. - apply match_option_state_intro_X. - apply comp_bblock_correct. -Qed. - - - - -(* NB: pretty-printing functions below only mandatory for IDT.verb_bblock_eq_test *) -Local Open Scope string_scope. - -Definition string_of_name (x: P.R.t): ?? pstring := - match x with - | xH => RET (Str ("the_mem")) - | _ as x => - DO s <~ string_of_Z (Zpos (Pos.pred x)) ;; - RET ("R" +; s) - end. - -Definition string_of_op (op: P.op): ?? pstring := - match op with - | P.Imm i => - DO s <~ string_of_Z i ;; - RET s - | P.ARITH ADD => RET (Str "ADD") - | P.ARITH SUB => RET (Str "SUB") - | P.ARITH MUL => RET (Str "MUL") - | P.LOAD => RET (Str "LOAD") - | P.STORE => RET (Str "STORE") - end. - -Definition bblock_eq_test (verb: bool) (p1 p2: bblock) : ?? bool := - if verb then - IDT.verb_bblock_eq_test string_of_name string_of_op ge (comp_bblock p1) (comp_bblock p2) - else - IDT.bblock_eq_test ge (comp_bblock p1) (comp_bblock p2). - -Local Hint Resolve IDT.bblock_eq_test_correct bblock_equiv_reduce IDT.verb_bblock_eq_test_correct: wlp. - - -Theorem bblock_eq_test_correct verb p1 p2 : - WHEN bblock_eq_test verb p1 p2 ~> b THEN b=true -> bblock_equiv p1 p2. -Proof. - wlp_simplify. -Qed. -Global Opaque bblock_eq_test. -Hint Resolve bblock_eq_test_correct: wlp. - -End SECT. -(* TEST: we can coerce this bblock_eq_test into a pure function (even if this is a little unsafe). *) -(* -Import UnsafeImpure. - -Definition pure_eq_test v (p1 p2: bblock) : bool := unsafe_coerce (bblock_eq_test v p1 p2). - -Theorem pure_eq_test_correct v p1 p2 : - pure_eq_test v p1 p2 = true -> bblock_equiv p1 p2. -Proof. - unfold pure_eq_test. intros; eapply bblock_eq_test_correct. - - apply unsafe_coerce_not_really_correct; eauto. - - eauto. -Qed. -*)
\ No newline at end of file |