From 00ebd4125f46e4b21e18f907fc0498c078f38e95 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Tue, 16 Feb 2021 13:02:04 +0000 Subject: Fix RTLPar to use instr list list list --- src/hls/HTLPargen.v | 33 ++++++++++++++++++--------------- src/hls/RTLPar.v | 17 ++++++++++++++--- src/hls/RTLPargen.v | 8 +------- 3 files changed, 33 insertions(+), 25 deletions(-) (limited to 'src') diff --git a/src/hls/HTLPargen.v b/src/hls/HTLPargen.v index fcd4441..9213514 100644 --- a/src/hls/HTLPargen.v +++ b/src/hls/HTLPargen.v @@ -39,6 +39,8 @@ Hint Resolve AssocMap.gss : htlh. Hint Resolve Ple_refl : htlh. Hint Resolve Ple_succ : htlh. +Definition assignment : Type := expr -> expr -> stmnt. + Record state: Type := mkstate { st_st: reg; st_freshreg: reg; @@ -666,35 +668,33 @@ Fixpoint pred_expr (preg: reg) (p: pred_op) := Vbinop Vor (pred_expr preg p1) (pred_expr preg p2) end. -Definition translate_predicate (preg: reg) (p: option pred_op) (dst e: expr) := +Definition translate_predicate (a : assignment) + (preg: reg) (p: option pred_op) (dst e: expr) := match p with - | None => ret (Vnonblock dst e) + | None => ret (a dst e) | Some pos => - ret (Vnonblock dst (Vternary (pred_expr preg pos) e dst)) + ret (a dst (Vternary (pred_expr preg pos) e dst)) end. -Definition translate_inst (fin rtrn stack preg : reg) (n : node) (i : instr) - : mon unit := +Definition translate_inst a (fin rtrn stack preg : reg) (n : node) (i : instr) + : mon stmnt := match i with | RBnop => - add_data_instr n Vskip + ret Vskip | RBop p op args dst => do instr <- translate_instr op args; do _ <- declare_reg None dst 32; - do pred <- translate_predicate preg p (Vvar dst) instr; - add_data_instr n pred + translate_predicate a preg p (Vvar dst) instr | RBload p chunk addr args dst => do src <- translate_arr_access chunk addr args stack; do _ <- declare_reg None dst 32; - do pred <- translate_predicate preg p (Vvar dst) src; - add_data_instr n pred + translate_predicate a preg p (Vvar dst) src | RBstore p chunk addr args src => do dst <- translate_arr_access chunk addr args stack; - do pred <- translate_predicate preg p dst (Vvar src); - add_data_instr n pred + translate_predicate a preg p dst (Vvar src) | RBsetpred c args p => do cond <- translate_condition c args; - add_data_instr n (Vnonblock (pred_expr preg (Pvar p)) cond) + ret (a (pred_expr preg (Pvar p)) cond) end. Lemma create_new_state_state_incr: @@ -722,10 +722,13 @@ Definition create_new_state (p: node): mon node := s.(st_controllogic)) (create_new_state_state_incr s p). -Definition translate_inst_list (fin rtrn stack preg: reg) (ni : node * node * list instr) := +Definition translate_inst_list (fin rtrn stack preg: reg) (ni : node * node * list (list instr)) := match ni with | (n, p, li) => - do _ <- collectlist (translate_inst fin rtrn stack preg n) li; + do _ <- collectlist + (fun l => + do stmnt <- translate_inst Vblock fin rtrn stack preg n l; + add_data_instr n stmnt) (concat li); do st <- get; add_control_instr n (state_goto st.(st_st) p) end. diff --git a/src/hls/RTLPar.v b/src/hls/RTLPar.v index be9ff22..2e78d36 100644 --- a/src/hls/RTLPar.v +++ b/src/hls/RTLPar.v @@ -30,7 +30,7 @@ Require Import compcert.verilog.Op. Require Import vericert.hls.RTLBlockInstr. -Definition bb := list (list instr). +Definition bb := list (list (list instr)). Definition bblock := @bblock bb. Definition code := @code bb. @@ -56,11 +56,22 @@ Section RELSEM. forall state sp, step_instr_list sp state nil state. + Inductive step_instr_seq (sp : val) + : instr_state -> list (list instr) -> instr_state -> Prop := + | exec_instr_seq_cons: + forall state i state' state'' instrs, + step_instr_list sp state i state' -> + step_instr_seq sp state' instrs state'' -> + step_instr_seq sp state (i :: instrs) state'' + | exec_instr_seq_nil: + forall state, + step_instr_seq sp state nil state. + Inductive step_instr_block (sp : val) : instr_state -> bb -> instr_state -> Prop := | exec_instr_block_cons: forall state i state' state'' instrs, - step_instr_list sp state i state' -> + step_instr_seq sp state i state' -> step_instr_block sp state' instrs state'' -> step_instr_block sp state (i :: instrs) state'' | exec_instr_block_nil: @@ -113,7 +124,7 @@ Definition semantics (p: program) := Semantics step (initial_state p) final_state (Genv.globalenv p). Definition max_reg_bblock (m : positive) (pc : node) (bb : bblock) := - let max_body := fold_left (fun x l => fold_left max_reg_instr l x) bb.(bb_body) m in + let max_body := fold_left (fun x l => fold_left (fun x' l' => fold_left max_reg_instr l' x') l x) bb.(bb_body) m in max_reg_cfi max_body bb.(bb_exit). Definition max_reg_function (f: function) := diff --git a/src/hls/RTLPargen.v b/src/hls/RTLPargen.v index 39c57df..e2e9a90 100644 --- a/src/hls/RTLPargen.v +++ b/src/hls/RTLPargen.v @@ -591,12 +591,6 @@ Fixpoint abstract_sequence (f : forest) (b : list instr) : forest := | i :: l => update (abstract_sequence f l) i end. -Fixpoint abstract_sequence_par (f : forest) (b : list (list instr)) : forest := - match b with - | nil => f - | i :: l => abstract_sequence (abstract_sequence_par f l) i - end. - (*| Check equivalence of control flow instructions. As none of the basic blocks should have been moved, none of the labels should be different, meaning the control-flow instructions should match exactly. @@ -622,7 +616,7 @@ Definition empty_trees (bb: RTLBlock.bb) (bbt: RTLPar.bb) : bool := Definition schedule_oracle (bb: RTLBlock.bblock) (bbt: RTLPar.bblock) : bool := check (abstract_sequence empty (bb_body bb)) - (abstract_sequence_par empty (bb_body bbt)) && + (abstract_sequence empty (concat (concat (bb_body bbt)))) && check_control_flow_instr (bb_exit bb) (bb_exit bbt) && empty_trees (bb_body bb) (bb_body bbt). -- cgit