aboutsummaryrefslogtreecommitdiffstats
path: root/src/translation/HTLgen.v
diff options
context:
space:
mode:
Diffstat (limited to 'src/translation/HTLgen.v')
-rw-r--r--src/translation/HTLgen.v81
1 files changed, 47 insertions, 34 deletions
diff --git a/src/translation/HTLgen.v b/src/translation/HTLgen.v
index f109a8e..44b2937 100644
--- a/src/translation/HTLgen.v
+++ b/src/translation/HTLgen.v
@@ -17,7 +17,7 @@
*)
From compcert Require Import Maps.
-From compcert Require Errors Globalenvs.
+From compcert Require Errors Globalenvs Integers.
From compcert Require Import AST RTL.
From coqup Require Import Verilog HTL Coquplib AssocMap Value Statemonad.
@@ -131,7 +131,7 @@ Lemma declare_reg_state_incr :
s.(st_st)
s.(st_freshreg)
s.(st_freshstate)
- (AssocMap.set r (i, Scalar sz) s.(st_scldecls))
+ (AssocMap.set r (i, VScalar sz) s.(st_scldecls))
s.(st_arrdecls)
s.(st_datapath)
s.(st_controllogic)).
@@ -142,7 +142,7 @@ Definition declare_reg (i : option io) (r : reg) (sz : nat) : mon unit :=
s.(st_st)
s.(st_freshreg)
s.(st_freshstate)
- (AssocMap.set r (i, Scalar sz) s.(st_scldecls))
+ (AssocMap.set r (i, VScalar sz) s.(st_scldecls))
s.(st_arrdecls)
s.(st_datapath)
s.(st_controllogic))
@@ -280,19 +280,28 @@ Definition translate_condition (c : Op.condition) (args : list reg) : mon expr :
| _, _ => error (Errors.msg "Htlgen: condition instruction not implemented: other")
end.
+Definition check_address_parameter (p : Z) : bool :=
+ Z.eqb (Z.modulo p 4) 0
+ && Z.leb Integers.Ptrofs.min_signed p
+ && Z.leb p Integers.Ptrofs.min_signed.
+
Definition translate_eff_addressing (a: Op.addressing) (args: list reg) : mon expr :=
- match a, args with
+ match a, args with (* TODO: We should be more methodical here; what are the possibilities?*)
| Op.Aindexed off, r1::nil => ret (boplitz Vadd r1 off)
- | Op.Aindexed2 off, r1::r2::nil => ret (Vbinop Vadd (Vvar r1) (boplitz Vadd r2 off))
| Op.Ascaled scale offset, r1::nil =>
- ret (Vbinop Vadd (boplitz Vmul r1 scale) (Vlit (ZToValue 32 offset)))
- | Op.Aindexed2scaled scale offset, r1::r2::nil =>
- ret (Vbinop Vadd (boplitz Vadd r1 offset) (boplitz Vmul r2 scale))
- (* Stack arrays/referenced variables *)
+ if (check_address_parameter scale) && (check_address_parameter offset)
+ then ret (Vbinop Vadd (boplitz Vmul r1 scale) (Vlit (ZToValue 32 offset)))
+ else error (Errors.msg "Veriloggen: translate_eff_addressing address misaligned")
+ | Op.Aindexed2scaled scale offset, r1::r2::nil => (* Typical for dynamic array addressing *)
+ if (check_address_parameter scale) && (check_address_parameter offset)
+ then ret (Vbinop Vadd (boplitz Vadd r1 offset) (boplitz Vmul r2 scale))
+ else error (Errors.msg "Veriloggen: translate_eff_addressing address misaligned")
| Op.Ainstack a, nil => (* We need to be sure that the base address is aligned *)
- let a := Integers.Ptrofs.unsigned a in (* FIXME: Assuming stack offsets are +ve; is this ok? *)
- ret (Vlit (ZToValue 32 a))
- | _, _ => error (Errors.msg "Htlgen: eff_addressing instruction not implemented: other")
+ let a := Integers.Ptrofs.unsigned a in
+ if (check_address_parameter a)
+ then ret (Vlit (ZToValue 32 a))
+ else error (Errors.msg "Veriloggen: translate_eff_addressing address misaligned")
+ | _, _ => error (Errors.msg "Veriloggen: translate_eff_addressing unsuported addressing")
end.
(** Translate an instruction to a statement. FIX mulhs mulhu *)
@@ -374,24 +383,25 @@ Definition add_branch_instr (e: expr) (n n1 n2: node) : mon unit :=
Definition translate_arr_access (mem : AST.memory_chunk) (addr : Op.addressing)
(args : list reg) (stack : reg) : mon expr :=
- match addr, args with (* TODO: We should be more methodical here; what are the possibilities?*)
- | Op.Aindexed off, r1::nil => (* FIXME: Cannot guarantee alignment *)
+ match mem, addr, args with (* TODO: We should be more methodical here; what are the possibilities?*)
+ | Mint32, Op.Aindexed off, r1::nil =>
ret (Vvari stack (Vbinop Vadd (boplitz Vdiv r1 4) (Vlit (ZToValue 32 (off / 4)))))
- | Op.Ascaled scale offset, r1::nil =>
- if ((Z.eqb (Z.modulo scale 4) 0) && (Z.eqb (Z.modulo offset 4) 0))
+ | Mint32, Op.Ascaled scale offset, r1::nil =>
+ if (check_address_parameter scale) && (check_address_parameter offset)
then ret (Vvari stack (Vbinop Vadd (boplitz Vmul r1 (scale / 4)) (Vlit (ZToValue 32 (offset / 4)))))
else error (Errors.msg "Htlgen: translate_arr_access address misaligned")
- | Op.Aindexed2scaled scale offset, r1::r2::nil => (* Typical for dynamic array addressing *)
- if ((Z.eqb (Z.modulo scale 4) 0) && (Z.eqb (Z.modulo offset 4) 0))
+ | Mint32, Op.Aindexed2scaled scale offset, r1::r2::nil => (* Typical for dynamic array addressing *)
+ if (check_address_parameter scale) && (check_address_parameter offset)
then ret (Vvari stack
(Vbinop Vadd (Vbinop Vadd (boplitz Vdiv r1 4) (Vlit (ZToValue 32 (offset / 4))))
(boplitz Vmul r2 (scale / 4))))
else error (Errors.msg "Htlgen: translate_arr_access address misaligned")
- | Op.Ainstack a, nil => (* We need to be sure that the base address is aligned *)
- let a := Integers.Ptrofs.unsigned a in (* FIXME: Assuming stack offsets are +ve; is this ok? *)
- if (Z.eq_dec (Z.modulo a 4) 0) then ret (Vvari stack (Vlit (ZToValue 32 (a / 4))))
- else error (Errors.msg "Htlgen: eff_addressing misaligned stack offset")
- | _, _ => error (Errors.msg "Htlgen: translate_arr_access unsupported addressing")
+ | 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 a)
+ then ret (Vvari stack (Vlit (ZToValue 32 (a / 4))))
+ else error (Errors.msg "Veriloggen: eff_addressing misaligned stack offset")
+ | _, _, _ => error (Errors.msg "Veriloggen: translate_arr_access unsuported addressing")
end.
Fixpoint enumerate (i : nat) (ns : list node) {struct ns} : list (nat * node) :=
@@ -418,10 +428,10 @@ Definition transf_instr (fin rtrn stack: reg) (ni: node * instruction) : mon uni
| Iload mem addr args dst n' =>
do src <- translate_arr_access mem addr args stack;
do _ <- declare_reg None dst 32;
- add_instr n n' (block dst src)
+ add_instr n n' (nonblock dst src)
| Istore mem addr args src n' =>
do dst <- translate_arr_access mem addr args stack;
- add_instr n n' (Vblock dst (Vvar src)) (* TODO: Could juse use add_instr? reg exists. *)
+ add_instr n n' (Vnonblock dst (Vvar src)) (* TODO: Could juse use add_instr? reg exists. *)
| Icall _ _ _ _ _ => error (Errors.msg "Calls are not implemented.")
| Itailcall _ _ _ => error (Errors.msg "Tailcalls are not implemented.")
| Ibuiltin _ _ _ _ => error (Errors.msg "Builtin functions not implemented.")
@@ -447,7 +457,7 @@ Lemma create_reg_state_incr:
s.(st_st)
(Pos.succ (st_freshreg s))
(st_freshstate s)
- (AssocMap.set s.(st_freshreg) (i, Scalar sz) s.(st_scldecls))
+ (AssocMap.set s.(st_freshreg) (i, VScalar sz) s.(st_scldecls))
s.(st_arrdecls)
(st_datapath s)
(st_controllogic s)).
@@ -459,7 +469,7 @@ Definition create_reg (i : option io) (sz : nat) : mon reg :=
s.(st_st)
(Pos.succ r)
(st_freshstate s)
- (AssocMap.set s.(st_freshreg) (i, Scalar sz) s.(st_scldecls))
+ (AssocMap.set s.(st_freshreg) (i, VScalar sz) s.(st_scldecls))
(st_arrdecls s)
(st_datapath s)
(st_controllogic s))
@@ -472,27 +482,28 @@ Lemma create_arr_state_incr:
(Pos.succ (st_freshreg s))
(st_freshstate s)
s.(st_scldecls)
- (AssocMap.set s.(st_freshreg) (i, Array sz ln) s.(st_arrdecls))
+ (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 :=
+Definition create_arr (i : option io) (sz : nat) (ln : nat) : mon (reg * nat) :=
fun s => let r := s.(st_freshreg) in
- OK r (mkstate
+ OK (r, ln) (mkstate
s.(st_st)
(Pos.succ r)
(st_freshstate s)
s.(st_scldecls)
- (AssocMap.set s.(st_freshreg) (i, Array sz ln) s.(st_arrdecls))
+ (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 transf_module (f: function) : mon module :=
+ if (Z.eq_dec (Z.modulo f.(fn_stacksize) 4) 0) then
do fin <- create_reg (Some Voutput) 1;
do rtrn <- create_reg (Some Voutput) 32;
- do stack <- create_arr None 32 (Z.to_nat (f.(fn_stacksize) / 4));
+ do (stack, stack_len) <- create_arr None 32 (Z.to_nat (f.(fn_stacksize) / 4));
do _ <- collectlist (transf_instr fin rtrn stack) (Maps.PTree.elements f.(RTL.fn_code));
do _ <- collectlist (fun r => declare_reg (Some Vinput) r 32) f.(RTL.fn_params);
do start <- create_reg (Some Vinput) 1;
@@ -506,20 +517,22 @@ Definition transf_module (f: function) : mon module :=
f.(fn_entrypoint)
current_state.(st_st)
stack
+ stack_len
fin
rtrn
start
rst
clk
current_state.(st_scldecls)
- current_state.(st_arrdecls)).
+ current_state.(st_arrdecls))
+ 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, Scalar 32) (st_scldecls (init_state st)))
+ (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)).
generated by cgit (git 2.34.1) at 2024-07-07 23:50:41 +0000