diff options
author | Michalis Pardalos <m.pardalos@gmail.com> | 2021-03-29 17:31:26 +0100 |
---|---|---|
committer | Michalis Pardalos <m.pardalos@gmail.com> | 2021-03-29 17:31:26 +0100 |
commit | a5ab34ebcf5ce1e39be78268e24c07c7ad32a9de (patch) | |
tree | 36e8c6794f9974431aa1375e318631b7b5235802 /src/hls/HTLPargen.v | |
parent | 5c36514942b335f42044ab41d0433e952f979f24 (diff) | |
parent | 83fff1638e851256273cd802288577a0c47dca5e (diff) | |
download | vericert-a5ab34ebcf5ce1e39be78268e24c07c7ad32a9de.tar.gz vericert-a5ab34ebcf5ce1e39be78268e24c07c7ad32a9de.zip |
Merge remote-tracking branch 'upstream/master' into dev-michalis
Diffstat (limited to 'src/hls/HTLPargen.v')
-rw-r--r-- | src/hls/HTLPargen.v | 33 |
1 files changed, 18 insertions, 15 deletions
diff --git a/src/hls/HTLPargen.v b/src/hls/HTLPargen.v index b5951c3..9045499 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; @@ -671,35 +673,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: @@ -727,10 +727,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. |