diff --git a/src/plugins/wp/Cint.ml b/src/plugins/wp/Cint.ml
index 7866b2d1414f6e61c4e9bfdb736e4146ba851655..866b9aa56bbde81fed16fd1205f11967c5c18991 100644
--- a/src/plugins/wp/Cint.ml
+++ b/src/plugins/wp/Cint.ml
@@ -590,6 +590,10 @@ let smp_shift zf = (* f(e1,0)~>e1, c2>0==>f(c1,c2)~>zf(c1,c2), c2>0==>f(0,c2)~>0
end
| _ -> raise Not_found
+(* -------------------------------------------------------------------------- *)
+(* --- Comparision with L-AND / L-OR / L-NOT --- *)
+(* -------------------------------------------------------------------------- *)
+
let smp_leq_with_land a b =
let es = match_fun f_land a in
let a1,_ = match_list_head match_positive_or_null_integer es in
@@ -649,6 +653,10 @@ let smp_eq_with_lnot a b = (* b1==~e <==> ~b1==e *)
let k1 = Integer.lognot b1 in
e_eq (e_zint k1) e
+(* -------------------------------------------------------------------------- *)
+(* --- Comparision with LSL / LSR --- *)
+(* -------------------------------------------------------------------------- *)
+
let two_power_k_minus1 k =
try Integer.pred (Integer.two_power k)
with Z.Overflow -> raise Not_found
@@ -715,28 +723,25 @@ let smp_eq_with_lsl a b =
let smp_leq_with_lsl a0 b0 = smp_cmp_with_lsl e_leq a0 b0
-let mk_cmp_with_lsr_cst cmp e x2 x1 =
- (* build (e&~((2**x2)-1)) cmp (x1<<x2) *)
- cmp
- (e_zint (Integer.shift_left x1 x2))
- (e_fun f_land [e_zint (Integer.lognot (two_power_k_minus1 x2));e])
-
-let smp_cmp_with_lsr cmp a0 b0 =
+let smp_eq_with_lsr a0 b0 =
try
let b1 = match_integer b0 in
let e,a2 = match_fun f_lsr a0 |> match_positive_or_null_integer_arg2 in
- (* (e>>a2) cmp b1 <==> (e&~((2**a2)-1)) cmp (b1<<a2)
+ (* (e>>a2) == b1 <==> (e&~((2**a2)-1)) == (b1<<a2)
That rule is similar to
- e/A2 cmp b2 <==> (e/A2)*A2 cmp b2*A2) with A2==2**a2
+ e/A2 == b2 <==> (e/A2)*A2 == b2*A2) with A2==2**a2
So, A2>0 and (e/A2)*A2 == e&~((2**a2)-1)
*)
- mk_cmp_with_lsr_cst cmp e a2 b1
+ (* build (e&~((2**a2)-1)) == (b1<<a2) *)
+ e_eq
+ (e_zint (Integer.shift_left b1 a2))
+ (e_fun f_land [e_zint (Integer.lognot (two_power_k_minus1 a2));e])
with Not_found ->
(* This rule takes into acount several cases.
One of them is
- (a>>p) cmp (b>>(n+p)) <==> (a&~((2**p)-1)) cmp (b>>n)&~((2**p)-1)
+ (a>>p) == (b>>(n+p)) <==> (a&~((2**p)-1)) == (b>>n)&~((2**p)-1)
That rule is similar to
- (a/P)cmp(b/(N*P)) <==> (a/P)*P cmp ((b/N)/P)*P
+ (a/P) == (b/(N*P)) <==> (a/P)*P == ((b/N)/P)*P
with P==2**p, N=2**n, q=p+n.
So, (a/P)*P==a&~((2**p)-1), b/N==b>>n, ((b/N)/P)*P==(b>>n)&~((2**p)-1) *)
let a,p = match_fun f_lsr a0 |> match_positive_or_null_integer_arg2 in
@@ -745,10 +750,7 @@ let smp_cmp_with_lsr cmp a0 b0 =
let a = if Integer.lt n p then e_fun f_lsr [a;e_zint (Z.sub p n)] else a in
let b = if Integer.lt n q then e_fun f_lsr [b;e_zint (Z.sub q n)] else b in
let m = F.e_zint (Integer.lognot (two_power_k_minus1 n)) in
- cmp (e_fun f_land [a;m]) (e_fun f_land [b;m])
-
-let smp_eq_with_lsr a0 b0 =
- smp_cmp_with_lsr e_eq a0 b0
+ e_eq (e_fun f_land [a;m]) (e_fun f_land [b;m])
let smp_leq_with_lsr a0 b0 =
try
@@ -758,17 +760,32 @@ let smp_leq_with_lsr a0 b0 =
(* b2>= 0 ==> (0<=(e>>b2) <==> 0<=e) (note: invalid for `e_eq`) *)
e_leq e_zero e
else
- let a1 = match_integer a0 in
let e,b2 = match_positive_or_null_integer_arg2 bs in
- (* a1 <= (e>>b2) <==> (e&~((2**b2)-1)) >= (a1<<b2) *)
- mk_cmp_with_lsr_cst (fun a b -> e_leq b a) e b2 a1
+ let k = Integer.two_power b2 in
+ let m = e_times k a0 in
+ if is_positive_or_null e then
+ (* e >= 0 ==> a0 <= (e / 2^b2) <==> (a0 * 2^b2) <= e *)
+ e_leq m e
+ else
+ let r = e_zint (Z.sub k Z.one) in
+ (* a1 <= (e / 2^b2) <==> a0 * 2^b2 - 2^b2 + 1) <= e *)
+ e_leq (e_sub m r) e
with Not_found ->
if b0 == e_zero then
let e,_ = match_fun f_lsr a0 |> match_positive_or_null_arg2 in
(* a2>= 0 ==> ((e>>a2)<=0 <==> e<=0) (note: invalid for `e_eq`) *)
e_leq e e_zero
else
- smp_cmp_with_lsr e_leq a0 b0
+ let e,a1 = match_fun f_lsr a0 |> match_positive_or_null_integer_arg2 in
+ let k = Integer.two_power a1 in
+ let m = e_times k b0 in
+ if is_negative e then
+ (* e <= 0 ==> (e / 2^a1) <= b0 <==> e <= (b0 * 2^a1) *)
+ e_leq e m
+ else
+ let r = e_zint (Z.sub k Z.one) in
+ (* (e / 2^b1) <= a1 <==> e <= (a1 * 2^b1 + 2^b1 - 1) *)
+ e_leq e (e_add m r)
(* Rewritting at export *)
let bitk_export k e = F.e_fun ~result:Logic.Bool f_bit_export [e;k]