recognize insf (missing one case)

2 files changed, 37 insertions, 0 deletions

diff --git a/kvx/SelectOp.vp b/kvx/SelectOp.vp
index 16607cf5..295506b9 100644
--- a/kvx/SelectOp.vp
+++ b/kvx/SelectOp.vp
@@ -411,6 +411,19 @@ Nondetfunction or (e1: expr) (e2: expr) :=
           then Eop (Oinsf zstop zstart) (prev:::fld:::Enil)
           else Eop Oor (e1:::e2:::Enil)
       else Eop Oor (e1:::e2:::Enil)
+  | (Eop (Oandimm mask)
+         ((Eop (Oshlimm start) (fld:::Enil)):::Enil)),
+    (Eop (Oandimm nmask) (prev:::Enil)) =>
+      let zstart := Int.unsigned start in
+      let zstop := int_highest_bit mask in
+      if is_bitfield zstop zstart
+      then
+        let mask' := Int.repr (zbitfield_mask zstop zstart) in
+          if and_dec (Int.eq_dec mask mask')
+                     (Int.eq_dec nmask (Int.not mask'))
+          then Eop (Oinsf zstop zstart) (prev:::fld:::Enil)
+          else Eop Oor (e1:::e2:::Enil)
+      else Eop Oor (e1:::e2:::Enil)
   | (Eop (Oandimm nmask) (prev:::Enil)),
     (Eop (Oandimm mask) (fld:::Enil)) =>
       let zstart := 0 in
@@ -425,6 +438,7 @@ Nondetfunction or (e1: expr) (e2: expr) :=
       else Eop Oor (e1:::e2:::Enil)
   | _, _ => Eop Oor (e1:::e2:::Enil)
   end.
+(* TODO traiter le cas pas de shift *)
 
 Nondetfunction xorimm (n1: int) (e2: expr) :=
   if Int.eq n1 Int.zero
diff --git a/kvx/SelectOpproof.v b/kvx/SelectOpproof.v
index 45aa3343..392e1077 100644
--- a/kvx/SelectOpproof.v
+++ b/kvx/SelectOpproof.v
@@ -788,6 +788,29 @@ Proof.
       * apply DEFAULT.
     + apply DEFAULT.
   - set (zstop := (int_highest_bit mask)).
+    set (zstart := (Int.unsigned start)).
+    destruct (is_bitfield _ _) eqn:Risbitfield.
+    + destruct (and_dec _ _) as [[Rmask Rnmask] | ].
+      * simpl in H6.
+        injection H6.
+        clear H6.
+        intro. subst y. subst x.
+        TrivialExists.
+        rewrite Val.or_commut.
+        simpl. f_equal.
+        unfold insf.
+        rewrite Risbitfield.
+        rewrite Rmask.
+        rewrite Rnmask.
+        simpl.
+        unfold bitfield_mask.
+        subst v1.
+        subst zstart.
+        rewrite Int.repr_unsigned.
+        reflexivity.
+      * apply DEFAULT.
+    + apply DEFAULT.
+  - set (zstop := (int_highest_bit mask)).
     set (zstart := 0).
     destruct (is_bitfield _ _) eqn:Risbitfield.
     + destruct (and_dec _ _) as [[Rmask Rnmask] | ].