recognize insf (missing one case)

1 files changed, 14 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