From 9e2aca04a7af7987fb8226fb9e211194a7f195ff Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Mon, 11 Jan 2021 18:06:03 +0000 Subject: Add equality check for symbolic expressions --- src/hls/Scheduleoracle.v | 347 +++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 347 insertions(+) create mode 100644 src/hls/Scheduleoracle.v (limited to 'src') diff --git a/src/hls/Scheduleoracle.v b/src/hls/Scheduleoracle.v new file mode 100644 index 0000000..bc62d47 --- /dev/null +++ b/src/hls/Scheduleoracle.v @@ -0,0 +1,347 @@ +(* + * 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 Import Globalenvs Values Integers Floats. +Require RTLBlock RTLPar Op Memory AST Registers. +Require Import 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 instruction_eq: forall (x y : RTLBlock.instruction), {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. + +(*| +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; intro; try (simpl in H; congruence). + 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 Rmap := Maps.IMap(R_indexed). + +Definition regset := Registers.Regmap.t val. + +Notation "a # b" := (Rmap.get b a) (at level 1). +Notation "a # b <- c" := (Rmap.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). + +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). + (* 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. +Qed. + +(*| +We define the top-level oracle that will check if two basic blocks are equivalent after a scheduling +transformation. +|*) + +Definition schedule_oracle (p : RTLBlock.bblock) (pt : RTLPar.bblock) : bool := + true. -- cgit