From d43f57ea8df27684bd2ad094998655066fdba99c Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Thu, 4 Aug 2022 00:47:46 +0100 Subject: Add back changes to Abstr --- flake.nix | 4 +- src/hls/Abstr.v | 482 +++++++++++++++++++++++++++++++------------------- src/hls/GiblePargen.v | 126 ++++++------- 3 files changed, 364 insertions(+), 248 deletions(-) diff --git a/flake.nix b/flake.nix index 7303d3b..5153395 100644 --- a/flake.nix +++ b/flake.nix @@ -15,7 +15,7 @@ devShell.x86_64-linux = pkgs.mkShell { buildInputs = with pkgs; [ ncoq - dune_2 + dune_3 gcc ncoq.ocaml ncoq.ocamlPackages.findlib @@ -35,7 +35,7 @@ devShell.x86_64-darwin = dpkgs.mkShell { buildInputs = with dpkgs; [ dncoq - dune_2 + dune_3 gcc dncoq.ocaml dncoq.ocamlPackages.findlib diff --git a/src/hls/Abstr.v b/src/hls/Abstr.v index 9c62bde..b129afb 100644 --- a/src/hls/Abstr.v +++ b/src/hls/Abstr.v @@ -133,21 +133,21 @@ with expression_list : Type := | Enil : expression_list | Econs : expression -> expression_list -> expression_list. -Variant pred_expression : Type := - | PEbase : positive -> pred_expression - | PEsetpred : Op.condition -> expression_list -> pred_expression. - Variant exit_expression : Type := | EEbase : exit_expression - | Eexit : cf_instr -> exit_expression. + | EEexit : cf_instr -> exit_expression. Definition pred_op := @Predicate.pred_op positive. Definition predicate := positive. Definition predicated A := NE.non_empty (pred_op * A). +Variant pred_expression : Type := + | PEbase : positive -> pred_expression + | PEsetpred : Op.condition -> expression_list -> pred_expression. + Definition pred_expr := predicated expression. -Definition pred_pexpr := predicated pred_expression. +Definition pred_pexpr := @Predicate.pred_op pred_expression. Definition pred_eexpr := predicated exit_expression. (*| @@ -155,25 +155,46 @@ Using ``IMap`` we can create a map from resources to any other type, as resources can be uniquely identified as positive numbers. |*) -Module Rtree := ITree(R_indexed). +Module RTree := ITree(R_indexed). Record forest : Type := mk_forest { - forest_regs : Rtree.t pred_expr; + forest_regs : RTree.t pred_expr; forest_preds : PTree.t pred_pexpr; forest_exit : pred_eexpr }. +Definition empty : forest := + mk_forest (RTree.empty _) (PTree.empty _) (NE.singleton (Ptrue, EEbase)). + Definition get_forest v (f: forest) := - match Rtree.get v f with + match RTree.get v f.(forest_regs) with | None => NE.singleton (Ptrue, (Ebase v)) | Some v' => v' end. +Definition set_forest r v (f: forest) := + mk_forest (RTree.set r v f.(forest_regs)) f.(forest_preds) f.(forest_exit). + +Definition get_forest_p p (f: forest) := + match PTree.get p f.(forest_preds) with + | None => Plit (true, PEbase p) + | Some v' => v' + end. + +Definition set_forest_p p v (f: forest) := + mk_forest f.(forest_regs) (PTree.set p v f.(forest_preds)) f.(forest_exit). + +Definition set_forest_e e (f: forest) := + mk_forest f.(forest_regs) f.(forest_preds) e. + Declare Scope forest. -Notation "a # b" := (get_forest b a) (at level 1) : forest. -Notation "a # b <- c" := (Rtree.set b c a) (at level 1, b at next level) : forest. +Notation "a '#r' b" := (get_forest b a) (at level 1) : forest. +Notation "a '#r' b <- c" := (set_forest b c a) (at level 1, b at next level) : forest. +Notation "a '#p' b" := (get_forest_p b a) (at level 1) : forest. +Notation "a '#p' b <- c" := (get_forest_p b c a) (at level 1, b at next level) : forest. +Notation "a '<-e' e" := (set_forest_e e a) (at level 1) : forest. #[local] Open Scope forest. @@ -226,15 +247,6 @@ Inductive sem_value : ctx -> expression -> val -> Prop := Op.eval_addressing (ctx_ge ctx) (ctx_sp ctx) addr lv = Some a -> Memory.Mem.loadv chunk m' a = Some v -> sem_value ctx (Eload chunk addr args mexp) v -with sem_pred : ctx -> expression -> bool -> Prop := -| Spred: - forall ctx args c lv v, - sem_val_list ctx args lv -> - Op.eval_condition c lv (ctx_mem ctx) = Some v -> - sem_pred ctx (Esetpred c args) v -| Sbase_pred: - forall ctx p, - sem_pred ctx (Ebase (Pred p)) ((ctx_ps ctx) !! p) with sem_mem : ctx -> expression -> Memory.mem -> Prop := | Sstore : forall ctx mexp vexp chunk addr args lv v a m' m'', @@ -247,13 +259,6 @@ 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, @@ -265,41 +270,73 @@ with sem_val_list : ctx -> expression_list -> list val -> Prop := sem_val_list ctx (Econs e l) (v :: lv) . -Inductive eval_apred (c: ctx): apred_op -> bool -> Prop := -| eval_APtrue : eval_apred c Ptrue true -| eval_APfalse : eval_apred c Pfalse false -| eval_APlit : forall p (b: bool) bres, +Variant sem_exit : ctx -> exit_expression -> option cf_instr -> Prop := +| Sexit : + forall ctx cf, + sem_exit ctx (EEexit cf) (Some cf) +| Sbase_exit : + forall ctx, + sem_exit ctx EEbase None. + +Variant sem_pred : ctx -> pred_expression -> bool -> Prop := +| Spred: + forall ctx args c lv v, + sem_val_list ctx args lv -> + Op.eval_condition c lv (ctx_mem ctx) = Some v -> + sem_pred ctx (PEsetpred c args) v +| Sbase_pred: + forall ctx p, + sem_pred ctx (PEbase p) ((ctx_ps ctx) !! p). + +(*| +I was trying to avoid such rich semantics for pred_pexpr (by not having the type +in the first place), but I think it is needed to model predicates properly. +|*) + +Inductive sem_pexpr (c: ctx) : pred_pexpr -> bool -> Prop := +| sem_pexpr_Ptrue : sem_pexpr c Ptrue true +| sem_pexpr_Pfalse : sem_pexpr c Pfalse false +| sem_pexpr_Plit : forall p (b: bool) bres, sem_pred c p (if b then bres else negb bres) -> - eval_apred c (Plit (b, p)) bres -| eval_APand : forall p1 p2 b1 b2, - eval_apred c p1 b1 -> - eval_apred c p2 b2 -> - eval_apred c (Pand p1 p2) (b1 && b2) -| eval_APor1 : forall p1 p2 b1 b2, - eval_apred c p1 b1 -> - eval_apred c p2 b2 -> - eval_apred c (Por p1 p2) (b1 || b2). - -Inductive sem_pred_expr {B: Type} (sem: ctx -> expression -> B -> Prop): - ctx -> apred_expr -> B -> Prop := + sem_pexpr c (Plit (b, p)) bres +| sem_pexpr_Pand : forall p1 p2 b1 b2, + sem_pexpr c p1 b1 -> + sem_pexpr c p2 b2 -> + sem_pexpr c (Pand p1 p2) (b1 && b2) +| sem_pexpr_Por : forall p1 p2 b1 b2, + sem_pexpr c p1 b1 -> + sem_pexpr c p2 b2 -> + sem_pexpr c (Por p1 p2) (b1 || b2). + +Fixpoint from_pred_op (f: forest) (p: pred_op): pred_pexpr := + match p with + | Ptrue => Ptrue + | Pfalse => Pfalse + | Plit (b, p') => if b then f #p p' else negate (f #p p') + | Pand a b => Pand (from_pred_op f a) (from_pred_op f b) + | Por a b => Por (from_pred_op f a) (from_pred_op f b) + end. + +Inductive sem_pred_expr {A B: Type} (f: forest) (sem: ctx -> A -> B -> Prop): + ctx -> predicated A -> B -> Prop := | sem_pred_expr_cons_true : forall ctx e pr p' v, - eval_apred ctx pr true -> + sem_pexpr ctx (from_pred_op f pr) true -> sem ctx e v -> - sem_pred_expr sem ctx ((pr, e) ::| p') v + sem_pred_expr f sem ctx ((pr, e) ::| p') v | sem_pred_expr_cons_false : forall ctx e pr p' v, - eval_apred ctx pr false -> - sem_pred_expr sem ctx p' v -> - sem_pred_expr sem ctx ((pr, e) ::| p') v + sem_pexpr ctx (from_pred_op f pr) false -> + sem_pred_expr f sem ctx p' v -> + sem_pred_expr f sem ctx ((pr, e) ::| p') v | sem_pred_expr_single : forall ctx e pr v, - eval_apred ctx pr true -> + sem_pexpr ctx (from_pred_op f pr) true -> sem ctx e v -> - sem_pred_expr sem ctx (NE.singleton (pr, e)) v + sem_pred_expr f sem ctx (NE.singleton (pr, e)) v . -Definition collapse_pe (p: apred_expr) : option expression := +Definition collapse_pe (p: pred_expr) : option expression := match p with | NE.singleton (APtrue, p) => Some p | _ => None @@ -307,14 +344,14 @@ Definition collapse_pe (p: apred_expr) : option expression := Inductive sem_predset : ctx -> forest -> predset -> Prop := | Spredset: - forall ctx f rs', - (forall x, sem_pred_expr sem_pred ctx (f # (Pred x)) (rs' !! x)) -> + forall ctx f rs', + (forall x, sem_pexpr ctx (f #p x) (rs' !! x)) -> sem_predset ctx f rs'. Inductive sem_regset : ctx -> forest -> regset -> Prop := | Sregset: - forall ctx f rs', - (forall x, sem_pred_expr sem_value ctx (f # (Reg x)) (rs' !! x)) -> + forall ctx f rs', + (forall x, sem_pred_expr f sem_value ctx (f #r (Reg x)) (rs' !! x)) -> sem_regset ctx f rs'. Inductive sem : ctx -> forest -> instr_state * option cf_instr -> Prop := @@ -322,8 +359,8 @@ Inductive sem : ctx -> forest -> instr_state * option cf_instr -> Prop := 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_pred_expr sem_exit ctx (f # Exit) cf -> + sem_pred_expr f sem_mem ctx (f #r Mem) m' -> + sem_pred_expr f sem_exit ctx f.(forest_exit) cf -> sem ctx f (mk_instr_state rs' pr' m', cf). End SEMANTICS. @@ -345,10 +382,6 @@ Fixpoint beq_expression (e1 e2: expression) {struct e1}: bool := then if beq_expression_list el1 el2 then if beq_expression m1 m2 then beq_expression e1 e2 else false else false else false else false - | Esetpred c1 el1, 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 := @@ -359,6 +392,22 @@ with beq_expression_list (el1 el2: expression_list) {struct el1} : bool := end . +Definition beq_pred_expression (e1 e2: pred_expression) : bool := + match e1, e2 with + | PEbase p1, PEbase p2 => if peq p1 p2 then true else false + | PEsetpred c1 el1, PEsetpred c2 el2 => + if condition_eq c1 c2 + then beq_expression_list el1 el2 else false + | _, _ => false + end. + +Definition beq_exit_expression (e1 e2: exit_expression) : bool := + match e1, e2 with + | EEbase, EEbase => true + | EEexit cf1, EEexit cf2 => if cf_instr_eq cf1 cf2 then true else false + | _, _ => false + end. + Scheme expression_ind2 := Induction for expression Sort Prop with expression_list_ind2 := Induction for expression_list Sort Prop. @@ -404,9 +453,8 @@ Proof. inv H0. rewrite beq_expression_refl in H; crush. inv H. rewrite beq_expression_refl in Heqb0; crush. inv H. rewrite beq_expression_list_refl in Heqb; crush. - - simplify. repeat (destruct_match; crush); subst. - 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. *) + (* 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. apply andb_false_iff in H. inv H. unfold not in *; intros. @@ -421,6 +469,62 @@ Proof. apply beq_expression_correct2 in Heqb. auto. Defined. +Lemma beq_expression_list_correct: + forall e1 e2, beq_expression_list e1 e2 = true -> e1 = e2. +Proof. + induction e1; crush. + - destruct_match; crush. + - destruct_match; crush. + apply IHe1 in H1; subst. + apply beq_expression_correct in H0; subst. + trivial. +Qed. + +Lemma beq_expression_list_correct2: + forall e1 e2, beq_expression_list e1 e2 = false -> e1 <> e2. +Proof. + induction e1; crush. + - destruct_match; crush. + - destruct_match; crush. + apply andb_false_iff in H. inv H. apply beq_expression_correct2 in H0. + unfold not in *; intros. apply H0. inv H. auto. + apply IHe1 in H0. unfold not in *; intros. apply H0. inv H. + auto. +Qed. + +Lemma beq_pred_expression_correct: + forall e1 e2, beq_pred_expression e1 e2 = true -> e1 = e2. +Proof. + destruct e1, e2; crush. + - destruct_match; crush. + - destruct_match; subst; crush. + apply beq_expression_list_correct in H; subst. + trivial. +Qed. + +Lemma beq_pred_expression_refl: + forall e, beq_pred_expression e e = true. +Proof. + destruct e; crush; destruct_match; crush. + apply beq_expression_list_refl. +Qed. + +Lemma beq_pred_expression_correct2: + forall e1 e2, beq_pred_expression e1 e2 = false -> e1 <> e2. +Proof. + destruct e1, e2; unfold not; crush. + + destruct_match; crush. + + destruct_match; crush. inv H0. + now rewrite beq_expression_list_refl in H. +Qed. + +Lemma beq_exit_expression_correct: + forall e1 e2, beq_exit_expression e1 e2 = true <-> e1 = e2. +Proof. + destruct e1, e2; split; crush; + destruct_match; subst; crush. +Qed. + Definition pred_expr_item_eq (pe1 pe2: pred_op * expression) : bool := @equiv_dec _ SATSetoid _ (fst pe1) (fst pe2) && beq_expression (snd pe1) (snd pe2). @@ -436,6 +540,29 @@ Proof. intros; destruct (pred_expr_item_eq pe1 pe2) eqn:?; unfold not; [tauto | now right]. Qed. +Lemma pred_expression_dec: + forall e1 e2: pred_expression, {e1 = e2} + {e1 <> e2}. +Proof. + intros. destruct (beq_pred_expression e1 e2) eqn:?. + eauto using beq_pred_expression_correct. + eauto using beq_pred_expression_correct2. +Qed. + +Lemma exit_expression_refl: + forall e, beq_exit_expression e e = true. +Proof. destruct e; crush; destruct_match; crush. Qed. + +Lemma exit_expression_dec: + forall e1 e2: exit_expression, {e1 = e2} + {e1 <> e2}. +Proof. + intros. destruct (beq_exit_expression e1 e2) eqn:?. + - left. eapply beq_exit_expression_correct; eauto. + - right. unfold not; intros. + assert (X: ~ (beq_exit_expression e1 e2 = true)) + by eauto with bool. + subst. apply X. apply exit_expression_refl. +Qed. + Module HashExpr' <: MiniDecidableType. Definition t := expression. Definition eq_dec := expression_dec. @@ -445,13 +572,29 @@ Module HashExpr := Make_UDT(HashExpr'). Module HT := HashTree(HashExpr). Import HT. -Fixpoint hash_predicate (max: predicate) (ap: apred_op) (h: hash_tree) - : pred_op * hash_tree := +Module PHashExpr' <: MiniDecidableType. + Definition t := pred_expression. + Definition eq_dec := pred_expression_dec. +End PHashExpr'. + +Module PHashExpr := Make_UDT(PHashExpr'). +Module PHT := HashTree(PHashExpr). + +Module EHashExpr' <: MiniDecidableType. + Definition t := exit_expression. + Definition eq_dec := exit_expression_dec. +End EHashExpr'. + +Module EHashExpr := Make_UDT(EHashExpr'). +Module EHT := HashTree(EHashExpr). + +Fixpoint hash_predicate (max: predicate) (ap: pred_pexpr) (h: PHT.hash_tree) + : pred_op * PHT.hash_tree := match ap with | Ptrue => (Ptrue, h) | Pfalse => (Pfalse, h) | Plit (b, ap') => - let (p', h') := hash_value max ap' h in + let (p', h') := PHT.hash_value max ap' h in (Plit (b, p'), h') | Pand p1 p2 => let (p1', h') := hash_predicate max p1 h in @@ -463,55 +606,40 @@ Fixpoint hash_predicate (max: predicate) (ap: apred_op) (h: hash_tree) (Por p1' p2', h'') end. -Fixpoint anorm_expression (max: predicate) (pe: apred_expr) (h: hash_tree) - : (PTree.t pred_op) * hash_tree := - match pe with - | NE.singleton (p, e) => - let (hashed_e, h') := hash_value max e h in - let (hashed_p, h'') := hash_predicate max p h' in - (PTree.set hashed_e hashed_p (PTree.empty _), h'') - | (p, e) ::| pr => - let (hashed_e, h') := hash_value max e h in - let (norm_pr, h'') := anorm_expression max pr h' in - let (hashed_p, h''') := hash_predicate max p h'' in - match norm_pr ! hashed_e with - | Some pr_op => - (PTree.set hashed_e (pr_op ∨ hashed_p) norm_pr, h''') - | None => - (PTree.set hashed_e hashed_p norm_pr, h''') - end - end. - -Fixpoint norm_expression (max: predicate) (pe: pred_expr) (h: hash_tree) - : (PTree.t pred_op) * hash_tree := - match pe with - | NE.singleton (p, e) => - let (hashed_e, h') := hash_value max e h in - (PTree.set hashed_e p (PTree.empty _), h') - | (p, e) ::| pr => - let (hashed_e, h') := hash_value max e h in - let (norm_pr, h'') := norm_expression max pr h' in - match norm_pr ! hashed_e with - | Some pr_op => - (PTree.set hashed_e (pr_op ∨ p) norm_pr, h'') - | None => - (PTree.set hashed_e p norm_pr, h'') - end - end. +Module HashExprNorm(H: Hashable). + Module H := HashTree(H). + + Fixpoint norm_expression (max: predicate) (pe: predicated H.t) (h: H.hash_tree) + : (PTree.t pred_op) * H.hash_tree := + match pe with + | NE.singleton (p, e) => + let (hashed_e, h') := H.hash_value max e h in + (PTree.set hashed_e p (PTree.empty _), h') + | (p, e) ::| pr => + let (hashed_e, h') := H.hash_value max e h in + let (norm_pr, h'') := norm_expression max pr h' in + match norm_pr ! hashed_e with + | Some pr_op => + (PTree.set hashed_e (pr_op ∨ p) norm_pr, h'') + | None => + (PTree.set hashed_e p norm_pr, h'') + end + end. -Definition mk_pred_stmnt' (e: predicate) p_e := ¬ p_e ∨ Plit (true, e). + Definition mk_pred_stmnt' (e: predicate) p_e := ¬ p_e ∨ Plit (true, e). -Definition mk_pred_stmnt t := PTree.fold (fun x a b => mk_pred_stmnt' a b ∧ x) t T. + Definition mk_pred_stmnt t := PTree.fold (fun x a b => mk_pred_stmnt' a b ∧ x) t T. -Definition mk_pred_stmnt_l (t: list (predicate * pred_op)) := fold_left (fun x a => uncurry mk_pred_stmnt' a ∧ x) t T. + Definition mk_pred_stmnt_l (t: list (predicate * pred_op)) := + fold_left (fun x a => uncurry mk_pred_stmnt' a ∧ x) t T. -Definition encode_expression max pe h := - let (tree, h) := norm_expression max pe h in - (mk_pred_stmnt tree, h). + Definition encode_expression max pe h := + let (tree, h) := norm_expression max pe h in + (mk_pred_stmnt tree, h). +End HashExprNorm. -Definition aencode_expression max pe h := - let (tree, h) := anorm_expression max pe h in - (mk_pred_stmnt tree, h). +Module HN := HashExprNorm(HashExpr). +Module EHN := HashExprNorm(EHashExpr). (*Fixpoint encode_expression_ne (max: predicate) (pe: pred_expr_ne) (h: hash_tree) : (PTree.t pred_op) * hash_tree := @@ -531,8 +659,6 @@ Fixpoint max_pred_expr (pe: pred_expr) : positive := | (p, e) ::| pe' => Pos.max (max_predicate p) (max_pred_expr pe') end. -Definition empty : forest := Rtree.empty _. - Definition ge_preserved {A B C D: Type} (ge: Genv.t A B) (tge: Genv.t C D) : Prop := (forall sp op vl m, Op.eval_operation ge sp op vl m = Op.eval_operation tge sp op vl m) @@ -575,9 +701,14 @@ Inductive similar {A B} : @ctx A -> @ctx B -> Prop := match_states ist ist' -> similar (mk_ctx ist sp ge) (mk_ctx ist' sp tge). -Definition beq_pred_expr_once (pe1 pe2: apred_expr) : bool := - let (p1, h) := aencode_expression 1%positive pe1 (PTree.empty _) in - let (p2, h') := aencode_expression 1%positive pe2 h in +Definition beq_pred_expr_once (pe1 pe2: pred_expr) : bool := + let (p1, h) := HN.encode_expression 1%positive pe1 (PTree.empty _) in + let (p2, h') := HN.encode_expression 1%positive pe2 h in + equiv_check p1 p2. + +Definition beq_pred_eexpr (pe1 pe2: pred_eexpr) : bool := + let (p1, h) := EHN.encode_expression 1%positive pe1 (PTree.empty _) in + let (p2, h') := EHN.encode_expression 1%positive pe2 h in equiv_check p1 p2. Definition tree_equiv_check_el (np2: PTree.t pred_op) (n: positive) (p: pred_op): bool := @@ -620,7 +751,7 @@ Qed. Lemma norm_expr_constant : forall x m h t h' e p, - norm_expression m x h = (t, h') -> + HN.norm_expression m x h = (t, h') -> h ! e = Some p -> h' ! e = Some p. Proof. Admitted. @@ -634,19 +765,6 @@ Proof. apply H; auto; constructor; tauto. Qed. -Module Type AbstrPredSet. - - Parameter apred_list : list apred_op. - - Parameter h : hash_tree. - - Axiom h_valid : - forall a, - In a apred_list -> - exists p, hash_predicate 1 a h = (p, h). - -End AbstrPredSet. - Definition sat_aequiv ap1 ap2 := exists h p1 p2, sat_equiv p1 p2 @@ -683,7 +801,7 @@ Abort. Lemma norm_expr_mutexcl : forall m pe h t h' e e' p p', - norm_expression m pe h = (t, h') -> + HN.norm_expression m pe h = (t, h') -> predicated_mutexcl pe -> t ! e = Some p -> t ! e' = Some p' -> @@ -747,19 +865,21 @@ Lemma norm_expression_sem_pred2 : sem_pred_expr sem ctx pe v. Proof. Admitted.*) -Definition beq_pred_expr (pe1 pe2: apred_expr) : bool := - let (np1, h) := anorm_expression 1 pe1 (PTree.empty _) in - let (np2, h') := anorm_expression 1 pe2 h in +Definition beq_pred_expr (pe1 pe2: pred_expr) : bool := + let (np1, h) := HN.norm_expression 1 pe1 (PTree.empty _) in + let (np2, h') := HN.norm_expression 1 pe2 h in forall_ptree (tree_equiv_check_el np2) np1 && forall_ptree (tree_equiv_check_None_el np1) np2. -Definition check := Rtree.beq beq_pred_expr. +Definition beq_pred_pexpr (pe1 pe2: pred_pexpr): bool := + let (np1, h) := hash_predicate 1 pe1 (PTree.empty _) in + let (np2, h') := hash_predicate 1 pe2 h in + equiv_check np1 np2. -(* Compute (check (empty # (Reg 2) <- *) -(* ((((Pand (Plit (true, 4)) (¬ (Plit (true, 4))))), (Ebase (Reg 9))) ::| *) -(* (NE.singleton (((Plit (true, 2))), (Ebase (Reg 3)))))) *) -(* (empty # (Reg 2) <- (NE.singleton (((Por (Plit (true, 2)) (Pand (Plit (true, 3)) (¬ (Plit (true, 3)))))), *) -(* (Ebase (Reg 3)))))). *) +Definition check f1 f2 := + RTree.beq beq_pred_expr f1.(forest_regs) f2.(forest_regs) + && PTree.beq beq_pred_pexpr f1.(forest_preds) f2.(forest_preds) + && beq_pred_eexpr f1.(forest_exit) f2.(forest_exit). Lemma inj_asgn_eg : forall a b, (a =? b)%nat = (a =? a)%nat -> a = b. Proof. @@ -925,10 +1045,6 @@ Section CORRECT. - inv H0. eapply IHe1 in H11; auto. eapply IHe2 in H12; auto. eapply IHe3 in H9; auto. econstructor; try eassumption. 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. @@ -1007,7 +1123,7 @@ Section CORRECT. Lemma exists_norm_expr : forall x pe expr m t h h', NE.In (pe, expr) x -> - norm_expression m x h = (t, h') -> + HN.norm_expression m x h = (t, h') -> exists e pe', t ! e = Some pe' /\ pe ⇒ pe' /\ h' ! e = Some expr. Proof. Admitted. @@ -1216,21 +1332,7 @@ Section CORRECT. sem octx fb i' -> match_states (fst i) (fst i') /\ snd i = snd i'. Proof using HSIM. - intros. - unfold check, get_forest in *; intros; - pose proof beq_expression_correct. - pose proof (Rtree.beq_sound beq_pred_expr fa fb H). - inv H0; inv H1. - constructor; simplify. - { admit. } - { inv H0; inv H4. - repeat match goal with - | H: forall _ : reg, _ |- _ => specialize (H x) - | H: forall _ : Rtree.elt, _ |- _ => specialize (H (Reg x)) - end. - repeat (destruct_match; try contradiction). - unfold "#" in *. -Admitted. + Admitted. Lemma check_correct2: forall (fa fb : forest) i, @@ -1242,14 +1344,8 @@ Admitted. End CORRECT. Lemma get_empty: - forall r, empty#r = NE.singleton (Ptrue, Ebase r). -Proof. - intros; unfold get_forest; - destruct_match; auto; [ ]; - match goal with - [ H : context[Rtree.get _ empty] |- _ ] => rewrite Rtree.gempty in H - end; discriminate. -Qed. + forall r, empty#r r = NE.singleton (Ptrue, Ebase r). +Proof. unfold "#r"; intros. rewrite RTree.gempty. trivial. Qed. Section BOOLEAN_EQUALITY. @@ -1334,24 +1430,40 @@ Section BOOLEAN_EQUALITY. End BOOLEAN_EQUALITY. -Lemma map1: - forall w dst dst', +Lemma forest_reg_gso: + forall (f : forest) w dst dst', dst <> dst' -> - (empty # dst <- w) # dst' = NE.singleton (Ptrue, Ebase dst'). -Proof. intros; unfold get_forest; rewrite Rtree.gso; auto; apply get_empty. Qed. + (f #r dst <- w) #r dst' = f #r dst'. +Proof. + unfold "#r"; intros. + unfold forest_regs. unfold set_forest. + rewrite RTree.gso; auto. +Qed. -Lemma genmap1: +Lemma forest_reg_gss: + forall (f : forest) w dst, + (f #r dst <- w) #r dst = w. +Proof. + unfold "#r"; intros. + unfold forest_regs. unfold set_forest. + rewrite RTree.gss; auto. +Qed. + +Lemma forest_pred_gso: forall (f : forest) w dst dst', dst <> dst' -> - (f # dst <- w) # dst' = f # dst'. -Proof. intros; unfold get_forest; rewrite Rtree.gso; auto. Qed. - -Lemma map2: - forall (v : apred_expr) x rs, - (rs # x <- v) # x = v. -Proof. intros; unfold get_forest; rewrite Rtree.gss; trivial. Qed. - -Lemma tri1: - forall x y, - Reg x <> Reg y -> x <> y. -Proof. crush. Qed. + (set_forest_p dst w f) #p dst' = f #p dst'. +Proof. + unfold "#p"; intros. + unfold forest_preds. unfold set_forest_p. + rewrite PTree.gso; auto. +Qed. + +Lemma forest_pred_gss: + forall (f : forest) w dst, + (set_forest_p dst w f) #p dst = w. +Proof. + unfold "#p"; intros. + unfold forest_preds. unfold set_forest_p. + rewrite PTree.gss; auto. +Qed. diff --git a/src/hls/GiblePargen.v b/src/hls/GiblePargen.v index b7f4446..907266c 100644 --- a/src/hls/GiblePargen.v +++ b/src/hls/GiblePargen.v @@ -59,10 +59,10 @@ to correctly translate the predicates. |*) Fixpoint list_translation (l : list reg) (f : forest) {struct l} - : list apred_expr := + : list pred_expr := match l with | nil => nil - | i :: l => (f # (Reg i)) :: (list_translation l f) + | i :: l => (f #r (Reg i)) :: (list_translation l f) end. Fixpoint replicate {A} (n: nat) (l: A) := @@ -89,40 +89,40 @@ Definition map_pred_op {A B P: Type} (pf: option (@Predicate.pred_op P) * (A -> | (p, a), (p', f) => (merge''' p p', f a) end. -Definition predicated_prod {A B: Type} (p1: apredicated A) (p2: apredicated B) := +Definition predicated_prod {A B: Type} (p1: predicated A) (p2: predicated B) := NE.map (fun x => match x with ((a, b), (c, d)) => (Pand a c, (b, d)) end) (NE.non_empty_prod p1 p2). -Definition predicated_map {A B: Type} (f: A -> B) (p: apredicated A) - : apredicated B := NE.map (fun x => (fst x, f (snd x))) p. +Definition predicated_map {A B: Type} (f: A -> B) (p: predicated A) + : predicated B := NE.map (fun x => (fst x, f (snd x))) p. (*map (fun x => (fst x, Econs (snd x) Enil)) pel*) -Definition merge' (pel: apred_expr) (tpel: apredicated expression_list) := +Definition merge' (pel: pred_expr) (tpel: predicated expression_list) := predicated_map (uncurry Econs) (predicated_prod pel tpel). -Fixpoint merge (pel: list apred_expr): apredicated expression_list := +Fixpoint merge (pel: list pred_expr): predicated expression_list := match pel with | nil => NE.singleton (T, Enil) | a :: b => merge' a (merge b) end. -Definition map_predicated {A B} (pf: apredicated (A -> B)) (pa: apredicated A) - : apredicated B := +Definition map_predicated {A B} (pf: predicated (A -> B)) (pa: predicated A) + : predicated B := predicated_map (fun x => (fst x) (snd x)) (predicated_prod pf pa). -Definition predicated_apply1 {A B} (pf: apredicated (A -> B)) (pa: A) - : apredicated B := +Definition predicated_apply1 {A B} (pf: predicated (A -> B)) (pa: A) + : predicated B := NE.map (fun x => (fst x, (snd x) pa)) pf. -Definition predicated_apply2 {A B C} (pf: apredicated (A -> B -> C)) (pa: A) - (pb: B): apredicated C := +Definition predicated_apply2 {A B C} (pf: predicated (A -> B -> C)) (pa: A) + (pb: B): predicated C := NE.map (fun x => (fst x, (snd x) pa pb)) pf. -Definition predicated_apply3 {A B C D} (pf: apredicated (A -> B -> C -> D)) - (pa: A) (pb: B) (pc: C): apredicated D := +Definition predicated_apply3 {A B C D} (pf: predicated (A -> B -> C -> D)) + (pa: A) (pb: B) (pc: C): predicated D := NE.map (fun x => (fst x, (snd x) pa pb pc)) pf. -Definition predicated_from_opt {A: Type} (p: option apred_op) (a: A) := +Definition predicated_from_opt {A: Type} (p: option pred_op) (a: A) := match p with | Some p' => NE.singleton (p', a) | None => NE.singleton (T, a) @@ -143,19 +143,19 @@ Fixpoint NEapp {A} (l m: NE.non_empty A) := | a ::| b => a ::| NEapp b m end. -Definition app_predicated' {A: Type} (a b: apredicated A) := +Definition app_predicated' {A: Type} (a b: predicated A) := let negation := ¬ (NEfold_left (fun a b => a ∨ (fst b)) b ⟂) in NEapp (NE.map (fun x => (negation ∧ fst x, snd x)) a) b. -Definition app_predicated {A: Type} (p': apred_op) (a b: apredicated A) := +Definition app_predicated {A: Type} (p': pred_op) (a b: predicated A) := NEapp (NE.map (fun x => (¬ p' ∧ fst x, snd x)) a) (NE.map (fun x => (p' ∧ fst x, snd x)) b). -Definition prune_predicated {A: Type} (a: apredicated A) := - NE.filter (fun x => match deep_simplify expression_dec (fst x) with ⟂ => false | _ => true end) - (NE.map (fun x => (deep_simplify expression_dec (fst x), snd x)) a). +Definition prune_predicated {A: Type} (a: predicated A) := + NE.filter (fun x => match deep_simplify peq (fst x) with ⟂ => false | _ => true end) + (NE.map (fun x => (deep_simplify peq (fst x), snd x)) a). -Definition pred_ret {A: Type} (a: A) : apredicated A := +Definition pred_ret {A: Type} (a: A) : predicated A := NE.singleton (T, a). (*| @@ -174,13 +174,15 @@ This is done by multiplying the predicates together, and assigning the negation of the expression to the other predicates. |*) -Definition upd_pred_forest (p: apred_op) (f: forest) := - PTree.map (fun i e => - NE.map (fun (x: apred_op * expression) => +Definition upd_pred_forest (p: pred_op) (f: forest): forest := + mk_forest (PTree.map (fun i e => + NE.map (fun (x: pred_op * expression) => let (pred, expr) := x in - (Pand p pred, expr)) e) f. + (Pand p pred, expr)) e) f.(forest_regs)) + f.(forest_preds) + f.(forest_exit). -Fixpoint apredicated_to_apred_op (b: bool) (a: apredicated expression): apred_op := +Fixpoint apredicated_to_apred_op (b: bool) (a: predicated pred_expression): pred_pexpr := match a with | NE.singleton (p, e) => Pimplies p (Plit (b, e)) | (p, e) ::| r => @@ -209,70 +211,72 @@ Fixpoint apredicated_to_apred_op (b: bool) (a: apredicated expression): apred_op (* Definition get_pred (f: forest) (ap: option pred_op): option apred_op := *) (* get_pred' f (Option.default T ap). *) -Fixpoint get_pred' (f: forest) (ap: pred_op): apred_op := - match ap with - | Ptrue => Ptrue - | Pfalse => Pfalse - | Plit (a, b) => - apredicated_to_apred_op a (f # (Pred b)) - | Pand a b => Pand (get_pred' f a) (get_pred' f b) - | Por a b => Por (get_pred' f a) (get_pred' f b) - end. +(* Fixpoint get_pred' (f: forest) (ap: pred_op): apred_op := *) +(* match ap with *) +(* | Ptrue => Ptrue *) +(* | Pfalse => Pfalse *) +(* | Plit (a, b) => *) +(* apredicated_to_apred_op a (f # (Pred b)) *) +(* | Pand a b => Pand (get_pred' f a) (get_pred' f b) *) +(* | Por a b => Por (get_pred' f a) (get_pred' f b) *) +(* end. *) -Definition get_pred (f: forest) (ap: option pred_op): apred_op := - get_pred' f (Option.default Ptrue ap). +(* Definition get_pred (f: forest) (ap: option pred_op): apred_op := *) +(* get_pred' f (Option.default Ptrue ap). *) #[local] Open Scope monad_scope. Definition simpl_combine {A: Type} (a b: option (@Predicate.pred_op A)) := Option.map simplify (combine_pred a b). -Definition update (fop : option (apred_op * forest)) (i : instr): option (apred_op * forest) := +Definition dfltp {A} (p: option (@Predicate.pred_op A)) := Option.default T p. + +Definition update (fop : option (pred_op * forest)) (i : instr): option (pred_op * forest) := do (pred, f) <- fop; match i with | RBnop => fop | RBop p op rl r => do pruned <- prune_predicated - (app_predicated (get_pred f p ∧ pred) - (f # (Reg r)) + (app_predicated (dfltp p ∧ pred) + (f #r (Reg r)) (map_predicated (pred_ret (Eop op)) (merge (list_translation rl f)))); - Some (pred, f # (Reg r) <- pruned) + Some (pred, f #r (Reg r) <- pruned) | RBload p chunk addr rl r => do pruned <- prune_predicated - (app_predicated (get_pred f p ∧ pred) - (f # (Reg r)) + (app_predicated (dfltp p ∧ pred) + (f #r (Reg r)) (map_predicated (map_predicated (pred_ret (Eload chunk addr)) (merge (list_translation rl f))) - (f # Mem))); - Some (pred, f # (Reg r) <- pruned) + (f #r Mem))); + Some (pred, f #r (Reg r) <- pruned) | RBstore p chunk addr rl r => do pruned <- prune_predicated - (app_predicated (get_pred f p ∧ pred) - (f # Mem) + (app_predicated (dfltp p ∧ pred) + (f #r Mem) (map_predicated (map_predicated (predicated_apply2 (map_predicated (pred_ret Estore) - (f # (Reg r))) chunk addr) - (merge (list_translation rl f))) (f # Mem))); - Some (pred, f # Mem <- pruned) + (f #r (Reg r))) chunk addr) + (merge (list_translation rl f))) (f #r Mem))); + Some (pred, f #r Mem <- pruned) | RBsetpred p' c args p => - do pruned <- - prune_predicated - (app_predicated (get_pred f p' ∧ pred) - (f # (Pred p)) - (map_predicated (pred_ret (Esetpred c)) - (merge (list_translation args f)))); - Some (pred, f # (Pred p) <- pruned) + let new_pred := + (f #p p) ∧ + ((dfltp p' ∧ pred) + → map_predicated (pred_ret (PEsetpred c)) + (merge (list_translation args f))) + in + Some (pred, f #p p <- new_pred) | RBexit p c => - let new_p := simplify (get_pred' f (negate (Option.default T p)) ∧ pred) in + let new_p := simplify (negate (dfltp p) ∧ pred) in do pruned <- prune_predicated - (app_predicated (get_pred f p ∧ pred) (f # Exit) (pred_ret (Eexit c))); - Some (new_p, f # Exit <- pruned) + (app_predicated (dfltp p ∧ pred) (f.(forest_exit)) (pred_ret (EEexit c))); + Some (new_p, f <-e pruned) end. (*| -- cgit