From ac8b7ae094cf7741fec63effd8fcfd1467fb2edf Mon Sep 17 00:00:00 2001 From: Sylvain Boulmé Date: Thu, 7 Jan 2021 13:05:18 +0100 Subject: directory postpass_lib --- scheduling/abstractbb/AbstractBasicBlocksDef.v | 473 +++++++++++++++++++++++++ 1 file changed, 473 insertions(+) create mode 100644 scheduling/abstractbb/AbstractBasicBlocksDef.v (limited to 'scheduling/abstractbb') diff --git a/scheduling/abstractbb/AbstractBasicBlocksDef.v b/scheduling/abstractbb/AbstractBasicBlocksDef.v new file mode 100644 index 00000000..34d72de1 --- /dev/null +++ b/scheduling/abstractbb/AbstractBasicBlocksDef.v @@ -0,0 +1,473 @@ +(* *************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Sylvain Boulmé Grenoble-INP, VERIMAG *) +(* David Monniaux CNRS, VERIMAG *) +(* Cyril Six Kalray *) +(* *) +(* Copyright Kalray. Copyright VERIMAG. All rights reserved. *) +(* This file is distributed under the terms of the INRIA *) +(* Non-Commercial License Agreement. *) +(* *) +(* *************************************************************) + +(** Syntax and Sequential Semantics of Abstract Basic Blocks. +*) +Require Import Setoid. +Require Import ImpPrelude. + +Module Type PseudoRegisters. + +Parameter t: Type. + +Parameter eq_dec: forall (x y: t), { x = y } + { x<>y }. + +End PseudoRegisters. + + +(** * Parameters of the language of Basic Blocks *) +Module Type LangParam. + +Declare Module R: PseudoRegisters. + +Parameter value: Type. + +(** Declare the type of operations *) + +Parameter op: Type. (* type of operations *) + +Parameter genv: Type. (* environment to be used for evaluating an op *) + +Parameter op_eval: genv -> op -> list value -> option value. + +End LangParam. + + + +(** * Syntax and (sequential) semantics of "abstract basic blocks" *) +Module MkSeqLanguage(P: LangParam). + +Export P. + +Local Open Scope list. + +Section SEQLANG. + +Variable ge: genv. + +Definition mem := R.t -> value. + +Definition assign (m: mem) (x:R.t) (v: value): mem + := fun y => if R.eq_dec x y then v else m y. + + +(** Expressions *) + +Inductive exp := + | PReg (x:R.t) (**r pseudo-register *) + | Op (o:op) (le: list_exp) (**r operation *) + | Old (e: exp) (**r evaluation of [e] in the initial state of the instruction (see [inst] below) *) +with list_exp := + | Enil + | Econs (e:exp) (le:list_exp) + | LOld (le: list_exp) +. + +Fixpoint exp_eval (e: exp) (m old: mem): option value := + match e with + | PReg x => Some (m x) + | Op o le => + match list_exp_eval le m old with + | Some lv => op_eval ge o lv + | _ => None + end + | Old e => exp_eval e old old + end +with list_exp_eval (le: list_exp) (m old: mem): option (list value) := + match le with + | Enil => Some nil + | Econs e le' => + match exp_eval e m old, list_exp_eval le' m old with + | Some v, Some lv => Some (v::lv) + | _, _ => None + end + | LOld le => list_exp_eval le old old + end. + +(** An instruction represents a sequence of assignments where [Old] refers to the initial state of the sequence. *) +Definition inst := list (R.t * exp). + +Fixpoint inst_run (i: inst) (m old: mem): option mem := + match i with + | nil => Some m + | (x, e)::i' => + match exp_eval e m old with + | Some v' => inst_run i' (assign m x v') old + | None => None + end + end. + +(** A basic block is a sequence of instructions. *) +Definition bblock := list inst. + +Fixpoint run (p: bblock) (m: mem): option mem := + match p with + | nil => Some m + | i::p' => + match inst_run i m m with + | Some m' => run p' m' + | None => None + end + end. + +(* A few useful lemma *) +Lemma assign_eq m x v: + (assign m x v) x = v. +Proof. + unfold assign. destruct (R.eq_dec x x); try congruence. +Qed. + +Lemma assign_diff m x y v: + x<>y -> (assign m x v) y = m y. +Proof. + unfold assign. destruct (R.eq_dec x y); try congruence. +Qed. + +Lemma assign_skips m x y: + (assign m x (m x)) y = m y. +Proof. + unfold assign. destruct (R.eq_dec x y); try congruence. +Qed. + +Lemma assign_swap m x1 v1 x2 v2 y: + x1 <> x2 -> (assign (assign m x1 v1) x2 v2) y = (assign (assign m x2 v2) x1 v1) y. +Proof. + intros; destruct (R.eq_dec x2 y). + - subst. rewrite assign_eq, assign_diff; auto. rewrite assign_eq; auto. + - rewrite assign_diff; auto. + destruct (R.eq_dec x1 y). + + subst; rewrite! assign_eq. auto. + + rewrite! assign_diff; auto. +Qed. + + +(** A small theory of bblock simulation *) + +(* equalities on bblock outputs *) +Definition res_eq (om1 om2: option mem): Prop := + match om1 with + | Some m1 => exists m2, om2 = Some m2 /\ forall x, m1 x = m2 x + | None => om2 = None + end. + +Scheme exp_mut := Induction for exp Sort Prop +with list_exp_mut := Induction for list_exp Sort Prop. + +Lemma exp_equiv e old1 old2: + (forall x, old1 x = old2 x) -> + forall m1 m2, (forall x, m1 x = m2 x) -> + (exp_eval e m1 old1) = (exp_eval e m2 old2). +Proof. + intros H1. + induction e using exp_mut with (P0:=fun l => forall m1 m2, (forall x, m1 x = m2 x) -> list_exp_eval l m1 old1 = list_exp_eval l m2 old2); cbn; try congruence; auto. + - intros; erewrite IHe; eauto. + - intros; erewrite IHe, IHe0; auto. +Qed. + +Definition bblock_simu (p1 p2: bblock): Prop + := forall m, (run p1 m) <> None -> res_eq (run p1 m) (run p2 m). + +Lemma inst_equiv_refl i old1 old2: + (forall x, old1 x = old2 x) -> + forall m1 m2, (forall x, m1 x = m2 x) -> + res_eq (inst_run i m1 old1) (inst_run i m2 old2). +Proof. + intro H; induction i as [ | [x e]]; cbn; eauto. + intros m1 m2 H1. erewrite exp_equiv; eauto. + destruct (exp_eval e m2 old2); cbn; auto. + apply IHi. + unfold assign; intro y. destruct (R.eq_dec x y); auto. +Qed. + +Lemma bblock_equiv_refl p: forall m1 m2, (forall x, m1 x = m2 x) -> res_eq (run p m1) (run p m2). +Proof. + induction p as [ | i p']; cbn; eauto. + intros m1 m2 H; lapply (inst_equiv_refl i m1 m2); auto. + intros X; lapply (X m1 m2); auto; clear X. + destruct (inst_run i m1 m1); cbn. + - intros [m3 [H1 H2]]; rewrite H1; cbn; auto. + - intros H1; rewrite H1; cbn; auto. +Qed. + +Lemma res_eq_sym om1 om2: res_eq om1 om2 -> res_eq om2 om1. +Proof. + destruct om1; cbn. + - intros [m2 [H1 H2]]; subst; cbn. eauto. + - intros; subst; cbn; eauto. +Qed. + +Lemma res_eq_trans (om1 om2 om3: option mem): + (res_eq om1 om2) -> (res_eq om2 om3) -> (res_eq om1 om3). +Proof. + destruct om1; cbn. + - intros [m2 [H1 H2]]; subst; cbn. + intros [m3 [H3 H4]]; subst; cbn. + eapply ex_intro; intuition eauto. rewrite H2; auto. + - intro; subst; cbn; auto. +Qed. + +Lemma bblock_simu_alt p1 p2: bblock_simu p1 p2 <-> (forall m1 m2, (forall x, m1 x = m2 x) -> (run p1 m1)<>None -> res_eq (run p1 m1) (run p2 m2)). +Proof. + unfold bblock_simu; intuition. + intros; eapply res_eq_trans. eauto. + eapply bblock_equiv_refl; eauto. +Qed. + + +Lemma run_app p1: forall m1 p2, + run (p1++p2) m1 = + match run p1 m1 with + | Some m2 => run p2 m2 + | None => None + end. +Proof. + induction p1; cbn; try congruence. + intros; destruct (inst_run _ _ _); cbn; auto. +Qed. + +Lemma run_app_None p1 m1 p2: + run p1 m1 = None -> + run (p1++p2) m1 = None. +Proof. + intro H; rewrite run_app. rewrite H; auto. +Qed. + +Lemma run_app_Some p1 m1 m2 p2: + run p1 m1 = Some m2 -> + run (p1++p2) m1 = run p2 m2. +Proof. + intros H; rewrite run_app. rewrite H; auto. +Qed. + +End SEQLANG. + + +(** * Terms in the symbolic execution *) + +(** Such a term represents the successive computations in one given pseudo-register. +The [hid] has no formal semantics: it is only used by the hash-consing oracle (itself dynamically checked to behave like an identity function). + +*) + +Module Terms. + +Inductive term := + | Input (x:R.t) (hid:hashcode) + | App (o: op) (l: list_term) (hid:hashcode) +with list_term := + | LTnil (hid:hashcode) + | LTcons (t:term) (l:list_term) (hid:hashcode) + . + +Scheme term_mut := Induction for term Sort Prop +with list_term_mut := Induction for list_term Sort Prop. + +Declare Scope pattern_scope. +Declare Scope term_scope. +Bind Scope pattern_scope with term. +Delimit Scope term_scope with term. +Delimit Scope pattern_scope with pattern. + +Local Open Scope pattern_scope. + +Notation "[ ]" := (LTnil _) (format "[ ]"): pattern_scope. +Notation "[ x ]" := (LTcons x [ ] _): pattern_scope. +Notation "[ x ; y ; .. ; z ]" := (LTcons x (LTcons y .. (LTcons z (LTnil _) _) .. _) _): pattern_scope. +Notation "o @ l" := (App o l _) (at level 50, no associativity): pattern_scope. + +Import HConsingDefs. + +Notation "[ ]" := (LTnil unknown_hid) (format "[ ]"): term_scope. +Notation "[ x ]" := (LTcons x []%term unknown_hid): term_scope. +Notation "[ x ; y ; .. ; z ]" := (LTcons x (LTcons y .. (LTcons z (LTnil unknown_hid) unknown_hid) .. unknown_hid) unknown_hid): term_scope. +Notation "o @ l" := (App o l unknown_hid) (at level 50, no associativity): term_scope. + + +Fixpoint term_eval (ge: genv) (t: term) (m: mem): option value := + match t with + | Input x _ => Some (m x) + | o @ l => + match list_term_eval ge l m with + | Some v => op_eval ge o v + | _ => None + end + end +with list_term_eval ge (l: list_term) (m: mem) {struct l}: option (list value) := + match l with + | [] => Some nil + | LTcons t l' _ => + match term_eval ge t m, list_term_eval ge l' m with + | Some v, Some lv => Some (v::lv) + | _, _ => None + end + end. + + +Definition term_get_hid (t: term): hashcode := + match t with + | Input _ hid => hid + | App _ _ hid => hid + end. + +Definition list_term_get_hid (l: list_term): hashcode := + match l with + | LTnil hid => hid + | LTcons _ _ hid => hid + end. + + +Fixpoint allvalid ge (l: list term) m : Prop := + match l with + | nil => True + | t::nil => term_eval ge t m <> None + | t::l' => term_eval ge t m <> None /\ allvalid ge l' m + end. + +Lemma allvalid_extensionality ge (l: list term) m: + allvalid ge l m <-> (forall t, List.In t l -> term_eval ge t m <> None). +Proof. + induction l as [|t l]; cbn; try (tauto). + destruct l. + - intuition (congruence || eauto). + - rewrite IHl; clear IHl. intuition (congruence || eauto). +Qed. + +(** * Rewriting rules in the symbolic execution *) + +(** The symbolic execution is parametrized by rewriting rules on pseudo-terms. *) + +Record pseudo_term: Type := intro_fail { + mayfail: list term; + effect: term +}. + +(** Simulation relation between a term and a pseudo-term *) + +Definition match_pt (t: term) (pt: pseudo_term) := + (forall ge m, term_eval ge t m <> None <-> allvalid ge pt.(mayfail) m) + /\ (forall ge m0 m1, term_eval ge t m0 = Some m1 -> term_eval ge pt.(effect) m0 = Some m1). + +Lemma inf_option_equivalence (A:Type) (o1 o2: option A): + (o1 <> None -> o1 = o2) <-> (forall m1, o1 = Some m1 -> o2 = Some m1). +Proof. + destruct o1; intuition (congruence || eauto). + symmetry; eauto. +Qed. + +Lemma intro_fail_correct (l: list term) (t: term) : + (forall ge m, term_eval ge t m <> None <-> allvalid ge l m) -> match_pt t (intro_fail l t). +Proof. + unfold match_pt; cbn; intros; intuition congruence. +Qed. +Hint Resolve intro_fail_correct: wlp. + +(** The default reduction of a term to a pseudo-term *) +Definition identity_fail (t: term):= intro_fail (t::nil) t. + +Lemma identity_fail_correct (t: term): match_pt t (identity_fail t). +Proof. + eapply intro_fail_correct; cbn; tauto. +Qed. +Global Opaque identity_fail. +Hint Resolve identity_fail_correct: wlp. + +(** The reduction for constant term *) +Definition nofail (is_constant: op -> bool) (t: term):= + match t with + | Input x _ => intro_fail nil t + | o @ [] => if is_constant o then (intro_fail nil t) else (identity_fail t) + | _ => identity_fail t + end. + +Lemma nofail_correct (is_constant: op -> bool) t: + (forall ge o, is_constant o = true -> op_eval ge o nil <> None) -> match_pt t (nofail is_constant t). +Proof. + destruct t; cbn. + + intros; eapply intro_fail_correct; cbn; intuition congruence. + + intros; destruct l; cbn; auto with wlp. + destruct (is_constant o) eqn:Heqo; cbn; intuition eauto with wlp. + eapply intro_fail_correct; cbn; intuition eauto with wlp. +Qed. +Global Opaque nofail. +Hint Resolve nofail_correct: wlp. + +(** Term equivalence preserve the simulation by pseudo-terms *) +Definition term_equiv t1 t2:= forall ge m, term_eval ge t1 m = term_eval ge t2 m. + +Global Instance term_equiv_Equivalence : Equivalence term_equiv. +Proof. + split; intro x; unfold term_equiv; intros; eauto. + eapply eq_trans; eauto. +Qed. + +Lemma match_pt_term_equiv t1 t2 pt: term_equiv t1 t2 -> match_pt t1 pt -> match_pt t2 pt. +Proof. + unfold match_pt, term_equiv. + intros H. intuition; try (erewrite <- H1 in * |- *; congruence). + erewrite <- H2; eauto; congruence. +Qed. +Hint Resolve match_pt_term_equiv: wlp. + +(** Other generic reductions *) +Definition app_fail (l: list term) (pt: pseudo_term): pseudo_term := + {| mayfail := List.rev_append l pt.(mayfail); effect := pt.(effect) |}. + +Lemma app_fail_allvalid_correct l pt t1 t2: forall + (V1: forall (ge : genv) (m : mem), term_eval ge t1 m <> None <-> allvalid ge (mayfail pt) m) + (V2: forall (ge : genv) (m : mem), term_eval ge t2 m <> None <-> allvalid ge (mayfail {| mayfail := t1 :: l; effect := t1 |}) m) + (ge : genv) (m : mem), term_eval ge t2 m <> None <-> allvalid ge (mayfail (app_fail l pt)) m. +Proof. + intros; generalize (V1 ge m) (V2 ge m); rewrite !allvalid_extensionality; cbn. clear V1 V2. + intuition subst. + + rewrite rev_append_rev, in_app_iff, <- in_rev in H3. destruct H3; eauto. + + eapply H3; eauto. + intros. intuition subst. + * eapply H2; eauto. intros; eapply H0; eauto. rewrite rev_append_rev, in_app_iff; auto. + * intros; eapply H0; eauto. rewrite rev_append_rev, in_app_iff, <- in_rev; auto. +Qed. +Local Hint Resolve app_fail_allvalid_correct: core. + +Lemma app_fail_correct l pt t1 t2: + match_pt t1 pt -> + match_pt t2 {| mayfail:=t1::l; effect:=t1 |} -> + match_pt t2 (app_fail l pt). +Proof. + unfold match_pt in * |- *; intros (V1 & E1) (V2 & E2); split; intros ge m; try (eauto; fail). +Qed. +Extraction Inline app_fail. + +Import ImpCore.Notations. +Local Open Scope impure_scope. + +(** Specification of rewriting functions in parameter of the symbolic execution: in the impure monad, because the rewriting functions produce hash-consed terms (wrapped in pseudo-terms). +*) +Record reduction:= { + result:> term -> ?? pseudo_term; + result_correct: forall t, WHEN result t ~> pt THEN match_pt t pt; +}. +Hint Resolve result_correct: wlp. + +End Terms. + +End MkSeqLanguage. + + +Module Type SeqLanguage. + +Declare Module LP: LangParam. + +Include MkSeqLanguage LP. + +End SeqLanguage. + -- cgit