diff --git a/Changelog b/Changelog
index 9d8f9ba13e5990263aaab2f766001a4d49fbaa17..a33504178e2ce8d98d26925b7b661617ad238a2a 100644
--- a/Changelog
+++ b/Changelog
@@ -21,6 +21,8 @@ Open Source Release <next-release>
distinguishing between for, while and dowhile loops.
-! Kernel [2019/01/03] Add statement attributes (sattr) to the AST. They
are not printed by default, use -kernel-msg-key printer:attrs
+-! Kernel [2019/01/03] Improved precision of integer abstract bitwise
+ operators.
################################
Open Source Release 18.0 (Argon)
diff --git a/src/kernel_services/abstract_interp/ival.ml b/src/kernel_services/abstract_interp/ival.ml
index c6aed4e7b02d279a199745b85bc87a71f96c9905..7a70c5e190c63bc239521e4d5aecdbdc4de4ef6f 100644
--- a/src/kernel_services/abstract_interp/ival.ml
+++ b/src/kernel_services/abstract_interp/ival.ml
@@ -795,7 +795,7 @@ let array_filter (f : Int.t -> bool) (a : Int.t array) : t =
let l = Array.length a in
let r = Array.make l Int.zero in
let j = ref 0 in
- for i = 0 to Array.length a - 1 do
+ for i = 0 to l - 1 do
let x = a.(i) in
if f x then begin
r.(!j) <- x;
@@ -804,11 +804,9 @@ let array_filter (f : Int.t -> bool) (a : Int.t array) : t =
done;
array_truncate r !j
-exception Empty
-
let array_map_reduce (f : 'a -> 'b) (g : 'b -> 'b -> 'b) (set : 'a array) : 'b =
if Array.length set <= 0 then
- raise Empty
+ raise Error_Bottom
else
let acc = ref (f set.(0)) in
for i = 1 to Array.length set - 1 do
@@ -2570,11 +2568,9 @@ end
(* --- Bit operators --- *)
-exception NoBackward
-
module type BitOperator =
sig
- (** Printable version of the operator *)
+ (* Printable version of the operator *)
val representation : string
(* forward is given here as the lifted function of some bit operator op
where op
@@ -2586,12 +2582,11 @@ sig
we don't know unless one of the operands is negative;
3. is not constant, otherwise nothing of all of this makes sense.
forward is defined as
- forward b1 b2 = { x1 op x2 | x1 \in b1, x2 \in b2 }
- *)
+ forward b1 b2 = { x1 op x2 | x1 \in b1, x2 \in b2 } *)
val forward : bit_value -> bit_value -> bit_value
- (** backward_off b = { x | \exist y \in b . x op y = y op x = 1 } *)
+ (* backward_off b = { x | \exist y \in b . x op y = y op x = 1 } *)
val backward_off : bit_value -> bit_value
- (** backward_on b = { x | \exist y \in b . x op y = y op x = 0 } *)
+ (* backward_on b = { x | \exist y \in b . x op y = y op x = 0 } *)
val backward_on : bit_value -> bit_value
end
@@ -2610,7 +2605,7 @@ struct
| On -> Off
let backward_on = function
- | Off -> raise NoBackward
+ | Off -> assert false
| (On | Both) -> On
end
@@ -2625,7 +2620,7 @@ struct
| Both -> if v2 = On then On else Both
let backward_off = function
- | On -> raise NoBackward
+ | On -> assert false
| (Off | Both) -> Off
let backward_on = function
@@ -2651,34 +2646,10 @@ end
(* --- Bit extraction and mutation --- *)
-module Int =
-struct
- include Integer
-
- let significant_bits (i : t) : int =
- (* shift right until nothing changes *)
- let rec count i acc =
- let new_i = shift_right i one in
- if equal i new_i
- then acc
- else count new_i (acc + 1)
- in
- count i 0
-
- let biggest_power_of_two_divider (i : t) : int =
- let rec aux p acc =
- if equal (logand i p) zero
- then aux (shift_left p one) (acc + 1)
- else acc
- in
- aux Int.one 0
-end
-
let significant_bits (v : t) : int option =
match min_and_max v with
| None, _ | _, None -> None
- | Some l, Some u ->
- Some (max (Int.significant_bits l) (Int.significant_bits u))
+ | Some l, Some u -> Some (max (Z.numbits l) (Z.numbits u))
let extract_sign (v : t) : bit_value =
match min_and_max v with
@@ -2686,19 +2657,15 @@ let extract_sign (v : t) : bit_value =
| Some l, _ when Int.(ge l zero) -> Off
| _, _ -> Both
-let extract_bit (v : t) (i : int) : bit_value =
- let power = Int.(two_power_of_int i) in
- let bit_value x =
- if Int.(is_zero (logand power x)) then Off else On
- in
+let extract_bit (i : int) (v : t) : bit_value =
+ let bit_value x = if Z.testbit x i then On else Off in
match v with
| Float _ -> Both
- | Set s ->
- array_map_reduce bit_value Bit.union s
+ | Set s -> array_map_reduce bit_value Bit.union s
| Top (None, _, _r, _m) | Top (_, None, _r, _m) -> Both
| Top (Some l, Some u, _r, _m) ->
(* It does not take modulo into account *)
- if Int.(ge (sub u power)) l (* u - l >= mask *)
+ if Int.(ge (sub u l) (two_power_of_int i)) (* u - l >= mask *)
then Both
else Bit.union (bit_value l) (bit_value u)
@@ -2724,25 +2691,22 @@ let reduce_sign (v : t) (b : bit_value) : t =
inject_top l u r modu
end
-let reduce_bit (v : t) (i : int) (b : bit_value) : t =
- let power = Int.(two_power_of_int i) in (* 001000 *)
- let mask = Int.(pred (two_power_of_int (i+1))) in (* 001111 *)
- let bit_value (x : Int.t) =
- if Int.(is_zero (logand power x)) then Off else On
- in
+let reduce_bit (i : int) (v : t) (b : bit_value) : t =
+ let bit_value x = if Z.testbit x i then On else Off in
if b = Both
then v
else match v with
| Float _ -> v
- | Set s ->
- array_filter (fun x -> bit_value x = b) s
+ | Set s -> array_filter (fun x -> bit_value x = b) s
| Top (l, u, r, modu) ->
+ let power = Int.(two_power_of_int i) in (* 001000 *)
+ let mask = Int.(pred (two_power_of_int (i+1))) in (* 001111 *)
(* Reduce bounds to the nearest satisfying bound *)
let l' = match l with
| Some l when bit_value l <> b ->
let min = match b with
| On -> Int.(logor (logand l (lognot mask)) power) (* ll1000 *)
- | Off -> Int.(succ (logor l mask)) (* ll0000 *)
+ | Off -> Int.(succ (logor l mask)) (* ll1111 + 1 *)
| Both -> assert false
in
Some (Int.round_up_to_r ~min ~r ~modu)
@@ -2750,8 +2714,8 @@ let reduce_bit (v : t) (i : int) (b : bit_value) : t =
and u' = match u with
| Some u when bit_value u <> b ->
let max = match b with
- | On -> Int.(pred (logand u (lognot mask))) (* ll1111 *)
- | Off -> Int.(logand (logor u mask) (lognot power)) (* ll0111 *)
+ | On -> Int.(pred (logand u (lognot mask))) (* uu0000 - 1 *)
+ | Off -> Int.(logand (logor u mask) (lognot power)) (* uu0111 *)
| Both -> assert false
in
Some (Int.round_down_to_r ~max ~r ~modu)
@@ -2759,238 +2723,174 @@ let reduce_bit (v : t) (i : int) (b : bit_value) : t =
in
inject_top l' u' r modu
+type bit = Sign | Bit of int
-(* --- Bit masks --- *)
-
-(** bit masks are composed of an array of significant bit values where index 0
- represents the lowest bit, and a single bit_value to represent the possible
- leading bits. *)
-type bit_mask = bit_value array * bit_value
+let extract_bit = function
+ | Sign -> extract_sign
+ | Bit i -> extract_bit i
-let int_to_bit_array n (x : Int.t) =
- let a = Array.make n On in
- let p = ref Int.one in
- for i = 0 to n-1 do
- if Int.(equal (logand x !p) zero) then
- a.(i) <- Off;
- p := Int.(shift_left !p one)
- done;
- a
-
-(** Compute a mask only precise for low bits, overapproximating the high ones.
- More precisely, bit values are computed until an uncertainty appears
- in the mask *)
-let low_bit_mask (v : t) =
- match v with
- | Set [| |] -> raise Error_Bottom
- | Set [| x |] -> (* singleton : build a full mask *)
- let n = Int.significant_bits x in
- int_to_bit_array n x, if Int.(ge x zero) then Off else On
- | _ ->
- let _,_,r,modu = min_max_r_mod v in (* requires cardinal > 1 *)
- (* Find how much modu can be divided by two *)
- let n = Int.biggest_power_of_two_divider modu in
- (* Recompute rest *)
- let r = Int.(logand (sub (two_power_of_int n) one) r) in
- int_to_bit_array n r, Both
-
-let combine_masks (op : bit_value -> bit_value -> bit_value)
- (b1,s1 : bit_mask) (b2,s2 : bit_mask) : bit_mask =
- let n = max (Array.length b1) (Array.length b2) in
- let r = Array.make n Both in
- for i = 0 to n-1 do
- let b1 = try b1.(i) with _ -> s1
- and b2 = try b2.(i) with _ -> s2
- in
- r.(i) <- op b1 b2
- done;
- r, op s1 s2
-
-let mask_to_r_modu (b,_s : bit_mask) : Int.t * Int.t =
- let n = Array.length b in
- let r = ref Int.zero (* current rest *)
- and p = ref Int.one (* current bit *) in
- begin try
- for i = 0 to n-1 do
- begin match b.(i) with
- | On -> r := Int.(logor !r !p)
- | Off -> ()
- | Both -> raise Exit
- end;
- p := Int.(shift_left !p one)
- done;
- with Exit -> ()
- end;
- !r, !p
+let set_bit_on ~size bit =
+ let mask = match bit with
+ | Sign -> Int.(neg (two_power_of_int size))
+ | Bit i -> Int.(two_power_of_int i)
+ in
+ fun v -> Int.logor mask v
+let reduce_bit = function
+ | Sign -> reduce_sign
+ | Bit i -> reduce_bit i
(* --- Bitwise binary operators --- *)
module BitwiseOperator (Op : BitOperator) =
struct
- include Op
-
- exception Result_does_not_fit_small_sets
-
let backward (b : bit_value) = function
- | On -> backward_on b
- | Off -> backward_off b
+ | On -> Op.backward_on b
+ | Off -> Op.backward_off b
| Both -> assert false
+ (** Bit masks are composed of an array of significant bit values where index 0
+ represents the lowest bit, and a single bit_value to represent the
+ possible leading bits. *)
+ type bit_mask = bit_value array * bit_value
+
+ (* Converts an integer [x] into a bit array of size [n]. *)
+ let int_to_bit_array n (x : Int.t) =
+ let make i = if Z.testbit x i then On else Off in
+ Array.init n make
+
+ (* Computes a bit_mask for the lowest bits of an ival, using the modulo
+ information for non singleton values. *)
+ let low_bit_mask : t -> bit_mask = function
+ | Set [| |] -> raise Error_Bottom
+ | Set [| x |] -> (* singleton : build a full mask *)
+ let n = Z.numbits x in
+ int_to_bit_array n x, if Int.(ge x zero) then Off else On
+ | v ->
+ let _,_,r,modu = min_max_r_mod v in (* requires cardinal > 1 *)
+ (* Find how much [modu] can be divided by two. *)
+ let n = Z.trailing_zeros modu in
+ int_to_bit_array n r, Both
+
+ (* Computes a remainder and modulo for the result of [v1 op v2]. *)
+ let compute_modulo v1 v2 =
+ let b1, s1 = low_bit_mask v1
+ and b2, s2 = low_bit_mask v2 in
+ let size = max (Array.length b1) (Array.length b2) in
+ (* Sets the [i] nth bits of [rem] until an uncertainty appears. *)
+ let rec step i rem =
+ let b1 = try b1.(i) with _ -> s1
+ and b2 = try b2.(i) with _ -> s2 in
+ let b = Op.forward b1 b2 in
+ if i >= size || b = Both
+ then rem, Int.two_power_of_int i
+ else
+ (* [rem] starts at 0, so we only need to turn on the 1 bits. *)
+ let rem = if b = On then set_bit_on ~size (Bit i) rem else rem in
+ step (i+1) rem
+ in
+ step 0 Int.zero
+
(* The number of bits on which the result should be significant *)
- let result_size (v1 : t) (v2 : t)
- ?(s1 : bit_value = extract_sign v1)
- ?(s2 : bit_value = extract_sign v2)
- ()
- : int option =
+ let result_size (v1 : t) (v2 : t) : int option =
let n1 = significant_bits v1 and n2 = significant_bits v2 in
- let n1_greater =
+ let n1_greater =
match n1, n2 with
+ | None, _ -> true
| _, None -> false
- | Some n1, Some n2 when n1 <= n2 -> false
- | _ -> true
+ | Some n1, Some n2 -> n1 >= n2
in
(* whether n1 or n2 is greater, look if the sign bit oped with anything is
not constant. If it is constant, then the highest bits are irrelevant. *)
- if n1_greater then
- if forward Both s2 = Both then n1 else n2
- else
- if forward s1 Both = Both then n2 else n1
+ if n1_greater
+ then if Op.forward Both (extract_sign v2) = Both then n1 else n2
+ else if Op.forward (extract_sign v1) Both = Both then n2 else n1
+ exception Do_not_fit_small_sets
(* Try to build a small set.
It is basically enumerating the possible results, by choosing the possible
- bits from left to right. This function aborts if we ever exceed the small
+ bits from left to right. This function aborts if it ever exceeds the small
set size. The algorithm is probably not complete, as it is not always
possible to reduce the operands leading to a result (without an
exponential cost) meaning that sometimes small sets can be obtained but
- the algorithm will fail to find them.
- *)
- let compute_small_set (v1 : t) (v2 : t) (r : Int.t) (modu : Int.t) =
- let s1 = extract_sign v1 and s2 = extract_sign v2 in
- match result_size v1 v2 ~s1 ~s2 () with
- | None -> raise Result_does_not_fit_small_sets
- | Some n ->
- let acc = [] in (* List of possible results, with the operands leading
- to these results *)
- let s = forward s1 s2 in
- (* Either the result is positive *)
- let acc =
- if s <> On then
- let v1 = reduce_sign v1 (backward_off s2)
- and v2 = reduce_sign v2 (backward_off s1) in
- (r, v1, v2) :: acc
- else acc
- in
- (* Or negative *)
- let acc =
- if s <> Off then
- let v1 = reduce_sign v1 (backward_on s2)
- and v2 = reduce_sign v2 (backward_on s1) in
- (Int.(logor r (neg (two_power_of_int n))), v1, v2) :: acc
- else
- acc
- in
- let rec step acc i =
- if List.length acc > !small_cardinal then
- raise Result_does_not_fit_small_sets;
- if i < 0 then acc
- else
- let mask = Int.(two_power_of_int i) in
- let set_one_bit acc (r,v1,v2) =
- let b1 = extract_bit v1 i and b2 = extract_bit v2 i in
- let b = forward b1 b2 in
- (* Either the bit is on *)
- let acc =
- if b <> Off then
- let v1 = reduce_bit v1 i (backward_on b2)
- and v2 = reduce_bit v2 i (backward_on b1) in
- (Int.logor mask r, v1, v2) :: acc
- else acc
- in
- (* Or off *)
- let acc =
- if b <> On then
- let v1 = reduce_bit v1 i (backward_off b2)
- and v2 = reduce_bit v2 i (backward_off b1) in
- (r, v1, v2) :: acc
- else acc
- in
- acc
- in
- if mask < modu
- then acc
- else step (List.fold_left set_one_bit [] acc) (i-1)
- in
- let acc = step acc (n-1) in
- let o = List.fold_left (fun o (r,_,_) -> O.add r o) O.empty acc in
- share_set o (O.cardinal o)
+ the algorithm will fail to find them. *)
+ let compute_small_set ~size (v1 : t) (v2 : t) (r : Int.t) (modu : Int.t) =
+ let set_bit i acc (r, v1, v2) =
+ let b1 = extract_bit i v1
+ and b2 = extract_bit i v2 in
+ match Op.forward b1 b2 with
+ | On -> (set_bit_on ~size i r, v1, v2) :: acc
+ | Off -> (r, v1, v2) :: acc
+ | Both ->
+ let v1_off = reduce_bit i v1 (Op.backward_off b2)
+ and v2_off = reduce_bit i v2 (Op.backward_off b1) in
+ let v1_on = reduce_bit i v1 (Op.backward_on b2)
+ and v2_on = reduce_bit i v2 (Op.backward_on b1) in
+ (set_bit_on ~size i r, v1_on, v2_on) :: (r, v1_off, v2_off) :: acc
+ in
+ let acc = ref (set_bit Sign [] (r, v1, v2)) in
+ for i = size - 1 downto Z.numbits modu - 1 do
+ acc := List.fold_left (set_bit (Bit i)) [] !acc;
+ if List.length !acc > !small_cardinal then raise Do_not_fit_small_sets
+ done;
+ let o = List.fold_left (fun o (r,_,_) -> O.add r o) O.empty !acc in
+ share_set o (O.cardinal o)
(* If lower is true (resp. false), compute the lower (resp. upper) bound of
- the result interval when applying op to v1 and v2.
- We iterate from left to right. We keep track of an ival for each operand
- such that, by applying the operator on the two ivals, we can find the
- actual bound of the operation.
- This function should be exact when the operands are small sets or tops
+ the result interval when applying the bitwise operator to [v1] and [v2].
+ [size] is the number of bits of the result.
+ This function should be exact when the operands are small sets or tops
with modulo 1. Otherwise, it is an overapproximation of the bound. *)
- let compute_bound (v1 : t) (v2 : t) (lower : bool) =
- (* What is the sign of the result *)
- let s1 = extract_sign v1 and s2 = extract_sign v2 in
- let s,s1,v1,s2,v2 =
- match forward s1 s2 with
- | (On | Off) as s -> s,s1,v1,s2,v2 (* constant sign *)
- | Both -> (* choose the best sign *)
- let s = if lower then On else Off in
- let s1 = backward s2 s and s2 = backward s1 s in
- let v1 = reduce_sign v1 s1 and v2 = reduce_sign v2 s2 in
- s,s1,v1,s2,v2
- in
- (* Is the result bounded ? *)
- match result_size v1 v2 ~s1 ~s2 () with
- | None ->
- (* Unbounded result *)
- None
- | Some n ->
- (* The result is bounded: iterate from the rightmost significant bit *)
- let rec step r v1 v2 i =
- if i < 0 then r
- else
- let mask = Int.(two_power_of_int i) in
- let b1 = extract_bit v1 i and b2 = extract_bit v2 i in
- let b, v1, v2 = match forward b1 b2 with
- | (On | Off) as b -> b,v1,v2 (* constant bit *)
- | Both -> (* choose the best bit *)
- let b = if lower then Off else On in
- let b1 = backward b2 b and b2 = backward b1 b in
- let v1 = reduce_bit v1 i b1 and v2 = reduce_bit v2 i b2 in
- b, v1, v2
+ let compute_bound ~size v1 v2 lower =
+ (* Sets the [i]-nth bit of the currently computed bound [r] of [v1 op v2].
+ If possible, reduces [v1] and [v2] accordingly. *)
+ let set_bit i (r, v1, v2) =
+ let b1 = extract_bit i v1
+ and b2 = extract_bit i v2 in
+ let b, v1, v2 =
+ match Op.forward b1 b2 with
+ | On | Off as b -> b, v1, v2 (* Constant bit, no reduction. *)
+ | Both ->
+ (* Choose the best bit for the searched bound, and reduces [v1] and
+ [v2] accordingly. *)
+ let b = match i with
+ | Sign -> if lower then On else Off
+ | Bit _ -> if lower then Off else On
in
- let r = match b with
- | On -> Int.logor mask r
- | Off -> r
- | Both -> assert false
- in
- step r v1 v2 (i-1)
- in
- let r = match s with
- | On -> Int.(neg (two_power_of_int n))
- | Off -> Int.zero
- | Both -> assert false
+ let v1 = reduce_bit i v1 (backward b2 b)
+ and v2 = reduce_bit i v2 (backward b1 b) in
+ b, v1, v2
in
- Some (step r v1 v2 (n - 1))
+ (* Only sets 1 bit, as [r] is 0 at the beginning. *)
+ let r = if b = On then set_bit_on ~size i r else r in
+ r, v1, v2
+ in
+ (* The result is 0 at the beginning, and [set_bit] turns on the 1 bits. *)
+ let r = ref (Int.zero, v1, v2) in
+ (* Sets the sign bit, and then the bits from size to 0. *)
+ r := set_bit Sign !r;
+ for i = (size - 1) downto 0 do
+ r := set_bit (Bit i) !r;
+ done;
+ let bound, _v1, _v2 = !r in
+ bound
let bitwise_forward (v1 : t) (v2 : t) : t =
try
- let mask1 = low_bit_mask v1
- and mask2 = low_bit_mask v2 in
- let r, modu = mask_to_r_modu (combine_masks forward mask1 mask2) in
- try
- compute_small_set v1 v2 r modu
- with Result_does_not_fit_small_sets ->
- let min = compute_bound v1 v2 true
- and max = compute_bound v1 v2 false in
- inject_interval min max r modu
+ let r, modu = compute_modulo v1 v2 in
+ match result_size v1 v2 with
+ | None ->
+ (* We could do better here, as one of the bound may be finite. However,
+ this case should occur rarely or not at all. *)
+ inject_interval None None r modu
+ | Some size ->
+ try compute_small_set ~size v1 v2 r modu
+ with Do_not_fit_small_sets ->
+ let min = compute_bound ~size v1 v2 true
+ and max = compute_bound ~size v1 v2 false in
+ inject_interval (Some min) (Some max) r modu
with Error_Bottom -> bottom
end
diff --git a/src/plugins/value/values/cvalue_forward.ml b/src/plugins/value/values/cvalue_forward.ml
index d417304af105379bcdf6c584f2aa2c9b1d84e4dd..c1a6a73c03d3e1033a252f44239ced56b307d191 100644
--- a/src/plugins/value/values/cvalue_forward.ml
+++ b/src/plugins/value/values/cvalue_forward.ml
@@ -381,7 +381,7 @@ let forward_binop_float fkind ev1 op ev2 =
This is left to the caller *)
let forward_uneg v t =
try
- match Cil. unrollType t with
+ match Cil.unrollType t with
| TFloat _ ->
let v = V.project_float v in
V.inject_ival (Ival.inject_float (Fval.neg v))
diff --git a/tests/idct/diff_bitwise b/tests/idct/diff_bitwise
index 19f21ca2757655aeae5469fe7ed060bf2bc7750b..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 100644
--- a/tests/idct/diff_bitwise
+++ b/tests/idct/diff_bitwise
@@ -1,5 +0,0 @@
-diff tests/idct/oracle/ieee_1180_1990.res.oracle tests/idct/oracle_bitwise/ieee_1180_1990.res.oracle
-920c920
-< i ∈ [0..2147483646]
----
-> i ∈ [0..2147483646],0%2
diff --git a/tests/value/bitwise.i b/tests/value/bitwise.i
index 765c7bcb82a6d3e836c7cb5991573b88f3993882..7803ea7f36d1538b8c338aa8002c10eebd591e1c 100644
--- a/tests/value/bitwise.i
+++ b/tests/value/bitwise.i
@@ -1,6 +1,80 @@
+/* run.config*
+ STDOPT: +"-big-ints-hex 256"
+*/
+
+/*@ assigns \result \from min, max;
+ ensures min <= \result <= max ;
+ */
+int Frama_C_interval(int min, int max);
+
+
volatile long v;
-
-void main_and_or_rel(void)
+volatile unsigned char input[3];
+
+
+extern unsigned short s;
+
+void test1(void) {
+ int or1, or2, or3, or4, or5;
+ int and1, and2, and3, and4, xor1, xor2;
+ unsigned int uand1, uand2, uand3, uand4, uand5;
+ int a,b,c,d,e;
+
+ a = Frama_C_interval(3,17);
+ b = Frama_C_interval(-3,17);
+ c = Frama_C_interval(13,27);
+ or1 = a | b;
+ or2 = a | c;
+ or3 = b | c;
+
+ and1 = a & b;
+ and2 = a & c;
+ and3 = b & c;
+
+ uand4 = 0xFFFFFFF8U & (unsigned int) c;
+
+ xor1 = a ^ a;
+ xor2 = a ^ b;
+
+ unsigned i1 = s * 2;
+ unsigned i2 = s * 4;
+ unsigned v1 = i1 & i2;
+ unsigned v2 = i1 | i2;
+
+ unsigned mask07 = (16 * s + 13) & 0x7;
+ unsigned mask0f = (16 * s + 13) & 0xF;
+ unsigned mask1f = (16 * s + 13) & 0x1F;
+}
+
+void test2(void) {
+ int x = Frama_C_interval(62,110) & ~(7);
+}
+
+void test3(void) {
+ int x = (input[0] & 0x10 ? -1^255 : 0) | input[1];
+ int y = (input[0] & 0x20 ? -1^255 : 0) | input[2];
+}
+
+int test4(void)
+{
+ unsigned something = v;
+ //@ slevel 2;
+ //@ assert something >= 0x80000000 || something < 0x80000000;
+ unsigned topBitOnly = something & 0x80000000;
+ Frama_C_show_each_1(something,topBitOnly);
+ something ^= topBitOnly;
+ Frama_C_show_each_2(something,something & 0x80000000,topBitOnly);
+ if (something & 0x80000000) {
+ Frama_C_show_each_true(something);
+ return 0;
+ }
+ else {
+ Frama_C_show_each_false(something);
+ return 1;
+ }
+}
+
+void and_or_rel(void)
{
long x, r1, r2, r3;
@@ -19,13 +93,13 @@ void main_and_or_rel(void)
}
-void main_bitwise() {
+void double_neg() {
unsigned int i = 5;
unsigned int j = ~i;
int k = ~(int)i;
}
-void main_bug1()
+void bug1()
{
unsigned char msb = 3 << 1;
unsigned char lsb = 3;
@@ -35,22 +109,22 @@ void main_bug1()
par = (unsigned char)(((int)par & 0x0F) ^ ((int)par >> 4));
}
-void main_bug2() {
+void bug2() {
int t = v ? 1 : 2;
if ((t & 7) == 1) { Frama_C_show_each_then(); } else { Frama_C_show_each_else(); }
}
/* See issue Value/Value#82 on the bitwise domain. */
-void main_bug3 () {
+void bug3 () {
unsigned long l_1180 = 10022045811482781039u;
unsigned long foo = ~ (l_1180 ^ (unsigned long)(l_1180 != 0UL));
- Frama_C_dump_each();
+ Frama_C_show_each(l_1180, foo);
foo ^= 0;
}
/* Due to signedness mismatches, the bitwise domain incorrectly returned
Bottom on one of the branches. */
-void main_bug4() {
+void bug4() {
int g_2 = v ? -1 : 0;
short tmp = -0x1578;
if ((g_2 | (int)tmp) & 1) {
@@ -60,11 +134,15 @@ void main_bug4() {
}
}
-void main() {
- main_and_or_rel();
- main_bitwise();
- main_bug1();
- main_bug2();
- main_bug3();
- main_bug4();
+void main(void) {
+ test1();
+ test2();
+ test3();
+ test4();
+ and_or_rel();
+ double_neg();
+ bug1();
+ bug2();
+ bug3();
+ bug4();
}
diff --git a/tests/value/bitwise_or.c b/tests/value/bitwise_or.c
deleted file mode 100644
index 0a89e7c301047dddb70d2945444470911269d4e7..0000000000000000000000000000000000000000
--- a/tests/value/bitwise_or.c
+++ /dev/null
@@ -1,56 +0,0 @@
-/* run.config*
- OPT: -no-autoload-plugins -load-module inout,eva -big-ints-hex 256 -eva @VALUECONFIG@ -journal-disable
-*/
-#include "__fc_builtin.h"
-
-extern unsigned short s;
-
-void f1(void) {
- int or1, or2, or3, or4, or5;
- int and1, and2, and3, and4, xor1, xor2;
- unsigned int uand1, uand2, uand3, uand4, uand5;
- int a,b,c,d,e;
-
- a = Frama_C_interval(3,17);
- b = Frama_C_interval(-3,17);
- c = Frama_C_interval(13,27);
- or1 = a | b;
- or2 = a | c;
- or3 = b | c;
-
- and1 = a & b;
- and2 = a & c;
- and3 = b & c;
-
- uand4 = 0xFFFFFFF8U & (unsigned int) c;
-
- xor1 = a ^ a;
- xor2 = a ^ b;
-
- unsigned i1 = s * 2;
- unsigned i2 = s * 4;
- unsigned v1 = i1 & i2;
- unsigned v2 = i1 | i2;
-
- unsigned mask07 = (16 * s + 13) & 0x7;
- unsigned mask0f = (16 * s + 13) & 0xF;
- unsigned mask1f = (16 * s + 13) & 0x1F;
-}
-
-void f2(void) {
- int x = Frama_C_interval(62,110) & ~(7);
-}
-
-volatile unsigned char t[3];
-
-void f3(void) {
- int x = (t[0] & 0x10 ? -1^255 : 0) | t[1];
- int y = (t[0] & 0x20 ? -1^255 : 0) | t[2];
-}
-
-void main(void) {
- f1();
- f2();
- f3();
-}
-
diff --git a/tests/value/diff_bitwise b/tests/value/diff_bitwise
index 29219259f932f06bb3ee7cd0bea4b6ccec489a42..be860471315a12c865ad8b280eee88bf57f61cda 100644
--- a/tests/value/diff_bitwise
+++ b/tests/value/diff_bitwise
@@ -9,35 +9,20 @@ diff tests/value/oracle/addition.res.oracle tests/value/oracle_bitwise/addition.
> {{ garbled mix of &{p1} (origin: Misaligned {tests/value/addition.i:52}) }}
130a130
> {{ garbled mix of &{p2} (origin: Misaligned {tests/value/addition.i:56}) }}
-166,169c166,167
+166,168c166
< p10 ∈
< {{ garbled mix of &{p1}
< (origin: Arithmetic {tests/value/addition.i:52}) }}
-< p11 ∈ [-2147483648..0]
---
> p10 ∈ {{ garbled mix of &{p1} }}
-> p11 ∈ [-2147483648..0],0%4
358a357
> {{ garbled mix of &{p1} (origin: Misaligned {tests/value/addition.i:52}) }}
-397,400c396,397
+397,399c396
< p10 ∈
< {{ garbled mix of &{p1}
< (origin: Arithmetic {tests/value/addition.i:52}) }}
-< p11 ∈ [-2147483648..0]
---
> p10 ∈ {{ garbled mix of &{p1} }}
-> p11 ∈ [-2147483648..0],0%4
-diff tests/value/oracle/bitwise_or.res.oracle tests/value/oracle_bitwise/bitwise_or.res.oracle
-57c57
-< uand4 ∈ [8..24]
----
-> uand4 ∈ {8; 16; 24}
-63,64c63,64
-< v1 ∈ [0..0x1FFFE],0%2
-< v2 ∈ [0..0x3FFFF]
----
-> v1 ∈ [0..0x1FFFC],0%4
-> v2 ∈ [0..0x3FFFE],0%2
diff tests/value/oracle/bitwise_pointer.res.oracle tests/value/oracle_bitwise/bitwise_pointer.res.oracle
32,34c32
< [eva] tests/value/bitwise_pointer.i:18:
@@ -51,15 +36,6 @@ diff tests/value/oracle/bitwise_pointer.res.oracle tests/value/oracle_bitwise/bi
< The imprecision originates from Arithmetic {tests/value/bitwise_pointer.i:22}
---
> [eva] tests/value/bitwise_pointer.i:22: Assigning imprecise value to p1.
-diff tests/value/oracle/cast.res.oracle tests/value/oracle_bitwise/cast.res.oracle
-71c71
-< G ∈ [0..12]
----
-> G ∈ [2..12]
-89c89
-< G ∈ [0..12]
----
-> G ∈ [2..12]
diff tests/value/oracle/logic_ptr_cast.res.oracle tests/value/oracle_bitwise/logic_ptr_cast.res.oracle
8,10c8
< [eva] tests/value/logic_ptr_cast.i:8:
diff --git a/tests/value/oracle/bitwise.res.oracle b/tests/value/oracle/bitwise.res.oracle
index 029bed271752f5eb1cd0c396981f09d85eee18df..29d9bbe232251a10bb728dfe3c9ea3e635cb8fc0 100644
--- a/tests/value/oracle/bitwise.res.oracle
+++ b/tests/value/oracle/bitwise.res.oracle
@@ -4,126 +4,226 @@
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
v ∈ [--..--]
-[eva] computing for function main_and_or_rel <- main.
- Called from tests/value/bitwise.i:64.
-[eva:alarm] tests/value/bitwise.i:13: Warning: assertion got status unknown.
-[eva] Recording results for main_and_or_rel
-[eva] Done for function main_and_or_rel
-[eva] computing for function main_bitwise <- main.
- Called from tests/value/bitwise.i:65.
-[eva] Recording results for main_bitwise
-[eva] Done for function main_bitwise
-[eva] computing for function main_bug1 <- main.
- Called from tests/value/bitwise.i:66.
-[eva] Recording results for main_bug1
-[eva] Done for function main_bug1
-[eva] computing for function main_bug2 <- main.
- Called from tests/value/bitwise.i:67.
-[eva] tests/value/bitwise.i:40: Frama_C_show_each_then:
-[eva] tests/value/bitwise.i:40: Frama_C_show_each_else:
-[eva] Recording results for main_bug2
-[eva] Done for function main_bug2
-[eva] computing for function main_bug3 <- main.
- Called from tests/value/bitwise.i:68.
-[eva] tests/value/bitwise.i:47:
- Frama_C_dump_each:
- # Cvalue domain:
- v ∈ [--..--]
- l_1180 ∈ {69166447}
- foo ∈ {4225800849}
- ==END OF DUMP==
-[eva] Recording results for main_bug3
-[eva] Done for function main_bug3
-[eva] computing for function main_bug4 <- main.
- Called from tests/value/bitwise.i:69.
-[eva] tests/value/bitwise.i:57: Frama_C_show_each_then:
-[eva] tests/value/bitwise.i:59: Frama_C_show_each_else:
-[eva] Recording results for main_bug4
-[eva] Done for function main_bug4
+ input[0..2] ∈ [--..--]
+ s ∈ [--..--]
+[eva] computing for function test1 <- main.
+ Called from tests/value/bitwise.i:138.
+[eva] computing for function Frama_C_interval <- test1 <- main.
+ Called from tests/value/bitwise.i:23.
+[eva] using specification for function Frama_C_interval
+[eva] Done for function Frama_C_interval
+[eva] computing for function Frama_C_interval <- test1 <- main.
+ Called from tests/value/bitwise.i:24.
+[eva] Done for function Frama_C_interval
+[eva] computing for function Frama_C_interval <- test1 <- main.
+ Called from tests/value/bitwise.i:25.
+[eva] Done for function Frama_C_interval
+[eva] Recording results for test1
+[eva] Done for function test1
+[eva] computing for function test2 <- main.
+ Called from tests/value/bitwise.i:139.
+[eva] computing for function Frama_C_interval <- test2 <- main.
+ Called from tests/value/bitwise.i:50.
+[eva] Done for function Frama_C_interval
+[eva] Recording results for test2
+[eva] Done for function test2
+[eva] computing for function test3 <- main.
+ Called from tests/value/bitwise.i:140.
+[eva] Recording results for test3
+[eva] Done for function test3
+[eva] computing for function test4 <- main.
+ Called from tests/value/bitwise.i:141.
+[eva] tests/value/bitwise.i:62: assertion got status valid.
+[eva] tests/value/bitwise.i:64: Frama_C_show_each_1: [0..0x7FFFFFFF], {0}
+[eva] tests/value/bitwise.i:64:
+ Frama_C_show_each_1: [0x80000000..0xFFFFFFFF], {0x80000000}
+[eva] tests/value/bitwise.i:66: Frama_C_show_each_2: [0..0x7FFFFFFF], {0}, {0}
+[eva] tests/value/bitwise.i:66:
+ Frama_C_show_each_2: [0..0x7FFFFFFF], {0}, {0x80000000}
+[eva] tests/value/bitwise.i:72: Frama_C_show_each_false: [0..0x7FFFFFFF]
+[eva] tests/value/bitwise.i:72: Frama_C_show_each_false: [0..0x7FFFFFFF]
+[eva] Recording results for test4
+[eva] Done for function test4
+[eva] computing for function and_or_rel <- main.
+ Called from tests/value/bitwise.i:142.
+[eva:alarm] tests/value/bitwise.i:87: Warning: assertion got status unknown.
+[eva] Recording results for and_or_rel
+[eva] Done for function and_or_rel
+[eva] computing for function double_neg <- main.
+ Called from tests/value/bitwise.i:143.
+[eva] Recording results for double_neg
+[eva] Done for function double_neg
+[eva] computing for function bug1 <- main.
+ Called from tests/value/bitwise.i:144.
+[eva] Recording results for bug1
+[eva] Done for function bug1
+[eva] computing for function bug2 <- main.
+ Called from tests/value/bitwise.i:145.
+[eva] tests/value/bitwise.i:114: Frama_C_show_each_then:
+[eva] tests/value/bitwise.i:114: Frama_C_show_each_else:
+[eva] Recording results for bug2
+[eva] Done for function bug2
+[eva] computing for function bug3 <- main.
+ Called from tests/value/bitwise.i:146.
+[eva] tests/value/bitwise.i:121: Frama_C_show_each: {0x41F656F}, {0xFBE09A91}
+[eva] Recording results for bug3
+[eva] Done for function bug3
+[eva] computing for function bug4 <- main.
+ Called from tests/value/bitwise.i:147.
+[eva] tests/value/bitwise.i:131: Frama_C_show_each_then:
+[eva] tests/value/bitwise.i:133: Frama_C_show_each_else:
+[eva] Recording results for bug4
+[eva] Done for function bug4
[eva] Recording results for main
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
-[eva:final-states] Values at end of function main_and_or_rel:
+[eva:final-states] Values at end of function and_or_rel:
x ∈ [20..40]
r1 ∈ [17..63] or UNINITIALIZED
r2 ∈ [20..40] or UNINITIALIZED
r3 ∈ [24..37] or UNINITIALIZED
-[eva:final-states] Values at end of function main_bitwise:
- i ∈ {5}
- j ∈ {4294967290}
- k ∈ {-6}
-[eva:final-states] Values at end of function main_bug1:
+[eva:final-states] Values at end of function bug1:
msb ∈ {6}
lsb ∈ {3}
par ∈ {5}
p1 ∈ {5}
p2 ∈ {0}
-[eva:final-states] Values at end of function main_bug2:
+[eva:final-states] Values at end of function bug2:
t ∈ {1; 2}
-[eva:final-states] Values at end of function main_bug3:
- l_1180 ∈ {69166447}
- foo ∈ {4225800849}
-[eva:final-states] Values at end of function main_bug4:
+[eva:final-states] Values at end of function bug3:
+ l_1180 ∈ {0x41F656F}
+ foo ∈ {0xFBE09A91}
+[eva:final-states] Values at end of function bug4:
g_2 ∈ {-1; 0}
- tmp_0 ∈ {-5496}
+ tmp_0 ∈ {-0x1578}
+[eva:final-states] Values at end of function double_neg:
+ i ∈ {5}
+ j ∈ {0xFFFFFFFA}
+ k ∈ {-6}
+[eva:final-states] Values at end of function test1:
+ or1 ∈ [-3..31]
+ or2 ∈ [13..31]
+ or3 ∈ [-3..31]
+ and1 ∈ [0..17]
+ and2 ∈ [0..17]
+ and3 ∈ [0..27]
+ xor1 ∈ [0..31]
+ xor2 ∈ [-20..31]
+ uand4 ∈ {8; 16; 24}
+ a ∈ [3..17]
+ b ∈ [-3..17]
+ c ∈ [13..27]
+ i1 ∈ [0..0x1FFFE],0%2
+ i2 ∈ [0..0x3FFFC],0%4
+ v1 ∈ [0..0x1FFFC],0%4
+ v2 ∈ [0..0x3FFFE],0%2
+ mask07 ∈ {5}
+ mask0f ∈ {13}
+ mask1f ∈ {13; 29}
+[eva:final-states] Values at end of function test2:
+ x ∈ {56; 64; 72; 80; 88; 96; 104}
+[eva:final-states] Values at end of function test3:
+ x ∈ [-256..255]
+ y ∈ [-256..255]
+[eva:final-states] Values at end of function test4:
+ something ∈ [0..0x7FFFFFFF]
+ topBitOnly ∈ {0; 0x80000000}
+ __retres ∈ {1}
[eva:final-states] Values at end of function main:
-[from] Computing for function main_and_or_rel
-[from] Done for function main_and_or_rel
-[from] Computing for function main_bitwise
-[from] Done for function main_bitwise
-[from] Computing for function main_bug1
-[from] Done for function main_bug1
-[from] Computing for function main_bug2
-[from] Done for function main_bug2
-[from] Computing for function main_bug3
-[from] Done for function main_bug3
-[from] Computing for function main_bug4
-[from] Done for function main_bug4
+[from] Computing for function and_or_rel
+[from] Done for function and_or_rel
+[from] Computing for function bug1
+[from] Done for function bug1
+[from] Computing for function bug2
+[from] Done for function bug2
+[from] Computing for function bug3
+[from] Done for function bug3
+[from] Computing for function bug4
+[from] Done for function bug4
+[from] Computing for function double_neg
+[from] Done for function double_neg
+[from] Computing for function test1
+[from] Computing for function Frama_C_interval <-test1
+[from] Done for function Frama_C_interval
+[from] Done for function test1
+[from] Computing for function test2
+[from] Done for function test2
+[from] Computing for function test3
+[from] Done for function test3
+[from] Computing for function test4
+[from] Done for function test4
[from] Computing for function main
[from] Done for function main
[from] ====== DEPENDENCIES COMPUTED ======
These dependencies hold at termination for the executions that terminate:
-[from] Function main_and_or_rel:
+[from] Function Frama_C_interval:
+ \result FROM min; max
+[from] Function and_or_rel:
+ NO EFFECTS
+[from] Function bug1:
+ NO EFFECTS
+[from] Function bug2:
+ NO EFFECTS
+[from] Function bug3:
NO EFFECTS
-[from] Function main_bitwise:
+[from] Function bug4:
NO EFFECTS
-[from] Function main_bug1:
+[from] Function double_neg:
NO EFFECTS
-[from] Function main_bug2:
+[from] Function test1:
NO EFFECTS
-[from] Function main_bug3:
+[from] Function test2:
NO EFFECTS
-[from] Function main_bug4:
+[from] Function test3:
NO EFFECTS
+[from] Function test4:
+ \result FROM v
[from] Function main:
NO EFFECTS
[from] ====== END OF DEPENDENCIES ======
-[inout] Out (internal) for function main_and_or_rel:
+[inout] Out (internal) for function and_or_rel:
x; r1; r2; r3
-[inout] Inputs for function main_and_or_rel:
+[inout] Inputs for function and_or_rel:
v
-[inout] Out (internal) for function main_bitwise:
- i; j; k
-[inout] Inputs for function main_bitwise:
- \nothing
-[inout] Out (internal) for function main_bug1:
+[inout] Out (internal) for function bug1:
msb; lsb; par; p1; p2
-[inout] Inputs for function main_bug1:
+[inout] Inputs for function bug1:
\nothing
-[inout] Out (internal) for function main_bug2:
+[inout] Out (internal) for function bug2:
t; tmp
-[inout] Inputs for function main_bug2:
+[inout] Inputs for function bug2:
v
-[inout] Out (internal) for function main_bug3:
+[inout] Out (internal) for function bug3:
l_1180; foo
-[inout] Inputs for function main_bug3:
+[inout] Inputs for function bug3:
\nothing
-[inout] Out (internal) for function main_bug4:
+[inout] Out (internal) for function bug4:
g_2; tmp; tmp_0
-[inout] Inputs for function main_bug4:
+[inout] Inputs for function bug4:
+ v
+[inout] Out (internal) for function double_neg:
+ i; j; k
+[inout] Inputs for function double_neg:
+ \nothing
+[inout] Out (internal) for function test1:
+ or1; or2; or3; and1; and2; and3; xor1; xor2; uand4; a; b; c; i1; i2;
+ v1; v2; mask07; mask0f; mask1f
+[inout] Inputs for function test1:
+ s
+[inout] Out (internal) for function test2:
+ x; tmp
+[inout] Inputs for function test2:
+ \nothing
+[inout] Out (internal) for function test3:
+ x; tmp; y; tmp_0
+[inout] Inputs for function test3:
+ input[0..2]
+[inout] Out (internal) for function test4:
+ something; topBitOnly; __retres
+[inout] Inputs for function test4:
v
[inout] Out (internal) for function main:
\nothing
[inout] Inputs for function main:
- v
+ v; input[0..2]; s
diff --git a/tests/value/oracle/bitwise_or.res.oracle b/tests/value/oracle/bitwise_or.res.oracle
deleted file mode 100644
index 3a0e350f43ac2c40d13e7c3c4f296c3c3fc84fc4..0000000000000000000000000000000000000000
--- a/tests/value/oracle/bitwise_or.res.oracle
+++ /dev/null
@@ -1,72 +0,0 @@
-[kernel] Parsing tests/value/bitwise_or.c (with preprocessing)
-[eva] Analyzing a complete application starting at main
-[eva] Computing initial state
-[eva] Initial state computed
-[eva:initial-state] Values of globals at initialization
- s ∈ [--..--]
- t[0..2] ∈ [--..--]
-[eva] computing for function f1 <- main.
- Called from tests/value/bitwise_or.c:52.
-[eva] computing for function Frama_C_interval <- f1 <- main.
- Called from tests/value/bitwise_or.c:14.
-[eva] using specification for function Frama_C_interval
-[eva] tests/value/bitwise_or.c:14:
- function Frama_C_interval: precondition 'order' got status valid.
-[eva] Done for function Frama_C_interval
-[eva] computing for function Frama_C_interval <- f1 <- main.
- Called from tests/value/bitwise_or.c:15.
-[eva] tests/value/bitwise_or.c:15:
- function Frama_C_interval: precondition 'order' got status valid.
-[eva] Done for function Frama_C_interval
-[eva] computing for function Frama_C_interval <- f1 <- main.
- Called from tests/value/bitwise_or.c:16.
-[eva] tests/value/bitwise_or.c:16:
- function Frama_C_interval: precondition 'order' got status valid.
-[eva] Done for function Frama_C_interval
-[eva] Recording results for f1
-[eva] Done for function f1
-[eva] computing for function f2 <- main.
- Called from tests/value/bitwise_or.c:53.
-[eva] computing for function Frama_C_interval <- f2 <- main.
- Called from tests/value/bitwise_or.c:41.
-[eva] tests/value/bitwise_or.c:41:
- function Frama_C_interval: precondition 'order' got status valid.
-[eva] Done for function Frama_C_interval
-[eva] Recording results for f2
-[eva] Done for function f2
-[eva] computing for function f3 <- main.
- Called from tests/value/bitwise_or.c:54.
-[eva] Recording results for f3
-[eva] Done for function f3
-[eva] Recording results for main
-[eva] done for function main
-[eva] ====== VALUES COMPUTED ======
-[eva:final-states] Values at end of function f1:
- Frama_C_entropy_source ∈ [--..--]
- or1 ∈ [-3..31]
- or2 ∈ [13..31]
- or3 ∈ [-3..31]
- and1 ∈ [0..17]
- and2 ∈ [0..17]
- and3 ∈ [0..27]
- xor1 ∈ [0..31]
- xor2 ∈ [-20..31]
- uand4 ∈ {8; 16; 24}
- a ∈ [3..17]
- b ∈ [-3..17]
- c ∈ [13..27]
- i1 ∈ [0..0x1FFFE],0%2
- i2 ∈ [0..0x3FFFC],0%4
- v1 ∈ [0..0x1FFFC],0%4
- v2 ∈ [0..0x3FFFE],0%2
- mask07 ∈ {5}
- mask0f ∈ {13}
- mask1f ∈ {13; 29}
-[eva:final-states] Values at end of function f2:
- Frama_C_entropy_source ∈ [--..--]
- x ∈ {56; 64; 72; 80; 88; 96; 104}
-[eva:final-states] Values at end of function f3:
- x ∈ [-256..255]
- y ∈ [-256..255]
-[eva:final-states] Values at end of function main:
- Frama_C_entropy_source ∈ [--..--]