From dc9ad1382ee548019e6ff546a24954057cdd8ff0 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Sat, 13 Nov 2021 23:02:44 +0000 Subject: Add RTLPar with functional units --- src/hls/HTLParFugen.v | 879 ++++++++++++++++++++++++++++++++++++++++++++++++++ src/hls/RTLParFU.v | 402 +++++++++++++++++++++++ src/hls/RTLParFUgen.v | 21 ++ 3 files changed, 1302 insertions(+) create mode 100644 src/hls/HTLParFugen.v create mode 100644 src/hls/RTLParFU.v create mode 100644 src/hls/RTLParFUgen.v (limited to 'src') diff --git a/src/hls/HTLParFugen.v b/src/hls/HTLParFugen.v new file mode 100644 index 0000000..a002e15 --- /dev/null +++ b/src/hls/HTLParFugen.v @@ -0,0 +1,879 @@ +(* + * Vericert: Verified high-level synthesis. + * Copyright (C) 2020 Yann Herklotz + * + * 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 . + *) + +Require Import Coq.micromega.Lia. + +Require Import compcert.common.AST. +Require compcert.common.Errors. +Require compcert.common.Globalenvs. +Require compcert.lib.Integers. +Require Import compcert.lib.Maps. + +Require Import vericert.common.Statemonad. +Require Import vericert.common.Vericertlib. +Require Import vericert.hls.AssocMap. +Require Import vericert.hls.HTL. +Require Import vericert.hls.Predicate. +Require Import vericert.hls.RTLParFU. +Require Import vericert.hls.ValueInt. +Require Import vericert.hls.Verilog. + +#[local] Hint Resolve AssocMap.gempty : htlh. +#[local] Hint Resolve AssocMap.gso : htlh. +#[local] Hint Resolve AssocMap.gss : htlh. +#[local] Hint Resolve Ple_refl : htlh. +#[local] Hint Resolve Ple_succ : htlh. + +Definition assignment : Type := expr -> expr -> stmnt. + +Record state: Type := mkstate { + st_st: reg; + st_freshreg: reg; + st_freshstate: node; + st_scldecls: AssocMap.t (option io * scl_decl); + st_arrdecls: AssocMap.t (option io * arr_decl); + st_datapath: datapath; + st_controllogic: controllogic; +}. + +Definition init_state (st : reg) : state := + mkstate st + 1%positive + 1%positive + (AssocMap.empty (option io * scl_decl)) + (AssocMap.empty (option io * arr_decl)) + (AssocMap.empty stmnt) + (AssocMap.empty stmnt). + +Module HTLState <: State. + + Definition st := state. + + Inductive st_incr: state -> state -> Prop := + state_incr_intro: + forall (s1 s2: state), + st_st s1 = st_st s2 -> + Ple s1.(st_freshreg) s2.(st_freshreg) -> + Ple s1.(st_freshstate) s2.(st_freshstate) -> + (forall n, + s1.(st_controllogic)!n = None + \/ s2.(st_controllogic)!n = s1.(st_controllogic)!n) -> + st_incr s1 s2. + #[local] Hint Constructors st_incr : htlh. + + Definition st_prop := st_incr. + #[local] Hint Unfold st_prop : htlh. + + Lemma st_refl : forall s, st_prop s s. + Proof. auto with htlh. Qed. + + Lemma st_trans : + forall s1 s2 s3, st_prop s1 s2 -> st_prop s2 s3 -> st_prop s1 s3. + Proof. + intros. inv H. inv H0. + apply state_incr_intro; eauto using Ple_trans; intros; try congruence. + destruct H4 with n; destruct H7 with n; intuition congruence. + Qed. + +End HTLState. +Export HTLState. + +Module HTLMonad := Statemonad(HTLState). +Export HTLMonad. + +Module HTLMonadExtra := Monad.MonadExtra(HTLMonad). +Import HTLMonadExtra. +Export MonadNotation. + +Definition state_goto (st : reg) (n : node) : stmnt := + Vnonblock (Vvar st) (Vlit (posToValue n)). + +Definition state_cond (st : reg) (c : expr) (n1 n2 : node) : stmnt := + Vnonblock (Vvar st) (Vternary c (posToExpr n1) (posToExpr n2)). + +Definition check_empty_node_datapath: + forall (s: state) (n: node), { s.(st_datapath)!n = None } + { True }. +Proof. + intros. case (s.(st_datapath)!n); tauto. +Defined. + +Definition check_empty_node_controllogic: + forall (s: state) (n: node), { s.(st_controllogic)!n = None } + { True }. +Proof. + intros. case (s.(st_controllogic)!n); tauto. +Defined. + +Lemma declare_reg_state_incr : + forall i s r sz, + st_incr s + (mkstate + s.(st_st) + s.(st_freshreg) + s.(st_freshstate) + (AssocMap.set r (i, VScalar sz) s.(st_scldecls)) + s.(st_arrdecls) + s.(st_datapath) + s.(st_controllogic)). +Proof. Admitted. + +Definition declare_reg (i : option io) (r : reg) (sz : nat) : mon unit := + fun s => OK tt (mkstate + s.(st_st) + s.(st_freshreg) + s.(st_freshstate) + (AssocMap.set r (i, VScalar sz) s.(st_scldecls)) + s.(st_arrdecls) + s.(st_datapath) + s.(st_controllogic)) + (declare_reg_state_incr i s r sz). + +Lemma add_instr_state_incr : + forall s n n' st, + (st_controllogic s)!n = None -> + st_incr s + (mkstate + s.(st_st) + s.(st_freshreg) + (st_freshstate s) + s.(st_scldecls) + s.(st_arrdecls) + (AssocMap.set n st s.(st_datapath)) + (AssocMap.set n (state_goto s.(st_st) n') s.(st_controllogic))). +Proof. + constructor; intros; + try (simpl; destruct (peq n n0); subst); + auto with htlh. +Qed. + +Definition add_instr (n : node) (n' : node) (st : stmnt) : mon unit := + fun s => + match check_empty_node_controllogic s n with + | left TRANS => + OK tt (mkstate + s.(st_st) + s.(st_freshreg) + (st_freshstate s) + s.(st_scldecls) + s.(st_arrdecls) + (AssocMap.set n st s.(st_datapath)) + (AssocMap.set n (state_goto s.(st_st) n') s.(st_controllogic))) + (add_instr_state_incr s n n' st TRANS) + | _ => Error (Errors.msg "HTL.add_instr") + end. + +Lemma add_instr_skip_state_incr : + forall s n st, + (st_controllogic s)!n = None -> + st_incr s + (mkstate + s.(st_st) + s.(st_freshreg) + (st_freshstate s) + s.(st_scldecls) + s.(st_arrdecls) + (AssocMap.set n st s.(st_datapath)) + (AssocMap.set n Vskip s.(st_controllogic))). +Proof. + constructor; intros; + try (simpl; destruct (peq n n0); subst); + auto with htlh. +Qed. + +Definition add_instr_skip (n : node) (st : stmnt) : mon unit := + fun s => + match check_empty_node_controllogic s n with + | left TRANS => + OK tt (mkstate + s.(st_st) + s.(st_freshreg) + (st_freshstate s) + s.(st_scldecls) + s.(st_arrdecls) + (AssocMap.set n st s.(st_datapath)) + (AssocMap.set n Vskip s.(st_controllogic))) + (add_instr_skip_state_incr s n st TRANS) + | _ => Error (Errors.msg "HTL.add_instr_skip") + end. + +Lemma add_node_skip_state_incr : + forall s n st, + (st_controllogic s)!n = None -> + st_incr s + (mkstate + s.(st_st) + s.(st_freshreg) + (st_freshstate s) + s.(st_scldecls) + s.(st_arrdecls) + (AssocMap.set n Vskip s.(st_datapath)) + (AssocMap.set n st s.(st_controllogic))). +Proof. + constructor; intros; + try (simpl; destruct (peq n n0); subst); + auto with htlh. +Qed. + +Definition add_node_skip (n : node) (st : stmnt) : mon unit := + fun s => + match check_empty_node_controllogic s n with + | left TRANS => + OK tt (mkstate + s.(st_st) + s.(st_freshreg) + (st_freshstate s) + s.(st_scldecls) + s.(st_arrdecls) + (AssocMap.set n Vskip s.(st_datapath)) + (AssocMap.set n st s.(st_controllogic))) + (add_node_skip_state_incr s n st TRANS) + | _ => Error (Errors.msg "HTL.add_node_skip") + end. + +Definition nonblock (dst : reg) (e : expr) := Vnonblock (Vvar dst) e. +Definition block (dst : reg) (e : expr) := Vblock (Vvar dst) e. + +Definition bop (op : binop) (r1 r2 : reg) : expr := + Vbinop op (Vvar r1) (Vvar r2). + +Definition boplit (op : binop) (r : reg) (l : Integers.int) : expr := + Vbinop op (Vvar r) (Vlit (intToValue l)). + +Definition boplitz (op: binop) (r: reg) (l: Z) : expr := + Vbinop op (Vvar r) (Vlit (ZToValue l)). + +Definition translate_comparison (c : Integers.comparison) (args : list reg) + : mon expr := + match c, args with + | Integers.Ceq, r1::r2::nil => ret (bop Veq r1 r2) + | Integers.Cne, r1::r2::nil => ret (bop Vne r1 r2) + | Integers.Clt, r1::r2::nil => ret (bop Vlt r1 r2) + | Integers.Cgt, r1::r2::nil => ret (bop Vgt r1 r2) + | Integers.Cle, r1::r2::nil => ret (bop Vle r1 r2) + | Integers.Cge, r1::r2::nil => ret (bop Vge r1 r2) + | _, _ => error (Errors.msg + "Htlgen: comparison instruction not implemented: other") + end. + +Definition translate_comparison_imm (c : Integers.comparison) (args : list reg) + (i: Integers.int) : mon expr := + match c, args with + | Integers.Ceq, r1::nil => ret (boplit Veq r1 i) + | Integers.Cne, r1::nil => ret (boplit Vne r1 i) + | Integers.Clt, r1::nil => ret (boplit Vlt r1 i) + | Integers.Cgt, r1::nil => ret (boplit Vgt r1 i) + | Integers.Cle, r1::nil => ret (boplit Vle r1 i) + | Integers.Cge, r1::nil => ret (boplit Vge r1 i) + | _, _ => error (Errors.msg + "Htlgen: comparison_imm instruction not implemented: other") + end. + +Definition translate_comparisonu (c : Integers.comparison) (args : list reg) + : mon expr := + match c, args with + | Integers.Clt, r1::r2::nil => ret (bop Vltu r1 r2) + | Integers.Cgt, r1::r2::nil => ret (bop Vgtu r1 r2) + | Integers.Cle, r1::r2::nil => ret (bop Vleu r1 r2) + | Integers.Cge, r1::r2::nil => ret (bop Vgeu r1 r2) + | _, _ => error (Errors.msg + "Htlgen: comparison instruction not implemented: other") + end. + +Definition translate_comparison_immu (c : Integers.comparison) + (args : list reg) (i: Integers.int) : mon expr := + match c, args with + | Integers.Clt, r1::nil => ret (boplit Vltu r1 i) + | Integers.Cgt, r1::nil => ret (boplit Vgtu r1 i) + | Integers.Cle, r1::nil => ret (boplit Vleu r1 i) + | Integers.Cge, r1::nil => ret (boplit Vgeu r1 i) + | _, _ => error (Errors.msg + "Htlgen: comparison_imm instruction not implemented: other") + end. + +Definition translate_condition (c : Op.condition) (args : list reg) + : mon expr := + match c, args with + | Op.Ccomp c, _ => translate_comparison c args + | Op.Ccompu c, _ => translate_comparisonu c args + | Op.Ccompimm c i, _ => translate_comparison_imm c args i + | Op.Ccompuimm c i, _ => translate_comparison_immu c args i + | Op.Cmaskzero n, _ => + error (Errors.msg "Htlgen: condition instruction not implemented: Cmaskzero") + | Op.Cmasknotzero n, _ => + error (Errors.msg + "Htlgen: condition instruction not implemented: Cmasknotzero") + | _, _ => + error (Errors.msg "Htlgen: condition instruction not implemented: other") + end. + +Definition check_address_parameter_signed (p : Z) : bool := + Z.leb Integers.Ptrofs.min_signed p + && Z.leb p Integers.Ptrofs.max_signed. + +Definition check_address_parameter_unsigned (p : Z) : bool := + Z.leb p Integers.Ptrofs.max_unsigned. + +Definition translate_eff_addressing (a: Op.addressing) (args: list reg) + : mon expr := + match a, args with (* TODO: We should be more methodical here; what are the possibilities?*) + | Op.Aindexed off, r1::nil => + if (check_address_parameter_signed off) + then ret (boplitz Vadd r1 off) + else error (Errors.msg ("HTLPargen: translate_eff_addressing (Aindexed): address out of bounds")) + | Op.Ascaled scale offset, r1::nil => + if (check_address_parameter_signed scale) && (check_address_parameter_signed offset) + then ret (Vbinop Vadd (boplitz Vmul r1 scale) (Vlit (ZToValue offset))) + else error (Errors.msg "HTLPargen: translate_eff_addressing (Ascaled): address out of bounds") + | Op.Aindexed2 offset, r1::r2::nil => + if (check_address_parameter_signed offset) + then ret (Vbinop Vadd (bop Vadd r1 r2) (Vlit (ZToValue offset))) + else error (Errors.msg "HTLPargen: translate_eff_addressing (Aindexed2): address out of bounds") + | Op.Aindexed2scaled scale offset, r1::r2::nil => (* Typical for dynamic array addressing *) + if (check_address_parameter_signed scale) && (check_address_parameter_signed offset) + then ret (Vbinop Vadd (Vvar r1) (Vbinop Vadd (boplitz Vmul r2 scale) (Vlit (ZToValue offset)))) + else error (Errors.msg "HTLPargen: translate_eff_addressing (Aindexed2scaled): address out of bounds") + | Op.Ainstack a, nil => (* We need to be sure that the base address is aligned *) + let a := Integers.Ptrofs.unsigned a in + if (check_address_parameter_unsigned a) + then ret (Vlit (ZToValue a)) + else error (Errors.msg "HTLPargen: translate_eff_addressing (Ainstack): address out of bounds") + | _, _ => error (Errors.msg "HTLPargen: translate_eff_addressing unsuported addressing") + end. + +(** Translate an instruction to a statement. FIX mulhs mulhu *) +Definition translate_instr (op : Op.operation) (args : list reg) : mon expr := + match op, args with + | Op.Omove, r::nil => ret (Vvar r) + | Op.Ointconst n, _ => ret (Vlit (intToValue n)) + | Op.Oneg, r::nil => ret (Vunop Vneg (Vvar r)) + | Op.Osub, r1::r2::nil => ret (bop Vsub r1 r2) + | Op.Omul, r1::r2::nil => ret (bop Vmul r1 r2) + | Op.Omulimm n, r::nil => ret (boplit Vmul r n) + | Op.Omulhs, r1::r2::nil => error (Errors.msg "Htlgen: Instruction not implemented: mulhs") + | Op.Omulhu, r1::r2::nil => error (Errors.msg "Htlgen: Instruction not implemented: mulhu") + | Op.Odiv, r1::r2::nil => ret (bop Vdiv r1 r2) + | Op.Odivu, r1::r2::nil => ret (bop Vdivu r1 r2) + | Op.Omod, r1::r2::nil => ret (bop Vmod r1 r2) + | Op.Omodu, r1::r2::nil => ret (bop Vmodu r1 r2) + | Op.Oand, r1::r2::nil => ret (bop Vand r1 r2) + | Op.Oandimm n, r::nil => ret (boplit Vand r n) + | Op.Oor, r1::r2::nil => ret (bop Vor r1 r2) + | Op.Oorimm n, r::nil => ret (boplit Vor r n) + | Op.Oxor, r1::r2::nil => ret (bop Vxor r1 r2) + | Op.Oxorimm n, r::nil => ret (boplit Vxor r n) + | Op.Onot, r::nil => ret (Vunop Vnot (Vvar r)) + | Op.Oshl, r1::r2::nil => ret (bop Vshl r1 r2) + | Op.Oshlimm n, r::nil => ret (boplit Vshl r n) + | Op.Oshr, r1::r2::nil => ret (bop Vshr r1 r2) + | Op.Oshrimm n, r::nil => ret (boplit Vshr r n) + | Op.Oshrximm n, r::nil => + ret (Vternary (Vbinop Vlt (Vvar r) (Vlit (ZToValue 0))) + (Vunop Vneg (Vbinop Vshru (Vunop Vneg (Vvar r)) (Vlit n))) + (Vbinop Vshru (Vvar r) (Vlit n))) + | Op.Oshru, r1::r2::nil => ret (bop Vshru r1 r2) + | Op.Oshruimm n, r::nil => ret (boplit Vshru r n) + | Op.Ororimm n, r::nil => error (Errors.msg "Htlgen: Instruction not implemented: Ororimm") + (*ret (Vbinop Vor (boplit Vshru r (Integers.Int.modu n (Integers.Int.repr 32))) + (boplit Vshl r (Integers.Int.sub (Integers.Int.repr 32) (Integers.Int.modu n (Integers.Int.repr 32)))))*) + | Op.Oshldimm n, r::nil => ret (Vbinop Vor (boplit Vshl r n) (boplit Vshr r (Integers.Int.sub (Integers.Int.repr 32) n))) + | Op.Ocmp c, _ => translate_condition c args + | Op.Osel c AST.Tint, r1::r2::rl => + do tc <- translate_condition c rl; + ret (Vternary tc (Vvar r1) (Vvar r2)) + | Op.Olea a, _ => translate_eff_addressing a args + | _, _ => error (Errors.msg "Htlgen: Instruction not implemented: other") + end. + +Lemma add_branch_instr_state_incr: + forall s e n n1 n2, + (st_controllogic s) ! n = None -> + st_incr s (mkstate + s.(st_st) + (st_freshreg s) + (st_freshstate s) + s.(st_scldecls) + s.(st_arrdecls) + (AssocMap.set n Vskip (st_datapath s)) + (AssocMap.set n (state_cond s.(st_st) e n1 n2) (st_controllogic s))). +Proof. + intros. apply state_incr_intro; simpl; + try (intros; destruct (peq n0 n); subst); + auto with htlh. +Qed. + +Definition add_branch_instr (e: expr) (n n1 n2: node) : mon unit := + fun s => + match check_empty_node_controllogic s n with + | left NTRANS => + OK tt (mkstate + s.(st_st) + (st_freshreg s) + (st_freshstate s) + s.(st_scldecls) + s.(st_arrdecls) + (AssocMap.set n Vskip (st_datapath s)) + (AssocMap.set n (state_cond s.(st_st) e n1 n2) (st_controllogic s))) + (add_branch_instr_state_incr s e n n1 n2 NTRANS) + | _ => Error (Errors.msg "Htlgen: add_branch_instr") + end. + +Definition translate_arr_access (mem : AST.memory_chunk) (addr : Op.addressing) + (args : list reg) (stack : reg) : mon expr := + match mem, addr, args with (* TODO: We should be more methodical here; what are the possibilities?*) + | Mint32, Op.Aindexed off, r1::nil => + if (check_address_parameter_signed off) + then ret (Vvari stack (Vbinop Vdivu (boplitz Vadd r1 off) (Vlit (ZToValue 4)))) + else error (Errors.msg "HTLgen: translate_arr_access address out of bounds") + | Mint32, Op.Aindexed2scaled scale offset, r1::r2::nil => (* Typical for dynamic array addressing *) + if (check_address_parameter_signed scale) && (check_address_parameter_signed offset) + then ret (Vvari stack + (Vbinop Vdivu + (Vbinop Vadd (boplitz Vadd r1 offset) (boplitz Vmul r2 scale)) + (Vlit (ZToValue 4)))) + else error (Errors.msg "HTLgen: translate_arr_access address out of bounds") + | Mint32, Op.Ainstack a, nil => (* We need to be sure that the base address is aligned *) + let a := Integers.Ptrofs.unsigned a in + if (check_address_parameter_unsigned a) + then ret (Vvari stack (Vlit (ZToValue (a / 4)))) + else error (Errors.msg "HTLgen: eff_addressing out of bounds stack offset") + | _, _, _ => error (Errors.msg "HTLgen: translate_arr_access unsuported addressing") + end. + +Fixpoint enumerate (i : nat) (ns : list node) {struct ns} : list (nat * node) := + match ns with + | n :: ns' => (i, n) :: enumerate (i+1) ns' + | nil => nil + end. + +Definition tbl_to_case_expr (st : reg) (ns : list node) : list (expr * stmnt) := + List.map (fun a => match a with + (i, n) => (Vlit (natToValue i), Vnonblock (Vvar st) (Vlit (posToValue n))) + end) + (enumerate 0 ns). + +Definition stack_correct (sz : Z) : bool := + (0 <=? sz) && (sz let r := s.(st_freshreg) in + OK r (mkstate + s.(st_st) + (Pos.succ r) + (st_freshstate s) + (AssocMap.set s.(st_freshreg) (i, VScalar sz) s.(st_scldecls)) + (st_arrdecls s) + (st_datapath s) + (st_controllogic s)) + (create_reg_state_incr s sz i). + +Lemma create_arr_state_incr: + forall s sz ln i, + st_incr s (mkstate + s.(st_st) + (Pos.succ (st_freshreg s)) + (st_freshstate s) + s.(st_scldecls) + (AssocMap.set s.(st_freshreg) (i, VArray sz ln) s.(st_arrdecls)) + (st_datapath s) + (st_controllogic s)). +Proof. constructor; simpl; auto with htlh. Qed. + +Definition create_arr (i : option io) (sz : nat) (ln : nat) : mon (reg * nat) := + fun s => let r := s.(st_freshreg) in + OK (r, ln) (mkstate + s.(st_st) + (Pos.succ r) + (st_freshstate s) + s.(st_scldecls) + (AssocMap.set s.(st_freshreg) (i, VArray sz ln) s.(st_arrdecls)) + (st_datapath s) + (st_controllogic s)) + (create_arr_state_incr s sz ln i). + +Definition max_pc_map (m : Maps.PTree.t stmnt) := + PTree.fold (fun m pc i => Pos.max m pc) m 1%positive. + +Lemma max_pc_map_sound: + forall m pc i, m!pc = Some i -> Ple pc (max_pc_map m). +Proof. + intros until i. + apply PTree_Properties.fold_rec with (P := fun c m => c!pc = Some i -> Ple pc m). + (* extensionality *) + intros. apply H0. rewrite H; auto. + (* base case *) + rewrite PTree.gempty. congruence. + (* inductive case *) + intros. rewrite PTree.gsspec in H2. destruct (peq pc k). + inv H2. unfold Ple, Plt in *. lia. + apply Ple_trans with a. auto. + unfold Ple, Plt in *. lia. +Qed. + +Lemma max_pc_wf : + forall m, Z.pos (max_pc_map m) <= Integers.Int.max_unsigned -> + map_well_formed 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. + +Definition poslength {A : Type} (l : list A) : positive := + match Zlength l with + | Z.pos p => p + | _ => 1 + end. + +Fixpoint penumerate {A : Type} (p : positive) (l : list A) {struct l} + : list (positive * A) := + match l with + | x :: xs => (p, x) :: penumerate (Pos.pred p) xs + | nil => nil + end. + +Fixpoint prange {A: Type} (p1 p2: positive) (l: list A) {struct l} := + match l with + | x :: xs => (p1, p2, x) :: prange p2 (Pos.pred p2) xs + | nil => nil + end. + +Lemma add_data_instr_state_incr : + forall s n st, + st_incr s + (mkstate + s.(st_st) + s.(st_freshreg) + (st_freshstate s) + s.(st_scldecls) + s.(st_arrdecls) + (AssocMap.set n (Vseq (AssocMapExt.get_default + _ Vskip n s.(st_datapath)) st) s.(st_datapath)) + s.(st_controllogic)). +Proof. + constructor; intros; + try (simpl; destruct (peq n n0); subst); + auto with htlh. +Qed. + +Definition add_data_instr (n : node) (st : stmnt) : mon unit := + fun s => + OK tt (mkstate + s.(st_st) + s.(st_freshreg) + (st_freshstate s) + s.(st_scldecls) + s.(st_arrdecls) + (AssocMap.set n (Vseq (AssocMapExt.get_default _ Vskip n s.(st_datapath)) st) s.(st_datapath)) + s.(st_controllogic)) + (add_data_instr_state_incr s n st). + +Lemma add_control_instr_state_incr : + forall s n st, + (st_controllogic s) ! n = None -> + st_incr s + (mkstate + s.(st_st) + s.(st_freshreg) + (st_freshstate s) + s.(st_scldecls) + s.(st_arrdecls) + s.(st_datapath) + (AssocMap.set n st s.(st_controllogic))). +Proof. + constructor; intros; + try (simpl; destruct (peq n n0); subst); + auto with htlh. +Qed. + +Definition add_control_instr (n : node) (st : stmnt) : mon unit := + fun s => + match check_empty_node_controllogic s n with + | left CTRL => + OK tt (mkstate + s.(st_st) + s.(st_freshreg) + (st_freshstate s) + s.(st_scldecls) + s.(st_arrdecls) + s.(st_datapath) + (AssocMap.set n st s.(st_controllogic))) + (add_control_instr_state_incr s n st CTRL) + | _ => + Error (Errors.msg "HTLPargen.add_control_instr: control logic is not empty") + end. + +Definition add_control_instr_force_state_incr : + forall s n st, + st_incr s + (mkstate + s.(st_st) + s.(st_freshreg) + (st_freshstate s) + s.(st_scldecls) + s.(st_arrdecls) + s.(st_datapath) + (AssocMap.set n st s.(st_controllogic))). +Admitted. + +Definition add_control_instr_force (n : node) (st : stmnt) : mon unit := + fun s => + OK tt (mkstate + s.(st_st) + s.(st_freshreg) + (st_freshstate s) + s.(st_scldecls) + s.(st_arrdecls) + s.(st_datapath) + (AssocMap.set n st s.(st_controllogic))) + (add_control_instr_force_state_incr s n st). + +Fixpoint pred_expr (preg: reg) (p: pred_op) := + match p with + | Plit (b, pred) => + if b + then Vrange preg (Vlit (posToValue pred)) (Vlit (posToValue pred)) + else Vunop Vnot (Vrange preg (Vlit (posToValue pred)) (Vlit (posToValue pred))) + | Ptrue => Vlit (ZToValue 1) + | Pfalse => Vlit (ZToValue 0) + | Pand p1 p2 => + Vbinop Vand (pred_expr preg p1) (pred_expr preg p2) + | Por p1 p2 => + Vbinop Vor (pred_expr preg p1) (pred_expr preg p2) + end. + +Definition translate_predicate (a : assignment) + (preg: reg) (p: option pred_op) (dst e: expr) := + match p with + | None => ret (a dst e) + | Some pos => + ret (a dst (Vternary (pred_expr preg pos) e dst)) + end. + +Definition translate_inst a (fin rtrn stack preg : reg) (n : node) (i : instr) + : mon stmnt := + match i with + | FUnop => + ret Vskip + | FUop p op args dst => + do instr <- translate_instr op args; + do _ <- declare_reg None dst 32; + translate_predicate a preg p (Vvar dst) instr + | FUload p chunk addr args dst => + do src <- translate_arr_access chunk addr args stack; + do _ <- declare_reg None dst 32; + translate_predicate a preg p (Vvar dst) src + | FUstore p chunk addr args src => + do dst <- translate_arr_access chunk addr args stack; + translate_predicate a preg p dst (Vvar src) + | FUsetpred _ c args p => + do cond <- translate_condition c args; + ret (a (pred_expr preg (Plit (true, p))) cond) + end. + +Lemma create_new_state_state_incr: + forall s p, + st_incr s + (mkstate + s.(st_st) + s.(st_freshreg) + (s.(st_freshstate) + p)%positive + s.(st_scldecls) + s.(st_arrdecls) + s.(st_datapath) + s.(st_controllogic)). +Admitted. + +Definition create_new_state (p: node): mon node := + fun s => OK s.(st_freshstate) + (mkstate + s.(st_st) + s.(st_freshreg) + (s.(st_freshstate) + p)%positive + s.(st_scldecls) + s.(st_arrdecls) + s.(st_datapath) + s.(st_controllogic)) + (create_new_state_state_incr s p). + +Definition translate_inst_list (fin rtrn stack preg: reg) (ni : node * node * list (list instr)) := + match ni with + | (n, p, 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. + +Fixpoint translate_cfi' (fin rtrn stack preg: reg) (cfi: cf_instr) + : mon (stmnt * stmnt) := + match cfi with + | FUgoto n' => + do st <- get; + ret (Vskip, state_goto st.(st_st) n') + | FUcond c args n1 n2 => + do st <- get; + do e <- translate_condition c args; + ret (Vskip, state_cond st.(st_st) e n1 n2) + | FUreturn r => + match r with + | Some r' => + ret ((Vseq (block fin (Vlit (ZToValue 1%Z))) (block rtrn (Vvar r'))), + Vskip) + | None => + ret ((Vseq (block fin (Vlit (ZToValue 1%Z))) (block rtrn (Vlit (ZToValue 0%Z)))), + Vskip) + end + | FUpred_cf p c1 c2 => + do (tc1s, tc1c) <- translate_cfi' fin rtrn stack preg c1; + do (tc2s, tc2c) <- translate_cfi' fin rtrn stack preg c2; + ret ((Vcond (pred_expr preg p) tc1s tc2s), (Vcond (pred_expr preg p) tc1c tc2c)) + | FUjumptable r tbl => + do s <- get; + ret (Vskip, Vcase (Vvar r) (list_to_stmnt (tbl_to_case_expr s.(st_st) tbl)) (Some Vskip)) + | FUcall sig ri rl r n => + error (Errors.msg "HTLPargen: RPcall not supported.") + | FUtailcall sig ri lr => + error (Errors.msg "HTLPargen: RPtailcall not supported.") + | FUbuiltin e lb b n => + error (Errors.msg "HTLPargen: RPbuildin not supported.") + end. + +Definition translate_cfi (fin rtrn stack preg: reg) (ni: node * cf_instr) + : mon unit := + let (n, cfi) := ni in + do (s, c) <- translate_cfi' fin rtrn stack preg cfi; + do _ <- add_control_instr n c; + add_data_instr n s. + +Definition transf_bblock (fin rtrn stack preg: reg) (ni : node * bblock) + : mon unit := + let (n, bb) := ni in + do nstate <- create_new_state ((poslength bb.(bb_body)))%positive; + do _ <- collectlist (translate_inst_list fin rtrn stack preg) + (prange n (nstate + poslength bb.(bb_body) - 1)%positive + bb.(bb_body)); + match bb.(bb_body) with + | nil => translate_cfi fin rtrn stack preg (n, bb.(bb_exit)) + | _ => translate_cfi fin rtrn stack preg (nstate, bb.(bb_exit)) + end. + +Definition decide_order a b c d e f g : {module_ordering a b c d e f g} + {True}. + refine (match bool_dec ((a left _ + | _ => _ + end); auto. + simplify; repeat match goal with + | H: context[(_ apply Pos.ltb_lt in H + end; unfold module_ordering; auto. +Defined. + +Definition transf_module (f: function) : mon HTL.module. + refine ( + if stack_correct f.(fn_stacksize) then + do fin <- create_reg (Some Voutput) 1; + do rtrn <- create_reg (Some Voutput) 32; + do (stack, stack_len) <- create_arr None 32 + (Z.to_nat (f.(fn_stacksize) / 4)); + do preg <- create_reg None 32; + do _ <- collectlist (transf_bblock fin rtrn stack preg) + (Maps.PTree.elements f.(fn_code)); + do _ <- collectlist (fun r => declare_reg (Some Vinput) r 32) + f.(fn_params); + do start <- create_reg (Some Vinput) 1; + do rst <- create_reg (Some Vinput) 1; + do clk <- create_reg (Some Vinput) 1; + do current_state <- get; + match zle (Z.pos (max_pc_map current_state.(st_datapath))) + Integers.Int.max_unsigned, + zle (Z.pos (max_pc_map current_state.(st_controllogic))) + Integers.Int.max_unsigned, + decide_order (st_st current_state) fin rtrn stack start rst clk, + max_list_dec (fn_params f) (st_st current_state) + with + | left LEDATA, left LECTRL, left MORD, left WFPARAMS => + ret (HTL.mkmodule + f.(fn_params) + current_state.(st_datapath) + current_state.(st_controllogic) + f.(fn_entrypoint) + current_state.(st_st) + stack + stack_len + fin + rtrn + start + rst + clk + current_state.(st_scldecls) + current_state.(st_arrdecls) + None + (conj (max_pc_wf _ LECTRL) (max_pc_wf _ LEDATA)) + MORD + _ + WFPARAMS) + | _, _, _, _ => error (Errors.msg "More than 2^32 states.") + end + else error (Errors.msg "Stack size misalignment.")); discriminate. +Defined. + +Definition max_state (f: function) : state := + let st := Pos.succ (max_reg_function f) in + mkstate st + (Pos.succ st) + (Pos.succ (max_pc_function f)) + (AssocMap.set st (None, VScalar 32) (st_scldecls (init_state st))) + (st_arrdecls (init_state st)) + (st_datapath (init_state st)) + (st_controllogic (init_state st)). + +Definition transl_module (f : function) : Errors.res HTL.module := + run_mon (max_state f) (transf_module f). + +Definition transl_fundef := transf_partial_fundef transl_module. + +Definition main_is_internal (p : RTLParFU.program) : bool := + let ge := Globalenvs.Genv.globalenv p in + match Globalenvs.Genv.find_symbol ge p.(AST.prog_main) with + | Some b => + match Globalenvs.Genv.find_funct_ptr ge b with + | Some (AST.Internal _) => true + | _ => false + end + | _ => false + end. + +Definition transl_program (p : RTLParFU.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/RTLParFU.v b/src/hls/RTLParFU.v new file mode 100644 index 0000000..3442ff0 --- /dev/null +++ b/src/hls/RTLParFU.v @@ -0,0 +1,402 @@ +(* + * Vericert: Verified high-level synthesis. + * Copyright (C) 2020-2021 Yann Herklotz + * + * 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 . + *) + +Require Import compcert.backend.Registers. +Require Import compcert.common.AST. +Require Import compcert.common.Events. +Require Import compcert.common.Globalenvs. +Require Import compcert.common.Memory. +Require Import compcert.common.Smallstep. +Require Import compcert.common.Values. +Require Import compcert.lib.Coqlib. +Require Import compcert.lib.Integers. +Require Import compcert.lib.Maps. +Require Import compcert.verilog.Op. + +Require Import vericert.hls.FunctionalUnits. +Require Import Predicate. +Require Import Vericertlib. + +Definition node := positive. + +Inductive instr : Type := +| FUnop : instr +| FUop : option pred_op -> operation -> list reg -> reg -> instr +| FUload : option pred_op -> memory_chunk -> addressing -> list reg -> reg -> instr +| FUstore : option pred_op -> memory_chunk -> addressing -> list reg -> reg -> instr +| FUsetpred : option pred_op -> condition -> list reg -> predicate -> instr. + +Inductive cf_instr : Type := +| FUcall : signature -> reg + ident -> list reg -> reg -> node -> cf_instr +| FUtailcall : signature -> reg + ident -> list reg -> cf_instr +| FUbuiltin : external_function -> list (builtin_arg reg) -> + builtin_res reg -> node -> cf_instr +| FUcond : condition -> list reg -> node -> node -> cf_instr +| FUjumptable : reg -> list node -> cf_instr +| FUreturn : option reg -> cf_instr +| FUgoto : node -> cf_instr +| FUpred_cf : pred_op -> cf_instr -> cf_instr -> cf_instr. + +Fixpoint successors_instr (i : cf_instr) : list node := + match i with + | FUcall sig ros args res s => s :: nil + | FUtailcall sig ros args => nil + | FUbuiltin ef args res s => s :: nil + | FUcond cond args ifso ifnot => ifso :: ifnot :: nil + | FUjumptable arg tbl => tbl + | FUreturn optarg => nil + | FUgoto n => n :: nil + | FUpred_cf p c1 c2 => concat (successors_instr c1 :: successors_instr c2 :: nil) + end. + +Definition max_reg_instr (m: positive) (i: instr) := + match i with + | FUnop => m + | FUop p op args res => + fold_left Pos.max args (Pos.max res m) + | FUload p chunk addr args dst => + fold_left Pos.max args (Pos.max dst m) + | FUstore p chunk addr args src => + fold_left Pos.max args (Pos.max src m) + | FUsetpred p' c args p => + fold_left Pos.max args m + end. + +Fixpoint max_reg_cfi (m : positive) (i : cf_instr) := + match i with + | FUcall sig (inl r) args res s => + fold_left Pos.max args (Pos.max r (Pos.max res m)) + | FUcall sig (inr id) args res s => + fold_left Pos.max args (Pos.max res m) + | FUtailcall sig (inl r) args => + fold_left Pos.max args (Pos.max r m) + | FUtailcall sig (inr id) args => + fold_left Pos.max args m + | FUbuiltin ef args res s => + fold_left Pos.max (params_of_builtin_args args) + (fold_left Pos.max (params_of_builtin_res res) m) + | FUcond cond args ifso ifnot => fold_left Pos.max args m + | FUjumptable arg tbl => Pos.max arg m + | FUreturn None => m + | FUreturn (Some arg) => Pos.max arg m + | FUgoto n => m + | FUpred_cf p c1 c2 => Pos.max (max_reg_cfi m c1) (max_reg_cfi m c2) + end. + +Definition regset := Regmap.t val. +Definition predset := PMap.t bool. + +Definition eval_predf (pr: predset) (p: pred_op) := + sat_predicate p (fun x => pr !! (Pos.of_nat x)). + +#[global] + Instance eval_predf_Proper : Proper (eq ==> equiv ==> eq) eval_predf. +Proof. + unfold Proper. simplify. unfold "==>". + intros. + unfold sat_equiv in *. intros. unfold eval_predf. subst. apply H0. +Qed. + +#[local] Open Scope pred_op. + +Lemma eval_predf_Pand : + forall ps p p', + eval_predf ps (p ∧ p') = eval_predf ps p && eval_predf ps p'. +Proof. unfold eval_predf; split; simplify; auto with bool. Qed. + +Lemma eval_predf_Por : + forall ps p p', + eval_predf ps (p ∨ p') = eval_predf ps p || eval_predf ps p'. +Proof. unfold eval_predf; split; simplify; auto with bool. Qed. + +Lemma eval_predf_pr_equiv : + forall p ps ps', + (forall x, ps !! x = ps' !! x) -> + eval_predf ps p = eval_predf ps' p. +Proof. + induction p; simplify; auto; + try (unfold eval_predf; simplify; repeat (destruct_match; []); inv Heqp0; rewrite <- H; auto); + [repeat rewrite eval_predf_Pand|repeat rewrite eval_predf_Por]; + erewrite IHp1; try eassumption; erewrite IHp2; eauto. +Qed. + +Fixpoint init_regs (vl: list val) (rl: list reg) {struct rl} : regset := + match rl, vl with + | r1 :: rs, v1 :: vs => Regmap.set r1 v1 (init_regs vs rs) + | _, _ => Regmap.init Vundef + end. + +Definition bblock_body := list (list (list instr)). + +Record bblock : Type := + mk_bblock { + bb_body: bblock_body; + bb_exit: cf_instr + }. + +Definition code: Type := PTree.t bblock. + +Record function: Type := + mkfunction { + fn_sig: signature; + fn_params: list reg; + fn_stacksize: Z; + fn_code: code; + fn_funct_units: funct_unit; + fn_entrypoint: node; + }. + +Definition fundef := AST.fundef function. +Definition program := AST.program fundef unit. + +Definition funsig (fd: fundef) := + match fd with + | Internal f => fn_sig f + | External ef => ef_sig ef + end. + +Inductive stackframe : Type := +| Stackframe: + forall (res: reg) (**r where to store the result *) + (f: function) (**r calling function *) + (sp: val) (**r stack pointer in calling function *) + (pc: node) (**r program point in calling function *) + (rs: regset) (**r register state in calling function *) + (pr: predset), (**r predicate state of the calling function *) + stackframe. + +Inductive state : Type := +| State: + forall (stack: list stackframe) (**r call stack *) + (f: function) (**r current function *) + (sp: val) (**r stack pointer *) + (pc: node) (**r current program point in [c] *) + (rs: regset) (**r register state *) + (pr: predset) (**r predicate register state *) + (m: mem), (**r memory state *) + state +| Callstate: + forall (stack: list stackframe) (**r call stack *) + (f: fundef) (**r function to call *) + (args: list val) (**r arguments to the call *) + (m: mem), (**r memory state *) + state +| Returnstate: + forall (stack: list stackframe) (**r call stack *) + (v: val) (**r return value for the call *) + (m: mem), (**r memory state *) + state. + +Record instr_state := mk_instr_state { + is_rs: regset; + is_ps: predset; + is_mem: mem; + }. + +Definition genv := Genv.t fundef unit. + +Section RELSEM. + + Context (ge: genv). + + Definition find_function + (ros: reg + ident) (rs: regset) : option fundef := + match ros with + | inl r => Genv.find_funct ge rs#r + | inr symb => + match Genv.find_symbol ge symb with + | None => None + | Some b => Genv.find_funct_ptr ge b + end + end. + + Inductive eval_pred: option pred_op -> instr_state -> instr_state -> instr_state -> Prop := + | eval_pred_true: + forall i i' p, + eval_predf (is_ps i) p = true -> + eval_pred (Some p) i i' i' + | eval_pred_false: + forall i i' p, + eval_predf (is_ps i) p = false -> + eval_pred (Some p) i i' i + | eval_pred_none: + forall i i', eval_pred None i i' i. + + Inductive step_instr: val -> instr_state -> instr -> instr_state -> Prop := + | exec_FUnop: + forall sp ist, + step_instr sp ist FUnop ist + | exec_FUop: + forall op v res args rs m sp p ist pr, + eval_operation ge sp op rs##args m = Some v -> + 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) (FUop p op args res) ist + | exec_FUload: + 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 (mk_instr_state rs pr m) (mk_instr_state (rs#dst <- v) pr m) ist -> + step_instr sp (mk_instr_state rs pr m) (FUload p chunk addr args dst) ist + | exec_FUstore: + 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 (mk_instr_state rs pr m) (mk_instr_state rs pr m') ist -> + step_instr sp (mk_instr_state rs pr m) (FUstore p chunk addr args src) ist + | exec_FUsetpred: + forall sp rs pr m p c b args p' ist, + Op.eval_condition c rs##args m = Some b -> + eval_pred p' (mk_instr_state rs pr m) (mk_instr_state rs (pr#p <- b) m) ist -> + step_instr sp (mk_instr_state rs pr m) (FUsetpred p' c args p) ist. + + Inductive step_instr_list: val -> instr_state -> list instr -> instr_state -> Prop := + | exec_RBcons: + forall state i state' state'' instrs sp, + step_instr sp state i state' -> + step_instr_list sp state' instrs state'' -> + step_instr_list sp state (i :: instrs) state'' + | exec_RBnil: + 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 -> bblock_body -> instr_state -> Prop := + | exec_instr_block_cons: + forall state i state' state'' instrs, + 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: + forall state, + step_instr_block sp state nil state. + + Inductive step_cf_instr: state -> cf_instr -> trace -> state -> Prop := + | exec_FUcall: + forall s f sp rs m res fd ros sig args pc pc' pr, + find_function ros rs = Some fd -> + funsig fd = sig -> + step_cf_instr (State s f sp pc rs pr m) (FUcall sig ros args res pc') + E0 (Callstate (Stackframe res f sp pc' rs pr :: s) fd rs##args m) + | exec_FUtailcall: + forall s f stk rs m sig ros args fd m' pc pr, + find_function ros rs = Some fd -> + funsig fd = sig -> + Mem.free m stk 0 f.(fn_stacksize) = Some m' -> + step_cf_instr (State s f (Vptr stk Ptrofs.zero) pc rs pr m) (FUtailcall sig ros args) + E0 (Callstate s fd rs##args m') + | exec_FUbuiltin: + forall s f sp rs m ef args res pc' vargs t vres m' pc pr, + eval_builtin_args ge (fun r => rs#r) sp m args vargs -> + external_call ef ge vargs m t vres m' -> + step_cf_instr (State s f sp pc rs pr m) (FUbuiltin ef args res pc') + t (State s f sp pc' (regmap_setres res vres rs) pr m') + | exec_FUcond: + forall s f sp rs m cond args ifso ifnot b pc pc' pr, + eval_condition cond rs##args m = Some b -> + pc' = (if b then ifso else ifnot) -> + step_cf_instr (State s f sp pc rs pr m) (FUcond cond args ifso ifnot) + E0 (State s f sp pc' rs pr m) + | exec_FUjumptable: + forall s f sp rs m arg tbl n pc pc' pr, + rs#arg = Vint n -> + list_nth_z tbl (Int.unsigned n) = Some pc' -> + step_cf_instr (State s f sp pc rs pr m) (FUjumptable arg tbl) + E0 (State s f sp pc' rs pr m) + | exec_FUreturn: + forall s f stk rs m or pc m' pr, + Mem.free m stk 0 f.(fn_stacksize) = Some m' -> + step_cf_instr (State s f (Vptr stk Ptrofs.zero) pc rs pr m) (FUreturn or) + E0 (Returnstate s (regmap_optget or Vundef rs) m') + | exec_FUgoto: + forall s f sp pc rs pr m pc', + step_cf_instr (State s f sp pc rs pr m) (FUgoto pc') E0 (State s f sp pc' rs pr m) + | exec_FUpred_cf: + forall s f sp pc rs pr m cf1 cf2 st' p t, + step_cf_instr (State s f sp pc rs pr m) (if eval_predf pr p then cf1 else cf2) t st' -> + step_cf_instr (State s f sp pc rs pr m) (FUpred_cf p cf1 cf2) t st'. + + Inductive step: state -> trace -> state -> Prop := + | 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 (mk_instr_state rs pr m) bb.(bb_body) (mk_instr_state rs' pr' m') -> + step_cf_instr (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: + forall s f args m m' stk, + Mem.alloc m 0 f.(fn_stacksize) = (m', stk) -> + step (Callstate s (Internal f) args m) + E0 (State s + f + (Vptr stk Ptrofs.zero) + f.(fn_entrypoint) + (init_regs args f.(fn_params)) + (PMap.init false) m') + | exec_function_external: + forall s ef args res t m m', + external_call ef ge args m t res m' -> + step (Callstate s (External ef) args m) + t (Returnstate s res m') + | exec_return: + forall res f sp pc rs s vres m pr, + step (Returnstate (Stackframe res f sp pc rs pr :: s) vres m) + E0 (State s f sp pc (rs#res <- vres) pr m). + +End RELSEM. + +Inductive initial_state (p: program): state -> Prop := +| initial_state_intro: forall b f m0, + let ge := Genv.globalenv p in + Genv.init_mem p = Some m0 -> + Genv.find_symbol ge p.(prog_main) = Some b -> + Genv.find_funct_ptr ge b = Some f -> + funsig f = signature_main -> + initial_state p (Callstate nil f nil m0). + +Inductive final_state: state -> int -> Prop := +| final_state_intro: forall r m, + final_state (Returnstate nil (Vint r) m) r. + +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 (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) := + Pos.max + (PTree.fold max_reg_bblock f.(fn_code) 1%positive) + (fold_left Pos.max f.(fn_params) 1%positive). + +Definition max_pc_function (f: function) : positive := + PTree.fold (fun m pc i => (Pos.max m + (pc + match Zlength i.(bb_body) + with Z.pos p => p | _ => 1 end))%positive) + f.(fn_code) 1%positive. diff --git a/src/hls/RTLParFUgen.v b/src/hls/RTLParFUgen.v new file mode 100644 index 0000000..389d76c --- /dev/null +++ b/src/hls/RTLParFUgen.v @@ -0,0 +1,21 @@ +Require Import Coq.micromega.Lia. + +Require Import compcert.common.AST. +Require compcert.common.Errors. +Require compcert.common.Globalenvs. +Require compcert.lib.Integers. +Require Import compcert.lib.Maps. + +Require Import vericert.common.Statemonad. +Require Import vericert.common.Vericertlib. +Require Import vericert.hls.AssocMap. +Require Import vericert.hls.HTL. +Require Import vericert.hls.Predicate. +Require Import vericert.hls.RTLParFU. +Require Import vericert.hls.ValueInt. +Require Import vericert.hls.Verilog. +Require Import vericert.hls.RTLBlockInstr. +Require Import vericert.hls.RTLPar. + +Definition transl_program (p : RTLParFU.program) : Errors.res HTL.program := + transform_partial_program transl_fundef p. -- cgit