diff options
Diffstat (limited to 'src/hls/RTLParFUgen.v')
-rw-r--r-- | src/hls/RTLParFUgen.v | 280 |
1 files changed, 140 insertions, 140 deletions
diff --git a/src/hls/RTLParFUgen.v b/src/hls/RTLParFUgen.v index a15be1c..f1b3ba6 100644 --- a/src/hls/RTLParFUgen.v +++ b/src/hls/RTLParFUgen.v @@ -35,143 +35,143 @@ Require Import vericert.hls.GiblePar. Require Import vericert.hls.RTLParFU. Require Import vericert.hls.FunctionalUnits. -#[local] Open Scope error_monad_scope. - -Definition update {A: Type} (i: positive) (f: option A -> A) (pt: PTree.t A) := - PTree.set i (f (pt ! i)) pt. - -Definition add_instr (instr_: instr) x := - match x with Some i => instr_ :: i | None => instr_ :: nil end. - -Definition transl_instr (res: resources) (cycle: positive) (i: Gible.instr) - (li: Errors.res (list instr * PTree.t (list instr))): - Errors.res (list instr * PTree.t (list instr)) := - do (instr_list, d_tree) <- li; - match i with - | RBnop => Errors.OK (FUnop :: instr_list, d_tree) - | RBop po op args d => Errors.OK (FUop po op args d :: instr_list, d_tree) - | RBload po chunk addr args d => - match get_ram 0 res with - | Some (ri, r) => - Errors.OK (FUop po Op.Onot (ram_u_en r::nil) (ram_u_en r) - :: FUop po (Op.Ointconst (Int.repr 0)) nil (ram_wr_en r) - :: FUop po (Op.Olea addr) args (ram_addr r) - :: FUop po (Op.Oshruimm (Int.repr 2)) ((ram_addr r)::nil) (ram_addr r) - :: instr_list, update (Pos.pred cycle) - (add_instr (FUop po Op.Omove (ram_d_out r::nil) d)) - d_tree) - | _ => Errors.Error (Errors.msg "Could not find RAM") - end - | RBstore po chunk addr args d => - match get_ram 0 res with - | Some (ri, r) => - Errors.OK (FUop po Op.Onot (ram_u_en r::nil) (ram_u_en r) - :: FUop po (Op.Ointconst (Int.repr 1)) nil (ram_wr_en r) - :: FUop po Op.Omove (d::nil) (ram_d_in r) - :: FUop po (Op.Olea addr) args (ram_addr r) - :: FUop po (Op.Oshruimm (Int.repr 2)) ((ram_addr r)::nil) (ram_addr r) - :: instr_list, d_tree) - | _ => Errors.Error (Errors.msg "Could not find RAM") - end - | RBsetpred op c args p => Errors.OK (FUsetpred op c args p :: instr_list, d_tree) - | RBexit po cf => Errors.Error (Errors.msg "Wrong.") - end. - -Definition transl_cf_instr (i: Gible.cf_instr): RTLParFU.cf_instr := - match i with - | RBcall sig r args d n => FUcall sig r args d n - | RBtailcall sig r args => FUtailcall sig r args - | RBbuiltin ef args r n => FUbuiltin ef args r n - | RBcond c args n1 n2 => FUcond c args n1 n2 - | RBjumptable r ns => FUjumptable r ns - | RBreturn r => FUreturn r - | RBgoto n => FUgoto n - end. - -Definition list_split {A:Type} (l: list (Z * A)) : (list (Z * A)) * (list (Z * A)) := - (filter (fun x => Z.eqb 0 (fst x)) l, - map (fun x => (Z.pred (fst x), snd x)) (filter (fun x => negb (Z.eqb 0 (fst x))) l)). - -Fixpoint map_error {A B : Type} (f : A -> res B) (l : list A) {struct l} : res (list B) := - match l with - | nil => OK nil - | x::xs => - do y <- f x ; - do ys <- map_error f xs ; - OK (y::ys) - end. - -Definition transl_op_chain_block (res: resources) (cycle: positive) (instrs: list Gible.instr) - (state: Errors.res (list (list instr) * PTree.t (list instr))) - : Errors.res (list (list instr) * PTree.t (list instr)) := - do (li, tr) <- state; - do (li', tr') <- fold_right (transl_instr res cycle) (OK (nil, tr)) instrs; - OK (li' :: li, tr'). - -(*Compute transl_op_chain_block initial_resources 10%nat (RBop None (Op.Ointconst (Int.repr 1)) nil 1%positive::RBnop::RBnop::RBnop::nil) (OK (nil, PTree.empty _)).*) - -Definition transl_par_block (res: resources) (cycle: positive) (instrs: list (list Gible.instr)) - (state: Errors.res (list (list (list instr)) * PTree.t (list instr))) - : Errors.res (list (list (list instr)) * PTree.t (list instr)) := - do (li, tr) <- state; - do (li', tr') <- fold_right (transl_op_chain_block res cycle) (OK (nil, tr)) instrs; - OK (li' :: li, tr'). - -(*Compute transl_par_block initial_resources 10%nat ((RBop None (Op.Ointconst (Int.repr 1)) nil 1%positive::RBnop::nil)::(RBop None (Op.Ointconst (Int.repr 2)) nil 2%positive::RBnop::nil)::nil) (OK (((FUnop::nil)::nil)::nil, PTree.empty _)).*) - -Definition transl_seq_block (res: resources) (b: list (list Gible.instr)) - (a: Errors.res (list (list (list instr)) * PTree.t (list instr) * positive)) := - do (litr, n) <- a; - let (li, tr) := litr in - do (li', tr') <- transl_par_block res n b (OK (li, tr)); - OK (li', tr', (n+1)%positive). - -Definition insert_extra (pt: PTree.t (list instr)) (curr: list (list instr)) - (cycle_bb: (positive * list (list (list instr)))) := - let (cycle, bb) := cycle_bb in - match pt ! cycle with - | Some instrs => ((cycle + 1)%positive, (curr ++ (map (fun x => x :: nil) instrs)) :: bb) - | None => ((cycle + 1)%positive, curr :: bb) - end. - -Definition transl_bb (res: resources) (bb: ParBB.t): Errors.res RTLParFU.bblock_body := - do (litr, n) <- fold_right (transl_seq_block res) (OK (nil, PTree.empty _, 1%positive)) bb; - let (li, tr) := litr in - OK (snd (fold_right (insert_extra tr) (1%positive, nil) li)). - -(*Definition transl_bblock (res: resources) (bb: ParBB.t): Errors.res ParBB.t := - transl_bb res bb. - -Definition error_map_ptree {A B: Type} (f: positive -> A -> res B) (pt: PTree.t A) := - do ptl' <- map_error (fun x => do x' <- uncurry f x; OK (fst x, x')) (PTree.elements pt); - OK (PTree_Properties.of_list ptl'). - -Definition transl_code (fu: resources) (c: RTLPar.code): res code := - error_map_ptree (fun _ => transl_bblock fu) c. - -Definition transl_function (f: RTLPar.function): Errors.res RTLParFU.function := - let max := RTLPar.max_reg_function f in - let fu := set_res (Ram (mk_ram - (Z.to_nat (RTLBlockInstr.fn_stacksize f)) - (max+1)%positive - (max+3)%positive - (max+7)%positive - (max+2)%positive - (max+6)%positive - (max+4)%positive - (max+5)%positive - )) initial_resources in - do c' <- transl_code fu (RTLBlockInstr.fn_code f); - Errors.OK (mkfunction (RTLBlockInstr.fn_sig f) - (RTLBlockInstr.fn_params f) - (RTLBlockInstr.fn_stacksize f) - c' - fu - (RTLBlockInstr.fn_entrypoint f)). - -Definition transl_fundef p := - transf_partial_fundef transl_function p. - -Definition transl_program (p : RTLPar.program) : Errors.res RTLParFU.program := - transform_partial_program transl_fundef p. -*) +(* #[local] Open Scope error_monad_scope. *) + +(* Definition update {A: Type} (i: positive) (f: option A -> A) (pt: PTree.t A) := *) +(* PTree.set i (f (pt ! i)) pt. *) + +(* Definition add_instr (instr_: instr) x := *) +(* match x with Some i => instr_ :: i | None => instr_ :: nil end. *) + +(* Definition transl_instr (res: resources) (cycle: positive) (i: Gible.instr) *) +(* (li: Errors.res (list instr * PTree.t (list instr))): *) +(* Errors.res (list instr * PTree.t (list instr)) := *) +(* do (instr_list, d_tree) <- li; *) +(* match i with *) +(* | RBnop => Errors.OK (FUnop :: instr_list, d_tree) *) +(* | RBop po op args d => Errors.OK (FUop po op args d :: instr_list, d_tree) *) +(* | RBload po chunk addr args d => *) +(* match get_ram 0 res with *) +(* | Some (ri, r) => *) +(* Errors.OK (FUop po Op.Onot (ram_u_en r::nil) (ram_u_en r) *) +(* :: FUop po (Op.Ointconst (Int.repr 0)) nil (ram_wr_en r) *) +(* :: FUop po (Op.Olea addr) args (ram_addr r) *) +(* :: FUop po (Op.Oshruimm (Int.repr 2)) ((ram_addr r)::nil) (ram_addr r) *) +(* :: instr_list, update (Pos.pred cycle) *) +(* (add_instr (FUop po Op.Omove (ram_d_out r::nil) d)) *) +(* d_tree) *) +(* | _ => Errors.Error (Errors.msg "Could not find RAM") *) +(* end *) +(* | RBstore po chunk addr args d => *) +(* match get_ram 0 res with *) +(* | Some (ri, r) => *) +(* Errors.OK (FUop po Op.Onot (ram_u_en r::nil) (ram_u_en r) *) +(* :: FUop po (Op.Ointconst (Int.repr 1)) nil (ram_wr_en r) *) +(* :: FUop po Op.Omove (d::nil) (ram_d_in r) *) +(* :: FUop po (Op.Olea addr) args (ram_addr r) *) +(* :: FUop po (Op.Oshruimm (Int.repr 2)) ((ram_addr r)::nil) (ram_addr r) *) +(* :: instr_list, d_tree) *) +(* | _ => Errors.Error (Errors.msg "Could not find RAM") *) +(* end *) +(* | RBsetpred op c args p => Errors.OK (FUsetpred op c args p :: instr_list, d_tree) *) +(* | RBexit po cf => Errors.Error (Errors.msg "Wrong.") *) +(* end. *) + +(* Definition transl_cf_instr (i: Gible.cf_instr): RTLParFU.cf_instr := *) +(* match i with *) +(* | RBcall sig r args d n => FUcall sig r args d n *) +(* | RBtailcall sig r args => FUtailcall sig r args *) +(* | RBbuiltin ef args r n => FUbuiltin ef args r n *) +(* | RBcond c args n1 n2 => FUcond c args n1 n2 *) +(* | RBjumptable r ns => FUjumptable r ns *) +(* | RBreturn r => FUreturn r *) +(* | RBgoto n => FUgoto n *) +(* end. *) + +(* Definition list_split {A:Type} (l: list (Z * A)) : (list (Z * A)) * (list (Z * A)) := *) +(* (filter (fun x => Z.eqb 0 (fst x)) l, *) +(* map (fun x => (Z.pred (fst x), snd x)) (filter (fun x => negb (Z.eqb 0 (fst x))) l)). *) + +(* Fixpoint map_error {A B : Type} (f : A -> res B) (l : list A) {struct l} : res (list B) := *) +(* match l with *) +(* | nil => OK nil *) +(* | x::xs => *) +(* do y <- f x ; *) +(* do ys <- map_error f xs ; *) +(* OK (y::ys) *) +(* end. *) + +(* Definition transl_op_chain_block (res: resources) (cycle: positive) (instrs: list Gible.instr) *) +(* (state: Errors.res (list (list instr) * PTree.t (list instr))) *) +(* : Errors.res (list (list instr) * PTree.t (list instr)) := *) +(* do (li, tr) <- state; *) +(* do (li', tr') <- fold_right (transl_instr res cycle) (OK (nil, tr)) instrs; *) +(* OK (li' :: li, tr'). *) + +(* (*Compute transl_op_chain_block initial_resources 10%nat (RBop None (Op.Ointconst (Int.repr 1)) nil 1%positive::RBnop::RBnop::RBnop::nil) (OK (nil, PTree.empty _)).*) *) + +(* Definition transl_par_block (res: resources) (cycle: positive) (instrs: list (list Gible.instr)) *) +(* (state: Errors.res (list (list (list instr)) * PTree.t (list instr))) *) +(* : Errors.res (list (list (list instr)) * PTree.t (list instr)) := *) +(* do (li, tr) <- state; *) +(* do (li', tr') <- fold_right (transl_op_chain_block res cycle) (OK (nil, tr)) instrs; *) +(* OK (li' :: li, tr'). *) + +(* (*Compute transl_par_block initial_resources 10%nat ((RBop None (Op.Ointconst (Int.repr 1)) nil 1%positive::RBnop::nil)::(RBop None (Op.Ointconst (Int.repr 2)) nil 2%positive::RBnop::nil)::nil) (OK (((FUnop::nil)::nil)::nil, PTree.empty _)).*) *) + +(* Definition transl_seq_block (res: resources) (b: list (list Gible.instr)) *) +(* (a: Errors.res (list (list (list instr)) * PTree.t (list instr) * positive)) := *) +(* do (litr, n) <- a; *) +(* let (li, tr) := litr in *) +(* do (li', tr') <- transl_par_block res n b (OK (li, tr)); *) +(* OK (li', tr', (n+1)%positive). *) + +(* Definition insert_extra (pt: PTree.t (list instr)) (curr: list (list instr)) *) +(* (cycle_bb: (positive * list (list (list instr)))) := *) +(* let (cycle, bb) := cycle_bb in *) +(* match pt ! cycle with *) +(* | Some instrs => ((cycle + 1)%positive, (curr ++ (map (fun x => x :: nil) instrs)) :: bb) *) +(* | None => ((cycle + 1)%positive, curr :: bb) *) +(* end. *) + +(* Definition transl_bb (res: resources) (bb: ParBB.t): Errors.res RTLParFU.bblock_body := *) +(* do (litr, n) <- fold_right (transl_seq_block res) (OK (nil, PTree.empty _, 1%positive)) bb; *) +(* let (li, tr) := litr in *) +(* OK (snd (fold_right (insert_extra tr) (1%positive, nil) li)). *) + +(* (*Definition transl_bblock (res: resources) (bb: ParBB.t): Errors.res ParBB.t := *) +(* transl_bb res bb. *) + +(* Definition error_map_ptree {A B: Type} (f: positive -> A -> res B) (pt: PTree.t A) := *) +(* do ptl' <- map_error (fun x => do x' <- uncurry f x; OK (fst x, x')) (PTree.elements pt); *) +(* OK (PTree_Properties.of_list ptl'). *) + +(* Definition transl_code (fu: resources) (c: RTLPar.code): res code := *) +(* error_map_ptree (fun _ => transl_bblock fu) c. *) + +(* Definition transl_function (f: RTLPar.function): Errors.res RTLParFU.function := *) +(* let max := RTLPar.max_reg_function f in *) +(* let fu := set_res (Ram (mk_ram *) +(* (Z.to_nat (RTLBlockInstr.fn_stacksize f)) *) +(* (max+1)%positive *) +(* (max+3)%positive *) +(* (max+7)%positive *) +(* (max+2)%positive *) +(* (max+6)%positive *) +(* (max+4)%positive *) +(* (max+5)%positive *) +(* )) initial_resources in *) +(* do c' <- transl_code fu (RTLBlockInstr.fn_code f); *) +(* Errors.OK (mkfunction (RTLBlockInstr.fn_sig f) *) +(* (RTLBlockInstr.fn_params f) *) +(* (RTLBlockInstr.fn_stacksize f) *) +(* c' *) +(* fu *) +(* (RTLBlockInstr.fn_entrypoint f)). *) + +(* Definition transl_fundef p := *) +(* transf_partial_fundef transl_function p. *) + +(* Definition transl_program (p : RTLPar.program) : Errors.res RTLParFU.program := *) +(* transform_partial_program transl_fundef p. *) +(* *) *) |