From 7145dfbe0c74e4a6ce2197b3d766a30787987600 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Wed, 13 Jan 2021 17:57:51 +0000 Subject: Correct translation of scheduling with oracle check --- src/hls/RTLPargen.v | 57 +++++++++++++++++++++++++++++++++++++++++++++++++---- 1 file changed, 53 insertions(+), 4 deletions(-) (limited to 'src/hls/RTLPargen.v') diff --git a/src/hls/RTLPargen.v b/src/hls/RTLPargen.v index a0f6fbb..836ceac 100644 --- a/src/hls/RTLPargen.v +++ b/src/hls/RTLPargen.v @@ -16,12 +16,61 @@ * along with this program. If not, see . *) -From compcert Require Import AST. -From vericert Require Import RTLBlock RTLPar. +From compcert Require Import AST Maps. +From vericert Require Import Vericertlib RTLBlock RTLPar Scheduleoracle. -Parameter schedule : RTLBlock.function -> Errors.res RTLPar.function. +Fixpoint beq {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 + && beq beqA l1 l2 && beq beqA r1 r2 + end. -Definition transl_fundef := transf_partial_fundef schedule. +Lemma beq_correct: + forall A B beqA m1 m2, + @beq 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 beq. 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. + +Parameter schedule : RTLBlock.function -> RTLPar.function. + +Definition transl_function (f : RTLBlock.function) : Errors.res RTLPar.function := + let tf := schedule f in + if beq schedule_oracle f.(RTLBlock.fn_code) tf.(fn_code) then + Errors.OK tf + else + Errors.Error (Errors.msg "RTLPargen: Could not prove the blocks equivalent."). + +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