From 89bc64204b4d99cb7dc9eacb1ecdf26b30dc26a0 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Thu, 2 Jul 2020 01:57:46 +0100 Subject: Fix spec by adding details about reg vals --- src/translation/HTLgenspec.v | 203 ++++++++++++++++++++++++++++++++++++++----- 1 file changed, 181 insertions(+), 22 deletions(-) (limited to 'src/translation/HTLgenspec.v') diff --git a/src/translation/HTLgenspec.v b/src/translation/HTLgenspec.v index 0cdecba..d2bd5af 100644 --- a/src/translation/HTLgenspec.v +++ b/src/translation/HTLgenspec.v @@ -19,6 +19,7 @@ From compcert Require RTL Op Maps Errors. From compcert Require Import Maps. From coqup Require Import Coquplib Verilog Value HTL HTLgen AssocMap. +Require Import Lia. Hint Resolve Maps.PTree.elements_keys_norepet : htlspec. Hint Resolve Maps.PTree.elements_correct : htlspec. @@ -161,16 +162,23 @@ Hint Constructors tr_code : htlspec. Inductive tr_module (f : RTL.function) : module -> Prop := tr_module_intro : forall data control fin rtrn st stk stk_len m start rst clk scldecls arrdecls, - (forall pc i, Maps.PTree.get pc f.(RTL.fn_code) = Some i -> - tr_code f.(RTL.fn_code) pc i data control fin rtrn st stk) -> - stk_len = Z.to_nat (f.(RTL.fn_stacksize) / 4) -> - Z.modulo (f.(RTL.fn_stacksize)) 4 = 0 -> - 0 <= f.(RTL.fn_stacksize) < Integers.Ptrofs.modulus -> m = (mkmodule f.(RTL.fn_params) data control f.(RTL.fn_entrypoint) st stk stk_len fin rtrn start rst clk scldecls arrdecls) -> + (forall pc i, Maps.PTree.get pc f.(RTL.fn_code) = Some i -> + tr_code f.(RTL.fn_code) pc i data control fin rtrn st stk) -> + stk_len = Z.to_nat (f.(RTL.fn_stacksize) / 4) -> + Z.modulo (f.(RTL.fn_stacksize)) 4 = 0 -> + 0 <= f.(RTL.fn_stacksize) < Integers.Ptrofs.modulus -> + st = ((RTL.max_reg_function f) + 1)%positive -> + fin = ((RTL.max_reg_function f) + 2)%positive -> + rtrn = ((RTL.max_reg_function f) + 3)%positive -> + stk = ((RTL.max_reg_function f) + 4)%positive -> + start = ((RTL.max_reg_function f) + 5)%positive -> + rst = ((RTL.max_reg_function f) + 6)%positive -> + clk = ((RTL.max_reg_function f) + 7)%positive -> tr_module f m. Hint Constructors tr_module : htlspec. @@ -202,6 +210,13 @@ Lemma declare_reg_controllogic_trans : Proof. intros. monadInv H. trivial. Qed. Hint Resolve create_reg_controllogic_trans : htlspec. +Lemma declare_reg_freshreg_trans : + forall sz s s' x i iop r, + declare_reg iop r sz s = OK x s' i -> + s.(st_freshreg) = s'.(st_freshreg). +Proof. inversion 1; auto. Qed. +Hint Resolve declare_reg_freshreg_trans : htlspec. + Lemma create_arr_datapath_trans : forall sz ln s s' x i iop, create_arr iop sz ln s = OK x s' i -> @@ -268,6 +283,16 @@ Proof. - apply H in EQ. rewrite EQ. eauto. Qed. +Lemma collect_freshreg_trans : + forall A f l cs cs' ci, + (forall s s' x i y, f y s = OK x s' i -> s.(st_freshreg) = s'.(st_freshreg)) -> + @HTLMonadExtra.collectlist A f l cs = OK tt cs' ci -> cs.(st_freshreg) = cs'.(st_freshreg). +Proof. + induction l; intros; monadInv H0. + - trivial. + - apply H in EQ. rewrite EQ. eauto. +Qed. + Lemma collect_declare_controllogic_trans : forall io n l s s' i, HTLMonadExtra.collectlist (fun r : reg => declare_reg io r n) l s = OK tt s' i -> @@ -286,6 +311,130 @@ Proof. intros. eapply declare_reg_datapath_trans. simpl in H0. eassumption. Qed. +Lemma collect_declare_freshreg_trans : + forall io n l s s' i, + HTLMonadExtra.collectlist (fun r : reg => declare_reg io r n) l s = OK tt s' i -> + s.(st_freshreg) = s'.(st_freshreg). +Proof. + intros. eapply collect_freshreg_trans; try eassumption. + inversion 1. auto. +Qed. + +Ltac unfold_match H := + match type of H with + | context[match ?g with _ => _ end] => destruct g eqn:?; try discriminate + end. + +Lemma translate_eff_addressing_freshreg_trans : + forall op args s r s' i, + translate_eff_addressing op args s = OK r s' i -> + s.(st_freshreg) = s'.(st_freshreg). +Proof. + destruct op; intros; simpl in *; repeat (unfold_match H); inv H; auto. +Qed. +Hint Resolve translate_eff_addressing_freshreg_trans : htlspec. + +Lemma translate_comparison_freshreg_trans : + forall op args s r s' i, + translate_comparison op args s = OK r s' i -> + s.(st_freshreg) = s'.(st_freshreg). +Proof. + destruct op; intros; simpl in *; repeat (unfold_match H); inv H; auto. +Qed. +Hint Resolve translate_comparison_freshreg_trans : htlspec. + +Lemma translate_comparison_imm_freshreg_trans : + forall op args s r s' i n, + translate_comparison_imm op args n s = OK r s' i -> + s.(st_freshreg) = s'.(st_freshreg). +Proof. + destruct op; intros; simpl in *; repeat (unfold_match H); inv H; auto. +Qed. +Hint Resolve translate_comparison_imm_freshreg_trans : htlspec. + +Lemma translate_condition_freshreg_trans : + forall op args s r s' i, + translate_condition op args s = OK r s' i -> + s.(st_freshreg) = s'.(st_freshreg). +Proof. + destruct op; intros; simpl in *; repeat (unfold_match H); inv H; eauto with htlspec. +Qed. +Hint Resolve translate_condition_freshreg_trans : htlspec. + +Lemma translate_instr_freshreg_trans : + forall op args s r s' i, + translate_instr op args s = OK r s' i -> + s.(st_freshreg) = s'.(st_freshreg). +Proof. + destruct op; intros; simpl in *; repeat (unfold_match H); inv H; eauto with htlspec. + monadInv H1. eauto with htlspec. +Qed. +Hint Resolve translate_instr_freshreg_trans : htlspec. + +Lemma translate_arr_access_freshreg_trans : + forall mem addr args st s r s' i, + translate_arr_access mem addr args st s = OK r s' i -> + s.(st_freshreg) = s'.(st_freshreg). +Proof. + intros. unfold translate_arr_access in H. repeat (unfold_match H); inv H; eauto with htlspec. +Qed. +Hint Resolve translate_arr_access_freshreg_trans : htlspec. + +Lemma add_instr_freshreg_trans : + forall n n' st s r s' i, + add_instr n n' st s = OK r s' i -> + s.(st_freshreg) = s'.(st_freshreg). +Proof. intros. unfold add_instr in H. repeat (unfold_match H). inv H. auto. Qed. +Hint Resolve add_instr_freshreg_trans : htlspec. + +Lemma add_branch_instr_freshreg_trans : + forall n n0 n1 e s r s' i, + add_branch_instr e n n0 n1 s = OK r s' i -> + s.(st_freshreg) = s'.(st_freshreg). +Proof. intros. unfold add_branch_instr in H. repeat (unfold_match H). inv H. auto. Qed. +Hint Resolve add_branch_instr_freshreg_trans : htlspec. + +Lemma add_node_skip_freshreg_trans : + forall n1 n2 s r s' i, + add_node_skip n1 n2 s = OK r s' i -> + s.(st_freshreg) = s'.(st_freshreg). +Proof. intros. unfold add_node_skip in H. repeat (unfold_match H). inv H. auto. Qed. +Hint Resolve add_node_skip_freshreg_trans : htlspec. + +Lemma add_instr_skip_freshreg_trans : + forall n1 n2 s r s' i, + add_instr_skip n1 n2 s = OK r s' i -> + s.(st_freshreg) = s'.(st_freshreg). +Proof. intros. unfold add_instr_skip in H. repeat (unfold_match H). inv H. auto. Qed. +Hint Resolve add_instr_skip_freshreg_trans : htlspec. + +Lemma transf_instr_freshreg_trans : + forall fin ret st instr s v s' i, + transf_instr fin ret st instr s = OK v s' i -> + s.(st_freshreg) = s'.(st_freshreg). +Proof. + intros. destruct instr eqn:?. subst. unfold transf_instr in H. + destruct i0; try (monadInv H); try (unfold_match H); eauto with htlspec. + - apply add_instr_freshreg_trans in EQ2. apply translate_instr_freshreg_trans in EQ. + apply declare_reg_freshreg_trans in EQ1. congruence. + - apply add_instr_freshreg_trans in EQ2. apply translate_arr_access_freshreg_trans in EQ. + apply declare_reg_freshreg_trans in EQ1. congruence. + - apply add_instr_freshreg_trans in EQ0. apply translate_arr_access_freshreg_trans in EQ. congruence. + - apply translate_condition_freshreg_trans in EQ. apply add_branch_instr_freshreg_trans in EQ0. + congruence. + - inv EQ. apply add_node_skip_freshreg_trans in EQ0. congruence. +Qed. +Hint Resolve transf_instr_freshreg_trans : htlspec. + +Lemma collect_trans_instr_freshreg_trans : + forall fin ret st l s s' i, + HTLMonadExtra.collectlist (transf_instr fin ret st) l s = OK tt s' i -> + s.(st_freshreg) = s'.(st_freshreg). +Proof. + intros. eapply collect_freshreg_trans; try eassumption. + eauto with htlspec. +Qed. + Ltac rewrite_states := match goal with | [ H: ?x ?s = ?x ?s' |- _ ] => @@ -294,11 +443,6 @@ Ltac rewrite_states := remember (?x ?s) as c1; remember (?x ?s') as c2; try subst end. -Ltac unfold_match H := - match type of H with - | context[match ?g with _ => _ end] => destruct g eqn:?; try discriminate - end. - Ltac inv_add_instr' H := match type of H with | ?f _ _ _ = OK _ _ _ => unfold f in H @@ -405,9 +549,17 @@ Qed. Hint Resolve iter_expand_instr_spec : htlspec. Lemma create_arr_inv : forall w x y z a b c d, - create_arr w x y z = OK (a, b) c d -> y = b. + create_arr w x y z = OK (a, b) c d -> + y = b /\ a = z.(st_freshreg) /\ c.(st_freshreg) = Pos.succ (z.(st_freshreg)). +Proof. + inversion 1; split; auto. +Qed. + +Lemma create_reg_inv : forall a b s r s' i, + create_reg a b s = OK r s' i -> + r = s.(st_freshreg) /\ s'.(st_freshreg) = Pos.succ (s.(st_freshreg)). Proof. - inversion 1. reflexivity. + inversion 1; auto. Qed. Theorem transl_module_correct : @@ -430,20 +582,27 @@ Proof. monadInv Heqr. (* TODO: We should be able to fold this into the automation. *) - pose proof (create_arr_inv _ _ _ _ _ _ _ _ EQ0) as STK_LEN. - rewrite <- STK_LEN. - - econstructor; simpl; auto. - intros. + pose proof (create_arr_inv _ _ _ _ _ _ _ _ EQ0) as STK_LEN. inv STK_LEN. inv H5. + pose proof (create_reg_inv _ _ _ _ _ _ EQ) as FIN_VAL. inv FIN_VAL. + pose proof (create_reg_inv _ _ _ _ _ _ EQ1) as RET_VAL. inv RET_VAL. + destruct x3. destruct x4. + pose proof (collect_trans_instr_freshreg_trans _ _ _ _ _ _ _ EQ2) as TR_INSTR. + pose proof (collect_declare_freshreg_trans _ _ _ _ _ _ EQ3) as TR_DEC. + pose proof (create_reg_inv _ _ _ _ _ _ EQ4) as START_VAL. inv START_VAL. + pose proof (create_reg_inv _ _ _ _ _ _ EQ5) as RESET_VAL. inv RESET_VAL. + pose proof (create_reg_inv _ _ _ _ _ _ EQ6) as CLK_VAL. inv CLK_VAL. + simpl. + rewrite H9 in *. rewrite H8 in *. replace (st_freshreg s4) with (st_freshreg s2) in * by congruence. + rewrite H6 in *. rewrite H7 in *. rewrite H5 in *. simpl in *. inv_incr. + econstructor; simpl; auto; try lia. + intros. assert (EQ3D := EQ3). - destruct x4. apply collect_declare_datapath_trans in EQ3. apply collect_declare_controllogic_trans in EQ3D. - assert (STC: st_controllogic s10 = st_controllogic s3) by congruence. - assert (STD: st_datapath s10 = st_datapath s3) by congruence. - assert (STST: st_st s10 = st_st s3) by congruence. - rewrite STC. rewrite STD. rewrite STST. + replace (st_controllogic s10) with (st_controllogic s3) by congruence. + replace (st_datapath s10) with (st_datapath s3) by congruence. + replace (st_st s10) with (st_st s3) by congruence. eapply iter_expand_instr_spec; eauto with htlspec. apply PTree.elements_complete. Qed. -- cgit From 594c2825012d94675317f51cf6a3e97c2f88cd02 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Fri, 3 Jul 2020 21:05:45 +0100 Subject: Fixing HTLgenproof --- src/translation/HTLgenspec.v | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'src/translation/HTLgenspec.v') diff --git a/src/translation/HTLgenspec.v b/src/translation/HTLgenspec.v index d2bd5af..799b198 100644 --- a/src/translation/HTLgenspec.v +++ b/src/translation/HTLgenspec.v @@ -18,7 +18,7 @@ From compcert Require RTL Op Maps Errors. From compcert Require Import Maps. -From coqup Require Import Coquplib Verilog Value HTL HTLgen AssocMap. +From coqup Require Import Coquplib Verilog ValueInt HTL HTLgen AssocMap. Require Import Lia. Hint Resolve Maps.PTree.elements_keys_norepet : htlspec. @@ -127,12 +127,12 @@ Inductive tr_instr (fin rtrn st stk : reg) : RTL.instruction -> stmnt -> stmnt - translate_condition cond args s = OK c s' i -> tr_instr fin rtrn st stk (RTL.Icond cond args n1 n2) Vskip (state_cond st c n1 n2) | tr_instr_Ireturn_None : - tr_instr fin rtrn st stk (RTL.Ireturn None) (Vseq (block fin (Vlit (ZToValue 1%nat 1%Z))) - (block rtrn (Vlit (ZToValue 1%nat 0%Z)))) Vskip + tr_instr fin rtrn st stk (RTL.Ireturn None) (Vseq (block fin (Vlit (ZToValue 1%Z))) + (block rtrn (Vlit (ZToValue 0%Z)))) Vskip | tr_instr_Ireturn_Some : forall r, tr_instr fin rtrn st stk (RTL.Ireturn (Some r)) - (Vseq (block fin (Vlit (ZToValue 1%nat 1%Z))) (block rtrn (Vvar r))) Vskip + (Vseq (block fin (Vlit (ZToValue 1%Z))) (block rtrn (Vvar r))) Vskip | tr_instr_Iload : forall mem addr args s s' i c dst n, translate_arr_access mem addr args stk s = OK c s' i -> -- cgit From e3b7213e552d601094d784042cc502cd518d3125 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Sun, 5 Jul 2020 13:50:22 +0100 Subject: Fix HTLgenspec --- src/translation/HTLgenspec.v | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) (limited to 'src/translation/HTLgenspec.v') diff --git a/src/translation/HTLgenspec.v b/src/translation/HTLgenspec.v index 799b198..a9626c4 100644 --- a/src/translation/HTLgenspec.v +++ b/src/translation/HTLgenspec.v @@ -161,12 +161,12 @@ Hint Constructors tr_code : htlspec. Inductive tr_module (f : RTL.function) : module -> Prop := tr_module_intro : - forall data control fin rtrn st stk stk_len m start rst clk scldecls arrdecls, + forall data control fin rtrn st stk stk_len m start rst clk scldecls arrdecls wf, m = (mkmodule f.(RTL.fn_params) data control f.(RTL.fn_entrypoint) - st stk stk_len fin rtrn start rst clk scldecls arrdecls) -> + st stk stk_len fin rtrn start rst clk scldecls arrdecls wf) -> (forall pc i, Maps.PTree.get pc f.(RTL.fn_code) = Some i -> tr_code f.(RTL.fn_code) pc i data control fin rtrn st stk) -> stk_len = Z.to_nat (f.(RTL.fn_stacksize) / 4) -> @@ -581,6 +581,8 @@ Proof. crush; monadInv Heqr. + repeat unfold_match EQ9. monadInv EQ9. + (* TODO: We should be able to fold this into the automation. *) pose proof (create_arr_inv _ _ _ _ _ _ _ _ EQ0) as STK_LEN. inv STK_LEN. inv H5. pose proof (create_reg_inv _ _ _ _ _ _ EQ) as FIN_VAL. inv FIN_VAL. @@ -591,7 +593,6 @@ Proof. pose proof (create_reg_inv _ _ _ _ _ _ EQ4) as START_VAL. inv START_VAL. pose proof (create_reg_inv _ _ _ _ _ _ EQ5) as RESET_VAL. inv RESET_VAL. pose proof (create_reg_inv _ _ _ _ _ _ EQ6) as CLK_VAL. inv CLK_VAL. - simpl. rewrite H9 in *. rewrite H8 in *. replace (st_freshreg s4) with (st_freshreg s2) in * by congruence. rewrite H6 in *. rewrite H7 in *. rewrite H5 in *. simpl in *. inv_incr. -- cgit From c76ac9be323e3513aa0db2721ecd0f6c3987aef0 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Sun, 5 Jul 2020 18:45:14 +0100 Subject: Fix Inop --- src/translation/HTLgenspec.v | 30 ++++++++++++++++++++++-------- 1 file changed, 22 insertions(+), 8 deletions(-) (limited to 'src/translation/HTLgenspec.v') diff --git a/src/translation/HTLgenspec.v b/src/translation/HTLgenspec.v index a9626c4..f0508bd 100644 --- a/src/translation/HTLgenspec.v +++ b/src/translation/HTLgenspec.v @@ -17,7 +17,7 @@ *) From compcert Require RTL Op Maps Errors. -From compcert Require Import Maps. +From compcert Require Import Maps Integers. From coqup Require Import Coquplib Verilog ValueInt HTL HTLgen AssocMap. Require Import Lia. @@ -117,13 +117,17 @@ translations for each of the elements *) Inductive tr_instr (fin rtrn st stk : reg) : RTL.instruction -> stmnt -> stmnt -> Prop := | tr_instr_Inop : forall n, + Z.pos n <= Int.max_unsigned -> tr_instr fin rtrn st stk (RTL.Inop n) Vskip (state_goto st n) | tr_instr_Iop : forall n op args dst s s' e i, + Z.pos n <= Int.max_unsigned -> translate_instr op args s = OK e s' i -> tr_instr fin rtrn st stk (RTL.Iop op args dst n) (Vnonblock (Vvar dst) e) (state_goto st n) | tr_instr_Icond : forall n1 n2 cond args s s' i c, + Z.pos n1 <= Int.max_unsigned -> + Z.pos n2 <= Int.max_unsigned -> translate_condition cond args s = OK c s' i -> tr_instr fin rtrn st stk (RTL.Icond cond args n1 n2) Vskip (state_cond st c n1 n2) | tr_instr_Ireturn_None : @@ -135,10 +139,12 @@ Inductive tr_instr (fin rtrn st stk : reg) : RTL.instruction -> stmnt -> stmnt - (Vseq (block fin (Vlit (ZToValue 1%Z))) (block rtrn (Vvar r))) Vskip | tr_instr_Iload : forall mem addr args s s' i c dst n, + Z.pos n <= Int.max_unsigned -> translate_arr_access mem addr args stk s = OK c s' i -> tr_instr fin rtrn st stk (RTL.Iload mem addr args dst n) (nonblock dst c) (state_goto st n) | tr_instr_Istore : forall mem addr args s s' i c src n, + Z.pos n <= Int.max_unsigned -> translate_arr_access mem addr args stk s = OK c s' i -> tr_instr fin rtrn st stk (RTL.Istore mem addr args src n) (Vnonblock c (Vvar src)) (state_goto st n) @@ -415,12 +421,12 @@ Lemma transf_instr_freshreg_trans : Proof. intros. destruct instr eqn:?. subst. unfold transf_instr in H. destruct i0; try (monadInv H); try (unfold_match H); eauto with htlspec. - - apply add_instr_freshreg_trans in EQ2. apply translate_instr_freshreg_trans in EQ. + - monadInv H. apply add_instr_freshreg_trans in EQ2. apply translate_instr_freshreg_trans in EQ. apply declare_reg_freshreg_trans in EQ1. congruence. - - apply add_instr_freshreg_trans in EQ2. apply translate_arr_access_freshreg_trans in EQ. + - monadInv H. apply add_instr_freshreg_trans in EQ2. apply translate_arr_access_freshreg_trans in EQ. apply declare_reg_freshreg_trans in EQ1. congruence. - - apply add_instr_freshreg_trans in EQ0. apply translate_arr_access_freshreg_trans in EQ. congruence. - - apply translate_condition_freshreg_trans in EQ. apply add_branch_instr_freshreg_trans in EQ0. + - monadInv H. apply add_instr_freshreg_trans in EQ0. apply translate_arr_access_freshreg_trans in EQ. congruence. + - monadInv H. apply translate_condition_freshreg_trans in EQ. apply add_branch_instr_freshreg_trans in EQ0. congruence. - inv EQ. apply add_node_skip_freshreg_trans in EQ0. congruence. Qed. @@ -445,13 +451,16 @@ Ltac rewrite_states := Ltac inv_add_instr' H := match type of H with + | ?f _ _ = OK _ _ _ => unfold f in H | ?f _ _ _ = OK _ _ _ => unfold f in H | ?f _ _ _ _ = OK _ _ _ => unfold f in H | ?f _ _ _ _ _ = OK _ _ _ => unfold f in H + | ?f _ _ _ _ _ _ = OK _ _ _ => unfold f in H end; repeat unfold_match H; inversion H. Ltac inv_add_instr := - lazymatch goal with + match goal with + | H: (if ?c then _ else _) _ = OK _ _ _ |- _ => destruct c eqn:EQN; try discriminate; inv_add_instr | H: context[add_instr_skip _ _ _] |- _ => inv_add_instr' H | H: context[add_instr_skip _ _] |- _ => @@ -491,23 +500,27 @@ Proof. + destruct o with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. + destruct o0 with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. + inversion H2. inversion H9. rewrite H. apply tr_instr_Inop. + apply Z.leb_le. assumption. eapply in_map with (f := fst) in H9. contradiction. + destruct o with pc1; destruct H16; simpl in *; rewrite AssocMap.gss in H14; eauto; congruence. + destruct o0 with pc1; destruct H16; simpl in *; rewrite AssocMap.gss in H14; eauto; congruence. + inversion H2. inversion H14. unfold nonblock. replace (st_st s4) with (st_st s2) by congruence. - econstructor. apply EQ1. eapply in_map with (f := fst) in H14. contradiction. + econstructor. apply Z.leb_le; assumption. + apply EQ1. eapply in_map with (f := fst) in H14. contradiction. + destruct o with pc1; destruct H16; simpl in *; rewrite AssocMap.gss in H14; eauto; congruence. + destruct o0 with pc1; destruct H16; simpl in *; rewrite AssocMap.gss in H14; eauto; congruence. + inversion H2. inversion H14. rewrite <- e2. replace (st_st s2) with (st_st s0) by congruence. - econstructor. apply EQ1. eapply in_map with (f := fst) in H14. contradiction. + econstructor. apply Z.leb_le; assumption. + apply EQ1. eapply in_map with (f := fst) in H14. contradiction. + destruct o with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. + destruct o0 with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. + destruct H2. * inversion H2. replace (st_st s2) with (st_st s0) by congruence. + econstructor. apply Z.leb_le; assumption. eauto with htlspec. * apply in_map with (f := fst) in H2. contradiction. @@ -516,6 +529,7 @@ Proof. + destruct H2. * inversion H2. replace (st_st s2) with (st_st s0) by congruence. + econstructor; try (apply Z.leb_le; apply andb_prop in EQN; apply EQN). eauto with htlspec. * apply in_map with (f := fst) in H2. contradiction. -- cgit From ec97745e4675b72cbabd2a3bd12d6efdd8bfa6d6 Mon Sep 17 00:00:00 2001 From: James Pollard Date: Mon, 6 Jul 2020 15:33:04 +0100 Subject: Implemented algorithm for new byte-addressed stack. --- src/translation/HTLgenspec.v | 918 +++++++++++++++++++++---------------------- 1 file changed, 459 insertions(+), 459 deletions(-) (limited to 'src/translation/HTLgenspec.v') diff --git a/src/translation/HTLgenspec.v b/src/translation/HTLgenspec.v index a9626c4..4662cf4 100644 --- a/src/translation/HTLgenspec.v +++ b/src/translation/HTLgenspec.v @@ -148,462 +148,462 @@ Inductive tr_instr (fin rtrn st stk : reg) : RTL.instruction -> stmnt -> stmnt - tr_instr fin rtrn st stk (RTL.Ijumptable r tbl) (Vskip) (Vcase (Vvar r) cexpr (Some Vskip)). Hint Constructors tr_instr : htlspec. -Inductive tr_code (c : RTL.code) (pc : RTL.node) (i : RTL.instruction) (stmnts trans : PTree.t stmnt) - (fin rtrn st stk : reg) : Prop := - tr_code_intro : - forall s t, - c!pc = Some i -> - stmnts!pc = Some s -> - trans!pc = Some t -> - tr_instr fin rtrn st stk i s t -> - tr_code c pc i stmnts trans fin rtrn st stk. -Hint Constructors tr_code : htlspec. - -Inductive tr_module (f : RTL.function) : module -> Prop := - tr_module_intro : - forall data control fin rtrn st stk stk_len m start rst clk scldecls arrdecls wf, - m = (mkmodule f.(RTL.fn_params) - data - control - f.(RTL.fn_entrypoint) - st stk stk_len fin rtrn start rst clk scldecls arrdecls wf) -> - (forall pc i, Maps.PTree.get pc f.(RTL.fn_code) = Some i -> - tr_code f.(RTL.fn_code) pc i data control fin rtrn st stk) -> - stk_len = Z.to_nat (f.(RTL.fn_stacksize) / 4) -> - Z.modulo (f.(RTL.fn_stacksize)) 4 = 0 -> - 0 <= f.(RTL.fn_stacksize) < Integers.Ptrofs.modulus -> - st = ((RTL.max_reg_function f) + 1)%positive -> - fin = ((RTL.max_reg_function f) + 2)%positive -> - rtrn = ((RTL.max_reg_function f) + 3)%positive -> - stk = ((RTL.max_reg_function f) + 4)%positive -> - start = ((RTL.max_reg_function f) + 5)%positive -> - rst = ((RTL.max_reg_function f) + 6)%positive -> - clk = ((RTL.max_reg_function f) + 7)%positive -> - tr_module f m. -Hint Constructors tr_module : htlspec. - -Lemma create_reg_datapath_trans : - forall sz s s' x i iop, - create_reg iop sz s = OK x s' i -> - s.(st_datapath) = s'.(st_datapath). -Proof. intros. monadInv H. trivial. Qed. -Hint Resolve create_reg_datapath_trans : htlspec. - -Lemma create_reg_controllogic_trans : - forall sz s s' x i iop, - create_reg iop sz s = OK x s' i -> - s.(st_controllogic) = s'.(st_controllogic). -Proof. intros. monadInv H. trivial. Qed. -Hint Resolve create_reg_controllogic_trans : htlspec. - -Lemma declare_reg_datapath_trans : - forall sz s s' x i iop r, - declare_reg iop r sz s = OK x s' i -> - s.(st_datapath) = s'.(st_datapath). -Proof. intros. monadInv H. trivial. Qed. -Hint Resolve create_reg_datapath_trans : htlspec. - -Lemma declare_reg_controllogic_trans : - forall sz s s' x i iop r, - declare_reg iop r sz s = OK x s' i -> - s.(st_controllogic) = s'.(st_controllogic). -Proof. intros. monadInv H. trivial. Qed. -Hint Resolve create_reg_controllogic_trans : htlspec. - -Lemma declare_reg_freshreg_trans : - forall sz s s' x i iop r, - declare_reg iop r sz s = OK x s' i -> - s.(st_freshreg) = s'.(st_freshreg). -Proof. inversion 1; auto. Qed. -Hint Resolve declare_reg_freshreg_trans : htlspec. - -Lemma create_arr_datapath_trans : - forall sz ln s s' x i iop, - create_arr iop sz ln s = OK x s' i -> - s.(st_datapath) = s'.(st_datapath). -Proof. intros. monadInv H. trivial. Qed. -Hint Resolve create_arr_datapath_trans : htlspec. - -Lemma create_arr_controllogic_trans : - forall sz ln s s' x i iop, - create_arr iop sz ln s = OK x s' i -> - s.(st_controllogic) = s'.(st_controllogic). -Proof. intros. monadInv H. trivial. Qed. -Hint Resolve create_arr_controllogic_trans : htlspec. - -Lemma get_refl_x : - forall s s' x i, - get s = OK x s' i -> - s = x. -Proof. inversion 1. trivial. Qed. -Hint Resolve get_refl_x : htlspec. - -Lemma get_refl_s : - forall s s' x i, - get s = OK x s' i -> - s = s'. -Proof. inversion 1. trivial. Qed. -Hint Resolve get_refl_s : htlspec. - -Ltac inv_incr := - repeat match goal with - | [ H: create_reg _ _ ?s = OK _ ?s' _ |- _ ] => - let H1 := fresh "H" in - assert (H1 := H); eapply create_reg_datapath_trans in H; - eapply create_reg_controllogic_trans in H1 - | [ H: create_arr _ _ _ ?s = OK _ ?s' _ |- _ ] => - let H1 := fresh "H" in - assert (H1 := H); eapply create_arr_datapath_trans in H; - eapply create_arr_controllogic_trans in H1 - | [ H: get ?s = OK _ _ _ |- _ ] => - let H1 := fresh "H" in - assert (H1 := H); apply get_refl_x in H; apply get_refl_s in H1; - subst - | [ H: st_prop _ _ |- _ ] => unfold st_prop in H; destruct H - | [ H: st_incr _ _ |- _ ] => destruct st_incr - end. - -Lemma collect_controllogic_trans : - forall A f l cs cs' ci, - (forall s s' x i y, f y s = OK x s' i -> s.(st_controllogic) = s'.(st_controllogic)) -> - @HTLMonadExtra.collectlist A f l cs = OK tt cs' ci -> cs.(st_controllogic) = cs'.(st_controllogic). -Proof. - induction l; intros; monadInv H0. - - trivial. - - apply H in EQ. rewrite EQ. eauto. -Qed. - -Lemma collect_datapath_trans : - forall A f l cs cs' ci, - (forall s s' x i y, f y s = OK x s' i -> s.(st_datapath) = s'.(st_datapath)) -> - @HTLMonadExtra.collectlist A f l cs = OK tt cs' ci -> cs.(st_datapath) = cs'.(st_datapath). -Proof. - induction l; intros; monadInv H0. - - trivial. - - apply H in EQ. rewrite EQ. eauto. -Qed. - -Lemma collect_freshreg_trans : - forall A f l cs cs' ci, - (forall s s' x i y, f y s = OK x s' i -> s.(st_freshreg) = s'.(st_freshreg)) -> - @HTLMonadExtra.collectlist A f l cs = OK tt cs' ci -> cs.(st_freshreg) = cs'.(st_freshreg). -Proof. - induction l; intros; monadInv H0. - - trivial. - - apply H in EQ. rewrite EQ. eauto. -Qed. - -Lemma collect_declare_controllogic_trans : - forall io n l s s' i, - HTLMonadExtra.collectlist (fun r : reg => declare_reg io r n) l s = OK tt s' i -> - s.(st_controllogic) = s'.(st_controllogic). -Proof. - intros. eapply collect_controllogic_trans; try eassumption. - intros. eapply declare_reg_controllogic_trans. simpl in H0. eassumption. -Qed. - -Lemma collect_declare_datapath_trans : - forall io n l s s' i, - HTLMonadExtra.collectlist (fun r : reg => declare_reg io r n) l s = OK tt s' i -> - s.(st_datapath) = s'.(st_datapath). -Proof. - intros. eapply collect_datapath_trans; try eassumption. - intros. eapply declare_reg_datapath_trans. simpl in H0. eassumption. -Qed. - -Lemma collect_declare_freshreg_trans : - forall io n l s s' i, - HTLMonadExtra.collectlist (fun r : reg => declare_reg io r n) l s = OK tt s' i -> - s.(st_freshreg) = s'.(st_freshreg). -Proof. - intros. eapply collect_freshreg_trans; try eassumption. - inversion 1. auto. -Qed. - -Ltac unfold_match H := - match type of H with - | context[match ?g with _ => _ end] => destruct g eqn:?; try discriminate - end. - -Lemma translate_eff_addressing_freshreg_trans : - forall op args s r s' i, - translate_eff_addressing op args s = OK r s' i -> - s.(st_freshreg) = s'.(st_freshreg). -Proof. - destruct op; intros; simpl in *; repeat (unfold_match H); inv H; auto. -Qed. -Hint Resolve translate_eff_addressing_freshreg_trans : htlspec. - -Lemma translate_comparison_freshreg_trans : - forall op args s r s' i, - translate_comparison op args s = OK r s' i -> - s.(st_freshreg) = s'.(st_freshreg). -Proof. - destruct op; intros; simpl in *; repeat (unfold_match H); inv H; auto. -Qed. -Hint Resolve translate_comparison_freshreg_trans : htlspec. - -Lemma translate_comparison_imm_freshreg_trans : - forall op args s r s' i n, - translate_comparison_imm op args n s = OK r s' i -> - s.(st_freshreg) = s'.(st_freshreg). -Proof. - destruct op; intros; simpl in *; repeat (unfold_match H); inv H; auto. -Qed. -Hint Resolve translate_comparison_imm_freshreg_trans : htlspec. - -Lemma translate_condition_freshreg_trans : - forall op args s r s' i, - translate_condition op args s = OK r s' i -> - s.(st_freshreg) = s'.(st_freshreg). -Proof. - destruct op; intros; simpl in *; repeat (unfold_match H); inv H; eauto with htlspec. -Qed. -Hint Resolve translate_condition_freshreg_trans : htlspec. - -Lemma translate_instr_freshreg_trans : - forall op args s r s' i, - translate_instr op args s = OK r s' i -> - s.(st_freshreg) = s'.(st_freshreg). -Proof. - destruct op; intros; simpl in *; repeat (unfold_match H); inv H; eauto with htlspec. - monadInv H1. eauto with htlspec. -Qed. -Hint Resolve translate_instr_freshreg_trans : htlspec. - -Lemma translate_arr_access_freshreg_trans : - forall mem addr args st s r s' i, - translate_arr_access mem addr args st s = OK r s' i -> - s.(st_freshreg) = s'.(st_freshreg). -Proof. - intros. unfold translate_arr_access in H. repeat (unfold_match H); inv H; eauto with htlspec. -Qed. -Hint Resolve translate_arr_access_freshreg_trans : htlspec. - -Lemma add_instr_freshreg_trans : - forall n n' st s r s' i, - add_instr n n' st s = OK r s' i -> - s.(st_freshreg) = s'.(st_freshreg). -Proof. intros. unfold add_instr in H. repeat (unfold_match H). inv H. auto. Qed. -Hint Resolve add_instr_freshreg_trans : htlspec. - -Lemma add_branch_instr_freshreg_trans : - forall n n0 n1 e s r s' i, - add_branch_instr e n n0 n1 s = OK r s' i -> - s.(st_freshreg) = s'.(st_freshreg). -Proof. intros. unfold add_branch_instr in H. repeat (unfold_match H). inv H. auto. Qed. -Hint Resolve add_branch_instr_freshreg_trans : htlspec. - -Lemma add_node_skip_freshreg_trans : - forall n1 n2 s r s' i, - add_node_skip n1 n2 s = OK r s' i -> - s.(st_freshreg) = s'.(st_freshreg). -Proof. intros. unfold add_node_skip in H. repeat (unfold_match H). inv H. auto. Qed. -Hint Resolve add_node_skip_freshreg_trans : htlspec. - -Lemma add_instr_skip_freshreg_trans : - forall n1 n2 s r s' i, - add_instr_skip n1 n2 s = OK r s' i -> - s.(st_freshreg) = s'.(st_freshreg). -Proof. intros. unfold add_instr_skip in H. repeat (unfold_match H). inv H. auto. Qed. -Hint Resolve add_instr_skip_freshreg_trans : htlspec. - -Lemma transf_instr_freshreg_trans : - forall fin ret st instr s v s' i, - transf_instr fin ret st instr s = OK v s' i -> - s.(st_freshreg) = s'.(st_freshreg). -Proof. - intros. destruct instr eqn:?. subst. unfold transf_instr in H. - destruct i0; try (monadInv H); try (unfold_match H); eauto with htlspec. - - apply add_instr_freshreg_trans in EQ2. apply translate_instr_freshreg_trans in EQ. - apply declare_reg_freshreg_trans in EQ1. congruence. - - apply add_instr_freshreg_trans in EQ2. apply translate_arr_access_freshreg_trans in EQ. - apply declare_reg_freshreg_trans in EQ1. congruence. - - apply add_instr_freshreg_trans in EQ0. apply translate_arr_access_freshreg_trans in EQ. congruence. - - apply translate_condition_freshreg_trans in EQ. apply add_branch_instr_freshreg_trans in EQ0. - congruence. - - inv EQ. apply add_node_skip_freshreg_trans in EQ0. congruence. -Qed. -Hint Resolve transf_instr_freshreg_trans : htlspec. - -Lemma collect_trans_instr_freshreg_trans : - forall fin ret st l s s' i, - HTLMonadExtra.collectlist (transf_instr fin ret st) l s = OK tt s' i -> - s.(st_freshreg) = s'.(st_freshreg). -Proof. - intros. eapply collect_freshreg_trans; try eassumption. - eauto with htlspec. -Qed. - -Ltac rewrite_states := - match goal with - | [ H: ?x ?s = ?x ?s' |- _ ] => - let c1 := fresh "c" in - let c2 := fresh "c" in - remember (?x ?s) as c1; remember (?x ?s') as c2; try subst - end. - -Ltac inv_add_instr' H := - match type of H with - | ?f _ _ _ = OK _ _ _ => unfold f in H - | ?f _ _ _ _ = OK _ _ _ => unfold f in H - | ?f _ _ _ _ _ = OK _ _ _ => unfold f in H - end; repeat unfold_match H; inversion H. - -Ltac inv_add_instr := - lazymatch goal with - | H: context[add_instr_skip _ _ _] |- _ => - inv_add_instr' H - | H: context[add_instr_skip _ _] |- _ => - monadInv H; inv_incr; inv_add_instr - | H: context[add_instr _ _ _ _] |- _ => - inv_add_instr' H - | H: context[add_instr _ _ _] |- _ => - monadInv H; inv_incr; inv_add_instr - | H: context[add_branch_instr _ _ _ _ _] |- _ => - inv_add_instr' H - | H: context[add_branch_instr _ _ _ _] |- _ => - monadInv H; inv_incr; inv_add_instr - | H: context[add_node_skip _ _ _] |- _ => - inv_add_instr' H - | H: context[add_node_skip _ _] |- _ => - monadInv H; inv_incr; inv_add_instr - end. - -Ltac destruct_optional := - match goal with H: option ?r |- _ => destruct H end. - -Lemma iter_expand_instr_spec : - forall l fin rtrn stack s s' i x c, - HTLMonadExtra.collectlist (transf_instr fin rtrn stack) l s = OK x s' i -> - list_norepet (List.map fst l) -> - (forall pc instr, In (pc, instr) l -> c!pc = Some instr) -> - (forall pc instr, In (pc, instr) l -> - c!pc = Some instr -> - tr_code c pc instr s'.(st_datapath) s'.(st_controllogic) fin rtrn s'.(st_st) stack). -Proof. - induction l; simpl; intros; try contradiction. - destruct a as [pc1 instr1]; simpl in *. inv H0. monadInv H. inv_incr. - destruct (peq pc pc1). - - subst. - destruct instr1 eqn:?; try discriminate; - try destruct_optional; inv_add_instr; econstructor; try assumption. - + destruct o with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. - + destruct o0 with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. - + inversion H2. inversion H9. rewrite H. apply tr_instr_Inop. - eapply in_map with (f := fst) in H9. contradiction. - - + destruct o with pc1; destruct H16; simpl in *; rewrite AssocMap.gss in H14; eauto; congruence. - + destruct o0 with pc1; destruct H16; simpl in *; rewrite AssocMap.gss in H14; eauto; congruence. - + inversion H2. inversion H14. unfold nonblock. replace (st_st s4) with (st_st s2) by congruence. - econstructor. apply EQ1. eapply in_map with (f := fst) in H14. contradiction. - - + destruct o with pc1; destruct H16; simpl in *; rewrite AssocMap.gss in H14; eauto; congruence. - + destruct o0 with pc1; destruct H16; simpl in *; rewrite AssocMap.gss in H14; eauto; congruence. - + inversion H2. inversion H14. rewrite <- e2. replace (st_st s2) with (st_st s0) by congruence. - econstructor. apply EQ1. eapply in_map with (f := fst) in H14. contradiction. - - + destruct o with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. - + destruct o0 with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. - + destruct H2. - * inversion H2. - replace (st_st s2) with (st_st s0) by congruence. - eauto with htlspec. - * apply in_map with (f := fst) in H2. contradiction. - - + destruct o with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. - + destruct o0 with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. - + destruct H2. - * inversion H2. - replace (st_st s2) with (st_st s0) by congruence. - eauto with htlspec. - * apply in_map with (f := fst) in H2. contradiction. - - + destruct o with pc1; destruct H16; simpl in *; rewrite AssocMap.gss in H14; eauto; congruence. - + destruct o0 with pc1; destruct H16; simpl in *; rewrite AssocMap.gss in H14; eauto; congruence. - + inversion H2. - * inversion H14. constructor. congruence. - * apply in_map with (f := fst) in H14. contradiction. - - + destruct o with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. - + destruct o0 with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. - + inversion H2. - * inversion H9. - replace (st_st s2) with (st_st s0) by congruence. - eauto with htlspec. - * apply in_map with (f := fst) in H9. contradiction. - - + destruct o with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. - + destruct o0 with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. - + inversion H2. - * inversion H9. - replace (st_st s2) with (st_st s0) by congruence. - eauto with htlspec. - * apply in_map with (f := fst) in H9. contradiction. - - - eapply IHl. apply EQ0. assumption. - destruct H2. inversion H2. subst. contradiction. - intros. specialize H1 with pc0 instr0. destruct H1. tauto. trivial. - destruct H2. inv H2. contradiction. assumption. assumption. -Qed. -Hint Resolve iter_expand_instr_spec : htlspec. - -Lemma create_arr_inv : forall w x y z a b c d, - create_arr w x y z = OK (a, b) c d -> - y = b /\ a = z.(st_freshreg) /\ c.(st_freshreg) = Pos.succ (z.(st_freshreg)). -Proof. - inversion 1; split; auto. -Qed. - -Lemma create_reg_inv : forall a b s r s' i, - create_reg a b s = OK r s' i -> - r = s.(st_freshreg) /\ s'.(st_freshreg) = Pos.succ (s.(st_freshreg)). -Proof. - inversion 1; auto. -Qed. - -Theorem transl_module_correct : - forall f m, - transl_module f = Errors.OK m -> tr_module f m. -Proof. - intros until m. - unfold transl_module. - unfold run_mon. - destruct (transf_module f (max_state f)) eqn:?; try discriminate. - intros. inv H. - inversion s; subst. - - unfold transf_module in *. - unfold stack_correct in *. - destruct (0 <=? RTL.fn_stacksize f) eqn:STACK_BOUND_LOW; - destruct (RTL.fn_stacksize f *) +(* stmnts!pc = Some s -> *) +(* trans!pc = Some t -> *) +(* tr_instr fin rtrn st stk i s t -> *) +(* tr_code c pc i stmnts trans fin rtrn st stk. *) +(* Hint Constructors tr_code : htlspec. *) + +(* Inductive tr_module (f : RTL.function) : module -> Prop := *) +(* tr_module_intro : *) +(* forall data control fin rtrn st stk stk_len m start rst clk scldecls arrdecls wf, *) +(* m = (mkmodule f.(RTL.fn_params) *) +(* data *) +(* control *) +(* f.(RTL.fn_entrypoint) *) +(* st stk stk_len fin rtrn start rst clk scldecls arrdecls wf) -> *) +(* (forall pc i, Maps.PTree.get pc f.(RTL.fn_code) = Some i -> *) +(* tr_code f.(RTL.fn_code) pc i data control fin rtrn st stk) -> *) +(* stk_len = Z.to_nat (f.(RTL.fn_stacksize) / 4) -> *) +(* Z.modulo (f.(RTL.fn_stacksize)) 4 = 0 -> *) +(* 0 <= f.(RTL.fn_stacksize) < Integers.Ptrofs.modulus -> *) +(* st = ((RTL.max_reg_function f) + 1)%positive -> *) +(* fin = ((RTL.max_reg_function f) + 2)%positive -> *) +(* rtrn = ((RTL.max_reg_function f) + 3)%positive -> *) +(* stk = ((RTL.max_reg_function f) + 4)%positive -> *) +(* start = ((RTL.max_reg_function f) + 5)%positive -> *) +(* rst = ((RTL.max_reg_function f) + 6)%positive -> *) +(* clk = ((RTL.max_reg_function f) + 7)%positive -> *) +(* tr_module f m. *) +(* Hint Constructors tr_module : htlspec. *) + +(* Lemma create_reg_datapath_trans : *) +(* forall sz s s' x i iop, *) +(* create_reg iop sz s = OK x s' i -> *) +(* s.(st_datapath) = s'.(st_datapath). *) +(* Proof. intros. monadInv H. trivial. Qed. *) +(* Hint Resolve create_reg_datapath_trans : htlspec. *) + +(* Lemma create_reg_controllogic_trans : *) +(* forall sz s s' x i iop, *) +(* create_reg iop sz s = OK x s' i -> *) +(* s.(st_controllogic) = s'.(st_controllogic). *) +(* Proof. intros. monadInv H. trivial. Qed. *) +(* Hint Resolve create_reg_controllogic_trans : htlspec. *) + +(* Lemma declare_reg_datapath_trans : *) +(* forall sz s s' x i iop r, *) +(* declare_reg iop r sz s = OK x s' i -> *) +(* s.(st_datapath) = s'.(st_datapath). *) +(* Proof. intros. monadInv H. trivial. Qed. *) +(* Hint Resolve create_reg_datapath_trans : htlspec. *) + +(* Lemma declare_reg_controllogic_trans : *) +(* forall sz s s' x i iop r, *) +(* declare_reg iop r sz s = OK x s' i -> *) +(* s.(st_controllogic) = s'.(st_controllogic). *) +(* Proof. intros. monadInv H. trivial. Qed. *) +(* Hint Resolve create_reg_controllogic_trans : htlspec. *) + +(* Lemma declare_reg_freshreg_trans : *) +(* forall sz s s' x i iop r, *) +(* declare_reg iop r sz s = OK x s' i -> *) +(* s.(st_freshreg) = s'.(st_freshreg). *) +(* Proof. inversion 1; auto. Qed. *) +(* Hint Resolve declare_reg_freshreg_trans : htlspec. *) + +(* Lemma create_arr_datapath_trans : *) +(* forall sz ln s s' x i iop, *) +(* create_arr iop sz ln s = OK x s' i -> *) +(* s.(st_datapath) = s'.(st_datapath). *) +(* Proof. intros. monadInv H. trivial. Qed. *) +(* Hint Resolve create_arr_datapath_trans : htlspec. *) + +(* Lemma create_arr_controllogic_trans : *) +(* forall sz ln s s' x i iop, *) +(* create_arr iop sz ln s = OK x s' i -> *) +(* s.(st_controllogic) = s'.(st_controllogic). *) +(* Proof. intros. monadInv H. trivial. Qed. *) +(* Hint Resolve create_arr_controllogic_trans : htlspec. *) + +(* Lemma get_refl_x : *) +(* forall s s' x i, *) +(* get s = OK x s' i -> *) +(* s = x. *) +(* Proof. inversion 1. trivial. Qed. *) +(* Hint Resolve get_refl_x : htlspec. *) + +(* Lemma get_refl_s : *) +(* forall s s' x i, *) +(* get s = OK x s' i -> *) +(* s = s'. *) +(* Proof. inversion 1. trivial. Qed. *) +(* Hint Resolve get_refl_s : htlspec. *) + +(* Ltac inv_incr := *) +(* repeat match goal with *) +(* | [ H: create_reg _ _ ?s = OK _ ?s' _ |- _ ] => *) +(* let H1 := fresh "H" in *) +(* assert (H1 := H); eapply create_reg_datapath_trans in H; *) +(* eapply create_reg_controllogic_trans in H1 *) +(* | [ H: create_arr _ _ _ ?s = OK _ ?s' _ |- _ ] => *) +(* let H1 := fresh "H" in *) +(* assert (H1 := H); eapply create_arr_datapath_trans in H; *) +(* eapply create_arr_controllogic_trans in H1 *) +(* | [ H: get ?s = OK _ _ _ |- _ ] => *) +(* let H1 := fresh "H" in *) +(* assert (H1 := H); apply get_refl_x in H; apply get_refl_s in H1; *) +(* subst *) +(* | [ H: st_prop _ _ |- _ ] => unfold st_prop in H; destruct H *) +(* | [ H: st_incr _ _ |- _ ] => destruct st_incr *) +(* end. *) + +(* Lemma collect_controllogic_trans : *) +(* forall A f l cs cs' ci, *) +(* (forall s s' x i y, f y s = OK x s' i -> s.(st_controllogic) = s'.(st_controllogic)) -> *) +(* @HTLMonadExtra.collectlist A f l cs = OK tt cs' ci -> cs.(st_controllogic) = cs'.(st_controllogic). *) +(* Proof. *) +(* induction l; intros; monadInv H0. *) +(* - trivial. *) +(* - apply H in EQ. rewrite EQ. eauto. *) +(* Qed. *) + +(* Lemma collect_datapath_trans : *) +(* forall A f l cs cs' ci, *) +(* (forall s s' x i y, f y s = OK x s' i -> s.(st_datapath) = s'.(st_datapath)) -> *) +(* @HTLMonadExtra.collectlist A f l cs = OK tt cs' ci -> cs.(st_datapath) = cs'.(st_datapath). *) +(* Proof. *) +(* induction l; intros; monadInv H0. *) +(* - trivial. *) +(* - apply H in EQ. rewrite EQ. eauto. *) +(* Qed. *) + +(* Lemma collect_freshreg_trans : *) +(* forall A f l cs cs' ci, *) +(* (forall s s' x i y, f y s = OK x s' i -> s.(st_freshreg) = s'.(st_freshreg)) -> *) +(* @HTLMonadExtra.collectlist A f l cs = OK tt cs' ci -> cs.(st_freshreg) = cs'.(st_freshreg). *) +(* Proof. *) +(* induction l; intros; monadInv H0. *) +(* - trivial. *) +(* - apply H in EQ. rewrite EQ. eauto. *) +(* Qed. *) + +(* Lemma collect_declare_controllogic_trans : *) +(* forall io n l s s' i, *) +(* HTLMonadExtra.collectlist (fun r : reg => declare_reg io r n) l s = OK tt s' i -> *) +(* s.(st_controllogic) = s'.(st_controllogic). *) +(* Proof. *) +(* intros. eapply collect_controllogic_trans; try eassumption. *) +(* intros. eapply declare_reg_controllogic_trans. simpl in H0. eassumption. *) +(* Qed. *) + +(* Lemma collect_declare_datapath_trans : *) +(* forall io n l s s' i, *) +(* HTLMonadExtra.collectlist (fun r : reg => declare_reg io r n) l s = OK tt s' i -> *) +(* s.(st_datapath) = s'.(st_datapath). *) +(* Proof. *) +(* intros. eapply collect_datapath_trans; try eassumption. *) +(* intros. eapply declare_reg_datapath_trans. simpl in H0. eassumption. *) +(* Qed. *) + +(* Lemma collect_declare_freshreg_trans : *) +(* forall io n l s s' i, *) +(* HTLMonadExtra.collectlist (fun r : reg => declare_reg io r n) l s = OK tt s' i -> *) +(* s.(st_freshreg) = s'.(st_freshreg). *) +(* Proof. *) +(* intros. eapply collect_freshreg_trans; try eassumption. *) +(* inversion 1. auto. *) +(* Qed. *) + +(* Ltac unfold_match H := *) +(* match type of H with *) +(* | context[match ?g with _ => _ end] => destruct g eqn:?; try discriminate *) +(* end. *) + +(* Lemma translate_eff_addressing_freshreg_trans : *) +(* forall op args s r s' i, *) +(* translate_eff_addressing op args s = OK r s' i -> *) +(* s.(st_freshreg) = s'.(st_freshreg). *) +(* Proof. *) +(* destruct op; intros; simpl in *; repeat (unfold_match H); inv H; auto. *) +(* Qed. *) +(* Hint Resolve translate_eff_addressing_freshreg_trans : htlspec. *) + +(* Lemma translate_comparison_freshreg_trans : *) +(* forall op args s r s' i, *) +(* translate_comparison op args s = OK r s' i -> *) +(* s.(st_freshreg) = s'.(st_freshreg). *) +(* Proof. *) +(* destruct op; intros; simpl in *; repeat (unfold_match H); inv H; auto. *) +(* Qed. *) +(* Hint Resolve translate_comparison_freshreg_trans : htlspec. *) + +(* Lemma translate_comparison_imm_freshreg_trans : *) +(* forall op args s r s' i n, *) +(* translate_comparison_imm op args n s = OK r s' i -> *) +(* s.(st_freshreg) = s'.(st_freshreg). *) +(* Proof. *) +(* destruct op; intros; simpl in *; repeat (unfold_match H); inv H; auto. *) +(* Qed. *) +(* Hint Resolve translate_comparison_imm_freshreg_trans : htlspec. *) + +(* Lemma translate_condition_freshreg_trans : *) +(* forall op args s r s' i, *) +(* translate_condition op args s = OK r s' i -> *) +(* s.(st_freshreg) = s'.(st_freshreg). *) +(* Proof. *) +(* destruct op; intros; simpl in *; repeat (unfold_match H); inv H; eauto with htlspec. *) +(* Qed. *) +(* Hint Resolve translate_condition_freshreg_trans : htlspec. *) + +(* Lemma translate_instr_freshreg_trans : *) +(* forall op args s r s' i, *) +(* translate_instr op args s = OK r s' i -> *) +(* s.(st_freshreg) = s'.(st_freshreg). *) +(* Proof. *) +(* destruct op; intros; simpl in *; repeat (unfold_match H); inv H; eauto with htlspec. *) +(* monadInv H1. eauto with htlspec. *) +(* Qed. *) +(* Hint Resolve translate_instr_freshreg_trans : htlspec. *) + +(* Lemma translate_arr_access_freshreg_trans : *) +(* forall mem addr args st s r s' i, *) +(* translate_arr_access mem addr args st s = OK r s' i -> *) +(* s.(st_freshreg) = s'.(st_freshreg). *) +(* Proof. *) +(* intros. unfold translate_arr_access in H. repeat (unfold_match H); inv H; eauto with htlspec. *) +(* Qed. *) +(* Hint Resolve translate_arr_access_freshreg_trans : htlspec. *) + +(* Lemma add_instr_freshreg_trans : *) +(* forall n n' st s r s' i, *) +(* add_instr n n' st s = OK r s' i -> *) +(* s.(st_freshreg) = s'.(st_freshreg). *) +(* Proof. intros. unfold add_instr in H. repeat (unfold_match H). inv H. auto. Qed. *) +(* Hint Resolve add_instr_freshreg_trans : htlspec. *) + +(* Lemma add_branch_instr_freshreg_trans : *) +(* forall n n0 n1 e s r s' i, *) +(* add_branch_instr e n n0 n1 s = OK r s' i -> *) +(* s.(st_freshreg) = s'.(st_freshreg). *) +(* Proof. intros. unfold add_branch_instr in H. repeat (unfold_match H). inv H. auto. Qed. *) +(* Hint Resolve add_branch_instr_freshreg_trans : htlspec. *) + +(* Lemma add_node_skip_freshreg_trans : *) +(* forall n1 n2 s r s' i, *) +(* add_node_skip n1 n2 s = OK r s' i -> *) +(* s.(st_freshreg) = s'.(st_freshreg). *) +(* Proof. intros. unfold add_node_skip in H. repeat (unfold_match H). inv H. auto. Qed. *) +(* Hint Resolve add_node_skip_freshreg_trans : htlspec. *) + +(* Lemma add_instr_skip_freshreg_trans : *) +(* forall n1 n2 s r s' i, *) +(* add_instr_skip n1 n2 s = OK r s' i -> *) +(* s.(st_freshreg) = s'.(st_freshreg). *) +(* Proof. intros. unfold add_instr_skip in H. repeat (unfold_match H). inv H. auto. Qed. *) +(* Hint Resolve add_instr_skip_freshreg_trans : htlspec. *) + +(* Lemma transf_instr_freshreg_trans : *) +(* forall fin ret st instr s v s' i, *) +(* transf_instr fin ret st instr s = OK v s' i -> *) +(* s.(st_freshreg) = s'.(st_freshreg). *) +(* Proof. *) +(* intros. destruct instr eqn:?. subst. unfold transf_instr in H. *) +(* destruct i0; try (monadInv H); try (unfold_match H); eauto with htlspec. *) +(* - apply add_instr_freshreg_trans in EQ2. apply translate_instr_freshreg_trans in EQ. *) +(* apply declare_reg_freshreg_trans in EQ1. congruence. *) +(* - apply add_instr_freshreg_trans in EQ2. apply translate_arr_access_freshreg_trans in EQ. *) +(* apply declare_reg_freshreg_trans in EQ1. congruence. *) +(* - apply add_instr_freshreg_trans in EQ0. apply translate_arr_access_freshreg_trans in EQ. congruence. *) +(* - apply translate_condition_freshreg_trans in EQ. apply add_branch_instr_freshreg_trans in EQ0. *) +(* congruence. *) +(* - inv EQ. apply add_node_skip_freshreg_trans in EQ0. congruence. *) +(* Qed. *) +(* Hint Resolve transf_instr_freshreg_trans : htlspec. *) + +(* Lemma collect_trans_instr_freshreg_trans : *) +(* forall fin ret st l s s' i, *) +(* HTLMonadExtra.collectlist (transf_instr fin ret st) l s = OK tt s' i -> *) +(* s.(st_freshreg) = s'.(st_freshreg). *) +(* Proof. *) +(* intros. eapply collect_freshreg_trans; try eassumption. *) +(* eauto with htlspec. *) +(* Qed. *) + +(* Ltac rewrite_states := *) +(* match goal with *) +(* | [ H: ?x ?s = ?x ?s' |- _ ] => *) +(* let c1 := fresh "c" in *) +(* let c2 := fresh "c" in *) +(* remember (?x ?s) as c1; remember (?x ?s') as c2; try subst *) +(* end. *) + +(* Ltac inv_add_instr' H := *) +(* match type of H with *) +(* | ?f _ _ _ = OK _ _ _ => unfold f in H *) +(* | ?f _ _ _ _ = OK _ _ _ => unfold f in H *) +(* | ?f _ _ _ _ _ = OK _ _ _ => unfold f in H *) +(* end; repeat unfold_match H; inversion H. *) + +(* Ltac inv_add_instr := *) +(* lazymatch goal with *) +(* | H: context[add_instr_skip _ _ _] |- _ => *) +(* inv_add_instr' H *) +(* | H: context[add_instr_skip _ _] |- _ => *) +(* monadInv H; inv_incr; inv_add_instr *) +(* | H: context[add_instr _ _ _ _] |- _ => *) +(* inv_add_instr' H *) +(* | H: context[add_instr _ _ _] |- _ => *) +(* monadInv H; inv_incr; inv_add_instr *) +(* | H: context[add_branch_instr _ _ _ _ _] |- _ => *) +(* inv_add_instr' H *) +(* | H: context[add_branch_instr _ _ _ _] |- _ => *) +(* monadInv H; inv_incr; inv_add_instr *) +(* | H: context[add_node_skip _ _ _] |- _ => *) +(* inv_add_instr' H *) +(* | H: context[add_node_skip _ _] |- _ => *) +(* monadInv H; inv_incr; inv_add_instr *) +(* end. *) + +(* Ltac destruct_optional := *) +(* match goal with H: option ?r |- _ => destruct H end. *) + +(* Lemma iter_expand_instr_spec : *) +(* forall l fin rtrn stack s s' i x c, *) +(* HTLMonadExtra.collectlist (transf_instr fin rtrn stack) l s = OK x s' i -> *) +(* list_norepet (List.map fst l) -> *) +(* (forall pc instr, In (pc, instr) l -> c!pc = Some instr) -> *) +(* (forall pc instr, In (pc, instr) l -> *) +(* c!pc = Some instr -> *) +(* tr_code c pc instr s'.(st_datapath) s'.(st_controllogic) fin rtrn s'.(st_st) stack). *) +(* Proof. *) +(* induction l; simpl; intros; try contradiction. *) +(* destruct a as [pc1 instr1]; simpl in *. inv H0. monadInv H. inv_incr. *) +(* destruct (peq pc pc1). *) +(* - subst. *) +(* destruct instr1 eqn:?; try discriminate; *) +(* try destruct_optional; inv_add_instr; econstructor; try assumption. *) +(* + destruct o with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. *) +(* + destruct o0 with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. *) +(* + inversion H2. inversion H9. rewrite H. apply tr_instr_Inop. *) +(* eapply in_map with (f := fst) in H9. contradiction. *) + +(* + destruct o with pc1; destruct H16; simpl in *; rewrite AssocMap.gss in H14; eauto; congruence. *) +(* + destruct o0 with pc1; destruct H16; simpl in *; rewrite AssocMap.gss in H14; eauto; congruence. *) +(* + inversion H2. inversion H14. unfold nonblock. replace (st_st s4) with (st_st s2) by congruence. *) +(* econstructor. apply EQ1. eapply in_map with (f := fst) in H14. contradiction. *) + +(* + destruct o with pc1; destruct H16; simpl in *; rewrite AssocMap.gss in H14; eauto; congruence. *) +(* + destruct o0 with pc1; destruct H16; simpl in *; rewrite AssocMap.gss in H14; eauto; congruence. *) +(* + inversion H2. inversion H14. rewrite <- e2. replace (st_st s2) with (st_st s0) by congruence. *) +(* econstructor. apply EQ1. eapply in_map with (f := fst) in H14. contradiction. *) + +(* + destruct o with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. *) +(* + destruct o0 with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. *) +(* + destruct H2. *) +(* * inversion H2. *) +(* replace (st_st s2) with (st_st s0) by congruence. *) +(* eauto with htlspec. *) +(* * apply in_map with (f := fst) in H2. contradiction. *) + +(* + destruct o with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. *) +(* + destruct o0 with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. *) +(* + destruct H2. *) +(* * inversion H2. *) +(* replace (st_st s2) with (st_st s0) by congruence. *) +(* eauto with htlspec. *) +(* * apply in_map with (f := fst) in H2. contradiction. *) + +(* + destruct o with pc1; destruct H16; simpl in *; rewrite AssocMap.gss in H14; eauto; congruence. *) +(* + destruct o0 with pc1; destruct H16; simpl in *; rewrite AssocMap.gss in H14; eauto; congruence. *) +(* + inversion H2. *) +(* * inversion H14. constructor. congruence. *) +(* * apply in_map with (f := fst) in H14. contradiction. *) + +(* + destruct o with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. *) +(* + destruct o0 with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. *) +(* + inversion H2. *) +(* * inversion H9. *) +(* replace (st_st s2) with (st_st s0) by congruence. *) +(* eauto with htlspec. *) +(* * apply in_map with (f := fst) in H9. contradiction. *) + +(* + destruct o with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. *) +(* + destruct o0 with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. *) +(* + inversion H2. *) +(* * inversion H9. *) +(* replace (st_st s2) with (st_st s0) by congruence. *) +(* eauto with htlspec. *) +(* * apply in_map with (f := fst) in H9. contradiction. *) + +(* - eapply IHl. apply EQ0. assumption. *) +(* destruct H2. inversion H2. subst. contradiction. *) +(* intros. specialize H1 with pc0 instr0. destruct H1. tauto. trivial. *) +(* destruct H2. inv H2. contradiction. assumption. assumption. *) +(* Qed. *) +(* Hint Resolve iter_expand_instr_spec : htlspec. *) + +(* Lemma create_arr_inv : forall w x y z a b c d, *) +(* create_arr w x y z = OK (a, b) c d -> *) +(* y = b /\ a = z.(st_freshreg) /\ c.(st_freshreg) = Pos.succ (z.(st_freshreg)). *) +(* Proof. *) +(* inversion 1; split; auto. *) +(* Qed. *) + +(* Lemma create_reg_inv : forall a b s r s' i, *) +(* create_reg a b s = OK r s' i -> *) +(* r = s.(st_freshreg) /\ s'.(st_freshreg) = Pos.succ (s.(st_freshreg)). *) +(* Proof. *) +(* inversion 1; auto. *) +(* Qed. *) + +(* Theorem transl_module_correct : *) +(* forall f m, *) +(* transl_module f = Errors.OK m -> tr_module f m. *) +(* Proof. *) +(* intros until m. *) +(* unfold transl_module. *) +(* unfold run_mon. *) +(* destruct (transf_module f (max_state f)) eqn:?; try discriminate. *) +(* intros. inv H. *) +(* inversion s; subst. *) + +(* unfold transf_module in *. *) +(* unfold stack_correct in *. *) +(* destruct (0 <=? RTL.fn_stacksize f) eqn:STACK_BOUND_LOW; *) +(* destruct (RTL.fn_stacksize f Date: Mon, 6 Jul 2020 19:27:51 +0100 Subject: Fix HTLgenspec. --- src/translation/HTLgenspec.v | 925 +++++++++++++++++++++---------------------- 1 file changed, 459 insertions(+), 466 deletions(-) (limited to 'src/translation/HTLgenspec.v') diff --git a/src/translation/HTLgenspec.v b/src/translation/HTLgenspec.v index 4662cf4..bbcde14 100644 --- a/src/translation/HTLgenspec.v +++ b/src/translation/HTLgenspec.v @@ -134,476 +134,469 @@ Inductive tr_instr (fin rtrn st stk : reg) : RTL.instruction -> stmnt -> stmnt - tr_instr fin rtrn st stk (RTL.Ireturn (Some r)) (Vseq (block fin (Vlit (ZToValue 1%Z))) (block rtrn (Vvar r))) Vskip | tr_instr_Iload : - forall mem addr args s s' i c dst n, - translate_arr_access mem addr args stk s = OK c s' i -> - tr_instr fin rtrn st stk (RTL.Iload mem addr args dst n) (nonblock dst c) (state_goto st n) + forall mem addr args s s' i e dst n, + translate_eff_addressing addr args s = OK e s' i -> + tr_instr fin rtrn st stk (RTL.Iload mem addr args dst n) + (create_single_cycle_load stk e dst) (state_goto st n) | tr_instr_Istore : - forall mem addr args s s' i c src n, - translate_arr_access mem addr args stk s = OK c s' i -> - tr_instr fin rtrn st stk (RTL.Istore mem addr args src n) (Vnonblock c (Vvar src)) - (state_goto st n) + forall mem addr args s s' i e src n, + translate_eff_addressing addr args s = OK e s' i -> + tr_instr fin rtrn st stk (RTL.Istore mem addr args src n) + (create_single_cycle_store stk e src) (state_goto st n) | tr_instr_Ijumptable : forall cexpr tbl r, cexpr = tbl_to_case_expr st tbl -> tr_instr fin rtrn st stk (RTL.Ijumptable r tbl) (Vskip) (Vcase (Vvar r) cexpr (Some Vskip)). Hint Constructors tr_instr : htlspec. -(* Inductive tr_code (c : RTL.code) (pc : RTL.node) (i : RTL.instruction) (stmnts trans : PTree.t stmnt) *) -(* (fin rtrn st stk : reg) : Prop := *) -(* tr_code_intro : *) -(* forall s t, *) -(* c!pc = Some i -> *) -(* stmnts!pc = Some s -> *) -(* trans!pc = Some t -> *) -(* tr_instr fin rtrn st stk i s t -> *) -(* tr_code c pc i stmnts trans fin rtrn st stk. *) -(* Hint Constructors tr_code : htlspec. *) - -(* Inductive tr_module (f : RTL.function) : module -> Prop := *) -(* tr_module_intro : *) -(* forall data control fin rtrn st stk stk_len m start rst clk scldecls arrdecls wf, *) -(* m = (mkmodule f.(RTL.fn_params) *) -(* data *) -(* control *) -(* f.(RTL.fn_entrypoint) *) -(* st stk stk_len fin rtrn start rst clk scldecls arrdecls wf) -> *) -(* (forall pc i, Maps.PTree.get pc f.(RTL.fn_code) = Some i -> *) -(* tr_code f.(RTL.fn_code) pc i data control fin rtrn st stk) -> *) -(* stk_len = Z.to_nat (f.(RTL.fn_stacksize) / 4) -> *) -(* Z.modulo (f.(RTL.fn_stacksize)) 4 = 0 -> *) -(* 0 <= f.(RTL.fn_stacksize) < Integers.Ptrofs.modulus -> *) -(* st = ((RTL.max_reg_function f) + 1)%positive -> *) -(* fin = ((RTL.max_reg_function f) + 2)%positive -> *) -(* rtrn = ((RTL.max_reg_function f) + 3)%positive -> *) -(* stk = ((RTL.max_reg_function f) + 4)%positive -> *) -(* start = ((RTL.max_reg_function f) + 5)%positive -> *) -(* rst = ((RTL.max_reg_function f) + 6)%positive -> *) -(* clk = ((RTL.max_reg_function f) + 7)%positive -> *) -(* tr_module f m. *) -(* Hint Constructors tr_module : htlspec. *) - -(* Lemma create_reg_datapath_trans : *) -(* forall sz s s' x i iop, *) -(* create_reg iop sz s = OK x s' i -> *) -(* s.(st_datapath) = s'.(st_datapath). *) -(* Proof. intros. monadInv H. trivial. Qed. *) -(* Hint Resolve create_reg_datapath_trans : htlspec. *) - -(* Lemma create_reg_controllogic_trans : *) -(* forall sz s s' x i iop, *) -(* create_reg iop sz s = OK x s' i -> *) -(* s.(st_controllogic) = s'.(st_controllogic). *) -(* Proof. intros. monadInv H. trivial. Qed. *) -(* Hint Resolve create_reg_controllogic_trans : htlspec. *) - -(* Lemma declare_reg_datapath_trans : *) -(* forall sz s s' x i iop r, *) -(* declare_reg iop r sz s = OK x s' i -> *) -(* s.(st_datapath) = s'.(st_datapath). *) -(* Proof. intros. monadInv H. trivial. Qed. *) -(* Hint Resolve create_reg_datapath_trans : htlspec. *) - -(* Lemma declare_reg_controllogic_trans : *) -(* forall sz s s' x i iop r, *) -(* declare_reg iop r sz s = OK x s' i -> *) -(* s.(st_controllogic) = s'.(st_controllogic). *) -(* Proof. intros. monadInv H. trivial. Qed. *) -(* Hint Resolve create_reg_controllogic_trans : htlspec. *) - -(* Lemma declare_reg_freshreg_trans : *) -(* forall sz s s' x i iop r, *) -(* declare_reg iop r sz s = OK x s' i -> *) -(* s.(st_freshreg) = s'.(st_freshreg). *) -(* Proof. inversion 1; auto. Qed. *) -(* Hint Resolve declare_reg_freshreg_trans : htlspec. *) - -(* Lemma create_arr_datapath_trans : *) -(* forall sz ln s s' x i iop, *) -(* create_arr iop sz ln s = OK x s' i -> *) -(* s.(st_datapath) = s'.(st_datapath). *) -(* Proof. intros. monadInv H. trivial. Qed. *) -(* Hint Resolve create_arr_datapath_trans : htlspec. *) - -(* Lemma create_arr_controllogic_trans : *) -(* forall sz ln s s' x i iop, *) -(* create_arr iop sz ln s = OK x s' i -> *) -(* s.(st_controllogic) = s'.(st_controllogic). *) -(* Proof. intros. monadInv H. trivial. Qed. *) -(* Hint Resolve create_arr_controllogic_trans : htlspec. *) - -(* Lemma get_refl_x : *) -(* forall s s' x i, *) -(* get s = OK x s' i -> *) -(* s = x. *) -(* Proof. inversion 1. trivial. Qed. *) -(* Hint Resolve get_refl_x : htlspec. *) - -(* Lemma get_refl_s : *) -(* forall s s' x i, *) -(* get s = OK x s' i -> *) -(* s = s'. *) -(* Proof. inversion 1. trivial. Qed. *) -(* Hint Resolve get_refl_s : htlspec. *) - -(* Ltac inv_incr := *) -(* repeat match goal with *) -(* | [ H: create_reg _ _ ?s = OK _ ?s' _ |- _ ] => *) -(* let H1 := fresh "H" in *) -(* assert (H1 := H); eapply create_reg_datapath_trans in H; *) -(* eapply create_reg_controllogic_trans in H1 *) -(* | [ H: create_arr _ _ _ ?s = OK _ ?s' _ |- _ ] => *) -(* let H1 := fresh "H" in *) -(* assert (H1 := H); eapply create_arr_datapath_trans in H; *) -(* eapply create_arr_controllogic_trans in H1 *) -(* | [ H: get ?s = OK _ _ _ |- _ ] => *) -(* let H1 := fresh "H" in *) -(* assert (H1 := H); apply get_refl_x in H; apply get_refl_s in H1; *) -(* subst *) -(* | [ H: st_prop _ _ |- _ ] => unfold st_prop in H; destruct H *) -(* | [ H: st_incr _ _ |- _ ] => destruct st_incr *) -(* end. *) - -(* Lemma collect_controllogic_trans : *) -(* forall A f l cs cs' ci, *) -(* (forall s s' x i y, f y s = OK x s' i -> s.(st_controllogic) = s'.(st_controllogic)) -> *) -(* @HTLMonadExtra.collectlist A f l cs = OK tt cs' ci -> cs.(st_controllogic) = cs'.(st_controllogic). *) -(* Proof. *) -(* induction l; intros; monadInv H0. *) -(* - trivial. *) -(* - apply H in EQ. rewrite EQ. eauto. *) -(* Qed. *) - -(* Lemma collect_datapath_trans : *) -(* forall A f l cs cs' ci, *) -(* (forall s s' x i y, f y s = OK x s' i -> s.(st_datapath) = s'.(st_datapath)) -> *) -(* @HTLMonadExtra.collectlist A f l cs = OK tt cs' ci -> cs.(st_datapath) = cs'.(st_datapath). *) -(* Proof. *) -(* induction l; intros; monadInv H0. *) -(* - trivial. *) -(* - apply H in EQ. rewrite EQ. eauto. *) -(* Qed. *) - -(* Lemma collect_freshreg_trans : *) -(* forall A f l cs cs' ci, *) -(* (forall s s' x i y, f y s = OK x s' i -> s.(st_freshreg) = s'.(st_freshreg)) -> *) -(* @HTLMonadExtra.collectlist A f l cs = OK tt cs' ci -> cs.(st_freshreg) = cs'.(st_freshreg). *) -(* Proof. *) -(* induction l; intros; monadInv H0. *) -(* - trivial. *) -(* - apply H in EQ. rewrite EQ. eauto. *) -(* Qed. *) - -(* Lemma collect_declare_controllogic_trans : *) -(* forall io n l s s' i, *) -(* HTLMonadExtra.collectlist (fun r : reg => declare_reg io r n) l s = OK tt s' i -> *) -(* s.(st_controllogic) = s'.(st_controllogic). *) -(* Proof. *) -(* intros. eapply collect_controllogic_trans; try eassumption. *) -(* intros. eapply declare_reg_controllogic_trans. simpl in H0. eassumption. *) -(* Qed. *) - -(* Lemma collect_declare_datapath_trans : *) -(* forall io n l s s' i, *) -(* HTLMonadExtra.collectlist (fun r : reg => declare_reg io r n) l s = OK tt s' i -> *) -(* s.(st_datapath) = s'.(st_datapath). *) -(* Proof. *) -(* intros. eapply collect_datapath_trans; try eassumption. *) -(* intros. eapply declare_reg_datapath_trans. simpl in H0. eassumption. *) -(* Qed. *) - -(* Lemma collect_declare_freshreg_trans : *) -(* forall io n l s s' i, *) -(* HTLMonadExtra.collectlist (fun r : reg => declare_reg io r n) l s = OK tt s' i -> *) -(* s.(st_freshreg) = s'.(st_freshreg). *) -(* Proof. *) -(* intros. eapply collect_freshreg_trans; try eassumption. *) -(* inversion 1. auto. *) -(* Qed. *) - -(* Ltac unfold_match H := *) -(* match type of H with *) -(* | context[match ?g with _ => _ end] => destruct g eqn:?; try discriminate *) -(* end. *) - -(* Lemma translate_eff_addressing_freshreg_trans : *) -(* forall op args s r s' i, *) -(* translate_eff_addressing op args s = OK r s' i -> *) -(* s.(st_freshreg) = s'.(st_freshreg). *) -(* Proof. *) -(* destruct op; intros; simpl in *; repeat (unfold_match H); inv H; auto. *) -(* Qed. *) -(* Hint Resolve translate_eff_addressing_freshreg_trans : htlspec. *) - -(* Lemma translate_comparison_freshreg_trans : *) -(* forall op args s r s' i, *) -(* translate_comparison op args s = OK r s' i -> *) -(* s.(st_freshreg) = s'.(st_freshreg). *) -(* Proof. *) -(* destruct op; intros; simpl in *; repeat (unfold_match H); inv H; auto. *) -(* Qed. *) -(* Hint Resolve translate_comparison_freshreg_trans : htlspec. *) - -(* Lemma translate_comparison_imm_freshreg_trans : *) -(* forall op args s r s' i n, *) -(* translate_comparison_imm op args n s = OK r s' i -> *) -(* s.(st_freshreg) = s'.(st_freshreg). *) -(* Proof. *) -(* destruct op; intros; simpl in *; repeat (unfold_match H); inv H; auto. *) -(* Qed. *) -(* Hint Resolve translate_comparison_imm_freshreg_trans : htlspec. *) - -(* Lemma translate_condition_freshreg_trans : *) -(* forall op args s r s' i, *) -(* translate_condition op args s = OK r s' i -> *) -(* s.(st_freshreg) = s'.(st_freshreg). *) -(* Proof. *) -(* destruct op; intros; simpl in *; repeat (unfold_match H); inv H; eauto with htlspec. *) -(* Qed. *) -(* Hint Resolve translate_condition_freshreg_trans : htlspec. *) - -(* Lemma translate_instr_freshreg_trans : *) -(* forall op args s r s' i, *) -(* translate_instr op args s = OK r s' i -> *) -(* s.(st_freshreg) = s'.(st_freshreg). *) -(* Proof. *) -(* destruct op; intros; simpl in *; repeat (unfold_match H); inv H; eauto with htlspec. *) -(* monadInv H1. eauto with htlspec. *) -(* Qed. *) -(* Hint Resolve translate_instr_freshreg_trans : htlspec. *) - -(* Lemma translate_arr_access_freshreg_trans : *) -(* forall mem addr args st s r s' i, *) -(* translate_arr_access mem addr args st s = OK r s' i -> *) -(* s.(st_freshreg) = s'.(st_freshreg). *) -(* Proof. *) -(* intros. unfold translate_arr_access in H. repeat (unfold_match H); inv H; eauto with htlspec. *) -(* Qed. *) -(* Hint Resolve translate_arr_access_freshreg_trans : htlspec. *) - -(* Lemma add_instr_freshreg_trans : *) -(* forall n n' st s r s' i, *) -(* add_instr n n' st s = OK r s' i -> *) -(* s.(st_freshreg) = s'.(st_freshreg). *) -(* Proof. intros. unfold add_instr in H. repeat (unfold_match H). inv H. auto. Qed. *) -(* Hint Resolve add_instr_freshreg_trans : htlspec. *) - -(* Lemma add_branch_instr_freshreg_trans : *) -(* forall n n0 n1 e s r s' i, *) -(* add_branch_instr e n n0 n1 s = OK r s' i -> *) -(* s.(st_freshreg) = s'.(st_freshreg). *) -(* Proof. intros. unfold add_branch_instr in H. repeat (unfold_match H). inv H. auto. Qed. *) -(* Hint Resolve add_branch_instr_freshreg_trans : htlspec. *) - -(* Lemma add_node_skip_freshreg_trans : *) -(* forall n1 n2 s r s' i, *) -(* add_node_skip n1 n2 s = OK r s' i -> *) -(* s.(st_freshreg) = s'.(st_freshreg). *) -(* Proof. intros. unfold add_node_skip in H. repeat (unfold_match H). inv H. auto. Qed. *) -(* Hint Resolve add_node_skip_freshreg_trans : htlspec. *) - -(* Lemma add_instr_skip_freshreg_trans : *) -(* forall n1 n2 s r s' i, *) -(* add_instr_skip n1 n2 s = OK r s' i -> *) -(* s.(st_freshreg) = s'.(st_freshreg). *) -(* Proof. intros. unfold add_instr_skip in H. repeat (unfold_match H). inv H. auto. Qed. *) -(* Hint Resolve add_instr_skip_freshreg_trans : htlspec. *) - -(* Lemma transf_instr_freshreg_trans : *) -(* forall fin ret st instr s v s' i, *) -(* transf_instr fin ret st instr s = OK v s' i -> *) -(* s.(st_freshreg) = s'.(st_freshreg). *) -(* Proof. *) -(* intros. destruct instr eqn:?. subst. unfold transf_instr in H. *) -(* destruct i0; try (monadInv H); try (unfold_match H); eauto with htlspec. *) -(* - apply add_instr_freshreg_trans in EQ2. apply translate_instr_freshreg_trans in EQ. *) -(* apply declare_reg_freshreg_trans in EQ1. congruence. *) -(* - apply add_instr_freshreg_trans in EQ2. apply translate_arr_access_freshreg_trans in EQ. *) -(* apply declare_reg_freshreg_trans in EQ1. congruence. *) -(* - apply add_instr_freshreg_trans in EQ0. apply translate_arr_access_freshreg_trans in EQ. congruence. *) -(* - apply translate_condition_freshreg_trans in EQ. apply add_branch_instr_freshreg_trans in EQ0. *) -(* congruence. *) -(* - inv EQ. apply add_node_skip_freshreg_trans in EQ0. congruence. *) -(* Qed. *) -(* Hint Resolve transf_instr_freshreg_trans : htlspec. *) - -(* Lemma collect_trans_instr_freshreg_trans : *) -(* forall fin ret st l s s' i, *) -(* HTLMonadExtra.collectlist (transf_instr fin ret st) l s = OK tt s' i -> *) -(* s.(st_freshreg) = s'.(st_freshreg). *) -(* Proof. *) -(* intros. eapply collect_freshreg_trans; try eassumption. *) -(* eauto with htlspec. *) -(* Qed. *) - -(* Ltac rewrite_states := *) -(* match goal with *) -(* | [ H: ?x ?s = ?x ?s' |- _ ] => *) -(* let c1 := fresh "c" in *) -(* let c2 := fresh "c" in *) -(* remember (?x ?s) as c1; remember (?x ?s') as c2; try subst *) -(* end. *) - -(* Ltac inv_add_instr' H := *) -(* match type of H with *) -(* | ?f _ _ _ = OK _ _ _ => unfold f in H *) -(* | ?f _ _ _ _ = OK _ _ _ => unfold f in H *) -(* | ?f _ _ _ _ _ = OK _ _ _ => unfold f in H *) -(* end; repeat unfold_match H; inversion H. *) - -(* Ltac inv_add_instr := *) -(* lazymatch goal with *) -(* | H: context[add_instr_skip _ _ _] |- _ => *) -(* inv_add_instr' H *) -(* | H: context[add_instr_skip _ _] |- _ => *) -(* monadInv H; inv_incr; inv_add_instr *) -(* | H: context[add_instr _ _ _ _] |- _ => *) -(* inv_add_instr' H *) -(* | H: context[add_instr _ _ _] |- _ => *) -(* monadInv H; inv_incr; inv_add_instr *) -(* | H: context[add_branch_instr _ _ _ _ _] |- _ => *) -(* inv_add_instr' H *) -(* | H: context[add_branch_instr _ _ _ _] |- _ => *) -(* monadInv H; inv_incr; inv_add_instr *) -(* | H: context[add_node_skip _ _ _] |- _ => *) -(* inv_add_instr' H *) -(* | H: context[add_node_skip _ _] |- _ => *) -(* monadInv H; inv_incr; inv_add_instr *) -(* end. *) - -(* Ltac destruct_optional := *) -(* match goal with H: option ?r |- _ => destruct H end. *) - -(* Lemma iter_expand_instr_spec : *) -(* forall l fin rtrn stack s s' i x c, *) -(* HTLMonadExtra.collectlist (transf_instr fin rtrn stack) l s = OK x s' i -> *) -(* list_norepet (List.map fst l) -> *) -(* (forall pc instr, In (pc, instr) l -> c!pc = Some instr) -> *) -(* (forall pc instr, In (pc, instr) l -> *) -(* c!pc = Some instr -> *) -(* tr_code c pc instr s'.(st_datapath) s'.(st_controllogic) fin rtrn s'.(st_st) stack). *) -(* Proof. *) -(* induction l; simpl; intros; try contradiction. *) -(* destruct a as [pc1 instr1]; simpl in *. inv H0. monadInv H. inv_incr. *) -(* destruct (peq pc pc1). *) -(* - subst. *) -(* destruct instr1 eqn:?; try discriminate; *) -(* try destruct_optional; inv_add_instr; econstructor; try assumption. *) -(* + destruct o with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. *) -(* + destruct o0 with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. *) -(* + inversion H2. inversion H9. rewrite H. apply tr_instr_Inop. *) -(* eapply in_map with (f := fst) in H9. contradiction. *) - -(* + destruct o with pc1; destruct H16; simpl in *; rewrite AssocMap.gss in H14; eauto; congruence. *) -(* + destruct o0 with pc1; destruct H16; simpl in *; rewrite AssocMap.gss in H14; eauto; congruence. *) -(* + inversion H2. inversion H14. unfold nonblock. replace (st_st s4) with (st_st s2) by congruence. *) -(* econstructor. apply EQ1. eapply in_map with (f := fst) in H14. contradiction. *) - -(* + destruct o with pc1; destruct H16; simpl in *; rewrite AssocMap.gss in H14; eauto; congruence. *) -(* + destruct o0 with pc1; destruct H16; simpl in *; rewrite AssocMap.gss in H14; eauto; congruence. *) -(* + inversion H2. inversion H14. rewrite <- e2. replace (st_st s2) with (st_st s0) by congruence. *) -(* econstructor. apply EQ1. eapply in_map with (f := fst) in H14. contradiction. *) - -(* + destruct o with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. *) -(* + destruct o0 with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. *) -(* + destruct H2. *) -(* * inversion H2. *) -(* replace (st_st s2) with (st_st s0) by congruence. *) -(* eauto with htlspec. *) -(* * apply in_map with (f := fst) in H2. contradiction. *) - -(* + destruct o with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. *) -(* + destruct o0 with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. *) -(* + destruct H2. *) -(* * inversion H2. *) -(* replace (st_st s2) with (st_st s0) by congruence. *) -(* eauto with htlspec. *) -(* * apply in_map with (f := fst) in H2. contradiction. *) - -(* + destruct o with pc1; destruct H16; simpl in *; rewrite AssocMap.gss in H14; eauto; congruence. *) -(* + destruct o0 with pc1; destruct H16; simpl in *; rewrite AssocMap.gss in H14; eauto; congruence. *) -(* + inversion H2. *) -(* * inversion H14. constructor. congruence. *) -(* * apply in_map with (f := fst) in H14. contradiction. *) - -(* + destruct o with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. *) -(* + destruct o0 with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. *) -(* + inversion H2. *) -(* * inversion H9. *) -(* replace (st_st s2) with (st_st s0) by congruence. *) -(* eauto with htlspec. *) -(* * apply in_map with (f := fst) in H9. contradiction. *) - -(* + destruct o with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. *) -(* + destruct o0 with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. *) -(* + inversion H2. *) -(* * inversion H9. *) -(* replace (st_st s2) with (st_st s0) by congruence. *) -(* eauto with htlspec. *) -(* * apply in_map with (f := fst) in H9. contradiction. *) - -(* - eapply IHl. apply EQ0. assumption. *) -(* destruct H2. inversion H2. subst. contradiction. *) -(* intros. specialize H1 with pc0 instr0. destruct H1. tauto. trivial. *) -(* destruct H2. inv H2. contradiction. assumption. assumption. *) -(* Qed. *) -(* Hint Resolve iter_expand_instr_spec : htlspec. *) - -(* Lemma create_arr_inv : forall w x y z a b c d, *) -(* create_arr w x y z = OK (a, b) c d -> *) -(* y = b /\ a = z.(st_freshreg) /\ c.(st_freshreg) = Pos.succ (z.(st_freshreg)). *) -(* Proof. *) -(* inversion 1; split; auto. *) -(* Qed. *) - -(* Lemma create_reg_inv : forall a b s r s' i, *) -(* create_reg a b s = OK r s' i -> *) -(* r = s.(st_freshreg) /\ s'.(st_freshreg) = Pos.succ (s.(st_freshreg)). *) -(* Proof. *) -(* inversion 1; auto. *) -(* Qed. *) - -(* Theorem transl_module_correct : *) -(* forall f m, *) -(* transl_module f = Errors.OK m -> tr_module f m. *) -(* Proof. *) -(* intros until m. *) -(* unfold transl_module. *) -(* unfold run_mon. *) -(* destruct (transf_module f (max_state f)) eqn:?; try discriminate. *) -(* intros. inv H. *) -(* inversion s; subst. *) - -(* unfold transf_module in *. *) -(* unfold stack_correct in *. *) -(* destruct (0 <=? RTL.fn_stacksize f) eqn:STACK_BOUND_LOW; *) -(* destruct (RTL.fn_stacksize f + stmnts!pc = Some s -> + trans!pc = Some t -> + tr_instr fin rtrn st stk i s t -> + tr_code c pc i stmnts trans fin rtrn st stk. +Hint Constructors tr_code : htlspec. + +Inductive tr_module (f : RTL.function) : module -> Prop := + tr_module_intro : + forall data control fin rtrn st stk stk_len m start rst clk scldecls arrdecls wf, + m = (mkmodule f.(RTL.fn_params) + data + control + f.(RTL.fn_entrypoint) + st stk stk_len fin rtrn start rst clk scldecls arrdecls wf) -> + (forall pc i, Maps.PTree.get pc f.(RTL.fn_code) = Some i -> + tr_code f.(RTL.fn_code) pc i data control fin rtrn st stk) -> + stk_len = Z.to_nat f.(RTL.fn_stacksize) -> + Z.modulo (f.(RTL.fn_stacksize)) 4 = 0 -> + 0 <= f.(RTL.fn_stacksize) < Integers.Ptrofs.modulus -> + st = ((RTL.max_reg_function f) + 1)%positive -> + fin = ((RTL.max_reg_function f) + 2)%positive -> + rtrn = ((RTL.max_reg_function f) + 3)%positive -> + stk = ((RTL.max_reg_function f) + 4)%positive -> + start = ((RTL.max_reg_function f) + 5)%positive -> + rst = ((RTL.max_reg_function f) + 6)%positive -> + clk = ((RTL.max_reg_function f) + 7)%positive -> + tr_module f m. +Hint Constructors tr_module : htlspec. + +Lemma create_reg_datapath_trans : + forall sz s s' x i iop, + create_reg iop sz s = OK x s' i -> + s.(st_datapath) = s'.(st_datapath). +Proof. intros. monadInv H. trivial. Qed. +Hint Resolve create_reg_datapath_trans : htlspec. + +Lemma create_reg_controllogic_trans : + forall sz s s' x i iop, + create_reg iop sz s = OK x s' i -> + s.(st_controllogic) = s'.(st_controllogic). +Proof. intros. monadInv H. trivial. Qed. +Hint Resolve create_reg_controllogic_trans : htlspec. + +Lemma declare_reg_datapath_trans : + forall sz s s' x i iop r, + declare_reg iop r sz s = OK x s' i -> + s.(st_datapath) = s'.(st_datapath). +Proof. intros. monadInv H. trivial. Qed. +Hint Resolve create_reg_datapath_trans : htlspec. + +Lemma declare_reg_controllogic_trans : + forall sz s s' x i iop r, + declare_reg iop r sz s = OK x s' i -> + s.(st_controllogic) = s'.(st_controllogic). +Proof. intros. monadInv H. trivial. Qed. +Hint Resolve create_reg_controllogic_trans : htlspec. + +Lemma declare_reg_freshreg_trans : + forall sz s s' x i iop r, + declare_reg iop r sz s = OK x s' i -> + s.(st_freshreg) = s'.(st_freshreg). +Proof. inversion 1; auto. Qed. +Hint Resolve declare_reg_freshreg_trans : htlspec. + +Lemma create_arr_datapath_trans : + forall sz ln s s' x i iop, + create_arr iop sz ln s = OK x s' i -> + s.(st_datapath) = s'.(st_datapath). +Proof. intros. monadInv H. trivial. Qed. +Hint Resolve create_arr_datapath_trans : htlspec. + +Lemma create_arr_controllogic_trans : + forall sz ln s s' x i iop, + create_arr iop sz ln s = OK x s' i -> + s.(st_controllogic) = s'.(st_controllogic). +Proof. intros. monadInv H. trivial. Qed. +Hint Resolve create_arr_controllogic_trans : htlspec. + +Lemma get_refl_x : + forall s s' x i, + get s = OK x s' i -> + s = x. +Proof. inversion 1. trivial. Qed. +Hint Resolve get_refl_x : htlspec. + +Lemma get_refl_s : + forall s s' x i, + get s = OK x s' i -> + s = s'. +Proof. inversion 1. trivial. Qed. +Hint Resolve get_refl_s : htlspec. + +Ltac inv_incr := + repeat match goal with + | [ H: create_reg _ _ ?s = OK _ ?s' _ |- _ ] => + let H1 := fresh "H" in + assert (H1 := H); eapply create_reg_datapath_trans in H; + eapply create_reg_controllogic_trans in H1 + | [ H: create_arr _ _ _ ?s = OK _ ?s' _ |- _ ] => + let H1 := fresh "H" in + assert (H1 := H); eapply create_arr_datapath_trans in H; + eapply create_arr_controllogic_trans in H1 + | [ H: get ?s = OK _ _ _ |- _ ] => + let H1 := fresh "H" in + assert (H1 := H); apply get_refl_x in H; apply get_refl_s in H1; + subst + | [ H: st_prop _ _ |- _ ] => unfold st_prop in H; destruct H + | [ H: st_incr _ _ |- _ ] => destruct st_incr + end. + +Lemma collect_controllogic_trans : + forall A f l cs cs' ci, + (forall s s' x i y, f y s = OK x s' i -> s.(st_controllogic) = s'.(st_controllogic)) -> + @HTLMonadExtra.collectlist A f l cs = OK tt cs' ci -> cs.(st_controllogic) = cs'.(st_controllogic). +Proof. + induction l; intros; monadInv H0. + - trivial. + - apply H in EQ. rewrite EQ. eauto. +Qed. + +Lemma collect_datapath_trans : + forall A f l cs cs' ci, + (forall s s' x i y, f y s = OK x s' i -> s.(st_datapath) = s'.(st_datapath)) -> + @HTLMonadExtra.collectlist A f l cs = OK tt cs' ci -> cs.(st_datapath) = cs'.(st_datapath). +Proof. + induction l; intros; monadInv H0. + - trivial. + - apply H in EQ. rewrite EQ. eauto. +Qed. + +Lemma collect_freshreg_trans : + forall A f l cs cs' ci, + (forall s s' x i y, f y s = OK x s' i -> s.(st_freshreg) = s'.(st_freshreg)) -> + @HTLMonadExtra.collectlist A f l cs = OK tt cs' ci -> cs.(st_freshreg) = cs'.(st_freshreg). +Proof. + induction l; intros; monadInv H0. + - trivial. + - apply H in EQ. rewrite EQ. eauto. +Qed. + +Lemma collect_declare_controllogic_trans : + forall io n l s s' i, + HTLMonadExtra.collectlist (fun r : reg => declare_reg io r n) l s = OK tt s' i -> + s.(st_controllogic) = s'.(st_controllogic). +Proof. + intros. eapply collect_controllogic_trans; try eassumption. + intros. eapply declare_reg_controllogic_trans. simpl in H0. eassumption. +Qed. + +Lemma collect_declare_datapath_trans : + forall io n l s s' i, + HTLMonadExtra.collectlist (fun r : reg => declare_reg io r n) l s = OK tt s' i -> + s.(st_datapath) = s'.(st_datapath). +Proof. + intros. eapply collect_datapath_trans; try eassumption. + intros. eapply declare_reg_datapath_trans. simpl in H0. eassumption. +Qed. + +Lemma collect_declare_freshreg_trans : + forall io n l s s' i, + HTLMonadExtra.collectlist (fun r : reg => declare_reg io r n) l s = OK tt s' i -> + s.(st_freshreg) = s'.(st_freshreg). +Proof. + intros. eapply collect_freshreg_trans; try eassumption. + inversion 1. auto. +Qed. + +Ltac unfold_match H := + match type of H with + | context[match ?g with _ => _ end] => destruct g eqn:?; try discriminate + end. + +Lemma translate_eff_addressing_freshreg_trans : + forall op args s r s' i, + translate_eff_addressing op args s = OK r s' i -> + s.(st_freshreg) = s'.(st_freshreg). +Proof. + destruct op; intros; simpl in *; repeat (unfold_match H); inv H; auto. +Qed. +Hint Resolve translate_eff_addressing_freshreg_trans : htlspec. + +Lemma translate_comparison_freshreg_trans : + forall op args s r s' i, + translate_comparison op args s = OK r s' i -> + s.(st_freshreg) = s'.(st_freshreg). +Proof. + destruct op; intros; simpl in *; repeat (unfold_match H); inv H; auto. +Qed. +Hint Resolve translate_comparison_freshreg_trans : htlspec. + +Lemma translate_comparison_imm_freshreg_trans : + forall op args s r s' i n, + translate_comparison_imm op args n s = OK r s' i -> + s.(st_freshreg) = s'.(st_freshreg). +Proof. + destruct op; intros; simpl in *; repeat (unfold_match H); inv H; auto. +Qed. +Hint Resolve translate_comparison_imm_freshreg_trans : htlspec. + +Lemma translate_condition_freshreg_trans : + forall op args s r s' i, + translate_condition op args s = OK r s' i -> + s.(st_freshreg) = s'.(st_freshreg). +Proof. + destruct op; intros; simpl in *; repeat (unfold_match H); inv H; eauto with htlspec. +Qed. +Hint Resolve translate_condition_freshreg_trans : htlspec. + +Lemma translate_instr_freshreg_trans : + forall op args s r s' i, + translate_instr op args s = OK r s' i -> + s.(st_freshreg) = s'.(st_freshreg). +Proof. + destruct op; intros; simpl in *; repeat (unfold_match H); inv H; eauto with htlspec. + monadInv H1. eauto with htlspec. +Qed. +Hint Resolve translate_instr_freshreg_trans : htlspec. + +Lemma add_instr_freshreg_trans : + forall n n' st s r s' i, + add_instr n n' st s = OK r s' i -> + s.(st_freshreg) = s'.(st_freshreg). +Proof. intros. unfold add_instr in H. repeat (unfold_match H). inv H. auto. Qed. +Hint Resolve add_instr_freshreg_trans : htlspec. + +Lemma add_branch_instr_freshreg_trans : + forall n n0 n1 e s r s' i, + add_branch_instr e n n0 n1 s = OK r s' i -> + s.(st_freshreg) = s'.(st_freshreg). +Proof. intros. unfold add_branch_instr in H. repeat (unfold_match H). inv H. auto. Qed. +Hint Resolve add_branch_instr_freshreg_trans : htlspec. + +Lemma add_node_skip_freshreg_trans : + forall n1 n2 s r s' i, + add_node_skip n1 n2 s = OK r s' i -> + s.(st_freshreg) = s'.(st_freshreg). +Proof. intros. unfold add_node_skip in H. repeat (unfold_match H). inv H. auto. Qed. +Hint Resolve add_node_skip_freshreg_trans : htlspec. + +Lemma add_instr_skip_freshreg_trans : + forall n1 n2 s r s' i, + add_instr_skip n1 n2 s = OK r s' i -> + s.(st_freshreg) = s'.(st_freshreg). +Proof. intros. unfold add_instr_skip in H. repeat (unfold_match H). inv H. auto. Qed. +Hint Resolve add_instr_skip_freshreg_trans : htlspec. + +Lemma transf_instr_freshreg_trans : + forall fin ret st instr s v s' i, + transf_instr fin ret st instr s = OK v s' i -> + s.(st_freshreg) = s'.(st_freshreg). +Proof. + intros. destruct instr eqn:?. subst. unfold transf_instr in H. + destruct i0; try (monadInv H); try (unfold_match H); eauto with htlspec. + - apply add_instr_freshreg_trans in EQ2. apply translate_instr_freshreg_trans in EQ. + apply declare_reg_freshreg_trans in EQ1. congruence. + - apply add_instr_freshreg_trans in EQ2. apply translate_eff_addressing_freshreg_trans in EQ. + apply declare_reg_freshreg_trans in EQ1. congruence. + - apply add_instr_freshreg_trans in EQ0. apply translate_eff_addressing_freshreg_trans in EQ. + congruence. + - apply translate_condition_freshreg_trans in EQ. apply add_branch_instr_freshreg_trans in EQ0. + congruence. + - inv EQ. apply add_node_skip_freshreg_trans in EQ0. congruence. +Qed. +Hint Resolve transf_instr_freshreg_trans : htlspec. + +Lemma collect_trans_instr_freshreg_trans : + forall fin ret st l s s' i, + HTLMonadExtra.collectlist (transf_instr fin ret st) l s = OK tt s' i -> + s.(st_freshreg) = s'.(st_freshreg). +Proof. + intros. eapply collect_freshreg_trans; try eassumption. + eauto with htlspec. +Qed. + +Ltac rewrite_states := + match goal with + | [ H: ?x ?s = ?x ?s' |- _ ] => + let c1 := fresh "c" in + let c2 := fresh "c" in + remember (?x ?s) as c1; remember (?x ?s') as c2; try subst + end. + +Ltac inv_add_instr' H := + match type of H with + | ?f _ _ _ = OK _ _ _ => unfold f in H + | ?f _ _ _ _ = OK _ _ _ => unfold f in H + | ?f _ _ _ _ _ = OK _ _ _ => unfold f in H + end; repeat unfold_match H; inversion H. + +Ltac inv_add_instr := + lazymatch goal with + | H: context[add_instr_skip _ _ _] |- _ => + inv_add_instr' H + | H: context[add_instr_skip _ _] |- _ => + monadInv H; inv_incr; inv_add_instr + | H: context[add_instr _ _ _ _] |- _ => + inv_add_instr' H + | H: context[add_instr _ _ _] |- _ => + monadInv H; inv_incr; inv_add_instr + | H: context[add_branch_instr _ _ _ _ _] |- _ => + inv_add_instr' H + | H: context[add_branch_instr _ _ _ _] |- _ => + monadInv H; inv_incr; inv_add_instr + | H: context[add_node_skip _ _ _] |- _ => + inv_add_instr' H + | H: context[add_node_skip _ _] |- _ => + monadInv H; inv_incr; inv_add_instr + end. + +Ltac destruct_optional := + match goal with H: option ?r |- _ => destruct H end. + +Lemma iter_expand_instr_spec : + forall l fin rtrn stack s s' i x c, + HTLMonadExtra.collectlist (transf_instr fin rtrn stack) l s = OK x s' i -> + list_norepet (List.map fst l) -> + (forall pc instr, In (pc, instr) l -> c!pc = Some instr) -> + (forall pc instr, In (pc, instr) l -> + c!pc = Some instr -> + tr_code c pc instr s'.(st_datapath) s'.(st_controllogic) fin rtrn s'.(st_st) stack). +Proof. + induction l; simpl; intros; try contradiction. + destruct a as [pc1 instr1]; simpl in *. inv H0. monadInv H. inv_incr. + destruct (peq pc pc1). + - subst. + destruct instr1 eqn:?; try discriminate; + try destruct_optional; inv_add_instr; econstructor; try assumption. + + destruct o with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. + + destruct o0 with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. + + inversion H2. inversion H9. rewrite H. apply tr_instr_Inop. + eapply in_map with (f := fst) in H9. contradiction. + + + destruct o with pc1; destruct H16; simpl in *; rewrite AssocMap.gss in H14; eauto; congruence. + + destruct o0 with pc1; destruct H16; simpl in *; rewrite AssocMap.gss in H14; eauto; congruence. + + inversion H2. inversion H14. unfold nonblock. replace (st_st s4) with (st_st s2) by congruence. + econstructor. apply EQ1. eapply in_map with (f := fst) in H14. contradiction. + + + destruct o with pc1; destruct H16; simpl in *; rewrite AssocMap.gss in H14; eauto; congruence. + + destruct o0 with pc1; destruct H16; simpl in *; rewrite AssocMap.gss in H14; eauto; congruence. + + inversion H2. inversion H14. rewrite <- e2. replace (st_st s2) with (st_st s0) by congruence. + econstructor. apply EQ1. eapply in_map with (f := fst) in H14. contradiction. + + + destruct o with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. + + destruct o0 with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. + + destruct H2. + * inversion H2. + replace (st_st s2) with (st_st s0) by congruence. + eauto with htlspec. + * apply in_map with (f := fst) in H2. contradiction. + + + destruct o with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. + + destruct o0 with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. + + destruct H2. + * inversion H2. + replace (st_st s2) with (st_st s0) by congruence. + eauto with htlspec. + * apply in_map with (f := fst) in H2. contradiction. + + + destruct o with pc1; destruct H16; simpl in *; rewrite AssocMap.gss in H14; eauto; congruence. + + destruct o0 with pc1; destruct H16; simpl in *; rewrite AssocMap.gss in H14; eauto; congruence. + + inversion H2. + * inversion H14. constructor. congruence. + * apply in_map with (f := fst) in H14. contradiction. + + + destruct o with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. + + destruct o0 with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. + + inversion H2. + * inversion H9. + replace (st_st s2) with (st_st s0) by congruence. + eauto with htlspec. + * apply in_map with (f := fst) in H9. contradiction. + + + destruct o with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. + + destruct o0 with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. + + inversion H2. + * inversion H9. + replace (st_st s2) with (st_st s0) by congruence. + eauto with htlspec. + * apply in_map with (f := fst) in H9. contradiction. + + - eapply IHl. apply EQ0. assumption. + destruct H2. inversion H2. subst. contradiction. + intros. specialize H1 with pc0 instr0. destruct H1. tauto. trivial. + destruct H2. inv H2. contradiction. assumption. assumption. +Qed. +Hint Resolve iter_expand_instr_spec : htlspec. + +Lemma create_arr_inv : forall w x y z a b c d, + create_arr w x y z = OK (a, b) c d -> + y = b /\ a = z.(st_freshreg) /\ c.(st_freshreg) = Pos.succ (z.(st_freshreg)). +Proof. + inversion 1; split; auto. +Qed. + +Lemma create_reg_inv : forall a b s r s' i, + create_reg a b s = OK r s' i -> + r = s.(st_freshreg) /\ s'.(st_freshreg) = Pos.succ (s.(st_freshreg)). +Proof. + inversion 1; auto. +Qed. + +Theorem transl_module_correct : + forall f m, + transl_module f = Errors.OK m -> tr_module f m. +Proof. + intros until m. + unfold transl_module. + unfold run_mon. + destruct (transf_module f (max_state f)) eqn:?; try discriminate. + intros. inv H. + inversion s; subst. + + unfold transf_module in *. + unfold stack_correct in *. + destruct (0 <=? RTL.fn_stacksize f) eqn:STACK_BOUND_LOW; + destruct (RTL.fn_stacksize f Date: Mon, 6 Jul 2020 20:54:40 +0100 Subject: Check chunk size during translation. --- src/translation/HTLgenspec.v | 22 ++++++++++++++-------- 1 file changed, 14 insertions(+), 8 deletions(-) (limited to 'src/translation/HTLgenspec.v') diff --git a/src/translation/HTLgenspec.v b/src/translation/HTLgenspec.v index aba5d0c..dda91ca 100644 --- a/src/translation/HTLgenspec.v +++ b/src/translation/HTLgenspec.v @@ -138,16 +138,18 @@ Inductive tr_instr (fin rtrn st stk : reg) : RTL.instruction -> stmnt -> stmnt - tr_instr fin rtrn st stk (RTL.Ireturn (Some r)) (Vseq (block fin (Vlit (ZToValue 1%Z))) (block rtrn (Vvar r))) Vskip | tr_instr_Iload : - forall mem addr args s s' i e dst n, + forall chunk addr args s s' i e dst n, Z.pos n <= Int.max_unsigned -> + chunk = AST.Mint32 -> translate_eff_addressing addr args s = OK e s' i -> - tr_instr fin rtrn st stk (RTL.Iload mem addr args dst n) + tr_instr fin rtrn st stk (RTL.Iload chunk addr args dst n) (create_single_cycle_load stk e dst) (state_goto st n) | tr_instr_Istore : - forall mem addr args s s' i e src n, + forall chunk addr args s s' i e src n, Z.pos n <= Int.max_unsigned -> + chunk = AST.Mint32 -> translate_eff_addressing addr args s = OK e s' i -> - tr_instr fin rtrn st stk (RTL.Istore mem addr args src n) + tr_instr fin rtrn st stk (RTL.Istore chunk addr args src n) (create_single_cycle_store stk e src) (state_goto st n) | tr_instr_Ijumptable : forall cexpr tbl r, @@ -415,10 +417,12 @@ Proof. destruct i0; try (monadInv H); try (unfold_match H); eauto with htlspec. - monadInv H. apply add_instr_freshreg_trans in EQ2. apply translate_instr_freshreg_trans in EQ. apply declare_reg_freshreg_trans in EQ1. congruence. - - monadInv H. apply add_instr_freshreg_trans in EQ2. + - destruct (Z.pos n0 <=? Int.max_unsigned); try discriminate. + monadInv H. apply add_instr_freshreg_trans in EQ2. apply translate_eff_addressing_freshreg_trans in EQ. apply declare_reg_freshreg_trans in EQ1. congruence. - - monadInv H. apply add_instr_freshreg_trans in EQ0. + - destruct (Z.pos n0 <=? Int.max_unsigned); try discriminate. + monadInv H. apply add_instr_freshreg_trans in EQ0. apply translate_eff_addressing_freshreg_trans in EQ. congruence. - monadInv H. apply translate_condition_freshreg_trans in EQ. apply add_branch_instr_freshreg_trans in EQ0. @@ -491,7 +495,8 @@ Proof. destruct (peq pc pc1). - subst. destruct instr1 eqn:?; try discriminate; - try destruct_optional; inv_add_instr; econstructor; try assumption. + try destruct_optional; try (destruct m; try discriminate); + inv_add_instr; econstructor; try assumption. + destruct o with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. + destruct o0 with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. + inversion H2. inversion H9. rewrite H. apply tr_instr_Inop. @@ -508,6 +513,7 @@ Proof. + destruct o0 with pc1; destruct H16; simpl in *; rewrite AssocMap.gss in H14; eauto; congruence. + inversion H2. inversion H14. rewrite <- e2. replace (st_st s2) with (st_st s0) by congruence. econstructor. apply Z.leb_le; assumption. + reflexivity. apply EQ1. eapply in_map with (f := fst) in H14. contradiction. + destruct o with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. @@ -516,7 +522,7 @@ Proof. * inversion H2. replace (st_st s2) with (st_st s0) by congruence. econstructor. apply Z.leb_le; assumption. - eauto with htlspec. + eauto with htlspec. eassumption. * apply in_map with (f := fst) in H2. contradiction. + destruct o with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. -- cgit From b0e1a1383890d9b0a14ffaabce4c3d6453eb0a9c Mon Sep 17 00:00:00 2001 From: James Pollard Date: Mon, 6 Jul 2020 21:05:05 +0100 Subject: Reduce number of array addressing modes. --- src/translation/HTLgenspec.v | 17 +++++++++++++---- 1 file changed, 13 insertions(+), 4 deletions(-) (limited to 'src/translation/HTLgenspec.v') diff --git a/src/translation/HTLgenspec.v b/src/translation/HTLgenspec.v index dda91ca..1b04b1f 100644 --- a/src/translation/HTLgenspec.v +++ b/src/translation/HTLgenspec.v @@ -141,14 +141,14 @@ Inductive tr_instr (fin rtrn st stk : reg) : RTL.instruction -> stmnt -> stmnt - forall chunk addr args s s' i e dst n, Z.pos n <= Int.max_unsigned -> chunk = AST.Mint32 -> - translate_eff_addressing addr args s = OK e s' i -> + translate_arr_addressing addr args s = OK e s' i -> tr_instr fin rtrn st stk (RTL.Iload chunk addr args dst n) (create_single_cycle_load stk e dst) (state_goto st n) | tr_instr_Istore : forall chunk addr args s s' i e src n, Z.pos n <= Int.max_unsigned -> chunk = AST.Mint32 -> - translate_eff_addressing addr args s = OK e s' i -> + translate_arr_addressing addr args s = OK e s' i -> tr_instr fin rtrn st stk (RTL.Istore chunk addr args src n) (create_single_cycle_store stk e src) (state_goto st n) | tr_instr_Ijumptable : @@ -343,6 +343,15 @@ Proof. Qed. Hint Resolve translate_eff_addressing_freshreg_trans : htlspec. +Lemma translate_arr_addressing_freshreg_trans : + forall op args s r s' i, + translate_arr_addressing op args s = OK r s' i -> + s.(st_freshreg) = s'.(st_freshreg). +Proof. + destruct op; intros; simpl in *; repeat (unfold_match H); inv H; auto. +Qed. +Hint Resolve translate_eff_addressing_freshreg_trans : htlspec. + Lemma translate_comparison_freshreg_trans : forall op args s r s' i, translate_comparison op args s = OK r s' i -> @@ -419,11 +428,11 @@ Proof. apply declare_reg_freshreg_trans in EQ1. congruence. - destruct (Z.pos n0 <=? Int.max_unsigned); try discriminate. monadInv H. apply add_instr_freshreg_trans in EQ2. - apply translate_eff_addressing_freshreg_trans in EQ. + apply translate_arr_addressing_freshreg_trans in EQ. apply declare_reg_freshreg_trans in EQ1. congruence. - destruct (Z.pos n0 <=? Int.max_unsigned); try discriminate. monadInv H. apply add_instr_freshreg_trans in EQ0. - apply translate_eff_addressing_freshreg_trans in EQ. congruence. + apply translate_arr_addressing_freshreg_trans in EQ. congruence. - monadInv H. apply translate_condition_freshreg_trans in EQ. apply add_branch_instr_freshreg_trans in EQ0. congruence. -- cgit From fcb129725a68a052a079f882396be8e28142e1e0 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Tue, 7 Jul 2020 13:50:55 +0100 Subject: Only translate_cond left --- src/translation/HTLgenspec.v | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) (limited to 'src/translation/HTLgenspec.v') diff --git a/src/translation/HTLgenspec.v b/src/translation/HTLgenspec.v index f0508bd..71fb618 100644 --- a/src/translation/HTLgenspec.v +++ b/src/translation/HTLgenspec.v @@ -349,6 +349,15 @@ Proof. Qed. Hint Resolve translate_comparison_freshreg_trans : htlspec. +Lemma translate_comparisonu_freshreg_trans : + forall op args s r s' i, + translate_comparisonu op args s = OK r s' i -> + s.(st_freshreg) = s'.(st_freshreg). +Proof. + destruct op; intros; simpl in *; repeat (unfold_match H); inv H; auto. +Qed. +Hint Resolve translate_comparisonu_freshreg_trans : htlspec. + Lemma translate_comparison_imm_freshreg_trans : forall op args s r s' i n, translate_comparison_imm op args n s = OK r s' i -> @@ -358,6 +367,15 @@ Proof. Qed. Hint Resolve translate_comparison_imm_freshreg_trans : htlspec. +Lemma translate_comparison_immu_freshreg_trans : + forall op args s r s' i n, + translate_comparison_immu op args n s = OK r s' i -> + s.(st_freshreg) = s'.(st_freshreg). +Proof. + destruct op; intros; simpl in *; repeat (unfold_match H); inv H; auto. +Qed. +Hint Resolve translate_comparison_immu_freshreg_trans : htlspec. + Lemma translate_condition_freshreg_trans : forall op args s r s' i, translate_condition op args s = OK r s' i -> -- cgit