insfl generation

2 files changed, 86 insertions, 0 deletions

diff --git a/mppa_k1c/SelectLong.vp b/mppa_k1c/SelectLong.vp
index a2bc0587..3b9e5bf9 100644
--- a/mppa_k1c/SelectLong.vp
+++ b/mppa_k1c/SelectLong.vp
@@ -24,6 +24,7 @@ Require Import Op CminorSel.
 Require Import OpHelpers.
 Require Import SelectOp SplitLong.
 Require Import ExtValues.
+Require Import DecBoolOps.
 
 Local Open Scope cminorsel_scope.
 Local Open Scope string_scope.
@@ -311,6 +312,31 @@ Nondetfunction orl (e1: expr) (e2: expr) :=
      && Int64.eq zero1 Int64.zero                 
      then Eop (Oselectl (Ccompl0 Cne)) (v0:::v1:::y0:::Enil)
      else Eop Oorl (e1:::e2:::Enil)
+  | (Eop (Oandlimm nmask) (prev:::Enil)),
+    (Eop (Oandlimm mask)
+      ((Eop (Oshllimm start) (fld:::Enil)):::Enil)) =>
+      let zstart := Int.unsigned start in
+      let zstop := int64_highest_bit mask in
+      if is_bitfieldl zstop zstart
+      then
+        let mask' := Int64.repr (zbitfield_mask zstop zstart) in
+          if and_dec (Int64.eq_dec mask mask')
+                     (Int64.eq_dec nmask (Int64.not mask'))
+          then Eop (Oinsfl zstop zstart) (prev:::fld:::Enil)
+          else Eop Oorl (e1:::e2:::Enil)
+      else Eop Oorl (e1:::e2:::Enil)
+  | (Eop (Oandlimm nmask) (prev:::Enil)),
+    (Eop (Oandlimm mask) (fld:::Enil)) =>
+      let zstart := 0 in
+      let zstop := int64_highest_bit mask in
+      if is_bitfieldl zstop zstart
+      then
+        let mask' := Int64.repr (zbitfield_mask zstop zstart) in
+          if and_dec (Int64.eq_dec mask mask')
+                     (Int64.eq_dec nmask (Int64.not mask'))
+          then Eop (Oinsfl zstop zstart) (prev:::fld:::Enil)
+          else Eop Oorl (e1:::e2:::Enil)
+      else Eop Oorl (e1:::e2:::Enil)
   | _, _ => Eop Oorl (e1:::e2:::Enil)
   end.
 
@@ -421,3 +447,7 @@ Definition singleoflong (e: expr) := SplitLong.singleoflong e.
 Definition singleoflongu (e: expr) := SplitLong.singleoflongu e.
 
 End SELECT.
+
+(* Local Variables: *)
+(* mode: coq *)
+(* End: *)
\ No newline at end of file
diff --git a/mppa_k1c/SelectLongproof.v b/mppa_k1c/SelectLongproof.v
index b3cb1ce0..cf8eed2b 100644
--- a/mppa_k1c/SelectLongproof.v
+++ b/mppa_k1c/SelectLongproof.v
@@ -24,6 +24,7 @@ Require Import Cminor Op CminorSel.
 Require Import OpHelpers OpHelpersproof.
 Require Import SelectOp SelectOpproof SplitLong SplitLongproof.
 Require Import SelectLong.
+Require Import DecBoolOps.
 
 Local Open Scope cminorsel_scope.
 Local Open Scope string_scope.
@@ -588,6 +589,61 @@ Proof.
       rewrite Int64.and_zero.
       rewrite Int64.or_zero.
       reflexivity.
+
+  - (*insfl first case*)
+    destruct (is_bitfieldl _ _) eqn:Risbitfield.
+    + destruct (and_dec _ _) as [[Rmask Rnmask] | ].
+      * rewrite Rnmask in *.
+        inv H. inv H0. inv H4. inv H3. inv H9. inv H8.
+        simpl in H6, H7.
+        inv H6. inv H7.
+        inv H4. inv H3. inv H7.
+        simpl in H6.
+        inv H6.
+        set (zstop := (int64_highest_bit mask)) in *.
+        set (zstart := (Int.unsigned start)) in *.
+        
+        TrivialExists.
+        simpl. f_equal.
+        
+        unfold insfl.
+        rewrite Risbitfield.
+        rewrite Rmask.
+        simpl.
+        unfold bitfield_maskl.
+        subst zstart.
+        rewrite Int.repr_unsigned.
+        reflexivity.
+      * TrivialExists.
+    + TrivialExists.
+  - destruct (is_bitfieldl _ _) eqn:Risbitfield.
+    + destruct (and_dec _ _) as [[Rmask Rnmask] | ].
+      * rewrite Rnmask in *.
+        inv H. inv H0. inv H4. inv H6. inv H8. inv H3. inv H8.
+        inv H0. simpl in H7. inv H7.
+        set (zstop := (int64_highest_bit mask)) in *.
+        set (zstart := 0) in *.
+    
+        TrivialExists. simpl. f_equal.
+        unfold insfl.
+        rewrite Risbitfield.
+        rewrite Rmask.
+        simpl.
+        subst zstart.
+        f_equal.
+        destruct v0; simpl; trivial.
+        unfold Int.ltu, Int64.iwordsize', Int64.zwordsize, Int64.wordsize.
+        rewrite Int.unsigned_repr.
+        ** rewrite Int.unsigned_repr.
+           *** simpl.
+               rewrite Int64.shl'_zero.
+               reflexivity.
+           *** simpl. unfold Int.max_unsigned. unfold Int.modulus.
+               simpl. omega.
+        ** unfold Int.max_unsigned. unfold Int.modulus.
+               simpl. omega.
+      * TrivialExists.
+    + TrivialExists.
 - TrivialExists.
 Qed.