vericert.hls.HTLPargen
#[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.
Lemma st_trans :
forall s1 s2 s3, st_prop s1 s2 -> st_prop s2 s3 -> st_prop s1 s3.
End HTLState.
Module HTLMonad := Statemonad(HTLState).
Module HTLMonadExtra := Monad.MonadExtra(HTLMonad).
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 }.
Definition check_empty_node_controllogic:
forall (s: state) (n: node), { s.(st_controllogic)!n = None } + { True }.
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)).
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 declare_arr_state_incr :
forall i s r sz ln,
st_incr s
(mkstate
s.(st_st)
s.(st_freshreg)
s.(st_freshstate)
s.(st_scldecls)
(AssocMap.set r (i, VArray sz ln) s.(st_arrdecls))
s.(st_datapath)
s.(st_controllogic)).
Definition declare_arr (i : option io) (r : reg) (sz : nat) (ln : nat) : mon unit :=
fun s => OK tt (mkstate
s.(st_st)
s.(st_freshreg)
s.(st_freshstate)
s.(st_scldecls)
(AssocMap.set r (i, VArray sz ln) s.(st_arrdecls))
s.(st_datapath)
s.(st_controllogic))
(declare_arr_state_incr i s r sz ln).
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))).
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))).
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))).
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.
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)).
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 :=
match a, args with
| 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 =>
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 =>
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")
| 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))).
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.
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 <? Integers.Ptrofs.modulus) && (Z.modulo sz 4 =? 0).
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)).
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).
Lemma max_pc_wf :
forall m, Z.pos (max_pc_map m) <= Integers.Int.max_unsigned ->
map_well_formed m.
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)).
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))).
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 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
| FUread p1 p2 r => ret Vskip
| FUwrite p1 p2 r => ret Vskip
| 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)).
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 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 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 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 preg c1;
do (tc2s, tc2c) <- translate_cfi' fin rtrn 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 preg: reg) (ni: node * cf_instr)
: mon unit :=
let (n, cfi) := ni in
do (s, c) <- translate_cfi' fin rtrn preg cfi;
do _ <- add_control_instr n c;
add_data_instr n s.
Definition transf_bblock (fin rtrn 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 preg)
(prange n (nstate + poslength bb.(bb_body) - 1)%positive
bb.(bb_body));
match bb.(bb_body) with
| nil => translate_cfi fin rtrn preg (n, bb.(bb_exit))
| _ => translate_cfi fin rtrn preg (nstate, bb.(bb_exit))
end.
Lemma clk_greater :
forall ram clk r',
Some ram = Some r' -> (clk < ram_addr r')%positive.
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 :=
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 32;
do _ <- collectlist (transf_bblock fin rtrn 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;
match get_ram 0 (fn_funct_units f) with
| Some (_, r) =>
do _ <- declare_ram r;
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)
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)
r)
| _, _, _=> error (Errors.msg "More than 2^32 states.")
end
| _ => error (Errors.msg "Stack RAM not found.")
end
else error (Errors.msg "Stack size misalignment.").
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.").
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")
| 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))).
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.
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 <? Integers.Ptrofs.modulus) && (Z.modulo sz 4 =? 0).
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)).
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).
Lemma max_pc_wf :
forall m, Z.pos (max_pc_map m) <= Integers.Int.max_unsigned ->
map_well_formed m.
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)).
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))).
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 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
| FUread p1 p2 r => ret Vskip
| FUwrite p1 p2 r => ret Vskip
| 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)).
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 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 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 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 preg c1;
do (tc2s, tc2c) <- translate_cfi' fin rtrn 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 preg: reg) (ni: node * cf_instr)
: mon unit :=
let (n, cfi) := ni in
do (s, c) <- translate_cfi' fin rtrn preg cfi;
do _ <- add_control_instr n c;
add_data_instr n s.
Definition transf_bblock (fin rtrn 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 preg)
(prange n (nstate + poslength bb.(bb_body) - 1)%positive
bb.(bb_body));
match bb.(bb_body) with
| nil => translate_cfi fin rtrn preg (n, bb.(bb_exit))
| _ => translate_cfi fin rtrn preg (nstate, bb.(bb_exit))
end.
Lemma clk_greater :
forall ram clk r',
Some ram = Some r' -> (clk < ram_addr r')%positive.
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 :=
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 32;
do _ <- collectlist (transf_bblock fin rtrn 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;
match get_ram 0 (fn_funct_units f) with
| Some (_, r) =>
do _ <- declare_ram r;
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)
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)
r)
| _, _, _=> error (Errors.msg "More than 2^32 states.")
end
| _ => error (Errors.msg "Stack RAM not found.")
end
else error (Errors.msg "Stack size misalignment.").
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.").