From 395ad9a0cfbd5cf8a5cd4c9992d3b7e4f86a1cf1 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Wed, 1 Dec 2021 10:39:13 +0100 Subject: [PATCH 01/15] Steps towards removing Cilint --- src/cilint.ml | 128 ++++++++----------------------------------------- src/cilint.mli | 2 +- 2 files changed, 21 insertions(+), 109 deletions(-) diff --git a/src/cilint.ml b/src/cilint.ml index 1b7e5de6f..8ba890017 100644 --- a/src/cilint.ml +++ b/src/cilint.ml @@ -23,11 +23,11 @@ open Big_int_Z -type cilint = Small of int | Big of big_int +type cilint = big_int type truncation = NoTruncation | ValueTruncation | BitTruncation -let zero_cilint = Small 0 -let one_cilint = Small 1 +let zero_cilint = zero_big_int +let one_cilint = unit_big_int (* Precompute useful big_ints *) let b30 = power_int_positive_int 2 30 @@ -37,21 +37,10 @@ let m1 = minus_big_int unit_big_int let nobits (b:big_int) : bool = sign_big_int b = 0 || compare_big_int b m1 = 0 -let big_int_of_cilint (c:cilint) : big_int = - match c with - | Small i -> big_int_of_int i - | Big b -> b +let big_int_of_cilint (c:cilint) : big_int = c +let cilint_of_big_int (b:big_int) : cilint = b -let cilint_of_big_int (b:big_int) : cilint = - if is_int_big_int b then - Small (int_of_big_int b) - else - Big b - -let neg_cilint c = - match c with - | Small i when i <> min_int -> Small (-i) - | _ -> Big (minus_big_int (big_int_of_cilint c)) +let neg_cilint c = minus_big_int (big_int_of_cilint c) (* Apply big_int 'op' to two cilints, returning a cilint *) let b op c1 c2 = cilint_of_big_int (op (big_int_of_cilint c1) (big_int_of_cilint c2)) @@ -62,33 +51,17 @@ let mul_cilint = b mult_big_int let div_cilint = b div_big_int let mod_cilint = b mod_big_int -let compare_cilint (c1:cilint) (c2:cilint) : int = - match c1, c2 with - | Small i1, Small i2 -> compare i1 i2 - | _ -> compare_big_int (big_int_of_cilint c1) (big_int_of_cilint c2) +let compare_cilint (c1:cilint) (c2:cilint) : int = compare_big_int (big_int_of_cilint c1) (big_int_of_cilint c2) -let is_zero_cilint (c:cilint) : bool = - match c with - | Small i -> i = 0 - | Big b -> sign_big_int b = 0 +let is_zero_cilint (c:cilint) : bool = sign_big_int c = 0 -let negative_cilint (c:cilint) : bool = - match c with - | Small i -> i < 0 - | Big b -> sign_big_int b < 0 +let negative_cilint (c:cilint) : bool = sign_big_int c < 0 -let cilint_of_int (i:int) : cilint = Small i +let cilint_of_int (i:int) : cilint = big_int_of_int i -let int_of_cilint (c:cilint) : int = - match c with - | Small i -> i - | Big b -> int_of_big_int b +let int_of_cilint (c:cilint) : int = int_of_big_int c let cilint_of_int64 (i64:int64) : cilint = - if Int64.compare i64 (Int64.of_int min_int) >= 0 && - Int64.compare i64 (Int64.of_int max_int) <= 0 then - Small (Int64.to_int i64) - else (* We convert 30 bits at a time *) let rec loop i mul acc = if i = 0L then acc @@ -97,14 +70,11 @@ let cilint_of_int64 (i64:int64) : cilint = let lo30 = Int64.to_int (Int64.logand i 0x3fffffffL) in loop (Int64.shift_right i 30) (mult_big_int mul b30) (add_big_int acc (mult_big_int mul (big_int_of_int lo30))) - in Big (loop i64 unit_big_int zero_big_int) + in (loop i64 unit_big_int zero_big_int) (* Note that this never fails, instead it returns the low-order 64-bits of the cilint. *) -let int64_of_cilint (c:cilint) : int64 = - match c with - | Small i -> Int64.of_int i - | Big b -> +let int64_of_cilint (b:cilint) : int64 = let rec loop b mul acc = if sign_big_int b = 0 then acc @@ -119,26 +89,20 @@ let int64_of_cilint (c:cilint) : int64 = let cilint_of_string (s:string) : cilint = cilint_of_big_int (big_int_of_string s) -let string_of_cilint (c:cilint) : string = - match c with - | Small i -> string_of_int i - | Big b -> string_of_big_int b +let string_of_cilint (c:cilint) : string = string_of_big_int c (* Divide rounding towards zero *) let div0_cilint (c1:cilint) (c2:cilint) = - match c1, c2 with - | Small i1, Small i2 -> Small (i1 / i2) - | _ -> let b1 = big_int_of_cilint c1 in let b2 = big_int_of_cilint c2 in let q, r = quomod_big_int b1 b2 in if lt_big_int b1 zero_big_int && (not (eq_big_int r zero_big_int)) then if gt_big_int b2 zero_big_int then - Big (succ_big_int q) + (succ_big_int q) else - Big (pred_big_int q) + (pred_big_int q) else - Big q + q (* And the corresponding remainder *) let rem_cilint (c1:cilint) (c2:cilint) = @@ -147,9 +111,6 @@ let rem_cilint (c1:cilint) (c2:cilint) = (* Perform logical op 'op' over 'int' on two cilints. Does it work 30-bits at a time as that is guaranteed to fit in an 'int'. *) let logop op c1 c2 = - match c1, c2 with - | Small i1, Small i2 -> Small (op i1 i2) - | _ -> let b1 = big_int_of_cilint c1 in let b2 = big_int_of_cilint c2 in let rec loop b1 b2 mul acc = @@ -173,44 +134,14 @@ let logand_cilint = logop (land) let logor_cilint = logop (lor) let logxor_cilint = logop (lxor) -let shift_right_cilint (c1:cilint) (n:int) : cilint = - match c1 with - | Small i -> Small (i asr n) - | Big b -> cilint_of_big_int (div_big_int b (power_int_positive_int 2 n)) +let shift_right_cilint (c1:cilint) (n:int) : cilint = cilint_of_big_int (div_big_int c1 (power_int_positive_int 2 n)) let shift_left_cilint (c1:cilint) (n:int) : cilint = cilint_of_big_int (mult_big_int (big_int_of_cilint c1) (power_int_positive_int 2 n)) -let lognot_cilint (c1:cilint) : cilint = - match c1 with - | Small i -> Small (lnot i) - | Big b -> Big (pred_big_int (minus_big_int b)) +let lognot_cilint (c1:cilint) : cilint = (pred_big_int (minus_big_int c1)) let truncate_signed_cilint (c:cilint) (n:int) : cilint * truncation = - match c with - | Small i when n >= Nativeint.size - 1 -> Small i, NoTruncation - | Small i when n < Nativeint.size - 2 -> - let max = 1 lsl (n - 1) in - let truncmax = 1 lsl n in - let bits = i land (truncmax - 1) in - let tval = - (* check if the n-th bit is 1... *) - if bits < max then - bits - else - (* and fill with 1 bits on the left if it is *) - bits - truncmax - in - let trunc = - if i >= max || i < -max then - if i >= truncmax then - BitTruncation - else - ValueTruncation - else - NoTruncation - in Small tval, trunc - | _ -> let b = big_int_of_cilint c in let max = power_int_positive_int 2 (n - 1) in let truncmax = power_int_positive_int 2 n in @@ -232,22 +163,6 @@ let truncate_signed_cilint (c:cilint) (n:int) : cilint * truncation = in cilint_of_big_int tval, trunc let truncate_unsigned_cilint (c:cilint) (n:int) : cilint * truncation = - match c with - | Small i when i > 0 && n >= Nativeint.size - 2 -> Small i, NoTruncation - | Small i when n < Nativeint.size - 2 -> - let max = 1 lsl (n - 1) in - let truncmax = 1 lsl n in - let bits = i land (truncmax - 1) in - let trunc = - if i >= truncmax || i < 0 then - if i < -max then - BitTruncation - else - ValueTruncation - else - NoTruncation - in Small bits, trunc - | _ -> let b = big_int_of_cilint c in let max = power_int_positive_int 2 (n - 1) in let truncmax = power_int_positive_int 2 n in @@ -262,7 +177,4 @@ let truncate_unsigned_cilint (c:cilint) (n:int) : cilint * truncation = NoTruncation in cilint_of_big_int bits, trunc -let is_int_cilint (c:cilint) : bool = - match c with - | Small _ -> true - | Big b -> is_int_big_int b +let is_int_cilint (c:cilint) : bool = is_int_big_int c diff --git a/src/cilint.mli b/src/cilint.mli index 1f5b02662..fea83976b 100644 --- a/src/cilint.mli +++ b/src/cilint.mli @@ -3,7 +3,7 @@ (** The cilint type is public and not just big_int to make life with ocamldebug easier. Please do not rely on this representation, use the ..._of_cilint functions to get at a cilint's value. *) -type cilint = Small of int | Big of Big_int_Z.big_int +type cilint = Big_int_Z.big_int (** 0 as a cilint *) val zero_cilint : cilint From 93eecd7ea06116b7856d12d591af2dd1f5910326 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Wed, 1 Dec 2021 10:55:47 +0100 Subject: [PATCH 02/15] Make indentation less crazy --- src/cilint.ml | 149 +++++++++++++++++++++++++------------------------- 1 file changed, 75 insertions(+), 74 deletions(-) diff --git a/src/cilint.ml b/src/cilint.ml index 8ba890017..6a87d57b5 100644 --- a/src/cilint.ml +++ b/src/cilint.ml @@ -62,29 +62,29 @@ let cilint_of_int (i:int) : cilint = big_int_of_int i let int_of_cilint (c:cilint) : int = int_of_big_int c let cilint_of_int64 (i64:int64) : cilint = - (* We convert 30 bits at a time *) - let rec loop i mul acc = - if i = 0L then acc - else if i = -1L then sub_big_int acc mul - else + (* We convert 30 bits at a time *) + let rec loop i mul acc = + if i = 0L then acc + else if i = -1L then sub_big_int acc mul + else let lo30 = Int64.to_int (Int64.logand i 0x3fffffffL) in loop (Int64.shift_right i 30) (mult_big_int mul b30) (add_big_int acc (mult_big_int mul (big_int_of_int lo30))) - in (loop i64 unit_big_int zero_big_int) + in (loop i64 unit_big_int zero_big_int) (* Note that this never fails, instead it returns the low-order 64-bits of the cilint. *) let int64_of_cilint (b:cilint) : int64 = - let rec loop b mul acc = - if sign_big_int b = 0 then - acc - else if compare_big_int b m1 == 0 then - Int64.sub acc mul - else - let hi, lo = quomod_big_int b b30 in - loop hi (Int64.mul mul 0x40000000L) - (Int64.add acc (Int64.mul mul (Int64.of_int (int_of_big_int lo)))) - in loop b 1L 0L + let rec loop b mul acc = + if sign_big_int b = 0 then + acc + else if compare_big_int b m1 == 0 then + Int64.sub acc mul + else + let hi, lo = quomod_big_int b b30 in + loop hi (Int64.mul mul 0x40000000L) + (Int64.add acc (Int64.mul mul (Int64.of_int (int_of_big_int lo)))) + in loop b 1L 0L let cilint_of_string (s:string) : cilint = cilint_of_big_int (big_int_of_string s) @@ -93,16 +93,16 @@ let string_of_cilint (c:cilint) : string = string_of_big_int c (* Divide rounding towards zero *) let div0_cilint (c1:cilint) (c2:cilint) = - let b1 = big_int_of_cilint c1 in - let b2 = big_int_of_cilint c2 in - let q, r = quomod_big_int b1 b2 in - if lt_big_int b1 zero_big_int && (not (eq_big_int r zero_big_int)) then - if gt_big_int b2 zero_big_int then - (succ_big_int q) - else - (pred_big_int q) - else - q + let b1 = big_int_of_cilint c1 in + let b2 = big_int_of_cilint c2 in + let q, r = quomod_big_int b1 b2 in + if lt_big_int b1 zero_big_int && (not (eq_big_int r zero_big_int)) then + if gt_big_int b2 zero_big_int then + (succ_big_int q) + else + (pred_big_int q) + else + q (* And the corresponding remainder *) let rem_cilint (c1:cilint) (c2:cilint) = @@ -111,24 +111,24 @@ let rem_cilint (c1:cilint) (c2:cilint) = (* Perform logical op 'op' over 'int' on two cilints. Does it work 30-bits at a time as that is guaranteed to fit in an 'int'. *) let logop op c1 c2 = - let b1 = big_int_of_cilint c1 in - let b2 = big_int_of_cilint c2 in - let rec loop b1 b2 mul acc = - if nobits b1 && nobits b2 then - (* Once we only have all-0/all-1 values left, we can find whether - the infinite high-order bits are all-0 or all-1 by checking the - behaviour of op on b1 and b2. *) - if op (int_of_big_int b1) (int_of_big_int b2) = 0 then - acc - else - sub_big_int acc mul - else - let hi1, lo1 = quomod_big_int b1 b30 in - let hi2, lo2 = quomod_big_int b2 b30 in - let lo = op (int_of_big_int lo1) (int_of_big_int lo2) in - loop hi1 hi2 (mult_big_int mul b30) - (add_big_int acc (mult_big_int mul (big_int_of_int lo))) - in cilint_of_big_int (loop b1 b2 unit_big_int zero_big_int) + let b1 = big_int_of_cilint c1 in + let b2 = big_int_of_cilint c2 in + let rec loop b1 b2 mul acc = + if nobits b1 && nobits b2 then + (* Once we only have all-0/all-1 values left, we can find whether + the infinite high-order bits are all-0 or all-1 by checking the + behaviour of op on b1 and b2. *) + if op (int_of_big_int b1) (int_of_big_int b2) = 0 then + acc + else + sub_big_int acc mul + else + let hi1, lo1 = quomod_big_int b1 b30 in + let hi2, lo2 = quomod_big_int b2 b30 in + let lo = op (int_of_big_int lo1) (int_of_big_int lo2) in + loop hi1 hi2 (mult_big_int mul b30) + (add_big_int acc (mult_big_int mul (big_int_of_int lo))) + in cilint_of_big_int (loop b1 b2 unit_big_int zero_big_int) let logand_cilint = logop (land) let logor_cilint = logop (lor) @@ -142,39 +142,40 @@ let shift_left_cilint (c1:cilint) (n:int) : cilint = let lognot_cilint (c1:cilint) : cilint = (pred_big_int (minus_big_int c1)) let truncate_signed_cilint (c:cilint) (n:int) : cilint * truncation = - let b = big_int_of_cilint c in - let max = power_int_positive_int 2 (n - 1) in - let truncmax = power_int_positive_int 2 n in - let bits = mod_big_int b truncmax in - let tval = - if lt_big_int bits max then - bits - else - sub_big_int bits truncmax - in - let trunc = - if ge_big_int b max || lt_big_int b (minus_big_int max) then - if ge_big_int b truncmax then - BitTruncation + let b = big_int_of_cilint c in + let max = power_int_positive_int 2 (n - 1) in + let truncmax = power_int_positive_int 2 n in + let bits = mod_big_int b truncmax in + let tval = if lt_big_int bits max then + bits else - ValueTruncation - else - NoTruncation - in cilint_of_big_int tval, trunc + sub_big_int bits truncmax + in + let trunc = + if ge_big_int b max || lt_big_int b (minus_big_int max) then + if ge_big_int b truncmax then + BitTruncation + else + ValueTruncation + else + NoTruncation + in + cilint_of_big_int tval, trunc let truncate_unsigned_cilint (c:cilint) (n:int) : cilint * truncation = - let b = big_int_of_cilint c in - let max = power_int_positive_int 2 (n - 1) in - let truncmax = power_int_positive_int 2 n in - let bits = mod_big_int b truncmax in - let trunc = - if ge_big_int b truncmax || lt_big_int b zero_big_int then - if lt_big_int b (minus_big_int max) then - BitTruncation + let b = big_int_of_cilint c in + let max = power_int_positive_int 2 (n - 1) in + let truncmax = power_int_positive_int 2 n in + let bits = mod_big_int b truncmax in + let trunc = + if ge_big_int b truncmax || lt_big_int b zero_big_int then + if lt_big_int b (minus_big_int max) then + BitTruncation + else + ValueTruncation else - ValueTruncation - else - NoTruncation - in cilint_of_big_int bits, trunc + NoTruncation + in + cilint_of_big_int bits, trunc let is_int_cilint (c:cilint) : bool = is_int_big_int c From 23705af896e689e8104031a87abc08de638ffa32 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Wed, 1 Dec 2021 11:12:47 +0100 Subject: [PATCH 03/15] More simplication --- src/cilint.ml | 90 ++++++++++++++++++--------------------------------- 1 file changed, 31 insertions(+), 59 deletions(-) diff --git a/src/cilint.ml b/src/cilint.ml index 6a87d57b5..6f5c3d423 100644 --- a/src/cilint.ml +++ b/src/cilint.ml @@ -10,16 +10,7 @@ 3 = ...0000000000011 -3 = ...1111111111101 - We represent cilints using a big_int, except that we specialise the - case where the number fits in a regular int. This specialisation - has two benefits: - - more compact (and potentially faster ops, though more would need to be - specialised for this to be really worth it) - - ability to see the value of small constants in ocamldebug - - The implementation can be simplified once OCaml 3.11.1 shows up, with - bitwise operations on big_ints, and bug-fixed versions of int64_of_big_int - and big_int_of_int64. *) + We represent cilints using a big_int but define some operations differently *) open Big_int_Z @@ -40,37 +31,23 @@ let nobits (b:big_int) : bool = let big_int_of_cilint (c:cilint) : big_int = c let cilint_of_big_int (b:big_int) : cilint = b -let neg_cilint c = minus_big_int (big_int_of_cilint c) - -(* Apply big_int 'op' to two cilints, returning a cilint *) -let b op c1 c2 = cilint_of_big_int (op (big_int_of_cilint c1) (big_int_of_cilint c2)) - -let add_cilint = b add_big_int -let sub_cilint = b sub_big_int -let mul_cilint = b mult_big_int -let div_cilint = b div_big_int -let mod_cilint = b mod_big_int +let neg_cilint = minus_big_int -let compare_cilint (c1:cilint) (c2:cilint) : int = compare_big_int (big_int_of_cilint c1) (big_int_of_cilint c2) +let add_cilint = add_big_int +let sub_cilint = sub_big_int +let mul_cilint = mult_big_int +let div_cilint = div_big_int +let mod_cilint = mod_big_int +let compare_cilint = compare_big_int let is_zero_cilint (c:cilint) : bool = sign_big_int c = 0 let negative_cilint (c:cilint) : bool = sign_big_int c < 0 -let cilint_of_int (i:int) : cilint = big_int_of_int i +let cilint_of_int = big_int_of_int +let int_of_cilint = int_of_big_int -let int_of_cilint (c:cilint) : int = int_of_big_int c - -let cilint_of_int64 (i64:int64) : cilint = - (* We convert 30 bits at a time *) - let rec loop i mul acc = - if i = 0L then acc - else if i = -1L then sub_big_int acc mul - else - let lo30 = Int64.to_int (Int64.logand i 0x3fffffffL) in - loop (Int64.shift_right i 30) (mult_big_int mul b30) - (add_big_int acc (mult_big_int mul (big_int_of_int lo30))) - in (loop i64 unit_big_int zero_big_int) +let cilint_of_int64 (i64:int64) : cilint = big_int_of_int64 i64 (* Note that this never fails, instead it returns the low-order 64-bits of the cilint. *) @@ -86,33 +63,30 @@ let int64_of_cilint (b:cilint) : int64 = (Int64.add acc (Int64.mul mul (Int64.of_int (int_of_big_int lo)))) in loop b 1L 0L -let cilint_of_string (s:string) : cilint = - cilint_of_big_int (big_int_of_string s) - -let string_of_cilint (c:cilint) : string = string_of_big_int c +let cilint_of_string = big_int_of_string +let string_of_cilint = string_of_big_int (* Divide rounding towards zero *) let div0_cilint (c1:cilint) (c2:cilint) = - let b1 = big_int_of_cilint c1 in - let b2 = big_int_of_cilint c2 in - let q, r = quomod_big_int b1 b2 in - if lt_big_int b1 zero_big_int && (not (eq_big_int r zero_big_int)) then - if gt_big_int b2 zero_big_int then + let q, r = quomod_big_int c1 c2 in + if lt_big_int c1 zero_big_int && (not (eq_big_int r zero_big_int)) then + if gt_big_int c2 zero_big_int then (succ_big_int q) else (pred_big_int q) else q -(* And the corresponding remainder *) +(* And the corresponding remainder! Different from *) +(* Big_int_Z.mod_big_int computes the Euclidian Modulus, but what we want here is the remainder, as returned by mod on ints + -1 rem 5 == -1, whereas -1 Euclid-Mod 5 == 4 +*) let rem_cilint (c1:cilint) (c2:cilint) = (sub_cilint c1 (mul_cilint c2 (div0_cilint c1 c2))) (* Perform logical op 'op' over 'int' on two cilints. Does it work 30-bits at a time as that is guaranteed to fit in an 'int'. *) let logop op c1 c2 = - let b1 = big_int_of_cilint c1 in - let b2 = big_int_of_cilint c2 in let rec loop b1 b2 mul acc = if nobits b1 && nobits b2 then (* Once we only have all-0/all-1 values left, we can find whether @@ -128,54 +102,52 @@ let logop op c1 c2 = let lo = op (int_of_big_int lo1) (int_of_big_int lo2) in loop hi1 hi2 (mult_big_int mul b30) (add_big_int acc (mult_big_int mul (big_int_of_int lo))) - in cilint_of_big_int (loop b1 b2 unit_big_int zero_big_int) + in loop c1 c2 unit_big_int zero_big_int let logand_cilint = logop (land) let logor_cilint = logop (lor) let logxor_cilint = logop (lxor) -let shift_right_cilint (c1:cilint) (n:int) : cilint = cilint_of_big_int (div_big_int c1 (power_int_positive_int 2 n)) +let shift_right_cilint (c1:cilint) (n:int) : cilint = div_big_int c1 (power_int_positive_int 2 n) let shift_left_cilint (c1:cilint) (n:int) : cilint = - cilint_of_big_int (mult_big_int (big_int_of_cilint c1) (power_int_positive_int 2 n)) + mult_big_int c1 (power_int_positive_int 2 n) let lognot_cilint (c1:cilint) : cilint = (pred_big_int (minus_big_int c1)) let truncate_signed_cilint (c:cilint) (n:int) : cilint * truncation = - let b = big_int_of_cilint c in let max = power_int_positive_int 2 (n - 1) in let truncmax = power_int_positive_int 2 n in - let bits = mod_big_int b truncmax in + let bits = mod_big_int c truncmax in let tval = if lt_big_int bits max then bits else sub_big_int bits truncmax in let trunc = - if ge_big_int b max || lt_big_int b (minus_big_int max) then - if ge_big_int b truncmax then + if ge_big_int c max || lt_big_int c (minus_big_int max) then + if ge_big_int c truncmax then BitTruncation else ValueTruncation else NoTruncation in - cilint_of_big_int tval, trunc + tval, trunc let truncate_unsigned_cilint (c:cilint) (n:int) : cilint * truncation = - let b = big_int_of_cilint c in let max = power_int_positive_int 2 (n - 1) in let truncmax = power_int_positive_int 2 n in - let bits = mod_big_int b truncmax in + let bits = mod_big_int c truncmax in let trunc = - if ge_big_int b truncmax || lt_big_int b zero_big_int then - if lt_big_int b (minus_big_int max) then + if ge_big_int c truncmax || lt_big_int c zero_big_int then + if lt_big_int c (minus_big_int max) then BitTruncation else ValueTruncation else NoTruncation in - cilint_of_big_int bits, trunc + bits, trunc let is_int_cilint (c:cilint) : bool = is_int_big_int c From 1bb71407676c5791d228ad30c48580c3c0ff32f4 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Wed, 1 Dec 2021 13:55:48 +0100 Subject: [PATCH 04/15] Switch Cint64 to cilint --- src/check.ml | 8 +- src/cil.ml | 171 +++++++++---------------------------- src/cil.mli | 27 ++---- src/cilint.ml | 1 + src/cilint.mli | 3 + src/ext/zrapp/rmciltmps.ml | 12 +-- src/formatparse.mly | 2 +- src/frontc/cabs2cil.ml | 50 +++++------ src/mergecil.ml | 2 +- 9 files changed, 86 insertions(+), 190 deletions(-) diff --git a/src/check.ml b/src/check.ml index 1b96991c3..96cdfac2c 100644 --- a/src/check.ml +++ b/src/check.ml @@ -641,8 +641,8 @@ and checkInit (i: init) : typ = match elen with | None -> 0L | Some e -> (ignore (checkExp true e); - match isInteger (constFold true e) with - Some len -> len + match getInteger (constFold true e) with + Some len -> Z.to_int64 len (* Z on purpose, we don;t want to ingore overflows here *) | None -> ignore (warn "Array length is not a constant"); 0L) @@ -653,9 +653,9 @@ and checkInit (i: init) : typ = ignore (warn "Wrong number of initializers in array") | (Index(Const(CInt64(i', _, _)), NoOffset), ei) :: rest -> - if i' <> i then + if Int64.compare (Z.to_int64 i') i <> 0 then ignore (warn "Initializer for index %s when %s was expected" - (Int64.format "%d" i') (Int64.format "%d" i)); + (Int64.format "%d" (Z.to_int64 i')) (Int64.format "%d" i)); checkInitType ei bt; loopIndex (Int64.succ i) rest | _ :: rest -> diff --git a/src/cil.ml b/src/cil.ml index 69084666f..eb0c1f0a3 100755 --- a/src/cil.ml +++ b/src/cil.ml @@ -543,12 +543,10 @@ and exp = (** Literal constants *) and constant = - | CInt64 of int64 * ikind * string option + | CInt64 of cilint * ikind * string option (** Integer constant. Give the ikind (see ISO9899 6.1.3.2) * and the textual representation, if available. Use - * {!Cil.integer} or {!Cil.kinteger} to create these. Watch - * out for integers that cannot be represented on 64 bits. - * OCAML does not give Overflow exceptions. *) + * {!Cil.integer} or {!Cil.kinteger} to create these. *) | CStr of string (** String constant (of pointer type) *) | CWStr of int64 list (** Wide string constant (of type "wchar_t *") *) | CChr of char (** Character constant. This has type int, so use @@ -873,7 +871,7 @@ and location = { (* Type signatures. Two types are identical iff they have identical * signatures *) and typsig = - TSArray of typsig * int64 option * attribute list + TSArray of typsig * cilint option * attribute list | TSPtr of typsig * attribute list | TSComp of bool * string * attribute list | TSFun of typsig * typsig list option * bool * attribute list @@ -1241,7 +1239,7 @@ let warnLoc (loc: location) (fmt : ('a,unit,doc) format) : 'a = in Pretty.gprintf f fmt -let zero = Const(CInt64(Int64.zero, IInt, None)) +let zero = Const(CInt64(zero_cilint, IInt, None)) (** Given the character c in a (CChr c), sign-extend it to 32 bits. (This is the official way of interpreting character constants, according to @@ -1251,8 +1249,8 @@ let charConstToInt (c: char) : constant = let c' = Char.code c in let value = if c' < 128 - then Int64.of_int c' - else Int64.of_int (c' - 256) + then cilint_of_int c' + else cilint_of_int (c' - 256) in CInt64(value, IInt, None) @@ -1719,8 +1717,8 @@ let d_storage () = function | Register -> text "register " (* sm: need this value below *) -let mostNeg32BitInt : int64 = (Int64.of_string "-0x80000000") -let mostNeg64BitInt : int64 = (Int64.of_string "-0x8000000000000000") +let mostNeg32BitInt : cilint = cilint_of_string "-0x80000000" +let mostNeg64BitInt : cilint = cilint_of_string "-0x8000000000000000" let bytesSizeOfInt (ik: ikind): int = match ik with @@ -1760,26 +1758,26 @@ let d_const () c = in (* Watch out here for negative integers that we should be printing as * large positive ones *) - if i < Int64.zero && (not (isSigned ik)) then + if compare_cilint i zero_cilint < 0 && (not (isSigned ik)) then if bytesSizeOfInt ik <> 8 then (* I am convinced that we shall never store smaller than 64-bits * integers in negative form. -- Gabriel *) E.s (E.bug "unexpected negative unsigned integer (please report this bug)") else - text (prefix ^ "0x" ^ Int64.format "%x" i ^ suffix) + text (prefix ^ "0x" ^ Z.format "%x" i ^ suffix) else ( - if (i = mostNeg32BitInt) then + if (compare_cilint i mostNeg32BitInt = 0) then (* sm: quirk here: if you print -2147483648 then this is two tokens *) (* in C, and the second one is too large to represent in a signed *) (* int.. so we do what's done in limits.h, and print (-2147483467-1); *) (* in gcc this avoids a warning, but it might avoid a real problem *) (* on another compiler or a 64-bit architecture *) text (prefix ^ "(-0x7FFFFFFF-1)") - else if (i = mostNeg64BitInt) then + else if (compare_cilint i mostNeg64BitInt = 0) then (* The same is true of the largest 64-bit negative. *) text (prefix ^ "(-0x7FFFFFFFFFFFFFFF-1)") else - text (prefix ^ (Int64.to_string i ^ suffix)) + text (prefix ^ (string_of_cilint i ^ suffix)) ) | CStr(s) -> text ("\"" ^ escape_string s ^ "\"") @@ -2079,8 +2077,12 @@ let truncateCilint (k: ikind) (i: cilint) : cilint * truncation = else truncate_unsigned_cilint i nrBits +let mkCilintIk (ik:ikind) (i:cilint) : cilint = + fst (truncateCilint ik i) + let mkCilint (ik:ikind) (i:int64) : cilint = - fst (truncateCilint ik (cilint_of_int64 i)) + mkCilintIk ik (cilint_of_int64 i) + (* Construct an integer constant with possible truncation *) let kintegerCilint (k: ikind) (i: cilint) : exp = @@ -2088,16 +2090,7 @@ let kintegerCilint (k: ikind) (i: cilint) : exp = if truncated = BitTruncation && !warnTruncate then ignore (warnOpt "Truncating integer %s to %s" (string_of_cilint i) (string_of_cilint i')); - let str = - let int64_min = cilint_of_int64 Int64.min_int in - let int64_max = cilint_of_int64 Int64.max_int in - (* if the resulting value can not be represented by an Int64, store its string representation *) - if Cilint.compare_cilint i' int64_min < 0 || Cilint.compare_cilint int64_max i' < 0 then ( - Some (string_of_cilint i') - ) - else None - in - Const (CInt64(int64_of_cilint i', k, str)) + Const (CInt64(i', k, None)) (* Construct an integer constant with possible truncation *) let kinteger64 (k: ikind) (i: int64) : exp = @@ -2145,7 +2138,7 @@ let intKindForValue (i: cilint) (unsigned: bool) = Otherwise return None. *) let rec getInteger (e:exp) : cilint option = match e with - | Const(CInt64 (n, ik, _)) -> Some (mkCilint ik n) + | Const(CInt64 (n, ik, _)) -> Some (mkCilintIk ik n) | Const(CChr c) -> getInteger (Const (charConstToInt c)) | Const(CEnum(v, _, _)) -> getInteger v | CastE(t, e) -> begin @@ -2410,7 +2403,7 @@ and bitsSizeOf t = | TArray(bt, Some len, _) -> begin match constFold true len with Const(CInt64(l,lk,_)) -> - let sz = mul_cilint (mkCilint lk l) (cilint_of_int (bitsSizeOf bt)) in + let sz = mul_cilint (mkCilintIk lk l) (cilint_of_int (bitsSizeOf bt)) in (* Check for overflow. There are other places in these cil.ml that overflow can occur, but this multiplication is the most likely to be a problem. *) @@ -2508,7 +2501,7 @@ and constFold (machdep: bool) (e: exp) : exp = in match constFold machdep e1 with Const(CInt64(i,ik,_)) -> begin - let ic = mkCilint ik i in + let ic = mkCilintIk ik i in match unop with Neg -> kintegerCilint tk (neg_cilint ic) | BNot -> kintegerCilint tk (lognot_cilint ic) @@ -2558,8 +2551,8 @@ and constFold (machdep: bool) (e: exp) : exp = (* It's okay to drop a cast to const. If the cast has any other attributes, leave the cast alone. *) when (dropAttributes ["const"] a) = [] -> - let i', _ = truncateCilint nk (mkCilint k i) in - Const(CInt64(int64_of_cilint i', nk, None)) + let i', _ = truncateCilint nk (mkCilintIk k i) in + Const(CInt64(i', nk, None)) | e', _ -> CastE (t, e') end | Lval lv -> Lval (constFoldLval machdep lv) @@ -3509,20 +3502,20 @@ class defaultCilPrinterClass : cilPrinter = object (self) (* Be nice to some special cases *) match e with BinOp((PlusA|PlusPI|IndexPI),Lval(lv'),Const(CInt64(one,_,_)),_) - when Util.equals lv lv' && one = Int64.one && not !printCilAsIs -> + when Util.equals lv lv' && compare_cilint one one_cilint = 0 && not !printCilAsIs -> self#pLineDirective l ++ self#pLvalPrec indexLevel () lv ++ text (" ++" ^ printInstrTerminator) | BinOp((MinusA|MinusPI),Lval(lv'), Const(CInt64(one,_,_)), _) - when Util.equals lv lv' && one = Int64.one && not !printCilAsIs -> + when Util.equals lv lv' && compare_cilint one one_cilint = 0 && not !printCilAsIs -> self#pLineDirective l ++ self#pLvalPrec indexLevel () lv ++ text (" --" ^ printInstrTerminator) | BinOp((PlusA|PlusPI|IndexPI),Lval(lv'),Const(CInt64(mone,_,_)),_) - when Util.equals lv lv' && mone = Int64.minus_one + when Util.equals lv lv' && compare_cilint mone mone_cilint = 0 && not !printCilAsIs -> self#pLineDirective l ++ self#pLvalPrec indexLevel () lv @@ -4606,7 +4599,7 @@ class plainCilPrinterClass = CInt64(i, ik, so) -> let fmt = if isSigned ik then "%d" else "%x" in dprintf "Int64(%s,%a,%s)" - (Int64.format fmt i) + (Z.format fmt i) d_ikind ik (match so with Some s -> s | _ -> "None") | CStr(s) -> @@ -4807,7 +4800,7 @@ let rec d_typsig () = function dprintf "TSArray(@[%a,@?%a,@?%a@])" d_typsig ts insert (text (match eo with None -> "None" - | Some e -> "Some " ^ Int64.to_string e)) + | Some e -> "Some " ^ string_of_cilint e)) d_attrlist al | TSPtr (ts, al) -> dprintf "TSPtr(@[%a,@?%a@])" @@ -5804,7 +5797,7 @@ exception NotAnAttrParam of exp let rec expToAttrParam (e: exp) : attrparam = match e with Const(CInt64(i,k,_)) -> - let i' = mkCilint k i in + let i' = mkCilintIk k i in if not (is_int_cilint i') then raise (NotAnAttrParam e); AInt (int_of_cilint i') @@ -6036,10 +6029,10 @@ let mkCastT ~(e: exp) ~(oldt: typ) ~(newt: typ) = match newt, e with (* Casts to _Bool are special: they behave like "!= 0" ISO C99 6.3.1.2 *) TInt(IBool, []), Const(CInt64(i, _, _)) -> - let v = if i = Int64.zero then Int64.zero else Int64.one in + let v = if compare i zero_cilint = 0 then zero_cilint else one_cilint in Const (CInt64(v, IBool, None)) | TInt(newik, []), Const(CInt64(_, _, Some s)) -> kintegerCilint newik (Cilint.cilint_of_string s) - | TInt(newik, []), Const(CInt64(i, _, None)) -> kinteger64 newik i + | TInt(newik, []), Const(CInt64(i, _, None)) -> kintegerCilint newik i | _ -> CastE(newt,e) end @@ -6092,8 +6085,8 @@ let lenOfArray (eo: exp option) : int = None -> raise LenOfArray | Some e -> begin match constFold true e with - | Const(CInt64(ni, _, _)) when ni >= Int64.zero -> - i64_to_int ni + | Const(CInt64(ni, _, _)) when compare_cilint ni zero_cilint >= 0 -> + cilint_to_int ni | e -> raise LenOfArray end @@ -6101,7 +6094,7 @@ let lenOfArray (eo: exp option) : int = (*** Make an initializer for zeroe-ing a data type ***) let rec makeZeroInit (t: typ) : init = match unrollType t with - TInt (ik, _) -> SingleInit (Const(CInt64(Int64.zero, ik, None))) + TInt (ik, _) -> SingleInit (Const(CInt64(zero_cilint, ik, None))) | TFloat(fk, _) -> SingleInit(Const(CReal(0.0, fk, None))) | TEnum (e, _) -> SingleInit (kinteger e.ekind 0) | TComp (comp, _) as t' when comp.cstruct -> @@ -6145,7 +6138,7 @@ let rec makeZeroInit (t: typ) : init = | TArray(bt, Some len, _) as t' -> let n = match constFold true len with - Const(CInt64(n, _, _)) -> i64_to_int n + Const(CInt64(n, _, _)) -> cilint_to_int n | _ -> E.s (E.unimp "Cannot understand length of array") in let initbt = makeZeroInit bt in @@ -6189,7 +6182,7 @@ let foldLeftCompound Some lene when implicit -> begin match constFold true lene with Const(CInt64(i, _, _)) -> - let len_array = i64_to_int i in + let len_array = cilint_to_int i in let len_init = List.length initl in if len_array > len_init then let zi = makeZeroInit bt in @@ -6485,7 +6478,7 @@ let caseRangeFold (l: label list) = let il, ih, ik = match constFold true el, constFold true eh with Const(CInt64(il, ilk, _)), Const(CInt64(ih, ihk, _)) -> - mkCilint ilk il, mkCilint ihk ih, commonIntKind ilk ihk + mkCilintIk ilk il, mkCilintIk ihk ih, commonIntKind ilk ihk | _ -> E.s (error "Cannot understand the constants in case range") in if compare_cilint il ih > 0 then @@ -6933,94 +6926,6 @@ let d_formatarg () = function (* These will eventually go away *) (* ------------------------------------------------------------------------- *) -(** Deprecated (can't handle large 64-bit unsigned constants - correctly) - use getInteger instead. If the given expression - is a (possibly cast'ed) character or an integer constant, return - that integer. Otherwise, return None. *) -let rec isInteger : exp -> int64 option = function - | Const(CInt64 (n,_,_)) -> Some n - | Const(CChr c) -> isInteger (Const (charConstToInt c)) (* sign-extend *) - | Const(CEnum(v, s, ei)) -> isInteger v - | CastE(_, e) -> isInteger e - | _ -> None - (** Deprecated. For compatibility with older programs, these are aliases for {!Cil.builtinFunctions} *) let gccBuiltins = builtinFunctions - -(* Deprecated. Represents an integer as for a given kind. - Returns a flag saying whether the value was changed - during truncation (because it was too large to fit in k). *) -let truncateInteger64 (k: ikind) (i: int64) : int64 * bool = - let nrBits = 8 * (bytesSizeOfInt k) in - let signed = isSigned k in - if nrBits = 64 then - i, false - else begin - let i1 = Int64.shift_left i (64 - nrBits) in - let i2 = - if signed then Int64.shift_right i1 (64 - nrBits) - else Int64.shift_right_logical i1 (64 - nrBits) - in - let truncated = - if i2 = i then false - else - (* Examine the bits that we chopped off. If they are all zero, then - * any difference between i2 and i is due to a simple sign-extension. - * e.g. casting the constant 0x80000000 to int makes it - * 0xffffffff80000000. - * Suppress the truncation warning in this case. *) - let chopped = Int64.shift_right i nrBits in - chopped <> Int64.zero - (* matth: also suppress the warning if we only chop off 1s. - This is probably due to a negative number being cast to an - unsigned value. While potentially a bug, this is almost - always what the programmer intended. *) - && chopped <> Int64.minus_one - in - i2, truncated - end - -(* Convert 2 integer constants to integers with the same type, in preparation - for a binary operation. See ISO C 6.3.1.8p1 *) -let convertInts (i1:int64) (ik1:ikind) (i2:int64) (ik2:ikind) - : int64 * int64 * ikind = - if ik1 = ik2 then (* nothing to do *) - i1, i2, ik1 - else begin - let rank : ikind -> int = function - (* these are just unique numbers representing the integer - conversion rank. *) - | IBool -> 0 - | IChar | ISChar | IUChar -> 1 - | IShort | IUShort -> 2 - | IInt | IUInt -> 3 - | ILong | IULong -> 4 - | ILongLong | IULongLong -> 5 - | IInt128 | IUInt128 -> 6 - in - let r1 = rank ik1 in - let r2 = rank ik2 in - let ik' = - if (isSigned ik1) = (isSigned ik2) then begin - (* Both signed or both unsigned. *) - if r1 > r2 then ik1 else ik2 - end - else begin - let signedKind, unsignedKind, signedRank, unsignedRank = - if isSigned ik1 then ik1, ik2, r1, r2 else ik2, ik1, r2, r1 - in - (* The rules for signed + unsigned get hairy. - (unsigned short + long) is converted to signed long, - but (unsigned int + long) is converted to unsigned long.*) - if unsignedRank >= signedRank then unsignedKind - else if (bytesSizeOfInt signedKind) > (bytesSizeOfInt unsignedKind) then - signedKind - else - unsignedVersionOf signedKind - end - in - let i1',_ = truncateInteger64 ik' i1 in - let i2',_ = truncateInteger64 ik' i2 in - i1', i2', ik' - end diff --git a/src/cil.mli b/src/cil.mli index 110efc7f6..1b33e6931 100644 --- a/src/cil.mli +++ b/src/cil.mli @@ -635,12 +635,11 @@ and exp = (** Literal constants *) and constant = - | CInt64 of int64 * ikind * string option + | CInt64 of cilint * ikind * string option (** Integer constant. Give the ikind (see ISO9899 6.1.3.2) and the * textual representation, if available. (This allows us to print a * constant as, for example, 0xF instead of 15.) Use {!Cil.integer} or - * {!Cil.kinteger} to create these. Watch out for integers that cannot be - * represented on 64 bits. OCAML does not give Overflow exceptions. *) + * {!Cil.kinteger} to create these. *) | CStr of string (** String constant. The escape characters inside the string have been * already interpreted. This constant has pointer to character type! The @@ -1110,7 +1109,7 @@ and location = { * the formal arguments are given the same signature. Also, [TNamed] * constructors are unrolled. *) and typsig = - TSArray of typsig * int64 option * attribute list + TSArray of typsig * cilint option * attribute list | TSPtr of typsig * attribute list | TSComp of bool * string * attribute list | TSFun of typsig * typsig list option * bool * attribute list @@ -2570,6 +2569,8 @@ val intKindForValue: cilint -> bool -> ikind * constant. *) val mkCilint : ikind -> int64 -> cilint +val mkCilintIk : ikind -> cilint -> cilint + (** The size of a type, in bytes. Returns a constant expression or a * "sizeof" expression if it cannot compute the size. This function * is architecture dependent, so you should only call this after you @@ -2688,20 +2689,6 @@ val envMachine : Machdep.mach option ref (* These will eventually go away *) (* ------------------------------------------------------------------------- *) -(** @deprecated. Convert two int64/kind pairs to a common int64/int64/kind triple. *) -val convertInts: int64 -> ikind -> int64 -> ikind -> int64 * int64 * ikind - -(** @deprecated. Can't handle large 64-bit unsigned constants - correctly - use getInteger instead. If the given expression - is a (possibly cast'ed) character or an integer constant, return - that integer. Otherwise, return None. *) -val isInteger: exp -> int64 option - -(** @deprecated. Use truncateCilint instead. Represents an integer as - * for a given kind. Returns a flag saying whether the value was - * changed during truncation (because it was too large to fit in k). *) -val truncateInteger64: ikind -> int64 -> int64 * bool - -(** @deprecated. For compatibility with older programs, these are - aliases for {!Cil.builtinFunctions} *) +(** @deprecated. For compatibility with older programs, this is an + alias for {!Cil.builtinFunctions} *) val gccBuiltins: (string, typ * typ list * bool) Hashtbl.t diff --git a/src/cilint.ml b/src/cilint.ml index 6f5c3d423..eaa8b3e35 100644 --- a/src/cilint.ml +++ b/src/cilint.ml @@ -19,6 +19,7 @@ type truncation = NoTruncation | ValueTruncation | BitTruncation let zero_cilint = zero_big_int let one_cilint = unit_big_int +let mone_cilint = minus_big_int unit_big_int (* Precompute useful big_ints *) let b30 = power_int_positive_int 2 30 diff --git a/src/cilint.mli b/src/cilint.mli index fea83976b..d142b3baf 100644 --- a/src/cilint.mli +++ b/src/cilint.mli @@ -11,6 +11,9 @@ val zero_cilint : cilint (** 1 as a cilint *) val one_cilint : cilint +(** -1 as a cilint *) +val mone_cilint : cilint + (** Result type for truncate_... functions *) type truncation = NoTruncation | ValueTruncation | BitTruncation diff --git a/src/ext/zrapp/rmciltmps.ml b/src/ext/zrapp/rmciltmps.ml index 885bbd504..cdf02bd3e 100644 --- a/src/ext/zrapp/rmciltmps.ml +++ b/src/ext/zrapp/rmciltmps.ml @@ -3,7 +3,7 @@ others must wait until pretty printing *) open Cil - +open Cilint module E = Errormsg module RD = Reachingdefs module AELV = Availexpslv @@ -287,15 +287,15 @@ let ok_to_replace_with_incdec curiosh defiosh f id vi r = let inc_or_dec e vi = match e with BinOp((PlusA|PlusPI|IndexPI), Lval(Var vi', NoOffset), - Const(CInt64(one,_,_)),_) -> - if vi.vid = vi'.vid && one = Int64.one + Const(CInt64(a,_,_)),_) -> + if vi.vid = vi'.vid && compare_cilint a one_cilint = 0 then Some(PlusA) - else if vi.vid = vi'.vid && one = Int64.minus_one + else if vi.vid = vi'.vid && compare_cilint a mone_cilint = 0 then Some(MinusA) else None | BinOp((MinusA|MinusPI), Lval(Var vi', NoOffset), - Const(CInt64(one,_,_)),_) -> - if vi.vid = vi'.vid && one = Int64.one + Const(CInt64(a,_,_)),_) -> + if vi.vid = vi'.vid && compare_cilint a one_cilint = 0 then Some(MinusA) else None | _ -> None diff --git a/src/formatparse.mly b/src/formatparse.mly index 1f71f15bc..5bca0631b 100644 --- a/src/formatparse.mly +++ b/src/formatparse.mly @@ -552,7 +552,7 @@ constant: fun e -> match e with Const(CInt64(n, _, _)) -> - Some [ Fd (Int64.to_int n) ] + Some [ Fd (Cilint.int_of_cilint n) ] | _ -> None) } diff --git a/src/frontc/cabs2cil.ml b/src/frontc/cabs2cil.ml index b5e45a161..b4f8bde43 100644 --- a/src/frontc/cabs2cil.ml +++ b/src/frontc/cabs2cil.ml @@ -222,20 +222,20 @@ let isVariadicListType t = * values, turn it into a CIL constant. Multi-character constants are * treated as multi-digit numbers with radix given by the bit width of * the specified type (either char or wchar_t). *) -let reduce_multichar typ : int64 list -> int64 = +let reduce_multichar typ = let radix = bitsSizeOf typ in List.fold_left - (fun acc -> Int64.add (Int64.shift_left acc radix)) - Int64.zero + (fun acc v -> add_cilint (shift_left_cilint acc radix) @@ (cilint_of_int64 v)) + zero_cilint let interpret_character_constant char_list = let value = reduce_multichar charType char_list in - if value < (Int64.of_int 256) then + if compare_cilint value (cilint_of_int 256) < 0 then (* ISO C 6.4.4.4.10: single-character constants have type int *) - (CChr(Char.chr (Int64.to_int value))), intType + (CChr(Char.chr (cilint_to_int value))), intType else begin let orig_rep = None (* Some("'" ^ (String.escaped str) ^ "'") *) in - if value <= (Int64.of_int32 Int32.max_int) then + if compare_cilint value (cilint_of_int64 (Int64.of_int32 Int32.max_int)) <= 0 then (CInt64(value,IULong,orig_rep)),(TInt(IULong,[])) else (CInt64(value,IULongLong,orig_rep)),(TInt(IULongLong,[])) (* 128bit constants are only supported if long long is also 128bit wide *) @@ -1439,7 +1439,7 @@ let checkBool (ot : typ) (e : exp) : bool = is it a nonzero constant? *) let rec isConstTrue (e:exp): bool = match e with - | Const(CInt64 (n,_,_)) -> n <> Int64.zero + | Const(CInt64 (n,_,_)) -> not (is_zero_cilint n) | Const(CChr c) -> 0 <> Char.code c | Const(CStr _ | CWStr _) -> true | Const(CReal(f, _, _)) -> f <> 0.0; @@ -1451,7 +1451,7 @@ let rec isConstTrue (e:exp): bool = On constant expressions, either isConstTrue or isConstFalse will hold. *) let rec isConstFalse (e:exp): bool = match e with - | Const(CInt64 (n,_,_)) -> n = Int64.zero + | Const(CInt64 (n,_,_)) -> is_zero_cilint n | Const(CChr c) -> 0 = Char.code c | Const(CReal(f, _, _)) -> f = 0.0; | CastE(_, e) -> isConstFalse e @@ -1933,7 +1933,7 @@ let rec setOneInit (this: preInit) let idx, (* Index in the current comp *) restoff (* Rest offset *) = match o with - | Index(Const(CInt64(i,_,_)), off) -> i64_to_int i, off + | Index(Const(CInt64(i,_,_)), off) -> cilint_to_int i, off | Field (f, off) -> (* Find the index of the field *) let rec loop (idx: int) = function @@ -1995,8 +1995,8 @@ let rec collectInitializer match leno with Some len -> begin match constFold true len with - Const(CInt64(ni, _, _)) when ni >= 0L -> - (i64_to_int ni), TArray(bt,leno,at) + Const(CInt64(ni, _, _)) when compare_cilint ni zero_cilint >= 0 -> + (cilint_to_int ni), TArray(bt,leno,at) | _ -> E.s (error "Array length is not a constant expression %a" d_exp len) @@ -2736,7 +2736,7 @@ and doAttr (a: A.attribute) : attribute list = | A.CONSTANT (A.CONST_INT str) -> begin match parseInt str with Const (CInt64 (v64,_,_)) -> - AInt (i64_to_int v64) + AInt (cilint_to_int v64) | _ -> E.s (error "Invalid attribute constant: %s") end @@ -2922,7 +2922,7 @@ and doType (nameortype: attributeClass) (* This is AttrName if we are doing match constFold true len' with | Const(CInt64(i, ik, _)) -> (* If len' is a constant, we check that the array size is non-negative *) - let elems = mkCilint ik i in + let elems = mkCilintIk ik i in if compare_cilint elems zero_cilint < 0 then E.s (error "Length of array is negative") else @@ -3535,7 +3535,7 @@ and doExp (asconst: bool) (* This expression is used as a constant *) * L'c'). But gcc allows L'abc', so I'll leave this here in case * I'm missing some architecture dependent behavior. *) let value = reduce_multichar !wcharType char_list in - let result = kinteger64 !wcharKind value in + let result = kintegerCilint !wcharKind value in finishExp empty result (typeOf result) | A.CONST_FLOAT str -> begin @@ -3786,7 +3786,7 @@ and doExp (asconst: bool) (* This expression is used as a constant *) let tres = integralPromotion t in let e'' = match e', tres with - | Const(CInt64(i, _, _)), TInt(ik, _) -> kinteger64 ik (Int64.neg i) + | Const(CInt64(i, _, _)), TInt(ik, _) -> kintegerCilint ik (neg_cilint i) | _ -> UnOp(Neg, makeCastT ~e:e' ~oldt:t ~newt:tres, tres) in finishExp se e'' tres @@ -4455,11 +4455,11 @@ and doExp (asconst: bool) (* This expression is used as a constant *) (match !pargs with [ ptr; typ ] -> begin match constFold true typ with - | Const (CInt64 (0L,_,_)) | Const (CInt64 (1L,_,_)) -> + | Const (CInt64 (a,_,_)) when is_zero_cilint a || compare_cilint one_cilint a = 0 -> piscall := false; pres := kinteger !kindOfSizeOf (-1); prestype := !typeOfSizeOf - | Const (CInt64 (2L,_,_)) | Const (CInt64 (3L,_,_)) -> + | Const (CInt64 (a,_,_)) when compare_cilint (cilint_of_int 2) a = 0 || compare_cilint (cilint_of_int 3) a = 0 -> piscall := false; pres := kinteger !kindOfSizeOf 0; prestype := !typeOfSizeOf @@ -5006,8 +5006,8 @@ and compileCondExp (ce: condExpRes) (st: chunk) (sf: chunk) : chunk = | CEExp (se, e) -> begin match e with - Const(CInt64(i,_,_)) when i <> Int64.zero && canDrop sf -> se @@ st - | Const(CInt64(z,_,_)) when z = Int64.zero && canDrop st -> se @@ sf + Const(CInt64(i,_,_)) when not (is_zero_cilint i) && canDrop sf -> se @@ st + | Const(CInt64(z,_,_)) when is_zero_cilint z && canDrop st -> se @@ sf | _ -> se @@ ifChunk e !currentLoc !currentExpLoc st sf end @@ -5406,7 +5406,7 @@ and doInit let (doidx, idxe', _) = doExp true idx (AExp(Some intType)) in match constFold true idxe', isNotEmpty doidx with - Const(CInt64(x, _, _)), false -> i64_to_int x, doidx + Const(CInt64(x, _, _)), false -> cilint_to_int x, doidx | _ -> E.s (error "INDEX initialization designator is not a constant") in @@ -5443,7 +5443,7 @@ and doInit match constFold true idxs', constFold true idxe' with Const(CInt64(s, _, _)), Const(CInt64(e, _, _)) -> - i64_to_int s, i64_to_int e + cilint_to_int s, cilint_to_int e | _ -> E.s (error "INDEX_RANGE initialization designator is not a constant") in @@ -6378,7 +6378,7 @@ and assignInit (lv: lval) match leno with Some len -> begin match constFold true len with - Const(CInt64(ni, _, _)) when ni >= 0L -> + Const(CInt64(ni, _, _)) when compare_cilint ni zero_cilint >= 0 -> (* Write any initializations in initl using one instruction per element. *) let b = foldLeftCompound @@ -6389,14 +6389,14 @@ and assignInit (lv: lval) ~initl:initl ~acc:acc in let ilen = List.length initl in - if ilen >= i64_to_int ni then + if ilen >= cilint_to_int ni then (* There are no remaining initializations *) b else (* Use a loop for any remaining initializations *) let ctrv = newTempVar (text "init counter") true uintType in let ctrlval = Var ctrv, NoOffset in - let init = Set(ctrlval, Const(CInt64(Int64.of_int ilen, IUInt, None)), !currentLoc, !currentExpLoc) in + let init = Set(ctrlval, Const(CInt64(cilint_of_int ilen, IUInt, None)), !currentLoc, !currentExpLoc) in startLoop false; let bodyc = let ifc = @@ -6406,7 +6406,7 @@ and assignInit (lv: lval) in let dest = addOffsetLval (Index(Lval ctrlval, NoOffset)) lv in let assignc = assignInit dest (makeZeroInit bt) bt empty in - let inci = Set(ctrlval, BinOp(PlusA, Lval ctrlval, Const(CInt64(1L, IUInt, None)), uintType), !currentLoc, !currentExpLoc) in + let inci = Set(ctrlval, BinOp(PlusA, Lval ctrlval, Const(CInt64(one_cilint, IUInt, None)), uintType), !currentLoc, !currentExpLoc) in (ifc @@ assignc) +++ inci in exitLoop (); let loopc = loopChunk bodyc in diff --git a/src/mergecil.ml b/src/mergecil.ml index 3198e49e3..02b90f1e7 100644 --- a/src/mergecil.ml +++ b/src/mergecil.ml @@ -1247,7 +1247,7 @@ begin ( (* CIL changes (unsigned)0 into 0U during printing.. *) match xc,yc with - | CInt64(0L,_,_),CInt64(0L,_,_) -> true (* ok if they're both 0 *) + | CInt64(a,_,_),CInt64(b,_,_) when Cilint.is_zero_cilint a && Cilint.is_zero_cilint b -> true (* ok if they're both 0 *) | _,_ -> false ) | Lval(xl), Lval(yl) -> (equalLvals xl yl) From d3ca4e7f1847d019cad3dabcecb9473064b5d7a8 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Wed, 1 Dec 2021 14:12:08 +0100 Subject: [PATCH 05/15] Rename CInt64 -> CInt --- src/check.ml | 2 +- src/cil.ml | 56 +++++++++++++++++++------------------- src/cil.mli | 6 ++-- src/ext/zrapp/rmciltmps.ml | 4 +-- src/formatparse.mly | 8 +++--- src/frontc/cabs2cil.ml | 52 +++++++++++++++++------------------ src/mergecil.ml | 6 ++-- 7 files changed, 67 insertions(+), 67 deletions(-) diff --git a/src/check.ml b/src/check.ml index 96cdfac2c..5c4801b4e 100644 --- a/src/check.ml +++ b/src/check.ml @@ -652,7 +652,7 @@ and checkInit (i: init) : typ = if i > len then ignore (warn "Wrong number of initializers in array") - | (Index(Const(CInt64(i', _, _)), NoOffset), ei) :: rest -> + | (Index(Const(CInt(i', _, _)), NoOffset), ei) :: rest -> if Int64.compare (Z.to_int64 i') i <> 0 then ignore (warn "Initializer for index %s when %s was expected" (Int64.format "%d" (Z.to_int64 i')) (Int64.format "%d" i)); diff --git a/src/cil.ml b/src/cil.ml index eb0c1f0a3..e6168ca61 100755 --- a/src/cil.ml +++ b/src/cil.ml @@ -543,7 +543,7 @@ and exp = (** Literal constants *) and constant = - | CInt64 of cilint * ikind * string option + | CInt of cilint * ikind * string option (** Integer constant. Give the ikind (see ISO9899 6.1.3.2) * and the textual representation, if available. Use * {!Cil.integer} or {!Cil.kinteger} to create these. *) @@ -1239,12 +1239,12 @@ let warnLoc (loc: location) (fmt : ('a,unit,doc) format) : 'a = in Pretty.gprintf f fmt -let zero = Const(CInt64(zero_cilint, IInt, None)) +let zero = Const(CInt(zero_cilint, IInt, None)) (** Given the character c in a (CChr c), sign-extend it to 32 bits. (This is the official way of interpreting character constants, according to ISO C 6.4.4.4.10, which says that character constants are chars cast to ints) - Returns CInt64(sign-extended c, IInt, None) *) + Returns CInt(sign-extended c, IInt, None) *) let charConstToInt (c: char) : constant = let c' = Char.code c in let value = @@ -1252,7 +1252,7 @@ let charConstToInt (c: char) : constant = then cilint_of_int c' else cilint_of_int (c' - 256) in - CInt64(value, IInt, None) + CInt(value, IInt, None) (** Convert a 64-bit int to an OCaml int, or raise an exception if that @@ -1733,8 +1733,8 @@ let bytesSizeOfInt (ik: ikind): int = (* constant *) let d_const () c = match c with - CInt64(_, _, Some s) -> text s (* Always print the text if there is one *) - | CInt64(i, ik, None) -> + CInt(_, _, Some s) -> text s (* Always print the text if there is one *) + | CInt(i, ik, None) -> (* We must make sure to capture the type of the constant. For some * constants this is done with a suffix, for others with a cast prefix.*) let suffix : string = @@ -1901,7 +1901,7 @@ let isFunctionType t = (**** Compute the type of an expression ****) let rec typeOf (e: exp) : typ = match e with - | Const(CInt64 (_, ik, _)) -> TInt(ik, []) + | Const(CInt (_, ik, _)) -> TInt(ik, []) (* Character constants have type int. ISO/IEC 9899:1999 (E), * section 6.4.4.4 [Character constants], paragraph 10, if you @@ -2090,7 +2090,7 @@ let kintegerCilint (k: ikind) (i: cilint) : exp = if truncated = BitTruncation && !warnTruncate then ignore (warnOpt "Truncating integer %s to %s" (string_of_cilint i) (string_of_cilint i')); - Const (CInt64(i', k, None)) + Const (CInt(i', k, None)) (* Construct an integer constant with possible truncation *) let kinteger64 (k: ikind) (i: int64) : exp = @@ -2138,7 +2138,7 @@ let intKindForValue (i: cilint) (unsigned: bool) = Otherwise return None. *) let rec getInteger (e:exp) : cilint option = match e with - | Const(CInt64 (n, ik, _)) -> Some (mkCilintIk ik n) + | Const(CInt (n, ik, _)) -> Some (mkCilintIk ik n) | Const(CChr c) -> getInteger (Const (charConstToInt c)) | Const(CEnum(v, _, _)) -> getInteger v | CastE(t, e) -> begin @@ -2402,7 +2402,7 @@ and bitsSizeOf t = | TArray(bt, Some len, _) -> begin match constFold true len with - Const(CInt64(l,lk,_)) -> + Const(CInt(l,lk,_)) -> let sz = mul_cilint (mkCilintIk lk l) (cilint_of_int (bitsSizeOf bt)) in (* Check for overflow. There are other places in these cil.ml that overflow can occur, @@ -2500,7 +2500,7 @@ and constFold (machdep: bool) (e: exp) : exp = | _ -> raise Not_found (* probably a float *) in match constFold machdep e1 with - Const(CInt64(i,ik,_)) -> begin + Const(CInt(i,ik,_)) -> begin let ic = mkCilintIk ik i in match unop with Neg -> kintegerCilint tk (neg_cilint ic) @@ -2547,12 +2547,12 @@ and constFold (machdep: bool) (e: exp) : exp = | CastE (t, e) -> begin match constFold machdep e, unrollType t with (* Might truncate silently *) - | Const(CInt64(i,k,_)), TInt(nk,a) + | Const(CInt(i,k,_)), TInt(nk,a) (* It's okay to drop a cast to const. If the cast has any other attributes, leave the cast alone. *) when (dropAttributes ["const"] a) = [] -> let i', _ = truncateCilint nk (mkCilintIk k i) in - Const(CInt64(i', nk, None)) + Const(CInt(i', nk, None)) | e', _ -> CastE (t, e') end | Lval lv -> Lval (constFoldLval machdep lv) @@ -3501,20 +3501,20 @@ class defaultCilPrinterClass : cilPrinter = object (self) | Set(lv,e,l,el) -> begin (* Be nice to some special cases *) match e with - BinOp((PlusA|PlusPI|IndexPI),Lval(lv'),Const(CInt64(one,_,_)),_) + BinOp((PlusA|PlusPI|IndexPI),Lval(lv'),Const(CInt(one,_,_)),_) when Util.equals lv lv' && compare_cilint one one_cilint = 0 && not !printCilAsIs -> self#pLineDirective l ++ self#pLvalPrec indexLevel () lv ++ text (" ++" ^ printInstrTerminator) | BinOp((MinusA|MinusPI),Lval(lv'), - Const(CInt64(one,_,_)), _) + Const(CInt(one,_,_)), _) when Util.equals lv lv' && compare_cilint one one_cilint = 0 && not !printCilAsIs -> self#pLineDirective l ++ self#pLvalPrec indexLevel () lv ++ text (" --" ^ printInstrTerminator) - | BinOp((PlusA|PlusPI|IndexPI),Lval(lv'),Const(CInt64(mone,_,_)),_) + | BinOp((PlusA|PlusPI|IndexPI),Lval(lv'),Const(CInt(mone,_,_)),_) when Util.equals lv lv' && compare_cilint mone mone_cilint = 0 && not !printCilAsIs -> self#pLineDirective l @@ -4596,7 +4596,7 @@ class plainCilPrinterClass = Const(c) -> let d_plainconst () c = match c with - CInt64(i, ik, so) -> + CInt(i, ik, so) -> let fmt = if isSigned ik then "%d" else "%x" in dprintf "Int64(%s,%a,%s)" (Z.format fmt i) @@ -5796,7 +5796,7 @@ let dumpFile (pp: cilPrinter) (out : out_channel) (outfile: string) file = exception NotAnAttrParam of exp let rec expToAttrParam (e: exp) : attrparam = match e with - Const(CInt64(i,k,_)) -> + Const(CInt(i,k,_)) -> let i' = mkCilintIk k i in if not (is_int_cilint i') then raise (NotAnAttrParam e); @@ -5914,7 +5914,7 @@ let rec typeSigWithAttrs ?(ignoreSign=false) doattr t = match l with Some l -> begin match constFold true l with - Const(CInt64(i, _, _)) -> Some i + Const(CInt(i, _, _)) -> Some i | e -> None (* Returning None for length in a typesig if the length is not a constant (VLA) *) end | None -> None @@ -6028,11 +6028,11 @@ let mkCastT ~(e: exp) ~(oldt: typ) ~(newt: typ) = (* Watch out for constants *) match newt, e with (* Casts to _Bool are special: they behave like "!= 0" ISO C99 6.3.1.2 *) - TInt(IBool, []), Const(CInt64(i, _, _)) -> + TInt(IBool, []), Const(CInt(i, _, _)) -> let v = if compare i zero_cilint = 0 then zero_cilint else one_cilint in - Const (CInt64(v, IBool, None)) - | TInt(newik, []), Const(CInt64(_, _, Some s)) -> kintegerCilint newik (Cilint.cilint_of_string s) - | TInt(newik, []), Const(CInt64(i, _, None)) -> kintegerCilint newik i + Const (CInt(v, IBool, None)) + | TInt(newik, []), Const(CInt(_, _, Some s)) -> kintegerCilint newik (Cilint.cilint_of_string s) + | TInt(newik, []), Const(CInt(i, _, None)) -> kintegerCilint newik i | _ -> CastE(newt,e) end @@ -6085,7 +6085,7 @@ let lenOfArray (eo: exp option) : int = None -> raise LenOfArray | Some e -> begin match constFold true e with - | Const(CInt64(ni, _, _)) when compare_cilint ni zero_cilint >= 0 -> + | Const(CInt(ni, _, _)) when compare_cilint ni zero_cilint >= 0 -> cilint_to_int ni | e -> raise LenOfArray end @@ -6094,7 +6094,7 @@ let lenOfArray (eo: exp option) : int = (*** Make an initializer for zeroe-ing a data type ***) let rec makeZeroInit (t: typ) : init = match unrollType t with - TInt (ik, _) -> SingleInit (Const(CInt64(zero_cilint, ik, None))) + TInt (ik, _) -> SingleInit (Const(CInt(zero_cilint, ik, None))) | TFloat(fk, _) -> SingleInit(Const(CReal(0.0, fk, None))) | TEnum (e, _) -> SingleInit (kinteger e.ekind 0) | TComp (comp, _) as t' when comp.cstruct -> @@ -6138,7 +6138,7 @@ let rec makeZeroInit (t: typ) : init = | TArray(bt, Some len, _) as t' -> let n = match constFold true len with - Const(CInt64(n, _, _)) -> cilint_to_int n + Const(CInt(n, _, _)) -> cilint_to_int n | _ -> E.s (E.unimp "Cannot understand length of array") in let initbt = makeZeroInit bt in @@ -6181,7 +6181,7 @@ let foldLeftCompound match leno with Some lene when implicit -> begin match constFold true lene with - Const(CInt64(i, _, _)) -> + Const(CInt(i, _, _)) -> let len_array = cilint_to_int i in let len_init = List.length initl in if len_array > len_init then @@ -6477,7 +6477,7 @@ let caseRangeFold (l: label list) = | CaseRange(el, eh, loc, eloc) :: xs -> let il, ih, ik = match constFold true el, constFold true eh with - Const(CInt64(il, ilk, _)), Const(CInt64(ih, ihk, _)) -> + Const(CInt(il, ilk, _)), Const(CInt(ih, ihk, _)) -> mkCilintIk ilk il, mkCilintIk ihk ih, commonIntKind ilk ihk | _ -> E.s (error "Cannot understand the constants in case range") in diff --git a/src/cil.mli b/src/cil.mli index 1b33e6931..7ad9548e3 100644 --- a/src/cil.mli +++ b/src/cil.mli @@ -635,7 +635,7 @@ and exp = (** Literal constants *) and constant = - | CInt64 of cilint * ikind * string option + | CInt of cilint * ikind * string option (** Integer constant. Give the ikind (see ISO9899 6.1.3.2) and the * textual representation, if available. (This allows us to print a * constant as, for example, 0xF instead of 15.) Use {!Cil.integer} or @@ -1647,7 +1647,7 @@ val isNullPtrConstant: exp -> bool (** Given the character c in a (CChr c), sign-extend it to 32 bits. (This is the official way of interpreting character constants, according to ISO C 6.4.4.4.10, which says that character constants are chars cast to ints) - Returns CInt64(sign-extended c, IInt, None) *) + Returns CInt(sign-extended c, IInt, None) *) val charConstToInt: char -> constant (** Do constant folding on an expression. If the first argument is true then @@ -2565,7 +2565,7 @@ val fitsInInt: ikind -> cilint -> bool val intKindForValue: cilint -> bool -> ikind (** Construct a cilint from an integer kind and int64 value. Used for - * getting the actual constant value from a CInt64(n, ik, _) + * getting the actual constant value from a CInt(n, ik, _) * constant. *) val mkCilint : ikind -> int64 -> cilint diff --git a/src/ext/zrapp/rmciltmps.ml b/src/ext/zrapp/rmciltmps.ml index cdf02bd3e..4af909fc6 100644 --- a/src/ext/zrapp/rmciltmps.ml +++ b/src/ext/zrapp/rmciltmps.ml @@ -287,14 +287,14 @@ let ok_to_replace_with_incdec curiosh defiosh f id vi r = let inc_or_dec e vi = match e with BinOp((PlusA|PlusPI|IndexPI), Lval(Var vi', NoOffset), - Const(CInt64(a,_,_)),_) -> + Const(CInt(a,_,_)),_) -> if vi.vid = vi'.vid && compare_cilint a one_cilint = 0 then Some(PlusA) else if vi.vid = vi'.vid && compare_cilint a mone_cilint = 0 then Some(MinusA) else None | BinOp((MinusA|MinusPI), Lval(Var vi', NoOffset), - Const(CInt64(a,_,_)),_) -> + Const(CInt(a,_,_)),_) -> if vi.vid = vi'.vid && compare_cilint a one_cilint = 0 then Some(MinusA) else None diff --git a/src/formatparse.mly b/src/formatparse.mly index 5bca0631b..aba2abf04 100644 --- a/src/formatparse.mly +++ b/src/formatparse.mly @@ -115,7 +115,7 @@ let rec checkSameFormat (fl1: formatArg list) (fl2: formatArg list) = and checkExpEq e1 e2 = match e1, e2 with - Const(CInt64(n1, _, _)), Const(CInt64(n2, _, _)) -> n1 = n2 + Const(CInt(n1, _, _)), Const(CInt(n2, _, _)) -> n1 = n2 | Lval l1, Lval l2 -> checkLvalEq l1 l2 | UnOp(uo1, e1, _), UnOp(uo2, e2, _) -> uo1 = uo2 && checkExpEq e1 e2 @@ -551,7 +551,7 @@ constant: | a -> wrongArgType currentArg "integer" a), fun e -> match e with - Const(CInt64(n, _, _)) -> + Const(CInt(n, _, _)) -> Some [ Fd (Cilint.int_of_cilint n) ] | _ -> None) } @@ -571,8 +571,8 @@ constant: ((fun args -> n), (fun e -> match e, n with - Const(CInt64(e', _, _)), - Const(CInt64(n', _, _)) when e' = n' -> Some [] + Const(CInt(e', _, _)), + Const(CInt(n', _, _)) when e' = n' -> Some [] | _ -> None)) } ; diff --git a/src/frontc/cabs2cil.ml b/src/frontc/cabs2cil.ml index b4f8bde43..6fd0463c2 100644 --- a/src/frontc/cabs2cil.ml +++ b/src/frontc/cabs2cil.ml @@ -236,9 +236,9 @@ let interpret_character_constant char_list = else begin let orig_rep = None (* Some("'" ^ (String.escaped str) ^ "'") *) in if compare_cilint value (cilint_of_int64 (Int64.of_int32 Int32.max_int)) <= 0 then - (CInt64(value,IULong,orig_rep)),(TInt(IULong,[])) + (CInt(value,IULong,orig_rep)),(TInt(IULong,[])) else - (CInt64(value,IULongLong,orig_rep)),(TInt(IULongLong,[])) (* 128bit constants are only supported if long long is also 128bit wide *) + (CInt(value,IULongLong,orig_rep)),(TInt(IULongLong,[])) (* 128bit constants are only supported if long long is also 128bit wide *) end (*** EXPRESSIONS *************) @@ -1038,7 +1038,7 @@ module BlockChunk = let constFold = constFold false in let e'' = if !lowerConstants then constFold e' else e' in begin match (constFold e), (constFold e'') with - | Const(CInt64(i1, _, _)), Const(CInt64(i2, _, _)) + | Const(CInt(i1, _, _)), Const(CInt(i2, _, _)) when i1 <> i2 -> ignore (warnOpt "Case label %a exceeds range for switch expression" d_exp e); @@ -1439,7 +1439,7 @@ let checkBool (ot : typ) (e : exp) : bool = is it a nonzero constant? *) let rec isConstTrue (e:exp): bool = match e with - | Const(CInt64 (n,_,_)) -> not (is_zero_cilint n) + | Const(CInt (n,_,_)) -> not (is_zero_cilint n) | Const(CChr c) -> 0 <> Char.code c | Const(CStr _ | CWStr _) -> true | Const(CReal(f, _, _)) -> f <> 0.0; @@ -1451,7 +1451,7 @@ let rec isConstTrue (e:exp): bool = On constant expressions, either isConstTrue or isConstFalse will hold. *) let rec isConstFalse (e:exp): bool = match e with - | Const(CInt64 (n,_,_)) -> is_zero_cilint n + | Const(CInt (n,_,_)) -> is_zero_cilint n | Const(CChr c) -> 0 = Char.code c | Const(CReal(f, _, _)) -> f = 0.0; | CastE(_, e) -> isConstFalse e @@ -1933,7 +1933,7 @@ let rec setOneInit (this: preInit) let idx, (* Index in the current comp *) restoff (* Rest offset *) = match o with - | Index(Const(CInt64(i,_,_)), off) -> cilint_to_int i, off + | Index(Const(CInt(i,_,_)), off) -> cilint_to_int i, off | Field (f, off) -> (* Find the index of the field *) let rec loop (idx: int) = function @@ -1995,7 +1995,7 @@ let rec collectInitializer match leno with Some len -> begin match constFold true len with - Const(CInt64(ni, _, _)) when compare_cilint ni zero_cilint >= 0 -> + Const(CInt(ni, _, _)) when compare_cilint ni zero_cilint >= 0 -> (cilint_to_int ni), TArray(bt,leno,at) | _ -> E.s (error "Array length is not a constant expression %a" @@ -2735,7 +2735,7 @@ and doAttr (a: A.attribute) : attribute list = | A.CONSTANT (A.CONST_STRING s) -> AStr s | A.CONSTANT (A.CONST_INT str) -> begin match parseInt str with - Const (CInt64 (v64,_,_)) -> + Const (CInt (v64,_,_)) -> AInt (cilint_to_int v64) | _ -> E.s (error "Invalid attribute constant: %s") @@ -2920,7 +2920,7 @@ and doType (nameortype: attributeClass) (* This is AttrName if we are doing E.s (error "Array length %a does not have an integral type.") else match constFold true len' with - | Const(CInt64(i, ik, _)) -> + | Const(CInt(i, ik, _)) -> (* If len' is a constant, we check that the array size is non-negative *) let elems = mkCilintIk ik i in if compare_cilint elems zero_cilint < 0 then @@ -3234,7 +3234,7 @@ and getIntConstExp (aexp) : exp = E.s (error "Constant expression %a has effects" d_exp e); match e with (* first, filter for those Const exps that are integers *) - | Const (CInt64 _ ) -> e + | Const (CInt _ ) -> e | Const (CEnum _) -> e | Const (CChr i) -> Const(charConstToInt i) @@ -3484,7 +3484,7 @@ and doExp (asconst: bool) (* This expression is used as a constant *) match s with [] -> [] | wc::rest -> - let wc_cilexp = Const (CInt64(wc, IInt, None)) in + let wc_cilexp = Const (CInt(wc, IInt, None)) in (Index(integer idx, NoOffset), SingleInit (makeCast wc_cilexp wchar_t)) :: loop (idx + 1) rest @@ -3786,7 +3786,7 @@ and doExp (asconst: bool) (* This expression is used as a constant *) let tres = integralPromotion t in let e'' = match e', tres with - | Const(CInt64(i, _, _)), TInt(ik, _) -> kintegerCilint ik (neg_cilint i) + | Const(CInt(i, _, _)), TInt(ik, _) -> kintegerCilint ik (neg_cilint i) | _ -> UnOp(Neg, makeCastT ~e:e' ~oldt:t ~newt:tres, tres) in finishExp se e'' tres @@ -4455,11 +4455,11 @@ and doExp (asconst: bool) (* This expression is used as a constant *) (match !pargs with [ ptr; typ ] -> begin match constFold true typ with - | Const (CInt64 (a,_,_)) when is_zero_cilint a || compare_cilint one_cilint a = 0 -> + | Const (CInt (a,_,_)) when is_zero_cilint a || compare_cilint one_cilint a = 0 -> piscall := false; pres := kinteger !kindOfSizeOf (-1); prestype := !typeOfSizeOf - | Const (CInt64 (a,_,_)) when compare_cilint (cilint_of_int 2) a = 0 || compare_cilint (cilint_of_int 3) a = 0 -> + | Const (CInt (a,_,_)) when compare_cilint (cilint_of_int 2) a = 0 || compare_cilint (cilint_of_int 3) a = 0 -> piscall := false; pres := kinteger !kindOfSizeOf 0; prestype := !typeOfSizeOf @@ -4704,8 +4704,8 @@ and doExp (asconst: bool) (* This expression is used as a constant *) let e3'' = makeCastT e3' t3' tresult in let resexp = match e1' with - Const(CInt64(i, _, _)) when i <> Int64.zero -> e2'' - | Const(CInt64(z, _, _)) when z = Int64.zero -> e3'' + Const(CInt(i, _, _)) when i <> Int64.zero -> e2'' + | Const(CInt(z, _, _)) when z = Int64.zero -> e3'' | _ -> Question(e1', e2'', e3'') in finishExp se1 resexp tresult @@ -4939,7 +4939,7 @@ and doCondExp (asconst: bool) (* Try to evaluate the conditional expression let ce1 = doCondExp asconst e1 in let ce2 = doCondExp asconst e2 in match ce1, ce2 with - CEExp (se1, (Const(CInt64 _) as ci1)), _ -> + CEExp (se1, (Const(CInt _) as ci1)), _ -> if isConstFalse ci1 then addChunkBeforeCE se1 ce2 else @@ -5006,8 +5006,8 @@ and compileCondExp (ce: condExpRes) (st: chunk) (sf: chunk) : chunk = | CEExp (se, e) -> begin match e with - Const(CInt64(i,_,_)) when not (is_zero_cilint i) && canDrop sf -> se @@ st - | Const(CInt64(z,_,_)) when is_zero_cilint z && canDrop st -> se @@ sf + Const(CInt(i,_,_)) when not (is_zero_cilint i) && canDrop sf -> se @@ st + | Const(CInt(z,_,_)) when is_zero_cilint z && canDrop st -> se @@ sf | _ -> se @@ ifChunk e !currentLoc !currentExpLoc st sf end @@ -5406,7 +5406,7 @@ and doInit let (doidx, idxe', _) = doExp true idx (AExp(Some intType)) in match constFold true idxe', isNotEmpty doidx with - Const(CInt64(x, _, _)), false -> cilint_to_int x, doidx + Const(CInt(x, _, _)), false -> cilint_to_int x, doidx | _ -> E.s (error "INDEX initialization designator is not a constant") in @@ -5441,8 +5441,8 @@ and doInit E.s (error "Range designators are not constants"); let first, last = match constFold true idxs', constFold true idxe' with - Const(CInt64(s, _, _)), - Const(CInt64(e, _, _)) -> + Const(CInt(s, _, _)), + Const(CInt(e, _, _)) -> cilint_to_int s, cilint_to_int e | _ -> E.s (error "INDEX_RANGE initialization designator is not a constant") @@ -6378,7 +6378,7 @@ and assignInit (lv: lval) match leno with Some len -> begin match constFold true len with - Const(CInt64(ni, _, _)) when compare_cilint ni zero_cilint >= 0 -> + Const(CInt(ni, _, _)) when compare_cilint ni zero_cilint >= 0 -> (* Write any initializations in initl using one instruction per element. *) let b = foldLeftCompound @@ -6396,17 +6396,17 @@ and assignInit (lv: lval) (* Use a loop for any remaining initializations *) let ctrv = newTempVar (text "init counter") true uintType in let ctrlval = Var ctrv, NoOffset in - let init = Set(ctrlval, Const(CInt64(cilint_of_int ilen, IUInt, None)), !currentLoc, !currentExpLoc) in + let init = Set(ctrlval, Const(CInt(cilint_of_int ilen, IUInt, None)), !currentLoc, !currentExpLoc) in startLoop false; let bodyc = let ifc = let ife = - BinOp(Ge, Lval ctrlval, Const(CInt64(ni, IUInt, None)), intType) in + BinOp(Ge, Lval ctrlval, Const(CInt(ni, IUInt, None)), intType) in ifChunk ife !currentLoc locUnknown (breakChunk !currentLoc) skipChunk in let dest = addOffsetLval (Index(Lval ctrlval, NoOffset)) lv in let assignc = assignInit dest (makeZeroInit bt) bt empty in - let inci = Set(ctrlval, BinOp(PlusA, Lval ctrlval, Const(CInt64(one_cilint, IUInt, None)), uintType), !currentLoc, !currentExpLoc) in + let inci = Set(ctrlval, BinOp(PlusA, Lval ctrlval, Const(CInt(one_cilint, IUInt, None)), uintType), !currentLoc, !currentExpLoc) in (ifc @@ assignc) +++ inci in exitLoop (); let loopc = loopChunk bodyc in diff --git a/src/mergecil.ml b/src/mergecil.ml index 02b90f1e7..50442ef27 100644 --- a/src/mergecil.ml +++ b/src/mergecil.ml @@ -506,7 +506,7 @@ let rec combineTypes (what: combineWhat) | Some oldsz', Some sz' -> let samesz = match constFold true oldsz', constFold true sz' with - Const(CInt64(oldi, _, _)), Const(CInt64(i, _, _)) -> oldi = i + Const(CInt(oldi, _, _)), Const(CInt(i, _, _)) -> oldi = i | _, _ -> false in if samesz then oldsz else @@ -702,7 +702,7 @@ and matchEnumInfo (oldfidx: int) (oldei: enuminfo) raise (Failure "(different names for enumeration items)"); let samev = match constFold true old_iv, constFold true iv with - Const(CInt64(oldi, _, _)), Const(CInt64(i, _, _)) -> oldi = i + Const(CInt(oldi, _, _)), Const(CInt(i, _, _)) -> oldi = i | _ -> false in if not samev then @@ -1247,7 +1247,7 @@ begin ( (* CIL changes (unsigned)0 into 0U during printing.. *) match xc,yc with - | CInt64(a,_,_),CInt64(b,_,_) when Cilint.is_zero_cilint a && Cilint.is_zero_cilint b -> true (* ok if they're both 0 *) + | CInt(a,_,_),CInt(b,_,_) when Cilint.is_zero_cilint a && Cilint.is_zero_cilint b -> true (* ok if they're both 0 *) | _,_ -> false ) | Lval(xl), Lval(yl) -> (equalLvals xl yl) From ddddac070b3a5b3c3d496b135da50b7f6c252d45 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Wed, 1 Dec 2021 15:59:25 +0100 Subject: [PATCH 06/15] typos --- src/check.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/check.ml b/src/check.ml index 5c4801b4e..4615ab528 100644 --- a/src/check.ml +++ b/src/check.ml @@ -642,7 +642,7 @@ and checkInit (i: init) : typ = | None -> 0L | Some e -> (ignore (checkExp true e); match getInteger (constFold true e) with - Some len -> Z.to_int64 len (* Z on purpose, we don;t want to ingore overflows here *) + Some len -> Z.to_int64 len (* Z on purpose, we don't want to ignore overflows here *) | None -> ignore (warn "Array length is not a constant"); 0L) From b99151a7134c76233cb4f4f0fd9868f4fcc72d0e Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Wed, 1 Dec 2021 16:07:49 +0100 Subject: [PATCH 07/15] Make pExp output consistent --- src/cil.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/cil.ml b/src/cil.ml index e6168ca61..ce72105fd 100755 --- a/src/cil.ml +++ b/src/cil.ml @@ -4598,7 +4598,7 @@ class plainCilPrinterClass = match c with CInt(i, ik, so) -> let fmt = if isSigned ik then "%d" else "%x" in - dprintf "Int64(%s,%a,%s)" + dprintf "Int(%s,%a,%s)" (Z.format fmt i) d_ikind ik (match so with Some s -> s | _ -> "None") From 9c0efdf4f9dde304f70726363964029a2a8d763a Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Wed, 1 Dec 2021 16:31:38 +0100 Subject: [PATCH 08/15] Rm polymorphic compare on cilint --- src/mergecil.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/mergecil.ml b/src/mergecil.ml index 50442ef27..e5dfe5ba4 100644 --- a/src/mergecil.ml +++ b/src/mergecil.ml @@ -506,7 +506,7 @@ let rec combineTypes (what: combineWhat) | Some oldsz', Some sz' -> let samesz = match constFold true oldsz', constFold true sz' with - Const(CInt(oldi, _, _)), Const(CInt(i, _, _)) -> oldi = i + Const(CInt(oldi, _, _)), Const(CInt(i, _, _)) -> Cilint.compare_cilint oldi i = 0 | _, _ -> false in if samesz then oldsz else @@ -702,7 +702,7 @@ and matchEnumInfo (oldfidx: int) (oldei: enuminfo) raise (Failure "(different names for enumeration items)"); let samev = match constFold true old_iv, constFold true iv with - Const(CInt(oldi, _, _)), Const(CInt(i, _, _)) -> oldi = i + Const(CInt(oldi, _, _)), Const(CInt(i, _, _)) -> Cilint.compare_cilint oldi i = 0 | _ -> false in if not samev then From f9f8e64195fc5a67f05fad51c272d0c7707e20a8 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Wed, 1 Dec 2021 16:47:08 +0100 Subject: [PATCH 09/15] Slightly less bonkers indentation --- src/cil.ml | 11 +++++------ 1 file changed, 5 insertions(+), 6 deletions(-) diff --git a/src/cil.ml b/src/cil.ml index ce72105fd..ea6214cde 100755 --- a/src/cil.ml +++ b/src/cil.ml @@ -2768,14 +2768,13 @@ let parseInt (str: string) : exp = * POSITIVE *) let res = let rec loop = function - k::rest -> - if fitsInInt k i then kintegerCilint k i - else loop rest - | [] -> E.s (E.unimp "Cannot represent the integer %s\n" - (string_of_cilint i)) + | k::rest -> + if fitsInInt k i then kintegerCilint k i + else loop rest + | [] -> E.s (E.unimp "Cannot represent the integer %s\n" (string_of_cilint i)) in loop kinds - in + in res (* with e -> begin *) (* ignore (E.log "int_of_string %s (%s)\n" str *) From 9c34b06be1efb2b3417bf2a5a5313612bf319921 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Wed, 1 Dec 2021 17:08:42 +0100 Subject: [PATCH 10/15] Simplify parseInt --- src/cil.ml | 36 ++++++++---------------------------- 1 file changed, 8 insertions(+), 28 deletions(-) diff --git a/src/cil.ml b/src/cil.ml index ea6214cde..e8c82ad63 100755 --- a/src/cil.ml +++ b/src/cil.ml @@ -2732,38 +2732,18 @@ let parseInt (str: string) : exp = b) for constants bigger than long long producing a "Unimplemented: Cannot represent the integer" warning in C99 mode vs. unsigned long long if c99mode is off. *) in - (* Convert to integer. To prevent overflow we do the arithmetic on - * cilints. We work only with positive integers since the lexer - * takes care of the sign *) - let rec toInt (base: cilint) (acc: cilint) (idx: int) : cilint = - let doAcc (what: int) = - let acc' = add_cilint (mul_cilint base acc) (cilint_of_int what) in - toInt base acc' (idx + 1) - in - if idx >= l - suffixlen then begin - acc - end else - let ch = String.get str idx in - if ch >= '0' && ch <= '9' then - doAcc (Char.code ch - Char.code '0') - else if ch >= 'a' && ch <= 'f' then - doAcc (10 + Char.code ch - Char.code 'a') - else if ch >= 'A' && ch <= 'F' then - doAcc (10 + Char.code ch - Char.code 'A') - else - E.s (bug "Invalid integer constant: %s (char %c at idx=%d)" - str ch idx) - in - let i = + let start, base = if octalhex then - if l >= 2 && - (let c = String.get str 1 in c = 'x' || c = 'X') then - toInt (cilint_of_int 16) zero_cilint 2 + if l >= 2 && (let c = String.get str 1 in c = 'x' || c = 'X') then + 2, 16 else - toInt (cilint_of_int 8) zero_cilint 1 + 1, 8 else - toInt (cilint_of_int 10) zero_cilint 0 + 0, 10 in + let t = String.sub str start (String.length str - start - suffixlen) in + (* Normal Z.of_string does not work here as 0 is not recognized as the prefix for octal here *) + let i = Z.of_string_base base t in (* Construct an integer of the first kinds that fits. i must be * POSITIVE *) let res = From 5fcf2dd06f9447095fe4f5eae5f7192778edb5af Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Wed, 1 Dec 2021 17:28:54 +0100 Subject: [PATCH 11/15] Output string in parseInt --- src/cil.ml | 12 +++++++----- 1 file changed, 7 insertions(+), 5 deletions(-) diff --git a/src/cil.ml b/src/cil.ml index e8c82ad63..b93d87b0b 100755 --- a/src/cil.ml +++ b/src/cil.ml @@ -2085,12 +2085,15 @@ let mkCilint (ik:ikind) (i:int64) : cilint = (* Construct an integer constant with possible truncation *) -let kintegerCilint (k: ikind) (i: cilint) : exp = +let kintegerCilintString (k: ikind) (i: cilint) (s:string option): exp = let i', truncated = truncateCilint k i in if truncated = BitTruncation && !warnTruncate then ignore (warnOpt "Truncating integer %s to %s" (string_of_cilint i) (string_of_cilint i')); - Const (CInt(i', k, None)) + Const (CInt(i', k, s)) + +let kintegerCilint (k: ikind) (i: cilint) : exp = + kintegerCilintString k i None (* Construct an integer constant with possible truncation *) let kinteger64 (k: ikind) (i: int64) : exp = @@ -2749,7 +2752,7 @@ let parseInt (str: string) : exp = let res = let rec loop = function | k::rest -> - if fitsInInt k i then kintegerCilint k i + if fitsInInt k i then kintegerCilintString k i (Some str) else loop rest | [] -> E.s (E.unimp "Cannot represent the integer %s\n" (string_of_cilint i)) in @@ -6010,8 +6013,7 @@ let mkCastT ~(e: exp) ~(oldt: typ) ~(newt: typ) = TInt(IBool, []), Const(CInt(i, _, _)) -> let v = if compare i zero_cilint = 0 then zero_cilint else one_cilint in Const (CInt(v, IBool, None)) - | TInt(newik, []), Const(CInt(_, _, Some s)) -> kintegerCilint newik (Cilint.cilint_of_string s) - | TInt(newik, []), Const(CInt(i, _, None)) -> kintegerCilint newik i + | TInt(newik, []), Const(CInt(i, _, _)) -> kintegerCilint newik i | _ -> CastE(newt,e) end From fae401bbf4a8c0f20ec5a49d2120421f9111ca35 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Wed, 1 Dec 2021 17:53:24 +0100 Subject: [PATCH 12/15] Rm commented out code --- src/cil.ml | 9 +-------- 1 file changed, 1 insertion(+), 8 deletions(-) diff --git a/src/cil.ml b/src/cil.ml index b93d87b0b..7d1e08b4e 100755 --- a/src/cil.ml +++ b/src/cil.ml @@ -2747,8 +2747,7 @@ let parseInt (str: string) : exp = let t = String.sub str start (String.length str - start - suffixlen) in (* Normal Z.of_string does not work here as 0 is not recognized as the prefix for octal here *) let i = Z.of_string_base base t in - (* Construct an integer of the first kinds that fits. i must be - * POSITIVE *) + (* Construct an integer of the first kinds that fits. i must be POSITIVE *) let res = let rec loop = function | k::rest -> @@ -2759,12 +2758,6 @@ let parseInt (str: string) : exp = loop kinds in res -(* with e -> begin *) -(* ignore (E.log "int_of_string %s (%s)\n" str *) -(* (Printexc.to_string e)); *) -(* zero *) -(* end *) - let d_unop () u = From ca7c9954dd2e49514842fc1a901d2dfe95eb9427 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Thu, 2 Dec 2021 08:05:14 +0100 Subject: [PATCH 13/15] Make parseInt code more ordinary --- src/cil.ml | 23 ++++++++--------------- 1 file changed, 8 insertions(+), 15 deletions(-) diff --git a/src/cil.ml b/src/cil.ml index 7d1e08b4e..3a1871541 100755 --- a/src/cil.ml +++ b/src/cil.ml @@ -2699,11 +2699,10 @@ and isConstantOffset = function | Index(e, off) -> isConstant e && isConstantOffset off let parseInt (str: string) : exp = - let hasSuffix str = + let hasSuffix str suff = let l = String.length str in - fun s -> - let ls = String.length s in - l >= ls && s = String.uppercase_ascii (String.sub str (l - ls) ls) + let lsuff = String.length suff in + l >= lsuff && suff = String.uppercase_ascii (String.sub str (l - lsuff) lsuff) in let l = String.length str in (* See if it is octal or hex *) @@ -2747,17 +2746,11 @@ let parseInt (str: string) : exp = let t = String.sub str start (String.length str - start - suffixlen) in (* Normal Z.of_string does not work here as 0 is not recognized as the prefix for octal here *) let i = Z.of_string_base base t in - (* Construct an integer of the first kinds that fits. i must be POSITIVE *) - let res = - let rec loop = function - | k::rest -> - if fitsInInt k i then kintegerCilintString k i (Some str) - else loop rest - | [] -> E.s (E.unimp "Cannot represent the integer %s\n" (string_of_cilint i)) - in - loop kinds - in - res + try + (* Construct an integer of the first kinds that fits. i must be POSITIVE *) + let ik = List.find (fun ik -> fitsInInt ik i) kinds in + kintegerCilintString ik i (Some str) + with Not_found -> E.s (E.unimp "Cannot represent the integer %s\n" (string_of_cilint i)) let d_unop () u = From 718339bf0e3797f1958cb11d81d62c9167419d66 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Thu, 2 Dec 2021 08:06:08 +0100 Subject: [PATCH 14/15] Change indent --- src/cil.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/cil.ml b/src/cil.ml index 3a1871541..af1243cc6 100755 --- a/src/cil.ml +++ b/src/cil.ml @@ -2750,7 +2750,8 @@ let parseInt (str: string) : exp = (* Construct an integer of the first kinds that fits. i must be POSITIVE *) let ik = List.find (fun ik -> fitsInInt ik i) kinds in kintegerCilintString ik i (Some str) - with Not_found -> E.s (E.unimp "Cannot represent the integer %s\n" (string_of_cilint i)) + with Not_found -> + E.s (E.unimp "Cannot represent the integer %s\n" (string_of_cilint i)) let d_unop () u = From 70662520656375f2a0c71b530a003790d65262c2 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Thu, 2 Dec 2021 08:09:23 +0100 Subject: [PATCH 15/15] Add zarith to merlin file --- .merlin | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.merlin b/.merlin index 286dbbc8a..27b68d5aa 100644 --- a/.merlin +++ b/.merlin @@ -9,4 +9,4 @@ B _build/src/ext/ B _build/src/ext/pta/ B _build/src/frontc/ B _build/src/ocamlutil/ -PKG findlib +PKG findlib, zarith