From 581d576e96463da6be672db1a85678a2a15f93a6 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Thu, 25 Apr 2019 07:17:06 +0200
Subject: some progress on bitfields

---
 mppa_k1c/NeedOp.v        |  1 +
 mppa_k1c/Op.v            | 16 +++++++++++++++-
 mppa_k1c/SelectOp.vp     |  8 ++++++++
 mppa_k1c/SelectOpproof.v |  9 +++++++++
 4 files changed, 33 insertions(+), 1 deletion(-)

diff --git a/mppa_k1c/NeedOp.v b/mppa_k1c/NeedOp.v
index ba051c90..150c59e9 100644
--- a/mppa_k1c/NeedOp.v
+++ b/mppa_k1c/NeedOp.v
@@ -118,6 +118,7 @@ Definition needs_of_operation (op: operation) (nv: nval): list nval :=
   | Olongofsingle | Olonguofsingle | Osingleoflong | Osingleoflongu => op1 (default nv)
   | Ocmp c => needs_of_condition c
   | Oselect _ | Oselectl _ | Oselectf _ | Oselectfs _ => op3 (default nv)
+  | Oextfz _ _ => op1 (default nv)
   end.
 
 Definition operation_is_redundant (op: operation) (nv: nval): bool :=
diff --git a/mppa_k1c/Op.v b/mppa_k1c/Op.v
index 14758bee..8180c43f 100644
--- a/mppa_k1c/Op.v
+++ b/mppa_k1c/Op.v
@@ -197,7 +197,8 @@ Inductive operation : Type :=
   | Oselect (cond: condition0)    (**r [rd = if cond r3 then r2 else r1] *)
   | Oselectl (cond: condition0)   (**r [rd = if cond r3 then r2 else r1] *)
   | Oselectf (cond: condition0)   (**r [rd = if cond r3 then r2 else r1] *)
-  | Oselectfs (cond: condition0). (**r [rd = if cond r3 then r2 else r1] *)
+  | Oselectfs (cond: condition0) (**r [rd = if cond r3 then r2 else r1] *)
+  | Oextfz (stop : int) (start : int).
 
 (** Addressing modes.  [r1], [r2], etc, are the arguments to the
   addressing. *)
@@ -498,6 +499,7 @@ Definition eval_operation
   | (Oselectl cond), v0::v1::vselect::nil => Some (eval_selectl cond v0 v1 vselect m)
   | (Oselectf cond), v0::v1::vselect::nil => Some (eval_selectf cond v0 v1 vselect m)
   | (Oselectfs cond), v0::v1::vselect::nil => Some (eval_selectfs cond v0 v1 vselect m)
+  | (Oextfz stop start), v0::nil => Some (Val.extfz stop start v0)
   | _, _ => None
   end.
 
@@ -691,6 +693,7 @@ Definition type_of_operation (op: operation) : list typ * typ :=
   | Oselectl cond => (Tlong :: Tlong :: (arg_type_of_condition0 cond) :: nil, Tlong)
   | Oselectf cond => (Tfloat :: Tfloat :: (arg_type_of_condition0 cond) :: nil, Tfloat)
   | Oselectfs cond => (Tsingle :: Tsingle ::  (arg_type_of_condition0 cond) :: nil, Tsingle)
+  | Oextfz _ _ => (Tint :: nil, Tint)
   end.
 
 Definition type_of_addressing (addr: addressing) : list typ :=
@@ -963,6 +966,11 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type).
     + destruct Archi.ptr64; simpl; trivial.
       destruct (_ && _); simpl; trivial.
       destruct (Val.cmp_different_blocks _); simpl; trivial.
+ (* extfz *)
+  - unfold Val.extfz.
+    destruct (_ && _ && _).
+    + destruct v0; simpl; trivial.
+    + constructor.
 Qed.
 
 End SOUNDNESS.
@@ -1572,6 +1580,12 @@ Proof.
       reflexivity.
       assumption.
     * rewrite Hcond'. constructor.
+
+ (* extfz *)
+  - unfold Val.extfz.
+    destruct (_ && _ && _).
+    + inv H4; trivial.
+    + trivial.
 Qed.
 
 Lemma eval_addressing_inj:
diff --git a/mppa_k1c/SelectOp.vp b/mppa_k1c/SelectOp.vp
index d5e3ee4a..8f953425 100644
--- a/mppa_k1c/SelectOp.vp
+++ b/mppa_k1c/SelectOp.vp
@@ -202,6 +202,14 @@ Nondetfunction shrimm (e1: expr) (n: int) :=
         if Int.ltu (Int.add n n1) Int.iwordsize
         then Eop (Oshrimm (Int.add n n1)) (t1:::Enil)
         else Eop (Oshrimm n) (e1:::Enil)
+    | Eop (Oshlimm n1) (t1:::Enil) =>
+        let stop := Int.sub Int.iwordsize (Int.add n1 Int.one) in
+	let start := Int.sub (Int.add (Int.add n stop) Int.one) Int.iwordsize in
+	if (Int.cmp Cle start stop)
+         && (Int.cmp Cge start Int.zero)
+         && (Int.cmp Clt stop Int.iwordsize)
+        then Eop (Oextfz stop start) (t1:::Enil)
+	else Eop (Oshrimm n) (e1:::Enil)
     | _ =>
         Eop (Oshrimm n) (e1:::Enil)
     end.
diff --git a/mppa_k1c/SelectOpproof.v b/mppa_k1c/SelectOpproof.v
index fe2ff816..65ed212b 100644
--- a/mppa_k1c/SelectOpproof.v
+++ b/mppa_k1c/SelectOpproof.v
@@ -334,6 +334,15 @@ Proof.
     rewrite Int.add_commut. rewrite Int.shr_shr; auto. rewrite Int.add_commut; auto.
     subst. TrivialExists. econstructor. EvalOp. simpl; eauto. constructor.
     simpl. auto.
+  - subst x.
+    destruct (_ && _ && _) eqn:BOUNDS.
+    + exists (Val.extfz (Int.sub Int.iwordsize (Int.add n1 Int.one))
+            (Int.sub
+               (Int.add
+                  (Int.add n (Int.sub Int.iwordsize (Int.add n1 Int.one)))
+                  Int.one) Int.iwordsize) v1).
+      split.
+      ++ constructor.
   - TrivialExists.
   - intros; TrivialExists. constructor. eauto. constructor. EvalOp. simpl; eauto. constructor.
     auto.
-- 
cgit