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 diff --git a/src/check.ml b/src/check.ml index 1b96991c3..4615ab528 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 ignore overflows here *) | None -> ignore (warn "Array length is not a constant"); 0L) @@ -652,10 +652,10 @@ and checkInit (i: init) : typ = if i > len then ignore (warn "Wrong number of initializers in array") - | (Index(Const(CInt64(i', _, _)), NoOffset), ei) :: rest -> - if i' <> i then + | (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" 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 0d6f6e398..c3a456122 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 + | 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. 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,20 +1239,20 @@ 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(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 = 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) + CInt(value, IInt, None) (** Convert a 64-bit int to an OCaml int, or raise an exception if that @@ -1718,8 +1716,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 @@ -1734,8 +1732,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 = @@ -1759,26 +1757,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 ^ "\"") @@ -1902,7 +1900,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 @@ -2078,25 +2076,23 @@ 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 = +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')); - 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 (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 = @@ -2144,7 +2140,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(CInt (n, ik, _)) -> Some (mkCilintIk ik n) | Const(CChr c) -> getInteger (Const (charConstToInt c)) | Const(CEnum(v, _, _)) -> getInteger v | CastE(t, e) -> begin @@ -2408,8 +2404,8 @@ 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 + 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, but this multiplication is the most likely to be a problem. *) @@ -2506,8 +2502,8 @@ and constFold (machdep: bool) (e: exp) : exp = | _ -> raise Not_found (* probably a float *) in match constFold machdep e1 with - Const(CInt64(i,ik,_)) -> begin - let ic = mkCilint ik i in + Const(CInt(i,ik,_)) -> begin + let ic = mkCilintIk ik i in match unop with Neg -> kintegerCilint tk (neg_cilint ic) | BNot -> kintegerCilint tk (lognot_cilint ic) @@ -2553,12 +2549,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 (mkCilint k i) in - Const(CInt64(int64_of_cilint i', nk, None)) + let i', _ = truncateCilint nk (mkCilintIk k i) in + Const(CInt(i', nk, None)) | e', _ -> CastE (t, e') end | Lval lv -> Lval (constFoldLval machdep lv) @@ -2702,11 +2698,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 *) @@ -2738,57 +2733,24 @@ 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 - (* 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 kintegerCilint k i - else loop rest - | [] -> E.s (E.unimp "Cannot represent the integer %s\n" - (string_of_cilint i)) - in - loop kinds - in - res -(* with e -> begin *) -(* ignore (E.log "int_of_string %s (%s)\n" str *) -(* (Printexc.to_string e)); *) -(* zero *) -(* end *) - + 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 + 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 = @@ -3507,21 +3469,21 @@ 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,_,_)),_) - when Util.equals lv lv' && one = Int64.one && not !printCilAsIs -> + 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,_,_)), _) - when Util.equals lv lv' && one = Int64.one && not !printCilAsIs -> + 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,_,_)),_) - when Util.equals lv lv' && mone = Int64.minus_one + | 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 ++ self#pLvalPrec indexLevel () lv @@ -4602,10 +4564,10 @@ 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)" - (Int64.format fmt i) + dprintf "Int(%s,%a,%s)" + (Z.format fmt i) d_ikind ik (match so with Some s -> s | _ -> "None") | CStr(s) -> @@ -4806,7 +4768,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@])" @@ -5802,8 +5764,8 @@ 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,_)) -> - let i' = mkCilint k i in + Const(CInt(i,k,_)) -> + let i' = mkCilintIk k i in if not (is_int_cilint i') then raise (NotAnAttrParam e); AInt (int_of_cilint i') @@ -5920,7 +5882,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 @@ -6034,11 +5996,10 @@ 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, _, _)) -> - let v = if i = Int64.zero then Int64.zero else Int64.one 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(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(i, _, _)) -> kintegerCilint newik i | _ -> CastE(newt,e) end @@ -6091,8 +6052,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(CInt(ni, _, _)) when compare_cilint ni zero_cilint >= 0 -> + cilint_to_int ni | e -> raise LenOfArray end @@ -6100,7 +6061,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(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 -> @@ -6144,7 +6105,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(CInt(n, _, _)) -> cilint_to_int n | _ -> E.s (E.unimp "Cannot understand length of array") in let initbt = makeZeroInit bt in @@ -6187,8 +6148,8 @@ let foldLeftCompound match leno with Some lene when implicit -> begin match constFold true lene with - Const(CInt64(i, _, _)) -> - let len_array = i64_to_int i in + Const(CInt(i, _, _)) -> + 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 @@ -6483,8 +6444,8 @@ 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, _)) -> - mkCilint ilk il, mkCilint ihk ih, commonIntKind ilk 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 if compare_cilint il ih > 0 then @@ -6932,94 +6893,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..7ad9548e3 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 + | 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 - * {!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 @@ -1648,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 @@ -2566,10 +2565,12 @@ 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 +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 1b7e5de6f..eaa8b3e35 100644 --- a/src/cilint.ml +++ b/src/cilint.ml @@ -10,24 +10,16 @@ 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 -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 +let mone_cilint = minus_big_int unit_big_int (* Precompute useful big_ints *) let b30 = power_int_positive_int 2 30 @@ -37,232 +29,126 @@ 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 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)) - -(* 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 big_int_of_cilint (c:cilint) : big_int = c +let cilint_of_big_int (b:big_int) : cilint = b -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 = - 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 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 is_zero_cilint (c:cilint) : bool = - match c with - | Small i -> i = 0 - | Big b -> sign_big_int b = 0 +let compare_cilint = compare_big_int +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 = big_int_of_int +let int_of_cilint = int_of_big_int -let int_of_cilint (c:cilint) : int = - match c with - | Small i -> i - | Big b -> int_of_big_int b - -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 - 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 Big (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. *) -let int64_of_cilint (c:cilint) : int64 = - match c with - | Small i -> Int64.of_int i - | Big b -> - 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) - -let string_of_cilint (c:cilint) : string = - match c with - | Small i -> string_of_int i - | Big b -> string_of_big_int b +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 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) = - 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) - else - Big (pred_big_int q) - else - Big q + 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 = - 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 = - 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 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 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 = - 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 = 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 = - 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 + let max = power_int_positive_int 2 (n - 1) in + let truncmax = power_int_positive_int 2 n in + let bits = mod_big_int c truncmax in + let tval = if lt_big_int bits max then + bits 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 - 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 - else - ValueTruncation - else - NoTruncation - in cilint_of_big_int tval, trunc + sub_big_int bits truncmax + in + let trunc = + 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 + 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 - 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 max = power_int_positive_int 2 (n - 1) in + let truncmax = power_int_positive_int 2 n in + let bits = mod_big_int c truncmax in + let trunc = + 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 - ValueTruncation - else - NoTruncation - in cilint_of_big_int bits, trunc + NoTruncation + in + 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..d142b3baf 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 @@ -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..4af909fc6 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(CInt(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(CInt(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..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,8 +551,8 @@ constant: | a -> wrongArgType currentArg "integer" a), fun e -> match e with - Const(CInt64(n, _, _)) -> - Some [ Fd (Int64.to_int 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 b5e45a161..6fd0463c2 100644 --- a/src/frontc/cabs2cil.ml +++ b/src/frontc/cabs2cil.ml @@ -222,23 +222,23 @@ 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 - (CInt64(value,IULong,orig_rep)),(TInt(IULong,[])) + if compare_cilint value (cilint_of_int64 (Int64.of_int32 Int32.max_int)) <= 0 then + (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,_,_)) -> n <> Int64.zero + | 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,_,_)) -> n = Int64.zero + | 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) -> i64_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,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(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" d_exp len) @@ -2735,8 +2735,8 @@ 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,_,_)) -> - AInt (i64_to_int v64) + Const (CInt (v64,_,_)) -> + AInt (cilint_to_int v64) | _ -> E.s (error "Invalid attribute constant: %s") end @@ -2920,9 +2920,9 @@ 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 = 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 @@ -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 @@ -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(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 (0L,_,_)) | Const (CInt64 (1L,_,_)) -> + | Const (CInt (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 (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 i <> Int64.zero && canDrop sf -> se @@ st - | Const(CInt64(z,_,_)) when z = Int64.zero && 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 -> i64_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,9 +5441,9 @@ 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, _, _)) -> - i64_to_int s, i64_to_int 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") 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(CInt(ni, _, _)) when compare_cilint ni zero_cilint >= 0 -> (* Write any initializations in initl using one instruction per element. *) let b = foldLeftCompound @@ -6389,24 +6389,24 @@ 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(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(1L, 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 3198e49e3..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(CInt64(oldi, _, _)), Const(CInt64(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(CInt64(oldi, _, _)), Const(CInt64(i, _, _)) -> oldi = i + Const(CInt(oldi, _, _)), Const(CInt(i, _, _)) -> Cilint.compare_cilint oldi i = 0 | _ -> false in if not samev then @@ -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 *) + | 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)