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