diff options
Diffstat (limited to 'docs/basic-block-generation.org')
| -rw-r--r-- | docs/basic-block-generation.org | 497 |
1 files changed, 497 insertions, 0 deletions
diff --git a/docs/basic-block-generation.org b/docs/basic-block-generation.org new file mode 100644 index 0000000..1d78dad --- /dev/null +++ b/docs/basic-block-generation.org @@ -0,0 +1,497 @@ +#+title: Basic Block Generation +#+author: Yann Herklotz +#+email: yann [at] yannherklotz [dot] com + +* RTLBlockgen +:PROPERTIES: +:header-args:coq: :comments noweb :noweb no-export :padline yes :tangle ../src/hls/RTLBlockgen.v +:END: + +Refers to [[rtlblockgen-equalities][rtlblockgen-equalities]]. + +#+begin_src coq :comments no :padline no :exports none +<<license>> +#+end_src + +#+name: rtlblockgen-imports +#+begin_src coq +Require compcert.backend.RTL. +Require Import compcert.common.AST. +Require Import compcert.lib.Maps. +Require Import compcert.lib.Integers. +Require Import compcert.lib.Floats. + +Require Import vericert.common.Vericertlib. +Require Import vericert.hls.RTLBlockInstr. +Require Import vericert.hls.RTLBlock. + +#[local] Open Scope positive. +#+end_src + +#+name: rtlblockgen-equalities-insert +#+begin_src coq :comments no +<<rtlblockgen-equalities>> +#+end_src + +#+name: rtlblockgen-main +#+begin_src coq +Parameter partition : RTL.function -> Errors.res function. + +(** [find_block max nodes index]: Does not need to be sorted, because we use filter and the max fold + function to find the desired element. *) +Definition find_block (max: positive) (nodes: list positive) (index: positive) : positive := + List.fold_right Pos.min max (List.filter (fun x => (index <=? x)) nodes). + +(*Compute find_block (2::94::28::40::19::nil) 40.*) + +Definition check_instr (n: positive) (istr: RTL.instruction) (istr': instr) := + match istr, istr' with + | RTL.Inop n', RBnop => (n' + 1 =? n) + | RTL.Iop op args dst n', RBop None op' args' dst' => + ceq operation_eq op op' && + ceq list_pos_eq args args' && + ceq peq dst dst' && (n' + 1 =? n) + | RTL.Iload chunk addr args dst n', RBload None chunk' addr' args' dst' => + ceq memory_chunk_eq chunk chunk' && + ceq addressing_eq addr addr' && + ceq list_pos_eq args args' && + ceq peq dst dst' && + (n' + 1 =? n) + | RTL.Istore chunk addr args src n', RBstore None chunk' addr' args' src' => + ceq memory_chunk_eq chunk chunk' && + ceq addressing_eq addr addr' && + ceq list_pos_eq args args' && + ceq peq src src' && + (n' + 1 =? n) + | _, _ => false + end. + +Definition check_cf_instr_body (istr: RTL.instruction) (istr': instr): bool := + match istr, istr' with + | RTL.Iop op args dst _, RBop None op' args' dst' => + ceq operation_eq op op' && + ceq list_pos_eq args args' && + ceq peq dst dst' + | RTL.Iload chunk addr args dst _, RBload None chunk' addr' args' dst' => + ceq memory_chunk_eq chunk chunk' && + ceq addressing_eq addr addr' && + ceq list_pos_eq args args' && + ceq peq dst dst' + | RTL.Istore chunk addr args src _, RBstore None chunk' addr' args' src' => + ceq memory_chunk_eq chunk chunk' && + ceq addressing_eq addr addr' && + ceq list_pos_eq args args' && + ceq peq src src' + | RTL.Inop _, RBnop + | RTL.Icall _ _ _ _ _, RBnop + | RTL.Itailcall _ _ _, RBnop + | RTL.Ibuiltin _ _ _ _, RBnop + | RTL.Icond _ _ _ _, RBnop + | RTL.Ijumptable _ _, RBnop + | RTL.Ireturn _, RBnop => true + | _, _ => false + end. + +Definition check_cf_instr (istr: RTL.instruction) (istr': cf_instr) := + match istr, istr' with + | RTL.Inop n, RBgoto n' => (n =? n') + | RTL.Iop _ _ _ n, RBgoto n' => (n =? n') + | RTL.Iload _ _ _ _ n, RBgoto n' => (n =? n') + | RTL.Istore _ _ _ _ n, RBgoto n' => (n =? n') + | RTL.Icall sig (inl r) args dst n, RBcall sig' (inl r') args' dst' n' => + ceq signature_eq sig sig' && + ceq peq r r' && + ceq list_pos_eq args args' && + ceq peq dst dst' && + (n =? n') + | RTL.Icall sig (inr i) args dst n, RBcall sig' (inr i') args' dst' n' => + ceq signature_eq sig sig' && + ceq peq i i' && + ceq list_pos_eq args args' && + ceq peq dst dst' && + (n =? n') + | RTL.Itailcall sig (inl r) args, RBtailcall sig' (inl r') args' => + ceq signature_eq sig sig' && + ceq peq r r' && + ceq list_pos_eq args args' + | RTL.Itailcall sig (inr r) args, RBtailcall sig' (inr r') args' => + ceq signature_eq sig sig' && + ceq peq r r' && + ceq list_pos_eq args args' + | RTL.Icond cond args n1 n2, RBcond cond' args' n1' n2' => + ceq condition_eq cond cond' && + ceq list_pos_eq args args' && + ceq peq n1 n1' && ceq peq n2 n2' + | RTL.Ijumptable r ns, RBjumptable r' ns' => + ceq peq r r' && ceq list_pos_eq ns ns' + | RTL.Ireturn (Some r), RBreturn (Some r') => + ceq peq r r' + | RTL.Ireturn None, RBreturn None => true + | _, _ => false + end. + +Definition is_cf_instr (n: positive) (i: RTL.instruction) := + match i with + | RTL.Inop n' => negb (n' + 1 =? n) + | RTL.Iop _ _ _ n' => negb (n' + 1 =? n) + | RTL.Iload _ _ _ _ n' => negb (n' + 1 =? n) + | RTL.Istore _ _ _ _ n' => negb (n' + 1 =? n) + | RTL.Icall _ _ _ _ _ => true + | RTL.Itailcall _ _ _ => true + | RTL.Ibuiltin _ _ _ _ => true + | RTL.Icond _ _ _ _ => true + | RTL.Ijumptable _ _ => true + | RTL.Ireturn _ => true + end. + +Definition check_present_blocks (c: code) (n: list positive) (max: positive) (i: positive) (istr: RTL.instruction) := + let blockn := find_block max n i in + match c ! blockn with + | Some istrs => + match List.nth_error istrs.(bb_body) (Pos.to_nat blockn - Pos.to_nat i)%nat with + | Some istr' => + if is_cf_instr i istr + then check_cf_instr istr istrs.(bb_exit) && check_cf_instr_body istr istr' + else check_instr i istr istr' + | None => false + end + | None => false + end. + +Definition transl_function (f: RTL.function) := + match partition f with + | Errors.OK f' => + let blockids := map fst (PTree.elements f'.(fn_code)) in + if forall_ptree (check_present_blocks f'.(fn_code) blockids (fold_right Pos.max 1 blockids)) + f.(RTL.fn_code) then + Errors.OK f' + else Errors.Error (Errors.msg "check_present_blocks failed") + | Errors.Error msg => Errors.Error msg + end. + +Definition transl_fundef := transf_partial_fundef transl_function. + +Definition transl_program : RTL.program -> Errors.res program := + transform_partial_program transl_fundef. +#+end_src + +** Equalities + +#+name: rtlblockgen-equalities +#+begin_src coq :tangle no +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_pos_eq : forall (x y : list positive), {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_pos_eq; intro. + generalize AST.ident_eq; intro. + repeat 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_pos_eq; intro. + generalize AST.ident_eq; intro. + repeat decide equality. +Defined. + +Definition ceq {A: Type} (eqd: forall a b: A, {a = b} + {a <> b}) (a b: A): bool := + if eqd a b then true else false. +#+end_src + +* RTLBlockgenproof +:PROPERTIES: +:header-args:coq: :comments noweb :noweb no-export :padline yes :tangle ../src/hls/RTLBlockgenproof.v +:END: + +#+begin_src coq :comments no :padline no :exports none +<<license>> +#+end_src + +** Imports + +#+name: rtlblockgenproof-imports +#+begin_src coq +Require compcert.backend.RTL. +Require Import compcert.common.AST. +Require Import compcert.lib.Maps. + +Require Import vericert.hls.RTLBlock. +Require Import vericert.hls.RTLBlockgen. +#+end_src + +** Match states + +The ~match_states~ predicate describes which states are equivalent between the two languages, in this +case ~RTL~ and ~RTLBlock~. + +#+name: rtlblockgenproof-match-states +#+begin_src coq +Inductive match_states : RTL.state -> RTLBlock.state -> Prop := +| match_state : + forall stk f tf sp pc rs m + (TF: transl_function f = OK tf), + match_states (RTL.State stk f sp pc rs m) + (RTLBlock.State stk tf sp (find_block max n i) rs m). +#+end_src + +** Correctness + +#+name: rtlblockgenproof-correctness +#+begin_src coq +Section CORRECTNESS. + + Context (prog : RTL.program). + Context (tprog : RTLBlock.program). + + Context (TRANSL : match_prog prog tprog). + + Theorem transf_program_correct: + Smallstep.forward_simulation (RTL.semantics prog) (RTLBlock.semantics tprog). + Proof. + eapply Smallstep.forward_simulation_plus; eauto with htlproof. + apply senv_preserved. + +End CORRECTNESS. +#+end_src + +* Partition +:PROPERTIES: +:header-args:ocaml: :comments noweb :noweb no-export :padline yes :tangle ../src/hls/Partition.ml +:END: + +#+begin_src ocaml :comments no :padline no :exports none +<<license>> +#+end_src + +#+name: partition-main +#+begin_src ocaml +open Printf +open Clflags +open Camlcoq +open Datatypes +open Coqlib +open Maps +open AST +open Kildall +open Op +open RTLBlockInstr +open RTLBlock + +(** Assuming that the nodes of the CFG [code] are numbered in reverse postorder (cf. pass + [Renumber]), an edge from [n] to [s] is a normal edge if [s < n] and a back-edge otherwise. *) +let find_edge i n = + let succ = RTL.successors_instr i in + let filt = List.filter (fun s -> P.lt n s || P.lt s (P.pred n)) succ in + ((match filt with [] -> [] | _ -> [n]), filt) + +let find_edges c = + PTree.fold (fun l n i -> + let f = find_edge i n in + (List.append (fst f) (fst l), List.append (snd f) (snd l))) c ([], []) + +let prepend_instr i = function + | {bb_body = bb; bb_exit = e} -> {bb_body = (i :: bb); bb_exit = e} + +let translate_inst = function + | RTL.Inop _ -> Some RBnop + | RTL.Iop (op, ls, dst, _) -> Some (RBop (None, op, ls, dst)) + | RTL.Iload (m, addr, ls, dst, _) -> Some (RBload (None, m, addr, ls, dst)) + | RTL.Istore (m, addr, ls, src, _) -> Some (RBstore (None, m, addr, ls, src)) + | _ -> None + +let translate_cfi = function + | RTL.Icall (s, r, ls, dst, n) -> Some (RBcall (s, r, ls, dst, n)) + | RTL.Itailcall (s, r, ls) -> Some (RBtailcall (s, r, ls)) + | RTL.Ibuiltin (e, ls, r, n) -> Some (RBbuiltin (e, ls, r, n)) + | RTL.Icond (c, ls, dst1, dst2) -> Some (RBcond (c, ls, dst1, dst2)) + | RTL.Ijumptable (r, ls) -> Some (RBjumptable (r, ls)) + | RTL.Ireturn r -> Some (RBreturn r) + | _ -> None + +let rec next_bblock_from_RTL is_start e (c : RTL.code) s i = + let succ = List.map (fun i -> (i, PTree.get i c)) (RTL.successors_instr i) in + let trans_inst = (translate_inst i, translate_cfi i) in + match trans_inst, succ with + | (None, Some i'), _ -> + if List.exists (fun x -> x = s) (snd e) && not is_start then + Errors.OK { bb_body = [RBnop]; bb_exit = RBgoto s } + else + Errors.OK { bb_body = [RBnop]; bb_exit = i' } + | (Some i', None), (s', Some i_n)::[] -> + if List.exists (fun x -> x = s) (fst e) then + Errors.OK { bb_body = [i']; bb_exit = RBgoto s' } + else if List.exists (fun x -> x = s) (snd e) && not is_start then + Errors.OK { bb_body = [RBnop]; bb_exit = RBgoto s } + else begin + match next_bblock_from_RTL false e c s' i_n with + | Errors.OK bb -> + Errors.OK (prepend_instr i' bb) + | Errors.Error msg -> Errors.Error msg + end + | _, _ -> + Errors.Error (Errors.msg (coqstring_of_camlstring "next_bblock_from_RTL went wrong.")) + +let rec traverseacc f l c = + match l with + | [] -> Errors.OK c + | x::xs -> + match f x c with + | Errors.Error msg -> Errors.Error msg + | Errors.OK x' -> + match traverseacc f xs x' with + | Errors.Error msg -> Errors.Error msg + | Errors.OK xs' -> Errors.OK xs' + +let rec translate_all edge c s res = + let c_bb, translated = res in + if List.exists (fun x -> P.eq x s) translated then Errors.OK (c_bb, translated) else + (match PTree.get s c with + | None -> Errors.Error (Errors.msg (coqstring_of_camlstring "Could not translate all.")) + | Some i -> + match next_bblock_from_RTL true edge c s i with + | Errors.Error msg -> Errors.Error msg + | Errors.OK {bb_body = bb; bb_exit = e} -> + let succ = List.filter (fun x -> P.lt x s) (successors_instr e) in + (match traverseacc (translate_all edge c) succ (c_bb, s :: translated) with + | Errors.Error msg -> Errors.Error msg + | Errors.OK (c', t') -> + Errors.OK (PTree.set s {bb_body = bb; bb_exit = e} c', t'))) + +(* Partition a function and transform it into RTLBlock. *) +let function_from_RTL f = + let e = find_edges f.RTL.fn_code in + match translate_all e f.RTL.fn_code f.RTL.fn_entrypoint (PTree.empty, []) with + | Errors.Error msg -> Errors.Error msg + | Errors.OK (c, _) -> + Errors.OK { fn_sig = f.RTL.fn_sig; + fn_stacksize = f.RTL.fn_stacksize; + fn_params = f.RTL.fn_params; + fn_entrypoint = f.RTL.fn_entrypoint; + fn_code = c + } + +let partition = function_from_RTL +#+end_src + +* License + +#+name: license +#+begin_src coq :tangle no +(* + * Vericert: Verified high-level synthesis. + * Copyright (C) 2020-2022 Yann Herklotz <yann@yannherklotz.com> + * + * 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 <https://www.gnu.org/licenses/>. + *) +#+end_src |