Merge pull request #1794 from goblint/create2-check_ov

Remove overflow checks for integer constants

Author: sim642

src/analyses/base.ml

@@ -803,9 +803,7 @@ struct
       (* Integer literals *)
       (* seems like constFold already converts CChr to CInt *)
       | Const (CChr x) -> eval_rv ~man st (Const (charConstToInt x)) (* char becomes int, see Cil doc/ISO C 6.4.4.4.10 *)
-      | Const (CInt (num,ikind,str)) ->
-        GobOption.iter (fun x -> if M.tracing then M.tracel "casto" "CInt (%s, %a, %s)" (Z.to_string num) d_ikind ikind x) str;
-        Int (ID.cast_to ikind (IntDomain.of_const (num,ikind,str)))
+      | Const (CInt (num,ikind,str)) -> Int (IntDomain.of_const (num,ikind,str)) (* no cast to ikind needed: CIL ensures that the literal fits ikind, either by silently truncating it (!) or having an explicit CastE around this *)
       | Const (CReal (_,fkind, Some str)) when not (Cilfacade.isComplexFKind fkind) -> Float (FD.of_string fkind str) (* prefer parsing from string due to higher precision *)
       | Const (CReal (num, fkind, None)) when not (Cilfacade.isComplexFKind fkind) && num = 0.0 -> Float (FD.of_const fkind num) (* constant 0 is ok, CIL creates these for zero-initializers; it is safe across float types *)
       | Const (CReal (_, fkind, None)) when not (Cilfacade.isComplexFKind fkind) ->  assert false (* Cil does not create other CReal without string representation *)

src/cdomain/value/cdomains/int/intDomTuple.ml

@@ -119,7 +119,7 @@ module IntDomTupleImpl = struct
   let bot_of = create { fi = fun (type a) (module I:SOverflow with type t = a) -> I.bot_of }
   let of_bool ik = create { fi = fun (type a) (module I:SOverflow with type t = a) -> I.of_bool ik }
   let of_excl_list ik = create2 { fi2 = fun (type a) (module I:SOverflow with type t = a and type int_t = int_t) -> I.of_excl_list ik}
-  let of_int ik = create2_ovc ik { fi2_ovc = fun (type a) (module I:SOverflow with type t = a and type int_t = int_t) -> I.of_int ik }
+  let of_int ?(suppress_ovwarn=false) ik = create2_ovc ~suppress_ovwarn ik { fi2_ovc = fun (type a) (module I:SOverflow with type t = a and type int_t = int_t) -> I.of_int ik }
   let starting ?(suppress_ovwarn=false) ik = create2_ovc ~suppress_ovwarn ik { fi2_ovc = fun (type a) (module I:SOverflow with type t = a and type int_t = int_t) -> I.starting ik }
   let ending ?(suppress_ovwarn=false) ik = create2_ovc ~suppress_ovwarn ik { fi2_ovc = fun (type a) (module I:SOverflow with type t = a and type int_t = int_t) -> I.ending ik }
   let of_interval ?(suppress_ovwarn=false) ik = create2_ovc ~suppress_ovwarn ik { fi2_ovc = fun (type a) (module I:SOverflow with type t = a and type int_t = int_t) -> I.of_interval ik }
@@ -558,4 +558,4 @@ struct
   let no_bitfield (x: I.t) = {x with v = IntDomTupleImpl.no_bitfield x.v}
 end
 
-let of_const (i, ik, str) = IntDomTuple.of_int ik i
+let of_const (i, ik, str) = IntDomTuple.of_int ~suppress_ovwarn:true ik i

src/cdomain/value/cdomains/intDomain0.ml

@@ -166,7 +166,7 @@ struct
   let tag x = I.tag x.v
   let arbitrary ik = failwith @@ "Arbitrary not implement for " ^ (name ()) ^ "."
   let to_int x = I.to_int x.v
-  let of_int ikind x = { v = I.of_int ikind x; ikind}
+  let of_int ?(suppress_ovwarn=false) ikind x = { v = I.of_int ~suppress_ovwarn ikind x; ikind}
   let equal_to i x = I.equal_to i x.v
   let to_bool x = I.to_bool x.v
   let of_bool ikind b = { v = I.of_bool ikind b; ikind}
@@ -511,7 +511,7 @@ module SOverflowUnlifter (D : SOverflow) : S2 with type int_t = D.int_t and type
 
   let cast_to ?suppress_ovwarn ?torg ?no_ov ik x = fst @@ D.cast_to ?torg ?no_ov ik x
 
-  let of_int ik x = fst @@ D.of_int ik x
+  let of_int ?suppress_ovwarn ik x = fst @@ D.of_int ik x
 
   let of_interval ?suppress_ovwarn ik x = fst @@ D.of_interval ik x
 

src/cdomain/value/cdomains/intDomain_intf.ml

@@ -279,6 +279,7 @@ module type S2 =
 sig
   include S
 
+  val of_int: ?suppress_ovwarn:bool -> Cil.ikind -> int_t -> t
   val starting : ?suppress_ovwarn:bool -> Cil.ikind -> int_t -> t
   val ending : ?suppress_ovwarn:bool -> Cil.ikind -> int_t -> t
   val of_interval: ?suppress_ovwarn:bool -> Cil.ikind -> int_t * int_t -> t
@@ -321,7 +322,7 @@ sig
   include Lattice.Top with type t := t
   include Arith with type t:=t
 
-  val of_int: Cil.ikind -> int_t -> t
+  val of_int: ?suppress_ovwarn:bool -> Cil.ikind -> int_t -> t
   (** Transform an integer literal to your internal domain representation with the specified ikind. *)
 
   val of_bool: Cil.ikind -> bool -> t

src/cdomains/unionFind.ml

@@ -226,7 +226,7 @@ module T = struct
   let offset_to_index ?typ offset =
     let ptr_diff_ikind = Cilfacade.ptrdiff_ikind () in
     let offset_in_bytes = PreValueDomain.Offs.to_index ?typ offset in
-    let bytes_to_bits = IntDomain.of_const (Z.of_int 8, ptr_diff_ikind, None) in
+    let bytes_to_bits = IntDomain.IntDomTuple.of_int  ptr_diff_ikind (Z.of_int 8) in
     IntDomain.IntDomTuple.mul bytes_to_bits offset_in_bytes
 
   (** Convert a Cil offset to an integer offset. *)

src/domains/intDomainProperties.ml

@@ -29,6 +29,7 @@ module MakeS2 (I: S): S2 =
 struct
   include I
 
+  let of_int ?suppress_ovwarn ik x = of_int ik x
   let starting ?suppress_ovwarn ik x = starting ik x
   let ending ?suppress_ovwarn ik x = ending ik x
   let of_interval ?suppress_ovwarn ik x = of_interval ik x