[WP] bitwise simplifier improvement

src/plugins/wp/tests/wp_acsl/bitwise.i

@@ -136,13 +136,22 @@ unsigned char cast_uchar(int x) {
   //@ check bit_unset:      ok: (c & 0x77) == 0x66 ==> (x & 1) == 0 ;
   //@ check bit_set_unset:  ok: (c & 0x77) == 0x66 && (x & 5) == (x & 7) ==> (x & 4) == (x & 6) ;
   //@ check bit_set_unset2: ok: (c & 0x77) == 0x66 && (x & 5) == (x & 7) ==> (P(x & 4) <==> P(x & 6)) ;
+
   //@ check bit_defined:    ok: (c & 0x77) == 0x66 && (x & ~0x77) == (~0x77 & 0xFFF0) ==> (P(c)<==>P(0xE6));
   //@ check bit_defined2:   ok: (c & 0x77) == 0x66 && (x & ~0x77) == (~0x77 & 0xFFF0) ==> (P(x)<==>P(0xFFE6));
+
   //@ check bit_to_signed_positive:  ok: (x & 0xFF) == 0x60 ==> (P((signed char) x) <==> P(0x60));
   //@ check bit_to_signed_positive2: ok: (x & 0xF0) == 0x60 ==> (((signed char) x) & (1 << 10)) == 0;
   //@ check bit_to_signed_negative:  ok: (x & 0xFF) == 0x86 ==>  (P((signed char) x) <==> P(0x86|~255));
   //@ check bit_to_signed_negative2: ok: (x & 0xF0) == 0x80 ==> (((signed char) x) & (1 << 10)) != 0;
   //@ check bit_to_signed:           ok: (x & 0x0F) == 0x06 ==> (((signed char) x) & (1 << 3)) == 0;
   //@ check bit_to_signed2:          ok: (x & 0x0F) == 0x06 ==> (((signed char) x) & (1 << 2)) != 0;
+
+  //@ check bit_lsl_lowest:          ok: ((x<<2) & 0x0F) != 0x03 ;
+  //@ check bit_lsl_higher_set:      ok: ((x<<2) & 0xFF) == (0x0F & ~0x03) ==> (x & 0x03) != 0 ;
+  //@ check bit_lsl_higher_unset:    ok: ((x<<2) & 0xFF) == (0x0F & ~0x03) ==> (x & (0xFF>>2) & ~0x03) == 0 ;
+
+  //@ check bit_lsr_set:             ok: ((x>>2) & 0xFF) == (0x0F & ~0x03) ==> (x & 0x30) != 0 ;
+  //@ check bit_lsr_unset:           ok: ((x>>2) & 0xFF) == (0x0F & ~0x03) ==> (x & ((0xFF<<2) & ~0x30)) == 0 ;
   return c;
 }

src/plugins/wp/tests/wp_acsl/oracle/bitwise.res.oracle

@@ -247,42 +247,67 @@ Prove: true.
 
 ------------------------------------------------------------
 
-Goal Check 'bit_defined,ok' (file bitwise.i, line 139):
+Goal Check 'bit_defined,ok' (file bitwise.i, line 140):
 Prove: true.
 
 ------------------------------------------------------------
 
-Goal Check 'bit_defined2,ok' (file bitwise.i, line 140):
+Goal Check 'bit_defined2,ok' (file bitwise.i, line 141):
 Prove: true.
 
 ------------------------------------------------------------
 
-Goal Check 'bit_to_signed_positive,ok' (file bitwise.i, line 141):
+Goal Check 'bit_to_signed_positive,ok' (file bitwise.i, line 143):
 Prove: true.
 
 ------------------------------------------------------------
 
-Goal Check 'bit_to_signed_positive2,ok' (file bitwise.i, line 142):
+Goal Check 'bit_to_signed_positive2,ok' (file bitwise.i, line 144):
 Prove: true.
 
 ------------------------------------------------------------
 
-Goal Check 'bit_to_signed_negative,ok' (file bitwise.i, line 143):
+Goal Check 'bit_to_signed_negative,ok' (file bitwise.i, line 145):
 Prove: true.
 
 ------------------------------------------------------------
 
-Goal Check 'bit_to_signed_negative2,ok' (file bitwise.i, line 144):
+Goal Check 'bit_to_signed_negative2,ok' (file bitwise.i, line 146):
 Prove: true.
 
 ------------------------------------------------------------
 
-Goal Check 'bit_to_signed,ok' (file bitwise.i, line 145):
+Goal Check 'bit_to_signed,ok' (file bitwise.i, line 147):
 Prove: true.
 
 ------------------------------------------------------------
 
-Goal Check 'bit_to_signed2,ok' (file bitwise.i, line 146):
+Goal Check 'bit_to_signed2,ok' (file bitwise.i, line 148):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Check 'bit_lsl_lowest,ok' (file bitwise.i, line 150):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Check 'bit_lsl_higher_set,ok' (file bitwise.i, line 151):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Check 'bit_lsl_higher_unset,ok' (file bitwise.i, line 152):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Check 'bit_lsr_set,ok' (file bitwise.i, line 154):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Check 'bit_lsr_unset,ok' (file bitwise.i, line 155):
 Prove: true.
 
 ------------------------------------------------------------

src/plugins/wp/tests/wp_acsl/oracle_qualif/bitwise.res.oracle

@@ -2,7 +2,7 @@
 [kernel] Parsing bitwise.i (no preprocessing)
 [wp] Running WP plugin...
 [wp] Warning: Missing RTE guards
-[wp] 51 goals scheduled
+[wp] 56 goals scheduled
 [wp] [Qed] Goal typed_band_ensures : Valid
 [wp] [Qed] Goal typed_band_ensures_band0 : Valid
 [wp] [Qed] Goal typed_band_bit0_ensures_band1 : Valid
@@ -54,8 +54,13 @@
 [wp] [Qed] Goal typed_cast_uchar_check_bit_to_signed_negative2_ok : Valid
 [wp] [Qed] Goal typed_cast_uchar_check_bit_to_signed_ok : Valid
 [wp] [Qed] Goal typed_cast_uchar_check_bit_to_signed2_ok : Valid
-[wp] Proved goals:   51 / 51
-  Qed:            48 
+[wp] [Qed] Goal typed_cast_uchar_check_bit_lsl_lowest_ok : Valid
+[wp] [Qed] Goal typed_cast_uchar_check_bit_lsl_higher_set_ok : Valid
+[wp] [Qed] Goal typed_cast_uchar_check_bit_lsl_higher_unset_ok : Valid
+[wp] [Qed] Goal typed_cast_uchar_check_bit_lsr_set_ok : Valid
+[wp] [Qed] Goal typed_cast_uchar_check_bit_lsr_unset_ok : Valid
+[wp] Proved goals:   56 / 56
+  Qed:            53 
   Alt-Ergo:        3
 ------------------------------------------------------------
  Functions                 WP     Alt-Ergo  Total   Success
@@ -69,5 +74,5 @@
   band_bool                 1        1        2       100%
   bxor_bool                 1        1        2       100%
   lemma                     7        -        7       100%
-  cast_uchar               14        -       14       100%
+  cast_uchar               19        -       19       100%
 ------------------------------------------------------------