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(-) 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(-) 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(-) 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(-) 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 +++++++++++++++++++++++++++++++++++++++++++---- src/hls/RTLPargenproof.v | 82 ++++++++++++++++++++++++++--------- 2 files changed, 164 insertions(+), 27 deletions(-) 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. diff --git a/src/hls/RTLPargenproof.v b/src/hls/RTLPargenproof.v index eb7931e..e8167e9 100644 --- a/src/hls/RTLPargenproof.v +++ b/src/hls/RTLPargenproof.v @@ -38,7 +38,7 @@ Inductive match_stackframes: RTLBlock.stackframe -> RTLPar.stackframe -> Prop := | match_stackframe: forall f tf res sp pc rs rs', transl_function f = OK tf -> - regs_lessdef rs rs' -> + (forall x, rs !! x = rs' !! x) -> match_stackframes (Stackframe res f sp pc rs) (Stackframe res tf sp pc rs'). @@ -47,25 +47,23 @@ Inductive match_states: RTLBlock.state -> RTLPar.state -> Prop := forall sf f sp pc rs rs' m m' sf' tf (TRANSL: transl_function f = OK tf) (STACKS: list_forall2 match_stackframes sf sf') - (REG: regs_lessdef rs rs') + (REG: forall x, rs !! x = rs' !! x) (MEM: Mem.extends m m'), match_states (State sf f sp pc rs m) (State sf' tf sp pc rs' m') | match_returnstate: - forall stack stack' v v' m m' + forall stack stack' v m m' (STACKS: list_forall2 match_stackframes stack stack') - (MEM: Mem.extends m m') - (LD: Val.lessdef v v'), + (MEM: Mem.extends m m'), match_states (Returnstate stack v m) - (Returnstate stack' v' m') + (Returnstate stack' v m') | match_callstate: - forall stack stack' f tf args args' m m' + forall stack stack' f tf args m m' (TRANSL: transl_fundef f = OK tf) (STACKS: list_forall2 match_stackframes stack stack') - (LD: Val.lessdef_list args args') (MEM: Mem.extends m m'), match_states (Callstate stack f args m) - (Callstate stack' tf args' m'). + (Callstate stack' tf args m'). Section CORRECTNESS. @@ -121,7 +119,7 @@ Section CORRECTNESS. Lemma find_function_translated: forall ros rs rs' f, - regs_lessdef rs rs' -> + (forall x, rs !! x = rs' !! x) -> find_function ge ros rs = Some f -> exists tf, find_function tge ros rs' = Some tf /\ transl_fundef f = OK tf. @@ -134,7 +132,7 @@ Section CORRECTNESS. | [ H: Genv.find_funct _ Vundef = Some _ |- _] => solve [inv H] | _ => solve [exploit functions_translated; eauto] end. - unfold regs_lessdef; destruct ros; simplify; try rewrite <- H; + destruct ros; simplify; try rewrite <- H; [| rewrite symbols_preserved; destruct_match; try (apply function_ptr_translated); crush ]; intros; @@ -160,8 +158,8 @@ Section CORRECTNESS. Qed. Lemma eval_op_eq: - forall (sp0 : Values.val) (op : Op.operation) (vl : list Values.val), - Op.eval_operation ge sp0 op vl = Op.eval_operation tge sp0 op vl. + forall (sp0 : Values.val) (op : Op.operation) (vl : list Values.val) m, + Op.eval_operation ge sp0 op vl m = Op.eval_operation tge sp0 op vl m. Proof using TRANSL. intros. destruct op; auto; unfold Op.eval_operation, Genv.symbol_address, Op.eval_addressing32; @@ -197,6 +195,16 @@ Section CORRECTNESS. Proof using. destruct or; crush. Qed. Hint Resolve lessdef_regmap_optget : rtlgp. + Lemma regmap_equiv_lessdef: + forall rs rs', + (forall x, rs !! x = rs' !! x) -> + regs_lessdef rs rs'. + Proof using. + intros; unfold regs_lessdef; intros. + rewrite H. apply Val.lessdef_refl. + Qed. + Hint Resolve regmap_equiv_lessdef : rtlgp. + Lemma int_lessdef: forall rs rs', regs_lessdef rs rs' -> @@ -227,8 +235,8 @@ Section CORRECTNESS. let H2 := fresh "SCHED" in learn H as H2; apply schedule_oracle_nil in H2 - | [ H: find_function _ _ _ = Some _ |- _ ] => - learn H; exploit find_function_translated; eauto; inversion 1 + | [ H: find_function _ _ _ = Some _, H2: forall x, ?rs !! x = ?rs' !! x |- _ ] => + learn H; exploit find_function_translated; try apply H2; eauto; inversion 1 | [ H: Mem.free ?m _ _ _ = Some ?m', H2: Mem.extends ?m ?m'' |- _ ] => learn H; exploit Mem.free_parallel_extends; eauto; intros | [ H: Events.eval_builtin_args _ _ _ _ _ _, H2: regs_lessdef ?rs ?rs' |- _ ] => @@ -249,6 +257,29 @@ Section CORRECTNESS. Hint Resolve set_reg_lessdef : rtlgp. Hint Resolve Op.eval_condition_lessdef : rtlgp. + Hint Constructors Events.eval_builtin_arg: barg. + + Lemma eval_builtin_arg_eq: + forall A ge a v1 m1 e1 e2 sp, + (forall x, e1 x = e2 x) -> + @Events.eval_builtin_arg A ge e1 sp m1 a v1 -> + Events.eval_builtin_arg ge e2 sp m1 a v1. +Proof. induction 2; try rewrite H; eauto with barg. Qed. + + Lemma eval_builtin_args_lessdef: + forall A ge e1 sp m1 e2 al vl1, + (forall x, e1 x = e2 x) -> + @Events.eval_builtin_args A ge e1 sp m1 al vl1 -> + Events.eval_builtin_args ge e2 sp m1 al vl1. + Proof. + induction 2. + - econstructor; split. + - exploit eval_builtin_arg_eq; eauto. intros. + destruct IHlist_forall2 as [| y]. constructor; eauto. + constructor. constructor; auto. + constructor; eauto. + Qed. + Lemma step_cf_instr_correct: forall cfi t s s', step_cf_instr ge s cfi t s' -> @@ -256,8 +287,20 @@ Section CORRECTNESS. match_states s r -> exists r', step_cf_instr tge r cfi t r' /\ match_states s' r'. Proof using TRANSL. - induction 1; repeat semantics_simpl; + induction 1; repeat semantics_simpl. + { repeat (try erewrite match_states_list by eauto; econstructor; eauto with rtlgp). } + { repeat (try erewrite match_states_list by eauto; econstructor; eauto with rtlgp). } + { (try erewrite match_states_list by eauto; econstructor; eauto with rtlgp). + (try erewrite match_states_list by eauto; econstructor; eauto with rtlgp). + (try erewrite match_states_list by eauto; econstructor; eauto with rtlgp). + exploit Events.eval_builtin_args_lessdef. + } repeat (econstructor; eauto with rtlgp). + erewrite match_states_list; eauto. + repeat (econstructor; eauto with rtlgp). + } + repeat (econstructor; eauto with rtlgp). + exploit find_function_translated. eauto. Qed. Theorem transl_step_correct : @@ -269,11 +312,12 @@ Section CORRECTNESS. Proof. induction 1; repeat semantics_simpl. - Abort. -(* { destruct bb as [bbc bbe]; destruct x as [bbc' bbe']. + { destruct bb as [bbc bbe]; destruct x as [bbc' bbe']. assert (bbe = bbe') by admit. rewrite H3 in H5. + exploit abstract_execution_correct. eauto. apply ge_preserved_lem. + eauto. eapply abstract_execution_correct in H5; eauto with rtlgp. repeat econstructor; eauto with rtlgp. simplify. exploit step_cf_instr_correct. eauto. @@ -283,6 +327,6 @@ Section CORRECTNESS. repeat econstructor; eauto. } { inv TRANSL0. repeat econstructor; eauto using Events.external_call_symbols_preserved, symbols_preserved, senv_preserved, Events.E0_right. } { inv STACKS. inv H2. repeat econstructor; eauto. } - Qed.*) + Qed. End CORRECTNESS. -- 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 ++++++++++++++++++ src/hls/RTLPargenproof.v | 44 +++++++++++++++++++++++++------------------- 2 files changed, 43 insertions(+), 19 deletions(-) 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 =================== diff --git a/src/hls/RTLPargenproof.v b/src/hls/RTLPargenproof.v index e8167e9..8ecaba2 100644 --- a/src/hls/RTLPargenproof.v +++ b/src/hls/RTLPargenproof.v @@ -44,26 +44,23 @@ Inductive match_stackframes: RTLBlock.stackframe -> RTLPar.stackframe -> Prop := Inductive match_states: RTLBlock.state -> RTLPar.state -> Prop := | match_state: - forall sf f sp pc rs rs' m m' sf' tf + forall sf f sp pc rs rs' m sf' tf (TRANSL: transl_function f = OK tf) (STACKS: list_forall2 match_stackframes sf sf') - (REG: forall x, rs !! x = rs' !! x) - (MEM: Mem.extends m m'), + (REG: forall x, rs !! x = rs' !! x), match_states (State sf f sp pc rs m) - (State sf' tf sp pc rs' m') + (State sf' tf sp pc rs' m) | match_returnstate: - forall stack stack' v m m' - (STACKS: list_forall2 match_stackframes stack stack') - (MEM: Mem.extends m m'), + forall stack stack' v m + (STACKS: list_forall2 match_stackframes stack stack'), match_states (Returnstate stack v m) - (Returnstate stack' v m') + (Returnstate stack' v m) | match_callstate: - forall stack stack' f tf args m m' + forall stack stack' f tf args m (TRANSL: transl_fundef f = OK tf) - (STACKS: list_forall2 match_stackframes stack stack') - (MEM: Mem.extends m m'), + (STACKS: list_forall2 match_stackframes stack stack'), match_states (Callstate stack f args m) - (Callstate stack' tf args m'). + (Callstate stack' tf args m). Section CORRECTNESS. @@ -266,7 +263,7 @@ Section CORRECTNESS. Events.eval_builtin_arg ge e2 sp m1 a v1. Proof. induction 2; try rewrite H; eauto with barg. Qed. - Lemma eval_builtin_args_lessdef: + Lemma eval_builtin_args_eq: forall A ge e1 sp m1 e2 al vl1, (forall x, e1 x = e2 x) -> @Events.eval_builtin_args A ge e1 sp m1 al vl1 -> @@ -293,14 +290,23 @@ Proof. induction 2; try rewrite H; eauto with barg. Qed. { (try erewrite match_states_list by eauto; econstructor; eauto with rtlgp). (try erewrite match_states_list by eauto; econstructor; eauto with rtlgp). (try erewrite match_states_list by eauto; econstructor; eauto with rtlgp). - exploit Events.eval_builtin_args_lessdef. + eapply eval_builtin_args_eq. eapply REG. + eapply Events.eval_builtin_args_preserved. eapply symbols_preserved. + eauto. + (econstructor; eauto with rtlgp). + intros. + unfold regmap_setres. destruct res. + destruct (Pos.eq_dec x0 x); subst. + repeat rewrite Regmap.gss; auto. + repeat rewrite Regmap.gso; auto. + eapply REG. eapply REG. } - repeat (econstructor; eauto with rtlgp). - erewrite match_states_list; eauto. - repeat (econstructor; eauto with rtlgp). + { repeat (try erewrite match_states_list; eauto; econstructor; eauto with rtlgp). } + { repeat (try erewrite match_states_list; eauto; econstructor; eauto with rtlgp). } + { repeat (try erewrite match_states_list; eauto; econstructor; eauto with rtlgp). + unfold regmap_optget. destruct or. rewrite REG. constructor; eauto. + constructor; eauto. } - repeat (econstructor; eauto with rtlgp). - exploit find_function_translated. eauto. Qed. Theorem transl_step_correct : -- cgit From 51d25ab7feeaca959d35fbd4fa905f8ce003e07b Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Sun, 16 May 2021 11:35:31 +0100 Subject: Minimise the proof a bit --- src/hls/RTLPargenproof.v | 30 ++++++++++++------------------ 1 file changed, 12 insertions(+), 18 deletions(-) diff --git a/src/hls/RTLPargenproof.v b/src/hls/RTLPargenproof.v index 8ecaba2..9cfee3a 100644 --- a/src/hls/RTLPargenproof.v +++ b/src/hls/RTLPargenproof.v @@ -284,25 +284,19 @@ Proof. induction 2; try rewrite H; eauto with barg. Qed. match_states s r -> exists r', step_cf_instr tge r cfi t r' /\ match_states s' r'. Proof using TRANSL. - induction 1; repeat semantics_simpl. - { repeat (try erewrite match_states_list by eauto; econstructor; eauto with rtlgp). } - { repeat (try erewrite match_states_list by eauto; econstructor; eauto with rtlgp). } - { (try erewrite match_states_list by eauto; econstructor; eauto with rtlgp). - (try erewrite match_states_list by eauto; econstructor; eauto with rtlgp). - (try erewrite match_states_list by eauto; econstructor; eauto with rtlgp). - eapply eval_builtin_args_eq. eapply REG. - eapply Events.eval_builtin_args_preserved. eapply symbols_preserved. - eauto. - (econstructor; eauto with rtlgp). - intros. - unfold regmap_setres. destruct res. - destruct (Pos.eq_dec x0 x); subst. - repeat rewrite Regmap.gss; auto. - repeat rewrite Regmap.gso; auto. - eapply REG. eapply REG. + induction 1; repeat semantics_simpl; + try solve [repeat (try erewrite match_states_list; eauto; econstructor; eauto with rtlgp)]. + { do 3 (try erewrite match_states_list by eauto; econstructor; eauto with rtlgp). + eapply eval_builtin_args_eq. eapply REG. + eapply Events.eval_builtin_args_preserved. eapply symbols_preserved. + eauto. + intros. + unfold regmap_setres. destruct res. + destruct (Pos.eq_dec x0 x); subst. + repeat rewrite Regmap.gss; auto. + repeat rewrite Regmap.gso; auto. + eapply REG. eapply REG. } - { repeat (try erewrite match_states_list; eauto; econstructor; eauto with rtlgp). } - { repeat (try erewrite match_states_list; eauto; econstructor; eauto with rtlgp). } { repeat (try erewrite match_states_list; eauto; econstructor; eauto with rtlgp). unfold regmap_optget. destruct or. rewrite REG. constructor; eauto. constructor; eauto. -- 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 +--------- src/hls/RTLPargenproof.v | 35 ++++++++++++++++++++++------------- 2 files changed, 23 insertions(+), 22 deletions(-) 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. diff --git a/src/hls/RTLPargenproof.v b/src/hls/RTLPargenproof.v index 9cfee3a..119ed59 100644 --- a/src/hls/RTLPargenproof.v +++ b/src/hls/RTLPargenproof.v @@ -313,20 +313,29 @@ Proof. induction 2; try rewrite H; eauto with barg. Qed. induction 1; repeat semantics_simpl. - { destruct bb as [bbc bbe]; destruct x as [bbc' bbe']. - assert (bbe = bbe') by admit. - rewrite H3 in H5. - exploit abstract_execution_correct. eauto. apply ge_preserved_lem. - eauto. - eapply abstract_execution_correct in H5; eauto with rtlgp. - repeat econstructor; eauto with rtlgp. simplify. - exploit step_cf_instr_correct. eauto. - econstructor; eauto with rtlgp. + { destruct bb; destruct x. + assert (bb_exit = bb_exit0) by admit; subst. + + exploit abstract_execution_correct; try eassumption. eapply ge_preserved_lem. + econstructor; eauto. + inv_simp. destruct x. inv H7. + + exploit step_cf_instr_correct; try eassumption. econstructor; eauto. + inv_simp. + + econstructor. econstructor. eapply Smallstep.plus_one. econstructor. + eauto. eauto. simplify. eauto. eauto. + } + { unfold bind in *. inv TRANSL0. clear Learn. inv H0. destruct_match; crush. + inv H2. unfold transl_function in Heqr. destruct_match; crush. + inv Heqr. + repeat econstructor; eauto. + unfold bind in *. destruct_match; crush. } - { unfold bind in *. destruct_match; try discriminate. repeat semantics_simpl. inv TRANSL0. - repeat econstructor; eauto. } { inv TRANSL0. repeat econstructor; eauto using Events.external_call_symbols_preserved, symbols_preserved, senv_preserved, Events.E0_right. } - { inv STACKS. inv H2. repeat econstructor; eauto. } - Qed. + { inv STACKS. inv H2. repeat econstructor; eauto. + intros. admit. + } + Admitted. End CORRECTNESS. -- cgit From 8a944ab3c58854f19197745f1b3c1f9ea6c3093f Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Fri, 21 May 2021 19:42:46 +0100 Subject: Fix admitted in last theorem --- src/hls/RTLPargenproof.v | 11 ++++++++--- 1 file changed, 8 insertions(+), 3 deletions(-) diff --git a/src/hls/RTLPargenproof.v b/src/hls/RTLPargenproof.v index 119ed59..e0c20c1 100644 --- a/src/hls/RTLPargenproof.v +++ b/src/hls/RTLPargenproof.v @@ -314,7 +314,12 @@ Proof. induction 2; try rewrite H; eauto with barg. Qed. induction 1; repeat semantics_simpl. { destruct bb; destruct x. - assert (bb_exit = bb_exit0) by admit; subst. + assert (bb_exit = bb_exit0). + { unfold schedule_oracle in *. simplify. + unfold check_control_flow_instr in *. + destruct_match; crush. + } + subst. exploit abstract_execution_correct; try eassumption. eapply ge_preserved_lem. econstructor; eauto. @@ -334,8 +339,8 @@ Proof. induction 2; try rewrite H; eauto with barg. Qed. } { inv TRANSL0. repeat econstructor; eauto using Events.external_call_symbols_preserved, symbols_preserved, senv_preserved, Events.E0_right. } { inv STACKS. inv H2. repeat econstructor; eauto. - intros. admit. + intros. apply PTree_matches; eauto. } - Admitted. + Qed. End CORRECTNESS. -- cgit From 69a61d57f53b56f4efa0c78054aad9fce56f0422 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Sun, 23 May 2021 09:38:17 +0100 Subject: Add very top-level proof --- src/hls/RTLPargenproof.v | 33 +++++++++++++++++++++++++++++++++ 1 file changed, 33 insertions(+) diff --git a/src/hls/RTLPargenproof.v b/src/hls/RTLPargenproof.v index e0c20c1..c610ff0 100644 --- a/src/hls/RTLPargenproof.v +++ b/src/hls/RTLPargenproof.v @@ -343,4 +343,37 @@ Proof. induction 2; try rewrite H; eauto with barg. Qed. } Qed. + Lemma transl_initial_states: + forall S, + RTLBlock.initial_state prog S -> + exists R, RTLPar.initial_state tprog R /\ match_states S R. + Proof. + induction 1. + exploit function_ptr_translated; eauto. intros [tf [A B]]. + econstructor; split. + econstructor. apply (Genv.init_mem_transf_partial TRANSL); eauto. + replace (prog_main tprog) with (prog_main prog). rewrite symbols_preserved; eauto. + symmetry; eapply match_program_main; eauto. + eexact A. + rewrite <- H2. apply sig_transl_function; auto. + constructor. auto. constructor. + Qed. + + Lemma transl_final_states: + forall S R r, + match_states S R -> RTLBlock.final_state S r -> RTLPar.final_state R r. + Proof. + intros. inv H0. inv H. inv STACKS. constructor. + Qed. + + Theorem transf_program_correct: + Smallstep.forward_simulation (RTLBlock.semantics prog) (RTLPar.semantics tprog). + Proof. + eapply Smallstep.forward_simulation_plus. + apply senv_preserved. + eexact transl_initial_states. + eexact transl_final_states. + exact transl_step_correct. + Qed. + End CORRECTNESS. -- cgit From cb82a024b748ccaa7d607741a21b3eb6e0e347ff Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Wed, 26 May 2021 19:24:46 +0100 Subject: Change naturals to positive in predicates --- src/hls/HTLPargen.v | 2 +- src/hls/RTLBlockInstr.v | 122 +++++++++++++++++++++++++++++++----------------- 2 files changed, 79 insertions(+), 45 deletions(-) diff --git a/src/hls/HTLPargen.v b/src/hls/HTLPargen.v index 7ce6c7a..9746f92 100644 --- a/src/hls/HTLPargen.v +++ b/src/hls/HTLPargen.v @@ -659,7 +659,7 @@ Definition add_control_instr_force (n : node) (st : stmnt) : mon unit := Fixpoint pred_expr (preg: reg) (p: pred_op) := match p with | Pvar pred => - Vrange preg (Vlit (natToValue pred)) (Vlit (natToValue pred)) + Vrange preg (Vlit (posToValue pred)) (Vlit (posToValue pred)) | Pnot pred => Vunop Vnot (pred_expr preg pred) | Pand p1 p2 => diff --git a/src/hls/RTLBlockInstr.v b/src/hls/RTLBlockInstr.v index 86f8eba..ecd644b 100644 --- a/src/hls/RTLBlockInstr.v +++ b/src/hls/RTLBlockInstr.v @@ -34,7 +34,7 @@ Require Import vericert.hls.Sat. Local Open Scope rtl. Definition node := positive. -Definition predicate := nat. +Definition predicate := positive. Inductive pred_op : Type := | Pvar: predicate -> pred_op @@ -44,7 +44,7 @@ Inductive pred_op : Type := Fixpoint sat_predicate (p: pred_op) (a: asgn) : bool := match p with - | Pvar p' => a p' + | Pvar p' => a (Pos.to_nat p') | Pnot p' => negb (sat_predicate p' a) | Pand p1 p2 => sat_predicate p1 a && sat_predicate p2 a | Por p1 p2 => sat_predicate p1 a || sat_predicate p2 a @@ -152,7 +152,7 @@ Fixpoint trans_pred_temp (bound: nat) (p: pred_op) : option formula := | O => None | S n => match p with - | Pvar p' => Some (((true, p') :: nil) :: nil) + | Pvar p' => Some (((true, Pos.to_nat p') :: nil) :: nil) | Pand p1 p2 => match trans_pred_temp n p1, trans_pred_temp n p2 with | Some p1', Some p2' => @@ -165,7 +165,7 @@ Fixpoint trans_pred_temp (bound: nat) (p: pred_op) : option formula := Some (mult p1' p2') | _, _ => None end - | Pnot (Pvar p') => Some (((false, p') :: nil) :: nil) + | Pnot (Pvar p') => Some (((false, Pos.to_nat p') :: nil) :: nil) | Pnot (Pnot p) => trans_pred_temp n p | Pnot (Pand p1 p2) => trans_pred_temp n (Por (Pnot p1) (Pnot p2)) | Pnot (Por p1 p2) => trans_pred_temp n (Pand (Pnot p1) (Pnot p2)) @@ -180,7 +180,7 @@ Fixpoint trans_pred (bound: nat) (p: pred_op) : | O => None | S n => match p with - | Pvar p' => Some (exist _ (((true, p') :: nil) :: nil) _) + | Pvar p' => Some (exist _ (((true, Pos.to_nat p') :: nil) :: nil) _) | Pand p1 p2 => match trans_pred n p1, trans_pred n p2 with | Some (exist p1' _), Some (exist p2' _) => @@ -193,7 +193,7 @@ Fixpoint trans_pred (bound: nat) (p: pred_op) : Some (exist _ (mult p1' p2') _) | _, _ => None end - | Pnot (Pvar p') => Some (exist _ (((false, p') :: nil) :: nil) _) + | Pnot (Pvar p') => Some (exist _ (((false, Pos.to_nat p') :: nil) :: nil) _) | _ => None end end); split; intros; simpl in *; auto. @@ -310,6 +310,15 @@ Fixpoint max_reg_cfi (m : positive) (i : cf_instr) := end. Definition regset := Regmap.t val. +Definition predset := PMap.t bool. + +Fixpoint eval_predf (pr: predset) (p: pred_op) {struct p} := + match p with + | Pvar p' => PMap.get p' pr + | Pnot p' => negb (eval_predf pr p') + | Pand p' p'' => (eval_predf pr p') && (eval_predf pr p'') + | Por p' p'' => (eval_predf pr p') || (eval_predf pr p'') + end. Fixpoint init_regs (vl: list val) (rl: list reg) {struct rl} : regset := match rl, vl with @@ -320,6 +329,7 @@ Fixpoint init_regs (vl: list val) (rl: list reg) {struct rl} : regset := Inductive instr_state : Type := | InstrState: forall (rs: regset) + (pr: predset) (m: mem), instr_state. @@ -358,7 +368,8 @@ Section DEFINITION. (f: function) (**r calling function *) (sp: val) (**r stack pointer in calling function *) (pc: node) (**r program point in calling function *) - (rs: regset), (**r register state in calling function *) + (rs: regset) (**r register state in calling function *) + (pr: predset), (**r predicate state of the calling function *) stackframe. Inductive state : Type := @@ -368,6 +379,7 @@ Section DEFINITION. (sp: val) (**r stack pointer *) (pc: node) (**r current program point in [c] *) (rs: regset) (**r register state *) + (pr: predset) (**r predicate register state *) (m: mem), (**r memory state *) state | Callstate: @@ -403,67 +415,89 @@ Section RELSEM. end end. + Inductive eval_pred: option pred_op -> instr_state -> instr_state -> instr_state -> Prop := + | eval_pred_true: + forall (pr: predset) p rs pr m i, + eval_predf pr p = true -> + eval_pred (Some p) (InstrState rs pr m) i i + | eval_pred_false: + forall (pr: predset) p rs pr m i, + eval_predf pr p = false -> + eval_pred (Some p) (InstrState rs pr m) i (InstrState rs pr m) + | eval_pred_none: + forall i i', + eval_pred None i i' i. + Inductive step_instr: val -> instr_state -> instr -> instr_state -> Prop := | exec_RBnop: - forall rs m sp, - step_instr sp (InstrState rs m) RBnop (InstrState rs m) + forall sp ist, + step_instr sp ist RBnop ist | exec_RBop: - forall op v res args rs m sp p, - eval_operation ge sp op rs##args m = Some v -> - step_instr sp (InstrState rs m) - (RBop p op args res) - (InstrState (rs#res <- v) m) + forall op v res args rs m sp p ist pr, + eval_operation ge sp op rs##args m = Some v -> + eval_pred p (InstrState rs pr m) (InstrState (rs#res <- v) pr m) ist -> + step_instr sp (InstrState rs pr m) (RBop p op args res) ist | exec_RBload: - forall addr rs args a chunk m v dst sp p, - eval_addressing ge sp addr rs##args = Some a -> - Mem.loadv chunk m a = Some v -> - step_instr sp (InstrState rs m) - (RBload p chunk addr args dst) - (InstrState (rs#dst <- v) m) + forall addr rs args a chunk m v dst sp p pr ist, + eval_addressing ge sp addr rs##args = Some a -> + Mem.loadv chunk m a = Some v -> + eval_pred p (InstrState rs pr m) (InstrState (rs#dst <- v) pr m) ist -> + step_instr sp (InstrState rs pr m) (RBload p chunk addr args dst) ist | exec_RBstore: - forall addr rs args a chunk m src m' sp p, - eval_addressing ge sp addr rs##args = Some a -> - Mem.storev chunk m a rs#src = Some m' -> - step_instr sp (InstrState rs m) - (RBstore p chunk addr args src) - (InstrState rs m'). + forall addr rs args a chunk m src m' sp p pr ist, + eval_addressing ge sp addr rs##args = Some a -> + Mem.storev chunk m a rs#src = Some m' -> + eval_pred p (InstrState rs pr m) (InstrState rs pr m') ist -> + step_instr sp (InstrState rs pr m) (RBstore p chunk addr args src) ist + | exec_RBsetpred: + forall sp rs pr m p c b args, + Op.eval_condition c rs##args m = Some b -> + step_instr sp (InstrState rs pr m) (RBsetpred c args p) + (InstrState rs (PMap.set p b pr) m). Inductive step_cf_instr: state -> cf_instr -> trace -> state -> Prop := | exec_RBcall: - forall s f sp rs m res fd ros sig args pc pc', + forall s f sp rs m res fd ros sig args pc pc' pr, find_function ros rs = Some fd -> funsig fd = sig -> - step_cf_instr (State s f sp pc rs m) (RBcall sig ros args res pc') - E0 (Callstate (Stackframe res f sp pc' rs :: s) fd rs##args m) + step_cf_instr (State s f sp pc rs pr m) (RBcall sig ros args res pc') + E0 (Callstate (Stackframe res f sp pc' rs pr :: s) fd rs##args m) | exec_RBtailcall: - forall s f stk rs m sig ros args fd m' pc, + forall s f stk rs m sig ros args fd m' pc pr, find_function ros rs = Some fd -> funsig fd = sig -> Mem.free m stk 0 f.(fn_stacksize) = Some m' -> - step_cf_instr (State s f (Vptr stk Ptrofs.zero) pc rs m) (RBtailcall sig ros args) + step_cf_instr (State s f (Vptr stk Ptrofs.zero) pc rs pr m) (RBtailcall sig ros args) E0 (Callstate s fd rs##args m') | exec_RBbuiltin: - forall s f sp rs m ef args res pc' vargs t vres m' pc, + forall s f sp rs m ef args res pc' vargs t vres m' pc pr, eval_builtin_args ge (fun r => rs#r) sp m args vargs -> external_call ef ge vargs m t vres m' -> - step_cf_instr (State s f sp pc rs m) (RBbuiltin ef args res pc') - t (State s f sp pc' (regmap_setres res vres rs) m') + step_cf_instr (State s f sp pc rs pr m) (RBbuiltin ef args res pc') + t (State s f sp pc' (regmap_setres res vres rs) pr m') | exec_RBcond: - forall s f sp rs m cond args ifso ifnot b pc pc', + forall s f sp rs m cond args ifso ifnot b pc pc' pr, eval_condition cond rs##args m = Some b -> pc' = (if b then ifso else ifnot) -> - step_cf_instr (State s f sp pc rs m) (RBcond cond args ifso ifnot) - E0 (State s f sp pc' rs m) + step_cf_instr (State s f sp pc rs pr m) (RBcond cond args ifso ifnot) + E0 (State s f sp pc' rs pr m) | exec_RBjumptable: - forall s f sp rs m arg tbl n pc pc', + forall s f sp rs m arg tbl n pc pc' pr, rs#arg = Vint n -> list_nth_z tbl (Int.unsigned n) = Some pc' -> - step_cf_instr (State s f sp pc rs m) (RBjumptable arg tbl) - E0 (State s f sp pc' rs m) - | exec_Ireturn: - forall s f stk rs m or pc m', + step_cf_instr (State s f sp pc rs pr m) (RBjumptable arg tbl) + E0 (State s f sp pc' rs pr m) + | exec_RBreturn: + forall s f stk rs m or pc m' pr, Mem.free m stk 0 f.(fn_stacksize) = Some m' -> - step_cf_instr (State s f (Vptr stk Ptrofs.zero) pc rs m) (RBreturn or) - E0 (Returnstate s (regmap_optget or Vundef rs) m'). + step_cf_instr (State s f (Vptr stk Ptrofs.zero) pc rs pr m) (RBreturn or) + E0 (Returnstate s (regmap_optget or Vundef rs) m') + | exec_RBgoto: + forall s f sp pc rs pr m pc', + step_cf_instr (State s f sp pc rs pr m) (RBgoto pc') E0 (State s f sp pc' rs pr m) + | exec_RBpred_cf: + forall s f sp pc rs pr m cf1 cf2 st' p t, + step_cf_instr (State s f sp pc rs pr m) (if eval_predf pr p then cf1 else cf2) t st' -> + step_cf_instr (State s f sp pc rs pr m) (RBpred_cf p cf1 cf2) t st'. End RELSEM. -- cgit From 0cb04624f564ffd5e5e5b76cd2c5cf18a42465ac Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Wed, 26 May 2021 19:25:03 +0100 Subject: Fix if-conversion pass with positives --- src/hls/IfConversion.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/hls/IfConversion.v b/src/hls/IfConversion.v index 39d9fd2..f8d404c 100644 --- a/src/hls/IfConversion.v +++ b/src/hls/IfConversion.v @@ -106,7 +106,7 @@ Definition find_blocks_with_cond (c: code) : list (node * bblock) := Definition if_convert_code (p: nat * code) (nb: node * bblock) := let (n, bb) := nb in let (p', c) := p in - let nbb := if_convert_block c p' bb in + let nbb := if_convert_block c (Pos.of_nat p') bb in (S p', PTree.set n nbb c). Definition transf_function (f: function) : function := -- cgit From 14f10d3e983c53e525bf4056f9d43ecb9371ae83 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Wed, 26 May 2021 19:25:31 +0100 Subject: Add predicate semantics to RTLBlock --- src/hls/RTLBlock.v | 15 ++++++++------- 1 file changed, 8 insertions(+), 7 deletions(-) diff --git a/src/hls/RTLBlock.v b/src/hls/RTLBlock.v index 6a3487a..aaa3c6c 100644 --- a/src/hls/RTLBlock.v +++ b/src/hls/RTLBlock.v @@ -58,11 +58,11 @@ Section RELSEM. Inductive step: state -> trace -> state -> Prop := | exec_bblock: - forall s f sp pc rs rs' m m' t s' bb, + forall s f sp pc rs rs' m m' t s' bb pr pr', f.(fn_code)!pc = Some bb -> - step_instr_list sp (InstrState rs m) bb.(bb_body) (InstrState rs' m') -> - step_cf_instr ge (State s f sp pc rs' m') bb.(bb_exit) t s' -> - step (State s f sp pc rs m) t s' + step_instr_list sp (InstrState rs pr m) bb.(bb_body) (InstrState rs' pr' m') -> + step_cf_instr ge (State s f sp pc rs' pr' m') bb.(bb_exit) t s' -> + step (State s f sp pc rs pr m) t s' | exec_function_internal: forall s f args m m' stk, Mem.alloc m 0 f.(fn_stacksize) = (m', stk) -> @@ -72,6 +72,7 @@ Section RELSEM. (Vptr stk Ptrofs.zero) f.(fn_entrypoint) (init_regs args f.(fn_params)) + (PMap.init false) m') | exec_function_external: forall s ef args res t m m', @@ -79,9 +80,9 @@ Section RELSEM. step (Callstate s (External ef) args m) t (Returnstate s res m') | exec_return: - forall res f sp pc rs s vres m, - step (Returnstate (Stackframe res f sp pc rs :: s) vres m) - E0 (State s f sp pc (rs#res <- vres) m). + forall res f sp pc rs s vres m pr, + step (Returnstate (Stackframe res f sp pc rs pr :: s) vres m) + E0 (State s f sp pc (rs#res <- vres) pr m). End RELSEM. -- cgit From f40d3dfdf1412802f2f3a6f6f51a848bf5ff5704 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Wed, 26 May 2021 19:25:46 +0100 Subject: Add predicate semantics to RTLPar --- src/hls/RTLPar.v | 15 ++++++++------- 1 file changed, 8 insertions(+), 7 deletions(-) diff --git a/src/hls/RTLPar.v b/src/hls/RTLPar.v index 2e78d36..9d5fc77 100644 --- a/src/hls/RTLPar.v +++ b/src/hls/RTLPar.v @@ -80,11 +80,11 @@ Section RELSEM. Inductive step: state -> trace -> state -> Prop := | exec_bblock: - forall s f sp pc rs rs' m m' t s' bb, + forall s f sp pc rs rs' m m' t s' bb pr pr', f.(fn_code)!pc = Some bb -> - step_instr_block sp (InstrState rs m) bb.(bb_body) (InstrState rs' m') -> - step_cf_instr ge (State s f sp pc rs' m') bb.(bb_exit) t s' -> - step (State s f sp pc rs m) t s' + step_instr_block sp (InstrState rs pr m) bb.(bb_body) (InstrState rs' pr' m') -> + step_cf_instr ge (State s f sp pc rs' pr' m') bb.(bb_exit) t s' -> + step (State s f sp pc rs pr m) t s' | exec_function_internal: forall s f args m m' stk, Mem.alloc m 0 f.(fn_stacksize) = (m', stk) -> @@ -94,6 +94,7 @@ Section RELSEM. (Vptr stk Ptrofs.zero) f.(fn_entrypoint) (init_regs args f.(fn_params)) + (PMap.init false) m') | exec_function_external: forall s ef args res t m m', @@ -101,9 +102,9 @@ Section RELSEM. step (Callstate s (External ef) args m) t (Returnstate s res m') | exec_return: - forall res f sp pc rs s vres m, - step (Returnstate (Stackframe res f sp pc rs :: s) vres m) - E0 (State s f sp pc (rs#res <- vres) m). + forall res f sp pc rs s vres m pr, + step (Returnstate (Stackframe res f sp pc rs pr :: s) vres m) + E0 (State s f sp pc (rs#res <- vres) pr m). End RELSEM. -- 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(-) 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 8273bfff6ab40cd7c0e0f316551e17e509c46a47 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Wed, 7 Jul 2021 22:21:20 +0200 Subject: Add changelog which mentions the RAM support --- CHANGELOG.org | 1 + 1 file changed, 1 insertion(+) diff --git a/CHANGELOG.org b/CHANGELOG.org index 621683c..108dc30 100644 --- a/CHANGELOG.org +++ b/CHANGELOG.org @@ -10,6 +10,7 @@ RTL. - Add *RTLPar*, which can execute groups of instructions in parallel. - Add scheduling pass to go from RTLBlock to RTLPar. +- Proper RAM inference support. ** v1.1.0 - 2020-12-17 -- cgit From c4d44af5f3135aba4d4878f8f41c80d1f0b9e9a2 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Wed, 7 Jul 2021 22:23:53 +0200 Subject: New release information to the changelog --- CHANGELOG.org | 3 +++ 1 file changed, 3 insertions(+) diff --git a/CHANGELOG.org b/CHANGELOG.org index 108dc30..52db994 100644 --- a/CHANGELOG.org +++ b/CHANGELOG.org @@ -10,6 +10,9 @@ RTL. - Add *RTLPar*, which can execute groups of instructions in parallel. - Add scheduling pass to go from RTLBlock to RTLPar. + +** v1.2.0 - 2021-04-07 + - Proper RAM inference support. ** v1.1.0 - 2020-12-17 -- cgit From 728eb045e69f6a69c0cd089ba26e921d6bb65540 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Fri, 16 Jul 2021 10:03:02 +0200 Subject: Finish SAT proof --- src/hls/RTLBlockInstr.v | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/src/hls/RTLBlockInstr.v b/src/hls/RTLBlockInstr.v index ecd644b..36856f0 100644 --- a/src/hls/RTLBlockInstr.v +++ b/src/hls/RTLBlockInstr.v @@ -198,8 +198,9 @@ Fixpoint trans_pred (bound: nat) (p: pred_op) : end end); split; intros; simpl in *; auto. - inv H. inv H0; auto. - - admit. - - admit. + - split; auto. destruct (a p') eqn:?; crush. + - inv H. inv H0. unfold satLit in H. simplify. rewrite H. auto. + crush. - apply satFormula_concat. apply andb_prop in H. inv H. apply i in H0. auto. apply andb_prop in H. inv H. apply i0 in H1. auto. @@ -211,7 +212,7 @@ Fixpoint trans_pred (bound: nat) (p: pred_op) : - apply orb_true_intro. apply satFormula_mult2 in H. inv H. apply i in H0. auto. apply i0 in H0. auto. -Admitted. +Qed. Definition sat_pred (bound: nat) (p: pred_op) : option ({al : alist | sat_predicate p (interp_alist al) = true} -- cgit From c114bd7a269824623f2dbb41322d95d5056fca02 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Sun, 18 Jul 2021 14:07:49 +0200 Subject: Add full proof of SAT conversion --- src/hls/RTLBlockInstr.v | 24 ++++++++++++++++++++++-- 1 file changed, 22 insertions(+), 2 deletions(-) diff --git a/src/hls/RTLBlockInstr.v b/src/hls/RTLBlockInstr.v index 36856f0..c1d74b5 100644 --- a/src/hls/RTLBlockInstr.v +++ b/src/hls/RTLBlockInstr.v @@ -193,14 +193,34 @@ Fixpoint trans_pred (bound: nat) (p: pred_op) : Some (exist _ (mult p1' p2') _) | _, _ => None end - | Pnot (Pvar p') => Some (exist _ (((false, Pos.to_nat p') :: nil) :: nil) _) - | _ => None + | Pnot (Pvar p') => Some (exist _ (((false, p') :: nil) :: nil) _) + | Pnot (Pnot p') => + match trans_pred n p' with + | Some (exist p1' _) => Some (exist _ p1' _) + | None => None + end + | Pnot (Pand p1 p2) => + match trans_pred n (Por (Pnot p1) (Pnot p2)) with + | Some (exist p1' _) => Some (exist _ p1' _) + | None => None + end + | Pnot (Por p1 p2) => + match trans_pred n (Pand (Pnot p1) (Pnot p2)) with + | Some (exist p1' _) => Some (exist _ p1' _) + | None => None + end end end); split; intros; simpl in *; auto. - inv H. inv H0; auto. - split; auto. destruct (a p') eqn:?; crush. - inv H. inv H0. unfold satLit in H. simplify. rewrite H. auto. crush. + - rewrite negb_involutive in H. apply i in H. auto. + - rewrite negb_involutive. apply i; auto. + - rewrite negb_andb in H. apply i. auto. + - rewrite negb_andb. apply i. auto. + - rewrite negb_orb in H. apply i. auto. + - rewrite negb_orb. apply i. auto. - apply satFormula_concat. apply andb_prop in H. inv H. apply i in H0. auto. apply andb_prop in H. inv H. apply i0 in H1. auto. -- 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/RTLBlockInstr.v | 4 ++-- src/hls/RTLPargen.v | 54 ++++++++++++++++++++++++++++++++++++++++++++----- 2 files changed, 51 insertions(+), 7 deletions(-) diff --git a/src/hls/RTLBlockInstr.v b/src/hls/RTLBlockInstr.v index 79e3149..8063fd2 100644 --- a/src/hls/RTLBlockInstr.v +++ b/src/hls/RTLBlockInstr.v @@ -193,7 +193,7 @@ Fixpoint trans_pred (bound: nat) (p: pred_op) : Some (exist _ (mult p1' p2') _) | _, _ => None end - | Pnot (Pvar p') => Some (exist _ (((false, p') :: nil) :: nil) _) + | Pnot (Pvar p') => Some (exist _ (((false, Pos.to_nat p') :: nil) :: nil) _) | Pnot (Pnot p') => match trans_pred n p' with | Some (exist _ p1' _) => Some (exist _ p1' _) @@ -212,7 +212,7 @@ Fixpoint trans_pred (bound: nat) (p: pred_op) : end end); split; intros; simpl in *; auto. - inv H. inv H0; auto. - - split; auto. destruct (a p') eqn:?; crush. + - split; auto. destruct (a (Pos.to_nat p')) eqn:?; crush. - inv H. inv H0. unfold satLit in H. simplify. rewrite H. auto. crush. - rewrite negb_involutive in H. apply i in H. auto. 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 bddb95b05ace79d9298552873caa5a71733f1112 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Wed, 22 Sep 2021 14:54:29 +0100 Subject: Change Inductive to record --- src/hls/RTLBlock.v | 2 +- src/hls/RTLBlockInstr.v | 31 +++++++++++++++---------------- src/hls/RTLPar.v | 2 +- 3 files changed, 17 insertions(+), 18 deletions(-) diff --git a/src/hls/RTLBlock.v b/src/hls/RTLBlock.v index aaa3c6c..bf5c37a 100644 --- a/src/hls/RTLBlock.v +++ b/src/hls/RTLBlock.v @@ -60,7 +60,7 @@ Section RELSEM. | exec_bblock: forall s f sp pc rs rs' m m' t s' bb pr pr', f.(fn_code)!pc = Some bb -> - step_instr_list sp (InstrState rs pr m) bb.(bb_body) (InstrState rs' pr' m') -> + step_instr_list sp (mk_instr_state rs pr m) bb.(bb_body) (mk_instr_state rs' pr' m') -> step_cf_instr ge (State s f sp pc rs' pr' m') bb.(bb_exit) t s' -> step (State s f sp pc rs pr m) t s' | exec_function_internal: diff --git a/src/hls/RTLBlockInstr.v b/src/hls/RTLBlockInstr.v index 8063fd2..8cd3468 100644 --- a/src/hls/RTLBlockInstr.v +++ b/src/hls/RTLBlockInstr.v @@ -347,12 +347,11 @@ Fixpoint init_regs (vl: list val) (rl: list reg) {struct rl} : regset := | _, _ => Regmap.init Vundef end. -Inductive instr_state : Type := -| InstrState: - forall (rs: regset) - (pr: predset) - (m: mem), - instr_state. +Record instr_state := mk_instr_state { + instr_st_regset: regset; + instr_st_predset: predset; + instr_st_mem: mem; +}. Section DEFINITION. @@ -440,11 +439,11 @@ Section RELSEM. | eval_pred_true: forall (pr: predset) p rs pr m i, eval_predf pr p = true -> - eval_pred (Some p) (InstrState rs pr m) i i + eval_pred (Some p) (mk_instr_state rs pr m) i i | eval_pred_false: forall (pr: predset) p rs pr m i, eval_predf pr p = false -> - eval_pred (Some p) (InstrState rs pr m) i (InstrState rs pr m) + eval_pred (Some p) (mk_instr_state rs pr m) i (mk_instr_state rs pr m) | eval_pred_none: forall i i', eval_pred None i i' i. @@ -456,25 +455,25 @@ Section RELSEM. | exec_RBop: forall op v res args rs m sp p ist pr, eval_operation ge sp op rs##args m = Some v -> - eval_pred p (InstrState rs pr m) (InstrState (rs#res <- v) pr m) ist -> - step_instr sp (InstrState rs pr m) (RBop p op args res) ist + eval_pred p (mk_instr_state rs pr m) (mk_instr_state (rs#res <- v) pr m) ist -> + step_instr sp (mk_instr_state rs pr m) (RBop p op args res) ist | exec_RBload: forall addr rs args a chunk m v dst sp p pr ist, eval_addressing ge sp addr rs##args = Some a -> Mem.loadv chunk m a = Some v -> - eval_pred p (InstrState rs pr m) (InstrState (rs#dst <- v) pr m) ist -> - step_instr sp (InstrState rs pr m) (RBload p chunk addr args dst) ist + eval_pred p (mk_instr_state rs pr m) (mk_instr_state (rs#dst <- v) pr m) ist -> + step_instr sp (mk_instr_state rs pr m) (RBload p chunk addr args dst) ist | exec_RBstore: forall addr rs args a chunk m src m' sp p pr ist, eval_addressing ge sp addr rs##args = Some a -> Mem.storev chunk m a rs#src = Some m' -> - eval_pred p (InstrState rs pr m) (InstrState rs pr m') ist -> - step_instr sp (InstrState rs pr m) (RBstore p chunk addr args src) ist + eval_pred p (mk_instr_state rs pr m) (mk_instr_state rs pr m') ist -> + step_instr sp (mk_instr_state rs pr m) (RBstore p chunk addr args src) ist | exec_RBsetpred: forall sp rs pr m p c b args, Op.eval_condition c rs##args m = Some b -> - step_instr sp (InstrState rs pr m) (RBsetpred c args p) - (InstrState rs (PMap.set p b pr) m). + step_instr sp (mk_instr_state rs pr m) (RBsetpred c args p) + (mk_instr_state rs (PMap.set p b pr) m). Inductive step_cf_instr: state -> cf_instr -> trace -> state -> Prop := | exec_RBcall: diff --git a/src/hls/RTLPar.v b/src/hls/RTLPar.v index 9d5fc77..4986cff 100644 --- a/src/hls/RTLPar.v +++ b/src/hls/RTLPar.v @@ -82,7 +82,7 @@ Section RELSEM. | exec_bblock: forall s f sp pc rs rs' m m' t s' bb pr pr', f.(fn_code)!pc = Some bb -> - step_instr_block sp (InstrState rs pr m) bb.(bb_body) (InstrState rs' pr' m') -> + step_instr_block sp (mk_instr_state rs pr m) bb.(bb_body) (mk_instr_state rs' pr' m') -> step_cf_instr ge (State s f sp pc rs' pr' m') bb.(bb_exit) t s' -> step (State s f sp pc rs pr m) t s' | exec_function_internal: -- 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(-) 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/RTLBlockInstr.v | 4 ++-- src/hls/RTLPargen.v | 24 ++++++++++++++++-------- 2 files changed, 18 insertions(+), 10 deletions(-) diff --git a/src/hls/RTLBlockInstr.v b/src/hls/RTLBlockInstr.v index 8cd3468..8d3fde4 100644 --- a/src/hls/RTLBlockInstr.v +++ b/src/hls/RTLBlockInstr.v @@ -232,7 +232,7 @@ Fixpoint trans_pred (bound: nat) (p: pred_op) : - apply orb_true_intro. apply satFormula_mult2 in H. inv H. apply i in H0. auto. apply i0 in H0. auto. -Qed. +Defined. Definition sat_pred (bound: nat) (p: pred_op) : option ({al : alist | sat_predicate p (interp_alist al) = true} @@ -251,7 +251,7 @@ Definition sat_pred (bound: nat) (p: pred_op) : - intros. specialize (n a). specialize (i a). destruct (sat_predicate p a). exfalso. apply n. apply i. auto. auto. -Qed. +Defined. Definition sat_pred_simple (bound: nat) (p: pred_op) := match sat_pred bound p with 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(-) 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(-) 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 a6fb1adadcf2421b76cde649369f457a2a9ed66c Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Fri, 24 Sep 2021 12:59:06 +0100 Subject: Compile HTLPargen again --- src/Compiler.v | 4 ++-- src/hls/HTLPargen.v | 7 +++---- 2 files changed, 5 insertions(+), 6 deletions(-) diff --git a/src/Compiler.v b/src/Compiler.v index de29889..268f451 100644 --- a/src/Compiler.v +++ b/src/Compiler.v @@ -216,7 +216,7 @@ Definition transf_hls (p : Csyntax.program) : res Verilog.program := (* This is an unverified version of transf_hls with some experimental additions such as scheduling that aren't completed yet. *) -(*Definition transf_hls_temp (p : Csyntax.program) : res Verilog.program := +Definition transf_hls_temp (p : Csyntax.program) : res Verilog.program := OK p @@@ SimplExpr.transl_program @@@ SimplLocals.transf_program @@ -245,7 +245,7 @@ that aren't completed yet. *) @@@ RTLPargen.transl_program @@@ HTLPargen.transl_program @@ print print_HTL - @@ Veriloggen.transl_program.*) + @@ Veriloggen.transl_program. (*| Correctness Proof diff --git a/src/hls/HTLPargen.v b/src/hls/HTLPargen.v index 40d1dcc..9746f92 100644 --- a/src/hls/HTLPargen.v +++ b/src/hls/HTLPargen.v @@ -641,9 +641,9 @@ Definition add_control_instr_force_state_incr : s.(st_arrdecls) s.(st_datapath) (AssocMap.set n st s.(st_controllogic))). -Abort. +Admitted. -(*Definition add_control_instr_force (n : node) (st : stmnt) : mon unit := +Definition add_control_instr_force (n : node) (st : stmnt) : mon unit := fun s => OK tt (mkstate s.(st_st) @@ -708,7 +708,7 @@ Lemma create_new_state_state_incr: s.(st_arrdecls) s.(st_datapath) s.(st_controllogic)). -Abort. +Admitted. Definition create_new_state (p: node): mon node := fun s => OK s.(st_freshstate) @@ -876,4 +876,3 @@ Definition transl_program (p : RTLBlockInstr.program) : Errors.res HTL.program : if main_is_internal p then transform_partial_program transl_fundef p else Errors.Error (Errors.msg "Main function is not Internal."). -*) -- cgit From bb5695f5bcb9f3c3c7948c0f3a36da55ba5dcbcf Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Mon, 27 Sep 2021 01:17:32 +0100 Subject: Export without title --- README.org | 2 ++ 1 file changed, 2 insertions(+) diff --git a/README.org b/README.org index 4426561..368804f 100644 --- a/README.org +++ b/README.org @@ -1,3 +1,5 @@ +#+options: title:nil + #+html: #+html:

 

-- cgit From 02ca043e9c2d2aec31aec5a323535924a4414696 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Mon, 27 Sep 2021 18:14:33 +0100 Subject: Add dependencies for Alectryon documentation Update README on the status of Vericert --- README.org | 6 ++++-- default.nix | 6 +++++- docs | 2 +- src/extraction/Extraction.v | 8 ++++---- src/hls/Sat.v | 4 ++-- 5 files changed, 16 insertions(+), 10 deletions(-) diff --git a/README.org b/README.org index 4426561..faee0cc 100644 --- a/README.org +++ b/README.org @@ -1,3 +1,5 @@ +#+title: + #+html: #+html:

 

@@ -11,8 +13,8 @@ correctness. :PROPERTIES: :CUSTOM_ID: features :END: -The project is currently a work in progress, so proofs remain to be finished. Currently, the -following C features are supported, but are not all proven correct yet: + +Currently all proofs of the following features have been completed. - all int operations, - non-recursive function calls, diff --git a/default.nix b/default.nix index 1121469..fa60637 100644 --- a/default.nix +++ b/default.nix @@ -1,4 +1,4 @@ -with import (fetchTarball "https://github.com/NixOS/nixpkgs/archive/8dd8bd8be74879f9f7919b16a4cb5ab2a75f18e5.tar.gz") {}; +with import (fetchTarball "https://github.com/NixOS/nixpkgs/archive/1a56d76d718afb6c47dd96602c915b6d23f7c45d.tar.gz") {}; let ncoq = coq_8_13; ncoqPackages = coqPackages_8_13; @@ -10,6 +10,10 @@ stdenv.mkDerivation { buildInputs = [ ncoq dune_2 gcc ncoq.ocaml ncoq.ocamlPackages.findlib ncoq.ocamlPackages.menhir ncoq.ocamlPackages.ocamlgraph + ncoqPackages.serapi + python3 python3Packages.docutils python3Packages.pygments + python3Packages.dominate + python3Packages.pelican ]; enableParallelBuilding = true; diff --git a/docs b/docs index 5508c21..42e19f2 160000 --- a/docs +++ b/docs @@ -1 +1 @@ -Subproject commit 5508c21e064276aa4d5146b3af5b6f6e9a4c2364 +Subproject commit 42e19f2b20c907505a28486a8071147ed6c610fb diff --git a/src/extraction/Extraction.v b/src/extraction/Extraction.v index 6abe4e0..6bbfc05 100644 --- a/src/extraction/Extraction.v +++ b/src/extraction/Extraction.v @@ -179,7 +179,7 @@ Extract Inlined Constant Bracket.inbetween_loc => "fun _ -> assert false". Extract Constant Pipeline.pipeline => "SoftwarePipelining.pipeline". Extract Constant RTLBlockgen.partition => "Partition.partition". -(*Extract Constant RTLPargen.schedule => "Schedule.schedule_fn".*) +Extract Constant RTLPargen.schedule => "Schedule.schedule_fn". (* Needed in Coq 8.4 to avoid problems with Function definitions. *) Set Extraction AccessOpaque. @@ -187,11 +187,11 @@ Set Extraction AccessOpaque. Cd "src/extraction". Separate Extraction Verilog.module vericert.Compiler.transf_hls -(* vericert.Compiler.transf_hls_temp*) -(* RTLBlockgen.transl_program RTLBlockInstr.successors_instr*) + vericert.Compiler.transf_hls_temp + RTLBlockgen.transl_program RTLBlockInstr.successors_instr HTLgen.tbl_to_case_expr Pipeline.pipeline -(* RTLBlockInstr.sat_pred_temp*) + RTLBlockInstr.sat_pred_simple Verilog.stmnt_to_list Compiler.transf_c_program Compiler.transf_cminor_program diff --git a/src/hls/Sat.v b/src/hls/Sat.v index 9549947..679f5ec 100644 --- a/src/hls/Sat.v +++ b/src/hls/Sat.v @@ -202,9 +202,9 @@ Local Hint Resolve satLit_contra : core. obligations that it can't solve, or obligations that it takes 42 years to solve. However, if you think enough like me, each of the four definitions you fill in - should read like: [[ + should read like: refine some_expression_with_holes; clear function_name; magic_solver. -]] leaving out the [clear] invocation for non-recursive function definitions. + leaving out the [clear] invocation for non-recursive function definitions. *) Ltac magic_solver := simpl; intros; subst; intuition eauto; firstorder; match goal with -- cgit From 4101773e008b04c88cb5c78565afc6e08a9c4b5f Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Mon, 27 Sep 2021 20:25:27 +0100 Subject: Revert "Remove more OCaml files to compile successfully without admits." This reverts commit 9a4122dba9bdc33a8e912d5a45bae35e05afb229. --- driver/VericertDriver.ml | 1 + src/hls/Partition.ml | 124 +++++++ src/hls/PrintRTLBlock.ml | 72 ++++ src/hls/PrintRTLBlockInstr.ml | 87 +++++ src/hls/Schedule.ml | 801 ++++++++++++++++++++++++++++++++++++++++++ 5 files changed, 1085 insertions(+) create mode 100644 src/hls/Partition.ml create mode 100644 src/hls/PrintRTLBlock.ml create mode 100644 src/hls/PrintRTLBlockInstr.ml create mode 100644 src/hls/Schedule.ml diff --git a/driver/VericertDriver.ml b/driver/VericertDriver.ml index 1ea580f..aa5309a 100644 --- a/driver/VericertDriver.ml +++ b/driver/VericertDriver.ml @@ -65,6 +65,7 @@ let compile_c_file sourcename ifile ofile = set_dest Vericert.PrintClight.destination option_dclight ".light.c"; set_dest Vericert.PrintCminor.destination option_dcminor ".cm"; set_dest Vericert.PrintRTL.destination option_drtl ".rtl"; + set_dest Vericert.PrintRTLBlock.destination option_drtlblock ".rtlblock"; set_dest Vericert.PrintHTL.destination option_dhtl ".htl"; set_dest Vericert.Regalloc.destination_alloctrace option_dalloctrace ".alloctrace"; set_dest Vericert.PrintLTL.destination option_dltl ".ltl"; diff --git a/src/hls/Partition.ml b/src/hls/Partition.ml new file mode 100644 index 0000000..19c6048 --- /dev/null +++ b/src/hls/Partition.ml @@ -0,0 +1,124 @@ + (* + * Vericert: Verified high-level synthesis. + * Copyright (C) 2020 Yann Herklotz + * + * This program is free software: you can redistribute it and/or modify + * it under the terms of the GNU General Public License as published by + * the Free Software Foundation, either version 3 of the License, or + * (at your option) any later version. + * + * This program is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with this program. If not, see . + *) + +open Printf +open Clflags +open Camlcoq +open Datatypes +open Coqlib +open Maps +open AST +open Kildall +open Op +open RTLBlockInstr +open RTLBlock + +(* Assuming that the nodes of the CFG [code] are numbered in reverse postorder (cf. pass + [Renumber]), an edge from [n] to [s] is a normal edge if [s < n] and a back-edge otherwise. *) +let find_edge i n = + let succ = RTL.successors_instr i in + let filt = List.filter (fun s -> P.lt n s || P.lt s (P.pred n)) succ in + ((match filt with [] -> [] | _ -> [n]), filt) + +let find_edges c = + PTree.fold (fun l n i -> + let f = find_edge i n in + (List.append (fst f) (fst l), List.append (snd f) (snd l))) c ([], []) + +let prepend_instr i = function + | {bb_body = bb; bb_exit = e} -> {bb_body = (i :: bb); bb_exit = e} + +let translate_inst = function + | RTL.Inop _ -> Some RBnop + | RTL.Iop (op, ls, dst, _) -> Some (RBop (None, op, ls, dst)) + | RTL.Iload (m, addr, ls, dst, _) -> Some (RBload (None, m, addr, ls, dst)) + | RTL.Istore (m, addr, ls, src, _) -> Some (RBstore (None, m, addr, ls, src)) + | _ -> None + +let translate_cfi = function + | RTL.Icall (s, r, ls, dst, n) -> Some (RBcall (s, r, ls, dst, n)) + | RTL.Itailcall (s, r, ls) -> Some (RBtailcall (s, r, ls)) + | RTL.Ibuiltin (e, ls, r, n) -> Some (RBbuiltin (e, ls, r, n)) + | RTL.Icond (c, ls, dst1, dst2) -> Some (RBcond (c, ls, dst1, dst2)) + | RTL.Ijumptable (r, ls) -> Some (RBjumptable (r, ls)) + | RTL.Ireturn r -> Some (RBreturn r) + | _ -> None + +let rec next_bblock_from_RTL is_start e (c : RTL.code) s i = + let succ = List.map (fun i -> (i, PTree.get i c)) (RTL.successors_instr i) in + let trans_inst = (translate_inst i, translate_cfi i) in + match trans_inst, succ with + | (None, Some i'), _ -> + if List.exists (fun x -> x = s) (snd e) && not is_start then + Errors.OK { bb_body = []; bb_exit = RBgoto s } + else + Errors.OK { bb_body = []; bb_exit = i' } + | (Some i', None), (s', Some i_n)::[] -> + if List.exists (fun x -> x = s) (fst e) then + Errors.OK { bb_body = [i']; bb_exit = RBgoto s' } + else if List.exists (fun x -> x = s) (snd e) && not is_start then + Errors.OK { bb_body = []; bb_exit = RBgoto s } + else begin + match next_bblock_from_RTL false e c s' i_n with + | Errors.OK bb -> + Errors.OK (prepend_instr i' bb) + | Errors.Error msg -> Errors.Error msg + end + | _, _ -> + Errors.Error (Errors.msg (coqstring_of_camlstring "next_bblock_from_RTL went wrong.")) + +let rec traverseacc f l c = + match l with + | [] -> Errors.OK c + | x::xs -> + match f x c with + | Errors.Error msg -> Errors.Error msg + | Errors.OK x' -> + match traverseacc f xs x' with + | Errors.Error msg -> Errors.Error msg + | Errors.OK xs' -> Errors.OK xs' + +let rec translate_all edge c s res = + let c_bb, translated = res in + if List.exists (fun x -> P.eq x s) translated then Errors.OK (c_bb, translated) else + (match PTree.get s c with + | None -> Errors.Error (Errors.msg (coqstring_of_camlstring "Could not translate all.")) + | Some i -> + match next_bblock_from_RTL true edge c s i with + | Errors.Error msg -> Errors.Error msg + | Errors.OK {bb_body = bb; bb_exit = e} -> + let succ = List.filter (fun x -> P.lt x s) (successors_instr e) in + (match traverseacc (translate_all edge c) succ (c_bb, s :: translated) with + | Errors.Error msg -> Errors.Error msg + | Errors.OK (c', t') -> + Errors.OK (PTree.set s {bb_body = bb; bb_exit = e} c', t'))) + +(* Partition a function and transform it into RTLBlock. *) +let function_from_RTL f = + let e = find_edges f.RTL.fn_code in + match translate_all e f.RTL.fn_code f.RTL.fn_entrypoint (PTree.empty, []) with + | Errors.Error msg -> Errors.Error msg + | Errors.OK (c, _) -> + Errors.OK { fn_sig = f.RTL.fn_sig; + fn_stacksize = f.RTL.fn_stacksize; + fn_params = f.RTL.fn_params; + fn_entrypoint = f.RTL.fn_entrypoint; + fn_code = c + } + +let partition = function_from_RTL diff --git a/src/hls/PrintRTLBlock.ml b/src/hls/PrintRTLBlock.ml new file mode 100644 index 0000000..8fef401 --- /dev/null +++ b/src/hls/PrintRTLBlock.ml @@ -0,0 +1,72 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + +(** Pretty-printers for RTL code *) + +open Printf +open Camlcoq +open Datatypes +open Maps +open AST +open RTLBlockInstr +open RTLBlock +open PrintAST +open PrintRTLBlockInstr + +(* Printing of RTL code *) + +let reg pp r = + fprintf pp "x%d" (P.to_int r) + +let rec regs pp = function + | [] -> () + | [r] -> reg pp r + | r1::rl -> fprintf pp "%a, %a" reg r1 regs rl + +let ros pp = function + | Coq_inl r -> reg pp r + | Coq_inr s -> fprintf pp "\"%s\"" (extern_atom s) + +let print_bblock pp (pc, i) = + fprintf pp "%5d:{\n" pc; + List.iter (print_bblock_body pp) i.bb_body; + print_bblock_exit pp i.bb_exit; + fprintf pp "\t}\n\n" + +let print_function pp id f = + fprintf pp "%s(%a) {\n" (extern_atom id) regs f.fn_params; + let instrs = + List.sort + (fun (pc1, _) (pc2, _) -> compare pc2 pc1) + (List.rev_map + (fun (pc, i) -> (P.to_int pc, i)) + (PTree.elements f.fn_code)) in + List.iter (print_bblock pp) instrs; + fprintf pp "}\n\n" + +let print_globdef pp (id, gd) = + match gd with + | Gfun(Internal f) -> print_function pp id f + | _ -> () + +let print_program pp (prog: program) = + List.iter (print_globdef pp) prog.prog_defs + +let destination : string option ref = ref None + +let print_if passno prog = + match !destination with + | None -> () + | Some f -> + let oc = open_out (f ^ "." ^ Z.to_string passno) in + print_program oc prog; + close_out oc diff --git a/src/hls/PrintRTLBlockInstr.ml b/src/hls/PrintRTLBlockInstr.ml new file mode 100644 index 0000000..ba7241b --- /dev/null +++ b/src/hls/PrintRTLBlockInstr.ml @@ -0,0 +1,87 @@ +open Printf +open Camlcoq +open Datatypes +open Maps +open AST +open RTLBlockInstr +open PrintAST + +let reg pp r = + fprintf pp "x%d" (P.to_int r) + +let pred pp r = + fprintf pp "p%d" (Nat.to_int r) + +let rec regs pp = function + | [] -> () + | [r] -> reg pp r + | r1::rl -> fprintf pp "%a, %a" reg r1 regs rl + +let ros pp = function + | Coq_inl r -> reg pp r + | Coq_inr s -> fprintf pp "\"%s\"" (extern_atom s) + +let rec print_pred_op pp = function + | Pvar p -> pred pp p + | Pnot p -> fprintf pp "(~ %a)" print_pred_op p + | Pand (p1, p2) -> fprintf pp "(%a & %a)" print_pred_op p1 print_pred_op p2 + | Por (p1, p2) -> fprintf pp "(%a | %a)" print_pred_op p1 print_pred_op p2 + +let print_pred_option pp = function + | Some x -> fprintf pp "(%a)" print_pred_op x + | None -> () + +let print_bblock_body pp i = + fprintf pp "\t\t"; + match i with + | RBnop -> fprintf pp "nop\n" + | RBop(p, op, ls, dst) -> + fprintf pp "%a %a = %a\n" + print_pred_option p reg dst (PrintOp.print_operation reg) (op, ls) + | RBload(p, chunk, addr, args, dst) -> + fprintf pp "%a %a = %s[%a]\n" + print_pred_option p reg dst (name_of_chunk chunk) + (PrintOp.print_addressing reg) (addr, args) + | RBstore(p, chunk, addr, args, src) -> + fprintf pp "%a %s[%a] = %a\n" + print_pred_option p + (name_of_chunk chunk) + (PrintOp.print_addressing reg) (addr, args) + reg src + | RBsetpred (c, args, p) -> + fprintf pp "%a = %a\n" + pred p + (PrintOp.print_condition reg) (c, args) + +let rec print_bblock_exit pp i = + fprintf pp "\t\t"; + match i with + | RBcall(_, fn, args, res, _) -> + fprintf pp "%a = %a(%a)\n" + reg res ros fn regs args; + | RBtailcall(_, fn, args) -> + fprintf pp "tailcall %a(%a)\n" + ros fn regs args + | RBbuiltin(ef, args, res, _) -> + fprintf pp "%a = %s(%a)\n" + (print_builtin_res reg) res + (name_of_external ef) + (print_builtin_args reg) args + | RBcond(cond, args, s1, s2) -> + fprintf pp "if (%a) goto %d else goto %d\n" + (PrintOp.print_condition reg) (cond, args) + (P.to_int s1) (P.to_int s2) + | RBjumptable(arg, tbl) -> + let tbl = Array.of_list tbl in + fprintf pp "jumptable (%a)\n" reg arg; + for i = 0 to Array.length tbl - 1 do + fprintf pp "\tcase %d: goto %d\n" i (P.to_int tbl.(i)) + done + | RBreturn None -> + fprintf pp "return\n" + | RBreturn (Some arg) -> + fprintf pp "return %a\n" reg arg + | RBgoto n -> + fprintf pp "goto %d\n" (P.to_int n) + | RBpred_cf (p, c1, c2) -> + fprintf pp "if %a then (%a) else (%a)\n" print_pred_op p print_bblock_exit c1 print_bblock_exit c2 diff --git a/src/hls/Schedule.ml b/src/hls/Schedule.ml new file mode 100644 index 0000000..c6c8bf4 --- /dev/null +++ b/src/hls/Schedule.ml @@ -0,0 +1,801 @@ +(* + * Vericert: Verified high-level synthesis. + * Copyright (C) 2020 Yann Herklotz + * + * This program is free software: you can redistribute it and/or modify + * it under the terms of the GNU General Public License as published by + * the Free Software Foundation, either version 3 of the License, or + * (at your option) any later version. + * + * This program is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with this program. If not, see . + *) + +open Printf +open Clflags +open Camlcoq +open Datatypes +open Coqlib +open Maps +open AST +open Kildall +open Op +open RTLBlockInstr +open RTLBlock +open HTL +open Verilog +open HTLgen +open HTLMonad +open HTLMonadExtra + +module SS = Set.Make(P) + +type svtype = + | BBType of int + | VarType of int * int + +type sv = { + sv_type: svtype; + sv_num: int; +} + +let print_sv v = + match v with + | { sv_type = BBType bbi; sv_num = n } -> sprintf "bb%d_%d" bbi n + | { sv_type = VarType (bbi, i); sv_num = n } -> sprintf "var%dn%d_%d" bbi i n + +module G = Graph.Persistent.Digraph.ConcreteLabeled(struct + type t = sv + let compare = compare + let equal = (=) + let hash = Hashtbl.hash +end)(struct + type t = int + let compare = compare + let hash = Hashtbl.hash + let equal = (=) + let default = 0 +end) + +module GDot = Graph.Graphviz.Dot(struct + let graph_attributes _ = [] + let default_vertex_attributes _ = [] + let vertex_name = print_sv + let vertex_attributes _ = [] + let get_subgraph _ = None + let default_edge_attributes _ = [] + let edge_attributes _ = [] + + include G + end) + +module DFG = Graph.Persistent.Digraph.ConcreteLabeled(struct + type t = int * instr + let compare = compare + let equal = (=) + let hash = Hashtbl.hash +end)(struct + type t = int + let compare = compare + let hash = Hashtbl.hash + let equal = (=) + let default = 0 +end) + +let reg r = sprintf "r%d" (P.to_int r) +let print_pred r = sprintf "p%d" (Nat.to_int r) + +let print_instr = function + | RBnop -> "" + | RBload (_, _, _, _, r) -> sprintf "load(%s)" (reg r) + | RBstore (_, _, _, _, r) -> sprintf "store(%s)" (reg r) + | RBsetpred (_, _, p) -> sprintf "setpred(%s)" (print_pred p) + | RBop (_, op, args, d) -> + (match op, args with + | Omove, _ -> "mov" + | Ointconst n, _ -> sprintf "%s=%ld" (reg d) (camlint_of_coqint n) + | Olongconst n, _ -> sprintf "%s=%LdL" (reg d) (camlint64_of_coqint n) + | Ofloatconst n, _ -> sprintf "%s=%.15F" (reg d) (camlfloat_of_coqfloat n) + | Osingleconst n, _ -> sprintf "%s=%.15Ff" (reg d) (camlfloat_of_coqfloat32 n) + | Oindirectsymbol id, _ -> sprintf "%s=&%s" (reg d) (extern_atom id) + | Ocast8signed, [r1] -> sprintf "%s=int8signed(%s)" (reg d) (reg r1) + | Ocast8unsigned, [r1] -> sprintf "%s=int8unsigned(%s)" (reg d) (reg r1) + | Ocast16signed, [r1] -> sprintf "%s=int16signed(%s)" (reg d) (reg r1) + | Ocast16unsigned, [r1] -> sprintf "%s=int16unsigned(%s)" (reg d) (reg r1) + | Oneg, [r1] -> sprintf "%s=-%s" (reg d) (reg r1) + | Osub, [r1;r2] -> sprintf "%s=%s-%s" (reg d) (reg r1) (reg r2) + | Omul, [r1;r2] -> sprintf "%s=%s*%s" (reg d) (reg r1) (reg r2) + | Omulimm n, [r1] -> sprintf "%s=%s*%ld" (reg d) (reg r1) (camlint_of_coqint n) + | Omulhs, [r1;r2] -> sprintf "%s=mulhs(%s,%s)" (reg d) (reg r1) (reg r2) + | Omulhu, [r1;r2] -> sprintf "%s=mulhu(%s,%s)" (reg d) (reg r1) (reg r2) + | Odiv, [r1;r2] -> sprintf "%s=%s /s %s" (reg d) (reg r1) (reg r2) + | Odivu, [r1;r2] -> sprintf "%s=%s /u %s" (reg d) (reg r1) (reg r2) + | Omod, [r1;r2] -> sprintf "%s=%s %%s %s" (reg d) (reg r1) (reg r2) + | Omodu, [r1;r2] -> sprintf "%s=%s %%u %s" (reg d) (reg r1) (reg r2) + | Oand, [r1;r2] -> sprintf "%s=%s & %s" (reg d) (reg r1) (reg r2) + | Oandimm n, [r1] -> sprintf "%s=%s & %ld" (reg d) (reg r1) (camlint_of_coqint n) + | Oor, [r1;r2] -> sprintf "%s=%s | %s" (reg d) (reg r1) (reg r2) + | Oorimm n, [r1] -> sprintf "%s=%s | %ld" (reg d) (reg r1) (camlint_of_coqint n) + | Oxor, [r1;r2] -> sprintf "%s=%s ^ %s" (reg d) (reg r1) (reg r2) + | Oxorimm n, [r1] -> sprintf "%s=%s ^ %ld" (reg d) (reg r1) (camlint_of_coqint n) + | Onot, [r1] -> sprintf "%s=not(%s)" (reg d) (reg r1) + | Oshl, [r1;r2] -> sprintf "%s=%s << %s" (reg d) (reg r1) (reg r2) + | Oshlimm n, [r1] -> sprintf "%s=%s << %ld" (reg d) (reg r1) (camlint_of_coqint n) + | Oshr, [r1;r2] -> sprintf "%s=%s >>s %s" (reg d) (reg r1) (reg r2) + | Oshrimm n, [r1] -> sprintf "%s=%s >>s %ld" (reg d) (reg r1) (camlint_of_coqint n) + | Oshrximm n, [r1] -> sprintf "%s=%s >>x %ld" (reg d) (reg r1) (camlint_of_coqint n) + | Oshru, [r1;r2] -> sprintf "%s=%s >>u %s" (reg d) (reg r1) (reg r2) + | Oshruimm n, [r1] -> sprintf "%s=%s >>u %ld" (reg d) (reg r1) (camlint_of_coqint n) + | Ororimm n, [r1] -> sprintf "%s=%s ror %ld" (reg d) (reg r1) (camlint_of_coqint n) + | Oshldimm n, [r1;r2] -> sprintf "%s=(%s, %s) << %ld" (reg d) (reg r1) (reg r2) (camlint_of_coqint n) + | Olea addr, args -> sprintf "%s=addr" (reg d) + | Omakelong, [r1;r2] -> sprintf "%s=makelong(%s,%s)" (reg d) (reg r1) (reg r2) + | Olowlong, [r1] -> sprintf "%s=lowlong(%s)" (reg d) (reg r1) + | Ohighlong, [r1] -> sprintf "%s=highlong(%s)" (reg d) (reg r1) + | Ocast32signed, [r1] -> sprintf "%s=long32signed(%s)" (reg d) (reg r1) + | Ocast32unsigned, [r1] -> sprintf "%s=long32unsigned(%s)" (reg d) (reg r1) + | Onegl, [r1] -> sprintf "%s=-l %s" (reg d) (reg r1) + | Osubl, [r1;r2] -> sprintf "%s=%s -l %s" (reg d) (reg r1) (reg r2) + | Omull, [r1;r2] -> sprintf "%s=%s *l %s" (reg d) (reg r1) (reg r2) + | Omullimm n, [r1] -> sprintf "%s=%s *l %Ld" (reg d) (reg r1) (camlint64_of_coqint n) + | Omullhs, [r1;r2] -> sprintf "%s=mullhs(%s,%s)" (reg d) (reg r1) (reg r2) + | Omullhu, [r1;r2] -> sprintf "%s=mullhu(%s,%s)" (reg d) (reg r1) (reg r2) + | Odivl, [r1;r2] -> sprintf "%s=%s /ls %s" (reg d) (reg r1) (reg r2) + | Odivlu, [r1;r2] -> sprintf "%s=%s /lu %s" (reg d) (reg r1) (reg r2) + | Omodl, [r1;r2] -> sprintf "%s=%s %%ls %s" (reg d) (reg r1) (reg r2) + | Omodlu, [r1;r2] -> sprintf "%s=%s %%lu %s" (reg d) (reg r1) (reg r2) + | Oandl, [r1;r2] -> sprintf "%s=%s &l %s" (reg d) (reg r1) (reg r2) + | Oandlimm n, [r1] -> sprintf "%s=%s &l %Ld" (reg d) (reg r1) (camlint64_of_coqint n) + | Oorl, [r1;r2] -> sprintf "%s=%s |l %s" (reg d) (reg r1) (reg r2) + | Oorlimm n, [r1] -> sprintf "%s=%s |l %Ld" (reg d) (reg r1) (camlint64_of_coqint n) + | Oxorl, [r1;r2] -> sprintf "%s=%s ^l %s" (reg d) (reg r1) (reg r2) + | Oxorlimm n, [r1] -> sprintf "%s=%s ^l %Ld" (reg d) (reg r1) (camlint64_of_coqint n) + | Onotl, [r1] -> sprintf "%s=notl(%s)" (reg d) (reg r1) + | Oshll, [r1;r2] -> sprintf "%s=%s < sprintf "%s=%s < sprintf "%s=%s >>ls %s" (reg d) (reg r1) (reg r2) + | Oshrlimm n, [r1] -> sprintf "%s=%s >>ls %ld" (reg d) (reg r1) (camlint_of_coqint n) + | Oshrxlimm n, [r1] -> sprintf "%s=%s >>lx %ld" (reg d) (reg r1) (camlint_of_coqint n) + | Oshrlu, [r1;r2] -> sprintf "%s=%s >>lu %s" (reg d) (reg r1) (reg r2) + | Oshrluimm n, [r1] -> sprintf "%s=%s >>lu %ld" (reg d) (reg r1) (camlint_of_coqint n) + | Ororlimm n, [r1] -> sprintf "%s=%s rorl %ld" (reg d) (reg r1) (camlint_of_coqint n) + | Oleal addr, args -> sprintf "%s=addr" (reg d) + | Onegf, [r1] -> sprintf "%s=negf(%s)" (reg d) (reg r1) + | Oabsf, [r1] -> sprintf "%s=absf(%s)" (reg d) (reg r1) + | Oaddf, [r1;r2] -> sprintf "%s=%s +f %s" (reg d) (reg r1) (reg r2) + | Osubf, [r1;r2] -> sprintf "%s=%s -f %s" (reg d) (reg r1) (reg r2) + | Omulf, [r1;r2] -> sprintf "%s=%s *f %s" (reg d) (reg r1) (reg r2) + | Odivf, [r1;r2] -> sprintf "%s=%s /f %s" (reg d) (reg r1) (reg r2) + | Onegfs, [r1] -> sprintf "%s=negfs(%s)" (reg d) (reg r1) + | Oabsfs, [r1] -> sprintf "%s=absfs(%s)" (reg d) (reg r1) + | Oaddfs, [r1;r2] -> sprintf "%s=%s +fs %s" (reg d) (reg r1) (reg r2) + | Osubfs, [r1;r2] -> sprintf "%s=%s -fs %s" (reg d) (reg r1) (reg r2) + | Omulfs, [r1;r2] -> sprintf "%s=%s *fs %s" (reg d) (reg r1) (reg r2) + | Odivfs, [r1;r2] -> sprintf "%s=%s /fs %s" (reg d) (reg r1) (reg r2) + | Osingleoffloat, [r1] -> sprintf "%s=singleoffloat(%s)" (reg d) (reg r1) + | Ofloatofsingle, [r1] -> sprintf "%s=floatofsingle(%s)" (reg d) (reg r1) + | Ointoffloat, [r1] -> sprintf "%s=intoffloat(%s)" (reg d) (reg r1) + | Ofloatofint, [r1] -> sprintf "%s=floatofint(%s)" (reg d) (reg r1) + | Ointofsingle, [r1] -> sprintf "%s=intofsingle(%s)" (reg d) (reg r1) + | Osingleofint, [r1] -> sprintf "%s=singleofint(%s)" (reg d) (reg r1) + | Olongoffloat, [r1] -> sprintf "%s=longoffloat(%s)" (reg d) (reg r1) + | Ofloatoflong, [r1] -> sprintf "%s=floatoflong(%s)" (reg d) (reg r1) + | Olongofsingle, [r1] -> sprintf "%s=longofsingle(%s)" (reg d) (reg r1) + | Osingleoflong, [r1] -> sprintf "%s=singleoflong(%s)" (reg d) (reg r1) + | Ocmp c, args -> sprintf "%s=cmp" (reg d) + | Osel (c, ty), r1::r2::args -> sprintf "%s=sel" (reg d) + | _, _ -> sprintf "N/a") + +module DFGDot = Graph.Graphviz.Dot(struct + let graph_attributes _ = [] + let default_vertex_attributes _ = [] + let vertex_name = function (i, instr) -> sprintf "\"%d:%s\"" i (print_instr instr) + let vertex_attributes _ = [] + let get_subgraph _ = None + let default_edge_attributes _ = [] + let edge_attributes _ = [] + + include DFG + end) + +module IMap = Map.Make (struct + type t = int + + let compare = compare +end) + +let gen_vertex instrs i = (i, List.nth instrs i) + +(** The DFG type defines a list of instructions with their data dependencies as [edges], which are + the pairs of integers that represent the index of the instruction in the [nodes]. The edges + always point from left to right. *) + +let print_list f out_chan a = + fprintf out_chan "[ "; + List.iter (fprintf out_chan "%a " f) a; + fprintf out_chan "]" + +let print_tuple out_chan a = + let l, r = a in + fprintf out_chan "(%d,%d)" l r + +(*let print_dfg out_chan dfg = + fprintf out_chan "{ nodes = %a, edges = %a }" + (print_list PrintRTLBlockInstr.print_bblock_body) + dfg.nodes (print_list print_tuple) dfg.edges*) + +let print_dfg = DFGDot.output_graph + +let read_process command = + let buffer_size = 2048 in + let buffer = Buffer.create buffer_size in + let string = Bytes.create buffer_size in + let in_channel = Unix.open_process_in command in + let chars_read = ref 1 in + while !chars_read <> 0 do + chars_read := input in_channel string 0 buffer_size; + Buffer.add_substring buffer (Bytes.to_string string) 0 !chars_read + done; + ignore (Unix.close_process_in in_channel); + Buffer.contents buffer + +let comb_delay = function + | RBnop -> 0 + | RBop (_, op, _, _) -> + (match op with + | Omove -> 0 + | Ointconst _ -> 0 + | Olongconst _ -> 0 + | Ocast8signed -> 0 + | Ocast8unsigned -> 0 + | Ocast16signed -> 0 + | Ocast16unsigned -> 0 + | Oneg -> 0 + | Onot -> 0 + | Oor -> 0 + | Oorimm _ -> 0 + | Oand -> 0 + | Oandimm _ -> 0 + | Oxor -> 0 + | Oxorimm _ -> 0 + | Omul -> 8 + | Omulimm _ -> 8 + | Omulhs -> 8 + | Omulhu -> 8 + | Odiv -> 72 + | Odivu -> 72 + | Omod -> 72 + | Omodu -> 72 + | _ -> 1) + | _ -> 1 + +let pipeline_stages = function + | RBop (_, op, _, _) -> + (match op with + | Odiv -> 32 + | Odivu -> 32 + | Omod -> 32 + | Omodu -> 32 + | _ -> 0) + | _ -> 0 + +(** Add a dependency if it uses a register that was written to previously. *) +let add_dep map i tree dfg curr = + match PTree.get curr tree with + | None -> dfg + | Some ip -> + let ipv = (List.nth map ip) in + DFG.add_edge_e dfg (ipv, comb_delay (snd ipv), List.nth map i) + +(** This function calculates the dependencies of each instruction. The nodes correspond to previous + registers that were allocated and show which instruction caused it. + + This function only gathers the RAW constraints, and will therefore only be active for operations + that modify registers, which is this case only affects loads and operations. *) +let accumulate_RAW_deps map dfg curr = + let i, dst_map, graph = dfg in + let acc_dep_instruction rs dst = + ( i + 1, + PTree.set dst i dst_map, + List.fold_left (add_dep map i dst_map) graph rs + ) + in + let acc_dep_instruction_nodst rs = + ( i + 1, + dst_map, + List.fold_left (add_dep map i dst_map) graph rs) + in + match curr with + | RBop (op, _, rs, dst) -> acc_dep_instruction rs dst + | RBload (op, _mem, _addr, rs, dst) -> acc_dep_instruction rs dst + | RBstore (op, _mem, _addr, rs, src) -> acc_dep_instruction_nodst (src :: rs) + | _ -> (i + 1, dst_map, graph) + +(** Finds the next write to the [dst] register. This is a small optimisation so that only one + dependency is generated for a data dependency. *) +let rec find_next_dst_write i dst i' curr = + let check_dst dst' curr' = + if dst = dst' then Some (i, i') + else find_next_dst_write i dst (i' + 1) curr' + in + match curr with + | [] -> None + | RBop (_, _, _, dst') :: curr' -> check_dst dst' curr' + | RBload (_, _, _, _, dst') :: curr' -> check_dst dst' curr' + | _ :: curr' -> find_next_dst_write i dst (i' + 1) curr' + +let rec find_all_next_dst_read i dst i' curr = + let check_dst rs curr' = + if List.exists (fun x -> x = dst) rs + then (i, i') :: find_all_next_dst_read i dst (i' + 1) curr' + else find_all_next_dst_read i dst (i' + 1) curr' + in + match curr with + | [] -> [] + | RBop (_, _, rs, _) :: curr' -> check_dst rs curr' + | RBload (_, _, _, rs, _) :: curr' -> check_dst rs curr' + | RBstore (_, _, _, rs, src) :: curr' -> check_dst (src :: rs) curr' + | RBnop :: curr' -> find_all_next_dst_read i dst (i' + 1) curr' + | RBsetpred (_, rs, _) :: curr' -> check_dst rs curr' + +let drop i lst = + let rec drop' i' lst' = + match lst' with + | _ :: ls -> if i' = i then ls else drop' (i' + 1) ls + | [] -> [] + in + if i = 0 then lst else drop' 1 lst + +let take i lst = + let rec take' i' lst' = + match lst' with + | l :: ls -> if i' = i then [ l ] else l :: take' (i' + 1) ls + | [] -> [] + in + if i = 0 then [] else take' 1 lst + +let rec next_store i = function + | [] -> None + | RBstore (_, _, _, _, _) :: _ -> Some i + | _ :: rst -> next_store (i + 1) rst + +let rec next_load i = function + | [] -> None + | RBload (_, _, _, _, _) :: _ -> Some i + | _ :: rst -> next_load (i + 1) rst + +let accumulate_RAW_mem_deps instrs dfg curri = + let i, curr = curri in + match curr with + | RBload (_, _, _, _, _) -> ( + match next_store 0 (take i instrs |> List.rev) with + | None -> dfg + | Some d -> DFG.add_edge dfg (gen_vertex instrs (i - d - 1)) (gen_vertex instrs i) ) + | _ -> dfg + +let accumulate_WAR_mem_deps instrs dfg curri = + let i, curr = curri in + match curr with + | RBstore (_, _, _, _, _) -> ( + match next_load 0 (take i instrs |> List.rev) with + | None -> dfg + | Some d -> DFG.add_edge dfg (gen_vertex instrs (i - d - 1)) (gen_vertex instrs i) ) + | _ -> dfg + +let accumulate_WAW_mem_deps instrs dfg curri = + let i, curr = curri in + match curr with + | RBstore (_, _, _, _, _) -> ( + match next_store 0 (take i instrs |> List.rev) with + | None -> dfg + | Some d -> DFG.add_edge dfg (gen_vertex instrs (i - d - 1)) (gen_vertex instrs i) ) + | _ -> dfg + +(** Predicate dependencies. *) + +let rec in_predicate p p' = + match p' with + | Pvar p'' -> Nat.to_int p = Nat.to_int p'' + | Pnot p'' -> in_predicate p p'' + | Pand (p1, p2) -> in_predicate p p1 || in_predicate p p2 + | Por (p1, p2) -> in_predicate p p1 || in_predicate p p2 + +let get_predicate = function + | RBop (p, _, _, _) -> p + | RBload (p, _, _, _, _) -> p + | RBstore (p, _, _, _, _) -> p + | _ -> None + +let rec next_setpred p i = function + | [] -> None + | RBsetpred (_, _, p') :: rst -> + if in_predicate p' p then + Some i + else + next_setpred p (i + 1) rst + | _ :: rst -> next_setpred p (i + 1) rst + +let rec next_preduse p i instr= + let next p' rst = + if in_predicate p p' then + Some i + else + next_preduse p (i + 1) rst + in + match instr with + | [] -> None + | RBload (Some p', _, _, _, _) :: rst -> next p' rst + | RBstore (Some p', _, _, _, _) :: rst -> next p' rst + | RBop (Some p', _, _, _) :: rst -> next p' rst + | _ :: rst -> next_load (i + 1) rst + +let accumulate_RAW_pred_deps instrs dfg curri = + let i, curr = curri in + match get_predicate curr with + | Some p -> ( + match next_setpred p 0 (take i instrs |> List.rev) with + | None -> dfg + | Some d -> DFG.add_edge dfg (gen_vertex instrs (i - d - 1)) (gen_vertex instrs i) ) + | _ -> dfg + +let accumulate_WAR_pred_deps instrs dfg curri = + let i, curr = curri in + match curr with + | RBsetpred (_, _, p) -> ( + match next_preduse p 0 (take i instrs |> List.rev) with + | None -> dfg + | Some d -> DFG.add_edge dfg (gen_vertex instrs (i - d - 1)) (gen_vertex instrs i) ) + | _ -> dfg + +let accumulate_WAW_pred_deps instrs dfg curri = + let i, curr = curri in + match curr with + | RBsetpred (_, _, p) -> ( + match next_setpred (Pvar p) 0 (take i instrs |> List.rev) with + | None -> dfg + | Some d -> DFG.add_edge dfg (gen_vertex instrs (i - d - 1)) (gen_vertex instrs i) ) + | _ -> dfg + +(** This function calculates the WAW dependencies, which happen when two writes are ordered one + after another and therefore have to be kept in that order. This accumulation might be redundant + if register renaming is done before hand, because then these dependencies can be avoided. *) +let accumulate_WAW_deps instrs dfg curri = + let i, curr = curri in + let dst_dep dst = + match find_next_dst_write i dst (i + 1) (drop (i + 1) instrs) with + | Some (a, b) -> DFG.add_edge dfg (gen_vertex instrs a) (gen_vertex instrs b) + | _ -> dfg + in + match curr with + | RBop (_, _, _, dst) -> dst_dep dst + | RBload (_, _, _, _, dst) -> dst_dep dst + | RBstore (_, _, _, _, _) -> ( + match next_store (i + 1) (drop (i + 1) instrs) with + | None -> dfg + | Some i' -> DFG.add_edge dfg (gen_vertex instrs i) (gen_vertex instrs i') ) + | _ -> dfg + +let accumulate_WAR_deps instrs dfg curri = + let i, curr = curri in + let dst_dep dst = + let dep_list = find_all_next_dst_read i dst 0 (take i instrs |> List.rev) + |> List.map (function (d, d') -> (i - d' - 1, d)) + in + List.fold_left (fun g -> + function (d, d') -> DFG.add_edge g (gen_vertex instrs d) (gen_vertex instrs d')) dfg dep_list + in + match curr with + | RBop (_, _, _, dst) -> dst_dep dst + | RBload (_, _, _, _, dst) -> dst_dep dst + | _ -> dfg + +let assigned_vars vars = function + | RBnop -> vars + | RBop (_, _, _, dst) -> dst :: vars + | RBload (_, _, _, _, dst) -> dst :: vars + | RBstore (_, _, _, _, _) -> vars + | RBsetpred (_, _, _) -> vars + +let get_pred = function + | RBnop -> None + | RBop (op, _, _, _) -> op + | RBload (op, _, _, _, _) -> op + | RBstore (op, _, _, _, _) -> op + | RBsetpred (_, _, _) -> None + +let independant_pred p p' = + match sat_pred_temp (Nat.of_int 100000) (Pand (p, p')) with + | Some None -> true + | _ -> false + +let check_dependent op1 op2 = + match op1, op2 with + | Some p, Some p' -> not (independant_pred p p') + | _, _ -> true + +let remove_unnecessary_deps graph = + let is_dependent v1 v2 g = + let (_, instr1) = v1 in + let (_, instr2) = v2 in + if check_dependent (get_pred instr1) (get_pred instr2) + then g + else DFG.remove_edge g v1 v2 + in + DFG.fold_edges is_dependent graph graph + +(** All the nodes in the DFG have to come after the source of the basic block, and should terminate + before the sink of the basic block. After that, there should be constraints for data + dependencies between nodes. *) +let gather_bb_constraints debug bb = + let ibody = List.mapi (fun i a -> (i, a)) bb.bb_body in + let dfg = List.fold_left (fun dfg v -> DFG.add_vertex dfg v) DFG.empty ibody in + let _, _, dfg' = + List.fold_left (accumulate_RAW_deps ibody) + (0, PTree.empty, dfg) + bb.bb_body + in + let dfg'' = List.fold_left (fun dfg f -> List.fold_left (f bb.bb_body) dfg ibody) dfg' + [ accumulate_WAW_deps; + accumulate_WAR_deps; + accumulate_RAW_mem_deps; + accumulate_WAR_mem_deps; + accumulate_WAW_mem_deps; + accumulate_RAW_pred_deps; + accumulate_WAR_pred_deps; + accumulate_WAW_pred_deps + ] + in + let dfg''' = remove_unnecessary_deps dfg'' in + (List.length bb.bb_body, dfg''', successors_instr bb.bb_exit) + +let encode_var bbn n i = { sv_type = VarType (bbn, n); sv_num = i } +let encode_bb bbn i = { sv_type = BBType bbn; sv_num = i } + +let add_super_nodes n dfg = + DFG.fold_vertex (function v1 -> fun g -> + (if DFG.in_degree dfg v1 = 0 + then G.add_edge_e g (encode_bb n 0, 0, encode_var n (fst v1) 0) + else g) |> + (fun g' -> + if DFG.out_degree dfg v1 = 0 + then G.add_edge_e g' (encode_var n (fst v1) 0, 0, encode_bb n 1) + else g')) dfg + +let add_data_deps n = + DFG.fold_edges_e (function ((i1, _), l, (i2, _)) -> fun g -> + G.add_edge_e g (encode_var n i1 0, 0, encode_var n i2 0) + ) + +let add_ctrl_deps n succs constr = + List.fold_left (fun g n' -> + G.add_edge_e g (encode_bb n 1, -1, encode_bb n' 0) + ) constr succs + +module BFDFG = Graph.Path.BellmanFord(DFG)(struct + include DFG + type t = int + let weight = DFG.E.label + let compare = compare + let add = (+) + let zero = 0 + end) + +module TopoDFG = Graph.Topological.Make(DFG) + +let negate_graph constr = + DFG.fold_edges_e (function (v1, e, v2) -> fun g -> + DFG.add_edge_e g (v1, -e, v2) + ) constr DFG.empty + +let add_cycle_constr max n dfg constr = + let negated_dfg = negate_graph dfg in + let longest_path v = BFDFG.all_shortest_paths negated_dfg v + |> BFDFG.H.to_seq |> List.of_seq in + let constrained_paths = List.filter (function (v, m) -> - m > max) in + List.fold_left (fun g -> function (v, v', w) -> + G.add_edge_e g (encode_var n (fst v) 0, + - (int_of_float (Float.ceil (Float.div (float_of_int w) (float_of_int max))) - 1), + encode_var n (fst v') 0) + ) constr (DFG.fold_vertex (fun v l -> + List.append l (longest_path v |> constrained_paths + |> List.map (function (v', w) -> (v, v', - w))) + ) dfg []) + +type resource = + | Mem + | SDiv + | UDiv + +type resources = { + res_mem: DFG.V.t list; + res_udiv: DFG.V.t list; + res_sdiv: DFG.V.t list; +} + +let find_resource = function + | RBload _ -> Some Mem + | RBstore _ -> Some Mem + | RBop (_, op, _, _) -> + ( match op with + | Odiv -> Some SDiv + | Odivu -> Some UDiv + | Omod -> Some SDiv + | Omodu -> Some UDiv + | _ -> None ) + | _ -> None + +let add_resource_constr n dfg constr = + let res = TopoDFG.fold (function (i, instr) -> + function {res_mem = ml; res_sdiv = sdl; res_udiv = udl} as r -> + match find_resource instr with + | Some SDiv -> {r with res_sdiv = (i, instr) :: sdl} + | Some UDiv -> {r with res_udiv = (i, instr) :: udl} + | Some Mem -> {r with res_mem = (i, instr) :: ml} + | None -> r + ) dfg {res_mem = []; res_sdiv = []; res_udiv = []} + in + let get_constraints l g = List.fold_left (fun gv v' -> + match gv with + | (g, None) -> (g, Some v') + | (g, Some v) -> + (G.add_edge_e g (encode_var n (fst v) 0, -1, encode_var n (fst v') 0), Some v') + ) (g, None) l |> fst + in + get_constraints (List.rev res.res_mem) constr + |> get_constraints (List.rev res.res_udiv) + |> get_constraints (List.rev res.res_sdiv) + +let gather_cfg_constraints c constr curr = + let (n, dfg) = curr in + match PTree.get (P.of_int n) c with + | None -> assert false + | Some { bb_exit = ctrl; _ } -> + add_super_nodes n dfg constr + |> add_data_deps n dfg + |> add_ctrl_deps n (successors_instr ctrl + |> List.map P.to_int + |> List.filter (fun n' -> n' < n)) + |> add_cycle_constr 8 n dfg + |> add_resource_constr n dfg + +let rec intersperse s = function + | [] -> [] + | [ a ] -> [ a ] + | x :: xs -> x :: s :: intersperse s xs + +let print_objective constr = + let vars = G.fold_vertex (fun v1 l -> + match v1 with + | { sv_type = VarType _; sv_num = 0 } -> print_sv v1 :: l + | _ -> l + ) constr [] + in + "min: " ^ String.concat "" (intersperse " + " vars) ^ ";\n" + +let print_lp constr = + print_objective constr ^ + (G.fold_edges_e (function (e1, w, e2) -> fun s -> + s ^ sprintf "%s - %s <= %d;\n" (print_sv e1) (print_sv e2) w + ) constr "" |> + G.fold_vertex (fun v1 s -> + s ^ sprintf "int %s;\n" (print_sv v1) + ) constr) + +let update_schedule v = function Some l -> Some (v :: l) | None -> Some [ v ] + +let parse_soln tree s = + let r = Str.regexp "var\\([0-9]+\\)n\\([0-9]+\\)_0[ ]+\\([0-9]+\\)" in + if Str.string_match r s 0 then + IMap.update + (Str.matched_group 1 s |> int_of_string) + (update_schedule + ( Str.matched_group 2 s |> int_of_string, + Str.matched_group 3 s |> int_of_string )) + tree + else tree + +let solve_constraints constr = + let oc = open_out "lpsolve.txt" in + fprintf oc "%s\n" (print_lp constr); + close_out oc; + + Str.split (Str.regexp_string "\n") (read_process "lp_solve lpsolve.txt") + |> drop 3 + |> List.fold_left parse_soln IMap.empty + +let subgraph dfg l = + let dfg' = List.fold_left (fun g v -> DFG.add_vertex g v) DFG.empty l in + List.fold_left (fun g v -> + List.fold_left (fun g' v' -> + let edges = DFG.find_all_edges dfg v v' in + List.fold_left (fun g'' e -> + DFG.add_edge_e g'' e + ) g' edges + ) g l + ) dfg' l + +let rec all_successors dfg v = + List.concat (List.fold_left (fun l v -> + all_successors dfg v :: l + ) [] (DFG.succ dfg v)) + +let order_instr dfg = + DFG.fold_vertex (fun v li -> + if DFG.in_degree dfg v = 0 + then (List.map snd (v :: all_successors dfg v)) :: li + else li + ) dfg [] + +let combine_bb_schedule schedule s = + let i, st = s in + IMap.update st (update_schedule i) schedule + +(** Should generate the [RTLPar] code based on the input [RTLBlock] description. *) +let transf_rtlpar c c' (schedule : (int * int) list IMap.t) = + let f i bb : RTLPar.bblock = + match bb with + | { bb_body = []; bb_exit = c } -> { bb_body = []; bb_exit = c } + | { bb_body = bb_body'; bb_exit = ctrl_flow } -> + let dfg = match PTree.get i c' with None -> assert false | Some x -> x in + let i_sched = IMap.find (P.to_int i) schedule in + let i_sched_tree = + List.fold_left combine_bb_schedule IMap.empty i_sched + in + let body = IMap.to_seq i_sched_tree |> List.of_seq |> List.map snd + |> List.map (List.map (fun x -> (x, List.nth bb_body' x))) + in + (*let final_body = List.map (fun x -> subgraph dfg x |> order_instr) body in*) + let final_body2 = List.map (fun x -> subgraph dfg x + |> (fun x -> TopoDFG.fold (fun i l -> snd i :: l) x []) + |> List.rev) body + in + { bb_body = List.map (fun x -> [x]) final_body2; + bb_exit = ctrl_flow + } + in + PTree.map f c + +let schedule entry (c : RTLBlock.bb RTLBlockInstr.code) = + let debug = true in + let transf_graph (_, dfg, _) = dfg in + let c' = PTree.map1 (fun x -> gather_bb_constraints false x |> transf_graph) c in + (*let _ = if debug then PTree.map (fun r o -> printf "##### %d #####\n%a\n\n" (P.to_int r) print_dfg (second o)) c' else PTree.empty in*) + let cgraph = PTree.elements c' + |> List.map (function (x, y) -> (P.to_int x, y)) + |> List.fold_left (gather_cfg_constraints c) G.empty + in + let graph = open_out "constr_graph.dot" in + fprintf graph "%a\n" GDot.output_graph cgraph; + close_out graph; + let schedule' = solve_constraints cgraph in + (**IMap.iter (fun a b -> printf "##### %d #####\n%a\n\n" a (print_list print_tuple) b) schedule';*) + (*printf "Schedule: %a\n" (fun a x -> IMap.iter (fun d -> fprintf a "%d: %a\n" d (print_list print_tuple)) x) schedule';*) + transf_rtlpar c c' schedule' + +let rec find_reachable_states c e = + match PTree.get e c with + | Some { bb_exit = ex; _ } -> + e :: List.fold_left (fun x a -> List.concat [x; find_reachable_states c a]) [] + (successors_instr ex |> List.filter (fun x -> P.lt x e)) + | None -> assert false + +let add_to_tree c nt i = + match PTree.get i c with + | Some p -> PTree.set i p nt + | None -> assert false + +let schedule_fn (f : RTLBlock.coq_function) : RTLPar.coq_function = + let scheduled = schedule f.fn_entrypoint f.fn_code in + let reachable = find_reachable_states scheduled f.fn_entrypoint + |> List.to_seq |> SS.of_seq |> SS.to_seq |> List.of_seq in + { fn_sig = f.fn_sig; + fn_params = f.fn_params; + fn_stacksize = f.fn_stacksize; + fn_code = List.fold_left (add_to_tree scheduled) PTree.empty reachable; + fn_entrypoint = f.fn_entrypoint + } -- cgit From ab1e748f622f4345a3fc13ebbdbc8f223bd10e5c Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Wed, 29 Sep 2021 17:11:34 +0100 Subject: Make all OCaml files compile Reverted commit to get back the scheduling and pretty printing files. --- src/hls/PrintRTLBlockInstr.ml | 2 +- src/hls/Schedule.ml | 6 +++--- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/src/hls/PrintRTLBlockInstr.ml b/src/hls/PrintRTLBlockInstr.ml index ba7241b..979ca38 100644 --- a/src/hls/PrintRTLBlockInstr.ml +++ b/src/hls/PrintRTLBlockInstr.ml @@ -10,7 +10,7 @@ let reg pp r = fprintf pp "x%d" (P.to_int r) let pred pp r = - fprintf pp "p%d" (Nat.to_int r) + fprintf pp "p%d" (P.to_int r) let rec regs pp = function | [] -> () diff --git a/src/hls/Schedule.ml b/src/hls/Schedule.ml index c6c8bf4..7756181 100644 --- a/src/hls/Schedule.ml +++ b/src/hls/Schedule.ml @@ -88,7 +88,7 @@ end)(struct end) let reg r = sprintf "r%d" (P.to_int r) -let print_pred r = sprintf "p%d" (Nat.to_int r) +let print_pred r = sprintf "p%d" (P.to_int r) let print_instr = function | RBnop -> "" @@ -400,7 +400,7 @@ let accumulate_WAW_mem_deps instrs dfg curri = let rec in_predicate p p' = match p' with - | Pvar p'' -> Nat.to_int p = Nat.to_int p'' + | Pvar p'' -> P.to_int p = P.to_int p'' | Pnot p'' -> in_predicate p p'' | Pand (p1, p2) -> in_predicate p p1 || in_predicate p p2 | Por (p1, p2) -> in_predicate p p1 || in_predicate p p2 @@ -509,7 +509,7 @@ let get_pred = function | RBsetpred (_, _, _) -> None let independant_pred p p' = - match sat_pred_temp (Nat.of_int 100000) (Pand (p, p')) with + match sat_pred_simple (Nat.of_int 100000) (Pand (p, p')) with | Some None -> true | _ -> false -- cgit From e7679bd745ddd7362524676465314dfef3257458 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Thu, 30 Sep 2021 09:35:37 +0100 Subject: Add back scheduling to the driver --- driver/VericertDriver.ml | 2 +- test/test_all.sh | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/driver/VericertDriver.ml b/driver/VericertDriver.ml index aa5309a..0706d79 100644 --- a/driver/VericertDriver.ml +++ b/driver/VericertDriver.ml @@ -93,7 +93,7 @@ let compile_c_file sourcename ifile ofile = end else begin let verilog = let translation = if !option_hls_schedule - then Vericert.Compiler0.transf_hls + then Vericert.Compiler0.transf_hls_temp else Vericert.Compiler0.transf_hls in match translation csyntax with diff --git a/test/test_all.sh b/test/test_all.sh index f072eba..2d78890 100755 --- a/test/test_all.sh +++ b/test/test_all.sh @@ -31,7 +31,7 @@ for cfile in $test_dir/*.c; do gcc -o $outbase.gcc $cfile >/dev/null 2>&1 $outbase.gcc expected=$? - vericert -drtl -o $outbase.v $cfile >/dev/null 2>&1 + vericert -fschedule -drtl -o $outbase.v $cfile >/dev/null 2>&1 if [[ ! -f $outbase.v ]]; then echo "ERROR" continue -- cgit From 545d7e40b40a990d1945984ca70c750f18712131 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Fri, 1 Oct 2021 14:15:36 +0100 Subject: Fix scheduler for operation chaining --- src/hls/Schedule.ml | 30 ++++++++++++++++++++++-------- 1 file changed, 22 insertions(+), 8 deletions(-) diff --git a/src/hls/Schedule.ml b/src/hls/Schedule.ml index 7756181..26cd382 100644 --- a/src/hls/Schedule.ml +++ b/src/hls/Schedule.ml @@ -203,6 +203,8 @@ module DFGDot = Graph.Graphviz.Dot(struct include DFG end) +module DFGDfs = Graph.Traverse.Dfs(DFG) + module IMap = Map.Make (struct type t = int @@ -713,9 +715,7 @@ let subgraph dfg l = List.fold_left (fun g v -> List.fold_left (fun g' v' -> let edges = DFG.find_all_edges dfg v v' in - List.fold_left (fun g'' e -> - DFG.add_edge_e g'' e - ) g' edges + List.fold_left DFG.add_edge_e g' edges ) g l ) dfg' l @@ -735,6 +735,15 @@ let combine_bb_schedule schedule s = let i, st = s in IMap.update st (update_schedule i) schedule +(**let add_el dfg i l = + List.*) + +let all_dfs dfg = + let roots = DFG.fold_vertex (fun v li -> + if DFG.in_degree dfg v = 0 then v :: li else li + ) dfg [] in + List.map (fun r -> DFGDfs.fold_component (fun v l -> v :: l) [] dfg r) roots + (** Should generate the [RTLPar] code based on the input [RTLBlock] description. *) let transf_rtlpar c c' (schedule : (int * int) list IMap.t) = let f i bb : RTLPar.bblock = @@ -750,11 +759,16 @@ let transf_rtlpar c c' (schedule : (int * int) list IMap.t) = |> List.map (List.map (fun x -> (x, List.nth bb_body' x))) in (*let final_body = List.map (fun x -> subgraph dfg x |> order_instr) body in*) + Printf.printf "%a\n" print_dfg (subgraph dfg (List.hd body)); let final_body2 = List.map (fun x -> subgraph dfg x - |> (fun x -> TopoDFG.fold (fun i l -> snd i :: l) x []) - |> List.rev) body + |> (fun x -> + all_dfs x + |> List.map (subgraph x) + |> List.map (fun y -> + TopoDFG.fold (fun i l -> snd i :: l) y [] + |> List.rev))) body in - { bb_body = List.map (fun x -> [x]) final_body2; + { bb_body = final_body2; bb_exit = ctrl_flow } in @@ -764,7 +778,7 @@ let schedule entry (c : RTLBlock.bb RTLBlockInstr.code) = let debug = true in let transf_graph (_, dfg, _) = dfg in let c' = PTree.map1 (fun x -> gather_bb_constraints false x |> transf_graph) c in - (*let _ = if debug then PTree.map (fun r o -> printf "##### %d #####\n%a\n\n" (P.to_int r) print_dfg (second o)) c' else PTree.empty in*) + (*let _ = if debug then PTree.map (fun r o -> printf "##### %d #####\n%a\n\n" (P.to_int r) print_dfg o) c' else PTree.empty in*) let cgraph = PTree.elements c' |> List.map (function (x, y) -> (P.to_int x, y)) |> List.fold_left (gather_cfg_constraints c) G.empty @@ -774,7 +788,7 @@ let schedule entry (c : RTLBlock.bb RTLBlockInstr.code) = close_out graph; let schedule' = solve_constraints cgraph in (**IMap.iter (fun a b -> printf "##### %d #####\n%a\n\n" a (print_list print_tuple) b) schedule';*) - (*printf "Schedule: %a\n" (fun a x -> IMap.iter (fun d -> fprintf a "%d: %a\n" d (print_list print_tuple)) x) schedule';*) + (**printf "Schedule: %a\n" (fun a x -> IMap.iter (fun d -> fprintf a "%d: %a\n" d (print_list print_tuple)) x) schedule';*) transf_rtlpar c c' schedule' let rec find_reachable_states c e = -- 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(-) 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 23c700b5fb35fb00d994cb66e4597fe8ea0b28e1 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Fri, 1 Oct 2021 14:16:31 +0100 Subject: Fix compilation of new intermediate languages --- default.nix | 11 ++++++----- driver/VericertDriver.ml | 3 +++ src/Compiler.v | 13 ++++++++----- src/VericertClflags.ml | 1 + src/extraction/Extraction.v | 1 + src/hls/PrintHTL.ml | 4 ++-- 6 files changed, 21 insertions(+), 12 deletions(-) diff --git a/default.nix b/default.nix index fa60637..0e5b40d 100644 --- a/default.nix +++ b/default.nix @@ -9,11 +9,12 @@ stdenv.mkDerivation { buildInputs = [ ncoq dune_2 gcc ncoq.ocaml ncoq.ocamlPackages.findlib ncoq.ocamlPackages.menhir - ncoq.ocamlPackages.ocamlgraph - ncoqPackages.serapi - python3 python3Packages.docutils python3Packages.pygments - python3Packages.dominate - python3Packages.pelican + ncoq.ocamlPackages.ocamlgraph ncoq.ocamlPackages.merlin + + ncoqPackages.serapi + python3 python3Packages.docutils python3Packages.pygments + python3Packages.dominate + python3Packages.pelican ]; enableParallelBuilding = true; diff --git a/driver/VericertDriver.ml b/driver/VericertDriver.ml index 0706d79..a36f375 100644 --- a/driver/VericertDriver.ml +++ b/driver/VericertDriver.ml @@ -66,6 +66,7 @@ let compile_c_file sourcename ifile ofile = set_dest Vericert.PrintCminor.destination option_dcminor ".cm"; set_dest Vericert.PrintRTL.destination option_drtl ".rtl"; set_dest Vericert.PrintRTLBlock.destination option_drtlblock ".rtlblock"; + set_dest Vericert.PrintRTLPar.destination option_drtlpar ".rtlpar"; set_dest Vericert.PrintHTL.destination option_dhtl ".htl"; set_dest Vericert.Regalloc.destination_alloctrace option_dalloctrace ".alloctrace"; set_dest Vericert.PrintLTL.destination option_dltl ".ltl"; @@ -391,6 +392,7 @@ let cmdline_actions = Exact "-dcminor", Set option_dcminor; Exact "-drtl", Set option_drtl; Exact "-drtlblock", Set option_drtlblock; + Exact "-drtlpar", Set option_drtlpar; Exact "-dhtl", Set option_dhtl; Exact "-dltl", Set option_dltl; Exact "-dalloctrace", Set option_dalloctrace; @@ -404,6 +406,7 @@ let cmdline_actions = option_dcminor := true; option_drtl := true; option_drtlblock := true; + option_drtlpar := true; option_dhtl := true; option_dltl := true; option_dalloctrace := true; diff --git a/src/Compiler.v b/src/Compiler.v index 268f451..ecea2fc 100644 --- a/src/Compiler.v +++ b/src/Compiler.v @@ -81,8 +81,9 @@ We then need to declare the external OCaml functions used to print out intermedi |*) Parameter print_RTL: Z -> RTL.program -> unit. -Parameter print_HTL: HTL.program -> unit. +Parameter print_HTL: Z -> HTL.program -> unit. Parameter print_RTLBlock: Z -> RTLBlock.program -> unit. +Parameter print_RTLPar: Z -> RTLPar.program -> unit. Definition print {A: Type} (printer: A -> unit) (prog: A) : A := let unused := printer prog in prog. @@ -191,8 +192,9 @@ Definition transf_backend (r : RTL.program) : res Verilog.program := @@@ time "Unused globals" Unusedglob.transform_program @@ print (print_RTL 7) @@@ HTLgen.transl_program - @@ print print_HTL + @@ print (print_HTL 0) @@ total_if HLSOpts.optim_ram Memorygen.transf_program + @@ print (print_HTL 1) @@ Veriloggen.transl_program. (*| @@ -239,12 +241,13 @@ Definition transf_hls_temp (p : Csyntax.program) : res Verilog.program := @@@ time "Unused globals" Unusedglob.transform_program @@ print (print_RTL 7) @@@ RTLBlockgen.transl_program - @@ print (print_RTLBlock 1) + @@ print (print_RTLBlock 0) @@ total_if HLSOpts.optim_if_conversion IfConversion.transf_program - @@ print (print_RTLBlock 2) + @@ print (print_RTLBlock 1) @@@ RTLPargen.transl_program + @@ print (print_RTLPar 0) @@@ HTLPargen.transl_program - @@ print print_HTL + @@ print (print_HTL 0) @@ Veriloggen.transl_program. (*| diff --git a/src/VericertClflags.ml b/src/VericertClflags.ml index 977ca00..ab3c949 100644 --- a/src/VericertClflags.ml +++ b/src/VericertClflags.ml @@ -5,6 +5,7 @@ let option_debug_hls = ref false let option_initial = ref false let option_dhtl = ref false let option_drtlblock = ref false +let option_drtlpar = ref false let option_hls_schedule = ref false let option_fif_conv = ref false let option_fram = ref true diff --git a/src/extraction/Extraction.v b/src/extraction/Extraction.v index 6bbfc05..97f0d2a 100644 --- a/src/extraction/Extraction.v +++ b/src/extraction/Extraction.v @@ -144,6 +144,7 @@ Extract Constant driver.Compiler.print_RTL => "PrintRTL.print_if". Extract Constant Compiler.print_RTL => "PrintRTL.print_if". Extract Constant Compiler.print_RTLBlock => "PrintRTLBlock.print_if". Extract Constant Compiler.print_HTL => "PrintHTL.print_if". +Extract Constant Compiler.print_RTLPar => "PrintRTLPar.print_if". Extract Constant Compiler.print_LTL => "PrintLTL.print_if". Extract Constant Compiler.print_Mach => "PrintMach.print_if". Extract Constant Compiler.print => "fun (f: 'a -> unit) (x: 'a) -> f x; x". diff --git a/src/hls/PrintHTL.ml b/src/hls/PrintHTL.ml index a75d0ee..5963be0 100644 --- a/src/hls/PrintHTL.ml +++ b/src/hls/PrintHTL.ml @@ -71,10 +71,10 @@ let print_program pp prog = let destination : string option ref = ref None -let print_if prog = +let print_if passno prog = match !destination with | None -> () | Some f -> - let oc = open_out f in + let oc = open_out (f ^ "." ^ Z.to_string passno) in print_program oc prog; close_out oc -- cgit From c689bcc4eaaaf052ecb35539dff653185192b5e9 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Fri, 1 Oct 2021 14:16:52 +0100 Subject: Add printers for expressions and RTLPar --- src/hls/PrintExpression.ml | 40 +++++++++++++++++++++++++ src/hls/PrintRTLPar.ml | 74 ++++++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 114 insertions(+) create mode 100644 src/hls/PrintExpression.ml create mode 100644 src/hls/PrintRTLPar.ml diff --git a/src/hls/PrintExpression.ml b/src/hls/PrintExpression.ml new file mode 100644 index 0000000..cfe6750 --- /dev/null +++ b/src/hls/PrintExpression.ml @@ -0,0 +1,40 @@ +(*open Printf +open Camlcoq +open Datatypes +open Maps +open PrintAST +open RTLPargen + +let reg pp r = + fprintf pp "x%d" (P.to_int r) + +let pred pp r = + fprintf pp "p%d" (P.to_int r) + +let print_resource pp = function + | Reg r -> reg pp r + | Pred r -> pred pp r + | Mem -> fprintf pp "M" + +let rec to_expr_list = function + | Enil -> [] + | Econs (e, elist) -> e :: to_expr_list elist + +let rec print_expression pp = function + | Ebase r -> print_resource pp r + | Eop (op, elist, e) -> + PrintOp.print_operation print_expression pp (op, to_expr_list elist); + Printf.printf "; "; + print_expression pp e + | Eload (chunk, addr, elist, e) -> + fprintf pp "%s[%a]; " (name_of_chunk chunk) (PrintOp.print_addressing print_expression) (addr, to_expr_list elist); + print_expression pp e + | Estore (e, chunk, addr, elist, e') -> + fprintf pp "%s[%a] = %a; " (name_of_chunk chunk) + (PrintOp.print_addressing print_expression) (addr, to_expr_list elist) + print_expression e; + print_expression pp e + | Esetpred (p, cond, elist, e) -> + fprintf pp "%a = %a; " pred p (PrintOp.print_condition print_expression) (cond, to_expr_list elist); + print_expression pp e +*) diff --git a/src/hls/PrintRTLPar.ml b/src/hls/PrintRTLPar.ml new file mode 100644 index 0000000..ab93fa5 --- /dev/null +++ b/src/hls/PrintRTLPar.ml @@ -0,0 +1,74 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + +(** Pretty-printers for RTL code *) + +open Printf +open Camlcoq +open Datatypes +open Maps +open AST +open RTLBlockInstr +open RTLPar +open PrintAST +open PrintRTLBlockInstr + +(* Printing of RTL code *) + +let reg pp r = + fprintf pp "x%d" (P.to_int r) + +let rec regs pp = function + | [] -> () + | [r] -> reg pp r + | r1::rl -> fprintf pp "%a, %a" reg r1 regs rl + +let ros pp = function + | Coq_inl r -> reg pp r + | Coq_inr s -> fprintf pp "\"%s\"" (extern_atom s) + +let print_bblock pp (pc, i) = + fprintf pp "%5d:{\n" pc; + List.iter (fun x -> fprintf pp "{\n"; + List.iter (fun x -> fprintf pp "( "; List.iter (print_bblock_body pp) x; fprintf pp " )") x; + fprintf pp "}\n") i.bb_body; + print_bblock_exit pp i.bb_exit; + fprintf pp "\t}\n\n" + +let print_function pp id f = + fprintf pp "%s(%a) {\n" (extern_atom id) regs f.fn_params; + let instrs = + List.sort + (fun (pc1, _) (pc2, _) -> compare pc2 pc1) + (List.rev_map + (fun (pc, i) -> (P.to_int pc, i)) + (PTree.elements f.fn_code)) in + List.iter (print_bblock pp) instrs; + fprintf pp "}\n\n" + +let print_globdef pp (id, gd) = + match gd with + | Gfun(Internal f) -> print_function pp id f + | _ -> () + +let print_program pp (prog: program) = + List.iter (print_globdef pp) prog.prog_defs + +let destination : string option ref = ref None + +let print_if passno prog = + match !destination with + | None -> () + | Some f -> + let oc = open_out (f ^ "." ^ Z.to_string passno) in + print_program oc prog; + close_out oc -- 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 ++---- src/hls/Schedule.ml | 1 - 2 files changed, 2 insertions(+), 5 deletions(-) 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 := diff --git a/src/hls/Schedule.ml b/src/hls/Schedule.ml index 26cd382..1052cb3 100644 --- a/src/hls/Schedule.ml +++ b/src/hls/Schedule.ml @@ -759,7 +759,6 @@ let transf_rtlpar c c' (schedule : (int * int) list IMap.t) = |> List.map (List.map (fun x -> (x, List.nth bb_body' x))) in (*let final_body = List.map (fun x -> subgraph dfg x |> order_instr) body in*) - Printf.printf "%a\n" print_dfg (subgraph dfg (List.hd body)); let final_body2 = List.map (fun x -> subgraph dfg x |> (fun x -> all_dfs x -- cgit