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 +++++++++++++++++++++++++++++++++++++++++++++++++++- 1 file changed, 515 insertions(+), 3 deletions(-) (limited to 'src/hls/RTLPargen.v') 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."). -- cgit