diff options
author | Yann Herklotz <git@yannherklotz.com> | 2021-01-13 17:57:51 +0000 |
---|---|---|
committer | Yann Herklotz <git@yannherklotz.com> | 2021-01-13 17:57:51 +0000 |
commit | 7145dfbe0c74e4a6ce2197b3d766a30787987600 (patch) | |
tree | cc6e7cc37c75bc836a06d4b22a8e2d8a3afd6fc6 | |
parent | 9cf525f98785f66066ed841f07c1b69312a0a0f9 (diff) | |
download | vericert-kvx-7145dfbe0c74e4a6ce2197b3d766a30787987600.tar.gz vericert-kvx-7145dfbe0c74e4a6ce2197b3d766a30787987600.zip |
Correct translation of scheduling with oracle check
-rw-r--r-- | src/hls/RTLPargen.v | 57 |
1 files changed, 53 insertions, 4 deletions
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 <https://www.gnu.org/licenses/>. *) -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. |