From 5ee912632a4ea43905dc210042679cac36204898 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Mon, 3 May 2021 19:24:58 +0100 Subject: Add admitted proof of translations in RTLPargen --- src/hls/RTLPargen.v | 204 +++++++++++++++++++++++++++++++++++++++++++++------- 1 file changed, 177 insertions(+), 27 deletions(-) (limited to 'src/hls/RTLPargen.v') diff --git a/src/hls/RTLPargen.v b/src/hls/RTLPargen.v index e2e9a90..0434893 100644 --- a/src/hls/RTLPargen.v +++ b/src/hls/RTLPargen.v @@ -19,7 +19,7 @@ Require Import compcert.backend.Registers. Require Import compcert.common.AST. Require Import compcert.common.Globalenvs. -Require compcert.common.Memory. +Require Import compcert.common.Memory. Require Import compcert.common.Values. Require Import compcert.lib.Floats. Require Import compcert.lib.Integers. @@ -246,7 +246,7 @@ the result of executing the expressions will be an expressions. Section SEMANTICS. -Context (A : Set) (genv : Genv.t A unit). +Context {A : Type} (genv : Genv.t A unit). Inductive sem_value : val -> sem_state -> expression -> val -> Prop := @@ -276,8 +276,8 @@ with sem_mem : Memory.Mem.storev chunk m' a v = Some m'' -> sem_mem sp st (Estore mem_exp chunk addr args val_exp) m'' | Sbase_mem : - forall st m sp, - sem_mem sp st (Ebase Mem) m + forall st sp, + sem_mem sp st (Ebase Mem) (sem_state_memory st) with sem_val_list : val -> sem_state -> expression_list -> list val -> Prop := | Snil : @@ -292,7 +292,7 @@ with sem_val_list : Inductive sem_regset : val -> sem_state -> forest -> regset -> Prop := | Sregset: - forall st f rs' sp, + forall st f sp rs', (forall x, sem_value sp st (f # (Reg x)) (Registers.Regmap.get x rs')) -> sem_regset sp st f rs'. @@ -460,6 +460,8 @@ Lemma ge_preserved_same: Proof. unfold ge_preserved; auto. Qed. Hint Resolve ge_preserved_same : rtlpar. +Ltac rtlpar_crush := crush; eauto with rtlpar. + Inductive sem_state_ld : sem_state -> sem_state -> Prop := | sem_state_ld_intro: forall rs rs' m m', @@ -471,15 +473,15 @@ Lemma sems_det: forall A ge tge sp st f, ge_preserved ge tge -> forall v v' mv mv', - (sem_value A ge sp st f v /\ sem_value A tge sp st f v' -> v = v') /\ - (sem_mem A ge sp st f mv /\ sem_mem A tge sp st f mv' -> mv = mv'). + (@sem_value A ge sp st f v /\ @sem_value A tge sp st f v' -> v = v') /\ + (@sem_mem A ge sp st f mv /\ @sem_mem A tge sp st f mv' -> mv = mv'). Proof. Admitted. Lemma sem_value_det: forall A ge tge sp st f v v', ge_preserved ge tge -> - sem_value A ge sp st f v -> - sem_value A tge sp st f v' -> + @sem_value A ge sp st f v -> + @sem_value A tge sp st f v' -> v = v'. Proof. intros; @@ -491,8 +493,8 @@ Hint Resolve sem_value_det : rtlpar. Lemma sem_value_det': forall FF ge sp s f v v', - sem_value FF ge sp s f v -> - sem_value FF ge sp s f v' -> + @sem_value FF ge sp s f v -> + @sem_value FF ge sp s f v' -> v = v'. Proof. simplify; eauto with rtlpar. @@ -501,8 +503,8 @@ Qed. Lemma sem_mem_det: forall A ge tge sp st f m m', ge_preserved ge tge -> - sem_mem A ge sp st f m -> - sem_mem A tge sp st f m' -> + @sem_mem A ge sp st f m -> + @sem_mem A tge sp st f m' -> m = m'. Proof. intros; @@ -513,8 +515,8 @@ Hint Resolve sem_mem_det : rtlpar. Lemma sem_mem_det': forall FF ge sp s f m m', - sem_mem FF ge sp s f m -> - sem_mem FF ge sp s f m' -> + @sem_mem FF ge sp s f m -> + @sem_mem FF ge sp s f m' -> m = m'. Proof. simplify; eauto with rtlpar. @@ -525,8 +527,8 @@ Hint Resolve Val.lessdef_same : rtlpar. Lemma sem_regset_det: forall FF ge tge sp st f v v', ge_preserved ge tge -> - sem_regset FF ge sp st f v -> - sem_regset FF tge sp st f v' -> + @sem_regset FF ge sp st f v -> + @sem_regset FF tge sp st f v' -> regs_lessdef v v'. Proof. intros; unfold regs_lessdef. @@ -538,8 +540,8 @@ Hint Resolve sem_regset_det : rtlpar. Lemma sem_det: forall FF ge tge sp st f st' st'', ge_preserved ge tge -> - sem FF ge sp st f st' -> - sem FF tge sp st f st'' -> + @sem FF ge sp st f st' -> + @sem FF tge sp st f st'' -> sem_state_ld st' st''. Proof. intros. @@ -551,8 +553,8 @@ Hint Resolve sem_det : rtlpar. Lemma sem_det': forall FF ge sp st f st' st'', - sem FF ge sp st f st' -> - sem FF ge sp st f st'' -> + @sem FF ge sp st f st' -> + @sem FF ge sp st f st'' -> sem_state_ld st' st''. Proof. eauto with rtlpar. Qed. @@ -588,7 +590,7 @@ Get a sequence from the basic block. Fixpoint abstract_sequence (f : forest) (b : list instr) : forest := match b with | nil => f - | i :: l => update (abstract_sequence f l) i + | i :: l => abstract_sequence (update f i) l end. (*| @@ -650,14 +652,162 @@ Abstract computations ===================== |*) +Definition is_regs i := match i with InstrState rs _ => rs end. +Definition is_mem i := match i with InstrState _ m => m end. + +Lemma regs_lessdef_refl r : regs_lessdef r r. +Proof. unfold regs_lessdef; auto using Val.lessdef_refl. Qed. + +Inductive state_lessdef : instr_state -> instr_state -> Prop := + state_lessdef_intro : + forall rs1 rs2 m1, + regs_lessdef rs1 rs2 -> + state_lessdef (InstrState rs1 m1) (InstrState rs2 m1). + +(*| +RTLBlock to abstract translation +-------------------------------- + +Correctness of translation from RTLBlock to the abstract interpretation language. +|*) + +Inductive match_abstr_st : instr_state -> sem_state -> Prop := +| match_abstr_st_intro : + forall m rs1 rs2, + regs_lessdef rs1 rs2 -> + match_abstr_st (InstrState rs1 m) (mk_sem_state rs2 m). + +Inductive match_abstr_st' : sem_state -> instr_state -> Prop := +| match_abstr_st'_intro : + forall m rs1 rs2, + regs_lessdef rs1 rs2 -> + match_abstr_st' (mk_sem_state rs1 m) (InstrState rs2 m). + +Inductive match_sem_st : sem_state -> sem_state -> Prop := +| match_sem_st_intro : + forall m rs1 rs2, + regs_lessdef rs1 rs2 -> + match_sem_st (mk_sem_state rs1 m) (mk_sem_state rs2 m). + +Definition tr_instr_state s := match s with InstrState r m => mk_sem_state r m end. +Definition tr_sem_state s := match s with mk_sem_state r m => InstrState r m end. + +Lemma tr_instr_state_eq s : tr_sem_state (tr_instr_state s) = s. +Proof. destruct s; auto. Qed. + +Lemma tr_sem_state_eq s : tr_instr_state (tr_sem_state s) = s. +Proof. destruct s; auto. Qed. + +Lemma tr_instr_state_ld st : match_abstr_st st (tr_instr_state st). +Proof. destruct st. constructor. apply regs_lessdef_refl. Qed. + +Lemma tr_sem_state_ld st : match_abstr_st (tr_sem_state st) st. +Proof. destruct st. constructor. apply regs_lessdef_refl. Qed. + +Lemma abstract_interp_empty A ge sp st : @sem A ge sp st empty st. +Proof. destruct st; repeat constructor. Qed. + +Lemma abstract_interp_empty3 : + forall A ge sp st st', + @sem A ge sp st empty st' -> + match_sem_st st st'. +Proof. + inversion 1; subst; simplify. + destruct st. inv H1. simplify. + constructor. unfold regs_lessdef. + intros. inv H0. + specialize (H1 r). inv H1. auto. +Qed. + +Lemma abstract_sequence_trans : + forall c A ge sp st1 st2 st2' st3 i, + @sem A ge sp st1 (update empty i) st2 -> + sem ge sp st2' (abstract_sequence empty c) st3 -> + match_sem_st st2 st2' -> + exists st3', sem ge sp st1 (abstract_sequence (update empty i) c) st3 + /\ match_sem_st st3 st3'. +Proof. + intros * UP RA MA. Admitted. + +Lemma rtlblock_trans_correct : + forall ge sp st bb st', + RTLBlock.step_instr_list ge sp st bb st' -> + exists sem_st', sem ge sp (tr_instr_state st) (abstract_sequence empty bb) sem_st' + /\ match_abstr_st st' sem_st'. +Proof. Admitted. + +Lemma rtlpar_trans_correct : + forall ge sp bb sem_st' sem_st, + sem ge sp sem_st (abstract_sequence empty (concat (concat bb))) sem_st' -> + exists st', RTLPar.step_instr_block ge sp (tr_sem_state sem_st) bb st' + /\ match_abstr_st' sem_st' st'. +Proof. Admitted. + +Lemma abstract_execution_correct': + forall A B ge tge sp sem_st' a a' sem_st tsem_st, + ge_preserved ge tge -> + check a a' = true -> + @sem A ge sp sem_st a sem_st' -> + match_sem_st sem_st tsem_st -> + exists tsem_st', @sem B tge sp tsem_st a' tsem_st' + /\ match_sem_st sem_st' tsem_st'. +Proof. Admitted. + +Lemma states_match : + forall st1 st2 st3 st4, + match_abstr_st st1 st2 -> + match_sem_st st2 st3 -> + match_abstr_st' st3 st4 -> + state_lessdef st1 st4. +Proof. + intros * H1 H2 H3; destruct st1; destruct st2; destruct st3; destruct st4. + inv H1. inv H2. inv H3; constructor. + unfold regs_lessdef in *. intros. + repeat match goal with + | H: forall _, _, r : positive |- _ => specialize (H r) + end. + eapply Val.lessdef_trans. eassumption. + eapply Val.lessdef_trans; eassumption. +Qed. + +Ltac inv_simp := + repeat match goal with + | H: exists _, _ |- _ => inv H + end; simplify. + +Lemma match_sem_st_refl r : match_sem_st r r. +Proof. destruct r; constructor; apply regs_lessdef_refl. Qed. + +Lemma state_lessdef_match_sem: + forall st tst, + state_lessdef st tst -> + match_sem_st (tr_instr_state st) (tr_instr_state tst). +Proof. + intros * H; destruct st; destruct tst; simplify; + inv H; constructor; auto. +Qed. + Lemma abstract_execution_correct: - forall bb bb' cfi ge tge sp rs m rs' m', + forall bb bb' cfi ge tge sp st st' tst, + RTLBlock.step_instr_list ge sp st bb st' -> ge_preserved ge tge -> schedule_oracle (mk_bblock bb cfi) (mk_bblock bb' cfi) = true -> - RTLBlock.step_instr_list ge sp (InstrState rs m) bb (InstrState rs' m') -> - exists rs'', RTLPar.step_instr_block tge sp (InstrState rs m) bb' (InstrState rs'' m') - /\ regs_lessdef rs' rs''. -Proof. Admitted. + state_lessdef st tst -> + exists tst', RTLPar.step_instr_block tge sp tst bb' tst' + /\ state_lessdef st' tst'. +Proof. + intros. + unfold schedule_oracle in *. simplify. + exploit rtlblock_trans_correct; try eassumption; []; inv_simp. + exploit abstract_execution_correct'; + try solve [eassumption | apply state_lessdef_match_sem; eassumption]; inv_simp. + exploit rtlpar_trans_correct; try eassumption; []; inv_simp. + econstructor; simplify. + match goal with + | H: context[tr_sem_state (tr_instr_state _)] |- _ => rewrite tr_instr_state_eq in H + end; eassumption. + eapply states_match; eauto. +Qed. (*| Top-level functions -- cgit From 61714e10c2ffe86acb8c148914ae1d8250630090 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Thu, 6 May 2021 09:39:58 +0100 Subject: Finish correctness of semantics wrt. RTBlock --- src/hls/RTLPargen.v | 411 +++++++++++++++++++++++++++++++++++++++++----------- 1 file changed, 327 insertions(+), 84 deletions(-) (limited to 'src/hls/RTLPargen.v') diff --git a/src/hls/RTLPargen.v b/src/hls/RTLPargen.v index 0434893..a94aa5f 100644 --- a/src/hls/RTLPargen.v +++ b/src/hls/RTLPargen.v @@ -234,11 +234,6 @@ Definition get_forest v f := Notation "a # b" := (get_forest b a) (at level 1). Notation "a # b <- c" := (Rtree.set b c a) (at level 1, b at next level). -Record sem_state := mk_sem_state { - sem_state_regset : regset; - sem_state_memory : Memory.mem - }. - (*| Finally we want to define the semantics of execution for the expressions with symbolic values, so the result of executing the expressions will be an expressions. @@ -249,15 +244,16 @@ Section SEMANTICS. Context {A : Type} (genv : Genv.t A unit). Inductive sem_value : - val -> sem_state -> expression -> val -> Prop := + val -> instr_state -> expression -> val -> Prop := | Sbase_reg: - forall sp st r, - sem_value sp st (Ebase (Reg r)) (Registers.Regmap.get r (sem_state_regset st)) + forall sp rs r m, + sem_value sp (InstrState rs m) (Ebase (Reg r)) (rs !! r) | Sop: - forall st op args v lv sp, - sem_val_list sp st args lv -> - Op.eval_operation genv sp op lv (sem_state_memory st) = Some v -> - sem_value sp st (Eop op args) v + forall rs m op args v lv sp m' mem_exp, + sem_mem sp (InstrState rs m) mem_exp m' -> + sem_val_list sp (InstrState rs m) args lv -> + Op.eval_operation genv sp op lv m' = Some v -> + sem_value sp (InstrState rs m) (Eop op args) v | Sload : forall st mem_exp addr chunk args a v m' lv sp, sem_mem sp st mem_exp m' -> @@ -266,7 +262,7 @@ Inductive sem_value : Memory.Mem.loadv chunk m' a = Some v -> sem_value sp st (Eload chunk addr args mem_exp) v with sem_mem : - val -> sem_state -> expression -> Memory.mem -> Prop := + val -> instr_state -> expression -> Memory.mem -> Prop := | Sstore : forall st mem_exp val_exp m'' addr v a m' chunk args lv sp, sem_mem sp st mem_exp m' -> @@ -276,10 +272,10 @@ with sem_mem : Memory.Mem.storev chunk m' a v = Some m'' -> sem_mem sp st (Estore mem_exp chunk addr args val_exp) m'' | Sbase_mem : - forall st sp, - sem_mem sp st (Ebase Mem) (sem_state_memory st) + forall rs m sp, + sem_mem sp (InstrState rs m) (Ebase Mem) m with sem_val_list : - val -> sem_state -> expression_list -> list val -> Prop := + val -> instr_state -> expression_list -> list val -> Prop := | Snil : forall st sp, sem_val_list sp st Enil nil @@ -290,19 +286,19 @@ with sem_val_list : sem_val_list sp st (Econs e l) (v :: lv). Inductive sem_regset : - val -> sem_state -> forest -> regset -> Prop := + val -> instr_state -> forest -> regset -> Prop := | Sregset: forall st f sp rs', (forall x, sem_value sp st (f # (Reg x)) (Registers.Regmap.get x rs')) -> sem_regset sp st f rs'. Inductive sem : - val -> sem_state -> forest -> sem_state -> Prop := + val -> instr_state -> forest -> instr_state -> Prop := | Sem: forall st rs' m' f sp, sem_regset sp st f rs' -> sem_mem sp st (f # Mem) m' -> - sem sp st f (mk_sem_state rs' m'). + sem sp st f (InstrState rs' m'). End SEMANTICS. @@ -450,8 +446,8 @@ Lemma tri1: Proof. crush. Qed. Definition ge_preserved {A B C D: Type} (ge: Genv.t A B) (tge: Genv.t C D) : Prop := - (forall sp op vl, Op.eval_operation ge sp op vl = - Op.eval_operation tge sp op vl) + (forall sp op vl m, Op.eval_operation ge sp op vl m = + Op.eval_operation tge sp op vl m) /\ (forall sp addr vl, Op.eval_addressing ge sp addr vl = Op.eval_addressing tge sp addr vl). @@ -462,12 +458,12 @@ Hint Resolve ge_preserved_same : rtlpar. Ltac rtlpar_crush := crush; eauto with rtlpar. -Inductive sem_state_ld : sem_state -> sem_state -> Prop := -| sem_state_ld_intro: +Inductive match_states : instr_state -> instr_state -> Prop := +| match_states_intro: forall rs rs' m m', - regs_lessdef rs rs' -> + (forall x, rs !! x = rs' !! x) -> m = m' -> - sem_state_ld (mk_sem_state rs m) (mk_sem_state rs' m'). + match_states (InstrState rs m) (InstrState rs' m'). Lemma sems_det: forall A ge tge sp st f, @@ -484,9 +480,9 @@ Lemma sem_value_det: @sem_value A tge sp st f v' -> v = v'. Proof. - intros; - generalize (sems_det A ge tge sp st f H v v' - st.(sem_state_memory) st.(sem_state_memory)); + intros. destruct st. + generalize (sems_det A ge tge sp (InstrState rs m) f H v v' + m m); crush. Qed. Hint Resolve sem_value_det : rtlpar. @@ -507,8 +503,8 @@ Lemma sem_mem_det: @sem_mem A tge sp st f m' -> m = m'. Proof. - intros; - generalize (sems_det A ge tge sp st f H sp sp m m'); + intros. destruct st. + generalize (sems_det A ge tge sp (InstrState rs m0) f H sp sp m m'); crush. Qed. Hint Resolve sem_mem_det : rtlpar. @@ -529,7 +525,7 @@ Lemma sem_regset_det: ge_preserved ge tge -> @sem_regset FF ge sp st f v -> @sem_regset FF tge sp st f v' -> - regs_lessdef v v'. + (forall x, v !! x = v' !! x). Proof. intros; unfold regs_lessdef. inv H0; inv H1; @@ -542,7 +538,7 @@ Lemma sem_det: ge_preserved ge tge -> @sem FF ge sp st f st' -> @sem FF tge sp st f st'' -> - sem_state_ld st' st''. + match_states st' st''. Proof. intros. destruct st; destruct st'; destruct st''. @@ -555,7 +551,7 @@ Lemma sem_det': forall FF ge sp st f st' st'', @sem FF ge sp st f st' -> @sem FF ge sp st f st'' -> - sem_state_ld st' st''. + match_states st' st''. Proof. eauto with rtlpar. Qed. (*| @@ -655,13 +651,10 @@ Abstract computations Definition is_regs i := match i with InstrState rs _ => rs end. Definition is_mem i := match i with InstrState _ m => m end. -Lemma regs_lessdef_refl r : regs_lessdef r r. -Proof. unfold regs_lessdef; auto using Val.lessdef_refl. Qed. - Inductive state_lessdef : instr_state -> instr_state -> Prop := state_lessdef_intro : forall rs1 rs2 m1, - regs_lessdef rs1 rs2 -> + (forall x, rs1 !! x = rs2 !! x) -> state_lessdef (InstrState rs1 m1) (InstrState rs2 m1). (*| @@ -671,38 +664,20 @@ RTLBlock to abstract translation Correctness of translation from RTLBlock to the abstract interpretation language. |*) -Inductive match_abstr_st : instr_state -> sem_state -> Prop := -| match_abstr_st_intro : - forall m rs1 rs2, - regs_lessdef rs1 rs2 -> - match_abstr_st (InstrState rs1 m) (mk_sem_state rs2 m). - -Inductive match_abstr_st' : sem_state -> instr_state -> Prop := -| match_abstr_st'_intro : - forall m rs1 rs2, - regs_lessdef rs1 rs2 -> - match_abstr_st' (mk_sem_state rs1 m) (InstrState rs2 m). +Lemma match_states_refl x : match_states x x. +Proof. destruct x; constructor; crush. Qed. -Inductive match_sem_st : sem_state -> sem_state -> Prop := -| match_sem_st_intro : - forall m rs1 rs2, - regs_lessdef rs1 rs2 -> - match_sem_st (mk_sem_state rs1 m) (mk_sem_state rs2 m). +Lemma match_states_commut x y : match_states x y -> match_states y x. +Proof. inversion 1; constructor; crush. Qed. -Definition tr_instr_state s := match s with InstrState r m => mk_sem_state r m end. -Definition tr_sem_state s := match s with mk_sem_state r m => InstrState r m end. +Lemma match_states_trans x y z : + match_states x y -> match_states y z -> match_states x z. +Proof. repeat inversion 1; constructor; crush. Qed. -Lemma tr_instr_state_eq s : tr_sem_state (tr_instr_state s) = s. -Proof. destruct s; auto. Qed. - -Lemma tr_sem_state_eq s : tr_instr_state (tr_sem_state s) = s. -Proof. destruct s; auto. Qed. - -Lemma tr_instr_state_ld st : match_abstr_st st (tr_instr_state st). -Proof. destruct st. constructor. apply regs_lessdef_refl. Qed. - -Lemma tr_sem_state_ld st : match_abstr_st (tr_sem_state st) st. -Proof. destruct st. constructor. apply regs_lessdef_refl. Qed. +Ltac inv_simp := + repeat match goal with + | H: exists _, _ |- _ => inv H + end; simplify. Lemma abstract_interp_empty A ge sp st : @sem A ge sp st empty st. Proof. destruct st; repeat constructor. Qed. @@ -710,31 +685,304 @@ Proof. destruct st; repeat constructor. Qed. Lemma abstract_interp_empty3 : forall A ge sp st st', @sem A ge sp st empty st' -> - match_sem_st st st'. + match_states st st'. Proof. inversion 1; subst; simplify. destruct st. inv H1. simplify. constructor. unfold regs_lessdef. - intros. inv H0. - specialize (H1 r). inv H1. auto. + intros. inv H0. specialize (H1 x). inv H1; auto. + auto. Qed. +Lemma abstract_sequence_run : + forall A ge sp tst st i st', + @step_instr A ge sp st i st' -> + match_states st tst -> + exists tst', sem ge sp tst (update empty i) tst' + /\ match_states st' tst'. +Proof. +Admitted. + +Lemma match_start_state : + forall b A ge sp st1 st2, + @sem A ge sp st1 b st2 -> + forall st1', + match_states st1 st1' -> + sem ge sp st1' b st2. +Proof. + Admitted. + Lemma abstract_sequence_trans : - forall c A ge sp st1 st2 st2' st3 i, + forall i c A ge sp st1 st2 st2' st3, @sem A ge sp st1 (update empty i) st2 -> sem ge sp st2' (abstract_sequence empty c) st3 -> - match_sem_st st2 st2' -> - exists st3', sem ge sp st1 (abstract_sequence (update empty i) c) st3 - /\ match_sem_st st3 st3'. + match_states st2 st2' -> + sem ge sp st1 (abstract_sequence empty (i :: c)) st3. +Proof. + induction i. simplify. apply abstract_interp_empty3 in H. + eapply match_states_trans in H1; eauto. eapply match_start_state. + apply H0. apply match_states_commut. auto. + { simplify. inv H. inv H3. inv H2. destruct st3. constructor. + constructor. intros. specialize (H x). inv H1. specialize (H4 x). + rewrite H4 in *. inv H0. inv H7. specialize (H0 x). admit. + inv H1. admit. + } + { admit. + } + { admit. + } Admitted. + +Definition check_dest i r' := + match i with + | RBop p op rl r => (r =? r')%positive + | RBload p chunk addr rl r => (r =? r')%positive + | _ => false + end. + +Lemma check_dest_dec i r : {check_dest i r = true} + {check_dest i r = false}. +Proof. destruct (check_dest i r); tauto. Qed. + +Fixpoint check_dest_l l r := + match l with + | nil => false + | a :: b => check_dest a r || check_dest_l b r + end. + +Lemma check_dest_l_forall : + forall l r, + check_dest_l l r = false -> + Forall (fun x => check_dest x r = false) l. +Proof. induction l; crush. Qed. + +Lemma check_dest_l_ex : + forall l r, + check_dest_l l r = true -> + exists a, In a l /\ check_dest a r = true. +Proof. + induction l; crush. + destruct (check_dest a r) eqn:?; try solve [econstructor; crush]. + simplify. + exploit IHl. apply H. inv_simp. econstructor. simplify. right. eassumption. + auto. +Qed. + +Lemma check_dest_l_dec i r : {check_dest_l i r = true} + {check_dest_l i r = false}. +Proof. destruct (check_dest_l i r); tauto. Qed. + +Lemma check_dest_l_dec2 l r : + {Forall (fun x => check_dest x r = false) l} + + {exists a, In a l /\ check_dest a r = true}. +Proof. + destruct (check_dest_l_dec l r); [right | left]; + auto using check_dest_l_ex, check_dest_l_forall. +Qed. + +Lemma check_dest_l_forall2 : + forall l r, + Forall (fun x => check_dest x r = false) l -> + check_dest_l l r = false. +Proof. + induction l; crush. + inv H. apply orb_false_intro; crush. +Qed. + +Lemma check_dest_l_ex2 : + forall l r, + (exists a, In a l /\ check_dest a r = true) -> + check_dest_l l r = true. +Proof. + induction l; crush. + specialize (IHl r). inv H. + apply orb_true_intro; crush. + apply orb_true_intro; crush. + right. apply IHl. exists x. auto. +Qed. + +Lemma check_dest_update : + forall f i r, + check_dest i r = false -> + (update f i) # (Reg r) = f # (Reg r). +Proof. + destruct i; crush; try apply Pos.eqb_neq in H; apply genmap1; crush. +Qed. + +Lemma check_dest_update2 : + forall f r rl op p, + (update f (RBop p op rl r)) # (Reg r) = Eop op (list_translation rl f). +Proof. crush; rewrite map2; auto. Qed. + +Lemma check_dest_update3 : + forall f r rl p addr chunk, + (update f (RBload p chunk addr rl r)) # (Reg r) = Eload chunk addr (list_translation rl f) (f # Mem). +Proof. crush; rewrite map2; auto. Qed. + +Lemma abstr_comp : + forall l i f x x0, + abstract_sequence f (l ++ i :: nil) = x -> + abstract_sequence f l = x0 -> + x = update x0 i. +Proof. induction l; intros; crush; eapply IHl; eauto. Qed. + +Lemma abstract_seq : + forall l f i, + abstract_sequence f (l ++ i :: nil) = update (abstract_sequence f l) i. +Proof. induction l; crush. Qed. + +Lemma check_list_l_false : + forall l x r, + check_dest_l (l ++ x :: nil) r = false -> + check_dest_l l r = false /\ check_dest x r = false. +Proof. + simplify. + apply check_dest_l_forall in H. apply Forall_app in H. + simplify. apply check_dest_l_forall2; auto. + apply check_dest_l_forall in H. apply Forall_app in H. + simplify. inv H1. auto. +Qed. + +Lemma check_list_l_true : + forall l x r, + check_dest_l (l ++ x :: nil) r = true -> + check_dest_l l r = true \/ check_dest x r = true. +Proof. + simplify. + apply check_dest_l_ex in H; inv_simp. + apply in_app_or in H. inv H. left. + apply check_dest_l_ex2. exists x0. auto. + inv H0; auto. +Qed. + +Lemma abstract_sequence_update : + forall l r f, + check_dest_l l r = false -> + (abstract_sequence f l) # (Reg r) = f # (Reg r). +Proof. + induction l using rev_ind; crush. + rewrite abstract_seq. rewrite check_dest_update. apply IHl. + apply check_list_l_false in H. tauto. + apply check_list_l_false in H. tauto. +Qed. + +Lemma rtlblock_trans_correct' : + forall bb ge sp st x st'', + RTLBlock.step_instr_list ge sp st (bb ++ x :: nil) st'' -> + exists st', RTLBlock.step_instr_list ge sp st bb st' + /\ step_instr ge sp st' x st''. +Proof. + induction bb. + crush. exists st. + split. constructor. inv H. inv H6. auto. + crush. inv H. exploit IHbb. eassumption. inv_simp. + econstructor. split. + econstructor; eauto. eauto. +Qed. + +Lemma sem_update_RBnop : + forall A ge sp st f st', + @sem A ge sp st f st' -> sem ge sp st (update f RBnop) st'. +Proof. crush. Qed. + +Lemma gen_list_base: + forall FF ge sp l rs exps st1, + (forall x, @sem_value FF ge sp st1 (exps # (Reg x)) (rs !! x)) -> + sem_val_list ge sp st1 (list_translation l exps) rs ## l. Proof. - intros * UP RA MA. Admitted. + induction l. + intros. simpl. constructor. + intros. simpl. eapply Scons; eauto. +Qed. + +Lemma abstract_seq_correct_aux: + forall FF ge sp i st1 st2 st3 f, + @step_instr FF ge sp st3 i st2 -> + sem ge sp st1 f st3 -> + sem ge sp st1 (update f i) st2. +Proof. + intros; inv H; simplify. + { simplify; eauto. } (*apply match_states_refl. }*) + { inv H0. inv H6. destruct st1. econstructor. simplify. + constructor. intros. + destruct (resource_eq (Reg res) (Reg x)). inv e. + rewrite map2. econstructor. eassumption. apply gen_list_base; eauto. + rewrite Regmap.gss. eauto. + assert (res <> x). { unfold not in *. intros. apply n. rewrite H0. auto. } + rewrite Regmap.gso by auto. + rewrite genmap1 by auto. auto. + + rewrite genmap1; crush. } + { inv H0. inv H7. constructor. constructor. intros. + destruct (Pos.eq_dec dst x); subst. + rewrite map2. econstructor; eauto. + apply gen_list_base. auto. rewrite Regmap.gss. auto. + rewrite genmap1. rewrite Regmap.gso by auto. auto. + unfold not in *; intros. inv H0. auto. + rewrite genmap1; crush. + } + { inv H0. inv H7. constructor. constructor; intros. + rewrite genmap1; crush. + rewrite map2. econstructor; eauto. + apply gen_list_base; auto. + } +Qed. + +Lemma list_translate: + forall l A ge sp rs1 m0 f rs0 m rs o0 v, + @sem A ge sp (InstrState rs1 m0) f (InstrState rs0 m) -> + Op.eval_operation ge sp o0 (rs ## l) m = Some v -> + (forall r, rs0 !! r = rs !! r) -> + sem_val_list ge sp (InstrState rs1 m0) (list_translation l f) (rs ## l). +Proof. + intros. + destruct l. simplify; constructor. + constructor; simplify. + +Lemma sem_update_Op : + forall A ge sp st f st' r l o0 o m rs v, + @sem A ge sp st f st' -> + Op.eval_operation ge sp o0 rs ## l m = Some v -> + match_states st' (InstrState rs m) -> + exists tst, + sem ge sp st (update f (RBop o o0 l r)) tst /\ match_states (InstrState (Regmap.set r v rs) m) tst. +Proof. + intros. inv H1. simplify. + destruct st. + econstructor. simplify. + constructor. constructor. intros. destruct (Pos.eq_dec x r); subst. specialize (H5 r). + rewrite map2. econstructor. + +Lemma sem_update : + forall A ge sp st x st' st'' st''' f, + sem ge sp st f st' -> + match_states st' st''' -> + @step_instr A ge sp st''' x st'' -> + exists tst, sem ge sp st (update f x) tst /\ match_states st'' tst. +Proof. + intros. destruct x. + { inv H1. + econstructor. split. + apply sem_update_RBnop. eassumption. + apply match_states_commut. auto. } + { inv H1. Lemma rtlblock_trans_correct : - forall ge sp st bb st', - RTLBlock.step_instr_list ge sp st bb st' -> - exists sem_st', sem ge sp (tr_instr_state st) (abstract_sequence empty bb) sem_st' - /\ match_abstr_st st' sem_st'. -Proof. Admitted. + forall bb ge sp st st', + RTLBlock.step_instr_list ge sp st bb st' -> + forall tst, + match_states st tst -> + exists tst', sem ge sp tst (abstract_sequence empty bb) tst' + /\ match_states st' tst'. +Proof. + induction bb using rev_ind; simplify. + { econstructor. simplify. apply abstract_interp_empty. + inv H. auto. } + { apply rtlblock_trans_correct' in H. inv_simp. + rewrite abstract_seq. + exploit IHbb; try eassumption; []; inv_simp. + exploit sem_update. apply H1. apply match_states_commut; eassumption. + eauto. inv_simp. econstructor. split. apply H3. + auto. + } +Qed. Lemma rtlpar_trans_correct : forall ge sp bb sem_st' sem_st, @@ -770,11 +1018,6 @@ Proof. eapply Val.lessdef_trans; eassumption. Qed. -Ltac inv_simp := - repeat match goal with - | H: exists _, _ |- _ => inv H - end; simplify. - Lemma match_sem_st_refl r : match_sem_st r r. Proof. destruct r; constructor; apply regs_lessdef_refl. Qed. -- cgit From d7230c6c5c332ce4767e8300f652f8f17dae7850 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Mon, 10 May 2021 20:36:03 +0100 Subject: Fix admitted in first proof of sem. preservation --- src/hls/RTLPargen.v | 87 +++++++++++++++++++++++++++++++++++++++++------------ 1 file changed, 68 insertions(+), 19 deletions(-) (limited to 'src/hls/RTLPargen.v') diff --git a/src/hls/RTLPargen.v b/src/hls/RTLPargen.v index a94aa5f..75d8130 100644 --- a/src/hls/RTLPargen.v +++ b/src/hls/RTLPargen.v @@ -925,16 +925,11 @@ Proof. } Qed. -Lemma list_translate: - forall l A ge sp rs1 m0 f rs0 m rs o0 v, - @sem A ge sp (InstrState rs1 m0) f (InstrState rs0 m) -> - Op.eval_operation ge sp o0 (rs ## l) m = Some v -> - (forall r, rs0 !! r = rs !! r) -> - sem_val_list ge sp (InstrState rs1 m0) (list_translation l f) (rs ## l). -Proof. - intros. - destruct l. simplify; constructor. - constructor; simplify. +Lemma regmap_list_equiv : + forall A (rs1: Regmap.t A) rs2, + (forall x, rs1 !! x = rs2 !! x) -> + forall rl, rs1##rl = rs2##rl. +Proof. induction rl; crush. Qed. Lemma sem_update_Op : forall A ge sp st f st' r l o0 o m rs v, @@ -947,8 +942,61 @@ Proof. intros. inv H1. simplify. destruct st. econstructor. simplify. - constructor. constructor. intros. destruct (Pos.eq_dec x r); subst. specialize (H5 r). - rewrite map2. econstructor. + { constructor. + { constructor. intros. destruct (Pos.eq_dec x r); subst. + { pose proof (H5 r). rewrite map2. pose proof H. inv H. econstructor; eauto. + { inv H9. eapply gen_list_base; eauto. } + { instantiate (1 := (Regmap.set r v rs0)). rewrite Regmap.gss. erewrite regmap_list_equiv; eauto. } } + { rewrite Regmap.gso by auto. rewrite genmap1; crush. inv H. inv H7; eauto. } } + { inv H. rewrite genmap1; crush. eauto. } } + { constructor; eauto. intros. + destruct (Pos.eq_dec r x); + subst; [repeat rewrite Regmap.gss | repeat rewrite Regmap.gso]; auto. } +Qed. + +Lemma sem_update_load : + forall A ge sp st f st' r o m a l m0 rs v a0, + @sem A ge sp st f st' -> + Op.eval_addressing ge sp a rs ## l = Some a0 -> + Mem.loadv m m0 a0 = Some v -> + match_states st' (InstrState rs m0) -> + exists tst : instr_state, + sem ge sp st (update f (RBload o m a l r)) tst + /\ match_states (InstrState (Regmap.set r v rs) m0) tst. +Proof. + intros. inv H2. pose proof H. inv H. inv H9. + destruct st. + econstructor; simplify. + { constructor. + { constructor. intros. + destruct (Pos.eq_dec x r); subst. + { rewrite map2. econstructor; eauto. eapply gen_list_base. intros. + rewrite <- H6. eauto. + instantiate (1 := (Regmap.set r v rs0)). rewrite Regmap.gss. auto. } + { rewrite Regmap.gso by auto. rewrite genmap1; crush. } } + { rewrite genmap1; crush. eauto. } } + { constructor; auto; intros. destruct (Pos.eq_dec r x); + subst; [repeat rewrite Regmap.gss | repeat rewrite Regmap.gso]; auto. } +Qed. + +Lemma sem_update_store : + forall A ge sp a0 m a l r o f st m' rs m0 st', + @sem A ge sp st f st' -> + Op.eval_addressing ge sp a rs ## l = Some a0 -> + Mem.storev m m0 a0 rs !! r = Some m' -> + match_states st' (InstrState rs m0) -> + exists tst, sem ge sp st (update f (RBstore o m a l r)) tst + /\ match_states (InstrState rs m') tst. +Proof. + intros. inv H2. pose proof H. inv H. inv H9. + destruct st. + econstructor; simplify. + { econstructor. + { econstructor; intros. rewrite genmap1; crush. } + { rewrite map2. econstructor; eauto. eapply gen_list_base. intros. rewrite <- H6. + eauto. specialize (H6 r). rewrite H6. eauto. } } + { econstructor; eauto. } +Qed. Lemma sem_update : forall A ge sp st x st' st'' st''' f, @@ -957,12 +1005,14 @@ Lemma sem_update : @step_instr A ge sp st''' x st'' -> exists tst, sem ge sp st (update f x) tst /\ match_states st'' tst. Proof. - intros. destruct x. - { inv H1. - econstructor. split. + intros. destruct x; inv H1. + { econstructor. split. apply sem_update_RBnop. eassumption. apply match_states_commut. auto. } - { inv H1. + { eapply sem_update_Op; eauto. } + { eapply sem_update_load; eauto. } + { eapply sem_update_store; eauto. } +Qed. Lemma rtlblock_trans_correct : forall bb ge sp st st', @@ -974,14 +1024,13 @@ Lemma rtlblock_trans_correct : Proof. induction bb using rev_ind; simplify. { econstructor. simplify. apply abstract_interp_empty. - inv H. auto. } + inv H. auto. } { apply rtlblock_trans_correct' in H. inv_simp. rewrite abstract_seq. exploit IHbb; try eassumption; []; inv_simp. exploit sem_update. apply H1. apply match_states_commut; eassumption. eauto. inv_simp. econstructor. split. apply H3. - auto. - } + auto. } Qed. Lemma rtlpar_trans_correct : -- cgit From 47181b44f21736431419bf977132e9f4f0ea1ba4 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Wed, 12 May 2021 22:07:08 +0100 Subject: Finish abstract interpretation --- src/hls/RTLPargen.v | 274 ++++++++++++++++++++++++++++++++++++++-------------- 1 file changed, 199 insertions(+), 75 deletions(-) (limited to 'src/hls/RTLPargen.v') diff --git a/src/hls/RTLPargen.v b/src/hls/RTLPargen.v index 75d8130..f64a796 100644 --- a/src/hls/RTLPargen.v +++ b/src/hls/RTLPargen.v @@ -207,7 +207,7 @@ that enables mutual recursive definitions over the datatypes. Inductive expression : Set := | Ebase : resource -> expression -| Eop : Op.operation -> expression_list -> expression +| Eop : Op.operation -> expression_list -> expression -> expression | Eload : AST.memory_chunk -> Op.addressing -> expression_list -> expression -> expression | Estore : expression -> AST.memory_chunk -> Op.addressing -> expression_list -> expression -> expression with expression_list : Set := @@ -253,7 +253,7 @@ Inductive sem_value : sem_mem sp (InstrState rs m) mem_exp m' -> sem_val_list sp (InstrState rs m) args lv -> Op.eval_operation genv sp op lv m' = Some v -> - sem_value sp (InstrState rs m) (Eop op args) v + sem_value sp (InstrState rs m) (Eop op args mem_exp) v | Sload : forall st mem_exp addr chunk args a v m' lv sp, sem_mem sp st mem_exp m' -> @@ -305,8 +305,10 @@ End SEMANTICS. Fixpoint beq_expression (e1 e2: expression) {struct e1}: bool := match e1, e2 with | Ebase r1, Ebase r2 => if resource_eq r1 r2 then true else false - | Eop op1 el1, Eop op2 el2 => - if operation_eq op1 op2 then beq_expression_list el1 el2 else false + | Eop op1 el1 exp1, Eop op2 el2 exp2 => + if operation_eq op1 op2 then + if beq_expression exp1 exp2 then + beq_expression_list el1 el2 else false else false | Eload chk1 addr1 el1 e1, Eload chk2 addr2 el2 e2 => if memory_chunk_eq chk1 chk2 then if addressing_eq addr1 addr2 @@ -353,7 +355,7 @@ This function checks if all the elements in [fa] are in [fb], but not the other Definition check := Rtree.beq beq_expression. -Lemma check_correct: forall (fa fb : forest) (x : resource), +Lemma check_correct: forall (fa fb : forest), check fa fb = true -> (forall x, fa # x = fb # x). Proof. unfold check, get_forest; intros; @@ -568,7 +570,7 @@ Definition update (f : forest) (i : instr) : forest := match i with | RBnop => f | RBop p op rl r => - f # (Reg r) <- (Eop op (list_translation rl f)) + f # (Reg r) <- (Eop op (list_translation rl f) (f # Mem)) | RBload p chunk addr rl r => f # (Reg r) <- (Eload chunk addr (list_translation rl f) (f # Mem)) | RBstore p chunk addr rl r => @@ -694,44 +696,6 @@ Proof. auto. Qed. -Lemma abstract_sequence_run : - forall A ge sp tst st i st', - @step_instr A ge sp st i st' -> - match_states st tst -> - exists tst', sem ge sp tst (update empty i) tst' - /\ match_states st' tst'. -Proof. -Admitted. - -Lemma match_start_state : - forall b A ge sp st1 st2, - @sem A ge sp st1 b st2 -> - forall st1', - match_states st1 st1' -> - sem ge sp st1' b st2. -Proof. - Admitted. - -Lemma abstract_sequence_trans : - forall i c A ge sp st1 st2 st2' st3, - @sem A ge sp st1 (update empty i) st2 -> - sem ge sp st2' (abstract_sequence empty c) st3 -> - match_states st2 st2' -> - sem ge sp st1 (abstract_sequence empty (i :: c)) st3. -Proof. - induction i. simplify. apply abstract_interp_empty3 in H. - eapply match_states_trans in H1; eauto. eapply match_start_state. - apply H0. apply match_states_commut. auto. - { simplify. inv H. inv H3. inv H2. destruct st3. constructor. - constructor. intros. specialize (H x). inv H1. specialize (H4 x). - rewrite H4 in *. inv H0. inv H7. specialize (H0 x). admit. - inv H1. admit. - } - { admit. - } - { admit. - } Admitted. - Definition check_dest i r' := match i with | RBop p op rl r => (r =? r')%positive @@ -808,7 +772,7 @@ Qed. Lemma check_dest_update2 : forall f r rl op p, - (update f (RBop p op rl r)) # (Reg r) = Eop op (list_translation rl f). + (update f (RBop p op rl r)) # (Reg r) = Eop op (list_translation rl f) (f # Mem). Proof. crush; rewrite map2; auto. Qed. Lemma check_dest_update3 : @@ -1036,26 +1000,118 @@ Qed. Lemma rtlpar_trans_correct : forall ge sp bb sem_st' sem_st, sem ge sp sem_st (abstract_sequence empty (concat (concat bb))) sem_st' -> - exists st', RTLPar.step_instr_block ge sp (tr_sem_state sem_st) bb st' - /\ match_abstr_st' sem_st' st'. + exists st', RTLPar.step_instr_block ge sp sem_st bb st' + /\ match_states sem_st' st'. Proof. Admitted. +Lemma abstr_sem_val_mem : + forall A B ge tge st tst sp a, + ge_preserved ge tge -> + forall v m, + (@sem_mem A ge sp st a m /\ match_states st tst -> @sem_mem B tge sp tst a m) /\ + (@sem_value A ge sp st a v /\ match_states st tst -> @sem_value B tge sp tst a v). +Proof. + intros * H. + apply expression_ind2 with + + (P := fun (e1: expression) => + forall v m, + (@sem_mem A ge sp st e1 m /\ match_states st tst -> @sem_mem B tge sp tst e1 m) /\ + (@sem_value A ge sp st e1 v /\ match_states st tst -> @sem_value B tge sp tst e1 v)) + + (P0 := fun (e1: expression_list) => + forall lv, @sem_val_list A ge sp st e1 lv /\ match_states st tst -> @sem_val_list B tge sp tst e1 lv); + simplify; intros; simplify. + { inv H1. inv H2. constructor. } + { inv H2. inv H1. rewrite H0. constructor. } + { inv H3. } + { inv H3. inv H4. econstructor. apply H1; auto. simplify. eauto. constructor. auto. auto. + apply H0; simplify; eauto. constructor; eauto. + unfold ge_preserved in *. simplify. rewrite <- H2. auto. + } + { inv H3. } + { inv H3. inv H4. econstructor. apply H1; eauto; simplify; eauto. constructor; eauto. + apply H0; simplify; eauto. constructor; eauto. + inv H. rewrite <- H4. eauto. + auto. + } + { inv H4. inv H5. econstructor. apply H0; eauto. simplify; eauto. constructor; eauto. + apply H2; eauto. simplify; eauto. constructor; eauto. + apply H1; eauto. simplify; eauto. constructor; eauto. + inv H. rewrite <- H5. eauto. auto. + } + { inv H4. } + { inv H1. constructor. } + { inv H3. constructor; auto. apply H0; eauto. apply Mem.empty. } +Qed. + +Lemma abstr_sem_value : + forall a A B ge tge sp st tst v, + @sem_value A ge sp st a v -> + ge_preserved ge tge -> + match_states st tst -> + @sem_value B tge sp tst a v. +Proof. intros; eapply abstr_sem_val_mem; eauto; apply Mem.empty. Qed. + +Lemma abstr_sem_mem : + forall a A B ge tge sp st tst v, + @sem_mem A ge sp st a v -> + ge_preserved ge tge -> + match_states st tst -> + @sem_mem B tge sp tst a v. +Proof. intros; eapply abstr_sem_val_mem; eauto. Qed. + +Lemma abstr_sem_regset : + forall a a' A B ge tge sp st tst rs, + @sem_regset A ge sp st a rs -> + ge_preserved ge tge -> + (forall x, a # x = a' # x) -> + match_states st tst -> + exists rs', @sem_regset B tge sp tst a' rs' /\ (forall x, rs !! x = rs' !! x). +Proof. + inversion 1; intros. + inv H7. + econstructor. simplify. econstructor. intros. + eapply abstr_sem_value; eauto. rewrite <- H6. + eapply H0. constructor; eauto. + auto. +Qed. + +Lemma abstr_sem : + forall a a' A B ge tge sp st tst st', + @sem A ge sp st a st' -> + ge_preserved ge tge -> + (forall x, a # x = a' # x) -> + match_states st tst -> + exists tst', @sem B tge sp tst a' tst' /\ match_states st' tst'. +Proof. + inversion 1; subst; intros. + inversion H4; subst. + exploit abstr_sem_regset; eauto; inv_simp. + do 3 econstructor; eauto. + rewrite <- H3. + eapply abstr_sem_mem; eauto. +Qed. + Lemma abstract_execution_correct': - forall A B ge tge sp sem_st' a a' sem_st tsem_st, + forall A B ge tge sp st' a a' st tst, + @sem A ge sp st a st' -> ge_preserved ge tge -> check a a' = true -> - @sem A ge sp sem_st a sem_st' -> - match_sem_st sem_st tsem_st -> - exists tsem_st', @sem B tge sp tsem_st a' tsem_st' - /\ match_sem_st sem_st' tsem_st'. -Proof. Admitted. + match_states st tst -> + exists tst', @sem B tge sp tst a' tst' /\ match_states st' tst'. +Proof. + intros; + pose proof (check_correct a a' H1); + eapply abstr_sem; eauto. +Qed. Lemma states_match : forall st1 st2 st3 st4, - match_abstr_st st1 st2 -> - match_sem_st st2 st3 -> - match_abstr_st' st3 st4 -> - state_lessdef st1 st4. + match_states st1 st2 -> + match_states st2 st3 -> + match_states st3 st4 -> + match_states st1 st4. Proof. intros * H1 H2 H3; destruct st1; destruct st2; destruct st3; destruct st4. inv H1. inv H2. inv H3; constructor. @@ -1063,20 +1119,88 @@ Proof. repeat match goal with | H: forall _, _, r : positive |- _ => specialize (H r) end. - eapply Val.lessdef_trans. eassumption. - eapply Val.lessdef_trans; eassumption. + congruence. + auto. +Qed. + +Lemma step_instr_block_same : + forall ge sp st st', + step_instr_block ge sp st nil st' -> + st = st'. +Proof. inversion 1; auto. Qed. + +Lemma step_instr_seq_same : + forall ge sp st st', + step_instr_seq ge sp st nil st' -> + st = st'. +Proof. inversion 1; auto. Qed. + +Lemma match_states_list : + forall A (rs: Regmap.t A) rs', + (forall r, rs !! r = rs' !! r) -> + forall l, rs ## l = rs' ## l. +Proof. induction l; crush. Qed. + +Lemma PTree_matches : + forall A (v: A) res rs rs', + (forall r, rs !! r = rs' !! r) -> + forall x, (Regmap.set res v rs) !! x = (Regmap.set res v rs') !! x. +Proof. + intros; destruct (Pos.eq_dec x res); subst; + [ repeat rewrite Regmap.gss by auto + | repeat rewrite Regmap.gso by auto ]; auto. Qed. -Lemma match_sem_st_refl r : match_sem_st r r. -Proof. destruct r; constructor; apply regs_lessdef_refl. Qed. +Lemma step_instr_matches : + forall A a ge sp st st', + @step_instr A ge sp st a st' -> + forall tst, match_states st tst -> + exists tst', step_instr ge sp tst a tst' + /\ match_states st' tst'. +Proof. + induction 1; simplify; + match goal with H: match_states _ _ |- _ => inv H end; + repeat econstructor; try erewrite match_states_list; + try apply PTree_matches; eauto; + match goal with + H: forall _, _ |- context[Mem.storev] => erewrite <- H; eauto + end. +Qed. + +Lemma step_instr_list_matches : + forall a ge sp st st', + step_instr_list ge sp st a st' -> + forall tst, match_states st tst -> + exists tst', step_instr_list ge sp tst a tst' + /\ match_states st' tst'. +Proof. + induction a; intros; inv H; + try (exploit step_instr_matches; eauto; []; inv_simp; + exploit IHa; eauto; []; inv_simp); repeat econstructor; eauto. +Qed. -Lemma state_lessdef_match_sem: - forall st tst, - state_lessdef st tst -> - match_sem_st (tr_instr_state st) (tr_instr_state tst). +Lemma step_instr_seq_matches : + forall a ge sp st st', + step_instr_seq ge sp st a st' -> + forall tst, match_states st tst -> + exists tst', step_instr_seq ge sp tst a tst' + /\ match_states st' tst'. Proof. - intros * H; destruct st; destruct tst; simplify; - inv H; constructor; auto. + induction a; intros; inv H; + try (exploit step_instr_list_matches; eauto; []; inv_simp; + exploit IHa; eauto; []; inv_simp); repeat econstructor; eauto. +Qed. + +Lemma step_instr_block_matches : + forall bb ge sp st st', + step_instr_block ge sp st bb st' -> + forall tst, match_states st tst -> + exists tst', step_instr_block ge sp tst bb tst' + /\ match_states st' tst'. +Proof. + induction bb; intros; inv H; + try (exploit step_instr_seq_matches; eauto; []; inv_simp; + exploit IHbb; eauto; []; inv_simp); repeat econstructor; eauto. Qed. Lemma abstract_execution_correct: @@ -1084,21 +1208,21 @@ Lemma abstract_execution_correct: RTLBlock.step_instr_list ge sp st bb st' -> ge_preserved ge tge -> schedule_oracle (mk_bblock bb cfi) (mk_bblock bb' cfi) = true -> - state_lessdef st tst -> + match_states st tst -> exists tst', RTLPar.step_instr_block tge sp tst bb' tst' - /\ state_lessdef st' tst'. + /\ match_states st' tst'. Proof. intros. unfold schedule_oracle in *. simplify. exploit rtlblock_trans_correct; try eassumption; []; inv_simp. exploit abstract_execution_correct'; - try solve [eassumption | apply state_lessdef_match_sem; eassumption]; inv_simp. + try solve [eassumption | apply state_lessdef_match_sem; eassumption]. + apply match_states_commut. eauto. inv_simp. exploit rtlpar_trans_correct; try eassumption; []; inv_simp. - econstructor; simplify. - match goal with - | H: context[tr_sem_state (tr_instr_state _)] |- _ => rewrite tr_instr_state_eq in H - end; eassumption. - eapply states_match; eauto. + exploit step_instr_block_matches; eauto; inv_simp. + repeat match goal with | H: match_states _ _ |- _ => inv H end. + do 2 econstructor; eauto. + econstructor; congruence. Qed. (*| -- cgit From fdd6af98c91b6f1206e5f1aef3bfc1f02c7d64aa Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Sat, 15 May 2021 21:06:10 +0100 Subject: Fix the top-level proofs with new state_match --- src/hls/RTLPargen.v | 109 ++++++++++++++++++++++++++++++++++++++++++++++++---- 1 file changed, 101 insertions(+), 8 deletions(-) (limited to 'src/hls/RTLPargen.v') diff --git a/src/hls/RTLPargen.v b/src/hls/RTLPargen.v index f64a796..d2a7174 100644 --- a/src/hls/RTLPargen.v +++ b/src/hls/RTLPargen.v @@ -978,6 +978,62 @@ Proof. { eapply sem_update_store; eauto. } Qed. +Lemma sem_update2_Op : + forall A ge sp st f r l o0 o m rs v, + @sem A ge sp st f (InstrState rs m) -> + Op.eval_operation ge sp o0 rs ## l m = Some v -> + sem ge sp st (update f (RBop o o0 l r)) (InstrState (Regmap.set r v rs) m). +Proof. + intros. destruct st. constructor. + inv H. inv H6. + { constructor; intros. simplify. + destruct (Pos.eq_dec r x); subst. + { rewrite map2. econstructor. eauto. + apply gen_list_base. eauto. + rewrite Regmap.gss. auto. } + { rewrite genmap1; crush. rewrite Regmap.gso; auto. } } + { simplify. rewrite genmap1; crush. inv H. eauto. } +Qed. + +Lemma sem_update2_load : + forall A ge sp st f r o m a l m0 rs v a0, + @sem A ge sp st f (InstrState rs m0) -> + Op.eval_addressing ge sp a rs ## l = Some a0 -> + Mem.loadv m m0 a0 = Some v -> + sem ge sp st (update f (RBload o m a l r)) (InstrState (Regmap.set r v rs) m0). +Proof. + intros. simplify. inv H. inv H7. constructor. + { constructor; intros. destruct (Pos.eq_dec r x); subst. + { rewrite map2. rewrite Regmap.gss. econstructor; eauto. + apply gen_list_base; eauto. } + { rewrite genmap1; crush. rewrite Regmap.gso; eauto. } + } + { simplify. rewrite genmap1; crush. } +Qed. + +Lemma sem_update2_store : + forall A ge sp a0 m a l r o f st m' rs m0, + @sem A ge sp st f (InstrState rs m0) -> + Op.eval_addressing ge sp a rs ## l = Some a0 -> + Mem.storev m m0 a0 rs !! r = Some m' -> + sem ge sp st (update f (RBstore o m a l r)) (InstrState rs m'). +Proof. + intros. simplify. inv H. inv H7. constructor; simplify. + { econstructor; intros. rewrite genmap1; crush. } + { rewrite map2. econstructor; eauto. apply gen_list_base; eauto. } +Qed. + +Lemma sem_update2 : + forall A ge sp st x st' st'' f, + sem ge sp st f st' -> + @step_instr A ge sp st' x st'' -> + sem ge sp st (update f x) st''. +Proof. + intros. + destruct x; inv H0; + eauto using sem_update_RBnop, sem_update2_Op, sem_update2_load, sem_update2_store. +Qed. + Lemma rtlblock_trans_correct : forall bb ge sp st st', RTLBlock.step_instr_list ge sp st bb st' -> @@ -997,13 +1053,6 @@ Proof. auto. } Qed. -Lemma rtlpar_trans_correct : - forall ge sp bb sem_st' sem_st, - sem ge sp sem_st (abstract_sequence empty (concat (concat bb))) sem_st' -> - exists st', RTLPar.step_instr_block ge sp sem_st bb st' - /\ match_states sem_st' st'. -Proof. Admitted. - Lemma abstr_sem_val_mem : forall A B ge tge st tst sp a, ge_preserved ge tge -> @@ -1203,6 +1252,50 @@ Proof. exploit IHbb; eauto; []; inv_simp); repeat econstructor; eauto. Qed. +Lemma sem_update' : + forall A ge sp st a x st', + sem ge sp st (update (abstract_sequence empty a) x) st' -> + exists st'', + @step_instr A ge sp st'' x st' /\ + sem ge sp st (abstract_sequence empty a) st''. +Proof. + Admitted. + +Lemma sem_separate : + forall A (ge: @RTLBlockInstr.genv A) b a sp st st', + sem ge sp st (abstract_sequence empty (a ++ b)) st' -> + exists st'', + sem ge sp st (abstract_sequence empty a) st'' + /\ sem ge sp st'' (abstract_sequence empty b) st'. +Proof. + induction b using rev_ind; simplify. + { econstructor. simplify. rewrite app_nil_r in H. eauto. apply abstract_interp_empty. } + { simplify. rewrite app_assoc in H. rewrite abstract_seq in H. + exploit sem_update'; eauto; inv_simp. + exploit IHb; eauto; inv_simp. + econstructor; split; eauto. + rewrite abstract_seq. + eapply sem_update2; eauto. + } +Qed. + +Lemma rtlpar_trans_correct : + forall bb ge sp sem_st' sem_st st, + sem ge sp sem_st (abstract_sequence empty (concat (concat bb))) sem_st' -> + match_states sem_st st -> + exists st', RTLPar.step_instr_block ge sp st bb st' + /\ match_states sem_st' st'. +Proof. + induction bb using rev_ind. + { repeat econstructor. eapply abstract_interp_empty3 in H. + inv H. inv H0. constructor; congruence. } + { simplify. inv H0. repeat rewrite concat_app in H. simplify. + rewrite app_nil_r in H. + exploit sem_separate; eauto; inv_simp. + repeat econstructor. admit. admit. + } +Admitted. + Lemma abstract_execution_correct: forall bb bb' cfi ge tge sp st st' tst, RTLBlock.step_instr_list ge sp st bb st' -> @@ -1219,7 +1312,7 @@ Proof. try solve [eassumption | apply state_lessdef_match_sem; eassumption]. apply match_states_commut. eauto. inv_simp. exploit rtlpar_trans_correct; try eassumption; []; inv_simp. - exploit step_instr_block_matches; eauto; inv_simp. + exploit step_instr_block_matches; eauto. apply match_states_commut; eauto. inv_simp. repeat match goal with | H: match_states _ _ |- _ => inv H end. do 2 econstructor; eauto. econstructor; congruence. -- cgit From becbab413e16e40069329d8e7f21dc92e2e4c4e4 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Sun, 16 May 2021 11:26:22 +0100 Subject: Finish up step_cf_instr_correct again --- src/hls/RTLPargen.v | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) (limited to 'src/hls/RTLPargen.v') diff --git a/src/hls/RTLPargen.v b/src/hls/RTLPargen.v index d2a7174..a8da344 100644 --- a/src/hls/RTLPargen.v +++ b/src/hls/RTLPargen.v @@ -467,6 +467,13 @@ Inductive match_states : instr_state -> instr_state -> Prop := m = m' -> match_states (InstrState rs m) (InstrState rs' m'). +Inductive match_states_ld : instr_state -> instr_state -> Prop := +| match_states_ld_intro: + forall rs rs' m m', + regs_lessdef rs rs' -> + Mem.extends m m' -> + match_states_ld (InstrState rs m) (InstrState rs' m'). + Lemma sems_det: forall A ge tge sp st f, ge_preserved ge tge -> @@ -1318,6 +1325,17 @@ Proof. econstructor; congruence. Qed. +(*Lemma abstract_execution_correct_ld: + forall bb bb' cfi ge tge sp st st' tst, + RTLBlock.step_instr_list ge sp st bb st' -> + ge_preserved ge tge -> + schedule_oracle (mk_bblock bb cfi) (mk_bblock bb' cfi) = true -> + match_states_ld st tst -> + exists tst', RTLPar.step_instr_block tge sp tst bb' tst' + /\ match_states st' tst'. +Proof. + intros.*) + (*| Top-level functions =================== -- cgit From e1d0762daf0dd4d8f826decaa4c0498c75aa9119 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Fri, 21 May 2021 18:28:58 +0100 Subject: Finish top-level of proof --- src/hls/RTLPargen.v | 10 +--------- 1 file changed, 1 insertion(+), 9 deletions(-) (limited to 'src/hls/RTLPargen.v') diff --git a/src/hls/RTLPargen.v b/src/hls/RTLPargen.v index a8da344..be57e7f 100644 --- a/src/hls/RTLPargen.v +++ b/src/hls/RTLPargen.v @@ -1354,15 +1354,7 @@ Definition transl_function (f: RTLBlock.function) : Errors.res RTLPar.function : else Errors.Error (Errors.msg "RTLPargen: Could not prove the blocks equivalent."). -Definition transl_function_temp (f: RTLBlock.function) : Errors.res RTLPar.function := - let tfcode := fn_code (schedule f) in - Errors.OK (mkfunction f.(fn_sig) - f.(fn_params) - f.(fn_stacksize) - tfcode - f.(fn_entrypoint)). - -Definition transl_fundef := transf_partial_fundef transl_function_temp. +Definition transl_fundef := transf_partial_fundef transl_function. Definition transl_program (p : RTLBlock.program) : Errors.res RTLPar.program := transform_partial_program transl_fundef p. -- cgit From da56228e5938fd835910e7aaf345c1ff684234e8 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Wed, 26 May 2021 19:25:55 +0100 Subject: Add predicate semantics to abstract --- src/hls/RTLPargen.v | 365 ++++++++++++++++++++++++++++++++++++++++++---------- 1 file changed, 296 insertions(+), 69 deletions(-) (limited to 'src/hls/RTLPargen.v') diff --git a/src/hls/RTLPargen.v b/src/hls/RTLPargen.v index be57e7f..00adc32 100644 --- a/src/hls/RTLPargen.v +++ b/src/hls/RTLPargen.v @@ -44,6 +44,7 @@ Definition reg := positive. Inductive resource : Set := | Reg : reg -> resource +| Pred : reg -> resource | Mem : resource. (*| @@ -53,7 +54,7 @@ optimised heavily if written manually, as their proofs are not needed. Lemma resource_eq : forall (r1 r2 : resource), {r1 = r2} + {r1 <> r2}. Proof. - decide equality. apply Pos.eq_dec. + decide equality; apply Pos.eq_dec. Defined. Lemma comparison_eq: forall (x y : comparison), {x = y} + {x <> y}. @@ -181,7 +182,8 @@ Module R_indexed. Definition t := resource. Definition index (rs: resource) : positive := match rs with - | Reg r => xO r + | Reg r => xO (xO r) + | Pred r => xI (xI r) | Mem => 1%positive end. @@ -205,14 +207,171 @@ Then, to make recursion over expressions easier, expression_list is also defined that enables mutual recursive definitions over the datatypes. |*) -Inductive expression : Set := +Definition unsat p := forall a, sat_predicate p a = false. +Definition sat p := exists a, sat_predicate p a = true. + +Inductive expression : Type := | Ebase : resource -> expression | Eop : Op.operation -> expression_list -> expression -> expression | Eload : AST.memory_chunk -> Op.addressing -> expression_list -> expression -> expression | Estore : expression -> AST.memory_chunk -> Op.addressing -> expression_list -> expression -> expression -with expression_list : Set := +| Esetpred : predicate -> Op.condition -> expression_list -> expression -> expression +| Econd : expr_pred_list -> expression +with expression_list : Type := | Enil : expression_list -| Econs : expression -> expression_list -> expression_list. +| Econs : expression -> expression_list -> expression_list +with expr_pred_list : Type := +| EPnil : expr_pred_list +| EPcons : pred_op -> expression -> expr_pred_list -> expr_pred_list +. + +Definition pred_list_wf l : Prop := + forall a b, In a l -> In b l -> a <> b -> unsat (Pand a b). + +Fixpoint expr_pred_list_to_list e := + match e with + | EPnil => nil + | EPcons p e l => (p, e) :: expr_pred_list_to_list l + end. + +Definition pred_list_wf_ep l : Prop := + pred_list_wf (map fst (expr_pred_list_to_list l)). + +Lemma unsat_correct1 : + forall a b c, + unsat (Pand a b) -> + sat_predicate a c = true -> + sat_predicate b c = false. +Proof. + unfold unsat in *. intros. + simplify. specialize (H c). + apply andb_false_iff in H. inv H. rewrite H0 in H1. discriminate. + auto. +Qed. + +Lemma unsat_correct2 : + forall a b c, + unsat (Pand a b) -> + sat_predicate b c = true -> + sat_predicate a c = false. +Proof. + unfold unsat in *. intros. + simplify. specialize (H c). + apply andb_false_iff in H. inv H. auto. rewrite H0 in H1. discriminate. +Qed. + +Lemma unsat_not a: unsat (Pand a (Pnot a)). +Proof. unfold unsat; simplify; auto with bool. Qed. + +Lemma unsat_commut a b: unsat (Pand a b) -> unsat (Pand b a). +Proof. unfold unsat; simplify; eauto with bool. Qed. + +Lemma sat_dec a n b: sat_pred n a = Some b -> {sat a} + {unsat a}. +Proof. + unfold sat, unsat. destruct b. + intros. left. destruct s. + exists (Sat.interp_alist x). auto. + intros. tauto. +Qed. + +Lemma sat_equiv : + forall a b, + unsat (Por (Pand a (Pnot b)) (Pand (Pnot a) b)) -> + forall c, sat_predicate a c = sat_predicate b c. +Proof. + unfold unsat. intros. specialize (H c); simplify. + destruct (sat_predicate b c) eqn:X; + destruct (sat_predicate a c) eqn:X2; + crush. +Qed. + +(*Parameter op_le : Op.operation -> Op.operation -> bool. +Parameter chunk_le : AST.memory_chunk -> AST.memory_chunk -> bool. +Parameter addr_le : Op.addressing -> Op.addressing -> bool. +Parameter cond_le : Op.condition -> Op.condition -> bool. + +Fixpoint pred_le (p1 p2: pred_op) : bool := + match p1, p2 with + | Pvar i, Pvar j => (i <=? j)%positive + | Pnot p1, Pnot p2 => pred_le p1 p2 + | Pand p1 p1', Pand p2 p2' => if pred_le p1 p2 then true else pred_le p1' p2' + | Por p1 p1', Por p2 p2' => if pred_le p1 p2 then true else pred_le p1' p2' + | Pvar _, _ => true + | Pnot _, Pvar _ => false + | Pnot _, _ => true + | Pand _ _, Pvar _ => false + | Pand _ _, Pnot _ => false + | Pand _ _, _ => true + | Por _ _, _ => false + end. + +Import Lia. + +Lemma pred_le_trans : + forall p1 p2 p3 b, pred_le p1 p2 = b -> pred_le p2 p3 = b -> pred_le p1 p3 = b. +Proof. + induction p1; destruct p2; destruct p3; crush. + destruct b. rewrite Pos.leb_le in *. lia. rewrite Pos.leb_gt in *. lia. + firstorder. + destruct (pred_le p1_1 p2_1) eqn:?. subst. destruct (pred_le p2_1 p3_1) eqn:?. + apply IHp1_1 in Heqb. rewrite Heqb. auto. auto. + + +Fixpoint expr_le (e1 e2: expression) {struct e2}: bool := + match e1, e2 with + | Ebase r1, Ebase r2 => (R_indexed.index r1 <=? R_indexed.index r2)%positive + | Ebase _, _ => true + | Eop op1 elist1 m1, Eop op2 elist2 m2 => + if op_le op1 op2 then true + else if elist_le elist1 elist2 then true + else expr_le m1 m2 + | Eop _ _ _, Ebase _ => false + | Eop _ _ _, _ => true + | Eload chunk1 addr1 elist1 expr1, Eload chunk2 addr2 elist2 expr2 => + if chunk_le chunk1 chunk2 then true + else if addr_le addr1 addr2 then true + else if elist_le elist1 elist2 then true + else expr_le expr1 expr2 + | Eload _ _ _ _, Ebase _ => false + | Eload _ _ _ _, Eop _ _ _ => false + | Eload _ _ _ _, _ => true + | Estore m1 chunk1 addr1 elist1 expr1, Estore m2 chunk2 addr2 elist2 expr2 => + if expr_le m1 m2 then true + else if chunk_le chunk1 chunk2 then true + else if addr_le addr1 addr2 then true + else if elist_le elist1 elist2 then true + else expr_le expr1 expr2 + | Estore _ _ _ _ _, Ebase _ => false + | Estore _ _ _ _ _, Eop _ _ _ => false + | Estore _ _ _ _ _, Eload _ _ _ _ => false + | Estore _ _ _ _ _, _ => true + | Esetpred p1 cond1 elist1 m1, Esetpred p2 cond2 elist2 m2 => + if (p1 <=? p2)%positive then true + else if cond_le cond1 cond2 then true + else if elist_le elist1 elist2 then true + else expr_le m1 m2 + | Esetpred _ _ _ _, Econd _ => true + | Esetpred _ _ _ _, _ => false + | Econd eplist1, Econd eplist2 => eplist_le eplist1 eplist2 + | Econd eplist1, _ => false + end +with elist_le (e1 e2: expression_list) : bool := + match e1, e2 with + | Enil, Enil => true + | Econs a1 b1, Econs a2 b2 => if expr_le a1 a2 then true else elist_le b1 b2 + | Enil, _ => true + | _, Enil => false + end +with eplist_le (e1 e2: expr_pred_list) : bool := + match e1, e2 with + | EPnil, EPnil => true + | EPcons p1 a1 b1, EPcons p2 a2 b2 => + if pred_le p1 p2 then true + else if expr_le a1 a2 then true else eplist_le b1 b2 + | EPnil, _ => true + | _, EPnil => false + end +.*) (*| Using IMap we can create a map from resources to any other type, as resources can be uniquely @@ -223,8 +382,6 @@ Module Rtree := ITree(R_indexed). Definition forest : Type := Rtree.t expression. -Definition regset := Registers.Regmap.t val. - Definition get_forest v f := match Rtree.get v f with | None => Ebase v @@ -234,6 +391,19 @@ Definition get_forest v f := Notation "a # b" := (get_forest b a) (at level 1). Notation "a # b <- c" := (Rtree.set b c a) (at level 1, b at next level). +Definition maybe {A: Type} (vo: A) (pr: predset) p (v: A) := + match p with + | Some p' => if eval_predf pr p' then v else vo + | None => v + end. + +Definition get_pr i := match i with InstrState a b c => b end. + +Definition get_m i := match i with InstrState a b c => c end. + +Definition eval_predf_opt pr p := + match p with Some p' => eval_predf pr p' | None => true end. + (*| Finally we want to define the semantics of execution for the expressions with symbolic values, so the result of executing the expressions will be an expressions. @@ -244,61 +414,100 @@ Section SEMANTICS. Context {A : Type} (genv : Genv.t A unit). Inductive sem_value : - val -> instr_state -> expression -> val -> Prop := - | Sbase_reg: - forall sp rs r m, - sem_value sp (InstrState rs m) (Ebase (Reg r)) (rs !! r) - | Sop: - forall rs m op args v lv sp m' mem_exp, - sem_mem sp (InstrState rs m) mem_exp m' -> - sem_val_list sp (InstrState rs m) args lv -> - Op.eval_operation genv sp op lv m' = Some v -> - sem_value sp (InstrState rs m) (Eop op args mem_exp) v - | Sload : - forall st mem_exp addr chunk args a v m' lv sp, - sem_mem sp st mem_exp m' -> - sem_val_list sp st args lv -> - Op.eval_addressing genv sp addr lv = Some a -> - Memory.Mem.loadv chunk m' a = Some v -> - sem_value sp st (Eload chunk addr args mem_exp) v + val -> instr_state -> expression -> val -> Prop := +| Sbase_reg: + forall sp rs r m pr, + sem_value sp (InstrState rs pr m) (Ebase (Reg r)) (rs !! r) +| Sop: + forall rs m op args v lv sp m' mem_exp pr, + sem_mem sp (InstrState rs pr m) mem_exp m' -> + sem_val_list sp (InstrState rs pr m) args lv -> + Op.eval_operation genv sp op lv m' = Some v -> + sem_value sp (InstrState rs pr m) (Eop op args mem_exp) v +| Sload : + forall st mem_exp addr chunk args a v m' lv sp, + sem_mem sp st mem_exp m' -> + sem_val_list sp st args lv -> + Op.eval_addressing genv sp addr lv = Some a -> + Memory.Mem.loadv chunk m' a = Some v -> + sem_value sp st (Eload chunk addr args mem_exp) v +| Scond : + forall sp st e v, + sem_val_ep_list sp st e v -> + sem_value sp st (Econd e) v +with sem_pred : + val -> instr_state -> expression -> bool -> Prop := +| Spred: + forall st mem_exp args p c lv m m' v sp, + sem_mem sp st mem_exp m' -> + sem_val_list sp st args lv -> + Op.eval_condition c lv m = Some v -> + sem_pred sp st (Esetpred p c args mem_exp) v +| Sbase_pred: + forall rs pr m p sp, + sem_pred sp (InstrState rs pr m) (Ebase (Pred p)) (PMap.get p pr) with sem_mem : - val -> instr_state -> expression -> Memory.mem -> Prop := - | Sstore : - forall st mem_exp val_exp m'' addr v a m' chunk args lv sp, - sem_mem sp st mem_exp m' -> - sem_value sp st val_exp v -> - sem_val_list sp st args lv -> - Op.eval_addressing genv sp addr lv = Some a -> - Memory.Mem.storev chunk m' a v = Some m'' -> - sem_mem sp st (Estore mem_exp chunk addr args val_exp) m'' - | Sbase_mem : - forall rs m sp, - sem_mem sp (InstrState rs m) (Ebase Mem) m + val -> instr_state -> expression -> Memory.mem -> Prop := +| Sstore : + forall st mem_exp val_exp m'' addr v a m' chunk args lv sp, + sem_mem sp st mem_exp m' -> + sem_value sp st val_exp v -> + sem_val_list sp st args lv -> + Op.eval_addressing genv sp addr lv = Some a -> + Memory.Mem.storev chunk m' a v = Some m'' -> + sem_mem sp st (Estore mem_exp chunk addr args val_exp) m'' +| Sbase_mem : + forall rs m sp pr, + sem_mem sp (InstrState rs pr m) (Ebase Mem) m with sem_val_list : - val -> instr_state -> expression_list -> list val -> Prop := - | Snil : - forall st sp, - sem_val_list sp st Enil nil - | Scons : - forall st e v l lv sp, - sem_value sp st e v -> - sem_val_list sp st l lv -> - sem_val_list sp st (Econs e l) (v :: lv). + val -> instr_state -> expression_list -> list val -> Prop := +| Snil : + forall st sp, + sem_val_list sp st Enil nil +| Scons : + forall st e v l lv sp, + sem_value sp st e v -> + sem_val_list sp st l lv -> + sem_val_list sp st (Econs e l) (v :: lv) +with sem_val_ep_list : + val -> instr_state -> expr_pred_list -> val -> Prop := +| SPnil : + forall sp rs r m pr, + sem_val_ep_list sp (InstrState rs pr m) EPnil (rs !! r) +| SPconsTrue : + forall pr p sp rs m e v el, + eval_predf pr p = true -> + sem_value sp (InstrState rs pr m) e v -> + sem_val_ep_list sp (InstrState rs pr m) (EPcons p e el) v +| SPconsFalse : + forall pr p sp rs m e v el, + eval_predf pr p = false -> + sem_val_ep_list sp (InstrState rs pr m) el v -> + sem_val_ep_list sp (InstrState rs pr m) (EPcons p e el) v +. + +Inductive sem_predset : + val -> instr_state -> forest -> predset -> Prop := +| Spredset: + forall st f sp rs', + (forall x, sem_pred sp st (f # (Pred x)) (PMap.get x rs')) -> + sem_predset sp st f rs'. Inductive sem_regset : val -> instr_state -> forest -> regset -> Prop := - | Sregset: - forall st f sp rs', - (forall x, sem_value sp st (f # (Reg x)) (Registers.Regmap.get x rs')) -> - sem_regset sp st f rs'. +| Sregset: + forall st f sp rs', + (forall x, sem_value sp st (f # (Reg x)) (rs' !! x)) -> + sem_regset sp st f rs'. Inductive sem : val -> instr_state -> forest -> instr_state -> Prop := - | Sem: - forall st rs' m' f sp, - sem_regset sp st f rs' -> - sem_mem sp st (f # Mem) m' -> - sem sp st f (InstrState rs' m'). +| Sem: + forall st rs' m' f sp pr', + sem_regset sp st f rs' -> + sem_predset sp st f pr' -> + sem_mem sp st (f # Mem) m' -> + sem sp st f (InstrState rs' pr' m'). End SEMANTICS. @@ -306,20 +515,26 @@ Fixpoint beq_expression (e1 e2: expression) {struct e1}: bool := match e1, e2 with | Ebase r1, Ebase r2 => if resource_eq r1 r2 then true else false | Eop op1 el1 exp1, Eop op2 el2 exp2 => - if operation_eq op1 op2 then - if beq_expression exp1 exp2 then - beq_expression_list el1 el2 else false else false + if operation_eq op1 op2 then + if beq_expression exp1 exp2 then + beq_expression_list el1 el2 else false else false | Eload chk1 addr1 el1 e1, Eload chk2 addr2 el2 e2 => - if memory_chunk_eq chk1 chk2 - then if addressing_eq addr1 addr2 - then if beq_expression_list el1 el2 - then beq_expression e1 e2 else false else false else false + if memory_chunk_eq chk1 chk2 + then if addressing_eq addr1 addr2 + then if beq_expression_list el1 el2 + then beq_expression e1 e2 else false else false else false | Estore m1 chk1 addr1 el1 e1, Estore m2 chk2 addr2 el2 e2=> - if memory_chunk_eq chk1 chk2 - then if addressing_eq addr1 addr2 - then if beq_expression_list el1 el2 - then if beq_expression m1 m2 - then beq_expression e1 e2 else false else false else false else false + if memory_chunk_eq chk1 chk2 + then if addressing_eq addr1 addr2 + then if beq_expression_list el1 el2 + then if beq_expression m1 m2 + then beq_expression e1 e2 else false else false else false else false + | Esetpred p1 c1 el1 m1, Esetpred p2 c2 el2 m2 => + if Pos.eqb p1 p2 + then if condition_eq c1 c2 + then if beq_expression_list el1 el2 + then beq_expression m1 m2 else false else false else false + | Econd el1, Econd el2 => beq_expr_pred_list el1 el2 | _, _ => false end with beq_expression_list (el1 el2: expression_list) {struct el1} : bool := @@ -327,10 +542,19 @@ with beq_expression_list (el1 el2: expression_list) {struct el1} : bool := | Enil, Enil => true | Econs e1 t1, Econs e2 t2 => beq_expression e1 e2 && beq_expression_list t1 t2 | _, _ => false - end. + end +with beq_expr_pred_list (el1 el2: expr_pred_list) {struct el1} : bool := + match el1, el2 with + | EPnil, EPnil => true + | EPcons p1 e1 el1', EPcons p2 e2 el2' => true + | _, _ => false + end +. Scheme expression_ind2 := Induction for expression Sort Prop - with expression_list_ind2 := Induction for expression_list Sort Prop. + with expression_list_ind2 := Induction for expression_list Sort Prop + with expr_pred_list_ind2 := Induction for expr_pred_list Sort Prop +. Lemma beq_expression_correct: forall e1 e2, beq_expression e1 e2 = true -> e1 = e2. @@ -340,11 +564,14 @@ Proof. (P := fun (e1 : expression) => forall e2, beq_expression e1 e2 = true -> e1 = e2) (P0 := fun (e1 : expression_list) => - forall e2, beq_expression_list e1 e2 = true -> e1 = e2); simplify; + forall e2, beq_expression_list e1 e2 = true -> e1 = e2) + (P1 := fun (e1 : expr_pred_list) => + forall e2, beq_expr_pred_list e1 e2 = true -> e1 = e2); simplify; repeat match goal with | [ H : context[match ?x with _ => _ end] |- _ ] => destruct x eqn:? | [ H : context[if ?x then _ else _] |- _ ] => destruct x eqn:? end; subst; f_equal; crush. + eauto using Peqb_true_eq. Qed. Definition empty : forest := Rtree.empty _. -- cgit From 72384a6bf701f4e1c256bec8ed85605d444f5b61 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Mon, 20 Sep 2021 21:40:53 +0100 Subject: Start adding hashing to RTLPargen --- src/hls/RTLPargen.v | 54 ++++++++++++++++++++++++++++++++++++++++++++++++----- 1 file changed, 49 insertions(+), 5 deletions(-) (limited to 'src/hls/RTLPargen.v') diff --git a/src/hls/RTLPargen.v b/src/hls/RTLPargen.v index 727ccf3..b06bf0a 100644 --- a/src/hls/RTLPargen.v +++ b/src/hls/RTLPargen.v @@ -511,6 +511,50 @@ Inductive sem : End SEMANTICS. +Definition hash_pred := @pred positive. + +Definition hash_tree := PTree.t (condition * list reg). + +Definition find_tree (el: predicate * list reg) (h: hash_tree) : option positive := + match + filter (fun x => match x with (a, b) => if hash_el_dec el b then true else false end) + (PTree.elements h) with + | (p, _) :: nil => Some p + | _ => None + end. + +Definition combine_option {A} (a b: option A) : option A := + match a, b with + | Some a', _ => Some a' + | _, Some b' => Some b' + | _, _ => None + end. + +Definition max_key {A} (t: PTree.t A) := + fold_right Pos.max 1 (map fst (PTree.elements t)). + +Fixpoint hash_predicate (p: predicate) (h: PTree.t (condition * list reg)) + : hash_pred * PTree.t (condition * list reg) := + match p with + | T => (T, h) + | ⟂ => (⟂, h) + | Pbase (b, (c, args)) => + match find_tree (c, args) h with + | Some p => (Pbase (b, p), h) + | None => + let nkey := max_key h + 1 in + (Pbase (b, nkey), PTree.set nkey (c, args) h) + end + | p1 ∧ p2 => + let (p1', t1) := hash_predicate p1 h in + let (p2', t2) := hash_predicate p2 t1 in + (p1' ∧ p2', t2) + | p1 ∨ p2 => + let (p1', t1) := hash_predicate p1 h in + let (p2', t2) := hash_predicate p2 t1 in + (p1' ∨ p2', t2) + end. + Fixpoint beq_expression (e1 e2: expression) {struct e1}: bool := match e1, e2 with | Ebase r1, Ebase r2 => if resource_eq r1 r2 then true else false @@ -567,11 +611,11 @@ Proof. forall e2, beq_expression_list e1 e2 = true -> e1 = e2) (P1 := fun (e1 : expr_pred_list) => forall e2, beq_expr_pred_list e1 e2 = true -> e1 = e2); simplify; - repeat match goal with - | [ H : context[match ?x with _ => _ end] |- _ ] => destruct x eqn:? - | [ H : context[if ?x then _ else _] |- _ ] => destruct x eqn:? - end; subst; f_equal; crush. - eauto using Peqb_true_eq. + try solve [repeat match goal with + | [ H : context[match ?x with _ => _ end] |- _ ] => destruct x eqn:? + | [ H : context[if ?x then _ else _] |- _ ] => destruct x eqn:? + end; subst; f_equal; crush; eauto using Peqb_true_eq]. + destruct e2; try discriminate. eauto. Qed. Definition empty : forest := Rtree.empty _. -- cgit From 8386bed39f413bb461c19debbad92e85f927c4b5 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Wed, 22 Sep 2021 14:54:46 +0100 Subject: Fix the comparison of predicated expressions --- src/hls/RTLPargen.v | 312 +++++++++++++++++++++++++++++----------------------- 1 file changed, 174 insertions(+), 138 deletions(-) (limited to 'src/hls/RTLPargen.v') diff --git a/src/hls/RTLPargen.v b/src/hls/RTLPargen.v index b06bf0a..09eabc9 100644 --- a/src/hls/RTLPargen.v +++ b/src/hls/RTLPargen.v @@ -31,6 +31,8 @@ Require Import vericert.hls.RTLBlock. Require Import vericert.hls.RTLPar. Require Import vericert.hls.RTLBlockInstr. +#[local] Open Scope positive. + (*| Schedule Oracle =============== @@ -216,26 +218,27 @@ Inductive expression : Type := | Eload : AST.memory_chunk -> Op.addressing -> expression_list -> expression -> expression | Estore : expression -> AST.memory_chunk -> Op.addressing -> expression_list -> expression -> expression | Esetpred : predicate -> Op.condition -> expression_list -> expression -> expression -| Econd : expr_pred_list -> expression with expression_list : Type := | Enil : expression_list | Econs : expression -> expression_list -> expression_list -with expr_pred_list : Type := -| EPnil : expr_pred_list -| EPcons : pred_op -> expression -> expr_pred_list -> expr_pred_list . +Inductive pred_expr : Type := +| PEsingleton : option pred_op -> expression -> pred_expr +| PEcons : pred_op -> expression -> pred_expr -> pred_expr. + Definition pred_list_wf l : Prop := forall a b, In a l -> In b l -> a <> b -> unsat (Pand a b). -Fixpoint expr_pred_list_to_list e := - match e with - | EPnil => nil - | EPcons p e l => (p, e) :: expr_pred_list_to_list l +Fixpoint pred_expr_list (p: pred_expr) := + match p with + | PEsingleton None _ => nil + | PEsingleton (Some pr) e => (pr, e) :: nil + | PEcons pr e p' => (pr, e) :: pred_expr_list p' end. -Definition pred_list_wf_ep l : Prop := - pred_list_wf (map fst (expr_pred_list_to_list l)). +Definition pred_list_wf_ep (l: pred_expr) : Prop := + pred_list_wf (map fst (pred_expr_list l)). Lemma unsat_correct1 : forall a b c, @@ -380,11 +383,11 @@ identified as positive numbers. Module Rtree := ITree(R_indexed). -Definition forest : Type := Rtree.t expression. +Definition forest : Type := Rtree.t pred_expr. -Definition get_forest v f := +Definition get_forest v (f: forest) := match Rtree.get v f with - | None => Ebase v + | None => PEsingleton None (Ebase v) | Some v' => v' end. @@ -397,9 +400,9 @@ Definition maybe {A: Type} (vo: A) (pr: predset) p (v: A) := | None => v end. -Definition get_pr i := match i with InstrState a b c => b end. +Definition get_pr i := match i with mk_instr_state a b c => b end. -Definition get_m i := match i with InstrState a b c => c end. +Definition get_m i := match i with mk_instr_state a b c => c end. Definition eval_predf_opt pr p := match p with Some p' => eval_predf pr p' | None => true end. @@ -417,13 +420,13 @@ Inductive sem_value : val -> instr_state -> expression -> val -> Prop := | Sbase_reg: forall sp rs r m pr, - sem_value sp (InstrState rs pr m) (Ebase (Reg r)) (rs !! r) + sem_value sp (mk_instr_state rs pr m) (Ebase (Reg r)) (rs !! r) | Sop: forall rs m op args v lv sp m' mem_exp pr, - sem_mem sp (InstrState rs pr m) mem_exp m' -> - sem_val_list sp (InstrState rs pr m) args lv -> + sem_mem sp (mk_instr_state rs pr m) mem_exp m' -> + sem_val_list sp (mk_instr_state rs pr m) args lv -> Op.eval_operation genv sp op lv m' = Some v -> - sem_value sp (InstrState rs pr m) (Eop op args mem_exp) v + sem_value sp (mk_instr_state rs pr m) (Eop op args mem_exp) v | Sload : forall st mem_exp addr chunk args a v m' lv sp, sem_mem sp st mem_exp m' -> @@ -431,21 +434,17 @@ Inductive sem_value : Op.eval_addressing genv sp addr lv = Some a -> Memory.Mem.loadv chunk m' a = Some v -> sem_value sp st (Eload chunk addr args mem_exp) v -| Scond : - forall sp st e v, - sem_val_ep_list sp st e v -> - sem_value sp st (Econd e) v with sem_pred : val -> instr_state -> expression -> bool -> Prop := | Spred: - forall st mem_exp args p c lv m m' v sp, - sem_mem sp st mem_exp m' -> + forall st pred_exp args p c lv m m' v sp, + sem_pred sp st pred_exp m' -> sem_val_list sp st args lv -> Op.eval_condition c lv m = Some v -> - sem_pred sp st (Esetpred p c args mem_exp) v + sem_pred sp st (Esetpred p c args pred_exp) v | Sbase_pred: forall rs pr m p sp, - sem_pred sp (InstrState rs pr m) (Ebase (Pred p)) (PMap.get p pr) + sem_pred sp (mk_instr_state rs pr m) (Ebase (Pred p)) (PMap.get p pr) with sem_mem : val -> instr_state -> expression -> Memory.mem -> Prop := | Sstore : @@ -458,7 +457,7 @@ with sem_mem : sem_mem sp st (Estore mem_exp chunk addr args val_exp) m'' | Sbase_mem : forall rs m sp pr, - sem_mem sp (InstrState rs pr m) (Ebase Mem) m + sem_mem sp (mk_instr_state rs pr m) (Ebase Mem) m with sem_val_list : val -> instr_state -> expression_list -> list val -> Prop := | Snil : @@ -469,35 +468,51 @@ with sem_val_list : sem_value sp st e v -> sem_val_list sp st l lv -> sem_val_list sp st (Econs e l) (v :: lv) -with sem_val_ep_list : - val -> instr_state -> expr_pred_list -> val -> Prop := -| SPnil : - forall sp rs r m pr, - sem_val_ep_list sp (InstrState rs pr m) EPnil (rs !! r) -| SPconsTrue : - forall pr p sp rs m e v el, - eval_predf pr p = true -> - sem_value sp (InstrState rs pr m) e v -> - sem_val_ep_list sp (InstrState rs pr m) (EPcons p e el) v -| SPconsFalse : - forall pr p sp rs m e v el, - eval_predf pr p = false -> - sem_val_ep_list sp (InstrState rs pr m) el v -> - sem_val_ep_list sp (InstrState rs pr m) (EPcons p e el) v . +Inductive sem_pred_expr {A: Type} (sem: val -> instr_state -> expression -> A -> Prop): + val -> instr_state -> pred_expr -> A -> Prop := +| sem_pred_expr_base : + forall sp st e v, + sem sp st e v -> + sem_pred_expr sem sp st (PEsingleton None e) v +| sem_pred_expr_p : + forall sp st e p v, + eval_predf (instr_st_predset st) p = true -> + sem sp st e v -> + sem_pred_expr sem sp st (PEsingleton (Some p) e) v +| sem_pred_expr_cons_true : + forall sp st e pr p' v, + eval_predf (instr_st_predset st) pr = true -> + sem sp st e v -> + sem_pred_expr sem sp st (PEcons pr e p') v +| sem_pred_expr_cons_false : + forall sp st e pr p' v, + eval_predf (instr_st_predset st) pr = false -> + sem_pred_expr sem sp st p' v -> + sem_pred_expr sem sp st (PEcons pr e p') v +. + +Definition collapse_pe (p: pred_expr) : option expression := + match p with + | PEsingleton None p => Some p + | _ => None + end. + Inductive sem_predset : val -> instr_state -> forest -> predset -> Prop := | Spredset: forall st f sp rs', - (forall x, sem_pred sp st (f # (Pred x)) (PMap.get x rs')) -> + (forall pe x, + collapse_pe (f # (Pred x)) = Some pe -> + sem_pred sp st pe (PMap.get x rs')) -> sem_predset sp st f rs'. Inductive sem_regset : val -> instr_state -> forest -> regset -> Prop := | Sregset: forall st f sp rs', - (forall x, sem_value sp st (f # (Reg x)) (rs' !! x)) -> + (forall x, sem_pred_expr sem_value sp st (f # (Reg x)) (rs' !! x)) -> sem_regset sp st f rs'. Inductive sem : @@ -506,55 +521,11 @@ Inductive sem : forall st rs' m' f sp pr', sem_regset sp st f rs' -> sem_predset sp st f pr' -> - sem_mem sp st (f # Mem) m' -> - sem sp st f (InstrState rs' pr' m'). + sem_pred_expr sem_mem sp st (f # Mem) m' -> + sem sp st f (mk_instr_state rs' pr' m'). End SEMANTICS. -Definition hash_pred := @pred positive. - -Definition hash_tree := PTree.t (condition * list reg). - -Definition find_tree (el: predicate * list reg) (h: hash_tree) : option positive := - match - filter (fun x => match x with (a, b) => if hash_el_dec el b then true else false end) - (PTree.elements h) with - | (p, _) :: nil => Some p - | _ => None - end. - -Definition combine_option {A} (a b: option A) : option A := - match a, b with - | Some a', _ => Some a' - | _, Some b' => Some b' - | _, _ => None - end. - -Definition max_key {A} (t: PTree.t A) := - fold_right Pos.max 1 (map fst (PTree.elements t)). - -Fixpoint hash_predicate (p: predicate) (h: PTree.t (condition * list reg)) - : hash_pred * PTree.t (condition * list reg) := - match p with - | T => (T, h) - | ⟂ => (⟂, h) - | Pbase (b, (c, args)) => - match find_tree (c, args) h with - | Some p => (Pbase (b, p), h) - | None => - let nkey := max_key h + 1 in - (Pbase (b, nkey), PTree.set nkey (c, args) h) - end - | p1 ∧ p2 => - let (p1', t1) := hash_predicate p1 h in - let (p2', t2) := hash_predicate p2 t1 in - (p1' ∧ p2', t2) - | p1 ∨ p2 => - let (p1', t1) := hash_predicate p1 h in - let (p2', t2) := hash_predicate p2 t1 in - (p1' ∨ p2', t2) - end. - Fixpoint beq_expression (e1 e2: expression) {struct e1}: bool := match e1, e2 with | Ebase r1, Ebase r2 => if resource_eq r1 r2 then true else false @@ -578,7 +549,6 @@ Fixpoint beq_expression (e1 e2: expression) {struct e1}: bool := then if condition_eq c1 c2 then if beq_expression_list el1 el2 then beq_expression m1 m2 else false else false else false - | Econd el1, Econd el2 => beq_expr_pred_list el1 el2 | _, _ => false end with beq_expression_list (el1 el2: expression_list) {struct el1} : bool := @@ -587,17 +557,10 @@ with beq_expression_list (el1 el2: expression_list) {struct el1} : bool := | Econs e1 t1, Econs e2 t2 => beq_expression e1 e2 && beq_expression_list t1 t2 | _, _ => false end -with beq_expr_pred_list (el1 el2: expr_pred_list) {struct el1} : bool := - match el1, el2 with - | EPnil, EPnil => true - | EPcons p1 e1 el1', EPcons p2 e2 el2' => true - | _, _ => false - end . Scheme expression_ind2 := Induction for expression Sort Prop with expression_list_ind2 := Induction for expression_list Sort Prop - with expr_pred_list_ind2 := Induction for expr_pred_list Sort Prop . Lemma beq_expression_correct: @@ -608,38 +571,116 @@ Proof. (P := fun (e1 : expression) => forall e2, beq_expression e1 e2 = true -> e1 = e2) (P0 := fun (e1 : expression_list) => - forall e2, beq_expression_list e1 e2 = true -> e1 = e2) - (P1 := fun (e1 : expr_pred_list) => - forall e2, beq_expr_pred_list e1 e2 = true -> e1 = e2); simplify; + forall e2, beq_expression_list e1 e2 = true -> e1 = e2); try solve [repeat match goal with | [ H : context[match ?x with _ => _ end] |- _ ] => destruct x eqn:? | [ H : context[if ?x then _ else _] |- _ ] => destruct x eqn:? end; subst; f_equal; crush; eauto using Peqb_true_eq]. destruct e2; try discriminate. eauto. -Qed. +Abort. -Definition empty : forest := Rtree.empty _. +Definition hash_tree := PTree.t expression. -(*| -This function checks if all the elements in [fa] are in [fb], but not the other way round. -|*) +Definition find_tree (el: expression) (h: hash_tree) : option positive := + match filter (fun x => beq_expression el (snd x)) (PTree.elements h) with + | (p, _) :: nil => Some p + | _ => None + end. -Definition check := Rtree.beq beq_expression. +Definition combine_option {A} (a b: option A) : option A := + match a, b with + | Some a', _ => Some a' + | _, Some b' => Some b' + | _, _ => None + end. + +Definition max_key {A} (t: PTree.t A) := + fold_right Pos.max 1%positive (map fst (PTree.elements t)). + +Definition hash_expr (max: predicate) (e: expression) (h: hash_tree): predicate * hash_tree := + match find_tree e h with + | Some p => (p, h) + | None => + let nkey := Pos.max max (max_key h) + 1 in + (nkey, PTree.set nkey e h) + end. + +Fixpoint encode_expression (max: predicate) (pe: pred_expr) (h: hash_tree): pred_op * hash_tree := + match pe with + | PEsingleton None e => + let (p, h') := hash_expr max e h in + (Pvar p, h') + | PEsingleton (Some p) e => + let (p', h') := hash_expr max e h in + (Por (Pnot p) (Pvar p'), h') + | PEcons p e pe' => + let (p', h') := hash_expr max e h in + let (p'', h'') := encode_expression max pe' h' in + (Pand (Por (Pnot p) (Pvar p')) p'', h'') + end. + +Fixpoint max_predicate (p: pred_op) : positive := + match p with + | Pvar p => p + | Pand a b => Pos.max (max_predicate a) (max_predicate b) + | Por a b => Pos.max (max_predicate a) (max_predicate b) + | Pnot a => max_predicate a + end. + +Fixpoint max_pred_expr (pe: pred_expr) : positive := + match pe with + | PEsingleton None _ => 1 + | PEsingleton (Some p) _ => max_predicate p + | PEcons p _ pe' => Pos.max (max_predicate p) (max_pred_expr pe') + end. + +Definition beq_pred_expr (bound: nat) (pe1 pe2: pred_expr) : bool := + match pe1, pe2 with + (*| PEsingleton None e1, PEsingleton None e2 => beq_expression e1 e2 + | PEsingleton (Some p1) e1, PEsingleton (Some p2) e2 => + if beq_expression e1 e2 + then match sat_pred_simple bound (Por (Pand p1 (Pnot p2)) (Pand p2 (Pnot p1))) with + | Some None => true + | _ => false + end + else false + | PEsingleton (Some p) e1, PEsingleton None e2 + | PEsingleton None e1, PEsingleton (Some p) e2 => + if beq_expression e1 e2 + then match sat_pred_simple bound (Pnot p) with + | Some None => true + | _ => false + end + else false*) + | pe1, pe2 => + let max := Pos.max (max_pred_expr pe1) (max_pred_expr pe2) in + let (p1, h) := encode_expression max pe1 (PTree.empty _) in + let (p2, h') := encode_expression max pe2 h in + match sat_pred_simple bound (Por (Pand p1 (Pnot p2)) (Pand p2 (Pnot p1))) with + | Some None => true + | _ => false + end + end. + +Definition empty : forest := Rtree.empty _. + +Definition check := Rtree.beq (beq_pred_expr 10000). Lemma check_correct: forall (fa fb : forest), check fa fb = true -> (forall x, fa # x = fb # x). Proof. - unfold check, get_forest; intros; + (*unfold check, get_forest; intros; pose proof beq_expression_correct; match goal with [ Hbeq : context[Rtree.beq], y : Rtree.elt |- _ ] => apply (Rtree.beq_sound beq_expression fa fb) with (x := y) in Hbeq end; repeat destruct_match; crush. -Qed. +Qed.*) + Abort. Lemma get_empty: - forall r, empty#r = Ebase r. + forall r, empty#r = PEsingleton None (Ebase r). Proof. intros; unfold get_forest; destruct_match; auto; [ ]; @@ -691,16 +732,11 @@ Proof. apply IHm1_2. intros; apply (H (xI x)). Qed. -Lemma map0: - forall r, - empty # r = Ebase r. -Proof. intros; eapply get_empty. Qed. - Lemma map1: forall w dst dst', dst <> dst' -> - (empty # dst <- w) # dst' = Ebase dst'. -Proof. intros; unfold get_forest; rewrite Rtree.gso; auto; apply map0. Qed. + (empty # dst <- w) # dst' = PEsingleton None (Ebase dst'). +Proof. intros; unfold get_forest; rewrite Rtree.gso; auto; apply get_empty. Qed. Lemma genmap1: forall (f : forest) w dst dst', @@ -709,7 +745,7 @@ Lemma genmap1: Proof. intros; unfold get_forest; rewrite Rtree.gso; auto. Qed. Lemma map2: - forall (v : expression) x rs, + forall (v : pred_expr) x rs, (rs # x <- v) # x = v. Proof. intros; unfold get_forest; rewrite Rtree.gss; trivial. Qed. @@ -736,14 +772,14 @@ Inductive match_states : instr_state -> instr_state -> Prop := forall rs rs' m m', (forall x, rs !! x = rs' !! x) -> m = m' -> - match_states (InstrState rs m) (InstrState rs' m'). + match_states (mk_instr_state rs m) (mk_instr_state rs' m'). Inductive match_states_ld : instr_state -> instr_state -> Prop := | match_states_ld_intro: forall rs rs' m m', regs_lessdef rs rs' -> Mem.extends m m' -> - match_states_ld (InstrState rs m) (InstrState rs' m'). + match_states_ld (mk_instr_state rs m) (mk_instr_state rs' m'). Lemma sems_det: forall A ge tge sp st f, @@ -761,7 +797,7 @@ Proof. Abort. v = v'. Proof. intros. destruct st. - generalize (sems_det A ge tge sp (InstrState rs m) f H v v' + generalize (sems_det A ge tge sp (mk_instr_state rs m) f H v v' m m); crush. Qed. @@ -784,7 +820,7 @@ Lemma sem_mem_det: m = m'. Proof. intros. destruct st. - generalize (sems_det A ge tge sp (InstrState rs m0) f H sp sp m m'); + generalize (sems_det A ge tge sp (mk_instr_state rs m0) f H sp sp m m'); crush. Qed. Hint Resolve sem_mem_det : rtlpar. @@ -928,14 +964,14 @@ Abstract computations ===================== |*) -Definition is_regs i := match i with InstrState rs _ => rs end. -Definition is_mem i := match i with InstrState _ m => m end. +Definition is_regs i := match i with mk_instr_state rs _ => rs end. +Definition is_mem i := match i with mk_instr_state _ m => m end. Inductive state_lessdef : instr_state -> instr_state -> Prop := state_lessdef_intro : forall rs1 rs2 m1, (forall x, rs1 !! x = rs2 !! x) -> - state_lessdef (InstrState rs1 m1) (InstrState rs2 m1). + state_lessdef (mk_instr_state rs1 m1) (mk_instr_state rs2 m1). (*| RTLBlock to abstract translation @@ -1177,9 +1213,9 @@ Lemma sem_update_Op : forall A ge sp st f st' r l o0 o m rs v, @sem A ge sp st f st' -> Op.eval_operation ge sp o0 rs ## l m = Some v -> - match_states st' (InstrState rs m) -> + match_states st' (mk_instr_state rs m) -> exists tst, - sem ge sp st (update f (RBop o o0 l r)) tst /\ match_states (InstrState (Regmap.set r v rs) m) tst. + sem ge sp st (update f (RBop o o0 l r)) tst /\ match_states (mk_instr_state (Regmap.set r v rs) m) tst. Proof. intros. inv H1. simplify. destruct st. @@ -1201,10 +1237,10 @@ Lemma sem_update_load : @sem A ge sp st f st' -> Op.eval_addressing ge sp a rs ## l = Some a0 -> Mem.loadv m m0 a0 = Some v -> - match_states st' (InstrState rs m0) -> + match_states st' (mk_instr_state rs m0) -> exists tst : instr_state, sem ge sp st (update f (RBload o m a l r)) tst - /\ match_states (InstrState (Regmap.set r v rs) m0) tst. + /\ match_states (mk_instr_state (Regmap.set r v rs) m0) tst. Proof. intros. inv H2. pose proof H. inv H. inv H9. destruct st. @@ -1226,9 +1262,9 @@ Lemma sem_update_store : @sem A ge sp st f st' -> Op.eval_addressing ge sp a rs ## l = Some a0 -> Mem.storev m m0 a0 rs !! r = Some m' -> - match_states st' (InstrState rs m0) -> + match_states st' (mk_instr_state rs m0) -> exists tst, sem ge sp st (update f (RBstore o m a l r)) tst - /\ match_states (InstrState rs m') tst. + /\ match_states (mk_instr_state rs m') tst. Proof. intros. inv H2. pose proof H. inv H. inv H9. destruct st. @@ -1258,9 +1294,9 @@ Qed. Lemma sem_update2_Op : forall A ge sp st f r l o0 o m rs v, - @sem A ge sp st f (InstrState rs m) -> + @sem A ge sp st f (mk_instr_state rs m) -> Op.eval_operation ge sp o0 rs ## l m = Some v -> - sem ge sp st (update f (RBop o o0 l r)) (InstrState (Regmap.set r v rs) m). + sem ge sp st (update f (RBop o o0 l r)) (mk_instr_state (Regmap.set r v rs) m). Proof. intros. destruct st. constructor. inv H. inv H6. @@ -1275,10 +1311,10 @@ Qed. Lemma sem_update2_load : forall A ge sp st f r o m a l m0 rs v a0, - @sem A ge sp st f (InstrState rs m0) -> + @sem A ge sp st f (mk_instr_state rs m0) -> Op.eval_addressing ge sp a rs ## l = Some a0 -> Mem.loadv m m0 a0 = Some v -> - sem ge sp st (update f (RBload o m a l r)) (InstrState (Regmap.set r v rs) m0). + sem ge sp st (update f (RBload o m a l r)) (mk_instr_state (Regmap.set r v rs) m0). Proof. intros. simplify. inv H. inv H7. constructor. { constructor; intros. destruct (Pos.eq_dec r x); subst. @@ -1291,10 +1327,10 @@ Qed. Lemma sem_update2_store : forall A ge sp a0 m a l r o f st m' rs m0, - @sem A ge sp st f (InstrState rs m0) -> + @sem A ge sp st f (mk_instr_state rs m0) -> Op.eval_addressing ge sp a rs ## l = Some a0 -> Mem.storev m m0 a0 rs !! r = Some m' -> - sem ge sp st (update f (RBstore o m a l r)) (InstrState rs m'). + sem ge sp st (update f (RBstore o m a l r)) (mk_instr_state rs m'). Proof. intros. simplify. inv H. inv H7. constructor; simplify. { econstructor; intros. rewrite genmap1; crush. } -- cgit From 3f6f15b6f59df5aa78df6e77cdf970af7eb25302 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Wed, 22 Sep 2021 19:54:11 +0100 Subject: RTLpargen passes compilation again --- src/hls/RTLPargen.v | 24 ++++++++++++++++-------- 1 file changed, 16 insertions(+), 8 deletions(-) (limited to 'src/hls/RTLPargen.v') diff --git a/src/hls/RTLPargen.v b/src/hls/RTLPargen.v index 09eabc9..46b06c0 100644 --- a/src/hls/RTLPargen.v +++ b/src/hls/RTLPargen.v @@ -444,7 +444,7 @@ with sem_pred : sem_pred sp st (Esetpred p c args pred_exp) v | Sbase_pred: forall rs pr m p sp, - sem_pred sp (mk_instr_state rs pr m) (Ebase (Pred p)) (PMap.get p pr) + sem_pred sp (mk_instr_state rs pr m) (Ebase (Pred p)) (pr !! p) with sem_mem : val -> instr_state -> expression -> Memory.mem -> Prop := | Sstore : @@ -505,7 +505,7 @@ Inductive sem_predset : forall st f sp rs', (forall pe x, collapse_pe (f # (Pred x)) = Some pe -> - sem_pred sp st pe (PMap.get x rs')) -> + sem_pred sp st pe (rs' !! x)) -> sem_predset sp st f rs'. Inductive sem_regset : @@ -666,6 +666,12 @@ Definition empty : forest := Rtree.empty _. Definition check := Rtree.beq (beq_pred_expr 10000). +Compute (check (empty # (Reg 2) <- + (PEcons (Pand (Pvar 4) (Pnot (Pvar 4))) (Ebase (Reg 9)) + (PEsingleton (Some (Pvar 2)) (Ebase (Reg 3))))) + (empty # (Reg 2) <- (PEsingleton (Some (Por (Pvar 2) (Pand (Pvar 3) (Pnot (Pvar 3))))) + (Ebase (Reg 3))))). + Lemma check_correct: forall (fa fb : forest), check fa fb = true -> (forall x, fa # x = fb # x). Proof. @@ -769,24 +775,26 @@ Ltac rtlpar_crush := crush; eauto with rtlpar. Inductive match_states : instr_state -> instr_state -> Prop := | match_states_intro: - forall rs rs' m m', + forall ps ps' rs rs' m m', (forall x, rs !! x = rs' !! x) -> + (forall x, ps !! x = ps' !! x) -> m = m' -> - match_states (mk_instr_state rs m) (mk_instr_state rs' m'). + match_states (mk_instr_state rs ps m) (mk_instr_state rs' ps' m'). Inductive match_states_ld : instr_state -> instr_state -> Prop := | match_states_ld_intro: - forall rs rs' m m', + forall ps ps' rs rs' m m', regs_lessdef rs rs' -> + (forall x, ps !! x = ps' !! x) -> Mem.extends m m' -> - match_states_ld (mk_instr_state rs m) (mk_instr_state rs' m'). + match_states_ld (mk_instr_state rs ps m) (mk_instr_state rs' ps' m'). Lemma sems_det: forall A ge tge sp st f, ge_preserved ge tge -> forall v v' mv mv', - (sem_value A ge sp st f v /\ sem_value A tge sp st f v' -> v = v') /\ - (sem_mem A ge sp st f mv /\ sem_mem A tge sp st f mv' -> mv = mv'). + (@sem_value A ge sp st f v /\ @sem_value A tge sp st f v' -> v = v') /\ + (@sem_mem A ge sp st f mv /\ @sem_mem A tge sp st f mv' -> mv = mv'). Proof. Abort. (*Lemma sem_value_det: -- cgit From d8609f77bf5a29c52da8f51b3a248050716c30a4 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Fri, 24 Sep 2021 12:45:37 +0100 Subject: Add back top-level functions --- src/hls/RTLPargen.v | 197 +++++++++++++++++++++++++++++++++++++++++----------- 1 file changed, 157 insertions(+), 40 deletions(-) (limited to 'src/hls/RTLPargen.v') diff --git a/src/hls/RTLPargen.v b/src/hls/RTLPargen.v index 46b06c0..208a966 100644 --- a/src/hls/RTLPargen.v +++ b/src/hls/RTLPargen.v @@ -31,7 +31,8 @@ Require Import vericert.hls.RTLBlock. Require Import vericert.hls.RTLPar. Require Import vericert.hls.RTLBlockInstr. -#[local] Open Scope positive. +#[local] +Open Scope positive. (*| Schedule Oracle @@ -223,22 +224,82 @@ with expression_list : Type := | Econs : expression -> expression_list -> expression_list . -Inductive pred_expr : Type := +(*Inductive pred_expr : Type := | PEsingleton : option pred_op -> expression -> pred_expr -| PEcons : pred_op -> expression -> pred_expr -> pred_expr. +| PEcons : option pred_op -> expression -> pred_expr -> pred_expr.*) -Definition pred_list_wf l : Prop := - forall a b, In a l -> In b l -> a <> b -> unsat (Pand a b). +Module NonEmpty. -Fixpoint pred_expr_list (p: pred_expr) := - match p with - | PEsingleton None _ => nil - | PEsingleton (Some pr) e => (pr, e) :: nil - | PEcons pr e p' => (pr, e) :: pred_expr_list p' +Inductive non_empty (A: Type) := +| singleton : A -> non_empty A +| cons : A -> non_empty A -> non_empty A +. + +Arguments singleton [A]. +Arguments cons [A]. + +Delimit Scope list_scope with list. + +Infix "::|" := cons (at level 60, right associativity) : list_scope. + +#[local] Open Scope list_scope. + +Fixpoint map {A B} (f: A -> B) (l: non_empty A): non_empty B := + match l with + | singleton a => singleton (f a) + | a ::| b => f a ::| map f b + end. + +Fixpoint to_list {A} (l: non_empty A): list A := + match l with + | singleton a => a::nil + | a ::| b => a :: to_list b + end. + +Fixpoint app {A} (l1 l2: non_empty A) := + match l1 with + | singleton a => a ::| l2 + | a ::| b => a ::| app b l2 end. +Fixpoint non_empty_prod {A B} (l: non_empty A) (l': non_empty B) := + match l with + | singleton a => map (fun x => (a, x)) l' + | a ::| b => app (map (fun x => (a, x)) l') (non_empty_prod b l') + end. + +Fixpoint of_list {A} (l: list A): option (non_empty A) := + match l with + | a::b => + match of_list b with + | Some b' => Some (a ::| b') + | _ => None + end + | nil => None + end. + +End NonEmpty. +Module NE := NonEmpty. + +Module NonEmptyNotation. + + Notation "A '::|' B" := (NE.cons A B) (at level 70, right associativity) : non_empty. + +End NonEmptyNotation. +Import NonEmptyNotation. + +#[local] + Open Scope non_empty. + +Definition predicated A := NE.non_empty (option pred_op * A). + +Definition pred_expr := predicated expression. + +Definition pred_list_wf l : Prop := + forall a b, In (Some a) l -> In (Some b) l -> a <> b -> unsat (Pand a b). + Definition pred_list_wf_ep (l: pred_expr) : Prop := - pred_list_wf (map fst (pred_expr_list l)). + pred_list_wf (NE.to_list (NE.map fst l)). Lemma unsat_correct1 : forall a b c, @@ -387,7 +448,7 @@ Definition forest : Type := Rtree.t pred_expr. Definition get_forest v (f: forest) := match Rtree.get v f with - | None => PEsingleton None (Ebase v) + | None => NE.singleton (None, (Ebase v)) | Some v' => v' end. @@ -475,27 +536,31 @@ Inductive sem_pred_expr {A: Type} (sem: val -> instr_state -> expression -> A -> | sem_pred_expr_base : forall sp st e v, sem sp st e v -> - sem_pred_expr sem sp st (PEsingleton None e) v + sem_pred_expr sem sp st (NE.singleton (None, e)) v | sem_pred_expr_p : forall sp st e p v, eval_predf (instr_st_predset st) p = true -> sem sp st e v -> - sem_pred_expr sem sp st (PEsingleton (Some p) e) v + sem_pred_expr sem sp st (NE.singleton (Some p, e)) v | sem_pred_expr_cons_true : forall sp st e pr p' v, eval_predf (instr_st_predset st) pr = true -> sem sp st e v -> - sem_pred_expr sem sp st (PEcons pr e p') v + sem_pred_expr sem sp st ((Some pr, e)::|p') v | sem_pred_expr_cons_false : forall sp st e pr p' v, eval_predf (instr_st_predset st) pr = false -> sem_pred_expr sem sp st p' v -> - sem_pred_expr sem sp st (PEcons pr e p') v + sem_pred_expr sem sp st ((Some pr, e)::|p') v +| sem_pred_expr_cons_None : + forall sp st e p' v, + sem sp st e v -> + sem_pred_expr sem sp st ((None, e)::|p') v . Definition collapse_pe (p: pred_expr) : option expression := match p with - | PEsingleton None p => Some p + | NE.singleton (None, p) => Some p | _ => None end. @@ -607,16 +672,20 @@ Definition hash_expr (max: predicate) (e: expression) (h: hash_tree): predicate Fixpoint encode_expression (max: predicate) (pe: pred_expr) (h: hash_tree): pred_op * hash_tree := match pe with - | PEsingleton None e => + | NE.singleton (None, e) => let (p, h') := hash_expr max e h in (Pvar p, h') - | PEsingleton (Some p) e => + | NE.singleton (Some p, e) => let (p', h') := hash_expr max e h in (Por (Pnot p) (Pvar p'), h') - | PEcons p e pe' => + | (Some p, e)::|pe' => let (p', h') := hash_expr max e h in let (p'', h'') := encode_expression max pe' h' in (Pand (Por (Pnot p) (Pvar p')) p'', h'') + | (None, e)::|pe' => + let (p', h') := hash_expr max e h in + let (p'', h'') := encode_expression max pe' h' in + (Pand (Pvar p') p'', h'') end. Fixpoint max_predicate (p: pred_op) : positive := @@ -629,9 +698,10 @@ Fixpoint max_predicate (p: pred_op) : positive := Fixpoint max_pred_expr (pe: pred_expr) : positive := match pe with - | PEsingleton None _ => 1 - | PEsingleton (Some p) _ => max_predicate p - | PEcons p _ pe' => Pos.max (max_predicate p) (max_pred_expr pe') + | NE.singleton (None, _) => 1 + | NE.singleton (Some p, _) => max_predicate p + | (Some p, _) ::| pe' => Pos.max (max_predicate p) (max_pred_expr pe') + | (None, _) ::| pe' => (max_pred_expr pe') end. Definition beq_pred_expr (bound: nat) (pe1 pe2: pred_expr) : bool := @@ -667,10 +737,10 @@ Definition empty : forest := Rtree.empty _. Definition check := Rtree.beq (beq_pred_expr 10000). Compute (check (empty # (Reg 2) <- - (PEcons (Pand (Pvar 4) (Pnot (Pvar 4))) (Ebase (Reg 9)) - (PEsingleton (Some (Pvar 2)) (Ebase (Reg 3))))) - (empty # (Reg 2) <- (PEsingleton (Some (Por (Pvar 2) (Pand (Pvar 3) (Pnot (Pvar 3))))) - (Ebase (Reg 3))))). + (((Some (Pand (Pvar 4) (Pnot (Pvar 4)))), (Ebase (Reg 9))) ::| + (NE.singleton ((Some (Pvar 2)), (Ebase (Reg 3)))))) + (empty # (Reg 2) <- (NE.singleton ((Some (Por (Pvar 2) (Pand (Pvar 3) (Pnot (Pvar 3))))), + (Ebase (Reg 3)))))). Lemma check_correct: forall (fa fb : forest), check fa fb = true -> (forall x, fa # x = fb # x). @@ -686,7 +756,7 @@ Qed.*) Abort. Lemma get_empty: - forall r, empty#r = PEsingleton None (Ebase r). + forall r, empty#r = NE.singleton (None, Ebase r). Proof. intros; unfold get_forest; destruct_match; auto; [ ]; @@ -741,7 +811,7 @@ Qed. Lemma map1: forall w dst dst', dst <> dst' -> - (empty # dst <- w) # dst' = PEsingleton None (Ebase dst'). + (empty # dst <- w) # dst' = NE.singleton (None, Ebase dst'). Proof. intros; unfold get_forest; rewrite Rtree.gso; auto; apply get_empty. Qed. Lemma genmap1: @@ -881,22 +951,70 @@ Proof. eauto with rtlpar. Qed. (*| Update functions. |*) +*) -Fixpoint list_translation (l : list reg) (f : forest) {struct l} : expression_list := +Fixpoint list_translation (l : list reg) (f : forest) {struct l} : list pred_expr := match l with - | nil => Enil - | i :: l => Econs (f # (Reg i)) (list_translation l f) + | nil => nil + | i :: l => (f # (Reg i)) :: (list_translation l f) + end. + +Fixpoint replicate {A} (n: nat) (l: A) := + match n with + | O => nil + | S n => l :: replicate n l + end. + +Definition merge''' x y := + match x, y with + | Some p1, Some p2 => Some (Pand p1 p2) + | Some p, None | None, Some p => Some p + | None, None => None end. +Definition merge'' x := + match x with + | ((a, e), (b, el)) => (merge''' a b, Econs e el) + end. + +(*map (fun x => (fst x, Econs (snd x) Enil)) pel*) +Fixpoint merge' (pel: pred_expr) (tpel: predicated expression_list) := + NE.map merge'' (NE.non_empty_prod pel tpel). + +Fixpoint merge (pel: list pred_expr): predicated expression_list := + match pel with + | nil => NE.singleton (None, Enil) + | a :: b => merge' a (merge b) + end. + +Definition map_pred_op {A B} (pf: option pred_op * (A -> B)) (pa: option pred_op * A): option pred_op * B := + match pa, pf with + | (p, a), (p', f) => (merge''' p p', f a) + end. + +Definition map_predicated {A B} (pf: predicated (A -> B)) (pa: predicated A): predicated B := + NE.map (fun x => match x with ((p1, f), (p2, a)) => (merge''' p1 p2, f a) end) (NE.non_empty_prod pf pa). + +Definition apply1_predicated {A B} (pf: predicated (A -> B)) (pa: A): predicated B := + NE.map (fun x => (fst x, (snd x) pa)) pf. + +Definition apply2_predicated {A B C} (pf: predicated (A -> B -> C)) (pa: A) (pb: B): predicated C := + NE.map (fun x => (fst x, (snd x) pa pb)) pf. + +Definition apply3_predicated {A B C D} (pf: predicated (A -> B -> C -> D)) (pa: A) (pb: B) (pc: C): predicated D := + NE.map (fun x => (fst x, (snd x) pa pb pc)) pf. + +(*Compute merge (((Some (Pvar 2), Ebase (Reg 4))::nil)::((Some (Pvar 3), Ebase (Reg 3))::(Some (Pvar 1), Ebase (Reg 3))::nil)::nil).*) + Definition update (f : forest) (i : instr) : forest := match i with | RBnop => f | RBop p op rl r => - f # (Reg r) <- (Eop op (list_translation rl f) (f # Mem)) + f # (Reg r) <- (map_predicated (map_predicated (NE.singleton (p, Eop op)) (merge (list_translation rl f))) (f # Mem)) | RBload p chunk addr rl r => - f # (Reg r) <- (Eload chunk addr (list_translation rl f) (f # Mem)) + f # (Reg r) <- (map_predicated (map_predicated (NE.singleton (p, Eload chunk addr)) (merge (list_translation rl f))) (f # Mem)) | RBstore p chunk addr rl r => - f # Mem <- (Estore (f # Mem) chunk addr (list_translation rl f) (f # (Reg r))) + f # Mem <- (map_predicated (map_predicated (apply2_predicated (map_predicated (NE.singleton (p, Estore)) (f # Mem)) chunk addr) (merge (list_translation rl f))) (f # (Reg r))) | RBsetpred c addr p => f end. @@ -972,7 +1090,7 @@ Abstract computations ===================== |*) -Definition is_regs i := match i with mk_instr_state rs _ => rs end. +(*Definition is_regs i := match i with mk_instr_state rs _ => rs end. Definition is_mem i := match i with mk_instr_state _ m => m end. Inductive state_lessdef : instr_state -> instr_state -> Prop := @@ -1016,7 +1134,7 @@ Proof. constructor. unfold regs_lessdef. intros. inv H0. specialize (H1 x). inv H1; auto. auto. -Qed. +Qed.*) Definition check_dest i r' := match i with @@ -1040,7 +1158,7 @@ Lemma check_dest_l_forall : Forall (fun x => check_dest x r = false) l. Proof. induction l; crush. Qed. -Lemma check_dest_l_ex : +(*Lemma check_dest_l_ex : forall l r, check_dest_l l r = true -> exists a, In a l /\ check_dest a r = true. @@ -1650,7 +1768,7 @@ Qed. /\ match_states st' tst'. Proof. intros.*) - +*) (*| Top-level functions @@ -1674,4 +1792,3 @@ Definition transl_fundef := transf_partial_fundef transl_function. Definition transl_program (p : RTLBlock.program) : Errors.res RTLPar.program := transform_partial_program transl_fundef p. -*) -- cgit From 244270b446721d5eeb1ed15ec2839aa4d246965c Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Fri, 24 Sep 2021 12:57:32 +0100 Subject: Fix scoping --- src/hls/RTLPargen.v | 22 ++++++++++------------ 1 file changed, 10 insertions(+), 12 deletions(-) (limited to 'src/hls/RTLPargen.v') diff --git a/src/hls/RTLPargen.v b/src/hls/RTLPargen.v index 208a966..adcd2b3 100644 --- a/src/hls/RTLPargen.v +++ b/src/hls/RTLPargen.v @@ -238,11 +238,15 @@ Inductive non_empty (A: Type) := Arguments singleton [A]. Arguments cons [A]. -Delimit Scope list_scope with list. +Declare Scope non_empty_scope. +Delimit Scope non_empty_scope with non_empty. -Infix "::|" := cons (at level 60, right associativity) : list_scope. +Module NonEmptyNotation. +Infix "::|" := cons (at level 60, right associativity) : non_empty_scope. +End NonEmptyNotation. +Import NonEmptyNotation. -#[local] Open Scope list_scope. +#[local] Open Scope non_empty_scope. Fixpoint map {A B} (f: A -> B) (l: non_empty A): non_empty B := match l with @@ -279,17 +283,11 @@ Fixpoint of_list {A} (l: list A): option (non_empty A) := end. End NonEmpty. -Module NE := NonEmpty. - -Module NonEmptyNotation. - Notation "A '::|' B" := (NE.cons A B) (at level 70, right associativity) : non_empty. - -End NonEmptyNotation. -Import NonEmptyNotation. +Module NE := NonEmpty. +Import NE.NonEmptyNotation. -#[local] - Open Scope non_empty. +#[local] Open Scope non_empty_scope. Definition predicated A := NE.non_empty (option pred_op * A). -- cgit From c5003f6f33c2f54e16f03773b49f93f33643d0c9 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Fri, 1 Oct 2021 14:15:55 +0100 Subject: Improve equivalence checking using SAT --- src/hls/RTLPargen.v | 37 ++++++++++++++++++++++--------------- 1 file changed, 22 insertions(+), 15 deletions(-) (limited to 'src/hls/RTLPargen.v') diff --git a/src/hls/RTLPargen.v b/src/hls/RTLPargen.v index adcd2b3..44a7721 100644 --- a/src/hls/RTLPargen.v +++ b/src/hls/RTLPargen.v @@ -218,7 +218,7 @@ Inductive expression : Type := | Eop : Op.operation -> expression_list -> expression -> expression | Eload : AST.memory_chunk -> Op.addressing -> expression_list -> expression -> expression | Estore : expression -> AST.memory_chunk -> Op.addressing -> expression_list -> expression -> expression -| Esetpred : predicate -> Op.condition -> expression_list -> expression -> expression +| Esetpred : Op.condition -> expression_list -> expression -> expression with expression_list : Type := | Enil : expression_list | Econs : expression -> expression_list -> expression_list @@ -496,11 +496,11 @@ Inductive sem_value : with sem_pred : val -> instr_state -> expression -> bool -> Prop := | Spred: - forall st pred_exp args p c lv m m' v sp, - sem_pred sp st pred_exp m' -> + forall st mem_exp args c lv m' v sp, + sem_mem sp st mem_exp m' -> sem_val_list sp st args lv -> - Op.eval_condition c lv m = Some v -> - sem_pred sp st (Esetpred p c args pred_exp) v + Op.eval_condition c lv m' = Some v -> + sem_pred sp st (Esetpred c args mem_exp) v | Sbase_pred: forall rs pr m p sp, sem_pred sp (mk_instr_state rs pr m) (Ebase (Pred p)) (pr !! p) @@ -513,7 +513,7 @@ with sem_mem : sem_val_list sp st args lv -> Op.eval_addressing genv sp addr lv = Some a -> Memory.Mem.storev chunk m' a v = Some m'' -> - sem_mem sp st (Estore mem_exp chunk addr args val_exp) m'' + sem_mem sp st (Estore val_exp chunk addr args mem_exp) m'' | Sbase_mem : forall rs m sp pr, sem_mem sp (mk_instr_state rs pr m) (Ebase Mem) m @@ -601,17 +601,16 @@ Fixpoint beq_expression (e1 e2: expression) {struct e1}: bool := then if addressing_eq addr1 addr2 then if beq_expression_list el1 el2 then beq_expression e1 e2 else false else false else false - | Estore m1 chk1 addr1 el1 e1, Estore m2 chk2 addr2 el2 e2=> + | Estore e1 chk1 addr1 el1 m1, Estore e2 chk2 addr2 el2 m2 => if memory_chunk_eq chk1 chk2 then if addressing_eq addr1 addr2 then if beq_expression_list el1 el2 then if beq_expression m1 m2 then beq_expression e1 e2 else false else false else false else false - | Esetpred p1 c1 el1 m1, Esetpred p2 c2 el2 m2 => - if Pos.eqb p1 p2 - then if condition_eq c1 c2 - then if beq_expression_list el1 el2 - then beq_expression m1 m2 else false else false else false + | Esetpred c1 el1 m1, Esetpred c2 el2 m2 => + if condition_eq c1 c2 + then if beq_expression_list el1 el2 + then beq_expression m1 m2 else false else false | _, _ => false end with beq_expression_list (el1 el2: expression_list) {struct el1} : bool := @@ -1008,11 +1007,19 @@ Definition update (f : forest) (i : instr) : forest := match i with | RBnop => f | RBop p op rl r => - f # (Reg r) <- (map_predicated (map_predicated (NE.singleton (p, Eop op)) (merge (list_translation rl f))) (f # Mem)) + f # (Reg r) <- + (map_predicated (map_predicated (NE.singleton (p, Eop op)) (merge (list_translation rl f))) (f # Mem)) | RBload p chunk addr rl r => - f # (Reg r) <- (map_predicated (map_predicated (NE.singleton (p, Eload chunk addr)) (merge (list_translation rl f))) (f # Mem)) + f # (Reg r) <- + (map_predicated + (map_predicated (NE.singleton (p, Eload chunk addr)) (merge (list_translation rl f))) + (f # Mem)) | RBstore p chunk addr rl r => - f # Mem <- (map_predicated (map_predicated (apply2_predicated (map_predicated (NE.singleton (p, Estore)) (f # Mem)) chunk addr) (merge (list_translation rl f))) (f # (Reg r))) + f # Mem <- + (map_predicated + (map_predicated + (apply2_predicated (map_predicated (NE.singleton (p, Estore)) (f # (Reg r))) chunk addr) + (merge (list_translation rl f))) (f # Mem)) | RBsetpred c addr p => f end. -- cgit From 0ad95850cf12bfecbb25af9721f0626d4f75c687 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Fri, 1 Oct 2021 14:59:10 +0100 Subject: Fix equivalence checking Do not compare memories in standard operations --- src/hls/RTLPargen.v | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) (limited to 'src/hls/RTLPargen.v') diff --git a/src/hls/RTLPargen.v b/src/hls/RTLPargen.v index 44a7721..2f24a42 100644 --- a/src/hls/RTLPargen.v +++ b/src/hls/RTLPargen.v @@ -594,8 +594,7 @@ Fixpoint beq_expression (e1 e2: expression) {struct e1}: bool := | Ebase r1, Ebase r2 => if resource_eq r1 r2 then true else false | Eop op1 el1 exp1, Eop op2 el2 exp2 => if operation_eq op1 op2 then - if beq_expression exp1 exp2 then - beq_expression_list el1 el2 else false else false + beq_expression_list el1 el2 else false | Eload chk1 addr1 el1 e1, Eload chk2 addr2 el2 e2 => if memory_chunk_eq chk1 chk2 then if addressing_eq addr1 addr2 @@ -609,8 +608,7 @@ Fixpoint beq_expression (e1 e2: expression) {struct e1}: bool := then beq_expression e1 e2 else false else false else false else false | Esetpred c1 el1 m1, Esetpred c2 el2 m2 => if condition_eq c1 c2 - then if beq_expression_list el1 el2 - then beq_expression m1 m2 else false else false + then beq_expression_list el1 el2 else false | _, _ => false end with beq_expression_list (el1 el2: expression_list) {struct el1} : bool := -- cgit From 5e74413490019b0909f248ec2e0c331f11be6f5d Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Thu, 7 Oct 2021 19:48:51 +0100 Subject: RTLPargen now uses Abstr as symbolic execution target --- src/hls/RTLPargen.v | 706 +--------------------------------------------------- 1 file changed, 1 insertion(+), 705 deletions(-) (limited to 'src/hls/RTLPargen.v') diff --git a/src/hls/RTLPargen.v b/src/hls/RTLPargen.v index 2f24a42..fee24f3 100644 --- a/src/hls/RTLPargen.v +++ b/src/hls/RTLPargen.v @@ -31,321 +31,7 @@ Require Import vericert.hls.RTLBlock. Require Import vericert.hls.RTLPar. Require Import vericert.hls.RTLBlockInstr. -#[local] -Open Scope positive. - -(*| -Schedule Oracle -=============== - -This oracle determines if a schedule was valid by performing symbolic execution on the input and -output and showing that these behave the same. This acts on each basic block separately, as the -rest of the functions should be equivalent. -|*) - -Definition reg := positive. - -Inductive resource : Set := -| Reg : reg -> resource -| Pred : reg -> resource -| Mem : resource. - -(*| -The following defines quite a few equality comparisons automatically, however, these can be -optimised heavily if written manually, as their proofs are not needed. -|*) - -Lemma resource_eq : forall (r1 r2 : resource), {r1 = r2} + {r1 <> r2}. -Proof. - decide equality; apply Pos.eq_dec. -Defined. - -Lemma comparison_eq: forall (x y : comparison), {x = y} + {x <> y}. -Proof. - decide equality. -Defined. - -Lemma condition_eq: forall (x y : Op.condition), {x = y} + {x <> y}. -Proof. - generalize comparison_eq; intro. - generalize Int.eq_dec; intro. - generalize Int64.eq_dec; intro. - decide equality. -Defined. - -Lemma addressing_eq : forall (x y : Op.addressing), {x = y} + {x <> y}. -Proof. - generalize Int.eq_dec; intro. - generalize AST.ident_eq; intro. - generalize Z.eq_dec; intro. - generalize Ptrofs.eq_dec; intro. - decide equality. -Defined. - -Lemma typ_eq : forall (x y : AST.typ), {x = y} + {x <> y}. -Proof. - decide equality. -Defined. - -Lemma operation_eq: forall (x y : Op.operation), {x = y} + {x <> y}. -Proof. - generalize Int.eq_dec; intro. - generalize Int64.eq_dec; intro. - generalize Float.eq_dec; intro. - generalize Float32.eq_dec; intro. - generalize AST.ident_eq; intro. - generalize condition_eq; intro. - generalize addressing_eq; intro. - generalize typ_eq; intro. - decide equality. -Defined. - -Lemma memory_chunk_eq : forall (x y : AST.memory_chunk), {x = y} + {x <> y}. -Proof. - decide equality. -Defined. - -Lemma list_typ_eq: forall (x y : list AST.typ), {x = y} + {x <> y}. -Proof. - generalize typ_eq; intro. - decide equality. -Defined. - -Lemma option_typ_eq : forall (x y : option AST.typ), {x = y} + {x <> y}. -Proof. - generalize typ_eq; intro. - decide equality. -Defined. - -Lemma signature_eq: forall (x y : AST.signature), {x = y} + {x <> y}. -Proof. - repeat decide equality. -Defined. - -Lemma list_operation_eq : forall (x y : list Op.operation), {x = y} + {x <> y}. -Proof. - generalize operation_eq; intro. - decide equality. -Defined. - -Lemma list_reg_eq : forall (x y : list reg), {x = y} + {x <> y}. -Proof. - generalize Pos.eq_dec; intros. - decide equality. -Defined. - -Lemma sig_eq : forall (x y : AST.signature), {x = y} + {x <> y}. -Proof. - repeat decide equality. -Defined. - -Lemma instr_eq: forall (x y : instr), {x = y} + {x <> y}. -Proof. - generalize Pos.eq_dec; intro. - generalize typ_eq; intro. - generalize Int.eq_dec; intro. - generalize memory_chunk_eq; intro. - generalize addressing_eq; intro. - generalize operation_eq; intro. - generalize condition_eq; intro. - generalize signature_eq; intro. - generalize list_operation_eq; intro. - generalize list_reg_eq; intro. - generalize AST.ident_eq; intro. - repeat decide equality. -Defined. - -Lemma cf_instr_eq: forall (x y : cf_instr), {x = y} + {x <> y}. -Proof. - generalize Pos.eq_dec; intro. - generalize typ_eq; intro. - generalize Int.eq_dec; intro. - generalize Int64.eq_dec; intro. - generalize Float.eq_dec; intro. - generalize Float32.eq_dec; intro. - generalize Ptrofs.eq_dec; intro. - generalize memory_chunk_eq; intro. - generalize addressing_eq; intro. - generalize operation_eq; intro. - generalize condition_eq; intro. - generalize signature_eq; intro. - generalize list_operation_eq; intro. - generalize list_reg_eq; intro. - generalize AST.ident_eq; intro. - repeat decide equality. -Defined. - -(*| -We then create equality lemmas for a resource and a module to index resources uniquely. The -indexing is done by setting Mem to 1, whereas all other infinitely many registers will all be -shifted right by 1. This means that they will never overlap. -|*) - -Module R_indexed. - Definition t := resource. - Definition index (rs: resource) : positive := - match rs with - | Reg r => xO (xO r) - | Pred r => xI (xI r) - | Mem => 1%positive - end. - - Lemma index_inj: forall (x y: t), index x = index y -> x = y. - Proof. destruct x; destruct y; crush. Qed. - - Definition eq := resource_eq. -End R_indexed. - -(*| -We can then create expressions that mimic the expressions defined in RTLBlock and RTLPar, which use -expressions instead of registers as their inputs and outputs. This means that we can accumulate all -the results of the operations as general expressions that will be present in those registers. - -- Ebase: the starting value of the register. -- Eop: Some arithmetic operation on a number of registers. -- Eload: A load from a memory location into a register. -- Estore: A store from a register to a memory location. - -Then, to make recursion over expressions easier, expression_list is also defined in the datatype, as -that enables mutual recursive definitions over the datatypes. -|*) - -Definition unsat p := forall a, sat_predicate p a = false. -Definition sat p := exists a, sat_predicate p a = true. - -Inductive expression : Type := -| Ebase : resource -> expression -| Eop : Op.operation -> expression_list -> expression -> expression -| Eload : AST.memory_chunk -> Op.addressing -> expression_list -> expression -> expression -| Estore : expression -> AST.memory_chunk -> Op.addressing -> expression_list -> expression -> expression -| Esetpred : Op.condition -> expression_list -> expression -> expression -with expression_list : Type := -| Enil : expression_list -| Econs : expression -> expression_list -> expression_list -. - -(*Inductive pred_expr : Type := -| PEsingleton : option pred_op -> expression -> pred_expr -| PEcons : option pred_op -> expression -> pred_expr -> pred_expr.*) - -Module NonEmpty. - -Inductive non_empty (A: Type) := -| singleton : A -> non_empty A -| cons : A -> non_empty A -> non_empty A -. - -Arguments singleton [A]. -Arguments cons [A]. - -Declare Scope non_empty_scope. -Delimit Scope non_empty_scope with non_empty. - -Module NonEmptyNotation. -Infix "::|" := cons (at level 60, right associativity) : non_empty_scope. -End NonEmptyNotation. -Import NonEmptyNotation. - -#[local] Open Scope non_empty_scope. - -Fixpoint map {A B} (f: A -> B) (l: non_empty A): non_empty B := - match l with - | singleton a => singleton (f a) - | a ::| b => f a ::| map f b - end. - -Fixpoint to_list {A} (l: non_empty A): list A := - match l with - | singleton a => a::nil - | a ::| b => a :: to_list b - end. - -Fixpoint app {A} (l1 l2: non_empty A) := - match l1 with - | singleton a => a ::| l2 - | a ::| b => a ::| app b l2 - end. - -Fixpoint non_empty_prod {A B} (l: non_empty A) (l': non_empty B) := - match l with - | singleton a => map (fun x => (a, x)) l' - | a ::| b => app (map (fun x => (a, x)) l') (non_empty_prod b l') - end. - -Fixpoint of_list {A} (l: list A): option (non_empty A) := - match l with - | a::b => - match of_list b with - | Some b' => Some (a ::| b') - | _ => None - end - | nil => None - end. - -End NonEmpty. - -Module NE := NonEmpty. -Import NE.NonEmptyNotation. - -#[local] Open Scope non_empty_scope. - -Definition predicated A := NE.non_empty (option pred_op * A). - -Definition pred_expr := predicated expression. - -Definition pred_list_wf l : Prop := - forall a b, In (Some a) l -> In (Some b) l -> a <> b -> unsat (Pand a b). - -Definition pred_list_wf_ep (l: pred_expr) : Prop := - pred_list_wf (NE.to_list (NE.map fst l)). - -Lemma unsat_correct1 : - forall a b c, - unsat (Pand a b) -> - sat_predicate a c = true -> - sat_predicate b c = false. -Proof. - unfold unsat in *. intros. - simplify. specialize (H c). - apply andb_false_iff in H. inv H. rewrite H0 in H1. discriminate. - auto. -Qed. - -Lemma unsat_correct2 : - forall a b c, - unsat (Pand a b) -> - sat_predicate b c = true -> - sat_predicate a c = false. -Proof. - unfold unsat in *. intros. - simplify. specialize (H c). - apply andb_false_iff in H. inv H. auto. rewrite H0 in H1. discriminate. -Qed. - -Lemma unsat_not a: unsat (Pand a (Pnot a)). -Proof. unfold unsat; simplify; auto with bool. Qed. - -Lemma unsat_commut a b: unsat (Pand a b) -> unsat (Pand b a). -Proof. unfold unsat; simplify; eauto with bool. Qed. - -Lemma sat_dec a n b: sat_pred n a = Some b -> {sat a} + {unsat a}. -Proof. - unfold sat, unsat. destruct b. - intros. left. destruct s. - exists (Sat.interp_alist x). auto. - intros. tauto. -Qed. - -Lemma sat_equiv : - forall a b, - unsat (Por (Pand a (Pnot b)) (Pand (Pnot a) b)) -> - forall c, sat_predicate a c = sat_predicate b c. -Proof. - unfold unsat. intros. specialize (H c); simplify. - destruct (sat_predicate b c) eqn:X; - destruct (sat_predicate a c) eqn:X2; - crush. -Qed. +#[local] Open Scope positive. (*Parameter op_le : Op.operation -> Op.operation -> bool. Parameter chunk_le : AST.memory_chunk -> AST.memory_chunk -> bool. @@ -435,396 +121,6 @@ with eplist_le (e1 e2: expr_pred_list) : bool := end .*) -(*| -Using IMap we can create a map from resources to any other type, as resources can be uniquely -identified as positive numbers. -|*) - -Module Rtree := ITree(R_indexed). - -Definition forest : Type := Rtree.t pred_expr. - -Definition get_forest v (f: forest) := - match Rtree.get v f with - | None => NE.singleton (None, (Ebase v)) - | Some v' => v' - end. - -Notation "a # b" := (get_forest b a) (at level 1). -Notation "a # b <- c" := (Rtree.set b c a) (at level 1, b at next level). - -Definition maybe {A: Type} (vo: A) (pr: predset) p (v: A) := - match p with - | Some p' => if eval_predf pr p' then v else vo - | None => v - end. - -Definition get_pr i := match i with mk_instr_state a b c => b end. - -Definition get_m i := match i with mk_instr_state a b c => c end. - -Definition eval_predf_opt pr p := - match p with Some p' => eval_predf pr p' | None => true end. - -(*| -Finally we want to define the semantics of execution for the expressions with symbolic values, so -the result of executing the expressions will be an expressions. -|*) - -Section SEMANTICS. - -Context {A : Type} (genv : Genv.t A unit). - -Inductive sem_value : - val -> instr_state -> expression -> val -> Prop := -| Sbase_reg: - forall sp rs r m pr, - sem_value sp (mk_instr_state rs pr m) (Ebase (Reg r)) (rs !! r) -| Sop: - forall rs m op args v lv sp m' mem_exp pr, - sem_mem sp (mk_instr_state rs pr m) mem_exp m' -> - sem_val_list sp (mk_instr_state rs pr m) args lv -> - Op.eval_operation genv sp op lv m' = Some v -> - sem_value sp (mk_instr_state rs pr m) (Eop op args mem_exp) v -| Sload : - forall st mem_exp addr chunk args a v m' lv sp, - sem_mem sp st mem_exp m' -> - sem_val_list sp st args lv -> - Op.eval_addressing genv sp addr lv = Some a -> - Memory.Mem.loadv chunk m' a = Some v -> - sem_value sp st (Eload chunk addr args mem_exp) v -with sem_pred : - val -> instr_state -> expression -> bool -> Prop := -| Spred: - forall st mem_exp args c lv m' v sp, - sem_mem sp st mem_exp m' -> - sem_val_list sp st args lv -> - Op.eval_condition c lv m' = Some v -> - sem_pred sp st (Esetpred c args mem_exp) v -| Sbase_pred: - forall rs pr m p sp, - sem_pred sp (mk_instr_state rs pr m) (Ebase (Pred p)) (pr !! p) -with sem_mem : - val -> instr_state -> expression -> Memory.mem -> Prop := -| Sstore : - forall st mem_exp val_exp m'' addr v a m' chunk args lv sp, - sem_mem sp st mem_exp m' -> - sem_value sp st val_exp v -> - sem_val_list sp st args lv -> - Op.eval_addressing genv sp addr lv = Some a -> - Memory.Mem.storev chunk m' a v = Some m'' -> - sem_mem sp st (Estore val_exp chunk addr args mem_exp) m'' -| Sbase_mem : - forall rs m sp pr, - sem_mem sp (mk_instr_state rs pr m) (Ebase Mem) m -with sem_val_list : - val -> instr_state -> expression_list -> list val -> Prop := -| Snil : - forall st sp, - sem_val_list sp st Enil nil -| Scons : - forall st e v l lv sp, - sem_value sp st e v -> - sem_val_list sp st l lv -> - sem_val_list sp st (Econs e l) (v :: lv) -. - -Inductive sem_pred_expr {A: Type} (sem: val -> instr_state -> expression -> A -> Prop): - val -> instr_state -> pred_expr -> A -> Prop := -| sem_pred_expr_base : - forall sp st e v, - sem sp st e v -> - sem_pred_expr sem sp st (NE.singleton (None, e)) v -| sem_pred_expr_p : - forall sp st e p v, - eval_predf (instr_st_predset st) p = true -> - sem sp st e v -> - sem_pred_expr sem sp st (NE.singleton (Some p, e)) v -| sem_pred_expr_cons_true : - forall sp st e pr p' v, - eval_predf (instr_st_predset st) pr = true -> - sem sp st e v -> - sem_pred_expr sem sp st ((Some pr, e)::|p') v -| sem_pred_expr_cons_false : - forall sp st e pr p' v, - eval_predf (instr_st_predset st) pr = false -> - sem_pred_expr sem sp st p' v -> - sem_pred_expr sem sp st ((Some pr, e)::|p') v -| sem_pred_expr_cons_None : - forall sp st e p' v, - sem sp st e v -> - sem_pred_expr sem sp st ((None, e)::|p') v -. - -Definition collapse_pe (p: pred_expr) : option expression := - match p with - | NE.singleton (None, p) => Some p - | _ => None - end. - -Inductive sem_predset : - val -> instr_state -> forest -> predset -> Prop := -| Spredset: - forall st f sp rs', - (forall pe x, - collapse_pe (f # (Pred x)) = Some pe -> - sem_pred sp st pe (rs' !! x)) -> - sem_predset sp st f rs'. - -Inductive sem_regset : - val -> instr_state -> forest -> regset -> Prop := -| Sregset: - forall st f sp rs', - (forall x, sem_pred_expr sem_value sp st (f # (Reg x)) (rs' !! x)) -> - sem_regset sp st f rs'. - -Inductive sem : - val -> instr_state -> forest -> instr_state -> Prop := -| Sem: - forall st rs' m' f sp pr', - sem_regset sp st f rs' -> - sem_predset sp st f pr' -> - sem_pred_expr sem_mem sp st (f # Mem) m' -> - sem sp st f (mk_instr_state rs' pr' m'). - -End SEMANTICS. - -Fixpoint beq_expression (e1 e2: expression) {struct e1}: bool := - match e1, e2 with - | Ebase r1, Ebase r2 => if resource_eq r1 r2 then true else false - | Eop op1 el1 exp1, Eop op2 el2 exp2 => - if operation_eq op1 op2 then - beq_expression_list el1 el2 else false - | Eload chk1 addr1 el1 e1, Eload chk2 addr2 el2 e2 => - if memory_chunk_eq chk1 chk2 - then if addressing_eq addr1 addr2 - then if beq_expression_list el1 el2 - then beq_expression e1 e2 else false else false else false - | Estore e1 chk1 addr1 el1 m1, Estore e2 chk2 addr2 el2 m2 => - if memory_chunk_eq chk1 chk2 - then if addressing_eq addr1 addr2 - then if beq_expression_list el1 el2 - then if beq_expression m1 m2 - then beq_expression e1 e2 else false else false else false else false - | Esetpred c1 el1 m1, Esetpred c2 el2 m2 => - if condition_eq c1 c2 - then beq_expression_list el1 el2 else false - | _, _ => false - end -with beq_expression_list (el1 el2: expression_list) {struct el1} : bool := - match el1, el2 with - | Enil, Enil => true - | Econs e1 t1, Econs e2 t2 => beq_expression e1 e2 && beq_expression_list t1 t2 - | _, _ => false - end -. - -Scheme expression_ind2 := Induction for expression Sort Prop - with expression_list_ind2 := Induction for expression_list Sort Prop -. - -Lemma beq_expression_correct: - forall e1 e2, beq_expression e1 e2 = true -> e1 = e2. -Proof. - intro e1; - apply expression_ind2 with - (P := fun (e1 : expression) => - forall e2, beq_expression e1 e2 = true -> e1 = e2) - (P0 := fun (e1 : expression_list) => - forall e2, beq_expression_list e1 e2 = true -> e1 = e2); - try solve [repeat match goal with - | [ H : context[match ?x with _ => _ end] |- _ ] => destruct x eqn:? - | [ H : context[if ?x then _ else _] |- _ ] => destruct x eqn:? - end; subst; f_equal; crush; eauto using Peqb_true_eq]. - destruct e2; try discriminate. eauto. -Abort. - -Definition hash_tree := PTree.t expression. - -Definition find_tree (el: expression) (h: hash_tree) : option positive := - match filter (fun x => beq_expression el (snd x)) (PTree.elements h) with - | (p, _) :: nil => Some p - | _ => None - end. - -Definition combine_option {A} (a b: option A) : option A := - match a, b with - | Some a', _ => Some a' - | _, Some b' => Some b' - | _, _ => None - end. - -Definition max_key {A} (t: PTree.t A) := - fold_right Pos.max 1%positive (map fst (PTree.elements t)). - -Definition hash_expr (max: predicate) (e: expression) (h: hash_tree): predicate * hash_tree := - match find_tree e h with - | Some p => (p, h) - | None => - let nkey := Pos.max max (max_key h) + 1 in - (nkey, PTree.set nkey e h) - end. - -Fixpoint encode_expression (max: predicate) (pe: pred_expr) (h: hash_tree): pred_op * hash_tree := - match pe with - | NE.singleton (None, e) => - let (p, h') := hash_expr max e h in - (Pvar p, h') - | NE.singleton (Some p, e) => - let (p', h') := hash_expr max e h in - (Por (Pnot p) (Pvar p'), h') - | (Some p, e)::|pe' => - let (p', h') := hash_expr max e h in - let (p'', h'') := encode_expression max pe' h' in - (Pand (Por (Pnot p) (Pvar p')) p'', h'') - | (None, e)::|pe' => - let (p', h') := hash_expr max e h in - let (p'', h'') := encode_expression max pe' h' in - (Pand (Pvar p') p'', h'') - end. - -Fixpoint max_predicate (p: pred_op) : positive := - match p with - | Pvar p => p - | Pand a b => Pos.max (max_predicate a) (max_predicate b) - | Por a b => Pos.max (max_predicate a) (max_predicate b) - | Pnot a => max_predicate a - end. - -Fixpoint max_pred_expr (pe: pred_expr) : positive := - match pe with - | NE.singleton (None, _) => 1 - | NE.singleton (Some p, _) => max_predicate p - | (Some p, _) ::| pe' => Pos.max (max_predicate p) (max_pred_expr pe') - | (None, _) ::| pe' => (max_pred_expr pe') - end. - -Definition beq_pred_expr (bound: nat) (pe1 pe2: pred_expr) : bool := - match pe1, pe2 with - (*| PEsingleton None e1, PEsingleton None e2 => beq_expression e1 e2 - | PEsingleton (Some p1) e1, PEsingleton (Some p2) e2 => - if beq_expression e1 e2 - then match sat_pred_simple bound (Por (Pand p1 (Pnot p2)) (Pand p2 (Pnot p1))) with - | Some None => true - | _ => false - end - else false - | PEsingleton (Some p) e1, PEsingleton None e2 - | PEsingleton None e1, PEsingleton (Some p) e2 => - if beq_expression e1 e2 - then match sat_pred_simple bound (Pnot p) with - | Some None => true - | _ => false - end - else false*) - | pe1, pe2 => - let max := Pos.max (max_pred_expr pe1) (max_pred_expr pe2) in - let (p1, h) := encode_expression max pe1 (PTree.empty _) in - let (p2, h') := encode_expression max pe2 h in - match sat_pred_simple bound (Por (Pand p1 (Pnot p2)) (Pand p2 (Pnot p1))) with - | Some None => true - | _ => false - end - end. - -Definition empty : forest := Rtree.empty _. - -Definition check := Rtree.beq (beq_pred_expr 10000). - -Compute (check (empty # (Reg 2) <- - (((Some (Pand (Pvar 4) (Pnot (Pvar 4)))), (Ebase (Reg 9))) ::| - (NE.singleton ((Some (Pvar 2)), (Ebase (Reg 3)))))) - (empty # (Reg 2) <- (NE.singleton ((Some (Por (Pvar 2) (Pand (Pvar 3) (Pnot (Pvar 3))))), - (Ebase (Reg 3)))))). - -Lemma check_correct: forall (fa fb : forest), - check fa fb = true -> (forall x, fa # x = fb # x). -Proof. - (*unfold check, get_forest; intros; - pose proof beq_expression_correct; - match goal with - [ Hbeq : context[Rtree.beq], y : Rtree.elt |- _ ] => - apply (Rtree.beq_sound beq_expression fa fb) with (x := y) in Hbeq - end; - repeat destruct_match; crush. -Qed.*) - Abort. - -Lemma get_empty: - forall r, empty#r = NE.singleton (None, Ebase r). -Proof. - intros; unfold get_forest; - destruct_match; auto; [ ]; - match goal with - [ H : context[Rtree.get _ empty] |- _ ] => rewrite Rtree.gempty in H - end; discriminate. -Qed. - -Fixpoint beq2 {A B : Type} (beqA : A -> B -> bool) (m1 : PTree.t A) (m2 : PTree.t B) {struct m1} : bool := - match m1, m2 with - | PTree.Leaf, _ => PTree.bempty m2 - | _, PTree.Leaf => PTree.bempty m1 - | PTree.Node l1 o1 r1, PTree.Node l2 o2 r2 => - match o1, o2 with - | None, None => true - | Some y1, Some y2 => beqA y1 y2 - | _, _ => false - end - && beq2 beqA l1 l2 && beq2 beqA r1 r2 - end. - -Lemma beq2_correct: - forall A B beqA m1 m2, - @beq2 A B beqA m1 m2 = true <-> - (forall (x: PTree.elt), - match PTree.get x m1, PTree.get x m2 with - | None, None => True - | Some y1, Some y2 => beqA y1 y2 = true - | _, _ => False - end). -Proof. - induction m1; intros. - - simpl. rewrite PTree.bempty_correct. split; intros. - rewrite PTree.gleaf. rewrite H. auto. - generalize (H x). rewrite PTree.gleaf. destruct (PTree.get x m2); tauto. - - destruct m2. - + unfold beq2. rewrite PTree.bempty_correct. split; intros. - rewrite H. rewrite PTree.gleaf. auto. - generalize (H x). rewrite PTree.gleaf. - destruct (PTree.get x (PTree.Node m1_1 o m1_2)); tauto. - + simpl. split; intros. - * destruct (andb_prop _ _ H). destruct (andb_prop _ _ H0). - rewrite IHm1_1 in H3. rewrite IHm1_2 in H1. - destruct x; simpl. apply H1. apply H3. - destruct o; destruct o0; auto || congruence. - * apply andb_true_intro. split. apply andb_true_intro. split. - generalize (H xH); simpl. destruct o; destruct o0; tauto. - apply IHm1_1. intros; apply (H (xO x)). - apply IHm1_2. intros; apply (H (xI x)). -Qed. - -Lemma map1: - forall w dst dst', - dst <> dst' -> - (empty # dst <- w) # dst' = NE.singleton (None, Ebase dst'). -Proof. intros; unfold get_forest; rewrite Rtree.gso; auto; apply get_empty. Qed. - -Lemma genmap1: - forall (f : forest) w dst dst', - dst <> dst' -> - (f # dst <- w) # dst' = f # dst'. -Proof. intros; unfold get_forest; rewrite Rtree.gso; auto. Qed. - -Lemma map2: - forall (v : pred_expr) x rs, - (rs # x <- v) # x = v. -Proof. intros; unfold get_forest; rewrite Rtree.gss; trivial. Qed. - -Lemma tri1: - forall x y, - Reg x <> Reg y -> x <> y. -Proof. crush. Qed. - Definition ge_preserved {A B C D: Type} (ge: Genv.t A B) (tge: Genv.t C D) : Prop := (forall sp op vl m, Op.eval_operation ge sp op vl m = Op.eval_operation tge sp op vl m) -- cgit From d25444b11036504df09b60090a6fc86f99bd9ca7 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Fri, 8 Oct 2021 23:02:02 +0100 Subject: Add abstract intermediate language to RTLPargen --- src/hls/RTLPargen.v | 66 +++++++++++++++++++++++++++++++++++++++-------------- 1 file changed, 49 insertions(+), 17 deletions(-) (limited to 'src/hls/RTLPargen.v') diff --git a/src/hls/RTLPargen.v b/src/hls/RTLPargen.v index fee24f3..3cc9a57 100644 --- a/src/hls/RTLPargen.v +++ b/src/hls/RTLPargen.v @@ -30,6 +30,7 @@ Require Import vericert.common.Vericertlib. Require Import vericert.hls.RTLBlock. Require Import vericert.hls.RTLPar. Require Import vericert.hls.RTLBlockInstr. +Require Import vericert.hls.Abstr. #[local] Open Scope positive. @@ -130,7 +131,7 @@ Definition ge_preserved {A B C D: Type} (ge: Genv.t A B) (tge: Genv.t C D) : Pro Lemma ge_preserved_same: forall A B ge, @ge_preserved A B A B ge ge. Proof. unfold ge_preserved; auto. Qed. -Hint Resolve ge_preserved_same : rtlpar. +#[local] Hint Resolve ge_preserved_same : rtlpar. Ltac rtlpar_crush := crush; eauto with rtlpar. @@ -151,11 +152,11 @@ Inductive match_states_ld : instr_state -> instr_state -> Prop := match_states_ld (mk_instr_state rs ps m) (mk_instr_state rs' ps' m'). Lemma sems_det: - forall A ge tge sp st f, + forall A ge tge sp f rs ps m, ge_preserved ge tge -> forall v v' mv mv', - (@sem_value A ge sp st f v /\ @sem_value A tge sp st f v' -> v = v') /\ - (@sem_mem A ge sp st f mv /\ @sem_mem A tge sp st f mv' -> mv = mv'). + (@sem_value A (mk_ctx rs ps m sp ge) f v /\ @sem_value A (mk_ctx rs ps m sp tge) f v' -> v = v') /\ + (@sem_mem A (mk_ctx rs ps m sp ge) f mv /\ @sem_mem A (mk_ctx rs ps m sp tge) f mv' -> mv = mv'). Proof. Abort. (*Lemma sem_value_det: @@ -268,13 +269,29 @@ Definition merge'' x := | ((a, e), (b, el)) => (merge''' a b, Econs e el) end. +Definition predicated_prod {A B: Type} (p1: predicated A) (p2: predicated B) := + match p1, p2 with + | Psingle a, Psingle b => Psingle (a, b) + | Psingle a, Plist b => Plist (NE.map (fun x => (fst x, (a, snd x))) b) + | Plist b, Psingle a => Plist (NE.map (fun x => (fst x, (snd x, a))) b) + | Plist a, Plist b => + Plist (NE.map (fun x => match x with ((a, b), (c, d)) => (Pand a c, (b, d)) end) + (NE.non_empty_prod a b)) + end. + +Definition predicated_map {A B: Type} (f: A -> B) (p: predicated A): predicated B := + match p with + | Psingle a => Psingle (f a) + | Plist b => Plist (NE.map (fun x => (fst x, f (snd x))) b) + end. + (*map (fun x => (fst x, Econs (snd x) Enil)) pel*) -Fixpoint merge' (pel: pred_expr) (tpel: predicated expression_list) := - NE.map merge'' (NE.non_empty_prod pel tpel). +Definition merge' (pel: pred_expr) (tpel: predicated expression_list) := + predicated_map (uncurry Econs) (predicated_prod pel tpel). Fixpoint merge (pel: list pred_expr): predicated expression_list := match pel with - | nil => NE.singleton (None, Enil) + | nil => Psingle Enil | a :: b => merge' a (merge b) end. @@ -284,35 +301,50 @@ Definition map_pred_op {A B} (pf: option pred_op * (A -> B)) (pa: option pred_op end. Definition map_predicated {A B} (pf: predicated (A -> B)) (pa: predicated A): predicated B := - NE.map (fun x => match x with ((p1, f), (p2, a)) => (merge''' p1 p2, f a) end) (NE.non_empty_prod pf pa). + predicated_map (fun x => (fst x) (snd x)) (predicated_prod pf pa). -Definition apply1_predicated {A B} (pf: predicated (A -> B)) (pa: A): predicated B := - NE.map (fun x => (fst x, (snd x) pa)) pf. +Definition predicated_apply1 {A B} (pf: predicated (A -> B)) (pa: A): predicated B := + match pf with + | Psingle f => Psingle (f pa) + | Plist pf' => Plist (NE.map (fun x => (fst x, (snd x) pa)) pf') + end. -Definition apply2_predicated {A B C} (pf: predicated (A -> B -> C)) (pa: A) (pb: B): predicated C := - NE.map (fun x => (fst x, (snd x) pa pb)) pf. +Definition predicated_apply2 {A B C} (pf: predicated (A -> B -> C)) (pa: A) (pb: B): predicated C := + match pf with + | Psingle f => Psingle (f pa pb) + | Plist pf' => Plist (NE.map (fun x => (fst x, (snd x) pa pb)) pf') + end. -Definition apply3_predicated {A B C D} (pf: predicated (A -> B -> C -> D)) (pa: A) (pb: B) (pc: C): predicated D := - NE.map (fun x => (fst x, (snd x) pa pb pc)) pf. +Definition predicated_apply3 {A B C D} (pf: predicated (A -> B -> C -> D)) (pa: A) (pb: B) (pc: C): predicated D := + match pf with + | Psingle f => Psingle (f pa pb pc) + | Plist pf' => Plist (NE.map (fun x => (fst x, (snd x) pa pb pc)) pf') + end. (*Compute merge (((Some (Pvar 2), Ebase (Reg 4))::nil)::((Some (Pvar 3), Ebase (Reg 3))::(Some (Pvar 1), Ebase (Reg 3))::nil)::nil).*) +Definition predicated_from_opt {A: Type} (p: option pred_op) (a: A) := + match p with + | None => Psingle a + | Some x => Plist (NE.singleton (x, a)) + end. + Definition update (f : forest) (i : instr) : forest := match i with | RBnop => f | RBop p op rl r => f # (Reg r) <- - (map_predicated (map_predicated (NE.singleton (p, Eop op)) (merge (list_translation rl f))) (f # Mem)) + (map_predicated (predicated_from_opt p (Eop op)) (merge (list_translation rl f))) | RBload p chunk addr rl r => f # (Reg r) <- (map_predicated - (map_predicated (NE.singleton (p, Eload chunk addr)) (merge (list_translation rl f))) + (map_predicated (predicated_from_opt p (Eload chunk addr)) (merge (list_translation rl f))) (f # Mem)) | RBstore p chunk addr rl r => f # Mem <- (map_predicated (map_predicated - (apply2_predicated (map_predicated (NE.singleton (p, Estore)) (f # (Reg r))) chunk addr) + (predicated_apply2 (map_predicated (predicated_from_opt p Estore) (f # (Reg r))) chunk addr) (merge (list_translation rl f))) (f # Mem)) | RBsetpred c addr p => f end. -- cgit From fe06668f0de56635efe55310d7a64289a37c1d90 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Thu, 14 Oct 2021 12:20:03 +0100 Subject: [sched] Fix passes with new predicates --- src/hls/RTLPargen.v | 1 + 1 file changed, 1 insertion(+) (limited to 'src/hls/RTLPargen.v') diff --git a/src/hls/RTLPargen.v b/src/hls/RTLPargen.v index 3cc9a57..13d9480 100644 --- a/src/hls/RTLPargen.v +++ b/src/hls/RTLPargen.v @@ -33,6 +33,7 @@ Require Import vericert.hls.RTLBlockInstr. Require Import vericert.hls.Abstr. #[local] Open Scope positive. +#[local] Open Scope forest. (*Parameter op_le : Op.operation -> Op.operation -> bool. Parameter chunk_le : AST.memory_chunk -> AST.memory_chunk -> bool. -- cgit