From 57ddece94f4c4b44e8e3127c6f5f72aaa5962250 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Wed, 1 May 2019 22:20:35 +0200
Subject: does not yet work, arity mismatch

---
 mppa_k1c/Asmblockdeps.v      |  1 +
 mppa_k1c/Asmblockgen.v       |  1 +
 mppa_k1c/Asmblockgenproof1.v |  1 +
 mppa_k1c/Asmvliw.v           | 16 +---------------
 mppa_k1c/SelectOp.vp         |  6 ++++++
 mppa_k1c/SelectOpproof.v     |  5 +++++
 6 files changed, 15 insertions(+), 15 deletions(-)

diff --git a/mppa_k1c/Asmblockdeps.v b/mppa_k1c/Asmblockdeps.v
index f6573838..1ee5002c 100644
--- a/mppa_k1c/Asmblockdeps.v
+++ b/mppa_k1c/Asmblockdeps.v
@@ -13,6 +13,7 @@ Require Import ImpDep.
 Require Import Axioms.
 Require Import Parallelizability.
 Require Import Asmvliw Permutation.
+Require Import Chunks.
 
 Open Scope impure.
 
diff --git a/mppa_k1c/Asmblockgen.v b/mppa_k1c/Asmblockgen.v
index ea99c098..ca7094da 100644
--- a/mppa_k1c/Asmblockgen.v
+++ b/mppa_k1c/Asmblockgen.v
@@ -22,6 +22,7 @@ Require Import Coqlib Errors.
 Require Import AST Integers Floats Memdata.
 Require Import Op Locations Machblock Asmblock.
 Require ExtValues.
+Require Import Chunks.
 
 Local Open Scope string_scope.
 Local Open Scope error_monad_scope.
diff --git a/mppa_k1c/Asmblockgenproof1.v b/mppa_k1c/Asmblockgenproof1.v
index 82f3b0fc..b265f221 100644
--- a/mppa_k1c/Asmblockgenproof1.v
+++ b/mppa_k1c/Asmblockgenproof1.v
@@ -19,6 +19,7 @@ Require Import Coqlib Errors Maps.
 Require Import AST Integers Floats Values Memory Globalenvs.
 Require Import Op Locations Machblock Conventions.
 Require Import Asmblock Asmblockgen Asmblockgenproof0.
+Require Import Chunks.
 
 (** Decomposition of integer constants. *)
 
diff --git a/mppa_k1c/Asmvliw.v b/mppa_k1c/Asmvliw.v
index 629d1449..e460727c 100644
--- a/mppa_k1c/Asmvliw.v
+++ b/mppa_k1c/Asmvliw.v
@@ -35,6 +35,7 @@ Require Stacklayout.
 Require Import Conventions.
 Require Import Errors.
 Require Import Sorting.Permutation.
+Require Import Chunks.
 
 (** * Abstract syntax *)
 
@@ -1119,21 +1120,6 @@ Definition parexec_load_reg (chunk: memory_chunk) (rsr rsw: regset) (mr mw: mem)
   | Some v => Next (rsw#d <- v) mw
   end.
 
-Definition zscale_of_chunk (chunk: memory_chunk) :=
-  match chunk with
-  | Mint8signed => 0
-  | Mint8unsigned => 0
-  | Mint16signed => 1
-  | Mint16unsigned => 1
-  | Mint32 => 2
-  | Mint64 => 3
-  | Mfloat32 => 2
-  | Mfloat64 => 3
-  | Many32 => 2
-  | Many64 => 3
-  end.
-Definition scale_of_chunk chunk := Vint (Int.repr (zscale_of_chunk chunk)).
-
 Definition parexec_load_regxs (chunk: memory_chunk) (rsr rsw: regset) (mr mw: mem) (d a ro: ireg) :=
   match Mem.loadv chunk mr (Val.addl (rsr a) (Val.shll (rsr ro) (scale_of_chunk chunk))) with
   | None => Stuck
diff --git a/mppa_k1c/SelectOp.vp b/mppa_k1c/SelectOp.vp
index 25f09e2e..28b91728 100644
--- a/mppa_k1c/SelectOp.vp
+++ b/mppa_k1c/SelectOp.vp
@@ -53,6 +53,7 @@ Require Import CminorSel.
 Require Import OpHelpers.
 Require Import ExtValues.
 Require Import DecBoolOps.
+Require Import Chunks.
 
 Local Open Scope cminorsel_scope.
 
@@ -584,6 +585,11 @@ 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:::(Eop (Oshllimm scale) (e2:::Enil)):::Enil) =>
+    let zscale := Int.unsigned scale in
+    if Z.eq_dec zscale (zscale_of_chunk chunk)
+    then (Aindexed2XS zscale, e1:::e2:::Enil) 
+    else (Aindexed2, e1:::(Eop (Oshllimm scale) (e2:::Enil)):::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 6fa93fd8..a92ed572 100644
--- a/mppa_k1c/SelectOpproof.v
+++ b/mppa_k1c/SelectOpproof.v
@@ -1265,6 +1265,11 @@ 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.
+  - destruct (Z.eq_dec _ _).
+    + exists (v1 :: v2 :: nil); split. repeat (constructor; auto). simpl. rewrite Int.repr_unsigned. destruct v2; simpl in *; congruence.
+    + exists (v1 :: v0 :: nil); split. repeat (constructor; auto). econstructor.
+      repeat (constructor; auto). eassumption. simpl. congruence.
+      simpl. congruence.
   - 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.
-- 
cgit