HTLgenspec status in line with develop

3 files changed, 57 insertions, 26 deletions

diff --git a/src/translation/HTLgen.v b/src/translation/HTLgen.v
index 04cb7b8..b573b06 100644
--- a/src/translation/HTLgen.v
+++ b/src/translation/HTLgen.v
@@ -274,7 +274,7 @@ Definition translate_instr (op : Op.operation) (args : list reg) : mon expr :=
   | Op.Ocmp c, _ => translate_condition c args
   | Op.Olea a, _ => translate_eff_addressing a args
   | Op.Oleal a, _ => translate_eff_addressing a args (* FIXME: Need to be careful here; large arrays might fail? *)
-  | Op.Ocast32signed, r::nill => ret (Vvar r) (* FIXME: Don't need to sign extend for now since everything is 32 bit? *)
+  | Op.Ocast32signed, r::nil => ret (Vvar r) (* FIXME: Don't need to sign extend for now since everything is 32 bit? *)
   | _, _ => error (Errors.msg "Veriloggen: Instruction not implemented: other")
   end.
 
@@ -425,6 +425,7 @@ Definition transf_module (f: function) : mon module :=
          current_state.(st_controllogic)
          f.(fn_entrypoint)
          current_state.(st_st)
+         stack
          fin
          rtrn).
 
diff --git a/src/translation/HTLgenspec.v b/src/translation/HTLgenspec.v
index ae2a58e..3b68a7f 100644
--- a/src/translation/HTLgenspec.v
+++ b/src/translation/HTLgenspec.v
@@ -136,68 +136,93 @@ Inductive tr_op : Op.operation -> list reg -> expr -> Prop :=
 | tr_op_Oshr : forall r1 r2, tr_op Op.Oshr (r1::r2::nil) (bop Vshr r1 r2)
 | tr_op_Oshrimm : forall n r, tr_op (Op.Oshrimm n) (r::nil) (boplit Vshr r n)
 | tr_op_Ocmp : forall c l e s s' i, translate_condition c l s = OK e s' i -> tr_op (Op.Ocmp c) l e
-| tr_op_Olea : forall a l e s s' i, translate_eff_addressing a l s = OK e s' i -> tr_op (Op.Olea a) l e.
+| tr_op_Olea : forall a l e s s' i, translate_eff_addressing a l s = OK e s' i -> tr_op (Op.Olea a) l e
+| tr_op_Oleal : forall a l e s s' i, translate_eff_addressing a l s = OK e s' i -> tr_op (Op.Oleal a) l e
+| tr_op_Ocast32signed : forall r, tr_op (Op.Ocast32signed) (r::nil) (Vvar r).
 Hint Constructors tr_op : htlspec.
 
-Inductive tr_instr (fin rtrn st : reg) : RTL.instruction -> stmnt -> stmnt -> Prop :=
+Inductive tr_instr (fin rtrn st stk : reg) : RTL.instruction -> stmnt -> stmnt -> Prop :=
 | tr_instr_Inop :
     forall n,
-      tr_instr fin rtrn st (RTL.Inop n) Vskip (state_goto st n)
+      tr_instr fin rtrn st stk (RTL.Inop n) Vskip (state_goto st n)
 | tr_instr_Iop :
     forall n op args e dst,
       tr_op op args e ->
-      tr_instr fin rtrn st (RTL.Iop op args dst n) (Vnonblock (Vvar dst) e) (state_goto st n)
+      tr_instr fin rtrn st stk (RTL.Iop op args dst n) (Vnonblock (Vvar dst) e) (state_goto st n)
 | tr_instr_Icond :
     forall n1 n2 cond args s s' i c,
       translate_condition cond args s = OK c s' i ->
-      tr_instr fin rtrn st (RTL.Icond cond args n1 n2) Vskip (state_cond st c n1 n2)
+      tr_instr fin rtrn st stk (RTL.Icond cond args n1 n2) Vskip (state_cond st c n1 n2)
 | tr_instr_Ireturn_None :
-    tr_instr fin rtrn st (RTL.Ireturn None) (Vseq (block fin (Vlit (ZToValue 1%nat 1%Z)))
+    tr_instr fin rtrn st stk (RTL.Ireturn None) (Vseq (block fin (Vlit (ZToValue 1%nat 1%Z)))
                                                   (block rtrn (Vlit (ZToValue 1%nat 0%Z)))) Vskip
 | tr_instr_Ireturn_Some :
     forall r,
-      tr_instr fin rtrn st (RTL.Ireturn (Some r))
-               (Vseq (block fin (Vlit (ZToValue 1%nat 1%Z))) (block rtrn (Vvar r))) Vskip.
+      tr_instr fin rtrn st stk (RTL.Ireturn (Some r))
+               (Vseq (block fin (Vlit (ZToValue 1%nat 1%Z))) (block rtrn (Vvar r))) Vskip
+| tr_instr_Iload :
+    forall mem addr args s s' i c dst n,
+      translate_arr_access mem addr args stk s = OK c s' i ->
+      tr_instr fin rtrn st stk (RTL.Iload mem addr args dst n) (block dst c) (state_goto st n)
+| tr_instr_Istore :
+    forall mem addr args s s' i c src n,
+      translate_arr_access mem addr args stk s = OK c s' i ->
+      tr_instr fin rtrn st stk (RTL.Istore mem addr args src n) (Vblock c (Vvar src))
+               (state_goto st n).
 Hint Constructors tr_instr : htlspec.
 
 Inductive tr_code (c : RTL.code) (pc : RTL.node) (i : RTL.instruction) (stmnts trans : PTree.t stmnt)
-          (fin rtrn st : reg) : Prop :=
+          (fin rtrn st stk : reg) : Prop :=
   tr_code_intro :
     forall s t,
       c!pc = Some i ->
       stmnts!pc = Some s ->
       trans!pc = Some t ->
-      tr_instr fin rtrn st i s t ->
-      tr_code c pc i stmnts trans fin rtrn st.
+      tr_instr fin rtrn st stk i s t ->
+      tr_code c pc i stmnts trans fin rtrn st stk.
 Hint Constructors tr_code : htlspec.
 
 Inductive tr_module (f : RTL.function) : module -> Prop :=
   tr_module_intro :
-    forall data control fin rtrn st m,
+    forall data control fin rtrn st stk m,
       (forall pc i, Maps.PTree.get pc f.(RTL.fn_code) = Some i ->
-                    tr_code f.(RTL.fn_code) pc i data control fin rtrn st) ->
+                    tr_code f.(RTL.fn_code) pc i data control fin rtrn st stk) ->
       m = (mkmodule f.(RTL.fn_params)
                         data
                         control
                         f.(RTL.fn_entrypoint)
-                            st fin rtrn) ->
+                            st stk fin rtrn) ->
       tr_module f m.
 Hint Constructors tr_module : htlspec.
 
 Lemma create_reg_datapath_trans :
-  forall s s' x i,
-    create_reg s = OK x s' i ->
+  forall sz s s' x i,
+    create_reg sz s = OK x s' i ->
     s.(st_datapath) = s'.(st_datapath).
 Proof. intros. monadInv H. trivial. Qed.
 Hint Resolve create_reg_datapath_trans : htlspec.
 
 Lemma create_reg_controllogic_trans :
-  forall s s' x i,
-    create_reg s = OK x s' i ->
+  forall sz s s' x i,
+    create_reg sz s = OK x s' i ->
     s.(st_controllogic) = s'.(st_controllogic).
 Proof. intros. monadInv H. trivial. Qed.
 Hint Resolve create_reg_controllogic_trans : htlspec.
 
+Lemma create_arr_datapath_trans :
+  forall sz ln s s' x i,
+    create_arr sz ln s = OK x s' i ->
+    s.(st_datapath) = s'.(st_datapath).
+Proof. intros. monadInv H. trivial. Qed.
+Hint Resolve create_arr_datapath_trans : htlspec.
+
+Lemma create_arr_controllogic_trans :
+  forall sz ln s s' x i,
+    create_arr sz ln s = OK x s' i ->
+    s.(st_controllogic) = s'.(st_controllogic).
+Proof. intros. monadInv H. trivial. Qed.
+Hint Resolve create_arr_controllogic_trans : htlspec.
+
 Lemma get_refl_x :
   forall s s' x i,
     get s = OK x s' i ->
@@ -214,10 +239,14 @@ Hint Resolve get_refl_s : htlspec.
 
 Ltac inv_incr :=
   repeat match goal with
-  | [ H: create_reg ?s = OK _ ?s' _ |- _ ] =>
+  | [ H: create_reg _ ?s = OK _ ?s' _ |- _ ] =>
     let H1 := fresh "H" in
     assert (H1 := H); eapply create_reg_datapath_trans in H;
     eapply create_reg_controllogic_trans in H1
+  | [ H: create_arr _ _ ?s = OK _ ?s' _ |- _ ] =>
+    let H1 := fresh "H" in
+    assert (H1 := H); eapply create_arr_datapath_trans in H;
+    eapply create_arr_controllogic_trans in H1
   | [ H: get ?s = OK _ _ _ |- _ ] =>
     let H1 := fresh "H" in
     assert (H1 := H); apply get_refl_x in H; apply get_refl_s in H1;
@@ -281,13 +310,13 @@ Ltac destruct_optional :=
   match goal with H: option ?r |- _ => destruct H end.
 
 Lemma iter_expand_instr_spec :
-  forall l fin rtrn s s' i x c,
-    HTLMonadExtra.collectlist (transf_instr fin rtrn) l s = OK x s' i ->
+  forall l fin rtrn stack s s' i x c,
+    HTLMonadExtra.collectlist (transf_instr fin rtrn stack) l s = OK x s' i ->
     list_norepet (List.map fst l) ->
     (forall pc instr, In (pc, instr) l -> c!pc = Some instr) ->
     (forall pc instr, In (pc, instr) l ->
                       c!pc = Some instr ->
-                      tr_code c pc instr s'.(st_datapath) s'.(st_controllogic) fin rtrn s'.(st_st)).
+                      tr_code c pc instr s'.(st_datapath) s'.(st_controllogic) fin rtrn s'.(st_st) stack).
 Proof.
   induction l; simpl; intros; try contradiction.
   destruct a as [pc1 instr1]; simpl in *. inv H0. monadInv H. inv_incr.
@@ -351,9 +380,9 @@ Proof.
   econstructor; simpl; trivial.
   intros.
   inv_incr.
-  assert (STC: st_controllogic s8 = st_controllogic s2) by congruence.
-  assert (STD: st_datapath s8 = st_datapath s2) by congruence.
-  assert (STST: st_st s8 = st_st s2) by congruence.
+  assert (STC: st_controllogic s9 = st_controllogic s3) by congruence.
+  assert (STD: st_datapath s9 = st_datapath s3) by congruence.
+  assert (STST: st_st s9 = st_st s3) by congruence.
   rewrite STC. rewrite STD. rewrite STST.
   eapply iter_expand_instr_spec; eauto with htlspec.
   apply PTree.elements_complete.
diff --git a/src/verilog/HTL.v b/src/verilog/HTL.v
index a553453..cb081b2 100644
--- a/src/verilog/HTL.v
+++ b/src/verilog/HTL.v
@@ -43,6 +43,7 @@ Record module: Type :=
     mod_controllogic : controllogic;
     mod_entrypoint : node;
     mod_st : reg;
+    mod_stk : reg;
     mod_finish : reg;
     mod_return : reg
   }.