Started to add addressing with register + register, Mach -> Asm not done yet

5 files changed, 12 insertions, 3 deletions

diff --git a/mppa_k1c/Op.v b/mppa_k1c/Op.v
index c4338857..d533a504 100644
--- a/mppa_k1c/Op.v
+++ b/mppa_k1c/Op.v
@@ -187,6 +187,7 @@ Inductive operation : Type :=
   addressing. *)
 
 Inductive addressing: Type :=
+  | Aindexed2: addressing                  (**r Address is [r1 + r2] *)
   | Aindexed: ptrofs -> addressing    (**r Address is [r1 + offset] *)
   | Aglobal: ident -> ptrofs -> addressing  (**r Address is global plus offset *)
   | Ainstack: ptrofs -> addressing.   (**r Address is [stack_pointer + offset] *)
@@ -385,6 +386,7 @@ Definition eval_addressing
     (F V: Type) (genv: Genv.t F V) (sp: val)
     (addr: addressing) (vl: list val) : option val :=
   match addr, vl with
+  | Aindexed2, v1 :: v2 :: nil => Some (Val.addl v1 v2)
   | Aindexed n, v1 :: nil => Some (Val.offset_ptr v1 n)
   | Aglobal s ofs, nil => Some (Genv.symbol_address genv s ofs)
   | Ainstack n, nil => Some (Val.offset_ptr sp n)
@@ -569,6 +571,7 @@ Definition type_of_operation (op: operation) : list typ * typ :=
 
 Definition type_of_addressing (addr: addressing) : list typ :=
   match addr with
+  | Aindexed2 => Tptr :: Tptr :: nil
   | Aindexed _ => Tptr :: nil
   | Aglobal _ _ => nil
   | Ainstack _ => nil
@@ -914,6 +917,7 @@ Qed.
 
 Definition offset_addressing (addr: addressing) (delta: Z) : option addressing :=
   match addr with
+  | Aindexed2 => None
   | Aindexed n => Some(Aindexed (Ptrofs.add n (Ptrofs.repr delta)))
   | Aglobal id n => Some(Aglobal id (Ptrofs.add n (Ptrofs.repr delta)))
   | Ainstack n => Some(Ainstack (Ptrofs.add n (Ptrofs.repr delta)))
@@ -1337,9 +1341,10 @@ Lemma eval_addressing_inj:
   exists v2, eval_addressing ge2 sp2 addr vl2 = Some v2 /\ Val.inject f v1 v2.
 Proof.
   intros. destruct addr; simpl in H2; simpl; FuncInv; InvInject; TrivialExists.
-  apply Val.offset_ptr_inject; auto.
-  apply H; simpl; auto.
-  apply Val.offset_ptr_inject; auto. 
+  - apply Val.addl_inject; auto.
+  - apply Val.offset_ptr_inject; auto.
+  - apply H; simpl; auto.
+  - apply Val.offset_ptr_inject; auto. 
 Qed.
 
 End EVAL_COMPAT.
diff --git a/mppa_k1c/PrintOp.ml b/mppa_k1c/PrintOp.ml
index 9ec474b3..5ac00404 100644
--- a/mppa_k1c/PrintOp.ml
+++ b/mppa_k1c/PrintOp.ml
@@ -160,6 +160,7 @@ let print_operation reg pp = function
 
 let print_addressing reg pp = function
   | Aindexed n, [r1] -> fprintf pp "%a + %Ld" reg r1 (camlint64_of_ptrofs n)
+  | Aindexed2, [r1;r2] -> fprintf pp "%a + %a" reg r1 reg r2
   | Aglobal(id, ofs), [] ->
       fprintf pp "\"%s\" + %Ld" (extern_atom id) (camlint64_of_ptrofs ofs)
   | Ainstack ofs, [] -> fprintf pp "stack(%Ld)" (camlint64_of_ptrofs ofs)
diff --git a/mppa_k1c/SelectOp.vp b/mppa_k1c/SelectOp.vp
index f6605c11..d82fe238 100644
--- a/mppa_k1c/SelectOp.vp
+++ b/mppa_k1c/SelectOp.vp
@@ -481,6 +481,7 @@ Nondetfunction addressing (chunk: memory_chunk) (e: expr) :=
   | Eop (Oaddrsymbol id ofs) Enil => if Archi.pic_code tt then (Aindexed Ptrofs.zero, e:::Enil) else (Aglobal id ofs, Enil)
   | Eop (Oaddimm n) (e1:::Enil) => (Aindexed (Ptrofs.of_int n), e1:::Enil)
   | Eop (Oaddlimm n) (e1:::Enil) => (Aindexed (Ptrofs.of_int64 n), e1:::Enil)
+  | Eop Oaddl (e1:::e2:::Enil) => (Aindexed2, e1:::e2:::Enil) 
   | _ => (Aindexed Ptrofs.zero, e:::Enil)
   end.
 
diff --git a/mppa_k1c/SelectOpproof.v b/mppa_k1c/SelectOpproof.v
index 89af39ee..d426e4f1 100644
--- a/mppa_k1c/SelectOpproof.v
+++ b/mppa_k1c/SelectOpproof.v
@@ -991,6 +991,7 @@ Proof.
   - exists (v1 :: nil); split. eauto with evalexpr. simpl.
     destruct v1; simpl in H; try discriminate. destruct Archi.ptr64 eqn:SF; inv H. 
     simpl. auto.
+  - exists (v1 :: v0 :: nil); split. repeat (constructor; auto). simpl. congruence.
   - exists (v :: nil);  split. eauto with evalexpr. subst. simpl. rewrite Ptrofs.add_zero; auto.
 Qed.
 
diff --git a/mppa_k1c/ValueAOp.v b/mppa_k1c/ValueAOp.v
index fb1977ea..a54dbd8f 100644
--- a/mppa_k1c/ValueAOp.v
+++ b/mppa_k1c/ValueAOp.v
@@ -36,6 +36,7 @@ Definition eval_static_condition (cond: condition) (vl: list aval): abool :=
 Definition eval_static_addressing (addr: addressing) (vl: list aval): aval :=
   match addr, vl with
   | Aindexed n, v1::nil => offset_ptr v1 n
+  | Aindexed2, v1::v2::nil => addl v1 v2
   | Aglobal s ofs, nil => Ptr (Gl s ofs)
   | Ainstack ofs, nil => Ptr (Stk ofs)
   | _, _ => Vbot