diff options
author | Yann Herklotz <git@yannherklotz.com> | 2023-07-29 13:49:03 +0100 |
---|---|---|
committer | Yann Herklotz <git@yannherklotz.com> | 2023-07-29 13:49:03 +0100 |
commit | 502e49e2f8c95b40cd0761cbb69c863904169f8b (patch) | |
tree | e417f9a1d17f84a25ecd00be1ccb9cdda8b8e6ea /src/hls/HTLPargen.v | |
parent | 93117b6e766c25c5aeecdc20a963d5114fb91e59 (diff) | |
download | vericert-502e49e2f8c95b40cd0761cbb69c863904169f8b.tar.gz vericert-502e49e2f8c95b40cd0761cbb69c863904169f8b.zip |
Add beginning to memory generation proof
Diffstat (limited to 'src/hls/HTLPargen.v')
-rw-r--r-- | src/hls/HTLPargen.v | 968 |
1 files changed, 334 insertions, 634 deletions
diff --git a/src/hls/HTLPargen.v b/src/hls/HTLPargen.v index b602ab6..10c4357 100644 --- a/src/hls/HTLPargen.v +++ b/src/hls/HTLPargen.v @@ -1,6 +1,7 @@ -(* +(* * Vericert: Verified high-level synthesis. - * Copyright (C) 2021 Yann Herklotz <yann@yannherklotz.com> + * Copyright (C) 2020 Yann Herklotz <yann@yannherklotz.com> + * 2020 James Pollard <j@mes.dev> * * 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 @@ -18,23 +19,21 @@ Require Import Coq.micromega.Lia. -Require Import compcert.common.AST. -Require compcert.common.Errors. +Require Import compcert.lib.Maps. +Require Import compcert.common.Errors. Require compcert.common.Globalenvs. Require compcert.lib.Integers. -Require Import compcert.lib.Maps. +Require Import compcert.common.AST. Require Import vericert.common.Statemonad. Require Import vericert.common.Vericertlib. Require Import vericert.hls.AssocMap. -Require Import vericert.hls.FunctionalUnits. -Require Import vericert.hls.HTL. -Require Import vericert.hls.Predicate. -Require Import vericert.hls.GiblePar. -Require Import vericert.hls.Gible. -Require Import vericert.hls.FunctionalUnits. +Require Import vericert.hls.DHTL. Require Import vericert.hls.ValueInt. Require Import vericert.hls.Verilog. +Require Import vericert.hls.Gible. +Require Import vericert.hls.GiblePar. +Require Import vericert.hls.Predicate. #[local] Hint Resolve AssocMap.gempty : htlh. #[local] Hint Resolve AssocMap.gso : htlh. @@ -42,16 +41,13 @@ Require Import vericert.hls.Verilog. #[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_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 := @@ -60,7 +56,6 @@ Definition init_state (st : reg) : state := 1%positive (AssocMap.empty (option io * scl_decl)) (AssocMap.empty (option io * arr_decl)) - (AssocMap.empty stmnt) (AssocMap.empty stmnt). Module HTLState <: State. @@ -74,23 +69,20 @@ Module HTLState <: State. 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) -> + s1.(st_datapath)!n = None \/ s2.(st_datapath)!n = s1.(st_datapath)!n) -> st_incr s1 s2. - #[local] Hint Constructors st_incr : htlh. + #[export] Hint Constructors st_incr : htlh. Definition st_prop := st_incr. - #[local] Hint Unfold st_prop : htlh. + #[export] Hint Unfold st_prop : htlh. - Lemma st_refl : forall s, st_prop s s. - Proof. auto with htlh. Qed. + 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. + 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. @@ -102,14 +94,18 @@ Export HTLMonad. Module HTLMonadExtra := Monad.MonadExtra(HTLMonad). Import HTLMonadExtra. Export MonadNotation. + #[local] Open Scope monad_scope. +Definition pred_lit (preg: reg) (pred: predicate) := + Vrange preg (Vlit (posToValue pred)) (Vlit (posToValue pred)). + 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))) + then pred_lit preg pred + else Vunop Vnot (pred_lit preg pred) | Ptrue => Vlit (ZToValue 1) | Pfalse => Vlit (ZToValue 0) | Pand p1 p2 => @@ -118,14 +114,20 @@ Fixpoint pred_expr (preg: reg) (p: pred_op) := Vbinop Vor (pred_expr preg p1) (pred_expr preg p2) end. +Definition assignment : Type := expr -> expr -> stmnt. + Definition translate_predicate (a : assignment) (preg: reg) (p: option pred_op) (dst e: expr) := match p with | None => a dst e | Some pos => - a dst (Vternary (pred_expr preg pos) e dst) + let pos' := deep_simplify peq pos in + match sat_pred_simple (negate pos') with + | None => a dst e + | Some _ => a dst (Vternary (pred_expr preg pos') e dst) + end end. - + Definition state_goto (preg: reg) (p: option pred_op) (st : reg) (n : node) : stmnt := translate_predicate Vblock preg p (Vvar st) (Vlit (posToValue n)). @@ -138,11 +140,11 @@ 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. +Definition append_instr (n : node) (st : stmnt) (d : datapath) : datapath := + match AssocMap.get n d with + | Some st' => AssocMap.set n (Vseq st' st) d + | None => AssocMap.set n st d + end. Lemma declare_reg_state_incr : forall i s r sz, @@ -153,8 +155,7 @@ Lemma declare_reg_state_incr : s.(st_freshstate) (AssocMap.set r (i, VScalar sz) s.(st_scldecls)) s.(st_arrdecls) - s.(st_datapath) - s.(st_controllogic)). + s.(st_datapath)). Proof. Admitted. Definition declare_reg (i : option io) (r : reg) (sz : nat) : mon unit := @@ -164,8 +165,7 @@ Definition declare_reg (i : option io) (r : reg) (sz : nat) : mon unit := s.(st_freshstate) (AssocMap.set r (i, VScalar sz) s.(st_scldecls)) s.(st_arrdecls) - s.(st_datapath) - s.(st_controllogic)) + s.(st_datapath)) (declare_reg_state_incr i s r sz). Lemma declare_arr_state_incr : @@ -177,8 +177,7 @@ Lemma declare_arr_state_incr : s.(st_freshstate) s.(st_scldecls) (AssocMap.set r (i, VArray sz ln) s.(st_arrdecls)) - s.(st_datapath) - s.(st_controllogic)). + s.(st_datapath)). Proof. Admitted. Definition declare_arr (i : option io) (r : reg) (sz : nat) (ln : nat) : mon unit := @@ -188,112 +187,9 @@ Definition declare_arr (i : option io) (r : reg) (sz : nat) (ln : nat) : mon uni s.(st_freshstate) s.(st_scldecls) (AssocMap.set r (i, VArray sz ln) s.(st_arrdecls)) - s.(st_datapath) - s.(st_controllogic)) + s.(st_datapath)) (declare_arr_state_incr i s r sz ln). -Lemma add_instr_state_incr : - forall s preg p 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 preg p s.(st_st) n') s.(st_controllogic))). -Proof. - constructor; intros; - try (simpl; destruct (peq n n0); subst); - auto with htlh. -Qed. - -Definition add_instr (preg: reg) (p: option pred_op) (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 preg p s.(st_st) n') s.(st_controllogic))) - (add_instr_state_incr s preg p 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. @@ -306,68 +202,57 @@ Definition boplit (op : binop) (r : reg) (l : Integers.int) : expr := 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 := +Definition translate_comparison (c : Integers.comparison) (args : list reg) : Errors.res 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") + | Integers.Ceq, r1::r2::nil => Errors.OK (bop Veq r1 r2) + | Integers.Cne, r1::r2::nil => Errors.OK (bop Vne r1 r2) + | Integers.Clt, r1::r2::nil => Errors.OK (bop Vlt r1 r2) + | Integers.Cgt, r1::r2::nil => Errors.OK (bop Vgt r1 r2) + | Integers.Cle, r1::r2::nil => Errors.OK (bop Vle r1 r2) + | Integers.Cge, r1::r2::nil => Errors.OK (bop Vge r1 r2) + | _, _ => Errors.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 := +Definition translate_comparison_imm (c : Integers.comparison) (args : list reg) (i: Integers.int) + : Errors.res 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") + | Integers.Ceq, r1::nil => Errors.OK (boplit Veq r1 i) + | Integers.Cne, r1::nil => Errors.OK (boplit Vne r1 i) + | Integers.Clt, r1::nil => Errors.OK (boplit Vlt r1 i) + | Integers.Cgt, r1::nil => Errors.OK (boplit Vgt r1 i) + | Integers.Cle, r1::nil => Errors.OK (boplit Vle r1 i) + | Integers.Cge, r1::nil => Errors.OK (boplit Vge r1 i) + | _, _ => Errors.Error (Errors.msg "Htlgen: comparison_imm instruction not implemented: other") end. -Definition translate_comparisonu (c : Integers.comparison) (args : list reg) - : mon expr := +Definition translate_comparisonu (c : Integers.comparison) (args : list reg) : Errors.res 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") + | Integers.Clt, r1::r2::nil => Errors.OK (bop Vltu r1 r2) + | Integers.Cgt, r1::r2::nil => Errors.OK (bop Vgtu r1 r2) + | Integers.Cle, r1::r2::nil => Errors.OK (bop Vleu r1 r2) + | Integers.Cge, r1::r2::nil => Errors.OK (bop Vgeu r1 r2) + | _, _ => Errors.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 := +Definition translate_comparison_immu (c : Integers.comparison) (args : list reg) (i: Integers.int) + : Errors.res 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") + | Integers.Clt, r1::nil => Errors.OK (boplit Vltu r1 i) + | Integers.Cgt, r1::nil => Errors.OK (boplit Vgtu r1 i) + | Integers.Cle, r1::nil => Errors.OK (boplit Vleu r1 i) + | Integers.Cge, r1::nil => Errors.OK (boplit Vgeu r1 i) + | _, _ => Errors.Error (Errors.msg "Htlgen: comparison_imm instruction not implemented: other") end. -Definition translate_condition (c : Op.condition) (args : list reg) - : mon expr := +Definition translate_condition (c : Op.condition) (args : list reg) : Errors.res 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") + | Op.Cmaskzero n, _ => Errors.Error (Errors.msg "Htlgen: condition instruction not implemented: Cmaskzero") + | Op.Cmasknotzero n, _ => Errors.Error (Errors.msg "Htlgen: condition instruction not implemented: Cmasknotzero") + | _, _ => Errors.Error (Errors.msg "Htlgen: condition instruction not implemented: other") end. Definition check_address_parameter_signed (p : Z) : bool := @@ -377,136 +262,100 @@ Definition check_address_parameter_signed (p : Z) : bool := Definition check_address_parameter_unsigned (p : Z) : bool := Z.leb p Integers.Ptrofs.max_unsigned. -Lemma create_reg_state_incr: - forall s sz i, - st_incr s (mkstate - s.(st_st) - (Pos.succ (st_freshreg s)) - (st_freshstate s) - (AssocMap.set s.(st_freshreg) (i, VScalar sz) s.(st_scldecls)) - s.(st_arrdecls) - (st_datapath s) - (st_controllogic s)). -Proof. constructor; simpl; auto with htlh. Qed. - -Definition create_reg (i : option io) (sz : nat) : mon reg := - fun s => 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). - -Definition translate_eff_addressing (a: Op.addressing) (args: list reg) - : mon expr := +Definition translate_eff_addressing (a: Op.addressing) (args: list reg) : Errors.res 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")) + then Errors.OK (boplitz Vadd r1 off) + else Errors.Error (Errors.msg "Veriloggen: 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") + then Errors.OK (Vbinop Vadd (boplitz Vmul r1 scale) (Vlit (ZToValue offset))) + else Errors.Error (Errors.msg "Veriloggen: 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") + then Errors.OK (Vbinop Vadd (bop Vadd r1 r2) (Vlit (ZToValue offset))) + else Errors.Error (Errors.msg "Veriloggen: 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") + then Errors.OK (Vbinop Vadd (Vvar r1) (Vbinop Vadd (boplitz Vmul r2 scale) (Vlit (ZToValue offset)))) + else Errors.Error (Errors.msg "Veriloggen: 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") + then Errors.OK (Vlit (ZToValue a)) + else Errors.Error (Errors.msg "Veriloggen: translate_eff_addressing (Ainstack): address out of bounds") + | _, _ => Errors.Error (Errors.msg "Veriloggen: translate_eff_addressing unsuported addressing") end. -(*| -Translate an instruction to a statement. FIX mulhs mulhu -|*) +#[local] Close Scope monad_scope. +#[local] Open Scope error_monad_scope. -Definition translate_instr (op : Op.operation) (args : list reg) : mon expr := +(** Translate an instruction to a statement. FIX mulhs mulhu *) +Definition translate_instr (op : Op.operation) (args : list reg) : Errors.res 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.Omove, r::nil => Errors.OK (Vvar r) + | Op.Ointconst n, _ => Errors.OK (Vlit (intToValue n)) + | Op.Oneg, r::nil => Errors.OK (Vunop Vneg (Vvar r)) + | Op.Osub, r1::r2::nil => Errors.OK (bop Vsub r1 r2) + | Op.Omul, r1::r2::nil => Errors.OK (bop Vmul r1 r2) + | Op.Omulimm n, r::nil => Errors.OK (boplit Vmul r n) + | Op.Omulhs, r1::r2::nil => Errors.Error (Errors.msg "Htlgen: Instruction not implemented: mulhs") + | Op.Omulhu, r1::r2::nil => Errors.Error (Errors.msg "Htlgen: Instruction not implemented: mulhu") + | Op.Odiv, r1::r2::nil => Errors.OK (bop Vdiv r1 r2) + | Op.Odivu, r1::r2::nil => Errors.OK (bop Vdivu r1 r2) + | Op.Omod, r1::r2::nil => Errors.OK (bop Vmod r1 r2) + | Op.Omodu, r1::r2::nil => Errors.OK (bop Vmodu r1 r2) + | Op.Oand, r1::r2::nil => Errors.OK (bop Vand r1 r2) + | Op.Oandimm n, r::nil => Errors.OK (boplit Vand r n) + | Op.Oor, r1::r2::nil => Errors.OK (bop Vor r1 r2) + | Op.Oorimm n, r::nil => Errors.OK (boplit Vor r n) + | Op.Oxor, r1::r2::nil => Errors.OK (bop Vxor r1 r2) + | Op.Oxorimm n, r::nil => Errors.OK (boplit Vxor r n) + | Op.Onot, r::nil => Errors.OK (Vunop Vnot (Vvar r)) + | Op.Oshl, r1::r2::nil => Errors.OK (bop Vshl r1 r2) + | Op.Oshlimm n, r::nil => Errors.OK (boplit Vshl r n) + | Op.Oshr, r1::r2::nil => Errors.OK (bop Vshr r1 r2) + | Op.Oshrimm n, r::nil => Errors.OK (boplit Vshr r n) | Op.Oshrximm n, r::nil => - ret (Vternary (Vbinop Vlt (Vvar r) (Vlit (ZToValue 0))) + Errors.OK (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))) + | Op.Oshru, r1::r2::nil => Errors.OK (bop Vshru r1 r2) + | Op.Oshruimm n, r::nil => Errors.OK (boplit Vshru r n) + | Op.Ororimm n, r::nil => Errors.Error (Errors.msg "Htlgen: Instruction not implemented: Ororimm") + (*Errors.OK (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.Oshldimm n, r::nil => Errors.OK (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)) + Errors.OK (Vternary tc (Vvar r1) (Vvar r2)) | Op.Olea a, _ => translate_eff_addressing a args - | _, _ => error (Errors.msg "Htlgen: Instruction not implemented: other") + | _, _ => Errors.Error (Errors.msg "Htlgen: Instruction not implemented: other") end. -Lemma add_branch_instr_state_incr: - forall s preg p 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 preg p 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 preg p (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 preg p s.(st_st) e n1 n2) (st_controllogic s))) - (add_branch_instr_state_incr s preg p 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) : Errors.res 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 Errors.OK (Vvari stack (Vbinop Vdivu (boplitz Vadd r1 off) (Vlit (ZToValue 4)))) + else Errors.Error (Errors.msg "HTLPargen: 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 Errors.OK (Vvari stack + (Vbinop Vdivu + (Vbinop Vadd (boplitz Vadd r1 offset) (boplitz Vmul r2 scale)) + (Vlit (ZToValue 4)))) + else Errors.Error (Errors.msg "HTLPargen: 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 Errors.OK (Vvari stack (Vlit (ZToValue (a / 4)))) + else Errors.Error (Errors.msg "HTLPargen: eff_addressing out of bounds stack offset") + | _, _, _ => Errors.Error (Errors.msg "HTLPargen: translate_arr_access unsuported addressing") + end. Fixpoint enumerate (i : nat) (ns : list node) {struct ns} : list (nat * node) := match ns with @@ -516,12 +365,156 @@ Fixpoint enumerate (i : nat) (ns : list node) {struct ns} : list (nat * node) := 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), Vblock (Vvar st) (Vlit (posToValue n))) + (i, n) => (Vlit (natToValue i), Vnonblock (Vvar st) (Vlit (posToValue n))) end) (enumerate 0 ns). -Definition stack_correct (sz : Z) : bool := - (0 <=? sz) && (sz <? Integers.Ptrofs.modulus) && (Z.modulo sz 4 =? 0). +Definition translate_cfi (fin rtrn state preg: reg) p (cfi: cf_instr) + : Errors.res stmnt := + match cfi with + | RBgoto n' => + Errors.OK (state_goto preg p state n') + | RBcond c args n1 n2 => + do e <- translate_condition c args; + Errors.OK (state_cond preg p state e n1 n2) + | RBreturn r => + match r with + | Some r' => + Errors.OK (Vseq (block fin (Vlit (ZToValue 1%Z))) (block rtrn (Vvar r'))) + | None => + Errors.OK (Vseq (block fin (Vlit (ZToValue 1%Z))) (block rtrn (Vlit (ZToValue 0%Z)))) + end + | RBjumptable r tbl => + Errors.OK (Vcase (Vvar r) (list_to_stmnt (tbl_to_case_expr state tbl)) (Some Vskip)) + | RBcall sig ri rl r n => + Errors.Error (Errors.msg "HTLPargen: RBcall not supported.") + | RBtailcall sig ri lr => + Errors.Error (Errors.msg "HTLPargen: RBtailcall not supported.") + | RBbuiltin e lb b n => + Errors.Error (Errors.msg "HTLPargen: RBbuildin not supported.") + end. + +Definition dfltp {A} (p: option (@Predicate.pred_op A)) := Option.default Ptrue p. + +Definition transf_instr (fin rtrn stack state preg: reg) + (dc: pred_op * stmnt) (i: instr) + : Errors.res (pred_op * stmnt) := + let '(curr_p, d) := dc in + let npred p := Some (Pand curr_p (dfltp p)) in + match i with + | RBnop => Errors.OK dc + | RBop p op args dst => + do instr <- translate_instr op args; + let stmnt := translate_predicate Vblock preg (npred p) (Vvar dst) instr in + Errors.OK (curr_p, Vseq d stmnt) + | RBload p mem addr args dst => + do src <- translate_arr_access mem addr args stack; + let stmnt := translate_predicate Vblock preg (npred p) (Vvar dst) src in + Errors.OK (curr_p, Vseq d stmnt) + | RBstore p mem addr args src => + do dst <- translate_arr_access mem addr args stack; + let stmnt := translate_predicate Vblock preg (npred p) dst (Vvar src) in + Errors.OK (curr_p, Vseq d stmnt) + | RBsetpred p' cond args p => + do cond' <- translate_condition cond args; + let stmnt := translate_predicate Vblock preg (npred p') (pred_expr preg (Plit (true, p))) cond' in + Errors.OK (curr_p, Vseq d stmnt) + | RBexit p cf => + do d_stmnt <- translate_cfi fin rtrn state preg (npred p) cf; + Errors.OK (Pand curr_p (negate (dfltp p)), Vseq d d_stmnt) + end. + +Definition fold_leftE {A B} (f: A -> B -> Errors.res A) (l: list B) (el: A): Errors.res A := + fold_left (fun a b => do a' <- a; f a' b) l (Errors.OK el). + +Definition transf_chained_block (fin rtrn stack state preg: reg) + (dc: @pred_op positive * stmnt) + (block: list instr) + : Errors.res (pred_op * stmnt) := + fold_leftE (transf_instr fin rtrn stack state preg) block dc. + +Definition transf_parallel_block (fin rtrn stack state preg: reg) + (dc: @pred_op positive * stmnt) + (block: list (list instr)) + : Errors.res (pred_op * stmnt) := + fold_leftE (transf_chained_block fin rtrn stack state preg) block dc. + +Definition transf_parallel_full_block (fin rtrn stack state preg: reg) + (dc: node * @pred_op positive * datapath) + (block: list (list instr)) + : Errors.res (node * pred_op * datapath) := + let '(n, curr_p, dt) := dc in + match AssocMap.get n dt with + | None => + do ctrl_init_stmnt <- + translate_cfi fin rtrn state preg (Some curr_p) (RBgoto (n - 1)%positive); + do dc' <- transf_parallel_block fin rtrn stack state preg (curr_p, ctrl_init_stmnt) block; + let '(curr_p', dt_stmnt) := dc' in + Errors.OK ((n - 1)%positive, curr_p', AssocMap.set n dt_stmnt dt) + | _ => Errors.Error (msg "HtlPargen.transf_parallel_full_block: block not empty") + end. + +Definition transf_seq_block (fin rtrn stack state preg: reg) + (d: datapath) (n: node) + (block: list (list (list instr))) + : Errors.res datapath := + do res <- fold_leftE + (transf_parallel_full_block fin rtrn stack state preg) block (n, Ptrue, d); + let '(_, _, d') := res in + Errors.OK d'. + +#[local] Close Scope error_monad_scope. +#[local] Open Scope monad_scope. + +Program Definition transf_seq_blockM (fin rtrn stack preg: reg) (ni: node * ParBB.t): mon unit := + fun st => + let (n, i) := ni in + match transf_seq_block fin rtrn stack st.(st_st) preg st.(st_datapath) n i with + | Errors.OK d => + OK tt (mkstate st.(st_st) + st.(st_freshreg) + st.(st_freshstate) + st.(st_scldecls) + st.(st_arrdecls) + d) _ + | Errors.Error m => Error m + end. +Next Obligation. +admit. +Admitted. + +Definition declare_regs (i: instr): mon unit := + match i with + | RBop _ _ _ d => declare_reg None d 32 + | RBload _ _ _ _ d => declare_reg None d 32 + | _ => ret tt + end. + +Definition declare_all_regs (ni: node * ParBB.t): mon unit := + let (n, i) := ni in + ParBB.foldl _ (fun (st_f: mon unit) i => do _tt <- st_f; declare_regs i) i (ret tt). + +Lemma create_reg_state_incr: + forall s sz i, + st_incr s (mkstate + s.(st_st) + (Pos.succ (st_freshreg s)) + (st_freshstate s) + (AssocMap.set s.(st_freshreg) (i, VScalar sz) s.(st_scldecls)) + s.(st_arrdecls) + (st_datapath s)). +Proof. constructor; simpl; auto with htlh. Qed. + +Definition create_reg (i : option io) (sz : nat) : mon reg := + fun s => 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)) + (create_reg_state_incr s sz i). Lemma create_arr_state_incr: forall s sz ln i, @@ -531,8 +524,7 @@ Lemma create_arr_state_incr: (st_freshstate s) s.(st_scldecls) (AssocMap.set s.(st_freshreg) (i, VArray sz ln) s.(st_arrdecls)) - (st_datapath s) - (st_controllogic s)). + (st_datapath s)). Proof. constructor; simpl; auto with htlh. Qed. Definition create_arr (i : option io) (sz : nat) (ln : nat) : mon (reg * nat) := @@ -543,17 +535,19 @@ Definition create_arr (i : option io) (sz : nat) (ln : nat) : mon (reg * nat) := (st_freshstate s) s.(st_scldecls) (AssocMap.set s.(st_freshreg) (i, VArray sz ln) s.(st_arrdecls)) - (st_datapath s) - (st_controllogic s)) + (st_datapath s)) (create_arr_state_incr s sz ln i). +Definition stack_correct (sz : Z) : bool := + (0 <=? sz) && (sz <? Integers.Ptrofs.modulus) && (Z.modulo sz 4 =? 0). + 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. + intros until i. unfold max_pc_function. apply PTree_Properties.fold_rec with (P := fun c m => c!pc = Some i -> Ple pc m). (* extensionality *) intros. apply H0. rewrite H; auto. @@ -561,9 +555,8 @@ Proof. 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. + inv H2. unfold Ple; lia. + apply Ple_trans with a. auto. unfold Ple; lia. Qed. Lemma max_pc_wf : @@ -577,282 +570,7 @@ Proof. 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 update_control_instr (n : node) (st : stmnt) : mon unit := - fun s => - match s.(st_controllogic) ! n with - | Some st' => - OK tt (mkstate - s.(st_st) - s.(st_freshreg) - (st_freshstate s) - s.(st_scldecls) - s.(st_arrdecls) - s.(st_datapath) - (AssocMap.set n (Vseq st' st) s.(st_controllogic))) - (add_control_instr_force_state_incr s n (Vseq st' st)) - | None => - 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) - end. - -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). - -Definition add_control_instr_try (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) - | _ => - OK tt s (st_refl s) - 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. - -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_cfi' (fin rtrn preg: reg) p (cfi: cf_instr) - : mon (stmnt * stmnt) := - match cfi with - | RBgoto n' => - do st <- get; - ret (Vskip, state_goto preg p st.(st_st) n') - | RBcond c args n1 n2 => - do st <- get; - do e <- translate_condition c args; - ret (Vskip, state_cond preg p st.(st_st) e n1 n2) - | RBreturn 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 - | RBjumptable r tbl => - do s <- get; - ret (Vskip, Vcase (Vvar r) (list_to_stmnt (tbl_to_case_expr s.(st_st) tbl)) (Some Vskip)) - | RBcall sig ri rl r n => - error (Errors.msg "HTLPargen: RPcall not supported.") - | RBtailcall sig ri lr => - error (Errors.msg "HTLPargen: RPtailcall not supported.") - | RBbuiltin e lb b n => - error (Errors.msg "HTLPargen: RPbuildin not supported.") - end. - -Definition translate_cfi (fin rtrn preg: reg) p (ni: node * cf_instr) : mon unit := - let (n, cfi) := ni in - do (s, c) <- translate_cfi' fin rtrn preg p cfi; - do _ <- update_control_instr n c; - add_data_instr n s. - -Definition translate_inst a (fin rtrn preg stack : reg) (n : node) (i : instr) := - match i with - | RBnop => - do stmnt <- ret Vskip; - add_data_instr n stmnt - | RBop p op args dst => - do instr <- translate_instr op args; - do _ <- declare_reg None dst 32; - add_data_instr n (translate_predicate a preg p (Vvar dst) instr) - | RBload p mem addr args dst => - do src <- translate_arr_access mem addr args stack; - do _ <- declare_reg None dst 32; - add_data_instr n (translate_predicate a preg p (Vvar dst) src) - | RBstore p mem addr args src => - do dst <- translate_arr_access mem addr args stack; - add_data_instr n (translate_predicate a preg p dst (Vvar src)) - | RBsetpred _ c args p => - do cond <- translate_condition c args; - do stmnt <- ret (a (pred_expr preg (Plit (true, p))) cond); - add_data_instr n stmnt - | RBexit p cf => - translate_cfi fin rtrn preg p (n, cf) - end. - -Definition translate_inst_list (fin rtrn preg stack: reg) (ni : node * node * list (list instr)) := - match ni with - | (n, p, li) => - do st <- get; - do _ <- add_control_instr n (state_goto preg None st.(st_st) p); - collectlist (fun l => translate_inst Vblock fin rtrn preg stack n l) (concat li) - end. - -Definition transf_bblock (fin rtrn preg stack: reg) (ni : node * ParBB.t) - : mon unit := - let (n, bb) := ni in - do nstate <- create_new_state ((poslength bb))%positive; - do _ <- add_control_instr nstate Vskip; - collectlist (translate_inst_list fin rtrn preg stack) - (prange n (nstate + poslength bb - 1)%positive - bb). - -(*Definition decide_order a b c d e f g : {module_ordering a b c d e f g} + {True}. +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 <? b) && (b <? c) && (c <? d) && (d <? e) && (e <? f) && (f <? g))%positive true with | left t => left _ @@ -861,67 +579,50 @@ Definition transf_bblock (fin rtrn preg stack: reg) (ni : node * ParBB.t) simplify; repeat match goal with | H: context[(_ <? _)%positive] |- _ => apply Pos.ltb_lt in H end; unfold module_ordering; auto. -Defined.*) - -Lemma clk_greater : - forall ram clk r', - Some ram = Some r' -> (clk < ram_addr r')%positive. -Proof. Admitted. +Defined. -Definition declare_ram (r: ram) : mon unit := - do _ <- declare_reg None r.(ram_en) 1; - do _ <- declare_reg None r.(ram_u_en) 1; - do _ <- declare_reg None r.(ram_wr_en) 1; - do _ <- declare_reg None r.(ram_addr) 32; - do _ <- declare_reg None r.(ram_d_in) 32; - do _ <- declare_reg None r.(ram_d_out) 32; - do _ <- declare_arr None r.(ram_mem) 32 r.(ram_size); - ret tt. - -Definition transf_module (f: function) : mon HTL.module := +Definition transf_module (f: function) : mon DHTL.module. + refine ( if stack_correct f.(fn_stacksize) then do fin <- create_reg (Some Voutput) 1; do rtrn <- create_reg (Some Voutput) 32; - do preg <- create_reg None 128; + do preg <- create_reg None 32; do (stack, stack_len) <- create_arr None 32 (Z.to_nat (f.(fn_stacksize) / 4)); - do _ <- collectlist (transf_bblock fin rtrn preg stack) - (Maps.PTree.elements f.(fn_code)); - do _ <- collectlist (fun r => declare_reg (Some Vinput) r 32) - f.(fn_params); + do _stmnt <- collectlist (transf_seq_blockM fin rtrn stack preg) (Maps.PTree.elements f.(GiblePar.fn_code)); + do _stmnt' <- collectlist (fun r => declare_reg (Some Vinput) r 32) f.(GiblePar.fn_params); + do _stmnt'' <- collectlist declare_all_regs (Maps.PTree.elements f.(GiblePar.fn_code)); do start <- create_reg (Some Vinput) 1; do rst <- create_reg (Some Vinput) 1; do clk <- create_reg (Some Vinput) 1; - do r_en <- create_reg None 1; - do r_u_en <- create_reg None 1; - do r_addr <- create_reg None 32; - do r_wr_en <- create_reg None 1; - do r_d_in <- create_reg None 32; - do r_d_out <- create_reg None 32; 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, - max_list_dec (fn_params f) (st_st current_state) + match zle (Z.pos (max_pc_map current_state.(st_datapath))) Integers.Int.max_unsigned, + decide_order (st_st current_state) fin rtrn stack start rst clk, + max_list_dec (GiblePar.fn_params f) (st_st current_state) with - | left LEDATA, left LECTRL, left WFPARAMS => - ret (HTL.mkmodule - f.(fn_params) - current_state.(st_datapath) - current_state.(st_controllogic) - f.(fn_entrypoint) - current_state.(st_st) - fin - rtrn - start - rst - clk - current_state.(st_scldecls) - current_state.(st_arrdecls) - (mk_ram stack_len stack r_en r_u_en r_addr r_wr_en r_d_in r_d_out)) - | _, _, _=> error (Errors.msg "More than 2^32 states.") + | left LEDATA, left MORD, left WFPARAMS => + ret (DHTL.mkmodule + f.(GiblePar.fn_params) + current_state.(st_datapath) + f.(fn_entrypoint) + current_state.(st_st) + stack + stack_len + fin + rtrn + start + rst + clk + current_state.(st_scldecls) + current_state.(st_arrdecls) + None + (max_pc_wf _ LEDATA) + MORD + _ + WFPARAMS) + | _, _, _ => error (Errors.msg "More than 2^32 states.") end - else error (Errors.msg "Stack size misalignment."). + else error (Errors.msg "Stack size misalignment.")); discriminate. +Defined. Definition max_state (f: function) : state := let st := Pos.succ (max_reg_function f) in @@ -930,10 +631,9 @@ Definition max_state (f: function) : state := (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)). + (st_datapath (init_state st)). -Definition transl_module (f : function) : Errors.res HTL.module := +Definition transl_module (f : function) : Errors.res DHTL.module := run_mon (max_state f) (transf_module f). Definition transl_fundef := transf_partial_fundef transl_module. @@ -949,7 +649,7 @@ Definition main_is_internal (p : GiblePar.program) : bool := | _ => false end. -Definition transl_program (p : GiblePar.program) : Errors.res HTL.program := +Definition transl_program (p : GiblePar.program) : Errors.res DHTL.program := if main_is_internal p then transform_partial_program transl_fundef p else Errors.Error (Errors.msg "Main function is not Internal."). |