Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
22 changes: 11 additions & 11 deletions src/cdomain/value/cdomains/int/bitfieldDomain.ml
Original file line number Diff line number Diff line change
Expand Up @@ -253,7 +253,7 @@ module BitfieldFunctor (Ints_t : IntOps.IntOps): Bitfield_SOverflow with type in
let newo = o &: (Ints_t.of_bigint max_ik) in
(newz,newo)

let norm ?(suppress_ovwarn=false) ?(ov=false) ik (z,o) =
let norm ?(ov=false) ik (z,o) =
if BArith.is_invalid (z,o) then
bot ()
else
Expand All @@ -263,7 +263,7 @@ module BitfieldFunctor (Ints_t : IntOps.IntOps): Bitfield_SOverflow with type in
else
top_of ik

let cast_to ?(suppress_ovwarn=false) ?torg ?(no_ov=false) ik (z,o) =
let cast_to ?torg ?(no_ov=false) ik (z,o) =
let (min_ik, max_ik) = Size.range ik in
let (underflow, overflow) = match torg with
| None -> (false, false) (* ik does not change *)
Expand All @@ -278,10 +278,10 @@ module BitfieldFunctor (Ints_t : IntOps.IntOps): Bitfield_SOverflow with type in
let overflow = (((!:(Ints_t.of_bigint max_ik)) &: o) <>: Ints_t.zero) && isPos in
(underflow, overflow)
in
let overflow_info = if suppress_ovwarn then {underflow=false; overflow=false} else {underflow=underflow; overflow=overflow} in
(norm ~suppress_ovwarn:(suppress_ovwarn) ~ov:(underflow || overflow) ik (z,o), overflow_info)
let overflow_info = {underflow; overflow} in
(norm ~ov:(underflow || overflow) ik (z,o), overflow_info)

let cast_to ?(suppress_ovwarn=false) ?torg ?(no_ov=false) ik (z,o) =
let cast_to ?torg ?(no_ov=false) ik (z,o) =
if ik = GoblintCil.IBool then (
let may_zero =
if Ints_t.equal z BArith.one_mask then (* zero bit may be in every position (one_mask) *)
Expand All @@ -298,7 +298,7 @@ module BitfieldFunctor (Ints_t : IntOps.IntOps): Bitfield_SOverflow with type in
(BArith.join may_zero may_one, {underflow=false; overflow=false})
)
else
cast_to ~suppress_ovwarn ?torg ~no_ov ik (z,o)
cast_to ?torg ~no_ov ik (z,o)

let join ik b1 b2 = norm ik @@ (BArith.join b1 b2)

Expand Down Expand Up @@ -335,7 +335,7 @@ module BitfieldFunctor (Ints_t : IntOps.IntOps): Bitfield_SOverflow with type in

type bit_status = Zero | One | Top

let of_interval ?(suppress_ovwarn=false) ik (x,y) =
let of_interval ik (x,y) =
let (min_ik, max_ik) = Size.range ik in
let startv = Ints_t.max x (Ints_t.of_bigint min_ik) in
let endv= Ints_t.min y (Ints_t.of_bigint max_ik) in
Expand Down Expand Up @@ -638,13 +638,13 @@ module BitfieldFunctor (Ints_t : IntOps.IntOps): Bitfield_SOverflow with type in
let exp1 = Invariant.of_exp (BinOp (Eq, (BinOp (BAnd, e, def1, TInt(ik,[]))), def1, intType)) in
Invariant.meet exp0 exp1

let starting ?(suppress_ovwarn=false) ik n =
let starting ik n =
let (min_ik, max_ik) = Size.range ik in
of_interval ~suppress_ovwarn ik (n, Ints_t.of_bigint max_ik)
of_interval ik (n, Ints_t.of_bigint max_ik)

let ending ?(suppress_ovwarn=false) ik n =
let ending ik n =
let (min_ik, max_ik) = Size.range ik in
of_interval ~suppress_ovwarn ik (Ints_t.of_bigint min_ik, n)
of_interval ik (Ints_t.of_bigint min_ik, n)

(* Refinements *)

Expand Down
3 changes: 2 additions & 1 deletion src/cdomain/value/cdomains/int/congruenceDomain.ml
Original file line number Diff line number Diff line change
Expand Up @@ -133,9 +133,10 @@ struct
| x when equal zero x -> Some false
| x -> if leq zero x then None else Some true

let starting ?(suppress_ovwarn=false) ik n = top()
let starting ik n = top()

let ending = starting
let of_interval ik x = of_interval ik x (* cast away optional suppress_ovwarn argument *)

let of_congruence ik (c,m) = normalize ik @@ Some(c,m)

Expand Down
12 changes: 6 additions & 6 deletions src/cdomain/value/cdomains/int/defExcDomain.ml
Original file line number Diff line number Diff line change
Expand Up @@ -298,12 +298,12 @@ struct
| _ -> None
let top_bool = `Excluded (S.empty (), R.of_interval range_ikind (0L, 1L))

let of_interval ?(suppress_ovwarn=false) ik (x,y) =
let of_interval ik (x,y) =
if Z.compare x y = 0 then
of_int ik x
else
let a, b = Size.min_range_sign_agnostic x, Size.min_range_sign_agnostic y in
let r = R.join (R.of_interval ~suppress_ovwarn range_ikind a) (R.of_interval ~suppress_ovwarn range_ikind b) in
let r = R.join (R.of_interval range_ikind a) (R.of_interval range_ikind b) in
let ex = if Z.gt x Z.zero || Z.lt y Z.zero then S.singleton Z.zero else S.empty () in
norm ik @@ (`Excluded (ex, r))

Expand All @@ -318,13 +318,13 @@ struct
let ik_mask = snd (Size.range ik) in
(one_mask, ik_mask)

let starting ?(suppress_ovwarn=false) ikind x =
let starting ikind x =
let _,u_ik = Size.range ikind in
of_interval ~suppress_ovwarn ikind (x, u_ik)
of_interval ikind (x, u_ik)

let ending ?(suppress_ovwarn=false) ikind x =
let ending ikind x =
let l_ik,_ = Size.range ikind in
of_interval ~suppress_ovwarn ikind (l_ik, x)
of_interval ikind (l_ik, x)

let of_excl_list t l =
let r = size t in (* elements in l are excluded from the full range of t! *)
Expand Down
12 changes: 6 additions & 6 deletions src/cdomain/value/cdomains/int/enumsDomain.ml
Original file line number Diff line number Diff line change
Expand Up @@ -119,12 +119,12 @@ module Enums : S with type int_t = Z.t = struct

let of_int ikind x = cast_to ikind (Inc (BISet.singleton x))

let of_interval ?(suppress_ovwarn=false) ik (x, y) =
let of_interval ik (x, y) =
if Z.compare x y = 0 then
of_int ik x
else
let a, b = Size.min_range_sign_agnostic x, Size.min_range_sign_agnostic y in
let r = R.join (R.of_interval ~suppress_ovwarn range_ikind a) (R.of_interval ~suppress_ovwarn range_ikind b) in
let r = R.join (R.of_interval range_ikind a) (R.of_interval range_ikind b) in
let ex = if Z.gt x Z.zero || Z.lt y Z.zero then BISet.singleton Z.zero else BISet.empty () in
norm ik @@ (Exc (ex, r))

Expand Down Expand Up @@ -380,13 +380,13 @@ module Enums : S with type int_t = Z.t = struct
| _ when Cil.isSigned ik -> (one_mask, one_mask)
| _ -> (one_mask, ik_mask)

let starting ?(suppress_ovwarn=false) ikind x =
let starting ikind x =
let _,u_ik = Size.range ikind in
of_interval ~suppress_ovwarn ikind (x, u_ik)
of_interval ikind (x, u_ik)

let ending ?(suppress_ovwarn=false) ikind x =
let ending ikind x =
let l_ik,_ = Size.range ikind in
of_interval ~suppress_ovwarn ikind (l_ik, x)
of_interval ikind (l_ik, x)

let c_lognot ik x =
if is_bot x
Expand Down
14 changes: 7 additions & 7 deletions src/cdomain/value/cdomains/int/intDomTuple.ml
Original file line number Diff line number Diff line change
Expand Up @@ -76,17 +76,17 @@ module IntDomTupleImpl = struct
);
no_ov

let create2_ovc ik r x ((p1, p2, p3, p4, p5, p6): int_precision) =
let create2_ovc ?(suppress_ovwarn = false) ik r x ((p1, p2, p3, p4, p5, p6): int_precision) =
let f b g = if b then Some (g x) else None in
let map x = Option.map fst x in
let intv = f p2 @@ r.fi2_ovc (module I2) in
let intv_set = f p5 @@ r.fi2_ovc (module I5) in
let bf = f p6 @@ r.fi2_ovc (module I6) in
ignore (check_ov ~cast:false ik intv intv_set bf);
ignore (check_ov ~suppress_ovwarn ~cast:false ik intv intv_set bf);
map @@ f p1 @@ r.fi2_ovc (module I1), map @@ f p2 @@ r.fi2_ovc (module I2), map @@ f p3 @@ r.fi2_ovc (module I3), map @@ f p4 @@ r.fi2_ovc (module I4), map @@ f p5 @@ r.fi2_ovc (module I5) , map @@ f p6 @@ r.fi2_ovc (module I6)

let create2_ovc ik r x = (* use where values are introduced *)
create2_ovc ik r x (int_precision_from_node_or_config ())
let create2_ovc ?(suppress_ovwarn = false) ik r x = (* use where values are introduced *)
create2_ovc ~suppress_ovwarn ik r x (int_precision_from_node_or_config ())


let opt_map2 f ?no_ov =
Expand Down Expand Up @@ -120,9 +120,9 @@ module IntDomTupleImpl = struct
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 starting ?(suppress_ovwarn=false) ik = create2_ovc ik { fi2_ovc = fun (type a) (module I:SOverflow with type t = a and type int_t = int_t) -> I.starting ~suppress_ovwarn ik }
let ending ?(suppress_ovwarn=false) ik = create2_ovc ik { fi2_ovc = fun (type a) (module I:SOverflow with type t = a and type int_t = int_t) -> I.ending ~suppress_ovwarn ik }
let of_interval ?(suppress_ovwarn=false) ik = create2_ovc ik { fi2_ovc = fun (type a) (module I:SOverflow with type t = a and type int_t = int_t) -> I.of_interval ~suppress_ovwarn 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 }
let of_congruence ik = create2 { fi2 = fun (type a) (module I:SOverflow with type t = a and type int_t = int_t) -> I.of_congruence ik }
let of_bitfield ik = create2 { fi2 = fun (type a) (module I:SOverflow with type t = a and type int_t = int_t) -> I.of_bitfield ik }

Expand Down
18 changes: 9 additions & 9 deletions src/cdomain/value/cdomains/int/intervalDomain.ml
Original file line number Diff line number Diff line change
Expand Up @@ -32,14 +32,14 @@ struct
| Some (a, b) ->
if a = b && b = i then `Eq else if Ints_t.compare a i <= 0 && Ints_t.compare i b <=0 then `Top else `Neq

let norm ?(suppress_ovwarn=false) ?(cast=false) ik : (t -> t * overflow_info) = function None -> (None, {underflow=false; overflow=false}) | Some (x,y) ->
let norm ?(cast=false) ik : (t -> t * overflow_info) = function None -> (None, {underflow=false; overflow=false}) | Some (x,y) ->
if Ints_t.compare x y > 0 then
(None,{underflow=false; overflow=false})
else (
let (min_ik, max_ik) = range ik in
let underflow = Ints_t.compare min_ik x > 0 in
let overflow = Ints_t.compare max_ik y < 0 in
let ov_info = { underflow = underflow && not suppress_ovwarn; overflow = overflow && not suppress_ovwarn } in
let ov_info = { underflow; overflow } in
let v =
if underflow || overflow then
if should_wrap ik then (* could add [|| cast], but that's GCC implementation-defined behavior: https://gcc.gnu.org/onlinedocs/gcc/Integers-implementation.html#Integers-implementation *)
Expand Down Expand Up @@ -88,7 +88,7 @@ struct

(* TODO: change to_int signature so it returns a big_int *)
let to_int x = Option.bind x (IArith.to_int)
let of_interval ?(suppress_ovwarn=false) ik (x,y) = norm ~suppress_ovwarn ik @@ Some (x,y)
let of_interval ik (x,y) = norm ik @@ Some (x,y)

let of_bitfield ik x =
let min ik (z,o) =
Expand Down Expand Up @@ -129,17 +129,17 @@ struct
| Some (l, u) when Ints_t.compare l Ints_t.zero = 0 && Ints_t.compare u Ints_t.zero = 0 -> Some false
| x -> if leq zero x then None else Some true

let starting ?(suppress_ovwarn=false) ik n =
norm ~suppress_ovwarn ik @@ Some (n, snd (range ik))
let starting ik n =
norm ik @@ Some (n, snd (range ik))

let ending ?(suppress_ovwarn=false) ik n =
norm ~suppress_ovwarn ik @@ Some (fst (range ik), n)
let ending ik n =
norm ik @@ Some (fst (range ik), n)

(* TODO: change signature of maximal, minimal to return big_int*)
let maximal = function None -> None | Some (x,y) -> Some y
let minimal = function None -> None | Some (x,y) -> Some x

let cast_to ?(suppress_ovwarn=false) ?torg ?no_ov t = norm ~cast:true t (* norm does all overflow handling *)
let cast_to ?torg ?no_ov t = norm ~cast:true t (* norm does all overflow handling *)

let widen ik x y =
match x, y with
Expand Down Expand Up @@ -524,7 +524,7 @@ struct
let l' = if Ints_t.equal l min_ik then l else shrink Ints_t.add l in
let u' = if Ints_t.equal u max_ik then u else shrink Ints_t.sub u in
let intv' = norm ik @@ Some (l', u') |> fst in
let range = norm ~suppress_ovwarn:true ik (Some (Ints_t.of_bigint (Size.min_from_bit_range rl), Ints_t.of_bigint (Size.max_from_bit_range rh))) |> fst in
let range = norm ik (Some (Ints_t.of_bigint (Size.min_from_bit_range rl), Ints_t.of_bigint (Size.max_from_bit_range rh))) |> fst in
meet ik intv' range

let refine_with_incl_list ik (intv: t) (incl : (int_t list) option) : t =
Expand Down
18 changes: 9 additions & 9 deletions src/cdomain/value/cdomains/int/intervalSetDomain.ml
Original file line number Diff line number Diff line change
Expand Up @@ -141,7 +141,7 @@ struct
| ys when List.for_all ((=) `Neq) ys -> `Neq
| _ -> `Top

let norm_interval ?(suppress_ovwarn=false) ?(cast=false) ik (x,y) : t*overflow_info =
let norm_interval ?(cast=false) ik (x,y) : t*overflow_info =
if x >. y then
([],{underflow=false; overflow=false})
else
Expand Down Expand Up @@ -173,10 +173,10 @@ struct
else
[(x,y)]
in
if suppress_ovwarn then (v, {underflow=false; overflow=false}) else (v, {underflow; overflow})
(v, {underflow; overflow})

let norm_intvs ?(suppress_ovwarn=false) ?(cast=false) (ik:ikind) (xs: t) : t*overflow_info =
let res = List.map (norm_interval ~suppress_ovwarn ~cast ik) xs in
let norm_intvs ?(cast=false) (ik:ikind) (xs: t) : t*overflow_info =
let res = List.map (norm_interval ~cast ik) xs in
let intvs = List.concat_map fst res in
let underflow = List.exists (fun (_,{underflow; _}) -> underflow) res in
let overflow = List.exists (fun (_,{overflow; _}) -> overflow) res in
Expand Down Expand Up @@ -249,7 +249,7 @@ struct

let of_bool _ = function true -> one | false -> zero

let of_interval ?(suppress_ovwarn=false) ik (x,y) = norm_interval ~suppress_ovwarn ~cast:false ik (x,y)
let of_interval ik (x,y) = norm_interval ~cast:false ik (x,y)

let of_bitfield ik x =
match Interval.of_bitfield ik x with
Expand Down Expand Up @@ -484,7 +484,7 @@ struct
in
binop x y interval_rem

let cast_to ?(suppress_ovwarn=false) ?torg ?no_ov ik x = norm_intvs ~cast:true ik x
let cast_to ?torg ?no_ov ik x = norm_intvs ~cast:true ik x

(*
narrows down the extremeties of xs if they are equal to boundary values of the ikind with (possibly) narrower values from ys
Expand Down Expand Up @@ -572,9 +572,9 @@ struct
in
interval_sets_to_partitions ik xs ys |> merge_list ik |> widen_left |> widen_right |> List.map snd

let starting ?(suppress_ovwarn=false) ik n = norm_interval ik ~suppress_ovwarn (n, snd (range ik))
let starting ik n = norm_interval ik (n, snd (range ik))

let ending ?(suppress_ovwarn=false) ik n = norm_interval ik ~suppress_ovwarn (fst (range ik), n)
let ending ik n = norm_interval ik (fst (range ik), n)

let invariant_ikind e ik xs =
List.map (fun x -> Interval.invariant_ikind e ik (Some x)) xs |>
Expand Down Expand Up @@ -620,7 +620,7 @@ struct
let excl_range_to_intervalset (ik: ikind) ((min, max): int_t * int_t) (excl: int_t): t =
let intv1 = (min, excl -. Ints_t.one) in
let intv2 = (excl +. Ints_t.one, max) in
norm_intvs ik ~suppress_ovwarn:true [intv1 ; intv2] |> fst
norm_intvs ik [intv1 ; intv2] |> fst

let of_excl_list ik (excls: int_t list) =
let excl_list = List.map (excl_range_to_intervalset ik (range ik)) excls in
Expand Down
20 changes: 10 additions & 10 deletions src/cdomain/value/cdomains/intDomain0.ml
Original file line number Diff line number Diff line change
Expand Up @@ -110,7 +110,7 @@ sig
end


module IntDomLifter (I : S) =
module IntDomLifter (I : S2) =
struct
open Cil
type int_t = I.int_t
Expand Down Expand Up @@ -477,7 +477,7 @@ struct
) (Invariant.top ()) ns
end

module SOverflowUnlifter (D : SOverflow) : S with type int_t = D.int_t and type t = D.t = struct
module SOverflowUnlifter (D : SOverflow) : S2 with type int_t = D.int_t and type t = D.t = struct
include D

let add ?no_ov ik x y = fst @@ D.add ?no_ov ik x y
Expand All @@ -490,15 +490,15 @@ module SOverflowUnlifter (D : SOverflow) : S with type int_t = D.int_t and type

let neg ?no_ov ik x = fst @@ D.neg ?no_ov ik x

let cast_to ?suppress_ovwarn ?torg ?no_ov ik x = fst @@ D.cast_to ?suppress_ovwarn ?torg ?no_ov ik x
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_interval ?suppress_ovwarn ik x = fst @@ D.of_interval ?suppress_ovwarn ik x
let of_interval ?suppress_ovwarn ik x = fst @@ D.of_interval ik x

let starting ?suppress_ovwarn ik x = fst @@ D.starting ?suppress_ovwarn ik x
let starting ?suppress_ovwarn ik x = fst @@ D.starting ik x

let ending ?suppress_ovwarn ik x = fst @@ D.ending ?suppress_ovwarn ik x
let ending ?suppress_ovwarn ik x = fst @@ D.ending ik x

let shift_left ik x y = fst @@ D.shift_left ik x y

Expand Down Expand Up @@ -742,15 +742,15 @@ module SOverflowLifter (D : S) : SOverflow with type int_t = D.int_t and type t

let neg ?no_ov ik x = lift @@ D.neg ?no_ov ik x

let cast_to ?suppress_ovwarn ?torg ?no_ov ik x = lift @@ D.cast_to ?suppress_ovwarn ?torg ?no_ov ik x
let cast_to ?torg ?no_ov ik x = lift @@ D.cast_to ?torg ?no_ov ik x

let of_int ik x = lift @@ D.of_int ik x

let of_interval ?suppress_ovwarn ik x = lift @@ D.of_interval ?suppress_ovwarn ik x
let of_interval ik x = lift @@ D.of_interval ik x

let starting ?suppress_ovwarn ik x = lift @@ D.starting ?suppress_ovwarn ik x
let starting ik x = lift @@ D.starting ik x

let ending ?suppress_ovwarn ik x = lift @@ D.ending ?suppress_ovwarn ik x
let ending ik x = lift @@ D.ending ik x

let shift_left ik x y = lift @@ D.shift_left ik x y

Expand Down
Loading
Loading