From 6b31e7c2219565671ede7d7049cd7135f04b0048 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Tue, 26 Jan 2021 11:58:22 +0000 Subject: Remove the schedule oracle --- src/hls/RTLPargen.v | 518 ++++++++++++++++++++++++++++++++++++++++++++++- src/hls/Scheduleoracle.v | 515 ---------------------------------------------- 2 files changed, 515 insertions(+), 518 deletions(-) delete mode 100644 src/hls/Scheduleoracle.v (limited to 'src/hls') diff --git a/src/hls/RTLPargen.v b/src/hls/RTLPargen.v index 55bf71c..f745466 100644 --- a/src/hls/RTLPargen.v +++ b/src/hls/RTLPargen.v @@ -16,19 +16,531 @@ * along with this program. If not, see . *) +Require compcert.backend.Registers. Require Import 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 Import vericert.common.Vericertlib. Require Import vericert.hls.RTLBlock. +Require Import vericert.hls.RTLBlockInstr. Require Import vericert.hls.RTLPar. -Require Import vericert.hls.Scheduleoracle. + +(*| +Schedule Oracle +=============== + +This oracle determines if a schedule was valid by performing symbolic execution on the input and +output and showing that these behave the same. This acts on each basic block separately, as the +rest of the functions should be equivalent. +|*) + +Definition reg := positive. + +Inductive resource : Set := +| Reg : reg -> resource +| Mem : resource. + +(*| +The following defines quite a few equality comparisons automatically, however, these can be +optimised heavily if written manually, as their proofs are not needed. +|*) + +Lemma resource_eq : forall (r1 r2 : resource), {r1 = r2} + {r1 <> r2}. +Proof. + decide equality. apply Pos.eq_dec. +Defined. + +Lemma comparison_eq: forall (x y : comparison), {x = y} + {x <> y}. +Proof. + decide equality. +Defined. + +Lemma condition_eq: forall (x y : Op.condition), {x = y} + {x <> y}. +Proof. + generalize comparison_eq; intro. + generalize Int.eq_dec; intro. + generalize Int64.eq_dec; intro. + decide equality. +Defined. + +Lemma addressing_eq : forall (x y : Op.addressing), {x = y} + {x <> y}. +Proof. + generalize Int.eq_dec; intro. + generalize AST.ident_eq; intro. + generalize Z.eq_dec; intro. + generalize Ptrofs.eq_dec; intro. + decide equality. +Defined. + +Lemma typ_eq : forall (x y : AST.typ), {x = y} + {x <> y}. +Proof. + decide equality. +Defined. + +Lemma operation_eq: forall (x y : Op.operation), {x = y} + {x <> y}. +Proof. + generalize Int.eq_dec; intro. + generalize Int64.eq_dec; intro. + generalize Float.eq_dec; intro. + generalize Float32.eq_dec; intro. + generalize AST.ident_eq; intro. + generalize condition_eq; intro. + generalize addressing_eq; intro. + generalize typ_eq; intro. + decide equality. +Defined. + +Lemma memory_chunk_eq : forall (x y : AST.memory_chunk), {x = y} + {x <> y}. +Proof. + decide equality. +Defined. + +Lemma list_typ_eq: forall (x y : list AST.typ), {x = y} + {x <> y}. +Proof. + generalize typ_eq; intro. + decide equality. +Defined. + +Lemma option_typ_eq : forall (x y : option AST.typ), {x = y} + {x <> y}. +Proof. + generalize typ_eq; intro. + decide equality. +Defined. + +Lemma signature_eq: forall (x y : AST.signature), {x = y} + {x <> y}. +Proof. + repeat decide equality. +Defined. + +Lemma list_operation_eq : forall (x y : list Op.operation), {x = y} + {x <> y}. +Proof. + generalize operation_eq; intro. + decide equality. +Defined. + +Lemma list_reg_eq : forall (x y : list reg), {x = y} + {x <> y}. +Proof. + generalize Pos.eq_dec; intros. + decide equality. +Defined. + +Lemma sig_eq : forall (x y : AST.signature), {x = y} + {x <> y}. +Proof. + repeat decide equality. +Defined. + +Lemma instr_eq: forall (x y : instr), {x = y} + {x <> y}. +Proof. + generalize Pos.eq_dec; intro. + generalize typ_eq; intro. + generalize Int.eq_dec; intro. + generalize memory_chunk_eq; intro. + generalize addressing_eq; intro. + generalize operation_eq; intro. + generalize condition_eq; intro. + generalize signature_eq; intro. + generalize list_operation_eq; intro. + generalize list_reg_eq; intro. + generalize AST.ident_eq; intro. + decide equality. +Defined. + +Lemma cf_instr_eq: forall (x y : cf_instr), {x = y} + {x <> y}. +Proof. + generalize Pos.eq_dec; intro. + generalize typ_eq; intro. + generalize Int.eq_dec; intro. + generalize Int64.eq_dec; intro. + generalize Float.eq_dec; intro. + generalize Float32.eq_dec; intro. + generalize Ptrofs.eq_dec; intro. + generalize memory_chunk_eq; intro. + generalize addressing_eq; intro. + generalize operation_eq; intro. + generalize condition_eq; intro. + generalize signature_eq; intro. + generalize list_operation_eq; intro. + generalize list_reg_eq; intro. + generalize AST.ident_eq; intro. + repeat decide equality. +Defined. + +(*| +We then create equality lemmas for a resource and a module to index resources uniquely. The +indexing is done by setting Mem to 1, whereas all other infinitely many registers will all be +shifted right by 1. This means that they will never overlap. +|*) + +Module R_indexed. + Definition t := resource. + Definition index (rs: resource) : positive := + match rs with + | Reg r => xO r + | Mem => 1%positive + end. + + Lemma index_inj: forall (x y: t), index x = index y -> x = y. + Proof. destruct x; destruct y; crush. Qed. + + Definition eq := resource_eq. +End R_indexed. + +(*| +We can then create expressions that mimic the expressions defined in RTLBlock and RTLPar, which use +expressions instead of registers as their inputs and outputs. This means that we can accumulate all +the results of the operations as general expressions that will be present in those registers. + +- Ebase: the starting value of the register. +- Eop: Some arithmetic operation on a number of registers. +- Eload: A load from a memory location into a register. +- Estore: A store from a register to a memory location. + +Then, to make recursion over expressions easier, expression_list is also defined in the datatype, as +that enables mutual recursive definitions over the datatypes. +|*) + +Inductive expression : Set := +| Ebase : resource -> expression +| Eop : Op.operation -> expression_list -> expression +| Eload : AST.memory_chunk -> Op.addressing -> expression_list -> expression -> expression +| Estore : expression -> AST.memory_chunk -> Op.addressing -> expression_list -> expression -> expression +with expression_list : Set := +| Enil : expression_list +| Econs : expression -> expression_list -> expression_list. + +(*| +Using IMap we can create a map from resources to any other type, as resources can be uniquely +identified as positive numbers. +|*) + +Module Rtree := ITree(R_indexed). + +Definition forest : Type := Rtree.t expression. + +Definition regset := Registers.Regmap.t val. + +Definition get_forest v f := + match Rtree.get v f with + | None => Ebase v + | Some v' => v' + end. + +Notation "a # b" := (get_forest b a) (at level 1). +Notation "a # b <- c" := (Rtree.set b c a) (at level 1, b at next level). + +Record sem_state := mk_sem_state { + sem_state_stackp : val; + sem_state_regset : regset; + sem_state_memory : Memory.mem + }. + +(*| +Finally we want to define the semantics of execution for the expressions with symbolic values, so +the result of executing the expressions will be an expressions. +|*) + +Section SEMANTICS. + +Context (A : Set) (genv : Genv.t A unit). + +Inductive sem_value : + val -> sem_state -> expression -> val -> Prop := + | Sbase_reg: + forall parent st r, + sem_value parent st (Ebase (Reg r)) (Registers.Regmap.get r (sem_state_regset st)) + | Sop: + forall parent st op args v lv, + sem_val_list parent st args lv -> + Op.eval_operation genv (sem_state_stackp st) op lv (sem_state_memory st) = Some v -> + sem_value parent st (Eop op args) v + | Sload : + forall parent st mem_exp addr chunk args a v m' lv , + sem_mem parent st mem_exp m' -> + sem_val_list parent st args lv -> + Op.eval_addressing genv (sem_state_stackp st) addr lv = Some a -> + Memory.Mem.loadv chunk m' a = Some v -> + sem_value parent st (Eload chunk addr args mem_exp) v +with sem_mem : + val -> sem_state -> expression -> Memory.mem -> Prop := + | Sstore : + forall parent st mem_exp val_exp m'' addr v a m' chunk args lv, + sem_mem parent st mem_exp m' -> + sem_value parent st val_exp v -> + sem_val_list parent st args lv -> + Op.eval_addressing genv (sem_state_stackp st) addr lv = Some a -> + Memory.Mem.storev chunk m' a v = Some m'' -> + sem_mem parent st (Estore mem_exp chunk addr args val_exp) m'' + | Sbase_mem : + forall parent st m, + sem_mem parent st (Ebase Mem) m +with sem_val_list : + val -> sem_state -> expression_list -> list val -> Prop := + | Snil : + forall parent st, + sem_val_list parent st Enil nil + | Scons : + forall parent st e v l lv, + sem_value parent st e v -> + sem_val_list parent st l lv -> + sem_val_list parent st (Econs e l) (v :: lv). + +Inductive sem_regset : + val -> sem_state -> forest -> regset -> Prop := + | Sregset: + forall parent st f rs', + (forall x, sem_value parent st (f # (Reg x)) (Registers.Regmap.get x rs')) -> + sem_regset parent st f rs'. + +Inductive sem : + val -> sem_state -> forest -> sem_state -> Prop := + | Sem: + forall st rs' fr' m' f parent, + sem_regset parent st f rs' -> + sem_mem parent st (f # Mem) m' -> + sem parent st fr' (mk_sem_state (sem_state_stackp st) rs' m'). + + +End SEMANTICS. + +Fixpoint beq_expression (e1 e2: expression) {struct e1}: bool := + match e1, e2 with + | Ebase r1, Ebase r2 => if resource_eq r1 r2 then true else false + | Eop op1 el1, Eop op2 el2 => + if operation_eq op1 op2 then beq_expression_list el1 el2 else false + | Eload chk1 addr1 el1 e1, Eload chk2 addr2 el2 e2 => + if memory_chunk_eq chk1 chk2 + then if addressing_eq addr1 addr2 + then if beq_expression_list el1 el2 + then beq_expression e1 e2 else false else false else false + | Estore m1 chk1 addr1 el1 e1, Estore m2 chk2 addr2 el2 e2=> + if memory_chunk_eq chk1 chk2 + then if addressing_eq addr1 addr2 + then if beq_expression_list el1 el2 + then if beq_expression m1 m2 + then beq_expression e1 e2 else false else false else false else false + | _, _ => false + end +with beq_expression_list (el1 el2: expression_list) {struct el1} : bool := + match el1, el2 with + | Enil, Enil => true + | Econs e1 t1, Econs e2 t2 => beq_expression e1 e2 && beq_expression_list t1 t2 + | _, _ => false + end. + +Scheme expression_ind2 := Induction for expression Sort Prop + with expression_list_ind2 := Induction for expression_list Sort Prop. + +Lemma beq_expression_correct: + forall e1 e2, beq_expression e1 e2 = true -> e1 = e2. +Proof. + 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); 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 _. + +(*| +This function checks if all the elements in [fa] are in [fb], but not the other way round. +|*) + +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; + 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; 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. + +Lemma map1: + forall w dst dst', + dst <> dst' -> + (empty # dst <- w) # dst' = Ebase dst'. +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; auto. Qed. + +Lemma map2: + forall (v : expression) x rs, + (rs # x <- v) # x = v. +Proof. intros; unfold get_forest; rewrite Rtree.gss; trivial. Qed. + +Lemma tri1: + forall x y, + Reg x <> Reg y -> x <> y. +Proof. unfold not; intros; subst; auto. Qed. + +(*| +Update functions. +|*) + +Fixpoint list_translation (l : list reg) (f : forest) {struct l} : expression_list := + match l with + | nil => Enil + | i :: l => Econs (f # (Reg i)) (list_translation l f) + end. + +Definition update (f : forest) (i : instr) : forest := + match i with + | RBnop => f + | RBop op rl r => + f # (Reg r) <- (Eop op (list_translation rl f)) + | RBload chunk addr rl r => + f # (Reg r) <- (Eload chunk addr (list_translation rl f) (f # Mem)) + | RBstore chunk addr rl r => + f # Mem <- (Estore (f # Mem) chunk addr (list_translation rl f) (f # (Reg r))) + 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. +|*) + +Fixpoint abstract_sequence (f : forest) (b : list instr) : forest := + match b with + | nil => f + | i :: l => abstract_sequence (update f i) l + end. + +Fixpoint abstract_sequence_par (f : forest) (b : list (list instr)) : forest := + match b with + | nil => f + | i :: l => abstract_sequence_par (abstract_sequence f i) l + end. + +(*| +Check equivalence of control flow instructions. As none of the basic blocks should have been moved, +none of the labels should be different, meaning the control-flow instructions should match exactly. +|*) + +Definition check_control_flow_instr (c1 c2: cf_instr) : bool := + if cf_instr_eq c1 c2 then true else false. + +(*| +We define the top-level oracle that will check if two basic blocks are equivalent after a scheduling +transformation. +|*) + +Definition schedule_oracle (bb: RTLBlock.bblock) (bbt: RTLPar.bblock) : bool := + check (abstract_sequence empty (bb_body bb)) + (abstract_sequence_par empty (bb_body bbt)). + +Definition check_scheduled_trees := beq2 schedule_oracle. + +Ltac solve_scheduled_trees_correct := + intros; unfold check_scheduled_trees in *; + match goal with + | [ H: context[beq2 _ _ _], x: positive |- _ ] => + rewrite beq2_correct in H; specialize (H x) + end; repeat destruct_match; crush. + +Lemma check_scheduled_trees_correct: + forall f1 f2, + check_scheduled_trees f1 f2 = true -> + (forall x y1, + PTree.get x f1 = Some y1 -> + exists y2, PTree.get x f2 = Some y2 /\ schedule_oracle y1 y2 = true). +Proof. solve_scheduled_trees_correct; eexists; crush. Qed. + +Lemma check_scheduled_trees_correct2: + forall f1 f2, + check_scheduled_trees f1 f2 = true -> + (forall x, + PTree.get x f1 = None -> + PTree.get x f2 = None). +Proof. solve_scheduled_trees_correct. Qed. Parameter schedule : RTLBlock.function -> RTLPar.function. -Definition transl_function (f : RTLBlock.function) : Errors.res RTLPar.function := +Definition transl_function (f: RTLBlock.function) : Errors.res RTLPar.function := let tf := schedule f in - if beq2 schedule_oracle f.(RTLBlock.fn_code) tf.(fn_code) then + if check_scheduled_trees f.(RTLBlock.fn_code) tf.(fn_code) then Errors.OK tf else Errors.Error (Errors.msg "RTLPargen: Could not prove the blocks equivalent."). diff --git a/src/hls/Scheduleoracle.v b/src/hls/Scheduleoracle.v deleted file mode 100644 index fdcb8bb..0000000 --- a/src/hls/Scheduleoracle.v +++ /dev/null @@ -1,515 +0,0 @@ -(*| -.. coq:: none -|*) - -(* - * Vericert: Verified high-level synthesis. - * Copyright (C) 2021 Yann Herklotz - * - * This program is free software: you can redistribute it and/or modify - * it under the terms of the GNU General Public License as published by - * the Free Software Foundation, either version 3 of the License, or - * (at your option) any later version. - * - * This program is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with this program. If not, see . - *) - -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.hls.RTLBlockInstr. -Require Import vericert.common.Vericertlib. - -(*| -Schedule Oracle -=============== - -This oracle determines if a schedule was valid by performing symbolic execution on the input and -output and showing that these behave the same. This acts on each basic block separately, as the -rest of the functions should be equivalent. -|*) - -Definition reg := positive. - -Inductive resource : Set := -| Reg : reg -> resource -| Mem : resource. - -(*| -The following defines quite a few equality comparisons automatically, however, these can be -optimised heavily if written manually, as their proofs are not needed. -|*) - -Lemma resource_eq : forall (r1 r2 : resource), {r1 = r2} + {r1 <> r2}. -Proof. - decide equality. apply Pos.eq_dec. -Defined. - -Lemma comparison_eq: forall (x y : comparison), {x = y} + {x <> y}. -Proof. - decide equality. -Defined. - -Lemma condition_eq: forall (x y : Op.condition), {x = y} + {x <> y}. -Proof. - generalize comparison_eq; intro. - generalize Int.eq_dec; intro. - generalize Int64.eq_dec; intro. - decide equality. -Defined. - -Lemma addressing_eq : forall (x y : Op.addressing), {x = y} + {x <> y}. -Proof. - generalize Int.eq_dec; intro. - generalize AST.ident_eq; intro. - generalize Z.eq_dec; intro. - generalize Ptrofs.eq_dec; intro. - decide equality. -Defined. - -Lemma typ_eq : forall (x y : AST.typ), {x = y} + {x <> y}. -Proof. - decide equality. -Defined. - -Lemma operation_eq: forall (x y : Op.operation), {x = y} + {x <> y}. -Proof. - generalize Int.eq_dec; intro. - generalize Int64.eq_dec; intro. - generalize Float.eq_dec; intro. - generalize Float32.eq_dec; intro. - generalize AST.ident_eq; intro. - generalize condition_eq; intro. - generalize addressing_eq; intro. - generalize typ_eq; intro. - decide equality. -Defined. - -Lemma memory_chunk_eq : forall (x y : AST.memory_chunk), {x = y} + {x <> y}. -Proof. - decide equality. -Defined. - -Lemma list_typ_eq: forall (x y : list AST.typ), {x = y} + {x <> y}. -Proof. - generalize typ_eq; intro. - decide equality. -Defined. - -Lemma option_typ_eq : forall (x y : option AST.typ), {x = y} + {x <> y}. -Proof. - generalize typ_eq; intro. - decide equality. -Defined. - -Lemma signature_eq: forall (x y : AST.signature), {x = y} + {x <> y}. -Proof. - repeat decide equality. -Defined. - -Lemma list_operation_eq : forall (x y : list Op.operation), {x = y} + {x <> y}. -Proof. - generalize operation_eq; intro. - decide equality. -Defined. - -Lemma list_reg_eq : forall (x y : list reg), {x = y} + {x <> y}. -Proof. - generalize Pos.eq_dec; intros. - decide equality. -Defined. - -Lemma sig_eq : forall (x y : AST.signature), {x = y} + {x <> y}. -Proof. - repeat decide equality. -Defined. - -Lemma instr_eq: forall (x y : instr), {x = y} + {x <> y}. -Proof. - generalize Pos.eq_dec; intro. - generalize typ_eq; intro. - generalize Int.eq_dec; intro. - generalize memory_chunk_eq; intro. - generalize addressing_eq; intro. - generalize operation_eq; intro. - generalize condition_eq; intro. - generalize signature_eq; intro. - generalize list_operation_eq; intro. - generalize list_reg_eq; intro. - generalize AST.ident_eq; intro. - decide equality. -Defined. - -Lemma cf_instr_eq: forall (x y : cf_instr), {x = y} + {x <> y}. -Proof. - generalize Pos.eq_dec; intro. - generalize typ_eq; intro. - generalize Int.eq_dec; intro. - generalize Int64.eq_dec; intro. - generalize Float.eq_dec; intro. - generalize Float32.eq_dec; intro. - generalize Ptrofs.eq_dec; intro. - generalize memory_chunk_eq; intro. - generalize addressing_eq; intro. - generalize operation_eq; intro. - generalize condition_eq; intro. - generalize signature_eq; intro. - generalize list_operation_eq; intro. - generalize list_reg_eq; intro. - generalize AST.ident_eq; intro. - repeat decide equality. -Defined. - -(*| -We then create equality lemmas for a resource and a module to index resources uniquely. The -indexing is done by setting Mem to 1, whereas all other infinitely many registers will all be -shifted right by 1. This means that they will never overlap. -|*) - -Module R_indexed. - Definition t := resource. - Definition index (rs: resource) : positive := - match rs with - | Reg r => xO r - | Mem => 1%positive - end. - - Lemma index_inj: forall (x y: t), index x = index y -> x = y. - Proof. destruct x; destruct y; crush. Qed. - - Definition eq := resource_eq. -End R_indexed. - -(*| -We can then create expressions that mimic the expressions defined in RTLBlock and RTLPar, which use -expressions instead of registers as their inputs and outputs. This means that we can accumulate all -the results of the operations as general expressions that will be present in those registers. - -- Ebase: the starting value of the register. -- Eop: Some arithmetic operation on a number of registers. -- Eload: A load from a memory location into a register. -- Estore: A store from a register to a memory location. - -Then, to make recursion over expressions easier, expression_list is also defined in the datatype, as -that enables mutual recursive definitions over the datatypes. -|*) - -Inductive expression : Set := -| Ebase : resource -> expression -| Eop : Op.operation -> expression_list -> expression -| Eload : AST.memory_chunk -> Op.addressing -> expression_list -> expression -> expression -| Estore : expression -> AST.memory_chunk -> Op.addressing -> expression_list -> expression -> expression -with expression_list : Set := -| Enil : expression_list -| Econs : expression -> expression_list -> expression_list. - -(*| -Using IMap we can create a map from resources to any other type, as resources can be uniquely -identified as positive numbers. -|*) - -Module Rtree := ITree(R_indexed). - -Definition forest : Type := Rtree.t expression. - -Definition regset := Registers.Regmap.t val. - -Definition get_forest v f := - match Rtree.get v f with - | None => Ebase v - | Some v' => v' - end. - -Notation "a # b" := (get_forest b a) (at level 1). -Notation "a # b <- c" := (Rtree.set b c a) (at level 1, b at next level). - -Record sem_state := mk_sem_state { - sem_state_stackp : val; - sem_state_regset : regset; - sem_state_memory : Memory.mem - }. - -(*| -Finally we want to define the semantics of execution for the expressions with symbolic values, so -the result of executing the expressions will be an expressions. -|*) - -Section SEMANTICS. - -Context (A : Set) (genv : Genv.t A unit). - -Inductive sem_value : - val -> sem_state -> expression -> val -> Prop := - | Sbase_reg: - forall parent st r, - sem_value parent st (Ebase (Reg r)) (Registers.Regmap.get r (sem_state_regset st)) - | Sop: - forall parent st op args v lv, - sem_val_list parent st args lv -> - Op.eval_operation genv (sem_state_stackp st) op lv (sem_state_memory st) = Some v -> - sem_value parent st (Eop op args) v - | Sload : - forall parent st mem_exp addr chunk args a v m' lv , - sem_mem parent st mem_exp m' -> - sem_val_list parent st args lv -> - Op.eval_addressing genv (sem_state_stackp st) addr lv = Some a -> - Memory.Mem.loadv chunk m' a = Some v -> - sem_value parent st (Eload chunk addr args mem_exp) v -with sem_mem : - val -> sem_state -> expression -> Memory.mem -> Prop := - | Sstore : - forall parent st mem_exp val_exp m'' addr v a m' chunk args lv, - sem_mem parent st mem_exp m' -> - sem_value parent st val_exp v -> - sem_val_list parent st args lv -> - Op.eval_addressing genv (sem_state_stackp st) addr lv = Some a -> - Memory.Mem.storev chunk m' a v = Some m'' -> - sem_mem parent st (Estore mem_exp chunk addr args val_exp) m'' - | Sbase_mem : - forall parent st m, - sem_mem parent st (Ebase Mem) m -with sem_val_list : - val -> sem_state -> expression_list -> list val -> Prop := - | Snil : - forall parent st, - sem_val_list parent st Enil nil - | Scons : - forall parent st e v l lv, - sem_value parent st e v -> - sem_val_list parent st l lv -> - sem_val_list parent st (Econs e l) (v :: lv). - -Inductive sem_regset : - val -> sem_state -> forest -> regset -> Prop := - | Sregset: - forall parent st f rs', - (forall x, sem_value parent st (f # (Reg x)) (Registers.Regmap.get x rs')) -> - sem_regset parent st f rs'. - -Inductive sem : - val -> sem_state -> forest -> sem_state -> Prop := - | Sem: - forall st rs' fr' m' f parent, - sem_regset parent st f rs' -> - sem_mem parent st (f # Mem) m' -> - sem parent st fr' (mk_sem_state (sem_state_stackp st) rs' m'). - - -End SEMANTICS. - -Fixpoint beq_expression (e1 e2: expression) {struct e1}: bool := - match e1, e2 with - | Ebase r1, Ebase r2 => if resource_eq r1 r2 then true else false - | Eop op1 el1, Eop op2 el2 => - if operation_eq op1 op2 then beq_expression_list el1 el2 else false - | Eload chk1 addr1 el1 e1, Eload chk2 addr2 el2 e2 => - if memory_chunk_eq chk1 chk2 - then if addressing_eq addr1 addr2 - then if beq_expression_list el1 el2 - then beq_expression e1 e2 else false else false else false - | Estore m1 chk1 addr1 el1 e1, Estore m2 chk2 addr2 el2 e2=> - if memory_chunk_eq chk1 chk2 - then if addressing_eq addr1 addr2 - then if beq_expression_list el1 el2 - then if beq_expression m1 m2 - then beq_expression e1 e2 else false else false else false else false - | _, _ => false - end -with beq_expression_list (el1 el2: expression_list) {struct el1} : bool := - match el1, el2 with - | Enil, Enil => true - | Econs e1 t1, Econs e2 t2 => beq_expression e1 e2 && beq_expression_list t1 t2 - | _, _ => false - end. - -Scheme expression_ind2 := Induction for expression Sort Prop - with expression_list_ind2 := Induction for expression_list Sort Prop. - -Lemma beq_expression_correct: - forall e1 e2, beq_expression e1 e2 = true -> e1 = e2. -Proof. - 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); 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 _. - -(*| -This function checks if all the elements in [fa] are in [fb], but not the other way round. -|*) - -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; - 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; 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. - -Lemma map1: - forall w dst dst', - dst <> dst' -> - (empty # dst <- w) # dst' = Ebase dst'. -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; auto. Qed. - -Lemma map2: - forall (v : expression) x rs, - (rs # x <- v) # x = v. -Proof. intros; unfold get_forest; rewrite Rtree.gss; trivial. Qed. - -Lemma tri1: - forall x y, - Reg x <> Reg y -> x <> y. -Proof. unfold not; intros; subst; auto. Qed. - -(*| -Update functions. -|*) - -Fixpoint list_translation (l : list reg) (f : forest) {struct l} : expression_list := - match l with - | nil => Enil - | i :: l => Econs (f # (Reg i)) (list_translation l f) - end. - -Definition update (f : forest) (i : instr) : forest := - match i with - | RBnop => f - | RBop op rl r => - f # (Reg r) <- (Eop op (list_translation rl f)) - | RBload chunk addr rl r => - f # (Reg r) <- (Eload chunk addr (list_translation rl f) (f # Mem)) - | RBstore chunk addr rl r => - f # Mem <- (Estore (f # Mem) chunk addr (list_translation rl f) (f # (Reg r))) - 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. -|*) - -Fixpoint abstract_sequence (f : forest) (b : list instr) : forest := - match b with - | nil => f - | i :: l => abstract_sequence (update f i) l - end. - -Fixpoint abstract_sequence_par (f : forest) (b : list (list instr)) : forest := - match b with - | nil => f - | i :: l => abstract_sequence_par (abstract_sequence f i) l - end. - -(*| -Check equivalence of control flow instructions. As none of the basic blocks should have been moved, -none of the labels should be different, meaning the control-flow instructions should match exactly. -|*) - -Definition check_control_flow_instr (c1 c2: cf_instr) : bool := - if cf_instr_eq c1 c2 then true else false. - -(*| -We define the top-level oracle that will check if two basic blocks are equivalent after a scheduling -transformation. -|*) - -Definition schedule_oracle (bb : RTLBlock.bblock) (bbt : RTLPar.bblock) : bool := - check (abstract_sequence empty (bb_body bb)) - (abstract_sequence_par empty (bb_body bbt)). -- cgit