Merge branch 'bitfields_fix' of /home/monniaux/work/Kalray/bitfields_fix into towards_3.10

2 files changed, 80 insertions, 3 deletions

diff --git a/kvx/SelectOp.vp b/kvx/SelectOp.vp
index 16607cf5..4e1087f9 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
@@ -421,7 +434,16 @@ Nondetfunction or (e1: expr) (e2: expr) :=
           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 let zstart := 0 in
+               let zstop := int_highest_bit nmask in
+               if is_bitfield zstop zstart
+               then
+                 let mask' := Int.repr (zbitfield_mask zstop zstart) in
+                 if and_dec (Int.eq_dec nmask mask')
+                            (Int.eq_dec mask (Int.not mask'))
+                 then Eop (Oinsf zstop zstart) (fld:::prev:::Enil)
+                 else Eop Oor (e1:::e2:::Enil)
+               else Eop Oor (e1:::e2:::Enil)
       else Eop Oor (e1:::e2:::Enil)
   | _, _ => Eop Oor (e1:::e2:::Enil)
   end.
diff --git a/kvx/SelectOpproof.v b/kvx/SelectOpproof.v
index 45aa3343..0ede1e2d 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] | ].
@@ -816,8 +839,40 @@ Proof.
         ** unfold Int.max_unsigned, Int.modulus.
            simpl.
            lia.
-      * apply DEFAULT.
-    + apply DEFAULT.
+      * clear Risbitfield. clear o.
+        clear zstop.
+        set (zstop := (int_highest_bit nmask)).
+        destruct (is_bitfield _ _) eqn:Risbitfield.
+        ++ destruct (and_dec _ _) as [[Rmask Rnmask] | ].
+           ** subst y. subst x.
+              TrivialExists. simpl. f_equal.
+              rewrite Val.or_commut.
+              unfold insf.
+              rewrite Risbitfield.
+              rewrite Rmask.
+              rewrite Rnmask.
+              simpl.
+              unfold bitfield_mask.
+              subst zstart.
+              rewrite (Val.or_commut (Val.and v0 _)).
+              rewrite (Val.or_commut (Val.and v0 _)).
+              destruct v1; simpl; trivial.
+              unfold Int.ltu, Int.iwordsize, Int.zwordsize.
+              rewrite Int.unsigned_repr.
+              *** rewrite Int.unsigned_repr.
+                  **** simpl.
+                       rewrite Int.shl_zero.
+                       reflexivity.
+                  **** simpl.
+                       unfold Int.max_unsigned, Int.modulus.
+                       simpl.
+                       lia.
+              *** unfold Int.max_unsigned, Int.modulus.
+                  simpl.
+                  lia.
+           ** apply DEFAULT.
+        ++ apply DEFAULT.
+      + apply DEFAULT.
   - apply DEFAULT.
 Qed.