diff options
Diffstat (limited to 'src/hls')
| -rw-r--r-- | src/hls/HTLPargen.v | 7 | ||||
| -rw-r--r-- | src/hls/Partition.ml | 124 | ||||
| -rw-r--r-- | src/hls/PrintRTLBlock.ml | 72 | ||||
| -rw-r--r-- | src/hls/PrintRTLBlockInstr.ml | 87 | ||||
| -rw-r--r-- | src/hls/PrintVerilog.ml | 2 | ||||
| -rw-r--r-- | src/hls/RTLBlock.v | 2 | ||||
| -rw-r--r-- | src/hls/RTLBlockInstr.v | 51 | ||||
| -rw-r--r-- | src/hls/RTLPar.v | 2 | ||||
| -rw-r--r-- | src/hls/RTLPargen.v | 288 | ||||
| -rw-r--r-- | src/hls/RTLPargenproof.v | 3 | ||||
| -rw-r--r-- | src/hls/Schedule.ml | 801 |
11 files changed, 219 insertions, 1220 deletions
diff --git a/src/hls/HTLPargen.v b/src/hls/HTLPargen.v index 9746f92..40d1dcc 100644 --- a/src/hls/HTLPargen.v +++ b/src/hls/HTLPargen.v @@ -641,9 +641,9 @@ Definition add_control_instr_force_state_incr : s.(st_arrdecls) s.(st_datapath) (AssocMap.set n st s.(st_controllogic))). -Admitted. +Abort. -Definition add_control_instr_force (n : node) (st : stmnt) : mon unit := +(*Definition add_control_instr_force (n : node) (st : stmnt) : mon unit := fun s => OK tt (mkstate s.(st_st) @@ -708,7 +708,7 @@ Lemma create_new_state_state_incr: s.(st_arrdecls) s.(st_datapath) s.(st_controllogic)). -Admitted. +Abort. Definition create_new_state (p: node): mon node := fun s => OK s.(st_freshstate) @@ -876,3 +876,4 @@ Definition transl_program (p : RTLBlockInstr.program) : Errors.res HTL.program : if main_is_internal p then transform_partial_program transl_fundef p else Errors.Error (Errors.msg "Main function is not Internal."). +*) diff --git a/src/hls/Partition.ml b/src/hls/Partition.ml deleted file mode 100644 index 19c6048..0000000 --- a/src/hls/Partition.ml +++ /dev/null @@ -1,124 +0,0 @@ - (* - * Vericert: Verified high-level synthesis. - * Copyright (C) 2020 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/>. - *) - -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 = []; bb_exit = RBgoto s } - else - Errors.OK { bb_body = []; 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 = []; 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 diff --git a/src/hls/PrintRTLBlock.ml b/src/hls/PrintRTLBlock.ml deleted file mode 100644 index 8fef401..0000000 --- a/src/hls/PrintRTLBlock.ml +++ /dev/null @@ -1,72 +0,0 @@ -(* *********************************************************************) -(* *) -(* 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 RTLBlockInstr -open RTLBlock -open PrintAST -open PrintRTLBlockInstr - -(* 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 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 passno prog = - match !destination with - | None -> () - | Some f -> - let oc = open_out (f ^ "." ^ Z.to_string passno) in - print_program oc prog; - close_out oc diff --git a/src/hls/PrintRTLBlockInstr.ml b/src/hls/PrintRTLBlockInstr.ml deleted file mode 100644 index ba7241b..0000000 --- a/src/hls/PrintRTLBlockInstr.ml +++ /dev/null @@ -1,87 +0,0 @@ -open Printf -open Camlcoq -open Datatypes -open Maps -open AST -open RTLBlockInstr -open PrintAST - -let reg pp r = - fprintf pp "x%d" (P.to_int r) - -let pred pp r = - fprintf pp "p%d" (Nat.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 rec print_pred_op pp = function - | Pvar p -> pred pp p - | Pnot p -> fprintf pp "(~ %a)" print_pred_op p - | Pand (p1, p2) -> fprintf pp "(%a & %a)" print_pred_op p1 print_pred_op p2 - | Por (p1, p2) -> fprintf pp "(%a | %a)" print_pred_op p1 print_pred_op p2 - -let print_pred_option pp = function - | Some x -> fprintf pp "(%a)" print_pred_op x - | None -> () - -let print_bblock_body pp i = - fprintf pp "\t\t"; - match i with - | RBnop -> fprintf pp "nop\n" - | RBop(p, op, ls, dst) -> - fprintf pp "%a %a = %a\n" - print_pred_option p reg dst (PrintOp.print_operation reg) (op, ls) - | RBload(p, chunk, addr, args, dst) -> - fprintf pp "%a %a = %s[%a]\n" - print_pred_option p reg dst (name_of_chunk chunk) - (PrintOp.print_addressing reg) (addr, args) - | RBstore(p, chunk, addr, args, src) -> - fprintf pp "%a %s[%a] = %a\n" - print_pred_option p - (name_of_chunk chunk) - (PrintOp.print_addressing reg) (addr, args) - reg src - | RBsetpred (c, args, p) -> - fprintf pp "%a = %a\n" - pred p - (PrintOp.print_condition reg) (c, args) - -let rec print_bblock_exit pp i = - fprintf pp "\t\t"; - match i with - | RBcall(_, fn, args, res, _) -> - fprintf pp "%a = %a(%a)\n" - reg res ros fn regs args; - | RBtailcall(_, fn, args) -> - fprintf pp "tailcall %a(%a)\n" - ros fn regs args - | RBbuiltin(ef, args, res, _) -> - fprintf pp "%a = %s(%a)\n" - (print_builtin_res reg) res - (name_of_external ef) - (print_builtin_args reg) args - | 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) - | 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 - | RBreturn None -> - fprintf pp "return\n" - | RBreturn (Some arg) -> - fprintf pp "return %a\n" reg arg - | RBgoto n -> - fprintf pp "goto %d\n" (P.to_int n) - | RBpred_cf (p, c1, c2) -> - fprintf pp "if %a then (%a) else (%a)\n" print_pred_op p print_bblock_exit c1 print_bblock_exit c2 diff --git a/src/hls/PrintVerilog.ml b/src/hls/PrintVerilog.ml index a2700a1..a5fa554 100644 --- a/src/hls/PrintVerilog.ml +++ b/src/hls/PrintVerilog.ml @@ -75,7 +75,7 @@ let pprint_binop l r = let unop = function | Vneg -> " - " - | Vnot -> " ! " + | Vnot -> " ~ " let register a = match PMap.find_opt a !name_map with diff --git a/src/hls/RTLBlock.v b/src/hls/RTLBlock.v index aaa3c6c..bf5c37a 100644 --- a/src/hls/RTLBlock.v +++ b/src/hls/RTLBlock.v @@ -60,7 +60,7 @@ Section RELSEM. | exec_bblock: forall s f sp pc rs rs' m m' t s' bb pr pr', f.(fn_code)!pc = Some bb -> - step_instr_list sp (InstrState rs pr m) bb.(bb_body) (InstrState rs' pr' m') -> + step_instr_list sp (mk_instr_state rs pr m) bb.(bb_body) (mk_instr_state rs' pr' m') -> step_cf_instr ge (State s f sp pc rs' pr' m') bb.(bb_exit) t s' -> step (State s f sp pc rs pr m) t s' | exec_function_internal: diff --git a/src/hls/RTLBlockInstr.v b/src/hls/RTLBlockInstr.v index c1d74b5..8cd3468 100644 --- a/src/hls/RTLBlockInstr.v +++ b/src/hls/RTLBlockInstr.v @@ -183,36 +183,36 @@ Fixpoint trans_pred (bound: nat) (p: pred_op) : | Pvar p' => Some (exist _ (((true, Pos.to_nat p') :: nil) :: nil) _) | Pand p1 p2 => match trans_pred n p1, trans_pred n p2 with - | Some (exist p1' _), Some (exist p2' _) => + | Some (exist _ p1' _), Some (exist _ p2' _) => Some (exist _ (p1' ++ p2') _) | _, _ => None end | Por p1 p2 => match trans_pred n p1, trans_pred n p2 with - | Some (exist p1' _), Some (exist p2' _) => + | Some (exist _ p1' _), Some (exist _ p2' _) => Some (exist _ (mult p1' p2') _) | _, _ => None end - | Pnot (Pvar p') => Some (exist _ (((false, p') :: nil) :: nil) _) + | Pnot (Pvar p') => Some (exist _ (((false, Pos.to_nat p') :: nil) :: nil) _) | Pnot (Pnot p') => match trans_pred n p' with - | Some (exist p1' _) => Some (exist _ p1' _) + | Some (exist _ p1' _) => Some (exist _ p1' _) | None => None end | Pnot (Pand p1 p2) => match trans_pred n (Por (Pnot p1) (Pnot p2)) with - | Some (exist p1' _) => Some (exist _ p1' _) + | Some (exist _ p1' _) => Some (exist _ p1' _) | None => None end | Pnot (Por p1 p2) => match trans_pred n (Pand (Pnot p1) (Pnot p2)) with - | Some (exist p1' _) => Some (exist _ p1' _) + | Some (exist _ p1' _) => Some (exist _ p1' _) | None => None end end end); split; intros; simpl in *; auto. - inv H. inv H0; auto. - - split; auto. destruct (a p') eqn:?; crush. + - split; auto. destruct (a (Pos.to_nat p')) eqn:?; crush. - inv H. inv H0. unfold satLit in H. simplify. rewrite H. auto. crush. - rewrite negb_involutive in H. apply i in H. auto. @@ -239,9 +239,9 @@ Definition sat_pred (bound: nat) (p: pred_op) : + {forall a : asgn, sat_predicate p a = false}). refine ( match trans_pred bound p with - | Some (exist fm _) => + | Some (exist _ fm _) => match boundedSat bound fm with - | Some (inleft (exist a _)) => Some (inleft (exist _ a _)) + | Some (inleft (exist _ a _)) => Some (inleft (exist _ a _)) | Some (inright _) => Some (inright _) | None => None end @@ -255,7 +255,7 @@ Qed. Definition sat_pred_simple (bound: nat) (p: pred_op) := match sat_pred bound p with - | Some (inleft (exist al _)) => Some (Some al) + | Some (inleft (exist _ al _)) => Some (Some al) | Some (inright _) => Some None | None => None end. @@ -347,12 +347,11 @@ Fixpoint init_regs (vl: list val) (rl: list reg) {struct rl} : regset := | _, _ => Regmap.init Vundef end. -Inductive instr_state : Type := -| InstrState: - forall (rs: regset) - (pr: predset) - (m: mem), - instr_state. +Record instr_state := mk_instr_state { + instr_st_regset: regset; + instr_st_predset: predset; + instr_st_mem: mem; +}. Section DEFINITION. @@ -440,11 +439,11 @@ Section RELSEM. | eval_pred_true: forall (pr: predset) p rs pr m i, eval_predf pr p = true -> - eval_pred (Some p) (InstrState rs pr m) i i + eval_pred (Some p) (mk_instr_state rs pr m) i i | eval_pred_false: forall (pr: predset) p rs pr m i, eval_predf pr p = false -> - eval_pred (Some p) (InstrState rs pr m) i (InstrState rs pr m) + eval_pred (Some p) (mk_instr_state rs pr m) i (mk_instr_state rs pr m) | eval_pred_none: forall i i', eval_pred None i i' i. @@ -456,25 +455,25 @@ Section RELSEM. | exec_RBop: forall op v res args rs m sp p ist pr, eval_operation ge sp op rs##args m = Some v -> - eval_pred p (InstrState rs pr m) (InstrState (rs#res <- v) pr m) ist -> - step_instr sp (InstrState rs pr m) (RBop p op args res) ist + eval_pred p (mk_instr_state rs pr m) (mk_instr_state (rs#res <- v) pr m) ist -> + step_instr sp (mk_instr_state rs pr m) (RBop p op args res) ist | exec_RBload: forall addr rs args a chunk m v dst sp p pr ist, eval_addressing ge sp addr rs##args = Some a -> Mem.loadv chunk m a = Some v -> - eval_pred p (InstrState rs pr m) (InstrState (rs#dst <- v) pr m) ist -> - step_instr sp (InstrState rs pr m) (RBload p chunk addr args dst) ist + eval_pred p (mk_instr_state rs pr m) (mk_instr_state (rs#dst <- v) pr m) ist -> + step_instr sp (mk_instr_state rs pr m) (RBload p chunk addr args dst) ist | exec_RBstore: forall addr rs args a chunk m src m' sp p pr ist, eval_addressing ge sp addr rs##args = Some a -> Mem.storev chunk m a rs#src = Some m' -> - eval_pred p (InstrState rs pr m) (InstrState rs pr m') ist -> - step_instr sp (InstrState rs pr m) (RBstore p chunk addr args src) ist + eval_pred p (mk_instr_state rs pr m) (mk_instr_state rs pr m') ist -> + step_instr sp (mk_instr_state rs pr m) (RBstore p chunk addr args src) ist | exec_RBsetpred: forall sp rs pr m p c b args, Op.eval_condition c rs##args m = Some b -> - step_instr sp (InstrState rs pr m) (RBsetpred c args p) - (InstrState rs (PMap.set p b pr) m). + step_instr sp (mk_instr_state rs pr m) (RBsetpred c args p) + (mk_instr_state rs (PMap.set p b pr) m). Inductive step_cf_instr: state -> cf_instr -> trace -> state -> Prop := | exec_RBcall: diff --git a/src/hls/RTLPar.v b/src/hls/RTLPar.v index 9d5fc77..4986cff 100644 --- a/src/hls/RTLPar.v +++ b/src/hls/RTLPar.v @@ -82,7 +82,7 @@ Section RELSEM. | exec_bblock: forall s f sp pc rs rs' m m' t s' bb pr pr', f.(fn_code)!pc = Some bb -> - step_instr_block sp (InstrState rs pr m) bb.(bb_body) (InstrState rs' pr' m') -> + step_instr_block sp (mk_instr_state rs pr m) bb.(bb_body) (mk_instr_state rs' pr' m') -> step_cf_instr ge (State s f sp pc rs' pr' m') bb.(bb_exit) t s' -> step (State s f sp pc rs pr m) t s' | exec_function_internal: diff --git a/src/hls/RTLPargen.v b/src/hls/RTLPargen.v index 00adc32..09eabc9 100644 --- a/src/hls/RTLPargen.v +++ b/src/hls/RTLPargen.v @@ -31,6 +31,8 @@ Require Import vericert.hls.RTLBlock. Require Import vericert.hls.RTLPar. Require Import vericert.hls.RTLBlockInstr. +#[local] Open Scope positive. + (*| Schedule Oracle =============== @@ -216,26 +218,27 @@ Inductive expression : Type := | Eload : AST.memory_chunk -> Op.addressing -> expression_list -> expression -> expression | Estore : expression -> AST.memory_chunk -> Op.addressing -> expression_list -> expression -> expression | Esetpred : predicate -> Op.condition -> expression_list -> expression -> expression -| Econd : expr_pred_list -> expression with expression_list : Type := | Enil : expression_list | Econs : expression -> expression_list -> expression_list -with expr_pred_list : Type := -| EPnil : expr_pred_list -| EPcons : pred_op -> expression -> expr_pred_list -> expr_pred_list . +Inductive pred_expr : Type := +| PEsingleton : option pred_op -> expression -> pred_expr +| PEcons : pred_op -> expression -> pred_expr -> pred_expr. + Definition pred_list_wf l : Prop := forall a b, In a l -> In b l -> a <> b -> unsat (Pand a b). -Fixpoint expr_pred_list_to_list e := - match e with - | EPnil => nil - | EPcons p e l => (p, e) :: expr_pred_list_to_list l +Fixpoint pred_expr_list (p: pred_expr) := + match p with + | PEsingleton None _ => nil + | PEsingleton (Some pr) e => (pr, e) :: nil + | PEcons pr e p' => (pr, e) :: pred_expr_list p' end. -Definition pred_list_wf_ep l : Prop := - pred_list_wf (map fst (expr_pred_list_to_list l)). +Definition pred_list_wf_ep (l: pred_expr) : Prop := + pred_list_wf (map fst (pred_expr_list l)). Lemma unsat_correct1 : forall a b c, @@ -380,11 +383,11 @@ identified as positive numbers. Module Rtree := ITree(R_indexed). -Definition forest : Type := Rtree.t expression. +Definition forest : Type := Rtree.t pred_expr. -Definition get_forest v f := +Definition get_forest v (f: forest) := match Rtree.get v f with - | None => Ebase v + | None => PEsingleton None (Ebase v) | Some v' => v' end. @@ -397,9 +400,9 @@ Definition maybe {A: Type} (vo: A) (pr: predset) p (v: A) := | None => v end. -Definition get_pr i := match i with InstrState a b c => b end. +Definition get_pr i := match i with mk_instr_state a b c => b end. -Definition get_m i := match i with InstrState a b c => c end. +Definition get_m i := match i with mk_instr_state a b c => c end. Definition eval_predf_opt pr p := match p with Some p' => eval_predf pr p' | None => true end. @@ -417,13 +420,13 @@ Inductive sem_value : val -> instr_state -> expression -> val -> Prop := | Sbase_reg: forall sp rs r m pr, - sem_value sp (InstrState rs pr m) (Ebase (Reg r)) (rs !! r) + sem_value sp (mk_instr_state rs pr m) (Ebase (Reg r)) (rs !! r) | Sop: forall rs m op args v lv sp m' mem_exp pr, - sem_mem sp (InstrState rs pr m) mem_exp m' -> - sem_val_list sp (InstrState rs pr m) args lv -> + sem_mem sp (mk_instr_state rs pr m) mem_exp m' -> + sem_val_list sp (mk_instr_state rs pr m) args lv -> Op.eval_operation genv sp op lv m' = Some v -> - sem_value sp (InstrState rs pr m) (Eop op args mem_exp) v + sem_value sp (mk_instr_state rs pr m) (Eop op args mem_exp) v | Sload : forall st mem_exp addr chunk args a v m' lv sp, sem_mem sp st mem_exp m' -> @@ -431,21 +434,17 @@ Inductive sem_value : Op.eval_addressing genv sp addr lv = Some a -> Memory.Mem.loadv chunk m' a = Some v -> sem_value sp st (Eload chunk addr args mem_exp) v -| Scond : - forall sp st e v, - sem_val_ep_list sp st e v -> - sem_value sp st (Econd e) v with sem_pred : val -> instr_state -> expression -> bool -> Prop := | Spred: - forall st mem_exp args p c lv m m' v sp, - sem_mem sp st mem_exp m' -> + forall st pred_exp args p c lv m m' v sp, + sem_pred sp st pred_exp m' -> sem_val_list sp st args lv -> Op.eval_condition c lv m = Some v -> - sem_pred sp st (Esetpred p c args mem_exp) v + sem_pred sp st (Esetpred p c args pred_exp) v | Sbase_pred: forall rs pr m p sp, - sem_pred sp (InstrState rs pr m) (Ebase (Pred p)) (PMap.get p pr) + sem_pred sp (mk_instr_state rs pr m) (Ebase (Pred p)) (PMap.get p pr) with sem_mem : val -> instr_state -> expression -> Memory.mem -> Prop := | Sstore : @@ -458,7 +457,7 @@ with sem_mem : sem_mem sp st (Estore mem_exp chunk addr args val_exp) m'' | Sbase_mem : forall rs m sp pr, - sem_mem sp (InstrState rs pr m) (Ebase Mem) m + sem_mem sp (mk_instr_state rs pr m) (Ebase Mem) m with sem_val_list : val -> instr_state -> expression_list -> list val -> Prop := | Snil : @@ -469,35 +468,51 @@ with sem_val_list : sem_value sp st e v -> sem_val_list sp st l lv -> sem_val_list sp st (Econs e l) (v :: lv) -with sem_val_ep_list : - val -> instr_state -> expr_pred_list -> val -> Prop := -| SPnil : - forall sp rs r m pr, - sem_val_ep_list sp (InstrState rs pr m) EPnil (rs !! r) -| SPconsTrue : - forall pr p sp rs m e v el, - eval_predf pr p = true -> - sem_value sp (InstrState rs pr m) e v -> - sem_val_ep_list sp (InstrState rs pr m) (EPcons p e el) v -| SPconsFalse : - forall pr p sp rs m e v el, - eval_predf pr p = false -> - sem_val_ep_list sp (InstrState rs pr m) el v -> - sem_val_ep_list sp (InstrState rs pr m) (EPcons p e el) v . +Inductive sem_pred_expr {A: Type} (sem: val -> instr_state -> expression -> A -> Prop): + val -> instr_state -> pred_expr -> A -> Prop := +| sem_pred_expr_base : + forall sp st e v, + sem sp st e v -> + sem_pred_expr sem sp st (PEsingleton None e) v +| sem_pred_expr_p : + forall sp st e p v, + eval_predf (instr_st_predset st) p = true -> + sem sp st e v -> + sem_pred_expr sem sp st (PEsingleton (Some p) e) v +| sem_pred_expr_cons_true : + forall sp st e pr p' v, + eval_predf (instr_st_predset st) pr = true -> + sem sp st e v -> + sem_pred_expr sem sp st (PEcons pr e p') v +| sem_pred_expr_cons_false : + forall sp st e pr p' v, + eval_predf (instr_st_predset st) pr = false -> + sem_pred_expr sem sp st p' v -> + sem_pred_expr sem sp st (PEcons pr e p') v +. + +Definition collapse_pe (p: pred_expr) : option expression := + match p with + | PEsingleton None p => Some p + | _ => None + end. + Inductive sem_predset : val -> instr_state -> forest -> predset -> Prop := | Spredset: forall st f sp rs', - (forall x, sem_pred sp st (f # (Pred x)) (PMap.get x rs')) -> + (forall pe x, + collapse_pe (f # (Pred x)) = Some pe -> + sem_pred sp st pe (PMap.get x rs')) -> sem_predset sp st f rs'. Inductive sem_regset : val -> instr_state -> forest -> regset -> Prop := | Sregset: forall st f sp rs', - (forall x, sem_value sp st (f # (Reg x)) (rs' !! x)) -> + (forall x, sem_pred_expr sem_value sp st (f # (Reg x)) (rs' !! x)) -> sem_regset sp st f rs'. Inductive sem : @@ -506,8 +521,8 @@ Inductive sem : forall st rs' m' f sp pr', sem_regset sp st f rs' -> sem_predset sp st f pr' -> - sem_mem sp st (f # Mem) m' -> - sem sp st f (InstrState rs' pr' m'). + sem_pred_expr sem_mem sp st (f # Mem) m' -> + sem sp st f (mk_instr_state rs' pr' m'). End SEMANTICS. @@ -534,7 +549,6 @@ Fixpoint beq_expression (e1 e2: expression) {struct e1}: bool := then if condition_eq c1 c2 then if beq_expression_list el1 el2 then beq_expression m1 m2 else false else false else false - | Econd el1, Econd el2 => beq_expr_pred_list el1 el2 | _, _ => false end with beq_expression_list (el1 el2: expression_list) {struct el1} : bool := @@ -543,17 +557,10 @@ with beq_expression_list (el1 el2: expression_list) {struct el1} : bool := | Econs e1 t1, Econs e2 t2 => beq_expression e1 e2 && beq_expression_list t1 t2 | _, _ => false end -with beq_expr_pred_list (el1 el2: expr_pred_list) {struct el1} : bool := - match el1, el2 with - | EPnil, EPnil => true - | EPcons p1 e1 el1', EPcons p2 e2 el2' => true - | _, _ => false - end . Scheme expression_ind2 := Induction for expression Sort Prop with expression_list_ind2 := Induction for expression_list Sort Prop - with expr_pred_list_ind2 := Induction for expr_pred_list Sort Prop . Lemma beq_expression_correct: @@ -564,38 +571,116 @@ Proof. (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) - (P1 := fun (e1 : expr_pred_list) => - forall e2, beq_expr_pred_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. - eauto using Peqb_true_eq. -Qed. + forall e2, beq_expression_list e1 e2 = true -> e1 = e2); + try solve [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; eauto using Peqb_true_eq]. + destruct e2; try discriminate. eauto. +Abort. + +Definition hash_tree := PTree.t expression. + +Definition find_tree (el: expression) (h: hash_tree) : option positive := + match filter (fun x => beq_expression el (snd x)) (PTree.elements h) with + | (p, _) :: nil => Some p + | _ => None + end. -Definition empty : forest := Rtree.empty _. +Definition combine_option {A} (a b: option A) : option A := + match a, b with + | Some a', _ => Some a' + | _, Some b' => Some b' + | _, _ => None + end. -(*| -This function checks if all the elements in [fa] are in [fb], but not the other way round. -|*) +Definition max_key {A} (t: PTree.t A) := + fold_right Pos.max 1%positive (map fst (PTree.elements t)). + +Definition hash_expr (max: predicate) (e: expression) (h: hash_tree): predicate * hash_tree := + match find_tree e h with + | Some p => (p, h) + | None => + let nkey := Pos.max max (max_key h) + 1 in + (nkey, PTree.set nkey e h) + end. + +Fixpoint encode_expression (max: predicate) (pe: pred_expr) (h: hash_tree): pred_op * hash_tree := + match pe with + | PEsingleton None e => + let (p, h') := hash_expr max e h in + (Pvar p, h') + | PEsingleton (Some p) e => + let (p', h') := hash_expr max e h in + (Por (Pnot p) (Pvar p'), h') + | PEcons p e pe' => + let (p', h') := hash_expr max e h in + let (p'', h'') := encode_expression max pe' h' in + (Pand (Por (Pnot p) (Pvar p')) p'', h'') + end. + +Fixpoint max_predicate (p: pred_op) : positive := + match p with + | Pvar p => p + | Pand a b => Pos.max (max_predicate a) (max_predicate b) + | Por a b => Pos.max (max_predicate a) (max_predicate b) + | Pnot a => max_predicate a + end. + +Fixpoint max_pred_expr (pe: pred_expr) : positive := + match pe with + | PEsingleton None _ => 1 + | PEsingleton (Some p) _ => max_predicate p + | PEcons p _ pe' => Pos.max (max_predicate p) (max_pred_expr pe') + end. + +Definition beq_pred_expr (bound: nat) (pe1 pe2: pred_expr) : bool := + match pe1, pe2 with + (*| PEsingleton None e1, PEsingleton None e2 => beq_expression e1 e2 + | PEsingleton (Some p1) e1, PEsingleton (Some p2) e2 => + if beq_expression e1 e2 + then match sat_pred_simple bound (Por (Pand p1 (Pnot p2)) (Pand p2 (Pnot p1))) with + | Some None => true + | _ => false + end + else false + | PEsingleton (Some p) e1, PEsingleton None e2 + | PEsingleton None e1, PEsingleton (Some p) e2 => + if beq_expression e1 e2 + then match sat_pred_simple bound (Pnot p) with + | Some None => true + | _ => false + end + else false*) + | pe1, pe2 => + let max := Pos.max (max_pred_expr pe1) (max_pred_expr pe2) in + let (p1, h) := encode_expression max pe1 (PTree.empty _) in + let (p2, h') := encode_expression max pe2 h in + match sat_pred_simple bound (Por (Pand p1 (Pnot p2)) (Pand p2 (Pnot p1))) with + | Some None => true + | _ => false + end + end. -Definition check := Rtree.beq beq_expression. +Definition empty : forest := Rtree.empty _. + +Definition check := Rtree.beq (beq_pred_expr 10000). Lemma check_correct: forall (fa fb : forest), check fa fb = true -> (forall x, fa # x = fb # x). Proof. - unfold check, get_forest; intros; + (*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. +Qed.*) + Abort. Lemma get_empty: - forall r, empty#r = Ebase r. + forall r, empty#r = PEsingleton None (Ebase r). Proof. intros; unfold get_forest; destruct_match; auto; [ ]; @@ -647,16 +732,11 @@ Proof. 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. + (empty # dst <- w) # dst' = PEsingleton None (Ebase dst'). +Proof. intros; unfold get_forest; rewrite Rtree.gso; auto; apply get_empty. Qed. Lemma genmap1: forall (f : forest) w dst dst', @@ -665,7 +745,7 @@ Lemma genmap1: Proof. intros; unfold get_forest; rewrite Rtree.gso; auto. Qed. Lemma map2: - forall (v : expression) x rs, + forall (v : pred_expr) x rs, (rs # x <- v) # x = v. Proof. intros; unfold get_forest; rewrite Rtree.gss; trivial. Qed. @@ -692,24 +772,24 @@ Inductive match_states : instr_state -> instr_state -> Prop := forall rs rs' m m', (forall x, rs !! x = rs' !! x) -> m = m' -> - match_states (InstrState rs m) (InstrState rs' m'). + match_states (mk_instr_state rs m) (mk_instr_state rs' m'). Inductive match_states_ld : instr_state -> instr_state -> Prop := | match_states_ld_intro: forall rs rs' m m', regs_lessdef rs rs' -> Mem.extends m m' -> - match_states_ld (InstrState rs m) (InstrState rs' m'). + match_states_ld (mk_instr_state rs m) (mk_instr_state rs' m'). Lemma sems_det: forall A ge tge sp st f, ge_preserved ge tge -> forall v v' mv mv', - (@sem_value A ge sp st f v /\ @sem_value A tge sp st f v' -> v = v') /\ - (@sem_mem A ge sp st f mv /\ @sem_mem A tge sp st f mv' -> mv = mv'). -Proof. Admitted. + (sem_value A ge sp st f v /\ sem_value A tge sp st f v' -> v = v') /\ + (sem_mem A ge sp st f mv /\ sem_mem A tge sp st f mv' -> mv = mv'). +Proof. Abort. -Lemma sem_value_det: +(*Lemma sem_value_det: forall A ge tge sp st f v v', ge_preserved ge tge -> @sem_value A ge sp st f v -> @@ -717,7 +797,7 @@ Lemma sem_value_det: v = v'. Proof. intros. destruct st. - generalize (sems_det A ge tge sp (InstrState rs m) f H v v' + generalize (sems_det A ge tge sp (mk_instr_state rs m) f H v v' m m); crush. Qed. @@ -740,7 +820,7 @@ Lemma sem_mem_det: m = m'. Proof. intros. destruct st. - generalize (sems_det A ge tge sp (InstrState rs m0) f H sp sp m m'); + generalize (sems_det A ge tge sp (mk_instr_state rs m0) f H sp sp m m'); crush. Qed. Hint Resolve sem_mem_det : rtlpar. @@ -884,14 +964,14 @@ Abstract computations ===================== |*) -Definition is_regs i := match i with InstrState rs _ => rs end. -Definition is_mem i := match i with InstrState _ m => m end. +Definition is_regs i := match i with mk_instr_state rs _ => rs end. +Definition is_mem i := match i with mk_instr_state _ m => m end. Inductive state_lessdef : instr_state -> instr_state -> Prop := state_lessdef_intro : forall rs1 rs2 m1, (forall x, rs1 !! x = rs2 !! x) -> - state_lessdef (InstrState rs1 m1) (InstrState rs2 m1). + state_lessdef (mk_instr_state rs1 m1) (mk_instr_state rs2 m1). (*| RTLBlock to abstract translation @@ -1133,9 +1213,9 @@ Lemma sem_update_Op : forall A ge sp st f st' r l o0 o m rs v, @sem A ge sp st f st' -> Op.eval_operation ge sp o0 rs ## l m = Some v -> - match_states st' (InstrState rs m) -> + match_states st' (mk_instr_state rs m) -> exists tst, - sem ge sp st (update f (RBop o o0 l r)) tst /\ match_states (InstrState (Regmap.set r v rs) m) tst. + sem ge sp st (update f (RBop o o0 l r)) tst /\ match_states (mk_instr_state (Regmap.set r v rs) m) tst. Proof. intros. inv H1. simplify. destruct st. @@ -1157,10 +1237,10 @@ Lemma sem_update_load : @sem A ge sp st f st' -> Op.eval_addressing ge sp a rs ## l = Some a0 -> Mem.loadv m m0 a0 = Some v -> - match_states st' (InstrState rs m0) -> + match_states st' (mk_instr_state rs m0) -> exists tst : instr_state, sem ge sp st (update f (RBload o m a l r)) tst - /\ match_states (InstrState (Regmap.set r v rs) m0) tst. + /\ match_states (mk_instr_state (Regmap.set r v rs) m0) tst. Proof. intros. inv H2. pose proof H. inv H. inv H9. destruct st. @@ -1182,9 +1262,9 @@ Lemma sem_update_store : @sem A ge sp st f st' -> Op.eval_addressing ge sp a rs ## l = Some a0 -> Mem.storev m m0 a0 rs !! r = Some m' -> - match_states st' (InstrState rs m0) -> + match_states st' (mk_instr_state rs m0) -> exists tst, sem ge sp st (update f (RBstore o m a l r)) tst - /\ match_states (InstrState rs m') tst. + /\ match_states (mk_instr_state rs m') tst. Proof. intros. inv H2. pose proof H. inv H. inv H9. destruct st. @@ -1214,9 +1294,9 @@ Qed. Lemma sem_update2_Op : forall A ge sp st f r l o0 o m rs v, - @sem A ge sp st f (InstrState rs m) -> + @sem A ge sp st f (mk_instr_state rs m) -> Op.eval_operation ge sp o0 rs ## l m = Some v -> - sem ge sp st (update f (RBop o o0 l r)) (InstrState (Regmap.set r v rs) m). + sem ge sp st (update f (RBop o o0 l r)) (mk_instr_state (Regmap.set r v rs) m). Proof. intros. destruct st. constructor. inv H. inv H6. @@ -1231,10 +1311,10 @@ Qed. Lemma sem_update2_load : forall A ge sp st f r o m a l m0 rs v a0, - @sem A ge sp st f (InstrState rs m0) -> + @sem A ge sp st f (mk_instr_state rs m0) -> Op.eval_addressing ge sp a rs ## l = Some a0 -> Mem.loadv m m0 a0 = Some v -> - sem ge sp st (update f (RBload o m a l r)) (InstrState (Regmap.set r v rs) m0). + sem ge sp st (update f (RBload o m a l r)) (mk_instr_state (Regmap.set r v rs) m0). Proof. intros. simplify. inv H. inv H7. constructor. { constructor; intros. destruct (Pos.eq_dec r x); subst. @@ -1247,10 +1327,10 @@ Qed. Lemma sem_update2_store : forall A ge sp a0 m a l r o f st m' rs m0, - @sem A ge sp st f (InstrState rs m0) -> + @sem A ge sp st f (mk_instr_state rs m0) -> Op.eval_addressing ge sp a rs ## l = Some a0 -> Mem.storev m m0 a0 rs !! r = Some m' -> - sem ge sp st (update f (RBstore o m a l r)) (InstrState rs m'). + sem ge sp st (update f (RBstore o m a l r)) (mk_instr_state rs m'). Proof. intros. simplify. inv H. inv H7. constructor; simplify. { econstructor; intros. rewrite genmap1; crush. } @@ -1563,6 +1643,7 @@ Qed. Proof. intros.*) + (*| Top-level functions =================== @@ -1585,3 +1666,4 @@ Definition transl_fundef := transf_partial_fundef transl_function. Definition transl_program (p : RTLBlock.program) : Errors.res RTLPar.program := transform_partial_program transl_fundef p. +*) diff --git a/src/hls/RTLPargenproof.v b/src/hls/RTLPargenproof.v index c610ff0..bb1cf97 100644 --- a/src/hls/RTLPargenproof.v +++ b/src/hls/RTLPargenproof.v @@ -16,7 +16,7 @@ * along with this program. If not, see <https://www.gnu.org/licenses/>. *) -Require Import compcert.backend.Registers. +(*Require Import compcert.backend.Registers. Require Import compcert.common.AST. Require Import compcert.common.Errors. Require Import compcert.common.Linking. @@ -377,3 +377,4 @@ Proof. induction 2; try rewrite H; eauto with barg. Qed. Qed. End CORRECTNESS. +*) diff --git a/src/hls/Schedule.ml b/src/hls/Schedule.ml deleted file mode 100644 index c6c8bf4..0000000 --- a/src/hls/Schedule.ml +++ /dev/null @@ -1,801 +0,0 @@ -(* - * Vericert: Verified high-level synthesis. - * Copyright (C) 2020 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/>. - *) - -open Printf -open Clflags -open Camlcoq -open Datatypes -open Coqlib -open Maps -open AST -open Kildall -open Op -open RTLBlockInstr -open RTLBlock -open HTL -open Verilog -open HTLgen -open HTLMonad -open HTLMonadExtra - -module SS = Set.Make(P) - -type svtype = - | BBType of int - | VarType of int * int - -type sv = { - sv_type: svtype; - sv_num: int; -} - -let print_sv v = - match v with - | { sv_type = BBType bbi; sv_num = n } -> sprintf "bb%d_%d" bbi n - | { sv_type = VarType (bbi, i); sv_num = n } -> sprintf "var%dn%d_%d" bbi i n - -module G = Graph.Persistent.Digraph.ConcreteLabeled(struct - type t = sv - let compare = compare - let equal = (=) - let hash = Hashtbl.hash -end)(struct - type t = int - let compare = compare - let hash = Hashtbl.hash - let equal = (=) - let default = 0 -end) - -module GDot = Graph.Graphviz.Dot(struct - let graph_attributes _ = [] - let default_vertex_attributes _ = [] - let vertex_name = print_sv - let vertex_attributes _ = [] - let get_subgraph _ = None - let default_edge_attributes _ = [] - let edge_attributes _ = [] - - include G - end) - -module DFG = Graph.Persistent.Digraph.ConcreteLabeled(struct - type t = int * instr - let compare = compare - let equal = (=) - let hash = Hashtbl.hash -end)(struct - type t = int - let compare = compare - let hash = Hashtbl.hash - let equal = (=) - let default = 0 -end) - -let reg r = sprintf "r%d" (P.to_int r) -let print_pred r = sprintf "p%d" (Nat.to_int r) - -let print_instr = function - | RBnop -> "" - | RBload (_, _, _, _, r) -> sprintf "load(%s)" (reg r) - | RBstore (_, _, _, _, r) -> sprintf "store(%s)" (reg r) - | RBsetpred (_, _, p) -> sprintf "setpred(%s)" (print_pred p) - | RBop (_, op, args, d) -> - (match op, args with - | Omove, _ -> "mov" - | Ointconst n, _ -> sprintf "%s=%ld" (reg d) (camlint_of_coqint n) - | Olongconst n, _ -> sprintf "%s=%LdL" (reg d) (camlint64_of_coqint n) - | Ofloatconst n, _ -> sprintf "%s=%.15F" (reg d) (camlfloat_of_coqfloat n) - | Osingleconst n, _ -> sprintf "%s=%.15Ff" (reg d) (camlfloat_of_coqfloat32 n) - | Oindirectsymbol id, _ -> sprintf "%s=&%s" (reg d) (extern_atom id) - | Ocast8signed, [r1] -> sprintf "%s=int8signed(%s)" (reg d) (reg r1) - | Ocast8unsigned, [r1] -> sprintf "%s=int8unsigned(%s)" (reg d) (reg r1) - | Ocast16signed, [r1] -> sprintf "%s=int16signed(%s)" (reg d) (reg r1) - | Ocast16unsigned, [r1] -> sprintf "%s=int16unsigned(%s)" (reg d) (reg r1) - | Oneg, [r1] -> sprintf "%s=-%s" (reg d) (reg r1) - | Osub, [r1;r2] -> sprintf "%s=%s-%s" (reg d) (reg r1) (reg r2) - | Omul, [r1;r2] -> sprintf "%s=%s*%s" (reg d) (reg r1) (reg r2) - | Omulimm n, [r1] -> sprintf "%s=%s*%ld" (reg d) (reg r1) (camlint_of_coqint n) - | Omulhs, [r1;r2] -> sprintf "%s=mulhs(%s,%s)" (reg d) (reg r1) (reg r2) - | Omulhu, [r1;r2] -> sprintf "%s=mulhu(%s,%s)" (reg d) (reg r1) (reg r2) - | Odiv, [r1;r2] -> sprintf "%s=%s /s %s" (reg d) (reg r1) (reg r2) - | Odivu, [r1;r2] -> sprintf "%s=%s /u %s" (reg d) (reg r1) (reg r2) - | Omod, [r1;r2] -> sprintf "%s=%s %%s %s" (reg d) (reg r1) (reg r2) - | Omodu, [r1;r2] -> sprintf "%s=%s %%u %s" (reg d) (reg r1) (reg r2) - | Oand, [r1;r2] -> sprintf "%s=%s & %s" (reg d) (reg r1) (reg r2) - | Oandimm n, [r1] -> sprintf "%s=%s & %ld" (reg d) (reg r1) (camlint_of_coqint n) - | Oor, [r1;r2] -> sprintf "%s=%s | %s" (reg d) (reg r1) (reg r2) - | Oorimm n, [r1] -> sprintf "%s=%s | %ld" (reg d) (reg r1) (camlint_of_coqint n) - | Oxor, [r1;r2] -> sprintf "%s=%s ^ %s" (reg d) (reg r1) (reg r2) - | Oxorimm n, [r1] -> sprintf "%s=%s ^ %ld" (reg d) (reg r1) (camlint_of_coqint n) - | Onot, [r1] -> sprintf "%s=not(%s)" (reg d) (reg r1) - | Oshl, [r1;r2] -> sprintf "%s=%s << %s" (reg d) (reg r1) (reg r2) - | Oshlimm n, [r1] -> sprintf "%s=%s << %ld" (reg d) (reg r1) (camlint_of_coqint n) - | Oshr, [r1;r2] -> sprintf "%s=%s >>s %s" (reg d) (reg r1) (reg r2) - | Oshrimm n, [r1] -> sprintf "%s=%s >>s %ld" (reg d) (reg r1) (camlint_of_coqint n) - | Oshrximm n, [r1] -> sprintf "%s=%s >>x %ld" (reg d) (reg r1) (camlint_of_coqint n) - | Oshru, [r1;r2] -> sprintf "%s=%s >>u %s" (reg d) (reg r1) (reg r2) - | Oshruimm n, [r1] -> sprintf "%s=%s >>u %ld" (reg d) (reg r1) (camlint_of_coqint n) - | Ororimm n, [r1] -> sprintf "%s=%s ror %ld" (reg d) (reg r1) (camlint_of_coqint n) - | Oshldimm n, [r1;r2] -> sprintf "%s=(%s, %s) << %ld" (reg d) (reg r1) (reg r2) (camlint_of_coqint n) - | Olea addr, args -> sprintf "%s=addr" (reg d) - | Omakelong, [r1;r2] -> sprintf "%s=makelong(%s,%s)" (reg d) (reg r1) (reg r2) - | Olowlong, [r1] -> sprintf "%s=lowlong(%s)" (reg d) (reg r1) - | Ohighlong, [r1] -> sprintf "%s=highlong(%s)" (reg d) (reg r1) - | Ocast32signed, [r1] -> sprintf "%s=long32signed(%s)" (reg d) (reg r1) - | Ocast32unsigned, [r1] -> sprintf "%s=long32unsigned(%s)" (reg d) (reg r1) - | Onegl, [r1] -> sprintf "%s=-l %s" (reg d) (reg r1) - | Osubl, [r1;r2] -> sprintf "%s=%s -l %s" (reg d) (reg r1) (reg r2) - | Omull, [r1;r2] -> sprintf "%s=%s *l %s" (reg d) (reg r1) (reg r2) - | Omullimm n, [r1] -> sprintf "%s=%s *l %Ld" (reg d) (reg r1) (camlint64_of_coqint n) - | Omullhs, [r1;r2] -> sprintf "%s=mullhs(%s,%s)" (reg d) (reg r1) (reg r2) - | Omullhu, [r1;r2] -> sprintf "%s=mullhu(%s,%s)" (reg d) (reg r1) (reg r2) - | Odivl, [r1;r2] -> sprintf "%s=%s /ls %s" (reg d) (reg r1) (reg r2) - | Odivlu, [r1;r2] -> sprintf "%s=%s /lu %s" (reg d) (reg r1) (reg r2) - | Omodl, [r1;r2] -> sprintf "%s=%s %%ls %s" (reg d) (reg r1) (reg r2) - | Omodlu, [r1;r2] -> sprintf "%s=%s %%lu %s" (reg d) (reg r1) (reg r2) - | Oandl, [r1;r2] -> sprintf "%s=%s &l %s" (reg d) (reg r1) (reg r2) - | Oandlimm n, [r1] -> sprintf "%s=%s &l %Ld" (reg d) (reg r1) (camlint64_of_coqint n) - | Oorl, [r1;r2] -> sprintf "%s=%s |l %s" (reg d) (reg r1) (reg r2) - | Oorlimm n, [r1] -> sprintf "%s=%s |l %Ld" (reg d) (reg r1) (camlint64_of_coqint n) - | Oxorl, [r1;r2] -> sprintf "%s=%s ^l %s" (reg d) (reg r1) (reg r2) - | Oxorlimm n, [r1] -> sprintf "%s=%s ^l %Ld" (reg d) (reg r1) (camlint64_of_coqint n) - | Onotl, [r1] -> sprintf "%s=notl(%s)" (reg d) (reg r1) - | Oshll, [r1;r2] -> sprintf "%s=%s <<l %s" (reg d) (reg r1) (reg r2) - | Oshllimm n, [r1] -> sprintf "%s=%s <<l %ld" (reg d) (reg r1) (camlint_of_coqint n) - | Oshrl, [r1;r2] -> sprintf "%s=%s >>ls %s" (reg d) (reg r1) (reg r2) - | Oshrlimm n, [r1] -> sprintf "%s=%s >>ls %ld" (reg d) (reg r1) (camlint_of_coqint n) - | Oshrxlimm n, [r1] -> sprintf "%s=%s >>lx %ld" (reg d) (reg r1) (camlint_of_coqint n) - | Oshrlu, [r1;r2] -> sprintf "%s=%s >>lu %s" (reg d) (reg r1) (reg r2) - | Oshrluimm n, [r1] -> sprintf "%s=%s >>lu %ld" (reg d) (reg r1) (camlint_of_coqint n) - | Ororlimm n, [r1] -> sprintf "%s=%s rorl %ld" (reg d) (reg r1) (camlint_of_coqint n) - | Oleal addr, args -> sprintf "%s=addr" (reg d) - | Onegf, [r1] -> sprintf "%s=negf(%s)" (reg d) (reg r1) - | Oabsf, [r1] -> sprintf "%s=absf(%s)" (reg d) (reg r1) - | Oaddf, [r1;r2] -> sprintf "%s=%s +f %s" (reg d) (reg r1) (reg r2) - | Osubf, [r1;r2] -> sprintf "%s=%s -f %s" (reg d) (reg r1) (reg r2) - | Omulf, [r1;r2] -> sprintf "%s=%s *f %s" (reg d) (reg r1) (reg r2) - | Odivf, [r1;r2] -> sprintf "%s=%s /f %s" (reg d) (reg r1) (reg r2) - | Onegfs, [r1] -> sprintf "%s=negfs(%s)" (reg d) (reg r1) - | Oabsfs, [r1] -> sprintf "%s=absfs(%s)" (reg d) (reg r1) - | Oaddfs, [r1;r2] -> sprintf "%s=%s +fs %s" (reg d) (reg r1) (reg r2) - | Osubfs, [r1;r2] -> sprintf "%s=%s -fs %s" (reg d) (reg r1) (reg r2) - | Omulfs, [r1;r2] -> sprintf "%s=%s *fs %s" (reg d) (reg r1) (reg r2) - | Odivfs, [r1;r2] -> sprintf "%s=%s /fs %s" (reg d) (reg r1) (reg r2) - | Osingleoffloat, [r1] -> sprintf "%s=singleoffloat(%s)" (reg d) (reg r1) - | Ofloatofsingle, [r1] -> sprintf "%s=floatofsingle(%s)" (reg d) (reg r1) - | Ointoffloat, [r1] -> sprintf "%s=intoffloat(%s)" (reg d) (reg r1) - | Ofloatofint, [r1] -> sprintf "%s=floatofint(%s)" (reg d) (reg r1) - | Ointofsingle, [r1] -> sprintf "%s=intofsingle(%s)" (reg d) (reg r1) - | Osingleofint, [r1] -> sprintf "%s=singleofint(%s)" (reg d) (reg r1) - | Olongoffloat, [r1] -> sprintf "%s=longoffloat(%s)" (reg d) (reg r1) - | Ofloatoflong, [r1] -> sprintf "%s=floatoflong(%s)" (reg d) (reg r1) - | Olongofsingle, [r1] -> sprintf "%s=longofsingle(%s)" (reg d) (reg r1) - | Osingleoflong, [r1] -> sprintf "%s=singleoflong(%s)" (reg d) (reg r1) - | Ocmp c, args -> sprintf "%s=cmp" (reg d) - | Osel (c, ty), r1::r2::args -> sprintf "%s=sel" (reg d) - | _, _ -> sprintf "N/a") - -module DFGDot = Graph.Graphviz.Dot(struct - let graph_attributes _ = [] - let default_vertex_attributes _ = [] - let vertex_name = function (i, instr) -> sprintf "\"%d:%s\"" i (print_instr instr) - let vertex_attributes _ = [] - let get_subgraph _ = None - let default_edge_attributes _ = [] - let edge_attributes _ = [] - - include DFG - end) - -module IMap = Map.Make (struct - type t = int - - let compare = compare -end) - -let gen_vertex instrs i = (i, List.nth instrs i) - -(** The DFG type defines a list of instructions with their data dependencies as [edges], which are - the pairs of integers that represent the index of the instruction in the [nodes]. The edges - always point from left to right. *) - -let print_list f out_chan a = - fprintf out_chan "[ "; - List.iter (fprintf out_chan "%a " f) a; - fprintf out_chan "]" - -let print_tuple out_chan a = - let l, r = a in - fprintf out_chan "(%d,%d)" l r - -(*let print_dfg out_chan dfg = - fprintf out_chan "{ nodes = %a, edges = %a }" - (print_list PrintRTLBlockInstr.print_bblock_body) - dfg.nodes (print_list print_tuple) dfg.edges*) - -let print_dfg = DFGDot.output_graph - -let read_process command = - let buffer_size = 2048 in - let buffer = Buffer.create buffer_size in - let string = Bytes.create buffer_size in - let in_channel = Unix.open_process_in command in - let chars_read = ref 1 in - while !chars_read <> 0 do - chars_read := input in_channel string 0 buffer_size; - Buffer.add_substring buffer (Bytes.to_string string) 0 !chars_read - done; - ignore (Unix.close_process_in in_channel); - Buffer.contents buffer - -let comb_delay = function - | RBnop -> 0 - | RBop (_, op, _, _) -> - (match op with - | Omove -> 0 - | Ointconst _ -> 0 - | Olongconst _ -> 0 - | Ocast8signed -> 0 - | Ocast8unsigned -> 0 - | Ocast16signed -> 0 - | Ocast16unsigned -> 0 - | Oneg -> 0 - | Onot -> 0 - | Oor -> 0 - | Oorimm _ -> 0 - | Oand -> 0 - | Oandimm _ -> 0 - | Oxor -> 0 - | Oxorimm _ -> 0 - | Omul -> 8 - | Omulimm _ -> 8 - | Omulhs -> 8 - | Omulhu -> 8 - | Odiv -> 72 - | Odivu -> 72 - | Omod -> 72 - | Omodu -> 72 - | _ -> 1) - | _ -> 1 - -let pipeline_stages = function - | RBop (_, op, _, _) -> - (match op with - | Odiv -> 32 - | Odivu -> 32 - | Omod -> 32 - | Omodu -> 32 - | _ -> 0) - | _ -> 0 - -(** Add a dependency if it uses a register that was written to previously. *) -let add_dep map i tree dfg curr = - match PTree.get curr tree with - | None -> dfg - | Some ip -> - let ipv = (List.nth map ip) in - DFG.add_edge_e dfg (ipv, comb_delay (snd ipv), List.nth map i) - -(** This function calculates the dependencies of each instruction. The nodes correspond to previous - registers that were allocated and show which instruction caused it. - - This function only gathers the RAW constraints, and will therefore only be active for operations - that modify registers, which is this case only affects loads and operations. *) -let accumulate_RAW_deps map dfg curr = - let i, dst_map, graph = dfg in - let acc_dep_instruction rs dst = - ( i + 1, - PTree.set dst i dst_map, - List.fold_left (add_dep map i dst_map) graph rs - ) - in - let acc_dep_instruction_nodst rs = - ( i + 1, - dst_map, - List.fold_left (add_dep map i dst_map) graph rs) - in - match curr with - | RBop (op, _, rs, dst) -> acc_dep_instruction rs dst - | RBload (op, _mem, _addr, rs, dst) -> acc_dep_instruction rs dst - | RBstore (op, _mem, _addr, rs, src) -> acc_dep_instruction_nodst (src :: rs) - | _ -> (i + 1, dst_map, graph) - -(** Finds the next write to the [dst] register. This is a small optimisation so that only one - dependency is generated for a data dependency. *) -let rec find_next_dst_write i dst i' curr = - let check_dst dst' curr' = - if dst = dst' then Some (i, i') - else find_next_dst_write i dst (i' + 1) curr' - in - match curr with - | [] -> None - | RBop (_, _, _, dst') :: curr' -> check_dst dst' curr' - | RBload (_, _, _, _, dst') :: curr' -> check_dst dst' curr' - | _ :: curr' -> find_next_dst_write i dst (i' + 1) curr' - -let rec find_all_next_dst_read i dst i' curr = - let check_dst rs curr' = - if List.exists (fun x -> x = dst) rs - then (i, i') :: find_all_next_dst_read i dst (i' + 1) curr' - else find_all_next_dst_read i dst (i' + 1) curr' - in - match curr with - | [] -> [] - | RBop (_, _, rs, _) :: curr' -> check_dst rs curr' - | RBload (_, _, _, rs, _) :: curr' -> check_dst rs curr' - | RBstore (_, _, _, rs, src) :: curr' -> check_dst (src :: rs) curr' - | RBnop :: curr' -> find_all_next_dst_read i dst (i' + 1) curr' - | RBsetpred (_, rs, _) :: curr' -> check_dst rs curr' - -let drop i lst = - let rec drop' i' lst' = - match lst' with - | _ :: ls -> if i' = i then ls else drop' (i' + 1) ls - | [] -> [] - in - if i = 0 then lst else drop' 1 lst - -let take i lst = - let rec take' i' lst' = - match lst' with - | l :: ls -> if i' = i then [ l ] else l :: take' (i' + 1) ls - | [] -> [] - in - if i = 0 then [] else take' 1 lst - -let rec next_store i = function - | [] -> None - | RBstore (_, _, _, _, _) :: _ -> Some i - | _ :: rst -> next_store (i + 1) rst - -let rec next_load i = function - | [] -> None - | RBload (_, _, _, _, _) :: _ -> Some i - | _ :: rst -> next_load (i + 1) rst - -let accumulate_RAW_mem_deps instrs dfg curri = - let i, curr = curri in - match curr with - | RBload (_, _, _, _, _) -> ( - match next_store 0 (take i instrs |> List.rev) with - | None -> dfg - | Some d -> DFG.add_edge dfg (gen_vertex instrs (i - d - 1)) (gen_vertex instrs i) ) - | _ -> dfg - -let accumulate_WAR_mem_deps instrs dfg curri = - let i, curr = curri in - match curr with - | RBstore (_, _, _, _, _) -> ( - match next_load 0 (take i instrs |> List.rev) with - | None -> dfg - | Some d -> DFG.add_edge dfg (gen_vertex instrs (i - d - 1)) (gen_vertex instrs i) ) - | _ -> dfg - -let accumulate_WAW_mem_deps instrs dfg curri = - let i, curr = curri in - match curr with - | RBstore (_, _, _, _, _) -> ( - match next_store 0 (take i instrs |> List.rev) with - | None -> dfg - | Some d -> DFG.add_edge dfg (gen_vertex instrs (i - d - 1)) (gen_vertex instrs i) ) - | _ -> dfg - -(** Predicate dependencies. *) - -let rec in_predicate p p' = - match p' with - | Pvar p'' -> Nat.to_int p = Nat.to_int p'' - | Pnot p'' -> in_predicate p p'' - | Pand (p1, p2) -> in_predicate p p1 || in_predicate p p2 - | Por (p1, p2) -> in_predicate p p1 || in_predicate p p2 - -let get_predicate = function - | RBop (p, _, _, _) -> p - | RBload (p, _, _, _, _) -> p - | RBstore (p, _, _, _, _) -> p - | _ -> None - -let rec next_setpred p i = function - | [] -> None - | RBsetpred (_, _, p') :: rst -> - if in_predicate p' p then - Some i - else - next_setpred p (i + 1) rst - | _ :: rst -> next_setpred p (i + 1) rst - -let rec next_preduse p i instr= - let next p' rst = - if in_predicate p p' then - Some i - else - next_preduse p (i + 1) rst - in - match instr with - | [] -> None - | RBload (Some p', _, _, _, _) :: rst -> next p' rst - | RBstore (Some p', _, _, _, _) :: rst -> next p' rst - | RBop (Some p', _, _, _) :: rst -> next p' rst - | _ :: rst -> next_load (i + 1) rst - -let accumulate_RAW_pred_deps instrs dfg curri = - let i, curr = curri in - match get_predicate curr with - | Some p -> ( - match next_setpred p 0 (take i instrs |> List.rev) with - | None -> dfg - | Some d -> DFG.add_edge dfg (gen_vertex instrs (i - d - 1)) (gen_vertex instrs i) ) - | _ -> dfg - -let accumulate_WAR_pred_deps instrs dfg curri = - let i, curr = curri in - match curr with - | RBsetpred (_, _, p) -> ( - match next_preduse p 0 (take i instrs |> List.rev) with - | None -> dfg - | Some d -> DFG.add_edge dfg (gen_vertex instrs (i - d - 1)) (gen_vertex instrs i) ) - | _ -> dfg - -let accumulate_WAW_pred_deps instrs dfg curri = - let i, curr = curri in - match curr with - | RBsetpred (_, _, p) -> ( - match next_setpred (Pvar p) 0 (take i instrs |> List.rev) with - | None -> dfg - | Some d -> DFG.add_edge dfg (gen_vertex instrs (i - d - 1)) (gen_vertex instrs i) ) - | _ -> dfg - -(** This function calculates the WAW dependencies, which happen when two writes are ordered one - after another and therefore have to be kept in that order. This accumulation might be redundant - if register renaming is done before hand, because then these dependencies can be avoided. *) -let accumulate_WAW_deps instrs dfg curri = - let i, curr = curri in - let dst_dep dst = - match find_next_dst_write i dst (i + 1) (drop (i + 1) instrs) with - | Some (a, b) -> DFG.add_edge dfg (gen_vertex instrs a) (gen_vertex instrs b) - | _ -> dfg - in - match curr with - | RBop (_, _, _, dst) -> dst_dep dst - | RBload (_, _, _, _, dst) -> dst_dep dst - | RBstore (_, _, _, _, _) -> ( - match next_store (i + 1) (drop (i + 1) instrs) with - | None -> dfg - | Some i' -> DFG.add_edge dfg (gen_vertex instrs i) (gen_vertex instrs i') ) - | _ -> dfg - -let accumulate_WAR_deps instrs dfg curri = - let i, curr = curri in - let dst_dep dst = - let dep_list = find_all_next_dst_read i dst 0 (take i instrs |> List.rev) - |> List.map (function (d, d') -> (i - d' - 1, d)) - in - List.fold_left (fun g -> - function (d, d') -> DFG.add_edge g (gen_vertex instrs d) (gen_vertex instrs d')) dfg dep_list - in - match curr with - | RBop (_, _, _, dst) -> dst_dep dst - | RBload (_, _, _, _, dst) -> dst_dep dst - | _ -> dfg - -let assigned_vars vars = function - | RBnop -> vars - | RBop (_, _, _, dst) -> dst :: vars - | RBload (_, _, _, _, dst) -> dst :: vars - | RBstore (_, _, _, _, _) -> vars - | RBsetpred (_, _, _) -> vars - -let get_pred = function - | RBnop -> None - | RBop (op, _, _, _) -> op - | RBload (op, _, _, _, _) -> op - | RBstore (op, _, _, _, _) -> op - | RBsetpred (_, _, _) -> None - -let independant_pred p p' = - match sat_pred_temp (Nat.of_int 100000) (Pand (p, p')) with - | Some None -> true - | _ -> false - -let check_dependent op1 op2 = - match op1, op2 with - | Some p, Some p' -> not (independant_pred p p') - | _, _ -> true - -let remove_unnecessary_deps graph = - let is_dependent v1 v2 g = - let (_, instr1) = v1 in - let (_, instr2) = v2 in - if check_dependent (get_pred instr1) (get_pred instr2) - then g - else DFG.remove_edge g v1 v2 - in - DFG.fold_edges is_dependent graph graph - -(** All the nodes in the DFG have to come after the source of the basic block, and should terminate - before the sink of the basic block. After that, there should be constraints for data - dependencies between nodes. *) -let gather_bb_constraints debug bb = - let ibody = List.mapi (fun i a -> (i, a)) bb.bb_body in - let dfg = List.fold_left (fun dfg v -> DFG.add_vertex dfg v) DFG.empty ibody in - let _, _, dfg' = - List.fold_left (accumulate_RAW_deps ibody) - (0, PTree.empty, dfg) - bb.bb_body - in - let dfg'' = List.fold_left (fun dfg f -> List.fold_left (f bb.bb_body) dfg ibody) dfg' - [ accumulate_WAW_deps; - accumulate_WAR_deps; - accumulate_RAW_mem_deps; - accumulate_WAR_mem_deps; - accumulate_WAW_mem_deps; - accumulate_RAW_pred_deps; - accumulate_WAR_pred_deps; - accumulate_WAW_pred_deps - ] - in - let dfg''' = remove_unnecessary_deps dfg'' in - (List.length bb.bb_body, dfg''', successors_instr bb.bb_exit) - -let encode_var bbn n i = { sv_type = VarType (bbn, n); sv_num = i } -let encode_bb bbn i = { sv_type = BBType bbn; sv_num = i } - -let add_super_nodes n dfg = - DFG.fold_vertex (function v1 -> fun g -> - (if DFG.in_degree dfg v1 = 0 - then G.add_edge_e g (encode_bb n 0, 0, encode_var n (fst v1) 0) - else g) |> - (fun g' -> - if DFG.out_degree dfg v1 = 0 - then G.add_edge_e g' (encode_var n (fst v1) 0, 0, encode_bb n 1) - else g')) dfg - -let add_data_deps n = - DFG.fold_edges_e (function ((i1, _), l, (i2, _)) -> fun g -> - G.add_edge_e g (encode_var n i1 0, 0, encode_var n i2 0) - ) - -let add_ctrl_deps n succs constr = - List.fold_left (fun g n' -> - G.add_edge_e g (encode_bb n 1, -1, encode_bb n' 0) - ) constr succs - -module BFDFG = Graph.Path.BellmanFord(DFG)(struct - include DFG - type t = int - let weight = DFG.E.label - let compare = compare - let add = (+) - let zero = 0 - end) - -module TopoDFG = Graph.Topological.Make(DFG) - -let negate_graph constr = - DFG.fold_edges_e (function (v1, e, v2) -> fun g -> - DFG.add_edge_e g (v1, -e, v2) - ) constr DFG.empty - -let add_cycle_constr max n dfg constr = - let negated_dfg = negate_graph dfg in - let longest_path v = BFDFG.all_shortest_paths negated_dfg v - |> BFDFG.H.to_seq |> List.of_seq in - let constrained_paths = List.filter (function (v, m) -> - m > max) in - List.fold_left (fun g -> function (v, v', w) -> - G.add_edge_e g (encode_var n (fst v) 0, - - (int_of_float (Float.ceil (Float.div (float_of_int w) (float_of_int max))) - 1), - encode_var n (fst v') 0) - ) constr (DFG.fold_vertex (fun v l -> - List.append l (longest_path v |> constrained_paths - |> List.map (function (v', w) -> (v, v', - w))) - ) dfg []) - -type resource = - | Mem - | SDiv - | UDiv - -type resources = { - res_mem: DFG.V.t list; - res_udiv: DFG.V.t list; - res_sdiv: DFG.V.t list; -} - -let find_resource = function - | RBload _ -> Some Mem - | RBstore _ -> Some Mem - | RBop (_, op, _, _) -> - ( match op with - | Odiv -> Some SDiv - | Odivu -> Some UDiv - | Omod -> Some SDiv - | Omodu -> Some UDiv - | _ -> None ) - | _ -> None - -let add_resource_constr n dfg constr = - let res = TopoDFG.fold (function (i, instr) -> - function {res_mem = ml; res_sdiv = sdl; res_udiv = udl} as r -> - match find_resource instr with - | Some SDiv -> {r with res_sdiv = (i, instr) :: sdl} - | Some UDiv -> {r with res_udiv = (i, instr) :: udl} - | Some Mem -> {r with res_mem = (i, instr) :: ml} - | None -> r - ) dfg {res_mem = []; res_sdiv = []; res_udiv = []} - in - let get_constraints l g = List.fold_left (fun gv v' -> - match gv with - | (g, None) -> (g, Some v') - | (g, Some v) -> - (G.add_edge_e g (encode_var n (fst v) 0, -1, encode_var n (fst v') 0), Some v') - ) (g, None) l |> fst - in - get_constraints (List.rev res.res_mem) constr - |> get_constraints (List.rev res.res_udiv) - |> get_constraints (List.rev res.res_sdiv) - -let gather_cfg_constraints c constr curr = - let (n, dfg) = curr in - match PTree.get (P.of_int n) c with - | None -> assert false - | Some { bb_exit = ctrl; _ } -> - add_super_nodes n dfg constr - |> add_data_deps n dfg - |> add_ctrl_deps n (successors_instr ctrl - |> List.map P.to_int - |> List.filter (fun n' -> n' < n)) - |> add_cycle_constr 8 n dfg - |> add_resource_constr n dfg - -let rec intersperse s = function - | [] -> [] - | [ a ] -> [ a ] - | x :: xs -> x :: s :: intersperse s xs - -let print_objective constr = - let vars = G.fold_vertex (fun v1 l -> - match v1 with - | { sv_type = VarType _; sv_num = 0 } -> print_sv v1 :: l - | _ -> l - ) constr [] - in - "min: " ^ String.concat "" (intersperse " + " vars) ^ ";\n" - -let print_lp constr = - print_objective constr ^ - (G.fold_edges_e (function (e1, w, e2) -> fun s -> - s ^ sprintf "%s - %s <= %d;\n" (print_sv e1) (print_sv e2) w - ) constr "" |> - G.fold_vertex (fun v1 s -> - s ^ sprintf "int %s;\n" (print_sv v1) - ) constr) - -let update_schedule v = function Some l -> Some (v :: l) | None -> Some [ v ] - -let parse_soln tree s = - let r = Str.regexp "var\\([0-9]+\\)n\\([0-9]+\\)_0[ ]+\\([0-9]+\\)" in - if Str.string_match r s 0 then - IMap.update - (Str.matched_group 1 s |> int_of_string) - (update_schedule - ( Str.matched_group 2 s |> int_of_string, - Str.matched_group 3 s |> int_of_string )) - tree - else tree - -let solve_constraints constr = - let oc = open_out "lpsolve.txt" in - fprintf oc "%s\n" (print_lp constr); - close_out oc; - - Str.split (Str.regexp_string "\n") (read_process "lp_solve lpsolve.txt") - |> drop 3 - |> List.fold_left parse_soln IMap.empty - -let subgraph dfg l = - let dfg' = List.fold_left (fun g v -> DFG.add_vertex g v) DFG.empty l in - List.fold_left (fun g v -> - List.fold_left (fun g' v' -> - let edges = DFG.find_all_edges dfg v v' in - List.fold_left (fun g'' e -> - DFG.add_edge_e g'' e - ) g' edges - ) g l - ) dfg' l - -let rec all_successors dfg v = - List.concat (List.fold_left (fun l v -> - all_successors dfg v :: l - ) [] (DFG.succ dfg v)) - -let order_instr dfg = - DFG.fold_vertex (fun v li -> - if DFG.in_degree dfg v = 0 - then (List.map snd (v :: all_successors dfg v)) :: li - else li - ) dfg [] - -let combine_bb_schedule schedule s = - let i, st = s in - IMap.update st (update_schedule i) schedule - -(** Should generate the [RTLPar] code based on the input [RTLBlock] description. *) -let transf_rtlpar c c' (schedule : (int * int) list IMap.t) = - let f i bb : RTLPar.bblock = - match bb with - | { bb_body = []; bb_exit = c } -> { bb_body = []; bb_exit = c } - | { bb_body = bb_body'; bb_exit = ctrl_flow } -> - let dfg = match PTree.get i c' with None -> assert false | Some x -> x in - let i_sched = IMap.find (P.to_int i) schedule in - let i_sched_tree = - List.fold_left combine_bb_schedule IMap.empty i_sched - in - let body = IMap.to_seq i_sched_tree |> List.of_seq |> List.map snd - |> List.map (List.map (fun x -> (x, List.nth bb_body' x))) - in - (*let final_body = List.map (fun x -> subgraph dfg x |> order_instr) body in*) - let final_body2 = List.map (fun x -> subgraph dfg x - |> (fun x -> TopoDFG.fold (fun i l -> snd i :: l) x []) - |> List.rev) body - in - { bb_body = List.map (fun x -> [x]) final_body2; - bb_exit = ctrl_flow - } - in - PTree.map f c - -let schedule entry (c : RTLBlock.bb RTLBlockInstr.code) = - let debug = true in - let transf_graph (_, dfg, _) = dfg in - let c' = PTree.map1 (fun x -> gather_bb_constraints false x |> transf_graph) c in - (*let _ = if debug then PTree.map (fun r o -> printf "##### %d #####\n%a\n\n" (P.to_int r) print_dfg (second o)) c' else PTree.empty in*) - let cgraph = PTree.elements c' - |> List.map (function (x, y) -> (P.to_int x, y)) - |> List.fold_left (gather_cfg_constraints c) G.empty - in - let graph = open_out "constr_graph.dot" in - fprintf graph "%a\n" GDot.output_graph cgraph; - close_out graph; - let schedule' = solve_constraints cgraph in - (**IMap.iter (fun a b -> printf "##### %d #####\n%a\n\n" a (print_list print_tuple) b) schedule';*) - (*printf "Schedule: %a\n" (fun a x -> IMap.iter (fun d -> fprintf a "%d: %a\n" d (print_list print_tuple)) x) schedule';*) - transf_rtlpar c c' schedule' - -let rec find_reachable_states c e = - match PTree.get e c with - | Some { bb_exit = ex; _ } -> - e :: List.fold_left (fun x a -> List.concat [x; find_reachable_states c a]) [] - (successors_instr ex |> List.filter (fun x -> P.lt x e)) - | None -> assert false - -let add_to_tree c nt i = - match PTree.get i c with - | Some p -> PTree.set i p nt - | None -> assert false - -let schedule_fn (f : RTLBlock.coq_function) : RTLPar.coq_function = - let scheduled = schedule f.fn_entrypoint f.fn_code in - let reachable = find_reachable_states scheduled f.fn_entrypoint - |> List.to_seq |> SS.of_seq |> SS.to_seq |> List.of_seq in - { fn_sig = f.fn_sig; - fn_params = f.fn_params; - fn_stacksize = f.fn_stacksize; - fn_code = List.fold_left (add_to_tree scheduled) PTree.empty reachable; - fn_entrypoint = f.fn_entrypoint - } |