some progress on bitfields

1 files changed, 15 insertions, 1 deletions

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: