From 26a7a6598a80c29a139c533419b38be63c88cd76 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Wed, 1 May 2019 16:24:32 +0200
Subject: indexed2XS begin

---
 mppa_k1c/Asmblockgen.v       | 1 +
 mppa_k1c/Asmblockgenproof1.v | 4 ++++
 mppa_k1c/Op.v                | 8 +++++---
 3 files changed, 10 insertions(+), 3 deletions(-)

diff --git a/mppa_k1c/Asmblockgen.v b/mppa_k1c/Asmblockgen.v
index 6cd31468..c2a0a315 100644
--- a/mppa_k1c/Asmblockgen.v
+++ b/mppa_k1c/Asmblockgen.v
@@ -888,6 +888,7 @@ Definition transl_load_rrr (chunk: memory_chunk) (addr: addressing)
 Definition transl_load (chunk: memory_chunk) (addr: addressing)
            (args: list mreg) (dst: mreg) (k: bcode) : res bcode :=
   match addr with
+  | Aindexed2XS _ => Error (msg "transl_load Aindexed2XS")
   | Aindexed2 => transl_load_rrr chunk addr args dst k
   | _ => transl_load_rro chunk addr args dst k
   end.
diff --git a/mppa_k1c/Asmblockgenproof1.v b/mppa_k1c/Asmblockgenproof1.v
index 40f9f08b..0cb2d83d 100644
--- a/mppa_k1c/Asmblockgenproof1.v
+++ b/mppa_k1c/Asmblockgenproof1.v
@@ -2168,6 +2168,7 @@ Lemma transl_load_memory_access_ok:
 Proof.
   intros until m. intros ADDR TR ? ?.
   unfold transl_load in TR. destruct addr; try contradiction.
+  - (* Indexed2XS*) monadInv TR.
   - monadInv TR. destruct chunk; ArgsInv; econstructor; (esplit; eauto).
   - monadInv TR. destruct chunk. all: ArgsInv; destruct args; try discriminate; monadInv EQ0; eexists; eexists; split; try split;
     [ instantiate (1 := (PLoadRRO _ x)); simpl; reflexivity
@@ -2210,6 +2211,7 @@ Lemma transl_load_correct:
   /\ forall r, r <> PC -> r <> RTMP -> r <> preg_of dst -> rs'#r = rs#r.
 Proof.
   intros until v; intros TR EV LOAD. destruct addr.
+  1: (* Aindexed2XS *) discriminate.
   2-4: exploit transl_load_memory_access_ok; eauto; try discriminate;
     intros A; destruct A as (mk_instr & rd & rdEq & B & C); rewrite rdEq;
     eapply transl_load_access_correct; eauto with asmgen.
@@ -2293,6 +2295,7 @@ Lemma transl_store_memory_access_ok:
 Proof.
   intros until m'. intros ? TR ? ?.
   unfold transl_store in TR. destruct addr; try contradiction.
+  - (* Aindex2XS *) discriminate.
   - monadInv TR. destruct chunk. all:
     ArgsInv; eexists; eexists; eexists; split; try split; [
       repeat (destruct args; try discriminate); eassumption
@@ -2362,6 +2365,7 @@ Lemma transl_store_correct:
   /\ forall r, r <> PC -> r <> RTMP -> rs'#r = rs#r.
 Proof.
   intros until m'; intros TR EV STORE. destruct addr.
+  1: (* AIndexed2XS *) discriminate.
   2-4: exploit transl_store_memory_access_ok; eauto; try discriminate; intro A;
     destruct A as (mk_instr & chunk' & rr & rrEq & B & C & D);
     rewrite D in STORE; clear D; 
diff --git a/mppa_k1c/Op.v b/mppa_k1c/Op.v
index baf17cc0..22fce4c9 100644
--- a/mppa_k1c/Op.v
+++ b/mppa_k1c/Op.v
@@ -207,7 +207,8 @@ Inductive operation : Type :=
   addressing. *)
 
 Inductive addressing: Type :=
-  | Aindexed2: addressing                  (**r Address is [r1 + r2] *)
+  | Aindexed2XS (scale : Z) : addressing (**r Address is [r1 + r2 << scale] *)
+  | 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] *)
@@ -230,7 +231,7 @@ Defined.
 
 Definition eq_addressing (x y: addressing) : {x=y} + {x<>y}.
 Proof.
-  generalize ident_eq Ptrofs.eq_dec; intros.
+  generalize ident_eq Ptrofs.eq_dec Z.eq_dec; intros.
   decide equality.
 Defined.
 
@@ -705,6 +706,7 @@ Definition type_of_operation (op: operation) : list typ * typ :=
 
 Definition type_of_addressing (addr: addressing) : list typ :=
   match addr with
+  | Aindexed2XS _ => Tptr :: Tptr :: Tptr :: nil
   | Aindexed2 => Tptr :: Tptr :: nil
   | Aindexed _ => Tptr :: nil
   | Aglobal _ _ => nil
@@ -1117,7 +1119,7 @@ Qed.
 
 Definition offset_addressing (addr: addressing) (delta: Z) : option addressing :=
   match addr with
-  | Aindexed2 => None
+  | Aindexed2 | Aindexed2XS _ => 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)))
-- 
cgit