diff options
Diffstat (limited to 'src/hls/Scheduleoracle.v')
-rw-r--r-- | src/hls/Scheduleoracle.v | 181 |
1 files changed, 88 insertions, 93 deletions
diff --git a/src/hls/Scheduleoracle.v b/src/hls/Scheduleoracle.v index b5aa86d..7c22995 100644 --- a/src/hls/Scheduleoracle.v +++ b/src/hls/Scheduleoracle.v @@ -20,9 +20,18 @@ * along with this program. If not, see <https://www.gnu.org/licenses/>. *) -Require Import Globalenvs Values Integers Floats Maps. -Require RTLBlock RTLPar Op Memory AST Registers. -Require Import Vericertlib. +Require compcert.backend.Registers. +Require compcert.common.AST. +Require Import compcert.common.Globalenvs. +Require compcert.common.Memory. +Require Import compcert.common.Values. +Require Import compcert.lib.Floats. +Require Import compcert.lib.Integers. +Require Import compcert.lib.Maps. +Require compcert.verilog.Op. +Require vericert.hls.RTLBlock. +Require vericert.hls.RTLPar. +Require Import vericert.common.Vericertlib. (*| Schedule Oracle @@ -154,9 +163,7 @@ Module R_indexed. end. Lemma index_inj: forall (x y: t), index x = index y -> x = y. - Proof. - destruct x; destruct y; intro; try (simpl in H; congruence). - Qed. + Proof. destruct x; destruct y; crush. Qed. Definition eq := resource_eq. End R_indexed. @@ -309,61 +316,16 @@ Scheme expression_ind2 := Induction for expression Sort Prop Lemma beq_expression_correct: forall e1 e2, beq_expression e1 e2 = true -> e1 = e2. Proof. - intro e1. + intro e1; apply expression_ind2 with - (P := fun (e1: expression) => forall e2, beq_expression e1 e2 = true -> e1 = e2) - (P0 := fun (e1: expression_list) => forall e2, beq_expression_list e1 e2 = true -> e1 = e2). - (* Ebase *) - intros r e2. - destruct e2; simpl; try congruence. - case (resource_eq r r0); congruence. - - (* Eop *) - intros o e HR e2. destruct e2; simpl; try congruence. - case (operation_eq o o0); intros. generalize (HR _ H). - congruence. congruence. - - (* Eload *) - intros m a e HR e3 HR3. destruct e2 ; simpl ; try congruence. - case (memory_chunk_eq m m0). - case (addressing_eq a a0). - caseEq (beq_expression_list e e0). - caseEq (beq_expression e3 e2). - intros. - generalize (HR e0 H0). generalize (HR3 e2 H). intros. - subst. trivial. - intros; discriminate. - intros; discriminate. - intros; discriminate. - intros; discriminate. - - (* Estore *) - intros e3 HR2 m a e HR e4 HR4 e2. - destruct e2; simpl; try congruence. - case (memory_chunk_eq m m0). case (addressing_eq a a0). - (*case (beq_expression_list e e0). case (beq_expression e3 e2). *) - intros. - caseEq (beq_expression_list e e0). intro. rewrite H0 in H. - caseEq (beq_expression e3 e2_1). intro. rewrite H1 in H. - generalize (HR2 e2_1 H1). intro. generalize (HR e0 H0). - generalize (HR4 e2_2 H). - congruence. - intro. rewrite H1 in H. discriminate. - intro. rewrite H0 in H. discriminate. - intros; congruence. - intros; congruence. - - (* Enil *) - intro e2. - unfold beq_expression_list. - case e2; intros; try congruence; trivial. - - (* Econs *) - intros e HR1 e0 HR2 e2. - destruct e2; simpl; try congruence. - caseEq (beq_expression e e2); caseEq (beq_expression_list e0 e3); simpl; try congruence. - intros. clear H1. generalize (HR1 e2 H0). generalize (HR2 e3 H). - congruence. + (P := fun (e1 : expression) => + forall e2, beq_expression e1 e2 = true -> e1 = e2) + (P0 := fun (e1 : expression_list) => + forall e2, beq_expression_list e1 e2 = true -> e1 = e2); simplify; + repeat match goal with + | [ H : context[match ?x with _ => _ end] |- _ ] => destruct x eqn:? + | [ H : context[if ?x then _ else _] |- _ ] => destruct x eqn:? + end; subst; f_equal; crush. Qed. Definition empty : forest := Rtree.empty _. @@ -377,67 +339,93 @@ Definition check := Rtree.beq beq_expression. Lemma check_correct: forall (fa fb : forest) (x : resource), check fa fb = true -> (forall x, fa # x = fb # x). Proof. - unfold check, get_forest. - intros fa fb res Hbeq x. - pose proof Hbeq as Hbeq2. - pose proof (Rtree.beq_sound beq_expression fa fb) as Hsound. - specialize (Hsound Hbeq2 x). - destruct (Rtree.get x fa) eqn:?; destruct (Rtree.get x fb) eqn:?; try contradiction. - apply beq_expression_correct. assumption. trivial. + unfold check, get_forest; intros; + pose proof beq_expression_correct; + match goal with + [ Hbeq : context[Rtree.beq], y : Rtree.elt |- _ ] => + apply (Rtree.beq_sound beq_expression fa fb) with (x := y) in Hbeq + end; + repeat destruct_match; crush. Qed. Lemma get_empty: forall r, empty#r = Ebase r. Proof. - intros r. unfold get_forest. - destruct (Rtree.get r empty) eqn:Heq; auto. - rewrite Rtree.gempty in Heq. discriminate. + intros; unfold get_forest; + destruct_match; auto; [ ]; + match goal with + [ H : context[Rtree.get _ empty] |- _ ] => rewrite Rtree.gempty in H + end; discriminate. +Qed. + +Fixpoint beq2 {A B : Type} (beqA : A -> B -> bool) (m1 : PTree.t A) (m2 : PTree.t B) {struct m1} : bool := + match m1, m2 with + | PTree.Leaf, _ => PTree.bempty m2 + | _, PTree.Leaf => PTree.bempty m1 + | PTree.Node l1 o1 r1, PTree.Node l2 o2 r2 => + match o1, o2 with + | None, None => true + | Some y1, Some y2 => beqA y1 y2 + | _, _ => false + end + && beq2 beqA l1 l2 && beq2 beqA r1 r2 + end. + +Lemma beq2_correct: + forall A B beqA m1 m2, + @beq2 A B beqA m1 m2 = true <-> + (forall (x: PTree.elt), + match PTree.get x m1, PTree.get x m2 with + | None, None => True + | Some y1, Some y2 => beqA y1 y2 = true + | _, _ => False + end). +Proof. + induction m1; intros. + - simpl. rewrite PTree.bempty_correct. split; intros. + rewrite PTree.gleaf. rewrite H. auto. + generalize (H x). rewrite PTree.gleaf. destruct (PTree.get x m2); tauto. + - destruct m2. + + unfold beq2. rewrite PTree.bempty_correct. split; intros. + rewrite H. rewrite PTree.gleaf. auto. + generalize (H x). rewrite PTree.gleaf. destruct (PTree.get x (PTree.Node m1_1 o m1_2)); tauto. + + simpl. split; intros. + * destruct (andb_prop _ _ H). destruct (andb_prop _ _ H0). + rewrite IHm1_1 in H3. rewrite IHm1_2 in H1. + destruct x; simpl. apply H1. apply H3. + destruct o; destruct o0; auto || congruence. + * apply andb_true_intro. split. apply andb_true_intro. split. + generalize (H xH); simpl. destruct o; destruct o0; tauto. + apply IHm1_1. intros; apply (H (xO x)). + apply IHm1_2. intros; apply (H (xI x)). Qed. Lemma map0: forall r, empty # r = Ebase r. -Proof. - intros. eapply get_empty. -Qed. +Proof. intros; eapply get_empty. Qed. Lemma map1: forall w dst dst', dst <> dst' -> (empty # dst <- w) # dst' = Ebase dst'. -Proof. - intros. - unfold get_forest. - rewrite Rtree.gso. eapply map0. auto. -Qed. +Proof. intros; unfold get_forest; rewrite Rtree.gso; auto; apply map0. Qed. Lemma genmap1: forall (f : forest) w dst dst', dst <> dst' -> (f # dst <- w) # dst' = f # dst'. -Proof. - intros. - unfold get_forest. - rewrite Rtree.gso. reflexivity. auto. -Qed. +Proof. intros; unfold get_forest; rewrite Rtree.gso; auto. Qed. Lemma map2: forall (v : expression) x rs, (rs # x <- v) # x = v. -Proof. - intros. - unfold get_forest. - rewrite Rtree.gss. trivial. -Qed. +Proof. intros; unfold get_forest; rewrite Rtree.gss; trivial. Qed. Lemma tri1: forall x y, Reg x <> Reg y -> x <> y. -Proof. - intros. unfold not in *; intros. - rewrite H0 in H. generalize (H (refl_equal (Reg y))). - auto. -Qed. +Proof. unfold not; intros; subst; auto. Qed. (*| Update functions. @@ -472,6 +460,13 @@ Definition update_par (f : forest) (i : RTLPar.instruction) : forest := end. (*| +Implementing which are necessary to show the correctness of the translation validation by showing +that there aren't any more effects in the resultant RTLPar code than in the RTLBlock code. +|*) + + + +(*| Get a sequence from the basic block. |*) |