directory postpass_lib

1 files changed, 473 insertions, 0 deletions

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.
+