From 77c5c01146fa9e2fa09779c1da642b8f5469dff5 Mon Sep 17 00:00:00 2001 From: Michalis Pardalos Date: Sun, 6 Jun 2021 12:39:04 +0100 Subject: Make externctrl application its own HTL pass --- src/hls/HTL.v | 31 ++++++++++++++++++++----------- 1 file changed, 20 insertions(+), 11 deletions(-) (limited to 'src/hls/HTL.v') diff --git a/src/hls/HTL.v b/src/hls/HTL.v index 1eb86e1..8d51750 100644 --- a/src/hls/HTL.v +++ b/src/hls/HTL.v @@ -105,6 +105,26 @@ Fixpoint init_regs (vl : list value) (rl : list reg) {struct rl} := Definition empty_stack (m : module) : Verilog.assocmap_arr := (AssocMap.set m.(mod_stk) (Array.arr_repeat None m.(mod_stk_len)) (AssocMap.empty Verilog.arr)). + +Definition prog_modmap (p : HTL.program) := + PTree_Properties.of_list (Option.map_option + (fun a => match a with + | (ident, (AST.Gfun (AST.Internal f))) => Some (ident, f) + | _ => None + end) + (AST.prog_defs p)). + +Lemma max_pc_wf : + forall T m, Z.pos (max_pc_map m) <= Integers.Int.max_unsigned -> + @map_well_formed T m. +Proof. + unfold map_well_formed. intros. + exploit list_in_map_inv. eassumption. intros [x [A B]]. destruct x. + apply Maps.PTree.elements_complete in B. apply max_pc_map_sound in B. + unfold Ple in B. apply Pos2Z.pos_le_pos in B. subst. + simplify. transitivity (Z.pos (max_pc_map m)); eauto. +Qed. + (** * Operational Semantics *) Definition genv := Globalenvs.Genv.t fundef unit. @@ -247,14 +267,3 @@ Inductive final_state : state -> Integers.int -> Prop := Definition semantics (m : program) := Smallstep.Semantics step (initial_state m) final_state (Globalenvs.Genv.globalenv m). - -Lemma max_pc_wf : - forall T m, Z.pos (max_pc_map m) <= Integers.Int.max_unsigned -> - @map_well_formed T m. -Proof. - unfold map_well_formed. intros. - exploit list_in_map_inv. eassumption. intros [x [A B]]. destruct x. - apply Maps.PTree.elements_complete in B. apply max_pc_map_sound in B. - unfold Ple in B. apply Pos2Z.pos_le_pos in B. subst. - simplify. transitivity (Z.pos (max_pc_map m)); eauto. -Qed. -- cgit