diff options
Diffstat (limited to 'src/hls')
-rw-r--r-- | src/hls/Abstr.v | 47 | ||||
-rw-r--r-- | src/hls/GiblePargen.v | 46 | ||||
-rw-r--r-- | src/hls/GiblePargenproof.v | 26 |
3 files changed, 63 insertions, 56 deletions
diff --git a/src/hls/Abstr.v b/src/hls/Abstr.v index 9992b1c..3001123 100644 --- a/src/hls/Abstr.v +++ b/src/hls/Abstr.v @@ -53,7 +53,8 @@ Definition reg := positive. Inductive resource : Set := | Reg : reg -> resource | Pred : reg -> resource -| Mem : resource. +| Mem : resource +| Exit : resource. (*| The following defines quite a few equality comparisons automatically, however, @@ -79,7 +80,8 @@ Module R_indexed. match rs with | Reg r => xO (xO r) | Pred r => xI (xI r) - | Mem => 1%positive + | Mem => 1 + | Exit => 2 end. Lemma index_inj: forall (x y: t), index x = index y -> x = y. @@ -110,6 +112,7 @@ 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 : Op.condition -> expression_list -> expression +| Eexit : cf_instr -> expression with expression_list : Type := | Enil : expression_list | Econs : expression -> expression_list -> expression_list @@ -303,6 +306,13 @@ with sem_mem : ctx -> expression -> Memory.mem -> Prop := | Sbase_mem : forall ctx, sem_mem ctx (Ebase Mem) (ctx_mem ctx) +with sem_exit : ctx -> expression -> option cf_instr -> Prop := +| Sexit : + forall ctx cf, + sem_exit ctx (Eexit cf) (Some cf) +| Sbase_exit : + forall ctx, + sem_exit ctx (Ebase Exit) None with sem_val_list : ctx -> expression_list -> list val -> Prop := | Snil : forall ctx, @@ -351,13 +361,14 @@ Inductive sem_regset : ctx -> forest -> regset -> Prop := (forall x, sem_pred_expr sem_value ctx (f # (Reg x)) (rs' !! x)) -> sem_regset ctx f rs'. -Inductive sem : ctx -> forest -> instr_state -> Prop := +Inductive sem : ctx -> forest -> instr_state * cf_instr -> Prop := | Sem: - forall ctx rs' m' f pr', + forall ctx rs' m' f pr' cf, sem_regset ctx f rs' -> sem_predset ctx f pr' -> sem_pred_expr sem_mem ctx (f # Mem) m' -> - sem ctx f (mk_instr_state rs' pr' m'). + sem_pred_expr sem_exit ctx (f # Exit) (Some cf) -> + sem ctx f (mk_instr_state rs' pr' m', cf). End SEMANTICS. @@ -381,6 +392,7 @@ Fixpoint beq_expression (e1 e2: expression) {struct e1}: bool := | Esetpred c1 el1, Esetpred c2 el2 => if condition_eq c1 c2 then beq_expression_list el1 el2 else false + | Eexit cf1, Eexit cf2 => if cf_instr_eq cf1 cf2 then true else false | _, _ => false end with beq_expression_list (el1 el2: expression_list) {struct el1} : bool := @@ -440,6 +452,7 @@ Proof. unfold not in *; intros. inv H0. rewrite beq_expression_list_refl in H; crush. - simplify. repeat (destruct_match; crush); subst. - simplify. repeat (destruct_match; crush); subst. + - simplify. repeat (destruct_match; crush); subst. apply andb_false_iff in H. inv H. unfold not in *; intros. inv H. rewrite beq_expression_refl in H0; discriminate. unfold not in *; intros. inv H. rewrite beq_expression_list_refl in H0; discriminate. @@ -900,6 +913,8 @@ Section CORRECT. unfold ctx_rs, ctx_ps, ctx_mem in *; cbn in *. inv H; crush. - inv H0. - inv H0. + - inv H0. + - inv H0. - inv H0. econstructor. - inv H0. eapply IHe in H6; auto. eapply IHe0 in H8. econstructor; eassumption. @@ -1185,7 +1200,7 @@ Section CORRECT. check fa fb = true -> sem ictx fa i -> sem octx fb i' -> - match_states i i'. + match_states (fst i) (fst i') /\ snd i = snd i'. Proof using HSIM. intros. unfold check, get_forest in *; intros; @@ -1200,18 +1215,14 @@ Section CORRECT. | H: forall _ : Rtree.elt, _ |- _ => specialize (H (Reg x)) end. repeat (destruct_match; try contradiction). - unfold "#" in *. rewrite Heqo in H0. - rewrite Heqo0 in H1. admit. - unfold "#" in H1. rewrite Heqo0 in H1. - unfold "#" in H0. rewrite Heqo in H0. admit. - } + unfold "#" in *. Admitted. Lemma check_correct2: forall (fa fb : forest) i, check fa fb = true -> sem ictx fa i -> - exists i', sem octx fb i' /\ match_states i i'. + exists i', sem octx fb i' /\ match_states (fst i) (fst i') /\ snd i = snd i'. Proof. Admitted. End CORRECT. @@ -1311,22 +1322,22 @@ End BOOLEAN_EQUALITY. Lemma map1: forall w dst dst', - dst <> dst' -> - (empty # dst <- w) # dst' = NE.singleton (T, Ebase dst'). + dst <> dst' -> + (empty # dst <- w) # dst' = NE.singleton (T, Ebase dst'). Proof. intros; unfold get_forest; rewrite Rtree.gso; auto; apply get_empty. Qed. Lemma genmap1: forall (f : forest) w dst dst', - dst <> dst' -> - (f # dst <- w) # dst' = f # dst'. + dst <> dst' -> + (f # dst <- w) # dst' = f # dst'. Proof. intros; unfold get_forest; rewrite Rtree.gso; auto. Qed. Lemma map2: forall (v : pred_expr) x rs, - (rs # x <- v) # x = v. + (rs # x <- v) # x = v. Proof. intros; unfold get_forest; rewrite Rtree.gss; trivial. Qed. Lemma tri1: forall x y, - Reg x <> Reg y -> x <> y. + Reg x <> Reg y -> x <> y. Proof. crush. Qed. diff --git a/src/hls/GiblePargen.v b/src/hls/GiblePargen.v index 778e0cd..da0567b 100644 --- a/src/hls/GiblePargen.v +++ b/src/hls/GiblePargen.v @@ -167,8 +167,6 @@ This is done by multiplying the predicates together, and assigning the negation of the expression to the other predicates. |*) -Definition forest_state : Type := forest * list (cf_instr * option pred_op * forest). - Definition upd_pred_forest (p: option pred_op) (f: forest) := match p with | Some p' => @@ -180,39 +178,42 @@ Definition upd_pred_forest (p: option pred_op) (f: forest) := | None => f end. -Definition update (flist : forest_state) (i : instr): forest_state := - let (f, fl) := flist in +Definition update (fop : option pred_op * forest) (i : instr): (option pred_op * forest) := + let (pred, f) := fop in match i with - | RBnop => flist + | RBnop => fop | RBop p op rl r => - (f # (Reg r) <- - (app_predicated p - (f # (Reg r)) - (map_predicated (pred_ret (Eop op)) (merge (list_translation rl f)))), fl) + (pred, f # (Reg r) <- + (app_predicated (combine_pred p pred) + (f # (Reg r)) + (map_predicated (pred_ret (Eop op)) (merge (list_translation rl f))))) | RBload p chunk addr rl r => - (f # (Reg r) <- - (app_predicated p + (pred, f # (Reg r) <- + (app_predicated (combine_pred p pred) (f # (Reg r)) (map_predicated (map_predicated (pred_ret (Eload chunk addr)) (merge (list_translation rl f))) - (f # Mem))), fl) + (f # Mem)))) | RBstore p chunk addr rl r => - (f # Mem <- - (app_predicated p + (pred, f # Mem <- + (app_predicated (combine_pred p pred) (f # Mem) (map_predicated (map_predicated (predicated_apply2 (map_predicated (pred_ret Estore) (f # (Reg r))) chunk addr) - (merge (list_translation rl f))) (f # Mem))), fl) + (merge (list_translation rl f))) (f # Mem)))) | RBsetpred p' c args p => - (f # (Pred p) <- - (app_predicated p' + (pred, f # (Pred p) <- + (app_predicated (combine_pred p' pred) (f # (Pred p)) (map_predicated (pred_ret (Esetpred c)) - (merge (list_translation args f)))), fl) - | RBexit p c => ((upd_pred_forest (option_map negate p) f), (c, p, upd_pred_forest p f) :: fl) + (merge (list_translation args f))))) + | RBexit p c => + (combine_pred (Option.map negate p) pred, + f # Exit <- + (app_predicated (combine_pred p pred) (f # Exit) (pred_ret (Eexit c)))) end. (*| @@ -223,7 +224,7 @@ code than in the RTLBlock code. Get a sequence from the basic block. |*) -Fixpoint abstract_sequence (f : forest_state) (b : list instr) : forest_state := +Fixpoint abstract_sequence (f : option pred_op * forest) (b : list instr) : option pred_op * forest := match b with | nil => f | i :: l => abstract_sequence (update f i) l @@ -254,9 +255,8 @@ Definition empty_trees (bb: SeqBB.t) (bbt: ParBB.t) : bool := end. Definition schedule_oracle (bb: SeqBB.t) (bbt: ParBB.t) : bool := - forallb (fun x => match x with ((_, _, f1), (_, _, f2)) => check f1 f2 end) - (combine (snd (abstract_sequence (empty, nil) bb)) - (snd (abstract_sequence (empty, nil) (concat (concat bbt))))) && + (check (snd (abstract_sequence (None, empty) bb)) + (snd (abstract_sequence (None, empty) (concat (concat bbt))))) && empty_trees bb bbt. Definition check_scheduled_trees := beq2 schedule_oracle. diff --git a/src/hls/GiblePargenproof.v b/src/hls/GiblePargenproof.v index 2abbea4..699a616 100644 --- a/src/hls/GiblePargenproof.v +++ b/src/hls/GiblePargenproof.v @@ -48,21 +48,16 @@ RTLBlock to abstract translation Correctness of translation from RTLBlock to the abstract interpretation language. |*) -(*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. +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. +Definition is_ps i := match i with mk_instr_state _ p _ => p end. Inductive state_lessdef : instr_state -> instr_state -> Prop := state_lessdef_intro : - forall rs1 rs2 m1, - (forall x, rs1 !! x = rs2 !! x) -> - state_lessdef (mk_instr_state rs1 m1) (mk_instr_state rs2 m1). - -Ltac inv_simp := - repeat match goal with - | H: exists _, _ |- _ => inv H - end; simplify. - -*) + forall rs1 rs2 ps1 ps2 m1, + (forall x, rs1 !! x = rs2 !! x) -> + (forall x, ps1 !! x = ps2 !! x) -> + state_lessdef (mk_instr_state rs1 ps1 m1) (mk_instr_state rs2 ps2 m1). Definition check_dest i r' := match i with @@ -89,12 +84,13 @@ Proof. induction l; crush. 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_update : +Lemma check_dest_update : forall f i r, check_dest i r = false -> - (update f i) # (Reg r) = f # (Reg r). + (snd (update f i)) # (Reg r) = (snd f) # (Reg r). Proof. - destruct i; crush; try apply Pos.eqb_neq in H; apply genmap1; crush. + destruct i; crush; try apply Pos.eqb_neq in H; unfold update; destruct_match; crush. + inv Heqp. Qed. Lemma check_dest_l_forall2 : |