progress

11 files changed, 104 insertions, 8 deletions

diff --git a/common/Values.v b/common/Values.v
index 837ed799..059a72d9 100644
--- a/common/Values.v
+++ b/common/Values.v
@@ -775,6 +775,20 @@ Definition extfz stop start v :=
     let stop' := Z.add stop Z.one in
     match v with
     | Vint w =>
+      Vint (Int.shru (Int.shl w (Int.repr (Z.sub Int.zwordsize stop'))) (Int.repr (Z.sub Int.zwordsize (Z.sub stop' start))))
+    | _ => Vundef
+    end
+  else Vundef.
+
+
+Definition extfs stop start v :=
+  if (Z.leb start stop)
+       && (Z.geb start Z.zero)
+       && (Z.ltb stop Int.zwordsize)
+  then
+    let stop' := Z.add stop Z.one in
+    match v with
+    | Vint w =>
       Vint (Int.shr (Int.shl w (Int.repr (Z.sub Int.zwordsize stop'))) (Int.repr (Z.sub Int.zwordsize (Z.sub stop' start))))
     | _ => Vundef
     end
diff --git a/mppa_k1c/Asm.v b/mppa_k1c/Asm.v
index 290691f4..1e1f6e36 100644
--- a/mppa_k1c/Asm.v
+++ b/mppa_k1c/Asm.v
@@ -131,6 +131,8 @@ Inductive instruction : Type :=
   | Pzxwd   (rd rs: ireg)                           (**r Zero Extend Word to Double Word *)

 

   | Pextfz  (rd : ireg) (rs : ireg) (stop : Z) (start : Z) (**r extract bitfields unsigned *)

+  | Pextfs  (rd : ireg) (rs : ireg) (stop : Z) (start : Z) (**r extract bitfields signed *)

+

   | Pfabsd  (rd rs: ireg)                           (**r float absolute double *)

   | Pfabsw  (rd rs: ireg)                           (**r float absolute word *)

   | Pfnegd  (rd rs: ireg)                           (**r float negate double *)

@@ -283,6 +285,7 @@ Definition basic_to_instruction (b: basic) :=
   | PArithRR Asmvliw.Psxwd rd rs  => Psxwd rd rs

   | PArithRR Asmvliw.Pzxwd rd rs  => Pzxwd rd rs

   | PArithRR (Asmvliw.Pextfz stop start) rd rs => Pextfz rd rs stop start

+  | PArithRR (Asmvliw.Pextfs stop start) rd rs => Pextfs rd rs stop start

   | PArithRR Asmvliw.Pfabsd rd rs => Pfabsd rd rs

   | PArithRR Asmvliw.Pfabsw rd rs => Pfabsw rd rs

   | PArithRR Asmvliw.Pfnegd rd rs  => Pfnegd rd rs

diff --git a/mppa_k1c/Asmblockdeps.v b/mppa_k1c/Asmblockdeps.v
index b9db7760..b3a72517 100644
--- a/mppa_k1c/Asmblockdeps.v
+++ b/mppa_k1c/Asmblockdeps.v
@@ -1214,6 +1214,7 @@ Definition string_of_name_rr (n: arith_name_rr): pstring :=
   | Psxwd => "Psxwd"
   | Pzxwd => "Pzxwd"
   | Pextfz _ _ => "Pextfz"
+  | Pextfs _ _ => "Pextfs"
   | Pfabsd => "Pfabsd"
   | Pfabsw => "Pfabsw"
   | Pfnegd => "Pfnegd"
diff --git a/mppa_k1c/Asmvliw.v b/mppa_k1c/Asmvliw.v
index b39ebd0e..13ff5422 100644
--- a/mppa_k1c/Asmvliw.v
+++ b/mppa_k1c/Asmvliw.v
@@ -308,6 +308,7 @@ Inductive arith_name_rr : Type :=
   | Pzxwd                                           (**r Zero Extend Word to Double Word *)
 (*  | Pextfs (stop : int) (start : int)               (**r extract bit field, signed *) *)
   | Pextfz (stop : Z) (start : Z)               (**r extract bit field, unsigned *)
+  | Pextfs (stop : Z) (start : Z)               (**r extract bit field, signed *)
            
   | Pfabsd                                          (**r float absolute double *)
   | Pfabsw                                          (**r float absolute word *)
@@ -881,6 +882,7 @@ Definition arith_eval_rr n v :=
   | Psxwd => Val.longofint v
   | Pzxwd => Val.longofintu v
   | Pextfz stop start => Val.extfz stop start v
+  | Pextfs stop start => Val.extfs stop start v
   | Pfnegd => Val.negf v
   | Pfnegw => Val.negfs v
   | Pfabsd => Val.absf v
diff --git a/mppa_k1c/NeedOp.v b/mppa_k1c/NeedOp.v
index 150c59e9..3a27df6a 100644
--- a/mppa_k1c/NeedOp.v
+++ b/mppa_k1c/NeedOp.v
@@ -118,7 +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)
+  | Oextfz _ _ | Oextfs _ _ => 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 8293af1e..f6433f90 100644
--- a/mppa_k1c/Op.v
+++ b/mppa_k1c/Op.v
@@ -198,7 +198,8 @@ Inductive operation : Type :=
   | 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] *)
-  | Oextfz (stop : Z) (start : Z).
+  | Oextfz (stop : Z) (start : Z)
+  | Oextfs (stop : Z) (start : Z).
 
 (** Addressing modes.  [r1], [r2], etc, are the arguments to the
   addressing. *)
@@ -500,6 +501,7 @@ Definition eval_operation
   | (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)
+  | (Oextfs stop start), v0::nil => Some (Val.extfs stop start v0)
   | _, _ => None
   end.
 
@@ -693,7 +695,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)
+  | Oextfz _ _ | Oextfs _ _ => (Tint :: nil, Tint)
   end.
 
 Definition type_of_addressing (addr: addressing) : list typ :=
@@ -971,6 +973,11 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type).
     destruct (_ && _ && _).
     + destruct v0; simpl; trivial.
     + constructor.
+ (* extfs *)
+  - unfold Val.extfs.
+    destruct (_ && _ && _).
+    + destruct v0; simpl; trivial.
+    + constructor.
 Qed.
 
 End SOUNDNESS.
@@ -1586,6 +1593,12 @@ Proof.
     destruct (_ && _ && _).
     + inv H4; trivial.
     + trivial.
+
+ (* extfs *)
+  - unfold Val.extfs.
+    destruct (_ && _ && _).
+    + inv H4; trivial.
+    + trivial.
 Qed.
 
 Lemma eval_addressing_inj:
diff --git a/mppa_k1c/PostpassSchedulingOracle.ml b/mppa_k1c/PostpassSchedulingOracle.ml
index 8f6484d6..78a29fbb 100644
--- a/mppa_k1c/PostpassSchedulingOracle.ml
+++ b/mppa_k1c/PostpassSchedulingOracle.ml
@@ -35,6 +35,7 @@ let arith_rr_str = function
   | Psxwd -> "Psxwd"
   | Pzxwd -> "Pzxwd"
   | Pextfz(_,_) -> "Pextfz"
+  | Pextfs(_,_) -> "Pextfs"
   | Pfabsw -> "Pfabsw"
   | Pfabsd -> "Pfabsd"
   | Pfnegw -> "Pfnegw"
diff --git a/mppa_k1c/SelectOp.vp b/mppa_k1c/SelectOp.vp
index 3e36a51c..6bb5ee56 100644
--- a/mppa_k1c/SelectOp.vp
+++ b/mppa_k1c/SelectOp.vp
@@ -186,6 +186,14 @@ Nondetfunction shruimm (e1: expr) (n: int) :=
         if Int.ltu (Int.add n n1) Int.iwordsize
         then Eop (Oshruimm (Int.add n n1)) (t1:::Enil)
         else Eop (Oshruimm n) (e1:::Enil)
+    | Eop (Oshlimm n1) (t1:::Enil) =>
+        let stop := Z.sub Int.zwordsize (Z.add (Int.unsigned n1) Z.one) in
+	let start := Z.sub (Z.add (Z.add (Int.unsigned n) stop) Z.one) Int.zwordsize in
+	if (Z.leb start stop)
+         && (Z.geb start Z.zero)
+         && (Z.ltb stop Int.zwordsize)
+        then Eop (Oextfz stop start) (t1:::Enil)
+	else Eop (Oshruimm n) (e1:::Enil)
     | _ =>
         Eop (Oshruimm n) (e1:::Enil)
     end.
@@ -208,7 +216,7 @@ Nondetfunction shrimm (e1: expr) (n: int) :=
 	if (Z.leb start stop)
          && (Z.geb start Z.zero)
          && (Z.ltb stop Int.zwordsize)
-        then Eop (Oextfz stop start) (t1:::Enil)
+        then Eop (Oextfs stop start) (t1:::Enil)
 	else Eop (Oshrimm n) (e1:::Enil)
     | _ =>
         Eop (Oshrimm n) (e1:::Enil)
diff --git a/mppa_k1c/SelectOpproof.v b/mppa_k1c/SelectOpproof.v
index d072bb7b..8bc8c96b 100644
--- a/mppa_k1c/SelectOpproof.v
+++ b/mppa_k1c/SelectOpproof.v
@@ -295,7 +295,7 @@ Proof.
   predSpec Int.eq Int.eq_spec n Int.zero.
   intros; subst. exists x; split; auto. destruct x; simpl; auto. rewrite Int.shru_zero; auto.
 
-  destruct (Int.ltu n Int.iwordsize) eqn:LT; simpl.
+  destruct (Int.ltu n Int.iwordsize) eqn:LT.
   destruct (shruimm_match a); intros; InvEval.
   - exists (Vint (Int.shru n1 n)); split. EvalOp.
     simpl. rewrite LT; auto.
@@ -307,6 +307,38 @@ Proof.
     rewrite LT. rewrite Int.add_commut. rewrite Int.shru_shru; auto. rewrite Int.add_commut; auto.
     subst. TrivialExists. econstructor. EvalOp. simpl; eauto. constructor.
     simpl. auto.
+  - subst x.
+    simpl negb.
+    cbn iota.
+    destruct (_ && _ && _) eqn:BOUNDS.
+    + exists (Val.extfz (Z.sub Int.zwordsize (Z.add (Int.unsigned n1) Z.one))
+            (Z.sub
+               (Z.add
+                  (Z.add (Int.unsigned n) (Z.sub Int.zwordsize (Z.add (Int.unsigned n1) Z.one)))
+                  Z.one) Int.zwordsize) v1).
+      split.
+      ++ EvalOp.
+      ++ unfold Val.extfz.
+         rewrite BOUNDS.
+         destruct v1; try (simpl; apply Val.lessdef_undef).
+        replace (Z.sub Int.zwordsize
+                         (Z.add (Z.sub Int.zwordsize (Z.add (Int.unsigned n1) Z.one)) Z.one)) with (Int.unsigned n1).
+        replace (Z.sub Int.zwordsize
+             (Z.sub
+                (Z.add (Z.sub Int.zwordsize (Z.add (Int.unsigned n1) Z.one)) Z.one)
+                (Z.sub
+                   (Z.add
+                      (Z.add (Int.unsigned n) (Z.sub Int.zwordsize (Z.add (Int.unsigned n1) Z.one)))
+                      Z.one) Int.zwordsize))) with (Int.unsigned n).
+        * rewrite Int.repr_unsigned.
+          rewrite Int.repr_unsigned.
+          simpl.
+          destruct (Int.ltu n1 Int.iwordsize) eqn:Hltu_n1; simpl; trivial.
+          simpl.
+          destruct (Int.ltu n Int.iwordsize) eqn:Hltu_n; simpl; trivial.
+        * omega.
+        * omega.
+    + TrivialExists. constructor. econstructor. constructor. eassumption. constructor. simpl. reflexivity. constructor. simpl. reflexivity.
   - TrivialExists.
   - intros; TrivialExists. constructor. eauto. constructor. EvalOp. simpl; eauto. constructor.
     auto.
@@ -338,14 +370,14 @@ Proof.
     simpl negb.
     cbn iota.
     destruct (_ && _ && _) eqn:BOUNDS.
-    + exists (Val.extfz (Z.sub Int.zwordsize (Z.add (Int.unsigned n1) Z.one))
+    + exists (Val.extfs (Z.sub Int.zwordsize (Z.add (Int.unsigned n1) Z.one))
             (Z.sub
                (Z.add
                   (Z.add (Int.unsigned n) (Z.sub Int.zwordsize (Z.add (Int.unsigned n1) Z.one)))
                   Z.one) Int.zwordsize) v1).
       split.
       ++ EvalOp.
-      ++ unfold Val.extfz.
+      ++ unfold Val.extfs.
          rewrite BOUNDS.
          destruct v1; try (simpl; apply Val.lessdef_undef).
         replace (Z.sub Int.zwordsize
diff --git a/mppa_k1c/TargetPrinter.ml b/mppa_k1c/TargetPrinter.ml
index dc207dc8..8826e6a2 100644
--- a/mppa_k1c/TargetPrinter.ml
+++ b/mppa_k1c/TargetPrinter.ml
@@ -379,6 +379,8 @@ module Target (*: TARGET*) =
          fprintf oc "	zxwd	%a = %a\n" ireg rd ireg rs
       | Pextfz(rd, rs, stop, start) ->
          fprintf oc "	extfz	%a = %a, %ld, %ld\n" ireg rd ireg rs (camlint_of_coqint stop) (camlint_of_coqint start)
+      | Pextfs(rd, rs, stop, start) ->
+         fprintf oc "	extfs	%a = %a, %ld, %ld\n" ireg rd ireg rs (camlint_of_coqint stop) (camlint_of_coqint start)
       | Pfabsd(rd, rs) ->
          fprintf oc "	fabsd	%a = %a\n" ireg rd ireg rs
       | Pfabsw(rd, rs) ->
diff --git a/mppa_k1c/ValueAOp.v b/mppa_k1c/ValueAOp.v
index e498d237..23514d21 100644
--- a/mppa_k1c/ValueAOp.v
+++ b/mppa_k1c/ValueAOp.v
@@ -75,7 +75,7 @@ Definition eval_static_selectfs (cond : condition0) (v0 v1 vselect : aval) : ava
   end.
   
 
-Definition eval_static_extfz (stop : Z) (start : Z) (v : aval) :=
+Definition eval_static_extfs (stop : Z) (start : Z) (v : aval) :=
   if (Z.leb start stop)
        && (Z.geb start Z.zero)
        && (Z.ltb stop Int.zwordsize)
@@ -88,6 +88,19 @@ Definition eval_static_extfz (stop : Z) (start : Z) (v : aval) :=
     end
   else Vtop.
 
+Definition eval_static_extfz (stop : Z) (start : Z) (v : aval) :=
+  if (Z.leb start stop)
+       && (Z.geb start Z.zero)
+       && (Z.ltb stop Int.zwordsize)
+  then
+    let stop' := Z.add stop Z.one in
+    match v with
+    | I w =>
+      I (Int.shru (Int.shl w (Int.repr (Z.sub Int.zwordsize stop'))) (Int.repr (Z.sub Int.zwordsize (Z.sub stop' start))))
+    | _ => Vtop
+    end
+  else Vtop.
+
 Definition eval_static_operation (op: operation) (vl: list aval): aval :=
   match op, vl with
   | Omove, v1::nil => v1
@@ -217,6 +230,7 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval :=
   | (Oselectf cond), v0::v1::vselect::nil => eval_static_selectf cond v0 v1 vselect
   | (Oselectfs cond), v0::v1::vselect::nil => eval_static_selectfs cond v0 v1 vselect
   | (Oextfz stop start), v0::nil => eval_static_extfz stop start v0
+  | (Oextfs stop start), v0::nil => eval_static_extfs stop start v0
   | _, _ => Vbot
   end.
 
@@ -348,6 +362,12 @@ Proof.
     destruct (_ && _ && _).
     + inv H1; constructor.
     + constructor.
+
+  (* extfs *)
+  - unfold Val.extfs, eval_static_extfs.
+    destruct (_ && _ && _).
+    + inv H1; constructor.
+    + constructor.
 Qed.
 
 End SOUNDNESS.