Reduce number of array addressing modes.

2 files changed, 27 insertions, 6 deletions

diff --git a/src/translation/HTLgen.v b/src/translation/HTLgen.v
index 04de548..35203f8 100644
--- a/src/translation/HTLgen.v
+++ b/src/translation/HTLgen.v
@@ -402,6 +402,18 @@ Definition add_branch_instr (e: expr) (n n1 n2: node) : mon unit :=
 (*   | _, _, _ => error (Errors.msg "HTLgen: translate_arr_access unsuported addressing") *)
 (*   end. *)
 
+Definition translate_arr_addressing (a: Op.addressing) (args: list reg) : mon expr :=
+  match a, args with (* TODO: We should be more methodical here; what are the possibilities?*)
+  | Op.Aindexed off, r1::nil =>
+    ret (boplitz Vadd r1 off)
+  | Op.Aindexed2scaled scale offset, r1::r2::nil => (* Typical for dynamic array addressing *)
+    ret (Vbinop Vadd (boplitz Vadd r1 offset) (boplitz Vmul r2 scale))
+  | Op.Ainstack a, nil => (* We need to be sure that the base address is aligned *)
+    let a := Integers.Ptrofs.unsigned a in
+    ret (Vlit (ZToValue a))
+  | _, _ => error (Errors.msg "Veriloggen: translate_arr_addressing unsuported addressing")
+  end.
+
 Fixpoint enumerate (i : nat) (ns : list node) {struct ns} : list (nat * node) :=
   match ns with
   | n :: ns' => (i, n) :: enumerate (i+1) ns'
@@ -446,7 +458,7 @@ Definition transf_instr (fin rtrn stack: reg) (ni: node * instruction) : mon uni
       match chunk with
       | Mint32 =>
         if Z.leb (Z.pos n') Integers.Int.max_unsigned
-        then do addr' <- translate_eff_addressing addr args;
+        then do addr' <- translate_arr_addressing addr args;
              do _ <- declare_reg None dst 32;
              add_instr n n' $ create_single_cycle_load stack addr' dst
         else error (Errors.msg "State is larger than 2^32.")
@@ -456,7 +468,7 @@ Definition transf_instr (fin rtrn stack: reg) (ni: node * instruction) : mon uni
       match chunk with
       | Mint32 =>
         if Z.leb (Z.pos n') Integers.Int.max_unsigned
-        then do addr' <- translate_eff_addressing addr args;
+        then do addr' <- translate_arr_addressing addr args;
              add_instr n n' $ create_single_cycle_store stack addr' src
         else error (Errors.msg "State is larger than 2^32.")
       | _ => error (Errors.msg "Istore invalid chunk size.")
diff --git a/src/translation/HTLgenspec.v b/src/translation/HTLgenspec.v
index dda91ca..1b04b1f 100644
--- a/src/translation/HTLgenspec.v
+++ b/src/translation/HTLgenspec.v
@@ -141,14 +141,14 @@ Inductive tr_instr (fin rtrn st stk : reg) : RTL.instruction -> stmnt -> stmnt -
     forall chunk addr args s s' i e dst n,
       Z.pos n <= Int.max_unsigned ->
       chunk = AST.Mint32 ->
-      translate_eff_addressing addr args s = OK e s' i ->
+      translate_arr_addressing addr args s = OK e s' i ->
       tr_instr fin rtrn st stk (RTL.Iload chunk addr args dst n)
                                (create_single_cycle_load stk e dst) (state_goto st n)
 | tr_instr_Istore :
     forall chunk addr args s s' i e src n,
       Z.pos n <= Int.max_unsigned ->
       chunk = AST.Mint32 ->
-      translate_eff_addressing addr args s = OK e s' i ->
+      translate_arr_addressing addr args s = OK e s' i ->
       tr_instr fin rtrn st stk (RTL.Istore chunk addr args src n)
                                (create_single_cycle_store stk e src) (state_goto st n)
 | tr_instr_Ijumptable :
@@ -343,6 +343,15 @@ Proof.
 Qed.
 Hint Resolve translate_eff_addressing_freshreg_trans : htlspec.
 
+Lemma translate_arr_addressing_freshreg_trans :
+  forall op args s r s' i,
+  translate_arr_addressing op args s = OK r s' i ->
+  s.(st_freshreg) = s'.(st_freshreg).
+Proof.
+  destruct op; intros; simpl in *; repeat (unfold_match H); inv H; auto.
+Qed.
+Hint Resolve translate_eff_addressing_freshreg_trans : htlspec.
+
 Lemma translate_comparison_freshreg_trans :
   forall op args s r s' i,
   translate_comparison op args s = OK r s' i ->
@@ -419,11 +428,11 @@ Proof.
     apply declare_reg_freshreg_trans in EQ1. congruence.
   - destruct (Z.pos n0 <=? Int.max_unsigned); try discriminate.
     monadInv H. apply add_instr_freshreg_trans in EQ2.
-    apply translate_eff_addressing_freshreg_trans in EQ.
+    apply translate_arr_addressing_freshreg_trans in EQ.
     apply declare_reg_freshreg_trans in EQ1. congruence.
   - destruct (Z.pos n0 <=? Int.max_unsigned); try discriminate.
     monadInv H. apply add_instr_freshreg_trans in EQ0.
-    apply translate_eff_addressing_freshreg_trans in EQ. congruence.
+    apply translate_arr_addressing_freshreg_trans in EQ. congruence.
   - monadInv H. apply translate_condition_freshreg_trans in EQ.
     apply add_branch_instr_freshreg_trans in EQ0.
     congruence.