From b431bdeb59e69df41cd98fadea49968d224493ee Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Mon, 31 Aug 2020 22:37:44 +0100 Subject: Add working partitioning algorithm --- src/hls/Partition.ml | 79 +++++++++++++++++++------------ src/hls/PrintRTLBlock.ml | 119 +++++++++++++++++++++++++++++++++++++++++++++++ src/hls/RTLBlock.v | 4 +- src/hls/RTLBlockgen.v | 15 ++---- 4 files changed, 175 insertions(+), 42 deletions(-) diff --git a/src/hls/Partition.ml b/src/hls/Partition.ml index 105dcdd..1c25cdc 100644 --- a/src/hls/Partition.ml +++ b/src/hls/Partition.ml @@ -1,4 +1,4 @@ -(* + (* * Vericert: Verified high-level synthesis. * Copyright (C) 2020 Yann Herklotz * @@ -29,12 +29,15 @@ 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_backedge i n = +let find_edge i n = let succ = RTL.successors_instr i in - List.filter (fun s -> P.lt n s) succ + let filt = List.filter (fun s -> P.lt n s || P.lt s (P.pred n)) succ in + (begin match filt with [] -> [] | _ -> [n] end, filt) -let find_backedges c = - PTree.fold (fun l n i -> List.append (find_backedge i n) l) c [] +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} @@ -55,47 +58,63 @@ let translate_cfi = function | RTL.Ireturn r -> Some (RBreturn r) | _ -> None -let rec next_bblock_from_RTL (c : RTL.code) i = - let succ = List.map (fun i -> PTree.get i c) (RTL.successors_instr i) in +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 - | (Some i', _), Some i::[] -> begin - match next_bblock_from_RTL c i with - | Errors.OK bb -> Errors.OK (prepend_instr i' bb) + | (None, Some i'), _ -> + Errors.OK {bb_body = []; bb_exit = Some 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 = Some (RBgoto s') } + else if List.exists (fun x -> x = s) (snd e) && not is_start then begin + Errors.OK { bb_body = []; bb_exit = Some (RBgoto s) } + end 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 - | (_, Some i'), _ -> - Errors.OK {bb_body = []; bb_exit = Some i'} - | _, _ -> Errors.Error (Errors.msg (coqstring_of_camlstring "next_bblock_from_RTL went wrong.")) + | _, _ -> + Errors.Error (Errors.msg (coqstring_of_camlstring "next_bblock_from_RTL went wrong.")) -let rec traverselist f l = +let rec traverseacc f l c = match l with - | [] -> Errors.OK [] + | [] -> Errors.OK c | x::xs -> - match f x with + match f x c with | Errors.Error msg -> Errors.Error msg | Errors.OK x' -> - match traverselist f xs with + match traverseacc f xs x' with | Errors.Error msg -> Errors.Error msg - | Errors.OK xs' -> - Errors.OK (x'::xs') + | Errors.OK xs' -> Errors.OK xs' -let rec translate_all start c = - match PTree.get start c with +let rec translate_all edge c s c_bb = + 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 c i with + match next_bblock_from_RTL true edge c s i with | Errors.Error msg -> Errors.Error msg + | Errors.OK {bb_exit = None; _} -> + Errors.Error (Errors.msg (coqstring_of_camlstring "Error in translate all")) | Errors.OK {bb_body = bb; bb_exit = Some e} -> let succ = successors_instr e in - match traverselist (fun s -> translate_all s c) succ with - | Errors.OK l -> + match traverseacc (translate_all edge c) succ c_bb with + | Errors.Error msg -> Errors.Error msg + | Errors.OK c' -> + Errors.OK (PTree.set s {bb_body = bb; bb_exit = Some e} c') (* Partition a function and transform it into RTLBlock. *) let function_from_RTL f = - let ba = find_backedges f.RTL.fn_code in - { fn_sig = f.RTL.fn_entrypoint; - fn_stacksize = f.RTL.fn_stacksize; - fn_entrypoint = f.RTL.fn_entrypoint; - fn_code = f.RTL.fn_code - } + 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 diff --git a/src/hls/PrintRTLBlock.ml b/src/hls/PrintRTLBlock.ml index e69de29..45bd253 100644 --- a/src/hls/PrintRTLBlock.ml +++ b/src/hls/PrintRTLBlock.ml @@ -0,0 +1,119 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + +(** Pretty-printers for RTL code *) + +open Printf +open Camlcoq +open Datatypes +open Maps +open AST +open RTLBlock +open PrintAST + +(* Printing of RTL code *) + +let reg pp r = + fprintf pp "x%d" (P.to_int r) + +let rec regs pp = function + | [] -> () + | [r] -> reg pp r + | r1::rl -> fprintf pp "%a, %a" reg r1 regs rl + +let ros pp = function + | Coq_inl r -> reg pp r + | Coq_inr s -> fprintf pp "\"%s\"" (extern_atom s) + +let print_bblock_body pp i = + fprintf pp "\t\t"; + match i with + | RBnop -> fprintf pp "nop\n" + | RBop(op, ls, dst) -> + fprintf pp "%a = %a\n" + reg dst (PrintOp.print_operation reg) (op, ls) + | RBload(chunk, addr, args, dst) -> + fprintf pp "%a = %s[%a]\n" + reg dst (name_of_chunk chunk) + (PrintOp.print_addressing reg) (addr, args) + | RBstore(chunk, addr, args, src) -> + fprintf pp "%s[%a] = %a\n" + (name_of_chunk chunk) + (PrintOp.print_addressing reg) (addr, args) + reg src + +let print_bblock_exit pp i = + fprintf pp "\t\t"; + match i with + | Some(RBcall(_, fn, args, res, _)) -> + fprintf pp "%a = %a(%a)\n" + reg res ros fn regs args; + | Some(RBtailcall(_, fn, args)) -> + fprintf pp "tailcall %a(%a)\n" + ros fn regs args + | Some(RBbuiltin(ef, args, res, _)) -> + fprintf pp "%a = %s(%a)\n" + (print_builtin_res reg) res + (name_of_external ef) + (print_builtin_args reg) args + | Some(RBcond(cond, args, s1, s2)) -> + fprintf pp "if (%a) goto %d else goto %d\n" + (PrintOp.print_condition reg) (cond, args) + (P.to_int s1) (P.to_int s2) + | Some(RBjumptable(arg, tbl)) -> + let tbl = Array.of_list tbl in + fprintf pp "jumptable (%a)\n" reg arg; + for i = 0 to Array.length tbl - 1 do + fprintf pp "\tcase %d: goto %d\n" i (P.to_int tbl.(i)) + done + | Some(RBreturn None) -> + fprintf pp "return\n" + | Some(RBreturn (Some arg)) -> + fprintf pp "return %a\n" reg arg + | Some(RBgoto n) -> + fprintf pp "goto %d\n" (P.to_int n) + | None -> fprintf pp "\n" + +let print_bblock pp (pc, i) = + fprintf pp "%5d:{\n" pc; + List.iter (print_bblock_body pp) i.bb_body; + print_bblock_exit pp i.bb_exit; + fprintf pp "\t}\n\n" + +let print_function pp id f = + fprintf pp "%s(%a) {\n" (extern_atom id) regs f.fn_params; + let instrs = + List.sort + (fun (pc1, _) (pc2, _) -> compare pc2 pc1) + (List.rev_map + (fun (pc, i) -> (P.to_int pc, i)) + (PTree.elements f.fn_code)) in + List.iter (print_bblock pp) instrs; + fprintf pp "}\n\n" + +let print_globdef pp (id, gd) = + match gd with + | Gfun(Internal f) -> print_function pp id f + | _ -> () + +let print_program pp (prog: program) = + List.iter (print_globdef pp) prog.prog_defs + +let destination : string option ref = ref None + +let print_if prog = + match !destination with + | None -> () + | Some f -> + let oc = open_out f in + print_program oc prog; + close_out oc diff --git a/src/hls/RTLBlock.v b/src/hls/RTLBlock.v index 2aaa010..a1c3f25 100644 --- a/src/hls/RTLBlock.v +++ b/src/hls/RTLBlock.v @@ -41,7 +41,8 @@ Inductive control_flow_inst : Type := builtin_res reg -> node -> control_flow_inst | RBcond : condition -> list reg -> node -> node -> control_flow_inst | RBjumptable : reg -> list node -> control_flow_inst -| RBreturn : option reg -> control_flow_inst. +| RBreturn : option reg -> control_flow_inst +| RBgoto : node -> control_flow_inst. Record bblock : Type := mk_bblock { bb_body: bblock_body; @@ -76,4 +77,5 @@ Definition successors_instr (i : control_flow_inst) : list node := | RBcond cond args ifso ifnot => ifso :: ifnot :: nil | RBjumptable arg tbl => tbl | RBreturn optarg => nil + | RBgoto n => n :: nil end. diff --git a/src/hls/RTLBlockgen.v b/src/hls/RTLBlockgen.v index 05f9a32..6b3e9c3 100644 --- a/src/hls/RTLBlockgen.v +++ b/src/hls/RTLBlockgen.v @@ -24,16 +24,9 @@ From compcert Require Import From vericert Require Import RTLBlock. -Parameter partition : RTL.code -> code. +Parameter partition : RTL.function -> Errors.res function. -Definition transl_function (f : RTL.function) : function := - mkfunction f.(RTL.fn_sig) - f.(RTL.fn_params) - f.(RTL.fn_stacksize) - (partition f.(RTL.fn_code)) - f.(RTL.fn_entrypoint). +Definition transl_fundef := transf_partial_fundef partition. -Definition transl_fundef := transf_fundef transl_function. - -Definition transl_program : RTL.program -> program := - transform_program transl_fundef. +Definition transl_program : RTL.program -> Errors.res program := + transform_partial_program transl_fundef. -- cgit